1 (* ================================ *)
\r
2 (* ===== NGUYEN QUANG TRUONG ====== *)
\r
6 Note: I have split the file into 2 pieces: geomdetail.ml and geomdetail_08.ml. Not everything in geomdetail_08.ml loads with the Multivariate directory, but these are the parts that are least likely to be used in the revision of the proof in 2009. Everything in this file now loads with Multivariate. --tch July 14, 2009
\r
9 let voronoi_trg = new_definition ` voronoi_trg v S = { x | !w. ((S w) /\ ~(w=v))
\r
10 ==> (dist ( x , v ) < dist ( x , w )) }`;;
\r
13 let conv0_2 = new_definition ` conv0_2 s = conv0 s `;;
\r
16 let convex = new_definition `convex s <=> !x y u v. x IN s /\ y IN s /\ &0 <= u /\
\r
17 &0 <= v /\ (u + v = &1) ==> (u % x + v % y) IN s`;;
\r
19 let aff = new_definition `aff = ( hull ) affine`;;
\r
23 let conv_trg = new_definition ` conv_trg s = convex hull s`;;
\r
25 let border = new_definition ` border s = { x | ! ep. ep > &0 /\ ( ? a b. ~ (b IN s ) /\
\r
26 dist (b, x) < ep /\ a IN s /\ dist (a, x) < ep ) }`;;
\r
28 let packing_trg = new_definition `packing_trg (s:real^3 -> bool) = (! x y. s x /\ s y /\ ( ~(x=y))
\r
29 ==> dist ( x, y) >= &2 ) `;;
\r
31 let center_pac = new_definition ` center_pac s v = ( packing_trg s /\ s v )`;;
\r
33 let centered_pac = new_definition ` centered_pac s v = ( packing s /\ v IN s )`;;
\r
35 let d3 = new_definition ` d3 x y = dist (x,y)`;;
\r
37 let voronoi2 = new_definition ` voronoi2 v S = {x| x IN voronoi_trg v S /\ d3 x v < &2 }`;;
\r
39 let voro2 = new_definition ` voro2 v s = {x| x IN voronoi v s /\ d3 x v < &2 }`;;
\r
41 let t0 = new_definition ` t0 = #1.255`;;
\r
44 let quasi_tri = new_definition ` quasi_tri tri s = ( packing s /\
\r
46 (? a b c. ~( a=b \/ b=c\/ c=a) /\ { a, b, c } = tri ) /\
\r
47 (! x y. ( x IN tri /\ y IN tri /\ (~(x=y)) ) ==> ( d3 x y <= &2 * t0 )))`;;
\r
50 let simplex = new_definition ` simplex (d:real^3 -> bool) s = ( packing s /\
\r
52 ( ? v1 v2 v3 v4. ~( v1 = v2 \/ v3 = v4 ) /\ {v1, v2 } INTER {v3, v4 } = {}/\ {v1,v2,v3,v4} = d )
\r
55 let quasi_reg_tet = new_definition ` quasi_reg_tet x s = ( simplex x s /\
\r
56 (! v w. ( v IN x /\ w IN x /\
\r
58 ==> ( d3 v w <= &2 * t0 )) )`;;
\r
60 let quarter = new_definition ` quarter (q:real^3 -> bool) s =
\r
66 &2 * t0 <= d3 v w /\
\r
67 d3 v w <= sqrt (&8) /\
\r
69 x IN q /\ y IN q /\ ~({x, y} = {v, w})
\r
70 ==> d3 x y <= &2 * t0)))`;;
\r
72 let diagonal = new_definition ` diagonal d1 d2 q s = ( quarter q s /\
\r
73 {d1, d2} SUBSET q /\
\r
74 (!x y. x IN q /\ y IN q ==> d3 x y <= d3 d1 d2))`;;
\r
76 let strict_qua = new_definition ` strict_qua d s = ( quarter d s /\
\r
77 ( ? x y. x IN d /\ y IN d /\ &2 * t0 < d3 x y /\ d3 x y < sqrt( &8 ) ))`;;
\r
79 let strict_qua2 = new_definition ` strict_qua2 d (ch:real^3 -> bool ) s = ( quarter d s /\ ch SUBSET d
\r
80 /\ ( ? x y. ~( x = y ) /\ ch = {x,y} /\ &2 * t0 < d3 x y /\ d3 x y < sqrt ( &8 ) ) )`;;
\r
84 let quartered_oct = new_definition `quartered_oct (v:real^3) (w:real^3) (v1:real^3) (v2:real^3) (v3:real^3) (v4:real^3) s =
\r
86 ( &2 * t0 < dist (v,w) /\ dist (v,w) < sqrt (&8) ) /\
\r
87 (!x. x IN {v1, v2, v3, v4}
\r
88 ==> dist (x,v) <= &2 * t0 /\ dist (x,w) <= &2 * t0) /\
\r
89 {v, w, v1, v2, v3, v4} SUBSET s /\
\r
90 (&2 <= dist (v1,v2) /\ dist (v1,v2) <= &2 * t0) /\
\r
91 (&2 <= dist (v2,v3) /\ dist (v2,v3) <= &2 * t0) /\
\r
92 (&2 <= dist (v3,v4) /\ dist (v3,v4) <= &2 * t0) /\
\r
93 &2 <= dist (v4,v1) /\
\r
94 dist (v4,v1) <= &2 * t0 ) `;;
\r
97 let adjacent_pai = new_definition ` adjacent_pai v v1 v3 v2 v4 s = ( strict_qua2 { v , v1 , v3 , v2 } { v1 , v3 } s
\r
98 /\ strict_qua2 { v , v1 , v3 , v4 } { v1 , v3 } s /\
\r
99 ( conv0 { v , v1 , v3 , v2 } INTER conv0 { v , v1 , v3 , v4 } = {} ) )`;;
\r
101 let conflicting_dia = new_definition ` conflicting_dia v v1 v3 v2 v4 s = ( adjacent_pai v v1 v3 v2 v4 s
\r
102 /\ adjacent_pai v v2 v4 v1 v3 s )`;;
\r
104 let interior_pos = new_definition `interior_pos v v1 v3 v2 v4 s = ( conflicting_dia v v1 v3 v2 v4 s
\r
105 /\ ~( conv0 { v1, v3 } INTER conv0 { v , v2 , v4 } = {} ))`;;
\r
107 let isolated_qua = new_definition ` isolated_qua q s = ( quarter q s /\ ~( ? v v1 v2 v3 v4. q =
\r
108 {v, v1, v2, v3} /\ adjacent_pai v v1 v2 v3 v4 s))`;;
\r
110 let isolated_pai = new_definition ` isolated_pai q1 q2 s = ( isolated_qua q1 s /\ isolated_qua q2 s /\
\r
111 ~ (conv0 q1 INTER conv0 q2 = {}))`;;
\r
113 let anchor = new_definition ` anchor (v:real^3) v1 v2 s = ( {v, v1, v2} SUBSET s /\ d3 v1 v2 <= sqrt ( &8 ) /\
\r
114 d3 v1 v2 >= &2 * t0 /\ d3 v v1 <= &2 * t0 /\ d3 v v2 <= &2 * t0 )`;;
\r
116 let anchor_points = new_definition ` anchor_points v w s = { t | &2 * t0 <= d3 v w /\
\r
117 anchor t v w s }`;;
\r
119 let Q_SYS = new_definition ` Q_SYS s = {q | quasi_reg_tet q s \/
\r
124 d3 c d > &2 * t0 /\
\r
125 (quasi_reg_tet qq s \/ strict_qua qq s) /\
\r
126 conv0 {c, d} INTER conv0 qq = {}) \/
\r
130 v IN q /\ w IN q /\ &2 * t0 < d3 v w /\ anchor t v w s} >
\r
134 v IN q /\ w IN q /\ &2 * t0 < d3 v w /\ anchor t v w s} =
\r
136 ~(?v1 v2 v3 v4 v w. v IN q /\
\r
138 {v1, v2, v3, v4} SUBSET anchor_points v w s
\r
141 &2 * t0 < d3 v w /\
\r
142 quartered_oct v w v1 v2 v3 v4 s))
\r
143 \/ (? v w v1 v2 v3 v4. q = { v, w, v1, v2} /\ quartered_oct v w v1 v2 v3 v4 s )
\r
144 \/ (? v v1 v3 v2 v4. ( q = {v, v1, v2, v3} \/ q = {v, v1, v3, v4} ) /\
\r
145 interior_pos v v1 v3 v2 v4 s /\ anchor_points v1 v3 s = { v, v2, v4} /\
\r
146 anchor_points v2 v4 s = { v, v1, v3 } )}`;;
\r
148 let barrier = new_definition ` barrier s = { { (v1 : real^3 ) , ( v2 :real^3 ) , (v3 :real^3) } |
\r
149 quasi_tri { v1 , v2 , v3 } s \/
\r
150 (? v4. ( { v1 , v2 , v3 } UNION { v4 }) IN Q_SYS s ) } `;;
\r
152 let obstructed = new_definition ` obstructed x y s = ( ? bar. bar IN barrier s /\
\r
153 ( ~ (conv0_2 { x , y } INTER conv_trg bar = {})))`;;
\r
155 let obstruct = new_definition ` obstruct x y s = ( ? bar. bar IN barrier s /\
\r
156 ( ~ (conv0 { x , y } INTER conv bar = {})))`;;
\r
158 let unobstructed = new_definition ` unobstructed x y s = ( ~( obstructed x y s ))`;;
\r
160 let VC_trg = new_definition ` VC_trg x s = { z | d3 x z < &2 /\ ~obstructed x z s /\
\r
161 (! y. y IN s /\ ~ ( x = y ) /\ ~(obstructed z y s) ==> d3 x z < d3 y z )} `;;
\r
163 let VC_INFI_trg = new_definition ` VC_INFI_trg s = { z | ( ! x. x IN s /\
\r
164 ~( z IN VC_trg x s ))}`;;
\r
167 let lambda_x = new_definition `lambda_x x s = {w | w IN s /\ d3 w x < &2 /\
\r
168 ~obstructed w x s }`;;
\r
170 let lambda_y = new_definition ` lambda_y y s = { w| w IN s /\ d3 w y < &2 /\
\r
171 ~obstruct w y s} `;;
\r
173 let VC = new_definition `VC v s = { x | v IN lambda_x x s /\
\r
174 (!w. w IN lambda_x x s /\ ~(w = v) ==> d3 x v < d3 x w) }`;;
\r
176 let VC_INFI = new_definition ` VC_INFI s = { z | ( ! x. ~( z IN VC x s ))}`;;
\r
181 [NOT_IN_EMPTY; IN_UNIV; IN_UNION; IN_INTER; IN_DIFF; IN_INSERT;
\r
182 IN_DELETE; IN_REST; IN_INTERS; IN_UNIONS; IN_IMAGE] in
\r
183 let allthms = basicthms @ map (REWRITE_RULE[IN]) basicthms @
\r
184 [IN_ELIM_THM; IN] in
\r
186 TRY(POP_ASSUM_LIST(MP_TAC o end_itlist CONJ)) THEN
\r
187 REPEAT COND_CASES_TAC THEN
\r
188 REWRITE_TAC[EXTENSION; SUBSET; PSUBSET; DISJOINT; SING] THEN
\r
189 REWRITE_TAC allthms in
\r
192 (if ths = [] then ALL_TAC else MP_TAC(end_itlist CONJ ths)) THEN
\r
195 let SET_RULE tm = prove(tm,SET_TAC[]);;
\r
197 (* some TRUONG TACTICS *)
\r
199 let PHA = REWRITE_TAC[ MESON[] ` (a/\b)/\c <=> a/\ b /\ c `];;
\r
201 let NGOAC = REWRITE_TAC[ MESON[] ` a/\b/\c <=> (a/\b)/\c `];;
\r
203 let DAO = NGOAC THEN REWRITE_TAC[ MESON[]` a /\ b <=> b /\ a`];;
\r
205 let PHAT = REWRITE_TAC[ MESON[] ` (a\/b)\/c <=> a\/b\/c `];;
\r
207 let NGOACT = REWRITE_TAC[ GSYM (MESON[] ` (a\/b)\/c <=> a\/b\/c `)];;
\r
209 let KHANANG = PHA THEN REWRITE_TAC[ MESON[]` ( a\/ b ) /\ c <=> a /\ c \/ b /\ c `] THEN
\r
210 REWRITE_TAC[ MESON[]` a /\ ( b \/ c ) <=> a /\ b \/ a /\ c `];;
\r
212 let ATTACH thm = MATCH_MP (MESON[]` ! a b. ( a ==> b ) ==> ( a <=> a /\ b )`) thm;;
\r
214 let CUTHE1 th = MATCH_MP (MESON[]` ( ! a. P a ) ==> P a `) th ;;
\r
216 let CUTHE2 th = MATCH_MP (MESON[]` ( ! a b. P a b ) ==> P a b`) th ;;
\r
218 let CUTHE3 th = MATCH_MP (MESON[]` ( ! a b c. P a b c ) ==> P a b c`) th ;;
\r
220 let CUTHE4 th = MATCH_MP (MESON[]` ( ! a b c d. P a b c d ) ==> P a b c d`) th ;;
\r
222 let CUTHE5 th = MATCH_MP (MESON[]` ( ! a b c d e. P a b c d e) ==> P a b c d e`) th ;;
\r
224 let CUTHE6 th = MATCH_MP (MESON[]` ( ! a b c d e f. P a b c d e f) ==> P a b c d e f`) th ;;
\r
226 let CUTHE7 th = MATCH_MP (MESON[]` ( ! a b c d e f h. P a b c d e f h) ==> P a b c d e f h`) th ;;
\r
228 let NHANH tm = ONCE_REWRITE_TAC[ ATTACH (tm)];;
\r
231 let trg_sub_bo = prove ( `A SUBSET B <=> (!x. A x ==> B x)`, SET_TAC[] );;
\r
233 let trg_sub_se = prove ( `A SUBSET B <=> (!x. x IN A ==> x IN B )`, SET_TAC[] );;
\r
235 let trg_setbool = prove (`x IN A <=> A x `, SET_TAC[] );;
\r
237 let trg_boolset = prove (` A x <=> x IN A `, SET_TAC[] );;
\r
239 let trg_in_union = prove (` x IN ( A UNION B ) <=> x IN A \/ x IN B `, SET_TAC[]);;
\r
241 let not_in_set3 = prove ( `~ ( x IN { z | A z /\ B z /\ C z } ) <=> ~ A x \/ ~ B x \/ ~ C x `,
\r
244 let trg_d3_sym = prove ( `! x y. d3 x y = d3 y x `, SIMP_TAC[d3; DIST_SYM]);;
\r
246 let affine_hull_e = prove (`affine hull {} = {}`,
\r
247 REWRITE_TAC[AFFINE_EMPTY; AFFINE_HULL_EQ]);;
\r
249 let wlog = MESON[]` (! a b. ( P a b = P b a ) /\ ( Q a b \/ Q b a ) ) ==> ((? a b . P a b ) <=> ( ? a b. P a b
\r
252 let wlog_real = MESON[REAL_ARITH `( ! a b:real. a <= b \/ b <= a )`] `
\r
253 (! a:real b:real . P a b = P b a ) ==> ((? a:real b . P a b ) <=> ( ? a b. P a b
\r
256 let dkdx = MESON[REAL_ARITH ` ! a b:real. a <= b \/ b <= a `]`! P. (!a b u v m n p . P a b u v m n p <=> P b a v u m n p)
\r
257 ==> ((?a b u v m n p. P a b u v m n p) <=> (?a b u v m n p. P a b u v m n p /\ a <= b))`;;
\r
260 let tarski_arith = new_axiom `! bar. bar IN barrier s /\
\r
261 ~(conv_trg bar INTER conv0_2 { v0 , x } ={}) /\
\r
263 x IN voronoi2 v0 s /\
\r
264 ~ ( x IN UNIONS {aff_ge {v0} {v1, v2} | {v0, v1, v2} IN barrier s} )
\r
265 ==> { v0 } UNION bar IN Q_SYS s `;;
\r
267 let simp_def = new_axiom ` (! a x y (z:real^A).
\r
268 aff_ge {a} {x, y, z} = { t | ? s i j k. &0 <= i
\r
269 /\ &0 <= j /\ &0 <= k /\ s + i + j + k = &1 /\
\r
270 t = s % a + i % x + j % y + k % z }) /\
\r
273 aff_ge {v0} {v1, v2} =
\r
278 t = u % v0 + v % v1 + w % v2}) /\
\r
280 aff_gt {v0} {v1, v2, v3} =
\r
285 x + y + z + w = &1 /\
\r
286 t = x % v0 + y % v1 + z % v2 + w % v3}) /\
\r
288 aff_le {v1, v2, v3} {v0} =
\r
291 a + b + c + d = &1 /\
\r
292 t = a % v1 + b % v2 + c % v3 + d % v0}) /\
\r
293 ( ! v0 v1. conv0_2 { v0, v1 } = { x | ? t. &0 < t /\ t < &1 /\ x = t % v0 + (&1 - t ) % v1 } ) /\
\r
294 (! s. conv_trg s = conv s )`;;
\r
297 let AFFINE_HULL_SINGLE = prove(`!x. affine hull {x} = {x}`,
\r
298 SIMP_TAC[AFFINE_SING; AFFINE_HULL_EQ]);;
\r
300 let usefull = MESON[] ` (!x. a x ==> b x ) ==>(?x. a x ) ==> c ==> d <=>
\r
301 (!x. a x ==> b x) ==> (?x. a x /\ b x ) ==> c ==> d `;;
\r
303 let v1_in_convex3 = prove (` ! v1 v2 v3. v1 IN {t | ?a b c.
\r
304 &0 <= a /\ &0 <= b /\ &0 <= c /\ a + b + c = &1 /\
\r
305 t = a % v1 + b % v2 + c % v3}`, REPEAT GEN_TAC THEN REWRITE_TAC[ IN_ELIM_THM] THEN
\r
306 EXISTS_TAC ` &1 ` THEN EXISTS_TAC ` &0 ` THEN EXISTS_TAC ` &0 ` THEN
\r
307 REWRITE_TAC[ VECTOR_ARITH ` &1 % v1 + &0 % v2 + &0 % v3 = v1 `] THEN REAL_ARITH_TAC);;
\r
310 let v3_in_convex3 = prove( `! v1 v2 v3. v3 IN
\r
316 t = a % v1 + b % v2 + c % v3}`, REWRITE_TAC[IN_ELIM_THM] THEN REPEAT GEN_TAC
\r
317 THEN REPLICATE_TAC 2 (EXISTS_TAC `&0`) THEN EXISTS_TAC ` &1` THEN REWRITE_TAC[VECTOR_MUL_LZERO;
\r
318 VECTOR_ADD_LID; VECTOR_MUL_LID] THEN REAL_ARITH_TAC);;
\r
321 let v1v2v3_in_convex3 = prove (` ! v1 v2 v3 . v1 IN {t | ?a b c. &0 <= a /\ &0 <= b /\ &0 <= c /\
\r
322 a + b + c = &1 /\ t = a % v1 + b % v2 + c % v3}
\r
323 /\ v2 IN {t | ?a b c. &0 <= a /\ &0 <= b /\ &0 <= c /\ a + b + c = &1 /\ t = a % v1 + b % v2 + c % v3}
\r
324 /\ v3 IN {t | ?a b c. &0 <= a /\ &0 <= b /\ &0 <= c /\ a + b + c = &1 /\ t = a % v1 + b % v2 + c % v3}`,
\r
325 REWRITE_TAC[v1_in_convex3; v3_in_convex3] THEN REPEAT GEN_TAC THEN REWRITE_TAC[IN_ELIM_THM] THEN
\r
326 EXISTS_TAC ` &0` THEN EXISTS_TAC ` &1` THEN EXISTS_TAC ` &0` THEN
\r
327 REWRITE_TAC[VECTOR_ARITH` v2 = &0 % v1 + &1 % v2 + &0 % v3`] THEN REAL_ARITH_TAC);;
\r
330 let convex3 = prove( `!v1 v2 v3.
\r
337 t = a % v1 + b % v2 + c % v3}`,
\r
338 REWRITE_TAC[convex; IN_ELIM_THM] THEN
\r
339 REPEAT GEN_TAC THEN STRIP_TAC THEN
\r
340 EXISTS_TAC ` u * a + v * a'` THEN
\r
341 EXISTS_TAC ` u * b + v * b'` THEN
\r
342 EXISTS_TAC ` u * c + v * c'` THEN
\r
343 REPEAT (FIRST_X_ASSUM MP_TAC) THEN
\r
344 REWRITE_TAC[MESON[] ` a==> b==> c <=> a /\ b==> c`] THEN PHA THEN
\r
345 REWRITE_TAC[ MESON[]` &0 <= a /\ l <=> l /\ &0 <= a `] THEN PHA THEN
\r
346 NHANH (MESON[REAL_LE_MUL; REAL_ARITH ` &0 <= a /\ &0 <= b ==> &0 <= a +b `]` &0 <= v /\
\r
353 &0 <= a ==> &0 <= u * c + v * c' /\
\r
354 &0 <= u * b + v * b' /\
\r
355 &0 <= u * a + v * a'`) THEN
\r
356 REWRITE_TAC[REAL_ARITH` ( a + y ) + ( b + x ) + c + z = ( a + b + c) + (
\r
357 y + x + z ) `] THEN
\r
358 REWRITE_TAC[REAL_ARITH ` a * b + a * c = a * ( b + c) `] THEN
\r
360 REWRITE_TAC[ REAL_ARITH ` a * &1 = a `] THEN SIMP_TAC[] THEN
\r
361 REWRITE_TAC[VECTOR_ARITH` u % (a % v1 + b % v2 + c % v3) + v % (a' % v1 + b' % v2 + c' % v3) =
\r
362 (u * a + v * a') % v1 + (u * b + v * b') % v2 + (u * c + v * c') % v3`]);;
\r
364 let INTERS_SUBSET = SET_RULE `! P t0. P t0 ==> INTERS { t| P t } SUBSET t0`;;
\r
366 let SET3_SUBSET = SET_RULE`! a b c. {a,b,c} SUBSET s <=> a IN s /\ b IN s /\ c IN s `;;
\r
368 let SUM_TWO_RATIO = REAL_FIELD ` ~(a + b = &0) <=> a / ( a + b) + b /(a+b) = &1`;;
\r
370 let minconvex3 = prove(`!t v1 v2 v3.
\r
371 convex t /\ {v1, v2, v3} SUBSET t
\r
373 &0 <= a /\ &0 <= b /\ &0 <= c /\ a + b + c = &1
\r
374 ==> a % v1 + b % v2 + c % v3 IN t)`,
\r
375 REPEAT GEN_TAC THEN
\r
376 REWRITE_TAC[convex; SET3_SUBSET] THEN
\r
378 REPEAT GEN_TAC THEN
\r
379 ONCE_REWRITE_TAC[ MESON[]` &0 <= a /\ &0 <= b /\ l<=> ( a + b = &0 \/
\r
380 ~( a + b = &0)) /\ &0 <= a /\ &0 <= b /\ l`] THEN
\r
381 REWRITE_TAC[RIGHT_OR_DISTRIB] THEN
\r
382 REWRITE_TAC[ MESON[]` a \/ b ==> c <=> ( a ==> c ) /\ ( b ==> c )`] THEN
\r
383 REWRITE_TAC[REAL_ARITH` a + b = &0 /\ &0 <= a /\ &0 <= b /\ &0 <= c /\ a + b + c = &1
\r
384 <=> &0 = a /\ &0 = b /\ &1 = c `] THEN
\r
385 ONCE_REWRITE_TAC[ EQ_SYM_EQ] THEN
\r
387 ASM_REWRITE_TAC[ VECTOR_MUL_LZERO; VECTOR_MUL_LID; VECTOR_ADD_LID] THEN
\r
388 REWRITE_TAC[MESON[]`&0 = a + b <=> a + b = &0`; SUM_TWO_RATIO] THEN
\r
389 NHANH (MESON[REAL_ARITH ` &0 <= a /\ &0 <= b ==> &0 <= a + b `]`
\r
390 dau /\ &0 <= a /\ &0 <= b /\ l ==> &0 <= a + b `) THEN
\r
391 NHANH (MESON[REAL_LE_DIV]` (aa /\ &0 <= a /\ &0 <= b /\ bb) /\ &0 <= a + b
\r
392 ==> &0 <= a / (a + b) /\ &0 <= b / (a + b)`) THEN
\r
393 REWRITE_TAC[GSYM SUM_TWO_RATIO] THEN
\r
395 NHANH (MESON[REAL_DIV_LMUL]` ~(a + b = &0) ==> a = (a+b) *(a/(a+b)) /\ b =
\r
396 (a+b) *(b/(a+b))`) THEN
\r
397 REWRITE_TAC[MESON[VECTOR_MUL_RCANCEL]` ( dau /\ a = (a + b) * a / (a + b) /\ b = (a + b) * b / (a + b))
\r
398 /\ l ==> a % v1 + b % v2 + c % v3 IN t <=>
\r
399 ( dau /\ a = (a + b) * a / (a + b) /\ b = (a + b) * b / (a + b))
\r
400 /\ l ==> ((a + b) * a / (a + b)) % v1 + ((a + b) * b / (a + b)) % v2 + c % v3 IN t`] THEN
\r
401 REWRITE_TAC[ VECTOR_ARITH ` ((a + b) * a / (a + b)) % v1 + ((a + b) * b / (a + b)) % v2 + c % v3
\r
402 = (a + b) % ( (a / (a + b)) % v1 + (b / (a + b)) % v2) + c % v3 `] THEN
\r
403 REWRITE_TAC[SUM_TWO_RATIO] THEN
\r
404 ASM_MESON_TAC[ REAL_ARITH` a + b + c = (a + b ) + c`]);;
\r
407 let EQ_EXPAND = MESON[] `(a <=> b) <=> ( a ==> b ) /\ ( b ==> a )` ;;
\r
411 let OTHER_CONVEX_CONDI = prove(` ! s. convex s <=> (! a b c v1 v2 v3. {v1, v2, v3} SUBSET s /\
\r
412 &0 <= a /\ &0 <= b /\ &0 <= c /\ a + b + c = &1
\r
413 ==> a % v1 + b % v2 + c % v3 IN s)`,
\r
414 REWRITE_TAC[EQ_EXPAND; MESON[minconvex3]`!s. (convex s
\r
415 ==> (!a b c v1 v2 v3.
\r
416 {v1, v2, v3} SUBSET s /\
\r
421 ==> a % v1 + b % v2 + c % v3 IN s))`; convex] THEN STRIP_TAC THEN
\r
422 REWRITE_TAC[SET3_SUBSET] THEN DISCH_TAC THEN
\r
423 REWRITE_TAC[REAL_ARITH`&0 <= u /\ &0 <= v /\ u + v = &1 <=>
\r
424 &0 <= u /\ &0 <= v / &2 /\ u + v/ &2 + v / &2 = &1`] THEN
\r
425 ONCE_REWRITE_TAC[MESON[REAL_ARITH` a = a / &2 + a / &2`]` u % x + v % y =
\r
426 u % x + ( v/ &2 + v/ &2 ) % y `] THEN REWRITE_TAC[ VECTOR_ADD_RDISTRIB] THEN
\r
430 (* ============== *)
\r
433 let convex3_in_inters = prove (` ! v1 v2 v3. {t | ?a b c.
\r
438 t = a % v1 + b % v2 + c % v3} SUBSET
\r
439 INTERS {t | convex t /\ {v1, v2, v3} SUBSET t} `,
\r
440 REPEAT GEN_TAC THEN
\r
441 MATCH_MP_TAC (SET_RULE ` ( ! x. x IN A ==> x IN B ) ==> A SUBSET B`) THEN
\r
442 REWRITE_TAC[IN_ELIM_THM] THEN REWRITE_TAC[IN_INTERS] THEN
\r
443 REWRITE_TAC[MESON[] `( !x. (?a b c.
\r
448 x = a % v1 + b % v2 + c % v3)
\r
449 ==> (!t. convex t /\ {v1, v2, v3} SUBSET t ==> x IN t))
\r
455 x = a % v1 + b % v2 + c % v3)
\r
456 ==> (!t. convex t /\ {v1, v2, v3} SUBSET t /\ (?a b c.
\r
461 x = a % v1 + b % v2 + c % v3) ==> x IN t)) `] THEN
\r
462 GEN_TAC THEN DISCH_TAC THEN GEN_TAC THEN FIRST_X_ASSUM MP_TAC THEN
\r
463 REWRITE_TAC[ IN_ELIM_THM ; TAUT ` a ==> b ==> c <=> a /\ b ==> c `] THEN
\r
464 MESON_TAC[minconvex3]);;
\r
471 let simpl_conv3 =prove(` ! v1 v2 v3. conv_trg {v1 , v2 ,v3} = {t | ?a b c. &0 <= a /\ &0 <= b /\ &0 <= c /\ a + b + c = &1
\r
472 /\ t = a % v1 + b % v2 + c % v3}`, REPEAT GEN_TAC THEN
\r
473 REWRITE_TAC[conv; hull] THEN REPEAT GEN_TAC THEN
\r
474 REWRITE_TAC[ SET_RULE` a = b <=> a SUBSET b /\ b SUBSET a `] THEN
\r
475 REWRITE_TAC[conv_trg; hull] THEN
\r
476 MATCH_MP_TAC (MATCH_MP ( MESON[] `(! a b. P a b) ==> P a b` ) (MESON[INTERS_SUBSET ]`
\r
477 ! P t0 . ( P t0 /\ aa ) ==> INTERS {t | P t} SUBSET t0 /\ aa`)) THEN
\r
478 REWRITE_TAC[convex3] THEN REWRITE_TAC[ SET_RULE `{v1 , v2, v3} SUBSET a <=>
\r
479 v1 IN a /\ v2 IN a /\ v3 IN a`] THEN REWRITE_TAC [ v1v2v3_in_convex3] THEN
\r
480 REWRITE_TAC[ SET_RULE` v1 IN t /\ v2 IN t /\ v3 IN t <=> {v1, v2, v3} SUBSET t`] THEN
\r
481 REWRITE_TAC[convex3_in_inters]);;
\r
504 (* =========== begining lemma 8.2 ========== *)
\r
506 let near = new_definition ` near (v0:real^N) (r:real) s = { x | x IN s /\
\r
507 dist(x,v0) < r } `;;
\r
509 let near2t0 = new_definition ` near2t0 v0 s = { x | x IN s /\ dist(v0,x) < &2 * t0 }`;;
\r
511 let e_plane = new_definition ` e_plane (a:real^N) (b:real^N) x = ( ~( a=b) /\ dist(a,x) = dist(b,x))`;;
\r
513 let min_dist = new_definition ` min_dist (x:real^3) s = ((?u. u IN s /\
\r
514 (!w. w IN s /\ ~(u = w) ==> dist (u,x) < dist (w,x))) \/
\r
519 dist (u,x) = dist (v,x) /\
\r
520 (!w. w IN s ==> dist (u,x) <= dist (w,x)))) `;;
\r
523 let exists_min_dist = new_axiom ` ! (x :real^3) (s:real^3 -> bool).
\r
524 ~(s = {}) /\ packing s
\r
525 ==> min_dist x s`;;
\r
528 let tarski_FFSXOWD = new_axiom ` !v0 v1 v2 v3 s.
\r
530 ~(v1 = v2 \/ v2 = v3 \/ v3 = v1) /\
\r
531 dist (v1,v2) <= #2.51 /\
\r
532 dist (v2,v3) <= #2.51 /\
\r
533 dist (v3,v1) < sqrt (&8) /\
\r
534 {v1, v2, v3} SUBSET s /\
\r
535 ~(v0 IN {v1, v2, v3})
\r
536 ==> normball v0 #1.255 INTER conv {v1, v2, v3} = {} `;;
\r
539 (* ========== simplize.ml ============ *)
\r
541 let SET3_SUBSET = SET_RULE`! a b c. {a,b,c} SUBSET s <=> a IN s /\ b IN s /\ c IN s `;;
\r
544 let FINITE6 = MESON[ FINITE_RULES ] `! a b c d e f.
\r
548 FINITE {a, b, c} /\
\r
549 FINITE {a, b, c, d} /\
\r
550 FINITE {a, b, c, d, e} /\
\r
551 FINITE {a, b, c, d, e, f} `;;
\r
553 (* ========= new simplizing ========== *)
\r
555 let elimin = REWRITE_RULE[IN];;
\r
557 let CONV_EM = prove(`conv {} = {}:real^A->bool`,
\r
558 REWRITE_TAC[conv;sgn_ge;affsign;UNION_EMPTY;FUN_EQ_THM;elimin
\r
559 NOT_IN_EMPTY;lin_combo;SUM_CLAUSES]
\r
560 THEN REAL_ARITH_TAC);;
\r
562 let CONV_SING = prove(`!u. conv {u:real^A} = {u}`,
\r
563 REWRITE_TAC[conv;sgn_ge;affsign;FUN_EQ_THM;UNION_EMPTY;lin_combo;SUM_SING;VSUM_SING;
\r
564 elimin IN_SING] THEN REPEAT GEN_TAC THEN
\r
565 REWRITE_TAC[TAUT `(p <=> q) = ((p ==> q) /\ (q ==> p))`] THEN
\r
566 REPEAT STRIP_TAC THENL [ASM_MESON_TAC[VECTOR_MUL_LID];
\r
567 ASM_REWRITE_TAC[]] THEN EXISTS_TAC `\ (v:real^A). &1` THEN
\r
568 MESON_TAC[VECTOR_MUL_LID;REAL_ARITH `&0 <= &1`] );;
\r
571 let NOV9 = prove(`!x y z.(x = y /\ y = z
\r
578 w = a % y + b % y + c % z})`,
\r
579 SIMP_TAC[] THEN REWRITE_TAC[SET_RULE` {a,a} = {a}`] THEN
\r
580 REWRITE_TAC[ CONV_SING; GSYM VECTOR_ADD_RDISTRIB] THEN
\r
581 REWRITE_TAC[ MESON[]` a + b + c = &1 /\ w = (a + b + c) % z <=>a + b + c = &1 /\
\r
582 w = &1 % z `; VECTOR_MUL_LID] THEN REWRITE_TAC[ FUN_EQ_THM] THEN
\r
583 REWRITE_TAC[ SET_RULE ` {a} x <=> a = x `; IN_ELIM_THM] THEN
\r
584 REPEAT GEN_TAC THEN DISCH_TAC THEN GEN_TAC THEN
\r
585 NGOAC THEN REWRITE_TAC[ LEFT_EXISTS_AND_THM] THEN
\r
586 MATCH_MP_TAC (MESON[] ` a ==> ( z = x <=> a /\ x = z )`) THEN
\r
587 REPLICATE_TAC 2 (EXISTS_TAC `&0`) THEN EXISTS_TAC ` &1` THEN REAL_ARITH_TAC);;
\r
590 let IN_ACT_SING = SET_RULE `! a x. ({a} x <=> a = x ) /\ ( x IN {a} <=> x = a) /\ {a} a`;;
\r
593 let NOV10 = prove(` ! x y. (x = y
\r
595 (?a b. &0 <= a /\ &0 <= b /\ a + b = &1 /\ x = a % y + b % y))) `,
\r
596 REWRITE_TAC[GSYM VECTOR_ADD_RDISTRIB] THEN
\r
597 REWRITE_TAC[ MESON[VECTOR_MUL_LID]` a + b = &1 /\ x = (a + b) % y <=> a + b = &1 /\
\r
598 x = y`]THEN REPEAT GEN_TAC THEN DISCH_TAC THEN GEN_TAC THEN NGOAC THEN
\r
599 REWRITE_TAC[LEFT_EXISTS_AND_THM] THEN MATCH_MP_TAC (MESON[]` a ==> ( x = y <=> a /\
\r
600 y = x )`)THEN EXISTS_TAC `&0` THEN EXISTS_TAC ` &1` THEN REAL_ARITH_TAC);;
\r
606 let IN_SET2 = SET_RULE `!a b x.
\r
607 (x IN {a, b} <=> x = a \/ x = b) /\ ({a, b} x <=> x = a \/ x = b)`;;
\r
610 let VSUM_DIS2 = prove(` ! x y f. ~(x=y) ==> vsum {x,y} f = f x + f y`, REWRITE_TAC[
\r
611 SET_RULE ` ~( x = y)
\r
612 <=> ~(x IN {y})`] THEN MESON_TAC[ FINITE_RULES; VSUM_CLAUSES; VSUM_SING]);;
\r
614 let SUM_DIS2 = prove(`! x y f. ~(x=y) ==> sum {x,y} f = f x + f y `,REWRITE_TAC[
\r
615 SET_RULE ` ~( x = y)
\r
616 <=> ~(x IN {y})`] THEN MESON_TAC[ FINITE_RULES; SUM_CLAUSES; SUM_SING]);;
\r
619 let TRUONG_LEMMA = prove
\r
621 (?f. x' = f x % x + f y % y /\ (&0 <= f x /\ &0 <= f y) /\
\r
622 f x + f y = &1) <=>
\r
623 (?a b. &0 <= a /\ &0 <= b /\ a + b = &1 /\ x' = a % x + b % y)` ,
\r
624 REPEAT GEN_TAC THEN EQ_TAC
\r
625 THENL [MESON_TAC[]; STRIP_TAC] THEN
\r
626 ASM_CASES_TAC `y:real^N = x` THENL
\r
627 [EXISTS_TAC `\x:real^N. &1 / &2`;
\r
628 EXISTS_TAC `\u:real^N. if u = x then (a:real) else b`] THEN
\r
629 ASM_REWRITE_TAC[GSYM VECTOR_ADD_RDISTRIB] THEN
\r
630 CONV_TAC REAL_RAT_REDUCE_CONV);;
\r
633 let NOV11 = prove(`! z. {z} =
\r
639 w = a % z + b % z + c % z}`,
\r
640 REWRITE_TAC[ FUN_EQ_THM; IN_ACT_SING; IN_ELIM_THM] THEN
\r
641 REWRITE_TAC[GSYM VECTOR_ADD_RDISTRIB] THEN
\r
642 REWRITE_TAC[ MESON[VECTOR_MUL_LID]`a + b + c = &1 /\
\r
643 x = (a + b + c) % z <=> a + b + c = &1 /\ x = z`] THEN
\r
644 NGOAC THEN MATCH_MP_TAC (MESON[]` (? a b c. P a b c) ==> (! z x. z = x <=>
\r
645 (? a b c. P a b c /\ x = z))`) THEN
\r
646 REPLICATE_TAC 2 (EXISTS_TAC `&0`) THEN
\r
647 EXISTS_TAC `&1` THEN REAL_ARITH_TAC);;
\r
651 let CONV2_CONV3 = prove(` !x' y z.
\r
652 (?a b. &0 <= a /\ &0 <= b /\ a + b = &1 /\ x' = a % y + b % z)
\r
658 x' = a % y + b % y + c % z)`,
\r
659 REPEAT GEN_TAC THEN REWRITE_TAC[ VECTOR_ARITH` a % y + b % y + c % z = (a+b) %y + c%z`] THEN STRIP_TAC THEN
\r
660 REPLICATE_TAC 2 (EXISTS_TAC `a/ &2`) THEN
\r
661 EXISTS_TAC `b:real` THEN
\r
662 REWRITE_TAC[ REAL_ARITH` a / &2 + a / &2 = a /\ a / &2 + a / &2 + b = a + b `] THEN
\r
663 ASM_SIMP_TAC[] THEN
\r
664 ASM_REAL_ARITH_TAC);;
\r
667 let CONV3_CONV2 = prove(`! x' y z. (?a b c.
\r
672 x' = a % y + b % y + c % z)
\r
673 ==> (?a b. &0 <= a /\ &0 <= b /\ a + b = &1 /\ x' = a % y + b % z)`,
\r
674 REPEAT GEN_TAC THEN STRIP_TAC THEN EXISTS_TAC ` a + b:real` THEN
\r
675 EXISTS_TAC `c:real` THEN
\r
676 REWRITE_TAC[VECTOR_ADD_RDISTRIB] THEN
\r
677 REWRITE_TAC[VECTOR_ARITH` (a % y + b % y) + c % z = a % y + b % y + c % z `] THEN
\r
678 ASM_SIMP_TAC[REAL_ARITH ` a + b + c = (a + b) + c`] THEN
\r
679 ASM_REAL_ARITH_TAC);;
\r
682 let CONV_SET2 = prove(` ! x y:real^A. conv {x,y} = {w | ? a b. &0 <= a /\ &0 <= b /\ a + b = &1 /\
\r
684 ONCE_REWRITE_TAC[ MESON[] ` (! a b. P a b ) <=> ( ! a b. a = b \/ ~( a= b)
\r
685 ==> P a b )`] THEN
\r
686 REWRITE_TAC[ MESON[]` a \/ b ==> c <=> ( a==> c) /\ ( b==> c)`] THEN
\r
688 REWRITE_TAC[ SET_RULE ` {a,a} = {a}`; CONV_SING; FUN_EQ_THM; IN_ELIM_THM] THEN
\r
689 REWRITE_TAC[ IN_ACT_SING] THEN
\r
690 REWRITE_TAC[NOV10] THEN
\r
691 REWRITE_TAC[conv; sgn_ge; affsign; lin_combo] THEN
\r
692 REWRITE_TAC[UNION_EMPTY; IN_SET2] THEN
\r
693 ONCE_REWRITE_TAC[ MESON[]` ~(x = y) ==> (!x'. (?f. P f x') <=> l x') <=>
\r
694 ~(x = y) ==> (!x'. (?f. ~(x=y) /\ P f x') <=> l x')`] THEN
\r
695 REWRITE_TAC[ MESON[VSUM_DIS2; SUM_DIS2]` ~(x = y) /\
\r
696 x' = vsum {x, y} ff /\ l /\ sum {x, y} f = &1 <=> ~(x = y) /\
\r
697 x' = ff x + ff y /\ l /\ f x + f y = &1 `] THEN
\r
698 REWRITE_TAC[ MESON[]` (!w. w = x \/ w = y ==> &0 <= f w) <=> &0 <= f x /\ &0 <= f y`] THEN
\r
699 ONCE_REWRITE_TAC[ GSYM (MESON[]` ~(x = y) ==> (!x'. (?f. P f x') <=> l x') <=>
\r
700 ~(x = y) ==> (!x'. (?f. ~(x=y) /\ P f x') <=> l x')`)] THEN
\r
701 REPEAT GEN_TAC THEN DISCH_TAC THEN GEN_TAC THEN
\r
702 REWRITE_TAC[ TRUONG_LEMMA]);;
\r
705 let CONV3_A_EQ = prove(`! x y z. (x = y \/ y = z \/ z = x
\r
706 ==> conv {x, y, z} =
\r
712 w = a % x + b % y + c % z})`,
\r
713 MATCH_MP_TAC (MESON[] `(! a b c. P a b c <=> P b a c) /\ (! a b c. a = b \/ b = c ==> P a b c)
\r
714 ==> (! a b c. a = b \/ b = c \/ c = a ==> P a b c )`) THEN
\r
715 SIMP_TAC[ MESON[ SET_RULE ` {a,b,c} = {b,a,c} `]`conv {x, y, z} = conv {y,x,z}`] THEN
\r
716 SIMP_TAC[ MESON[ REAL_ARITH` a + b + c = b + a + c`; VECTOR_ARITH` a % x + b % y + c % z
\r
717 = b % y + a % x + c % z `]` (?a b c.
\r
722 w = a % x + b % y + c % z)
\r
728 w = a % y + b % x + c % z)`] THEN
\r
729 MATCH_MP_TAC (MESON[]` (! a b c. P a b c <=> P c b a ) /\ (! a b c. a = b ==> P a b c)
\r
730 ==> (! a b c. a = b \/ b = c ==> P a b c)`) THEN
\r
731 SIMP_TAC[ MESON[SET_RULE `{a,b,c} ={c,b,a} `]` conv {a,b,c} = conv {c,b,a}`] THEN
\r
732 SIMP_TAC[ MESON[REAL_ARITH` a + b + c = c + b + a`; VECTOR_ARITH` a % x + b % y + c % z
\r
733 = c % z + b % y + a % x `]`(?a b c.
\r
738 w = a % x + b % y + c % z) <=>
\r
744 w = a % z + b % y + c % x)`] THEN
\r
745 REWRITE_TAC[ SET_RULE`{a,a,b} = {a,b}`] THEN
\r
746 ONCE_REWRITE_TAC[ MESON[]` x = y ==> conv {y,z} = s <=> x = y /\( y = z \/
\r
747 ~(y=z))==> conv {y,z} = s `] THEN
\r
748 KHANANG THEN REWRITE_TAC[ MESON[]` a \/ b ==> c <=> (a==> c) /\ (b==> c)`] THEN
\r
749 SIMP_TAC[] THEN REWRITE_TAC[SET_RULE`{a,a} ={a}`; CONV_SING] THEN
\r
750 SIMP_TAC[NOV11] THEN REWRITE_TAC [ GSYM NOV11] THEN
\r
751 REWRITE_TAC[CONV_SET2] THEN
\r
752 REPEAT GEN_TAC THEN STRIP_TAC THEN
\r
753 REWRITE_TAC[ FUN_EQ_THM; IN_ELIM_THM] THEN
\r
754 GEN_TAC THEN REWRITE_TAC[MESON[]` (a <=> b ) <=> ( a ==> b) /\ (b==> a)`] THEN
\r
755 REWRITE_TAC[CONV2_CONV3; CONV3_CONV2]);;
\r
758 let VSUM_DIS3 = prove( `! x y z f. ~(x=y\/y=z\/z=x) ==> vsum {x,y,z} f = f x + f y + f z `,
\r
759 NHANH (SET_RULE` ~(x = y \/ y = z \/ z = x) ==> ({x} INTER {y,z} = {}) `) THEN
\r
760 REWRITE_TAC[ GSYM DISJOINT; SET_RULE `{x, y, z} = {x} UNION {y,z}` ] THEN
\r
761 REWRITE_TAC[MESON[FINITE6; VSUM_UNION]` aa /\ DISJOINT {x} {y, z}
\r
762 ==> vsum ({x} UNION {y, z}) f = ab <=> aa /\ DISJOINT {x} {y, z} ==>
\r
763 vsum {x} f + vsum {y,z} f = ab `] THEN
\r
764 MESON_TAC[VSUM_SING; VSUM_DIS2]);;
\r
767 let SUM_DIS3 = prove(` ! x y z f. ~(x = y \/ y = z \/ z = x) ==> sum {x, y, z} f =
\r
769 NHANH (SET_RULE` ~(x = y \/ y = z \/ z = x) ==> ({x} INTER {y,z} = {}) `) THEN
\r
770 REWRITE_TAC[ GSYM DISJOINT; SET_RULE `{x, y, z} = {x} UNION {y,z}` ] THEN
\r
771 REWRITE_TAC[MESON[FINITE6; SUM_UNION]` aa /\ DISJOINT {x} {y, z}
\r
772 ==> sum ({x} UNION {y, z}) f = ab <=> aa /\ DISJOINT {x} {y, z} ==>
\r
773 sum {x} f + sum {y,z} f = ab `] THEN MESON_TAC[ SUM_SING; SUM_DIS2]);;
\r
777 let EQ_EXPAND = MESON[] `(a <=> b) <=> ( a ==> b ) /\ ( b ==> a )` ;;
\r
781 let CONV_SET3 = prove(`! x y z:real^A. conv {x,y,z} = { w | ? a b c. &0 <= a /\ &0 <= b /\ &0 <= c /\
\r
782 a + b + c = &1 /\ w = a % x + b % y + c % z } `,
\r
783 REPEAT GEN_TAC THEN
\r
784 ONCE_REWRITE_TAC[ MESON[]` conv {x,y,z} = s <=> (x = y \/ y= z \/ z = x ) \/
\r
785 ~(x = y \/ y= z \/ z = x ) ==> conv {x,y,z} = s`] THEN
\r
786 ONCE_REWRITE_TAC[ MESON[]` a \/ b ==> c <=> ( a ==> c ) /\(b==>c)`] THEN
\r
787 REWRITE_TAC[CONV3_A_EQ] THEN
\r
788 REWRITE_TAC[conv; FUN_EQ_THM; affsign; IN_ELIM_THM; sgn_ge; lin_combo; UNION_EMPTY] THEN
\r
789 DISCH_TAC THEN GEN_TAC THEN FIRST_X_ASSUM MP_TAC THEN
\r
790 ONCE_REWRITE_TAC[ MESON[]` a ==> ((?f. P f ) <=> la ) <=>
\r
791 a ==> ((?f. a /\ P f ) <=> la ) `] THEN REWRITE_TAC[MESON[VSUM_DIS3]` ~(x = y \/
\r
792 y = z \/ z = x) /\ x' = vsum {x, y, z} f /\ l <=> ~(x = y \/ y = z \/ z = x) /\
\r
793 x' = f x + f y + f z /\ l `] THEN
\r
794 REWRITE_TAC[ MESON[SUM_DIS3]` ~(x = y \/ y = z \/ z = x) /\ P /\ Q /\ sum {x,y,z} f = &1
\r
795 <=> ~(x = y \/ y = z \/ z = x) /\ P /\ Q /\ ( f x + f y + f z ) = &1`] THEN
\r
796 REWRITE_TAC[SET_RULE ` (!w. {x, y, z} w ==> &0 <= f w) <=> &0 <= f x /\
\r
797 &0 <= f y /\ &0 <= f z `] THEN
\r
798 ONCE_REWRITE_TAC[ GSYM (MESON[]` a ==> ((?f. P f ) <=> la ) <=>
\r
799 a ==> ((?f. a /\ P f ) <=> la ) `)] THEN DISCH_TAC THEN
\r
800 REWRITE_TAC[ EQ_EXPAND] THEN
\r
801 REWRITE_TAC[ MESON[]` (?f. x' = f x % x + f y % y + f z % z /\
\r
802 (&0 <= f x /\ &0 <= f y /\ &0 <= f z) /\
\r
803 f x + f y + f z = &1)
\r
809 x' = a % x + b % y + c % z)`] THEN STRIP_TAC THEN
\r
810 EXISTS_TAC ` (\d. if d = (x:real^A) then (a:real) else ( if d = (y:real^A) then
\r
811 (b:real) else c ))` THEN REPEAT (FIRST_X_ASSUM MP_TAC) THEN
\r
812 REWRITE_TAC[ MESON[]`~( a \/ b ) <=> ~a /\ ~b `] THEN SIMP_TAC[]);;
\r
815 let CONV3_EQ = prove(` ! x y z. conv_trg {x,y,z} = conv {x,y,z} `, REWRITE_TAC[simpl_conv3;
\r
819 let CONV_BAR_EQ = prove(`! bar s. bar IN barrier s ==> conv bar = conv_trg bar `,
\r
820 REWRITE_TAC[barrier; IN_ELIM_THM] THEN MESON_TAC[CONV_SET3; simpl_conv3]);;
\r
822 let OBSTRUCT_EQ = prove(`!x y s. obstruct x y s <=> obstructed x y s`,
\r
823 REWRITE_TAC[obstruct; obstructed] THEN REWRITE_TAC[obstruct; obstructed; conv0_2] THEN
\r
824 MESON_TAC[CONV_BAR_EQ]);;
\r
826 (* === repare VC === *)
\r
828 (* ==== CARD ASSERTION ==== *)
\r
831 let CARD_CLAUSES_IMP = prove(` !a s.
\r
833 ==> CARD (a INSERT s) <= SUC (CARD s) /\
\r
834 (a IN s ==> CARD (a INSERT s) = CARD s) /\
\r
835 (~(a IN s) ==> CARD (a INSERT s) = SUC (CARD s))`,
\r
836 ONCE_REWRITE_TAC[ MESON[] ` ( a ==> b /\ c ) <=> ( a ==> b ) /\ ( a ==> c )`] THEN
\r
837 REWRITE_TAC[ MESON[CARD_CLAUSES] ` FINITE s ==> ( a IN s ==> CARD (a INSERT s) = CARD s ) /\
\r
838 (~(a IN s) ==> CARD (a INSERT s) = SUC (CARD s))`] THEN
\r
839 MESON_TAC[ CARD_CLAUSES; ARITH_RULE ` a <= SUC a /\ a <= a `]);;
\r
841 (* =================== *)
\r
843 let CARD_SING = prove( `! a: A. CARD {a} = 1`, REWRITE_TAC[ MESON[ FINITE6; CARD_EQ_NSUM ]
\r
844 ` CARD {a} = nsum {a} (\x. 1)`] THEN REWRITE_TAC[ NSUM_SING ]);;
\r
846 let CARD_SET2 = prove( ` ! a b . ( CARD {a, b} = 2 <=> ~(a = b)) /\ (CARD {a, b} = 1 <=> a = b ) `,
\r
847 REWRITE_TAC[ MESON[ FINITE6; CARD_CLAUSES ] ` CARD {a,b} = (if a IN {b} then CARD {b} else SUC (CARD {b}))`]
\r
848 THEN REWRITE_TAC[ MESON[ FINITE6; CARD_CLAUSES ] ` CARD {a} = (if a IN {} then CARD {} else SUC (CARD {}))`]
\r
849 THEN REWRITE_TAC[ NOT_IN_EMPTY; IN_SING; CARD_CLAUSES; ADD1] THEN
\r
850 MESON_TAC[ ARITH_RULE ` ~( 0+ 1 = 2 ) /\ (0 + 1) + 1 = 2 /\ ~((0 + 1) + 1 = 1 ) /\ 0 + 1 = 1 `]);;
\r
852 (* ============== *)
\r
854 let CARD_EQUATION = prove(`!(s: A -> bool) t.
\r
855 FINITE s /\ FINITE t
\r
856 ==> CARD (s UNION t) + CARD (s INTER t) = CARD s + CARD t `,
\r
857 NHANH (MESON[FINITE_INTER; FINITE_UNION] `FINITE s /\ FINITE t ==> FINITE ( s UNION t ) /\
\r
858 FINITE ( s INTER t ) `) THEN MESON_TAC[ CARD_EQ_NSUM; NSUM_INCL_EXCL]);;
\r
861 let CARD_DISJOINT = prove(` ! s: A -> bool t. FINITE s /\ FINITE t ==>
\r
862 ( CARD s + CARD t = CARD ( s UNION t ) <=> s INTER t ={} )`,
\r
863 MESON_TAC[CARD_EQUATION; ARITH_RULE ` a + b = a <=> b = 0 `; FINITE_INTER; CARD_EQ_0]);;
\r
866 let CARD2 = prove(` ! a b . CARD {a,b} <= 2 /\ ( CARD {a,b} = 2 <=> ~(a = b ) )`,
\r
867 REWRITE_TAC[ MESON[ CARD_SET2] ` CARD {a, b} = 2 <=> ~(a = b)`] THEN MP_TAC CARD_SET2 THEN
\r
868 ONCE_REWRITE_TAC[ MESON[] ` CARD {a, b} <= 2 <=>
\r
869 ( a = b \/ ~( a = b)) /\ CARD {a, b} <= 2`] THEN KHANANG THEN
\r
870 REWRITE_TAC[ MESON[CARD_SET2] `a = b /\ CARD {a, b} <= 2 \/ ~(a = b) /\ CARD {a, b} <= 2
\r
871 <=> a = b /\ 1 <= 2 \/ ~(a = b) /\ 2 <= 2`] THEN
\r
872 MESON_TAC[ARITH_RULE ` 1 <= 2 /\ 2 <= 2 `]);;
\r
875 let CARD3 = prove(`! a b c . CARD {a,b,c} <= 3 /\
\r
876 ( CARD {a,b,c} = 3 <=> ~( a =b \/ b= c\/ c= a ))`,
\r
877 REWRITE_TAC[ SET_RULE ` {a,b,c} = {a} UNION {b,c}`] THEN
\r
878 REWRITE_TAC[ ARITH_RULE ` CARD ({a} UNION {b, c}) <= 3 <=>
\r
879 CARD ({a} UNION {b, c}) + CARD ({a} INTER {b, c}) <= 3 + CARD ({a} INTER {b, c})`] THEN
\r
880 REWRITE_TAC[ ARITH_RULE ` CARD ({a} UNION {b, c}) = 3 <=>
\r
881 CARD ({a} UNION {b, c}) + CARD ({a} INTER {b, c}) = 3 + CARD ({a} INTER {b, c})`] THEN
\r
882 REWRITE_TAC[ MESON[ FINITE_RULES; CARD_EQUATION] ` CARD ({a} UNION {b, c}) + CARD ({a} INTER {b, c})
\r
883 = CARD {a} + CARD {b,c} `] THEN REWRITE_TAC[ CARD_SING] THEN
\r
884 REWRITE_TAC[ ARITH_RULE `! a b. (1 + a <= 3 + b <=> a <= 2 + b ) /\
\r
885 (1 + a = 3 + b <=> a = 2 + b )`] THEN
\r
886 REWRITE_TAC[ MESON[CARD2; ARITH_RULE ` a <= b ==> a <= b + c: num`] ` CARD {b, c} <= 2 + CARD ({a} INTER {b, c})`] THEN
\r
887 ONCE_REWRITE_TAC[ MESON[CARD2]` CARD {b, c} = P b c <=> CARD {b, c} <= 2 /\ CARD {b, c} = P b c`] THEN
\r
888 REWRITE_TAC[ ARITH_RULE ` a <= 2 /\ a = 2 + b <=> a = 2 /\ b = 0`] THEN
\r
889 REWRITE_TAC[ MESON[FINITE_RULES; CARD2; FINITE_INTER; CARD_EQ_0] ` CARD {b, c} = 2 /\ CARD ({a} INTER {b, c}) = 0
\r
890 <=> ~(b=c) /\ {a} INTER {b, c} = {}`] THEN SET_TAC[]);;
\r
895 let CARD4 = prove(`!a b c d.
\r
896 CARD {a, b, c, d} <= 4 /\
\r
897 (CARD {a, b, c, d} = 4 <=>
\r
898 ~(a IN {b, c, d}) /\ ~(b = c \/ c = d \/ d = b))`,
\r
899 NHANH (MESON[FINITE6; CARD_CLAUSES_IMP]` CARD {a, b, c, d} <= 4 ==> CARD {a, b, c, d}
\r
900 <= SUC (CARD {b,c,d})`) THEN
\r
901 NHANH ( MESON[CARD3] ` aa <= SUC (CARD {b, c, d}) ==> CARD {b,c,d} <= 3 `) THEN
\r
902 REWRITE_TAC[ ARITH_RULE ` CARD {a, b, c, d} <= 4 /\
\r
903 CARD {a, b, c, d} <= SUC (CARD {b, c, d}) /\
\r
904 CARD {b, c, d} <= 3 <=>
\r
905 CARD {a, b, c, d} <= SUC (CARD {b, c, d}) /\ CARD {b, c, d} <= 3`] THEN
\r
906 SIMP_TAC[MESON[FINITE_RULES; CARD_CLAUSES_IMP] ` CARD {a, b, c, d} <= SUC
\r
907 (CARD {b, c, d})`; CARD3; CARD_CLAUSES_IMP] THEN
\r
908 REWRITE_TAC[ ARITH_RULE ` CARD {a, b, c, d} = 4 <=> CARD {a, b, c, d} + CARD ( {a}
\r
909 INTER {b,c,d} ) = 4 + CARD ({a} INTER {b,c,d})`] THEN
\r
910 REWRITE_TAC[ SET_RULE ` {a,b,c,d} = {a} UNION {b,c,d} ` ] THEN
\r
911 REWRITE_TAC[ MESON[FINITE_RULES; CARD_EQUATION; CARD_SING] ` CARD ({a} UNION {b, c, d}) + CARD ({a} INTER {b, c, d})
\r
912 = 1 + CARD {b,c,d} `] THEN
\r
913 NHANH (MESON[CARD3] ` 1 + CARD {b, c, d} = aa ==> CARD {b,c,d} <= 3 `) THEN
\r
914 REWRITE_TAC[ ARITH_RULE `1 + CARD {b, c, d} = 4 + CARD ({a} INTER {b, c, d}) /\
\r
915 CARD {b, c, d} <= 3 <=>
\r
916 CARD {b, c, d} = 3 /\ CARD ({a} INTER {b, c, d}) = 0`] THEN
\r
917 REWRITE_TAC[ CARD3] THEN
\r
918 MESON_TAC[ FINITE_RULES; FINITE_INTER; CARD_EQ_0; SET_RULE `
\r
919 {a} INTER {b, c, d} = {} <=> ~(a IN {b, c, d})` ]);;
\r
922 let CARD5 = prove(` ! a b c d e. CARD {a,b,c,d,e} <= 5 /\
\r
923 ( CARD {a,b,c,d,e} = 5 <=> ~( a IN {b,c,d,e}) /\
\r
924 ~(b IN {c, d, e}) /\ ~(c = d \/ d = e \/ e = c))`,
\r
925 ONCE_REWRITE_TAC[ MESON[ FINITE_RULES; CARD_CLAUSES_IMP] ` CARD {a, b, c, d, e} <= 5 <=>
\r
926 CARD {a, b, c, d, e} <= SUC ( CARD {b,c,d,e} ) ==> CARD {a, b, c, d, e} <= 5`] THEN
\r
927 ONCE_REWRITE_TAC[ MESON[CARD4] ` aa ==> CARD {a, b, c, d, e} <= 5 <=>
\r
928 aa /\ CARD {b,c,d,e} <= 4 ==> CARD {a, b, c, d, e} <= 5`] THEN
\r
929 REWRITE_TAC[ ARITH_RULE ` a <= SUC b /\ b <= 4 ==> a <= 5 `] THEN
\r
930 REWRITE_TAC[ ARITH_RULE ` CARD {a, b, c, d, e} = 5 <=>
\r
931 CARD {a, b, c, d, e} + CARD ({a} INTER {b,c,d,e} ) = 5 + CARD ({a} INTER {b,c,d,e} )`] THEN
\r
932 REWRITE_TAC[ SET_RULE ` {a,b,c,d,e} = {a} UNION {b,c,d,e} `] THEN
\r
933 REWRITE_TAC[ MESON[FINITE_RULES; CARD_EQUATION; CARD_SING ]` CARD ({a} UNION {b, c, d, e}) +
\r
934 CARD ({a} INTER {b, c, d, e}) = 1 + CARD {b,c,d,e} `] THEN
\r
935 ONCE_REWRITE_TAC[ MESON[ CARD4] ` 1 + CARD {b, c, d, e} = aa <=> CARD {b,c,d,e} <= 4 /\
\r
936 1 + CARD {b, c, d, e} = aa `] THEN
\r
937 REWRITE_TAC[ ARITH_RULE ` a <= 4 /\ 1 + a = 5 + b <=> a = 4 /\ b = 0`] THEN
\r
938 REWRITE_TAC[ CARD4; MESON[FINITE_RULES; FINITE_INTER; CARD_EQ_0] `
\r
939 CARD ({a} INTER {b, c, d, e}) = 0 <=> {a} INTER {b, c, d, e} ={} `] THEN SET_TAC[]);;
\r
942 let set_3elements = prove(`(?a b c. ~(a = b \/ b = c \/ c = a) /\ {a, b, c} = {v1, v2, v3}) <=>
\r
943 ~(v1 = v2 \/ v2 = v3 \/ v3 = v1)`, REWRITE_TAC[GSYM CARD3] THEN
\r
947 let db_t0 = prove(`&2 * t0 = &2 * #1.255 /\ &2 * t0 = #2.51 /\ &2 * #1.255 = #2.51`,
\r
948 REWRITE_TAC[t0] THEN REAL_ARITH_TAC);;
\r
951 let without_lost = MESON[] ` ! P x. (!a b. P a b <=> P b a) /\ (?a b. P a b /\ x = a)
\r
952 ==> (?a b. P a b /\ (x = a \/ x = b))`;;
\r
954 let condi_of_wlofg = MESON[]` (!a b. P a b <=> P b a)
\r
955 ==> ((?a b. P a b /\ (x = a \/ x = b)) <=> (?a b. P a b /\ x = a))`;;
\r
959 let CARD_SET_OF_LIST_LE = prove
\r
960 (`!l. CARD(set_of_list l) <= LENGTH l`,
\r
961 LIST_INDUCT_TAC THEN
\r
962 SIMP_TAC[LENGTH; set_of_list; CARD_CLAUSES; FINITE_SET_OF_LIST] THEN
\r
965 let HAS_SIZE_SET_OF_LIST = prove
\r
966 (`!l. (set_of_list l) HAS_SIZE (LENGTH l) <=> PAIRWISE (\x y. ~(x = y)) l`,
\r
967 REWRITE_TAC[HAS_SIZE; FINITE_SET_OF_LIST] THEN LIST_INDUCT_TAC THEN
\r
968 ASM_SIMP_TAC[CARD_CLAUSES; LENGTH; set_of_list; PAIRWISE; ALL;
\r
969 FINITE_SET_OF_LIST; GSYM ALL_MEM; IN_SET_OF_LIST] THEN
\r
970 COND_CASES_TAC THEN ASM_REWRITE_TAC[SUC_INJ] THEN
\r
971 ASM_MESON_TAC[CARD_SET_OF_LIST_LE; ARITH_RULE `~(SUC n <= n)`]);;
\r
973 (* ====================In your theorem we want the n=4 case, so we instantiate it:
\r
974 =========================== *)
\r
976 let HAS_SIZE_SET_OF_LIST_4 = prove
\r
977 (`!a b c d:A. {a,b,c,d} HAS_SIZE 4 <=> PAIRWISE (\x y. ~(x = y)) [a;b;c;d]`,
\r
978 REPEAT GEN_TAC THEN MP_TAC(ISPEC `[a;b;c;d]:A list`HAS_SIZE_SET_OF_LIST) THEN
\r
979 REWRITE_TAC[LENGTH; set_of_list; ARITH]) ;;
\r
981 (* ============================================================================
\r
982 Then finally, using this and a bit of straightforward rearrangement,
\r
983 we can collapse the desired theorem to a lemma that MESON can prove
\r
985 ===============================================================================*)
\r
987 let SET_OF_4 = prove
\r
988 (`! a b c d. ( ? v1 v2 v3 v4:A. ~( v1 = v2 \/ v3 = v4 ) /\
\r
989 {v1, v2 } INTER {v3, v4 } = {} /\
\r
990 { a , b , c , d } = { v1 , v2, v3 ,v4}) <=>
\r
991 ~ ( a = b \/ a = c \/ a = d \/ b = c \/ b = d \/ c = d )`,
\r
992 REPEAT GEN_TAC THEN
\r
993 REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY; INTER_EMPTY; SET_RULE
\r
994 `(a INSERT s) INTER t = {} <=> ~(a IN t) /\ s INTER t = {}`] THEN
\r
996 `(?v1 v2 v3 v4:A. {a,b,c,d} = {v1,v2,v3,v4} /\ {v1,v2,v3,v4} HAS_SIZE 4) <=>
\r
997 {a,b,c,d} HAS_SIZE 4`) THEN
\r
998 REWRITE_TAC[HAS_SIZE_SET_OF_LIST_4; PAIRWISE; ALL; DE_MORGAN_THM; CONJ_ACI]);;
\r
1001 let def_simplex = prove(`! s a b c d. simplex {a, b, c, d} s <=>
\r
1003 {a, b, c, d} SUBSET s /\
\r
1004 ~ ( a = b \/ a = c \/ a = d \/ b = c \/ b = d \/ c = d ) `, REWRITE_TAC[ simplex]
\r
1005 THEN REPEAT GEN_TAC THEN MATCH_MP_TAC (MESON[] ` ( x <=> y ) ==> ( a /\ b /\ x <=>
\r
1006 a /\ b /\ y ) `) THEN ONCE_REWRITE_TAC[MESON[]` {v1, v2, v3, v4} = {a, b, c, d} <=>
\r
1007 {a, b, c, d} = {v1, v2, v3, v4} ` ] THEN REWRITE_TAC[ SET_OF_4]);;
\r
1010 let strict_qua2_imply_strict_qua = prove(`! q d s. strict_qua2 q d s ==> strict_qua q s `,
\r
1011 REWRITE_TAC[ strict_qua2; strict_qua] THEN NHANH (SET_RULE` d = {x, y} ==> x IN d /\
\r
1012 y IN d `) THEN MESON_TAC[ SET_RULE ` x IN d /\ d SUBSET s ==> x IN s `]);;
\r
1014 (* ========== have added to database more =====================*)
\r
1017 let strict_qua2_interior_pos = prove( `!s v v1 v2 v3 v4.
\r
1018 interior_pos v v1 v3 v2 v4 s
\r
1019 ==> strict_qua2 {v, v1, v3, v2} {v1, v3} s /\
\r
1020 strict_qua2 {v, v1, v3, v4} {v1, v3} s /\
\r
1021 strict_qua2 {v, v2, v4, v1} {v2, v4} s /\
\r
1022 strict_qua2 {v, v2, v4, v3} {v2, v4} s`,
\r
1023 REWRITE_TAC[ interior_pos; conflicting_dia; adjacent_pai] THEN MESON_TAC[]);;
\r
1026 let RELATE_Q_SYS = prove (` ! q s. (?v v1 v3 v2 v4.
\r
1027 (q = {v, v1, v2, v3} \/ q = {v, v1, v3, v4}) /\
\r
1028 interior_pos v v1 v3 v2 v4 s /\
\r
1029 anchor_points v1 v3 s = {v, v2, v4} /\
\r
1030 anchor_points v2 v4 s = {v, v1, v3})
\r
1031 ==> strict_qua q s`,
\r
1032 NHANH (MATCH_MP (MESON[]`( ! a b c d e f. P a b c d e f )
\r
1033 ==> P a b c d e f`) strict_qua2_interior_pos) THEN
\r
1034 NHANH (MATCH_MP (MESON[] `( ! x y z. P x y z ) ==> P x y z `)
\r
1035 strict_qua2_imply_strict_qua) THEN
\r
1036 MESON_TAC[ SET_RULE ` {v, v1, v2 , v3 } = {v, v1, v3, v2}`]);;
\r
1040 let strict_qua_in_oct = prove (`! (q:real^3 -> bool) (s:real^3 -> bool ). (?v w v1 v2 v3 v4.
\r
1041 q = {v, w, v1, v2} /\ quartered_oct v w v1 v2 v3 v4 s)
\r
1042 ==> strict_qua q s `,
\r
1044 REWRITE_TAC[ quartered_oct; strict_qua; quarter] THEN
\r
1045 ONCE_REWRITE_TAC[ GSYM (MESON[ DIST_TRIANGLE]` dist (v,w) <= dist (v,v1) + dist (v1,w) /\
\r
1046 dist (v,w) <= dist (v,v2) + dist (v2,w) /\
\r
1047 q = {v, w, v1, v2} <=>
\r
1048 q = {v, w, v1, v2} `)] THEN
\r
1049 ONCE_REWRITE_TAC[SET_RULE ` (!x. x IN {v1, v2, v3, v4}
\r
1050 ==> dist (x,v) <= &2 * t0 /\ dist (x,w) <= &2 * t0) <=>
\r
1051 (!x. x IN {v1, v2, v3, v4}
\r
1052 ==> dist (x,v) <= &2 * t0 /\ dist (x,w) <= &2 * t0) /\
\r
1053 dist (v1,v) <= &2 * t0 /\
\r
1054 dist (v1,w) <= &2 * t0 /\
\r
1055 dist (v2,v) <= &2 * t0 /\
\r
1056 dist (v2,w) <= &2 * t0 `] THEN
\r
1057 PHA THEN REWRITE_TAC[ GSYM d3 ] THEN
\r
1058 ONCE_REWRITE_TAC[ SET_RULE ` q = {v, w, v1, v2} <=> q = {v, w, v1, v2} /\
\r
1059 v IN q /\ w IN q `] THEN
\r
1060 REWRITE_TAC[ MESON[]` d3 v w <= d3 v v1 + d3 v1 w /\
\r
1061 d3 v w <= d3 v v2 + d3 v2 w /\
\r
1062 (q = {v, w, v1, v2} /\ v IN q /\ w IN q) /\
\r
1064 &2 * t0 < d3 v w /\
\r
1065 d3 v w < sqrt (&8) /\ last <=> ((q = {v, w, v1, v2} /\ v IN q /\ w IN q) /\
\r
1067 &2 * t0 < d3 v w /\
\r
1068 d3 v w < sqrt (&8) ) /\ d3 v w <= d3 v v1 + d3 v1 w /\
\r
1069 d3 v w <= d3 v v2 + d3 v2 w /\ last ` ] THEN
\r
1070 REWRITE_TAC[ MESON[]` (?v w v1 v2 v3 v4.
\r
1071 ((q = {v, w, v1, v2} /\ v IN q /\ w IN q) /\
\r
1073 &2 * t0 < d3 v w /\
\r
1074 d3 v w < sqrt (&8)) /\
\r
1075 last v w v1 v2 v3 v4 )
\r
1076 ==> aa /\ bb /\ cc /\
\r
1077 (?x y. x IN q /\ y IN q /\ &2 * t0 < d3 x y /\ d3 x y < sqrt (&8)) <=>
\r
1078 (?v w v1 v2 v3 v4.
\r
1079 ((q = {v, w, v1, v2} /\ v IN q /\ w IN q) /\
\r
1081 &2 * t0 < d3 v w /\
\r
1082 d3 v w < sqrt (&8)) /\
\r
1083 last v w v1 v2 v3 v4)
\r
1084 ==> aa /\ bb /\ cc `] THEN
\r
1085 REWRITE_TAC[ simplex] THEN PHA THEN SIMP_TAC[] THEN REWRITE_TAC[ d3 ] THEN
\r
1086 ONCE_REWRITE_TAC[ MESON[ prove(
\r
1087 `dist (v,w) <= dist (v,v1) + dist (v1,w) /\
\r
1088 dist (v1,v) <= &2 * t0 /\
\r
1089 dist (v1,w) <= &2 * t0 /\
\r
1090 &2 * t0 < dist (v,w) /\
\r
1091 dist (v,w) < sqrt (&8)
\r
1092 ==> &0 < dist (v,v1) /\ &0 < dist (v1,w)`, SIMP_TAC[ DIST_SYM; t0] THEN
\r
1093 REAL_ARITH_TAC)] `
\r
1094 &2 * t0 < dist (v,w) /\
\r
1095 dist (v,w) < sqrt (&8) /\
\r
1096 dist (v,w) <= dist (v,v1) + dist (v1,w) /\
\r
1097 dist (v,w) <= dist (v,v2) + dist (v2,w) /\
\r
1098 (!x. x IN {v1, v2, v3, v4}
\r
1099 ==> dist (x,v) <= &2 * t0 /\ dist (x,w) <= &2 * t0) /\
\r
1100 dist (v1,v) <= &2 * t0 /\
\r
1101 dist (v1,w) <= &2 * t0 /\
\r
1102 dist (v2,v) <= &2 * t0 /\
\r
1103 dist (v2,w) <= &2 * t0 /\
\r
1105 &2 * t0 < dist (v,w) /\
\r
1106 dist (v,w) < sqrt (&8) /\
\r
1107 dist (v,w) <= dist (v,v1) + dist (v1,w) /\
\r
1108 dist (v,w) <= dist (v,v2) + dist (v2,w) /\
\r
1109 (!x. x IN {v1, v2, v3, v4}
\r
1110 ==> dist (x,v) <= &2 * t0 /\ dist (x,w) <= &2 * t0) /\
\r
1111 dist (v1,v) <= &2 * t0 /\
\r
1112 dist (v1,w) <= &2 * t0 /\
\r
1113 dist (v2,v) <= &2 * t0 /\
\r
1114 dist (v2,w) <= &2 * t0 /\
\r
1115 &0 < dist (v,v1) /\
\r
1116 &0 < dist (v1,w) /\ &0 < dist (v,v2) /\
\r
1117 &0 < dist (v2,w) /\
\r
1119 REWRITE_TAC[ t0] THEN
\r
1120 ONCE_REWRITE_TAC[ REAL_ARITH ` &2 <= dist (v1,v2) <=> &2 <= dist (v1,v2) /\
\r
1121 &0 < dist(v1,v2) `] THEN
\r
1122 REWRITE_TAC[ MESON[] ` &0 < dist ( a, b ) /\ sau <=> sau /\ &0 < dist ( a,b) `] THEN PHA THEN
\r
1123 ONCE_REWRITE_TAC[ MESON[ DIST_NZ]` &0 < dist(a,b) <=> &0 < dist(a,b) /\ ~(a=b) `] THEN
\r
1125 REWRITE_TAC[ MESON[]` ~(a=b) /\ last <=> last /\ ~( a=b) `] THEN PHA THEN
\r
1126 REWRITE_TAC[ MESON[] ` q = {v, w, v1, v2} /\
\r
1129 packing s /\ last <=> packing s /\ q = {v, w, v1, v2} /\
\r
1133 REWRITE_TAC[ MESON[] ` (?v w v1 v2 v3 v4.
\r
1134 packing s /\ last v w v1 v2 v3 v4 ) <=> packing s /\ (?v w v1 v2 v3 v4.
\r
1135 last v w v1 v2 v3 v4 ) `] THEN SIMP_TAC[] THEN
\r
1136 REWRITE_TAC[ MESON[] ` q = {v, w, v1, v2} /\ last <=> last /\ q = {v, w, v1, v2} `] THEN
\r
1137 ONCE_REWRITE_TAC[ SET_RULE ` {v, w, v1, v2, v3, v4} SUBSET s /\
\r
1138 q = {v, w, v1, v2} <=> {v, w, v1, v2, v3, v4} SUBSET s /\
\r
1139 q = {v, w, v1, v2} /\ q SUBSET s `] THEN
\r
1140 REWRITE_TAC[ MESON[] ` ~(v = v1) /\
\r
1148 {v, w, v1, v2, v3, v4} SUBSET s /\
\r
1149 q = {v, w, v1, v2} /\
\r
1150 q SUBSET s <=> {v, w, v1, v2, v3, v4} SUBSET s /\
\r
1151 q SUBSET s /\ ( ~(v = v1) /\
\r
1158 ~(v1 = v2) /\ q = {v, w, v1, v2} ) `] THEN
\r
1159 REWRITE_TAC[ MESON[] ` a /\ b/\ c <=> ( a/\ b) /\ c `] THEN
\r
1160 REWRITE_TAC[ MESON[]` a /\ b <=> b /\ a `] THEN
\r
1161 REWRITE_TAC[ MESON[] ` (?v w v1 v2 v3 v4.
\r
1162 q = {v, w, v1, v2} /\
\r
1171 q SUBSET s /\ la v w v1 v2 v3 v4 ) <=>
\r
1172 q SUBSET s /\ (?v w v1 v2 v3 v4.
\r
1173 q = {v, w, v1, v2} /\
\r
1182 la v w v1 v2 v3 v4 ) `] THEN SIMP_TAC[] THEN
\r
1183 ONCE_REWRITE_TAC[ MESON[ REAL_ARITH ` &0 < &2 * #1.255 /\
\r
1184 ( ! a b c. a < b /\ b < c ==> a < c )`; DIST_NZ ] ` &2 * #1.255 < dist (v,w)
\r
1185 <=> ~(v=w) /\ &2 * #1.255 < dist (v,w) ` ] THEN PHA THEN
\r
1186 REWRITE_TAC[ MESON[] ` (~(v = w) /\ &2 * #1.255 < dist (v,w) /\ v IN q /\ w IN q <=>
\r
1187 &2 * #1.255 < dist (v,w) /\ v IN q /\ w IN q /\ ~(v = w)) /\
\r
1188 (a /\ b /\ c <=> (a /\ b) /\ c) `] THEN
\r
1189 REWRITE_TAC[ MESON[] ` ~(v = w) /\ &2 * #1.255 < dist (v,w) /\ v IN q /\ w IN q <=>
\r
1190 &2 * #1.255 < dist (v,w) /\ v IN q /\ w IN q /\ ~(v = w)
\r
1192 REWRITE_TAC[ MESON[] ` a /\ b /\ c <=> (a/\b) /\ c `] THEN
\r
1193 REWRITE_TAC [MESON[] ` aa /\ ~(v = w) <=> ~(v=w) /\ aa `] THEN PHA THEN
\r
1194 REWRITE_TAC[ MESON[]` ~(v = w) /\
\r
1203 q = {v, w, v1, v2} /\ last <=> (~(v = w) /\
\r
1212 q = {v, w, v1, v2}) /\ last `] THEN
\r
1213 SIMP_TAC[ SET_RULE ` {v1, v2, v3, v4} = q <=> q = {v1, v2, v3, v4}`] THEN
\r
1214 ONCE_REWRITE_TAC[ MESON[ SET_RULE ` ~(v = w) /\
\r
1223 ( {v, w} INTER {v1, v2 } = {} /\ ~(v = w \/ v1 = v2 ) )` ] `
\r
1233 q = {v, w, v1, v2} <=>
\r
1234 (q = {v, w, v1, v2} /\
\r
1235 {v, w} INTER {v1, v2} = {} /\
\r
1236 ~(v = w \/ v1 = v2)) /\
\r
1245 ~(v1 = v2) `] THEN
\r
1246 PHA THEN ONCE_REWRITE_TAC[MESON[]` (?v w v1 v2 v3 v4.
\r
1247 q = {v, w, v1, v2} /\
\r
1248 {v, w} INTER {v1, v2} = {} /\
\r
1249 ~(v = w \/ v1 = v2) /\
\r
1250 last v w v1 v2 v3 v4) <=>
\r
1252 q = {v, w, v1, v2} /\
\r
1253 {v, w} INTER {v1, v2} = {} /\
\r
1254 ~(v = w \/ v1 = v2)) /\
\r
1255 (?v w v1 v2 v3 v4.
\r
1256 q = {v, w, v1, v2} /\
\r
1257 {v, w} INTER {v1, v2} = {} /\
\r
1258 ~(v = w \/ v1 = v2) /\
\r
1259 last v w v1 v2 v3 v4) `] THEN SIMP_TAC[] THEN PHA THEN
\r
1260 MATCH_MP_TAC (MESON[] `(! q s. gi q s ==> cc q s ) ==>
\r
1261 ( ! q s. a q /\ gi q s /\ b s ==> cc q s ) `) THEN
\r
1262 REWRITE_TAC[ MESON[] ` {v, w, v1, v2, v3, v4} SUBSET s /\ a <=> a /\
\r
1263 {v, w, v1, v2, v3, v4} SUBSET s `] THEN
\r
1264 REWRITE_TAC[ MESON[]` q = {v, w, v1, v2} /\ a <=> a /\ q = {v, w, v1, v2} `] THEN PHA THEN
\r
1265 ONCE_REWRITE_TAC[SET_RULE ` {v, w, v1, v2, v3, v4} SUBSET s /\ q = {v, w, v1, v2} <=>
\r
1266 {v, w, v1, v2, v3, v4} SUBSET s /\ q = {v, w, v1, v2} /\ q SUBSET s `] THEN
\r
1267 NGOAC THEN ONCE_REWRITE_TAC[MESON[] ` (?v w v1 v2 v3 v4. aaa v w v1 v2 v3 v4 /\
\r
1268 q SUBSET s ) <=> q SUBSET s /\ (?v w v1 v2 v3 v4. aaa v w v1 v2 v3 v4)`] THEN PHA THEN
\r
1270 REWRITE_TAC[ MESON[]` dist (v1,v2) <= &2 * #1.255 /\
\r
1271 &0 < dist (v1,v2) /\
\r
1272 &2 <= dist (v1,v2) /\
\r
1273 dist (v2,w) <= &2 * #1.255 /\
\r
1274 dist (v2,v) <= &2 * #1.255 /\
\r
1275 dist (v1,w) <= &2 * #1.255 /\
\r
1276 dist (v1,v) <= &2 * #1.255 /\
\r
1278 &0 < dist (v1,v2) /\
\r
1279 &2 <= dist (v1,v2) /\
\r
1281 dist (v1,v2) <= &2 * #1.255 /\
\r
1282 dist (v2,w) <= &2 * #1.255 /\
\r
1283 dist (v2,v) <= &2 * #1.255 /\
\r
1284 dist (v1,w) <= &2 * #1.255 /\
\r
1285 dist (v1,v) <= &2 * #1.255 `] THEN PHA THEN
\r
1286 ONCE_REWRITE_TAC[ SET_RULE ` q = {v, w, v1, v2} <=>
\r
1287 q = {v, w, v1, v2} /\
\r
1289 ~({x, y} = {v, w}) /\ x IN q /\ y IN q
\r
1290 ==> (x = v \/ x = w \/ x = v1 \/ x = v2) /\
\r
1291 (y = v \/ y = w \/ y = v1 \/ y = v2) /\
\r
1292 ~(x = v /\ y = w \/ x = w /\ y = v)) `] THEN
\r
1293 REWRITE_TAC[ MESON[] ` ~( a\/ b ) <=> ~ a /\ ~ b `] THEN
\r
1294 NGOAC THEN REWRITE_TAC[ MESON[] ` a /\ ( b \/ c ) <=> a /\ b \/ a /\ c `] THEN
\r
1296 PHA THEN REWRITE_TAC[ MESON[]` day /\ ~(x = v /\ y = w) /\
\r
1297 ~(x = w /\ y = v) <=>
\r
1298 ~(x = v /\ y = w) /\
\r
1299 ~(x = w /\ y = v) /\ day `] THEN
\r
1300 PHA THEN REWRITE_TAC[ MESON[] ` ( a \/ b ) /\c <=> a /\ c \/ b /\ c `] THEN PHA THEN
\r
1301 REWRITE_TAC[ MESON[] ` (a\/b) \/ c <=> a \/ b\/ c`] THEN
\r
1302 REWRITE_TAC[ MESON[] ` ~(x = v /\ y = w) /\
\r
1303 ~(x = w /\ y = v) /\
\r
1304 (x = v /\ y = v \/
\r
1306 x = v1 /\ y = v \/
\r
1307 x = v2 /\ y = v \/
\r
1310 ~(x = v /\ y = w) /\
\r
1311 ~(x = w /\ y = v) /\
\r
1312 (x = v /\ y = v \/ x = v1 /\ y = v \/ x = v2 /\ y = v \/ last) `] THEN
\r
1313 REWRITE_TAC[ MESON[ SET_RULE ` ~({x, y} = {v, w}) <=> ~(x = v /\ y = w) /\ ~(x = w /\ y = v)`]
\r
1315 ~({x, y} = {v, w}) /\ x IN q /\ y IN q
\r
1316 ==> ~(x = v /\ y = w) /\ ~(x = w /\ y = v) /\ last x y)
\r
1317 <=> (!x y. ~({x, y} = {v, w}) /\ x IN q /\ y IN q ==> last x y) `] THEN
\r
1318 ONCE_REWRITE_TAC[ MESON[DIST_REFL; REAL_ARITH ` a = &0 ==> a <= &2 * #1.255 `]
\r
1319 ` x = v /\ y = v <=> x = v /\ y = v /\ dist(x,y) <= &2 * #1.255 `] THEN
\r
1320 REWRITE_TAC[ MESON[]` ( ! x y. P x y ) /\ last <=> last /\ ( ! x y. P x y)`] THEN PHA THEN
\r
1321 ONCE_REWRITE_TAC[MESON[]` dist (v1,v2) <= &2 * #1.255 /\
\r
1322 dist (v2,w) <= &2 * #1.255 /\
\r
1323 dist (v2,v) <= &2 * #1.255 /\
\r
1324 dist (v1,w) <= &2 * #1.255 /\
\r
1325 dist (v1,v) <= &2 * #1.255 /\
\r
1326 (!x y. ~({x, y} = {v, w}) /\ x IN q /\ y IN q ==> last x y) <=>
\r
1327 dist (v1,v2) <= &2 * #1.255 /\
\r
1328 dist (v2,w) <= &2 * #1.255 /\
\r
1329 dist (v2,v) <= &2 * #1.255 /\
\r
1330 dist (v1,w) <= &2 * #1.255 /\
\r
1331 dist (v1,v) <= &2 * #1.255 /\
\r
1333 ~({x, y} = {v, w}) /\ x IN q /\ y IN q
\r
1335 dist (v1,v2) <= &2 * #1.255 /\
\r
1336 dist (v2,w) <= &2 * #1.255 /\
\r
1337 dist (v2,v) <= &2 * #1.255 /\
\r
1338 dist (v1,w) <= &2 * #1.255 /\
\r
1339 dist (v1,v) <= &2 * #1.255 /\ last x y) `] THEN
\r
1340 REWRITE_TAC[ MESON[ DIST_SYM]`dist (v1,v2) <= &2 * #1.255 /\
\r
1341 dist (v2,w) <= &2 * #1.255 /\
\r
1342 dist (v2,v) <= &2 * #1.255 /\
\r
1343 dist (v1,w) <= &2 * #1.255 /\
\r
1344 dist (v1,v) <= &2 * #1.255 /\
\r
1345 (x = v /\ y = v /\ dist (x,y) <= &2 * #1.255 \/
\r
1346 x = v1 /\ y = v \/
\r
1347 x = v2 /\ y = v \/
\r
1349 dist (v1,v2) <= &2 * #1.255 /\
\r
1350 dist (v2,w) <= &2 * #1.255 /\
\r
1351 dist (v2,v) <= &2 * #1.255 /\
\r
1352 dist (v1,w) <= &2 * #1.255 /\
\r
1353 dist (v1,v) <= &2 * #1.255 /\
\r
1354 (x = v /\ y = v /\ dist (x,y) <= &2 * #1.255 \/
\r
1355 x = v1 /\ y = v /\ dist (x,y) <= &2 * #1.255 \/
\r
1356 x = v2 /\ y = v /\ dist (x,y) <= &2 * #1.255 \/
\r
1358 REWRITE_TAC[ MESON[]` a \/ b \/ c <=> (a \/ b ) \/ c `] THEN
\r
1359 REWRITE_TAC[ MESON[] ` ((((a \/ x = v2 /\ y = v1) \/ x = v /\ y = v2) \/ x = w /\ y = v2) \/
\r
1360 x = v1 /\ y = v2) \/
\r
1361 x = v2 /\ y = v2 /\ dist (x,y) <= &2 * #1.255 <=>
\r
1362 (((x = v2 /\ y = v1 \/ x = v /\ y = v2) \/ x = w /\ y = v2) \/
\r
1363 x = v1 /\ y = v2) \/
\r
1364 x = v2 /\ y = v2 /\ dist (x,y) <= &2 * #1.255 \/
\r
1366 REWRITE_TAC[ GSYM (MESON[]` a \/ b \/ c <=> (a \/ b ) \/ c `)] THEN
\r
1367 REWRITE_TAC[MESON[DIST_SYM ]` dist (v1,v2) <= &2 * #1.255 /\
\r
1368 dist (v2,w) <= &2 * #1.255 /\
\r
1369 dist (v2,v) <= &2 * #1.255 /\
\r
1370 dist (v1,w) <= &2 * #1.255 /\
\r
1371 dist (v1,v) <= &2 * #1.255 /\
\r
1372 (x = v2 /\ y = v1 \/
\r
1373 x = v /\ y = v2 \/
\r
1374 x = w /\ y = v2 \/
\r
1375 x = v1 /\ y = v2 \/ last )
\r
1376 <=> dist (v1,v2) <= &2 * #1.255 /\
\r
1377 dist (v2,w) <= &2 * #1.255 /\
\r
1378 dist (v2,v) <= &2 * #1.255 /\
\r
1379 dist (v1,w) <= &2 * #1.255 /\
\r
1380 dist (v1,v) <= &2 * #1.255 /\
\r
1381 ((x = v2 /\ y = v1 \/
\r
1382 x = v /\ y = v2 \/
\r
1383 x = w /\ y = v2 \/
\r
1384 x = v1 /\ y = v2 ) /\ dist( x,y) <= &2 * #1.255 \/ last ) `] THEN
\r
1385 REWRITE_TAC[ MESON[]` a \/ b \/ c <=> (a \/ b ) \/ c `] THEN
\r
1386 REWRITE_TAC[ MESON[]` ((((a \/ x = v1 /\ y = w) \/
\r
1387 x = v2 /\ y = w) \/
\r
1388 x = v /\ y = v1) \/
\r
1389 x = w /\ y = v1) \/
\r
1390 x = v1 /\ y = v1 /\ dist (x,y) <= &2 * #1.255 <=>
\r
1391 (((x = v1 /\ y = w \/
\r
1392 x = v2 /\ y = w) \/
\r
1393 x = v /\ y = v1) \/
\r
1394 x = w /\ y = v1) \/
\r
1395 x = v1 /\ y = v1 /\ dist (x,y) <= &2 * #1.255 \/ a `] THEN
\r
1396 REWRITE_TAC[ GSYM (MESON[]` a \/ b \/ c <=> (a \/ b ) \/ c `)] THEN
\r
1397 REWRITE_TAC[ MESON[ DIST_SYM ] `
\r
1398 dist (v1,v2) <= &2 * #1.255 /\
\r
1399 dist (v2,w) <= &2 * #1.255 /\
\r
1400 dist (v2,v) <= &2 * #1.255 /\
\r
1401 dist (v1,w) <= &2 * #1.255 /\
\r
1402 dist (v1,v) <= &2 * #1.255 /\
\r
1403 (x = v1 /\ y = w \/
\r
1404 x = v2 /\ y = w \/
\r
1405 x = v /\ y = v1 \/
\r
1406 x = w /\ y = v1 \/
\r
1408 dist (v1,v2) <= &2 * #1.255 /\
\r
1409 dist (v2,w) <= &2 * #1.255 /\
\r
1410 dist (v2,v) <= &2 * #1.255 /\
\r
1411 dist (v1,w) <= &2 * #1.255 /\
\r
1412 dist (v1,v) <= &2 * #1.255 /\
\r
1413 ((x = v1 /\ y = w \/
\r
1414 x = v2 /\ y = w \/
\r
1415 x = v /\ y = v1 \/
\r
1416 x = w /\ y = v1) /\
\r
1417 dist (x,y) <= &2 * #1.255 \/
\r
1419 REWRITE_TAC[ MESON[] ` x = v1 /\ y = v2 /\ dist (x,y) <= &2 * #1.255
\r
1420 <=> (x = v1 /\ y = v2) /\ dist (x,y) <= &2 * #1.255 `] THEN
\r
1421 REWRITE_TAC[ GSYM (MESON[]` a \/ b \/ c <=> (a \/ b ) \/ c `)] THEN
\r
1422 REWRITE_TAC[ MESON[]` a /\ c \/ b /\ c <=> ( a\/ b) /\ c `] THEN NGOAC THEN
\r
1423 ONCE_REWRITE_TAC[ MESON[] ` ( ! x y. P x y ==> L x y /\ TT x y ) <=>
\r
1424 ( ! x y. P x y ==> L x y /\ TT x y ) /\ ( ! x y. P x y ==> TT x y ) `] THEN
\r
1426 REWRITE_TAC[ MESON[]` a /\ (!x y.
\r
1427 (~({x, y} = {v, w}) /\ x IN q) /\ y IN q
\r
1428 ==> dist (x,y) <= &2 * #1.255) <=> (!x y.
\r
1429 (~({x, y} = {v, w}) /\ x IN q) /\ y IN q
\r
1430 ==> dist (x,y) <= &2 * #1.255) /\ a `] THEN
\r
1431 REWRITE_TAC[ MESON[]` ((( a /\dist (v,w) < sqrt (&8)) /\
\r
1432 &2 * #1.255 < dist (v,w)) /\
\r
1435 <=> (((dist (v,w) < sqrt (&8)) /\
\r
1436 &2 * #1.255 < dist (v,w)) /\
\r
1438 w IN q /\ a `] THEN PHA THEN
\r
1439 ONCE_REWRITE_TAC[MESON[ REAL_ARITH ` a < b ==> a <= b `]` (?v w v1 v2 v3 v4.
\r
1441 ~({x, y} = {v, w}) /\ x IN q /\ y IN q
\r
1442 ==> dist (x,y) <= &2 * #1.255) /\
\r
1443 dist (v,w) < sqrt (&8) /\
\r
1444 &2 * #1.255 < dist (v,w) /\
\r
1446 w IN q /\ last v w v1 v2 v3 v4 )
\r
1449 ~({x, y} = {v, w}) /\ x IN q /\ y IN q
\r
1450 ==> dist (x,y) <= &2 * #1.255) /\
\r
1451 dist (v,w) <= sqrt (&8) /\
\r
1452 &2 * #1.255 <= dist (v,w) /\
\r
1454 w IN q) /\ (?v w v1 v2 v3 v4.
\r
1456 ~({x, y} = {v, w}) /\ x IN q /\ y IN q
\r
1457 ==> dist (x,y) <= &2 * #1.255) /\
\r
1458 dist (v,w) < sqrt (&8) /\
\r
1459 &2 * #1.255 < dist (v,w) /\
\r
1461 w IN q /\ last v w v1 v2 v3 v4 )`] THEN PHA THEN
\r
1462 REPEAT GEN_TAC THEN MATCH_MP_TAC (MESON[] ` ( b ==> d ) ==> (a /\ b /\ c ==> d) `) THEN
\r
1467 let WHEN_IN_Q_SYS = prove (`! q s. q IN Q_SYS s ==> quasi_reg_tet q s \/ strict_qua q s \/
\r
1469 (q = {v, v1, v2, v3} \/ q = {v, v1, v3, v4}) /\
\r
1470 interior_pos v v1 v3 v2 v4 s /\
\r
1471 anchor_points v1 v3 s = {v, v2, v4} /\
\r
1472 anchor_points v2 v4 s = {v, v1, v3})`,
\r
1473 REWRITE_TAC[ Q_SYS; IN_ELIM_THM] THEN MESON_TAC[strict_qua_in_oct] );;
\r
1478 let CASES_OF_Q_SYS = prove (`!q s. q IN Q_SYS s ==> quasi_reg_tet q s \/ strict_qua q s`,
\r
1479 NHANH (MATCH_MP (MESON[]` ( ! a b. P a b) ==> P a b` ) WHEN_IN_Q_SYS) THEN
\r
1480 REPEAT GEN_TAC THEN MATCH_MP_TAC (MESON[]` ( c ==> b) ==> aa /\ ( a \/ b\/ c )
\r
1481 ==> a \/ b `) THEN REWRITE_TAC[ RELATE_Q_SYS]);;
\r
1486 let simplex_interior_pos = prove(`!s v v1 v2 v3 v4.
\r
1487 interior_pos v v1 v3 v2 v4 s
\r
1488 ==> simplex {v, v1, v3, v2} s /\
\r
1489 simplex {v, v1, v3, v4} s /\
\r
1490 simplex {v, v2, v4, v1} s /\
\r
1491 simplex {v, v2, v4, v3} s`,
\r
1492 ONCE_REWRITE_TAC[ MESON[strict_qua2_interior_pos]`
\r
1493 interior_pos v v1 v3 v2 v4 s <=>
\r
1494 interior_pos v v1 v3 v2 v4 s /\ strict_qua2 {v, v1, v3, v2} {v1, v3} s /\
\r
1495 strict_qua2 {v, v1, v3, v4} {v1, v3} s /\
\r
1496 strict_qua2 {v, v2, v4, v1} {v2, v4} s /\
\r
1497 strict_qua2 {v, v2, v4, v3} {v2, v4} s `] THEN
\r
1498 REWRITE_TAC[ strict_qua2 ] THEN
\r
1499 NGOAC THEN REWRITE_TAC[ MESON[]` a /\ quarter {v, v1, v2, v3} s <=>
\r
1500 quarter {v, v1, v2, v3} s /\ a `] THEN PHA THEN
\r
1501 REPEAT GEN_TAC THEN MATCH_MP_TAC (MESON[] ` (a /\ b/\c /\ d ==> las )
\r
1502 ==> ( a/\ b/\ c/\ d /\ dd ==> las ) `) THEN
\r
1503 NGOAC THEN REWRITE_TAC[ MESON[] `(( a /\ packing s ) /\
\r
1504 simplex {v, v1, v2, v3} s) <=> simplex {v, v1, v2, v3} s /\ packing s /\ a`] THEN
\r
1505 REWRITE_TAC[MESON[]` packing s /\ a <=> a /\ packing s`] THEN PHA THEN
\r
1506 MESON_TAC[quarter]);;
\r
1511 let QUA_TET_IMPLY_QUA_TRI = prove(` ! s v0 v1 v2 . (?v4. quasi_reg_tet ({v0, v1, v2} UNION {v4}) s)
\r
1512 ==> quasi_tri {v0, v1, v2} s`, REWRITE_TAC[ quasi_reg_tet; quasi_tri] THEN
\r
1513 REWRITE_TAC[ SET_RULE ` {a,b,c} UNION {d} = {a,b,c,d} `; def_simplex; set_3elements] THEN
\r
1514 MESON_TAC[SET_RULE ` {a,b,c} SUBSET {a,b,c,d} ` ; SUBSET; SUBSET_TRANS]);;
\r
1517 let PAIR_D3 = prove(` ! i j u w. {u,w} = {i,j} ==> d3 i j = d3 u w `,
\r
1518 REWRITE_TAC[ SET_RULE ` {u, w} = {i, j} <=> u= i /\ w = j \/ u = j /\ w = i `] THEN
\r
1519 MESON_TAC[ trg_d3_sym]);;
\r
1522 let PAIR_DIST = prove(` ! i j u w. {u,w} = {i,j} ==> dist(i,j) = dist(u,w) `,
\r
1523 REWRITE_TAC[ SET_RULE ` {u, w} = {i, j} <=> u= i /\ w = j \/ u = j /\ w = i `] THEN
\r
1524 MESON_TAC[ DIST_SYM]);;
\r
1528 (* ============== *)
\r
1530 let DIAGONAL_QUA = prove(`!a b q s.
\r
1533 &2 * t0 < d3 a b /\
\r
1535 ==> diagonal a b q s `,
\r
1536 REWRITE_TAC[diagonal; SET_RULE ` a IN q /\ b IN q /\ &2 * t0 < d3 a b /\ quarter q s
\r
1537 ==> quarter q s /\ {a, b} SUBSET q /\ l <=> a IN q /\ b IN q /\ &2 * t0 < d3 a b
\r
1538 /\ quarter q s ==> l`] THEN REWRITE_TAC[quarter] THEN NGOAC THEN
\r
1539 REWRITE_TAC[ MESON[] ` a /\ (? u v. P u v ) <=> (? u v. a /\ P u v ) `] THEN
\r
1540 REWRITE_TAC[ REAL_ARITH ` a < b <=> ~( b <= a ) `] THEN
\r
1541 PHA THEN REWRITE_TAC[ MESON[]` a IN q /\ b IN q /\ ~(d3 a b <= &2 * t0) /\ las <=>
\r
1542 las /\ a IN q /\ b IN q /\ ~(d3 a b <= &2 * t0) `] THEN PHA THEN
\r
1543 NHANH (MESON[]` (!x y.
\r
1544 x IN q /\ y IN q /\ ~({x, y} = {v, w}) ==> d3 x y <= &2 * t0) /\
\r
1547 ~(d3 a b <= &2 * t0) ==> {a,b} = {v,w} `) THEN
\r
1548 NHANH (MESON[ PAIR_D3] ` aa /\ {a, b} = {v, w} ==> d3 a b = d3 v w `) THEN
\r
1549 MESON_TAC[ PAIR_D3; REAL_ARITH` (a <= a) /\ ( a <= b /\ b <= c ==> a <= c ) `]);;
\r
1554 let NOV2 = prove( `!a b c v4.
\r
1555 (?i j. i IN {a, b, c} /\ j IN {a, b, c} /\ ~(i = j) /\ #2.51 < d3 i j) /\
\r
1557 v IN {a, b, c, v4} /\
\r
1558 w IN {a, b, c, v4} /\
\r
1559 #2.51 <= d3 v w /\
\r
1560 d3 v w <= sqrt (&8) /\
\r
1562 x IN {a, b, c, v4} /\ y IN {a, b, c, v4} /\ ~({x, y} = {v, w})
\r
1563 ==> d3 x y <= #2.51))
\r
1569 x IN {a, b, c} /\ y IN {a, b, c} /\ ~({x, y} = {i, j})
\r
1570 ==> d3 x y <= #2.51))`,
\r
1571 REWRITE_TAC[ MESON[] ` (? i j. P i j ) /\ (? v w. Q v w ) <=> ( ? i j u w. P i j /\ Q u w ) `] THEN
\r
1572 REWRITE_TAC[ MESON[] ` (i IN {a, b, c} /\ j IN {a, b, c} /\ ~(i = j) /\ #2.51 < d3 i j) /\ aa <=>
\r
1573 aa /\ (i IN {a, b, c} /\ j IN {a, b, c} /\ ~(i = j) /\ #2.51 < d3 i j)`] THEN
\r
1575 REWRITE_TAC[ REAL_ARITH ` a < b <=> ~( b <= a ) `] THEN
\r
1576 NHANH (MESON[ SET_RULE ` x IN {a,b,c} ==> x IN {a,b,c,d} ` ] ` (!x y.
\r
1577 x IN {a, b, c, v4} /\ y IN {a, b, c, v4} /\ ~({x, y} = {u, w})
\r
1578 ==> d3 x y <= #2.51) /\
\r
1582 ~(d3 i j <= #2.51)
\r
1583 ==> {i,j} = {u,w} `) THEN PHA THEN
\r
1584 NHANH ( MESON[ PAIR_D3] ` ~(d3 i j <= #2.51) /\
\r
1585 {i, j} = {u, w} ==> d3 i j = d3 u w `) THEN
\r
1586 PHA THEN REWRITE_TAC[ MESON[]` {i, j} = {u, w} /\ a <=> a /\ {i, j} = {u, w}`] THEN
\r
1587 REWRITE_TAC[ MESON[] ` (! x y. P x y ) /\ a <=> a /\ (! x y. P x y) `] THEN PHA THEN
\r
1588 NHANH ( MESON[ SET_RULE ` x IN {a,b,c} ==> x IN {a,b,c,d} `] ` {i, j} = {u, w} /\
\r
1590 x IN {a, b, c, v4} /\ y IN {a, b, c, v4} /\ ~({x, y} = {u, w})
\r
1591 ==> d3 x y <= #2.51)
\r
1593 x IN {a, b, c} /\ y IN {a, b, c} /\ ~({x, y} = {i, j})
\r
1594 ==> d3 x y <= #2.51)`) THEN MESON_TAC[]);;
\r
1598 let TRIANGLE_IN_STRICT_QUA = prove( `!s a b c.
\r
1599 (?v4. strict_qua ( {a,b,c} UNION {v4}) s)
\r
1600 ==> quasi_tri {a,b,c} s \/
\r
1602 {aa, bb} SUBSET {a,b,c} /\
\r
1603 #2.51 < dist (aa,bb) /\
\r
1605 ~({x, y} = {aa, bb}) /\ {x, y} SUBSET {a,b,c}
\r
1606 ==> dist (x,y) <= #2.51))`,
\r
1607 REWRITE_TAC[ strict_qua; quarter; simplex] THEN
\r
1608 REWRITE_TAC[SET_RULE `{a, b, c} UNION {d} = {a,b,c,d}`;MESON[]` {v1, v2, v3, v4'} =
\r
1609 {a, b, c, v4} <=> {a, b, c, v4} = {v1, v2, v3, v4'} `; SET_OF_4] THEN
\r
1610 REWRITE_TAC[ quasi_tri] THEN
\r
1611 NHANH (MESON[] ` {a, b, c, v4} SUBSET s ==> ((!i j.
\r
1612 i IN {a, b, c} /\ j IN {a, b, c} /\ ~(i = j)
\r
1613 ==> d3 i j <= &2 * t0) \/
\r
1615 i IN {a, b, c} /\ j IN {a, b, c} /\ ~(i = j)
\r
1616 /\ ~(d3 i j <= &2 * t0))) `) THEN PHA THEN
\r
1617 NHANH (SET_RULE ` {a, b, c, v4} SUBSET s ==> {a, b, c} SUBSET s `) THEN
\r
1618 REPEAT GEN_TAC THEN KHANANG THEN
\r
1619 MATCH_MP_TAC (MESON[] ` ((? a. P a) ==> l) /\ ((?a. Q a ) ==> l ) ==>
\r
1620 (?a . P a \/ Q a ) ==> l `) THEN
\r
1621 REWRITE_TAC[ MESON[]` (?v4. packing s /\
\r
1623 {a, b, c, v4} SUBSET s /\
\r
1624 {a, b, c} SUBSET s /\
\r
1626 i IN {a, b, c} /\ j IN {a, b, c} /\ ~(i = j)
\r
1627 ==> d3 i j <= &2 * t0) /\
\r
1628 ~(a = b \/ a = c \/ a = v4 \/ b = c \/ b = v4 \/ c = v4) /\
\r
1630 v IN {a, b, c, v4} /\
\r
1631 w IN {a, b, c, v4} /\
\r
1632 &2 * t0 <= d3 v w /\
\r
1633 d3 v w <= sqrt (&8) /\
\r
1635 x IN {a, b, c, v4} /\
\r
1636 y IN {a, b, c, v4} /\
\r
1637 ~({x, y} = {v, w})
\r
1638 ==> d3 x y <= &2 * t0)) /\
\r
1640 x IN {a, b, c, v4} /\
\r
1641 y IN {a, b, c, v4} /\
\r
1642 &2 * t0 < d3 x y /\
\r
1643 d3 x y < sqrt (&8)))
\r
1645 {a, b, c} SUBSET s /\
\r
1647 ~(a' = b' \/ b' = c' \/ c' = a') /\ {a', b', c'} = {a, b, c}) /\
\r
1649 x IN {a, b, c} /\ y IN {a, b, c} /\ ~(x = y)
\r
1650 ==> d3 x y <= &2 * t0) \/
\r
1652 {aa, bb} SUBSET {a, b, c} /\
\r
1653 #2.51 < dist (aa,bb) /\
\r
1655 ~({x, y} = {aa, bb}) /\ {x, y} SUBSET {a, b, c}
\r
1656 ==> dist (x,y) <= #2.51))`] THEN
\r
1657 REWRITE_TAC[ GSYM d3; REAL_ARITH ` ~( a <= b ) <=> b < a `] THEN
\r
1658 REWRITE_TAC[ t0; REAL_ARITH` &2 * #1.255 = #2.51 `] THEN
\r
1659 REWRITE_TAC[ SET_RULE ` {aa, bb} SUBSET s <=> aa IN s /\ bb IN s `] THEN
\r
1660 ONCE_REWRITE_TAC[ MESON[]`(? x y. P x y ) /\ a <=> a /\ (? x y. P x y )`] THEN PHA THEN
\r
1661 ONCE_REWRITE_TAC[ MESON[] ` (? x y . P x y ) /\ a /\ b <=> a /\ b /\ (? x y. P x y)`] THEN
\r
1662 NHANH (CUTHE4 NOV2 ) THEN MESON_TAC[]);;
\r
1664 (* ================== *)
\r
1667 let A_LEMMA = prove(`!s v0 v1 v2.
\r
1668 quasi_tri {v0, v1, v2} s
\r
1670 ~(xx = yy) /\ {xx, yy} SUBSET {v1, v2, v0}
\r
1671 ==> &2 <= dist (xx,yy) /\ dist (xx,yy) <= sqrt (&8)) /\
\r
1673 aa IN {v1, v2, v0} /\ bb IN {v1, v2, v0}
\r
1674 ==> dist (aa,bb) <= #2.51) \/
\r
1676 {aa, bb} SUBSET {v1, v2, v0} /\
\r
1677 #2.51 < dist (aa,bb) /\
\r
1679 ~({x, y} = {aa, bb}) /\ {x, y} SUBSET {v1, v2, v0}
\r
1680 ==> dist (x,y) <= #2.51)))`,
\r
1681 REWRITE_TAC[ MESON[]` a /\ {v0, v1, v2} SUBSET s /\ c <=> ( a /\ {v0, v1, v2}
\r
1682 SUBSET s) /\ c ` ] THEN NHANH (MESON[SET_RULE ` {x,y} SUBSET b /\ b SUBSET s ==>
\r
1683 s x /\ s y `]` (!u v. s u /\ s v /\ ~(u = v) ==> &2 <= dist (u,v)) /\
\r
1684 {v0, v1, v2} SUBSET s ==> (!xx yy.
\r
1685 ~(xx = yy) /\ {xx, yy} SUBSET {v0, v1, v2}
\r
1686 ==> &2 <= dist (xx,yy) ) `) THEN
\r
1687 REWRITE_TAC[ quasi_tri; set_3elements; packing; MESON[] ` a /\ {v0, v1, v2} SUBSET s /\ c <=>
\r
1688 ( a /\ {v0, v1, v2} SUBSET s)/\c` ] THEN
\r
1689 NHANH (MESON[ SET_RULE ` x IN a /\ a SUBSET s ==> s x ` ] ` (!u v. s u /\ s v /\
\r
1690 ~(u = v) ==> &2 <= dist (u,v)) /\ {v0, v1, v2} SUBSET s ==> (!x y.
\r
1691 x IN {v0, v1, v2} /\ y IN {v0, v1, v2} /\ ~(x = y)
\r
1692 ==> &2 <= dist (x,y))`) THEN PHA THEN
\r
1693 REWRITE_TAC[ SET_RULE ` x IN {v0, v1, v2} /\ y IN {v0, v1, v2} /\ ~(x = y) <=>
\r
1694 ~(x = y) /\ {x, y } SUBSET {v0, v1, v2}`] THEN
\r
1695 REWRITE_TAC[ t0] THEN
\r
1696 ONCE_REWRITE_TAC[ MESON[ MATCH_MP REAL_LT_RSQRT (REAL_ARITH ` (&2 * #1.255) pow 2 < &8 `); REAL_ARITH` a <= b /\ b < c ==> a <= c ` ]`
\r
1697 d3 x y <= &2 * #1.255 <=> d3 x y <= &2 * #1.255 /\ d3 x y <= sqrt( &8 ) `] THEN
\r
1698 REWRITE_TAC[ REAL_ARITH ` &2 * #1.255 = #2.51`] THEN
\r
1699 NHANH ( MESON[d3; DIST_SYM; DIST_REFL; REAL_ARITH ` &0 <= #2.51 `]` (!x y.
\r
1700 ~(x = y) /\ {x, y} SUBSET {v0, v1, v2}
\r
1701 ==> d3 x y <= #2.51 /\ d3 x y <= sqrt (&8))
\r
1703 {x, y} SUBSET {v0, v1, v2}
\r
1704 ==> d3 x y <= #2.51 )`) THEN
\r
1705 REWRITE_TAC[ GSYM d3] THEN REWRITE_TAC[ SET_RULE ` a IN s /\ b IN s <=>
\r
1706 {a,b} SUBSET s `] THEN
\r
1707 MESON_TAC[ SET_RULE` {v0, v1, v2} = {v1, v2, v0}`]);;
\r
1711 let NOV1 = prove(` ! s v0 v1 v2 . (?v4. quasi_reg_tet ({v0, v1, v2} UNION {v4}) s)
\r
1713 ~(xx = yy) /\ {xx, yy} SUBSET {v1, v2, v0}
\r
1714 ==> &2 <= dist (xx,yy) /\ dist (xx,yy) <= sqrt (&8)) /\
\r
1716 aa IN {v1, v2, v0} /\ bb IN {v1, v2, v0} ==> dist (aa,bb) <= #2.51) \/
\r
1718 {aa, bb} SUBSET {v1, v2, v0} /\
\r
1719 #2.51 < dist (aa,bb) /\
\r
1721 ~({x, y} = {aa, bb}) /\ {x, y} SUBSET {v1, v2, v0}
\r
1722 ==> dist (x,y) <= #2.51)))`, NHANH (CUTHE4 QUA_TET_IMPLY_QUA_TRI) THEN
\r
1723 REPEAT GEN_TAC THEN MATCH_MP_TAC (MESON[]` (b ==> c) ==> a /\ b ==> c `) THEN
\r
1724 REWRITE_TAC[ A_LEMMA]);;
\r
1728 (* ================ *)
\r
1732 (* ======= have added to database_more =========== *)
\r
1736 let DOT_SUB_ADD = VECTOR_ARITH `! a b. b dot b - a dot a = (b - a) dot (b + a)` ;;
\r
1738 let DIST_LT_HALF_PLANE = prove(`!x:real^A a:real^A b:real^A.
\r
1739 dist(x,a) < dist(x,b) <=> &0 < (a - b) dot (&2 % x - (a + b))`,
\r
1740 ABBREV_TAC ` an a b x = ((a:real^A) - b) dot (&2 % x - (a + b))` THEN
\r
1741 REWRITE_TAC[dist; vector_norm] THEN
\r
1742 REWRITE_TAC[MESON[DOT_POS_LE; SQRT_MONO_LT_EQ]` sqrt ( x dot x) < sqrt (y dot y) <=>
\r
1743 x dot x < y dot y `] THEN
\r
1744 REWRITE_TAC[DOT_LSUB; DOT_RSUB] THEN
\r
1745 SIMP_TAC[DOT_SYM] THEN
\r
1746 ONCE_REWRITE_TAC[ GSYM REAL_SUB_LT] THEN
\r
1747 REWRITE_TAC[ REAL_ARITH ` x dot x -
\r
1749 (b dot x - b dot b) -
\r
1750 (x dot x - a dot x - (a dot x - a dot a)) =
\r
1751 &2 * (a dot x - b dot x) + b dot b - a dot a`] THEN
\r
1752 REWRITE_TAC[GSYM DOT_LSUB; GSYM DOT_RMUL] THEN
\r
1753 REWRITE_TAC[DOT_SUB_ADD; VECTOR_ARITH `(b - a) dot (b + a) =
\r
1754 ( -- ( a - b) ) dot ( a + b) `] THEN
\r
1755 REWRITE_TAC[VECTOR_ARITH ` (a - b) dot &2 % x + --(a - b) dot (a + b) =
\r
1756 (a-b) dot ( &2 % x - (a+b))`] THEN
\r
1757 ASM_REWRITE_TAC[REAL_ARITH ` a - &0 = a` ]);;
\r
1760 let OR_IMP_EX = MESON[]` ! a b c. a \/ b ==> c <=> (a ==> c) /\ ( b ==> c)` ;;
\r
1763 let HALF_PLANE_CONV = prove(`! a b:real^N. convex { x| x | dist(x,a) < dist (x,b) }`,
\r
1764 REWRITE_TAC[DIST_LT_HALF_PLANE; convex; IN_ELIM_THM] THEN
\r
1765 REWRITE_TAC[VECTOR_ARITH ` &2 % (u % x + v % y) - (a + b)
\r
1766 = u % ( &2 % x ) + v % ( &2 % y ) - &1 % (a + b )`] THEN
\r
1767 ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN SIMP_TAC[] THEN
\r
1768 REWRITE_TAC[VECTOR_ARITH ` (a - b) dot (u % &2 % x +
\r
1769 v % &2 % y - (u + v) % (a + b)) = u * (a - b) dot (&2 % x - (a + b))
\r
1770 + v * (a - b) dot (&2 % y - (a + b))`] THEN
\r
1771 REWRITE_TAC[REAL_ARITH` &0 <= u /\ &0 <= v /\ &1 = u + v <=>
\r
1772 &0 = u /\ &1 = v \/ &0 < u /\ &0 <= v /\ &1 = u + v`] THEN
\r
1774 REWRITE_TAC[OR_IMP_EX] THEN
\r
1775 ONCE_REWRITE_TAC[ EQ_SYM_EQ] THEN SIMP_TAC[] THEN
\r
1776 REWRITE_TAC[REAL_POLY_CLAUSES] THEN
\r
1777 SIMP_TAC[ REAL_ARITH ` a + &0 = a `] THEN
\r
1778 NHANH (MESON[REAL_LT_MUL]` &0 < (a - b) dot (&2 % x - (a + b)) /\
\r
1779 &0 < (a - b) dot (&2 % y - (a + b)) /\
\r
1780 &0 < u /\ l ==> &0 < u * ((a - b) dot (&2 % x - (a + b)))`) THEN
\r
1781 NHANH (MESON[REAL_ARITH` &0 < a ==> &0 <= a `; REAL_LE_MUL]`
\r
1782 &0 < (a - b) dot (&2 % y - (a + b)) /\
\r
1784 &0 <= v /\ l ==> &0 <= v * ((a - b) dot (&2 % y - (a + b)))`)
\r
1785 THEN REAL_ARITH_TAC);;
\r
1787 let HALF_PLANE_CONV_EP = REWRITE_RULE[convex; IN_ELIM_THM] HALF_PLANE_CONV;;
\r
1789 let VORONOI_CONV = prove( ` ! (s:real^A -> bool) v. convex (voronoi v s )`,
\r
1790 REWRITE_TAC[voronoi] THEN REPEAT GEN_TAC THEN
\r
1791 REWRITE_TAC[convex; IN_ELIM_THM] THEN MESON_TAC[HALF_PLANE_CONV_EP]);;
\r
1793 let CONVEX_IM_CONV2_SU = prove(`! s u v. convex s /\ u IN s /\ v IN s ==> conv {u,v} SUBSET s `,
\r
1794 REWRITE_TAC[convex; CONV_SET2] THEN SET_TAC[]);;
\r
1796 (* have not added *)
\r
1798 let U_IN_CONV2 = prove(`! u v. u IN conv {u,v} `,
\r
1799 REWRITE_TAC[ CONV_SET2; IN_ELIM_THM] THEN REPEAT GEN_TAC
\r
1800 THEN EXISTS_TAC `&1` THEN EXISTS_TAC `&0 ` THEN
\r
1801 REWRITE_TAC[VECTOR_MUL_LID; VECTOR_MUL_LZERO; VECTOR_ADD_RID] THEN
\r
1804 let UV_IN_CONV2 = prove(` ! u v. u IN conv {u,v} /\ v IN conv {u,v} `,
\r
1805 MESON_TAC[U_IN_CONV2; SET_RULE ` {u,v} = {v,u} `]);;
\r
1807 let CONVEX_AS_CONV2 = prove(` ! s. convex s ==> ( ! u v. u IN s /\ v IN s <=>
\r
1808 conv {u,v} SUBSET s )`, REWRITE_TAC[ EQ_EXPAND] THEN
\r
1809 SIMP_TAC[CONVEX_IM_CONV2_SU ] THEN MESON_TAC[SUBSET; UV_IN_CONV2]);;
\r
1816 let CONV0_SING = prove(`! x:real^A . conv0 {x} = {x} `,
\r
1817 REWRITE_TAC[conv0; FUN_EQ_THM; affsign; lin_combo] THEN
\r
1818 REWRITE_TAC[UNION_EMPTY; VSUM_SING; SUM_SING; IN_ACT_SING; sgn_gt] THEN
\r
1819 REWRITE_TAC[MESON[REAL_ARITH` &0 < &1 `]` (!w. x = w ==> &0 < f w) /\
\r
1820 f x = &1 <=> f x = &1 `] THEN
\r
1821 REWRITE_TAC[MESON[VECTOR_MUL_LID]` (?f. x' = f x % x /\ f x = &1) <=>
\r
1822 x' = x /\ (? f. f x = &1 ) `] THEN
\r
1823 MESON_TAC[prove(`!x:real^A. ? f. f x = &1`, GEN_TAC THEN EXISTS_TAC
\r
1824 `(\x:real^A. &1)` THEN MESON_TAC[])]);;
\r
1827 let NOV10' = prove(`! x y. (x = y
\r
1828 ==> (!x. y = x <=>
\r
1829 (?a b. &0 < a /\ &0 < b /\ a + b = &1 /\ x = a % y + b % y)))`,
\r
1830 REWRITE_TAC[GSYM VECTOR_ADD_RDISTRIB] THEN
\r
1831 REWRITE_TAC[MESON[VECTOR_MUL_LID]` a + b = &1 /\
\r
1832 x = (a + b) % y <=> a + b = &1 /\ x = y `] THEN
\r
1833 MESON_TAC[prove(` ?a b. &0 < a /\ &0 < b /\ a + b = &1`, REPEAT
\r
1834 (EXISTS_TAC ` &1 / &2 `) THEN REAL_ARITH_TAC)]);;
\r
1837 let CONV0_SET2 = prove(` ! x y:real^A. conv0 {x,y} = {w | ? a b. &0 < a /\ &0 < b /\ a + b = &1 /\
\r
1839 ONCE_REWRITE_TAC[ MESON[] ` (! a b. P a b ) <=> ( ! a b. a = b \/ ~( a= b)
\r
1840 ==> P a b )`] THEN
\r
1841 REWRITE_TAC[ MESON[]` a \/ b ==> c <=> ( a==> c) /\ ( b==> c)`] THEN
\r
1843 REWRITE_TAC[ SET_RULE ` {a,a} = {a}`; CONV0_SING; FUN_EQ_THM; IN_ELIM_THM] THEN
\r
1844 REWRITE_TAC[ IN_ACT_SING; NOV10'] THEN
\r
1845 REWRITE_TAC[conv0 ; sgn_gt; affsign; lin_combo] THEN
\r
1846 REWRITE_TAC[UNION_EMPTY; IN_SET2] THEN
\r
1847 ONCE_REWRITE_TAC[ MESON[]` ~(x = y) ==> (!x'. (?f. P f x') <=> l x') <=>
\r
1848 ~(x = y) ==> (!x'. (?f. ~(x=y) /\ P f x') <=> l x')`] THEN
\r
1849 REWRITE_TAC[ MESON[VSUM_DIS2; SUM_DIS2]` ~(x = y) /\
\r
1850 x' = vsum {x, y} ff /\ l /\ sum {x, y} f = &1 <=> ~(x = y) /\
\r
1851 x' = ff x + ff y /\ l /\ f x + f y = &1 `] THEN
\r
1852 REWRITE_TAC[ MESON[]` (!w. w = x \/ w = y ==> &0 < f w) <=> &0 < f x /\ &0 < f y`] THEN
\r
1853 ONCE_REWRITE_TAC[ GSYM (MESON[]` ~(x = y) ==> (!x'. (?f. P f x') <=> l x') <=>
\r
1854 ~(x = y) ==> (!x'. (?f. ~(x=y) /\ P f x') <=> l x')`)] THEN
\r
1855 REPEAT GEN_TAC THEN DISCH_TAC THEN GEN_TAC THEN
\r
1856 REWRITE_TAC[ EQ_EXPAND] THEN
\r
1857 SIMP_TAC[ MESON[]` ((?f. x' = f x % x + f y % y /\ (&0 < f x /\ &0 < f y) /\ f x + f y = &1)
\r
1858 ==> (?a b. &0 < a /\ &0 < b /\ a + b = &1 /\ x' = a % x + b % y)) `] THEN
\r
1859 STRIP_TAC THEN EXISTS_TAC ` (\(d:real^A). if d = x then (a:real) else b )` THEN
\r
1863 let CONV02_SU_CONV2 = prove(` ! u v. conv0 {u,v} SUBSET conv {u,v} `,
\r
1864 REWRITE_TAC[ CONV_SET2; CONV0_SET2] THEN
\r
1865 MP_TAC (REAL_ARITH ` ! a . &0 < a ==> &0 <= a `) THEN SET_TAC[]);;
\r
1868 let CONVEX_IM_CONV02_SU = prove(`! s u v. convex s /\ u IN s /\ v IN s ==>
\r
1869 conv0 {u, v} SUBSET s`,
\r
1870 MESON_TAC[CONV02_SU_CONV2; CONVEX_IM_CONV2_SU; SUBSET_TRANS]);;
\r
1872 let PAIR_EQ_EXPAND =
\r
1873 SET_RULE `{a,b} = {c,d} <=> a = c /\ b = d \/ a = d /\ b = c`;;
\r
1875 let IN_SET3 = SET_RULE ` x IN {a,b,c} <=> x = a \/ x = b \/ x = c `;;
\r
1877 let IN_SET4 = SET_RULE ` x IN {a,b,c,d} <=> x = a \/ x = b \/ x = c \/ x = d `;;
\r
1879 let FOUR_IN = SET_RULE `!a b c d. a IN {a,b,c,d} /\ b IN {a,b,c,d} /\c IN {a,b,c,d} /\ d IN {a,b,c,d} ` ;;
\r
1887 let DIA_OF_QUARTER = prove(`! a b q s. diagonal a b q s ==> &2 * t0 <= d3 a b /\ d3 a b
\r
1889 REWRITE_TAC[ diagonal; quarter] THEN
\r
1890 REWRITE_TAC[ SET_RULE ` {a,b} SUBSET s <=> a IN s /\ b IN s `] THEN
\r
1891 REWRITE_TAC[ SET_RULE ` {a,b} SUBSET s <=> a IN s /\ b IN s `; t0] THEN
\r
1892 MESON_TAC[PAIR_D3; MATCH_MP REAL_LE_RSQRT (REAL_ARITH ` (&2 * #1.255) pow 2 <= &8 `);
\r
1893 REAL_ARITH ` a <= b /\ b <= c ==> a <= c `]);;
\r
1895 let D3_REFL = prove(` !x. d3 x x = &0 ` , MESON_TAC[d3; DIST_REFL]);;
\r
1897 let db_t0_sq8 = MATCH_MP REAL_LT_RSQRT (REAL_ARITH ` #2.51 pow 2 < &8 `);;
\r
1899 let def_obstructed = prove(`!s x y.
\r
1900 obstructed x y s <=>
\r
1901 (?bar. bar IN barrier s /\ ~(conv0 {x, y} INTER conv bar = {}))`,
\r
1902 REWRITE_TAC[ obstructed; conv0_2] THEN REWRITE_TAC[ simp_def]);;
\r
1904 let SUB_PACKING = prove(`!sub s.
\r
1905 packing s /\ sub SUBSET s
\r
1906 ==> (!x y. x IN sub /\ y IN sub /\ ~(x = y) ==> &2 <= d3 x y)`,
\r
1907 REWRITE_TAC[ packing; GSYM d3] THEN SET_TAC[]);;
\r
1912 let SHORT_EDGES = prove(` ! a b c w. d3 c a <= &2 * t0 /\
\r
1913 d3 c b <= &2 * t0 /\
\r
1914 (!aa. aa IN {a, b, c} ==> d3 aa w <= &2 * t0)
\r
1916 x IN {a, b, c, w} /\ y IN {a, b, c, w} /\ ~({x, y} = {a, b})
\r
1917 ==> d3 x y <= &2 * t0)`,
\r
1918 REPEAT GEN_TAC THEN
\r
1919 REWRITE_TAC[ IN_SET3; IN_SET4; PAIR_EQ_EXPAND; t0] THEN
\r
1920 MESON_TAC[ D3_REFL; trg_d3_sym; REAL_ARITH ` &0 <= &2 * #1.255`]);;
\r
1924 (* == CARD ASSERTIONN == *)
\r
1925 (* changing truong *)
\r
1927 let OBS_SYM = prove(` ! a b s. obstructed a b s <=> obstructed b a s `,
\r
1928 REWRITE_TAC[ def_obstructed] THEN SIMP_TAC[ SET_RULE` {a,b} = {b,a}`]);;
\r
1931 let OBS_IMP_NOT_IN_VC = prove(`!x w s. obstructed x w s ==> ~(x IN VC w s \/ w IN VC x s)`,
\r
1932 REWRITE_TAC[VC; lambda_x; IN_ELIM_THM] THEN MESON_TAC[ OBS_SYM]);;
\r
1935 let IN_Q_IMP_BAR =
\r
1936 prove(` {v0, v1, v2, w} IN Q_SYS s ==> {v0,v1,v2} IN barrier s `,
\r
1937 REWRITE_TAC[ barrier; SET_RULE` {a,b,c} UNION {d} = {a,b,c,d} `; IN_ELIM_THM]
\r
1938 THEN MESON_TAC[]);;
\r
1941 let v_near2t0_v = MESON[near2t0; t0; DIST_REFL; SET_RULE ` x IN { x | P x} <=> P x ` ;
\r
1942 REAL_ARITH ` &0 < &2 * #1.255 `] ` w IN s ==> w IN near2t0 w s `;;
\r
1945 let in_VC = prove(
\r
1948 dist (w,x) < &2 /\
\r
1949 (!w'. s w' /\ ~(w' = w) ==> dist (x,w) < dist (x,w')) /\
\r
1951 ==> x IN VC w s`, REWRITE_TAC[ VC; lambda_x ; d3; IN_ELIM_THM] THEN
\r
1952 MESON_TAC[ DIST_SYM; SET_RULE ` i IN x <=> x i `]);;
\r
1955 let MEETING_CONDITION = prove(` ! x y v1 v2 v3. ~(conv0 {x, y} INTER conv_trg {v1, v2, v3} = {}) /\ dist (x,y) < t0
\r
1956 ==> ~(normball x #1.255 INTER conv {v1, v2, v3} = {})`,
\r
1957 REWRITE_TAC[ GSYM conv0_2; simp_def] THEN
\r
1958 REWRITE_TAC[ SET_RULE ` ~( a INTER b = {} ) <=> (? d. d IN a /\ d IN b )`;
\r
1959 IN_ELIM_THM] THEN
\r
1960 NHANH (MESON[ VECTOR_ARITH ` x = &1 % x ` ]` d = t % x + (&1 - t) % y ==>
\r
1961 x = &1 % x `) THEN
\r
1962 NHANH (VECTOR_ARITH ` d = t % x + (&1 - t) % y /\ x = &1 % x
\r
1963 ==> d - x = (t - &1) % ( x - y)`) THEN
\r
1964 NHANH ( MESON[NORM_MUL]` d - x = (t - &1) % (x - y) ==> norm ( d - x ) =
\r
1965 abs ( t- &1 ) * norm ( x-y)`) THEN
\r
1966 REWRITE_TAC[ GSYM dist] THEN
\r
1967 NHANH (REAL_ARITH `&0 < t /\ t < &1 /\ aa ==> abs (t - &1) < &1`) THEN
\r
1968 NHANH (MESON[DIST_POS_LE]` dist (d,x) = abs (t - &1) * dist (x,y) ==> &0 <= dist(x,y)`) THEN
\r
1970 REWRITE_TAC[ REAL_ARITH ` abs (t - &1) < &1 <=> &0 < &1 - abs (t - &1) `] THEN
\r
1971 NHANH (MESON[REAL_LE_MUL_EQ] ` &0 <= dist (x,y) /\
\r
1972 &0 < &1 - abs (t - &1) ==> &0 <= dist (x,y) * (&1 - abs (t - &1))`) THEN
\r
1973 REWRITE_TAC[ REAL_ARITH ` a * ( b - c ) = a * b - a * c `] THEN
\r
1974 REWRITE_TAC[ REAL_ARITH ` &0 <= a - b <=> b <= a `] THEN
\r
1975 NHANH (REAL_ARITH ` dist (d,x) = abs (t - &1) * dist (x,y) /\
\r
1976 (&0 <= dist (x,y) /\ &0 < &1 - abs (t - &1)) /\
\r
1977 dist (x,y) * abs (t - &1) <= dist (x,y) * &1
\r
1978 ==> dist(d,x) <= dist(x,y)`) THEN
\r
1979 NGOAC THEN NHANH (MESON[]`(? d . ( ? t. PP t d /\ dist (d,x) <= dist (x,y)) /\ aa d ) ==> (? d. dist (d,x)
\r
1980 <= dist (x,y) /\ aa d ) `) THEN
\r
1981 PHA THEN REPEAT GEN_TAC THEN
\r
1982 MATCH_MP_TAC (MESON[] ` (b /\ c ==> d) ==> ( a/\ b/\ c )==> d `) THEN
\r
1983 REWRITE_TAC[normball; IN_ELIM_THM; GSYM t0] THEN
\r
1984 REWRITE_TAC[ MESON[]` (? a . P a ) /\ aa <=> (? a. aa /\ P a ) `] THEN
\r
1985 MESON_TAC[ REAL_ARITH ` a < b /\ c <= a ==> c < b `]);;
\r
1989 let VC_DISJOINT = prove ( `! s a b. ( ~( a = b ) ==> VC a s INTER VC b s = {}) /\
\r
1990 VC a s INTER VC_INFI s = {} `,
\r
1991 REWRITE_TAC[ VC_INFI; SET_RULE ` VC a s INTER {z | !x. ~(z IN VC x s)} = {} `] THEN
\r
1992 REWRITE_TAC[ VC; lambda_x ] THEN
\r
1993 REWRITE_TAC[ SET_RULE` a INTER b = {} <=> (! x. ~( x IN a /\ x IN b ))`] THEN
\r
1994 REWRITE_TAC[ SET_RULE ` x IN { x | p x } <=> p x `] THEN
\r
1995 REWRITE_TAC[ MESON[] ` ! a P. a ==> (!x. ~P x) <=> a ==> (!x. ~a \/ ~P x) `] THEN
\r
1996 REWRITE_TAC[ MESON[] ` a = b \/
\r
1997 ~(((a IN s /\ d3 a x < &2 /\ ~obstructed a x s) /\
\r
1998 (!w. (w IN s /\ d3 w x < &2 /\ ~obstructed w x s) /\ ~(w = a)
\r
1999 ==> d3 x a < d3 x w)) /\
\r
2000 (b IN s /\ d3 b x < &2 /\ ~obstructed b x s) /\
\r
2001 (!w. (w IN s /\ d3 w x < &2 /\ ~obstructed w x s) /\ ~(w = b)
\r
2002 ==> d3 x b < d3 x w)) <=>
\r
2004 ((a IN s /\ d3 a x < &2 /\ ~obstructed a x s) /\
\r
2005 (!w. (w IN s /\ d3 w x < &2 /\ ~obstructed w x s) /\ ~(w = a)
\r
2006 ==> d3 x a < d3 x w)) /\
\r
2007 (b IN s /\ d3 b x < &2 /\ ~obstructed b x s) /\
\r
2008 (!w. (w IN s /\ d3 w x < &2 /\ ~obstructed w x s) /\ ~(w = b)
\r
2009 ==> d3 x b < d3 x w)) `] THEN PHA THEN
\r
2010 MESON_TAC[ REAL_ARITH ` ! a b. ~( a < b /\ b < a ) `]);;
\r
2013 let DIAGONAL_STRICT_QUA = prove(` !a b q s.
\r
2014 a IN q /\ b IN q /\ &2 * t0 < d3 a b /\ strict_qua q s
\r
2015 ==> diagonal a b q s`,
\r
2016 REWRITE_TAC[ SET_RULE ` a IN q /\ b IN q /\ l ==> aa /\ {a,b} SUBSET q /\ bb
\r
2017 <=> a IN q /\ b IN q /\ l ==> aa /\ bb `] THEN
\r
2018 REWRITE_TAC[ MESON[]` a /\ b/\ c /\ d /\ e ==> d /\ f <=> a /\ b/\ c /\ d /\ e ==> f `] THEN
\r
2019 MESON_TAC[strict_qua; DIAGONAL_QUA]);;
\r
2023 let DIAGONAL_BARRIER = prove(` ! s v1 v2 bar .v1 IN bar /\ v2 IN bar /\ bar IN barrier s /\ &2 * t0 < d3 v1 v2
\r
2024 ==> (? w. diagonal v1 v2 ( w INSERT bar ) s )`,
\r
2025 REWRITE_TAC[ barrier; IN_ELIM_THM] THEN
\r
2026 PHA THEN REWRITE_TAC[ MESON[] ` a /\ b /\ (? u v w. P u v w ) /\ d <=>
\r
2027 (? u v w. P u v w /\ a /\ b /\ d ) `] THEN
\r
2029 REWRITE_TAC[ MESON[]` (? a b c. P a b c) /\ l <=> (?a b c. P a b c /\ l)`] THEN
\r
2030 REWRITE_TAC[ quasi_tri; t0] THEN
\r
2031 NHANH ( REAL_ARITH ` &2 * #1.255 < a ==> ~( a = &0 ) `) THEN
\r
2032 REWRITE_TAC[d3; DIST_EQ_0] THEN
\r
2034 PURE_ONCE_REWRITE_TAC[ MESON[]` P {a,b,c} /\ bar = {a,b,c} <=> P bar /\ bar
\r
2035 = {a,b,c} `] THEN
\r
2036 REWRITE_TAC[quasi_tri; REAL_ARITH ` a <= b <=> ~( b < a ) `] THEN PHA THEN
\r
2037 REWRITE_TAC[ MESON[]` ~((!x y.
\r
2038 x IN bar /\ y IN bar /\ ~(x = y) ==> ~(&2 * #1.255 < dist (x,y))) /\
\r
2042 &2 * #1.255 < dist (v1,v2) /\
\r
2043 ~(v1 = v2))`] THEN
\r
2044 NHANH (CUTHE2 CASES_OF_Q_SYS) THEN
\r
2045 REWRITE_TAC[ MESON[]` (? a . P a ) /\ l <=> (? a. P a /\ l ) `] THEN
\r
2047 PURE_ONCE_REWRITE_TAC[ MESON[]` P bar /\ bar = s /\ l <=> P s /\ bar = s /\ l`] THEN
\r
2048 NHANH (MESON[QUA_TET_IMPLY_QUA_TRI] ` quasi_reg_tet ({v0, v1, v2} UNION {v4}) s ==>
\r
2049 quasi_tri {v0, v1, v2} s`) THEN
\r
2050 REWRITE_TAC[ quasi_tri] THEN
\r
2051 REWRITE_TAC[d3;t0; REAL_ARITH ` a <= &2 * #1.255 <=> ~(&2 * #1.255 < a ) `] THEN PHA THEN
\r
2052 REWRITE_TAC[ MESON[]` ~((!x y.
\r
2053 x IN {v1', v2', v3} /\ y IN {v1', v2', v3} /\ ~(x = y)
\r
2054 ==> ~(&2 * #1.255 < dist (x,y))) /\
\r
2055 bar = {v1', v2', v3} /\
\r
2058 &2 * #1.255 < dist (v1,v2) /\
\r
2059 ~(v1 = v2))`] THEN
\r
2060 REWRITE_TAC[ GSYM d3; GSYM t0] THEN
\r
2061 REWRITE_TAC[ MESON[]` strict_qua ({v1', v2', v3} UNION {v4}) s /\ bar = {v1', v2', v3} /\ l <=>
\r
2062 strict_qua (bar UNION {v4}) s /\ bar = {v1', v2', v3} /\ l`] THEN
\r
2063 ONCE_REWRITE_TAC[ SET_RULE ` bar UNION {v4} = v4 INSERT bar `] THEN
\r
2064 MESON_TAC[ DIAGONAL_STRICT_QUA; SET_RULE ` x IN bar ==> x IN ( a INSERT bar)`]);;
\r
2067 (* ======= end simplizee.ml =========== *)
\r
2069 (* ======= im_le_82.ml ================ *)
\r
2071 let quasi_tri_case = prove( ` ! s x y. (?v1 v2 v3.
\r
2072 ~(x IN {v1, v2, v3}) /\
\r
2073 quasi_tri {v1, v2, v3} s /\
\r
2074 ~(conv0 {x, y} INTER conv_trg {v1, v2, v3} = {}) /\
\r
2078 ~(v1 = v2 \/ v2 = v3 \/ v3 = v1) /\
\r
2079 dist (v1,v2) <= #2.51 /\
\r
2080 dist (v2,v3) <= #2.51 /\
\r
2081 dist (v3,v1) < sqrt (&8) /\
\r
2082 {v1, v2, v3} SUBSET s /\
\r
2083 ~(x IN {v1, v2, v3}) /\
\r
2084 ~(conv0 {x, y} INTER conv_trg {v1, v2, v3} = {}) /\
\r
2085 dist (x,y) < t0)`,
\r
2086 REWRITE_TAC[ quasi_tri; set_3elements] THEN PHA THEN
\r
2087 REWRITE_TAC[ d3; MESON[t0; REAL_ARITH ` &2 * #1.255 = #2.51 `] ` &2 * t0 = #2.51 `] THEN
\r
2088 REWRITE_TAC[ MESON[]` a /\ b /\ c /\ d /\e /\ f <=> a /\ b /\ c /\ (d /\e) /\ f`] THEN
\r
2089 ONCE_REWRITE_TAC[ SET_RULE ` ~(v1 = v2 \/ v2 = v3 \/ v3 = v1) /\
\r
2091 x IN {v1, v2, v3} /\ y IN {v1, v2, v3} /\ ~(x = y)
\r
2092 ==> dist (x,y) <= #2.51)
\r
2093 <=> ~(v1 = v2 \/ v2 = v3 \/ v3 = v1) /\
\r
2095 x IN {v1, v2, v3} /\ y IN {v1, v2, v3} /\ ~(x = y)
\r
2096 ==> dist (x,y) <= #2.51) /\
\r
2097 dist (v1,v2) <= #2.51 /\
\r
2098 dist (v2,v3) <= #2.51 /\
\r
2099 dist (v3,v1) <= #2.51 `] THEN
\r
2100 ONCE_REWRITE_TAC[MESON[ REAL_ARITH ` &2 * #1.255 = #2.51 `; MATCH_MP REAL_LT_RSQRT (REAL_ARITH `(&2 * #1.255) pow 2 < &8`);
\r
2101 REAL_ARITH` a <= b /\ b < c ==> a < c `] `
\r
2102 a /\ dist (v3,v1) <= #2.51 <=> a /\ dist (v3,v1) < sqrt ( &8 ) /\ dist (v3,v1) <= #2.51`] THEN
\r
2107 (* ----------- have added to database_more --------------*)
\r
2111 let OCT23 = prove(`! s v1 v2 v3 v4.
\r
2112 {v1, v2, v3} UNION {v4} IN Q_SYS s
\r
2114 ~(v1 = v2 \/ v2 = v3 \/ v3 = v1) /\
\r
2115 {v1, v2, v3} SUBSET s` ,
\r
2116 REPEAT GEN_TAC THEN MP_TAC (prove(`! q s. q IN Q_SYS s ==> quasi_reg_tet q s \/ strict_qua q s \/
\r
2118 (q = {v, v1, v2, v3} \/ q = {v, v1, v3, v4}) /\
\r
2119 interior_pos v v1 v3 v2 v4 s /\
\r
2120 anchor_points v1 v3 s = {v, v2, v4} /\
\r
2121 anchor_points v2 v4 s = {v, v1, v3})`,
\r
2122 REWRITE_TAC[ Q_SYS; IN_ELIM_THM] THEN MESON_TAC[strict_qua_in_oct] )) THEN
\r
2123 MATCH_MP_TAC (MESON[]`((!q s. q IN Q_SYS s ==> R q s)
\r
2124 ==> R ({v1, v2, v3} UNION {v4}) s
\r
2125 ==> last v1 v2 v3 s)
\r
2126 ==> (!q s. q IN Q_SYS s ==> R q s)
\r
2127 ==> {v1, v2, v3} UNION {v4} IN Q_SYS s
\r
2128 ==> last v1 v2 v3 s`) THEN
\r
2130 REWRITE_TAC[ quasi_reg_tet; strict_qua ] THEN
\r
2131 PHA THEN KHANANG THEN
\r
2132 REWRITE_TAC[ quarter] THEN
\r
2134 REWRITE_TAC[ MESON[]` packing s /\simplex ({v1, v2, v3} UNION {v4}) s /\ last <=>
\r
2135 simplex ({v1, v2, v3} UNION {v4}) s /\ packing s /\ last`] THEN
\r
2136 REWRITE_TAC[ SET_RULE ` {v1, v2, v3} UNION {v4} = { v1, v2, v3, v4} `] THEN
\r
2137 MP_TAC (MESON[ def_simplex; SET_RULE ` {a, b, c, d} SUBSET s ==> {a, b, c} SUBSET s `] `
\r
2138 simplex {v1, v2, v3, v4} s ==> packing s /\ ~(v1 = v2 \/ v2 = v3 \/ v3 = v1) /\ {v1, v2, v3} SUBSET s `) THEN
\r
2139 MATCH_MP_TAC (MESON[]` (cc ==> last)
\r
2141 ==> aa /\ la1 \/ aa /\ la2 \/ cc
\r
2143 REWRITE_TAC[ MESON[]` a = b /\ (aa /\ bb b s) /\ last <=> bb a s /\ aa /\ a = b /\ last`] THEN
\r
2144 REWRITE_TAC[def_simplex] THEN
\r
2145 ONCE_REWRITE_TAC[ MESON[simplex_interior_pos]` interior_pos v v1 v3 v2 v4 s <=> interior_pos v v1 v3 v2 v4 s
\r
2146 /\ simplex {v, v1, v3, v2} s /\
\r
2147 simplex {v, v1, v3, v4} s /\
\r
2148 simplex {v, v2, v4, v1} s /\
\r
2149 simplex {v, v2, v4, v3} s `] THEN PHA THEN
\r
2150 REWRITE_TAC[ MESON[]` {v1, v2, v3, v4} = {v, v1', v2', v3'} /\
\r
2151 aa /\ simplex {v, v1', v3', v2'} s /\ ss
\r
2152 <=> ( simplex {v, v1', v3', v2'} s /\ {v1, v2, v3, v4} = {v, v1', v2', v3'}) /\ aa /\ ss `] THEN
\r
2153 REWRITE_TAC[ MESON[SET_RULE ` {v, v1, v2 , v3} = {v, v1, v3, v2} ` ] `
\r
2154 (simplex {v, v1', v3', v2'} s /\ {v1, v2, v3, v4} = {v, v1', v2', v3'}) /\ ff <=>
\r
2155 simplex {v1, v2, v3, v4} s /\ {v1, v2, v3, v4} = {v, v1', v2', v3'} /\ ff`] THEN
\r
2156 MESON_TAC[ def_simplex; SET_RULE ` {v1, v2, v3, v4} SUBSET s ==> {v1, v2, v3} SUBSET s`]);;
\r
2159 (* ================== *)
\r
2162 let OCT24 = prove(`! s x y. (?v1 v2 v3.
\r
2163 ~(x IN {v1, v2, v3}) /\
\r
2164 (?v4. (!vv1 vv2 vv3.
\r
2165 {vv1, vv2, vv3} = {v1, v2, v3} ==> ~(#2.51 < dist (vv3,vv1))) /\
\r
2166 {v1, v2, v3} UNION {v4} IN Q_SYS s) /\
\r
2167 ~(conv0 {x, y} INTER conv_trg {v1, v2, v3} = {}) /\
\r
2168 dist (x,y) < t0) ==>
\r
2171 ~(v1 = v2 \/ v2 = v3 \/ v3 = v1) /\
\r
2172 dist (v1,v2) <= #2.51 /\
\r
2173 dist (v2,v3) <= #2.51 /\
\r
2174 dist (v3,v1) < sqrt (&8) /\
\r
2175 {v1, v2, v3} SUBSET s /\
\r
2176 ~(x IN {v1, v2, v3}) /\
\r
2177 ~(conv0 {x, y} INTER conv_trg {v1, v2, v3} = {}) /\
\r
2178 dist (x,y) < t0)`,
\r
2179 ONCE_REWRITE_TAC[ MESON[OCT23] ` {v1, v2, v3} UNION {v4} IN Q_SYS s <=>
\r
2180 {v1, v2, v3} UNION {v4} IN Q_SYS s /\ packing s /\
\r
2181 ~(v1 = v2 \/ v2 = v3 \/ v3 = v1) /\
\r
2182 {v1, v2, v3} SUBSET s `] THEN
\r
2183 ONCE_REWRITE_TAC[ MESON[ SET_RULE` {v1, v3 , v2 } = { v1, v2 , v3} /\ { v2, v1, v3 } = { v1, v2, v3 }`]`
\r
2185 {vv1, vv2, vv3} = {v1, v2, v3} ==> ~(#2.51 < dist (vv3,vv1)))
\r
2186 <=> (!vv1 vv2 vv3.
\r
2187 {vv1, vv2, vv3} = {v1, v2, v3} ==> ~(#2.51 < dist (vv3,vv1))) /\ ~(#2.51 < dist (v3,v1)) /\
\r
2188 ~(#2.51 < dist (v2,v1)) /\
\r
2189 ~(#2.51 < dist (v3,v2)) `] THEN
\r
2190 REWRITE_TAC[ REAL_ARITH ` ~( a < b ) <=> b <= a`] THEN SIMP_TAC[ DIST_SYM] THEN
\r
2191 MESON_TAC[MESON[ MATCH_MP REAL_LT_RSQRT (REAL_ARITH `(&2 * #1.255) pow 2 < &8`);
\r
2192 REAL_ARITH ` &2 * #1.255 = #2.51 /\ ( a <= b /\ b < c ==> a < c ) `]` dist (v1,v3) <= #2.51
\r
2193 <=> dist (v1,v3) <= #2.51 /\ dist (v1,v3) < sqrt (&8) `]);;
\r
2197 (* ============= *)
\r
2200 let quasi_reg_tet_case = prove (`! s x y. (?v1 v2 v3.
\r
2202 {vv1, vv2, vv3} = {v1, v2, v3} /\
\r
2203 #2.51 < dist (vv3,vv1) /\
\r
2204 {v1, v2, v3} UNION {v4} IN Q_SYS s /\
\r
2205 quasi_reg_tet ({v1, v2, v3} UNION {v4}) s) /\
\r
2206 ~(x IN {v1, v2, v3}) /\
\r
2207 ~(conv0 {x, y} INTER conv_trg {v1, v2, v3} = {}))
\r
2210 ~(v1 = v2 \/ v2 = v3 \/ v3 = v1) /\
\r
2211 dist (v1,v2) <= #2.51 /\
\r
2212 dist (v2,v3) <= #2.51 /\
\r
2213 dist (v3,v1) < sqrt (&8) /\
\r
2214 {v1, v2, v3} SUBSET s /\
\r
2215 ~(x IN {v1, v2, v3}) /\
\r
2216 ~(conv0 {x, y} INTER conv_trg {v1, v2, v3} = {}))`,
\r
2217 REWRITE_TAC[quasi_reg_tet; SET_RULE ` {v1, v2, v3} UNION {v4} = {v1, v2, v3, v4} `; def_simplex] THEN
\r
2218 REWRITE_TAC[ MESON[]` (packing s /\
\r
2219 {v1, v2, v3, v4} SUBSET s /\
\r
2220 ~(v1 = v2 \/ v1 = v3 \/ v1 = v4 \/ v2 = v3 \/ v2 = v4 \/ v3 = v4)) /\ a <=>
\r
2221 a /\ ~(v1 = v2 \/ v1 = v3 \/ v1 = v4 \/ v2 = v3 \/ v2 = v4 \/ v3 = v4) /\ (packing s /\
\r
2222 {v1, v2, v3, v4} SUBSET s
\r
2224 ONCE_REWRITE_TAC[ ATTACH (MESON[ SET_RULE` v1 IN {v1, v2, v3, v4} /\ v2 IN { v1, v2, v3, v4} /\ v3 IN { v1, v2, v3, v4} `] `
\r
2226 v IN {v1, v2, v3, v4} /\ w IN {v1, v2, v3, v4} /\ ~(v = w)
\r
2227 ==> d3 v w <= &2 * t0) /\
\r
2228 ~(v1 = v2 \/ v1 = v3 \/ v1 = v4 \/ v2 = v3 \/ v2 = v4 \/ v3 = v4) /\last
\r
2229 ==> d3 v1 v2 <= &2 * t0 /\ d3 v2 v3 <= &2 * t0 /\ d3 v3 v1 <= &2 * t0 `)] THEN
\r
2230 REWRITE_TAC[ t0; GSYM d3; REAL_ARITH ` &2 * #1.255 = #2.51 `] THEN
\r
2231 ONCE_REWRITE_TAC[ ATTACH (MESON[ MATCH_MP REAL_LT_RSQRT (REAL_ARITH `(&2 * #1.255) pow 2 < &8`) ; REAL_ARITH ` &2 * #1.255 = #2.51 /\ ( a <= b /\ b < c ==> a < c ) `]
\r
2232 ` d3 v1 v2 <= #2.51 /\
\r
2233 d3 v2 v3 <= #2.51 /\
\r
2234 d3 v3 v1 <= #2.51 ==> d3 v3 v1 < sqrt (&8) `)] THEN
\r
2235 MESON_TAC[ SET_RULE ` {v1, v2, v3, v4} SUBSET s ==> {v1, v2, v3} SUBSET s`]);;
\r
2237 let DIST_PAIR_LEMMA = prove
\r
2238 (`{a,b} = {c,d} ==> dist(a,b) = dist(c,d)`,
\r
2239 REWRITE_TAC[PAIR_EQ_EXPAND] THEN MESON_TAC[DIST_SYM]);;
\r
2241 let OTHER_LEMMA = prove
\r
2242 (`!a:real^3 b c d.
\r
2244 v IN {a, b, c, d} /\
\r
2245 w IN {a, b, c, d} /\
\r
2246 &2 * t0 <= d3 v w /\
\r
2247 d3 v w <= sqrt (&8) /\
\r
2249 x IN {a, b, c, d} /\
\r
2250 y IN {a, b, c, d} /\
\r
2251 ~(x = v /\ y = w \/ x = w /\ y = v)
\r
2252 ==> d3 x y <= &2 * t0)) /\
\r
2254 x IN {a, b, c, d} /\
\r
2255 y IN {a, b, c, d} /\
\r
2256 &2 * t0 < d3 x y /\
\r
2257 d3 x y < sqrt (&8)) /\
\r
2259 ==> &2 * t0 < d3 d b /\
\r
2260 d3 d b < sqrt (&8) /\
\r
2262 x IN {a, b, c, d} /\
\r
2263 y IN {a, b, c, d} /\
\r
2264 ~({x, y} = {d, b})
\r
2265 ==> d3 x y <= &2 * t0)`, REWRITE_TAC [d3] THEN
\r
2266 REPEAT GEN_TAC THEN REWRITE_TAC[t0; CONJ_ASSOC] THEN
\r
2267 DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
\r
2268 REWRITE_TAC[GSYM CONJ_ASSOC; GSYM PAIR_EQ_EXPAND] THEN
\r
2269 REWRITE_TAC[LEFT_AND_EXISTS_THM; LEFT_IMP_EXISTS_THM] THEN
\r
2270 MAP_EVERY X_GEN_TAC [`v:real^3`; `w:real^3`] THEN
\r
2271 DISCH_THEN(CONJUNCTS_THEN2 STRIP_ASSUME_TAC MP_TAC) THEN
\r
2272 ASM_CASES_TAC `{v,w} = {d,b:real^3}` THENL
\r
2273 [FIRST_ASSUM(SUBST_ALL_TAC o MATCH_MP DIST_PAIR_LEMMA) THEN
\r
2274 FIRST_X_ASSUM SUBST_ALL_TAC;
\r
2275 FIRST_X_ASSUM(MP_TAC o SPECL [`d:real^3`; `b:real^3`]) THEN
\r
2276 ASM_REWRITE_TAC[GSYM REAL_NOT_LT; IN_INSERT]] THEN
\r
2277 ASM_REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
\r
2278 MAP_EVERY X_GEN_TAC [`x:real^3`; `y:real^3`] THEN STRIP_TAC THEN
\r
2279 FIRST_X_ASSUM(MP_TAC o SPECL [`x:real^3`; `y:real^3`]) THEN
\r
2280 ASM_REWRITE_TAC[GSYM REAL_NOT_LT] THEN ASM_MESON_TAC[DIST_PAIR_LEMMA]);;
\r
2283 (* ======OCT 23====== *)
\r
2285 let hard_case = prove(`! s x y. (?v1 v2 v3.
\r
2287 {vv1, vv2, vv3} = {v1, v2, v3} /\
\r
2288 #2.51 < dist (vv3,vv1) /\
\r
2289 {v1, v2, v3} UNION {v4} IN Q_SYS s /\
\r
2290 strict_qua ({v1, v2, v3} UNION {v4}) s) /\
\r
2291 ~(x IN {v1, v2, v3}) /\
\r
2292 ~(conv0 {x, y} INTER conv_trg {v1, v2, v3} = {}))
\r
2295 ~(v1 = v2 \/ v2 = v3 \/ v3 = v1) /\
\r
2296 dist (v1,v2) <= #2.51 /\
\r
2297 dist (v2,v3) <= #2.51 /\
\r
2298 dist (v3,v1) < sqrt (&8) /\
\r
2299 {v1, v2, v3} SUBSET s /\
\r
2300 ~(x IN {v1, v2, v3}) /\
\r
2301 ~(conv0 {x, y} INTER conv_trg {v1, v2, v3} = {}))`,
\r
2302 REWRITE_TAC[ SET_RULE ` {v1, v2, v3} UNION { v4} = { v1, v2, v3 , v4} `;
\r
2304 REWRITE_TAC [ REAL_ARITH ` #2.51 = &2 * #1.255`] THEN
\r
2305 PURE_ONCE_REWRITE_TAC[ MESON[]` (?v4 v1 v2 v3. P v4 v1 v2 v3) <=> (?a b c d. P a b c d)`] THEN
\r
2306 ONCE_REWRITE_TAC[MESON[SET_RULE ` {b, c, d} = {v1, v2, v3} ==> {v1, v2, v3, a} = { a, b, c ,d }`]
\r
2307 ` (? a b c d. {b, c, d} = {v1, v2, v3} /\ P a b c d v1 v2 v3 {v1, v2, v3, a} )
\r
2308 <=> (? a b c d. {b, c, d} = {v1, v2, v3} /\ P a b c d v1 v2 v3 { a, b, c ,d })`] THEN
\r
2309 REWRITE_TAC[quarter] THEN
\r
2310 REWRITE_TAC[quarter;def_simplex] THEN PHA THEN
\r
2311 REWRITE_TAC[MESON[]`&2 * #1.255 < dist (d,b) /\ a <=> a /\ &2 * #1.255 < dist (d,b)`] THEN PHA THEN
\r
2312 REWRITE_TAC[ GSYM t0; GSYM d3] THEN
\r
2313 REWRITE_TAC[ SET_RULE ` ~({a, b} = {c, d}) <=> ~(a = c /\ b = d \/ a = d /\ b = c)`] THEN
\r
2314 NHANH (MATCH_MP (MESON[]` (! a b c d. P a b c d ) ==> P a b c d`) OTHER_LEMMA ) THEN PHA THEN
\r
2315 PURE_ONCE_REWRITE_TAC[ MESON[]` ~(a = b \/ a = c \/ a = d \/ b = c \/ b = d \/ c = d)
\r
2316 /\ aa <=> aa /\ ~(a = b \/ a = c \/ a = d \/ b = c \/ b = d \/ c = d)`] THEN PHA THEN
\r
2317 NHANH (SET_RULE ` ~(a = b \/ a = c \/ a = d \/ b = c \/ b = d \/ c = d)
\r
2318 ==> ~({b, c} = {d,b} ) /\ ~({c,d} = {d,b})`) THEN
\r
2319 NHANH (SET_RULE` ~({b, c} = {d, b}) /\
\r
2320 ~({c, d} = {d, b}) ==> b IN {a, b, c, d} /\
\r
2321 c IN {a, b, c, d} /\ d IN {a, b, c, d} `) THEN PHA THEN
\r
2322 NHANH (MESON[]` (!x y.
\r
2323 x IN {a, b, c, d} /\ y IN {a, b, c, d} /\ ~({x, y} = {d, b})
\r
2324 ==> d3 x y <= &2 * t0) /\
\r
2326 ~({b, c} = {d, b}) /\
\r
2327 ~({c, d} = {d, b}) /\
\r
2328 b IN {a, b, c, d} /\
\r
2329 c IN {a, b, c, d} /\
\r
2331 ==> d3 b c <= &2 * t0 /\ d3 c d <= &2 * t0`) THEN
\r
2332 REWRITE_TAC[ MESON[]`{b, c, d} = {v1, v2, v3} /\ a <=> a /\ {b, c, d} = {v1, v2, v3} `] THEN
\r
2333 PHA THEN REWRITE_TAC[ MESON[]`{a, b, c, d} SUBSET s /\ aa <=> aa /\ {a, b, c, d} SUBSET s`] THEN
\r
2334 REWRITE_TAC[ MESON[]` ~(a = b \/ a = c \/ a = d \/ b = c \/ b = d \/ c = d) /\ aa
\r
2335 <=> aa /\ ~(a = b \/ a = c \/ a = d \/ b = c \/ b = d \/ c = d) `] THEN
\r
2336 REWRITE_TAC[ MESON[]` (?a b c d. aa a b c d /\ packing s /\ P a b c d )
\r
2337 <=> packing s /\ (? a b c d. aa a b c d /\ P a b c d)`] THEN
\r
2338 SIMP_TAC[] THEN PHA THEN
\r
2339 REWRITE_TAC[ MESON[]` d3 d b < sqrt (&8)/\ a<=> a /\ d3 d b < sqrt (&8)`] THEN
\r
2340 PHA THEN NHANH (SET_RULE ` {b, c, d} = {v1, v2, v3} /\
\r
2341 ~(a = b \/ a = c \/ a = d \/ b = c \/ b = d \/ c = d) /\
\r
2342 {a, b, c, d} SUBSET s /\ last
\r
2343 ==> {v1, v2, v3} SUBSET s /\ ~( b = c \/ c= d \/ d= b )`) THEN PHA THEN
\r
2344 REWRITE_TAC[ MESON[]` d3 b c <= &2 * t0 /\
\r
2345 d3 c d <= &2 * t0 /\ a <=> a /\ d3 b c <= &2 * t0 /\
\r
2346 d3 c d <= &2 * t0 `] THEN
\r
2352 let OCTOR23 = prove(`(?v1 v2 v3.
\r
2353 ~(x IN {v1, v2, v3}) /\
\r
2355 {vv1, vv2, vv3} = {v1, v2, v3} /\
\r
2356 #2.51 < dist (vv3,vv1) /\
\r
2357 {v1, v2, v3} UNION {v4} IN Q_SYS s) /\
\r
2358 ~(conv0 {x, y} INTER conv_trg {v1, v2, v3} = {}) /\
\r
2362 ~(v1 = v2 \/ v2 = v3 \/ v3 = v1) /\
\r
2363 dist (v1,v2) <= #2.51 /\
\r
2364 dist (v2,v3) <= #2.51 /\
\r
2365 dist (v3,v1) < sqrt (&8) /\
\r
2366 {v1, v2, v3} SUBSET s /\
\r
2367 ~(x IN {v1, v2, v3}) /\
\r
2368 ~(conv0 {x, y} INTER conv_trg {v1, v2, v3} = {}) /\
\r
2369 dist (x,y) < t0)`,
\r
2370 REWRITE_TAC[ MESON[]` a /\ (?v4 vv1 vv2 vv3.
\r
2371 {vv1, vv2, vv3} = {v1, v2, v3} /\
\r
2372 #2.51 < dist (vv3,vv1) /\
\r
2373 {v1, v2, v3} UNION {v4} IN Q_SYS s) /\ b <=> (?v4 vv1 vv2 vv3.
\r
2374 {vv1, vv2, vv3} = {v1, v2, v3} /\
\r
2375 #2.51 < dist (vv3,vv1) /\
\r
2376 {v1, v2, v3} UNION {v4} IN Q_SYS s) /\ a /\ b `] THEN
\r
2377 NGOAC THEN REWRITE_TAC[ MESON[]` (( a /\ ~(x IN {v1, v2, v3})) /\
\r
2378 ~(conv0 {x, y} INTER conv_trg {v1, v2, v3} = {})) /\
\r
2379 dist (x,y) < t0 <=> a /\ ( ~(x IN {v1, v2, v3}) /\
\r
2380 ~(conv0 {x, y} INTER conv_trg {v1, v2, v3} = {}) /\
\r
2381 dist (x,y) < t0)`] THEN
\r
2382 NGOAC THEN MATCH_MP_TAC (MESON[]` ((? a b c. P a b c ) ==> (? a b c. Q a b c) )
\r
2383 ==> (? a b c. P a b c /\ d ) ==> ( ? a b c. Q a b c /\ d )`) THEN
\r
2384 ONCE_REWRITE_TAC[ prove (`!q s.
\r
2387 (quasi_reg_tet q s \/
\r
2390 (q = {v, v1, v2, v3} \/ q = {v, v1, v3, v4}) /\
\r
2391 interior_pos v v1 v3 v2 v4 s /\
\r
2392 anchor_points v1 v3 s = {v, v2, v4} /\
\r
2393 anchor_points v2 v4 s = {v, v1, v3}))`, MP_TAC WHEN_IN_Q_SYS THEN
\r
2394 REWRITE_TAC[ MESON[]` (! q s. P q s ==> R q s ) ==> ( ! q s. P q s <=> P q s
\r
2395 /\ R q s ) `])] THEN
\r
2397 MATCH_MP_TAC (MESON[]` ((?v1 v2 v3. (?a b c d. P v1 v2 v3 a b c d) /\ cc v1 v2 v3) ==> las) /\
\r
2398 ((?v1 v2 v3. (?a b c d. Q v1 v2 v3 a b c d) /\ cc v1 v2 v3) ==> las) /\
\r
2399 ((?v1 v2 v3. (?a b c d. R v1 v2 v3 a b c d) /\ cc v1 v2 v3) ==> las)
\r
2402 P v1 v2 v3 a b c d \/
\r
2403 Q v1 v2 v3 a b c d \/
\r
2404 R v1 v2 v3 a b c d) /\
\r
2407 SIMP_TAC[quasi_reg_tet_case; hard_case] THEN
\r
2408 REWRITE_TAC[ MESON[]` a /\ as \/ b /\ as <=> ( a \/ b ) /\ as `] THEN
\r
2409 NHANH (MATCH_MP (MESON[]` (! q s. P q s) ==> P q s`) RELATE_Q_SYS) THEN
\r
2411 MATCH_MP_TAC (MESON[]` ((? v1 v2 v3 . (? a b c d. aa a b c d v1 v2 v3 /\ bb a b c d v1 v2 v3
\r
2412 /\ cc a b c d v1 v2 v3 /\ ee a b c d v1 v2 v3 )
\r
2413 /\ las v1 v2 v3 ) ==> last )
\r
2414 ==> (? v1 v2 v3 . (? a b c d. aa a b c d v1 v2 v3 /\ bb a b c d v1 v2 v3
\r
2415 /\ cc a b c d v1 v2 v3 /\ dd a b c d v1 v2 v3 /\ ee a b c d v1 v2 v3 )
\r
2416 /\ las v1 v2 v3 ) ==> last `) THEN
\r
2417 REWRITE_TAC[ hard_case]);;
\r
2419 (* ============ *)
\r
2422 let OCTO23 = prove (` ! s x y. (?v1 v2 v3.
\r
2423 ~(x IN {v1, v2, v3}) /\
\r
2424 (quasi_tri {v1, v2, v3} s \/ (?v4. {v1, v2, v3} UNION {v4} IN Q_SYS s)) /\
\r
2425 ~(conv0 {x, y} INTER conv_trg {v1, v2, v3} = {}) /\
\r
2429 ~(v1 = v2 \/ v2 = v3 \/ v3 = v1) /\
\r
2430 dist (v1,v2) <= #2.51 /\
\r
2431 dist (v2,v3) <= #2.51 /\
\r
2432 dist (v3,v1) < sqrt (&8) /\
\r
2433 {v1, v2, v3} SUBSET s /\
\r
2434 ~(x IN {v1, v2, v3}) /\
\r
2435 ~(conv0 {x, y} INTER conv_trg {v1, v2, v3} = {}) /\
\r
2436 dist (x,y) < t0) `,
\r
2437 REWRITE_TAC[MESON[]` (?v4. {v1, v2, v3} UNION {v4} IN Q_SYS s) <=>
\r
2439 ({vv1, vv2, vv3} = {v1, v2, v3} /\ #2.51 < dist (vv3,vv1)) /\
\r
2440 {v1, v2, v3} UNION {v4} IN Q_SYS s) \/
\r
2441 (?v4. (!vv1 vv2 vv3.
\r
2442 {vv1, vv2, vv3} = {v1, v2, v3} ==> ~(#2.51 < dist (vv3,vv1))) /\
\r
2443 {v1, v2, v3} UNION {v4} IN Q_SYS s) `] THEN KHANANG THEN REPEAT GEN_TAC THEN
\r
2444 REWRITE_TAC[ MESON[]` (?a b c. P a b c \/ Q a b c \/ R a b c) <=>
\r
2445 (?a b c. P a b c) \/ (?a b c. Q a b c) \/ (?a b c. R a b c) `] THEN
\r
2446 MATCH_MP_TAC (MESON[]` ( a ==> l ) /\ ( b==> l ) /\ ( c==> l ) ==> a \/ b\/ c ==> l `) THEN
\r
2447 REWRITE_TAC[ quasi_tri_case; OCT24; OCTOR23 ]);;
\r
2454 let IN_AFF_GE_CON = prove(`!x y v3 v2.
\r
2455 ~(conv0 {x, y} INTER conv_trg {x, v2, v3} = {})
\r
2456 ==> y IN aff_ge {x} {v2, v3}`,
\r
2457 REWRITE_TAC[ GSYM conv0_2; simpl_conv3; simp_def; SET_RULE` ~( a INTER b = {}) <=>
\r
2458 (? x . x IN a /\ x IN b )`; IN_ELIM_THM] THEN
\r
2460 REWRITE_TAC[ MESON[]` (?x'. (?t. P t /\ x' = t % x + (&1 - t) % y) /\
\r
2461 (?a b c. Q a b c /\ x' = a % x + b % v2 + c % v3)) <=>
\r
2462 (?a b c t. P t /\ Q a b c /\ t % x + (&1 - t) % y = a % x + b % v2 + c % v3)`] THEN
\r
2463 REWRITE_TAC[ VECTOR_ARITH ` t % x + (&1 - t) % y = a % x + b % v2 + c % v3
\r
2464 <=> (&1 - t ) % y = ( a - t ) % x + b % v2 + c % v3 `] THEN
\r
2465 REWRITE_TAC[ MESON[]` t < &1 /\ a <=> a /\ t < &1 `] THEN PHA THEN
\r
2466 NHANH (REAL_ARITH` t < &1 ==> ~ ( &1 - t = &0 )`) THEN
\r
2467 REWRITE_TAC[ MESON[]` (t < &1 /\ ~(&1 - t = &0)) /\ aa <=> aa /\ ~(&1 - t = &0) /\
\r
2469 REWRITE_TAC[ MESON[]` (t < &1 /\ ~(&1 - t = &0)) /\ aa <=> t < &1 /\ aa /\ ~(&1 - t = &0)
\r
2471 ONCE_REWRITE_TAC[ MESON[REAL_FIELD `! a b. ~ ( b = &0 ) <=> a = b * a / b /\ ~ ( b = &0 ) `] `
\r
2472 ~ ( b = &0 ) <=> ( ! a . a = b * a / b ) /\ ~ ( b = &0 )`] THEN
\r
2473 PHA THEN REWRITE_TAC[ MESON[ VECTOR_MUL_RCANCEL ] ` (&1 - t) % y = (a - t) % x + b % v2 + c % v3 /\
\r
2474 (!a. a = (&1 - t) * a / (&1 - t)) /\ las
\r
2475 <=> (&1 - t) % y = ((&1 - t) * (a - t ) / (&1 - t)) % x + ((&1 - t) * b / (&1 - t)) % v2 + ((&1 - t) * c / (&1 - t)) % v3 /\
\r
2476 (!a. a = (&1 - t) * a / (&1 - t)) /\ las `] THEN
\r
2477 REWRITE_TAC[ VECTOR_ARITH ` ( a * b ) % v1 + ( a * c ) % v2 + ( a * d ) % v3 = a % ( b % v1 + c % v2 + d % v3 ) `] THEN
\r
2478 REWRITE_TAC[ MESON[ VECTOR_MUL_LCANCEL_IMP; VECTOR_MUL_RCANCEL ] ` (&1 - t) % y =
\r
2480 ((a - t) / (&1 - t) % x + b / (&1 - t) % v2 + c / (&1 - t) % v3) /\
\r
2482 ~(&1 - t = &0) /\ l <=> y =
\r
2484 ((a - t) / (&1 - t) % x + b / (&1 - t) % v2 + c / (&1 - t) % v3) /\
\r
2486 ~(&1 - t = &0) /\ l `] THEN
\r
2487 REWRITE_TAC[ REAL_ARITH ` t < &1 <=> &0 < &1 - t `] THEN
\r
2488 REWRITE_TAC[ MESON[]`&0 <= a /\ &0 <= b /\
\r
2489 &0 <= c /\ las <=> &0 <= a /\ las /\ &0 <= b /\
\r
2490 &0 <= c `] THEN PHA THEN
\r
2491 REWRITE_TAC[ MESON[REAL_ARITH ` &0 < a ==> &0 <= a `; REAL_LE_DIV ]`
\r
2492 &0 < &1 - t /\ &0 <= a /\ &0 <= b <=>
\r
2496 &0 <= a / (&1 - t) /\
\r
2497 &0 <= b / (&1 - t) `] THEN
\r
2498 MESON_TAC[MESON[REAL_FIELD `~(&1 - t = &0) /\ a + b + c = &1
\r
2499 ==> (a - t) / (&1 - t) + b / (&1 - t) + c / (&1 - t) = &1 `]`
\r
2501 y = (a - t) / (&1 - t) % x + b / (&1 - t) % v2 + c / (&1 - t) % v3 /\
\r
2503 ~(&1 - t = &0) /\ las
\r
2504 <=> a + b + c = &1 /\ cccc /\ ~(&1 - t = &0) /\ las /\ y = (a - t) / (&1 - t) % x + b / (&1 - t) % v2 + c / (&1 - t) % v3
\r
2505 /\ (a - t) / (&1 - t) + b / (&1 - t) + c / (&1 - t) = &1 `]);;
\r
2508 (* ============= *)
\r
2510 let xxii = MATCH_MP REAL_LT_RSQRT (REAL_ARITH `(&2 * #1.255) pow 2 < &8`);;
\r
2513 let import_le = prove( `!x y s.
\r
2515 dist (x,y) < t0 /\
\r
2516 ~(y IN UNIONS {aff_ge {x} {w1, w2} | w1,w2 | {x, w1, w2} IN barrier s})
\r
2517 ==> ~obstructed x y s`,
\r
2518 REWRITE_TAC[ MESON[]` a /\ b /\ ~c ==> ~d <=> a /\ b /\ d ==> c`] THEN
\r
2519 REWRITE_TAC[ obstructed ; barrier] THEN
\r
2520 REWRITE_TAC[ IN_ELIM_THM] THEN
\r
2521 ONCE_REWRITE_TAC[ MESON[]` (? a . P a ) <=> ( ? a. ( x IN a \/ ~( x IN a )) /\ P a)`] THEN
\r
2522 REWRITE_TAC[ MESON[] ` (?b. aa b /\ (?u v w. P u v w /\ b = {u, v, w}) /\ cc b) <=>
\r
2523 (?u v w. aa {u, v, w} /\ P u v w /\ cc {u, v, w}) `] THEN
\r
2524 REWRITE_TAC[ MESON[]` (x IN {v1, v2, v3} \/ ~(x IN {v1, v2, v3})) /\ a <=>
\r
2525 x IN {v1, v2, v3} /\ a \/ ~(x IN {v1, v2, v3}) /\ a `] THEN
\r
2526 ONCE_REWRITE_TAC[ MESON[]`(? a c b. P a b c \/ Q a b c )
\r
2527 <=> ( ? a b c. Q a b c \/ P a b c) `] THEN
\r
2528 ONCE_REWRITE_TAC[ MESON[]` aa /\ (?a c b. P a b c \/ Q a b c) <=>
\r
2529 aa /\ (?a b c. P a b c /\ aa \/ Q a b c) `] THEN PHA THEN
\r
2530 REWRITE_TAC[conv0_2] THEN
\r
2531 REWRITE_TAC[ MESON[]` (?a. P a \/ Q a) <=> (?a. P a) \/ (?a. Q a)`] THEN
\r
2532 NHANH (MATCH_MP (MESON[]` (! a b c. P a b c) ==> P a b c `) OCTO23) THEN
\r
2533 NHANH (MATCH_MP (MESON[]` (! x y a b c. P x y a b c ) ==> P x y a b c `)
\r
2534 MEETING_CONDITION) THEN
\r
2535 ONCE_REWRITE_TAC[MESON[]` v1 /\ v2/\ v3 /\ v4 /\ v5/\ v6 /\ v7 /\ las
\r
2536 <=> ( v1 /\ v2/\ v3 /\ v4 /\ v5/\ v6 /\ v7) /\ las`] THEN
\r
2537 NHANH (MATCH_MP (MESON[]` (! a b c d e. P a b c d e ) ==> P a b c d e`) tarski_FFSXOWD ) THEN
\r
2539 REWRITE_TAC[ MESON[]` normball x #1.255 INTER conv {v1, v2, v3} = {} /\ a
\r
2540 <=> a /\ normball x #1.255 INTER conv {v1, v2, v3} = {} `] THEN
\r
2541 PHA THEN SIMP_TAC[ MESON[]` ~ a /\ a <=> F `] THEN
\r
2542 REPEAT GEN_TAC THEN MATCH_MP_TAC (MESON[]` (c ==> l) ==> a /\ b/\ c==> l`) THEN
\r
2543 REWRITE_TAC[SET_RULE ` x IN {a, b, c} <=> x = a \/ x = b \/ x = c `] THEN
\r
2544 MATCH_MP_TAC (MESON[]` (!a b c. P a b c <=> P b a c) /\
\r
2545 ((?a b c. (x = a \/ x = c) /\ P a b c) ==> las)
\r
2546 ==> (?a b c. (x = a \/ x = b \/ x = c) /\ P a b c)
\r
2548 SIMP_TAC[ MESON[SET_RULE ` { a, b, c} = { b , a, c} ` ]` !v1 v2 v3.
\r
2549 (quasi_tri {v1, v2, v3} s \/
\r
2550 (?v4. {v1, v2, v3} UNION {v4} IN Q_SYS s)) /\
\r
2551 ~(conv0 {x, y} INTER conv_trg {v1, v2, v3} = {}) <=>
\r
2552 (quasi_tri {v2, v1, v3} s \/
\r
2553 (?v4. {v2, v1, v3} UNION {v4} IN Q_SYS s)) /\
\r
2554 ~(conv0 {x, y} INTER conv_trg {v2, v1, v3} = {})`] THEN
\r
2555 MATCH_MP_TAC (MESON[]` (!a b c. P a b c <=> P c b a ) /\
\r
2556 ((?a b c. (x = a ) /\ P a b c) ==> las)
\r
2557 ==> (?a b c. (x = a \/ x = c) /\ P a b c)
\r
2559 SIMP_TAC[ MESON[SET_RULE ` { a, b, c} = {c , b , a} ` ]` !v1 v2 v3.
\r
2560 (quasi_tri {v1, v2, v3} s \/ (?v4. {v1, v2, v3} UNION {v4} IN Q_SYS s)) /\
\r
2561 ~(conv0 {x, y} INTER conv_trg {v1, v2, v3} = {}) <=>
\r
2562 (quasi_tri {v3, v2, v1} s \/ (?v4. {v3, v2, v1} UNION {v4} IN Q_SYS s)) /\
\r
2563 ~(conv0 {x, y} INTER conv_trg {v3, v2, v1} = {})`] THEN
\r
2564 PURE_ONCE_REWRITE_TAC[ MESON[]` (?v1 v2 v3. x = v1 /\ P x v1 v2 v3) <=>
\r
2565 (?v1 v2 v3. x = v1 /\ P x x v2 v3) `] THEN
\r
2566 NHANH (MATCH_MP (MESON[]` (! a b c d. P a b c d) ==> P a b c d`) IN_AFF_GE_CON) THEN
\r
2567 MATCH_MP_TAC (MESON[]` ((? v1 v2 v3. P v1 v2 v3 /\ PP v1 v2 v3 )
\r
2569 ==> (? v1 v2 v3. a v1 /\ P v1 v2 v3 /\ b v2 v3 /\ PP v1 v2 v3 )
\r
2571 REWRITE_TAC[ IN_UNIONS; IN_ELIM_THM] THEN
\r
2579 (* ======================== end im_le_82.ml =============================== *)
\r
2581 let lemma_of_lemma82 = prove (` ! (x:real^3) (v0:real^3) s Z. centered_pac s v0 /\ Z = UNIONS {e_plane u v | u IN near2t0 v0 s /\ v IN near2t0 v0 s} /\
\r
2582 x IN normball v0 t0 DIFF Z
\r
2583 ==> (?w. w IN near2t0 v0 s /\ x IN voronoi w s)`, REPEAT GEN_TAC THEN REWRITE_TAC[centered_pac] THEN
\r
2584 REWRITE_TAC[ SET_RULE `packing s /\ v0 IN s <=> packing s /\ v0 IN s /\ ~(s={})`] THEN
\r
2585 REWRITE_TAC[MESON[exists_min_dist] ` (packing s /\ v0 IN s /\ ~(s = {})) /\
\r
2586 Z = UNIONS {e_plane u v | u IN near2t0 v0 s /\ v IN near2t0 v0 s} /\
\r
2587 x IN normball v0 t0 DIFF Z <=>(packing s /\ v0 IN s /\ ~(s = {})) /\
\r
2588 Z = UNIONS {e_plane u v | u IN near2t0 v0 s /\ v IN near2t0 v0 s} /\
\r
2589 x IN normball v0 t0 DIFF Z /\ min_dist x s `] THEN
\r
2590 SIMP_TAC[normball; min_dist] THEN
\r
2591 REWRITE_TAC[SET_RULE` x IN a DIFF b <=> x IN a /\ ~( x IN b )`] THEN
\r
2592 REWRITE_TAC[SET_RULE ` x IN { x | P x } <=> P x `] THEN PHA THEN
\r
2593 REWRITE_TAC[MESON[]` dist (x,v0) < t0 /\
\r
2595 ((?u. u IN s /\ (!w. w IN s /\ ~(u = w) ==> dist (u,x) < dist (w,x))) \/
\r
2600 dist (u,x) = dist (v,x) /\
\r
2601 (!w. w IN s ==> dist (u,x) <= dist (w,x)))) <=>
\r
2602 dist (x,v0) < t0 /\
\r
2604 ((?u. u IN s /\ (!w. w IN s /\ ~(u = w) ==> dist (u,x) < dist (w,x))) \/
\r
2605 ( ~(x IN Z) /\ (?u v.
\r
2609 dist (u,x) = dist (v,x) /\
\r
2610 (!w. w IN s ==> dist (u,x) <= dist (w,x)) /\ dist (x,v0) < t0 ))) `] THEN
\r
2611 REWRITE_TAC[MESON[DIST_TRIANGLE] ` v0 IN s /\
\r
2613 Z = UNIONS {e_plane u v | u IN near2t0 v0 s /\ v IN near2t0 v0 s} /\
\r
2614 dist (x,v0) < t0 /\
\r
2616 ((?u. u IN s /\ (!w. w IN s /\ ~(u = w) ==> dist (u,x) < dist (w,x))) \/
\r
2622 dist (u,x) = dist (v,x) /\
\r
2623 (!w. w IN s ==> dist (u,x) <= dist (w,x)) /\
\r
2624 dist (x,v0) < t0)) <=>
\r
2627 Z = UNIONS {e_plane u v | u IN near2t0 v0 s /\ v IN near2t0 v0 s} /\
\r
2628 dist (x,v0) < t0 /\
\r
2630 ((?u. u IN s /\ (!w. w IN s /\ ~(u = w) ==> dist (u,x) < dist (w,x))) \/
\r
2634 dist (u,v0) <= dist (u,x) + dist (x,v0) /\
\r
2635 dist (u,x) <= dist (v0,x) /\
\r
2637 dist (v,v0) <= dist (v,x) + dist (x,v0) /\
\r
2638 dist (v,x) <= dist (v0,x) /\
\r
2640 dist (u,x) = dist (v,x) /\
\r
2641 (!w. w IN s ==> dist (u,x) <= dist (w,x)) /\
\r
2642 dist (x,v0) < t0)) `] THEN
\r
2643 REWRITE_TAC[MESON[] ` u IN s /\
\r
2644 dist (u,v0) <= dist (u,x) + dist (x,v0) /\
\r
2645 dist (u,x) <= dist (v0,x) /\
\r
2647 dist (v,v0) <= dist (v,x) + dist (x,v0) /\
\r
2648 dist (v,x) <= dist (v0,x) /\
\r
2650 dist (u,x) = dist (v,x) /\
\r
2651 (!w. w IN s ==> dist (u,x) <= dist (w,x)) /\
\r
2652 dist (x,v0) < t0 <=>
\r
2654 (dist (u,v0) <= dist (u,x) + dist (x,v0) /\
\r
2655 dist (u,x) <= dist (v0,x) /\
\r
2656 dist (x,v0) < t0) /\
\r
2658 (dist (v,v0) <= dist (v,x) + dist (x,v0) /\
\r
2659 dist (v,x) <= dist (v0,x) /\
\r
2660 dist (x,v0) < t0) /\
\r
2662 dist (u,x) = dist (v,x) /\
\r
2663 (!w. w IN s ==> dist (u,x) <= dist (w,x))`] THEN
\r
2664 SIMP_TAC[DIST_SYM] THEN
\r
2665 REWRITE_TAC[REAL_ARITH ` dist (u,v0) <= dist (u,x) + dist (v0,x) /\
\r
2666 dist (u,x) <= dist (v0,x) /\
\r
2668 <=> dist (u,v0) <= dist (u,x) + dist (v0,x) /\
\r
2669 dist (u,x) <= dist (v0,x) /\
\r
2670 dist (v0,x) < t0 /\ dist(u, v0) < &2 * t0 `] THEN
\r
2671 REWRITE_TAC[ MESON[] ` a /\ b /\c/\ d /\ e ==> f <=> a/\b/\c/\d ==> e ==> f `] THEN SIMP_TAC[] THEN
\r
2672 REWRITE_TAC[ IN_UNIONS; e_plane; near2t0] THEN
\r
2673 REWRITE_TAC[SET_RULE ` x IN { x | P x } <=> P x `] THEN
\r
2674 REWRITE_TAC[IN_ELIM_THM] THEN REWRITE_TAC[ MESON[] ` (?t. (?u v.
\r
2675 ((u IN s /\ dist (v0,u) < &2 * t0) /\
\r
2677 dist (v0,v) < &2 * t0) /\
\r
2678 t = e_plane u v) /\
\r
2681 ((u IN s /\ dist (v0,u) < &2 * t0) /\
\r
2683 dist (v0,v) < &2 * t0) /\
\r
2684 x IN e_plane u v) `] THEN
\r
2685 REWRITE_TAC[ SET_RULE ` x IN e_plane u v <=> e_plane u v x `; e_plane] THEN
\r
2686 PHA THEN SIMP_TAC[ MESON[DIST_SYM] ` ~(?u v.
\r
2688 dist (v0,u) < &2 * t0 /\
\r
2690 dist (v0,v) < &2 * t0 /\
\r
2692 dist (u,x) = dist (v,x)) /\
\r
2695 dist (u,v0) <= dist (u,x) + dist (v0,x) /\
\r
2696 dist (u,x) <= dist (v0,x) /\
\r
2697 dist (v0,x) < t0 /\
\r
2698 dist (u,v0) < &2 * t0 /\
\r
2700 dist (v,v0) <= dist (v,x) + dist (v0,x) /\
\r
2701 dist (v,x) <= dist (v0,x) /\
\r
2702 dist (v0,x) < t0 /\
\r
2703 dist (v,v0) < &2 * t0 /\
\r
2705 dist (u,x) = dist (v,x) /\
\r
2706 (!w. w IN s ==> dist (u,x) <= dist (w,x))) <=> F `] THEN
\r
2707 REWRITE_TAC[voronoi] THEN REWRITE_TAC[ SET_RULE ` x IN { x | P x } <=> P x `] THEN
\r
2708 REWRITE_TAC[ MESON[] ` dist (v0,x) < t0 /\
\r
2711 dist (v0,u) < &2 * t0 /\
\r
2713 dist (v0,v) < &2 * t0 /\
\r
2715 dist (u,x) = dist (v,x)) /\
\r
2716 (?u. u IN s /\ (!w. w IN s /\ ~(u = w) ==> dist (u,x) < dist (w,x)))
\r
2717 <=> dist (v0,x) < t0 /\
\r
2720 dist (v0,u) < &2 * t0 /\
\r
2722 dist (v0,v) < &2 * t0 /\
\r
2724 dist (u,x) = dist (v,x)) /\
\r
2725 (?u. u IN s /\dist (v0,x) < t0 /\ (!w. w IN s /\ ~(u = w) ==> dist (u,x) < dist (w,x)))`] THEN
\r
2726 REWRITE_TAC[ MESON[DIST_TRIANGLE] `(?u. u IN s /\
\r
2727 dist (v0,x) < t0 /\
\r
2728 (!w. w IN s /\ ~(u = w) ==> dist (u,x) < dist (w,x))) <=>
\r
2730 dist (v0,x) < t0 /\
\r
2731 dist (u,v0) <= dist (u,x) + dist (x,v0) /\
\r
2732 (!w. w IN s /\ ~(u = w) ==> dist (u,x) < dist (w,x))) `] THEN
\r
2733 REWRITE_TAC[ MESON[] ` ( a ==> b==> c <=> a/\b ==> c ) `] THEN PHA THEN
\r
2734 ONCE_REWRITE_TAC[ MESON[] ` a /\ b /\ c ==> d <=> a/\c /\b ==> d `] THEN PHA THEN
\r
2735 ONCE_REWRITE_TAC[MESON[] ` !P. (?u. P u) /\ v0 IN s <=>
\r
2736 ((?u. u = v0 /\ P u) \/ (?u. ~(u = v0) /\ P u)) /\ v0 IN s`] THEN
\r
2737 REWRITE_TAC[t0] THEN ONCE_REWRITE_TAC[MESON[ DIST_REFL; REAL_ARITH ` &0 < &2 * #1.255 ` ] ` u = v0 /\ las <=> u = v0 /\ dist(u,v0 ) < &2 * #1.255 /\ las `] THEN
\r
2738 REWRITE_TAC[ MESON[] ` ((?u. u = v0 /\
\r
2739 dist (u,v0) < &2 * #1.255 /\
\r
2741 dist (v0,x) < #1.255 /\
\r
2742 dist (u,v0) <= dist (u,x) + dist (x,v0) /\
\r
2743 (!w. w IN s /\ ~(u = w) ==> dist (u,x) < dist (w,x))) \/
\r
2746 dist (v0,x) < #1.255 /\
\r
2747 dist (u,v0) <= dist (u,x) + dist (x,v0) /\
\r
2748 (!w. w IN s /\ ~(u = w) ==> dist (u,x) < dist (w,x)))) /\
\r
2751 dist (u,v0) < &2 * #1.255 /\
\r
2754 dist (v0,x) < #1.255 /\
\r
2755 dist (u,v0) <= dist (u,x) + dist (x,v0) /\
\r
2756 (!w. w IN s /\ ~(u = w) ==> dist (u,x) < dist (w,x))) \/
\r
2760 dist (v0,x) < #1.255 /\
\r
2761 dist (u,v0) <= dist (u,x) + dist (x,v0) /\
\r
2762 (!w. w IN s /\ ~(u = w) ==> dist (u,x) < dist (w,x)))) /\
\r
2763 v0 IN s `] THEN REWRITE_TAC[ MESON[] ` ~(u = v0) /\
\r
2766 dist (v0,x) < #1.255 /\
\r
2767 dist (u,v0) <= dist (u,x) + dist (x,v0) /\
\r
2768 (!w. w IN s /\ ~(u = w) ==> dist (u,x) < dist (w,x)) <=>
\r
2772 v0 IN s /\ ( dist (u,x) < dist (v0,x) /\
\r
2773 dist (v0,x) < #1.255 /\
\r
2774 dist (u,v0) <= dist (u,x) + dist (x,v0) ) /\
\r
2775 (!w. w IN s /\ ~(u = w) ==> dist (u,x) < dist (w,x)) `] THEN SIMP_TAC[DIST_SYM] THEN
\r
2776 PURE_ONCE_REWRITE_TAC[ REAL_ARITH ` ( dist (u,x) < dist (v0,x) /\
\r
2777 dist (v0,x) < #1.255 /\
\r
2778 dist (u,v0) <= dist (u,x) + dist (v0,x)) <=>
\r
2779 (dist (u,x) < dist (v0,x) /\
\r
2780 dist (v0,x) < #1.255 /\
\r
2781 dist (u,v0) <= dist (u,x) + dist (v0,x)) /\
\r
2782 dist (u,v0) < &2 * #1.255 ` ] THEN
\r
2783 MATCH_MP_TAC (MESON[] `((?u. u = v0 /\
\r
2784 dist (u,v0) < &2 * #1.255 /\
\r
2787 dist (v0,x) < #1.255 /\
\r
2788 dist (u,v0) <= dist (u,x) + dist (v0,x) /\
\r
2789 (!w. w IN s /\ ~(u = w) ==> dist (u,x) < dist (w,x))) \/
\r
2793 ((dist (u,x) < dist (v0,x) /\
\r
2794 dist (v0,x) < #1.255 /\
\r
2795 dist (u,v0) <= dist (u,x) + dist (v0,x)) /\
\r
2796 dist (u,v0) < &2 * #1.255) /\
\r
2797 (!w. w IN s /\ ~(u = w) ==> dist (u,x) < dist (w,x)))
\r
2798 ==> (?w. w IN s /\
\r
2799 dist (v0,w) < &2 * #1.255 /\
\r
2800 (!w'. s w' /\ ~(w' = w) ==> dist (w,x) < dist (w',x))))
\r
2805 {e_plane u v | u IN s /\
\r
2806 dist (u,v0) < &2 * #1.255 /\
\r
2808 dist (v,v0) < &2 * #1.255} /\
\r
2809 dist (v0,x) < #1.255 /\
\r
2812 dist (u,v0) < &2 * #1.255 /\
\r
2814 dist (v,v0) < &2 * #1.255 /\
\r
2816 dist (u,x) = dist (v,x)) /\
\r
2818 dist (u,v0) < &2 * #1.255 /\
\r
2821 dist (v0,x) < #1.255 /\
\r
2822 dist (u,v0) <= dist (u,x) + dist (v0,x) /\
\r
2823 (!w. w IN s /\ ~(u = w) ==> dist (u,x) < dist (w,x))) \/
\r
2827 ((dist (u,x) < dist (v0,x) /\
\r
2828 dist (v0,x) < #1.255 /\
\r
2829 dist (u,v0) <= dist (u,x) + dist (v0,x)) /\
\r
2830 dist (u,v0) < &2 * #1.255) /\
\r
2831 (!w. w IN s /\ ~(u = w) ==> dist (u,x) < dist (w,x)))) /\
\r
2833 ==> (?w. w IN s /\
\r
2834 dist (v0,w) < &2 * #1.255 /\
\r
2835 (!w'. s w' /\ ~(w' = w) ==> dist (w,x) < dist (w',x))) `) THEN
\r
2836 MESON_TAC [DIST_SYM; SET_RULE ` ! x s. s x <=> x IN s ` ]);;
\r