1 (* ========================================================================= *)
\r
2 (* FLYSPECK - BOOK FORMALIZATION *)
\r
4 (* Authour : VU KHAC KY *)
\r
6 (* Chaper : Packing (Marchal Cells 2) *)
\r
7 (* Date : October 3, 2010 *)
\r
9 (* ========================================================================= *)
\r
11 #use "/usr/programs/hollight/hollight-svn75/hol.ml";;
\r
12 loads "Multivariate/flyspeck.ml";;
\r
13 #use "/home/ky/flyspeck/working/boot.hl";;
\r
14 flyspeck_needs "trigonometry/trig1.hl";;
\r
15 flyspeck_needs "trigonometry/trig2.hl";;
\r
16 flyspeck_needs "trigonometry/trigonometry.hl";;
\r
18 (* ================= Loaded files ======================================== *)
\r
20 flyspeck_needs "leg/collect_geom.hl";;
\r
21 flyspeck_needs "fan/fan_defs.hl";;
\r
22 flyspeck_needs "fan/introduction.hl";;
\r
23 flyspeck_needs "fan/topology.hl";;
\r
24 flyspeck_needs "fan/fan_misc.hl";;
\r
25 flyspeck_needs "fan/HypermapAndFan.hl";;
\r
26 flyspeck_needs "packing/pack_defs.hl";;
\r
27 flyspeck_needs "packing/pack_concl.hl";;
\r
28 flyspeck_needs "packing/pack1.hl";;
\r
29 flyspeck_needs "packing/pack2.hl";;
\r
30 flyspeck_needs "packing/pack3.hl";;
\r
31 flyspeck_needs "packing/Rogers.hl";;
\r
32 flyspeck_needs "nonlinear/vukhacky_tactics.hl";;
\r
35 (* ====================== Open appropriate files ======================= *)
\r
37 module Marchal_cells_2 = struct
\r
41 open Prove_by_refinement;;
\r
42 open Vukhacky_tactics;;
\r
47 flyspeck_needs "packing/marchal_cells.hl";;
\r
48 open Marchal_cells;;
\r
49 flyspeck_needs "packing/EMNWUUS.hl";;
\r
53 let (tms,tm) = top_goal () in
\r
54 let vss = map frees (tm::tms) in
\r
55 let vs = setify (flat vss) in
\r
59 (* ======================================================================= *)
\r
61 let AFF_GE_2_2 = prove
\r
63 DISJOINT {x,v} {w,z}
\r
64 ==> aff_ge {x,v} {w, z} =
\r
66 &0 <= t3 /\ &0 <= t4 /\
\r
67 t1 + t2 + t3 + t4 = &1 /\
\r
68 y = t1 % x + t2 % v + t3 % w + t4 % z}`,
\r
70 (* ======================================================================= *)
\r
72 let MEASURABLE_ROGERS = prove_by_refinement (
\r
73 `!V (ul:(real^3)list) k.
\r
74 saturated V /\ packing V /\ barV V 3 ul ==> measurable (rogers V ul)`,
\r
75 [ (REPEAT STRIP_TAC);
\r
76 (REWRITE_TAC[ROGERS]);
\r
77 (MATCH_MP_TAC MEASURABLE_CONVEX_HULL);
\r
78 (MATCH_MP_TAC FINITE_IMP_BOUNDED);
\r
79 (MATCH_MP_TAC FINITE_IMAGE);
\r
80 (SUBGOAL_THEN `? u0 u1 u2 u3. (ul:(real^3)list) = [u0:real^3;u1;u2;u3]` CHOOSE_TAC);
\r
81 (MP_TAC (ASSUME `barV V 3 ul`));
\r
82 (REWRITE_TAC[BARV_3_EXPLICIT]);
\r
83 (FIRST_X_ASSUM CHOOSE_TAC);
\r
84 (FIRST_X_ASSUM CHOOSE_TAC);
\r
85 (FIRST_X_ASSUM CHOOSE_TAC);
\r
86 (NEW_GOAL `LENGTH (ul:(real^3)list) = 4`);
\r
87 (ASM_REWRITE_TAC[LENGTH]);
\r
89 (ASM_REWRITE_TAC[]);
\r
90 (REWRITE_TAC[FINITE_NUMSEG_LT])]);;
\r
92 (* ======================================================================= *)
\r
94 let CONVEX_RCONE_GE = prove_by_refinement (
\r
95 `!a:real^N b r. &0 <= r ==> convex (rcone_ge a b r)`,
\r
96 [ (REPEAT STRIP_TAC);
\r
97 (REWRITE_TAC[rcone_ge;convex;rconesgn;IN;IN_ELIM_THM]);
\r
99 (REWRITE_WITH `(u % x + v % y) - a = u % (x - a) + v % (y - a:real^N)`);
\r
100 (ASM_REWRITE_TAC[VECTOR_SUB_LDISTRIB; VECTOR_MUL_LID;
\r
101 VECTOR_ARITH `a - x % b + c - y % b = (a + c) - (x + y) % b`]);
\r
102 (REWRITE_TAC[DOT_LADD;DOT_LMUL]);
\r
103 (ASM_CASES_TAC `&0 < u`);
\r
108 `u * ((x:real^N - a) dot (b - a)) + v * ((y - a) dot (b - a)) >=
\r
109 u * dist (x,a) * dist (b,a) * r + v * dist (y,a) * dist (b,a) * r`);
\r
113 `u * ((x:real^N - a) dot (b - a)) >= u * dist (x,a) * dist (b,a) * r`);
\r
114 (MATCH_MP_TAC (REAL_ARITH `&0 <= a - b ==> a >= b`));
\r
115 (REWRITE_TAC[REAL_ARITH `a * b * c * d = a * (b * c * d)`;
\r
116 REAL_ARITH `a * b - a * c = a * (b - c)`]);
\r
117 (MATCH_MP_TAC REAL_LE_MUL);
\r
118 (ASM_REAL_ARITH_TAC);
\r
121 `v * ((y:real^N - a) dot (b - a)) >= v * dist (y,a) * dist (b,a) * r`);
\r
122 (MATCH_MP_TAC (REAL_ARITH `&0 <= a - b ==> a >= b`));
\r
123 (REWRITE_TAC[REAL_ARITH `a * b * c * d = a * (b * c * d)`;
\r
124 REAL_ARITH `a * b - a * c = a * (b - c)`]);
\r
125 (MATCH_MP_TAC REAL_LE_MUL);
\r
126 (ASM_REAL_ARITH_TAC);
\r
127 (ASM_REAL_ARITH_TAC);
\r
130 `dist (u % x + v % y,a) * dist (b,a:real^N) * r <=
\r
131 u * dist (x,a) * dist (b,a) * r + v * dist (y,a) * dist (b,a) * r`);
\r
134 (MATCH_MP_TAC (REAL_ARITH `&0 <= a - b ==> b <= a`));
\r
135 (REWRITE_TAC[REAL_ARITH `(a * b * x + c * d * x) - e * x =
\r
136 (a * b + c * d - e) * x`]);
\r
137 (MATCH_MP_TAC REAL_LE_MUL);
\r
139 (REWRITE_TAC[dist]);
\r
140 (REWRITE_WITH `(u % x + v % y) - a = u % (x - a) + v % (y - a:real^N)`);
\r
141 (ASM_REWRITE_TAC[VECTOR_SUB_LDISTRIB; VECTOR_MUL_LID;
\r
142 VECTOR_ARITH `a - x % b + c - y % b = (a + c) - (x + y) % b`]);
\r
143 (REWRITE_TAC[REAL_ARITH `&0 <= a + b - c <=> c <= a + b`]);
\r
144 (MATCH_MP_TAC (REAL_ARITH
\r
145 `m <= norm (u % (x - a:real^N)) + norm (v % (y - a)) /\
\r
146 norm (u % (x - a)) = b /\
\r
147 norm (v % (y - a)) = c ==> m <= b + c`));
\r
148 (REWRITE_TAC[NORM_TRIANGLE;NORM_MUL]);
\r
149 (REWRITE_WITH `abs u = u /\ abs v = v`);
\r
150 (ASM_SIMP_TAC[REAL_ABS_REFL]);
\r
152 (MATCH_MP_TAC REAL_LE_MUL);
\r
153 (ASM_REWRITE_TAC[DIST_POS_LE]);
\r
154 (ASM_REAL_ARITH_TAC);
\r
158 (NEW_GOAL `u = &0`);
\r
159 (ASM_REAL_ARITH_TAC);
\r
160 (NEW_GOAL `v = &1`);
\r
161 (ASM_REAL_ARITH_TAC);
\r
162 (ASM_REWRITE_TAC[REAL_MUL_LZERO;REAL_ADD_LID;REAL_MUL_LID]);
\r
163 (ASM_REWRITE_TAC[VECTOR_MUL_LZERO;VECTOR_ADD_LID;VECTOR_MUL_LID])]);;
\r
165 (* ======================================================================= *)
\r
167 let FINITE_PERMUTE_3 = prove_by_refinement
\r
168 (`FINITE {p | p permutes {0, 1, 2}}`,
\r
169 [MATCH_MP_TAC FINITE_PERMUTATIONS THEN MESON_TAC[FINITE_RULES]]);;
\r
170 let FINITE_PERMUTE_4 = prove_by_refinement
\r
171 (`FINITE {p | p permutes {0, 1, 2, 3}}`,
\r
172 [MATCH_MP_TAC FINITE_PERMUTATIONS THEN MESON_TAC[FINITE_RULES]]);;
\r
174 (* ======================================================================= *)
\r
176 let TRUONG_SET_TAC = let basicthms =
\r
177 [NOT_IN_EMPTY; IN_UNIV; IN_UNION; IN_INTER; IN_DIFF; IN_INSERT;
\r
178 IN_DELETE; IN_REST; IN_INTERS; IN_UNIONS; IN_IMAGE] in
\r
179 let allthms = basicthms @ map (REWRITE_RULE[IN]) basicthms @
\r
180 [IN_ELIM_THM; IN] in
\r
182 TRY(POP_ASSUM_LIST(MP_TAC o end_itlist CONJ)) THEN
\r
183 REPEAT COND_CASES_TAC THEN
\r
184 REWRITE_TAC[EXTENSION; SUBSET; PSUBSET; DISJOINT; SING] THEN
\r
185 REWRITE_TAC allthms in
\r
188 (if ths = [] then ALL_TAC else MP_TAC(end_itlist CONJ ths)) THEN
\r
191 (* ======================================================================= *)
\r
193 let DISJOINT_KY_LEMMA = prove_by_refinement (
\r
194 `~(x = y) /\ ~(x = z) ==> DISJOINT {x} {y, z:real^3}`,
\r
195 [(REPEAT STRIP_TAC);
\r
196 (REWRITE_TAC[DISJOINT; INTER ; IN; IN_ELIM_THM;Geomdetail.IN_ACT_SING]);
\r
197 (MATCH_MP_TAC (MESON [] `(~a ==> F) ==> a`));
\r
199 (SUBGOAL_THEN `?t. t IN {x' | x' = x /\ {y, z:real^3} x'}` ASSUME_TAC);
\r
200 (UP_ASM_TAC THEN SET_TAC[]);
\r
201 (FIRST_X_ASSUM CHOOSE_TAC);
\r
202 (UP_ASM_TAC THEN REWRITE_TAC[IN; IN_ELIM_THM]);
\r
203 (NEW_GOAL `{y, z:real^3} t <=> (t = y) \/ (t = z)`);
\r
204 (TRUONG_SET_TAC[]);
\r
205 (ASM_REWRITE_TAC[]);
\r
206 (ASM_MESON_TAC[])]);;
\r
208 (* ======================================================================= *)
\r
212 let DIHV_SYM = prove_by_refinement (
\r
213 `!(x:real^N) y z t. dihV x y z t = dihV y x z t`,
\r
214 [ (REPEAT GEN_TAC);
\r
215 (REWRITE_TAC[dihV] THEN REPEAT LET_TAC);
\r
216 (MATCH_MP_TAC (MESON[]
\r
217 `!a b c d x. (a = b) /\ (c = d) ==> arcV x a c = arcV x b d`));
\r
218 (REPEAT STRIP_TAC);
\r
219 (* Break into 2 subgoals with similar proofs *)
\r
222 (EXPAND_TAC "vap'" THEN EXPAND_TAC "vap");
\r
224 (REWRITE_WITH `(va':real^N) = va - vc`);
\r
225 (EXPAND_TAC "va'" THEN EXPAND_TAC "va" THEN EXPAND_TAC "vc");
\r
226 (VECTOR_ARITH_TAC);
\r
228 (REWRITE_WITH `(vc':real^N) = --vc`);
\r
229 (EXPAND_TAC "vc'" THEN EXPAND_TAC "vc");
\r
230 (VECTOR_ARITH_TAC);
\r
233 `(--vc dot --vc) % (va:real^N - vc) = (vc dot vc) % va - (vc dot vc) % vc`);
\r
234 (REWRITE_TAC[DOT_RNEG;DOT_LNEG;REAL_ARITH `-- --x = x `]);
\r
235 (VECTOR_ARITH_TAC);
\r
237 (MATCH_MP_TAC (VECTOR_ARITH `a = b + c ==> x:real^N - b - c = x - a `));
\r
238 (REWRITE_WITH `((va:real^N - vc) dot --vc) % --vc =
\r
239 (va dot vc) % vc - (vc dot vc) % vc`);
\r
240 (REWRITE_TAC[DOT_RNEG;DOT_LNEG;VECTOR_MUL_LNEG; VECTOR_MUL_RNEG]);
\r
241 (REWRITE_TAC[VECTOR_NEG_MINUS1;VECTOR_MUL_ASSOC]);
\r
242 (REWRITE_TAC[REAL_ARITH `-- &1 * -- &1 * x = x`;
\r
243 DOT_LSUB;VECTOR_SUB_RDISTRIB]);
\r
244 (VECTOR_ARITH_TAC);
\r
247 (EXPAND_TAC "vbp'" THEN EXPAND_TAC "vbp");
\r
248 (REWRITE_WITH `(vb':real^N) = vb - vc`);
\r
249 (EXPAND_TAC "vb'" THEN EXPAND_TAC "vb" THEN EXPAND_TAC "vc");
\r
250 (VECTOR_ARITH_TAC);
\r
252 (REWRITE_WITH `(vc':real^N) = --vc`);
\r
253 (EXPAND_TAC "vc'" THEN EXPAND_TAC "vc");
\r
254 (VECTOR_ARITH_TAC);
\r
257 `(--vc dot --vc) % (vb:real^N - vc) = (vc dot vc) % vb - (vc dot vc) % vc`);
\r
258 (REWRITE_TAC[DOT_RNEG;DOT_LNEG;REAL_ARITH `-- --x = x `]);
\r
259 (VECTOR_ARITH_TAC);
\r
261 (MATCH_MP_TAC (VECTOR_ARITH `a = b + c ==> x:real^N - b - c = x - a `));
\r
262 (REWRITE_WITH `((vb:real^N - vc) dot --vc) % --vc =
\r
263 (vb dot vc) % vc - (vc dot vc) % vc`);
\r
264 (REWRITE_TAC[DOT_RNEG;DOT_LNEG;VECTOR_MUL_LNEG; VECTOR_MUL_RNEG]);
\r
265 (REWRITE_TAC[VECTOR_NEG_MINUS1;VECTOR_MUL_ASSOC]);
\r
266 (REWRITE_TAC[REAL_ARITH `-- &1 * -- &1 * x = x`;
\r
267 DOT_LSUB;VECTOR_SUB_RDISTRIB]);
\r
268 (VECTOR_ARITH_TAC)]);;
\r
271 (* ======================================================================= *)
\r
273 let RCONE_GT_SUBSET_RCONE_GE = prove_by_refinement (
\r
274 `! z:real^3 w h. rcone_gt z w h SUBSET rcone_ge z w h`,
\r
275 [ (REPEAT GEN_TAC THEN REWRITE_TAC[RCONE_GT_GE]);
\r
278 (* ======================================================================= *)
\r
280 let MCELL_EXPLICIT = prove_by_refinement (
\r
282 mcell 0 V ul = mcell0 V ul /\
\r
283 mcell 1 V ul = mcell1 V ul /\
\r
284 mcell 2 V ul = mcell2 V ul /\
\r
285 mcell 3 V ul = mcell3 V ul /\
\r
286 (k >= 4 ==> mcell k V ul = mcell4 V ul)`,
\r
287 [ (NEW_GOAL `((1 = 0) ==> F) /\ ((2 = 0) ==> F) /\ ((3 = 0) ==> F) /\
\r
288 ((2 = 1) ==> F) /\ ((3 = 1) ==> F) /\ ((3 = 2) ==> F)`);
\r
290 (REPEAT STRIP_TAC); (REWRITE_TAC[mcell]);
\r
291 (REWRITE_TAC[mcell]); (COND_CASES_TAC);
\r
292 (ASM_MESON_TAC[]); (MESON_TAC[]);
\r
293 (REWRITE_TAC[mcell]); (COND_CASES_TAC);
\r
294 (ASM_MESON_TAC[]); (COND_CASES_TAC);
\r
295 (ASM_MESON_TAC[]); (MESON_TAC[]);
\r
296 (REWRITE_TAC[mcell]); (COND_CASES_TAC);
\r
297 (ASM_MESON_TAC[]); (COND_CASES_TAC);
\r
298 (ASM_MESON_TAC[]); (COND_CASES_TAC);
\r
299 (ASM_MESON_TAC[]); (MESON_TAC[]);
\r
300 (REWRITE_TAC[mcell]); (COND_CASES_TAC);
\r
301 (ASM_MESON_TAC[ARITH_RULE `~(0 >= 4)`]);
\r
302 (COND_CASES_TAC); (ASM_MESON_TAC[ARITH_RULE `~(1 >= 4)`]);
\r
303 (COND_CASES_TAC); (ASM_MESON_TAC[ARITH_RULE `~(2 >= 4)`]);
\r
304 (COND_CASES_TAC); (ASM_MESON_TAC[ARITH_RULE `~(3 >= 4)`]);
\r
307 (* ======================================================================= *)
\r
309 let EVENTUALLY_RADIAL_EMPTY = prove_by_refinement (
\r
310 `!v:real^3. eventually_radial v {} `,
\r
312 (REWRITE_TAC[eventually_radial;radial]);
\r
314 (REWRITE_TAC[REAL_ARITH `&1 > &0`;INTER_SUBSET]);
\r
315 (REPEAT STRIP_TAC);
\r
317 (DEL_TAC THEN DEL_TAC THEN UP_ASM_TAC);
\r
318 (REWRITE_TAC[INTER_EMPTY]);
\r
320 (UP_ASM_TAC THEN MESON_TAC[])]);;
\r
322 (* ======================================================================= *)
\r
324 let EVENTUALLY_RADIAL_NOT_IN_CLOSED_SET = prove_by_refinement (
\r
325 `!v:real^3 S. ~(S v) /\ (closed S)==> eventually_radial v S`,
\r
326 [(REPEAT STRIP_TAC);
\r
327 (NEW_GOAL `?r. r > &0 /\ ball(v:real^3, r) INTER S = {}`);
\r
328 (UP_ASM_TAC THEN REWRITE_TAC[closed; open_def]);
\r
330 (MP_TAC (SPEC `v:real^3` (ASSUME `!x. x IN (:real^3) DIFF S
\r
332 (!x'. dist (x',x) < e ==> x' IN (:real^3) DIFF S))`)));
\r
334 (NEW_GOAL `(?e. &0 < e /\ (!x'. dist (x',v:real^3) < e ==> x' IN (:real^3) DIFF S))`);
\r
335 (FIRST_X_ASSUM MATCH_MP_TAC);
\r
336 (REWRITE_TAC[IN_DIFF]);
\r
337 (ASM_REWRITE_TAC[IN]);
\r
338 (MESON_TAC[IN_UNIV;IN]);
\r
339 (FIRST_X_ASSUM CHOOSE_TAC);
\r
340 (EXISTS_TAC `e:real`);
\r
342 (ASM_REAL_ARITH_TAC);
\r
343 (REWRITE_TAC[ball]);
\r
344 (MATCH_MP_TAC (SET_RULE `(!a:real^3. (a IN A) ==> ~(a IN B)) ==> (A INTER B = {})`));
\r
345 (REWRITE_TAC[IN; IN_ELIM_THM]);
\r
346 (GEN_TAC THEN DISCH_TAC);
\r
347 (NEW_GOAL `a IN (:real^3) DIFF S ==> ~S a `);
\r
348 (REWRITE_TAC[IN_DIFF;IN; IN_ELIM_THM]);
\r
350 (FIRST_X_ASSUM MATCH_MP_TAC);
\r
351 (UP_ASM_TAC THEN ASM_REWRITE_TAC[DIST_SYM]);
\r
352 (REWRITE_TAC[eventually_radial;radial]);
\r
353 (FIRST_X_ASSUM CHOOSE_TAC);
\r
354 (EXISTS_TAC `r:real`);
\r
355 (ASM_REWRITE_TAC[INTER_SUBSET]);
\r
356 (REPEAT STRIP_TAC);
\r
358 (DEL_TAC THEN DEL_TAC);
\r
359 (UP_ASM_TAC THEN REWRITE_WITH `S INTER ball (v,r) = ball (v:real^3,r) INTER S`);
\r
361 (ASM_REWRITE_TAC[]);
\r
363 (UP_ASM_TAC THEN MESON_TAC[])]);;
\r
365 (* ======================================================================= *)
\r
367 let CLOSED_CONVEX_HULL_FINITE = prove
\r
368 (`!s. FINITE s ==> closed(convex hull s)`,
\r
369 MESON_TAC[COMPACT_IMP_CLOSED; COMPACT_CONVEX_HULL; FINITE_IMP_COMPACT]);;
\r
371 (* ======================================================================= *)
\r
373 let CLOSED_ROGERS = prove_by_refinement (
\r
374 `! V ul:(real^3)list.
\r
375 saturated V /\ packing V /\ barV V 3 ul ==> closed (rogers V ul)`,
\r
376 [(REPEAT STRIP_TAC THEN REWRITE_TAC[ROGERS]);
\r
377 (MATCH_MP_TAC CLOSED_CONVEX_HULL_FINITE);
\r
378 (MATCH_MP_TAC FINITE_IMAGE);
\r
379 (REWRITE_WITH `{j | j < LENGTH (ul:(real^3)list)} ={j| j < 4}`);
\r
380 (MATCH_MP_TAC (MESON[] `(a = b) ==> ({j:num| j < a} = {j | j < b})`));
\r
381 (NEW_GOAL `?u0 u1 u2 u3. (ul:(real^3)list) = [u0:real^3;u1;u2;u3]`);
\r
382 (MP_TAC (ASSUME `barV V 3 ul`));
\r
383 (REWRITE_TAC[BARV_3_EXPLICIT]);
\r
384 (FIRST_X_ASSUM CHOOSE_TAC);
\r
385 (FIRST_X_ASSUM CHOOSE_TAC);
\r
386 (FIRST_X_ASSUM CHOOSE_TAC);
\r
387 (FIRST_X_ASSUM CHOOSE_TAC);
\r
388 (ASM_REWRITE_TAC[LENGTH]);
\r
390 (REWRITE_TAC[FINITE_NUMSEG_LT])]);;
\r
392 (* ======================================================================= *)
\r
394 let CLOSED_SET_OF_LIST_KY_LEMMA_1 = prove_by_refinement (
\r
396 saturated V /\ packing V /\ barV V 3 (ul:(real^3)list)
\r
398 (convex hull (set_of_list (truncate_simplex 2 ul) UNION {mxi V ul}))`,
\r
399 [(REPEAT STRIP_TAC THEN MATCH_MP_TAC CLOSED_CONVEX_HULL_FINITE);
\r
400 (NEW_GOAL `?u0 u1 u2 u3. (ul:(real^3)list) = [u0:real^3;u1;u2;u3]`);
\r
401 (MP_TAC (ASSUME `barV V 3 ul`));
\r
402 (REWRITE_TAC[BARV_3_EXPLICIT]);
\r
403 (FIRST_X_ASSUM CHOOSE_TAC);
\r
404 (FIRST_X_ASSUM CHOOSE_TAC);
\r
405 (FIRST_X_ASSUM CHOOSE_TAC);
\r
406 (FIRST_X_ASSUM CHOOSE_TAC);
\r
407 (REWRITE_WITH `truncate_simplex 2 ul = [u0;u1;u2:real^3]`);
\r
408 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
\r
409 (REWRITE_TAC[set_of_list]);
\r
410 (REWRITE_TAC[ SET_RULE `!a b c d. {a,b,c} UNION {d:real^3} = {a,b,c,d}`]);
\r
411 (REWRITE_TAC[Geomdetail.FINITE6])]);;
\r
412 (* ======================================================================= *)
\r
414 let CLOSED_SET_OF_LIST_KY_LEMMA_2 = prove_by_refinement (
\r
415 `!V (ul:(real^3)list).
\r
416 saturated V /\ packing V /\ barV V 3 ul ==>
\r
417 closed (convex hull set_of_list ul)`,
\r
418 [(REPEAT STRIP_TAC THEN MATCH_MP_TAC CLOSED_CONVEX_HULL_FINITE);
\r
419 (NEW_GOAL `?u0 u1 u2 u3. (ul:(real^3)list) = [u0:real^3;u1;u2;u3]`);
\r
420 (MP_TAC (ASSUME `barV V 3 ul`));
\r
421 (REWRITE_TAC[BARV_3_EXPLICIT]);
\r
422 (FIRST_X_ASSUM CHOOSE_TAC);
\r
423 (FIRST_X_ASSUM CHOOSE_TAC);
\r
424 (FIRST_X_ASSUM CHOOSE_TAC);
\r
425 (FIRST_X_ASSUM CHOOSE_TAC);
\r
426 (ASM_REWRITE_TAC[set_of_list]);
\r
427 (REWRITE_TAC[Geomdetail.FINITE6])]);;
\r
429 (* ======================================================================= *)
\r
431 let CLOSED_RCONE_GE = prove_by_refinement (
\r
432 `!v0 v1:real^3 a. &0 < a ==> closed (rcone_ge v0 v1 a)`,
\r
433 [(REPEAT STRIP_TAC THEN REWRITE_TAC[rcone_ge;rconesgn]);
\r
434 (REWRITE_TAC[closed]);
\r
435 (REWRITE_WITH `(:real^3) DIFF
\r
436 {x | (x - v0) dot (v1 - v0) >= dist (x,v0) * dist (v1,v0) * a} =
\r
437 {x | (x - v0) dot (v1 - v0) < dist (x,v0) * dist (v1,v0) * a}`);
\r
438 (REWRITE_TAC[Vol1.SET_EQ]);
\r
439 (REWRITE_TAC[IN_DIFF;IN;IN_ELIM_THM;IN_UNIV]);
\r
440 (REPEAT STRIP_TAC);
\r
441 (UP_ASM_TAC THEN REAL_ARITH_TAC);
\r
442 (ASM_REAL_ARITH_TAC);
\r
443 (REWRITE_TAC[open_def;IN;IN_ELIM_THM]);
\r
444 (REPEAT STRIP_TAC);
\r
445 (NEW_GOAL `~(v0 = v1:real^3)`);
\r
447 (SWITCH_TAC THEN UP_ASM_TAC THEN ASM_REWRITE_TAC[]);
\r
448 (REWRITE_TAC[VECTOR_SUB_REFL; DOT_RZERO; DIST_REFL; REAL_MUL_LZERO;REAL_MUL_RZERO]);
\r
451 (ABBREV_TAC `s = dist (x,v0:real^3) * dist (v1,v0) * a`);
\r
452 (ABBREV_TAC `t = (x - v0) dot (v1 - v0:real^3)`);
\r
453 (EXISTS_TAC `(s - t) / (dist (v1,v0) * a + dist (v1, v0:real^3))`);
\r
455 (MATCH_MP_TAC REAL_LT_DIV);
\r
457 (ASM_REAL_ARITH_TAC);
\r
458 (MATCH_MP_TAC REAL_LT_ADD);
\r
459 (ASM_SIMP_TAC [DIST_POS_LT]);
\r
460 (MATCH_MP_TAC REAL_LT_MUL);
\r
461 (ASM_SIMP_TAC [DIST_POS_LT]);
\r
463 (REPEAT STRIP_TAC);
\r
464 (NEW_GOAL `(x' - v0) dot (v1 - v0) <=
\r
465 (x - v0:real^3) dot (v1 - v0) + dist (x',x) * dist (v1,v0) `);
\r
466 (MATCH_MP_TAC (REAL_ARITH `&0 <= a - b ==> b <= a`));
\r
467 (REWRITE_TAC[REAL_ARITH `(x + y) - z = (x - z) + y`]);
\r
468 (REWRITE_TAC[VECTOR_ARITH `x dot y - z dot y = (x - z) dot y`]);
\r
469 (REWRITE_TAC[VECTOR_ARITH `(x:real^3) - y - (z - y) = (x - z)`;dist]);
\r
470 (REWRITE_WITH ` (x - x':real^3) dot (v1 - v0:real^3) = -- ((x' - x) dot (v1 - v0))`);
\r
471 (VECTOR_ARITH_TAC);
\r
473 (MATCH_MP_TAC (REAL_ARITH `b <= a ==> &0 <= --b + a`));
\r
474 (REWRITE_TAC[NORM_CAUCHY_SCHWARZ]);
\r
475 (NEW_GOAL `dist (x',v0) * dist (v1,v0:real^3) * a >=
\r
476 dist (x,v0) * dist (v1,v0) * a - dist (x',x) * dist (v1,v0) * a `);
\r
477 (MATCH_MP_TAC (REAL_ARITH `&0 <= a - b ==> a >= b`));
\r
478 (REWRITE_TAC[REAL_ARITH `x * a * b - (y * a * b - z * a * b) = (x - y + z) * (a * b) `]);
\r
479 (MATCH_MP_TAC REAL_LE_MUL);
\r
481 (MATCH_MP_TAC (REAL_ARITH `b <= a + c ==> &0 <= a - b + c`));
\r
482 (REWRITE_TAC[DIST_SYM]);
\r
483 (REWRITE_WITH `dist (x, x':real^3) = dist (x', x)`);
\r
484 (REWRITE_TAC[DIST_SYM]);
\r
485 (REWRITE_TAC[DIST_TRIANGLE]);
\r
486 (MATCH_MP_TAC REAL_LE_MUL);
\r
488 (ASM_SIMP_TAC[REAL_ARITH `&0 < a ==> &0 <= a`; DIST_POS_LE ]);
\r
489 (MATCH_MP_TAC (REAL_ARITH `(?n q. m <= n /\ p >= q /\ n < q) ==> m < p`));
\r
490 (EXISTS_TAC `(x - v0) dot (v1 - v0) + dist (x',x) * dist (v1,v0:real^3)`);
\r
491 (EXISTS_TAC `dist (x,v0:real^3) * dist (v1,v0) * a - dist (x',x) * dist (v1,v0) * a`);
\r
492 (ASM_REWRITE_TAC[]);
\r
493 (REWRITE_TAC[REAL_ARITH `t + c * b < s - c * b * a <=> c * (b * a + b) < s - t
\r
495 (NEW_GOAL `dist (x',x) * (dist (v1,v0:real^3) * a + dist (v1,v0)) < s - t <=>
\r
496 dist (x':real^3,x) < (s - t) / (dist (v1,v0) * a + dist (v1,v0))`);
\r
497 (ONCE_REWRITE_TAC[MESON[] `!a b. (a <=> b) <=> (b <=> a)`]);
\r
498 (MATCH_MP_TAC REAL_LT_RDIV_EQ);
\r
499 (MATCH_MP_TAC REAL_LT_ADD);
\r
500 (ASM_SIMP_TAC[REAL_LT_MUL; REAL_ARITH `&0 < a ==> &0 <= a`; DIST_POS_LT]);
\r
501 (ASM_REWRITE_TAC[])]);;
\r
503 (* ======================================================================= *)
\r
505 let BARV_IMP_HL_1_POS_LT = prove_by_refinement (
\r
506 `!V ul:(real^3)list.
\r
507 saturated V /\ packing V /\ barV V 3 ul
\r
508 ==> &0 < hl (truncate_simplex 1 ul)`,
\r
509 [(REPEAT STRIP_TAC);
\r
510 (NEW_GOAL `?u0 u1 u2 u3. (ul:(real^3)list) = [u0:real^3;u1;u2;u3]`);
\r
511 (MP_TAC (ASSUME `barV V 3 ul`));
\r
512 (REWRITE_TAC[BARV_3_EXPLICIT]);
\r
513 (REPEAT (FIRST_X_ASSUM CHOOSE_TAC));
\r
514 (ABBREV_TAC `vl = truncate_simplex 1 (ul:(real^3)list)`);
\r
515 (NEW_GOAL `hl (vl:(real^3)list) = dist (circumcenter (set_of_list vl),HD vl)`);
\r
516 (MATCH_MP_TAC HL_EQ_DIST0);
\r
517 (EXISTS_TAC `V:real^3->bool`);
\r
519 (ASM_REWRITE_TAC[]);
\r
521 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
\r
523 (ASM_REWRITE_TAC[ARITH_RULE `1 <= 3`]);
\r
525 (NEW_GOAL `&0 <= hl (vl:(real^3)list)`);
\r
526 (ASM_REWRITE_TAC[DIST_POS_LE]);
\r
527 (ASM_CASES_TAC `&0 < hl (vl:(real^3)list)`);
\r
528 (ASM_REWRITE_TAC[]);
\r
529 (NEW_GOAL `hl (vl:(real^3)list) = &0`);
\r
530 (ASM_REAL_ARITH_TAC);
\r
532 (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);
\r
533 (REWRITE_TAC[DIST_EQ_0]);
\r
534 (REWRITE_WITH `vl = [u0;u1:real^3]`);
\r
535 (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
\r
536 (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
\r
537 (REWRITE_TAC[set_of_list;HD;CIRCUMCENTER_2;midpoint]);
\r
539 (NEW_GOAL `(u0:real^3) = u1`);
\r
540 (UP_ASM_TAC THEN VECTOR_ARITH_TAC);
\r
541 (NEW_GOAL `barV V 1 (vl:(real^3)list)`);
\r
543 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
\r
545 (ASM_REWRITE_TAC[ARITH_RULE `1 <= 3`]);
\r
546 (NEW_GOAL `CARD (set_of_list (vl:(real^3)list)) = 1 + 1`);
\r
547 (ASM_MESON_TAC[BARV_IMP_LENGTH_EQ_CARD]);
\r
548 (UP_ASM_TAC THEN REWRITE_WITH `vl = [u0;u1:real^3]`);
\r
549 (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]);
\r
550 (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
\r
551 (ASM_REWRITE_TAC[set_of_list]);
\r
552 (REWRITE_TAC[ SET_RULE `{u1, u1:real^3} = {u1}`]);
\r
553 (REWRITE_TAC[Hypermap.CARD_SINGLETON]);
\r
555 (UP_ASM_TAC THEN MESON_TAC[])]);;
\r
557 (* ======================================================================= *)
\r
559 let CLOSED_MCELL = prove_by_refinement (
\r
561 saturated V /\ packing V /\ barV V 3 ul
\r
562 ==> closed (mcell k V ul)`,
\r
563 [(REPEAT STRIP_TAC);
\r
564 (ASM_CASES_TAC `k = 0`);
\r
565 (ASM_REWRITE_TAC[MCELL_EXPLICIT;mcell0]);
\r
566 (MATCH_MP_TAC CLOSED_DIFF);
\r
567 (ASM_MESON_TAC[CLOSED_ROGERS; OPEN_BALL]);
\r
569 (ASM_CASES_TAC `k = 1`);
\r
570 (ASM_REWRITE_TAC[MCELL_EXPLICIT;mcell1]);
\r
572 (MATCH_MP_TAC CLOSED_DIFF);
\r
574 (MATCH_MP_TAC CLOSED_INTER);
\r
575 (ASM_MESON_TAC[CLOSED_ROGERS; CLOSED_CBALL]);
\r
576 (REWRITE_TAC[OPEN_RCONE_GT]);
\r
577 (REWRITE_TAC[CLOSED_EMPTY]);
\r
579 (SUBGOAL_THEN `? u0 u1 u2 u3. (ul:(real^3)list) = [u0:real^3;u1;u2;u3]` CHOOSE_TAC);
\r
580 (MP_TAC (ASSUME `barV V 3 ul`));
\r
581 (REWRITE_TAC[BARV_3_EXPLICIT]);
\r
582 (FIRST_X_ASSUM CHOOSE_TAC);
\r
583 (FIRST_X_ASSUM CHOOSE_TAC);
\r
584 (FIRST_X_ASSUM CHOOSE_TAC);
\r
585 (ASM_CASES_TAC `k = 2`);
\r
587 (ASM_REWRITE_TAC[MCELL_EXPLICIT;mcell2]);
\r
590 (MATCH_MP_TAC CLOSED_INTER);
\r
593 (MATCH_MP_TAC CLOSED_RCONE_GE);
\r
595 (MATCH_MP_TAC REAL_LT_DIV);
\r
596 (SIMP_TAC[SQRT_POS_LT; REAL_ARITH `&0 < &2`]);
\r
597 (ASM_MESON_TAC[BARV_IMP_HL_1_POS_LT]);
\r
599 (MATCH_MP_TAC CLOSED_INTER);
\r
601 (MATCH_MP_TAC CLOSED_RCONE_GE);
\r
603 (MATCH_MP_TAC REAL_LT_DIV);
\r
604 (SIMP_TAC[SQRT_POS_LT; REAL_ARITH `&0 < &2`]);
\r
605 (ASM_MESON_TAC[BARV_IMP_HL_1_POS_LT]);
\r
607 (MATCH_MP_TAC CLOSED_AFF_GE);
\r
608 (MESON_TAC[Geomdetail.FINITE6]);
\r
609 (MESON_TAC[CLOSED_EMPTY]);
\r
611 (ASM_CASES_TAC `k = 3`);
\r
612 (ASM_REWRITE_TAC[MCELL_EXPLICIT;mcell3]);
\r
614 (ASM_MESON_TAC[CLOSED_SET_OF_LIST_KY_LEMMA_1]);
\r
615 (MESON_TAC[CLOSED_EMPTY]);
\r
617 (NEW_GOAL `k >= 4`);
\r
619 (ASM_SIMP_TAC[MCELL_EXPLICIT;mcell4]);
\r
621 (ASM_MESON_TAC[CLOSED_SET_OF_LIST_KY_LEMMA_2]);
\r
622 (MESON_TAC[CLOSED_EMPTY])
\r
625 (* ======================================================================= *)
\r
627 let BARV_IMP_u0_IN_V = prove_by_refinement (
\r
628 `!V ul u0 u1 u2 u3.
\r
629 saturated V /\ packing V /\ barV V 3 ul /\ ul = [u0;u1;u2;u3:real^3]
\r
631 [(REWRITE_TAC[BARV; VORONOI_NONDG]);
\r
632 (REPEAT STRIP_TAC);
\r
633 (NEW_GOAL `initial_sublist [u0:real^3] ul /\ 0 < LENGTH [u0]`);
\r
634 (REWRITE_TAC[INITIAL_SUBLIST;LENGTH; APPEND; ARITH_RULE `0 < SUC 0`]);
\r
635 (EXISTS_TAC `[u1;u2;u3:real^3]`);
\r
636 (ASM_REWRITE_TAC[]);
\r
637 (NEW_GOAL `set_of_list [u0:real^3] SUBSET V`);
\r
639 (UP_ASM_TAC THEN REWRITE_TAC[set_of_list]);
\r
642 (* ======================================================================= *)
\r
644 let ROGERS_INTER_V_LEMMA = prove_by_refinement (
\r
646 saturated V /\ packing V /\ barV V 3 ul /\ v IN V /\ (rogers V ul v)
\r
648 [(REPEAT STRIP_TAC);
\r
649 (SUBGOAL_THEN `? u0 u1 u2 u3. (ul:(real^3)list) = [u0:real^3;u1;u2;u3]` CHOOSE_TAC);
\r
650 (MP_TAC (ASSUME `barV V 3 ul`));
\r
651 (REWRITE_TAC[BARV_3_EXPLICIT]);
\r
652 (FIRST_X_ASSUM CHOOSE_TAC);
\r
653 (FIRST_X_ASSUM CHOOSE_TAC);
\r
654 (FIRST_X_ASSUM CHOOSE_TAC);
\r
655 (ASM_REWRITE_TAC[HD]);
\r
657 (NEW_GOAL `(rogers V ul) SUBSET (voronoi_closed V (u0:real^3))`);
\r
658 (REWRITE_TAC[SUBSET]);
\r
659 (REPEAT STRIP_TAC);
\r
660 (NEW_GOAL `!p. p IN voronoi_closed V u0 <=>
\r
661 (?vl. vl IN barV V 3 /\
\r
662 p IN rogers V vl /\
\r
663 truncate_simplex 0 vl = [u0:real^3])`);
\r
664 (GEN_TAC THEN MATCH_MP_TAC GLTVHUM);
\r
665 (ASM_REWRITE_TAC[]);
\r
666 (ASM_MESON_TAC[BARV_IMP_u0_IN_V]);
\r
667 (ASM_REWRITE_TAC[]);
\r
668 (EXISTS_TAC `ul:(real^3)list`);
\r
669 (ASM_REWRITE_TAC[IN; TRUNCATE_SIMPLEX_EXPLICIT_0]);
\r
670 (NEW_GOAL `(v:real^3) IN (voronoi_closed V u0)`);
\r
672 (UP_ASM_TAC THEN REWRITE_TAC[voronoi_closed;IN;IN_ELIM_THM]);
\r
674 (NEW_GOAL `dist (v,u0) <= dist (v,v:real^3)`);
\r
675 (FIRST_ASSUM MATCH_MP_TAC);
\r
676 (ASM_REWRITE_TAC[GSYM IN]);
\r
677 (UP_ASM_TAC THEN REWRITE_TAC[DIST_REFL]);
\r
679 (NEW_GOAL `dist (v, u0:real^3) = &0`);
\r
680 (NEW_GOAL `&0 <= dist (v, u0:real^3)`);
\r
681 (REWRITE_TAC[DIST_POS_LE]);
\r
682 (ASM_REAL_ARITH_TAC);
\r
683 (UP_ASM_TAC THEN MESON_TAC[DIST_EQ_0])]);;
\r
685 (* ======================================================================= *)
\r
687 let CONVEX_HULL_4 = prove
\r
688 (`convex hull {a,b,c,d} =
\r
689 { u % a + v % b + w % c + z %d|
\r
690 &0 <= u /\ &0 <= v /\ &0 <= w /\ &0 <= z /\ u + v + w + z = &1}`,
\r
691 SIMP_TAC[CONVEX_HULL_FINITE; FINITE_INSERT; FINITE_RULES] THEN
\r
692 SIMP_TAC[CONVEX_HULL_FINITE_STEP; FINITE_INSERT; FINITE_RULES] THEN
\r
693 REWRITE_TAC[REAL_ARITH `x - y = z:real <=> x = y + z`;
\r
694 VECTOR_ARITH `x - y = z:real^N <=> x = y + z`] THEN
\r
695 REWRITE_TAC[VECTOR_ADD_RID; REAL_ADD_RID] THEN SET_TAC[]);;
\r
697 (* ======================================================================= *)
\r
699 let REAL_LE_DIV_SIMPLIFY_KY_LEMMA = prove_by_refinement (
\r
700 `!a b c. &0 < a /\ b <= c / a ==> a * b <= c`,
\r
701 [(REPEAT STRIP_TAC);
\r
702 (NEW_GOAL `a * b <= a * (c / a)`);
\r
703 (REWRITE_TAC[REAL_ARITH `x * y <= x * z <=> &0 <= x * (z - y)`]);
\r
704 (MATCH_MP_TAC REAL_LE_MUL);
\r
705 (ASM_REAL_ARITH_TAC);
\r
706 (NEW_GOAL `a * c / a = c`);
\r
707 (REWRITE_TAC[REAL_ARITH `a * c / a = c / a * a`]);
\r
708 (MATCH_MP_TAC REAL_DIV_RMUL);
\r
709 (ASM_REAL_ARITH_TAC);
\r
710 (ASM_MESON_TAC[])]);;
\r
712 (* ======================================================================= *)
\r
715 let EVENTUALLY_RADIAL_CONVEX_HULL_4_sub1 = prove_by_refinement (
\r
717 ~( a IN convex hull {b , c, d})
\r
718 ==> eventually_radial a (convex hull {a, b , c, d})`,
\r
719 [(REPEAT STRIP_TAC);
\r
720 (REWRITE_TAC[eventually_radial]);
\r
721 (ABBREV_TAC `s = convex hull {b , c, d:real^3}`);
\r
723 (NEW_GOAL `(?(x:real^3). x IN s /\
\r
724 (!y:real^3. y IN s ==> dist (a,x) <= dist (a,y)))`);
\r
725 (MATCH_MP_TAC DISTANCE_ATTAINS_INF);
\r
728 (MATCH_MP_TAC CLOSED_CONVEX_HULL_FINITE);
\r
729 (REWRITE_TAC[Geomdetail.FINITE6]);
\r
730 (REWRITE_TAC[CONVEX_HULL_EQ_EMPTY]);
\r
732 (FIRST_X_ASSUM CHOOSE_TAC);
\r
733 (EXISTS_TAC `dist (a, x:real^3)`);
\r
735 (NEW_GOAL `dist (a, x) <= dist (a, b:real^3) /\
\r
736 dist (a, x) <= dist (a, c:real^3) /\
\r
737 dist (a, x) <= dist (a, d:real^3)`);
\r
738 (UP_ASM_TAC THEN REPEAT STRIP_TAC);
\r
740 (FIRST_ASSUM MATCH_MP_TAC);
\r
742 (MATCH_MP_TAC (SET_RULE `b IN {b} /\ {b} SUBSET s ==> b IN s `));
\r
745 (NEW_GOAL `{b:real^3} = convex hull {b}`);
\r
746 (ONCE_REWRITE_TAC[MESON[] `a = b <=> b = a` ]);
\r
747 (REWRITE_TAC[CONVEX_HULL_EQ]);
\r
748 (REWRITE_TAC[CONVEX_SING]);
\r
749 (ONCE_ASM_REWRITE_TAC[]);
\r
751 (MATCH_MP_TAC Marchal_cells.CONVEX_HULL_SUBSET);
\r
754 (FIRST_ASSUM MATCH_MP_TAC);
\r
756 (MATCH_MP_TAC (SET_RULE `c IN {c} /\ {c} SUBSET s ==> c IN s `));
\r
759 (NEW_GOAL `{c:real^3} = convex hull {c}`);
\r
760 (ONCE_REWRITE_TAC[MESON[] `a = b <=> b = a` ]);
\r
761 (REWRITE_TAC[CONVEX_HULL_EQ]);
\r
762 (REWRITE_TAC[CONVEX_SING]);
\r
763 (ONCE_ASM_REWRITE_TAC[]);
\r
765 (MATCH_MP_TAC Marchal_cells.CONVEX_HULL_SUBSET);
\r
769 (FIRST_ASSUM MATCH_MP_TAC);
\r
771 (MATCH_MP_TAC (SET_RULE `c IN {c} /\ {c} SUBSET s ==> c IN s `));
\r
774 (NEW_GOAL `{d:real^3} = convex hull {d}`);
\r
775 (ONCE_REWRITE_TAC[MESON[] `a = b <=> b = a` ]);
\r
776 (REWRITE_TAC[CONVEX_HULL_EQ]);
\r
777 (REWRITE_TAC[CONVEX_SING]);
\r
778 (ONCE_ASM_REWRITE_TAC[]);
\r
780 (MATCH_MP_TAC Marchal_cells.CONVEX_HULL_SUBSET);
\r
783 (* ======== break main lemma into 2 smaller ones =============== *)
\r
787 (ASM_CASES_TAC `dist (a:real^3, x) = &0`);
\r
788 (UP_ASM_TAC THEN REWRITE_TAC[DIST_EQ_0]);
\r
792 (UP_ASM_TAC THEN MESON_TAC[]);
\r
793 (NEW_GOAL `&0 <= dist (a, x:real^3)`);
\r
794 (REWRITE_TAC[DIST_POS_LE]);
\r
795 (ASM_REAL_ARITH_TAC);
\r
799 (REWRITE_TAC[radial; INTER_SUBSET]);
\r
800 (REPEAT STRIP_TAC);
\r
801 (REWRITE_TAC[IN_INTER]);
\r
803 (ASM_CASES_TAC `u:real^3 = vec 0`);
\r
804 (ASM_REWRITE_TAC[VECTOR_MUL_RZERO; VECTOR_ADD_RID]);
\r
805 (REWRITE_TAC[CONVEX_HULL_4;IN;IN_ELIM_THM]);
\r
806 (EXISTS_TAC `&1` THEN EXISTS_TAC `&0` THEN EXISTS_TAC `&0` THEN EXISTS_TAC `&0`);
\r
807 (REWRITE_TAC[REAL_ARITH `&0 <= &1 /\ &0 <= &0 /\ &1 + &0 + &0 + &0 = &1`]);
\r
808 (VECTOR_ARITH_TAC);
\r
809 (NEW_GOAL `?y. y IN convex hull {b, c, d:real^3} /\
\r
810 (a + t % u) IN convex hull {a, y}`);
\r
811 (UNDISCH_TAC `a + u IN convex hull {a, b, c, d:real^3} INTER ball (a,dist (a,x))`);
\r
812 (REWRITE_TAC[CONVEX_HULL_4;IN_INTER;IN;IN_ELIM_THM]);
\r
813 (REPEAT STRIP_TAC);
\r
814 (EXISTS_TAC `(&1 / (&1 - u')) % (v % b + w % c + z % (d:real^3))`);
\r
816 (REWRITE_TAC[CONVEX_HULL_3;IN_ELIM_THM]);
\r
817 (EXISTS_TAC ` v / (&1 - u')`);
\r
818 (EXISTS_TAC ` w / (&1 - u')`);
\r
819 (EXISTS_TAC ` z / (&1 - u')`);
\r
820 (REPEAT STRIP_TAC);
\r
822 (MATCH_MP_TAC REAL_LE_DIV);
\r
823 (ASM_REAL_ARITH_TAC);
\r
824 (MATCH_MP_TAC REAL_LE_DIV);
\r
825 (ASM_REAL_ARITH_TAC);
\r
826 (MATCH_MP_TAC REAL_LE_DIV);
\r
827 (ASM_REAL_ARITH_TAC);
\r
828 (REWRITE_TAC[REAL_ARITH `a / x + b / x + c / x = (a + b + c) / x`]);
\r
829 (MATCH_MP_TAC (MESON [REAL_DIV_REFL] `~(y = &0) /\ (x = y) ==> x / y = &1`));
\r
830 (ASM_REWRITE_TAC[REAL_ARITH `!a b c d e.
\r
831 (&1 - a = &0 <=> a = &1) /\ ( b + c + d = &1 - e <=> e + b + c + d = &1)`]);
\r
833 (NEW_GOAL `v = &0 /\ w = &0 /\ z = &0`);
\r
834 (ASM_REAL_ARITH_TAC);
\r
835 (UNDISCH_TAC `(a:real^3) + u = u' % a + v % b + w % c + z % d`);
\r
836 (ASM_REWRITE_TAC[VECTOR_MUL_LID; VECTOR_MUL_LZERO]);
\r
837 (REWRITE_TAC[VECTOR_ARITH `a + (u:real^3) = a + vec 0 + vec 0 + vec 0 <=> u = vec 0`]);
\r
840 (REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC]);
\r
841 (REWRITE_TAC[REAL_ARITH `!x y. &1 / x * y = y / x`]);
\r
843 (REWRITE_WITH `v % (b:real^3) + w % c + z % d = a + u - u' % a`);
\r
844 (SWITCH_TAC THEN UP_ASM_TAC THEN VECTOR_ARITH_TAC);
\r
845 (REWRITE_TAC[VECTOR_ARITH `!a t u. a + u - t % a = (&1 - t) % a + u`]);
\r
846 (REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC]);
\r
847 (REWRITE_WITH `&1 / (&1 - u') * (&1 - u') = &1`);
\r
848 (REWRITE_TAC[REAL_ARITH `!x y. &1 / x * y = y / x`]);
\r
849 (MATCH_MP_TAC REAL_DIV_REFL);
\r
850 (REWRITE_TAC[REAL_ARITH `!a. &1 - a = &0 <=> a = &1`]);
\r
852 (NEW_GOAL `v = &0 /\ w = &0 /\ z = &0`);
\r
853 (ASM_REAL_ARITH_TAC);
\r
854 (UNDISCH_TAC `(a:real^3) + u = u' % a + v % b + w % c + z % d`);
\r
855 (ASM_REWRITE_TAC[VECTOR_MUL_LID; VECTOR_MUL_LZERO]);
\r
856 (REWRITE_TAC[VECTOR_ARITH `a + (u:real^3) = a + vec 0 + vec 0 + vec 0 <=> u = vec 0`]);
\r
858 (REWRITE_TAC[VECTOR_MUL_LID; CONVEX_HULL_2;IN_ELIM_THM]);
\r
859 (EXISTS_TAC `&1 - t * (&1 - u') `);
\r
860 (EXISTS_TAC `t * (&1 - u')`);
\r
861 (REPEAT STRIP_TAC);
\r
863 (REWRITE_TAC[REAL_ARITH `&0 <= &1 - a <=> a <= &1`]);
\r
864 (NEW_GOAL `dist (a:real^3, a + u) / (&1 - u') = dist (a, a + (&1 / (&1 - u')) % u)`);
\r
865 (REWRITE_TAC[dist; VECTOR_ARITH `a - (a + s:real^3) = -- s`; NORM_NEG; NORM_MUL; REAL_ABS_DIV; REAL_ABS_1]);
\r
866 (ONCE_REWRITE_TAC[REAL_ARITH `&1 / x * y = y / x`]);
\r
868 (ONCE_REWRITE_TAC[MESON[] `x = y <=> y = x`]);
\r
869 (REWRITE_TAC[REAL_ABS_REFL]);
\r
870 (REWRITE_TAC[REAL_ARITH `!a. &0 <= &1 - a <=> a <= &1`]);
\r
871 (ASM_REAL_ARITH_TAC);
\r
872 (NEW_GOAL `(&1 - u') * dist (a, x:real^3) <= norm (u:real^3) `);
\r
873 (REWRITE_WITH `norm (u:real^3) = dist (a, a +u)`);
\r
874 (REWRITE_TAC[dist]);
\r
876 (MATCH_MP_TAC REAL_LE_DIV_SIMPLIFY_KY_LEMMA);
\r
877 (ASM_REWRITE_TAC[]);
\r
880 (ASM_CASES_TAC `(&0 < &1 - u')`);
\r
881 (ASM_REWRITE_TAC[]);
\r
882 (NEW_GOAL `u' = &1`);
\r
883 (NEW_GOAL `u' <= &1`);
\r
884 (ASM_REAL_ARITH_TAC);
\r
885 (NEW_GOAL `&1 <= u'`);
\r
886 (ASM_REAL_ARITH_TAC);
\r
887 (ASM_REAL_ARITH_TAC);
\r
888 (NEW_GOAL `v = &0 /\ w = &0 /\ z = &0`);
\r
889 (ASM_REAL_ARITH_TAC);
\r
890 (UNDISCH_TAC `(a:real^3) + u = u' % a + v % b + w % c + z % d`);
\r
891 (ASM_REWRITE_TAC[VECTOR_MUL_LID; VECTOR_MUL_LZERO]);
\r
892 (REWRITE_TAC[VECTOR_ARITH `a + (u:real^3) = a + vec 0 + vec 0 + vec 0 <=> u = vec 0`]);
\r
895 (UNDISCH_TAC `x IN s /\ (!y. y IN s ==> dist (a:real^3,x) <= dist (a,y))`);
\r
896 (REPEAT STRIP_TAC);
\r
897 (FIRST_ASSUM MATCH_MP_TAC);
\r
898 (EXPAND_TAC "s" THEN REWRITE_TAC[CONVEX_HULL_3; IN; IN_ELIM_THM]);
\r
900 (EXISTS_TAC ` v / (&1 - u')`);
\r
901 (EXISTS_TAC ` w / (&1 - u')`);
\r
902 (EXISTS_TAC ` z / (&1 - u')`);
\r
903 (REPEAT STRIP_TAC);
\r
905 (MATCH_MP_TAC REAL_LE_DIV);
\r
906 (ASM_REAL_ARITH_TAC);
\r
907 (MATCH_MP_TAC REAL_LE_DIV);
\r
908 (ASM_REAL_ARITH_TAC);
\r
909 (MATCH_MP_TAC REAL_LE_DIV);
\r
910 (ASM_REAL_ARITH_TAC);
\r
911 (REWRITE_TAC[REAL_ARITH `a / x + b / x + c / x = (a + b + c) / x`]);
\r
912 (MATCH_MP_TAC (MESON [REAL_DIV_REFL] `~(y = &0) /\ (x = y) ==> x / y = &1`));
\r
913 (ASM_REWRITE_TAC[REAL_ARITH `!a b c d e.
\r
914 (&1 - a = &0 <=> a = &1) /\ ( b + c + d = &1 - e <=> e + b + c + d = &1)`]);
\r
916 (NEW_GOAL `v = &0 /\ w = &0 /\ z = &0`);
\r
917 (ASM_REAL_ARITH_TAC);
\r
918 (UNDISCH_TAC `(a:real^3) + u = u' % a + v % b + w % c + z % d`);
\r
919 (ASM_REWRITE_TAC[VECTOR_MUL_LID; VECTOR_MUL_LZERO]);
\r
920 (REWRITE_TAC[VECTOR_ARITH `a + (u:real^3) = a + vec 0 + vec 0 + vec 0 <=> u = vec 0`]);
\r
923 (REWRITE_WITH `v / (&1 - u') % b + w / (&1 - u') % c + z / (&1 - u') % d =
\r
924 &1 / (&1 - u') % (a + u:real^3) - u'/ (&1 - u') % a `);
\r
925 (ASM_REWRITE_TAC[]);
\r
926 (REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC]);
\r
927 (REWRITE_TAC[REAL_ARITH `&1 / x * y = y / x`]);
\r
928 (VECTOR_ARITH_TAC);
\r
929 (REWRITE_TAC[VECTOR_ADD_LDISTRIB]);
\r
932 (REWRITE_TAC[VECTOR_ARITH `a + b = (t % a + b) - s % a <=> a = (t - s) % a`]);
\r
933 (REWRITE_WITH `&1 / (&1 - u') - u' / (&1 - u') = &1`);
\r
934 (REWRITE_TAC[REAL_ARITH `a / b - c / b = (a - c) / b`]);
\r
935 (MATCH_MP_TAC REAL_DIV_REFL);
\r
936 (REWRITE_TAC[REAL_ARITH `!a. &1 - a = &0 <=> a = &1`]);
\r
938 (NEW_GOAL `v = &0 /\ w = &0 /\ z = &0`);
\r
939 (ASM_REAL_ARITH_TAC);
\r
940 (UNDISCH_TAC `(a:real^3) + u = u' % a + v % b + w % c + z % d`);
\r
941 (ASM_REWRITE_TAC[VECTOR_MUL_LID; VECTOR_MUL_LZERO]);
\r
942 (REWRITE_TAC[VECTOR_ARITH `a + (u:real^3) = a + vec 0 + vec 0 + vec 0 <=> u = vec 0`]);
\r
944 (REWRITE_TAC[VECTOR_MUL_LID]);
\r
948 (NEW_GOAL `t * ((&1 - u') * dist (a,x:real^3)) <= t * norm (u:real^3)`);
\r
949 (REWRITE_TAC[REAL_ARITH `t * s <= t * k <=> &0 <= t * (k - s)`]);
\r
950 (MATCH_MP_TAC REAL_LE_MUL);
\r
951 (ASM_REAL_ARITH_TAC);
\r
952 (NEW_GOAL `t * ((&1 - u') * dist (a,x:real^3)) <= dist (a, x)`);
\r
953 (ASM_REAL_ARITH_TAC);
\r
954 (NEW_GOAL ` t * (&1 - u') <= &1 <=>
\r
955 (t * (&1 - u')) * dist (a,x:real^3) <= &1 * dist (a,x)`);
\r
956 (ONCE_REWRITE_TAC[MESON[] `(a <=> b) <=> (b <=> a)`]);
\r
957 (MATCH_MP_TAC REAL_LE_RMUL_EQ);
\r
958 (ASM_CASES_TAC `dist (a:real^3, x) = &0`);
\r
959 (UP_ASM_TAC THEN REWRITE_TAC[DIST_EQ_0]);
\r
963 (UP_ASM_TAC THEN MESON_TAC[]);
\r
964 (NEW_GOAL `&0 <= dist (a, x:real^3)`);
\r
965 (REWRITE_TAC[DIST_POS_LE]);
\r
966 (ASM_REAL_ARITH_TAC);
\r
969 (ASM_REWRITE_TAC[]);
\r
970 (ASM_REAL_ARITH_TAC);
\r
971 (MATCH_MP_TAC REAL_LE_MUL);
\r
972 (ASM_REAL_ARITH_TAC);
\r
973 (ASM_REAL_ARITH_TAC);
\r
976 (REWRITE_TAC[VECTOR_SUB_RDISTRIB; VECTOR_ADD_LDISTRIB; VECTOR_MUL_LID; VECTOR_MUL_ASSOC]);
\r
978 (REWRITE_TAC [VECTOR_ARITH `a + m % u = a - t + t + n % u <=> (m - n) % u = vec 0`; VECTOR_MUL_EQ_0]);
\r
980 (REWRITE_TAC[REAL_ARITH `(a * b) * &1 / b = a * (b / b)`]);
\r
983 (* ======================================================================== *)
\r
985 (REWRITE_TAC[REAL_ARITH `t - t * s = t * (&1 - s)`]);
\r
986 (MATCH_MP_TAC (MESON[REAL_MUL_RZERO] ` x = &0 ==> t * x = &0`));
\r
987 (REWRITE_TAC[REAL_ARITH `&1 - t = &0 <=> t = &1`]);
\r
988 (MATCH_MP_TAC REAL_DIV_REFL);
\r
990 (REWRITE_TAC[REAL_ARITH `!a. &1 - a = &0 <=> a = &1`]);
\r
992 (NEW_GOAL `v = &0 /\ w = &0 /\ z = &0`);
\r
993 (ASM_REAL_ARITH_TAC);
\r
994 (UNDISCH_TAC `(a:real^3) + u = u' % a + v % b + w % c + z % d`);
\r
995 (ASM_REWRITE_TAC[VECTOR_MUL_LID; VECTOR_MUL_LZERO]);
\r
996 (REWRITE_TAC[VECTOR_ARITH `a + (u:real^3) = a + vec 0 + vec 0 + vec 0 <=> u = vec 0`]);
\r
999 (FIRST_X_ASSUM CHOOSE_TAC);
\r
1000 (UP_ASM_TAC THEN REPEAT STRIP_TAC);
\r
1001 (UP_ASM_TAC THEN MATCH_MP_TAC (SET_RULE `A SUBSET B ==> (a IN A ==> a IN B)`));
\r
1002 (NEW_GOAL `convex hull {a, b , c, d:real^3} = convex hull (convex hull {a, b, c, d})`);
\r
1003 (ONCE_REWRITE_TAC[MESON [] `!a b. a = b <=> b = a`]);
\r
1004 (REWRITE_TAC[CONVEX_HULL_EQ; CONVEX_CONVEX_HULL]);
\r
1005 (ONCE_ASM_REWRITE_TAC[]);
\r
1006 (MATCH_MP_TAC CONVEX_HULL_SUBSET);
\r
1007 (MATCH_MP_TAC (SET_RULE `!m a S. m IN S /\ a IN S ==> {a, m} SUBSET S`));
\r
1009 (MATCH_MP_TAC (SET_RULE `m IN convex hull {b, c, d:real^3} /\
\r
1010 convex hull {b, c, d} SUBSET n ==> m IN n`));
\r
1011 (ASM_REWRITE_TAC[]);
\r
1012 (EXPAND_TAC "s" THEN MATCH_MP_TAC CONVEX_HULL_SUBSET);
\r
1014 (REWRITE_TAC[CONVEX_HULL_4;IN;IN_ELIM_THM]);
\r
1015 (EXISTS_TAC `&1` THEN EXISTS_TAC `&0` THEN EXISTS_TAC `&0` THEN EXISTS_TAC `&0`);
\r
1016 (REWRITE_TAC[REAL_ARITH `&0 <= &1 /\ &0 <= &0 /\ &1 + &0 + &0 + &0 = &1`]);
\r
1017 (VECTOR_ARITH_TAC);
\r
1019 (REWRITE_TAC[ball;IN;IN_ELIM_THM]);
\r
1020 (REWRITE_WITH `dist (a:real^3,a + t % u) = t * norm u`);
\r
1021 (REWRITE_TAC[dist; VECTOR_ARITH `a - (a + b:real^3) = -- b`; NORM_NEG;
\r
1023 (AP_THM_TAC THEN AP_TERM_TAC);
\r
1024 (REWRITE_TAC[REAL_ABS_REFL]);
\r
1025 (ASM_REAL_ARITH_TAC);
\r
1026 (ASM_REWRITE_TAC[])]);;
\r
1028 (* ======================================================================= *)
\r
1030 let U0_NOT_IN_CONVEX_HULL_FROM_ROGERS = prove_by_refinement (
\r
1031 `!V (ul:(real^3)list).
\r
1032 saturated V /\ packing V /\ barV V 3 ul
\r
1035 {omega_list_n V ul 1, omega_list_n V ul 2, omega_list_n V ul 3})`,
\r
1036 [(REWRITE_TAC[ARITH_RULE `1 = SUC 0 /\ 2 = SUC 1 /\ 3 = SUC 2`; OMEGA_LIST_N]);
\r
1037 (REWRITE_TAC[ARITH_RULE `SUC 0 = 1 /\ SUC 1 = 2 /\ SUC 2 = 3`]);
\r
1038 (REPEAT STRIP_TAC);
\r
1039 (NEW_GOAL `?u0 u1 u2 u3. (ul:(real^3)list) = [u0:real^3;u1;u2;u3]`);
\r
1040 (MP_TAC (ASSUME `barV V 3 ul`));
\r
1041 (REWRITE_TAC[BARV_3_EXPLICIT]);
\r
1042 (FIRST_X_ASSUM CHOOSE_TAC);
\r
1043 (FIRST_X_ASSUM CHOOSE_TAC);
\r
1044 (FIRST_X_ASSUM CHOOSE_TAC);
\r
1045 (FIRST_X_ASSUM CHOOSE_TAC);
\r
1047 (ABBREV_TAC `a = closest_point (voronoi_list V
\r
1048 (truncate_simplex 1 (ul:(real^3)list)))`);
\r
1049 (ABBREV_TAC `b = closest_point (voronoi_list V
\r
1050 (truncate_simplex 2 (ul:(real^3)list)))`);
\r
1051 (ABBREV_TAC `c = closest_point (voronoi_list V
\r
1052 (truncate_simplex 3 (ul:(real^3)list)))`);
\r
1053 (* First estimation *)
\r
1055 (NEW_GOAL `(a (HD ul)) IN voronoi_list V (truncate_simplex 1 (ul:(real^3)list))`);
\r
1057 (MATCH_MP_TAC CLOSEST_POINT_IN_SET);
\r
1058 (REWRITE_TAC[Packing3.CLOSED_VORONOI_LIST]);
\r
1059 (MATCH_MP_TAC Packing3.BARV_IMP_VORONOI_LIST_NOT_EMPTY);
\r
1061 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
\r
1063 (ASM_REWRITE_TAC[]);
\r
1066 (* Second estimation *)
\r
1068 (NEW_GOAL `((b:real^3->real^3) (a (HD ul))) IN voronoi_list V (truncate_simplex 2 (ul:(real^3)list))`);
\r
1071 (MATCH_MP_TAC CLOSEST_POINT_IN_SET);
\r
1072 (REWRITE_TAC[Packing3.CLOSED_VORONOI_LIST]);
\r
1073 (MATCH_MP_TAC Packing3.BARV_IMP_VORONOI_LIST_NOT_EMPTY);
\r
1075 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
\r
1077 (ASM_REWRITE_TAC[]);
\r
1080 (* Third estimation *)
\r
1082 (NEW_GOAL `((c:(real^3->real^3))((b:real^3->real^3) (a (HD ul)))) IN voronoi_list V (truncate_simplex 3 (ul:(real^3)list))`);
\r
1084 (MATCH_MP_TAC CLOSEST_POINT_IN_SET);
\r
1085 (REWRITE_TAC[Packing3.CLOSED_VORONOI_LIST]);
\r
1086 (MATCH_MP_TAC Packing3.BARV_IMP_VORONOI_LIST_NOT_EMPTY);
\r
1088 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
\r
1090 (ASM_REWRITE_TAC[]);
\r
1093 (ABBREV_TAC `x:real^3 = (a (HD (ul:(real^3)list)))`);
\r
1094 (ABBREV_TAC `y:real^3 = b (x:real^3)`);
\r
1095 (ABBREV_TAC `z:real^3 = c (y:real^3)`);
\r
1098 (NEW_GOAL `(y:real^3) IN voronoi_list V (truncate_simplex 1 ul)`);
\r
1099 (MATCH_MP_TAC (SET_RULE `(?A. a IN A /\ A SUBSET B) ==> a IN B`));
\r
1100 (EXISTS_TAC `voronoi_list V (truncate_simplex 2 (ul:(real^3)list))`);
\r
1101 (ASM_REWRITE_TAC[VORONOI_LIST;VORONOI_SET]);
\r
1102 (MATCH_MP_TAC (SET_RULE `b SUBSET s ==> (INTERS s) SUBSET (INTERS b)`));
\r
1103 (REWRITE_TAC[SIMPLE_IMAGE]);
\r
1104 (MATCH_MP_TAC IMAGE_SUBSET);
\r
1105 (ASM_REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_1; TRUNCATE_SIMPLEX_EXPLICIT_2]);
\r
1108 (NEW_GOAL `(z:real^3) IN voronoi_list V (truncate_simplex 1 ul)`);
\r
1109 (MATCH_MP_TAC (SET_RULE `(?A. a IN A /\ A SUBSET B) ==> a IN B`));
\r
1110 (EXISTS_TAC `voronoi_list V (truncate_simplex 3 (ul:(real^3)list))`);
\r
1111 (ASM_REWRITE_TAC[VORONOI_LIST;VORONOI_SET]);
\r
1112 (MATCH_MP_TAC (SET_RULE `b SUBSET s ==> (INTERS s) SUBSET (INTERS b)`));
\r
1113 (REWRITE_TAC[SIMPLE_IMAGE]);
\r
1114 (MATCH_MP_TAC IMAGE_SUBSET);
\r
1115 (ASM_REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_1; TRUNCATE_SIMPLEX_EXPLICIT_3]);
\r
1118 (NEW_GOAL `convex hull {x, y, z:real^3} SUBSET (convex hull voronoi_list V (truncate_simplex 1 ul))`);
\r
1119 (MATCH_MP_TAC CONVEX_HULL_SUBSET);
\r
1122 (NEW_GOAL `convex hull voronoi_list V (truncate_simplex 1 (ul:(real^3)list))
\r
1123 = voronoi_list V (truncate_simplex 1 ul)`);
\r
1124 (REWRITE_TAC [CONVEX_HULL_EQ; Packing3.CONVEX_VORONOI_LIST]);
\r
1125 (NEW_GOAL `u0:real^3 IN voronoi_list V (truncate_simplex 1 ul)`);
\r
1126 (REWRITE_WITH `u0:real^3 = HD ul`);
\r
1127 (ASM_MESON_TAC[HD]);
\r
1130 (ASM_REWRITE_TAC[ TRUNCATE_SIMPLEX_EXPLICIT_1; VORONOI_LIST; VORONOI_SET;set_of_list]);
\r
1131 (REWRITE_WITH `INTERS {voronoi_closed V v | v IN {u0, u1:real^3}} =
\r
1132 voronoi_closed V u0 INTER voronoi_closed V u1`);
\r
1136 (REWRITE_TAC[IN_INTER; voronoi_closed; IN; IN_ELIM_THM; INTERS; DIST_REFL]);
\r
1137 (REPEAT STRIP_TAC);
\r
1138 (NEW_GOAL `dist (u0, u1:real^3) <= dist (u0, u0)`);
\r
1139 (FIRST_ASSUM MATCH_MP_TAC);
\r
1140 (ASM_SET_TAC[BARV_IMP_u0_IN_V]);
\r
1141 (NEW_GOAL `u0 = u1:real^3`);
\r
1142 (UP_ASM_TAC THEN REWRITE_TAC[DIST_REFL] THEN DISCH_TAC);
\r
1143 (NEW_GOAL `dist (u0,u1:real^3) = &0`);
\r
1144 (NEW_GOAL `&0 <= dist (u0,u1:real^3) `);
\r
1145 (REWRITE_TAC[DIST_POS_LE]);
\r
1146 (ASM_REAL_ARITH_TAC);
\r
1147 (ASM_MESON_TAC[DIST_EQ_0]);
\r
1148 (NEW_GOAL `aff_dim (set_of_list [u0;u1:real^3]) = &0`);
\r
1149 (ASM_REWRITE_TAC[set_of_list; SET_RULE `{x, x} = {x}`; AFF_DIM_SING]);
\r
1150 (NEW_GOAL `aff_dim (set_of_list [u0;u1:real^3]) = &1`);
\r
1151 (MATCH_MP_TAC MHFTTZN1);
\r
1152 (EXISTS_TAC `V:real^3->bool`);
\r
1153 (ASM_REWRITE_TAC[]);
\r
1154 (REWRITE_WITH `[u1; u1:real^3] = truncate_simplex 1 ul`);
\r
1155 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]);
\r
1156 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
\r
1158 (ASM_REWRITE_TAC[]);
\r
1161 (NEW_GOAL `&0 = &1`);
\r
1162 (ASM_MESON_TAC[INT_OF_NUM_EQ;REAL_OF_NUM_EQ]);
\r
1163 (UP_ASM_TAC THEN REAL_ARITH_TAC)]);;
\r
1165 (* ======================================================================= *)
\r
1167 let RADIAL_VS_RADIAL_NORM = prove_by_refinement (
\r
1168 `!(x:real^3) r C. radial r x C <=> radial_norm r x C`,
\r
1169 [ (REPEAT GEN_TAC);
\r
1170 (REWRITE_TAC[radial; Vol1.radial_norm]);
\r
1171 (REWRITE_WITH `!(x:real^3) r. ball (x, r) = normball x r`);
\r
1172 (REWRITE_TAC[ball; normball; DIST_SYM])]);;
\r
1174 (* ======================================================================= *)
\r
1177 let EVENTUALLY_RADIAL_INTER = prove_by_refinement (
\r
1178 `!(x:real^3) C C'.
\r
1179 eventually_radial x C /\ eventually_radial x C' ==>
\r
1180 eventually_radial x (C INTER C')`,
\r
1181 [ (REWRITE_TAC[eventually_radial; RADIAL_VS_RADIAL_NORM]);
\r
1182 (REWRITE_WITH `!(x:real^3) r. ball (x, r) = normball x r`);
\r
1183 (REWRITE_TAC[ball; normball; DIST_SYM]);
\r
1184 (REPEAT STRIP_TAC);
\r
1185 (ASM_CASES_TAC `r >= r'`);
\r
1186 (EXISTS_TAC `r':real`);
\r
1187 (ASM_REWRITE_TAC[]);
\r
1189 (REWRITE_WITH `(C INTER C') INTER normball (x:real^3) r' =
\r
1190 (C INTER normball x r') INTER (C' INTER normball x r')`);
\r
1192 (MATCH_MP_TAC Vol1.inter_radial);
\r
1193 (ASM_REWRITE_TAC[]);
\r
1194 (UNDISCH_TAC `radial_norm r (x:real^3) (C INTER normball x r)`);
\r
1195 (REWRITE_TAC[Vol1.radial_norm; normball]);
\r
1196 (REPEAT STRIP_TAC);
\r
1197 (REWRITE_TAC[INTER_SUBSET]);
\r
1199 (NEW_GOAL `x + u IN C INTER {y | dist (y,x:real^3) < r}`);
\r
1200 (MATCH_MP_TAC (SET_RULE `(?s. a IN s /\ s SUBSET t) ==> a IN t `));
\r
1201 (EXISTS_TAC `C INTER {y | dist (y,x:real^3) < r'}`);
\r
1202 (ASM_REWRITE_TAC[SUBSET;IN_INTER;IN; IN_ELIM_THM]);
\r
1203 (REPEAT STRIP_TAC);
\r
1204 (ASM_REWRITE_TAC[]);
\r
1205 (ASM_REAL_ARITH_TAC);
\r
1206 (NEW_GOAL `(!t. t > &0 /\ t * norm u < r
\r
1207 ==> x + t % u IN C INTER {y | dist (y,x:real^3) < r})`);
\r
1208 (ASM_MESON_TAC[]);
\r
1209 (NEW_GOAL `x + t % u IN C INTER {y | dist (y,x:real^3) < r}`);
\r
1210 (FIRST_ASSUM MATCH_MP_TAC);
\r
1211 (ASM_REAL_ARITH_TAC);
\r
1212 (UP_ASM_TAC THEN REWRITE_TAC[IN_INTER;IN;IN_ELIM_THM]);
\r
1213 (REPEAT STRIP_TAC);
\r
1214 (ASM_REWRITE_TAC[]);
\r
1215 (REWRITE_TAC[dist; VECTOR_ARITH `((a:real^3) + b) - a = b`; NORM_MUL]);
\r
1216 (REWRITE_WITH `abs t = t`);
\r
1217 (REWRITE_TAC[REAL_ABS_REFL]);
\r
1218 (ASM_REAL_ARITH_TAC);
\r
1219 (ASM_REWRITE_TAC[]);
\r
1221 (EXISTS_TAC `r:real`);
\r
1222 (ASM_REWRITE_TAC[]);
\r
1224 (REWRITE_WITH `(C INTER C') INTER normball (x:real^3) r =
\r
1225 (C INTER normball x r) INTER (C' INTER normball x r)`);
\r
1227 (MATCH_MP_TAC Vol1.inter_radial);
\r
1228 (ASM_REWRITE_TAC[]);
\r
1229 (UNDISCH_TAC `radial_norm r' (x:real^3) (C' INTER normball x r')`);
\r
1230 (REWRITE_TAC[Vol1.radial_norm; normball]);
\r
1231 (REPEAT STRIP_TAC);
\r
1232 (REWRITE_TAC[INTER_SUBSET]);
\r
1234 (NEW_GOAL `x + u IN C' INTER {y | dist (y,x:real^3) < r'}`);
\r
1235 (MATCH_MP_TAC (SET_RULE `(?s. a IN s /\ s SUBSET t) ==> a IN t `));
\r
1236 (EXISTS_TAC `C' INTER {y | dist (y,x:real^3) < r}`);
\r
1237 (ASM_REWRITE_TAC[SUBSET;IN_INTER;IN; IN_ELIM_THM]);
\r
1238 (REPEAT STRIP_TAC);
\r
1239 (ASM_REWRITE_TAC[]);
\r
1240 (ASM_REAL_ARITH_TAC);
\r
1241 (NEW_GOAL `(!t. t > &0 /\ t * norm u < r'
\r
1242 ==> x + t % u IN C' INTER {y | dist (y,x:real^3) < r'})`);
\r
1243 (ASM_MESON_TAC[]);
\r
1244 (NEW_GOAL `x + t % u IN C' INTER {y | dist (y,x:real^3) < r'}`);
\r
1245 (FIRST_ASSUM MATCH_MP_TAC);
\r
1246 (ASM_REAL_ARITH_TAC);
\r
1247 (UP_ASM_TAC THEN REWRITE_TAC[IN_INTER;IN;IN_ELIM_THM]);
\r
1248 (REPEAT STRIP_TAC);
\r
1249 (ASM_REWRITE_TAC[]);
\r
1250 (REWRITE_TAC[dist; VECTOR_ARITH `((a:real^3) + b) - a = b`; NORM_MUL]);
\r
1251 (REWRITE_WITH `abs t = t`);
\r
1252 (REWRITE_TAC[REAL_ABS_REFL]);
\r
1253 (ASM_REAL_ARITH_TAC);
\r
1254 (ASM_REWRITE_TAC[])]);;
\r
1256 (* ======================================================================= *)
\r
1258 let SET_EQ_LEMMA = SET_RULE
\r
1259 `A = B <=> (!x. (x IN A ==> x IN B) /\ (x IN B ==> x IN A))`;;
\r
1261 let SET_OF_0_TO_3 = prove_by_refinement (
\r
1262 `{j | j < 4} = {0,1,2,3}`,
\r
1263 [(REWRITE_TAC[SET_EQ_LEMMA;IN;IN_ELIM_THM] THEN GEN_TAC);
\r
1264 (ASM_CASES_TAC `x = 0`); (ASM_REWRITE_TAC[]);
\r
1265 (TRUONG_SET_TAC[ARITH_RULE `0 < 4`]);
\r
1266 (ASM_CASES_TAC `x = 1`);(ASM_REWRITE_TAC[]);
\r
1267 (TRUONG_SET_TAC[ARITH_RULE `1 < 4`]);
\r
1268 (ASM_CASES_TAC `x = 2`); (ASM_REWRITE_TAC[]);
\r
1269 (TRUONG_SET_TAC[ARITH_RULE `2 < 4`]);
\r
1270 (ASM_CASES_TAC `x = 3`); (ASM_REWRITE_TAC[]);
\r
1271 (TRUONG_SET_TAC[ARITH_RULE `3 < 4`]);
\r
1272 (NEW_GOAL `x >= 4`); (ASM_ARITH_TAC); (REPEAT STRIP_TAC);
\r
1273 (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (NEW_GOAL `F`);
\r
1274 (UP_ASM_TAC THEN TRUONG_SET_TAC[]); (ASM_MESON_TAC[])]);;
\r
1276 let SET_OF_0_TO_2 = prove_by_refinement (
\r
1277 `{j | j <= 2 } = {0,1,2}`,
\r
1278 [(REWRITE_TAC[SET_EQ_LEMMA;IN;IN_ELIM_THM] THEN GEN_TAC);
\r
1279 (ASM_CASES_TAC `x = 0`); (ASM_REWRITE_TAC[]);
\r
1280 (TRUONG_SET_TAC[ARITH_RULE `0 <= 2`]);
\r
1281 (ASM_CASES_TAC `x = 1`);(ASM_REWRITE_TAC[]);
\r
1282 (TRUONG_SET_TAC[ARITH_RULE `1 <= 2`]);
\r
1283 (ASM_CASES_TAC `x = 2`); (ASM_REWRITE_TAC[]);
\r
1284 (TRUONG_SET_TAC[ARITH_RULE `2 <= 2`]);
\r
1285 (NEW_GOAL `x >= 3`); (ASM_ARITH_TAC); (REPEAT STRIP_TAC);
\r
1286 (NEW_GOAL `F`); (ASM_ARITH_TAC); (ASM_MESON_TAC[]); (NEW_GOAL `F`);
\r
1287 (UP_ASM_TAC THEN TRUONG_SET_TAC[]); (ASM_MESON_TAC[])]);;
\r
1289 let ZERO_LT_SQRT_2 = prove_by_refinement(`&1 < sqrt (&2)`,
\r
1290 [(NEW_GOAL `&0 < sqrt (&2)`); (MATCH_MP_TAC SQRT_POS_LT THEN REAL_ARITH_TAC);
\r
1291 (NEW_GOAL `&1 = abs (&1) /\ sqrt (&2) = abs (sqrt (&2))`);
\r
1292 ONCE_REWRITE_TAC[EQ_SYM_EQ]; REWRITE_TAC[REAL_ABS_REFL]; ASM_REAL_ARITH_TAC;
\r
1293 ONCE_ASM_REWRITE_TAC[];
\r
1294 REWRITE_TAC[REAL_LT_SQUARE_ABS; REAL_ARITH `&1 pow 2 = &1`];
\r
1295 REWRITE_WITH `sqrt (&2) pow 2 = &2`; MATCH_MP_TAC SQRT_POW_2;REAL_ARITH_TAC;
\r
1296 REAL_ARITH_TAC]);;
\r
1298 (* ======================================================================= *)
\r
1300 let RCONE_GE_TRANS = prove_by_refinement (
\r
1301 `!(a:real^3) b r x t.
\r
1302 &0 <= t /\ (a + x) IN rcone_ge a b r ==> a + t % x IN rcone_ge a b r`,
\r
1303 [(REWRITE_TAC[rcone_ge; rconesgn; IN; IN_ELIM_THM; dist]);
\r
1304 (REWRITE_TAC[VECTOR_ARITH `((a:real^3) + x) - a = x`; DOT_LMUL; NORM_MUL]);
\r
1305 (REPEAT STRIP_TAC);
\r
1306 (REWRITE_WITH `abs t = t`);
\r
1307 (ASM_REWRITE_TAC[REAL_ABS_REFL]);
\r
1308 (REWRITE_TAC[REAL_ARITH `t * x >= ( t * m) * n <=> &0 <= t * (x - m * n)`]);
\r
1309 (MATCH_MP_TAC REAL_LE_MUL);
\r
1310 (ASM_REAL_ARITH_TAC)]);;
\r
1311 (* ======================================================================= *)
\r
1314 let RCONE_GE_INTERS_PROJECTION_KY_LEMMA = prove_by_refinement (
\r
1315 `!(a:real^3) b r x:real^3.
\r
1316 &0 < r /\ r < &1 /\ ~(a = b) /\
\r
1317 x IN (rcone_ge a b r) INTER (rcone_ge b a r)
\r
1318 ==> (?s. s IN convex hull {a, b} /\ (x - s) dot (a - b)= &0 )`,
\r
1319 [(REWRITE_TAC[rcone_ge; rconesgn; IN_INTER;IN; IN_ELIM_THM; dist]);
\r
1320 (REPEAT STRIP_TAC);
\r
1321 (NEW_GOAL `?s. s IN aff {a, b:real^3} /\ (x - s) dot (a - b) = &0`);
\r
1322 (MESON_TAC[Trigonometry2.EXISTS_PROJECTING_POINT2]);
\r
1323 (FIRST_X_ASSUM CHOOSE_TAC);
\r
1324 (EXISTS_TAC `s:real^3`);
\r
1326 ASM_REWRITE_TAC[Topology.affine_hull_2_fan; IN; IN_ELIM_THM]);
\r
1327 (REPEAT STRIP_TAC);
\r
1328 (ASM_REWRITE_TAC[CONVEX_HULL_2; IN_ELIM_THM]);
\r
1329 (EXISTS_TAC `t1:real`);
\r
1330 (EXISTS_TAC `t2:real`);
\r
1331 (ASM_REWRITE_TAC[]);
\r
1336 (ASM_CASES_TAC `t1 < &0`);
\r
1337 (NEW_GOAL `(x - b:real^3) dot (a - b) < &0`);
\r
1338 (REWRITE_WITH `(x - b:real^3) dot (a - b) =
\r
1339 (x - s) dot (a - b) + (s - b) dot (a - b)`);
\r
1340 (VECTOR_ARITH_TAC);
\r
1341 (ASM_REWRITE_TAC[REAL_ADD_RID; REAL_ADD_LID]);
\r
1342 (REWRITE_WITH `((t1 % a + t2 % b) - b) = t1 % (a - b:real^3)`);
\r
1343 (REWRITE_WITH `((t1 % a + t2 % b) - b:real^3) = (t1 % a + t2 % b) - (t1 + t2) % b`);
\r
1344 (ASM_REWRITE_TAC[VECTOR_MUL_LID]);
\r
1345 (VECTOR_ARITH_TAC);
\r
1346 (REWRITE_TAC[DOT_LMUL]);
\r
1347 (ONCE_REWRITE_TAC[GSYM REAL_LT_NEG]);
\r
1348 (REWRITE_TAC[REAL_ARITH `-- (a * b) = (-- a) * b`; REAL_NEG_0]);
\r
1349 (MATCH_MP_TAC REAL_LT_MUL);
\r
1351 (ASM_REAL_ARITH_TAC);
\r
1352 (REWRITE_TAC[GSYM NORM_POW_2]);
\r
1353 (MATCH_MP_TAC REAL_POW_LT);
\r
1354 (REWRITE_TAC[NORM_POS_LT]);
\r
1355 (ASM_REWRITE_TAC[VECTOR_ARITH `(a:real^3 - b = vec 0 <=> a = b)`]);
\r
1356 (NEW_GOAL `norm (x - b) * norm (a - b:real^3) * r < &0`);
\r
1357 (ASM_REAL_ARITH_TAC);
\r
1358 (NEW_GOAL `&0 <= norm (x - b) * norm (a - b:real^3) * r`);
\r
1359 (MATCH_MP_TAC REAL_LE_MUL);
\r
1360 (REWRITE_TAC[NORM_POS_LE]);
\r
1361 (MATCH_MP_TAC REAL_LE_MUL);
\r
1362 (REWRITE_TAC[NORM_POS_LE]);
\r
1363 (ASM_REAL_ARITH_TAC);
\r
1364 (ASM_REAL_ARITH_TAC);
\r
1365 (ASM_REAL_ARITH_TAC);
\r
1369 (ASM_CASES_TAC `t2 < &0`);
\r
1370 (NEW_GOAL `(x - a:real^3) dot (b - a) < &0`);
\r
1371 (REWRITE_WITH `(x - a:real^3) dot (b - a) =
\r
1372 (a - s) dot (a - b) - (x - s) dot (a - b)`);
\r
1373 (VECTOR_ARITH_TAC);
\r
1374 (ASM_REWRITE_TAC[REAL_ARITH `a - &0 = a`]);
\r
1375 (REWRITE_WITH `a - (t1 % a + t2 % b) = t2 % (a - b:real^3)`);
\r
1376 (REWRITE_WITH `(a:real^3) - (t1 % a + t2 % b) = (t1 + t2) % a - (t1 % a + t2 % b)`);
\r
1378 (ASM_REWRITE_TAC[VECTOR_MUL_LID]);
\r
1379 (VECTOR_ARITH_TAC);
\r
1380 (REWRITE_TAC[DOT_LMUL]);
\r
1381 (ONCE_REWRITE_TAC[GSYM REAL_LT_NEG]);
\r
1382 (REWRITE_TAC[REAL_ARITH `-- (a * b) = (-- a) * b`; REAL_NEG_0]);
\r
1383 (MATCH_MP_TAC REAL_LT_MUL);
\r
1385 (ASM_REAL_ARITH_TAC);
\r
1386 (REWRITE_TAC[GSYM NORM_POW_2]);
\r
1387 (MATCH_MP_TAC REAL_POW_LT);
\r
1388 (REWRITE_TAC[NORM_POS_LT]);
\r
1389 (ASM_REWRITE_TAC[VECTOR_ARITH `(a:real^3 - b = vec 0 <=> a = b)`]);
\r
1390 (NEW_GOAL `norm (x - a) * norm (b - a:real^3) * r < &0`);
\r
1391 (ASM_REAL_ARITH_TAC);
\r
1392 (NEW_GOAL `&0 <= norm (x - a) * norm (b - a:real^3) * r`);
\r
1393 (MATCH_MP_TAC REAL_LE_MUL);
\r
1394 (REWRITE_TAC[NORM_POS_LE]);
\r
1395 (MATCH_MP_TAC REAL_LE_MUL);
\r
1396 (REWRITE_TAC[NORM_POS_LE]);
\r
1397 (ASM_REAL_ARITH_TAC);
\r
1398 (ASM_REAL_ARITH_TAC);
\r
1399 (ASM_REAL_ARITH_TAC);
\r
1401 (ASM_REWRITE_TAC[])]);;
\r
1403 (* ======================================================================= *)
\r
1405 let RCONE_GE_INTER_VORONOI_CLOSED_PROJECTION_KY_LEMMA = prove_by_refinement(
\r
1406 `!(a:real^3) b r x:real^3 V.
\r
1407 &0 < r /\ ~(a = b) /\ a IN V /\ b IN V /\
\r
1408 x IN (rcone_ge a b r) INTER (voronoi_closed V a)
\r
1409 ==> (?s. s IN convex hull {a, b} /\ (x - s) dot (a - b)= &0 )`,
\r
1410 [(REWRITE_TAC[voronoi_closed; rcone_ge; rconesgn; IN_INTER;IN; IN_ELIM_THM; dist]);
\r
1411 (REPEAT STRIP_TAC);
\r
1412 (NEW_GOAL `?s. s IN aff {a, b:real^3} /\ (x - s) dot (a - b) = &0`);
\r
1413 (MESON_TAC[Trigonometry2.EXISTS_PROJECTING_POINT2]);
\r
1414 (FIRST_X_ASSUM CHOOSE_TAC);
\r
1415 (EXISTS_TAC `s:real^3`);
\r
1416 (ASM_REWRITE_TAC[]);
\r
1418 ASM_REWRITE_TAC[Topology.affine_hull_2_fan; IN; IN_ELIM_THM]);
\r
1419 (REPEAT STRIP_TAC);
\r
1420 (ASM_REWRITE_TAC[CONVEX_HULL_2; IN_ELIM_THM]);
\r
1421 (EXISTS_TAC `t1:real`);
\r
1422 (EXISTS_TAC `t2:real`);
\r
1423 (ASM_REWRITE_TAC[]);
\r
1424 (ONCE_REWRITE_TAC[MESON[] `a /\ b <=> b /\ a`]);
\r
1427 (* Case 1 : &0 <= t2 *)
\r
1429 (ASM_CASES_TAC `t2 < &0`);
\r
1430 (NEW_GOAL `(x - a:real^3) dot (b - a) < &0`);
\r
1431 (REWRITE_WITH `(x - a:real^3) dot (b - a) =
\r
1432 (a - s) dot (a - b) - (x - s) dot (a - b)`);
\r
1433 (VECTOR_ARITH_TAC);
\r
1434 (ASM_REWRITE_TAC[REAL_ARITH `a - &0 = a`]);
\r
1435 (REWRITE_WITH `a - (t1 % a + t2 % b) = t2 % (a - b:real^3)`);
\r
1436 (REWRITE_WITH `(a:real^3) - (t1 % a + t2 % b) = (t1 + t2) % a - (t1 % a + t2 % b)`);
\r
1438 (ASM_REWRITE_TAC[VECTOR_MUL_LID]);
\r
1439 (VECTOR_ARITH_TAC);
\r
1440 (REWRITE_TAC[DOT_LMUL]);
\r
1441 (ONCE_REWRITE_TAC[GSYM REAL_LT_NEG]);
\r
1442 (REWRITE_TAC[REAL_ARITH `-- (a * b) = (-- a) * b`; REAL_NEG_0]);
\r
1443 (MATCH_MP_TAC REAL_LT_MUL);
\r
1445 (ASM_REAL_ARITH_TAC);
\r
1446 (REWRITE_TAC[GSYM NORM_POW_2]);
\r
1447 (MATCH_MP_TAC REAL_POW_LT);
\r
1448 (REWRITE_TAC[NORM_POS_LT]);
\r
1449 (ASM_REWRITE_TAC[VECTOR_ARITH `(a:real^3 - b = vec 0 <=> a = b)`]);
\r
1450 (NEW_GOAL `norm (x - a) * norm (b - a:real^3) * r < &0`);
\r
1451 (ASM_REAL_ARITH_TAC);
\r
1452 (NEW_GOAL `&0 <= norm (x - a) * norm (b - a:real^3) * r`);
\r
1453 (MATCH_MP_TAC REAL_LE_MUL);
\r
1454 (REWRITE_TAC[NORM_POS_LE]);
\r
1455 (MATCH_MP_TAC REAL_LE_MUL);
\r
1456 (REWRITE_TAC[NORM_POS_LE]);
\r
1457 (ASM_REAL_ARITH_TAC);
\r
1458 (ASM_REAL_ARITH_TAC);
\r
1459 (ASM_REAL_ARITH_TAC);
\r
1461 (* Case 2 : &0 <= t1 *)
\r
1463 (ASM_CASES_TAC `t1 < &0`);
\r
1464 (NEW_GOAL `norm (x - a) <= norm (x - b:real^3)`);
\r
1466 (NEW_GOAL `norm (x - b) < norm (x - a:real^3)`);
\r
1467 (NEW_GOAL `norm (x - b) < norm (x - a:real^3) <=>
\r
1468 norm (x - b) pow 2 < norm (x - a) pow 2`);
\r
1469 (MATCH_MP_TAC Pack1.bp_bdt);
\r
1470 (REWRITE_TAC[NORM_POS_LE]);
\r
1471 (ASM_REWRITE_TAC[]);
\r
1474 (REWRITE_WITH `norm (x - b) pow 2 = norm (s - b) pow 2 + norm (x - s:real^3) pow 2`);
\r
1475 (MATCH_MP_TAC PYTHAGORAS);
\r
1476 (REWRITE_TAC[orthogonal]);
\r
1477 (REWRITE_WITH `b:real^3 - s = t1 % (b - a)`);
\r
1478 (ASM_REWRITE_TAC[]);
\r
1479 (REWRITE_WITH `b:real^3 - (t1 % a + t2 % b) = (t1 + t2) % b - (t1 % a + t2 % b)`);
\r
1480 (ASM_REWRITE_TAC[VECTOR_MUL_LID]);
\r
1481 (VECTOR_ARITH_TAC);
\r
1482 (REWRITE_TAC[DOT_LMUL]);
\r
1483 (REWRITE_WITH `(b - a:real^3) dot (x - s) = -- ((x - s) dot (a - b))`);
\r
1484 (VECTOR_ARITH_TAC);
\r
1485 (ASM_REWRITE_TAC[]);
\r
1489 (REWRITE_WITH `norm (x - a) pow 2 = norm (s - a) pow 2 + norm (x - s:real^3) pow 2`);
\r
1490 (MATCH_MP_TAC PYTHAGORAS);
\r
1491 (REWRITE_TAC[orthogonal]);
\r
1492 (REWRITE_WITH `a:real^3 - s = t2 % (a - b)`);
\r
1493 (ASM_REWRITE_TAC[]);
\r
1494 (REWRITE_WITH `a:real^3 - (t1 % a + t2 % b) = (t1 + t2) % a - (t1 % a + t2 % b)`);
\r
1495 (ASM_REWRITE_TAC[VECTOR_MUL_LID]);
\r
1496 (VECTOR_ARITH_TAC);
\r
1497 (REWRITE_TAC[DOT_LMUL]);
\r
1498 (REWRITE_WITH `(a - b:real^3) dot (x - s) = ((x - s) dot (a - b))`);
\r
1499 (VECTOR_ARITH_TAC);
\r
1500 (ASM_REWRITE_TAC[]);
\r
1504 (MATCH_MP_TAC (REAL_ARITH `x < y ==> x + z < y + z`));
\r
1505 (REWRITE_TAC[GSYM REAL_LT_SQUARE_ABS]);
\r
1506 (REWRITE_WITH `abs (norm (s - b:real^3)) = norm (s - b)`);
\r
1507 (REWRITE_TAC[REAL_ABS_REFL; NORM_POS_LE]);
\r
1508 (REWRITE_WITH `abs (norm (s - a:real^3)) = norm (s - a)`);
\r
1509 (REWRITE_TAC[REAL_ABS_REFL; NORM_POS_LE]);
\r
1511 (REWRITE_WITH `s:real^3 - a = t2 % (b - a)`);
\r
1512 (ASM_REWRITE_TAC[]);
\r
1513 (REWRITE_WITH `(t1 % a + t2 % b) - a:real^3 = (t1 % a + t2 % b) - (t1 + t2) % a`);
\r
1514 (ASM_REWRITE_TAC[VECTOR_MUL_LID]);
\r
1515 (VECTOR_ARITH_TAC);
\r
1516 (REWRITE_WITH `s:real^3 - b = t1 % (a - b)`);
\r
1517 (ASM_REWRITE_TAC[]);
\r
1518 (REWRITE_WITH `(t1 % a + t2 % b) - b:real^3 = (t1 % a + t2 % b) - (t1 + t2) % b`);
\r
1519 (ASM_REWRITE_TAC[VECTOR_MUL_LID]);
\r
1520 (VECTOR_ARITH_TAC);
\r
1521 (REWRITE_TAC[NORM_MUL; GSYM dist; DIST_SYM]);
\r
1522 (MATCH_MP_TAC (REAL_ARITH `&0 < x * (a - b) ==> b * x < a * x`));
\r
1523 (MATCH_MP_TAC REAL_LT_MUL);
\r
1525 (MATCH_MP_TAC DIST_POS_LT);
\r
1526 (ASM_REWRITE_TAC[]);
\r
1527 (REWRITE_WITH `t2 = &1 - t1`);
\r
1528 (ASM_REAL_ARITH_TAC);
\r
1529 (REWRITE_WITH `abs (t1) = abs (-- t1)`);
\r
1530 (REWRITE_TAC[REAL_ABS_NEG]);
\r
1531 (REWRITE_WITH `abs (&1 - t1) = &1 - t1`);
\r
1532 (REWRITE_TAC[REAL_ABS_REFL]);
\r
1533 (ASM_REAL_ARITH_TAC);
\r
1534 (REWRITE_WITH `abs (-- t1) = (-- t1)`);
\r
1535 (REWRITE_TAC[REAL_ABS_REFL]);
\r
1536 (ASM_REAL_ARITH_TAC);
\r
1537 (ASM_REAL_ARITH_TAC);
\r
1538 (ASM_REAL_ARITH_TAC);
\r
1539 (ASM_REAL_ARITH_TAC)]);;
\r
1541 (* ======================================================================= *)
\r
1543 let RCONEGE_INTER_VORONOI_CLOSED_IMP_RCONEGE = prove_by_refinement(
\r
1544 `!V a:real^3 b r x.
\r
1552 x IN rcone_ge a b r /\
\r
1553 x IN voronoi_closed V a ==> x IN rcone_ge b a r`,
\r
1555 [(REPEAT STRIP_TAC);
\r
1556 (NEW_GOAL `?s. s IN convex hull {a, b:real^3} /\ (x - s) dot (a - b) = &0`);
\r
1557 (MATCH_MP_TAC RCONE_GE_INTER_VORONOI_CLOSED_PROJECTION_KY_LEMMA);
\r
1558 (EXISTS_TAC `r:real`);
\r
1559 (EXISTS_TAC `V:real^3->bool`);
\r
1560 (ASM_REWRITE_TAC[IN_INTER]);
\r
1561 (FIRST_X_ASSUM CHOOSE_TAC);
\r
1562 (UNDISCH_TAC `x IN rcone_ge (a:real^3) b r`);
\r
1563 (REWRITE_TAC[rcone_ge; rconesgn; IN; IN_ELIM_THM; dist]);
\r
1565 (SWITCH_TAC THEN UP_ASM_TAC THEN REWRITE_TAC[CONVEX_HULL_2;IN;IN_ELIM_THM]);
\r
1566 (REPEAT STRIP_TAC);
\r
1570 (NEW_GOAL `((x - (b:real^3)) dot (a - b)) * norm (x - a) >=
\r
1571 ((x - a) dot (b - a)) * norm (x - b)`);
\r
1572 (REWRITE_WITH `(x - b) dot (a - b:real^3) =
\r
1573 (x - s) dot (a - b) + (s - b) dot (a - b)`);
\r
1574 (VECTOR_ARITH_TAC);
\r
1575 (REWRITE_WITH `(x - a) dot (b - a:real^3) =
\r
1576 (a - s) dot (a - b) - (x - s) dot (a - b)`);
\r
1577 (VECTOR_ARITH_TAC);
\r
1578 (ASM_REWRITE_TAC[REAL_ADD_LID; REAL_ARITH `a - &0 = a`]);
\r
1579 (REWRITE_WITH `(u % a + v % b) - b = u % (a - b:real^3)`);
\r
1580 (REWRITE_WITH `(u % a + v % b:real^3) - b = (u % a + v % b) - (u + v) % b`);
\r
1581 (ASM_REWRITE_TAC[VECTOR_MUL_LID]);
\r
1582 (VECTOR_ARITH_TAC);
\r
1584 (REWRITE_WITH `a - (u % a + v % b) = v % (a - b:real^3)`);
\r
1585 (REWRITE_WITH `a - (u % a + v % b:real^3) = (u + v) % a - (u % a + v % b)`);
\r
1586 (ASM_REWRITE_TAC[VECTOR_MUL_LID]);
\r
1587 (VECTOR_ARITH_TAC);
\r
1588 (REWRITE_TAC[DOT_LMUL; GSYM NORM_POW_2; GSYM dist]);
\r
1589 (REWRITE_TAC[REAL_ARITH `(a * x) * y >= (b * x) * z <=> &0 <= x * (a * y - b * z)`]);
\r
1590 (MATCH_MP_TAC REAL_LE_MUL);
\r
1591 (REWRITE_TAC[REAL_LE_POW_2]);
\r
1592 (REWRITE_TAC[REAL_ARITH `&0 <= a - b <=> b <= a`]);
\r
1593 (NEW_GOAL `v * dist (x,b) <= u * dist (x,a:real^3) <=>
\r
1594 (v * dist (x,b)) pow 2 <= (u * dist (x,a)) pow 2`);
\r
1595 (MATCH_MP_TAC Trigonometry2.POW2_COND);
\r
1596 (ASM_SIMP_TAC[REAL_LE_MUL; DIST_POS_LE]);
\r
1597 (ASM_REWRITE_TAC[]);
\r
1598 (REWRITE_TAC[REAL_ARITH `(x * y) pow 2 = (x pow 2) * (y pow 2)`; dist]);
\r
1600 (REWRITE_WITH `norm (x:real^3 - b) pow 2 = norm (s - b) pow 2 + norm (x - s) pow 2`);
\r
1601 (MATCH_MP_TAC PYTHAGORAS);
\r
1602 (REWRITE_TAC[orthogonal]);
\r
1603 (REWRITE_WITH `b - s:real^3 = -- u % (a - b)`);
\r
1604 (ASM_REWRITE_TAC[]);
\r
1605 (REWRITE_WITH `b:real^3 - (u % a + v % b) = (u + v) % b - (u % a + v % b)`);
\r
1606 (ASM_REWRITE_TAC[VECTOR_MUL_LID]);
\r
1607 (VECTOR_ARITH_TAC);
\r
1608 (ASM_MESON_TAC[DOT_LMUL; REAL_MUL_RZERO;DOT_SYM]);
\r
1609 (REWRITE_WITH `norm (s - b:real^3) = norm (b - s)`);
\r
1611 (REWRITE_WITH `b - s:real^3 = -- u % (a - b)`);
\r
1612 (ASM_REWRITE_TAC[]);
\r
1613 (REWRITE_WITH `b:real^3 - (u % a + v % b) = (u + v) % b - (u % a + v % b)`);
\r
1614 (ASM_REWRITE_TAC[VECTOR_MUL_LID]);
\r
1615 (VECTOR_ARITH_TAC);
\r
1616 (REWRITE_TAC[NORM_MUL; REAL_ABS_NEG]);
\r
1618 (REWRITE_WITH `norm (x:real^3 - a) pow 2 = norm (s - a) pow 2 + norm (x - s) pow 2`);
\r
1619 (MATCH_MP_TAC PYTHAGORAS);
\r
1620 (REWRITE_TAC[orthogonal]);
\r
1621 (REWRITE_WITH `a - s:real^3 = v % (a - b)`);
\r
1622 (ASM_REWRITE_TAC[]);
\r
1623 (REWRITE_WITH `a:real^3 - (u % a + v % b) = (u + v) % a - (u % a + v % b)`);
\r
1624 (ASM_REWRITE_TAC[VECTOR_MUL_LID]);
\r
1625 (VECTOR_ARITH_TAC);
\r
1626 (ASM_MESON_TAC[DOT_LMUL; REAL_MUL_RZERO;DOT_SYM]);
\r
1627 (REWRITE_WITH `norm (s - a:real^3) = norm (a - s)`);
\r
1629 (REWRITE_WITH `a - s:real^3 = v % (a - b)`);
\r
1630 (ASM_REWRITE_TAC[]);
\r
1631 (REWRITE_WITH `a:real^3 - (u % a + v % b) = (u + v) % a - (u % a + v % b)`);
\r
1632 (ASM_REWRITE_TAC[VECTOR_MUL_LID]);
\r
1633 (VECTOR_ARITH_TAC);
\r
1634 (REWRITE_TAC[NORM_MUL]);
\r
1636 (REWRITE_TAC[REAL_POW_MUL; REAL_POW2_ABS]);
\r
1637 (REWRITE_TAC[REAL_ARITH `x * (y * z + t) <= y * (x * z + t) <=>
\r
1638 &0 <= t * (y - x)`]);
\r
1639 (MATCH_MP_TAC REAL_LE_MUL);
\r
1640 (REWRITE_TAC[REAL_LE_POW_2]);
\r
1641 (REWRITE_TAC[REAL_ARITH `&0 <= x - y <=> y <= x`]);
\r
1642 (NEW_GOAL `v pow 2 <= u pow 2 <=> v <= u`);
\r
1643 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
\r
1644 (MATCH_MP_TAC Trigonometry2.POW2_COND THEN ASM_REWRITE_TAC[]);
\r
1645 (ASM_REWRITE_TAC[]);
\r
1646 (UNDISCH_TAC `(x:real^3) IN voronoi_closed V a`);
\r
1647 (REWRITE_TAC[voronoi_closed; IN; IN_ELIM_THM]);
\r
1648 (REPEAT STRIP_TAC);
\r
1649 (NEW_GOAL `dist (x,a) <= dist (x,b:real^3)`);
\r
1650 (FIRST_ASSUM MATCH_MP_TAC);
\r
1652 (NEW_GOAL `dist (x,a:real^3) <= dist (x,b) <=>
\r
1653 dist (x,a) pow 2 <= dist (x,b) pow 2`);
\r
1654 (MATCH_MP_TAC Trigonometry2.POW2_COND THEN ASM_REWRITE_TAC[]);
\r
1655 (REWRITE_TAC[DIST_POS_LE]);
\r
1656 (NEW_GOAL `dist (x,a) pow 2 <= dist (x,b:real^3) pow 2`);
\r
1657 (ASM_MESON_TAC[]);
\r
1658 (UP_ASM_TAC THEN REWRITE_TAC[dist]);
\r
1660 (REWRITE_WITH `norm (x:real^3 - a) pow 2 = norm (s - a) pow 2 + norm (x - s) pow 2`);
\r
1661 (MATCH_MP_TAC PYTHAGORAS);
\r
1662 (REWRITE_TAC[orthogonal]);
\r
1663 (REWRITE_WITH `a - s:real^3 = v % (a - b)`);
\r
1664 (ASM_REWRITE_TAC[]);
\r
1665 (REWRITE_WITH `a:real^3 - (u % a + v % b) = (u + v) % a - (u % a + v % b)`);
\r
1666 (ASM_REWRITE_TAC[VECTOR_MUL_LID]);
\r
1667 (VECTOR_ARITH_TAC);
\r
1668 (ASM_MESON_TAC[DOT_LMUL; REAL_MUL_RZERO;DOT_SYM]);
\r
1670 (REWRITE_WITH `norm (s - a:real^3) = norm (a - s)`);
\r
1672 (REWRITE_WITH `a - s:real^3 = v % (a - b)`);
\r
1673 (ASM_REWRITE_TAC[]);
\r
1674 (REWRITE_WITH `a:real^3 - (u % a + v % b) = (u + v) % a - (u % a + v % b)`);
\r
1675 (ASM_REWRITE_TAC[VECTOR_MUL_LID]);
\r
1676 (VECTOR_ARITH_TAC);
\r
1677 (REWRITE_TAC[NORM_MUL]);
\r
1678 (REWRITE_TAC[REAL_POW_MUL; REAL_POW2_ABS]);
\r
1680 (REWRITE_WITH `norm (x:real^3 - b) pow 2 = norm (s - b) pow 2 + norm (x - s) pow 2`);
\r
1681 (MATCH_MP_TAC PYTHAGORAS);
\r
1682 (REWRITE_TAC[orthogonal]);
\r
1683 (REWRITE_WITH `b - s:real^3 = -- u % (a - b)`);
\r
1684 (ASM_REWRITE_TAC[]);
\r
1685 (REWRITE_WITH `b:real^3 - (u % a + v % b) = (u + v) % b - (u % a + v % b)`);
\r
1686 (ASM_REWRITE_TAC[VECTOR_MUL_LID]);
\r
1687 (VECTOR_ARITH_TAC);
\r
1688 (ASM_MESON_TAC[DOT_LMUL; REAL_MUL_RZERO;DOT_SYM]);
\r
1689 (REWRITE_WITH `norm (s - b:real^3) = norm (b - s)`);
\r
1691 (REWRITE_WITH `b - s:real^3 = -- u % (a - b)`);
\r
1692 (ASM_REWRITE_TAC[]);
\r
1693 (REWRITE_WITH `b:real^3 - (u % a + v % b) = (u + v) % b - (u % a + v % b)`);
\r
1694 (ASM_REWRITE_TAC[VECTOR_MUL_LID]);
\r
1695 (VECTOR_ARITH_TAC);
\r
1696 (REWRITE_TAC[NORM_MUL; REAL_ABS_NEG; REAL_POW2_ABS; REAL_POW_MUL]);
\r
1698 (REWRITE_TAC[REAL_ARITH `a * x + b <= c * x + b <=> &0 <= x * (c - a)`]);
\r
1700 (REWRITE_WITH `v <= u <=> v pow 2 <= u pow 2`);
\r
1701 (MATCH_MP_TAC Trigonometry2.POW2_COND);
\r
1702 (ASM_REWRITE_TAC[]);
\r
1703 (ONCE_REWRITE_TAC[REAL_ARITH `a <= b <=> &0 <= b - a`]);
\r
1704 (REWRITE_WITH `&0 <= u pow 2 - v pow 2 <=>
\r
1705 &0 <= norm (a:real^3 - b) pow 2 * (u pow 2 - v pow 2)`);
\r
1706 (NEW_GOAL `(!x y. &0 < x ==> (&0 <= x * y <=> &0 <= y))`);
\r
1707 (MESON_TAC[REAL_LE_MUL_EQ]);
\r
1708 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
\r
1709 (FIRST_X_ASSUM MATCH_MP_TAC);
\r
1710 (MATCH_MP_TAC REAL_POW_LT);
\r
1711 (REWRITE_TAC[NORM_POS_LT]);
\r
1712 (REWRITE_TAC[VECTOR_ARITH `(a - b:real^3) = vec 0 <=> a = b`]);
\r
1713 (ASM_REWRITE_TAC[]);
\r
1714 (ASM_REWRITE_TAC[]);
\r
1717 (* ======================================================================== *)
\r
1719 (ASM_CASES_TAC `&0 < norm (x:real^3 - b)`);
\r
1720 (ASM_CASES_TAC `&0 < norm (x:real^3 - a)`);
\r
1722 (REWRITE_TAC[REAL_ARITH `a >= b * c <=> c * b <= a`]);
\r
1723 (REWRITE_WITH `(norm (a - b) * r) * norm (x - b) <= (x - b) dot (a - b) <=>
\r
1724 (norm (a - b) * r) <= ((x - b) dot (a - b)) / norm (x - b:real^3)`);
\r
1725 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
\r
1726 (MATCH_MP_TAC REAL_LE_RDIV_EQ);
\r
1727 (ASM_REWRITE_TAC[]);
\r
1729 (MATCH_MP_TAC (REAL_ARITH `(?x. a <= x /\ x <= b) ==> a <= b`));
\r
1731 (EXISTS_TAC `((x - a) dot (b - a)) / norm (x - a:real^3)`);
\r
1734 (REWRITE_WITH `norm (a - b) * r <=
\r
1735 ((x - a) dot (b - a)) / norm (x - a) <=>
\r
1736 (norm (a - b) * r) * norm (x - a) <=
\r
1737 ((x - a) dot (b - a:real^3))`);
\r
1738 (MATCH_MP_TAC REAL_LE_RDIV_EQ);
\r
1739 (ASM_REWRITE_TAC[]);
\r
1741 `(norm (a - b:real^3) * r) * norm (x - a) = norm (x - a) * norm (b - a) * r`);
\r
1742 (REWRITE_WITH `norm (a - b) = norm (b - a:real^3)`);
\r
1745 (ASM_REAL_ARITH_TAC);
\r
1747 (NEW_GOAL `((x - a) dot (b - a)) / norm (x - a:real^3) <=
\r
1748 ((x - b) dot (a - b)) / norm (x - b) <=>
\r
1749 ((x - a) dot (b - a)) * norm (x - b) <=
\r
1750 ((x - b) dot (a - b)) * norm (x - a)`);
\r
1751 (MATCH_MP_TAC RAT_LEMMA4);
\r
1752 (ASM_REWRITE_TAC[]);
\r
1753 (ASM_REWRITE_TAC[]);
\r
1754 (ASM_REAL_ARITH_TAC);
\r
1756 (NEW_GOAL `x = a:real^3`);
\r
1757 (ONCE_REWRITE_TAC[VECTOR_ARITH `a = b <=> a - b:real^3 = vec 0`]);
\r
1758 (REWRITE_TAC [GSYM NORM_EQ_0]);
\r
1759 (NEW_GOAL `&0 <= norm (x - a:real^3)`);
\r
1760 (REWRITE_TAC[NORM_POS_LE]);
\r
1761 (ASM_REAL_ARITH_TAC);
\r
1762 (ASM_REWRITE_TAC[GSYM NORM_POW_2]);
\r
1763 (ONCE_REWRITE_TAC[REAL_ARITH `a * a * b = (a pow 2) * b`]);
\r
1764 (REWRITE_TAC[REAL_ARITH `a >= a * b <=> &0 <= (&1 - b) * a`]);
\r
1765 (MATCH_MP_TAC REAL_LE_MUL);
\r
1766 (REWRITE_TAC[REAL_LE_POW_2]);
\r
1767 (ASM_REAL_ARITH_TAC);
\r
1770 (NEW_GOAL `x = b:real^3`);
\r
1771 (ONCE_REWRITE_TAC[VECTOR_ARITH `a = b <=> a - b:real^3 = vec 0`]);
\r
1772 (REWRITE_TAC [GSYM NORM_EQ_0]);
\r
1773 (NEW_GOAL `&0 <= norm (x - b:real^3)`);
\r
1774 (REWRITE_TAC[NORM_POS_LE]);
\r
1775 (ASM_REAL_ARITH_TAC);
\r
1777 (UNDISCH_TAC `x IN voronoi_closed V (a:real^3)`);
\r
1778 (REWRITE_TAC[voronoi_closed;IN;IN_ELIM_THM]);
\r
1780 (NEW_GOAL `dist (x,a) <= dist (x,b:real^3)`);
\r
1781 (FIRST_X_ASSUM MATCH_MP_TAC);
\r
1783 (UP_ASM_TAC THEN ASM_REWRITE_TAC[DIST_REFL]);
\r
1785 (NEW_GOAL `a = b:real^3`);
\r
1786 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
\r
1787 (REWRITE_TAC[GSYM DIST_EQ_0]);
\r
1788 (NEW_GOAL `&0 <= dist (b, a:real^3)`);
\r
1789 (REWRITE_TAC[DIST_POS_LE]);
\r
1790 (ASM_REAL_ARITH_TAC);
\r
1791 (ASM_MESON_TAC[]);
\r
1792 (ASM_MESON_TAC[])]);;
\r
1794 (* ======================================================================= *)
\r
1796 let OMEGA_LIST_1_EXPLICIT_NEW = prove_by_refinement (
\r
1797 `!a:real^3 b c d V ul.
\r
1801 ul = [a; b; c; d] /\
\r
1802 hl [a;b] < sqrt (&2)
\r
1803 ==> omega_list_n V ul 1 = circumcenter {a, b}`,
\r
1804 [ (REPEAT STRIP_TAC);
\r
1805 (REWRITE_WITH `{a,b} = set_of_list [a;(b:real^3)]`);
\r
1806 (MESON_TAC[set_of_list]);
\r
1807 (REWRITE_WITH `circumcenter (set_of_list [a; b:real^3]) = omega_list V [a:real^3; b]`);
\r
1808 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
\r
1809 (MATCH_MP_TAC XNHPWAB1);
\r
1811 (ASM_REWRITE_TAC[ARITH_RULE `1 <= 3`]);
\r
1812 (MP_TAC (ASSUME `ul IN barV V 3`) THEN REWRITE_TAC[IN;BARV]);
\r
1814 (REPEAT STRIP_TAC);
\r
1815 (REWRITE_TAC[LENGTH;ARITH_RULE `SUC (SUC 0) = 1 + 1`]);
\r
1816 (NEW_GOAL `initial_sublist vl (ul:(real^3)list)`);
\r
1817 (UNDISCH_TAC `initial_sublist vl [a:real^3; b]`);
\r
1818 (REWRITE_TAC[INITIAL_SUBLIST] THEN STRIP_TAC);
\r
1819 (EXISTS_TAC `APPEND yl [c;d:real^3]`);
\r
1820 (REWRITE_TAC[APPEND_ASSOC; GSYM (ASSUME `[a:real^3; b] = APPEND vl yl`)]);
\r
1821 (ASM_REWRITE_TAC[APPEND]);
\r
1822 (ASM_MESON_TAC[]);
\r
1823 (ASM_REWRITE_TAC[OMEGA_LIST_TRUNCATE_1])]);;
\r
1825 (* ======================================================================= *)
\r
1827 let IN_SET_IMP_IN_CONVEX_HULL_SET = prove_by_refinement (
\r
1828 `!a S:real^3->bool. a IN S ==> a IN convex hull S`,
\r
1829 [(REPEAT STRIP_TAC);
\r
1830 (REWRITE_TAC[SET_RULE `a IN s <=> {a} SUBSET s`]);
\r
1831 (NEW_GOAL `{a} = convex hull ({a:real^3})`);
\r
1832 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
\r
1833 (SIMP_TAC[CONVEX_HULL_EQ;CONVEX_SING]);
\r
1834 (ONCE_ASM_REWRITE_TAC[]);
\r
1835 (MATCH_MP_TAC CONVEX_HULL_SUBSET);
\r
1836 (ASM_SET_TAC[])]);;
\r
1838 (* ======================================================================= *)
\r
1840 let CONVEX_HULL_BREAK_KY_LEMMA = prove_by_refinement (
\r
1841 `!a:real^3 b c d x. between x (a,b) ==>
\r
1842 (convex hull {a,b,c,d} = convex hull {a,x, c,d} UNION convex hull {x,b,c,d})`,
\r
1844 [(REWRITE_TAC[BETWEEN_IN_CONVEX_HULL; CONVEX_HULL_2;IN; IN_ELIM_THM]);
\r
1845 (REWRITE_TAC[SET_EQ_LEMMA]);
\r
1846 (REPEAT STRIP_TAC);
\r
1847 (UP_ASM_TAC THEN REWRITE_TAC[CONVEX_HULL_4; IN_UNION;IN;IN_ELIM_THM]);
\r
1848 (REPEAT STRIP_TAC);
\r
1849 (ASM_CASES_TAC `u = &0`);
\r
1851 (EXISTS_TAC `u':real`);
\r
1852 (EXISTS_TAC `v':real`);
\r
1853 (EXISTS_TAC `w:real`);
\r
1854 (EXISTS_TAC `z:real`);
\r
1855 (ASM_REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_LID]);
\r
1856 (REWRITE_WITH `v = &1`);
\r
1857 (ASM_REAL_ARITH_TAC);
\r
1858 (VECTOR_ARITH_TAC);
\r
1859 (NEW_GOAL `&0 < u `);
\r
1860 (ASM_REAL_ARITH_TAC);
\r
1861 (SWITCH_TAC THEN DEL_TAC);
\r
1862 (ASM_CASES_TAC `v = &0`);
\r
1864 (EXISTS_TAC `u':real`);
\r
1865 (EXISTS_TAC `v':real`);
\r
1866 (EXISTS_TAC `w:real`);
\r
1867 (EXISTS_TAC `z:real`);
\r
1868 (ASM_REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_LID]);
\r
1869 (REWRITE_WITH `u = &1`);
\r
1870 (ASM_REAL_ARITH_TAC);
\r
1871 (VECTOR_ARITH_TAC);
\r
1872 (NEW_GOAL `&0 < v `);
\r
1873 (ASM_REAL_ARITH_TAC);
\r
1874 (SWITCH_TAC THEN DEL_TAC);
\r
1877 (ASM_CASES_TAC `&0 < u' + v'`);
\r
1878 (ASM_CASES_TAC `u' / (u' + v') <= u`);
\r
1882 (EXISTS_TAC `u' / u`);
\r
1883 (EXISTS_TAC `v' - v * (u'/ u)`);
\r
1884 (EXISTS_TAC `w:real`);
\r
1885 (EXISTS_TAC `z:real`);
\r
1886 (ASM_REWRITE_TAC[]);
\r
1887 (ASM_SIMP_TAC[REAL_LE_DIV]);
\r
1888 (REPEAT STRIP_TAC);
\r
1889 (REWRITE_WITH `v' - v * u' / u = (v' * u - v * u' )/ u`);
\r
1890 (REWRITE_TAC[REAL_ARITH `(a - b * d) / c = a / c - b * d / c`]);
\r
1891 (AP_THM_TAC THEN AP_TERM_TAC);
\r
1892 (REWRITE_WITH `v' = (v' * u) / u <=> v' * u = (v' * u)`);
\r
1893 (MATCH_MP_TAC REAL_EQ_RDIV_EQ);
\r
1894 (ASM_REWRITE_TAC[]);
\r
1895 (REWRITE_WITH `v * u' = u' - u * u'`);
\r
1896 (REWRITE_TAC[REAL_ARITH `a * b = b - c * b <=> ((c + a) - &1) * b = &0`]);
\r
1897 (ASM_REWRITE_TAC[]);
\r
1899 (REWRITE_TAC[REAL_ARITH `v' * u - (u' - u * u') = u * (u' + v') - u'`]);
\r
1900 (MATCH_MP_TAC REAL_LE_DIV);
\r
1901 (ASM_REWRITE_TAC[REAL_ARITH `&0 <= a - b <=> b <= a`]);
\r
1902 (NEW_GOAL `u' <= u * (u' + v') <=> u' / (u' + v') <= u`);
\r
1903 (ASM_MESON_TAC[REAL_LE_LDIV_EQ]);
\r
1904 (ONCE_ASM_REWRITE_TAC[]);
\r
1905 (ASM_MESON_TAC[]);
\r
1907 (REWRITE_TAC[REAL_ARITH `a + b - e + c + d = (a + b - e) + c + d`]);
\r
1908 (REWRITE_WITH `u' / u + v' - v * u' / u = u' + v'`);
\r
1909 (ONCE_REWRITE_TAC[REAL_ARITH `a/x + b - m*e/x = c + b <=> (a - m*e)/x = c`]);
\r
1910 (NEW_GOAL `(u' - v * u') / u = u' <=> (u' - v * u') = u' * u`);
\r
1911 (MATCH_MP_TAC REAL_EQ_LDIV_EQ);
\r
1912 (ASM_REWRITE_TAC[]);
\r
1913 (ONCE_ASM_REWRITE_TAC[]);
\r
1914 (REWRITE_WITH `u' - v * u' = u' * (u + v) - v * u'`);
\r
1915 (ASM_REWRITE_TAC[]);
\r
1917 (ASM_REAL_ARITH_TAC);
\r
1918 (ASM_REAL_ARITH_TAC);
\r
1919 (REWRITE_TAC[VECTOR_ADD_LDISTRIB;VECTOR_MUL_ASSOC]);
\r
1920 (REWRITE_TAC[VECTOR_ARITH `a + b + c + d = (x + m % y) + n % y + c + d <=>
\r
1921 (a - x) + (b - (m + n) % y) = vec 0 `]);
\r
1923 (MATCH_MP_TAC (VECTOR_ARITH `a = vec 0 /\ b = vec 0 ==> a + b = vec 0`));
\r
1925 (REWRITE_TAC[VECTOR_ARITH
\r
1926 `(x % a - y % a = vec 0) <=> (x - y) % a = vec 0`; VECTOR_MUL_EQ_0]);
\r
1928 (REWRITE_TAC[REAL_ARITH `x - y / z * t = &0 <=> (y * t) / z = x`]);
\r
1929 (NEW_GOAL `(u' * u) / u = u' <=> (u' * u) = u' * u`);
\r
1930 (MATCH_MP_TAC REAL_EQ_LDIV_EQ);
\r
1931 (ASM_REWRITE_TAC[]);
\r
1932 (ONCE_ASM_REWRITE_TAC[]);
\r
1935 (REWRITE_TAC[VECTOR_ARITH
\r
1936 `(x % a - y % a = vec 0) <=> (x - y) % a = vec 0`; VECTOR_MUL_EQ_0]);
\r
1943 (NEW_GOAL `v' / (u' + v') <= v`);
\r
1944 (REWRITE_WITH `v' / (u' + v') = &1 - u' /(u' + v')`);
\r
1945 (REWRITE_TAC[REAL_ARITH `a / x = &1 - b / x <=> (b + a) / x = &1`]);
\r
1946 (MATCH_MP_TAC REAL_DIV_REFL);
\r
1947 (ASM_REAL_ARITH_TAC);
\r
1948 (ASM_REAL_ARITH_TAC);
\r
1951 (EXISTS_TAC `u' - u * (v'/ v)`);
\r
1952 (EXISTS_TAC `v' / v`);
\r
1953 (EXISTS_TAC `w:real`);
\r
1954 (EXISTS_TAC `z:real`);
\r
1955 (ASM_REWRITE_TAC[]);
\r
1956 (ASM_SIMP_TAC[REAL_LE_DIV]);
\r
1957 (REPEAT STRIP_TAC);
\r
1959 (REWRITE_WITH `u' - u * v' / v = (u' * v - u * v' )/ v`);
\r
1960 (REWRITE_TAC[REAL_ARITH `(a - b * d) / c = a / c - b * d / c`]);
\r
1961 (AP_THM_TAC THEN AP_TERM_TAC);
\r
1962 (REWRITE_WITH `u' = (u' * v) / v <=> u' * v = (u' * v)`);
\r
1963 (MATCH_MP_TAC REAL_EQ_RDIV_EQ);
\r
1964 (ASM_REWRITE_TAC[]);
\r
1966 (REWRITE_WITH `u * v' = v' - v * v'`);
\r
1967 (REWRITE_TAC[REAL_ARITH `a * b = b - c * b <=> ((c + a) - &1) * b = &0`]);
\r
1968 (ASM_REWRITE_TAC[REAL_ARITH `v + u = u + v`]);
\r
1969 (ASM_REAL_ARITH_TAC);
\r
1970 (REWRITE_TAC[REAL_ARITH `v' * u - (u' - u * u') = u * (u' + v') - u'`]);
\r
1971 (MATCH_MP_TAC REAL_LE_DIV);
\r
1972 (ASM_REWRITE_TAC[REAL_ARITH `&0 <= a - b <=> b <= a`]);
\r
1974 (NEW_GOAL `v' <= v * (v' + u') <=> v' / (v' + u') <= v`);
\r
1975 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
\r
1976 (MATCH_MP_TAC REAL_LE_LDIV_EQ);
\r
1977 (ASM_REAL_ARITH_TAC);
\r
1978 (ONCE_ASM_REWRITE_TAC[]);
\r
1979 (ASM_MESON_TAC[REAL_ADD_SYM]);
\r
1981 (REWRITE_TAC[REAL_ARITH `a - e + b + c + d = (a + b - e) + c + d`]);
\r
1982 (REWRITE_WITH `u' + v' / v - u * v' / v = u' + v'`);
\r
1984 (ONCE_REWRITE_TAC[REAL_ARITH `b + a/x - m*e/x = b + c <=> (a - m*e)/x = c`]);
\r
1985 (NEW_GOAL `(v' - u * v') / v = v' <=> (v' - u * v') = v' * v`);
\r
1986 (MATCH_MP_TAC REAL_EQ_LDIV_EQ);
\r
1987 (ASM_REWRITE_TAC[]);
\r
1988 (ONCE_ASM_REWRITE_TAC[]);
\r
1989 (REWRITE_WITH `v' - u * v' = v' * (u + v) - u * v'`);
\r
1990 (ASM_REWRITE_TAC[]);
\r
1992 (ASM_REAL_ARITH_TAC);
\r
1993 (ASM_REAL_ARITH_TAC);
\r
1994 (REWRITE_TAC[VECTOR_ADD_LDISTRIB;VECTOR_MUL_ASSOC]);
\r
1995 (REWRITE_TAC[VECTOR_ARITH `a + b + c + d = (m % y) + (n % y + z) + c + d <=> (b - z) + (a - (m + n) % y) = vec 0 `]);
\r
1997 (MATCH_MP_TAC (VECTOR_ARITH `a = vec 0 /\ b = vec 0 ==> b + a = vec 0`));
\r
2000 (REWRITE_TAC[VECTOR_ARITH
\r
2001 `(x % a - y % a = vec 0) <=> (x - y) % a = vec 0`; VECTOR_MUL_EQ_0]);
\r
2004 (REWRITE_TAC[VECTOR_ARITH
\r
2005 `(x % a - y % a = vec 0) <=> (x - y) % a = vec 0`; VECTOR_MUL_EQ_0]);
\r
2008 (REWRITE_TAC[REAL_ARITH `x - y / z * t = &0 <=> (y * t) / z = x`]);
\r
2009 (NEW_GOAL `(v' * v) / v = v' <=> (v' * v) = v' * v`);
\r
2010 (MATCH_MP_TAC REAL_EQ_LDIV_EQ);
\r
2011 (ASM_REWRITE_TAC[]);
\r
2012 (ONCE_ASM_REWRITE_TAC[]);
\r
2017 (NEW_GOAL `u' + v' = &0`);
\r
2018 (ASM_REAL_ARITH_TAC);
\r
2020 (EXISTS_TAC `&0` THEN EXISTS_TAC `&0`);
\r
2021 (EXISTS_TAC `w:real` THEN EXISTS_TAC `z:real`);
\r
2022 (NEW_GOAL `u'= &0 /\ v' = &0`);
\r
2023 (ASM_REAL_ARITH_TAC);
\r
2024 (UNDISCH_TAC `x' = u' % a + v' % b + w % c + z % (d:real^3)`);
\r
2025 (ASM_REWRITE_TAC[VECTOR_MUL_LZERO; REAL_ARITH `&0 <= &0`]);
\r
2026 (REPEAT STRIP_TAC);
\r
2027 (ASM_MESON_TAC[]);
\r
2028 (ASM_MESON_TAC[]);
\r
2030 (* ================================ *)
\r
2032 (UP_ASM_TAC THEN REWRITE_TAC[IN_UNION]);
\r
2033 (REPEAT STRIP_TAC);
\r
2035 (NEW_GOAL `convex hull {a, x, c, d} SUBSET convex hull {a, b, c, d:real^3}`);
\r
2036 (NEW_GOAL `convex hull {a, b, c, d:real^3} =
\r
2037 convex hull (convex hull {a, b, c, d:real^3})`);
\r
2038 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
\r
2039 (REWRITE_TAC[CONVEX_HULL_EQ; CONVEX_CONVEX_HULL]);
\r
2040 (ONCE_ASM_REWRITE_TAC[]);
\r
2041 (MATCH_MP_TAC CONVEX_HULL_SUBSET);
\r
2042 (ONCE_REWRITE_TAC[SUBSET; IN;IN_ELIM_THM]);
\r
2043 (REPEAT STRIP_TAC);
\r
2044 (ASM_CASES_TAC `x'' = a:real^3`);
\r
2045 (MATCH_MP_TAC IN_SET_IMP_IN_CONVEX_HULL_SET);
\r
2047 (ASM_CASES_TAC `x'' = d:real^3`);
\r
2048 (MATCH_MP_TAC IN_SET_IMP_IN_CONVEX_HULL_SET);
\r
2050 (ASM_CASES_TAC `x'' = c:real^3`);
\r
2051 (MATCH_MP_TAC IN_SET_IMP_IN_CONVEX_HULL_SET);
\r
2053 (NEW_GOAL `x'' = u % a + v % (b:real^3)`);
\r
2055 (ASM_REWRITE_TAC[]);
\r
2056 (MATCH_MP_TAC (SET_RULE `(?s. p IN s /\ s SUBSET r) ==> p IN r`));
\r
2057 (EXISTS_TAC `convex hull {a, b:real^3}`);
\r
2059 (ASM_REWRITE_TAC[CONVEX_HULL_2; IN; IN_ELIM_THM]);
\r
2060 (EXISTS_TAC `u:real` THEN EXISTS_TAC `v:real`);
\r
2061 (ASM_REWRITE_TAC[]);
\r
2062 (MATCH_MP_TAC CONVEX_HULL_SUBSET);
\r
2068 (NEW_GOAL `convex hull {x, b, c, d} SUBSET convex hull {a, b, c, d:real^3}`);
\r
2069 (NEW_GOAL `convex hull {a, b, c, d:real^3} =
\r
2070 convex hull (convex hull {a, b, c, d:real^3})`);
\r
2071 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
\r
2072 (REWRITE_TAC[CONVEX_HULL_EQ; CONVEX_CONVEX_HULL]);
\r
2073 (ONCE_ASM_REWRITE_TAC[]);
\r
2074 (MATCH_MP_TAC CONVEX_HULL_SUBSET);
\r
2075 (ONCE_REWRITE_TAC[SUBSET; IN;IN_ELIM_THM]);
\r
2076 (REPEAT STRIP_TAC);
\r
2077 (ASM_CASES_TAC `x'' = b:real^3`);
\r
2078 (MATCH_MP_TAC IN_SET_IMP_IN_CONVEX_HULL_SET);
\r
2080 (ASM_CASES_TAC `x'' = d:real^3`);
\r
2081 (MATCH_MP_TAC IN_SET_IMP_IN_CONVEX_HULL_SET);
\r
2083 (ASM_CASES_TAC `x'' = c:real^3`);
\r
2084 (MATCH_MP_TAC IN_SET_IMP_IN_CONVEX_HULL_SET);
\r
2086 (NEW_GOAL `x'' = u % a + v % (b:real^3)`);
\r
2088 (ASM_REWRITE_TAC[]);
\r
2089 (MATCH_MP_TAC (SET_RULE `(?s. p IN s /\ s SUBSET r) ==> p IN r`));
\r
2090 (EXISTS_TAC `convex hull {a, b:real^3}`);
\r
2092 (ASM_REWRITE_TAC[CONVEX_HULL_2; IN; IN_ELIM_THM]);
\r
2093 (EXISTS_TAC `u:real` THEN EXISTS_TAC `v:real`);
\r
2094 (ASM_REWRITE_TAC[]);
\r
2095 (MATCH_MP_TAC CONVEX_HULL_SUBSET);
\r
2097 (ASM_SET_TAC[])]);;
\r
2099 (* ======================================================================= *)
\r
2101 let AFF_GE_BREAK_KY_LEMMA = prove_by_refinement (
\r
2102 `!a b c d (x:real^3).
\r
2103 between x (c, d) /\
\r
2104 DISJOINT {a, b} {c, d} /\
\r
2105 DISJOINT {a, b} {c, x} /\
\r
2106 DISJOINT {a, b} {x, d} ==>
\r
2107 aff_ge {a, b} {c, d} = aff_ge {a, b} {c, x} UNION aff_ge {a, b} {x, d}`,
\r
2108 [(REWRITE_TAC[BETWEEN_IN_CONVEX_HULL; CONVEX_HULL_2; IN; IN_ELIM_THM]);
\r
2109 (REPEAT STRIP_TAC);
\r
2111 (ASM_SIMP_TAC[AFF_GE_2_2]);
\r
2112 (REWRITE_TAC[SET_EQ_LEMMA; IN_UNION; IN; IN_ELIM_THM]);
\r
2113 (REPEAT STRIP_TAC);
\r
2115 (* Break to 3 subgoal *)
\r
2117 (ASM_CASES_TAC `u = &0`);
\r
2118 (REWRITE_WITH `v = &1`);
\r
2119 (ASM_REAL_ARITH_TAC);
\r
2120 (ASM_REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_LID; VECTOR_MUL_LID]);
\r
2123 (EXISTS_TAC `t1:real` THEN EXISTS_TAC `t2:real`);
\r
2124 (EXISTS_TAC `t3:real` THEN EXISTS_TAC `t4:real`);
\r
2125 (ASM_REWRITE_TAC[]);
\r
2126 (NEW_GOAL `&0 <u `);
\r
2127 (ASM_REAL_ARITH_TAC);
\r
2128 (ASM_CASES_TAC `v = &0`);
\r
2129 (REWRITE_WITH `u = &1`);
\r
2130 (ASM_REAL_ARITH_TAC);
\r
2131 (ASM_REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_RID; VECTOR_MUL_LID]);
\r
2133 (EXISTS_TAC `t1:real` THEN EXISTS_TAC `t2:real`);
\r
2134 (EXISTS_TAC `t3:real` THEN EXISTS_TAC `t4:real`);
\r
2135 (ASM_REWRITE_TAC[]);
\r
2136 (NEW_GOAL `&0 < v `);
\r
2137 (ASM_REAL_ARITH_TAC);
\r
2139 (ASM_CASES_TAC `&0 < t3 + t4`);
\r
2140 (ASM_CASES_TAC `v * (t3 + t4) >= t4`);
\r
2142 (EXISTS_TAC `t1:real` THEN EXISTS_TAC `t2:real`);
\r
2143 (EXISTS_TAC `t3 - u * t4 / v` THEN EXISTS_TAC `t4 / v`);
\r
2144 (REPEAT STRIP_TAC);
\r
2145 (REWRITE_TAC[REAL_ARITH `&0 <= a - b * c / d <=> (b * c) / d <= a `]);
\r
2146 (REWRITE_WITH `(u * t4) / v <= t3 <=> (u * t4) <= t3 * v`);
\r
2147 (MATCH_MP_TAC REAL_LE_LDIV_EQ);
\r
2148 (ASM_REWRITE_TAC[]);
\r
2149 (REWRITE_WITH `u * t4 <= t3 * v <=> v * (t3 + t4) >= t4`);
\r
2150 (REWRITE_WITH `v * (t3 + t4) >= t4 <=> v * (t3 + t4) >= t4 * (u + v)`);
\r
2151 (ASM_REWRITE_TAC[REAL_MUL_RID]);
\r
2153 (ASM_REWRITE_TAC[]);
\r
2154 (MATCH_MP_TAC REAL_LE_DIV);
\r
2155 (ASM_REAL_ARITH_TAC);
\r
2156 (REWRITE_WITH `t1 + t2 + t3 - u * t4 / v + t4 / v = t1 + t2 + t3 + t4`);
\r
2157 (REPEAT AP_TERM_TAC);
\r
2158 (REWRITE_TAC[REAL_ARITH
\r
2159 `t3 - u * t4 / v + t4 / v = t3 + t4 <=> (t4 - t4 * u) / v = t4`]);
\r
2161 (REWRITE_WITH `(t4 - t4 * u) / v = t4 <=> (t4 - t4 * u) = t4 * v`);
\r
2162 (MATCH_MP_TAC REAL_EQ_LDIV_EQ);
\r
2163 (ASM_REAL_ARITH_TAC);
\r
2164 (REWRITE_WITH `(t4 - t4 * u) = t4 * (u + v) - t4 * u`);
\r
2165 (ASM_REWRITE_TAC[REAL_MUL_RID]);
\r
2167 (ASM_REWRITE_TAC[]);
\r
2170 `t1 % a + t2 % b + (t3 - u * t4 / v) % c + t4 / v % (u % c + v % d) =
\r
2171 t1 % a + t2 % b + t3 % c + t4 % (d:real^3)`);
\r
2172 (REPEAT AP_TERM_TAC);
\r
2174 (REWRITE_TAC[VECTOR_SUB_RDISTRIB; VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC]);
\r
2175 (REWRITE_TAC[VECTOR_ARITH
\r
2176 `(x % c - y % c + t % c + z % d = x % c + n % d) <=>
\r
2177 (t - y) % c + (z - n) %d = vec 0`]);
\r
2178 (REWRITE_WITH `t4 / v * u - u * t4 / v = &0`);
\r
2180 (REWRITE_WITH `t4 / v * v - t4 = &0`);
\r
2181 (REWRITE_TAC[REAL_ARITH `a / b * c - d = &0 <=> (a * c) / b = d`]);
\r
2182 (REWRITE_WITH `(t4 * v) / v = t4 <=> (t4 * v) = t4 * v`);
\r
2183 (MATCH_MP_TAC REAL_EQ_LDIV_EQ);
\r
2184 (ASM_REWRITE_TAC[]);
\r
2185 (VECTOR_ARITH_TAC);
\r
2186 (ASM_REWRITE_TAC[]);
\r
2188 (ASM_CASES_TAC `(u * (t3 + t4) >= t3)`);
\r
2190 (EXISTS_TAC `t1:real` THEN EXISTS_TAC `t2:real`);
\r
2191 (EXISTS_TAC `t3 / u` THEN EXISTS_TAC `t4 - v * t3 / u`);
\r
2192 (REPEAT STRIP_TAC);
\r
2193 (MATCH_MP_TAC REAL_LE_DIV);
\r
2194 (ASM_REAL_ARITH_TAC);
\r
2196 (REWRITE_TAC[REAL_ARITH `&0 <= a - b * c / d <=> (b * c) / d <= a `]);
\r
2197 (REWRITE_WITH `(v * t3) / u <= t4 <=> (v * t3) <= t4 * u`);
\r
2198 (MATCH_MP_TAC REAL_LE_LDIV_EQ);
\r
2199 (ASM_REWRITE_TAC[]);
\r
2200 (REWRITE_WITH `v * t3 <= t4 * u <=> u * (t3 + t4) >= t3`);
\r
2201 (REWRITE_WITH `u * (t3 + t4) >= t3 <=> u * (t3 + t4) >= t3 * (u + v)`);
\r
2202 (ASM_REWRITE_TAC[REAL_MUL_RID]);
\r
2204 (ASM_REWRITE_TAC[]);
\r
2206 (REWRITE_WITH `t1 + t2 + t3 / u + t4 - v * t3 / u = t1 + t2 + t3 + t4`);
\r
2207 (REPEAT AP_TERM_TAC);
\r
2208 (REWRITE_TAC[REAL_ARITH
\r
2209 `t3 / u + t4 - v * t3 / u = t3 + t4 <=> (t3 - t3 * v) / u = t3`]);
\r
2211 (REWRITE_WITH `(t3 - t3 * v) / u = t3 <=> (t3 - t3 * v) = t3 * u`);
\r
2212 (MATCH_MP_TAC REAL_EQ_LDIV_EQ);
\r
2213 (ASM_REAL_ARITH_TAC);
\r
2214 (REWRITE_WITH `(t3 - t3 * v) = t3 * (u + v) - t3 * v`);
\r
2215 (ASM_REWRITE_TAC[REAL_MUL_RID]);
\r
2217 (ASM_REWRITE_TAC[]);
\r
2220 `t1 % a + t2 % b + t3 / u % (u % c + v % d) + (t4 - v * t3 / u) % d =
\r
2221 t1 % a + t2 % b + t3 % c + t4 % (d:real^3)`);
\r
2222 (REPEAT AP_TERM_TAC);
\r
2224 (REWRITE_TAC[VECTOR_SUB_RDISTRIB; VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC]);
\r
2225 (REWRITE_TAC[VECTOR_ARITH
\r
2226 `(x % c + y % d) + a - z % d = t % c + a <=>
\r
2227 (x - t) % c + (y - z) %d = vec 0`]);
\r
2228 (REWRITE_WITH `t3 / u * v - v * t3 / u = &0`);
\r
2230 (REWRITE_WITH `t3 / u * u - t3 = &0`);
\r
2231 (REWRITE_TAC[REAL_ARITH `a / b * c - d = &0 <=> (a * c) / b = d`]);
\r
2232 (REWRITE_WITH `(t3 * u) / u = t3 <=> (t3 * u) = t3 * u`);
\r
2233 (MATCH_MP_TAC REAL_EQ_LDIV_EQ);
\r
2234 (ASM_REWRITE_TAC[]);
\r
2235 (VECTOR_ARITH_TAC);
\r
2236 (ASM_REWRITE_TAC[]);
\r
2238 (NEW_GOAL `v * (t3 + t4) < t4 /\ u * (t3 + t4) < t3`);
\r
2239 (ASM_REAL_ARITH_TAC);
\r
2240 (NEW_GOAL `(u + v) * (t3 + t4) < (t3 + t4)`);
\r
2241 (ASM_REAL_ARITH_TAC);
\r
2242 (UP_ASM_TAC THEN ASM_REWRITE_TAC[REAL_MUL_LID]);
\r
2244 (UP_ASM_TAC THEN MESON_TAC[]);
\r
2245 (NEW_GOAL `t3 = &0 /\ t4 = &0`);
\r
2246 (ASM_REAL_ARITH_TAC);
\r
2248 (EXISTS_TAC `t1:real` THEN EXISTS_TAC `t2:real`);
\r
2249 (EXISTS_TAC `t3:real` THEN EXISTS_TAC `t4:real`);
\r
2250 (ASM_REWRITE_TAC[VECTOR_MUL_LZERO]);
\r
2251 (* finish the first subgoal *)
\r
2253 (EXISTS_TAC `t1:real` THEN EXISTS_TAC `t2:real`);
\r
2254 (EXISTS_TAC `t3 + t4 * u` THEN EXISTS_TAC `t4 * v`);
\r
2255 (REPEAT STRIP_TAC);
\r
2256 (MATCH_MP_TAC REAL_LE_ADD);
\r
2257 (ASM_SIMP_TAC[REAL_LE_MUL]);
\r
2258 (ASM_SIMP_TAC[REAL_LE_MUL]);
\r
2259 (REWRITE_WITH `t1 + t2 + (t3 + t4 * u) + t4 * v =
\r
2260 t1 + t2 + t3 + t4 * (u + v)`);
\r
2262 (ASM_REWRITE_TAC[REAL_MUL_RID]);
\r
2263 (REWRITE_WITH `t1 % a + t2 % b + (t3 + t4 * u) % c + (t4 * v) % d =
\r
2264 t1 % a + t2 % b + t3 % c + t4 % (u % c + v % (d:real^3))`);
\r
2265 (VECTOR_ARITH_TAC);
\r
2266 (ASM_REWRITE_TAC[]);
\r
2268 (EXISTS_TAC `t1:real` THEN EXISTS_TAC `t2:real`);
\r
2269 (EXISTS_TAC `t3 * u` THEN EXISTS_TAC `t4 + t3 * v`);
\r
2270 (REPEAT STRIP_TAC);
\r
2271 (ASM_SIMP_TAC[REAL_LE_MUL]);
\r
2272 (MATCH_MP_TAC REAL_LE_ADD);
\r
2273 (ASM_SIMP_TAC[REAL_LE_MUL]);
\r
2274 (REWRITE_WITH `t1 + t2 + t3 * u + t4 + t3 * v =
\r
2275 t1 + t2 + t3 * (u + v) + t4`);
\r
2277 (ASM_REWRITE_TAC[REAL_MUL_RID]);
\r
2278 (REWRITE_WITH `t1 % a + t2 % b + (t3 * u) % c + (t4 + t3 * v) % d =
\r
2279 t1 % a + t2 % b + t3 % (u % c + v % d) + t4 % (d:real^3)`);
\r
2280 (VECTOR_ARITH_TAC);
\r
2281 (ASM_REWRITE_TAC[])]);;
\r
2283 (* ======================================================================= *)
\r
2285 let CONVEX_HULL_4_SUBSET_AFF_GE_2_2 = prove_by_refinement (
\r
2286 `!a b c d:real^3.
\r
2287 convex hull ({a, b, c, d}) SUBSET aff_ge {a, b} {c, d}`,
\r
2288 [(REPEAT STRIP_TAC);
\r
2289 (ASM_CASES_TAC `DISJOINT {a, b} {c, d:real^3}`);
\r
2290 (REWRITE_TAC[SUBSET; IN; IN_ELIM_THM; CONVEX_HULL_4]);
\r
2291 (REPEAT STRIP_TAC);
\r
2292 (ASM_SIMP_TAC[AFF_GE_2_2]);
\r
2293 (REWRITE_TAC[IN_ELIM_THM]);
\r
2294 (EXISTS_TAC `u:real`);
\r
2295 (EXISTS_TAC `v:real`);
\r
2296 (EXISTS_TAC `w:real`);
\r
2297 (EXISTS_TAC `z:real`);
\r
2298 (ASM_REWRITE_TAC[]);
\r
2301 (ASM_CASES_TAC `c = a:real^3`);
\r
2302 (ASM_REWRITE_TAC[]);
\r
2303 (ONCE_REWRITE_TAC[AFF_GE_DISJOINT_DIFF]);
\r
2304 (ASM_CASES_TAC `b = a:real^3 \/ b = d`);
\r
2305 (REWRITE_WITH `{a, b:real^3} DIFF {a, d:real^3} = {}`);
\r
2307 (ONCE_REWRITE_TAC[CONVEX_HULL_AFF_GE]);
\r
2308 (REWRITE_WITH `{a, b, a , d:real^3} = {a, d}`);
\r
2309 (TRUONG_SET_TAC[]);
\r
2310 (TRUONG_SET_TAC[]);
\r
2311 (REWRITE_WITH `{a, b:real^3} DIFF {a, d:real^3} = {b}`);
\r
2312 (TRUONG_SET_TAC[]);
\r
2313 (NEW_GOAL `DISJOINT {b:real^3} {a, d}`);
\r
2314 (TRUONG_SET_TAC[]);
\r
2315 (ASM_SIMP_TAC[Fan.AFF_GE_1_2]);
\r
2316 (REWRITE_WITH `{a, b, a , d:real^3} = {a, b, d}`);
\r
2317 (TRUONG_SET_TAC[]);
\r
2318 (REWRITE_TAC[SUBSET; IN; IN_ELIM_THM; CONVEX_HULL_3]);
\r
2319 (REPEAT STRIP_TAC);
\r
2320 (EXISTS_TAC `v:real` THEN EXISTS_TAC `u:real` THEN EXISTS_TAC `w:real`);
\r
2321 (ASM_REWRITE_TAC[REAL_ARITH `a + b + c = b + a + c`]);
\r
2322 (VECTOR_ARITH_TAC);
\r
2325 (ASM_CASES_TAC `c = b:real^3`);
\r
2326 (ASM_REWRITE_TAC[]);
\r
2327 (ONCE_REWRITE_TAC[AFF_GE_DISJOINT_DIFF]);
\r
2328 (ASM_CASES_TAC `a = b:real^3 \/ a = d`);
\r
2329 (REWRITE_WITH `{a, b:real^3} DIFF {b, d:real^3} = {}`);
\r
2331 (ONCE_REWRITE_TAC[CONVEX_HULL_AFF_GE]);
\r
2332 (REWRITE_WITH `{a, b, b , d:real^3} = {b, d}`);
\r
2333 (TRUONG_SET_TAC[]);
\r
2334 (TRUONG_SET_TAC[]);
\r
2335 (REWRITE_WITH `{a, b:real^3} DIFF {b, d:real^3} = {a}`);
\r
2336 (TRUONG_SET_TAC[]);
\r
2337 (NEW_GOAL `DISJOINT {a:real^3} {b, d}`);
\r
2338 (TRUONG_SET_TAC[]);
\r
2339 (ASM_SIMP_TAC[Fan.AFF_GE_1_2]);
\r
2340 (REWRITE_WITH `{a, b, b , d:real^3} = {a, b, d}`);
\r
2341 (TRUONG_SET_TAC[]);
\r
2342 (REWRITE_TAC[SUBSET; IN; IN_ELIM_THM; CONVEX_HULL_3]);
\r
2343 (REPEAT STRIP_TAC);
\r
2344 (EXISTS_TAC `u:real` THEN EXISTS_TAC `v:real` THEN EXISTS_TAC `w:real`);
\r
2345 (ASM_REWRITE_TAC[]);
\r
2348 (ASM_CASES_TAC `d = a:real^3`);
\r
2349 (ASM_REWRITE_TAC[]);
\r
2350 (ONCE_REWRITE_TAC[AFF_GE_DISJOINT_DIFF]);
\r
2351 (ASM_CASES_TAC `b = a:real^3 \/ b = c`);
\r
2352 (REWRITE_WITH `{a, b:real^3} DIFF {c, a:real^3} = {}`);
\r
2354 (ONCE_REWRITE_TAC[CONVEX_HULL_AFF_GE]);
\r
2355 (REWRITE_WITH `{a, b, c , a:real^3} = {a, c}`);
\r
2356 (TRUONG_SET_TAC[]);
\r
2357 (REWRITE_TAC[SET_RULE `{x, y} = {y, x}`]);
\r
2358 (TRUONG_SET_TAC[]);
\r
2360 (REWRITE_WITH `{a, b:real^3} DIFF {c, a:real^3} = {b}`);
\r
2361 (TRUONG_SET_TAC[]);
\r
2362 (NEW_GOAL `DISJOINT {b:real^3} {c, a}`);
\r
2363 (TRUONG_SET_TAC[]);
\r
2364 (ASM_SIMP_TAC[Fan.AFF_GE_1_2]);
\r
2365 (REWRITE_WITH `{a, b, c, a:real^3} = {a, b, c}`);
\r
2366 (TRUONG_SET_TAC[]);
\r
2367 (REWRITE_TAC[SUBSET; IN; IN_ELIM_THM; CONVEX_HULL_3]);
\r
2368 (REPEAT STRIP_TAC);
\r
2369 (EXISTS_TAC `v:real` THEN EXISTS_TAC `w:real` THEN EXISTS_TAC `u:real`);
\r
2370 (ASM_REWRITE_TAC[REAL_ARITH `v + w + u = u + v + w`]);
\r
2371 (VECTOR_ARITH_TAC);
\r
2374 (NEW_GOAL `d = b:real^3`);
\r
2376 (ASM_REWRITE_TAC[]);
\r
2377 (ONCE_REWRITE_TAC[AFF_GE_DISJOINT_DIFF]);
\r
2378 (ASM_CASES_TAC `a = b:real^3 \/ a = c`);
\r
2379 (REWRITE_WITH `{a, b:real^3} DIFF {c, b:real^3} = {}`);
\r
2381 (ONCE_REWRITE_TAC[CONVEX_HULL_AFF_GE]);
\r
2382 (REWRITE_WITH `{a, b, c , b:real^3} = {c, b}`);
\r
2383 (TRUONG_SET_TAC[]);
\r
2384 (TRUONG_SET_TAC[]);
\r
2385 (REWRITE_WITH `{a, b:real^3} DIFF {c, b:real^3} = {a}`);
\r
2386 (TRUONG_SET_TAC[]);
\r
2387 (NEW_GOAL `DISJOINT {a:real^3} {c, b}`);
\r
2388 (TRUONG_SET_TAC[]);
\r
2389 (ASM_SIMP_TAC[Fan.AFF_GE_1_2]);
\r
2390 (REWRITE_WITH `{a, b, c , b:real^3} = {a, b, c}`);
\r
2391 (TRUONG_SET_TAC[]);
\r
2392 (REWRITE_TAC[SUBSET; IN; IN_ELIM_THM; CONVEX_HULL_3]);
\r
2393 (REPEAT STRIP_TAC);
\r
2394 (EXISTS_TAC `u:real` THEN EXISTS_TAC `w:real` THEN EXISTS_TAC `v:real`);
\r
2395 (ASM_REWRITE_TAC[REAL_ARITH `a + b + c = a + c + b`]);
\r
2396 (VECTOR_ARITH_TAC)]);;
\r
2398 (* ======================================================================= *)
\r
2400 let AFF_INDEPENDENT_SET_OF_LIST_BARV = prove_by_refinement (
\r
2401 `!V ul:(real^3)list.packing V /\ saturated V /\ barV V 3 ul
\r
2402 ==> ~ affine_dependent (set_of_list ul)`,
\r
2403 [(REPEAT STRIP_TAC);
\r
2404 (SUBGOAL_THEN `? u0 u1 u2 u3. (ul:(real^3)list) = [u0:real^3;u1;u2;u3]` CHOOSE_TAC);
\r
2405 (MP_TAC (ASSUME `barV V 3 ul`));
\r
2406 (REWRITE_TAC[BARV_3_EXPLICIT]);
\r
2407 (FIRST_X_ASSUM CHOOSE_TAC);
\r
2408 (FIRST_X_ASSUM CHOOSE_TAC);
\r
2409 (FIRST_X_ASSUM CHOOSE_TAC);
\r
2411 (NEW_GOAL `barV V 3 (ul:(real^3)list)`);
\r
2412 (ASM_REWRITE_TAC[]);
\r
2413 (NEW_GOAL `~affine_dependent {u0,u1,u2,u3:real^3}`);
\r
2414 (REWRITE_TAC[AFFINE_INDEPENDENT_IFF_CARD]);
\r
2416 (REWRITE_TAC[Geomdetail.FINITE6]);
\r
2417 (NEW_GOAL `aff_dim {u0, u1, u2, u3:real^3} = &3`);
\r
2418 (REWRITE_WITH `{u0, u1, u2, u3:real^3} = set_of_list ul`);
\r
2419 (ASM_REWRITE_TAC[set_of_list]);
\r
2420 (MATCH_MP_TAC Rogers.MHFTTZN1);
\r
2421 (EXISTS_TAC `V:real^3->bool`);
\r
2422 (ASM_REWRITE_TAC[]);
\r
2423 (ASM_REWRITE_TAC[]);
\r
2424 (ONCE_REWRITE_TAC[ARITH_RULE
\r
2425 `&3 = &(CARD {u0, u1, u2, u3:real^3}) - (&1):int
\r
2426 <=> &(CARD {u0, u1, u2, u3:real^3}) = (&4):int`]);
\r
2427 (ONCE_REWRITE_TAC[INT_OF_NUM_EQ]);
\r
2428 (REWRITE_TAC[Geomdetail.CARD4]);
\r
2429 (REPEAT STRIP_TAC);
\r
2431 (NEW_GOAL `CARD {u0, u1, u2, u3:real^3} <= 3`);
\r
2432 (REWRITE_WITH `{u0, u1, u2, u3} = {u1, u2, u3:real^3}`);
\r
2434 (REWRITE_TAC[Geomdetail.CARD3]);
\r
2435 (NEW_GOAL `aff_dim {u0, u1, u2, u3} <= &(CARD {u0, u1, u2, u3:real^3}) - (&1):int`);
\r
2436 (MATCH_MP_TAC AFF_DIM_LE_CARD);
\r
2437 (REWRITE_TAC[Geomdetail.FINITE6]);
\r
2438 (NEW_GOAL `(&4):int <= &(CARD {u0, u1, u2, u3:real^3})`);
\r
2439 (ONCE_REWRITE_TAC[ARITH_RULE
\r
2440 `(&4):int <= &(CARD {u0, u1, u2, u3:real^3}) <=>
\r
2441 &3 <= &(CARD {u0, u1, u2, u3:real^3}) - (&1):int`]);
\r
2442 (ASM_MESON_TAC[]);
\r
2443 (NEW_GOAL `&(CARD {u0, u1, u2, u3:real^3}) <= (&4):int`);
\r
2444 (ONCE_REWRITE_TAC[INT_OF_NUM_LE]);
\r
2445 (REWRITE_TAC[Geomdetail.CARD4]);
\r
2446 (NEW_GOAL `CARD {u0, u1, u2, u3:real^3} = 4`);
\r
2447 (ONCE_REWRITE_TAC[GSYM INT_OF_NUM_EQ]);
\r
2451 (NEW_GOAL `CARD {u0, u1, u2, u3:real^3} <= 3`);
\r
2452 (REWRITE_WITH `{u0, u1, u2, u3} = {u0, u2, u3:real^3}`);
\r
2454 (REWRITE_TAC[Geomdetail.CARD3]);
\r
2455 (NEW_GOAL `aff_dim {u0, u1, u2, u3} <= &(CARD {u0, u1, u2, u3:real^3}) - (&1):int`);
\r
2456 (MATCH_MP_TAC AFF_DIM_LE_CARD);
\r
2457 (REWRITE_TAC[Geomdetail.FINITE6]);
\r
2458 (NEW_GOAL `(&4):int <= &(CARD {u0, u1, u2, u3:real^3})`);
\r
2459 (ONCE_REWRITE_TAC[ARITH_RULE
\r
2460 `(&4):int <= &(CARD {u0, u1, u2, u3:real^3}) <=>
\r
2461 &3 <= &(CARD {u0, u1, u2, u3:real^3}) - (&1):int`]);
\r
2462 (ASM_MESON_TAC[]);
\r
2463 (NEW_GOAL `&(CARD {u0, u1, u2, u3:real^3}) <= (&4):int`);
\r
2464 (ONCE_REWRITE_TAC[INT_OF_NUM_LE]);
\r
2465 (REWRITE_TAC[Geomdetail.CARD4]);
\r
2466 (NEW_GOAL `CARD {u0, u1, u2, u3:real^3} = 4`);
\r
2467 (ONCE_REWRITE_TAC[GSYM INT_OF_NUM_EQ]);
\r
2471 (NEW_GOAL `CARD {u0, u1, u2, u3:real^3} <= 3`);
\r
2472 (REWRITE_WITH `{u0, u1, u2, u3} = {u1, u0, u3:real^3}`);
\r
2474 (REWRITE_TAC[Geomdetail.CARD3]);
\r
2475 (NEW_GOAL `aff_dim {u0, u1, u2, u3} <= &(CARD {u0, u1, u2, u3:real^3}) - (&1):int`);
\r
2476 (MATCH_MP_TAC AFF_DIM_LE_CARD);
\r
2477 (REWRITE_TAC[Geomdetail.FINITE6]);
\r
2478 (NEW_GOAL `(&4):int <= &(CARD {u0, u1, u2, u3:real^3})`);
\r
2479 (ONCE_REWRITE_TAC[ARITH_RULE
\r
2480 `(&4):int <= &(CARD {u0, u1, u2, u3:real^3}) <=>
\r
2481 &3 <= &(CARD {u0, u1, u2, u3:real^3}) - (&1):int`]);
\r
2482 (ASM_MESON_TAC[]);
\r
2483 (NEW_GOAL `&(CARD {u0, u1, u2, u3:real^3}) <= (&4):int`);
\r
2484 (ONCE_REWRITE_TAC[INT_OF_NUM_LE]);
\r
2485 (REWRITE_TAC[Geomdetail.CARD4]);
\r
2486 (NEW_GOAL `CARD {u0, u1, u2, u3:real^3} = 4`);
\r
2487 (ONCE_REWRITE_TAC[GSYM INT_OF_NUM_EQ]);
\r
2491 (NEW_GOAL `CARD {u0, u1, u2, u3:real^3} <= 3`);
\r
2492 (REWRITE_WITH `{u0, u1, u2, u3} = {u0, u2, u3:real^3}`);
\r
2494 (REWRITE_TAC[Geomdetail.CARD3]);
\r
2495 (NEW_GOAL `aff_dim {u0, u1, u2, u3} <= &(CARD {u0, u1, u2, u3:real^3}) - (&1):int`);
\r
2496 (MATCH_MP_TAC AFF_DIM_LE_CARD);
\r
2497 (REWRITE_TAC[Geomdetail.FINITE6]);
\r
2498 (NEW_GOAL `(&4):int <= &(CARD {u0, u1, u2, u3:real^3})`);
\r
2499 (ONCE_REWRITE_TAC[ARITH_RULE
\r
2500 `(&4):int <= &(CARD {u0, u1, u2, u3:real^3}) <=>
\r
2501 &3 <= &(CARD {u0, u1, u2, u3:real^3}) - (&1):int`]);
\r
2502 (ASM_MESON_TAC[]);
\r
2503 (NEW_GOAL `&(CARD {u0, u1, u2, u3:real^3}) <= (&4):int`);
\r
2504 (ONCE_REWRITE_TAC[INT_OF_NUM_LE]);
\r
2505 (REWRITE_TAC[Geomdetail.CARD4]);
\r
2506 (NEW_GOAL `CARD {u0, u1, u2, u3:real^3} = 4`);
\r
2507 (ONCE_REWRITE_TAC[GSYM INT_OF_NUM_EQ]);
\r
2510 (ASM_MESON_TAC[set_of_list])]);;
\r
2512 (* ======================================================================= *)
\r
2514 let VORONOI_LIST_3_SINGLETON_EXPLICIT = prove_by_refinement (
\r
2516 packing V /\ saturated V /\ barV V 3 ul
\r
2517 ==> (?a. voronoi_list V ul = {a} /\
\r
2518 a = circumcenter (set_of_list ul) /\
\r
2519 hl ul = dist (HD ul, a))`,
\r
2520 [(REPEAT STRIP_TAC);
\r
2521 (SUBGOAL_THEN `? u0 u1 u2 u3. (ul:(real^3)list) = [u0:real^3;u1;u2;u3]` CHOOSE_TAC);
\r
2522 (MP_TAC (ASSUME `barV V 3 ul`));
\r
2523 (REWRITE_TAC[BARV_3_EXPLICIT]);
\r
2524 (FIRST_X_ASSUM CHOOSE_TAC);
\r
2525 (FIRST_X_ASSUM CHOOSE_TAC);
\r
2526 (FIRST_X_ASSUM CHOOSE_TAC);
\r
2528 (NEW_GOAL `~affine_dependent {u0,u1,u2,u3:real^3}`);
\r
2529 (ASM_MESON_TAC[set_of_list; AFF_INDEPENDENT_SET_OF_LIST_BARV]);
\r
2531 (NEW_GOAL `barV V 3 ul`);
\r
2532 (ASM_REWRITE_TAC[]);
\r
2533 (UP_ASM_TAC THEN REWRITE_TAC[BARV; VORONOI_NONDG]);
\r
2534 (REPEAT STRIP_TAC);
\r
2536 (NEW_GOAL `initial_sublist ul (ul:(real^3)list) /\ 0 < LENGTH ul`);
\r
2537 (ASM_REWRITE_TAC[INITIAL_SUBLIST; LENGTH;
\r
2538 ARITH_RULE `0 < 3 + 1 /\ 0 < SUC (SUC (SUC (SUC 0)))`]);
\r
2539 (EXISTS_TAC `[]:(real^3)list`);
\r
2540 (REWRITE_TAC[APPEND]);
\r
2541 (NEW_GOAL `aff_dim (voronoi_list V (ul:(real^3)list)) + &(LENGTH ul) = &4`);
\r
2543 (UP_ASM_TAC THEN ASM_REWRITE_TAC[LENGTH; ARITH_RULE `3 + 1 = 4`]);
\r
2545 (NEW_GOAL `aff_dim (voronoi_list V [u0; u1; u2; u3:real^3]) = &0`);
\r
2547 (UP_ASM_TAC THEN REWRITE_TAC[AFF_DIM_EQ_0]);
\r
2548 (REPEAT STRIP_TAC);
\r
2550 (EXISTS_TAC `a:real^3`);
\r
2552 (NEW_GOAL `a = circumcenter (set_of_list [u0; u1; u2; u3:real^3])`);
\r
2553 (REWRITE_TAC[set_of_list]);
\r
2554 (NEW_GOAL `!p. p IN affine hull {u0, u1, u2, u3:real^3} /\
\r
2555 (?c. !w. w IN {u0, u1, u2, u3} ==> dist (p,w) = c)
\r
2556 ==> p = circumcenter {u0, u1, u2, u3}`);
\r
2557 (MATCH_MP_TAC Rogers.OAPVION3);
\r
2558 (ASM_REWRITE_TAC[]);
\r
2560 (FIRST_X_ASSUM MATCH_MP_TAC);
\r
2561 (NEW_GOAL `a IN voronoi_list V [u0; u1; u2; u3:real^3]`);
\r
2562 (UP_ASM_TAC THEN TRUONG_SET_TAC[]);
\r
2563 (NEW_GOAL `affine hull {u0, u1, u2, u3:real^3} = (:real^3)`);
\r
2564 (ONCE_ASM_REWRITE_TAC[GSYM AFF_DIM_EQ_FULL]);
\r
2565 (REWRITE_TAC[DIMINDEX_3]);
\r
2566 (REWRITE_WITH `{u0, u1, u2, u3:real^3} = set_of_list ul`);
\r
2567 (ASM_REWRITE_TAC[set_of_list]);
\r
2568 (MATCH_MP_TAC Rogers.MHFTTZN1);
\r
2569 (EXISTS_TAC `V:real^3->bool`);
\r
2570 (ASM_REWRITE_TAC[]);
\r
2571 (ASM_REWRITE_TAC[]);
\r
2572 (REWRITE_TAC[IN_UNIV]);
\r
2573 (EXISTS_TAC `dist (a,u0:real^3)`);
\r
2574 (UNDISCH_TAC `a IN voronoi_list V [u0; u1; u2; u3:real^3]`);
\r
2575 (REWRITE_TAC[VORONOI_LIST;VORONOI_SET; set_of_list;
\r
2576 IN_INTERS; voronoi_closed]);
\r
2577 (REPEAT STRIP_TAC);
\r
2580 (NEW_GOAL `a IN {x | !w. V w ==> dist (x,u0) <= dist (x,w:real^3)}`);
\r
2581 (FIRST_X_ASSUM MATCH_MP_TAC);
\r
2582 (REWRITE_TAC[IN; IN_ELIM_THM]);
\r
2583 (EXISTS_TAC `u0:real^3` THEN REWRITE_TAC[]);
\r
2584 (TRUONG_SET_TAC[]);
\r
2586 (NEW_GOAL `a IN {x | !w. V w ==> dist (x,u1) <= dist (x,w:real^3)}`);
\r
2587 (FIRST_X_ASSUM MATCH_MP_TAC);
\r
2588 (REWRITE_TAC[IN; IN_ELIM_THM]);
\r
2589 (EXISTS_TAC `u1:real^3` THEN REWRITE_TAC[]);
\r
2590 (TRUONG_SET_TAC[]);
\r
2592 (NEW_GOAL `a IN {x | !w. V w ==> dist (x,u2) <= dist (x,w:real^3)}`);
\r
2593 (FIRST_X_ASSUM MATCH_MP_TAC);
\r
2594 (REWRITE_TAC[IN; IN_ELIM_THM]);
\r
2595 (EXISTS_TAC `u2:real^3` THEN REWRITE_TAC[]);
\r
2596 (TRUONG_SET_TAC[]);
\r
2598 (NEW_GOAL `a IN {x | !w. V w ==> dist (x,u3) <= dist (x,w:real^3)}`);
\r
2599 (FIRST_X_ASSUM MATCH_MP_TAC);
\r
2600 (REWRITE_TAC[IN; IN_ELIM_THM]);
\r
2601 (EXISTS_TAC `u3:real^3` THEN REWRITE_TAC[]);
\r
2602 (TRUONG_SET_TAC[]);
\r
2604 (REPLICATE_TAC 4 UP_ASM_TAC THEN REWRITE_TAC[IN;IN_ELIM_THM]);
\r
2605 (REPEAT STRIP_TAC);
\r
2606 (NEW_GOAL `u0 IN V /\ u1 IN V /\ u2 IN V /\ (u3:real^3) IN V`);
\r
2607 (UNDISCH_TAC `barV V 3 (ul:(real^3)list)`);
\r
2608 (REWRITE_TAC[BARV]);
\r
2610 (NEW_GOAL `initial_sublist [u0;u1;u2;u3] ul /\
\r
2611 0 < LENGTH [u0;u1;u2;u3:real^3]`);
\r
2612 (REWRITE_TAC[LENGTH; INITIAL_SUBLIST]);
\r
2614 (EXISTS_TAC `[]:(real^3)list`);
\r
2615 (ASM_REWRITE_TAC[APPEND]);
\r
2618 (NEW_GOAL `voronoi_nondg V [u0;u1;u2;u3:real^3]`);
\r
2620 (UP_ASM_TAC THEN REWRITE_TAC[VORONOI_NONDG; set_of_list]);
\r
2623 (UNDISCH_TAC `w IN {u0, u1, u2, u3:real^3}`);
\r
2624 (REWRITE_TAC[Geomdetail.IN_SET4] THEN REPEAT STRIP_TAC);
\r
2625 (ASM_REWRITE_TAC[]);
\r
2627 (ASM_REWRITE_TAC[]);
\r
2628 (NEW_GOAL `dist (a,u0) <= dist (a,u1:real^3)`);
\r
2629 (MATCH_MP_TAC (ASSUME `!w. V w ==> dist (a,u0) <= dist (a,w:real^3)`));
\r
2630 (ASM_REWRITE_TAC[GSYM IN]);
\r
2631 (NEW_GOAL `dist (a,u1) <= dist (a,u0:real^3)`);
\r
2632 (MATCH_MP_TAC (ASSUME `!w. V w ==> dist (a,u1) <= dist (a,w:real^3)`));
\r
2633 (ASM_REWRITE_TAC[GSYM IN]);
\r
2634 (ASM_REAL_ARITH_TAC);
\r
2636 (ASM_REWRITE_TAC[]);
\r
2637 (NEW_GOAL `dist (a,u0) <= dist (a,u2:real^3)`);
\r
2638 (MATCH_MP_TAC (ASSUME `!w. V w ==> dist (a,u0) <= dist (a,w:real^3)`));
\r
2639 (ASM_REWRITE_TAC[GSYM IN]);
\r
2640 (NEW_GOAL `dist (a,u2) <= dist (a,u0:real^3)`);
\r
2641 (MATCH_MP_TAC (ASSUME `!w. V w ==> dist (a,u2) <= dist (a,w:real^3)`));
\r
2642 (ASM_REWRITE_TAC[GSYM IN]);
\r
2643 (ASM_REAL_ARITH_TAC);
\r
2645 (ASM_REWRITE_TAC[]);
\r
2646 (NEW_GOAL `dist (a,u0) <= dist (a,u3:real^3)`);
\r
2647 (MATCH_MP_TAC (ASSUME `!w. V w ==> dist (a,u0) <= dist (a,w:real^3)`));
\r
2648 (ASM_REWRITE_TAC[GSYM IN]);
\r
2649 (NEW_GOAL `dist (a,u3) <= dist (a,u0:real^3)`);
\r
2650 (MATCH_MP_TAC (ASSUME `!w. V w ==> dist (a,u3) <= dist (a,w:real^3)`));
\r
2651 (ASM_REWRITE_TAC[GSYM IN]);
\r
2652 (ASM_REAL_ARITH_TAC);
\r
2654 (ASM_REWRITE_TAC[]);
\r
2655 (REWRITE_TAC[HL;HD]);
\r
2656 (ONCE_REWRITE_TAC[DIST_SYM]);
\r
2657 (ABBREV_TAC `S = set_of_list [u0; u1; u2; u3:real^3]`);
\r
2658 (NEW_GOAL `(!w. w IN S ==> radV S = dist (circumcenter S,w:real^3))`);
\r
2659 (MATCH_MP_TAC Rogers.OAPVION2);
\r
2660 (EXPAND_TAC "S" THEN DEL_TAC THEN ASM_REWRITE_TAC[set_of_list]);
\r
2661 (FIRST_ASSUM MATCH_MP_TAC);
\r
2662 (EXPAND_TAC "S" THEN REWRITE_TAC[set_of_list]);
\r
2663 (TRUONG_SET_TAC[])]);;
\r
2665 (* ======================================================================= *)
\r
2667 let ORTHOGONAL_AFF_HULL_2_KY_LEMMA = prove_by_refinement (
\r
2668 `!n a b s p:real^3.
\r
2669 orthogonal (a - b) n /\ s IN aff {a, b} /\ p IN aff {a, b}
\r
2670 ==> orthogonal (s - p) n`,
\r
2671 [(REWRITE_TAC[Trigonometry2.AFF2; IN; IN_ELIM_THM; orthogonal]);
\r
2672 (REPEAT STRIP_TAC);
\r
2673 (ASM_REWRITE_TAC[VECTOR_ARITH `(t % a + (&1 - t) % b) - (t' % a + (&1 - t') % b)
\r
2674 = (t - t') % (a - b)`;DOT_LMUL;REAL_MUL_RZERO])]);;
\r
2675 (* ======================================================================= *)
\r
2678 let DIST_PROJECTION_LT_LEMMA = prove_by_refinement (
\r
2679 `!x a b:real^3. ?s. s IN aff {a, b} /\
\r
2680 (!m n. m IN aff {a, b} /\ n IN aff {a, b} ==>
\r
2681 (dist (x, m) < dist (x, n) <=> dist (s,m) < dist (s,n)) /\
\r
2682 (dist (x, m) <= dist (x, n) <=> dist (s,m) <= dist (s,n)))`,
\r
2683 [ (REPEAT STRIP_TAC);
\r
2684 (SUBGOAL_THEN `?s:real^3. s IN aff {a, b} /\ (x - s) dot (a - b) = &0` CHOOSE_TAC);
\r
2685 (REWRITE_TAC[Trigonometry2.EXISTS_PROJECTING_POINT2]) ;
\r
2686 (EXISTS_TAC `s:real^3` THEN ASM_REWRITE_TAC[]);
\r
2688 (REPEAT STRIP_TAC);
\r
2689 (NEW_GOAL `orthogonal (a - b) (x - s:real^3)`);
\r
2690 (REWRITE_TAC[orthogonal]);
\r
2691 (ONCE_REWRITE_TAC[DOT_SYM] THEN ASM_REWRITE_TAC[]);
\r
2694 (REPEAT STRIP_TAC);
\r
2695 (REWRITE_TAC[dist]);
\r
2696 (NEW_GOAL `norm (s - m:real^3) = abs (norm (s - m)) /\
\r
2697 norm (s - n) = abs (norm (s - n))`);
\r
2698 (MESON_TAC[REAL_ABS_REFL;NORM_POS_LE]);
\r
2699 (ONCE_ASM_REWRITE_TAC[]);
\r
2700 (REWRITE_TAC[REAL_LT_SQUARE_ABS]);
\r
2701 (NEW_GOAL `norm (x:real^3 - m) pow 2 < norm (x - n) pow 2`);
\r
2702 (ONCE_REWRITE_TAC[GSYM REAL_LT_SQUARE_ABS]);
\r
2704 (NEW_GOAL `abs (norm (x - m:real^3)) = (norm (x - m)) /\
\r
2705 abs (norm (x - n)) = (norm (x - n))`);
\r
2706 (MESON_TAC[REAL_ABS_REFL;NORM_POS_LE]);
\r
2707 (ASM_REWRITE_TAC[]);
\r
2708 (REWRITE_TAC[GSYM dist]);
\r
2709 (ASM_REWRITE_TAC[]);
\r
2710 (NEW_GOAL `norm (x - m:real^3) pow 2 = norm (s - m) pow 2 + norm (x - s) pow 2`);
\r
2711 (MATCH_MP_TAC PYTHAGORAS);
\r
2712 (MATCH_MP_TAC ORTHOGONAL_AFF_HULL_2_KY_LEMMA);
\r
2713 (EXISTS_TAC `a:real^3` THEN EXISTS_TAC `b:real^3`);
\r
2714 (ASM_REWRITE_TAC[]);
\r
2715 (NEW_GOAL `norm (x - n:real^3) pow 2 = norm (s - n) pow 2 + norm (x - s) pow 2`);
\r
2716 (MATCH_MP_TAC PYTHAGORAS);
\r
2717 (MATCH_MP_TAC ORTHOGONAL_AFF_HULL_2_KY_LEMMA);
\r
2718 (EXISTS_TAC `a:real^3` THEN EXISTS_TAC `b:real^3`);
\r
2719 (ASM_REWRITE_TAC[]);
\r
2720 (ASM_REAL_ARITH_TAC);
\r
2723 (REWRITE_TAC[dist]);
\r
2724 (NEW_GOAL `norm (x - m:real^3) = abs (norm (x - m)) /\
\r
2725 norm (x - n) = abs (norm (x - n))`);
\r
2726 (MESON_TAC[REAL_ABS_REFL;NORM_POS_LE]);
\r
2727 (ONCE_ASM_REWRITE_TAC[]);
\r
2728 (REWRITE_TAC[REAL_LT_SQUARE_ABS]);
\r
2729 (NEW_GOAL `norm (s:real^3 - m) pow 2 < norm (s - n) pow 2`);
\r
2730 (ONCE_REWRITE_TAC[GSYM REAL_LT_SQUARE_ABS]);
\r
2732 (NEW_GOAL `abs (norm (s - m:real^3)) = (norm (s - m)) /\
\r
2733 abs (norm (s - n)) = (norm (s - n))`);
\r
2734 (MESON_TAC[REAL_ABS_REFL;NORM_POS_LE]);
\r
2735 (ASM_REWRITE_TAC[]);
\r
2736 (REWRITE_TAC[GSYM dist]);
\r
2737 (ASM_REWRITE_TAC[]);
\r
2738 (NEW_GOAL `norm (x - m:real^3) pow 2 = norm (s - m) pow 2 + norm (x - s) pow 2`);
\r
2739 (MATCH_MP_TAC PYTHAGORAS);
\r
2740 (MATCH_MP_TAC ORTHOGONAL_AFF_HULL_2_KY_LEMMA);
\r
2741 (EXISTS_TAC `a:real^3` THEN EXISTS_TAC `b:real^3`);
\r
2742 (ASM_REWRITE_TAC[]);
\r
2744 (NEW_GOAL `norm (x - n:real^3) pow 2 = norm (s - n) pow 2 + norm (x - s) pow 2`);
\r
2745 (MATCH_MP_TAC PYTHAGORAS);
\r
2746 (MATCH_MP_TAC ORTHOGONAL_AFF_HULL_2_KY_LEMMA);
\r
2747 (EXISTS_TAC `a:real^3` THEN EXISTS_TAC `b:real^3`);
\r
2748 (ASM_REWRITE_TAC[]);
\r
2749 (ASM_REAL_ARITH_TAC);
\r
2751 (NEW_GOAL `orthogonal (a - b) (x - s:real^3)`);
\r
2752 (REWRITE_TAC[orthogonal]);
\r
2753 (ONCE_REWRITE_TAC[DOT_SYM] THEN ASM_REWRITE_TAC[]);
\r
2756 (REPEAT STRIP_TAC);
\r
2757 (REWRITE_TAC[dist]);
\r
2758 (NEW_GOAL `norm (s - m:real^3) = abs (norm (s - m)) /\
\r
2759 norm (s - n) = abs (norm (s - n))`);
\r
2760 (MESON_TAC[REAL_ABS_REFL;NORM_POS_LE]);
\r
2761 (ONCE_ASM_REWRITE_TAC[]);
\r
2762 (REWRITE_TAC[REAL_LE_SQUARE_ABS]);
\r
2763 (NEW_GOAL `norm (x:real^3 - m) pow 2 <= norm (x - n) pow 2`);
\r
2764 (ONCE_REWRITE_TAC[GSYM REAL_LE_SQUARE_ABS]);
\r
2766 (NEW_GOAL `abs (norm (x - m:real^3)) = (norm (x - m)) /\
\r
2767 abs (norm (x - n)) = (norm (x - n))`);
\r
2768 (MESON_TAC[REAL_ABS_REFL;NORM_POS_LE]);
\r
2769 (ASM_REWRITE_TAC[]);
\r
2770 (REWRITE_TAC[GSYM dist]);
\r
2771 (ASM_REWRITE_TAC[]);
\r
2772 (NEW_GOAL `norm (x - m:real^3) pow 2 = norm (s - m) pow 2 + norm (x - s) pow 2`);
\r
2773 (MATCH_MP_TAC PYTHAGORAS);
\r
2774 (MATCH_MP_TAC ORTHOGONAL_AFF_HULL_2_KY_LEMMA);
\r
2775 (EXISTS_TAC `a:real^3` THEN EXISTS_TAC `b:real^3`);
\r
2776 (ASM_REWRITE_TAC[]);
\r
2777 (NEW_GOAL `norm (x - n:real^3) pow 2 = norm (s - n) pow 2 + norm (x - s) pow 2`);
\r
2778 (MATCH_MP_TAC PYTHAGORAS);
\r
2779 (MATCH_MP_TAC ORTHOGONAL_AFF_HULL_2_KY_LEMMA);
\r
2780 (EXISTS_TAC `a:real^3` THEN EXISTS_TAC `b:real^3`);
\r
2781 (ASM_REWRITE_TAC[]);
\r
2782 (ASM_REAL_ARITH_TAC);
\r
2785 (REWRITE_TAC[dist]);
\r
2786 (NEW_GOAL `norm (x - m:real^3) = abs (norm (x - m)) /\
\r
2787 norm (x - n) = abs (norm (x - n))`);
\r
2788 (MESON_TAC[REAL_ABS_REFL;NORM_POS_LE]);
\r
2789 (ONCE_ASM_REWRITE_TAC[]);
\r
2790 (REWRITE_TAC[REAL_LE_SQUARE_ABS]);
\r
2791 (NEW_GOAL `norm (s:real^3 - m) pow 2 <= norm (s - n) pow 2`);
\r
2792 (ONCE_REWRITE_TAC[GSYM REAL_LE_SQUARE_ABS]);
\r
2794 (NEW_GOAL `abs (norm (s - m:real^3)) = (norm (s - m)) /\
\r
2795 abs (norm (s - n)) = (norm (s - n))`);
\r
2796 (MESON_TAC[REAL_ABS_REFL;NORM_POS_LE]);
\r
2797 (ASM_REWRITE_TAC[]);
\r
2798 (REWRITE_TAC[GSYM dist]);
\r
2799 (ASM_REWRITE_TAC[]);
\r
2800 (NEW_GOAL `norm (x - m:real^3) pow 2 = norm (s - m) pow 2 + norm (x - s) pow 2`);
\r
2801 (MATCH_MP_TAC PYTHAGORAS);
\r
2802 (MATCH_MP_TAC ORTHOGONAL_AFF_HULL_2_KY_LEMMA);
\r
2803 (EXISTS_TAC `a:real^3` THEN EXISTS_TAC `b:real^3`);
\r
2804 (ASM_REWRITE_TAC[]);
\r
2806 (NEW_GOAL `norm (x - n:real^3) pow 2 = norm (s - n) pow 2 + norm (x - s) pow 2`);
\r
2807 (MATCH_MP_TAC PYTHAGORAS);
\r
2808 (MATCH_MP_TAC ORTHOGONAL_AFF_HULL_2_KY_LEMMA);
\r
2809 (EXISTS_TAC `a:real^3` THEN EXISTS_TAC `b:real^3`);
\r
2810 (ASM_REWRITE_TAC[]);
\r
2811 (ASM_REAL_ARITH_TAC)
\r
2814 (* ======================================================================= *)
\r
2817 let SIMPLEX_FURTHEST_LT_2 = prove_by_refinement (
\r
2818 `!a (s:real^N->bool).
\r
2820 ==> (!x. x IN convex hull s /\ ~(x IN s)
\r
2821 ==> (?y. y IN s /\ norm (x - a) < norm (y - a)))`,
\r
2822 [(REPEAT STRIP_TAC);
\r
2823 (NEW_GOAL `(?y:real^N. y IN convex hull s /\ norm (x - a) < norm (y - a))`);
\r
2824 (ASM_SIMP_TAC[SIMPLEX_FURTHEST_LT]);
\r
2825 (FIRST_X_ASSUM CHOOSE_TAC);
\r
2826 (ASM_CASES_TAC `y:real^N IN s`);
\r
2827 (EXISTS_TAC `y:real^N`);
\r
2828 (ASM_REWRITE_TAC[]);
\r
2829 (SUBGOAL_THEN `(?y. y:real^N IN s /\
\r
2830 (!x. x IN convex hull s ==> norm (x - a) <= norm (y - a)))`
\r
2832 (MATCH_MP_TAC SIMPLEX_FURTHEST_LE);
\r
2833 (ASM_REWRITE_TAC[]);
\r
2835 (UNDISCH_TAC `x:real^N IN convex hull s`);
\r
2836 (ASM_REWRITE_TAC[CONVEX_HULL_EMPTY]);
\r
2838 (EXISTS_TAC `y':real^N`);
\r
2839 (ASM_REWRITE_TAC[]);
\r
2840 (MATCH_MP_TAC (REAL_ARITH `m < norm (y-a:real^N) /\ norm (y-a) <= n ==> m < n`));
\r
2841 (ASM_REWRITE_TAC[]);
\r
2842 (UP_ASM_TAC THEN STRIP_TAC THEN FIRST_ASSUM MATCH_MP_TAC);
\r
2843 (ASM_REWRITE_TAC[])]);;
\r
2845 (* ======================================================================= *)
\r
2848 let DIST_BETWEEN_FURTHEST_LT = prove_by_refinement (
\r
2849 `!x a b s:real^3.
\r
2850 between s (a, b) /\ ~(s = a) /\ ~(s = b) /\ ~(a = b) /\
\r
2851 dist (x, b) <= dist (x, a)
\r
2852 ==> dist (x,s) < dist (x,a)`,
\r
2853 [(REPEAT GEN_TAC THEN REWRITE_TAC[BETWEEN_IN_CONVEX_HULL] THEN REPEAT STRIP_TAC
\r
2854 THEN NEW_GOAL `(?y:real^3. y IN {a,b} /\ norm (s - x) < norm (y - x))`);
\r
2855 (NEW_GOAL`(!h. h IN convex hull {a,b} /\ ~(h IN {a,b:real^3})
\r
2856 ==> (?y. y IN {a,b} /\ norm (h - x) < norm (y - x)))`);
\r
2857 (MATCH_MP_TAC SIMPLEX_FURTHEST_LT_2 THEN REWRITE_TAC[Geomdetail.FINITE6]);
\r
2858 (FIRST_X_ASSUM MATCH_MP_TAC);
\r
2860 (FIRST_X_ASSUM CHOOSE_TAC THEN UP_ASM_TAC);
\r
2861 (REWRITE_TAC[SET_RULE `a IN {m,n} <=> a = m \/ a = n`]);
\r
2862 (REWRITE_TAC[GSYM dist] THEN REPEAT STRIP_TAC);
\r
2863 (ASM_MESON_TAC[DIST_SYM]);
\r
2864 (ASM_MESON_TAC[DIST_SYM; REAL_ARITH `x < y /\ y <= z ==> x < z`])]);;
\r
2866 (* ======================================================================= *)
\r
2869 let ROGERS_EXPLICIT = prove_by_refinement (
\r
2871 saturated V /\ packing V /\ barV V 3 ul ==>
\r
2872 rogers V ul = convex hull
\r
2873 {HD ul, omega_list_n V ul 1, omega_list_n V ul 2, omega_list_n V ul 3}`,
\r
2874 [(REPEAT STRIP_TAC THEN REWRITE_TAC[ROGERS]);
\r
2875 (NEW_GOAL `?u0 u1 u2 u3. (ul:(real^3)list) = [u0:real^3;u1;u2;u3]`);
\r
2876 (MP_TAC (ASSUME `barV V 3 ul`));
\r
2877 (REWRITE_TAC[BARV_3_EXPLICIT]);
\r
2878 (FIRST_X_ASSUM CHOOSE_TAC);
\r
2879 (FIRST_X_ASSUM CHOOSE_TAC);
\r
2880 (FIRST_X_ASSUM CHOOSE_TAC);
\r
2881 (FIRST_X_ASSUM CHOOSE_TAC);
\r
2882 (REWRITE_WITH `{j | j < LENGTH (ul:(real^3)list)} = {0, 1,2,3}`);
\r
2883 (ASM_REWRITE_TAC[LENGTH; ARITH_RULE `SUC (SUC (SUC (SUC 0))) = 4`]);
\r
2884 (MESON_TAC[SET_OF_0_TO_3]);
\r
2885 (REWRITE_TAC[IMAGE]);
\r
2887 (REWRITE_WITH `!x. x IN {0,1,2,3} <=> (x = 0 \/x = 1 \/x = 2 \/x = 3)`);
\r
2890 `!y. (?x. (x = 0 \/ x = 1 \/ x = 2 \/ x = 3) /\ y = omega_list_n V ul x)
\r
2891 <=> (y = omega_list_n V ul 0) \/ (y = omega_list_n V ul 1) \/
\r
2892 (y = omega_list_n V ul 2) \/(y = omega_list_n V ul 3)`);
\r
2893 (SET_TAC[BETA_THM]);
\r
2895 `{y | y = omega_list_n V ul 0 \/ y = omega_list_n V ul 1 \/
\r
2896 y = omega_list_n V ul 2 \/ y = omega_list_n V ul 3}
\r
2897 = {omega_list_n V ul 0, omega_list_n V ul 1,
\r
2898 omega_list_n V ul 2, omega_list_n V ul 3}`);
\r
2900 (REWRITE_WITH `omega_list_n V ul 0 = HD ul`);
\r
2901 (REWRITE_TAC[OMEGA_LIST_N])]);;
\r
2903 (* ======================================================================= *)
\r
2905 let SEGMENT_INTER_CBALL_LEMMA = prove
\r
2906 (`!x r a (b:real^3).
\r
2907 dist (x, a) <= r /\ r <= dist (x, b)
\r
2908 ==> (?c. between c (a, b) /\ dist (x, c) = r)`,
\r
2909 REPEAT STRIP_TAC THEN ASM_CASES_TAC `dist(x:real^3,b) = r` THENL
\r
2910 [EXISTS_TAC `b:real^3` THEN ASM_REWRITE_TAC[BETWEEN_REFL];
\r
2911 MP_TAC(ISPECL [`segment[a:real^3,b]`; `cball(x:real^3,r)`]
\r
2912 CONNECTED_INTER_FRONTIER) THEN
\r
2914 [REWRITE_TAC[CONNECTED_SEGMENT; GSYM MEMBER_NOT_EMPTY] THEN CONJ_TAC THENL
\r
2915 [EXISTS_TAC `a:real^3` THEN
\r
2916 ASM_REWRITE_TAC[IN_INTER; ENDS_IN_SEGMENT; IN_CBALL];
\r
2917 EXISTS_TAC `b:real^3` THEN
\r
2918 ASM_REWRITE_TAC[IN_DIFF; ENDS_IN_SEGMENT; IN_CBALL] THEN
\r
2919 ASM_REAL_ARITH_TAC];
\r
2920 REWRITE_TAC[GSYM MEMBER_NOT_EMPTY] THEN MATCH_MP_TAC MONO_EXISTS THEN
\r
2921 REWRITE_TAC[FRONTIER_CBALL; IN_ELIM_THM; IN_INTER;
\r
2922 BETWEEN_IN_SEGMENT]]]);;
\r
2924 (* ======================================================================= *)
\r
2926 let CLOSEST_POINT_SING = prove_by_refinement (
\r
2927 `!a (b:real^3). closest_point {a} b = a`,
\r
2928 [(REPEAT GEN_TAC THEN REWRITE_TAC
\r
2929 [closest_point;SET_RULE `a IN {x} <=> a = x`]);
\r
2930 (MATCH_MP_TAC SELECT_UNIQUE);
\r
2931 (REWRITE_TAC[BETA_THM] THEN GEN_TAC THEN EQ_TAC);
\r
2932 (REPEAT STRIP_TAC);
\r
2933 (REPEAT STRIP_TAC);
\r
2934 (ASM_REWRITE_TAC[]);
\r
2935 (ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC)]);;
\r
2937 (* ======================================================================= *)
\r
2940 let MXI_EXPLICIT = prove_by_refinement(
\r
2941 `!V ul. packing V /\ saturated V /\ barV V 3 ul /\ ul = [u0;u1;u2;u3] /\
\r
2942 hl (truncate_simplex 2 ul) < sqrt (&2) /\ sqrt (&2) <= hl ul
\r
2943 ==> (?s. between s (omega_list_n V ul 2, omega_list_n V ul 3) /\
\r
2944 dist (u0, s) = sqrt (&2) /\
\r
2946 [(REPEAT STRIP_TAC);
\r
2948 `?(s:real^3). between s (omega_list_n V ul 2, omega_list_n V ul 3) /\
\r
2949 dist (u0, s) = sqrt (&2)`);
\r
2950 (MATCH_MP_TAC SEGMENT_INTER_CBALL_LEMMA);
\r
2953 (REWRITE_WITH `dist (u0:real^3,omega_list_n V ul 2) =
\r
2954 hl (truncate_simplex 2 ul)`);
\r
2955 (ABBREV_TAC `vl = truncate_simplex 2 (ul:(real^3)list)`);
\r
2956 (REWRITE_WITH `hl (vl:(real^3)list) =
\r
2957 dist (circumcenter (set_of_list vl),HD vl)`);
\r
2958 (MATCH_MP_TAC Rogers.HL_EQ_DIST0);
\r
2959 (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `2`);
\r
2960 (ASM_REWRITE_TAC[]);
\r
2961 (EXPAND_TAC "vl");
\r
2962 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
\r
2963 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);
\r
2964 (REWRITE_TAC[DIST_SYM]);
\r
2966 (REWRITE_TAC[PAIR_EQ]);
\r
2968 (EXPAND_TAC "vl");
\r
2969 (DEL_TAC THEN ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2; HD]);
\r
2970 (ASM_REWRITE_TAC[Marchal_cells.OMEGA_LIST_TRUNCATE_2]);
\r
2971 (REWRITE_WITH `omega_list V [u0; u1; u2] = omega_list V (vl:(real^3)list)`);
\r
2972 (EXPAND_TAC "vl");
\r
2973 (DEL_TAC THEN ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]);
\r
2974 (MATCH_MP_TAC XNHPWAB1);
\r
2976 (ASM_REWRITE_TAC[]);
\r
2977 (REWRITE_TAC[IN] THEN EXPAND_TAC "vl");
\r
2978 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
\r
2979 (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]);
\r
2980 (ASM_REAL_ARITH_TAC);
\r
2982 (* ======================================================================== *)
\r
2984 (NEW_GOAL `~affine_dependent {u0,u1,u2,u3:real^3}`);
\r
2985 (ASM_MESON_TAC[set_of_list; AFF_INDEPENDENT_SET_OF_LIST_BARV]);
\r
2987 (REWRITE_WITH `dist (u0:real^3,omega_list_n V ul 3) =
\r
2988 hl (truncate_simplex 3 ul)`);
\r
2989 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_3]);
\r
2990 (REWRITE_TAC[OMEGA_LIST_N; ARITH_RULE `3 = SUC 2`]);
\r
2991 (ONCE_REWRITE_TAC[ARITH_RULE `SUC 2 = 3`]);
\r
2992 (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_3]);
\r
2994 (NEW_GOAL `barV V 3 ul`);
\r
2995 (ASM_REWRITE_TAC[]);
\r
2996 (UP_ASM_TAC THEN REWRITE_TAC[BARV; VORONOI_NONDG]);
\r
2997 (REPEAT STRIP_TAC);
\r
2998 (NEW_GOAL `(?a. voronoi_list V ul = {a:real^3} /\
\r
2999 a = circumcenter (set_of_list ul) /\
\r
3000 hl ul = dist (HD ul,a))`);
\r
3001 (ASM_SIMP_TAC[VORONOI_LIST_3_SINGLETON_EXPLICIT]);
\r
3002 (UP_ASM_TAC THEN ASM_REWRITE_TAC[HD] THEN REPEAT STRIP_TAC);
\r
3003 (REWRITE_TAC[ASSUME `voronoi_list V [u0; u1; u2; u3] = {a:real^3}`]);
\r
3004 (REWRITE_TAC[CLOSEST_POINT_SING]);
\r
3005 (ASM_MESON_TAC[]);
\r
3006 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_3]);
\r
3007 (ASM_MESON_TAC[]);
\r
3008 (UP_ASM_TAC THEN REPEAT STRIP_TAC);
\r
3010 (EXISTS_TAC `s:real^3`);
\r
3011 (ASM_REWRITE_TAC[]);
\r
3012 (REWRITE_TAC[mxi]);
\r
3015 (UNDISCH_TAC `hl (truncate_simplex 2 (ul:(real^3)list)) < sqrt (&2)`);
\r
3016 (ASM_REWRITE_TAC[]);
\r
3017 (ASM_REAL_ARITH_TAC);
\r
3019 (UP_ASM_TAC THEN MESON_TAC[]);
\r
3020 (MATCH_MP_TAC SELECT_UNIQUE);
\r
3021 (REPEAT STRIP_TAC);
\r
3022 (REWRITE_TAC[BETA_THM]);
\r
3023 (REWRITE_TAC[GSYM BETWEEN_IN_CONVEX_HULL;HD]);
\r
3024 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
\r
3027 (ASM_REWRITE_TAC[]);
\r
3028 (ASM_MESON_TAC[DIST_SYM]);
\r
3030 (DEL_TAC THEN UP_ASM_TAC THEN UP_ASM_TAC THEN
\r
3031 REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;
\r
3032 CONVEX_HULL_2; IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC);
\r
3033 (ABBREV_TAC `a = omega_list_n V [u0; u1; u2; u3:real^3] 2`);
\r
3034 (ABBREV_TAC `b = omega_list_n V [u0; u1; u2; u3:real^3] 3`);
\r
3035 (NEW_GOAL `s = u % a + v % (b:real^3)`);
\r
3036 (ASM_MESON_TAC[]);
\r
3037 (NEW_GOAL `?c. c IN aff {a, b} /\ (u0 - c) dot (a - b:real^3) = &0`);
\r
3038 (REWRITE_TAC[Trigonometry2.EXISTS_PROJECTING_POINT2]);
\r
3039 (FIRST_X_ASSUM CHOOSE_TAC);
\r
3040 (UP_ASM_TAC THEN REWRITE_TAC[Trigonometry2.AFF2;IN;IN_ELIM_THM]);
\r
3041 (REPEAT STRIP_TAC);
\r
3044 (NEW_GOAL `dist (u0, a:real^3) < sqrt (&2)`);
\r
3045 (REWRITE_WITH `dist (u0, a:real^3) = hl (truncate_simplex 2 (ul:(real^3)list))`);
\r
3046 (ABBREV_TAC `vl = truncate_simplex 2 (ul:(real^3)list)`);
\r
3047 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
\r
3048 (ONCE_REWRITE_TAC[DIST_SYM]);
\r
3049 (REWRITE_WITH `a:real^3 = omega_list V vl`);
\r
3050 (EXPAND_TAC "vl" THEN DEL_TAC);
\r
3051 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2; LENGTH; ARITH_RULE `SUC (SUC (SUC 0)) - 1 = 2`]);
\r
3053 (REWRITE_TAC[Marchal_cells.OMEGA_LIST_TRUNCATE_2]);
\r
3054 (REWRITE_WITH `u0:real^3 = HD vl`);
\r
3055 (EXPAND_TAC "vl" THEN DEL_TAC);
\r
3056 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2; HD]);
\r
3057 (MATCH_MP_TAC Rogers.WAUFCHE2);
\r
3059 (ASM_REWRITE_TAC[]);
\r
3060 (EXPAND_TAC "vl" THEN DEL_TAC);
\r
3061 (ASM_REWRITE_TAC[IN]);
\r
3062 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
\r
3064 (ASM_MESON_TAC [ARITH_RULE `2 <= 3 `]);
\r
3065 (ASM_REWRITE_TAC[]);
\r
3067 (NEW_GOAL `dist (u0, b:real^3) >= sqrt (&2)`);
\r
3068 (REWRITE_WITH `dist (u0, b:real^3) = hl (ul:(real^3)list)`);
\r
3069 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
\r
3070 (SUBGOAL_THEN `?m. voronoi_list V ul = {m:real^3} /\
\r
3071 m = circumcenter (set_of_list ul) /\
\r
3072 hl ul = dist (HD ul,m)` CHOOSE_TAC);
\r
3073 (ASM_SIMP_TAC [VORONOI_LIST_3_SINGLETON_EXPLICIT]);
\r
3074 (NEW_GOAL `(b:real^3) IN voronoi_list V ul`);
\r
3076 (REWRITE_TAC[OMEGA_LIST_N; ARITH_RULE `3 = SUC 2`]);
\r
3077 (REWRITE_TAC[ARITH_RULE `SUC 2 = 3`; TRUNCATE_SIMPLEX_EXPLICIT_3]);
\r
3078 (REWRITE_TAC[ASSUME `ul = [u0; u1; u2; u3:real^3]`]);
\r
3079 (MATCH_MP_TAC CLOSEST_POINT_IN_SET);
\r
3080 (REWRITE_TAC[Packing3.CLOSED_VORONOI_LIST]);
\r
3081 (REWRITE_TAC[GSYM (ASSUME `ul = [u0;u1;u2;u3:real^3]`)]);
\r
3082 (UP_ASM_TAC THEN REPEAT STRIP_TAC);
\r
3085 (UP_ASM_TAC THEN UP_ASM_TAC THEN REPEAT STRIP_TAC);
\r
3086 (UP_ASM_TAC THEN REWRITE_TAC[ASSUME `voronoi_list V ul = {m:real^3}`]);
\r
3087 (REWRITE_TAC[IN_SING] THEN STRIP_TAC);
\r
3088 (REWRITE_WITH `u0:real^3 = HD ul`);
\r
3089 (ASM_REWRITE_TAC[HD]);
\r
3090 (REWRITE_TAC[ASSUME `b = m:real^3`]);
\r
3091 (ASM_REWRITE_TAC[]);
\r
3092 (ASM_REWRITE_TAC[]);
\r
3094 (REWRITE_TAC[GSYM (ASSUME `ul = [u0;u1;u2;u3:real^3]`)]
\r
3095 THEN ASM_REAL_ARITH_TAC);
\r
3097 (* ======================================================================== *)
\r
3099 (ASM_CASES_TAC `y = s:real^3`);
\r
3100 (ASM_MESON_TAC[]);
\r
3101 (NEW_GOAL `between y (a, b:real^3)`);
\r
3102 (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL; CONVEX_HULL_2;IN;IN_ELIM_THM]);
\r
3103 (EXISTS_TAC `u':real` THEN EXISTS_TAC `v':real` THEN ASM_REWRITE_TAC[]);
\r
3104 (NEW_GOAL `between s (a, b:real^3)`);
\r
3105 (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL; CONVEX_HULL_2;IN;IN_ELIM_THM]);
\r
3106 (EXISTS_TAC `u:real` THEN EXISTS_TAC `v:real` THEN ASM_REWRITE_TAC[]);
\r
3107 (ASM_CASES_TAC `between y (s, a:real^3)`);
\r
3109 (NEW_GOAL `dist (u0,y) < dist (u0,s:real^3)`);
\r
3110 (MATCH_MP_TAC DIST_BETWEEN_FURTHEST_LT);
\r
3111 (EXISTS_TAC `a:real^3`);
\r
3112 (REPEAT STRIP_TAC);
\r
3114 (ASM_REWRITE_TAC[]);
\r
3115 (ASM_MESON_TAC[]);
\r
3116 (NEW_GOAL `dist (y:real^3,u0) < sqrt (&2)`);
\r
3117 (REWRITE_TAC[ASSUME `y = a:real^3`]);
\r
3118 (ONCE_REWRITE_TAC[DIST_SYM]);
\r
3119 (ASM_MESON_TAC[]);
\r
3120 (ASM_REAL_ARITH_TAC);
\r
3122 (NEW_GOAL `dist (u0:real^3,s) < sqrt (&2)`);
\r
3123 (REWRITE_TAC[ASSUME `s = a:real^3`]);
\r
3124 (ASM_MESON_TAC[]);
\r
3125 (ASM_REAL_ARITH_TAC);
\r
3127 (ASM_REAL_ARITH_TAC);
\r
3129 (UP_ASM_TAC THEN REWRITE_WITH `dist (u0,y) = dist (y,u0:real^3)`);
\r
3130 (MESON_TAC[DIST_SYM]);
\r
3131 (ASM_REWRITE_TAC[]);
\r
3133 (UP_ASM_TAC THEN MESON_TAC[]);
\r
3136 (ASM_CASES_TAC `between s (y, a:real^3)`);
\r
3138 (NEW_GOAL `dist (u0,s) < dist (u0,y:real^3)`);
\r
3139 (MATCH_MP_TAC DIST_BETWEEN_FURTHEST_LT);
\r
3140 (EXISTS_TAC `a:real^3`);
\r
3141 (REPEAT STRIP_TAC);
\r
3143 (ASM_REWRITE_TAC[]);
\r
3144 (ASM_MESON_TAC[]);
\r
3145 (NEW_GOAL `dist (u0,s:real^3) < sqrt (&2)`);
\r
3146 (REWRITE_TAC[ASSUME `s = a:real^3`]);
\r
3147 (ASM_MESON_TAC[]);
\r
3148 (ASM_REAL_ARITH_TAC);
\r
3150 (NEW_GOAL `dist (y, u0:real^3) < sqrt (&2)`);
\r
3151 (REWRITE_TAC[ASSUME `y = a:real^3`]);
\r
3152 (ONCE_REWRITE_TAC[DIST_SYM]);
\r
3153 (ASM_MESON_TAC[]);
\r
3154 (ASM_REAL_ARITH_TAC);
\r
3156 (REWRITE_WITH `dist (u0,y:real^3) = dist (y, u0)`);
\r
3157 (MESON_TAC[DIST_SYM]);
\r
3158 (ASM_REAL_ARITH_TAC);
\r
3160 (UP_ASM_TAC THEN REWRITE_WITH `dist (u0,y) = dist (y,u0:real^3)`);
\r
3161 (MESON_TAC[DIST_SYM]);
\r
3162 (ASM_REWRITE_TAC[]);
\r
3164 (UP_ASM_TAC THEN MESON_TAC[]);
\r
3166 (NEW_GOAL `collinear {y, s, a:real^3}`);
\r
3167 (MATCH_MP_TAC AFFINE_HULL_3_IMP_COLLINEAR);
\r
3168 (REWRITE_TAC[AFFINE_HULL_2;IN;IN_ELIM_THM]);
\r
3169 (ASM_REWRITE_TAC[]);
\r
3171 (EXISTS_TAC `v / (v - v')`);
\r
3172 (EXISTS_TAC `&1 - v / (v - v')`);
\r
3173 (REWRITE_TAC[REAL_ARITH `a + &1 - a = &1`]);
\r
3174 (REWRITE_TAC[VECTOR_ARITH `a = x1 % (u' % a + v' % b) + x2 % (u % a + v % b)
\r
3175 <=> (&1 - x1 * u' - x2 * u) % a - (x1 * v' + x2 * v) % b = vec 0`]);
\r
3176 (REWRITE_WITH `&1 - v / (v - v') * u' - (&1 - v / (v - v')) * u = &0`);
\r
3177 (REWRITE_TAC[REAL_ARITH `&1 - v / (v - v') * u' - (&1 - v / (v - v')) * u =
\r
3178 (&1 - u) + v * (u - u') / (v - v') `]);
\r
3179 (REWRITE_WITH `u - u' = v' - v:real`);
\r
3180 (ASM_REAL_ARITH_TAC);
\r
3181 (REWRITE_TAC[REAL_ARITH `&1 - u + v * (v' - v) / (v - v') = &1 - u - v * (v - v') / (v - v')`]);
\r
3182 (REWRITE_WITH `(v - v') / (v - v') = &1`);
\r
3183 (MATCH_MP_TAC REAL_DIV_REFL);
\r
3184 (REWRITE_TAC[REAL_ARITH `b - a = &0 <=> a = b`]);
\r
3187 (NEW_GOAL `s = y:real^3`);
\r
3188 (REWRITE_TAC[ASSUME `y = u' % a + v' % (b:real^3)`;
\r
3189 ASSUME `s = u % a + v % (b:real^3)`]);
\r
3190 (NEW_GOAL `u = u':real`);
\r
3191 (ASM_REAL_ARITH_TAC);
\r
3192 (REWRITE_TAC[ASSUME `v' = v:real`; ASSUME `u = u':real`]);
\r
3193 (ASM_MESON_TAC[]);
\r
3194 (ASM_REAL_ARITH_TAC);
\r
3196 (REWRITE_WITH `v / (v - v') * v' + (&1 - v / (v - v')) * v = &0`);
\r
3197 (REWRITE_TAC[REAL_ARITH `v / (v - v') * v' + (&1 - v / (v - v')) * v =
\r
3198 v - v * (v - v') / (v - v') `]);
\r
3199 (REWRITE_WITH `(v - v') / (v - v') = &1`);
\r
3200 (MATCH_MP_TAC REAL_DIV_REFL);
\r
3201 (REWRITE_TAC[REAL_ARITH `b - a = &0 <=> a = b`]);
\r
3203 (NEW_GOAL `s = y:real^3`);
\r
3204 (REWRITE_TAC[ASSUME `y = u' % a + v' % (b:real^3)`;
\r
3205 ASSUME `s = u % a + v % (b:real^3)`]);
\r
3206 (NEW_GOAL `u = u':real`);
\r
3207 (ASM_REAL_ARITH_TAC);
\r
3208 (REWRITE_TAC[ASSUME `v' = v:real`; ASSUME `u = u':real`]);
\r
3209 (ASM_MESON_TAC[]);
\r
3210 (ASM_REAL_ARITH_TAC);
\r
3211 (VECTOR_ARITH_TAC);
\r
3213 (NEW_GOAL `between a (s, y:real^3)`);
\r
3214 (UP_ASM_TAC THEN REWRITE_TAC[COLLINEAR_BETWEEN_CASES]);
\r
3215 (ASM_MESON_TAC[BETWEEN_SYM]);
\r
3216 (UP_ASM_TAC THEN REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;CONVEX_HULL_2;IN;
\r
3217 IN_ELIM_THM] THEN REPEAT STRIP_TAC);
\r
3218 (NEW_GOAL `a = u'' % s + v'' % (y:real^3)`);
\r
3219 (UP_ASM_TAC THEN REWRITE_TAC[]);
\r
3220 (UP_ASM_TAC THEN REWRITE_TAC[ASSUME `y = u' % a + v' % (b:real^3)`;
\r
3221 ASSUME `s = u % a + v % (b:real^3)`]);
\r
3223 (REWRITE_TAC[VECTOR_ARITH
\r
3224 `a = u'' % (u % a + v % b) + v'' % (u' % a + v' % b)
\r
3225 <=> (u''* u + v'' * u' - &1) % a + (u'' * v + v'' * v') % b = vec 0`]);
\r
3226 (REWRITE_WITH `(u'' * v + v'' * v') = -- (u'' * u + v'' * u' - &1)`);
\r
3227 (REWRITE_TAC[REAL_ARITH `u'' * v + v'' * v' = --(u'' * u + v'' * u' - &1) <=>
\r
3228 u'' * (u + v) + v'' * (u' + v') = &1`]);
\r
3229 (ASM_REWRITE_TAC[REAL_MUL_RID]);
\r
3230 (REWRITE_TAC[VECTOR_ARITH `a % x + -- a % y = a % (x - y)`;VECTOR_MUL_EQ_0]);
\r
3231 (REPEAT STRIP_TAC);
\r
3232 (NEW_GOAL `u'' * u <= u'' * (u + v)`);
\r
3233 (REWRITE_TAC[REAL_ARITH `a * b <= a * (b + c) <=> &0 <= a * c`]);
\r
3234 (ASM_SIMP_TAC[REAL_LE_MUL]);
\r
3235 (NEW_GOAL `v'' * u' <= v'' * (u' + v')`);
\r
3236 (REWRITE_TAC[REAL_ARITH `a * b <= a * (b + c) <=> &0 <= a * c`]);
\r
3237 (ASM_SIMP_TAC[REAL_LE_MUL]);
\r
3238 (NEW_GOAL `u'' * (u + v) + v'' * (u' + v') = &1`);
\r
3239 (ASM_REWRITE_TAC[REAL_MUL_RID]);
\r
3240 (NEW_GOAL `v'' * u' = v'' * (u' + v')`);
\r
3241 (ASM_REAL_ARITH_TAC);
\r
3242 (UP_ASM_TAC THEN REWRITE_TAC[REAL_ARITH `a * b = a * (b + c) <=> &0 = a * c`]);
\r
3244 (NEW_GOAL `u'' * u = u'' * (u + v)`);
\r
3245 (ASM_REAL_ARITH_TAC);
\r
3246 (UP_ASM_TAC THEN REWRITE_TAC[REAL_ARITH `a * b = a * (b + c) <=> &0 = a * c`]);
\r
3249 (NEW_GOAL `~(u'' = &0)`);
\r
3251 (NEW_GOAL `a = y:real^3`);
\r
3252 (REWRITE_TAC[ASSUME `a = u'' % s + v'' % (y:real^3)`]);
\r
3253 (REWRITE_WITH `u'' = &0 /\ v'' = &1`);
\r
3254 (ASM_REAL_ARITH_TAC);
\r
3255 (VECTOR_ARITH_TAC);
\r
3256 (NEW_GOAL `dist (y, u0:real^3) < sqrt (&2)`);
\r
3257 (ONCE_REWRITE_TAC[DIST_SYM]);
\r
3258 (REWRITE_TAC[GSYM (ASSUME `a = y:real^3`)]);
\r
3259 (ASM_MESON_TAC[]);
\r
3260 (ASM_REAL_ARITH_TAC);
\r
3262 (NEW_GOAL `v = &0`);
\r
3263 (MP_TAC (GSYM (ASSUME `&0 = u'' * v`)));
\r
3264 (REWRITE_TAC[REAL_ENTIRE]);
\r
3265 (ASM_MESON_TAC[]);
\r
3267 (NEW_GOAL `a = s:real^3`);
\r
3268 (REWRITE_TAC[ASSUME `s = u % a + v % (b:real^3)`]);
\r
3269 (REWRITE_WITH `u = &1 /\ v = &0`);
\r
3270 (ASM_REAL_ARITH_TAC);
\r
3271 (VECTOR_ARITH_TAC);
\r
3272 (NEW_GOAL `dist (u0:real^3, s) < sqrt (&2)`);
\r
3273 (REWRITE_TAC[GSYM (ASSUME `a = s:real^3`)]);
\r
3274 (ASM_MESON_TAC[]);
\r
3276 (ASM_REAL_ARITH_TAC);
\r
3277 (ASM_MESON_TAC[]);
\r
3278 (UP_ASM_TAC THEN REWRITE_TAC[VECTOR_ARITH `a - b = vec 0 <=> a = b`]);
\r
3280 (NEW_GOAL `dist (u0,a:real^3) >= sqrt (&2)`);
\r
3281 (REWRITE_TAC[(ASSUME `a = b:real^3`)]);
\r
3282 (ASM_MESON_TAC[]);
\r
3283 (ASM_REAL_ARITH_TAC)]);;
\r
3285 (* ======================================================================= *)
\r
3287 let CONVEX_HULL_4_IMP_2_2 = prove_by_refinement (
\r
3288 `!a b c d p:real^3.
\r
3289 p IN convex hull {a,b,c,d}
\r
3290 ==> (?m n. between p (m,n) /\ between m (a,b) /\ between n (c,d))`,
\r
3291 [(REWRITE_TAC[CONVEX_HULL_4;IN;IN_ELIM_THM] THEN REPEAT STRIP_TAC);
\r
3292 (ASM_CASES_TAC `u + v = &0`);
\r
3293 (NEW_GOAL `u = &0 /\ v = &0`);
\r
3294 (ASM_REAL_ARITH_TAC);
\r
3295 (EXISTS_TAC `a:real^3` THEN EXISTS_TAC `p:real^3`);
\r
3296 (REWRITE_TAC[BETWEEN_REFL]);
\r
3297 (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;CONVEX_HULL_2;IN;IN_ELIM_THM]);
\r
3298 (EXISTS_TAC `w:real` THEN EXISTS_TAC `z:real`);
\r
3299 (ASM_REWRITE_TAC[]);
\r
3301 (ASM_REAL_ARITH_TAC);
\r
3302 (VECTOR_ARITH_TAC);
\r
3304 (ASM_CASES_TAC `w + z = &0`);
\r
3305 (NEW_GOAL `w = &0 /\ z = &0`);
\r
3306 (ASM_REAL_ARITH_TAC);
\r
3307 (EXISTS_TAC `p:real^3` THEN EXISTS_TAC `c:real^3`);
\r
3308 (REWRITE_TAC[BETWEEN_REFL]);
\r
3309 (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;CONVEX_HULL_2;IN;IN_ELIM_THM]);
\r
3310 (EXISTS_TAC `u:real` THEN EXISTS_TAC `v:real`);
\r
3311 (ASM_REWRITE_TAC[]);
\r
3313 (ASM_REAL_ARITH_TAC);
\r
3314 (VECTOR_ARITH_TAC);
\r
3316 (EXISTS_TAC `u/(u+v) % (a:real^3) + v /(u+v) % b`);
\r
3317 (EXISTS_TAC `w/(w+z) % (c:real^3) + z/(w+z) % d`);
\r
3318 (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;CONVEX_HULL_2;IN;IN_ELIM_THM]);
\r
3319 (REPEAT STRIP_TAC);
\r
3320 (EXISTS_TAC `u + v` THEN EXISTS_TAC `w + z`);
\r
3321 (REPEAT STRIP_TAC);
\r
3322 (ASM_REAL_ARITH_TAC);
\r
3323 (ASM_REAL_ARITH_TAC);
\r
3324 (ASM_REAL_ARITH_TAC);
\r
3325 (ASM_REWRITE_TAC[VECTOR_ARITH `x % (y/x % a + z/x % b) = (x/x) % (y %a + z % b)`]);
\r
3326 (REWRITE_WITH `(u+v)/(u+v) = &1 /\ (w+z)/(w+z) = &1`);
\r
3328 (MATCH_MP_TAC REAL_DIV_REFL);
\r
3329 (ASM_REWRITE_TAC[]);
\r
3330 (MATCH_MP_TAC REAL_DIV_REFL);
\r
3331 (ASM_REWRITE_TAC[]);
\r
3332 (VECTOR_ARITH_TAC);
\r
3333 (EXISTS_TAC `u / (u + v)` THEN EXISTS_TAC `v / (u + v)`);
\r
3334 (ASM_REWRITE_TAC[]);
\r
3335 (REPEAT STRIP_TAC);
\r
3336 (MATCH_MP_TAC REAL_LE_DIV);
\r
3337 (ASM_REAL_ARITH_TAC);
\r
3338 (MATCH_MP_TAC REAL_LE_DIV);
\r
3339 (ASM_REAL_ARITH_TAC);
\r
3340 (REWRITE_TAC[REAL_ARITH `u /(u + v) + v / (u + v) = (u+v)/(u+v)`]);
\r
3341 (MATCH_MP_TAC REAL_DIV_REFL);
\r
3342 (ASM_REWRITE_TAC[]);
\r
3344 (EXISTS_TAC `w / (w + z)` THEN EXISTS_TAC `z / (w + z)`);
\r
3345 (ASM_REWRITE_TAC[]);
\r
3346 (REPEAT STRIP_TAC);
\r
3347 (MATCH_MP_TAC REAL_LE_DIV);
\r
3348 (ASM_REAL_ARITH_TAC);
\r
3349 (MATCH_MP_TAC REAL_LE_DIV);
\r
3350 (ASM_REAL_ARITH_TAC);
\r
3351 (REWRITE_TAC[REAL_ARITH `u /(u + v) + v / (u + v) = (u+v)/(u+v)`]);
\r
3352 (MATCH_MP_TAC REAL_DIV_REFL);
\r
3353 (ASM_REWRITE_TAC[])]);;
\r
3355 (* ======================================================================= *)
\r
3357 let proj_point = new_definition
\r
3358 `!e x. proj_point e x = x - projection e x`;;
\r
3360 let projection_proj_point = prove_by_refinement (
\r
3361 `!e x. projection e x = x - proj_point e x`,
\r
3362 [ REWRITE_TAC[proj_point] THEN VECTOR_ARITH_TAC]);;
\r
3364 let PRO_EXP = prove_by_refinement(
\r
3365 `!e x. proj_point e x = (x dot e) / (e dot e) % e`,
\r
3366 [REWRITE_TAC[projection;proj_point] THEN VECTOR_ARITH_TAC]);;
\r
3368 (* ======================================================================= *)
\r
3370 let BETWEEN_PROJ_POINT = prove_by_refinement (
\r
3371 `!a b x e. between x (a,b) ==>
\r
3372 between (proj_point e x) (proj_point e a, proj_point e b)`,
\r
3373 [(REWRITE_TAC[BETWEEN_IN_CONVEX_HULL; CONVEX_HULL_2;IN;IN_ELIM_THM; PRO_EXP]);
\r
3374 (REPEAT STRIP_TAC THEN EXISTS_TAC `u:real` THEN EXISTS_TAC `v:real`);
\r
3375 (ASM_REWRITE_TAC[]);
\r
3376 (REWRITE_TAC[VECTOR_MUL_ASSOC;
\r
3377 VECTOR_ARITH `x % a = m % a + n % a <=> (x -m - n) % a = vec 0`;
\r
3378 REAL_ARITH `a / x - u * b / x - v * c / x = (a - u*b - v*c) / x`]);
\r
3379 (REWRITE_TAC[VECTOR_ARITH
\r
3380 `(u % a + v % b) dot e - u * (a dot e) - v * (b dot e) = &0`]);
\r
3381 (REWRITE_TAC[REAL_ARITH `&0/a = &0`]);
\r
3382 (VECTOR_ARITH_TAC)]);;
\r
3384 (* ======================================================================= *)
\r
3386 let PARALLEL_PROJECTION = prove_by_refinement (
\r
3387 `!x y a:real^N b. between x (a, y) /\ ~(a = b)
\r
3388 ==> (?k. k <= &1 /\ &0 <= k /\
\r
3389 projection (b - a) (x - a) = k % projection (b - a) (y - a))`,
\r
3390 [(REWRITE_TAC[projection; BETWEEN_IN_CONVEX_HULL;CONVEX_HULL_2;IN;IN_ELIM_THM]
\r
3391 THEN REPEAT STRIP_TAC);
\r
3392 (NEW_GOAL `(x - a) = v % (y - a:real^N)`);
\r
3393 (REWRITE_WITH `x - a:real^N = (u % a + v % y) - (u + v) % a`);
\r
3394 (ASM_REWRITE_TAC[]);
\r
3395 (VECTOR_ARITH_TAC);
\r
3396 (VECTOR_ARITH_TAC);
\r
3397 (ASM_CASES_TAC `((y - a:real^N) dot (b - a) = &0)`);
\r
3398 (EXISTS_TAC `v:real`);
\r
3399 (REPEAT STRIP_TAC);
\r
3400 (ASM_REAL_ARITH_TAC);
\r
3401 (ASM_REAL_ARITH_TAC);
\r
3402 (ASM_REWRITE_TAC[DOT_LMUL;REAL_MUL_RZERO;Collect_geom.REAL_DIV_LZERO;
\r
3403 VECTOR_MUL_LZERO; VECTOR_SUB_RZERO]);
\r
3404 (EXISTS_TAC `((x - a) dot (b - a)) / ((y - a) dot (b - a:real^N))`);
\r
3405 (REPEAT STRIP_TAC);
\r
3406 (ASM_REWRITE_TAC[DOT_LMUL; REAL_ARITH `(a * b) / c = a * (b / c)`]);
\r
3407 (REWRITE_WITH `((y - a) dot (b - a)) / ((y - a) dot (b - a:real^N)) = &1`);
\r
3408 (MATCH_MP_TAC REAL_DIV_REFL);
\r
3409 (ASM_REWRITE_TAC[]);
\r
3410 (ASM_REAL_ARITH_TAC);
\r
3411 (ASM_REWRITE_TAC[DOT_LMUL; REAL_ARITH `(a * b) / c = a * (b / c)`]);
\r
3412 (REWRITE_WITH `((y - a) dot (b - a)) / ((y - a) dot (b - a:real^N)) = &1`);
\r
3413 (MATCH_MP_TAC REAL_DIV_REFL);
\r
3414 (ASM_REWRITE_TAC[]);
\r
3415 (ASM_REAL_ARITH_TAC);
\r
3416 (REWRITE_WITH `((x - a) dot (b - a)) / ((y - a) dot (b - a:real^N)) %
\r
3417 ((y - a):real^N - ((y - a) dot (b - a)) / ((b - a) dot (b - a)) %
\r
3418 (b - a:real^N)) =
\r
3419 &1 / ((y - a) dot (b - a)) %
\r
3420 ((x - a) dot (b - a)) % (((y - a) - ((y - a) dot (b - a)) / ((b - a) dot
\r
3421 (b - a)) % (b - a)))`);
\r
3422 (VECTOR_ARITH_TAC);
\r
3423 (MATCH_MP_TAC Trigonometry2.VECTOR_MUL_R_TO_L);
\r
3424 (REPEAT STRIP_TAC);
\r
3425 (ASM_MESON_TAC[]);
\r
3426 (ABBREV_TAC `m = (y - a) dot (b - a:real^N)`);
\r
3427 (ABBREV_TAC `n = (x - a) dot (b - a:real^N)`);
\r
3428 (ABBREV_TAC `p = (b - a) dot (b - a:real^N)`);
\r
3429 (REWRITE_TAC[VECTOR_ARITH
\r
3430 `m % (x - n / p % (b - a)) = n % (y - m / p % (b - a)) <=> m % x = n % y`]);
\r
3431 (EXPAND_TAC "m" THEN EXPAND_TAC "n");
\r
3432 (REWRITE_TAC[ASSUME `x - a = v % (y - a:real^N)`; VECTOR_MUL_ASSOC]);
\r
3433 (AP_THM_TAC THEN AP_TERM_TAC);
\r
3434 (VECTOR_ARITH_TAC)]);;
\r
3436 (* ======================================================================= *)
\r
3438 let NORM_PROJECTION_LE = prove_by_refinement(
\r
3439 `!x y a:real^N b. between x (a, y) /\ ~(a = b)
\r
3440 ==> norm (projection (b - a) (x - a)) <= norm (projection (b - a) (y - a))`,
\r
3441 [(REPEAT GEN_TAC THEN DISCH_TAC);
\r
3443 `(?k. k <= &1 /\ &0 <= k /\
\r
3444 projection (b - a) (x - a:real^N) = k % projection (b - a) (y - a))`
\r
3446 (ASM_SIMP_TAC[PARALLEL_PROJECTION]);
\r
3447 (ASM_REWRITE_TAC[NORM_MUL]);
\r
3448 (REWRITE_WITH `abs k = k`);
\r
3449 (ASM_SIMP_TAC[REAL_ABS_REFL]);
\r
3450 (REWRITE_TAC[REAL_ARITH `a * b <= b <=> &0 <= (&1 - a) * b`]);
\r
3451 (MATCH_MP_TAC REAL_LE_MUL);
\r
3453 (ASM_REAL_ARITH_TAC);
\r
3454 (REWRITE_TAC[NORM_POS_LE])]);;
\r
3456 (* ======================================================================= *)
\r
3458 let OMEGA_LIST_TRUNCATE_1_NEW1 = prove_by_refinement (
\r
3459 `!V u0:real^3 u1 u2 u3.
\r
3460 omega_list_n V [u0;u1;u2] 1 = omega_list V [u0;u1] `,
\r
3461 [ (REPEAT GEN_TAC);
\r
3462 (REWRITE_TAC[OMEGA_LIST]);
\r
3463 (REWRITE_WITH `LENGTH [u0:real^3;u1] - 1 = 1`);
\r
3464 (REWRITE_TAC[LENGTH; ARITH_RULE `SUC (SUC 0) - 1 = 1`]);
\r
3465 (REWRITE_TAC[ARITH_RULE `1 = SUC 0`; OMEGA_LIST_N]);
\r
3466 (REWRITE_TAC[ARITH_RULE `SUC 0 = 1`;TRUNCATE_SIMPLEX_EXPLICIT_1;HD])]);;
\r
3468 let OMEGA_LIST_TRUNCATE_1_NEW2 = prove_by_refinement (
\r
3469 `!V u0:real^3 u1 u2 u3.
\r
3470 omega_list_n V [u0;u1] 1 = omega_list V [u0;u1] `,
\r
3471 [ (REPEAT GEN_TAC);
\r
3472 (REWRITE_TAC[OMEGA_LIST]);
\r
3473 (REWRITE_WITH `LENGTH [u0:real^3;u1] - 1 = 1`);
\r
3474 (REWRITE_TAC[LENGTH; ARITH_RULE `SUC (SUC 0) - 1 = 1`])]);;
\r
3476 let OMEGA_LIST_TRUNCATE_2_NEW1 = prove_by_refinement (
\r
3477 `!V u0:real^3 u1 u2 u3.
\r
3478 omega_list_n V [u0;u1;u2:real^3] 2 = omega_list V [u0;u1;u2]`,
\r
3479 [(REPEAT GEN_TAC);
\r
3480 (REWRITE_TAC[OMEGA_LIST]);
\r
3481 (REWRITE_WITH `LENGTH [u0:real^3;u1;u2] - 1 = 2`);
\r
3482 (REWRITE_TAC[LENGTH; ARITH_RULE `SUC (SUC (SUC 0)) - 1 = 2`])]);;
\r
3484 (* ======================================================================= *)
\r
3486 let IN_AFFINE_KY_LEMMA1 = prove_by_refinement (
\r
3487 `!x s. x IN s ==> x IN affine hull s`,
\r
3488 [(REPEAT STRIP_TAC);
\r
3489 (REWRITE_TAC[affine;hull;IN_INTERS]);
\r
3490 (REWRITE_TAC[IN;IN_ELIM_THM]);
\r
3491 (REPEAT STRIP_TAC);
\r
3492 (UP_ASM_TAC THEN SWITCH_TAC THEN UP_ASM_TAC THEN SET_TAC[])]);;
\r
3494 (* ======================================================================= *)
\r
3496 let AFFINE_SUBSET_KY_LEMMA = prove_by_refinement (
\r
3497 `!S B:real^N ->bool. S SUBSET B ==> affine hull S SUBSET affine hull B`,
\r
3498 [(REWRITE_TAC[SUBSET;AFFINE_HULL_EXPLICIT; IN;IN_ELIM_THM] THEN
\r
3499 REPEAT STRIP_TAC);
\r
3500 (EXISTS_TAC `s:real^N->bool`);
\r
3501 (EXISTS_TAC `u:real^N->real`);
\r
3502 (ASM_REWRITE_TAC[]);
\r
3503 (ASM_MESON_TAC[])]);;
\r
3505 (* ======================================================================= *)
\r
3507 let TRANSLATE_AFFINE_KY_LEMMA1 = prove_by_refinement(
\r
3508 `!a:real^3 b c x y z k.
\r
3509 a IN affine hull {x,y,z} /\
\r
3510 b IN affine hull {x,y,z} /\
\r
3511 c IN affine hull {x,y,z}
\r
3512 ==> a + k % (b - c) IN affine hull {x,y,z}`,
\r
3513 [(REWRITE_TAC[AFFINE_HULL_3;IN;IN_ELIM_THM] THEN REPEAT STRIP_TAC);
\r
3514 (EXISTS_TAC `u + k * (u' - u'')`);
\r
3515 (EXISTS_TAC `v + k * (v' - v'')`);
\r
3516 (EXISTS_TAC `w + k * (w' - w'')`);
\r
3519 `(u + k * (u' - u'')) + (v + k * (v' - v'')) + w + k * (w' - w'') =
\r
3520 (u + v + w) + k * (u' + v' + w') - k * (u'' + v'' + w'')`);
\r
3522 (ASM_REWRITE_TAC[REAL_SUB_REFL;REAL_ADD_RID]);
\r
3523 (ASM_REWRITE_TAC[]);
\r
3524 (VECTOR_ARITH_TAC)]);;
\r
3526 (* ======================================================================= *)
\r
3528 let IN_AFFINE_HULL_KY_LEMMA3 = prove_by_refinement (
\r
3529 `!x:real^3 y z p a r.
\r
3530 p + a IN affine hull {x,y,z} /\
\r
3531 p + r % a IN affine hull {x,y,z} /\
\r
3533 ==> p IN affine hull {x,y,z}`,
\r
3534 [(REWRITE_TAC[AFFINE_HULL_3;IN;IN_ELIM_THM] THEN REPEAT STRIP_TAC);
\r
3535 (EXISTS_TAC `u + (u' - u) / (&1 - r)`);
\r
3536 (EXISTS_TAC `v + (v' - v) / (&1 - r)`);
\r
3537 (EXISTS_TAC `w + (w' - w) / (&1 - r)`);
\r
3539 (REWRITE_TAC [REAL_ARITH
\r
3540 `(u + (u' - u) / (&1 - r)) + (v + (v' - v) / (&1 - r)) +
\r
3541 w + (w' - w) / (&1 - r)
\r
3542 = (u + v + w) + ((u' + v' + w') - (u + v + w))/ (&1 - r)`]);
\r
3543 (ASM_REWRITE_TAC[]);
\r
3546 `(u + (u' - u) / (&1 - r)) % (x:real^3) +
\r
3547 (v + (v' - v) / (&1 - r)) % y +
\r
3548 (w + (w' - w) / (&1 - r)) % z =
\r
3549 (p + a) - (&1/(&1 - r)) % ((p + a) - (p + r % a))`);
\r
3550 (ASM_REWRITE_TAC[]);
\r
3551 (VECTOR_ARITH_TAC);
\r
3552 (REWRITE_TAC[VECTOR_ARITH
\r
3553 `p = (p + a) - &1 / (&1 - r) % ((p + a) - (p + r % a))
\r
3554 <=> ((&1 - r) / (&1 - r) - &1) % a = vec 0`]);
\r
3555 (REWRITE_WITH `(&1 - r) / (&1 - r) = &1`);
\r
3557 (MATCH_MP_TAC REAL_DIV_REFL);
\r
3558 (ASM_REAL_ARITH_TAC);
\r
3559 (REWRITE_TAC[REAL_SUB_REFL;VECTOR_MUL_LZERO])]);;
\r
3561 let IN_AFFINE_HULL_KY_LEMMA3_alt = prove_by_refinement (
\r
3562 `!x:real^3 y z p a r.
\r
3563 p - a IN affine hull {x, y, z} /\
\r
3564 p - r % a IN affine hull {x, y, z} /\
\r
3566 ==> p IN affine hull {x, y, z}`,
\r
3567 [(REWRITE_TAC[VECTOR_ARITH `p - a:real^3 = p + (-- a)`;
\r
3568 VECTOR_ARITH `--(r % a) = r % (-- a)`]);
\r
3569 (REWRITE_TAC[IN_AFFINE_HULL_KY_LEMMA3])]);;
\r
3571 (* ======================================================================= *)
\r
3573 let IN_AFFINE_HULL_3_KY_LEMMA2 = prove_by_refinement (
\r
3574 `!X Y Z a b c. X IN affine hull {a,b,c} /\
\r
3575 Y IN affine hull {a,b,c} /\
\r
3577 ==> Z IN affine hull {a,b,c:real^3}`,
\r
3578 [(REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;CONVEX_HULL_2;
\r
3579 AFFINE_HULL_3;IN;IN_ELIM_THM] THEN REPEAT STRIP_TAC);
\r
3580 (EXISTS_TAC `u'' * u + v'' * u'`);
\r
3581 (EXISTS_TAC `u'' * v + v'' * v'`);
\r
3582 (EXISTS_TAC `u'' * w + v'' * w'`);
\r
3584 (REWRITE_TAC[REAL_ARITH
\r
3585 `(a * x + b * x') + (a * y + b * y') + (a * z + b * z') =
\r
3586 a * (x + y + z) + b * (x' + y' + z')`]);
\r
3587 (ASM_REWRITE_TAC[]);
\r
3588 (ASM_REAL_ARITH_TAC);
\r
3589 (ASM_REWRITE_TAC[]);
\r
3590 (VECTOR_ARITH_TAC)]);;
\r
3592 (* ======================================================================= *)
\r
3594 let SUM_CLAUSES_alt = prove (`(!x f s.
\r
3596 ==> sum (x INSERT s) f =
\r
3597 (if x IN s then sum s f else f x + sum s f))`, REWRITE_TAC[SUM_CLAUSES]);;
\r
3599 let SUM_DIS4 = prove_by_refinement (
\r
3600 `!x:A y z t f. CARD {x,y, z, t} = 4
\r
3601 ==> sum {x,y,z,t} f = f x + f y + f z + f t`,
\r
3602 [(REPEAT STRIP_TAC);
\r
3603 (REWRITE_WITH `sum {x,y, z, t} f =
\r
3604 (if x IN {y, z, t:A} then sum {y, z, t} f
\r
3605 else f x + sum {y, z, t} f)`);
\r
3606 (MATCH_MP_TAC SUM_CLAUSES_alt);
\r
3607 (REWRITE_TAC[Geomdetail.FINITE6]);(COND_CASES_TAC);(NEW_GOAL `F`);
\r
3608 (UP_ASM_TAC THEN REWRITE_TAC
\r
3609 [SET_RULE `x IN {a,b,c} <=> x = a \/ x = b \/ x = c`]);
\r
3610 (REPEAT STRIP_TAC);
\r
3611 (SWITCH_TAC THEN UP_ASM_TAC THEN ASM_REWRITE_TAC
\r
3612 [SET_RULE `{y,y,z,t} = {y,z,t}`] THEN STRIP_TAC);
\r
3613 (NEW_GOAL `CARD {y, z, t:A} <= 3`);
\r
3614 (REWRITE_TAC[Geomdetail.CARD3]);
\r
3616 (SWITCH_TAC THEN UP_ASM_TAC THEN ASM_REWRITE_TAC
\r
3617 [SET_RULE `{z,y,z,t} = {y,z,t}`] THEN STRIP_TAC);
\r
3618 (NEW_GOAL `CARD {y, z, t:A} <= 3`);
\r
3619 (REWRITE_TAC[Geomdetail.CARD3]);
\r
3621 (SWITCH_TAC THEN UP_ASM_TAC THEN ASM_REWRITE_TAC
\r
3622 [SET_RULE `{t,y,z,t} = {y,z,t}`] THEN STRIP_TAC);
\r
3623 (NEW_GOAL `CARD {y, z, t:A} <= 3`);
\r
3624 (REWRITE_TAC[Geomdetail.CARD3]);
\r
3626 (ASM_MESON_TAC[]);
\r
3627 (REWRITE_WITH `sum {y, z, t} f =
\r
3628 (if y IN {z, t:A} then sum {z, t} f
\r
3629 else f y + sum {z, t} f)`);
\r
3630 (MATCH_MP_TAC SUM_CLAUSES_alt);
\r
3631 (REWRITE_TAC[Geomdetail.FINITE6]);
\r
3635 (UP_ASM_TAC THEN REWRITE_TAC[SET_RULE `x IN {a,b} <=> x = a \/ x = b`]);
\r
3636 (REPEAT STRIP_TAC);
\r
3637 (SWITCH_TAC THEN UP_ASM_TAC THEN ASM_REWRITE_TAC[SET_RULE `{x,z,z,t} = {x,z,t}`] THEN STRIP_TAC);
\r
3638 (NEW_GOAL `CARD {x, z, t:A} <= 3`);
\r
3639 (REWRITE_TAC[Geomdetail.CARD3]);
\r
3641 (SWITCH_TAC THEN UP_ASM_TAC THEN ASM_REWRITE_TAC[SET_RULE `{x,t,z,t} = {x,z,t}`] THEN STRIP_TAC);
\r
3642 (NEW_GOAL `CARD {x, z, t:A} <= 3`);
\r
3643 (REWRITE_TAC[Geomdetail.CARD3]);
\r
3645 (ASM_MESON_TAC[]);
\r
3647 (REWRITE_WITH `sum {z, t:A} f = f z + f t`);
\r
3648 (MATCH_MP_TAC Collect_geom.SUM_DIS2 THEN STRIP_TAC);
\r
3649 (SWITCH_TAC THEN UP_ASM_TAC THEN ASM_REWRITE_TAC[SET_RULE `{x,y,t,t} = {x,y,t}`] THEN STRIP_TAC);
\r
3650 (NEW_GOAL `CARD {x, y, t:A} <= 3`);
\r
3651 (REWRITE_TAC[Geomdetail.CARD3]);
\r
3652 (ASM_ARITH_TAC)]);;
\r
3654 (* ======================================================================= *)
\r
3656 let CARD4_IMP_DISTINCT = prove (
\r
3657 `!a b c d. CARD {a, b, c, d} = 4 ==> ~(a = b)`,
\r
3658 (REPEAT STRIP_TAC THEN SWITCH_TAC THEN UP_ASM_TAC THEN
\r
3659 ASM_REWRITE_TAC[SET_RULE `{a,a,c,d} = {a,c,d}`] THEN STRIP_TAC) THEN
\r
3660 (ASM_MESON_TAC[Geomdetail.CARD3; ARITH_RULE `~(4 <= 3)`]));;
\r
3662 (* ======================================================================= *)
\r
3664 let VSUM_CLAUSES_alt = prove (`(!x f s.
\r
3666 ==> vsum (x INSERT s) f =
\r
3667 (if x IN s then vsum s f else f x + vsum s f))`, REWRITE_TAC[VSUM_CLAUSES]);;
\r
3668 let VSUM_DIS4 = prove_by_refinement (
\r
3669 `!x:A y z t (f:A->real^N). CARD {x,y, z, t} = 4
\r
3670 ==> vsum {x,y,z,t} f = f x + f y + f z + f t`,
\r
3671 [(REPEAT STRIP_TAC);
\r
3672 (REWRITE_WITH `vsum {x,y, z, t} (f:A->real^N) =
\r
3673 (if x IN {y, z, t:A} then vsum {y, z, t} f
\r
3674 else f x + vsum {y, z, t} f)`);
\r
3675 (MATCH_MP_TAC VSUM_CLAUSES_alt);
\r
3676 (REWRITE_TAC[Geomdetail.FINITE6]);(COND_CASES_TAC);(NEW_GOAL `F`);
\r
3677 (UP_ASM_TAC THEN REWRITE_TAC
\r
3678 [SET_RULE `x IN {a,b,c} <=> x = a \/ x = b \/ x = c`]);
\r
3679 (REPEAT STRIP_TAC);
\r
3680 (SWITCH_TAC THEN UP_ASM_TAC THEN ASM_REWRITE_TAC
\r
3681 [SET_RULE `{y,y,z,t} = {y,z,t}`] THEN STRIP_TAC);
\r
3682 (NEW_GOAL `CARD {y, z, t:A} <= 3`);
\r
3683 (REWRITE_TAC[Geomdetail.CARD3]);
\r
3685 (SWITCH_TAC THEN UP_ASM_TAC THEN ASM_REWRITE_TAC
\r
3686 [SET_RULE `{z,y,z,t} = {y,z,t}`] THEN STRIP_TAC);
\r
3687 (NEW_GOAL `CARD {y, z, t:A} <= 3`);
\r
3688 (REWRITE_TAC[Geomdetail.CARD3]);
\r
3690 (SWITCH_TAC THEN UP_ASM_TAC THEN ASM_REWRITE_TAC
\r
3691 [SET_RULE `{t,y,z,t} = {y,z,t}`] THEN STRIP_TAC);
\r
3692 (NEW_GOAL `CARD {y, z, t:A} <= 3`);
\r
3693 (REWRITE_TAC[Geomdetail.CARD3]);
\r
3695 (ASM_MESON_TAC[]);
\r
3696 (REWRITE_WITH `vsum {y, z, t} (f:A->real^N) =
\r
3697 (if y IN {z, t:A} then vsum {z, t} f
\r
3698 else f y + vsum {z, t} f)`);
\r
3699 (MATCH_MP_TAC VSUM_CLAUSES_alt);
\r
3700 (REWRITE_TAC[Geomdetail.FINITE6]);
\r
3704 (UP_ASM_TAC THEN REWRITE_TAC[SET_RULE `x IN {a,b} <=> x = a \/ x = b`]);
\r
3705 (REPEAT STRIP_TAC);
\r
3706 (SWITCH_TAC THEN UP_ASM_TAC THEN ASM_REWRITE_TAC[SET_RULE `{x,z,z,t} = {x,z,t}`] THEN STRIP_TAC);
\r
3707 (NEW_GOAL `CARD {x, z, t:A} <= 3`);
\r
3708 (REWRITE_TAC[Geomdetail.CARD3]);
\r
3710 (SWITCH_TAC THEN UP_ASM_TAC THEN ASM_REWRITE_TAC[SET_RULE `{x,t,z,t} = {x,z,t}`] THEN STRIP_TAC);
\r
3711 (NEW_GOAL `CARD {x, z, t:A} <= 3`);
\r
3712 (REWRITE_TAC[Geomdetail.CARD3]);
\r
3714 (ASM_MESON_TAC[]);
\r
3716 (REWRITE_WITH `vsum {z, t:A} (f:A->real^N) = f z + f t`);
\r
3717 (MATCH_MP_TAC Collect_geom.VSUM_DIS2 THEN STRIP_TAC);
\r
3718 (SWITCH_TAC THEN UP_ASM_TAC THEN ASM_REWRITE_TAC[SET_RULE `{x,y,t,t} = {x,y,t}`] THEN STRIP_TAC);
\r
3719 (NEW_GOAL `CARD {x, y, t:A} <= 3`);
\r
3720 (REWRITE_TAC[Geomdetail.CARD3]);
\r
3721 (ASM_ARITH_TAC)]);;
\r
3723 (* ======================================================================= *)
\r
3725 let AFFINE_DEPENDENT_KY_LEMMA1 = prove_by_refinement (
\r
3726 `!a:real^3 b c d p:real^3 k1 k2 k3 k4.
\r
3727 ~(affine_dependent {a,b,c,d}) /\
\r
3728 CARD {a,b,c,d} = 4 /\
\r
3729 p IN convex hull {a,b,c,d} /\
\r
3730 k1 + k2 + k3 + k4 = &1 /\
\r
3731 p = k1 % a + k2 % b + k3 % c + k4 % d /\
\r
3732 k1 <= &0 ==> k1 = &0`,
\r
3733 [(REPEAT GEN_TAC);
\r
3734 (REWRITE_TAC[CONVEX_HULL_4; IN;IN_ELIM_THM]);
\r
3735 (REPEAT STRIP_TAC);
\r
3736 (ASM_CASES_TAC `k1 = &0`);
\r
3737 (ASM_REWRITE_TAC[]);
\r
3739 (NEW_GOAL `affine_dependent {a,b,c,d:real^3}`);
\r
3740 (REWRITE_TAC[AFFINE_DEPENDENT_EXPLICIT]);
\r
3741 (EXISTS_TAC `{a,b,c,d:real^3}`);
\r
3742 (ABBREV_TAC `f = (\x:real^3. if x = a then u - k1 else
\r
3743 if x = b then v - k2 else
\r
3744 if x = c then w - k3 else
\r
3745 if x = d then z - k4 else &0)`);
\r
3746 (EXISTS_TAC `f:real^3->real`);
\r
3748 (NEW_GOAL `f (a:real^3) = u - k1`);
\r
3753 (ASM_MESON_TAC[]);
\r
3754 (ASM_MESON_TAC[]);
\r
3756 (NEW_GOAL `f (b:real^3) = v - k2`);
\r
3759 (NEW_GOAL `F` THEN UP_ASM_TAC THEN REWRITE_TAC[]);
\r
3760 (MATCH_MP_TAC CARD4_IMP_DISTINCT);
\r
3761 (EXISTS_TAC `c:real^3` THEN EXISTS_TAC `d:real^3`);
\r
3762 (ASM_REWRITE_TAC[SET_RULE `{a,b,c,d} = {b,a,c,d}`]);
\r
3766 (ASM_MESON_TAC[]);
\r
3767 (ASM_MESON_TAC[]);
\r
3769 (NEW_GOAL `f (c:real^3) = w - k3`);
\r
3772 (NEW_GOAL `F` THEN UP_ASM_TAC THEN REWRITE_TAC[]);
\r
3773 (MATCH_MP_TAC CARD4_IMP_DISTINCT);
\r
3774 (EXISTS_TAC `b:real^3` THEN EXISTS_TAC `d:real^3`);
\r
3775 (ASM_REWRITE_TAC[SET_RULE `{c,a,b,d} = {a,b,c,d}`]);
\r
3777 (NEW_GOAL `F` THEN UP_ASM_TAC THEN REWRITE_TAC[]);
\r
3778 (MATCH_MP_TAC CARD4_IMP_DISTINCT);
\r
3779 (EXISTS_TAC `a:real^3` THEN EXISTS_TAC `d:real^3`);
\r
3780 (ASM_REWRITE_TAC[SET_RULE `{c,b,a,d} = {a,b,c,d}`]);
\r
3784 (ASM_MESON_TAC[]);
\r
3785 (ASM_MESON_TAC[]);
\r
3787 (NEW_GOAL `f (d:real^3) = z - k4`);
\r
3790 (NEW_GOAL `F` THEN UP_ASM_TAC THEN REWRITE_TAC[]);
\r
3791 (MATCH_MP_TAC CARD4_IMP_DISTINCT);
\r
3792 (EXISTS_TAC `c:real^3` THEN EXISTS_TAC `b:real^3`);
\r
3793 (ASM_REWRITE_TAC[SET_RULE `{d,a,c, b} = {a,b,c,d}`]);
\r
3795 (NEW_GOAL `F` THEN UP_ASM_TAC THEN REWRITE_TAC[]);
\r
3796 (MATCH_MP_TAC CARD4_IMP_DISTINCT);
\r
3797 (EXISTS_TAC `a:real^3` THEN EXISTS_TAC `c:real^3`);
\r
3798 (ASM_REWRITE_TAC[SET_RULE `{d,b,a,c} = {a,b,c,d}`]);
\r
3800 (NEW_GOAL `F` THEN UP_ASM_TAC THEN REWRITE_TAC[]);
\r
3801 (MATCH_MP_TAC CARD4_IMP_DISTINCT);
\r
3802 (EXISTS_TAC `a:real^3` THEN EXISTS_TAC `b:real^3`);
\r
3803 (ASM_REWRITE_TAC[SET_RULE `{d,c,a,b} = {a,b,c,d}`]);
\r
3807 (ASM_MESON_TAC[]);
\r
3808 (ASM_MESON_TAC[]);
\r
3810 (REPEAT STRIP_TAC);
\r
3811 (REWRITE_TAC[Geomdetail.FINITE6]);
\r
3814 (REWRITE_WITH `sum {a, b, c, d:real^3} f = f a + f b + f c + f d`);
\r
3815 (MATCH_MP_TAC SUM_DIS4);
\r
3816 (ASM_REWRITE_TAC[]);
\r
3817 (ASM_REWRITE_TAC[]);
\r
3818 (REWRITE_TAC[REAL_ARITH
\r
3819 `a - x + b - y + c - z + d - t = (a + b + c + d) - (x + y + z + t)`]);
\r
3820 (ASM_REWRITE_TAC[REAL_SUB_REFL]);
\r
3821 (EXISTS_TAC `a:real^3`);
\r
3824 (ASM_REWRITE_TAC[]);
\r
3825 (ASM_REAL_ARITH_TAC);
\r
3827 (REWRITE_WITH `vsum {a, b, c, d:real^3} (\v. f v % v) =
\r
3828 (\v. f v % v) a + (\v. f v % v) b + (\v. f v % v) c + (\v. f v % v) d`);
\r
3829 (MATCH_MP_TAC VSUM_DIS4);
\r
3830 (ASM_REWRITE_TAC[]);
\r
3831 (ASM_REWRITE_TAC[]);
\r
3832 (REWRITE_TAC[VECTOR_ARITH `
\r
3833 (u - k1) % a + (v - k2) % b + (w - k3) % c + (z - k4) % d =
\r
3834 (u % a + v % b + w % c + z % d) - (k1 % a + k2 % b + k3 % c + k4 % d)`]);
\r
3835 (ASM_MESON_TAC[VECTOR_ARITH `a:real^N - a = vec 0`]);
\r
3836 (ASM_MESON_TAC[]);
\r
3837 (ASM_MESON_TAC[])]);;
\r
3839 (* ======================================================================= *)
\r
3841 let IN_2_2_IMP_CONVEX_HULL_4 = prove (
\r
3842 `!a:real^N b x y m n p.
\r
3843 between p (m,n) /\ between m (a,b) /\ between n (x,y)
\r
3844 ==> p IN convex hull {a, b, x, y}`,
\r
3845 (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;CONVEX_HULL_2;CONVEX_HULL_4;
\r
3846 IN;IN_ELIM_THM] THEN REPEAT STRIP_TAC) THEN
\r
3847 (ASM_REWRITE_TAC[]) THEN
\r
3848 (EXISTS_TAC `u * u'` THEN EXISTS_TAC `u * v'`) THEN
\r
3849 (EXISTS_TAC `v * u''` THEN EXISTS_TAC `v * v''`) THEN
\r
3850 (ASM_SIMP_TAC[REAL_LE_MUL; REAL_ARITH `a * x + a * y + b * z + b * t =
\r
3851 a * (x + y) + b * (z + t)`; REAL_MUL_RID]) THEN
\r
3852 (VECTOR_ARITH_TAC));;
\r
3854 (* ======================================================================= *)
\r
3856 let BETWEEN_TRANS_3_CASES = prove_by_refinement (
\r
3857 `!a b x y:real^3. between x (a,b) /\ between y (a,b) ==>
\r
3858 between x (a, y) \/ between x (y, b) `,
\r
3859 [(REPEAT STRIP_TAC);
\r
3860 (ASM_CASES_TAC `(a = b:real^3)`);
\r
3861 (UNDISCH_TAC `between x (a,b:real^3)`);
\r
3862 (UNDISCH_TAC `between y (a,b:real^3)`);
\r
3863 (ASM_REWRITE_TAC[BETWEEN_REFL_EQ]);
\r
3864 (REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[BETWEEN_REFL_EQ]);
\r
3866 (ASM_CASES_TAC `between x (a,y:real^3)`);
\r
3867 (ASM_MESON_TAC[]);
\r
3869 (ONCE_REWRITE_TAC[BETWEEN_SYM]);
\r
3870 (MATCH_MP_TAC BETWEEN_TRANS_2);
\r
3871 (EXISTS_TAC `a:real^3` THEN ASM_REWRITE_TAC[]);
\r
3872 (NEW_GOAL `collinear {a,y,x:real^3}`);
\r
3873 (ONCE_REWRITE_TAC[SET_RULE `{a,y,x} = {x, a ,y}`]);
\r
3874 (MATCH_MP_TAC COLLINEAR_3_TRANS);
\r
3875 (EXISTS_TAC `b:real^3`);
\r
3876 (REPEAT STRIP_TAC);
\r
3877 (ONCE_REWRITE_TAC[SET_RULE `{x,a, b} = {a, x, b}`]);
\r
3878 (MATCH_MP_TAC BETWEEN_IMP_COLLINEAR);
\r
3879 (ASM_REWRITE_TAC[]);
\r
3880 (ONCE_REWRITE_TAC[SET_RULE `{a, b,y} = {a, y, b}`]);
\r
3881 (MATCH_MP_TAC BETWEEN_IMP_COLLINEAR);
\r
3882 (ASM_REWRITE_TAC[]);
\r
3883 (ASM_MESON_TAC[]);
\r
3884 (UP_ASM_TAC THEN REWRITE_TAC[COLLINEAR_BETWEEN_CASES]);
\r
3886 (ASM_CASES_TAC `between y (x,a:real^3)`);
\r
3887 (STRIP_TAC THEN ASM_REWRITE_TAC[]);
\r
3888 (ONCE_REWRITE_TAC[MESON[] `(A\/B\/C ==> B) <=> (C\/A ==> B)`]);
\r
3889 (REPEAT STRIP_TAC);
\r
3891 (ASM_MESON_TAC[]);
\r
3892 (ASM_MESON_TAC[]);
\r
3893 (ASM_CASES_TAC `x = y:real^3`);
\r
3894 (REWRITE_TAC[ASSUME `x = y:real^3`; BETWEEN_REFL]);
\r
3897 (UNDISCH_TAC `between x (a,b:real^3)` THEN
\r
3898 UNDISCH_TAC `between y (a,b:real^3)` THEN
\r
3899 UNDISCH_TAC `between a (y,x:real^3)`);
\r
3900 (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;CONVEX_HULL_2;IN;IN_ELIM_THM]);
\r
3901 (REPEAT STRIP_TAC);
\r
3903 (MP_TAC (ASSUME `a = u % y + v % x:real^3`));
\r
3904 (REWRITE_TAC[ASSUME `y = u' % a + v' % b:real^3`;
\r
3905 ASSUME `x = u'' % a + v'' % b:real^3`]);
\r
3907 (REWRITE_WITH `v' = &1 - u' /\ v = &1 - u /\ v'' = &1 - u''`);
\r
3908 (ASM_REAL_ARITH_TAC);
\r
3909 (REWRITE_TAC [VECTOR_ARITH `
\r
3910 a = u % (u' % a + (&1 - u') % b) + (&1 - u) % (u'' % a + (&1 - u'') % b)
\r
3911 <=> (&1 - u * u' - (&1 - u) * u'') % (a - b) = vec 0`]);
\r
3912 (REWRITE_TAC[VECTOR_MUL_EQ_0]);
\r
3913 (ASM_REWRITE_TAC[VECTOR_ARITH `a - b = vec 0 <=> a = b`]);
\r
3914 (REWRITE_TAC[REAL_ARITH
\r
3915 `&1 - u * u' - (&1 - u) * u'' = u * (&1 - u') + (&1 - u) * (&1 - u'')`]);
\r
3916 (NEW_GOAL `&0 <= u * (&1 - u')`);
\r
3917 (MATCH_MP_TAC REAL_LE_MUL);
\r
3918 (ASM_REAL_ARITH_TAC);
\r
3919 (NEW_GOAL `&0 <= (&1 - u) * (&1 - u'')`);
\r
3920 (MATCH_MP_TAC REAL_LE_MUL);
\r
3921 (ASM_REAL_ARITH_TAC);
\r
3923 (NEW_GOAL `u * (&1 - u') = &0 /\ (&1 - u) * (&1 - u'') = &0`);
\r
3924 (ASM_REAL_ARITH_TAC);
\r
3925 (UP_ASM_TAC THEN REWRITE_TAC[REAL_ENTIRE]);
\r
3926 (REPEAT STRIP_TAC);
\r
3927 (ASM_REAL_ARITH_TAC);
\r
3929 (UNDISCH_TAC `~between x (a,y:real^3)`);
\r
3930 (REWRITE_TAC[ASSUME `x = u'' % a + v'' % b:real^3`]);
\r
3931 (REWRITE_WITH `u'' = &1 /\ v'' = &0`);
\r
3932 (ASM_REAL_ARITH_TAC);
\r
3933 (REWRITE_TAC[VECTOR_MUL_LID; VECTOR_MUL_LZERO;VECTOR_ADD_RID; BETWEEN_REFL]);
\r
3935 (UNDISCH_TAC `~between y (x,a:real^3)`);
\r
3936 (REWRITE_TAC[ASSUME `y = u' % a + v' % b:real^3`]);
\r
3937 (REWRITE_WITH `u' = &1 /\ v' = &0`);
\r
3938 (ASM_REAL_ARITH_TAC);
\r
3939 (REWRITE_TAC[VECTOR_MUL_LID; VECTOR_MUL_LZERO;VECTOR_ADD_RID; BETWEEN_REFL]);
\r
3941 (UNDISCH_TAC `~between y (x,a:real^3)`);
\r
3942 (REWRITE_TAC[ASSUME `y = u' % a + v' % b:real^3`]);
\r
3943 (REWRITE_WITH `u' = &1 /\ v' = &0`);
\r
3944 (ASM_REAL_ARITH_TAC);
\r
3945 (REWRITE_TAC[VECTOR_MUL_LID; VECTOR_MUL_LZERO;VECTOR_ADD_RID; BETWEEN_REFL]);
\r
3946 (ASM_MESON_TAC[])]);;
\r
3948 (* ======================================================================= *)
\r
3951 let OMEGA_LIST_UP_TO_2 = prove_by_refinement (
\r
3952 `! V ul. {omega_list_n V ul i | i <= 2} =
\r
3953 {omega_list_n V ul 0, omega_list_n V ul 1, omega_list_n V ul 2}`,
\r
3954 [(REPEAT GEN_TAC);
\r
3955 (REWRITE_WITH `{omega_list_n V ul i | i <= 2} =
\r
3956 IMAGE (omega_list_n V ul) {i| i <= 2}`);
\r
3957 (REWRITE_TAC[IMAGE] THEN SET_TAC[]);
\r
3959 {omega_list_n V ul 0, omega_list_n V ul 1, omega_list_n V ul 2}
\r
3960 = IMAGE (omega_list_n V ul) {0,1,2}`);
\r
3961 (REWRITE_TAC[IMAGE] THEN SET_TAC[]);
\r
3963 (REWRITE_TAC[SET_OF_0_TO_2])]);;
\r
3965 (* ======================================================================= *)
\r
3967 let CONVEX_HULL_KY_LEMMA_5 = prove_by_refinement (
\r
3968 `!a:real^3 b c d x y d p.
\r
3969 ~(affine_dependent {a,b,c,d}) /\ CARD {a,b,c,d} = 4 /\ ~(d = x) /\
\r
3970 x IN convex hull {a,b,c} /\ between d (x,y) /\
\r
3971 ~( p IN affine hull {a,b,d}) /\
\r
3972 p IN convex hull {a,b,c,d} INTER convex hull {a,b,x,y} ==>
\r
3973 p IN convex hull {a,b,x,d}`,
\r
3974 [(REPEAT STRIP_TAC);
\r
3975 (NEW_GOAL `p IN convex hull {a, b, x, y:real^3}`);
\r
3976 (ASM_SET_TAC[IN_INTER]);
\r
3977 (SUBGOAL_THEN `?m n:real^3.
\r
3978 between p (m,n) /\ between m (a,b) /\ between n (x,y)` CHOOSE_TAC);
\r
3979 (ASM_SIMP_TAC[CONVEX_HULL_4_IMP_2_2]);
\r
3980 (UP_ASM_TAC THEN REPEAT STRIP_TAC);
\r
3982 (ASM_CASES_TAC `between n (x, d:real^3)`);
\r
3983 (MATCH_MP_TAC IN_2_2_IMP_CONVEX_HULL_4);
\r
3984 (EXISTS_TAC `m:real^3` THEN EXISTS_TAC `n:real^3`);
\r
3985 (ASM_REWRITE_TAC[]);
\r
3987 (NEW_GOAL `between n (x,d) \/ between n (d, y:real^3)`);
\r
3988 (MATCH_MP_TAC BETWEEN_TRANS_3_CASES);
\r
3989 (ASM_REWRITE_TAC[]);
\r
3990 (NEW_GOAL `between n (d,y:real^3)`);
\r
3991 (ASM_MESON_TAC[]);
\r
3993 (NEW_GOAL `?k1 k2. n = k1 % d + k2 % x:real^3 /\ k1 + k2 = &1 /\ k2 <= &0`);
\r
3994 (UP_ASM_TAC THEN UNDISCH_TAC `between d (x,y:real^3)`);
\r
3995 (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;IN;IN_ELIM_THM;CONVEX_HULL_2]);
\r
3996 (REPEAT STRIP_TAC);
\r
3997 (ASM_REWRITE_TAC[]);
\r
3998 (EXISTS_TAC `u' + (v'/ v)`);
\r
3999 (EXISTS_TAC `-- ((u * v')/ v)`);
\r
4000 (REPEAT STRIP_TAC);
\r
4002 (REWRITE_TAC[VECTOR_ARITH
\r
4003 `u' % (u % x + v % y) + v' % y =
\r
4004 (u' + v' / v) % (u % x + v % y) + --((u * v') / v) % x
\r
4005 <=> ((v /v - &1) * v') % y = vec 0`]);
\r
4006 (REWRITE_WITH `v / v = &1`);
\r
4007 (MATCH_MP_TAC REAL_DIV_REFL);
\r
4009 (NEW_GOAL `d = x:real^3`);
\r
4010 (REWRITE_TAC[ASSUME `d = u % x + v % y:real^3`]);
\r
4011 (REWRITE_WITH `v = &0 /\ u = &1`);
\r
4012 (ASM_REAL_ARITH_TAC);
\r
4013 (VECTOR_ARITH_TAC);
\r
4014 (ASM_MESON_TAC[]);
\r
4015 (VECTOR_ARITH_TAC);
\r
4017 (REWRITE_TAC[REAL_ARITH `(u' + v' / v) + --((u * v') / v) =
\r
4018 u' + v' * ((&1 - u) / v)`]);
\r
4019 (REWRITE_WITH `(&1 - u) / v = &1`);
\r
4020 (REWRITE_WITH `&1 - u = v`);
\r
4021 (ASM_REAL_ARITH_TAC);
\r
4022 (MATCH_MP_TAC REAL_DIV_REFL);
\r
4024 (NEW_GOAL `d = x:real^3`);
\r
4025 (REWRITE_TAC[ASSUME `d = u % x + v % y:real^3`]);
\r
4026 (REWRITE_WITH `v = &0 /\ u = &1`);
\r
4027 (ASM_REAL_ARITH_TAC);
\r
4028 (VECTOR_ARITH_TAC);
\r
4029 (ASM_MESON_TAC[]);
\r
4030 (ASM_REAL_ARITH_TAC);
\r
4031 (REWRITE_TAC[REAL_ARITH `-- a <= &0 <=> &0 <= a`]);
\r
4032 (MATCH_MP_TAC REAL_LE_DIV);
\r
4033 (ASM_SIMP_TAC[REAL_LE_MUL]);
\r
4034 (FIRST_X_ASSUM CHOOSE_TAC THEN FIRST_X_ASSUM CHOOSE_TAC);
\r
4036 (UNDISCH_TAC `between p (m,n:real^3)`);
\r
4037 (UNDISCH_TAC `between m (a,b:real^3)`);
\r
4038 (UNDISCH_TAC `x IN convex hull {a,b,c:real^3}`);
\r
4039 (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;CONVEX_HULL_2;
\r
4040 CONVEX_HULL_3;IN;IN_ELIM_THM]);
\r
4041 (REPEAT STRIP_TAC);
\r
4043 (UP_ASM_TAC THEN ASM_REWRITE_TAC[VECTOR_ADD_LDISTRIB;VECTOR_MUL_ASSOC]);
\r
4044 (REWRITE_TAC[VECTOR_ARITH
\r
4045 `(x % a + y % b) + z % d + x' % a + y' % b + z' % c =
\r
4046 z' % c + (x + x') % a + (y + y') % b + z % d`]);
\r
4048 (REPEAT STRIP_TAC);
\r
4050 (NEW_GOAL `v'' * k2 * w = &0`);
\r
4051 (MATCH_MP_TAC AFFINE_DEPENDENT_KY_LEMMA1);
\r
4052 (EXISTS_TAC `c:real^3` THEN EXISTS_TAC `a:real^3`);
\r
4053 (EXISTS_TAC `b:real^3` THEN EXISTS_TAC `d:real^3`);
\r
4054 (EXISTS_TAC `p:real^3`);
\r
4055 (EXISTS_TAC `u'' * u' + v'' * k2 * u` THEN
\r
4056 EXISTS_TAC `u'' * v' + v'' * k2 * v` THEN
\r
4057 EXISTS_TAC `v'' * k1`);
\r
4059 (ONCE_REWRITE_TAC[SET_RULE `{c,a,b,d} = {a,b,c,d}`]);
\r
4060 (ASM_REWRITE_TAC[]);
\r
4061 (REPEAT STRIP_TAC);
\r
4062 (ONCE_REWRITE_TAC[SET_RULE `{c,a,b,d} = {a,b,c,d}`]);
\r
4063 (ASM_REWRITE_TAC[]);
\r
4064 (ONCE_REWRITE_TAC[SET_RULE `{c,a,b,d} = {a,b,c,d}`]);
\r
4065 (ASM_SET_TAC[IN_INTER]);
\r
4066 (REWRITE_TAC[REAL_ARITH
\r
4067 `v'' * k2 * w + (u'' * u' + v'' * k2 * u) +
\r
4068 (u'' * v' + v'' * k2 * v) + v'' * k1
\r
4069 = u'' * (u' + v') + v'' * (k1 + k2 * (u + v + w))`]);
\r
4070 (ASM_REWRITE_TAC[REAL_MUL_RID]);
\r
4071 (ASM_REWRITE_TAC[]);
\r
4072 (REWRITE_TAC[REAL_ARITH `a * b * c <= &0 <=> &0 <= a * (-- b) * c`]);
\r
4073 (MATCH_MP_TAC REAL_LE_MUL);
\r
4074 (ASM_REWRITE_TAC[]);
\r
4075 (MATCH_MP_TAC REAL_LE_MUL);
\r
4076 (ASM_REWRITE_TAC[]);
\r
4077 (ASM_REAL_ARITH_TAC);
\r
4078 (NEW_GOAL `p IN affine hull {a,b,d:real^3}`);
\r
4079 (REWRITE_TAC[AFFINE_HULL_3;IN;IN_ELIM_THM]);
\r
4080 (EXISTS_TAC `u'' * u' + v'' * k2 * u` THEN
\r
4081 EXISTS_TAC `u'' * v' + v'' * k2 * v` THEN
\r
4082 EXISTS_TAC `v'' * k1`);
\r
4084 (REWRITE_WITH `(u'' * u' + v'' * k2 * u) + (u'' * v' + v'' * k2 * v) +
\r
4085 v'' * k1 = u'' * (u' + v') + v'' * (k1 + k2 * (u + v + w)) - (v'' * k2 * w)`);
\r
4086 (ASM_REAL_ARITH_TAC);
\r
4087 (ASM_REWRITE_TAC[REAL_MUL_RID]);
\r
4088 (ASM_REAL_ARITH_TAC);
\r
4089 (ASM_REWRITE_TAC[]);
\r
4090 (VECTOR_ARITH_TAC);
\r
4091 (ASM_MESON_TAC[]);
\r
4092 (ASM_MESON_TAC[])]);;
\r
4094 (* ======================================================================= *)
\r
4096 (* ======================================================================= *)
\r