(* tchales, This does not run in Multivariate *)
let TRIANGLE_IN_BARRIER = prove(` ! s v0 v1 v2 . {v0, v1, v2}
IN barrier s
==> (!xx yy.
~(xx = yy) /\ {xx, yy}
SUBSET {v1, v2, v0}
==> &2 <=
dist (xx,yy) /\
dist (xx,yy) <=
sqrt (&8)) /\
((!aa bb.
aa
IN {v1, v2, v0} /\ bb
IN {v1, v2, v0} ==>
dist (aa,bb) <= #2.51) \/
(?aa bb.
{aa, bb}
SUBSET {v1, v2, v0} /\
#2.51 <
dist (aa,bb) /\
(!x y.
~({x, y} = {aa, bb}) /\ {x, y}
SUBSET {v1, v2, v0}
==>
dist (x,y) <= #2.51)))`,
REWRITE_TAC[ barrier;
IN_ELIM_THM] THEN
REWRITE_TAC[ GSYM (MESON[]` P {x, y, z} <=>
(?a b c. P {a, b, c} /\ {x, y, z} = {a, b, c})`)] THEN
MP_TAC
A_LEMMA THEN
REWRITE_TAC[ MESON[]` (! a b c d. P a b c d ==> las a b c d ) ==> (! a b c d .
P a b c d \/ Q a b c d ==> las a b c d) <=>
(! a b c d. P a b c d ==> las a b c d ) ==> (! a b c d .
Q a b c d ==> las a b c d)`] THEN DISCH_TAC THEN
NHANH (CUTHE2
CASES_OF_Q_SYS) THEN
REPEAT GEN_TAC THEN
MATCH_MP_TAC (MESON[]` ((? a. Q a) ==> l) /\ ((?a. R a ) ==> l) ==>
(? a. P a /\ ( Q a \/ R a )) ==> l `) THEN
REWRITE_TAC[
NOV1] THEN
NHANH (CUTHE4
TRIANGLE_IN_STRICT_QUA) THEN
MATCH_MP_TAC (MESON[]` (b ==> l) /\ ( a /\ c ==> l) ==> a /\ ( b \/ c ) ==> l`) THEN
ASM_REWRITE_TAC[] THEN
REWRITE_TAC[
strict_qua; quarter; SET_RULE `{a,b,c}
UNION {d} = {a,b,c,d}`;
def_simplex] THEN
PHA THEN
REWRITE_TAC[ MESON[]` a /\ a /\ l <=> a /\ l `; packing ] THEN
MATCH_MP_TAC (MESON[] `(a ==> aa) /\ (b ==> bb) ==> a /\ b ==> aa /\ (cc \/ bb)`) THEN
SIMP_TAC[ SET_RULE `{a,b,c} = {c,a,b} `] THEN
NHANH (SET_RULE ` {v0, v1, v2, v4}
SUBSET s ==> {v0,v1,v2}
SUBSET s `) THEN
NHANH ( MESON[SET_RULE ` x
IN a /\ a
SUBSET s ==> s x `]`(!u v. s u /\ s v /\ ~(u = v) ==> &2 <=
dist (u,v)) /\
({v0, v1, v2, v4}
SUBSET s /\ {v0, v1, v2}
SUBSET s) /\ l ==>
(!u v. u
IN {v0,v1,v2} /\ v
IN {v0,v1,v2} /\ ~(u = v) ==> &2 <=
dist (u,v))`) THEN
REWRITE_TAC[t0] THEN
NHANH ( MESON[
PAIR_D3] ` d3 v w <=
sqrt (&8) ==> (! x y. x
IN {v0, v1, v2, v4} /\
y
IN {v0, v1, v2, v4} /\ {x,y} = {v,w} ==> d3 x y <=
sqrt (&8) )`) THEN
REWRITE_TAC[ SET_RULE ` {a,b}
SUBSET s <=> a
IN s /\ b
IN s `] THEN
SIMP_TAC[ SET_RULE ` {a,b,c} = {c,a,b} `] THEN
REWRITE_TAC[ GSYM d3 ] THEN
MESON_TAC[ MATCH_MP
REAL_LE_RSQRT (REAL_ARITH ` (&2 * #1.255 ) pow 2 <= &8 `);
SET_RULE ` x
IN {a,b,c} ==> x
IN {a,b,c,d} `; REAL_ARITH ` a <= b /\ b <= c ==> a <= c `]);;
let le1_82 = prove (`!s v0 Y.
centered_pac s v0 /\
w
IN near2t0 v0 s /\
Y =
UNIONS
{aff_ge {w} {w1, w2} | w
IN near2t0 v0 s /\ {w, w1, w2}
IN barrier s}
==>
UNIONS {aff_ge {w} {w1, w2} | w1,w2 | {w, w1, w2}
IN barrier s}
SUBSET
Y`,
SIMP_TAC[] THEN SET_TAC[]);;
let rhand_subset_lhand = prove (` ! (s:real^3 -> bool) (v0:real^3) Z Y.
centered_pac s v0 /\
Y =
UNIONS
{aff_ge {w} {w1, w2} | w
IN near2t0 v0 s /\ {w, w1, w2}
IN barrier s} /\
Z =
UNIONS {
e_plane u v | u
IN near2t0 v0 s /\ v
IN near2t0 v0 s}
==>
normball v0 t0
INTER voronoi v0 s
DIFF (Y
UNION Z)
SUBSET
normball v0 t0
INTER VC v0 s
DIFF (Y
UNION Z)`,
REWRITE_TAC[ SET_RULE ` a
INTER b
DIFF c
SUBSET a
INTER d
DIFF c <=>
(!x. x
IN a
INTER b
DIFF c ==> x
IN d) ` ] THEN
REWRITE_TAC[ GSYM ( MESON[
centered_pac;
le1_82; prove (` ! x s.
centered_pac s x ==> x
IN near2t0 x s `, REWRITE_TAC[
centered_pac; near2t0] THEN REWRITE_TAC[ MESON [
DIST_REFL; t0; REAL_ARITH ` &0 < &2 * #1.255 `] `
packing s /\ v0
IN s <=> packing s /\ v0
IN s /\
dist (v0,v0) < &2 * t0`] THEN
SET_TAC[] ) ] ` !s v0 Z Y.
centered_pac s v0 /\
Y =
UNIONS
{aff_ge {w} {w1, w2} | w
IN near2t0 v0 s /\ {w, w1, w2}
IN barrier s} /\
Z =
UNIONS {
e_plane u v | u
IN near2t0 v0 s /\ v
IN near2t0 v0 s} /\
UNIONS {aff_ge {v0} {w1, w2} | w1,w2 | {v0, w1, w2}
IN barrier s}
SUBSET
Y
==> last <=>
centered_pac s v0 /\
Y =
UNIONS
{aff_ge {w} {w1, w2} | w
IN near2t0 v0 s /\ {w, w1, w2}
IN barrier s} /\
Z =
UNIONS {
e_plane u v | u
IN near2t0 v0 s /\ v
IN near2t0 v0 s}
==> last `)] THEN
REWRITE_TAC[SET_RULE ` x
IN a
INTER b
DIFF c <=> x
IN a /\ x
IN b /\ ~( x
IN c )`] THEN
REWRITE_TAC[ MESON[] `
centered_pac s v0 /\
Y =
UNIONS
{aff_ge {w} {w1, w2} | w
IN near2t0 v0 s /\ {w, w1, w2}
IN barrier s} /\
Z =
UNIONS {
e_plane u v | u
IN near2t0 v0 s /\ v
IN near2t0 v0 s} /\
UNIONS {aff_ge {v0} {w1, w2} | w1,w2 | {v0, w1, w2}
IN barrier s}
SUBSET
Y
==> (!x. x
IN normball v0 t0 /\ x
IN voronoi v0 s /\ ~(x
IN Y
UNION Z)
==> x
IN VC v0 s) <=>
centered_pac s v0 /\
Y =
UNIONS
{aff_ge {w} {w1, w2} | w
IN near2t0 v0 s /\ {w, w1, w2}
IN barrier s} /\
Z =
UNIONS {
e_plane u v | u
IN near2t0 v0 s /\ v
IN near2t0 v0 s} /\
UNIONS {aff_ge {v0} {w1, w2} | w1,w2 | {v0, w1, w2}
IN barrier s}
SUBSET
Y
==> (!x. x
IN normball v0 t0 /\
x
IN voronoi v0 s /\
~(x
IN Y
UNION Z) /\
UNIONS
{aff_ge {v0} {w1, w2} | w1,w2 | {v0, w1, w2}
IN barrier s}
SUBSET
Y
==> x
IN VC v0 s) `] THEN
ONCE_REWRITE_TAC[ SET_RULE ` ~(x
IN Y
UNION Z) /\
UNIONS {aff_ge {v0} {w1, w2} | w1,w2 | {v0, w1, w2}
IN barrier s}
SUBSET
Y <=>
~(x
IN
UNIONS {aff_ge {v0} {w1, w2} | w1,w2 | {v0, w1, w2}
IN barrier s}) /\
~(x
IN Y
UNION Z) /\
UNIONS {aff_ge {v0} {w1, w2} | w1,w2 | {v0, w1, w2}
IN barrier s}
SUBSET
Y `] THEN REWRITE_TAC[
centered_pac ] THEN
REWRITE_TAC[ MESON[] ` (packing s /\ v0
IN s) /\
Y =
UNIONS
{aff_ge {w} {w1, w2} | w
IN near2t0 v0 s /\ {w, w1, w2}
IN barrier s} /\
Z =
UNIONS {
e_plane u v | u
IN near2t0 v0 s /\ v
IN near2t0 v0 s} /\
UNIONS {aff_ge {v0} {w1, w2} | w1,w2 | {v0, w1, w2}
IN barrier s}
SUBSET
Y
==> (!x. x
IN normball v0 t0 /\
x
IN voronoi v0 s /\
~(x
IN
UNIONS
{aff_ge {v0} {w1, w2} | w1,w2 | {v0, w1, w2}
IN barrier s}) /\
~(x
IN Y
UNION Z) /\
UNIONS
{aff_ge {v0} {w1, w2} | w1,w2 | {v0, w1, w2}
IN barrier s}
SUBSET
Y
==> x
IN VC v0 s) <=>
(packing s /\ v0
IN s) /\
Y =
UNIONS
{aff_ge {w} {w1, w2} | w
IN near2t0 v0 s /\ {w, w1, w2}
IN barrier s} /\
Z =
UNIONS {
e_plane u v | u
IN near2t0 v0 s /\ v
IN near2t0 v0 s} /\
UNIONS {aff_ge {v0} {w1, w2} | w1,w2 | {v0, w1, w2}
IN barrier s}
SUBSET
Y
==> (!x. v0
IN s /\
x
IN normball v0 t0 /\
x
IN voronoi v0 s /\
~(x
IN
UNIONS
{aff_ge {v0} {w1, w2} | w1,w2 | {v0, w1, w2}
IN barrier s}) /\
~(x
IN Y
UNION Z) /\
UNIONS
{aff_ge {v0} {w1, w2} | w1,w2 | {v0, w1, w2}
IN barrier s}
SUBSET
Y
==> x
IN VC v0 s) `] THEN
REPEAT GEN_TAC THEN DISCH_TAC THEN REWRITE_TAC[
normball] THEN
REWRITE_TAC[ SET_RULE ` z
IN { x | P x } <=> P z `] THEN
REWRITE_TAC[ voronoi;
VC;
lambda_x; d3 ] THEN
REWRITE_TAC[ SET_RULE ` x
IN { x | P x } <=> P x `] THEN
REWRITE_TAC[MESON[
DIST_SYM ;
import_le ] ` v0
IN s /\
dist (x,v0) < t0 /\
(!w. s w /\ ~(w = v0) ==>
dist (x,v0) <
dist (x,w)) /\
~(x
IN
UNIONS {aff_ge {v0} {w1, w2} | w1,w2 | {v0, w1, w2}
IN barrier s}) /\
~(x
IN Y
UNION Z) /\
UNIONS {aff_ge {v0} {w1, w2} | w1,w2 | {v0, w1, w2}
IN barrier s}
SUBSET
Y <=>
v0
IN s /\
dist (x,v0) < t0 /\
(!w. s w /\ ~(w = v0) ==>
dist (x,v0) <
dist (x,w)) /\
~(x
IN
UNIONS {aff_ge {v0} {w1, w2} | w1,w2 | {v0, w1, w2}
IN barrier s}) /\
~(x
IN Y
UNION Z) /\
UNIONS {aff_ge {v0} {w1, w2} | w1,w2 | {v0, w1, w2}
IN barrier s}
SUBSET
Y /\
~obstructed v0 x s `] THEN
ONCE_REWRITE_TAC[MESON[t0; REAL_ARITH ` #1.255 < &2 /\ (! a b (c:real). a < b
/\ b < c ==> a < c ) `;
DIST_SYM ]`
dist ( x, v0 ) < t0 <=>
dist ( x, v0 ) < t0 /\
dist ( v0, x) < &2 `] THEN
SIMP_TAC[
DIST_SYM ] THEN
MESON_TAC[ SET_RULE ` ! s x. s x <=> x
IN s `]);;
let lhand_subset_rhand = prove(` ! (s:real^3 -> bool) (v0:real^3) Z Y.
centered_pac s v0 /\
Y =
UNIONS
{aff_ge {w} {w1, w2} | w
IN near2t0 v0 s /\ {w, w1, w2}
IN barrier s} /\
Z =
UNIONS {
e_plane u v | u
IN near2t0 v0 s /\ v
IN near2t0 v0 s}
==>
normball v0 t0
INTER VC v0 s
DIFF (Y
UNION Z)
SUBSET
normball v0 t0
INTER voronoi v0 s
DIFF (Y
UNION Z)`,
REWRITE_TAC[ SET_RULE ` a
INTER b
DIFF c
SUBSET a
INTER d
DIFF c <=>
a
INTER b
DIFF c
DIFF d = {} `] THEN
REWRITE_TAC[ SET_RULE ` a = {} <=> (! x. ~ (x
IN a))`] THEN
REWRITE_TAC[ SET_RULE` x
IN a
DIFF b <=> x
IN a /\ ~( x
IN b ) `] THEN
REWRITE_TAC[ SET_RULE ` x
IN a
INTER b <=> x
IN a /\ x
IN b `] THEN PHA THEN
REWRITE_TAC[ SET_RULE ` x
IN normball v0 t0 /\ x
IN VC v0 s /\ ~(x
IN Y
UNION Z) /\ P x <=>
x
IN normball v0 t0
DIFF Z /\ x
IN VC v0 s /\ ~(x
IN Y
UNION Z) /\ P x `] THEN
REWRITE_TAC[MESON[
lemma_of_lemma82]`
centered_pac s v0 /\
Y =
UNIONS
{aff_ge {w} {w1, w2} | w
IN near2t0 v0 s /\ {w, w1, w2}
IN barrier s} /\
Z =
UNIONS {
e_plane u v | u
IN near2t0 v0 s /\ v
IN near2t0 v0 s}
==> (!x. ~(x
IN normball v0 t0
DIFF Z /\
x
IN VC v0 s /\
~(x
IN Y
UNION Z) /\
~(x
IN voronoi v0 s))) <=>
centered_pac s v0 /\
Y =
UNIONS
{aff_ge {w} {w1, w2} | w
IN near2t0 v0 s /\ {w, w1, w2}
IN barrier s} /\
Z =
UNIONS {
e_plane u v | u
IN near2t0 v0 s /\ v
IN near2t0 v0 s}
==> (!x. ~(x
IN normball v0 t0
DIFF Z /\
(?w. w
IN near2t0 v0 s /\ x
IN voronoi w s) /\
x
IN VC v0 s /\
~(x
IN Y
UNION Z) /\
~(x
IN voronoi v0 s))) `] THEN
REWRITE_TAC[ MESON[] `
(?w. w
IN near2t0 v0 s /\ x
IN voronoi w s) /\
x
IN VC v0 s /\
~(x
IN Y
UNION Z) /\
~(x
IN voronoi v0 s) <=>
(?w. w
IN near2t0 v0 s /\ x
IN voronoi w s /\ ~(w = v0)) /\
x
IN VC v0 s /\
~(x
IN Y
UNION Z) /\
~(x
IN voronoi v0 s) `] THEN
REWRITE_TAC[ MESON[near2t0] `
(?w. w
IN near2t0 v0 s /\ x
IN voronoi w s /\ ~(w = v0)) <=>
(?w. w
IN {x | x
IN s /\
dist (v0,x) < &2 * t0} /\
x
IN voronoi w s /\
~(w = v0)) `] THEN
REWRITE_TAC[ SET_RULE` a
IN { a | p a } <=> p a `] THEN
REWRITE_TAC[ voronoi;
lambda_x] THEN
REWRITE_TAC[ SET_RULE ` x
IN { v | P v } <=> P x `] THEN PHA THEN
REWRITE_TAC[ MESON[] ` a /\ b /\ d ==> c <=> b /\ d ==> a ==> c `] THEN
REPEAT GEN_TAC THEN DISCH_TAC THEN
REWRITE_TAC[
centered_pac] THEN
MATCH_MP_TAC (MESON[]` (a /\ b ==> (!x. ~b \/ P x)) ==> a /\ b ==> (!x. P x)`) THEN
REWRITE_TAC[ MESON[] ` ~(v0
IN s) \/ ~(x
IN normball v0 t0
DIFF Z /\ last) <=>
~(v0
IN s /\ x
IN normball v0 t0
DIFF Z /\ last)`] THEN
REWRITE_TAC[ MESON[]`
v0
IN s /\
x
IN normball v0 t0
DIFF Z /\
(?w. w
IN s /\
dist (v0,w) < &2 * t0 /\
(!w'. s w' /\ ~(w' = w) ==>
dist (x,w) <
dist (x,w')) /\
~(w = v0)) /\
last <=>
x
IN normball v0 t0
DIFF Z /\
(?w. w
IN s /\
v0
IN s /\
dist (v0,w) < &2 * t0 /\
(!w'. s w' /\ ~(w' = w) ==>
dist (x,w) <
dist (x,w')) /\
~(w = v0)) /\
last`] THEN
REWRITE_TAC[ MESON[ SET_RULE` x
IN s <=> s x `] `
(?w. w
IN s /\
v0
IN s /\
dist (v0,w) < &2 * t0 /\
(!w'. s w' /\ ~(w' = w) ==>
dist (x,w) <
dist (x,w')) /\
~(w = v0)) <=>
(?w. w
IN s /\
v0
IN s /\
dist (x,w) <
dist (x,v0) /\
dist (v0,w) < &2 * t0 /\
(!w'. s w' /\ ~(w' = w) ==>
dist (x,w) <
dist (x,w')) /\
~(w = v0)) `] THEN
REWRITE_TAC[ SET_RULE ` x
IN a
DIFF b <=> x
IN a /\ ~ ( x
IN b ) `] THEN
REWRITE_TAC[ MESON[
normball ; SET_RULE `x
IN { x | p x } <=> p x `] ` x
IN normball v0 t0
<=>
dist (x,v0) < t0 `] THEN
REWRITE_TAC[ MESON[REAL_ARITH ` a < b /\ b < c ==> a < c `]`
(
dist (x,v0) < t0 /\ ~(x
IN Z)) /\
(?w. w
IN s /\
v0
IN s /\
dist (x,w) <
dist (x,v0) /\
dist (v0,w) < &2 * t0 /\
(!w'. s w' /\ ~(w' = w) ==>
dist (x,w) <
dist (x,w')) /\
~(w = v0)) /\ las
<=> (
dist (x,v0) < t0 /\ ~(x
IN Z)) /\
(?w. w
IN s /\
v0
IN s /\
dist(x,w) < t0 /\
dist (x,w) <
dist (x,v0) /\
dist (v0,w) < &2 * t0 /\
(!w'. s w' /\ ~(w' = w) ==>
dist (x,w) <
dist (x,w')) /\
~(w = v0)) /\ las `] THEN
ASM_SIMP_TAC[] THEN PHA THEN
REWRITE_TAC[ MESON[] ` a /\ b /\ c /\ d /\ las <=> (a /\ d ) /\ b /\ c /\ las `] THEN
ONCE_REWRITE_TAC[ MESON[near2t0; SET_RULE ` x
IN { x | p x } <=> p x ` ]` (w
IN s /\
dist (v0,w) < &2 * t0) <=>
w
IN near2t0 v0 s /\ (w
IN s /\
dist (v0,w) < &2 * t0) `] THEN
REWRITE_TAC[ SET_RULE ` ~ ( x
IN a
UNION b) <=> ~( x
IN a ) /\ ~ (x
IN b)`] THEN PHA THEN
SIMP_TAC[MESON[] ` a /\ a /\ b <=> a /\ b `] THEN
REWRITE_TAC[ MESON[] ` a/\ b /\ ( ? w. P w ) /\ la <=> b /\ ( ? w. a /\ P w ) /\ la `] THEN
ONCE_REWRITE_TAC[ MESON[ SET_RULE ` w
IN near2t0 v0 s
==>
UNIONS {aff_ge {w} {w1, w2} | w1,w2 | {w, w1, w2}
IN barrier s}
SUBSET
UNIONS
{aff_ge {w} {w1, w2} | w
IN near2t0 v0 s /\ {w, w1, w2}
IN barrier s} `]
` w
IN near2t0 v0 s /\
w
IN s /\ last
<=>
UNIONS {aff_ge {w} {w1, w2} | w1,w2 | {w, w1, w2}
IN barrier s}
SUBSET
UNIONS
{aff_ge {w} {w1, w2} | w
IN near2t0 v0 s /\ {w, w1, w2}
IN barrier s} /\
w
IN near2t0 v0 s /\
w
IN s /\ last `] THEN
REWRITE_TAC[ MESON[] ` a /\ b /\ c /\ d /\ last <=> a /\ b /\ ( c/\ d ) /\ last `] THEN
REWRITE_TAC[ SET_RULE ` ~ ( x
IN a ) /\ b
SUBSET a <=> ~ ( x
IN a )/\ ~( x
IN b ) /\ b
SUBSET a`] THEN PHA THEN
REWRITE_TAC[ MESON[
DIST_SYM;
import_le ] `
dist (x,v0) < t0 /\
x
IN VC v0 s /\
~(x
IN
UNIONS
{aff_ge {w} {w1, w2} | w
IN near2t0 v0 s /\
{w, w1, w2}
IN barrier s}) /\
~(x
IN
UNIONS
{aff_ge {w} {w1, w2} | w1,w2 | {w, w1, w2}
IN barrier s}) /\
UNIONS
{aff_ge {w} {w1, w2} | w1,w2 | {w, w1, w2}
IN barrier s}
SUBSET
UNIONS
{aff_ge {w} {w1, w2} | w
IN near2t0 v0 s /\
{w, w1, w2}
IN barrier s} /\
w
IN near2t0 v0 s /\
w
IN s /\
dist (v0,w) < &2 * t0 /\
(!w'. s w' /\ ~(w' = w) ==>
dist (x,w) <
dist (x,w')) /\
dist (x,w) < t0 /\
dist (x,w) <
dist (x,v0) /\
~(w = v0)
<=>
dist (x,v0) < t0 /\
x
IN VC v0 s /\
~(x
IN
UNIONS
{aff_ge {w} {w1, w2} | w
IN near2t0 v0 s /\
{w, w1, w2}
IN barrier s}) /\
~(x
IN
UNIONS
{aff_ge {w} {w1, w2} | w1,w2 | {w, w1, w2}
IN barrier s}) /\
UNIONS
{aff_ge {w} {w1, w2} | w1,w2 | {w, w1, w2}
IN barrier s}
SUBSET
UNIONS
{aff_ge {w} {w1, w2} | w
IN near2t0 v0 s /\
{w, w1, w2}
IN barrier s} /\
w
IN near2t0 v0 s /\
w
IN s /\
dist (v0,w) < &2 * t0 /\
(!w'. s w' /\ ~(w' = w) ==>
dist (x,w) <
dist (x,w')) /\
dist (x,w) < t0 /\
dist (x,w) <
dist (x,v0) /\
~(w = v0) /\ ~obstructed w x s `] THEN
ONCE_REWRITE_TAC[ MESON[t0; REAL_ARITH ` #1.255 < &2 /\ (! a b c. a < b /\ b < c ==> a < c )` ] `
dist (x,w) < t0 /\
dist (x,w) <
dist (x,v0) /\ last <=>
dist (x,w) < &2 /\
dist (x,w) < t0 /\
dist (x,w) <
dist (x,v0) /\ last`] THEN
REWRITE_TAC[ MESON[
in_VC;
DIST_SYM ] `w
IN s /\
dist (v0,w) < &2 * t0 /\
(!w'. s w' /\ ~(w' = w) ==>
dist (x,w) <
dist (x,w')) /\
dist (x,w) < &2 /\
dist (x,w) < t0 /\
dist (x,w) <
dist (x,v0) /\
~(w = v0) /\
~obstructed w x s <=>
dist (v0,w) < &2 * t0 /\
dist (x,w) < t0 /\
~(w = v0) /\
dist (x,w) <
dist (x,v0) /\
w
IN s /\
(!w'. s w' /\ ~(w' = w) ==>
dist (x,w) <
dist (x,w')) /\
dist (x,w) < &2 /\
~obstructed w x s` ] THEN
REWRITE_TAC[ MESON[
DIST_SYM] `
dist(x,w) < &2 <=>
dist (w,x) < &2 `] THEN
REWRITE_TAC[MESON[
in_VC]` w
IN s /\
(!w'. s w' /\ ~(w' = w) ==>
dist (x,w) <
dist (x,w')) /\
dist (w,x) < &2 /\
~obstructed w x s
<=> w
IN s /\
(!w'. s w' /\ ~(w' = w) ==>
dist (x,w) <
dist (x,w')) /\
dist (w,x) < &2 /\
~obstructed w x s /\ x
IN VC w s ` ] THEN
REWRITE_TAC[ MESON[]` ~(w = v0) /\
dist (x,w) <
dist (x,v0) /\
w
IN s /\
(!w'. s w' /\ ~(w' = w) ==>
dist (x,w) <
dist (x,w')) /\
dist (w,x) < &2 /\
~obstructed w x s /\
x
IN VC w s <=>
dist (x,w) <
dist (x,v0) /\
w
IN s /\
(!w'. s w' /\ ~(w' = w) ==>
dist (x,w) <
dist (x,w')) /\
dist (w,x) < &2 /\
~obstructed w x s /\
~(w = v0) /\ x
IN VC w s `] THEN
ONCE_REWRITE_TAC[ MESON[]`
dist (x,v0) < t0 /\
x
IN VC v0 s /\ last <=>
dist (x,v0) < t0 /\ last /\ x
IN VC v0 s `]
THEN PHA THEN
ONCE_REWRITE_TAC[SET_RULE ` x
IN a /\ x
IN b <=> ~ ( a
INTER b = {} ) /\ x
IN a /\ x
IN b `] THEN
SIMP_TAC[ MESON[
VC_DISJOINT ] ` ~(w = v0) /\
~(
VC w s
INTER VC v0 s = {}) /\
x
IN VC w s /\
x
IN VC v0 s <=> F `]);;
let TRIANGLE_IN_BARRIER' = prove(
`!s v0 v1 v2.
{v0, v1, v2}
IN barrier' v0 s
==> (!xx yy.
~(xx = yy) /\ {xx, yy}
SUBSET {v1, v2, v0}
==> &2 <=
dist (xx,yy) /\
dist (xx,yy) <=
sqrt (&8)) /\
((!aa bb.
aa
IN {v1, v2, v0} /\ bb
IN {v1, v2, v0}
==>
dist (aa,bb) <= #2.51) \/
(?aa bb.
{aa, bb}
SUBSET {v1, v2, v0} /\
#2.51 <
dist (aa,bb) /\
(!x y.
~({x, y} = {aa, bb}) /\ {x, y}
SUBSET {v1, v2, v0}
==>
dist (x,y) <= #2.51))) `,
REWRITE_TAC[ barrier';
let NOV6 = prove(` ! s v0 v1 v2 w. packing s /\
CARD {v0, v1, v2, w} = 4 /\
(!a. a
IN {v1, v2, v0} ==>
dist (w,a) <= #2.51) /\
{v0, v1, v2, w}
SUBSET s /\
(?a b c.
{a, b, c} = {v0, v1, v2} /\
&2 * t0 <= d3 a b /\
d3 a b <=
sqrt (&8) /\
c
IN anchor_points a b s)
==> quarter {v0, v1, v2, w} s`,
REWRITE_TAC[ quarter;
def_simplex] THEN
REWRITE_TAC[ prove(`! v0 v1 v2 w.
CARD {v0, v1, v2, w} = 4 <=> ~(v0 = v1 \/ v0 = v2 \/ v0 = w \/ v1 = v2 \/ v1 = w \/ v2 = w)`,
REWRITE_TAC[
CARD4] THEN SET_TAC[])] THEN
SIMP_TAC[] THEN
NHANH ( SET_RULE ` {a, b, c} = {v0, v1, v2} ==> a
IN {v0,v1,v2,w} /\
b
IN {v0,v1,v2,w} `) THEN
REWRITE_TAC[ MESON[]` (!a . P a ) /\ a /\ (? a b c. Q a b c) <=>
a /\ (?a b c. Q a b c /\ (!a . P a ))`] THEN
REWRITE_TAC[
anchor_points; anchor;
IN_ELIM_THM] THEN PHA THEN
SIMP_TAC[ SET_RULE ` {v1, v2, v0} = {v0, v1, v2}`] THEN
PURE_ONCE_REWRITE_TAC[ MESON []` {a, b, c} = {v0, v1, v2} /\ P {v0, v1, v2}
<=> {a, b, c} = {v0, v1, v2} /\ P {a, b, c}`] THEN
ONCE_REWRITE_TAC[
DIST_SYM] THEN
REWRITE_TAC[ GSYM d3 ] THEN
REWRITE_TAC[ MESON[t0; REAL_ARITH ` #2.51 = &2 * #1.255 `] ` #2.51 = &2 * t0 `] THEN
NHANH (CUTHE4
SHORT_EDGES) THEN
PURE_ONCE_REWRITE_TAC[ SET_RULE ` {a, b, c, w} = w
INSERT {a,b,c} `] THEN
PURE_ONCE_REWRITE_TAC[ GSYM (MESON []` {a, b, c} = {v0, v1, v2} /\ P {v0, v1, v2}
<=> {a, b, c} = {v0, v1, v2} /\ P {a, b, c}`)] THEN MESON_TAC[]);;
let NOV7 = prove(`!s v0 v1 v2 w x .
CARD {v0, v1, v2, w, x} = 5 /\
(!a. a
IN {v1, v2, v0} ==>
dist (w,a) <= #2.51) /\
{v0, v1, v2, w}
SUBSET s /\
(?a b c.
(?q. diagonal a b q s /\ q
IN Q_SYS s /\ c
IN anchor_points a b s) /\
{v0, v1, v2} = {a, b, c})
==> {v0, v1, v2, w}
IN Q_SYS s`,
ONCE_REWRITE_TAC[ SET_RULE ` {v0, v1, v2, w, x} = {x,v0, v1, v2, w}`] THEN
REWRITE_TAC[
CARD5; GSYM
CARD4] THEN
NHANH (CUTHE4
DIA_OF_QUARTER) THEN
NHANH (MESON[diagonal; quarter] `diagonal a b q s ==> packing s `) THEN
PHA THEN REWRITE_TAC[ MESON[]` (?q. diagonal a b q s /\ a1 /\ a2 /\ a3 /\ q
IN Q_SYS s /\ a4) <=>
a1 /\ a2 /\ a3 /\ a4 /\ (?q. diagonal a b q s /\ q
IN Q_SYS s) `] THEN
NHANH ( MESON[
NOV6]`
CARD {v0, v1, v2, w} = 4 /\
(!a. a
IN {v1, v2, v0} ==>
dist (w,a) <= #2.51) /\
{v0, v1, v2, w}
SUBSET s /\
(?a b c.
(packing s /\
&2 * t0 <= d3 a b /\
d3 a b <=
sqrt (&8) /\
c
IN anchor_points a b s /\
(?q. diagonal a b q s /\ q
IN Q_SYS s)) /\
{v0, v1, v2} = {a, b, c})
==> quarter {v0, v1, v2, w} s`) THEN
PHA THEN REWRITE_TAC[ MESON[]` (? a. P a) /\ aa <=> (? a . P a /\ aa )`] THEN
NHANH (MESON[diagonal] ` diagonal a b q s ==> {a,b}
SUBSET q `) THEN
PHA THEN REWRITE_TAC[ MESON[]` (? a. P a) /\ aa <=> (? a . P a /\ aa )`] THEN
NHANH (SET_RULE ` {v0, v1, v2} = {a, b, c} ==> {a,b}
SUBSET {v0,v1,v2,w} `) THEN
REWRITE_TAC[ SET_RULE ` {a, b}
SUBSET q /\ aa /\ bb /\ {a, b}
SUBSET {v0, v1, v2, w} <=>
{a, b}
SUBSET q
INTER {v0, v1, v2, w} /\ aa /\ bb`] THEN
MESON_TAC[lemma7_7_CXRHOVG]);;
let lemma8_3_OVOAHCG =prove(`!s v0 v1 v2 w x. {v0, v1, v2, w}
SUBSET s /\
CARD {v0,v1,v2,w,x} = 5 /\
centered_pac s v0 /\
~(conv {x, w}
INTER aff_ge {v0} {v1, v2} = {}) /\
{v0, v1, v2}
IN barrier' v0 s /\
unobstructed v0 x s /\
dist (x,v0) <
dist (x,v1) /\
dist (x,v0) <
dist (x,v2)
==> ~(x
IN VC w s)`,
REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[ MESON[] ` a ==> ~b <=> a /\ b ==> ~b`] THEN
REWRITE_TAC[
IN_ELIM_THM] THEN
NHANH (MESON[
CARD5] `
CARD {x, w, v0, v1, v2} = 5 ==> ~(x
IN {w,v0,v1,v2})`) THEN
NHANH ( SET_RULE ` ~(x
IN {w,v0,v1,v2}) ==> ~( x = w ) `) THEN
PHA THEN REWRITE_TAC[ MESON[]` unobstructed v0 x s /\ a <=> a /\
unobstructed v0 x s `] THEN REWRITE_TAC[ MESON[]` ~(x = w) /\ a <=> a /\ ~(x = w) `]
THEN PHA THEN
NHANH (SET_RULE ` ~(v0
IN {v1, v2, w, x}) ==> ~( v0 = w )`) THEN
NGOAC THEN MATCH_MP_TAC (MESON[] ` (a ==> c) ==> ( a /\ b ==> c ) `) THEN PHA THEN
REWRITE_TAC[ unobstructed] THEN
REWRITE_TAC[ MESON[] ` ~(v0 = w) /\
centered_pac s v0 /\ aa /\ bb /\ cc /\
x
IN VC w s /\ ~obstructed v0 x s /\ las <=>
aa /\ bb /\ cc /\ las /\ (
centered_pac s v0 /\ ~(v0 = w) /\
~obstructed v0 x s /\ x
IN VC w s )`] THEN
NHANH (CUTHE4 (prove(` ! s v0 w x .
centered_pac s v0 /\ ~(v0 = w) /\ ~obstructed v0 x s /\ x
IN VC w s
==> d3 w x < d3 v0 x`, REWRITE_TAC[
VC;
lambda_x;
IN_ELIM_THM] THEN PURE_ONCE_REWRITE_TAC
[ MESON[] `( !s v0 w x. a v0 x s w ==> b v0 x w ) <=> ( ! s v0 w x. ( d3 v0 x < &2 \/
~(d3 v0 x < &2)) /\ a v0 x s w ==> b v0 x w) `] THEN MESON_TAC[
centered_pac;
trg_d3_sym;
REAL_ARITH` ~(d3 v0 x < &2) /\ d3 w x < &2 ==> d3 w x < d3 v0 x`]))) THEN
NHANH (CUTHE4 TRIANGLE_IN_BARRIER') THEN
PHA THEN
ONCE_REWRITE_TAC[MESON[] ` a1 /\ a2 /\ a3 /\ a4 /\
~(conv {x, w}
INTER aff_ge {v0} {v1, v2} = {}) /\ aa /\ bb /\ cc /\ dd /\ a5 <=> aa /\
bb /\ cc /\ dd /\ ~(conv {x, w}
INTER aff_ge {v0} {v1, v2} = {}) /\ a3 /\ a4 /\
a5 /\ a1 /\ a2`] THEN ONCE_REWRITE_TAC[
trg_d3_sym] THEN REWRITE_TAC[d3] THEN
REWRITE_TAC[MESON[
aff_ge_def;
cone]` aff_ge {v0} {v1, v2} =
cone v0 {v1,v2}`] THEN
ONCE_REWRITE_TAC[ MESON[] `
CARD {v0, v1, v2, w, x} = 5 /\ a1 /\ a2 /\ a3 /\ a4 /\ a5 /\ a6 /\ l <=>
a1 /\ a2 /\ a3 /\ a4 /\ a5 /\ a6 /\
CARD {v0, v1, v2, w, x} = 5 /\ l`] THEN
NHANH (CUTHE5 tarski_UMMNOJN) THEN
PHA THEN REWRITE_TAC[ MESON[] ` ( a \/ b ) /\ c <=> c /\ ( a \/ b ) `] THEN
REWRITE_TAC[ MESON[] `{v0, v1, v2}
IN barrier' v0 s /\ a <=>
a /\ {v0, v1, v2}
IN barrier' v0 s`] THEN
REWRITE_TAC[ barrier';
let BAR_TRI = prove(` ! b s. b
IN barrier s <=> (? x y z . b = {x,y,z} /\ {x,y,z}
IN barrier s)`,
REWRITE_TAC[ barrier ;
IN_ELIM_THM] THEN MESON_TAC[]);;
let NOV20 = prove(` ! v0 x' y z. v0
IN {x', y, z} <=> (?yy zz. {v0, yy, zz} = {x', y, z})`,
REPEAT GEN_TAC THEN
REWRITE_TAC[
EQ_EXPAND] THEN
REWRITE_TAC[SET_RULE `((?yy zz. {v0, yy, zz} = {x', y, z})
==> v0
IN {x', y, z})`] THEN
REWRITE_TAC[IN_SET3] THEN
MESON_TAC[SET_RULE ` x = a
==> {x, b, c} = {a, b, c} /\
{x, b, c} = {b, a, c} /\
{x, b, c} = {b, c, a}`]);;
let IN_VO2_EQ = prove(` ! s v0 x . x
IN voro2 v0 s <=>
(!w. s w /\ ~(w = v0) ==> d3 x v0 < d3 x w) /\ d3 x v0 < &2`,
let IN_BAR_DISTINCT = prove(` ! a b c s. {a,b,c}
IN barrier s ==>
~( a = b\/ b= c \/ c = a)`,
REWRITE_TAC[barrier;
IN_ELIM_THM;
quasi_tri;
set_3elements] THEN
KHANANG THEN REWRITE_TAC[
EXISTS_OR_THM] THEN NHANH ( MESON[]` (?v1 v2 v3.
(a1 /\ a2 v1 v2 v3 /\
~(v1 = v2 \/ v2 = v3 \/ v3 = v1) /\
a3 v1 v2 v3 ) /\
{a, b, c} = {v1, v2, v3}) ==> (?v1 v2 v3.
~(v1 = v2 \/ v2 = v3 \/ v3 = v1) /\
{a, b, c} = {v1, v2, v3})`) THEN
ONCE_REWRITE_TAC[MESON[
EQ_SYM_EQ]` {a,b,c} = {x,y,z} <=> {x,y,z} = {a,b,c}` ] THEN
REWRITE_TAC[
set_3elements] THEN MESON_TAC[
OCT23]);;
let FOUR_POINTS = prove(`!a b c d s.
{a, b, c}
IN barrier s /\ ~(d
IN {a, b, c}) ==>
CARD {a, b, c, d} = 4`,
NHANH (CUTHE4
IN_BAR_DISTINCT) THEN ONCE_REWRITE_TAC[
SET_RULE ` {a,b,c,d} = {d,a,b,c} `] THEN MESON_TAC[
CARD4]);;
let EXISTS_DIA = prove(`! q s. quarter q s ==> (? a b. diagonal a b q s)`,
REWRITE_TAC[quarter; diagonal] THEN
REWRITE_TAC[SET2_SU_EX] THEN
SIMP_TAC[] THEN
NHANH (MESON[
REAL_LE_TRANS]`&2 * t0 <= d3 v w /\ a1 /\ (!x y. P x y ==> d3 x y <= &2 * t0)
==> (!x y. P x y ==> d3 x y <= d3 v w)`) THEN
MP_TAC
PAIR_D3 THEN
REWRITE_TAC[MESON[REAL_ARITH ` a = b ==> a <= b `] ` a ==> b = c:real <=>
a ==> ( b = c /\ b <= c )`] THEN
MESON_TAC[]);;
let IMP_QUA_RE_TE = prove(`!s v0 x y z. v0
IN s /\ packing s /\
{x, y, z}
SUBSET s /\
(!aa bb. aa
IN {y, z, x} /\ bb
IN {y, z, x} ==>
dist (aa,bb) <= #2.51) /\
~(voronoi v0 s
INTER conv {x, y, z} = {}) /\
CARD {x, y, z, v0} = 4 ==>
quasi_reg_tet {v0,x,y,z} s `,
NHANH (SET_RULE ` (! aa bb. aa
IN {y, z, x} /\ bb
IN {y, z, x} ==> P aa bb )
==> P x y /\ P y z /\ P z x `) THEN
ONCE_REWRITE_TAC[ SET_RULE `{a,b,c,d} = {d,a,b,c}`] THEN
REWRITE_TAC[ SET_RULE ` v0
IN s /\ packing s /\
{x, y, z}
SUBSET s /\ l <=> packing s /\ {v0,x,y,z}
SUBSET s /\ l `] THEN
REWRITE_TAC[ MESON[]` a /\ b/\ (
c1 /\ c2 ) /\ d /\ e <=>
c1 /\ a /\ e
/\ b /\ c2 /\d `] THEN
ONCE_REWRITE_TAC[
INTER_COMM] THEN
REWRITE_TAC[ GSYM
db_t0; GSYM d3] THEN PHA THEN
NHANH (SPEC_ALL TCQPONA) THEN
REWRITE_TAC[
quasi_reg_tet;
def_simplex;
CARD4;IN_SET3; IN_SET4;
DE_MORGAN_THM; SET4_SUB_EX;
db_t0] THEN
SIMP_TAC[] THEN PHA THEN DAO THEN
REWRITE_TAC[ MESON[D3_SYM]` (!x'. x' = x \/ x' = y \/ x' = z ==>
d3 x' v0 <= #2.51 /\ &2 <= d3 x' v0) /\ a1 /\
d3 z x <= #2.51 /\
d3 y z <= #2.51 /\
d3 x y <= #2.51 /\
l ==> (!v w. ~(v = w) /\
(v = z \/ v = v0 \/ v = x \/ v = y) /\
(w = z \/ w = v0 \/ w = x \/ w = y)
==> d3 v w <= #2.51)`]);;
let IN_BA_IM_PA_SU = prove(`! s x y z. {x, y, z}
IN barrier s ==>
packing s /\ {x, y, z}
SUBSET s`,
REWRITE_TAC[barrier;
IN_ELIM_THM] THEN
NHANH (SPEC_ALL
CASES_OF_Q_SYS) THEN REPEAT GEN_TAC THEN
REWRITE_TAC[
quasi_tri] THEN KHANANG THEN
REWRITE_TAC[MESON[]` (?a b c. P a b c \/ Q a b c) ==> l <=>
((?a b c . P a b c ) ==> l) /\ ((?a b c. Q a b c) ==> l)`] THEN
REWRITE_TAC[MESON[]` (?v1 v2 v3. (packing s /\
{v1, v2, v3}
SUBSET s /\P v1 v2 v3 ) /\
{x, y, z} = {v1, v2, v3}) ==> packing s /\ {x, y, z}
SUBSET s`] THEN
REWRITE_TAC[
quasi_reg_tet;
strict_qua; quarter; SET3_U_SET1;
def_simplex] THEN
REWRITE_TAC[SET_RULE ` {a,b,c,d}
SUBSET s <=> {a,b,c}
SUBSET s /\ d
IN s `] THEN
MESON_TAC[]);;
let FIRST_NOV22 = prove(` ! s v0 x y z. {x, y, z}
IN barrier s /\
(!xx yy.
~(xx = yy) /\ {xx, yy}
SUBSET {y, z, x}
==> &2 <=
dist (xx,yy) /\
dist (xx,yy) <=
sqrt (&8)) /\
(!aa bb. aa
IN {y, z, x} /\ bb
IN {y, z, x} ==>
dist (aa,bb) <= #2.51) /\
v0
IN s /\
~(voronoi v0 s
INTER conv {x, y, z} = {}) /\
CARD {x, y, z, v0} = 4
==> {v0, x, y, z}
IN Q_SYS s`,
NHANH (SPEC_ALL
IN_BA_IM_PA_SU ) THEN
PHA THEN
ONCE_REWRITE_TAC[MESON[]` a1 /\ a2 /\ a3 /\ a4 /\ a5 /\ a6 /\ a7 /\ a8 <=>
a1 /\ a4 /\ a6 /\ a2 /\ a3 /\ a5 /\ a7 /\ a8 `] THEN
NHANH (SPEC_ALL
IMP_QUA_RE_TE) THEN
MESON_TAC[
COND_Q_SYS]);;
let EXI_THIRD_PO =prove( ` ! a b c x y: A. {x,y}
SUBSET {a,b,c} /\ ~(x=y)
==> (? z. {x,y,z} = {a,b,c} ) `,
REPEAT GEN_TAC THEN
REWRITE_TAC[SET2_SU_EX] THEN REWRITE_TAC[SET2_SU_EX; IN_SET3] THEN
KHANANG THEN REWRITE_TAC[MESON[]`x = a /\ y = a /\ ~(x = y) <=> F`] THEN
MESON_TAC[ PER_SET3]);;
let IMP_QUA = prove(` ! a b c s v0. packing s /\
CARD {v0, a, b, c} = 4 /\
{v0, a, b, c}
SUBSET s /\
d3 a b <= &2 * t0 /\
d3 b c <= &2 * t0 /\ &2 * t0 <= d3 a c /\
d3 a c <=
sqrt (&8) /\
(!x. x
IN {a, b, c} ==> &2 <= d3 x v0 /\ d3 x v0 <= &2 * t0)
==> quarter {v0, a, b, c} s `,
REWRITE_TAC[quarter;
def_simplex;
CARD4; IN_SET3; DE_MORGAN_THM] THEN
SIMP_TAC[] THEN REPEAT GEN_TAC THEN STRIP_TAC THEN
EXISTS_TAC `a:real^3` THEN EXISTS_TAC `c:real^3` THEN
ASM_SIMP_TAC[FOUR_IN] THEN REWRITE_TAC[IN_SET4; PAIR_EQ_EXPAND] THEN
MP_TAC (MESON[REAL_ARITH ` &0 <= #2.51`;
db_t0]` &0 <= &2*t0 `) THEN
ASM_MESON_TAC[D3_SYM;
D3_REFL]);;
let CONSI_OF_LE77 = prove(`!s v0 v4 w x y z.
quarter ({x, y, z}
UNION {v0}) s /\
aa
IN {x, y, z} /\
bb
IN {x, y, z} /\
{x, y, z}
UNION {v4}
IN Q_SYS s /\
diagonal aa bb ({x, y, z}
UNION {v4}) s
==> {x, y, z}
UNION {v0}
IN Q_SYS s`,
REWRITE_TAC[MESON[]` quarter q s /\ a <=>a/\quarter q s `] THEN
PHA THEN NHANH (SET_RULE ` aa
IN {x, y, z} /\ bb
IN {x, y, z} /\ l
==> (!v0 v4.
{aa, bb}
SUBSET
({x, y, z}
UNION {v4})
INTER ({x, y, z}
UNION {v0}))`) THEN
PHA THEN NHANH (MESON[]` diagonal aa bb ({x, y, z}
UNION {v4}) s /\
quarter ({x, y, z}
UNION {v0}) s /\
(!v0 v4. P v0 v4) ==> P v0 v4 `) THEN MESON_TAC[lemma7_7_CXRHOVG]);;
let IMP_IN_Q_SYS = prove( ` ! s v0 x y z . {x, y, z}
IN barrier s /\ v0
IN s /\
~(voronoi v0 s
INTER conv {x, y, z} = {}) /\
CARD {x, y, z, v0} = 4
==> {v0, x, y, z}
IN Q_SYS s`,
NHANH (CUTHE4
TRIANGLE_IN_BARRIER) THEN
KHANANG THEN
REWRITE_TAC[OR_IMP_EX] THEN
REWRITE_TAC[
FIRST_NOV22] THEN
REPEAT GEN_TAC THEN
MATCH_MP_TAC (MESON[]`(a /\ c ==> d ) ==> a /\ b /\ c ==> d `) THEN
NHANH (SPEC_ALL
IN_BA_IM_PA_SU) THEN
REWRITE_TAC[MESON[]` a /\ b /\ c ==> d <=> b ==> a /\ c ==> d`] THEN
NHANH (MESON[
DIST_NZ; REAL_ARITH ` &0 < #2.51 /\ ( a < b /\ b < c ==> a < c )`]`
#2.51 <
dist (aa,bb) ==> ~( aa = bb ) `) THEN
REWRITE_TAC[ MESON[]` a /\ ( b /\ c ) /\ l <=> (a /\ c ) /\ b /\ l`] THEN
NHANH (SPEC_ALL
EXI_THIRD_PO) THEN
REWRITE_TAC[MESON[]` a/\ b/\ c/\ d <=> c /\ a/\b/\d`] THEN
STRIP_TAC THEN REPEAT (FIRST_X_ASSUM MP_TAC) THEN
ONCE_REWRITE_TAC[
EQ_SYM_EQ] THEN
REWRITE_TAC[MESON[]` a = b ==> P a <=> a = b ==> P b `] THEN
ONCE_REWRITE_TAC[
EQ_SYM_EQ] THEN
ONCE_REWRITE_TAC[ SET_RULE ` {x, y, z, v0} = {v0,y,z,x} `] THEN
REWRITE_TAC[
CARD4; GSYM
CARD3] THEN
ONCE_REWRITE_TAC[
EQ_SYM_EQ] THEN
REWRITE_TAC[MESON[]` a = b ==> P a <=> a = b ==> P b `] THEN
REWRITE_TAC[IMP_IMP] THEN PHA THEN
REWRITE_TAC[MESON[]` (! a b. P a b ) /\l <=> l/\(!a b. P a b)`] THEN
PHA THEN
ONCE_REWRITE_TAC[
EQ_SYM_EQ] THEN
REWRITE_TAC[
CARD3] THEN
NHANH (SET_RULE ` ~(aa = bb \/ bb = z' \/ z' = aa) /\
(!x' y'.
~({x', y'} = {aa, bb}) /\ {x', y'}
SUBSET {aa, bb, z'}
==> P x' y') ==>
P bb z' /\ P z' aa `) THEN
PHA THEN
REWRITE_TAC[MESON[
CARD4]` ~(v0
IN {aa, bb, z'}) /\
~(aa = bb \/ bb = z' \/ z' = aa) /\ l <=>
CARD {v0,aa,bb,z'} = 4 /\ l `] THEN
ONCE_REWRITE_TAC[ SET_RULE ` {v0, aa, bb, z'} = {v0,bb,z',aa}`] THEN
SIMP_TAC[SET_RULE ` {y,z,x} = {x,y,z} `] THEN
REWRITE_TAC[ GSYM d3; GSYM
db_t0] THEN
REWRITE_TAC[ GSYM d3; GSYM
db_t0; SET2_SU_EX] THEN
REWRITE_TAC[MESON[]` (aa
IN {x, y, z} /\ bb
IN {x, y, z}) /\a1 /\a2 /\
&2 * t0 < d3 aa bb /\a3 /\ a4 /\ a5 /\ l <=> (aa
IN {x, y, z} /\ bb
IN {x, y, z}
/\ a5 /\ &2 * t0 < d3 aa bb) /\ a1 /\ a2 /\ a3 /\ a4 /\ l `] THEN
NHANH (SPEC_ALL
DIAGONAL_BARRIER) THEN
NHANH (SPEC_ALL
DIA_OF_QUARTER) THEN
REWRITE_TAC[ GSYM
LEFT_AND_EXISTS_THM] THEN
PHA THEN
REWRITE_TAC[MESON[]` d3 aa bb <=
sqrt (&8) /\ l <=>l/\d3 aa bb <=
sqrt (&8)`] THEN
REWRITE_TAC[MESON[]` a = b /\ P b <=> a = b /\ P a`] THEN
PHA THEN REWRITE_TAC[MESON[]` ~ ( a
INTER b = {}) /\ l <=> l/\ ~ ( a
INTER b = {})`]
THEN PHA THEN
REWRITE_TAC[SET_RULE` v0
IN s /\
a1 /\
{aa, bb, z'}
SUBSET s /\
CARD {v0, aa, bb, z'} = 4 /\
l /\
las <=>
l /\ a1 /\
CARD {v0, aa, bb, z'} = 4 /\ {v0, bb, z', aa}
SUBSET s /\ las`] THEN
ONCE_REWRITE_TAC[MESON[SET_RULE ` {v0, aa, bb, z'} = {v0,bb,z',aa}`]`
CARD {v0, aa, bb, z'} =4
<=>
CARD {v0,bb,z',aa} = 4 `] THEN
ONCE_REWRITE_TAC[
INTER_COMM] THEN
ONCE_REWRITE_TAC[MESON[SET_RULE ` {a,b,c} = {b,c,a}`]`
conv {a,b,c} = conv {b,c,a} `] THEN
ONCE_REWRITE_TAC[MESON[D3_SYM]` d3 aa bb <=
sqrt (&8) <=> d3 bb aa <=
sqrt (&8)`] THEN
NHANH (SPEC_ALL CEWWWDQ) THEN
NHANH (REAL_ARITH ` a < b ==> a <= b `) THEN
ONCE_REWRITE_TAC[MESON[]` ( a/\ b ) /\ c <=> c /\ b /\ a `] THEN
PHA THEN
NHANH (MESON[
IMP_QUA; D3_SYM]` packing s /\
CARD {v0, bb, z', aa} = 4 /\
{v0, bb, z', aa}
SUBSET s /\
d3 bb z' <= &2 * t0 /\
d3 z' aa <= &2 * t0 /\
d3 bb aa <=
sqrt (&8) /\ a2 /\
(!x. x
IN {bb, z', aa} ==> &2 <= d3 x v0 /\ d3 x v0 <= &2 * t0) /\
&2 * t0 <= d3 aa bb /\ a1 ==> quarter {v0, bb, z', aa} s`) THEN
REWRITE_TAC[MESON[]`( ? a. P a ) /\ l <=> l /\ (?a. P a) `] THEN
REWRITE_TAC[barrier;
IN_ELIM_THM] THEN
REWRITE_TAC[MESON[]` P b /\ a = b <=> a = b /\ P a `] THEN
REWRITE_TAC[GSYM
LEFT_AND_EXISTS_THM] THEN
PHA THEN
REWRITE_TAC[MESON[]`( a < b /\ l <=> l /\ a < b ) /\
( ( x \/ y ) /\ z <=> z /\ ( x \/ y ))`] THEN
REWRITE_TAC[ MESON[]` a
IN s /\ b /\ c <=> c /\ a
IN s /\ b `] THEN
NHANH (SPEC_ALL
QUA_TRI_EDGE) THEN
PHA THEN
REWRITE_TAC[MESON[
real_lt]`&2 * t0 < d3 aa bb /\
(a1 /\ (!a b. a
IN s /\ b
IN s ==> d3 a b <= &2 * t0) \/ a2) /\
aa
IN s /\
bb
IN s <=>
&2 * t0 < d3 aa bb /\ a2 /\ aa
IN s /\ bb
IN s`] THEN
NHANH (SPEC_ALL
CASES_OF_Q_SYS) THEN
REWRITE_TAC[
LEFT_AND_EXISTS_THM] THEN
KHANANG THEN
NHANH (MESON[SET_RULE ` a
IN s ==> a
IN ( s
UNION t )`;
QUA_RE_TE_EDGE]`
quasi_reg_tet ({x, y, z}
UNION {v4}) s /\
aa
IN {x, y, z} /\
bb
IN {x, y, z} ==> d3 aa bb <= &2 * t0 `) THEN
DAO THEN
REWRITE_TAC [REAL_ARITH ` a <= b <=> ~( b < a ) `] THEN
REWRITE_TAC[MESON[]`(?v4. ~(&2 * t0 < d3 aa bb) /\ P v4 \/ Q v4) /\ a1 /\ &2 * t0 < d3 aa bb <=>
(?v4. Q v4) /\ a1 /\ &2 * t0 < d3 aa bb`] THEN
REWRITE_TAC[
LEFT_AND_EXISTS_THM] THEN
PHA THEN
NHANH (MESON[SET_RULE` a
IN s ==> a
IN ( s
UNION t ) `;
DIAGONAL_STRICT_QUA]`
bb
IN {x, y, z} /\
aa
IN {x, y, z} /\ a1 /\
strict_qua ({x, y, z}
UNION {v4}) s /\
a2 /\
&2 * t0 < d3 aa bb /\ l ==> diagonal aa bb ({x, y, z}
UNION {v4}) s `) THEN
NHANH (MESON[
strict_qua]`
strict_qua q s /\ l ==> quarter q s `) THEN
PHA THEN
REWRITE_TAC[SET_RULE ` {v0, bb, z', aa} = {aa,bb,z'}
UNION {v0}`] THEN
DAO THEN
REWRITE_TAC[MESON[]` a = b /\ l <=> l/\ a= b `] THEN
REWRITE_TAC[MESON[]` quarter q s /\
&2 * t0 < d3 aa bb /\l <=> &2 * t0 < d3 aa bb /\l /\ quarter q s`] THEN
PHA THEN
REWRITE_TAC[MESON[]` quarter ({aa, bb, z'}
UNION {v0}) s /\
a1 /\
{aa, bb, z'} = {x, y, z} /\ l <=> l /\ a1 /\ {aa, bb, z'} = {x, y, z}
/\ quarter ({x, y, z}
UNION {v0}) s`] THEN
REWRITE_TAC[MESON[]` a
IN Q_SYS s /\ l <=> l /\ a
IN Q_SYS s`] THEN
REWRITE_TAC[MESON[]` a
IN s /\ b /\ l <=>l /\ a
IN s /\b `] THEN
REWRITE_TAC[ MESON[]` diagonal aa bb ({x, y, z}
UNION {v4}) s /\ l <=>
l /\ diagonal aa bb ({x, y, z}
UNION {v4}) s`] THEN
PHA THEN
NHANH (MESON[
CONSI_OF_LE77]` quarter ({x, y, z}
UNION {v0}) s /\
aa
IN {x, y, z} /\
bb
IN {x, y, z} /\
{x, y, z}
UNION {v4}
IN Q_SYS s /\a1/\
diagonal aa bb ({x, y, z}
UNION {v4}) s
==> {x, y, z}
UNION {v0}
IN Q_SYS s`) THEN
DAO THEN
REWRITE_TAC[GSYM
RIGHT_AND_EXISTS_THM] THEN
REWRITE_TAC[MESON[SET_RULE ` {x, y, z}
UNION {v0} = {y, v0, x}
UNION {z} `;
CASES_OF_Q_SYS]`
{x, y, z}
UNION {v0}
IN Q_SYS s /\ last
==> {y, v0, x}
UNION {z}
IN Q_SYS s /\
quasi_reg_tet ({y, v0, x}
UNION {z}) s \/
{y, v0, x}
UNION {z}
IN Q_SYS s /\
strict_qua ({y, v0, x}
UNION {z}) s`]);;
let POS_EQ_INV_POS = prove(`!x. &0 < x <=> &0 < &1 / x`,
GEN_TAC THEN EQ_TAC
THENL [REWRITE_TAC[MESON[
REAL_LT_RDIV_0; REAL_ARITH ` &0 < &1 `]`! b. &0 < b
==> &0 < &1 / b `];REWRITE_TAC[] THEN
MESON_TAC[MESON[
REAL_LT_RDIV_0; REAL_ARITH ` &0 < &1 `]` &0 < b
==> &0 < &1 / b `; REAL_FIELD ` &1 / ( &1 / x ) = x ` ]]);;
let AFF_LE_CONE =prove(` ! a b x y z. ~(
conv0 {a,b}
INTER conv {x,y,z} = {})
==> ( b
IN aff_le {x,y,z} {a}) /\ ( b
IN cone a {x,y,z}) `,
REWRITE_TAC[
CONV_SET3;
CONV0_SET2; INTER_DIF_EM_EX;
IN_ELIM_THM] THEN
REPEAT GEN_TAC THEN STRIP_TAC THEN REPEAT (FIRST_X_ASSUM MP_TAC) THEN
REWRITE_TAC[IMP_IMP] THEN PHA THEN REWRITE_TAC[MESON[]` x' = aa /\a1
/\a2 /\a3/\a4 /\ x' = bb <=> x' = aa /\a1 /\a2 /\a3/\a4 /\ aa = bb `]
THEN REWRITE_TAC[ VECTOR_ARITH ` a + b:real^N = c <=> b = c - a`] THEN
NHANH (MESON[
VECTOR_MUL_LCANCEL]` b' % b = a ==> (&1 / b') % (b' % b)
= (&1 / b') % a `) THEN REWRITE_TAC[
VECTOR_MUL_ASSOC;
VECTOR_SUB_LDISTRIB;
VECTOR_ADD_LDISTRIB; simp_def] THEN
NHANH (MESON[
POS_EQ_INV_POS]` &0 < a ==> &0 < &1 / a `) THEN
REWRITE_TAC[VECTOR_ARITH ` a - b % x = a + ( -- b ) % x `] THEN
MP_TAC (REAL_FIELD `! b. &0 < b ==> &1 / b * b = &1 `) THEN
REWRITE_TAC[IMP_IMP] THEN PHA THEN REWRITE_TAC[REAL_ARITH ` a / b * c
= (a * c) / b`; REAL_MUL_LID; VECTOR_ARITH ` a - b % x = a + (--b) % x `] THEN
REWRITE_TAC[REAL_ARITH ` -- ( a / b ) = ( -- a ) / b `] THEN
NHANH (MESON[REAL_ARITH ` a / m + b / m + c / m + d / m = ( a + b + c + d ) / m `]`
b' / b' % b = (a'' / b' % x + b'' / b' % y + c / b' % z) + --a' / b' % a
==> a'' / b' + b'' / b' + c / b' + -- a' / b' = ( a'' + b'' + c + -- a' ) / b' `)
THEN NHANH (MESON[REAL_ARITH ` a' + b' = &1 /\ a'' + b'' + c = &1
==> a'' + b'' + c + --a' = b' `]` a' + b' = &1 /\a1 /\a2 /\a3 /\a4 /\
a'' + b'' + c = &1 /\ l ==> a'' + b'' + c + --a' = b'`) THEN
MP_TAC (REAL_ARITH ` ! a. a < &0 ==> a <= &0 `) THEN REWRITE_TAC[
IN_ELIM_THM]
THEN NHANH (MESON[]`(!b. &0 < b ==> b / b = &1) /\ --a' / b' < &0 /\
&0 < a' /\ &0 < &1 / a' /\ &0 < b' /\ l ==> b' / b' = &1 `) THEN
REWRITE_TAC[MESON[] ` a /\ b' / b' = &1 ==> l <=> b' / b' = &1 ==> a ==> l`] THEN
SIMP_TAC[
VECTOR_MUL_LID] THEN PHA THEN NHANH (MESON[
REAL_LT_DIV]
` &0 < a' /\ &0 < &1 / a' /\ &0 < b' /\ l ==> &0 < a' / b' `) THEN
REWRITE_TAC[REAL_ARITH ` &0 < a' / b' <=> --a' / b' < &0 `] THEN
REWRITE_TAC[ MESON[]` a = x / y /\ x = y <=> a = y/ y /\ x = y `] THEN
REWRITE_TAC[ VECTOR_ARITH ` ((a:real^N) + b ) + c = a + b + c `] THEN
STRIP_TR THENL [MESON_TAC[
VECTOR_MUL_LID];
REWRITE_TAC[
cone; GSYM
aff_ge_def; simp_def;
IN_ELIM_THM]] THEN
MP_TAC
VECTOR_MUL_LID THEN SIMP_TAC[VECTOR_ARITH ` a + b + c + (d:real^N)
= b + c + d + a `] THEN REWRITE_TAC[MESON[]` &0 <= a /\ l <=> l /\ &0 <= a `]
THEN SIMP_TAC[ REAL_ARITH ` a + b + c + d = b + c + d + a `] THEN
REWRITE_TAC[ MESON[]` &0 < a /\ l <=> l /\ &0 < a `] THEN PHA THEN
NHANH (MESON[REAL_ARITH ` &0 < b ==> &0 <= b `;
REAL_LE_DIV]` &0 <= c /\
&0 <= b'' /\ &0 <= a'' /\ &0 < b' /\ &0 < a' ==>
&0 <= a'' / b' /\ &0 <= b''/ b' /\ &0 <= c/ b' `) THEN
NHANH (MESON[REAL_FIELD ` &0 < b' ==> b' / b' = &1 `]`(&0 <= c /\ &0
<= b'' /\ &0 <= a'' /\ &0 < b' /\ &0 < a') ==> b' / b' = &1 `) THEN
REWRITE_TAC[ MESON[]` a / a = &1 /\ l <=> l /\ a / a = &1 `] THEN DAO THEN
REWRITE_TAC[IMP_IMP] THEN REWRITE_TAC[ MESON[]`b' / b' = &1 /\ &0 < a' /\
&0 < b' /\ l <=> &0 < a' /\ l /\ &0 < b' /\ b' / b' = &1 `] THEN
REWRITE_TAC[ MESON[]` a = (b:real^N) /\ l <=> l /\ b = a `] THEN
PHA THEN REWRITE_TAC[ MESON[]` aaa = b' / b' % b /\ &0 < b' /\
b' / b' = &1 <=> &0 < b' /\ b' / b' = &1 /\ aaa = &1 % b `]
THEN REWRITE_TAC[
VECTOR_MUL_LID] THEN MESON_TAC[]);;
let NOVE30 = prove(`! P l. ( ! x y z i j k s. ( P x y z i j k s <=> P y x z j i k s)
/\ ( l x y z <=> l y x z ) ) /\ (! x y z i j k s. i <= j /\ P x y z i j k s ==>
l x y z ) ==> (! x y z i j k s. P x y z i j k s ==> l x y z ) `,
ONCE_REWRITE_TAC[ MESON[]` a ==> (!x y z i j k s. P x y z i j k s ==> l x y z) <=>
(a ==> (!x y z i j k s. i <= j /\ P x y z i j k s ==> l x y z)) /\(a ==>
(!x y z i j k s. ~(i <= j) /\ P x y z i j k s ==> l x y z)) `] THEN REPEAT
GEN_TAC THEN
CONJ_TAC THENL [MESON_TAC[]; MESON_TAC[REAL_ARITH ` ~( a <= b ) ==> b <= a `]]);;
let NOVE31 = prove(`! P l. ( ! x y z i j k s. ( P x y z i j k s <=> P z y x k j i s )
/\ ( l x y z <=> l z y x ) ) /\ (! x y z i j k s. i <= j /\ i <= k /\ P x y z i j k s
==> l x y z ) ==> (! x y z i j k s. i <= j /\ P x y z i j k s ==> l x y z ) `,
ONCE_REWRITE_TAC[ MESON[]` a ==> (!x y z i j k s. P x y z i j k s ==> l x y z) <=>
(a ==> (!x y z i j k s. i <= k /\ P x y z i j k s ==> l x y z)) /\(a ==>
(!x y z i j k s. ~(i <= k) /\ P x y z i j k s ==> l x y z)) `] THEN REPEAT
GEN_TAC THEN CONJ_TAC THENL [MESON_TAC[]; MESON_TAC[
REAL_LE_TRANS;
REAL_ARITH ` ~( a <= b ) ==> b <= a `]]);;
let IMP_IN_AFF4 = prove(` ! s v0 xx x y z. xx
IN cone v0 {x, y, z} /\
~(xx
IN UNIONS {aff_ge {v0} {v1, v2} | v1,v2 | barrier s {v0, v1, v2}}) /\
{v0, x, y, z}
IN Q_SYS s ==> xx
IN aff_gt {v0} {x, y, z}`,
REWRITE_TAC[
cone; GSYM
aff_ge_def; simp_def;
IN_ELIM_THM] THEN
REPLICATE_TAC 3 GEN_TAC THEN REWRITE_TAC[MESON[]` ( ! x y z. (? s i j k.
P s i j k x y z ) /\ Q x y z ==> l x y z) <=> ( ! x y z i j k s.
P s i j k x y z /\ Q x y z ==> l x y z ) `] THEN MATCH_MP_TAC
NOVE30 THEN
CONJ_TAC THENL [MESON_TAC[PER_SET3; REAL_ARITH ` a + b + c = b + a + c ` ;
VECTOR_ARITH `(a:real^N ) + b + c = b + a + c `]; MATCH_MP_TAC
NOVE31 THEN
CONJ_TAC]THENL [MESON_TAC[PER_SET3; REAL_ARITH ` a + b + c = c + b + a ` ;
VECTOR_ARITH `(a:real^N ) + b + c = c + b + a `]; PHA] THEN
REWRITE_TAC[MESON[REAL_ARITH ` &0 <= i <=> i = &0 \/ &0 < i `]`
&0 <= i /\ &0 <= j /\ &0 <= k /\ l <=> ( i = &0 \/ &0 < i ) /\ &0 <= j /\
&0 <= k /\ l `] THEN KHANANG THEN REPEAT GEN_TAC THEN
STRIP_TAC THENL [REPEAT (FIRST_X_ASSUM MP_TAC) THEN REPLICATE_TAC 3 DISCH_TAC
THEN REWRITE_TAC[IMP_IMP] THEN ASM_SIMP_TAC[] THEN REWRITE_TAC[
VECTOR_MUL_LZERO;
VECTOR_ADD_LID; REAL_ADD_LID] THEN REWRITE_TAC[SET_RULE ` {v0, x, y, z} = {v0,y,z}
UNION {x} `] THEN NHANH (SPEC_ALL
IMP_IN_BA) THEN REWRITE_TAC[
IN_UNIONS;
IN_ELIM_THM] THEN REWRITE_TAC[MESON[
IN]` barrier s a /\ l <=> a
IN barrier s /\
l`] THEN PHA THEN REWRITE_TAC[MESON[]` (? t. (? v1 v2 . P v1 v2 /\ t = Q v1 v2 )
/\ xx
IN t ) <=> (? v1 v2. P v1 v2 /\ xx
IN Q v1 v2 ) `] THEN REWRITE_TAC[
IN_ELIM_THM]
THEN MESON_TAC[]; STRIP_TR THEN REWRITE_TAC[MESON[REAL_ARITH ` i <= j /\ &0 < i
==> &0 < j `]` i <= j /\ i <= k /\ &0 < i /\l <=> i <= j /\ i <= k /\ &0 < j /\
&0 < k /\ &0 < i /\ l`] THEN MESON_TAC[]]);;
let VORO2_EX =prove(`! v0 s. voro2 v0 s = {x | (!w. s w /\ ~(w = v0) ==>
d3 x v0 < d3 x w) /\ d3 x v0 < &2} `,
REWRITE_TAC[voro2; voronoi; d3 ]
THEN SET_TAC[]);;
let LEMMA81 = prove(`!(X:real^3 -> bool) Z s v0:real^3 .
centered_pac s v0 /\
Z =
UNIONS {aff_ge {v0} {v1, v2} | v1,v2 | {v0, v1, v2}
IN barrier s} /\
X =
UNIONS
{aff_gt {v0} {v1, v2, v3}
INTER
aff_le {v1, v2, v3} {v0}
INTER
voro2 v0 s | v1,v2,v3 | {v0, v1, v2, v3}
IN Q_SYS s}
==> voro2 v0 s
SUBSET X
UNION Z
UNION VC v0 s`,
REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[SET_RULE ` as
SUBSET a
UNION b
UNION c <=>
( as
DIFF (b
UNION c))
SUBSET a`] THEN REWRITE_TAC[
SUBSET;
IN_DIFF;
IN_UNION;
VC;
lambda_x;
IN_ELIM_THM; voro2;voronoi; GSYM d3; DE_MORGAN_THM;
centered_pac]
THEN ABBREV_TAC ` ketluan x = ((x:real^3)
IN (X:real^3 -> bool))` THEN SIMP_TAC[]
THEN PHA THEN REWRITE_TAC[MESON[]` a /\b/\e/\c==>d <=> c ==> a/\b/\e==>d`] THEN
DISCH_TAC THEN REWRITE_TAC[GSYM (MESON[]` a /\b/\e/\c==>d <=> c ==> a/\b/\e==>d`)]
THEN REWRITE_TAC[MESON[
trg_d3_sym]` d3 x v0 < &2 /\ aa/\
((~(d3 v0 x < &2) \/ l) \/ l') <=> d3 x v0 < &2 /\ aa/\ (l\/ l')`;
IN] THEN
PHA THEN REWRITE_TAC[MESON[]` (!w. s w /\ ~(w = v0) ==> d3 x v0 < d3 x w) /\
aa /\ bb /\ (cc \/ ~(!w. s w /\ dd w /\ ee w /\ ~(w = v0) ==> d3 x v0 < d3 x w)) <=>
(!w. s w /\ ~(w = v0) ==> d3 x v0 < d3 x w) /\ aa /\ bb /\ cc`] THEN
REWRITE_TAC[obstruct] THEN ONCE_REWRITE_TAC[
BAR_TRI] THEN
REWRITE_TAC[ MESON[]`(?bar. (?x y z. bar = {x, y, z} /\ P {x, y, z}) /\ Q bar) <=>
(?x y z. P {x, y, z} /\ Q {x, y, z})`] THEN NHANH (MESON[]` ~(
conv0 {v0, x}
INTER
conv {x', y, z} = {}) ==> v0
IN {x' ,y,z} \/ ~( v0
IN {x', y,z})`) THEN KHANANG THEN
NHANH (MESON[IN_SET3; SET_RULE` x = a ==> {x,b,c} = {a,b,c} /\ {x,b,c} = {b,c,a} /\
{x,b,c} = {b,a,c} `]` x
IN {a,b,c} ==> (? yy zz. {x,yy,zz} = {a,b,c})`) THEN
REWRITE_TAC[
EXISTS_OR_THM] THEN NGOAC THEN REWRITE_TAC[MESON[]`(?x' y z. P {x', y, z}
/\ (?yy zz. {x, yy, zz} = {x', y, z})) <=> (?y z. P {x, y, z})`] THEN
NHANH (CUTHE4
IN_AFF_GE_CON) THEN PHA THEN
REWRITE_TAC[SET_RULE` ~UNIONS {aff_ge {v0} {v1, v2} | v1,v2 | barrier s {v0, v1, v2}} x /\
((?y z. {v0, y, z}
IN barrier s /\ aaa y z /\ x
IN aff_ge {v0} {y, z} /\
bbb y z) \/ last) <=> ~UNIONS {aff_ge {v0} {v1, v2} | v1,v2 | barrier s {v0, v1, v2}} x /\
last`] THEN REWRITE_TAC[DE_MORGAN_THM] THEN SIMP_TAC[GSYM
NOV20] THEN
REWRITE_TAC[d3; GSYM
IN_VO_EQ] THEN NHANH (MESON[
X_IN_VOR_X;
VORONOI_CONV]` x
IN voronoi v0 s
==> v0
IN voronoi v0 s /\
convex (voronoi v0 s )`) THEN
NHANH (MESON[
CONVEX_IM_CONV02_SU ]` x
IN voronoi v0 s /\ v0
IN voronoi v0 s /\
convex (voronoi v0 s) ==>
conv0 {v0,x}
SUBSET voronoi v0 s `) THEN PHA THEN
DISCH_TAC THEN GEN_TAC THEN STRIP_TAC THENL [REPEAT (FIRST_X_ASSUM MP_TAC) THEN
REWRITE_TAC[ IMP_IMP] THEN PHA THEN NHANH (SET_RULE`
conv0 {v0, x}
SUBSET voronoi v0 s
/\a1 /\a2 /\a3 /\ ~(
conv0 {v0, x}
INTER conv {x', y, z} = {}) /\ l ==>
~( voronoi v0 s
INTER conv {x', y, z} = {})`) THEN NHANH (MESON[
FOUR_POINTS]
` {x', y, z}
IN barrier s /\ a1 /\ ~(v0
IN {x', y, z}) ==>
CARD {x',y,z, v0} = 4 `)
THEN PHA THEN NHANH (SET_RULE `
conv0 {v0, x}
SUBSET s /\ a1 /\a2 /\a3 /\
~(
conv0 {v0, x}
INTER s1 = {}) /\ l ==> ~( s
INTER s1 = {}) `) THEN PHA THEN
REWRITE_TAC[MESON[]`( s x /\ l <=>l/\ s x)/\ (a
IN barrier s /\ l <=>
l /\ a
IN barrier s) `] THEN NHANH (SPEC_ALL (REWRITE_RULE[
CONV3_EQ]
IN_AFF_GE_CON))
THEN PHA THEN REWRITE_TAC[SET_RULE ` ~UNIONS {aff_ge {v0} {v1, v2} | v1,v2 |
barrier s {v0, v1, v2}} x /\ a1 /\ x
IN aff_ge {v0} {y, z} /\
a2 /\ a3/\ {v0, y, z}
IN barrier s /\ a4 <=> F `] ; REPEAT (FIRST_X_ASSUM MP_TAC)]
THEN REWRITE_TAC[ IMP_IMP] THEN PHA THEN
NHANH (SET_RULE`
conv0 {v0, x}
SUBSET voronoi v0 s /\a1 /\a2 /\a3 /\
~(
conv0 {v0, x}
INTER conv {x', y, z} = {}) /\ l ==>
~( voronoi v0 s
INTER conv {x', y, z} = {})`) THEN
NHANH (MESON[
FOUR_POINTS]` {x', y, z}
IN barrier s /\ a1 /\
~(v0
IN {x', y, z}) ==>
CARD {x',y,z, v0} = 4 `) THEN PHA THEN NHANH (SET_RULE `
conv0 {v0, x}
SUBSET s /\ a1 /\a2 /\a3 /\ ~(
conv0 {v0, x}
INTER s1 = {}) /\ l
==> ~( s
INTER s1 = {}) `) THEN PHA THEN REWRITE_TAC[MESON[]`( s x /\ l <=>l/\
s x)/\ (a
IN barrier s /\ l <=> l /\ a
IN barrier s) `] THEN PHA THEN
NHANH (MESON[
IMP_IN_Q_SYS;
IN]`
CARD {x', y, z, v0} = 4 /\
~(voronoi v0 s
INTER conv {x', y, z} = {}) /\ {x', y, z}
IN barrier s /\
s v0 ==> {v0,x',y,z}
IN Q_SYS s `) THEN NHANH (SPEC_ALL
AFF_LE_CONE) THEN PHA THEN
ONCE_REWRITE_TAC[MESON[
IN] ` ~
UNIONS s x <=> ~ ( x
IN UNIONS s ) `] THEN
ONCE_REWRITE_TAC[MESON[]` a1 /\a /\ b /\ x
IN cone v0 {x', y, z} /\ l <=>a /\ b /\ l /\
x
IN cone v0 {x', y, z} /\ a1 `] THEN PHA THEN REWRITE_TAC[MESON[]` a
IN Q_SYS s /\
b /\ c <=> b /\ c /\ a
IN Q_SYS s`] THEN NHANH (SPEC_ALL
IMP_IN_AFF4) THEN
NGOAC THEN REWRITE_TAC[MESON[]` (a /\ b ) /\ x
IN aff_gt {v0} {x', y, z} <=>
x
IN aff_gt {v0} {x', y, z}/\ b/\ a `] THEN PHA THEN DAO THEN
REWRITE_TAC[GSYM
VORO2_EX] THEN REWRITE_TAC[prove(`
dist (x,v0) < &2 /\a1/\a2/\a3 /\
x
IN voronoi v0 s /\ l <=> a1/\a2/\a3 /\ l /\ x
IN voro2 v0 s`, REWRITE_TAC[GSYM d3;
voro2;
IN_ELIM_THM] THEN MESON_TAC[])] THEN REWRITE_TAC[MESON[]`x
IN aff_le a s /\
l <=> l /\ x
IN aff_le a s `] THEN DAO THEN ONCE_REWRITE_TAC[
EQ_SYM_EQ] THEN
SIMP_TAC[] THEN ONCE_REWRITE_TAC[MESON[]` (! x. P x ) /\ a = b /\ l <=> b = a /\ l /\
(! x . P x )`] THEN SIMP_TAC[] THEN MATCH_MP_TAC (MESON[]` ( a1 /\a2/\a3/\a4 ==> l )
==> ( a1/\a2/\a3/\a4/\a5 ==> l ) `) THEN REWRITE_TAC[
IN_UNIONS;
IN_ELIM_THM] THEN
REWRITE_TAC[ MESON[]` (?t. (? a b c. P a b c /\ t = Q a b c ) /\ x
IN t )
<=> (? a b c. P a b c /\ x
IN Q a b c ) `] THEN REWRITE_TAC[
IN_INTER] THEN
SET_TAC[]);;