(* ========================================================================= *)
(* Pick's theorem. *)
(* ========================================================================= *)
needs "Multivariate/polytope.ml";;
needs "Multivariate/measure.ml";;
needs "Multivariate/transcendentals.ml";;
prioritize_real();;
(* ------------------------------------------------------------------------- *)
(* Misc lemmas. *)
(* ------------------------------------------------------------------------- *)
let CONVEX_HULL_3_0 = prove
(`!a b:real^N.
convex hull {vec 0,a,b} =
{x % a + y % b | &0 <= x /\ &0 <= y /\ x + y <= &1}`,
REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[SET_RULE `{c,a,b} = {a,b,c}`] THEN
REWRITE_TAC[
CONVEX_HULL_3;
EXTENSION;
IN_ELIM_THM] THEN
X_GEN_TAC `y:real^N` THEN
AP_TERM_TAC THEN REWRITE_TAC[
FUN_EQ_THM] THEN X_GEN_TAC `x:real` THEN
AP_TERM_TAC THEN REWRITE_TAC[
FUN_EQ_THM] THEN X_GEN_TAC `y:real` THEN
REWRITE_TAC[
VECTOR_MUL_RZERO;
VECTOR_ADD_RID] THEN
EQ_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THENL
[ASM_ARITH_TAC; EXISTS_TAC `&1 - x - y` THEN ASM_ARITH_TAC]);;
let INTERIOR_CONVEX_HULL_3_0 = prove
(`!a b:real^2.
~(collinear {vec 0,a,b})
==> interior(convex hull {vec 0,a,b}) =
{x % a + y % b | &0 < x /\ &0 < y /\ x + y < &1}`,
REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[SET_RULE `{c,a,b} = {a,b,c}`] THEN
STRIP_TAC THEN ASM_SIMP_TAC[
INTERIOR_CONVEX_HULL_3] THEN
REWRITE_TAC[TAUT `a /\ x = &1 /\ b <=> x = &1 /\ a /\ b`] THEN
REWRITE_TAC[
VECTOR_MUL_RZERO;
VECTOR_ADD_RID] THEN
REWRITE_TAC[REAL_ARITH `x + y + z = &1 <=> &1 - x - y = z`;
UNWIND_THM1] THEN
REWRITE_TAC[
EXTENSION;
IN_ELIM_THM] THEN
GEN_TAC THEN REPEAT(AP_TERM_TAC THEN ABS_TAC) THEN
EQ_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
ASM_REAL_ARITH_TAC);;
(* ------------------------------------------------------------------------- *)
(* Decomposing an additive function on a triangle. *)
(* ------------------------------------------------------------------------- *)
let TRIANGLE_DECOMPOSITION = prove
(`!a b c d:real^2.
d
IN convex hull {a,b,c}
==> (convex hull {a,b,c} =
convex hull {d,b,c}
UNION
convex hull {d,a,c}
UNION
convex hull {d,a,b})`,
let TRIANGLE_ADDITIVE_DECOMPOSITION = prove
(`!f:(real^2->bool)->real a b c d.
(!s t. compact s /\ compact t
==> f(s
UNION t) = f(s) + f(t) - f(s
INTER t)) /\
~(a = b) /\ ~(a = c) /\ ~(b = c) /\
~affine_dependent {a,b,c} /\ d
IN convex hull {a,b,c}
==> f(convex hull {a,b,c}) =
(f(convex hull {a,b,d}) +
f(convex hull {a,c,d}) +
f(convex hull {b,c,d})) -
(f(convex hull {a,d}) +
f(convex hull {b,d}) +
f(convex hull {c,d})) +
f(convex hull {d})`,
(* ------------------------------------------------------------------------- *)
(* Vectors all of whose coordinates are integers. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Properties of a basis for the integer lattice. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Pick's theorem for an elementary triangle. *)
(* ------------------------------------------------------------------------- *)
let PICK_ELEMENTARY_TRIANGLE_0 = prove
(`!a b:real^2.
{x | x
IN convex hull {vec 0,a,b} /\
integral_vector x} = {vec 0,a,b}
==> measure(convex hull {vec 0,a,b}) =
if collinear {vec 0,a,b} then &0 else &1 / &2`,
REPEAT GEN_TAC THEN COND_CASES_TAC THEN
ASM_SIMP_TAC[
MEASURE_EQ_0;
COLLINEAR_IMP_NEGLIGIBLE;
COLLINEAR_CONVEX_HULL_COLLINEAR] THEN
POP_ASSUM MP_TAC THEN
MAP_EVERY (fun t ->
ASM_CASES_TAC t THENL [ASM_REWRITE_TAC[
INSERT_AC;
COLLINEAR_2]; ALL_TAC])
[`a:real^2 = vec 0`; `b:real^2 = vec 0`; `a:real^2 = b`] THEN
DISCH_TAC THEN SUBGOAL_THEN `independent {a:real^2,b}` ASSUME_TAC THENL
[UNDISCH_TAC `~collinear{vec 0:real^2, a, b}` THEN
REWRITE_TAC[independent; CONTRAPOS_THM] THEN
REWRITE_TAC[dependent;
EXISTS_IN_INSERT;
NOT_IN_EMPTY] THEN STRIP_TAC THENL
[ONCE_REWRITE_TAC[SET_RULE `{c,a,b} = {c,b,a}`]; ALL_TAC] THEN
ASM_SIMP_TAC[
COLLINEAR_3_AFFINE_HULL] THEN
ASM_SIMP_TAC[
AFFINE_HULL_EQ_SPAN;
HULL_INC;
IN_INSERT] THEN
FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP
(SET_RULE `a
IN s ==> s
SUBSET t ==> a
IN t`)) THEN
MATCH_MP_TAC
SPAN_MONO THEN SET_TAC[];
ALL_TAC] THEN
SUBGOAL_THEN `span{a,b} = (:real^2)` ASSUME_TAC THENL
[MP_TAC(ISPECL [`(:real^2)`; `{a:real^2,b}`]
CARD_EQ_DIM) THEN
ASM_REWRITE_TAC[
SUBSET_UNIV;
SUBSET;
EXTENSION;
IN_ELIM_THM;
IN_UNIV] THEN
DISCH_THEN MATCH_MP_TAC THEN
REWRITE_TAC[
HAS_SIZE;
FINITE_INSERT;
FINITE_EMPTY] THEN
SIMP_TAC[
CARD_CLAUSES;
FINITE_INSERT;
FINITE_EMPTY;
IN_INSERT] THEN
ASM_REWRITE_TAC[
NOT_IN_EMPTY;
DIM_UNIV; DIMINDEX_2; ARITH];
ALL_TAC] THEN
REWRITE_TAC[GSYM
SUBSET_ANTISYM_EQ;
SUBSET;
FORALL_IN_INSERT;
FORALL_IN_GSPEC] THEN
REWRITE_TAC[
IN_ELIM_THM;
NOT_IN_EMPTY;
IN_INSERT] THEN STRIP_TAC THEN
MP_TAC(ISPEC `\x:real^2. transp(vector[a;b]:real^2^2) ** x`
INTEGRAL_BASIS_UNIMODULAR) THEN
REWRITE_TAC[
MATRIX_OF_MATRIX_VECTOR_MUL;
MATRIX_VECTOR_MUL_LINEAR] THEN
REWRITE_TAC[
DET_2;
MEASURE_TRIANGLE;
VECTOR_2;
DET_TRANSP;
VEC_COMPONENT] THEN
ANTS_TAC THENL [ALL_TAC; REAL_ARITH_TAC] THEN
MATCH_MP_TAC
SUBSET_ANTISYM THEN REWRITE_TAC[
SUBSET;
FORALL_IN_IMAGE] THEN
CONJ_TAC THENL
[REWRITE_TAC[
IN] THEN
SIMP_TAC[
LINEAR_INTEGRAL_VECTOR;
MATRIX_VECTOR_MUL_LINEAR;
LAMBDA_BETA;
MATRIX_OF_MATRIX_VECTOR_MUL; transp; DIMINDEX_2; ARITH] THEN
MAP_EVERY UNDISCH_TAC
[`
integral_vector(a:real^2)`; `
integral_vector(b:real^2)`] THEN
REWRITE_TAC[
integral_vector;
IMP_CONJ;
RIGHT_FORALL_IMP_THM] THEN
REWRITE_TAC[IMP_IMP;
FORALL_2; DIMINDEX_2;
VECTOR_2] THEN
REWRITE_TAC[
CONJ_ACI];
ALL_TAC] THEN
REWRITE_TAC[
IN_IMAGE] THEN REWRITE_TAC[
IN] THEN
X_GEN_TAC `x:real^2` THEN DISCH_TAC THEN REWRITE_TAC[
EXISTS_VECTOR_2] THEN
REWRITE_TAC[
MATRIX_VECTOR_COLUMN;
TRANSP_TRANSP] THEN
REWRITE_TAC[DIMINDEX_2;
VSUM_2;
VECTOR_2;
integral_vector;
FORALL_2] THEN
SUBGOAL_THEN `(x:real^2)
IN span{a,b}` MP_TAC THENL
[ASM_REWRITE_TAC[
IN_UNIV]; ALL_TAC] THEN
REWRITE_TAC[
SPAN_2;
IN_UNIV;
IN_ELIM_THM] THEN
MATCH_MP_TAC
MONO_EXISTS THEN X_GEN_TAC `u:real` THEN
MATCH_MP_TAC
MONO_EXISTS THEN X_GEN_TAC `v:real` THEN
DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
FIRST_ASSUM(MP_TAC o SPEC `frac u % a + frac v % b:real^2`) THEN
FIRST_X_ASSUM(MP_TAC o SPEC
`(&1 - frac u) % a + (&1 - frac v) % b:real^2`) THEN
MATCH_MP_TAC(TAUT
`b' /\ (b' ==> b) /\ (a \/ a') /\ (c \/ c' ==> x)
==> (a /\ b ==> c) ==> (a' /\ b' ==> c') ==> x`) THEN
REPEAT CONJ_TAC THENL
[SUBGOAL_THEN `
integral_vector(floor u % a + floor v % b:real^2)`
MP_TAC THENL
[MAP_EVERY UNDISCH_TAC
[`
integral_vector(a:real^2)`; `
integral_vector(b:real^2)`] THEN
SIMP_TAC[
integral_vector; DIMINDEX_2;
FORALL_2;
VECTOR_ADD_COMPONENT;
VECTOR_MUL_COMPONENT] THEN
SIMP_TAC[
FLOOR;
INTEGER_CLOSED];
UNDISCH_TAC `
integral_vector(x:real^2)` THEN REWRITE_TAC[IMP_IMP] THEN
DISCH_THEN(MP_TAC o MATCH_MP
INTEGRAL_VECTOR_SUB) THEN
ASM_REWRITE_TAC[VECTOR_ARITH
`(x % a + y % b) - (u % a + v % b) = (x - u) % a + (y - v) % b`] THEN
MATCH_MP_TAC EQ_IMP THEN AP_TERM_TAC THEN BINOP_TAC THEN
AP_THM_TAC THEN AP_TERM_TAC THEN
REWRITE_TAC[REAL_ARITH `u - x:real = y <=> u = x + y`] THEN
REWRITE_TAC[GSYM
FLOOR_FRAC]];
REWRITE_TAC[VECTOR_ARITH
`(&1 - u) % a + (&1 - v) % b = (a + b) - (u % a + v % b)`] THEN
ASM_SIMP_TAC[
INTEGRAL_VECTOR_ADD;
INTEGRAL_VECTOR_SUB];
REWRITE_TAC[
CONVEX_HULL_3_0;
IN_ELIM_THM] THEN
SUBGOAL_THEN
`&0 <= frac u /\ &0 <= frac v /\ frac u + frac v <= &1 \/
&0 <= &1 - frac u /\ &0 <= &1 - frac v /\
(&1 - frac u) + (&1 - frac v) <= &1`
MP_TAC THENL
[MP_TAC(SPEC `u:real`
FLOOR_FRAC) THEN
MP_TAC(SPEC `v:real`
FLOOR_FRAC) THEN REAL_ARITH_TAC;
MESON_TAC[]];
REWRITE_TAC
[VECTOR_ARITH `x % a + y % b = a <=> (x - &1) % a + y % b = vec 0`;
VECTOR_ARITH `x % a + y % b = b <=> x % a + (y - &1) % b = vec 0`] THEN
ASM_SIMP_TAC[
INDEPENDENT_2; GSYM
REAL_FRAC_EQ_0] THEN
MP_TAC(SPEC `u:real`
FLOOR_FRAC) THEN
MP_TAC(SPEC `v:real`
FLOOR_FRAC) THEN REAL_ARITH_TAC]);;
(* ------------------------------------------------------------------------- *)
(* Our form of Pick's theorem holds degenerately for a flat triangle. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Pick's theorem for a triangle. *)
(* ------------------------------------------------------------------------- *)
let PICK_TRIANGLE_ALT = prove
(`!a b c:real^2.
integral_vector a /\
integral_vector b /\
integral_vector c
==> measure(convex hull {a,b,c}) =
&(
CARD {x | x
IN convex hull {a,b,c} /\
integral_vector x}) -
(&(
CARD {x | x
IN convex hull {b,c} /\
integral_vector x}) +
&(
CARD {x | x
IN convex hull {a,c} /\
integral_vector x}) +
&(
CARD {x | x
IN convex hull {a,b} /\
integral_vector x})) / &2 +
&1 / &2`,
let tac a bc =
MATCH_MP_TAC
CARD_PSUBSET THEN
REWRITE_TAC[
FINITE_TRIANGLE_INTEGER_POINTS] THEN
REWRITE_TAC[
PSUBSET] THEN CONJ_TAC THENL
[MATCH_MP_TAC(SET_RULE
`s
SUBSET t ==> {x | x
IN s /\ P x}
SUBSET {x | x
IN t /\ P x}`) THEN
MATCH_MP_TAC
HULL_MINIMAL THEN REWRITE_TAC[
CONVEX_CONVEX_HULL] THEN
ASM_SIMP_TAC[
INSERT_SUBSET;
EMPTY_SUBSET;
IN_INSERT;
HULL_INC];
DISCH_TAC] THEN
SUBGOAL_THEN(subst[bc,`bc:real^2->bool`]
`convex hull {a:real^2,b,c} = convex hull bc`)
ASSUME_TAC THENL
[MATCH_MP_TAC
CONVEX_HULLS_EQ THEN
ASM_SIMP_TAC[
HULL_INC;
IN_INSERT;
INSERT_SUBSET;
EMPTY_SUBSET] THEN
SUBGOAL_THEN(subst [a,`x:real^2`] `x
IN convex hull {a:real^2,b,c}`)
MP_TAC THENL
[SIMP_TAC[
HULL_INC;
IN_INSERT]; ASM SET_TAC[]];
ALL_TAC] THEN
MP_TAC(ISPECL [`{a:real^2,b,c}`; a]
EXTREME_POINT_OF_CONVEX_HULL_AFFINE_INDEPENDENT) THEN
ASM_REWRITE_TAC[
IN_INSERT] THEN
DISCH_THEN(MP_TAC o MATCH_MP
EXTREME_POINT_OF_CONVEX_HULL) THEN
ASM_REWRITE_TAC[
IN_INSERT;
NOT_IN_EMPTY] in
REPEAT GEN_TAC THEN
WF_INDUCT_TAC `
CARD {x:real^2 | x
IN convex hull {a,b,c} /\
integral_vector x}` THEN
ASM_CASES_TAC `collinear{a:real^2,b,c}` THENL
[FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [
COLLINEAR_BETWEEN_CASES]) THEN
REWRITE_TAC[
BETWEEN_IN_SEGMENT] THEN REPEAT STRIP_TAC THENL
[MP_TAC(ISPECL [`b:real^2`; `c:real^2`; `a:real^2`]
PICK_TRIANGLE_FLAT);
MP_TAC(ISPECL [`a:real^2`; `c:real^2`; `b:real^2`]
PICK_TRIANGLE_FLAT);
MP_TAC(ISPECL [`a:real^2`; `b:real^2`; `c:real^2`]
PICK_TRIANGLE_FLAT)] THEN
(ANTS_TAC THENL [ASM_MESON_TAC[
SEGMENT_SYM]; ALL_TAC] THEN
REWRITE_TAC[SET_RULE `{x | x
IN s /\ P x} = s
INTER P`] THEN
REWRITE_TAC[
INSERT_AC;
REAL_ADD_AC]);
ALL_TAC] THEN
UNDISCH_TAC `~collinear{a:real^2,b,c}` THEN
MAP_EVERY
(fun t -> ASM_CASES_TAC t THENL
[ASM_REWRITE_TAC[
INSERT_AC;
COLLINEAR_2]; ALL_TAC])
[`a:real^2 = b`; `a:real^2 = c`; `b:real^2 = c`] THEN
DISCH_TAC THEN STRIP_TAC THEN
ASM_CASES_TAC
`{x:real^2 | x
IN convex hull {a, b, c} /\
integral_vector x} =
{a,b,c}`
THENL
[ASM_SIMP_TAC[
PICK_ELEMENTARY_TRIANGLE] THEN
SUBGOAL_THEN
`{x | x
IN convex hull {b,c} /\
integral_vector x} = {b,c} /\
{x | x
IN convex hull {a,c} /\
integral_vector x} = {a,c} /\
{x | x
IN convex hull {a,b} /\
integral_vector x} = {a:real^2,b}`
(REPEAT_TCL CONJUNCTS_THEN SUBST1_TAC) THENL
[REPEAT CONJ_TAC THEN
(FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (SET_RULE
`{x | x
IN cs /\ P x} = s
==> t
SUBSET s /\ t
SUBSET ct /\ ct
SUBSET cs /\
(s
DIFF t)
INTER ct = {}
==> {x | x
IN ct /\ P x} = t`)) THEN
REPEAT CONJ_TAC THENL
[SET_TAC[];
MATCH_ACCEPT_TAC
HULL_SUBSET;
MATCH_MP_TAC
HULL_MONO THEN SET_TAC[];
ASM_REWRITE_TAC[
INSERT_DIFF;
IN_INSERT;
NOT_IN_EMPTY;
EMPTY_DIFF] THEN
MATCH_MP_TAC(SET_RULE `~(x
IN s) ==> {x}
INTER s = {}`) THEN
REWRITE_TAC[GSYM
SEGMENT_CONVEX_HULL; GSYM
BETWEEN_IN_SEGMENT] THEN
DISCH_THEN(MP_TAC o MATCH_MP
BETWEEN_IMP_COLLINEAR) THEN
UNDISCH_TAC `~collinear{a:real^2,b,c}` THEN REWRITE_TAC[
INSERT_AC]]);
SIMP_TAC[
CARD_CLAUSES;
FINITE_INSERT;
FINITE_EMPTY] THEN
ASM_REWRITE_TAC[
IN_INSERT;
NOT_IN_EMPTY] THEN
CONV_TAC NUM_REDUCE_CONV THEN CONV_TAC REAL_RAT_REDUCE_CONV];
ALL_TAC] THEN
SUBGOAL_THEN
`?d:real^2. d
IN convex hull {a, b, c} /\
integral_vector d /\
~(d = a) /\ ~(d = b) /\ ~(d = c)`
STRIP_ASSUME_TAC THENL
[FIRST_X_ASSUM(MP_TAC o MATCH_MP (SET_RULE
`~(s = t) ==> t
SUBSET s ==> ?d. d
IN s /\ ~(d
IN t)`)) THEN
REWRITE_TAC[
SUBSET;
FORALL_IN_INSERT;
IN_ELIM_THM] THEN
ASM_SIMP_TAC[
IN_INSERT;
NOT_IN_EMPTY; DE_MORGAN_THM; GSYM
CONJ_ASSOC] THEN
DISCH_THEN MATCH_MP_TAC THEN SIMP_TAC[
HULL_INC;
IN_INSERT];
ALL_TAC] THEN
FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE RAND_CONV
[
COLLINEAR_3_EQ_AFFINE_DEPENDENT]) THEN
ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
MP_TAC(ISPECL
[`measure:(real^2->bool)->real`;
`a:real^2`; `b:real^2`; `c:real^2`; `d:real^2`]
TRIANGLE_ADDITIVE_DECOMPOSITION) THEN
SIMP_TAC[
MEASURE_UNION;
MEASURABLE_COMPACT] THEN
ASM_REWRITE_TAC[] THEN DISCH_THEN SUBST1_TAC THEN
REWRITE_TAC[
MEASURE_CONVEX_HULL_2_TRIVIAL;
REAL_ADD_RID;
REAL_SUB_RZERO] THEN
MP_TAC(ISPECL
[`\s. &(
CARD {x:real^2 | x
IN s /\
integral_vector x})`;
`a:real^2`; `b:real^2`; `c:real^2`; `d:real^2`]
TRIANGLE_ADDITIVE_DECOMPOSITION) THEN
ASM_REWRITE_TAC[] THEN ANTS_TAC THENL
[REWRITE_TAC[SET_RULE `{x | x
IN (s
UNION t) /\ P x} =
{x | x
IN s /\ P x}
UNION {x | x
IN t /\ P x}`;
SET_RULE `{x | x
IN (s
INTER t) /\ P x} =
{x | x
IN s /\ P x}
INTER {x | x
IN t /\ P x}`] THEN
REPEAT STRIP_TAC THEN
REWRITE_TAC[REAL_ARITH `x:real = y + z - w <=> x + w = y + z`] THEN
REWRITE_TAC[REAL_OF_NUM_ADD; REAL_OF_NUM_EQ] THEN
MATCH_MP_TAC(ARITH_RULE
`x:num = (y + z) - w /\ w <= z ==> x + w = y + z`) THEN
CONJ_TAC THENL
[MATCH_MP_TAC
CARD_UNION_GEN;
MATCH_MP_TAC
CARD_SUBSET THEN REWRITE_TAC[
INTER_SUBSET]] THEN
ASM_SIMP_TAC[
FINITE_BOUNDED_INTEGER_POINTS;
COMPACT_IMP_BOUNDED];
DISCH_THEN SUBST1_TAC] THEN
FIRST_X_ASSUM(fun th ->
MP_TAC(ISPECL [`a:real^2`; `b:real^2`; `d:real^2`] th) THEN
MP_TAC(ISPECL [`a:real^2`; `c:real^2`; `d:real^2`] th) THEN
MP_TAC(ISPECL [`b:real^2`; `c:real^2`; `d:real^2`] th)) THEN
ASM_REWRITE_TAC[] THEN
ANTS_TAC THENL [tac `a:real^2` `{b:real^2,c,d}`; DISCH_THEN SUBST1_TAC] THEN
ANTS_TAC THENL [tac `b:real^2` `{a:real^2,c,d}`; DISCH_THEN SUBST1_TAC] THEN
ANTS_TAC THENL [tac `c:real^2` `{a:real^2,b,d}`; DISCH_THEN SUBST1_TAC] THEN
SUBGOAL_THEN `{x:real^2 | x
IN convex hull {d} /\
integral_vector x} = {d}`
SUBST1_TAC THENL
[REWRITE_TAC[
CONVEX_HULL_SING] THEN ASM SET_TAC[]; ALL_TAC] THEN
SIMP_TAC[
CARD_CLAUSES;
FINITE_RULES;
NOT_IN_EMPTY] THEN
CONV_TAC NUM_REDUCE_CONV THEN
REWRITE_TAC[SET_RULE `{x | x
IN s /\ P x} = s
INTER P`] THEN
REWRITE_TAC[
INSERT_AC] THEN REAL_ARITH_TAC);;
(* ------------------------------------------------------------------------- *)
(* Parity lemma for segment crossing a polygon. *)
(* ------------------------------------------------------------------------- *)
let PARITY_LEMMA = prove
(`!a b c d p x:real^2.
simple_path(p ++ linepath(a,b)) /\
pathstart p = b /\ pathfinish p = a /\
segment(a,b)
INTER segment(c,d) = {x} /\
segment[c,d]
INTER path_image p = {}
==> (c
IN inside(
path_image(p ++ linepath(a,b))) <=>
d
IN outside(
path_image(p ++ linepath(a,b))))`,
let lemma = prove
(`!a b x y:real^N.
collinear{y,a,b} /\ between x (a,b) /\
dist(y,x) < dist(x,b) /\ dist(y,x) < dist(x,a)
==> y IN segment(a,b)`,
REPEAT STRIP_TAC THEN MATCH_MP_TAC COLLINEAR_DIST_IN_OPEN_SEGMENT THEN
ASM_REWRITE_TAC[] THEN
REPEAT(POP_ASSUM MP_TAC) THEN REWRITE_TAC[between; DIST_SYM] THEN
NORM_ARITH_TAC)
and symlemma = prove
(`(!n. P(--n) <=> P (n)) /\ (!n. &0 < n dot x ==> P n)
==> !n:real^N. ~(n dot x = &0) ==> P n`,
STRIP_TAC THEN GEN_TAC THEN
REWRITE_TAC[REAL_ARITH `~(x = &0) <=> &0 < x \/ &0 < --x`] THEN
REWRITE_TAC[GSYM DOT_LNEG] THEN ASM_MESON_TAC[]) in
REPEAT STRIP_TAC THEN
MP_TAC(ISPECL [`p:real^1->real^2`; `linepath(a:real^2,b)`]
SIMPLE_PATH_JOIN_LOOP_EQ) THEN
FIRST_ASSUM(MP_TAC o MATCH_MP SIMPLE_PATH_IMP_PATH) THEN
ASM_SIMP_TAC[PATH_JOIN; PATHSTART_LINEPATH; PATHFINISH_LINEPATH] THEN
DISCH_THEN(ASSUME_TAC o CONJUNCT1) THEN STRIP_TAC THEN
MP_TAC(ISPECL [`(a:real^2) INSERT b INSERT c INSERT d INSERT path_image p`;
`x:real^2`]
DISTANCE_ATTAINS_INF) THEN
REWRITE_TAC[FORALL_IN_INSERT] THEN
ONCE_REWRITE_TAC[SET_RULE `a INSERT b INSERT c INSERT d INSERT s =
{a,b,c,d} UNION s`] THEN
ASM_SIMP_TAC[CLOSED_UNION; FINITE_IMP_CLOSED; CLOSED_PATH_IMAGE;
FINITE_INSERT; FINITE_EMPTY] THEN
ANTS_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
DISCH_THEN(X_CHOOSE_THEN `cp:real^2` MP_TAC) THEN
DISJ_CASES_TAC(NORM_ARITH `cp = x \/ &0 < dist(x:real^2,cp)`) THENL
[FIRST_X_ASSUM SUBST_ALL_TAC THEN
MATCH_MP_TAC(TAUT `~a ==> a /\ b ==> c`) THEN
FIRST_ASSUM(MP_TAC o MATCH_MP (SET_RULE `a = {x} ==> x IN a`)) THEN
REWRITE_TAC[open_segment; IN_DIFF; IN_UNION; IN_INSERT; NOT_IN_EMPTY;
IN_INTER; DE_MORGAN_THM] THEN
STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (SET_RULE
`p INTER s SUBSET u ==> x IN (s DIFF u) ==> ~(x IN p)`)) THEN
ASM_REWRITE_TAC[IN_DIFF; IN_INSERT; NOT_IN_EMPTY; PATH_IMAGE_LINEPATH];
ALL_TAC] THEN
ABBREV_TAC `e = dist(x:real^2,cp)` THEN FIRST_X_ASSUM(K ALL_TAC o SYM) THEN
DISCH_THEN(STRIP_ASSUME_TAC o CONJUNCT2) THEN
RULE_ASSUM_TAC(REWRITE_RULE[ARC_LINEPATH_EQ]) THEN
MP_TAC(ISPECL [`a:real^2`; `b:real^2`; `c:real^2`; `d:real^2`]
FINITE_INTER_COLLINEAR_OPEN_SEGMENTS) THEN
MP_TAC(ISPECL [`a:real^2`; `b:real^2`; `d:real^2`; `c:real^2`]
FINITE_INTER_COLLINEAR_OPEN_SEGMENTS) THEN
SUBST1_TAC(MESON[SEGMENT_SYM] `segment(d:real^2,c) = segment(c,d)`) THEN
ASM_REWRITE_TAC[FINITE_SING; NOT_INSERT_EMPTY] THEN REPEAT DISCH_TAC THEN
SUBGOAL_THEN `~(a IN segment[c:real^2,d]) /\ ~(b IN segment[c,d])`
STRIP_ASSUME_TAC THENL
[ASM_MESON_TAC[PATHSTART_IN_PATH_IMAGE; PATHFINISH_IN_PATH_IMAGE;
IN_INTER; NOT_IN_EMPTY];
ALL_TAC] THEN
SUBGOAL_THEN `~(c:real^2 = a) /\ ~(c = b) /\ ~(d = a) /\ ~(d = b)`
STRIP_ASSUME_TAC THENL [ASM_MESON_TAC[ENDS_IN_SEGMENT]; ALL_TAC] THEN
SUBGOAL_THEN `x IN segment(a:real^2,b) /\ x IN segment(c,d)` MP_TAC THENL
[ASM SET_TAC[]; ALL_TAC] THEN
REWRITE_TAC[IN_OPEN_SEGMENT_ALT] THEN STRIP_TAC THEN
SUBGOAL_THEN
`{c,d} INTER path_image(p ++ linepath(a:real^2,b)) = {}`
ASSUME_TAC THENL
[ASM_SIMP_TAC[PATH_IMAGE_JOIN; PATH_LINEPATH; PATHSTART_LINEPATH] THEN
REWRITE_TAC[SET_RULE
`{c,d} INTER (s UNION t) = {} <=>
(~(c IN s) /\ ~(d IN s)) /\ ~(c IN t) /\ ~(d IN t)`] THEN
CONJ_TAC THENL
[ASM_MESON_TAC[ENDS_IN_SEGMENT; IN_INTER; NOT_IN_EMPTY];
REWRITE_TAC[PATH_IMAGE_LINEPATH; GSYM BETWEEN_IN_SEGMENT] THEN
CONJ_TAC THEN DISCH_THEN(ASSUME_TAC o MATCH_MP BETWEEN_IMP_COLLINEAR) THEN
RULE_ASSUM_TAC(REWRITE_RULE[INSERT_AC]) THEN ASM_MESON_TAC[]];
ALL_TAC] THEN
MP_TAC(ISPEC `b - x:real^2` ORTHOGONAL_TO_VECTOR_EXISTS) THEN
REWRITE_TAC[DIMINDEX_2; LE_REFL; LEFT_IMP_EXISTS_THM] THEN
X_GEN_TAC `n:real^2` THEN STRIP_TAC THEN
SUBGOAL_THEN `(x:real^2) IN segment(a,b) /\ x IN segment(c,d)` MP_TAC THENL
[ASM SET_TAC[];
SIMP_TAC[IN_OPEN_SEGMENT_ALT; GSYM BETWEEN_IN_SEGMENT] THEN STRIP_TAC] THEN
SUBGOAL_THEN `~collinear{a:real^2, b, c, d}` ASSUME_TAC THENL
[UNDISCH_TAC `~collinear{a:real^2,b,c}` THEN REWRITE_TAC[CONTRAPOS_THM] THEN
MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ_ALT] COLLINEAR_SUBSET) THEN SET_TAC[];
ALL_TAC] THEN
SUBGOAL_THEN `~(n dot (d - x:real^2) = &0)` MP_TAC THENL
[REWRITE_TAC[GSYM orthogonal] THEN DISCH_TAC THEN
MP_TAC(SPECL [`n:real^2`; `d - x:real^2`; `b - x:real^2`]
ORTHOGONAL_TO_ORTHOGONAL_2D) THEN
ANTS_TAC THENL [ASM_MESON_TAC[ORTHOGONAL_SYM]; ALL_TAC] THEN
REWRITE_TAC[GSYM COLLINEAR_3] THEN DISCH_TAC THEN
UNDISCH_TAC `~collinear{a:real^2, b, c, d}` THEN ASM_REWRITE_TAC[] THEN
ONCE_REWRITE_TAC[SET_RULE `{a,b,c,d} = {b,d,a,c}`] THEN
ASM_SIMP_TAC[COLLINEAR_4_3] THEN CONJ_TAC THENL
[MATCH_MP_TAC COLLINEAR_SUBSET THEN EXISTS_TAC `{b:real^2,x,a,d}` THEN
CONJ_TAC THENL [ASM_SIMP_TAC[COLLINEAR_4_3]; SET_TAC[]] THEN
ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {c,b,a}`] THEN
ASM_SIMP_TAC[BETWEEN_IMP_COLLINEAR];
MATCH_MP_TAC COLLINEAR_SUBSET THEN EXISTS_TAC `{d:real^2,x,b,c}` THEN
CONJ_TAC THENL [ASM_SIMP_TAC[COLLINEAR_4_3]; SET_TAC[]] THEN
ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {c,b,a}`] THEN
ASM_SIMP_TAC[BETWEEN_IMP_COLLINEAR]];
ALL_TAC] THEN
DISCH_THEN(fun th -> POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN
MP_TAC th) THEN
SPEC_TAC(`n:real^2`,`n:real^2`) THEN
MATCH_MP_TAC symlemma THEN CONJ_TAC THENL
[REWRITE_TAC[ORTHOGONAL_RNEG; VECTOR_NEG_EQ_0]; ALL_TAC] THEN
GEN_TAC THEN DISCH_TAC THEN STRIP_TAC THEN
SUBGOAL_THEN `n dot (c - x:real^2) < &0` ASSUME_TAC THENL
[UNDISCH_TAC `&0 < n dot (d - x:real^2)` THEN
SUBGOAL_THEN `(x:real^2) IN segment(c,d)` MP_TAC THENL
[ASM SET_TAC[]; ALL_TAC] THEN
ASM_REWRITE_TAC[IN_SEGMENT] THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
REWRITE_TAC[VECTOR_ARITH
`d - ((&1 - u) % c + u % d):real^N = (&1 - u) % (d - c) /\
c - ((&1 - u) % c + u % d) = --u % (d - c)`] THEN
REWRITE_TAC[DOT_RMUL; REAL_MUL_LNEG; REAL_ARITH `--x < &0 <=> &0 < x`] THEN
ASM_SIMP_TAC[REAL_LT_MUL_EQ; REAL_SUB_LT];
ALL_TAC] THEN
SUBGOAL_THEN
`!y. y IN ball(x:real^2,e)
==> y IN segment(a,b) \/
&0 < n dot (y - x) \/
n dot (y - x) < &0`
ASSUME_TAC THENL
[REWRITE_TAC[IN_BALL] THEN REPEAT STRIP_TAC THEN
MATCH_MP_TAC(TAUT `(~c /\ ~b ==> a) ==> a \/ b \/ c`) THEN
REWRITE_TAC[REAL_ARITH `~(x < &0) /\ ~(&0 < x) <=> x = &0`] THEN
REWRITE_TAC[GSYM orthogonal] THEN DISCH_TAC THEN
MP_TAC(SPECL [`n:real^2`; `y - x:real^2`; `b - x:real^2`]
ORTHOGONAL_TO_ORTHOGONAL_2D) THEN
ANTS_TAC THENL [ASM_MESON_TAC[ORTHOGONAL_SYM]; ALL_TAC] THEN
REWRITE_TAC[GSYM COLLINEAR_3] THEN DISCH_TAC THEN
MATCH_MP_TAC lemma THEN EXISTS_TAC `x:real^2` THEN
ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
[ALL_TAC; ASM_MESON_TAC[REAL_LTE_TRANS; DIST_SYM]] THEN
ONCE_REWRITE_TAC[SET_RULE `{y,a,b} = {a,b,y}`] THEN
MATCH_MP_TAC COLLINEAR_3_TRANS THEN EXISTS_TAC `x:real^2` THEN
ASM_REWRITE_TAC[] THEN UNDISCH_TAC `collinear{y:real^2, x, b}` THEN
MP_TAC(MATCH_MP BETWEEN_IMP_COLLINEAR (ASSUME
`between (x:real^2) (a,b)`)) THEN
SIMP_TAC[INSERT_AC];
ALL_TAC] THEN
MP_TAC(SPEC `p ++ linepath(a:real^2,b)` JORDAN_INSIDE_OUTSIDE) THEN
ASM_REWRITE_TAC[PATHFINISH_JOIN; PATHSTART_JOIN; PATHFINISH_LINEPATH] THEN
STRIP_TAC THEN
SUBGOAL_THEN
`~(connected_component((:real^2) DIFF path_image(p ++ linepath (a,b))) c d)`
MP_TAC THENL
[DISCH_TAC;
ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN
DISCH_THEN(MP_TAC o SPEC `path_image(p ++ linepath(a:real^2,b))` o
MATCH_MP (SET_RULE
`~(x IN s <=> y IN t)
==> !p. s UNION t = (:real^2) DIFF p /\ {x,y} INTER p = {}
==> x IN s /\ y IN s \/ x IN t /\ y IN t`)) THEN
ASM_REWRITE_TAC[connected_component] THEN
ASM_REWRITE_TAC[SET_RULE `t SUBSET UNIV DIFF s <=> t INTER s = {}`] THEN
ASM_MESON_TAC[INSIDE_NO_OVERLAP; OUTSIDE_NO_OVERLAP]] THEN
MP_TAC(SPEC `p ++ linepath(a:real^2,b)` JORDAN_DISCONNECTED) THEN
ASM_REWRITE_TAC[PATHFINISH_JOIN; PATHSTART_JOIN; PATHFINISH_LINEPATH] THEN
REWRITE_TAC[CONNECTED_IFF_CONNECTED_COMPONENT] THEN
SUBGOAL_THEN
`!u v. u IN inside(path_image(p ++ linepath(a,b))) /\
v IN outside(path_image(p ++ linepath(a,b)))
==> connected_component
((:real^2) DIFF path_image (p ++ linepath (a,b))) u v`
ASSUME_TAC THENL
[ALL_TAC;
MAP_EVERY X_GEN_TAC [`u:real^2`; `v:real^2`] THEN
GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV)
[SYM(ASSUME `inside (path_image (p ++ linepath (a,b))) UNION
outside (path_image (p ++ linepath (a,b))) =
(:real^2) DIFF path_image (p ++ linepath (a,b))`)] THEN
REWRITE_TAC[IN_UNION; CONNECTED_IFF_CONNECTED_COMPONENT] THEN
STRIP_TAC THENL
[REWRITE_TAC[connected_component] THEN
EXISTS_TAC `inside(path_image(p ++ linepath(a:real^2,b)))`;
ASM_MESON_TAC[];
ASM_MESON_TAC[CONNECTED_COMPONENT_SYM];
REWRITE_TAC[connected_component] THEN
EXISTS_TAC `outside(path_image(p ++ linepath(a:real^2,b)))`] THEN
ASM_REWRITE_TAC[SET_RULE `s SUBSET UNIV DIFF t <=> s INTER t = {}`] THEN
REWRITE_TAC[OUTSIDE_NO_OVERLAP; INSIDE_NO_OVERLAP]] THEN
SUBGOAL_THEN `(x:real^2) IN path_image(p ++ linepath(a,b))` ASSUME_TAC THENL
[ASM_SIMP_TAC[PATHSTART_LINEPATH; PATH_IMAGE_JOIN; PATH_LINEPATH] THEN
REWRITE_TAC[IN_UNION; PATH_IMAGE_LINEPATH] THEN DISJ2_TAC THEN
RULE_ASSUM_TAC(REWRITE_RULE[open_segment]) THEN ASM SET_TAC[];
ALL_TAC] THEN
MAP_EVERY X_GEN_TAC [`u:real^2`; `v:real^2`] THEN STRIP_TAC THEN
UNDISCH_TAC
`frontier(inside(path_image(p ++ linepath(a:real^2,b)))) =
path_image(p ++ linepath(a,b))` THEN
REWRITE_TAC[EXTENSION] THEN
DISCH_THEN(MP_TAC o SPEC `x:real^2`) THEN ASM_REWRITE_TAC[frontier] THEN
REWRITE_TAC[IN_DIFF; CLOSURE_APPROACHABLE] THEN
DISCH_THEN(MP_TAC o SPEC `e:real` o CONJUNCT1) THEN
ASM_REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
X_GEN_TAC `w:real^2` THEN STRIP_TAC THEN
MATCH_MP_TAC CONNECTED_COMPONENT_TRANS THEN EXISTS_TAC `w:real^2` THEN
CONJ_TAC THENL
[REWRITE_TAC[connected_component] THEN
EXISTS_TAC `inside(path_image(p ++ linepath(a:real^2,b)))` THEN
ASM_REWRITE_TAC[SET_RULE `s SUBSET UNIV DIFF t <=> s INTER t = {}`] THEN
REWRITE_TAC[INSIDE_NO_OVERLAP];
ALL_TAC] THEN
UNDISCH_TAC
`frontier(outside(path_image(p ++ linepath(a:real^2,b)))) =
path_image(p ++ linepath(a,b))` THEN
REWRITE_TAC[EXTENSION] THEN
DISCH_THEN(MP_TAC o SPEC `x:real^2`) THEN ASM_REWRITE_TAC[frontier] THEN
REWRITE_TAC[IN_DIFF; CLOSURE_APPROACHABLE] THEN
DISCH_THEN(MP_TAC o SPEC `e:real` o CONJUNCT1) THEN
ASM_REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
X_GEN_TAC `z:real^2` THEN STRIP_TAC THEN
MATCH_MP_TAC CONNECTED_COMPONENT_TRANS THEN EXISTS_TAC `z:real^2` THEN
CONJ_TAC THENL
[ALL_TAC;
REWRITE_TAC[connected_component] THEN
EXISTS_TAC `outside(path_image(p ++ linepath(a:real^2,b)))` THEN
ASM_REWRITE_TAC[SET_RULE `s SUBSET UNIV DIFF t <=> s INTER t = {}`] THEN
REWRITE_TAC[OUTSIDE_NO_OVERLAP]] THEN
SUBGOAL_THEN
`!y. dist(y,x) < e /\ ~(y IN path_image(p ++ linepath (a,b)))
==> connected_component
((:real^2) DIFF path_image(p ++ linepath(a,b))) c y`
ASSUME_TAC THENL
[ALL_TAC;
MATCH_MP_TAC CONNECTED_COMPONENT_TRANS THEN EXISTS_TAC `c:real^2` THEN
CONJ_TAC THENL [MATCH_MP_TAC CONNECTED_COMPONENT_SYM; ALL_TAC] THEN
FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN
ASM_MESON_TAC[INSIDE_NO_OVERLAP; OUTSIDE_NO_OVERLAP; IN_INTER;
NOT_IN_EMPTY]] THEN
X_GEN_TAC `y:real^2` THEN STRIP_TAC THEN
SUBGOAL_THEN `segment[c,d] INTER path_image(p ++ linepath(a,b)) = {x:real^2}`
ASSUME_TAC THENL
[MATCH_MP_TAC(SET_RULE
`{c,d} INTER p = {} /\ (segment[c,d] DIFF {c,d}) INTER p = {x}
==> segment[c,d] INTER p = {x}`) THEN
ASM_SIMP_TAC[PATH_IMAGE_JOIN; PATHSTART_LINEPATH; PATH_LINEPATH] THEN
MATCH_MP_TAC(SET_RULE
`cd INTER p = {} /\ l INTER (cd DIFF {c,d}) = {x}
==> (cd DIFF {c,d}) INTER (p UNION l) = {x}`) THEN
ASM_REWRITE_TAC[GSYM open_segment; PATH_IMAGE_LINEPATH] THEN
MATCH_MP_TAC(SET_RULE
`~(a IN segment[c,d]) /\ ~(b IN segment[c,d]) /\
segment(a,b) INTER segment(c,d) = {x} /\
segment(a,b) = segment[a,b] DIFF {a,b} /\
segment(c,d) = segment[c,d] DIFF {c,d}
==> segment[a,b] INTER segment(c,d) = {x}`) THEN
ASM_REWRITE_TAC[] THEN REWRITE_TAC[open_segment];
ALL_TAC] THEN
UNDISCH_THEN
`!y. y IN ball(x:real^2,e)
==> y IN segment(a,b) \/ &0 < n dot (y - x) \/ n dot (y - x) < &0`
(MP_TAC o SPEC `y:real^2`) THEN
REWRITE_TAC[IN_BALL] THEN ONCE_REWRITE_TAC[DIST_SYM] THEN
ASM_REWRITE_TAC[] THEN
DISCH_THEN(REPEAT_TCL DISJ_CASES_THEN MP_TAC) THENL
[MATCH_MP_TAC(TAUT `~p ==> p ==> q`) THEN
UNDISCH_TAC `~(y IN path_image(p ++ linepath(a:real^2,b)))` THEN
ASM_SIMP_TAC[PATHSTART_LINEPATH; PATH_IMAGE_JOIN; PATH_LINEPATH] THEN
SIMP_TAC[CONTRAPOS_THM; open_segment; IN_DIFF; IN_UNION;
PATH_IMAGE_LINEPATH];
DISCH_TAC THEN MATCH_MP_TAC CONNECTED_COMPONENT_TRANS THEN
EXISTS_TAC `d:real^2` THEN ASM_REWRITE_TAC[] THEN
MATCH_MP_TAC CONNECTED_COMPONENT_TRANS THEN
EXISTS_TAC `x + min (&1 / &2) (e / &2 / norm(d - x)) % (d - x):real^2` THEN
REWRITE_TAC[connected_component] THEN CONJ_TAC THENL
[EXISTS_TAC `segment[x:real^2,d] DELETE x` THEN
SIMP_TAC[CONVEX_SEMIOPEN_SEGMENT; CONVEX_CONNECTED] THEN
ASM_REWRITE_TAC[IN_DELETE; ENDS_IN_SEGMENT] THEN REPEAT CONJ_TAC THENL
[FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP (SET_RULE
`cd INTER p = {x}
==> xd SUBSET cd
==> (xd DELETE x) SUBSET (UNIV DIFF p)`)) THEN
REWRITE_TAC[SUBSET_SEGMENT; ENDS_IN_SEGMENT] THEN
UNDISCH_TAC `segment (a,b) INTER segment (c,d) = {x:real^2}` THEN
REWRITE_TAC[open_segment] THEN SET_TAC[];
REWRITE_TAC[IN_SEGMENT; VECTOR_ARITH
`x + a % (y - x):real^N = (&1 - a) % x + a % y`] THEN
EXISTS_TAC `min (&1 / &2) (e / &2 / norm(d - x:real^2))` THEN
REWRITE_TAC[] THEN CONJ_TAC THENL [ALL_TAC; REAL_ARITH_TAC] THEN
REWRITE_TAC[REAL_LE_MIN] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
ASM_SIMP_TAC[REAL_LE_DIV; REAL_POS; NORM_POS_LE; REAL_LT_IMP_LE];
ASM_REWRITE_TAC[VECTOR_MUL_EQ_0; VECTOR_SUB_EQ;
VECTOR_ARITH `x + a:real^N = x <=> a = vec 0`] THEN
MATCH_MP_TAC(REAL_ARITH `&0 < x ==> ~(min (&1 / &2) x = &0)`) THEN
MATCH_MP_TAC REAL_LT_DIV THEN ASM_REWRITE_TAC[REAL_HALF] THEN
ASM_REWRITE_TAC[NORM_POS_LT; VECTOR_SUB_EQ]];
EXISTS_TAC `ball(x,e) INTER {w:real^2 | &0 < n dot (w - x)}` THEN
REPEAT CONJ_TAC THENL
[MATCH_MP_TAC CONVEX_CONNECTED THEN MATCH_MP_TAC CONVEX_INTER THEN
REWRITE_TAC[CONVEX_BALL; DOT_RSUB; REAL_SUB_LT] THEN
REWRITE_TAC[GSYM real_gt; CONVEX_HALFSPACE_GT];
ASM_SIMP_TAC[PATHSTART_LINEPATH; PATH_IMAGE_JOIN; PATH_LINEPATH] THEN
MATCH_MP_TAC(SET_RULE
`p SUBSET (UNIV DIFF b) /\ l INTER w = {}
==> (b INTER w) SUBSET (UNIV DIFF (p UNION l))`) THEN
ASM_REWRITE_TAC[SUBSET; IN_DIFF; IN_UNIV; IN_BALL; REAL_NOT_LT] THEN
MATCH_MP_TAC(SET_RULE
`!t. t INTER u = {} /\ s SUBSET t ==> s INTER u = {}`) THEN
EXISTS_TAC `affine hull {x:real^2,b}` THEN CONJ_TAC THENL
[REWRITE_TAC[AFFINE_HULL_2; FORALL_IN_GSPEC; SET_RULE
`s INTER t = {} <=> !x. x IN s ==> ~(x IN t)`] THEN
REWRITE_TAC[IN_ELIM_THM] THEN
SIMP_TAC[REAL_ARITH `u + v = &1 <=> u = &1 - v`] THEN
REWRITE_TAC[DOT_RMUL; VECTOR_ARITH
`((&1 - v) % x + v % b) - x:real^N = v % (b - x)`] THEN
RULE_ASSUM_TAC(REWRITE_RULE[orthogonal]) THEN
ONCE_REWRITE_TAC[DOT_SYM] THEN
ASM_REWRITE_TAC[REAL_MUL_RZERO; REAL_LT_REFL];
REWRITE_TAC[PATH_IMAGE_LINEPATH; SEGMENT_CONVEX_HULL] THEN
SIMP_TAC[SUBSET_HULL; AFFINE_IMP_CONVEX; AFFINE_AFFINE_HULL] THEN
REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET] THEN
SIMP_TAC[HULL_INC; IN_INSERT] THEN
ASM_SIMP_TAC[GSYM COLLINEAR_3_AFFINE_HULL] THEN
ONCE_REWRITE_TAC[SET_RULE `{x,b,a} = {a,x,b}`] THEN
MATCH_MP_TAC BETWEEN_IMP_COLLINEAR THEN ASM_REWRITE_TAC[]];
REWRITE_TAC[IN_BALL; IN_INTER; IN_ELIM_THM; dist] THEN
REWRITE_TAC[NORM_ARITH `norm(x - (x + a):real^N) = norm a`] THEN
REWRITE_TAC[VECTOR_ARITH `(x + a) - x:real^N = a`] THEN CONJ_TAC THENL
[ASM_SIMP_TAC[NORM_MUL; GSYM REAL_LT_RDIV_EQ; NORM_POS_LT;
VECTOR_SUB_EQ] THEN
MATCH_MP_TAC(REAL_ARITH
`&0 < x /\ x < e ==> abs(min (&1 / &2) x) < e`) THEN
ASM_SIMP_TAC[REAL_LT_DIV; REAL_HALF; NORM_POS_LT; VECTOR_SUB_EQ;
REAL_LT_DIV2_EQ] THEN ASM_REAL_ARITH_TAC;
REWRITE_TAC[DOT_RMUL] THEN MATCH_MP_TAC REAL_LT_MUL THEN
ASM_REWRITE_TAC[REAL_LT_MIN] THEN
ASM_SIMP_TAC[REAL_LT_DIV; REAL_HALF; NORM_POS_LT; VECTOR_SUB_EQ;
REAL_LT_01]];
REWRITE_TAC[IN_BALL; IN_INTER; IN_ELIM_THM] THEN
ONCE_REWRITE_TAC[DIST_SYM] THEN ASM_REWRITE_TAC[]]];
DISCH_TAC THEN MATCH_MP_TAC CONNECTED_COMPONENT_TRANS THEN
EXISTS_TAC `x + min (&1 / &2) (e / &2 / norm(c - x)) % (c - x):real^2` THEN
REWRITE_TAC[connected_component] THEN CONJ_TAC THENL
[EXISTS_TAC `segment[x:real^2,c] DELETE x` THEN
SIMP_TAC[CONVEX_SEMIOPEN_SEGMENT; CONVEX_CONNECTED] THEN
ASM_REWRITE_TAC[IN_DELETE; ENDS_IN_SEGMENT] THEN REPEAT CONJ_TAC THENL
[FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP (SET_RULE
`cd INTER p = {x}
==> xd SUBSET cd
==> (xd DELETE x) SUBSET (UNIV DIFF p)`)) THEN
REWRITE_TAC[SUBSET_SEGMENT; ENDS_IN_SEGMENT] THEN
UNDISCH_TAC `segment (a,b) INTER segment (c,d) = {x:real^2}` THEN
REWRITE_TAC[open_segment] THEN SET_TAC[];
REWRITE_TAC[IN_SEGMENT; VECTOR_ARITH
`x + a % (y - x):real^N = (&1 - a) % x + a % y`] THEN
EXISTS_TAC `min (&1 / &2) (e / &2 / norm(c - x:real^2))` THEN
REWRITE_TAC[] THEN CONJ_TAC THENL [ALL_TAC; REAL_ARITH_TAC] THEN
REWRITE_TAC[REAL_LE_MIN] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
ASM_SIMP_TAC[REAL_LE_DIV; REAL_POS; NORM_POS_LE; REAL_LT_IMP_LE];
ASM_REWRITE_TAC[VECTOR_MUL_EQ_0; VECTOR_SUB_EQ;
VECTOR_ARITH `x + a:real^N = x <=> a = vec 0`] THEN
MATCH_MP_TAC(REAL_ARITH `&0 < x ==> ~(min (&1 / &2) x = &0)`) THEN
MATCH_MP_TAC REAL_LT_DIV THEN ASM_REWRITE_TAC[REAL_HALF] THEN
ASM_REWRITE_TAC[NORM_POS_LT; VECTOR_SUB_EQ]];
EXISTS_TAC `ball(x,e) INTER {w:real^2 | n dot (w - x) < &0}` THEN
REPEAT CONJ_TAC THENL
[MATCH_MP_TAC CONVEX_CONNECTED THEN MATCH_MP_TAC CONVEX_INTER THEN
REWRITE_TAC[CONVEX_BALL; DOT_RSUB; REAL_ARITH `a - b < &0 <=> a < b`;
CONVEX_HALFSPACE_LT];
ASM_SIMP_TAC[PATHSTART_LINEPATH; PATH_IMAGE_JOIN; PATH_LINEPATH] THEN
MATCH_MP_TAC(SET_RULE
`p SUBSET (UNIV DIFF b) /\ l INTER w = {}
==> (b INTER w) SUBSET (UNIV DIFF (p UNION l))`) THEN
ASM_REWRITE_TAC[SUBSET; IN_DIFF; IN_UNIV; IN_BALL; REAL_NOT_LT] THEN
MATCH_MP_TAC(SET_RULE
`!t. t INTER u = {} /\ s SUBSET t ==> s INTER u = {}`) THEN
EXISTS_TAC `affine hull {x:real^2,b}` THEN CONJ_TAC THENL
[REWRITE_TAC[AFFINE_HULL_2; FORALL_IN_GSPEC; SET_RULE
`s INTER t = {} <=> !x. x IN s ==> ~(x IN t)`] THEN
REWRITE_TAC[IN_ELIM_THM] THEN
SIMP_TAC[REAL_ARITH `u + v = &1 <=> u = &1 - v`] THEN
REWRITE_TAC[DOT_RMUL; VECTOR_ARITH
`((&1 - v) % x + v % b) - x:real^N = v % (b - x)`] THEN
RULE_ASSUM_TAC(REWRITE_RULE[orthogonal]) THEN
ONCE_REWRITE_TAC[DOT_SYM] THEN
ASM_REWRITE_TAC[REAL_MUL_RZERO; REAL_LT_REFL];
REWRITE_TAC[PATH_IMAGE_LINEPATH; SEGMENT_CONVEX_HULL] THEN
SIMP_TAC[SUBSET_HULL; AFFINE_IMP_CONVEX; AFFINE_AFFINE_HULL] THEN
REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET] THEN
SIMP_TAC[HULL_INC; IN_INSERT] THEN
ASM_SIMP_TAC[GSYM COLLINEAR_3_AFFINE_HULL] THEN
ONCE_REWRITE_TAC[SET_RULE `{x,b,a} = {a,x,b}`] THEN
MATCH_MP_TAC BETWEEN_IMP_COLLINEAR THEN ASM_REWRITE_TAC[]];
REWRITE_TAC[IN_BALL; IN_INTER; IN_ELIM_THM; dist] THEN
REWRITE_TAC[NORM_ARITH `norm(x - (x + a):real^N) = norm a`] THEN
REWRITE_TAC[VECTOR_ARITH `(x + a) - x:real^N = a`] THEN CONJ_TAC THENL
[ASM_SIMP_TAC[NORM_MUL; GSYM REAL_LT_RDIV_EQ; NORM_POS_LT;
VECTOR_SUB_EQ] THEN
MATCH_MP_TAC(REAL_ARITH
`&0 < x /\ x < e ==> abs(min (&1 / &2) x) < e`) THEN
ASM_SIMP_TAC[REAL_LT_DIV; REAL_HALF; NORM_POS_LT; VECTOR_SUB_EQ;
REAL_LT_DIV2_EQ] THEN ASM_REAL_ARITH_TAC;
REWRITE_TAC[DOT_RMUL; REAL_ARITH `x * y < &0 <=> &0 < x * --y`] THEN
MATCH_MP_TAC REAL_LT_MUL THEN ASM_REWRITE_TAC[REAL_LT_MIN] THEN
ASM_REWRITE_TAC[REAL_ARITH `&0 < --x <=> x < &0`] THEN
ASM_SIMP_TAC[REAL_LT_DIV; REAL_HALF; NORM_POS_LT; VECTOR_SUB_EQ;
REAL_LT_01]];
REWRITE_TAC[IN_BALL; IN_INTER; IN_ELIM_THM] THEN
ONCE_REWRITE_TAC[DIST_SYM] THEN ASM_REWRITE_TAC[]]]]);;
(* ------------------------------------------------------------------------- *)
(* Polygonal path; 0 in the empty case is just for linear invariance. *)
(* Note that we *are* forced to assume non-emptiness for translation. *)
(* ------------------------------------------------------------------------- *)
add_translation_invariants [POLYGONAL_PATH_TRANSLATION];;
add_linear_invariants [POLYGONAL_PATH_LINEAR_IMAGE];;
(* ------------------------------------------------------------------------- *)
(* Rotating the starting point to move a preferred vertex forward. *)
(* ------------------------------------------------------------------------- *)
let ROTATE_LIST_TO_FRONT_1 = prove
(`!P l a:A.
(!l. P(l) ==> 3 <=
LENGTH l /\
LAST l =
HD l) /\
(!l. P(l) ==> P(
APPEND (
TL l) [
HD(
TL l)])) /\
P l /\
MEM a l
==> ?l'.
EL 1 l' = a /\ P l'`,
let lemma0 = prove
(`!P. (!i. P i /\ 0 < i ==> P(i - 1)) /\ (?k. 0 < k /\ P k)
==> P 1`,
REPEAT STRIP_TAC THEN
SUBGOAL_THEN `!i:num. i < k ==> P(k - i)` MP_TAC THENL
[INDUCT_TAC THEN ASM_REWRITE_TAC[SUB_0] THEN DISCH_TAC THEN
REWRITE_TAC[ARITH_RULE `k - SUC i = k - i - 1`] THEN
FIRST_X_ASSUM MATCH_MP_TAC THEN
CONJ_TAC THEN TRY(FIRST_X_ASSUM MATCH_MP_TAC) THEN ASM_ARITH_TAC;
DISCH_THEN(MP_TAC o SPEC `k - 1`) THEN
ASM_SIMP_TAC[ARITH_RULE `0 < k ==> k - 1 < k /\ k - (k - 1) = 1`]]) in
REPEAT STRIP_TAC THEN
SUBGOAL_THEN
`?i l'. 0 < i /\ i < LENGTH l' /\ P l' /\ EL i l' = (a:A)`
MP_TAC THENL
[SUBGOAL_THEN `~(l:A list = [])` ASSUME_TAC THENL
[ASM_MESON_TAC[LENGTH; ARITH_RULE `~(3 <= 0)`]; ALL_TAC] THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [MEM_EXISTS_EL]) THEN
DISCH_THEN(X_CHOOSE_THEN `i:num` STRIP_ASSUME_TAC) THEN
DISJ_CASES_THEN2 SUBST_ALL_TAC ASSUME_TAC (ARITH_RULE `i = 0 \/ 0 < i`)
THENL
[EXISTS_TAC `LENGTH(l:A list) - 2` THEN
EXISTS_TAC `(APPEND (TL l) [HD(TL l):A])` THEN
ASM_SIMP_TAC[LENGTH_APPEND; LENGTH_TL; EL_APPEND] THEN
REWRITE_TAC[LT_REFL; LENGTH; SUB_REFL; EL; HD] THEN
SUBGOAL_THEN `3 <= LENGTH(l:A list)` ASSUME_TAC THENL
[ASM_MESON_TAC[]; ALL_TAC] THEN
REPLICATE_TAC 2 (CONJ_TAC THENL [ASM_ARITH_TAC; ALL_TAC]) THEN
ASM_SIMP_TAC[ARITH_RULE `3 <= n ==> n - 2 < n - 1`] THEN
ASM_SIMP_TAC[EL_TL; ARITH_RULE `3 <= n ==> n - 2 + 1 = n - 1`] THEN
ASM_MESON_TAC[LAST_EL];
MAP_EVERY EXISTS_TAC [`i:num`; `l:A list`] THEN ASM_REWRITE_TAC[]];
REWRITE_TAC[RIGHT_EXISTS_AND_THM] THEN
DISCH_THEN(MP_TAC o MATCH_MP (ONCE_REWRITE_RULE[IMP_CONJ_ALT] lemma0)) THEN
ANTS_TAC THENL [ALL_TAC; MESON_TAC[]] THEN X_GEN_TAC `k:num` THEN
DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
DISCH_THEN(X_CHOOSE_THEN `m:A list` STRIP_ASSUME_TAC) THEN
EXISTS_TAC `APPEND (TL m) [HD(TL m):A]` THEN
SUBGOAL_THEN `~(m:A list = [])` ASSUME_TAC THENL
[ASM_MESON_TAC[LENGTH; ARITH_RULE `~(3 <= 0)`]; ALL_TAC] THEN
ASM_SIMP_TAC[LENGTH_APPEND; LENGTH_TL; EL_APPEND] THEN
ASM_REWRITE_TAC[LENGTH] THEN CONJ_TAC THENL [ASM_ARITH_TAC; ALL_TAC] THEN
COND_CASES_TAC THENL [ALL_TAC; ASM_ARITH_TAC] THEN
ASM_SIMP_TAC[EL_TL; ARITH_RULE `0 < k ==> k - 1 + 1 = k`]]);;
(* ------------------------------------------------------------------------- *)
(* We can pick a transformation to make all y coordinates distinct. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Proof that we can chop a polygon's inside in two. *)
(* ------------------------------------------------------------------------- *)
let POLYGON_CHOP_IN_TWO = prove
(`!p:(real^2)list.
simple_path(
polygonal_path p) /\
pathfinish(
polygonal_path p) = pathstart(
polygonal_path p) /\
5 <=
LENGTH p
==> ?a b. ~(a = b) /\
MEM a p /\
MEM b p /\
segment(a,b)
SUBSET inside(
path_image(
polygonal_path p))`,
let wlog_lemma = MESON[]
`(!x. ?f:A->A y. transform f /\ nice y /\ f y = x)
==> !P. (!f x. transform f ==> (P(f x) <=> P x)) /\
(!x. nice x ==> P x)
==> !x. P x` in
let between_lemma = prove
(`!a c u v m:real^N.
collinear {a,c,u,v,m} /\ m IN segment[u,v] /\ m IN segment(a,c)
==> u IN segment(a,c) \/ v IN segment(a,c) \/
segment[a,c] SUBSET segment[u,v]`,
REPEAT GEN_TAC THEN
ONCE_REWRITE_TAC[IMP_CONJ] THEN REWRITE_TAC[COLLINEAR_AFFINE_HULL] THEN
REWRITE_TAC[INSERT_SUBSET; LEFT_IMP_EXISTS_THM; EMPTY_SUBSET] THEN
MAP_EVERY X_GEN_TAC [`origin:real^N`; `dir:real^N`] THEN
GEOM_ORIGIN_TAC `origin:real^N` THEN
REWRITE_TAC[AFFINE_HULL_2; VECTOR_MUL_RZERO; VECTOR_ADD_LID] THEN
REWRITE_TAC[IN_ELIM_THM] THEN REPEAT GEN_TAC THEN STRIP_TAC THEN
ASM_REWRITE_TAC[] THEN ASM_CASES_TAC `dir:real^N = vec 0` THENL
[ASM_REWRITE_TAC[VECTOR_MUL_RZERO; SEGMENT_REFL; SUBSET_REFL];
ALL_TAC] THEN
REWRITE_TAC[SUBSET_SEGMENT] THEN
ASM_SIMP_TAC[SEGMENT_SCALAR_MULTIPLE; IN_ELIM_THM] THEN
ASM_REWRITE_TAC[VECTOR_MUL_RCANCEL] THEN
REWRITE_TAC[ONCE_REWRITE_RULE[CONJ_SYM] UNWIND_THM1] THEN
REAL_ARITH_TAC) in
MATCH_MP_TAC(MATCH_MP wlog_lemma DISTINGUISHING_ROTATION_EXISTS_POLYGON) THEN
CONJ_TAC THENL
[REWRITE_TAC[MESON[] `(!x y. (?z. P z /\ x = f z) ==> Q x y) <=>
(!z y. P z ==> Q (f z) y)`] THEN
REWRITE_TAC[ORTHOGONAL_TRANSFORMATION] THEN
GEOM_TRANSFORM_TAC [];
ALL_TAC] THEN
X_GEN_TAC `q:(real^2)list` THEN DISCH_TAC THEN STRIP_TAC THEN
SUBGOAL_THEN
`?b:real^2. MEM b q /\ !d. MEM d q ==> b$2 <= d$2`
STRIP_ASSUME_TAC THENL
[MP_TAC(ISPEC `IMAGE (\x:real^2. x$2) (set_of_list q)`
INF_FINITE) THEN
SIMP_TAC[FINITE_SET_OF_LIST; FINITE_IMAGE] THEN
REWRITE_TAC[IMAGE_EQ_EMPTY; SET_OF_LIST_EQ_EMPTY] THEN
UNDISCH_TAC `5 <= LENGTH(q:(real^2)list)` THEN
ASM_CASES_TAC `q:(real^2)list = []` THEN
ASM_REWRITE_TAC[LENGTH; ARITH; FORALL_IN_IMAGE] THEN DISCH_TAC THEN
REWRITE_TAC[IN_IMAGE; LEFT_AND_EXISTS_THM; IN_SET_OF_LIST] THEN
MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `b:real^2` THEN
DISCH_THEN(CONJUNCTS_THEN2 STRIP_ASSUME_TAC MP_TAC) THEN
ASM_REWRITE_TAC[];
ALL_TAC] THEN
SUBGOAL_THEN
`?p:(real^2)list.
EL 1 p = b /\ LAST p = HD p /\
LENGTH p = LENGTH q /\ set_of_list p = set_of_list q /\
path_image(polygonal_path p) = path_image(polygonal_path q) /\
simple_path(polygonal_path p) /\
pathfinish(polygonal_path p) = pathstart(polygonal_path p)`
MP_TAC THENL
[MATCH_MP_TAC ROTATE_LIST_TO_FRONT_1 THEN EXISTS_TAC `q:(real^2)list` THEN
ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
[REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN ASM_ARITH_TAC; ALL_TAC] THEN
MAP_EVERY UNDISCH_TAC
[`pathfinish(polygonal_path(q:(real^2)list)) =
pathstart(polygonal_path q)`;
`5 <= LENGTH(q:(real^2)list)`] THEN
ASM_CASES_TAC `q:(real^2)list = []` THEN
ASM_REWRITE_TAC[LENGTH; ARITH] THEN
ASM_REWRITE_TAC[PATHSTART_POLYGONAL_PATH; PATHFINISH_POLYGONAL_PATH] THEN
DISCH_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
X_GEN_TAC `l:(real^2)list` THEN
REWRITE_TAC[APPEND_EQ_NIL; NOT_CONS_NIL] THEN
ASM_CASES_TAC `l:(real^2)list = []` THENL
[ASM_MESON_TAC[LENGTH_EQ_NIL]; ALL_TAC] THEN
ASM_REWRITE_TAC[] THEN DISCH_THEN(STRIP_ASSUME_TAC o GSYM) THEN
ASM_REWRITE_TAC[] THEN
SUBGOAL_THEN `~(TL l:(real^2)list = [])` ASSUME_TAC THENL
[DISCH_THEN(MP_TAC o AP_TERM `LENGTH:(real^2)list->num`) THEN
ASM_SIMP_TAC[LENGTH; LENGTH_TL] THEN ASM_ARITH_TAC;
ALL_TAC] THEN
ASM_SIMP_TAC[LAST_APPEND; LENGTH_APPEND; LENGTH_TL; NOT_CONS_NIL] THEN
ASM_REWRITE_TAC[LAST; HD_APPEND; LENGTH] THEN REPEAT CONJ_TAC THENL
[ASM_ARITH_TAC;
MAP_EVERY UNDISCH_TAC
[`HD(l:(real^2)list) = LAST l`; `5 <= LENGTH(q:(real^2)list)`;
`~(l:(real^2)list = [])`] THEN
ASM_REWRITE_TAC[] THEN
SPEC_TAC(`l:(real^2)list`,`l:(real^2)list`) THEN
LIST_INDUCT_TAC THEN REWRITE_TAC[HD; TL; APPEND] THEN
REWRITE_TAC[SET_OF_LIST_APPEND; set_of_list] THEN
REPEAT STRIP_TAC THEN MATCH_MP_TAC(SET_RULE
`a IN s /\ b IN s ==> s UNION {a} = b INSERT s`) THEN
ASM_REWRITE_TAC[LAST] THEN ONCE_ASM_REWRITE_TAC[] THEN
REWRITE_TAC[LAST] THEN UNDISCH_TAC `5 <= LENGTH(CONS (h:real^2) t)` THEN
COND_CASES_TAC THEN ASM_REWRITE_TAC[LENGTH; ARITH] THEN
REWRITE_TAC[IN_SET_OF_LIST; MEM_EXISTS_EL; LENGTH] THEN
DISCH_TAC THEN CONJ_TAC THENL
[EXISTS_TAC `0` THEN REWRITE_TAC[EL] THEN ASM_ARITH_TAC;
EXISTS_TAC `LENGTH(t:(real^2)list) - 1` THEN
ASM_SIMP_TAC[LAST_EL] THEN ASM_ARITH_TAC];
MATCH_MP_TAC PATH_IMAGE_POLYGONAL_PATH_ROTATE THEN
ASM_REWRITE_TAC[] THEN ASM_ARITH_TAC;
MP_TAC(ISPEC `l:(real^2)list` SIMPLE_PATH_POLYGONAL_PATH_ROTATE) THEN
ASM_REWRITE_TAC[] THEN DISCH_THEN MATCH_MP_TAC THEN ASM_ARITH_TAC];
ALL_TAC] THEN
UNDISCH_THEN `pathfinish(polygonal_path(q:(real^2)list)) =
pathstart(polygonal_path q)` (K ALL_TAC) THEN
UNDISCH_THEN `simple_path(polygonal_path(q:(real^2)list))` (K ALL_TAC) THEN
DISCH_THEN(X_CHOOSE_THEN `r:(real^2)list` MP_TAC) THEN
DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
DISCH_THEN(CONJUNCTS_THEN2 (SUBST_ALL_TAC o SYM) MP_TAC) THEN
GEN_REWRITE_TAC (LAND_CONV o LAND_CONV) [EXTENSION] THEN
REWRITE_TAC[IN_SET_OF_LIST] THEN DISCH_THEN(CONJUNCTS_THEN2
(fun th -> REWRITE_TAC[GSYM th] THEN
RULE_ASSUM_TAC(REWRITE_RULE[GSYM th])) MP_TAC) THEN
DISCH_THEN(CONJUNCTS_THEN2 (SUBST_ALL_TAC o SYM) STRIP_ASSUME_TAC) THEN
UNDISCH_THEN `MEM (b:real^2) r` (K ALL_TAC) THEN
POP_ASSUM_LIST(MP_TAC o end_itlist CONJ o rev) THEN
SPEC_TAC(`r:(real^2)list`,`r:(real^2)list`) THEN
MATCH_MP_TAC list_INDUCT THEN REWRITE_TAC[LENGTH; ARITH] THEN
X_GEN_TAC `a:real^2` THEN
MATCH_MP_TAC list_INDUCT THEN REWRITE_TAC[LENGTH; ARITH] THEN
X_GEN_TAC `b':real^2` THEN
MATCH_MP_TAC list_INDUCT THEN REWRITE_TAC[LENGTH; ARITH] THEN
X_GEN_TAC `c:real^2` THEN X_GEN_TAC `p:(real^2)list` THEN
REPLICATE_TAC 3 (DISCH_THEN(K ALL_TAC)) THEN
REWRITE_TAC[num_CONV `1`; EL; HD; TL] THEN
ASM_CASES_TAC `b':real^2 = b` THEN ASM_REWRITE_TAC[] THEN
POP_ASSUM(K ALL_TAC) THEN
REWRITE_TAC[ARITH_RULE `5 <= SUC(SUC(SUC n)) <=> ~(n = 0) /\ 2 <= n`] THEN
ASM_CASES_TAC `p:(real^2)list = []` THEN ASM_REWRITE_TAC[LENGTH_EQ_NIL] THEN
ASM_SIMP_TAC[POLYGONAL_PATH_CONS_CONS; LAST; NOT_CONS_NIL] THEN
REWRITE_TAC[PATHSTART_JOIN; PATHSTART_LINEPATH] THEN
REPLICATE_TAC 2 (DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
FIRST_X_ASSUM(MP_TAC o SPEC `b:real^2`) THEN
REWRITE_TAC[MESON[MEM] `MEM b (CONS a (CONS b l))`] THEN
DISCH_THEN(ASSUME_TAC o GSYM) THEN STRIP_TAC THEN
MP_TAC(ISPECL
[`linepath(a:real^2,b)`;
`polygonal_path(CONS (b:real^2) (CONS c p))`]
SIMPLE_PATH_JOIN_IMP) THEN
ASM_SIMP_TAC[POLYGONAL_PATH_CONS_CONS] THEN
REWRITE_TAC[PATHFINISH_LINEPATH; PATHSTART_JOIN; PATHSTART_LINEPATH] THEN
REWRITE_TAC[ARC_LINEPATH_EQ] THEN
DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
DISCH_THEN(CONJUNCTS_THEN2 (fun th -> ASSUME_TAC th THEN MP_TAC th)
MP_TAC) THEN
SIMP_TAC[ARC_JOIN_EQ; PATHFINISH_LINEPATH; PATHSTART_POLYGONAL_PATH;
NOT_CONS_NIL; HD] THEN
REWRITE_TAC[ARC_LINEPATH_EQ; GSYM CONJ_ASSOC; PATH_IMAGE_LINEPATH] THEN
SIMP_TAC[PATH_IMAGE_JOIN; PATHFINISH_LINEPATH; PATHSTART_POLYGONAL_PATH;
HD; NOT_CONS_NIL] THEN
REWRITE_TAC[SET_RULE `s INTER (t UNION u) SUBSET v <=>
s INTER t SUBSET v /\ s INTER u SUBSET v`] THEN
ASM_CASES_TAC `a:real^2 = c` THENL
[DISCH_THEN(MP_TAC o CONJUNCT1) THEN
ASM_REWRITE_TAC[PATH_IMAGE_LINEPATH; SEGMENT_SYM; INTER_ACI] THEN
DISCH_THEN(MP_TAC o MATCH_MP (REWRITE_RULE [IMP_CONJ_ALT]
FINITE_SUBSET)) THEN
REWRITE_TAC[FINITE_SEGMENT; FINITE_INSERT; FINITE_EMPTY] THEN
ASM_MESON_TAC[];
ALL_TAC] THEN
REWRITE_TAC[PATH_IMAGE_LINEPATH] THEN STRIP_TAC THEN STRIP_TAC THEN
MP_TAC(ISPEC `CONS (b:real^2) (CONS c p)`
ARC_POLYGONAL_PATH_IMP_DISTINCT) THEN
ASM_SIMP_TAC[POLYGONAL_PATH_CONS_CONS] THEN
REWRITE_TAC[PAIRWISE; ALL] THEN REWRITE_TAC[GSYM ALL_MEM] THEN
REWRITE_TAC[MESON[] `(!x. P x ==> ~(a = x)) <=> ~(P a)`] THEN
STRIP_TAC THEN
SUBGOAL_THEN `(b:real^2)$2 < (a:real^2)$2 /\
(b:real^2)$2 < (c:real^2)$2 /\
(!v. MEM v p ==> (b:real^2)$2 < (v:real^2)$2)`
STRIP_ASSUME_TAC THENL
[REPEAT STRIP_TAC THEN REWRITE_TAC[REAL_LT_LE] THEN
CONV_TAC(ONCE_DEPTH_CONV SYM_CONV) THEN
CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[MEM] THEN
ASM_MESON_TAC[];
ALL_TAC] THEN
SUBGOAL_THEN `~collinear{a:real^2,b,c}` ASSUME_TAC THENL
[REWRITE_TAC[COLLINEAR_BETWEEN_CASES; BETWEEN_IN_SEGMENT] THEN
SUBGOAL_THEN `FINITE(segment[a:real^2,b] INTER segment[b,c])` MP_TAC THENL
[MATCH_MP_TAC FINITE_SUBSET THEN
EXISTS_TAC `{a:real^2,b}` THEN ASM_REWRITE_TAC[] THEN
REWRITE_TAC[FINITE_INSERT; FINITE_EMPTY];
ALL_TAC] THEN
ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN REWRITE_TAC[] THEN
STRIP_TAC THENL
[SUBGOAL_THEN `segment[a:real^2,b] INTER segment[b,c] = segment[a,b]`
(fun th -> ASM_REWRITE_TAC[FINITE_SEGMENT; th]) THEN
REWRITE_TAC[SET_RULE `s INTER t = s <=> s SUBSET t`] THEN
ASM_REWRITE_TAC[SUBSET_SEGMENT; ENDS_IN_SEGMENT];
DISCH_TAC THEN UNDISCH_TAC `b IN segment[c:real^2,a]` THEN
ASM_REWRITE_TAC[SEGMENT_CLOSED_OPEN; IN_UNION; IN_INSERT] THEN
ASM_REWRITE_TAC[IN_SEGMENT; NOT_IN_EMPTY] THEN
DISCH_THEN(X_CHOOSE_THEN `u:real` MP_TAC) THEN
REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
DISCH_THEN(MP_TAC o AP_TERM `\x:real^2. x$2`) THEN
REWRITE_TAC[VECTOR_ADD_COMPONENT; VECTOR_MUL_COMPONENT] THEN
MATCH_MP_TAC(REAL_ARITH
`(&1 - u) * b < (&1 - u) * c /\ u * b < u * a
==> ~(b = (&1 - u) * c + u * a)`) THEN
ASM_SIMP_TAC[REAL_LT_LMUL_EQ; REAL_SUB_LT];
SUBGOAL_THEN `segment[a:real^2,b] INTER segment[b,c] = segment[b,c]`
(fun th -> ASM_REWRITE_TAC[FINITE_SEGMENT; th]) THEN
REWRITE_TAC[SET_RULE `s INTER t = t <=> t SUBSET s`] THEN
ASM_REWRITE_TAC[SUBSET_SEGMENT; ENDS_IN_SEGMENT]];
ALL_TAC] THEN
SUBGOAL_THEN
`?e. &0 < e /\
e <= (a:real^2)$2 - (b:real^2)$2 /\
e <= (c:real^2)$2 - (b:real^2)$2 /\
!v. MEM v p ==> e <= (v:real^2)$2 - (b:real^2)$2`
STRIP_ASSUME_TAC THENL
[MP_TAC(ISPEC `IMAGE (\v. (v:real^2)$2 - (b:real^2)$2)
(set_of_list(CONS a (CONS b (CONS c p)))
DELETE b)`
INF_FINITE) THEN
ASM_SIMP_TAC[FINITE_SET_OF_LIST; FINITE_IMAGE; FINITE_DELETE] THEN
ANTS_TAC THENL
[REWRITE_TAC[IMAGE_EQ_EMPTY] THEN
REWRITE_TAC[set_of_list; GSYM MEMBER_NOT_EMPTY] THEN
EXISTS_TAC `a:real^2` THEN ASM_REWRITE_TAC[IN_DELETE; IN_INSERT];
ALL_TAC] THEN
REWRITE_TAC[FORALL_IN_IMAGE] THEN REWRITE_TAC[IN_IMAGE] THEN
ASM_REWRITE_TAC[set_of_list; FORALL_IN_INSERT; IMP_CONJ; IN_DELETE] THEN
DISCH_THEN(X_CHOOSE_THEN `d:real^2` MP_TAC) THEN
DISCH_THEN(CONJUNCTS_THEN2 SUBST1_TAC STRIP_ASSUME_TAC) THEN
DISCH_TAC THEN DISCH_TAC THEN REWRITE_TAC[IN_SET_OF_LIST] THEN
DISCH_TAC THEN EXISTS_TAC `(d:real^2)$2 - (b:real^2)$2` THEN
ASM_REWRITE_TAC[REAL_SUB_LT] THEN
RULE_ASSUM_TAC(REWRITE_RULE[IN_INSERT; IN_SET_OF_LIST]) THEN
ASM_MESON_TAC[];
ALL_TAC] THEN
MAP_EVERY ABBREV_TAC
[`a':real^2 = (&1 - e / (a$2 - b$2)) % b + e / (a$2 - b$2) % a`;
`c':real^2 = (&1 - e / (c$2 - b$2)) % b + e / (c$2 - b$2) % c`] THEN
SUBGOAL_THEN
`a' IN segment[b:real^2,a] /\ c' IN segment[b,c]`
STRIP_ASSUME_TAC THENL
[MAP_EVERY EXPAND_TAC ["a'";
"c'"] THEN
REWRITE_TAC[IN_SEGMENT] THEN
REWRITE_TAC[VECTOR_ARITH
`(&1 - u) % a + u % b = (&1 - v) % a + v % b <=>
(u - v) % (b - a) = vec 0`] THEN
ASM_REWRITE_TAC[VECTOR_MUL_EQ_0; VECTOR_SUB_EQ; REAL_SUB_0] THEN
ONCE_REWRITE_TAC[TAUT `p /\ q /\ r <=> r /\ p /\ q`] THEN
REWRITE_TAC[UNWIND_THM1] THEN
ASM_SIMP_TAC[REAL_LT_IMP_LE; REAL_LE_DIV; REAL_SUB_LE;
REAL_LE_LDIV_EQ; REAL_SUB_LT; REAL_MUL_LID];
ALL_TAC] THEN
SUBGOAL_THEN `~(a':real^2 = b) /\ ~(c':real^2 = b)` STRIP_ASSUME_TAC THENL
[MAP_EVERY EXPAND_TAC ["a'"; "c'"] THEN
REWRITE_TAC[VECTOR_ARITH
`(&1 - u) % a + u % b = a <=> u % (b - a) = vec 0`] THEN
ASM_REWRITE_TAC[VECTOR_MUL_EQ_0; VECTOR_SUB_EQ] THEN
ASM_SIMP_TAC[REAL_EQ_LDIV_EQ; REAL_SUB_LT] THEN
ASM_SIMP_TAC[REAL_MUL_LZERO; REAL_LT_IMP_NZ];
ALL_TAC] THEN
SUBGOAL_THEN `~collinear{a':real^2,b,c'}` ASSUME_TAC THENL
[UNDISCH_TAC `~collinear{a:real^2,b,c}` THEN
REWRITE_TAC[CONTRAPOS_THM] THEN ONCE_REWRITE_TAC[COLLINEAR_3] THEN
MAP_EVERY EXPAND_TAC ["a'"; "c'"] THEN
REWRITE_TAC[VECTOR_ARITH `((&1 - u) % b + u % a) - b = u % (a - b)`] THEN
REWRITE_TAC[GSYM DOT_CAUCHY_SCHWARZ_EQUAL; DOT_LMUL; DOT_RMUL] THEN
MATCH_MP_TAC(REAL_FIELD
`~(a = &0) /\ ~(c = &0)
==> (a * c * x) pow 2 = (a * a * y) * (c * c * z)
==> x pow 2 = y * z`) THEN
ASM_SIMP_TAC[REAL_EQ_LDIV_EQ; REAL_SUB_LT] THEN
ASM_SIMP_TAC[REAL_MUL_LZERO; REAL_LT_IMP_NZ];
ALL_TAC] THEN
SUBGOAL_THEN `~(a':real^2 = c')` ASSUME_TAC THENL
[DISCH_TAC THEN UNDISCH_TAC `~collinear{a':real^2,b,c'}` THEN
ASM_REWRITE_TAC[INSERT_AC; COLLINEAR_2];
ALL_TAC] THEN
SUBGOAL_THEN `~affine_dependent{a':real^2,b,c'}` ASSUME_TAC THENL
[ASM_MESON_TAC[AFFINE_DEPENDENT_IMP_COLLINEAR_3]; ALL_TAC] THEN
MP_TAC(ISPEC `{a':real^2,b,c'}` INTERIOR_CONVEX_HULL_EQ_EMPTY) THEN
REWRITE_TAC[DIMINDEX_2; HAS_SIZE; ARITH; FINITE_INSERT; FINITE_EMPTY] THEN
SIMP_TAC[CARD_CLAUSES; FINITE_INSERT; FINITE_EMPTY] THEN
ASM_REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY; ARITH] THEN DISCH_TAC THEN
SUBGOAL_THEN `convex hull {a,b,c} INTER {x:real^2 | x$2 - b$2 <= e} =
convex hull {a',b,c'}`
ASSUME_TAC THENL
[MATCH_MP_TAC SUBSET_ANTISYM THEN CONJ_TAC THENL
[ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {b,a,c}`] THEN
REWRITE_TAC[CONVEX_HULL_3_ALT] THEN
REWRITE_TAC[SUBSET; IN_INTER; FORALL_IN_GSPEC; IMP_CONJ] THEN
REWRITE_TAC[IN_ELIM_THM; VECTOR_ARITH
`a + x:real^N = a + y <=> x = y`] THEN
MAP_EVERY X_GEN_TAC [`s:real`; `t:real`] THEN
REPLICATE_TAC 3 DISCH_TAC THEN MAP_EVERY EXPAND_TAC ["a'"; "c'"] THEN
REWRITE_TAC[VECTOR_ARITH
`((&1 - u) % b + u % a) - b:real^N = u % (a - b)`] THEN
REWRITE_TAC[VECTOR_ADD_COMPONENT; VECTOR_MUL_COMPONENT] THEN
REWRITE_TAC[REAL_ADD_SUB; VECTOR_SUB_COMPONENT] THEN STRIP_TAC THEN
EXISTS_TAC `(s * ((a:real^2)$2 - (b:real^2)$2)) / e` THEN
EXISTS_TAC `(t * ((c:real^2)$2 - (b:real^2)$2)) / e` THEN
ASM_SIMP_TAC[REAL_LE_DIV; REAL_LE_MUL; REAL_SUB_LT; REAL_LT_IMP_LE] THEN
REWRITE_TAC[REAL_ARITH `a / e + b / e:real = (a + b) / e`] THEN
ASM_SIMP_TAC[REAL_LE_LDIV_EQ; REAL_MUL_LID] THEN
REWRITE_TAC[VECTOR_MUL_ASSOC] THEN BINOP_TAC THEN
AP_THM_TAC THEN AP_TERM_TAC THEN MATCH_MP_TAC(REAL_FIELD
`y < x /\ &0 < e ==> s = (s * (x - y)) / e * e / (x - y)`) THEN
ASM_REWRITE_TAC[];
MATCH_MP_TAC HULL_MINIMAL THEN
REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET; IN_INTER; IN_ELIM_THM] THEN
ASM_SIMP_TAC[HULL_INC; IN_INSERT; REAL_SUB_REFL; REAL_LT_IMP_LE] THEN
SIMP_TAC[REAL_LE_SUB_RADD; CONVEX_INTER; CONVEX_HALFSPACE_COMPONENT_LE;
CONVEX_CONVEX_HULL] THEN
REPEAT CONJ_TAC THENL
[UNDISCH_TAC `a' IN segment[b:real^2,a]` THEN
SPEC_TAC(`a':real^2`,`x:real^2`) THEN REWRITE_TAC[GSYM SUBSET] THEN
REWRITE_TAC[SEGMENT_CONVEX_HULL] THEN MATCH_MP_TAC HULL_MONO THEN
SET_TAC[];
EXPAND_TAC "a'";
UNDISCH_TAC `c' IN segment[b:real^2,c]` THEN
SPEC_TAC(`c':real^2`,`x:real^2`) THEN REWRITE_TAC[GSYM SUBSET] THEN
REWRITE_TAC[SEGMENT_CONVEX_HULL] THEN MATCH_MP_TAC HULL_MONO THEN
SET_TAC[];
EXPAND_TAC "c'"] THEN
REWRITE_TAC[VECTOR_ADD_COMPONENT; VECTOR_MUL_COMPONENT] THEN
REWRITE_TAC[REAL_ARITH
`(&1 - u) * b + u * a <= e + b <=> (a - b) * u <= e`] THEN
ASM_SIMP_TAC[REAL_DIV_LMUL; REAL_LT_IMP_NZ; REAL_SUB_LT] THEN
REWRITE_TAC[REAL_LE_REFL]];
ALL_TAC] THEN
SUBGOAL_THEN
`interior(convex hull {a,b,c}) INTER {x:real^2 | x$2 - b$2 < e} =
interior(convex hull {a',b,c'})`
ASSUME_TAC THENL
[REWRITE_TAC[REAL_LT_SUB_RADD; GSYM INTERIOR_HALFSPACE_COMPONENT_LE] THEN
ASM_REWRITE_TAC[GSYM INTERIOR_INTER; GSYM REAL_LE_SUB_RADD];
ALL_TAC] THEN
SUBGOAL_THEN
`?d:real^2. d IN interior(convex hull {a',b,c'}) /\ ~(d$1 = b$1)`
STRIP_ASSUME_TAC THENL
[UNDISCH_TAC `~(interior(convex hull {a':real^2,b,c'}) = {})` THEN
REWRITE_TAC[GSYM MEMBER_NOT_EMPTY; LEFT_IMP_EXISTS_THM] THEN
X_GEN_TAC `x:real^2` THEN DISCH_TAC THEN
ASM_CASES_TAC `(x:real^2)$1 = (b:real^2)$1` THENL
[ALL_TAC; EXISTS_TAC `x:real^2` THEN ASM_REWRITE_TAC[]] THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [IN_INTERIOR]) THEN
DISCH_THEN(X_CHOOSE_THEN `k:real` MP_TAC) THEN
DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN REWRITE_TAC[SUBSET] THEN
DISCH_THEN(fun th -> ASSUME_TAC th THEN MP_TAC th) THEN
DISCH_THEN(MP_TAC o SPEC `x + k / &2 % basis 1:real^2`) THEN ANTS_TAC THENL
[REWRITE_TAC[IN_BALL; NORM_ARITH `dist(x,x + e) = norm e`] THEN
SIMP_TAC[NORM_MUL; NORM_BASIS; DIMINDEX_GE_1; ARITH] THEN
UNDISCH_TAC `&0 < k` THEN REAL_ARITH_TAC;
DISCH_TAC] THEN
EXISTS_TAC `x + k / &2 % basis 1:real^2` THEN
REWRITE_TAC[VECTOR_ADD_COMPONENT; VECTOR_MUL_COMPONENT] THEN
ASM_SIMP_TAC[BASIS_COMPONENT; DIMINDEX_GE_1; ARITH; REAL_MUL_RID] THEN
ASM_SIMP_TAC[REAL_ARITH `&0 < k ==> ~(b + k / &2 = b)`] THEN
REWRITE_TAC[IN_INTERIOR] THEN EXISTS_TAC `k / &2` THEN
ASM_REWRITE_TAC[REAL_HALF; SUBSET] THEN X_GEN_TAC `y:real^2` THEN
REWRITE_TAC[IN_BALL] THEN DISCH_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN
REWRITE_TAC[IN_BALL] THEN MATCH_MP_TAC(NORM_ARITH
`!a. dist(x + a,y) < k / &2 /\ norm(a) = k / &2 ==> dist(x,y) < k`) THEN
EXISTS_TAC `k / &2 % basis 1:real^2` THEN ASM_REWRITE_TAC[NORM_MUL] THEN
SIMP_TAC[NORM_BASIS; DIMINDEX_GE_1; LE_REFL] THEN
UNDISCH_TAC `&0 < k` THEN REAL_ARITH_TAC;
ALL_TAC] THEN
SUBGOAL_THEN
`path_image(polygonal_path(CONS a (CONS b (CONS c p))))
SUBSET {x:real^2 | x$2 >= b$2}`
MP_TAC THENL
[MATCH_MP_TAC SUBSET_TRANS THEN
EXISTS_TAC
`convex hull(set_of_list(CONS (a:real^2) (CONS b (CONS c p))))` THEN
SIMP_TAC[PATH_IMAGE_POLYGONAL_PATH_SUBSET_CONVEX_HULL; NOT_CONS_NIL] THEN
MATCH_MP_TAC HULL_MINIMAL THEN
REWRITE_TAC[CONVEX_HALFSPACE_COMPONENT_GE] THEN
REWRITE_TAC[set_of_list; INSERT_SUBSET; IN_ELIM_THM; EMPTY_SUBSET] THEN
ASM_SIMP_TAC[SUBSET; IN_SET_OF_LIST; real_ge; IN_ELIM_THM; REAL_LT_IMP_LE;
REAL_LE_REFL];
GEN_REWRITE_TAC LAND_CONV [SUBSET] THEN
ASM_SIMP_TAC[POLYGONAL_PATH_CONS_CONS; NOT_CONS_NIL] THEN
REWRITE_TAC[IN_ELIM_THM; real_ge] THEN DISCH_TAC] THEN
SUBGOAL_THEN
`(:real^2) DIFF {x | x$2 >= b$2} SUBSET
outside(path_image
(linepath(a,b) ++ linepath(b,c) ++ polygonal_path(CONS c p)))`
MP_TAC THENL
[MATCH_MP_TAC OUTSIDE_SUBSET_CONVEX THEN
REWRITE_TAC[CONVEX_HALFSPACE_COMPONENT_GE] THEN
ASM_REWRITE_TAC[SUBSET; real_ge; IN_ELIM_THM];
REWRITE_TAC[SUBSET; real_ge; IN_ELIM_THM; IN_UNIV;
IN_DIFF; REAL_NOT_LE] THEN
DISCH_TAC] THEN
ABBREV_TAC
`d':real^2 = d - (&1 + (d:real^2)$2 - (b:real^2)$2) % basis 2` THEN
SUBGOAL_THEN `(d':real^2) IN outside(path_image
(linepath(a,b) ++ linepath(b,c) ++ polygonal_path(CONS c p)))`
ASSUME_TAC THENL
[FIRST_X_ASSUM MATCH_MP_TAC THEN EXPAND_TAC "d'" THEN
REWRITE_TAC[VECTOR_SUB_COMPONENT; VECTOR_MUL_COMPONENT] THEN
SIMP_TAC[BASIS_COMPONENT; DIMINDEX_2; ARITH] THEN REAL_ARITH_TAC;
ALL_TAC] THEN
SUBGOAL_THEN `(a':real^2)$2 - (b:real^2)$2 = e /\
(c':real^2)$2 - (b:real^2)$2 = e`
STRIP_ASSUME_TAC THENL
[MAP_EVERY EXPAND_TAC ["a'"; "c'"] THEN
REWRITE_TAC[VECTOR_ADD_COMPONENT; VECTOR_MUL_COMPONENT] THEN
REWRITE_TAC[REAL_ARITH `((&1 - u) * b + u * a) - b = u * (a - b)`] THEN
ASM_SIMP_TAC[REAL_DIV_RMUL; REAL_ARITH `b < a ==> ~(a - b = &0)`];
ALL_TAC] THEN
SUBGOAL_THEN `(b:real^2)$2 < (d:real^2)$2 /\ (d:real^2)$2 < (b:real^2)$2 + e`
STRIP_ASSUME_TAC THENL
[UNDISCH_TAC `(d:real^2) IN interior(convex hull {a',b,c'})` THEN
ASM_SIMP_TAC[INTERIOR_CONVEX_HULL_3_MINIMAL] THEN
REWRITE_TAC[IN_ELIM_THM; LEFT_IMP_EXISTS_THM] THEN
MAP_EVERY X_GEN_TAC [`r:real`; `s:real`; `t:real`] THEN
REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
DISCH_THEN(SUBST1_TAC o SYM) THEN
REWRITE_TAC[VECTOR_ADD_COMPONENT; VECTOR_MUL_COMPONENT] THEN
RULE_ASSUM_TAC(REWRITE_RULE[REAL_EQ_SUB_RADD]) THEN ASM_REWRITE_TAC[] THEN
FIRST_ASSUM(SUBST1_TAC o MATCH_MP (REAL_ARITH
`r + s + t = &1 ==> s = &1 - (r + t)`)) THEN
REWRITE_TAC[REAL_ARITH
`b < r * x + (&1 - (r + t)) * b + t * x <=> (r + t) * b < (r + t) * x`;
REAL_ARITH
`r * (e + b) + (&1 - (r + t)) * b + t * (e + b) < b + e <=>
(r + t) * e < &1 * e`] THEN
ASM_SIMP_TAC[REAL_LT_LMUL_EQ; REAL_LT_ADD; REAL_LT_RMUL_EQ] THEN
ASM_REAL_ARITH_TAC;
ALL_TAC] THEN
SUBGOAL_THEN `(d':real^2)$2 + &1 = (b:real^2)$2` ASSUME_TAC THENL
[EXPAND_TAC "d'" THEN REWRITE_TAC[VECTOR_SUB_COMPONENT] THEN
SIMP_TAC[VECTOR_MUL_COMPONENT; BASIS_COMPONENT; DIMINDEX_2; ARITH] THEN
REAL_ARITH_TAC;
ALL_TAC] THEN
SUBGOAL_THEN
`convex hull {a':real^2,b,c'} SUBSET convex hull {a,b,c}`
ASSUME_TAC THENL
[MATCH_MP_TAC HULL_MINIMAL THEN
REWRITE_TAC[CONVEX_CONVEX_HULL; INSERT_SUBSET; EMPTY_SUBSET] THEN
SIMP_TAC[HULL_INC; IN_INSERT] THEN CONJ_TAC THENL
[UNDISCH_TAC `(a':real^2) IN segment[b,a]` THEN
SPEC_TAC(`a':real^2`,`x:real^2`);
UNDISCH_TAC `(c':real^2) IN segment[b,c]` THEN
SPEC_TAC(`c':real^2`,`x:real^2`)] THEN
REWRITE_TAC[GSYM SUBSET] THEN REWRITE_TAC[SEGMENT_CONVEX_HULL] THEN
MATCH_MP_TAC HULL_MONO THEN SET_TAC[];
ALL_TAC] THEN
SUBGOAL_THEN `~(d' IN convex hull {a:real^2,b,c})` ASSUME_TAC THENL
[MATCH_MP_TAC(SET_RULE
`!t. s SUBSET t /\ ~(x IN t) ==> ~(x IN s)`) THEN
EXISTS_TAC `{x | (x:real^2)$2 >= (b:real^2)$2}` THEN
SIMP_TAC[SUBSET_HULL; CONVEX_HALFSPACE_COMPONENT_GE] THEN
ASM_REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET; IN_ELIM_THM; real_ge] THEN
ASM_REAL_ARITH_TAC;
ALL_TAC] THEN
SUBGOAL_THEN `~(d' IN convex hull {a':real^2,b,c'})` ASSUME_TAC THENL
[ASM SET_TAC[]; ALL_TAC] THEN
SUBGOAL_THEN
`~(segment[d:real^2,d'] INTER frontier(convex hull {a',b,c'}) = {})`
MP_TAC THENL
[MATCH_MP_TAC CONNECTED_INTER_FRONTIER THEN
REWRITE_TAC[CONNECTED_SEGMENT; GSYM MEMBER_NOT_EMPTY] THEN CONJ_TAC THENL
[EXISTS_TAC `d:real^2` THEN REWRITE_TAC[ENDS_IN_SEGMENT; IN_INTER] THEN
ASM_MESON_TAC[INTERIOR_SUBSET; SUBSET];
EXISTS_TAC `d':real^2` THEN ASM_REWRITE_TAC[ENDS_IN_SEGMENT; IN_DIFF]];
ALL_TAC] THEN
GEN_REWRITE_TAC LAND_CONV [GSYM MEMBER_NOT_EMPTY] THEN
DISCH_THEN(X_CHOOSE_THEN `x:real^2` MP_TAC) THEN REWRITE_TAC[IN_INTER] THEN
ASM_CASES_TAC `x:real^2 = d` THENL
[ASM_REWRITE_TAC[IN_DIFF; frontier]; ALL_TAC] THEN
ASM_CASES_TAC `x:real^2 = d'` THENL
[ASM_REWRITE_TAC[IN_DIFF; frontier] THEN
SUBGOAL_THEN `closure(convex hull {a':real^2,b,c'}) = convex hull {a',b,c'}`
(fun th -> ASM_REWRITE_TAC[th]) THEN
MATCH_MP_TAC CLOSURE_CLOSED THEN MATCH_MP_TAC COMPACT_IMP_CLOSED THEN
MESON_TAC[COMPACT_CONVEX_HULL; FINITE_IMP_COMPACT; FINITE_RULES];
ALL_TAC] THEN
ASM_REWRITE_TAC[SEGMENT_CLOSED_OPEN; IN_UNION; IN_INSERT; NOT_IN_EMPTY] THEN
STRIP_TAC THEN
SUBGOAL_THEN `(d':real^2)$1 = (d:real^2)$1` ASSUME_TAC THENL
[EXPAND_TAC "d'" THEN REWRITE_TAC[VECTOR_SUB_COMPONENT] THEN
SIMP_TAC[VECTOR_MUL_COMPONENT; BASIS_COMPONENT; DIMINDEX_2; ARITH] THEN
REAL_ARITH_TAC;
ALL_TAC] THEN
SUBGOAL_THEN `(x:real^2)$1 = (d:real^2)$1` ASSUME_TAC THENL
[MP_TAC(ISPECL [`d:real^2`; `d':real^2`; `x:real^2`] SEGMENT_VERTICAL) THEN
ASM_REWRITE_TAC[SEGMENT_CLOSED_OPEN; IN_UNION] THEN ASM_REAL_ARITH_TAC;
ALL_TAC] THEN
SUBGOAL_THEN `~(x:real^2 = b)` ASSUME_TAC THENL
[ASM_MESON_TAC[]; ALL_TAC] THEN
SUBGOAL_THEN `(x:real^2)$2 < (b:real^2)$2 + e` ASSUME_TAC THENL
[MP_TAC(ISPECL [`d:real^2`; `d':real^2`; `x:real^2`] SEGMENT_VERTICAL) THEN
ASM_REWRITE_TAC[SEGMENT_CLOSED_OPEN; IN_UNION] THEN ASM_REAL_ARITH_TAC;
ALL_TAC] THEN
SUBGOAL_THEN `~(x:real^2 = a) /\ ~(x = c)` STRIP_ASSUME_TAC THENL
[REWRITE_TAC[CART_EQ; DIMINDEX_2; FORALL_2] THEN ASM_REAL_ARITH_TAC;
ALL_TAC] THEN
SUBGOAL_THEN `(x:real^2) IN (segment(b,a) UNION segment(b,c))`
ASSUME_TAC THENL
[UNDISCH_TAC `(x:real^2) IN frontier(convex hull {a':real^2,b,c'})` THEN
ASM_SIMP_TAC[open_segment; IN_UNION; IN_DIFF; IN_INSERT; NOT_IN_EMPTY] THEN
REWRITE_TAC[FRONTIER_OF_TRIANGLE] THEN MATCH_MP_TAC(SET_RULE
`~(x IN u) /\ s SUBSET s' /\ t SUBSET t'
==> x IN (s UNION t UNION u) ==> x IN s' \/ x IN t'`) THEN
ASM_REWRITE_TAC[SUBSET_SEGMENT; ENDS_IN_SEGMENT] THEN DISCH_TAC THEN
MP_TAC(ISPECL [`c':real^2`; `a':real^2`; `x:real^2`]
SEGMENT_HORIZONTAL) THEN
ASM_REWRITE_TAC[] THEN ASM_REAL_ARITH_TAC;
ALL_TAC] THEN
SUBGOAL_THEN
`segment[d:real^2,d'] INTER path_image(polygonal_path(CONS c p)) = {}`
ASSUME_TAC THENL
[MATCH_MP_TAC(SET_RULE
`!u. t SUBSET u /\ s INTER u = {} ==> s INTER t = {}`) THEN
EXISTS_TAC `{x:real^2 | x$2 >= (b:real^2)$2 + e}` THEN CONJ_TAC THENL
[MATCH_MP_TAC SUBSET_TRANS THEN
EXISTS_TAC `convex hull(set_of_list(CONS c p)) :real^2->bool` THEN
SIMP_TAC[PATH_IMAGE_POLYGONAL_PATH_SUBSET_CONVEX_HULL; NOT_CONS_NIL] THEN
MATCH_MP_TAC HULL_MINIMAL THEN
REWRITE_TAC[CONVEX_HALFSPACE_COMPONENT_GE;
set_of_list; INSERT_SUBSET] THEN
REWRITE_TAC[SUBSET; IN_SET_OF_LIST; IN_ELIM_THM] THEN
ASM_SIMP_TAC[real_ge; REAL_ARITH `b + e <= x <=> e <= x - b`];
REWRITE_TAC[SET_RULE `s INTER t = {} <=> !x. x IN s ==> ~(x IN t)`] THEN
X_GEN_TAC `y:real^2` THEN DISCH_TAC THEN
MP_TAC(ISPECL[`d:real^2`; `d':real^2`; `y:real^2`] SEGMENT_VERTICAL) THEN
ASM_REWRITE_TAC[IN_ELIM_THM; real_ge] THEN ASM_REAL_ARITH_TAC];
ALL_TAC] THEN
SUBGOAL_THEN `(d:real^2) IN interior(convex hull {a,b,c})` ASSUME_TAC THENL
[UNDISCH_TAC `(d:real^2) IN interior(convex hull {a', b, c'})` THEN
SPEC_TAC(`d:real^2`,`d:real^2`) THEN REWRITE_TAC[GSYM SUBSET] THEN
MATCH_MP_TAC SUBSET_INTERIOR THEN ASM_REWRITE_TAC[];
ALL_TAC] THEN
SUBGOAL_THEN `~(d':real^2 = d)` ASSUME_TAC THENL
[ASM_MESON_TAC[IN_SEGMENT]; ALL_TAC] THEN
SUBGOAL_THEN
`!y:real^2. y IN segment[d,d'] /\
y IN (segment (b,a) UNION segment (b,c))
==> y = x`
ASSUME_TAC THENL
[GEN_TAC THEN STRIP_TAC THEN
SUBGOAL_THEN `collinear {d:real^2,x,y}` MP_TAC THENL
[REWRITE_TAC[COLLINEAR_AFFINE_HULL] THEN
MAP_EVERY EXISTS_TAC [`d:real^2`; `d':real^2`] THEN
REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET] THEN
REPEAT CONJ_TAC THEN MATCH_MP_TAC
(REWRITE_RULE[SUBSET] CONVEX_HULL_SUBSET_AFFINE_HULL) THEN
ASM_REWRITE_TAC[GSYM SEGMENT_CONVEX_HULL; ENDS_IN_SEGMENT] THEN
ASM_REWRITE_TAC[SEGMENT_CLOSED_OPEN; IN_UNION];
ALL_TAC] THEN
REWRITE_TAC[COLLINEAR_BETWEEN_CASES; BETWEEN_IN_SEGMENT] THEN
ASM_SIMP_TAC[SEGMENT_CLOSED_OPEN; IN_UNION; IN_INSERT; NOT_IN_EMPTY] THEN
ASM_CASES_TAC `x:real^2 = y` THEN ASM_REWRITE_TAC[] THEN
SUBGOAL_THEN
`(x:real^2) IN frontier(convex hull {a,b,c}) /\
(y:real^2) IN frontier(convex hull {a,b,c})`
MP_TAC THENL
[REWRITE_TAC[FRONTIER_OF_TRIANGLE] THEN
REWRITE_TAC[SEGMENT_CLOSED_OPEN; IN_UNION] THEN
RULE_ASSUM_TAC(REWRITE_RULE[IN_UNION]) THEN ASM_MESON_TAC[SEGMENT_SYM];
REWRITE_TAC[frontier; IN_DIFF]] THEN
ASM_CASES_TAC `y:real^2 = d` THEN ASM_REWRITE_TAC[] THEN
REPEAT STRIP_TAC THENL
[MAP_EVERY UNDISCH_TAC
[`(d:real^2) IN segment (x,y)`;
`(y:real^2) IN segment [d,d']`;
`(x:real^2) IN segment(d,d')`] THEN
ASM_REWRITE_TAC[IN_SEGMENT] THEN
REPLICATE_TAC 2 (STRIP_TAC THEN ASM_REWRITE_TAC[]) THEN
ASM_REWRITE_TAC[VECTOR_MUL_EQ_0; VECTOR_SUB_EQ; VECTOR_ARITH
`d = (&1 - w) % ((&1 - u) % d + u % d') + w % ((&1 - v) % d + v % d') <=>
((&1 - w) * u + w * v) % (d' - d) = vec 0`] THEN
DISCH_THEN(CHOOSE_THEN MP_TAC) THEN
REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
ASM_SIMP_TAC[REAL_SUB_LE; REAL_LE_MUL; REAL_LT_IMP_LE; REAL_ARITH
`&0 <= x /\ &0 <= y ==> (x + y = &0 <=> x = &0 /\ y = &0)`] THEN
REWRITE_TAC[REAL_ENTIRE] THEN ASM_REAL_ARITH_TAC;
UNDISCH_TAC `~(x IN interior(convex hull {a:real^2, b, c}))` THEN
UNDISCH_TAC `x IN segment (y:real^2,d)` THEN
SPEC_TAC(`x:real^2`,`x:real^2`) THEN ASM_REWRITE_TAC[GSYM SUBSET] THEN
ONCE_REWRITE_TAC[SEGMENT_SYM] THEN
MATCH_MP_TAC IN_INTERIOR_CLOSURE_CONVEX_SEGMENT THEN
ASM_REWRITE_TAC[CONVEX_CONVEX_HULL];
UNDISCH_TAC `~(y IN interior(convex hull {a:real^2, b, c}))` THEN
UNDISCH_TAC `y IN segment (d:real^2,x)` THEN
SPEC_TAC(`y:real^2`,`y:real^2`) THEN ASM_REWRITE_TAC[GSYM SUBSET] THEN
MATCH_MP_TAC IN_INTERIOR_CLOSURE_CONVEX_SEGMENT THEN
ASM_REWRITE_TAC[CONVEX_CONVEX_HULL]];
ALL_TAC] THEN
SUBGOAL_THEN `pathfinish(polygonal_path p) = (a:real^2)` ASSUME_TAC THENL
[ASM_REWRITE_TAC[PATHFINISH_POLYGONAL_PATH]; ALL_TAC] THEN
SUBGOAL_THEN `segment(a:real^2,b) INTER segment(b,c) = {}` ASSUME_TAC THENL
[UNDISCH_TAC `segment[a:real^2,b] INTER segment[b,c] SUBSET {a, b}` THEN
REWRITE_TAC[SUBSET; EXTENSION; IN_INTER; NOT_IN_EMPTY] THEN
MATCH_MP_TAC MONO_FORALL THEN
REWRITE_TAC[open_segment; IN_DIFF; IN_INSERT; NOT_IN_EMPTY] THEN
MESON_TAC[];
ALL_TAC] THEN
SUBGOAL_THEN
`(d:real^2) IN inside(path_image
(linepath(a,b) ++ linepath(b,c) ++ polygonal_path(CONS c p)))`
ASSUME_TAC THENL
[UNDISCH_TAC `x IN segment(b:real^2,a) UNION segment (b,c)` THEN
REWRITE_TAC[IN_UNION] THEN STRIP_TAC THENL
[MP_TAC(ISPECL [`a:real^2`; `b:real^2`; `d:real^2`; `d':real^2`;
`linepath(b:real^2,c) ++ polygonal_path(CONS c p)`;
`x:real^2`] PARITY_LEMMA) THEN
SUBGOAL_THEN
`path_image((linepath(b:real^2,c) ++ polygonal_path(CONS c p)) ++
linepath(a,b)) =
path_image(linepath(a,b) ++ linepath(b:real^2,c) ++
polygonal_path(CONS c p))`
SUBST1_TAC THENL
[MATCH_MP_TAC PATH_IMAGE_SYM THEN
REWRITE_TAC[PATHSTART_JOIN; PATHFINISH_JOIN] THEN
REWRITE_TAC[PATHSTART_LINEPATH; PATHFINISH_LINEPATH] THEN
UNDISCH_TAC `pathfinish(linepath(a,b) ++
linepath (b,c) ++ polygonal_path(CONS c p)):real^2 = a` THEN
ASM_REWRITE_TAC[PATHFINISH_JOIN; PATHFINISH_POLYGONAL_PATH];
ALL_TAC] THEN
ASM_REWRITE_TAC[] THEN DISCH_THEN MATCH_MP_TAC THEN REPEAT CONJ_TAC THENL
[W(MP_TAC o PART_MATCH (lhs o rand) SIMPLE_PATH_SYM o snd) THEN
ASM_REWRITE_TAC[PATHSTART_JOIN; PATHFINISH_JOIN] THEN
ASM_REWRITE_TAC[PATHSTART_LINEPATH; PATHFINISH_LINEPATH] THEN
REWRITE_TAC[PATHFINISH_POLYGONAL_PATH] THEN
ASM_REWRITE_TAC[NOT_CONS_NIL; LAST];
REWRITE_TAC[PATHSTART_JOIN; PATHSTART_LINEPATH];
REWRITE_TAC[PATHFINISH_JOIN; PATHFINISH_POLYGONAL_PATH] THEN
ASM_REWRITE_TAC[NOT_CONS_NIL; LAST];
MATCH_MP_TAC(SET_RULE
`x IN s /\ x IN t /\ (!y. y IN s /\ y IN t ==> y = x)
==> s INTER t = {x}`) THEN
SUBST1_TAC(ISPECL[`a:real^2`; `b:real^2`] (CONJUNCT2 SEGMENT_SYM)) THEN
ASM_REWRITE_TAC[] THEN
RULE_ASSUM_TAC(REWRITE_RULE[SEGMENT_CLOSED_OPEN]) THEN ASM SET_TAC[];
SIMP_TAC[PATH_IMAGE_JOIN; PATHFINISH_LINEPATH; PATH_IMAGE_LINEPATH;
PATHSTART_POLYGONAL_PATH; NOT_CONS_NIL; HD] THEN
ASM_REWRITE_TAC[SET_RULE `s INTER (t UNION u) = {} <=>
s INTER t = {} /\ s INTER u = {}`] THEN
REWRITE_TAC[EXTENSION; IN_INTER; NOT_IN_EMPTY] THEN
X_GEN_TAC `y:real^2` THEN
DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
SUBGOAL_THEN `(y:real^2)$1 = (d:real^2)$1` ASSUME_TAC THENL
[MP_TAC(ISPECL [`d:real^2`; `d':real^2`; `y:real^2`]
SEGMENT_VERTICAL) THEN
ASM_REWRITE_TAC[SEGMENT_CLOSED_OPEN; IN_UNION] THEN
ASM_REAL_ARITH_TAC;
ALL_TAC] THEN
ASM_REWRITE_TAC[SEGMENT_CLOSED_OPEN; IN_UNION;
IN_INSERT; NOT_IN_EMPTY] THEN
ASM_CASES_TAC `y:real^2 = b` THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
RULE_ASSUM_TAC(SUBS[ISPECL [`a:real^2`; `b:real^2`]
(CONJUNCT2 SEGMENT_SYM)]) THEN
ASM_CASES_TAC `y:real^2 = c` THENL [ALL_TAC; ASM SET_TAC[]] THEN
UNDISCH_THEN `y:real^2 = c` SUBST_ALL_TAC THEN
MP_TAC(ISPECL [`d:real^2`; `d':real^2`; `c:real^2`]
SEGMENT_VERTICAL) THEN
ASM_REWRITE_TAC[SEGMENT_CLOSED_OPEN; IN_UNION] THEN
ASM_REAL_ARITH_TAC];
MP_TAC(ISPECL [`b:real^2`; `c:real^2`; `d:real^2`; `d':real^2`;
`polygonal_path(CONS c p) ++ linepath(a:real^2,b)`;
`x:real^2`] PARITY_LEMMA) THEN
SUBGOAL_THEN
`path_image((polygonal_path (CONS c p) ++ linepath (a,b)) ++
linepath(b:real^2,c)) =
path_image(linepath(a,b) ++ linepath(b:real^2,c) ++
polygonal_path(CONS c p))`
SUBST1_TAC THENL
[ASM_SIMP_TAC[PATH_IMAGE_JOIN; PATHSTART_JOIN; PATHFINISH_JOIN;
PATHSTART_LINEPATH; PATHFINISH_LINEPATH;
PATHSTART_POLYGONAL_PATH; PATHFINISH_POLYGONAL_PATH;
NOT_CONS_NIL; HD; LAST] THEN
REWRITE_TAC[UNION_ACI];
ALL_TAC] THEN
ASM_REWRITE_TAC[] THEN DISCH_THEN MATCH_MP_TAC THEN REPEAT CONJ_TAC THENL
[W(MP_TAC o PART_MATCH (lhs o rand) (GSYM SIMPLE_PATH_ASSOC) o snd) THEN
ANTS_TAC THENL
[ALL_TAC;
DISCH_THEN SUBST1_TAC THEN
W(MP_TAC o PART_MATCH (lhs o rand) SIMPLE_PATH_SYM o snd) THEN
ANTS_TAC THENL
[ALL_TAC;
DISCH_THEN SUBST1_TAC THEN
W(MP_TAC o PART_MATCH (lhs o rand) (GSYM SIMPLE_PATH_ASSOC) o
snd) THEN
ASM_REWRITE_TAC[] THEN DISCH_THEN MATCH_MP_TAC]] THEN
ASM_SIMP_TAC[GSYM SIMPLE_PATH_ASSOC;PATHSTART_JOIN;
PATHFINISH_JOIN;
PATHSTART_LINEPATH; PATHFINISH_LINEPATH;
PATHSTART_POLYGONAL_PATH; PATHFINISH_POLYGONAL_PATH;
NOT_CONS_NIL; HD; LAST];
REWRITE_TAC[PATHSTART_JOIN; PATHSTART_POLYGONAL_PATH] THEN
REWRITE_TAC[NOT_CONS_NIL; HD];
REWRITE_TAC[PATHFINISH_JOIN; PATHFINISH_LINEPATH];
MATCH_MP_TAC(SET_RULE
`x IN s /\ x IN t /\ (!y. y IN s /\ y IN t ==> y = x)
==> s INTER t = {x}`) THEN
SUBST1_TAC(ISPECL[`a:real^2`; `b:real^2`] (CONJUNCT2 SEGMENT_SYM)) THEN
ASM_REWRITE_TAC[] THEN
RULE_ASSUM_TAC(REWRITE_RULE[SEGMENT_CLOSED_OPEN]) THEN ASM SET_TAC[];
ASM_SIMP_TAC[PATH_IMAGE_JOIN; PATHSTART_LINEPATH; NOT_CONS_NIL; HD;
PATH_IMAGE_LINEPATH; PATHFINISH_POLYGONAL_PATH; LAST] THEN
ASM_REWRITE_TAC[SET_RULE `s INTER (t UNION u) = {} <=>
s INTER t = {} /\ s INTER u = {}`] THEN
REWRITE_TAC[EXTENSION; IN_INTER; NOT_IN_EMPTY] THEN
X_GEN_TAC `y:real^2` THEN
DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
SUBGOAL_THEN `(y:real^2)$1 = (d:real^2)$1` ASSUME_TAC THENL
[MP_TAC(ISPECL [`d:real^2`; `d':real^2`; `y:real^2`]
SEGMENT_VERTICAL) THEN
ASM_REWRITE_TAC[SEGMENT_CLOSED_OPEN; IN_UNION] THEN
ASM_REAL_ARITH_TAC;
ALL_TAC] THEN
ASM_REWRITE_TAC[SEGMENT_CLOSED_OPEN; IN_UNION;
IN_INSERT; NOT_IN_EMPTY] THEN
ASM_CASES_TAC `y:real^2 = b` THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
RULE_ASSUM_TAC(SUBS[ISPECL [`a:real^2`; `b:real^2`]
(CONJUNCT2 SEGMENT_SYM)]) THEN
ONCE_REWRITE_TAC[SEGMENT_SYM] THEN
ASM_CASES_TAC `y:real^2 = a` THENL [ALL_TAC; ASM SET_TAC[]] THEN
UNDISCH_THEN `y:real^2 = a` SUBST_ALL_TAC THEN
MP_TAC(ISPECL [`d:real^2`; `d':real^2`; `a:real^2`]
SEGMENT_VERTICAL) THEN
ASM_REWRITE_TAC[SEGMENT_CLOSED_OPEN; IN_UNION] THEN
ASM_REAL_ARITH_TAC]];
ALL_TAC] THEN
SUBGOAL_THEN `~affine_dependent{a:real^2,b,c}` ASSUME_TAC THENL
[ASM_MESON_TAC[AFFINE_DEPENDENT_IMP_COLLINEAR_3]; ALL_TAC] THEN
ASM_CASES_TAC
`path_image(polygonal_path(CONS c p)) INTER
convex hull {a,b,c} SUBSET {a:real^2,c}`
THENL
[MAP_EVERY EXISTS_TAC [`a:real^2`; `c:real^2`] THEN
ASM_REWRITE_TAC[MEM] THEN X_GEN_TAC `y:real^2` THEN DISCH_TAC THEN
MATCH_MP_TAC INSIDE_SAME_COMPONENT THEN
EXISTS_TAC `d:real^2` THEN ASM_REWRITE_TAC[] THEN
REWRITE_TAC[connected_component] THEN
EXISTS_TAC `segment[d:real^2,y]` THEN
REWRITE_TAC[CONNECTED_SEGMENT; ENDS_IN_SEGMENT] THEN
MATCH_MP_TAC SUBSET_TRANS THEN EXISTS_TAC
`convex hull {a:real^2,b,c} DIFF (segment[a,b] UNION segment[b,c])` THEN
CONJ_TAC THENL
[ALL_TAC;
SIMP_TAC[PATH_IMAGE_JOIN; PATHSTART_JOIN; PATHFINISH_LINEPATH;
PATHSTART_LINEPATH; PATHSTART_POLYGONAL_PATH; NOT_CONS_NIL; HD] THEN
REWRITE_TAC[PATH_IMAGE_LINEPATH] THEN
FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (SET_RULE
`t INTER s SUBSET c
==> c SUBSET (a UNION b)
==> s DIFF (a UNION b) SUBSET UNIV DIFF (a UNION b UNION t)`)) THEN
REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET; IN_UNION; ENDS_IN_SEGMENT]] THEN
REWRITE_TAC[SEGMENT_CONVEX_HULL] THEN MATCH_MP_TAC HULL_MINIMAL THEN
REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET] THEN REPEAT CONJ_TAC THENL
[REWRITE_TAC[IN_DIFF] THEN CONJ_TAC THENL
[ASM_MESON_TAC[INTERIOR_SUBSET; SUBSET]; ALL_TAC] THEN
SUBGOAL_THEN `~(d IN frontier(convex hull {a:real^2,b,c}))` MP_TAC THENL
[ASM_REWRITE_TAC[frontier; IN_DIFF];
REWRITE_TAC[FRONTIER_OF_TRIANGLE; SEGMENT_CONVEX_HULL] THEN SET_TAC[]];
REWRITE_TAC[IN_DIFF; IN_UNION] THEN REPEAT STRIP_TAC THENL
[UNDISCH_TAC `y IN segment(a:real^2,c)` THEN
REWRITE_TAC[open_segment; IN_DIFF; SEGMENT_CONVEX_HULL] THEN
MATCH_MP_TAC(SET_RULE `s SUBSET t ==> x IN s /\ P x ==> x IN t`) THEN
MATCH_MP_TAC HULL_MONO THEN SET_TAC[];
UNDISCH_TAC `~collinear{a:real^2,b,c}` THEN REWRITE_TAC[] THEN
ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {b,a,c}`] THEN
MATCH_MP_TAC COLLINEAR_3_TRANS THEN EXISTS_TAC `y:real^2` THEN
MAP_EVERY UNDISCH_TAC
[`y IN convex hull {a:real^2, b}`; `y IN segment(a:real^2,c)`] THEN
REWRITE_TAC[open_segment; GSYM SEGMENT_CONVEX_HULL; IN_DIFF] THEN
REWRITE_TAC[DE_MORGAN_THM; IN_INSERT; NOT_IN_EMPTY] THEN
DISCH_THEN(CONJUNCTS_THEN2 MP_TAC STRIP_ASSUME_TAC) THEN
ASM_REWRITE_TAC[IMP_IMP; GSYM BETWEEN_IN_SEGMENT] THEN
DISCH_THEN(CONJUNCTS_THEN(MP_TAC o
MATCH_MP BETWEEN_IMP_COLLINEAR)) THEN
REWRITE_TAC[INSERT_AC; IMP_IMP];
UNDISCH_TAC `~collinear{a:real^2,b,c}` THEN REWRITE_TAC[] THEN
ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {b,c,a}`] THEN
MATCH_MP_TAC COLLINEAR_3_TRANS THEN EXISTS_TAC `y:real^2` THEN
MAP_EVERY UNDISCH_TAC
[`y IN convex hull {b:real^2, c}`; `y IN segment(a:real^2,c)`] THEN
REWRITE_TAC[open_segment; GSYM SEGMENT_CONVEX_HULL; IN_DIFF] THEN
REWRITE_TAC[DE_MORGAN_THM; IN_INSERT; NOT_IN_EMPTY] THEN
DISCH_THEN(CONJUNCTS_THEN2 MP_TAC STRIP_ASSUME_TAC) THEN
ASM_REWRITE_TAC[IMP_IMP; GSYM BETWEEN_IN_SEGMENT] THEN
DISCH_THEN(CONJUNCTS_THEN(MP_TAC o
MATCH_MP BETWEEN_IMP_COLLINEAR)) THEN
REWRITE_TAC[INSERT_AC; IMP_IMP]];
REWRITE_TAC[SET_RULE
`s DIFF (t UNION u) = (s DIFF t) INTER (s DIFF u)`] THEN
MATCH_MP_TAC CONVEX_INTER THEN CONJ_TAC THENL
[MP_TAC(ISPECL [`convex hull {a:real^2,b,c}`; `convex hull{a:real^2,b}`]
FACE_OF_STILLCONVEX) THEN
REWRITE_TAC[CONVEX_CONVEX_HULL] THEN MATCH_MP_TAC(TAUT
`p ==> (p <=> q /\ r /\ s) ==> r`) THEN
ASM_SIMP_TAC[FACE_OF_CONVEX_HULL_AFFINE_INDEPENDENT] THEN
EXISTS_TAC `{a:real^2,b}` THEN SET_TAC[];
MP_TAC(ISPECL [`convex hull {a:real^2,b,c}`; `convex hull{b:real^2,c}`]
FACE_OF_STILLCONVEX) THEN
REWRITE_TAC[CONVEX_CONVEX_HULL] THEN MATCH_MP_TAC(TAUT
`p ==> (p <=> q /\ r /\ s) ==> r`) THEN
ASM_SIMP_TAC[FACE_OF_CONVEX_HULL_AFFINE_INDEPENDENT] THEN
EXISTS_TAC `{b:real^2,c}` THEN SET_TAC[]]];
ALL_TAC] THEN
SUBGOAL_THEN
`?n:real^2.
~(n = vec 0) /\ orthogonal n (c - a) /\
&0 < n dot (c - b)`
STRIP_ASSUME_TAC THENL
[SUBGOAL_THEN `?n:real^2. ~(n = vec 0) /\ orthogonal n (c - a)`
STRIP_ASSUME_TAC THENL
[ONCE_REWRITE_TAC[ORTHOGONAL_SYM] THEN
MATCH_MP_TAC ORTHOGONAL_TO_VECTOR_EXISTS THEN
REWRITE_TAC[DIMINDEX_2; LE_REFL];
ALL_TAC] THEN
REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC (REAL_ARITH
`&0 < n dot (c - b) \/ &0 < --(n dot (c - b)) \/
(n:real^2) dot (c - b) = &0`)
THENL
[EXISTS_TAC `n:real^2` THEN ASM_REWRITE_TAC[];
EXISTS_TAC `--n:real^2` THEN ASM_REWRITE_TAC[DOT_LNEG] THEN
ASM_REWRITE_TAC[VECTOR_NEG_EQ_0; ORTHOGONAL_LNEG];
UNDISCH_TAC `~collinear{a:real^2,b,c}` THEN
ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {a,c,b}`] THEN
MATCH_MP_TAC(TAUT `p ==> ~p ==> q`) THEN
ONCE_REWRITE_TAC[COLLINEAR_3] THEN
MATCH_MP_TAC ORTHOGONAL_TO_ORTHOGONAL_2D THEN
EXISTS_TAC `n:real^2` THEN
ONCE_REWRITE_TAC[GSYM ORTHOGONAL_RNEG] THEN
ASM_REWRITE_TAC[VECTOR_NEG_SUB] THEN
ASM_REWRITE_TAC[orthogonal]];
ALL_TAC] THEN
SUBGOAL_THEN `n dot (a - b:real^2) = n dot (c - b)` ASSUME_TAC THENL
[REWRITE_TAC[DOT_RSUB; real_sub; REAL_EQ_ADD_RCANCEL] THEN
ONCE_REWRITE_TAC[REAL_ARITH `x = y <=> y - x = &0`] THEN
ASM_REWRITE_TAC[GSYM DOT_RSUB; GSYM orthogonal];
ALL_TAC] THEN
SUBGOAL_THEN
`!y:real^2. y IN convex hull {a,b,c} /\ ~(y = b) ==> &0 < n dot (y - b)`
ASSUME_TAC THENL
[REWRITE_TAC[CONVEX_HULL_3_ALT; FORALL_IN_GSPEC; IMP_CONJ] THEN
REWRITE_TAC[VECTOR_ARITH
`(a + u % (b - a) + v % (c - a)) - b =
(&1 - u - v) % (a - b) + v % (c - b)`] THEN
ASM_REWRITE_TAC[DOT_RADD; DOT_RMUL] THEN
MAP_EVERY X_GEN_TAC [`r:real`; `s:real`] THEN REPEAT STRIP_TAC THEN
REWRITE_TAC[REAL_ARITH `(&1 - u - v) * x + v * x = (&1 - u) * x`] THEN
MATCH_MP_TAC REAL_LT_MUL THEN ASM_REWRITE_TAC[] THEN
ASM_CASES_TAC `r = &1 /\ s = &0` THENL [ALL_TAC; ASM_REAL_ARITH_TAC] THEN
UNDISCH_TAC `~(a + r % (b - a) + s % (c - a):real^2 = b)` THEN
ASM_REWRITE_TAC[REAL_LT_REFL; REAL_SUB_LT] THEN VECTOR_ARITH_TAC;
ALL_TAC] THEN
SUBGOAL_THEN
`!y:real^2. y IN convex hull {a,b,c} ==> &0 <= n dot (y - b)`
ASSUME_TAC THENL
[GEN_TAC THEN ASM_CASES_TAC `y:real^2 = b` THEN
ASM_REWRITE_TAC[VECTOR_SUB_REFL; DOT_RZERO; REAL_LE_REFL] THEN
ASM_MESON_TAC[REAL_LT_IMP_LE];
ALL_TAC] THEN
SUBGOAL_THEN
`!y:real^2. y IN convex hull {a,b,c} ==> n dot (y - b) <= n dot (c - b)`
ASSUME_TAC THENL
[REWRITE_TAC[CONVEX_HULL_3_ALT; FORALL_IN_GSPEC] THEN
REWRITE_TAC[VECTOR_ARITH
`(a + u % (b - a) + v % (c - a)) - b =
(&1 - u - v) % (a - b) + v % (c - b)`] THEN
ASM_REWRITE_TAC[DOT_RADD; DOT_RMUL; REAL_ARITH
`(&1 - u - v) * x + v * x <= x <=> &0 <= u * x`] THEN
ASM_SIMP_TAC[REAL_LE_MUL; REAL_LT_IMP_LE];
ALL_TAC] THEN
MP_TAC(ISPECL [`\x:real^2. n dot (x - b)`;
`path_image (polygonal_path(CONS c p)) INTER convex hull {a:real^2,b,c}`]
CONTINUOUS_ATTAINS_INF) THEN
REWRITE_TAC[] THEN ANTS_TAC THENL
[REPEAT CONJ_TAC THENL
[MATCH_MP_TAC COMPACT_INTER THEN
SIMP_TAC[COMPACT_PATH_IMAGE; PATH_POLYGONAL_PATH] THEN
SIMP_TAC[COMPACT_CONVEX_HULL; FINITE_IMP_COMPACT;
FINITE_INSERT; FINITE_EMPTY];
ASM SET_TAC[];
SUBGOAL_THEN
`(\x:real^2. n dot (x - b)) = (\x. n dot x) o (\x. x - b)`
SUBST1_TAC THENL [REWRITE_TAC[o_DEF]; ALL_TAC] THEN
REWRITE_TAC[o_ASSOC] THEN MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN
REWRITE_TAC[CONTINUOUS_ON_LIFT_DOT] THEN
SIMP_TAC[CONTINUOUS_ON_SUB; CONTINUOUS_ON_CONST; CONTINUOUS_ON_ID]];
ALL_TAC] THEN
DISCH_TAC THEN
SUBGOAL_THEN
`?mx:real^2.
~(mx = a) /\ ~(mx = c) /\
mx IN path_image(polygonal_path(CONS c p)) INTER convex hull {a, b, c} /\
(!y. y IN
path_image(polygonal_path(CONS c p)) INTER convex hull {a, b, c}
==> n dot (mx - b) <= n dot (y - b))`
STRIP_ASSUME_TAC THENL
[FIRST_X_ASSUM(X_CHOOSE_THEN `mx:real^2` STRIP_ASSUME_TAC) THEN
SUBGOAL_THEN `n dot (mx - b:real^2) <= n dot (c - b)` MP_TAC THENL
[ASM SET_TAC[]; ALL_TAC] THEN
GEN_REWRITE_TAC LAND_CONV [REAL_LE_LT] THEN STRIP_TAC THENL
[EXISTS_TAC `mx:real^2` THEN ASM_MESON_TAC[REAL_LT_REFL]; ALL_TAC] THEN
UNDISCH_TAC `~(path_image(polygonal_path(CONS c p)) INTER
convex hull {a, b, c} SUBSET {a:real^2, c})` THEN
REWRITE_TAC[SUBSET; NOT_FORALL_THM; NOT_IMP; IN_INSERT; NOT_IN_EMPTY] THEN
MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `my:real^2` THEN
REWRITE_TAC[DE_MORGAN_THM] THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
X_GEN_TAC `y:real^2` THEN REWRITE_TAC[IN_INTER] THEN STRIP_TAC THEN
MATCH_MP_TAC REAL_LE_TRANS THEN
EXISTS_TAC `n dot (mx - b:real^2)` THEN CONJ_TAC THENL
[ASM_REWRITE_TAC[] THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM SET_TAC[];
FIRST_X_ASSUM MATCH_MP_TAC THEN ASM SET_TAC[]];
FIRST_X_ASSUM(CHOOSE_THEN (K ALL_TAC))] THEN
ABBREV_TAC `m = (n:real^2) dot (mx - b)` THEN
SUBGOAL_THEN `&0 < m` ASSUME_TAC THENL
[EXPAND_TAC "m" THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
CONJ_TAC THENL [ASM SET_TAC[]; DISCH_THEN SUBST_ALL_TAC] THEN
UNDISCH_TAC
`segment[b:real^2,c] INTER path_image (polygonal_path (CONS c p))
SUBSET {c}` THEN
REWRITE_TAC[SUBSET; IN_INTER] THEN
DISCH_THEN(MP_TAC o SPEC `b:real^2`) THEN
ASM_REWRITE_TAC[IN_SING; ENDS_IN_SEGMENT] THEN ASM SET_TAC[];
ALL_TAC] THEN
SUBGOAL_THEN
`?z:real^2. MEM z p /\
z IN (convex hull {a,b,c} DIFF {a,c}) /\
n dot (z - b) = m`
STRIP_ASSUME_TAC THENL
[ALL_TAC;
MAP_EVERY EXISTS_TAC [`b:real^2`; `z:real^2`] THEN
ASM_REWRITE_TAC[MEM] THEN
MATCH_MP_TAC(TAUT `p /\ (p ==> q) ==> p /\ q`) THEN
CONJ_TAC THENL [ASM_MESON_TAC[REAL_LT_REFL]; DISCH_TAC] THEN
X_GEN_TAC `w:real^2` THEN DISCH_TAC THEN
MATCH_MP_TAC INSIDE_SAME_COMPONENT THEN
EXISTS_TAC `d:real^2` THEN ASM_REWRITE_TAC[] THEN
SUBGOAL_THEN `~(z:real^2 = a) /\ ~(z = c)` STRIP_ASSUME_TAC THENL
[ASM SET_TAC[]; ALL_TAC] THEN
SUBGOAL_THEN
`(z:real^2) IN path_image(polygonal_path(CONS c p)) /\
(z:real^2) IN path_image(polygonal_path p)`
STRIP_ASSUME_TAC THENL
[CONJ_TAC THEN MATCH_MP_TAC
(REWRITE_RULE[SUBSET] VERTICES_IN_PATH_IMAGE_POLYGONAL_PATH) THEN
ASM_REWRITE_TAC[IN_SET_OF_LIST; MEM];
ALL_TAC] THEN
SUBGOAL_THEN `~(z IN segment[a:real^2,b]) /\ ~(z IN segment[b,c])`
STRIP_ASSUME_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
SUBGOAL_THEN `~collinear{b:real^2,a,z} /\ ~collinear{b,c,z}`
STRIP_ASSUME_TAC THENL
[ASM_SIMP_TAC[COLLINEAR_3_AFFINE_HULL] THEN
MATCH_MP_TAC(SET_RULE
`!c. x IN c /\ ~(x IN (a INTER c)) /\ ~(x IN (b INTER c))
==> ~(x IN a) /\ ~(x IN b)`) THEN
EXISTS_TAC `convex hull {a:real^2,b,c}` THEN
CONJ_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
ASM_SIMP_TAC[GSYM AFFINE_INDEPENDENT_CONVEX_AFFINE_HULL;
INSERT_SUBSET; EMPTY_SUBSET; IN_INSERT] THEN
ASM_REWRITE_TAC[GSYM SEGMENT_CONVEX_HULL] THEN
ONCE_REWRITE_TAC[SEGMENT_SYM] THEN ASM_REWRITE_TAC[];
ALL_TAC] THEN
SUBGOAL_THEN
`segment(b:real^2,z) INTER segment[a,b] = {} /\
segment(b,z) INTER segment[b,c] = {}`
STRIP_ASSUME_TAC THENL
[REWRITE_TAC[EXTENSION; IN_INTER; NOT_IN_EMPTY] THEN
CONJ_TAC THEN X_GEN_TAC `v:real^2` THEN STRIP_TAC THENL
[UNDISCH_TAC `~collinear{b:real^2,a,z}`;
UNDISCH_TAC `~collinear{b:real^2,c,z}`] THEN
REWRITE_TAC[] THEN
ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {b,a,c}`] THEN
MATCH_MP_TAC COLLINEAR_3_TRANS THEN
EXISTS_TAC `v:real^2` THEN
UNDISCH_TAC `v IN segment(b:real^2,z)` THEN
REWRITE_TAC[open_segment; IN_DIFF; IN_INSERT; NOT_IN_EMPTY] THEN
REWRITE_TAC[DE_MORGAN_THM; IMP_CONJ] THENL
[UNDISCH_TAC `v IN segment[a:real^2,b]`;
UNDISCH_TAC `v IN segment[b:real^2,c]`] THEN
ONCE_REWRITE_TAC[IMP_IMP] THEN REWRITE_TAC[GSYM BETWEEN_IN_SEGMENT] THEN
DISCH_THEN(CONJUNCTS_THEN(MP_TAC o MATCH_MP BETWEEN_IMP_COLLINEAR)) THEN
REWRITE_TAC[INSERT_AC] THEN SIMP_TAC[];
ALL_TAC] THEN
SUBGOAL_THEN `segment[b:real^2,z] SUBSET convex hull {a,b,c}`
ASSUME_TAC THENL
[REWRITE_TAC[SEGMENT_CONVEX_HULL] THEN MATCH_MP_TAC HULL_MINIMAL THEN
REWRITE_TAC[CONVEX_CONVEX_HULL; INSERT_SUBSET; EMPTY_SUBSET] THEN
SIMP_TAC[HULL_INC; IN_INSERT] THEN ASM SET_TAC[];
ALL_TAC] THEN
SUBGOAL_THEN `segment(b:real^2,z) SUBSET convex hull {a,b,c}`
ASSUME_TAC THENL
[REWRITE_TAC[open_segment] THEN ASM SET_TAC[]; ALL_TAC] THEN
SUBGOAL_THEN
`segment(b:real^2,z) INTER path_image(polygonal_path(CONS c p)) = {}`
ASSUME_TAC THENL
[REWRITE_TAC[EXTENSION; IN_INTER; NOT_IN_EMPTY] THEN
X_GEN_TAC `v:real^2` THEN STRIP_TAC THEN
SUBGOAL_THEN `m <= n dot (v - b:real^2)` MP_TAC THENL
[FIRST_X_ASSUM MATCH_MP_TAC THEN ASM SET_TAC[]; ALL_TAC] THEN
REWRITE_TAC[REAL_NOT_LE] THEN
UNDISCH_TAC `v IN segment(b:real^2,z)` THEN REWRITE_TAC[IN_SEGMENT] THEN
DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
DISCH_THEN(X_CHOOSE_THEN `t:real` STRIP_ASSUME_TAC) THEN
ASM_REWRITE_TAC[DOT_RMUL; VECTOR_ARITH
`((&1 - t) % a + t % b) - a:real^N = t % (b - a)`] THEN
ONCE_REWRITE_TAC[REAL_ARITH `t * m < m <=> &0 < m * (&1 - t)`] THEN
MATCH_MP_TAC REAL_LT_MUL THEN ASM_REWRITE_TAC[REAL_SUB_LT];
ALL_TAC] THEN
SUBGOAL_THEN `segment(b:real^2,z) SUBSET interior(convex hull {a,b,c})`
ASSUME_TAC THENL
[MATCH_MP_TAC SUBSET_TRANS THEN EXISTS_TAC
`(convex hull {a:real^2,b,c}) DIFF frontier(convex hull {a,b,c})` THEN
CONJ_TAC THENL
[ALL_TAC;
REWRITE_TAC[frontier] THEN MATCH_MP_TAC(SET_RULE
`s SUBSET u ==> s DIFF (u DIFF t) SUBSET t`) THEN
REWRITE_TAC[CLOSURE_SUBSET]] THEN
REWRITE_TAC[FRONTIER_OF_TRIANGLE] THEN MATCH_MP_TAC(SET_RULE
`s INTER a = {} /\ s INTER b = {} /\ s INTER c = {} /\ s SUBSET u
==> s SUBSET u DIFF (a UNION b UNION c)`) THEN
ASM_REWRITE_TAC[] THEN
REWRITE_TAC[EXTENSION; IN_INTER; NOT_IN_EMPTY] THEN
X_GEN_TAC `v:real^2` THEN REWRITE_TAC[IN_SEGMENT] THEN
DISCH_THEN(CONJUNCTS_THEN2
(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) MP_TAC) THEN
DISCH_THEN(X_CHOOSE_THEN `s:real` STRIP_ASSUME_TAC) THEN
ASM_REWRITE_TAC[NOT_EXISTS_THM] THEN X_GEN_TAC `t:real` THEN
REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
DISCH_THEN(MP_TAC o AP_TERM `\x:real^2. n dot (x - b)`) THEN
REWRITE_TAC[VECTOR_ARITH
`((&1 - u) % c + u % a) - b =
(&1 - u) % (c - b) + u % (a - b)`] THEN
ASM_REWRITE_TAC[VECTOR_SUB_REFL; VECTOR_ADD_LID; VECTOR_MUL_RZERO] THEN
ASM_REWRITE_TAC[DOT_RADD; DOT_RMUL] THEN MATCH_MP_TAC(REAL_ARITH
`&0 < m * (&1 - t) /\ m <= x ==> ~((&1 - s) * x + s * x = t * m)`) THEN
ASM_SIMP_TAC[REAL_LT_MUL; REAL_SUB_LT] THEN
FIRST_X_ASSUM MATCH_MP_TAC THEN
SIMP_TAC[IN_INTER; IN_INSERT; HULL_INC] THEN MATCH_MP_TAC
(REWRITE_RULE[SUBSET] VERTICES_IN_PATH_IMAGE_POLYGONAL_PATH) THEN
REWRITE_TAC[set_of_list; IN_INSERT];
ALL_TAC] THEN
SUBGOAL_THEN
`?y:real^2. y IN segment(b,z) /\ y IN interior(convex hull {a',b,c'})`
STRIP_ASSUME_TAC THENL
[REWRITE_TAC[INTER; GSYM(ASSUME
`interior(convex hull {a, b, c}) INTER {x:real^2 | x$2 - b$2 < e} =
interior(convex hull {a', b, c'})`)] THEN
REWRITE_TAC[IN_ELIM_THM] THEN MATCH_MP_TAC(SET_RULE
`(?y. y IN s /\ P y) /\ s SUBSET t
==> ?y. y IN s /\ y IN t /\ P y`) THEN
ASM_REWRITE_TAC[] THEN ASM_REWRITE_TAC[IN_SEGMENT] THEN EXISTS_TAC
`b + min (&1 / &2) (e / &2 / norm(z - b)) % (z - b):real^2` THEN
CONJ_TAC THENL
[EXISTS_TAC `min (&1 / &2) (e / &2 / norm (z - b:real^2))` THEN
REPEAT CONJ_TAC THENL [ALL_TAC; REAL_ARITH_TAC; VECTOR_ARITH_TAC] THEN
REWRITE_TAC[REAL_LT_MIN] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
ASM_SIMP_TAC[REAL_HALF; REAL_LT_DIV; NORM_POS_LT; VECTOR_SUB_EQ];
REWRITE_TAC[VECTOR_ADD_COMPONENT; REAL_ADD_SUB] THEN
MATCH_MP_TAC(REAL_ARITH
`abs(x$2) <= norm x /\ norm x <= e / &2 /\ &0 < e ==> x$2 < e`) THEN
SIMP_TAC[COMPONENT_LE_NORM; DIMINDEX_2; ARITH] THEN
ASM_REWRITE_TAC[NORM_MUL] THEN
ASM_SIMP_TAC[GSYM REAL_LE_RDIV_EQ; NORM_POS_LT; VECTOR_SUB_EQ] THEN
MATCH_MP_TAC(REAL_ARITH `&0 <= x ==> abs(min (&1 / &2) x) <= x`) THEN
MATCH_MP_TAC REAL_LT_IMP_LE THEN MATCH_MP_TAC REAL_LT_DIV THEN
ASM_REWRITE_TAC[REAL_HALF; NORM_POS_LT; VECTOR_SUB_EQ]];
ALL_TAC] THEN
MATCH_MP_TAC CONNECTED_COMPONENT_TRANS THEN EXISTS_TAC `y:real^2` THEN
CONJ_TAC THENL
[REWRITE_TAC[connected_component] THEN
EXISTS_TAC `interior(convex hull {a':real^2,b,c'})` THEN
ASM_REWRITE_TAC[] THEN
SIMP_TAC[CONVEX_CONNECTED; CONVEX_INTERIOR; CONVEX_CONVEX_HULL] THEN
SIMP_TAC[PATH_IMAGE_JOIN; PATHSTART_JOIN; PATHSTART_LINEPATH;
PATHFINISH_LINEPATH; PATHSTART_POLYGONAL_PATH; NOT_CONS_NIL; HD] THEN
REWRITE_TAC[SET_RULE `s SUBSET UNIV DIFF (a UNION b UNION c) <=>
s INTER a = {} /\ s INTER b = {} /\ s INTER c = {}`] THEN
REPEAT CONJ_TAC THENL
[MATCH_MP_TAC(SET_RULE
`!t. s SUBSET t /\ t INTER u = {} ==> s INTER u = {}`) THEN
EXISTS_TAC `interior(convex hull {a:real^2,b,c})` THEN
ASM_SIMP_TAC[SUBSET_INTERIOR] THEN
MP_TAC(ISPECL [`a:real^2`; `b:real^2`; `c:real^2`]
FRONTIER_OF_TRIANGLE) THEN
REWRITE_TAC[PATH_IMAGE_LINEPATH; frontier] THEN
MATCH_MP_TAC(SET_RULE
`!s. i SUBSET s /\ s SUBSET c
==> c DIFF i = a UNION b ==> i INTER a = {}`) THEN
EXISTS_TAC `convex hull {a:real^2,b,c}` THEN
REWRITE_TAC[INTERIOR_SUBSET; CLOSURE_SUBSET];
MATCH_MP_TAC(SET_RULE
`!t. s SUBSET t /\ t INTER u = {} ==> s INTER u = {}`) THEN
EXISTS_TAC `interior(convex hull {a:real^2,b,c})` THEN
ASM_SIMP_TAC[SUBSET_INTERIOR] THEN
MP_TAC(ISPECL [`a:real^2`; `b:real^2`; `c:real^2`]
FRONTIER_OF_TRIANGLE) THEN
REWRITE_TAC[PATH_IMAGE_LINEPATH; frontier] THEN
MATCH_MP_TAC(SET_RULE
`!s. i SUBSET s /\ s SUBSET c
==> c DIFF i = a UNION b UNION d ==> i INTER b = {}`) THEN
EXISTS_TAC `convex hull {a:real^2,b,c}` THEN
REWRITE_TAC[INTERIOR_SUBSET; CLOSURE_SUBSET];
MATCH_MP_TAC(SET_RULE
`!t. s SUBSET t /\ u INTER t = {} ==> s INTER u = {}`) THEN
EXISTS_TAC `{x | (x:real^2)$2 - (b:real^2)$2 < e}` THEN
CONJ_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
REWRITE_TAC[SET_RULE `s INTER t = {} <=> s SUBSET (UNIV DIFF t)`] THEN
REWRITE_TAC[SUBSET; IN_DIFF; IN_ELIM_THM; REAL_NOT_LT; IN_UNIV] THEN
MP_TAC(ISPEC `CONS (c:real^2) p`
PATH_IMAGE_POLYGONAL_PATH_SUBSET_CONVEX_HULL) THEN
REWRITE_TAC[NOT_CONS_NIL] THEN
MATCH_MP_TAC(SET_RULE
`t SUBSET {x | P x} ==> s SUBSET t ==> !x. x IN s ==> P x`) THEN
REWRITE_TAC[REAL_ARITH `e <= x - b <=> x >= b + e`] THEN
SIMP_TAC[SUBSET_HULL; CONVEX_HALFSPACE_COMPONENT_GE] THEN
REWRITE_TAC[set_of_list; REAL_ARITH `x >= b + e <=> e <= x - b`] THEN
ASM_REWRITE_TAC[INSERT_SUBSET; IN_ELIM_THM] THEN
ASM_REWRITE_TAC[SUBSET; IN_SET_OF_LIST; IN_ELIM_THM]];
REWRITE_TAC[connected_component] THEN
EXISTS_TAC `segment(b:real^2,z)` THEN ASM_REWRITE_TAC[] THEN
REWRITE_TAC[CONNECTED_SEGMENT] THEN
SIMP_TAC[PATH_IMAGE_JOIN; PATHSTART_JOIN; PATHSTART_LINEPATH;
PATHFINISH_LINEPATH; PATHSTART_POLYGONAL_PATH; NOT_CONS_NIL; HD] THEN
REWRITE_TAC[PATH_IMAGE_LINEPATH] THEN ASM SET_TAC[]]] THEN
SUBGOAL_THEN
`?u v:real^2.
MEM u (CONS c p) /\ MEM v (CONS c p) /\
mx IN segment[u,v] /\
segment[u,v] SUBSET path_image(polygonal_path(CONS c p)) /\
~(a IN segment[u,v] /\ c IN segment[u,v]) /\
n dot (u - b) <= m`
STRIP_ASSUME_TAC THENL
[MP_TAC(ISPECL [`CONS (c:real^2) p`; `mx:real^2`]
PATH_IMAGE_POLYGONAL_PATH_SUBSET_SEGMENTS) THEN
ANTS_TAC THENL
[ASM_REWRITE_TAC[LENGTH; ARITH_RULE `3 <= SUC n <=> 2 <= n`] THEN
ASM SET_TAC[];
ALL_TAC] THEN
REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
MAP_EVERY X_GEN_TAC [`u:real^2`; `v:real^2`] THEN
ASM_REWRITE_TAC[PATHSTART_POLYGONAL_PATH; PATHFINISH_POLYGONAL_PATH] THEN
ASM_REWRITE_TAC[NOT_CONS_NIL; LAST; HD] THEN STRIP_TAC THEN
SUBGOAL_THEN `n dot (u - b) <= m \/ n dot (v - b:real^2) <= m`
STRIP_ASSUME_TAC THENL
[REWRITE_TAC[GSYM REAL_NOT_LT; GSYM DE_MORGAN_THM] THEN STRIP_TAC THEN
UNDISCH_TAC `n dot (mx - b:real^2) = m` THEN
UNDISCH_TAC `(mx:real^2) IN segment[u,v]` THEN
REWRITE_TAC[IN_SEGMENT] THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
REWRITE_TAC[VECTOR_ARITH
`((&1 - u) % x + u % y) - a:real^N =
(&1 - u) % (x - a) + u % (y - a)`] THEN
MATCH_MP_TAC(REAL_ARITH `--x < --m ==> ~(x = m)`) THEN
REWRITE_TAC[GSYM DOT_LNEG] THEN REWRITE_TAC[DOT_RADD; DOT_RMUL] THEN
MATCH_MP_TAC REAL_CONVEX_BOUND_LT THEN
ASM_REWRITE_TAC[DOT_LNEG; REAL_LT_NEG2] THEN ASM_REAL_ARITH_TAC;
MAP_EVERY EXISTS_TAC [`u:real^2`; `v:real^2`] THEN ASM_REWRITE_TAC[] THEN
ONCE_REWRITE_TAC[CONJ_SYM] THEN ASM_REWRITE_TAC[];
MAP_EVERY EXISTS_TAC [`v:real^2`; `u:real^2`] THEN
ONCE_REWRITE_TAC[SEGMENT_SYM] THEN ASM_REWRITE_TAC[] THEN
ONCE_REWRITE_TAC[CONJ_SYM] THEN ASM_REWRITE_TAC[]];
ALL_TAC] THEN
ASM_CASES_TAC `n dot (u - b:real^2) < n dot (c - b)` THENL
[SUBGOAL_THEN `~(u:real^2 = a) /\ ~(u = c)` STRIP_ASSUME_TAC THENL
[ASM_MESON_TAC[REAL_LT_REFL]; ALL_TAC] THEN
UNDISCH_TAC `MEM (u:real^2) (CONS c p)` THEN
ASM_REWRITE_TAC[MEM] THEN DISCH_TAC THEN EXISTS_TAC `u:real^2` THEN
ASM_REWRITE_TAC[IN_DIFF; IN_INSERT; NOT_IN_EMPTY] THEN
ASM_CASES_TAC `mx:real^2 = u` THENL [ASM SET_TAC[]; ALL_TAC] THEN
MATCH_MP_TAC(TAUT `(a ==> b) /\ a ==> a /\ b`) THEN CONJ_TAC THENL
[DISCH_TAC THEN ASM_REWRITE_TAC[GSYM REAL_LE_ANTISYM] THEN
FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[IN_INTER] THEN
MATCH_MP_TAC(REWRITE_RULE[SUBSET]
VERTICES_IN_PATH_IMAGE_POLYGONAL_PATH) THEN
ASM_REWRITE_TAC[IN_SET_OF_LIST; MEM];
ALL_TAC] THEN
MP_TAC(ISPECL
[`segment(u:real^2,mx)`; `convex hull {a:real^2,b,c}`]
CONNECTED_INTER_FRONTIER) THEN
REWRITE_TAC[CONNECTED_SEGMENT] THEN MATCH_MP_TAC(SET_RULE
`(s SUBSET c ==> u IN c) /\ s INTER f = {} /\ ~(s INTER c = {})
==> (~(s INTER c = {}) /\ ~(s DIFF c = {}) ==> ~(s INTER f = {}))
==> u IN c`) THEN
REPEAT CONJ_TAC THENL
[DISCH_TAC THEN
SUBGOAL_THEN `closure(segment(u:real^2,mx)) SUBSET convex hull {a,b,c}`
MP_TAC THENL
[MATCH_MP_TAC CLOSURE_MINIMAL THEN ASM_REWRITE_TAC[] THEN
MATCH_MP_TAC COMPACT_IMP_CLOSED THEN
MATCH_MP_TAC COMPACT_CONVEX_HULL THEN
SIMP_TAC[FINITE_IMP_COMPACT; FINITE_INSERT; FINITE_EMPTY];
ASM_REWRITE_TAC[SUBSET; CLOSURE_SEGMENT] THEN
DISCH_THEN MATCH_MP_TAC THEN REWRITE_TAC[ENDS_IN_SEGMENT]];
REWRITE_TAC[FRONTIER_OF_TRIANGLE] THEN
MATCH_MP_TAC(SET_RULE
`!a b c t u.
s SUBSET t /\ t SUBSET u /\
a IN ca /\ c IN ca /\
ab INTER u SUBSET {a,b} /\ bc INTER u SUBSET {c} /\
~(b IN u) /\ s INTER ca = {}
==> s INTER (ab UNION bc UNION ca) = {}`) THEN
MAP_EVERY EXISTS_TAC
[`a:real^2`; `b:real^2`; `c:real^2`; `segment[u:real^2,v]`;
`path_image(polygonal_path(CONS (c:real^2) p))`] THEN
ASM_REWRITE_TAC[ENDS_IN_SEGMENT; SUBSET_SEGMENT] THEN CONJ_TAC THENL
[MP_TAC(ISPEC `CONS (c:real^2) p`
PATH_IMAGE_POLYGONAL_PATH_SUBSET_CONVEX_HULL) THEN
REWRITE_TAC[NOT_CONS_NIL] THEN MATCH_MP_TAC(SET_RULE
`~(x IN t) ==> s SUBSET t ==> ~(x IN s)`) THEN
MATCH_MP_TAC(SET_RULE
`!t. ~(b IN t) /\ s SUBSET t ==> ~(b IN s)`) THEN
EXISTS_TAC `{x:real^2 | (x:real^2)$2 >= (b:real^2)$2 + e}` THEN
ASM_REWRITE_TAC[IN_ELIM_THM; real_ge; REAL_NOT_LE; REAL_LT_ADDR] THEN
MATCH_MP_TAC HULL_MINIMAL THEN
REWRITE_TAC[GSYM real_ge; CONVEX_HALFSPACE_COMPONENT_GE] THEN
REWRITE_TAC[SUBSET; set_of_list; FORALL_IN_INSERT; IN_ELIM_THM] THEN
ASM_REWRITE_TAC[IN_SET_OF_LIST; REAL_ARITH
`x >= b + e <=> e <= x - b`];
REWRITE_TAC[EXTENSION; IN_INTER; NOT_IN_EMPTY] THEN
X_GEN_TAC `y:real^2` THEN REWRITE_TAC[IN_SEGMENT] THEN
DISCH_THEN(CONJUNCTS_THEN MP_TAC) THEN
DISCH_THEN(X_CHOOSE_THEN `s:real` STRIP_ASSUME_TAC) THEN
ASM_REWRITE_TAC[NOT_EXISTS_THM] THEN X_GEN_TAC `t:real` THEN
REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
DISCH_THEN(MP_TAC o AP_TERM `\x:real^2. n dot (x - b)`) THEN
REWRITE_TAC[VECTOR_ARITH
`((&1 - u) % c + u % a) - b =
(&1 - u) % (c - b) + u % (a - b)`] THEN
ASM_REWRITE_TAC[DOT_RADD; DOT_RMUL] THEN MATCH_MP_TAC(REAL_ARITH
`(&1 - t) * a < (&1 - t) * m /\ t * b <= t * m
==> ~((&1 - s) * m + s * m = (&1 - t) * a + t * b)`) THEN
ASM_SIMP_TAC[REAL_LT_LMUL; REAL_SUB_LT] THEN
MATCH_MP_TAC REAL_LE_LMUL THEN
CONJ_TAC THENL [ASM_REAL_ARITH_TAC; FIRST_X_ASSUM MATCH_MP_TAC] THEN
SIMP_TAC[IN_INTER; HULL_INC; IN_INSERT] THEN
MATCH_MP_TAC(REWRITE_RULE[SUBSET]
VERTICES_IN_PATH_IMAGE_POLYGONAL_PATH) THEN
REWRITE_TAC[set_of_list; IN_INSERT]];
ALL_TAC] THEN
ASM_CASES_TAC `mx IN interior(convex hull {a:real^2,b,c})` THENL
[UNDISCH_TAC `mx IN interior(convex hull {a:real^2,b,c})` THEN
REWRITE_TAC[IN_INTERIOR_CBALL; SUBSET; IN_CBALL] THEN
DISCH_THEN(X_CHOOSE_THEN `ee:real` STRIP_ASSUME_TAC) THEN
REWRITE_TAC[GSYM MEMBER_NOT_EMPTY; IN_INTER] THEN
ONCE_REWRITE_TAC[SEGMENT_SYM] THEN ASM_REWRITE_TAC[IN_SEGMENT] THEN
REWRITE_TAC[MESON[]
`(?x. (?u. P u /\ Q u /\ x = f u) /\ R x) <=>
(?u. P u /\ Q u /\ R(f u))`] THEN
EXISTS_TAC `min (&1 / &2) (ee / norm(u - mx:real^2))` THEN
REPEAT CONJ_TAC THENL
[MATCH_MP_TAC(REAL_ARITH `&0 < x ==> &0 < min (&1 / &2) x`) THEN
ASM_SIMP_TAC[REAL_LT_DIV; NORM_POS_LT; VECTOR_SUB_EQ];
REAL_ARITH_TAC;
FIRST_X_ASSUM MATCH_MP_TAC THEN REWRITE_TAC[dist; VECTOR_ARITH
`a - ((&1 - u) % a + u % b):real^N = u % (a - b)`] THEN
ASM_SIMP_TAC[NORM_MUL; GSYM REAL_LE_RDIV_EQ; NORM_POS_LT;
VECTOR_SUB_EQ] THEN
REWRITE_TAC[NORM_SUB] THEN MATCH_MP_TAC(REAL_ARITH
`&0 < x ==> abs(min (&1 / &2) x) <= x`) THEN
ASM_SIMP_TAC[REAL_LT_DIV; NORM_POS_LT; VECTOR_SUB_EQ]];
ALL_TAC] THEN
MP_TAC(ISPEC `{a:real^2,b,c}` AFFINE_INDEPENDENT_SPAN_EQ) THEN
ANTS_TAC THENL
[ASM_REWRITE_TAC[] THEN
SIMP_TAC[CARD_CLAUSES; FINITE_INSERT; FINITE_EMPTY] THEN
ASM_REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY; DIMINDEX_2] THEN
CONV_TAC NUM_REDUCE_CONV;
ALL_TAC] THEN
GEN_REWRITE_TAC LAND_CONV [EXTENSION] THEN
REWRITE_TAC[AFFINE_HULL_3; IN_UNIV] THEN
DISCH_THEN(MP_TAC o SPEC `u:real^2`) THEN
REWRITE_TAC[IN_ELIM_THM; LEFT_IMP_EXISTS_THM] THEN
MAP_EVERY X_GEN_TAC [`r:real`; `s:real`; `t:real`] THEN STRIP_TAC THEN
SUBGOAL_THEN `mx IN convex hull {a:real^2,b,c}` MP_TAC THENL
[ASM SET_TAC[]; ALL_TAC] THEN
ONCE_REWRITE_TAC[SEGMENT_SYM] THEN REWRITE_TAC[CONVEX_HULL_3] THEN
REWRITE_TAC[GSYM MEMBER_NOT_EMPTY; IN_ELIM_THM] THEN
ONCE_REWRITE_TAC[INTER_COMM] THEN
REWRITE_TAC[IN_INTER; EXISTS_IN_GSPEC] THEN
REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
MAP_EVERY X_GEN_TAC [`rx:real`; `sx:real`; `tx:real`] THEN
ASM_CASES_TAC `rx = &0` THENL
[ASM_REWRITE_TAC[REAL_LE_REFL; REAL_ADD_LID] THEN
REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_LID] THEN STRIP_TAC THEN
UNDISCH_TAC
`segment[b:real^2,c] INTER path_image(polygonal_path(CONS c p))
SUBSET {c}` THEN
REWRITE_TAC[SUBSET] THEN
DISCH_THEN(MP_TAC o SPEC `mx:real^2`) THEN
MATCH_MP_TAC(TAUT `~q /\ p ==> (p ==> q) ==> r`) THEN
REWRITE_TAC[IN_SING] THEN CONJ_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
REWRITE_TAC[IN_INTER; SEGMENT_CONVEX_HULL] THEN
CONJ_TAC THENL [ALL_TAC; ASM SET_TAC[]] THEN
REWRITE_TAC[CONVEX_HULL_2; IN_ELIM_THM] THEN ASM_MESON_TAC[];
ALL_TAC] THEN
ASM_CASES_TAC `rx = &1` THENL
[ASM_REWRITE_TAC[] THEN
DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
SUBGOAL_THEN `sx = &0 /\ tx = &0` ASSUME_TAC THENL
[ASM_REAL_ARITH_TAC; ASM_REWRITE_TAC[]] THEN
ASM_REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_MUL_LID; VECTOR_ADD_RID];
ALL_TAC] THEN
ASM_CASES_TAC `tx = &0` THENL
[ASM_REWRITE_TAC[REAL_LE_REFL; REAL_ADD_RID] THEN
REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_RID] THEN STRIP_TAC THEN
UNDISCH_TAC
`segment[a:real^2,b] INTER path_image(polygonal_path(CONS c p))
SUBSET {a,b}` THEN
REWRITE_TAC[SUBSET] THEN
DISCH_THEN(MP_TAC o SPEC `mx:real^2`) THEN
MATCH_MP_TAC(TAUT `~q /\ p ==> (p ==> q) ==> r`) THEN CONJ_TAC THENL
[REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY; DE_MORGAN_THM] THEN
CONJ_TAC THENL [ASM_MESON_TAC[]; DISCH_THEN SUBST_ALL_TAC] THEN
UNDISCH_TAC `n dot (b - b:real^2) = m` THEN
REWRITE_TAC[VECTOR_SUB_REFL; DOT_RZERO] THEN
ASM_REAL_ARITH_TAC;
ALL_TAC] THEN
REWRITE_TAC[IN_INTER; SEGMENT_CONVEX_HULL] THEN
CONJ_TAC THENL [ALL_TAC; ASM SET_TAC[]] THEN
REWRITE_TAC[CONVEX_HULL_2; IN_ELIM_THM] THEN ASM_MESON_TAC[];
ALL_TAC] THEN
ASM_CASES_TAC `tx = &1` THENL
[ASM_REWRITE_TAC[] THEN
DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
SUBGOAL_THEN `sx = &0 /\ rx = &0` ASSUME_TAC THENL
[ASM_REAL_ARITH_TAC; ASM_REWRITE_TAC[]] THEN
ASM_REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_MUL_LID; VECTOR_ADD_LID];
ALL_TAC] THEN
ASM_CASES_TAC `sx = &1` THENL
[ASM_REWRITE_TAC[] THEN
DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
SUBGOAL_THEN `rx = &0 /\ tx = &0` ASSUME_TAC THENL
[ASM_REAL_ARITH_TAC; ASM_REWRITE_TAC[]] THEN
ASM_REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_MUL_LID; VECTOR_ADD_LID;
VECTOR_ADD_RID] THEN
DISCH_THEN SUBST_ALL_TAC THEN
UNDISCH_TAC `n dot (b - b:real^2) = m` THEN
REWRITE_TAC[VECTOR_SUB_REFL; DOT_RZERO] THEN
ASM_REAL_ARITH_TAC;
ALL_TAC] THEN
ASM_CASES_TAC `sx = &0` THENL
[ALL_TAC;
STRIP_TAC THEN
UNDISCH_TAC `~(mx IN interior(convex hull {a:real^2, b, c}))` THEN
MATCH_MP_TAC(TAUT `p ==> ~p ==> q`) THEN
ASM_SIMP_TAC[INTERIOR_CONVEX_HULL_3] THEN
REWRITE_TAC[IN_ELIM_THM] THEN
MAP_EVERY EXISTS_TAC [`rx:real`; `sx:real`; `tx:real`] THEN
REWRITE_TAC[] THEN ASM_REAL_ARITH_TAC] THEN
UNDISCH_THEN `sx = &0` SUBST_ALL_TAC THEN
REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_LID; REAL_LE_REFL] THEN
REWRITE_TAC[REAL_ADD_LID] THEN STRIP_TAC THEN
SUBGOAL_THEN
`&0 < rx /\ rx < &1 /\ &0 < tx /\ tx < &1`
STRIP_ASSUME_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC] THEN
ASM_REWRITE_TAC[IN_SEGMENT] THEN
SUBGOAL_THEN
`?q. q * (rx - r) <= rx /\
q * (tx - t) <= tx /\
&0 < q /\ q < &1`
STRIP_ASSUME_TAC THENL
[EXISTS_TAC
`min (&1 / &2)
(min (if rx:real = r then &1 / &2 else rx / abs(rx - r))
(if tx:real = t then &1 / &2 else tx / abs(tx - t)))` THEN
REWRITE_TAC[REAL_LT_MIN; REAL_MIN_LT] THEN
CONV_TAC REAL_RAT_REDUCE_CONV THEN REPEAT CONJ_TAC THENL
[ASM_CASES_TAC `r:real = rx` THENL
[ASM_REWRITE_TAC[REAL_SUB_REFL; REAL_MUL_RZERO]; ALL_TAC] THEN
MATCH_MP_TAC(REAL_ARITH `abs x <= a ==> x <= a`) THEN
REWRITE_TAC[REAL_ABS_MUL] THEN
ASM_SIMP_TAC[GSYM REAL_LE_RDIV_EQ; REAL_ARITH
`~(x = y) ==> &0 < abs(x - y)`] THEN
MATCH_MP_TAC(REAL_ARITH
`&0 <= a /\ &0 <= x /\ &0 <= b ==> abs(min a (min x b)) <= x`) THEN
CONV_TAC REAL_RAT_REDUCE_CONV THEN
COND_CASES_TAC THEN ASM_SIMP_TAC[REAL_LE_DIV; REAL_ABS_POS] THEN
CONV_TAC REAL_RAT_REDUCE_CONV;
ASM_CASES_TAC `t:real = tx` THENL
[ASM_REWRITE_TAC[REAL_SUB_REFL; REAL_MUL_RZERO]; ALL_TAC] THEN
MATCH_MP_TAC(REAL_ARITH `abs x <= a ==> x <= a`) THEN
REWRITE_TAC[REAL_ABS_MUL] THEN
ASM_SIMP_TAC[GSYM REAL_LE_RDIV_EQ; REAL_ARITH
`~(x = y) ==> &0 < abs(x - y)`] THEN
MATCH_MP_TAC(REAL_ARITH
`&0 <= a /\ &0 <= x /\ &0 <= b ==> abs(min a (min b x)) <= x`) THEN
CONV_TAC REAL_RAT_REDUCE_CONV THEN
COND_CASES_TAC THEN ASM_SIMP_TAC[REAL_LE_DIV; REAL_ABS_POS] THEN
CONV_TAC REAL_RAT_REDUCE_CONV;
COND_CASES_TAC THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
MATCH_MP_TAC REAL_LT_DIV THEN ASM_REAL_ARITH_TAC;
COND_CASES_TAC THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
MATCH_MP_TAC REAL_LT_DIV THEN ASM_REAL_ARITH_TAC];
ALL_TAC] THEN
MAP_EVERY EXISTS_TAC
[`(&1 - q) * rx + q * r`;
`q * s:real`;
`(&1 - q) * tx + q * t:real`] THEN
REWRITE_TAC[CONJ_ASSOC] THEN CONJ_TAC THENL
[ALL_TAC;
EXISTS_TAC `q:real` THEN ASM_REWRITE_TAC[] THEN VECTOR_ARITH_TAC] THEN
REWRITE_TAC[REAL_ARITH
`((&1 - q) * rx + q * r) +
q * s +
((&1 - q) * tx + q * t) =
(rx + tx) + q * ((r + s + t) - (rx + tx))`] THEN
ASM_REWRITE_TAC[] THEN CONJ_TAC THENL [ALL_TAC; REAL_ARITH_TAC] THEN
REWRITE_TAC[REAL_ARITH
`&0 <= (&1 - q) * r + q * s <=> q * (r - s) <= r`] THEN
ASM_REWRITE_TAC[] THEN MATCH_MP_TAC REAL_LE_MUL THEN
ASM_SIMP_TAC[REAL_LT_IMP_LE] THEN
UNDISCH_TAC `n dot (u - b:real^2) < n dot (c - b)` THEN
ASM_REWRITE_TAC[VECTOR_ARITH
`(r % a + s % b + t % c) - b =
r % (a - b) + t % (c - b) + ((r + s + t) - &1) % b`] THEN
REWRITE_TAC[REAL_SUB_REFL; VECTOR_MUL_LZERO; VECTOR_ADD_RID] THEN
ASM_REWRITE_TAC[DOT_RADD; DOT_RMUL] THEN
REWRITE_TAC[REAL_ARITH
`r * x + s * x < x <=> &0 < (&1 - r - s) * x`] THEN
ASM_SIMP_TAC[REAL_LT_MUL_EQ] THEN ASM_REAL_ARITH_TAC;
ALL_TAC] THEN
SUBGOAL_THEN `n dot (u - b) = m /\ n dot (c - b) = m` MP_TAC THENL
[MATCH_MP_TAC(REAL_ARITH
`!mx. n dot (u - b) <= m /\
~(n dot (u - b) < n dot (c - b)) /\
n dot (mx - b) = m /\
n dot (mx - b) <= n dot (c - b)
==> n dot (u - b) = m /\ n dot (c - b) = m`) THEN
EXISTS_TAC `mx:real^2` THEN ASM_REWRITE_TAC[] THEN
FIRST_X_ASSUM MATCH_MP_TAC THEN
SIMP_TAC[IN_INTER; HULL_INC; IN_INSERT] THEN
MATCH_MP_TAC(REWRITE_RULE[SUBSET]
VERTICES_IN_PATH_IMAGE_POLYGONAL_PATH) THEN
REWRITE_TAC[set_of_list; IN_INSERT];
ALL_TAC] THEN
DISCH_THEN(CONJUNCTS_THEN
(fun th -> SUBST_ALL_TAC th THEN ASSUME_TAC th)) THEN
MAP_EVERY (C UNDISCH_THEN (K ALL_TAC)) [`m <= m`; `~(m < m)`] THEN
SUBGOAL_THEN
`collinear {a:real^2,mx,c} /\ collinear {a,u,c}`
STRIP_ASSUME_TAC THENL
[SUBGOAL_THEN
`!y:real^2. n dot (y - b) = m ==> collinear {a,y,c}`
(fun th -> CONJ_TAC THEN MATCH_MP_TAC th THEN ASM_REWRITE_TAC[]) THEN
X_GEN_TAC `y:real^2` THEN DISCH_TAC THEN
ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {a,c,b}`] THEN
ONCE_REWRITE_TAC[COLLINEAR_3] THEN
MATCH_MP_TAC ORTHOGONAL_TO_ORTHOGONAL_2D THEN
EXISTS_TAC `n:real^2` THEN ASM_REWRITE_TAC[] THEN
ONCE_REWRITE_TAC[GSYM ORTHOGONAL_RNEG] THEN
ASM_REWRITE_TAC[VECTOR_NEG_SUB] THEN
MAP_EVERY UNDISCH_TAC
[`n dot (y - b:real^2) = m`; `n dot (c - b:real^2) = m`] THEN
REWRITE_TAC[orthogonal; DOT_RSUB] THEN REAL_ARITH_TAC;
ALL_TAC] THEN
ASM_CASES_TAC `mx:real^2 = u` THENL
[UNDISCH_THEN `mx:real^2 = u` SUBST_ALL_TAC THEN
UNDISCH_TAC `MEM (u:real^2) (CONS c p)` THEN
ASM_REWRITE_TAC[MEM] THEN DISCH_TAC THEN EXISTS_TAC `u:real^2` THEN
ASM_REWRITE_TAC[IN_DIFF; IN_INSERT; NOT_IN_EMPTY] THEN
ASM SET_TAC[];
ALL_TAC] THEN
ASM_CASES_TAC `mx:real^2 = v` THENL
[UNDISCH_THEN `mx:real^2 = v` SUBST_ALL_TAC THEN
UNDISCH_TAC `MEM (v:real^2) (CONS c p)` THEN
ASM_REWRITE_TAC[MEM] THEN DISCH_TAC THEN EXISTS_TAC `v:real^2` THEN
ASM_REWRITE_TAC[IN_DIFF; IN_INSERT; NOT_IN_EMPTY] THEN
ASM SET_TAC[];
ALL_TAC] THEN
SUBGOAL_THEN `collinear {a:real^2,c,mx,u}` ASSUME_TAC THENL
[ASM_SIMP_TAC[COLLINEAR_4_3] THEN
ONCE_REWRITE_TAC[SET_RULE `{a,c,b} = {a,b,c}`] THEN ASM_REWRITE_TAC[];
ALL_TAC] THEN
SUBGOAL_THEN `collinear {a:real^2,u,v}` ASSUME_TAC THENL
[MATCH_MP_TAC COLLINEAR_3_TRANS THEN EXISTS_TAC `mx:real^2` THEN
ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
[MATCH_MP_TAC COLLINEAR_SUBSET THEN
EXISTS_TAC `{a:real^2,c,mx,u}` THEN ASM_REWRITE_TAC[] THEN SET_TAC[];
MATCH_MP_TAC BETWEEN_IMP_COLLINEAR THEN
ASM_REWRITE_TAC[BETWEEN_IN_SEGMENT]];
ALL_TAC] THEN
SUBGOAL_THEN `collinear {c:real^2,u,v}` ASSUME_TAC THENL
[MATCH_MP_TAC COLLINEAR_3_TRANS THEN EXISTS_TAC `mx:real^2` THEN
ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
[MATCH_MP_TAC COLLINEAR_SUBSET THEN
EXISTS_TAC `{a:real^2,c,mx,u}` THEN ASM_REWRITE_TAC[] THEN SET_TAC[];
MATCH_MP_TAC BETWEEN_IMP_COLLINEAR THEN
ASM_REWRITE_TAC[BETWEEN_IN_SEGMENT]];
ALL_TAC] THEN
ASM_CASES_TAC `u:real^2 = v` THENL
[UNDISCH_THEN `u:real^2 = v` SUBST_ALL_TAC THEN
ASM_MESON_TAC[SEGMENT_REFL; IN_SING];
ALL_TAC] THEN
SUBGOAL_THEN `collinear {a:real^2,v,c}` ASSUME_TAC THENL
[MATCH_MP_TAC COLLINEAR_3_TRANS THEN EXISTS_TAC `u:real^2` THEN
RULE_ASSUM_TAC(REWRITE_RULE[INSERT_AC]) THEN
ASM_REWRITE_TAC[INSERT_AC];
ALL_TAC] THEN
MP_TAC(ISPECL [`a:real^2`; `c:real^2`; `u:real^2`; `v:real^2`;
`mx:real^2`] between_lemma) THEN
ASM_REWRITE_TAC[] THEN ANTS_TAC THENL
[CONJ_TAC THENL
[W(MP_TAC o PART_MATCH (lhs o rand) COLLINEAR_TRIPLES o snd) THEN
ASM_REWRITE_TAC[FORALL_IN_INSERT; NOT_IN_EMPTY] THEN
DISCH_THEN SUBST1_TAC THEN
ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {a,c,b}`] THEN
ASM_REWRITE_TAC[];
ASM_REWRITE_TAC[open_segment; IN_DIFF; IN_INSERT; NOT_IN_EMPTY] THEN
MP_TAC(ISPECL [`{a:real^2,b,c}`; `{a:real^2,c}`]
AFFINE_INDEPENDENT_CONVEX_AFFINE_HULL) THEN
ASM_REWRITE_TAC[SEGMENT_CONVEX_HULL] THEN
ANTS_TAC THENL [SET_TAC[]; DISCH_THEN SUBST1_TAC] THEN
REWRITE_TAC[IN_INTER] THEN CONJ_TAC THENL [ALL_TAC; ASM SET_TAC[]] THEN
ASM_SIMP_TAC[GSYM COLLINEAR_3_AFFINE_HULL] THEN
MATCH_MP_TAC COLLINEAR_SUBSET THEN
EXISTS_TAC `{a:real^2,c,mx,u}` THEN
ASM_REWRITE_TAC[] THEN SET_TAC[]];
ALL_TAC] THEN
STRIP_TAC THENL
[EXISTS_TAC `u:real^2` THEN
MP_TAC(ASSUME `u IN segment(a:real^2,c)`) THEN
REWRITE_TAC[open_segment; IN_DIFF; IN_INSERT; NOT_IN_EMPTY] THEN
REWRITE_TAC[DE_MORGAN_THM] THEN STRIP_TAC THEN
UNDISCH_TAC `MEM (u:real^2) (CONS c p)` THEN
ASM_REWRITE_TAC[MEM] THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
UNDISCH_TAC `(u:real^2) IN segment[a,c]` THEN
REWRITE_TAC[SEGMENT_CONVEX_HULL] THEN
SPEC_TAC(`u:real^2`,`u:real^2`) THEN REWRITE_TAC[GSYM SUBSET] THEN
MATCH_MP_TAC HULL_MONO THEN SET_TAC[];
EXISTS_TAC `v:real^2` THEN
MP_TAC(ASSUME `v IN segment(a:real^2,c)`) THEN
REWRITE_TAC[open_segment; IN_DIFF; IN_INSERT; NOT_IN_EMPTY] THEN
REWRITE_TAC[DE_MORGAN_THM] THEN STRIP_TAC THEN
UNDISCH_TAC `MEM (v:real^2) (CONS c p)` THEN
ASM_REWRITE_TAC[MEM] THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
CONJ_TAC THENL
[UNDISCH_TAC `(v:real^2) IN segment[a,c]` THEN
REWRITE_TAC[SEGMENT_CONVEX_HULL] THEN
SPEC_TAC(`v:real^2`,`v:real^2`) THEN REWRITE_TAC[GSYM SUBSET] THEN
MATCH_MP_TAC HULL_MONO THEN SET_TAC[];
UNDISCH_TAC `collinear {a:real^2, v, c}` THEN
ONCE_REWRITE_TAC[SET_RULE `{a,v,c} = {a,c,v}`] THEN
ASM_SIMP_TAC[COLLINEAR_3_AFFINE_HULL] THEN
REWRITE_TAC[AFFINE_HULL_2; IN_ELIM_THM] THEN
STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
REWRITE_TAC[VECTOR_ARITH
`(u % a + v % c) - b:real^N =
u % (a - b) + v % (c - b) + ((u + v) - &1) % b`] THEN
ASM_REWRITE_TAC[DOT_RADD; DOT_RMUL; REAL_SUB_REFL] THEN
ASM_REWRITE_TAC[REAL_MUL_LZERO; REAL_ADD_RID; GSYM REAL_ADD_RDISTRIB;
REAL_MUL_LID]];
UNDISCH_TAC `segment[a:real^2,c] SUBSET segment[u,v]` THEN
ASM_REWRITE_TAC[SUBSET_SEGMENT]]);;
(* ------------------------------------------------------------------------- *)
(* Hence the final Pick theorem by induction on number of polygon segments. *)
(* ------------------------------------------------------------------------- *)
let PICK = prove
(`!p:(real^2)list.
(!x.
MEM x p ==>
integral_vector x) /\
simple_path (
polygonal_path p) /\
pathfinish (
polygonal_path p) = pathstart (
polygonal_path p)
==> measure(inside(
path_image(
polygonal_path p))) =
&(
CARD {x | x
IN inside(
path_image(
polygonal_path p)) /\
integral_vector x}) +
&(
CARD {x | x
IN path_image(
polygonal_path p) /\
integral_vector x}) / &2 - &1`,
GEN_TAC THEN WF_INDUCT_TAC `
LENGTH(p:(real^2)list)` THEN DISJ_CASES_TAC
(ARITH_RULE `
LENGTH(p:(real^2)list) <= 4 \/ 5 <=
LENGTH p`) THENL
[UNDISCH_TAC `
LENGTH(p:(real^2)list) <= 4` THEN
POP_ASSUM(K ALL_TAC) THEN SPEC_TAC(`p:(real^2)list`,`p:(real^2)list`) THEN
MATCH_MP_TAC
list_INDUCT THEN
REWRITE_TAC[
polygonal_path;
SIMPLE_PATH_LINEPATH_EQ] THEN
X_GEN_TAC `a:real^2` THEN MATCH_MP_TAC
list_INDUCT THEN
REWRITE_TAC[
polygonal_path;
SIMPLE_PATH_LINEPATH_EQ] THEN
X_GEN_TAC `b:real^2` THEN MATCH_MP_TAC
list_INDUCT THEN CONJ_TAC THENL
[REWRITE_TAC[
polygonal_path;
SIMPLE_PATH_LINEPATH_EQ;
PATHSTART_LINEPATH;
PATHFINISH_LINEPATH] THEN
MESON_TAC[];
ALL_TAC] THEN
X_GEN_TAC `c:real^2` THEN MATCH_MP_TAC
list_INDUCT THEN CONJ_TAC THENL
[REPLICATE_TAC 4 (DISCH_THEN(K ALL_TAC)) THEN
REWRITE_TAC[
polygonal_path] THEN
REWRITE_TAC[
PATHSTART_JOIN;
PATHFINISH_JOIN;
PATHSTART_LINEPATH;
PATHFINISH_LINEPATH] THEN
ASM_CASES_TAC `c:real^2 = a` THEN ASM_REWRITE_TAC[] THEN
ASM_SIMP_TAC[
SIMPLE_PATH_JOIN_LOOP_EQ;
PATHSTART_LINEPATH;
PATHFINISH_LINEPATH] THEN
REWRITE_TAC[
ARC_LINEPATH_EQ] THEN
REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
REWRITE_TAC[
PATH_IMAGE_LINEPATH] THEN
SUBST1_TAC(ISPECL [`b:real^2`; `a:real^2`] (CONJUNCT1
SEGMENT_SYM)) THEN
REWRITE_TAC[
INTER_IDEMPOT] THEN DISCH_THEN(MP_TAC o MATCH_MP
(REWRITE_RULE[
IMP_CONJ_ALT]
FINITE_SUBSET)) THEN
ASM_REWRITE_TAC[
FINITE_SEGMENT;
FINITE_INSERT;
FINITE_EMPTY];
ALL_TAC] THEN
X_GEN_TAC `d:real^2` THEN MATCH_MP_TAC
list_INDUCT THEN CONJ_TAC THENL
[REPLICATE_TAC 5 (DISCH_THEN(K ALL_TAC));
REWRITE_TAC[
LENGTH; ARITH_RULE `~(SUC(SUC(SUC(SUC(SUC n)))) <= 4)`]] THEN
REWRITE_TAC[
polygonal_path;
PATHSTART_JOIN;
PATHFINISH_JOIN] THEN
REWRITE_TAC[GSYM
IN_SET_OF_LIST;
set_of_list] THEN
REWRITE_TAC[
FORALL_IN_INSERT;
NOT_IN_EMPTY] THEN
REWRITE_TAC[
PATHSTART_LINEPATH;
PATHFINISH_LINEPATH] THEN
ASM_CASES_TAC `d:real^2 = a` THEN ASM_REWRITE_TAC[] THEN
FIRST_X_ASSUM SUBST1_TAC THEN
DISCH_THEN(CONJUNCTS_THEN2 STRIP_ASSUME_TAC MP_TAC) THEN
SIMP_TAC[
SIMPLE_PATH_JOIN_LOOP_EQ;
PATH_IMAGE_JOIN;
PATHSTART_LINEPATH;
ARC_JOIN_EQ;
PATHSTART_JOIN;
PATHFINISH_JOIN;
PATHFINISH_LINEPATH] THEN
REWRITE_TAC[
PATH_IMAGE_LINEPATH] THEN REWRITE_TAC[
INSIDE_OF_TRIANGLE] THEN
REWRITE_TAC[GSYM
FRONTIER_OF_TRIANGLE] THEN
SIMP_TAC[
MEASURE_INTERIOR;
NEGLIGIBLE_CONVEX_FRONTIER;
CONVEX_CONVEX_HULL;
FINITE_IMP_BOUNDED_CONVEX_HULL;
FINITE_INSERT;
FINITE_EMPTY] THEN
ASM_SIMP_TAC[
PICK_TRIANGLE] THEN
COND_CASES_TAC THEN ASM_REWRITE_TAC[
ARC_LINEPATH_EQ] THEN
MATCH_MP_TAC(TAUT `~p ==> p ==> q`) THEN REWRITE_TAC[
UNION_OVER_INTER] THEN
REWRITE_TAC[
UNION_SUBSET] THEN STRIP_TAC THEN
SUBGOAL_THEN
`segment[b:real^2,c]
INTER segment [c,a] = segment[b,c] \/
segment[b,c]
INTER segment [c,a] = segment[c,a] \/
segment[a,b]
INTER segment [b,c] = segment[b,c]`
(REPEAT_TCL DISJ_CASES_THEN SUBST_ALL_TAC) THENL
[REWRITE_TAC[SET_RULE `s
INTER t = s <=> s
SUBSET t`;
SET_RULE `s
INTER t = t <=> t
SUBSET s`] THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [
COLLINEAR_BETWEEN_CASES]) THEN
REWRITE_TAC[
SUBSET_SEGMENT;
BETWEEN_IN_SEGMENT;
ENDS_IN_SEGMENT] THEN
REWRITE_TAC[
SEGMENT_SYM;
DISJ_ACI];
UNDISCH_TAC `segment [b,c]
SUBSET {c:real^2}`;
UNDISCH_TAC `segment [c,a]
SUBSET {c:real^2}`;
UNDISCH_TAC `segment [b,c]
SUBSET {a:real^2, b}`] THEN
DISCH_THEN(MP_TAC o MATCH_MP
(REWRITE_RULE[
IMP_CONJ_ALT]
FINITE_SUBSET)) THEN
ASM_REWRITE_TAC[
FINITE_SEGMENT;
FINITE_INSERT;
FINITE_EMPTY];
STRIP_TAC] THEN
MP_TAC(ISPEC `p:(real^2)list`
POLYGON_CHOP_IN_TWO) THEN
ASM_REWRITE_TAC[
LEFT_IMP_EXISTS_THM] THEN
MAP_EVERY X_GEN_TAC [`a:real^2`;`b:real^2`] THEN STRIP_TAC THEN
SUBGOAL_THEN
`?p':(real^2)list.
HD p' = a /\
LENGTH p' =
LENGTH p /\
path_image(
polygonal_path p') =
path_image(
polygonal_path p) /\
set_of_list p' =
set_of_list p /\
simple_path(
polygonal_path p') /\
pathfinish(
polygonal_path p') = pathstart(
polygonal_path p')`
STRIP_ASSUME_TAC THENL
[MATCH_MP_TAC
ROTATE_LIST_TO_FRONT_0 THEN
EXISTS_TAC `p:(real^2)list` THEN ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
[ASM_SIMP_TAC[ARITH_RULE `5 <= p ==> 3 <= p`] THEN
REWRITE_TAC[
PATHSTART_POLYGONAL_PATH;
PATHFINISH_POLYGONAL_PATH] THEN
GEN_TAC THEN COND_CASES_TAC THEN ASM_SIMP_TAC[
LENGTH] THEN
ASM_ARITH_TAC;
ALL_TAC] THEN
MAP_EVERY UNDISCH_TAC
[`pathfinish(
polygonal_path(p:(real^2)list)) =
pathstart(
polygonal_path p)`;
`5 <=
LENGTH(p:(real^2)list)`] THEN
ASM_CASES_TAC `p:(real^2)list = []` THEN
ASM_REWRITE_TAC[
LENGTH; ARITH] THEN
ASM_REWRITE_TAC[
PATHSTART_POLYGONAL_PATH;
PATHFINISH_POLYGONAL_PATH] THEN
DISCH_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
X_GEN_TAC `l:(real^2)list` THEN
REWRITE_TAC[
APPEND_EQ_NIL;
NOT_CONS_NIL] THEN
ASM_CASES_TAC `l:(real^2)list = []` THENL
[ASM_MESON_TAC[
LENGTH_EQ_NIL]; ALL_TAC] THEN
ASM_REWRITE_TAC[] THEN DISCH_THEN(STRIP_ASSUME_TAC o GSYM) THEN
ASM_REWRITE_TAC[] THEN
SUBGOAL_THEN `~(
TL l:(real^2)list = [])` ASSUME_TAC THENL
[DISCH_THEN(MP_TAC o AP_TERM `LENGTH:(real^2)list->num`) THEN
ASM_SIMP_TAC[
LENGTH;
LENGTH_TL] THEN ASM_ARITH_TAC;
ALL_TAC] THEN
ASM_SIMP_TAC[
LAST_APPEND;
LENGTH_APPEND;
LENGTH_TL;
NOT_CONS_NIL] THEN
ASM_REWRITE_TAC[
LAST;
HD_APPEND;
LENGTH] THEN REPEAT CONJ_TAC THENL
[ASM_ARITH_TAC;
MATCH_MP_TAC
PATH_IMAGE_POLYGONAL_PATH_ROTATE THEN
ASM_REWRITE_TAC[] THEN ASM_ARITH_TAC;
MAP_EVERY UNDISCH_TAC
[`
HD(l:(real^2)list) =
LAST l`; `5 <=
LENGTH(p:(real^2)list)`;
`~(l:(real^2)list = [])`] THEN
ASM_REWRITE_TAC[] THEN
SPEC_TAC(`l:(real^2)list`,`l:(real^2)list`) THEN
LIST_INDUCT_TAC THEN REWRITE_TAC[
HD;
TL;
APPEND] THEN
REWRITE_TAC[
SET_OF_LIST_APPEND;
set_of_list] THEN
REPEAT STRIP_TAC THEN MATCH_MP_TAC(SET_RULE
`a
IN s /\ b
IN s ==> s
UNION {a} = b
INSERT s`) THEN
ASM_REWRITE_TAC[
LAST] THEN ONCE_ASM_REWRITE_TAC[] THEN
REWRITE_TAC[
LAST] THEN UNDISCH_TAC `5 <=
LENGTH(CONS (h:real^2) t)` THEN
COND_CASES_TAC THEN ASM_REWRITE_TAC[
LENGTH; ARITH] THEN
REWRITE_TAC[
IN_SET_OF_LIST;
MEM_EXISTS_EL;
LENGTH] THEN
DISCH_TAC THEN CONJ_TAC THENL
[EXISTS_TAC `0` THEN REWRITE_TAC[
EL] THEN ASM_ARITH_TAC;
EXISTS_TAC `
LENGTH(t:(real^2)list) - 1` THEN
ASM_SIMP_TAC[
LAST_EL] THEN ASM_ARITH_TAC];
MP_TAC(ISPEC `l:(real^2)list`
SIMPLE_PATH_POLYGONAL_PATH_ROTATE) THEN
ASM_REWRITE_TAC[] THEN DISCH_THEN MATCH_MP_TAC THEN ASM_ARITH_TAC];
ALL_TAC] THEN
SUBGOAL_THEN `!x:real^2.
MEM x p <=>
MEM x p'`
(fun th -> REWRITE_TAC[th] THEN
RULE_ASSUM_TAC(REWRITE_RULE[th]))
THENL [ASM_REWRITE_TAC[GSYM
IN_SET_OF_LIST]; ALL_TAC] THEN
MAP_EVERY (C UNDISCH_THEN (SUBST_ALL_TAC o SYM))
[`
set_of_list(p':(real^2)list) =
set_of_list p`;
`
path_image(
polygonal_path(p':(real^2)list)) =
path_image (
polygonal_path p)`;
`
LENGTH(p':(real^2)list) =
LENGTH(p:(real^2)list)`] THEN
MAP_EVERY (C UNDISCH_THEN (K ALL_TAC))
[`
simple_path(
polygonal_path(p:(real^2)list))`;
`pathfinish(
polygonal_path(p:(real^2)list)) =
pathstart(
polygonal_path p)`] THEN
POP_ASSUM_LIST(MP_TAC o end_itlist CONJ o rev) THEN
SPEC_TAC(`p':(real^2)list`,`p:(real^2)list`) THEN
GEN_TAC THEN STRIP_TAC THEN
SUBGOAL_THEN
`?q r. 2 <=
LENGTH q /\ 2 <=
LENGTH r /\
LENGTH q +
LENGTH r =
LENGTH p + 1 /\
set_of_list q
UNION set_of_list r =
set_of_list p /\
pathstart(
polygonal_path q) = pathstart(
polygonal_path p) /\
pathfinish(
polygonal_path q) = (b:real^2) /\
pathstart(
polygonal_path r) = b /\
pathfinish(
polygonal_path r) = pathfinish(
polygonal_path p) /\
simple_path(
polygonal_path q ++
polygonal_path r) /\
path_image(
polygonal_path q ++
polygonal_path r) =
path_image(
polygonal_path p)`
STRIP_ASSUME_TAC THENL
[SUBGOAL_THEN
`
simple_path(
polygonal_path p) /\
2 <=
LENGTH p /\
MEM (b:real^2) p /\
~(pathstart(
polygonal_path p) = b) /\
~(pathfinish(
polygonal_path p) = b)`
MP_TAC THENL
[ASM_SIMP_TAC[ARITH_RULE `5 <= p ==> 2 <= p`] THEN
ASM_REWRITE_TAC[
PATHSTART_POLYGONAL_PATH;
CONJ_ASSOC] THEN
COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[
MEM];
POP_ASSUM_LIST(K ALL_TAC)] THEN
WF_INDUCT_TAC `
LENGTH(p:(real^2)list)` THEN POP_ASSUM MP_TAC THEN
SPEC_TAC(`p:(real^2)list`,`p:(real^2)list`) THEN
MATCH_MP_TAC
list_INDUCT THEN REWRITE_TAC[
LENGTH; ARITH] THEN
X_GEN_TAC `a:real^2` THEN
MATCH_MP_TAC
list_INDUCT THEN REWRITE_TAC[
LENGTH; ARITH] THEN
X_GEN_TAC `x:real^2` THEN
MATCH_MP_TAC
list_INDUCT THEN CONJ_TAC THENL
[REWRITE_TAC[
polygonal_path;
PATHSTART_LINEPATH;
PATHFINISH_LINEPATH;
MEM] THEN
MESON_TAC[];
REWRITE_TAC[
LENGTH; ARITH]] THEN
MAP_EVERY X_GEN_TAC [`y:real^2`; `l:(real^2)list`] THEN
REPLICATE_TAC 3 (DISCH_THEN(K ALL_TAC)) THEN DISCH_TAC THEN
REWRITE_TAC[
polygonal_path] THEN
REWRITE_TAC[
PATHSTART_JOIN;
PATHFINISH_JOIN] THEN
REWRITE_TAC[
PATHSTART_LINEPATH;
PATHFINISH_LINEPATH] THEN
ONCE_REWRITE_TAC[
MEM] THEN
ASM_CASES_TAC `a:real^2 = b` THEN ASM_REWRITE_TAC[] THEN
ONCE_REWRITE_TAC[
MEM] THEN
ASM_CASES_TAC `x:real^2 = b` THEN ASM_REWRITE_TAC[] THENL
[FIRST_X_ASSUM(K ALL_TAC o check is_forall o concl) THEN STRIP_TAC THEN
EXISTS_TAC `[a:real^2;b]` THEN
EXISTS_TAC `CONS (b:real^2) (CONS y l)` THEN
ASM_REWRITE_TAC[
polygonal_path;
LENGTH] THEN
REWRITE_TAC[
PATHSTART_POLYGONAL_PATH;
NOT_CONS_NIL;
HD] THEN
REWRITE_TAC[
PATHSTART_LINEPATH;
PATHFINISH_LINEPATH] THEN
REPEAT(CONJ_TAC THENL [ARITH_TAC; ALL_TAC]) THEN
REWRITE_TAC[
set_of_list] THEN SET_TAC[];
ALL_TAC] THEN
STRIP_TAC THEN
FIRST_X_ASSUM(MP_TAC o SPEC `CONS (x:real^2) (CONS y l)`) THEN
REWRITE_TAC[
LENGTH; ARITH_RULE `n < SUC n`] THEN ANTS_TAC THENL
[REWRITE_TAC[ARITH_RULE `2 <= SUC(SUC n)`] THEN
ONCE_REWRITE_TAC[
MEM] THEN ASM_REWRITE_TAC[] THEN
FIRST_ASSUM(MP_TAC o MATCH_MP (REWRITE_RULE[
IMP_CONJ]
SIMPLE_PATH_JOIN_IMP)) THEN
ASM_REWRITE_TAC[
PATHSTART_POLYGONAL_PATH;
NOT_CONS_NIL;
HD] THEN
SIMP_TAC[
PATHFINISH_LINEPATH;
ARC_IMP_SIMPLE_PATH];
ALL_TAC] THEN
REWRITE_TAC[
LEFT_IMP_EXISTS_THM] THEN
MAP_EVERY X_GEN_TAC [`q:(real^2)list`; `r:(real^2)list`] THEN
STRIP_TAC THEN MAP_EVERY EXISTS_TAC
[`CONS (a:real^2) q`; `r:(real^2)list`] THEN
ASM_REWRITE_TAC[
LENGTH;
NOT_CONS_NIL;
HD] THEN
REPLICATE_TAC 2 (CONJ_TAC THENL [ASM_ARITH_TAC; ALL_TAC]) THEN
CONJ_TAC THENL
[ASM_REWRITE_TAC[
set_of_list; SET_RULE
`(a
INSERT s)
UNION t = a
INSERT (s
UNION t)`];
ALL_TAC] THEN
CONJ_TAC THENL
[REWRITE_TAC[
PATHSTART_POLYGONAL_PATH;
NOT_CONS_NIL;
HD];
ALL_TAC] THEN
CONJ_TAC THENL
[UNDISCH_TAC `pathfinish(
polygonal_path q) = (b:real^2)` THEN
REWRITE_TAC[
PATHFINISH_POLYGONAL_PATH;
LAST;
NOT_CONS_NIL] THEN
UNDISCH_TAC `2 <=
LENGTH(q:(real^2)list)` THEN
COND_CASES_TAC THEN ASM_REWRITE_TAC[
LENGTH; ARITH];
ALL_TAC] THEN
SUBGOAL_THEN
`
polygonal_path(CONS (a:real^2) q) =
linepath(a,x) ++
polygonal_path q`
SUBST1_TAC THENL
[MAP_EVERY UNDISCH_TAC
[`pathstart(
polygonal_path q) =
pathstart(
polygonal_path (CONS (x:real^2) (CONS y l)))`;
`2 <=
LENGTH(q:(real^2)list)`] THEN
SPEC_TAC(`q:(real^2)list`,`q:(real^2)list`) THEN
POP_ASSUM_LIST(K ALL_TAC) THEN
MATCH_MP_TAC
list_INDUCT THEN REWRITE_TAC[
LENGTH; ARITH] THEN
GEN_TAC THEN MATCH_MP_TAC
list_INDUCT THEN
REWRITE_TAC[
LENGTH; ARITH;
polygonal_path] THEN
SIMP_TAC[
PATHSTART_POLYGONAL_PATH;
HD;
NOT_CONS_NIL];
ALL_TAC] THEN
SUBGOAL_THEN
`pathstart(
polygonal_path(CONS x (CONS y l))) = (x:real^2)`
(fun th -> SUBST_ALL_TAC th THEN ASSUME_TAC th) THENL
[REWRITE_TAC[
PATHSTART_POLYGONAL_PATH;
NOT_CONS_NIL;
HD]; ALL_TAC] THEN
CONJ_TAC THENL
[W(MP_TAC o PART_MATCH (rand o rand)
SIMPLE_PATH_ASSOC o snd) THEN
ASM_REWRITE_TAC[
PATHSTART_LINEPATH;
PATHFINISH_LINEPATH] THEN
REWRITE_TAC[
PATHSTART_POLYGONAL_PATH;
NOT_CONS_NIL;
HD] THEN
DISCH_THEN(SUBST1_TAC o SYM) THEN
UNDISCH_TAC `
simple_path(linepath(a:real^2,x) ++
polygonal_path (CONS x (CONS y l)))` THEN
ASM_CASES_TAC `pathfinish(
polygonal_path r) = (a:real^2)` THENL
[SUBGOAL_THEN
`pathfinish(
polygonal_path(CONS (x:real^2) (CONS y l))) = a`
ASSUME_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
ASM_SIMP_TAC[
SIMPLE_PATH_JOIN_LOOP_EQ;
PATHFINISH_LINEPATH;
PATHSTART_JOIN;
PATHFINISH_JOIN;
PATHSTART_LINEPATH] THEN
STRIP_TAC THEN MATCH_MP_TAC
SIMPLE_PATH_IMP_ARC THEN
ASM_REWRITE_TAC[
PATHSTART_JOIN;
PATHFINISH_JOIN] THEN
ASM_MESON_TAC[
ARC_LINEPATH_EQ];
SUBGOAL_THEN
`~(pathfinish(
polygonal_path(CONS (x:real^2) (CONS y l))) = a)`
ASSUME_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
ASM_SIMP_TAC[
SIMPLE_PATH_EQ_ARC;
PATHSTART_JOIN;
PATHSTART_LINEPATH;
PATHFINISH_JOIN] THEN
ASM_SIMP_TAC[
ARC_JOIN_EQ;
PATHFINISH_LINEPATH;
PATHSTART_JOIN] THEN
REWRITE_TAC[
ARC_LINEPATH_EQ] THEN STRIP_TAC THEN
SUBGOAL_THEN
`arc(
polygonal_path q ++
polygonal_path r:real^1->real^2)`
MP_TAC THENL
[ALL_TAC;
ASM_SIMP_TAC[
ARC_JOIN_EQ;
PATHFINISH_LINEPATH;
PATHSTART_JOIN]] THEN
MATCH_MP_TAC
SIMPLE_PATH_IMP_ARC THEN
ASM_REWRITE_TAC[
PATHSTART_JOIN;
PATHFINISH_JOIN] THEN
FIRST_X_ASSUM(MP_TAC o MATCH_MP
ARC_DISTINCT_ENDS) THEN
REWRITE_TAC[
PATHSTART_POLYGONAL_PATH;
HD;
NOT_CONS_NIL]];
ASM_SIMP_TAC[
PATH_IMAGE_JOIN;
PATHFINISH_JOIN;
PATHFINISH_LINEPATH] THEN
SIMP_TAC[
PATH_IMAGE_JOIN;
PATHFINISH_LINEPATH;
NOT_CONS_NIL;
HD;
PATHSTART_POLYGONAL_PATH] THEN
UNDISCH_THEN
`
path_image(
polygonal_path q ++
polygonal_path r) =
path_image(
polygonal_path(CONS (x:real^2) (CONS y l)))`
(SUBST1_TAC o SYM) THEN
ASM_SIMP_TAC[
PATH_IMAGE_JOIN;
PATHFINISH_JOIN;
PATHFINISH_LINEPATH] THEN
SET_TAC[]];
ALL_TAC] THEN
SUBGOAL_THEN `pathstart(
polygonal_path p) = (a:real^2)` SUBST_ALL_TAC THENL
[UNDISCH_TAC `5 <=
LENGTH(p:(real^2)list)` THEN
REWRITE_TAC[
PATHSTART_POLYGONAL_PATH] THEN
COND_CASES_TAC THEN ASM_REWRITE_TAC[
LENGTH; ARITH];
ALL_TAC] THEN
UNDISCH_THEN `pathfinish (
polygonal_path p) = (a:real^2)` SUBST_ALL_TAC THEN
UNDISCH_THEN `
path_image(
polygonal_path q ++
polygonal_path r):real^2->bool =
path_image(
polygonal_path p)` (SUBST_ALL_TAC o SYM) THEN
SUBGOAL_THEN
`(!x:real^2.
MEM x q ==>
integral_vector x) /\
(!x:real^2.
MEM x r ==>
integral_vector x)`
STRIP_ASSUME_TAC THENL
[REWRITE_TAC[GSYM
IN_SET_OF_LIST] THEN REPEAT STRIP_TAC THEN
FIRST_X_ASSUM MATCH_MP_TAC THEN
ASM_REWRITE_TAC[GSYM
IN_SET_OF_LIST;
IN_UNION] THEN
UNDISCH_THEN
`(
set_of_list q
UNION set_of_list r):real^2->bool =
set_of_list p`
(SUBST_ALL_TAC o SYM) THEN
ASM_REWRITE_TAC[
IN_UNION];
ALL_TAC] THEN
ABBREV_TAC `n =
LENGTH(p:(real^2)list)` THEN
SUBGOAL_THEN `
integral_vector(a:real^2) /\
integral_vector(b:real^2)`
STRIP_ASSUME_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
MAP_EVERY (C UNDISCH_THEN (K ALL_TAC))
[`!x:real^2.
MEM x p ==>
integral_vector x`;
`
MEM (a:real^2) p`;
`
MEM (b:real^2) p`;
`
HD p = (a:real^2)`;
`(
set_of_list q
UNION set_of_list r):real^2->bool =
set_of_list p`;
`
simple_path(
polygonal_path p :real^1->real^2)`] THEN
SUBGOAL_THEN `3 <=
LENGTH(q:(real^2)list)` ASSUME_TAC THENL
[REPEAT(FIRST_X_ASSUM(K ALL_TAC o check is_forall o concl)) THEN
REPEAT(POP_ASSUM MP_TAC) THEN
SPEC_TAC(`q:(real^2)list`,`q:(real^2)list`) THEN
MATCH_MP_TAC
list_INDUCT THEN REWRITE_TAC[
LENGTH; ARITH] THEN
X_GEN_TAC `a0:real^2` THEN
MATCH_MP_TAC
list_INDUCT THEN REWRITE_TAC[
LENGTH; ARITH] THEN
X_GEN_TAC `a1:real^2` THEN MATCH_MP_TAC
list_INDUCT THEN
REWRITE_TAC[
LENGTH; ARITH; ARITH_RULE `3 <= SUC(SUC(SUC n))`] THEN
REWRITE_TAC[
polygonal_path;
PATHSTART_LINEPATH;
PATHFINISH_LINEPATH] THEN
REPEAT STRIP_TAC THEN
UNDISCH_THEN `a0:real^2 = a` SUBST_ALL_TAC THEN
UNDISCH_THEN `a1:real^2 = b` SUBST_ALL_TAC THEN
UNDISCH_TAC `segment(a:real^2,b)
SUBSET
inside(
path_image(linepath(a,b) ++
polygonal_path r))` THEN
ASM_SIMP_TAC[
PATH_IMAGE_JOIN;
PATH_IMAGE_LINEPATH;
PATHFINISH_LINEPATH] THEN
MATCH_MP_TAC(SET_RULE
`inside(s'
UNION t)
INTER (s'
UNION t) = {} /\ ~(s = {}) /\ s
SUBSET s'
==> ~(s
SUBSET inside(s'
UNION t))`) THEN
REWRITE_TAC[
INSIDE_NO_OVERLAP] THEN
ASM_REWRITE_TAC[
SEGMENT_OPEN_SUBSET_CLOSED;
SEGMENT_EQ_EMPTY];
UNDISCH_THEN `2 <=
LENGTH(q:(real^2)list)` (K ALL_TAC)] THEN
SUBGOAL_THEN `3 <=
LENGTH(r:(real^2)list)` ASSUME_TAC THENL
[REPEAT(FIRST_X_ASSUM(K ALL_TAC o check is_forall o concl)) THEN
REPEAT(POP_ASSUM MP_TAC) THEN
SPEC_TAC(`r:(real^2)list`,`r:(real^2)list`) THEN
MATCH_MP_TAC
list_INDUCT THEN REWRITE_TAC[
LENGTH; ARITH] THEN
X_GEN_TAC `a0:real^2` THEN
MATCH_MP_TAC
list_INDUCT THEN REWRITE_TAC[
LENGTH; ARITH] THEN
X_GEN_TAC `a1:real^2` THEN MATCH_MP_TAC
list_INDUCT THEN
REWRITE_TAC[
LENGTH; ARITH; ARITH_RULE `3 <= SUC(SUC(SUC n))`] THEN
REWRITE_TAC[
polygonal_path;
PATHSTART_LINEPATH;
PATHFINISH_LINEPATH] THEN
REPEAT STRIP_TAC THEN
UNDISCH_THEN `a0:real^2 = b` SUBST_ALL_TAC THEN
UNDISCH_THEN `a1:real^2 = a` SUBST_ALL_TAC THEN
UNDISCH_TAC `segment(a:real^2,b)
SUBSET
inside(
path_image(
polygonal_path q ++ linepath(b,a)))` THEN
ASM_SIMP_TAC[
PATH_IMAGE_JOIN;
PATH_IMAGE_LINEPATH;
PATHSTART_LINEPATH] THEN
ONCE_REWRITE_TAC[CONJUNCT1
SEGMENT_SYM] THEN
MATCH_MP_TAC(SET_RULE
`inside(t
UNION s')
INTER (t
UNION s') = {} /\ ~(s = {}) /\ s
SUBSET s'
==> ~(s
SUBSET inside(t
UNION s'))`) THEN
REWRITE_TAC[
INSIDE_NO_OVERLAP] THEN
ASM_REWRITE_TAC[
SEGMENT_OPEN_SUBSET_CLOSED;
SEGMENT_EQ_EMPTY];
UNDISCH_THEN `2 <=
LENGTH(r:(real^2)list)` (K ALL_TAC)] THEN
FIRST_X_ASSUM(fun th ->
MP_TAC(ISPEC `CONS (a:real^2) r` th) THEN
MP_TAC(ISPEC `CONS (b:real^2) q` th)) THEN
REWRITE_TAC[
LENGTH] THEN ANTS_TAC THENL [ASM_ARITH_TAC; ALL_TAC] THEN
SUBGOAL_THEN
`
polygonal_path(CONS (b:real^2) q) = linepath(b,a) ++
polygonal_path q`
SUBST_ALL_TAC THENL
[POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN
SPEC_TAC(`q:(real^2)list`,`q:(real^2)list`) THEN
MATCH_MP_TAC
list_INDUCT THEN REWRITE_TAC[
LENGTH; ARITH] THEN
GEN_TAC THEN MATCH_MP_TAC
list_INDUCT THEN
REWRITE_TAC[
LENGTH; ARITH;
polygonal_path] THEN
SIMP_TAC[
PATHSTART_POLYGONAL_PATH;
HD;
NOT_CONS_NIL];
ALL_TAC] THEN
ANTS_TAC THENL
[ASM_REWRITE_TAC[
MEM;
PATHSTART_JOIN;
PATHFINISH_JOIN] THEN
CONJ_TAC THENL [ASM_MESON_TAC[]; REWRITE_TAC[
PATHSTART_LINEPATH]] THEN
UNDISCH_TAC
`
simple_path(
polygonal_path q ++
polygonal_path r :real^1->real^2)` THEN
ASM_SIMP_TAC[
SIMPLE_PATH_JOIN_LOOP_EQ;
PATHSTART_LINEPATH;
PATHFINISH_LINEPATH;
ARC_LINEPATH_EQ] THEN
STRIP_TAC THEN REWRITE_TAC[
PATH_IMAGE_LINEPATH] THEN
ONCE_REWRITE_TAC[
SEGMENT_SYM] THEN
REWRITE_TAC[
SEGMENT_CLOSED_OPEN] THEN
FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (SET_RULE
`s
SUBSET i
==> c
INTER i = {}
==> (s
UNION {a,b})
INTER c
SUBSET {b,a}`)) THEN
ASM_SIMP_TAC[
PATH_IMAGE_JOIN] THEN
MATCH_MP_TAC(SET_RULE
`inside(s
UNION t)
INTER (s
UNION t) = {}
==> s
INTER inside(s
UNION t) = {}`) THEN
REWRITE_TAC[
INSIDE_NO_OVERLAP];
STRIP_TAC] THEN
REWRITE_TAC[
LENGTH] THEN ANTS_TAC THENL [ASM_ARITH_TAC; ALL_TAC] THEN
SUBGOAL_THEN
`
polygonal_path(CONS (a:real^2) r) = linepath(a,b) ++
polygonal_path r`
SUBST_ALL_TAC THENL
[POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN
SPEC_TAC(`r:(real^2)list`,`r:(real^2)list`) THEN
MATCH_MP_TAC
list_INDUCT THEN REWRITE_TAC[
LENGTH; ARITH] THEN
GEN_TAC THEN MATCH_MP_TAC
list_INDUCT THEN
REWRITE_TAC[
LENGTH; ARITH;
polygonal_path] THEN
SIMP_TAC[
PATHSTART_POLYGONAL_PATH;
HD;
NOT_CONS_NIL];
ALL_TAC] THEN
ANTS_TAC THENL
[ASM_REWRITE_TAC[
MEM;
PATHSTART_JOIN;
PATHFINISH_JOIN] THEN
CONJ_TAC THENL [ASM_MESON_TAC[]; REWRITE_TAC[
PATHSTART_LINEPATH]] THEN
UNDISCH_TAC
`
simple_path(
polygonal_path q ++
polygonal_path r :real^1->real^2)` THEN
ASM_SIMP_TAC[
SIMPLE_PATH_JOIN_LOOP_EQ;
PATHSTART_LINEPATH;
PATHFINISH_LINEPATH;
ARC_LINEPATH_EQ] THEN
STRIP_TAC THEN REWRITE_TAC[
PATH_IMAGE_LINEPATH] THEN
REWRITE_TAC[
SEGMENT_CLOSED_OPEN] THEN
FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (SET_RULE
`s
SUBSET i
==> c
INTER i = {}
==> (s
UNION {a,b})
INTER c
SUBSET {a,b}`)) THEN
ASM_SIMP_TAC[
PATH_IMAGE_JOIN] THEN
MATCH_MP_TAC(SET_RULE
`inside(s
UNION t)
INTER (s
UNION t) = {}
==> t
INTER inside(s
UNION t) = {}`) THEN
REWRITE_TAC[
INSIDE_NO_OVERLAP];
STRIP_TAC] THEN
MP_TAC(ISPECL [`
polygonal_path q:real^1->real^2`;
`reversepath(
polygonal_path r):real^1->real^2`;
`linepath(a:real^2,b)`; `a:real^2`; `b:real^2`]
SPLIT_INSIDE_SIMPLE_CLOSED_CURVE) THEN
REWRITE_TAC[] THEN ANTS_TAC THENL
[ASM_REWRITE_TAC[
PATHSTART_LINEPATH;
PATHFINISH_LINEPATH;
PATHSTART_REVERSEPATH;
PATHFINISH_REVERSEPATH;
SIMPLE_PATH_LINEPATH_EQ] THEN
UNDISCH_TAC
`
simple_path(
polygonal_path q ++
polygonal_path r :real^1->real^2)` THEN
ASM_SIMP_TAC[
SIMPLE_PATH_JOIN_LOOP_EQ;
PATH_IMAGE_LINEPATH] THEN
ASM_SIMP_TAC[
PATH_IMAGE_REVERSEPATH;
ARC_IMP_SIMPLE_PATH;
SIMPLE_PATH_REVERSEPATH] THEN
STRIP_TAC THEN REPEAT CONJ_TAC THENL
[MATCH_MP_TAC(SET_RULE
`s
INTER t
SUBSET {a,b} /\
a
IN s /\ b
IN s /\ a
IN t /\ b
IN t
==> s
INTER t = {a,b}`) THEN
ASM_MESON_TAC[
PATHSTART_IN_PATH_IMAGE;
PATHFINISH_IN_PATH_IMAGE];
REWRITE_TAC[
SEGMENT_CLOSED_OPEN] THEN
UNDISCH_TAC
`segment(a:real^2,b)
SUBSET
inside(
path_image(
polygonal_path q ++
polygonal_path r))` THEN
ASM_SIMP_TAC[
PATH_IMAGE_JOIN] THEN MATCH_MP_TAC(SET_RULE
`a
IN t /\ b
IN t /\ inside(t
UNION u)
INTER (t
UNION u) = {}
==> s
SUBSET inside(t
UNION u)
==> t
INTER (s
UNION {a,b}) = {a,b}`) THEN
REWRITE_TAC[
INSIDE_NO_OVERLAP] THEN
ASM_MESON_TAC[
PATHSTART_IN_PATH_IMAGE;
PATHFINISH_IN_PATH_IMAGE];
REWRITE_TAC[
SEGMENT_CLOSED_OPEN] THEN
UNDISCH_TAC
`segment(a:real^2,b)
SUBSET
inside(
path_image(
polygonal_path q ++
polygonal_path r))` THEN
ASM_SIMP_TAC[
PATH_IMAGE_JOIN] THEN MATCH_MP_TAC(SET_RULE
`a
IN u /\ b
IN u /\ inside(t
UNION u)
INTER (t
UNION u) = {}
==> s
SUBSET inside(t
UNION u)
==> u
INTER (s
UNION {a,b}) = {a,b}`) THEN
REWRITE_TAC[
INSIDE_NO_OVERLAP] THEN
ASM_MESON_TAC[
PATHSTART_IN_PATH_IMAGE;
PATHFINISH_IN_PATH_IMAGE];
REWRITE_TAC[
SEGMENT_CLOSED_OPEN] THEN
FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (SET_RULE
`s
SUBSET i
==> inside(q
UNION r)
INTER (q
UNION r) = {} /\
inside(q
UNION r) = i /\
~(s = {})
==> ~((s
UNION {a,b})
INTER inside(q
UNION r) = {})`)) THEN
ASM_REWRITE_TAC[
INSIDE_NO_OVERLAP;
SEGMENT_EQ_EMPTY] THEN
ASM_SIMP_TAC[
PATH_IMAGE_JOIN]];
ALL_TAC] THEN
REPEAT(FIRST_X_ASSUM(MP_TAC o
check (free_in `measure:(real^2->bool)->real` o concl))) THEN
UNDISCH_TAC
`segment(a:real^2,b)
SUBSET
inside(
path_image (
polygonal_path q ++
polygonal_path r))` THEN
ASM_SIMP_TAC[
PATH_IMAGE_JOIN;
PATHSTART_LINEPATH;
PATHFINISH_LINEPATH] THEN
REWRITE_TAC[
PATH_IMAGE_REVERSEPATH;
PATH_IMAGE_LINEPATH] THEN
SUBST1_TAC(ISPECL [`b:real^2`; `a:real^2`] (CONJUNCT1
SEGMENT_SYM)) THEN
REPEAT STRIP_TAC THEN SUBST1_TAC(SYM(ASSUME
`inside(
path_image(
polygonal_path q)
UNION segment [a,b])
UNION
inside(
path_image(
polygonal_path r)
UNION segment [a,b])
UNION
(segment [a:real^2,b]
DIFF {a, b}) =
inside
(
path_image(
polygonal_path q)
UNION path_image(
polygonal_path r))`)) THEN
REWRITE_TAC[SET_RULE
`{x | x
IN (s
UNION t) /\ P x} =
{x | x
IN s /\ P x}
UNION {x | x
IN t /\ P x}`] THEN
MATCH_MP_TAC
EQ_TRANS THEN
EXISTS_TAC
`measure(inside(
path_image(
polygonal_path q)
UNION segment[a:real^2,b])) +
measure(inside(
path_image (
polygonal_path r)
UNION segment [a,b])
UNION
segment [a,b]
DIFF {a, b})` THEN
CONJ_TAC THENL
[MATCH_MP_TAC
MEASURE_NEGLIGIBLE_UNION THEN REPEAT CONJ_TAC THENL
[MATCH_MP_TAC
MEASURABLE_INSIDE THEN
MATCH_MP_TAC
COMPACT_UNION THEN
SIMP_TAC[
COMPACT_PATH_IMAGE;
COMPACT_SEGMENT;
PATH_POLYGONAL_PATH];
MATCH_MP_TAC
MEASURABLE_UNION THEN CONJ_TAC THENL
[MATCH_MP_TAC
MEASURABLE_INSIDE THEN
MATCH_MP_TAC
COMPACT_UNION THEN
SIMP_TAC[
COMPACT_PATH_IMAGE;
COMPACT_SEGMENT;
PATH_POLYGONAL_PATH];
MATCH_MP_TAC
MEASURABLE_DIFF THEN CONJ_TAC THEN
MATCH_MP_TAC
MEASURABLE_COMPACT THEN REWRITE_TAC[
COMPACT_SEGMENT] THEN
MATCH_MP_TAC
FINITE_IMP_COMPACT THEN
REWRITE_TAC[
FINITE_INSERT;
FINITE_EMPTY]];
ASM_REWRITE_TAC[
UNION_OVER_INTER;
UNION_EMPTY] THEN
MATCH_MP_TAC
NEGLIGIBLE_SUBSET THEN EXISTS_TAC `segment[a:real^2,b]` THEN
REWRITE_TAC[
NEGLIGIBLE_SEGMENT_2] THEN SET_TAC[]];
ALL_TAC] THEN
MATCH_MP_TAC
EQ_TRANS THEN
EXISTS_TAC
`measure(inside(
path_image(
polygonal_path q)
UNION segment[a:real^2,b])) +
measure(inside(
path_image(
polygonal_path r)
UNION segment[a,b]))` THEN
CONJ_TAC THENL
[AP_TERM_TAC THEN MATCH_MP_TAC
MEASURE_NEGLIGIBLE_SYMDIFF THEN
MATCH_MP_TAC
NEGLIGIBLE_SUBSET THEN
EXISTS_TAC `segment[a:real^2,b]` THEN
REWRITE_TAC[
NEGLIGIBLE_SEGMENT_2] THEN SET_TAC[];
ALL_TAC] THEN
REWRITE_TAC[GSYM REAL_OF_NUM_ADD] THEN
ONCE_REWRITE_TAC[SET_RULE `s
UNION segment[a,b] = segment[a,b]
UNION s`] THEN
ASM_REWRITE_TAC[] THEN
SUBGOAL_THEN
`
CARD({x | x
IN inside(segment[a,b]
UNION path_image(
polygonal_path q)) /\
integral_vector x}
UNION
{x | x
IN inside(segment[a,b]
UNION path_image(
polygonal_path r)) /\
integral_vector x}
UNION
{x | x
IN segment[a,b]
DIFF {a, b} /\
integral_vector x}) =
CARD {x | x
IN inside(segment[a,b]
UNION path_image(
polygonal_path q)) /\
integral_vector x} +
CARD {x | x
IN inside(segment[a,b]
UNION path_image(
polygonal_path r)) /\
integral_vector x} +
CARD {x:real^2 | x
IN segment[a,b]
DIFF {a, b} /\
integral_vector x}`
SUBST1_TAC THENL
[(CONV_TAC o GEN_SIMPLIFY_CONV TOP_DEPTH_SQCONV (basic_ss []) 5)
[
CARD_UNION_GEN;
FINITE_BOUNDED_INTEGER_POINTS;
FINITE_UNION;
BOUNDED_INSIDE;
BOUNDED_UNION;
BOUNDED_SEGMENT;
BOUNDED_PATH_IMAGE;
BOUNDED_DIFF;
PATH_POLYGONAL_PATH] THEN
MATCH_MP_TAC(ARITH_RULE
`pr = 0 /\ qrp = 0 ==> (q + (r + p) - pr) - qrp = q + r + p`) THEN
REWRITE_TAC[
UNION_OVER_INTER] THEN
REWRITE_TAC[SET_RULE
`{x | x
IN s /\ P x}
INTER {x | x
IN t /\ P x} =
{x | x
IN (s
INTER t) /\ P x}`] THEN
RULE_ASSUM_TAC(ONCE_REWRITE_RULE
[SET_RULE `s
UNION segment[a,b] = segment[a,b]
UNION s`]) THEN
ASM_REWRITE_TAC[
NOT_IN_EMPTY;
EMPTY_GSPEC;
UNION_EMPTY] THEN CONJ_TAC THEN
MATCH_MP_TAC(MESON[
CARD_CLAUSES] `s = {} ==>
CARD s = 0`) THEN
MATCH_MP_TAC(SET_RULE
`inside(s
UNION t)
INTER (s
UNION t) = {}
==> {x | x
IN inside(s
UNION t)
INTER (s
DIFF ab) /\ P x} = {}`) THEN
REWRITE_TAC[
INSIDE_NO_OVERLAP];
ALL_TAC] THEN
REWRITE_TAC[GSYM REAL_OF_NUM_ADD] THEN MATCH_MP_TAC(REAL_ARITH
`q + r = &2 * x + y + &2
==> (iq + q / &2 - &1) + (ir + r / &2 - &1) =
((iq + ir + x) + y / &2 - &1)`) THEN
REWRITE_TAC[SET_RULE
`{x | x
IN (s
UNION t) /\ P x} =
{x | x
IN s /\ P x}
UNION {x | x
IN t /\ P x}`] THEN
(CONV_TAC o GEN_SIMPLIFY_CONV TOP_DEPTH_SQCONV (basic_ss []) 5)
[
CARD_UNION_GEN;
FINITE_BOUNDED_INTEGER_POINTS;
BOUNDED_SEGMENT;
BOUNDED_PATH_IMAGE;
PATH_POLYGONAL_PATH; GSYM
REAL_OF_NUM_SUB;
INTER_SUBSET;
CARD_SUBSET; ARITH_RULE `x:num <= y ==> x <= y + z`] THEN
REWRITE_TAC[GSYM REAL_OF_NUM_ADD] THEN MATCH_MP_TAC(REAL_ARITH
`&2 * ab + qr = &2 * x + qab + rab + &2
==> ((ab + q) - qab) + ((ab + r) - rab) =
&2 * x + ((q + r) - qr) + &2`) THEN
SUBGOAL_THEN
`{x | x
IN segment[a,b] /\
integral_vector x}
INTER
{x | x
IN path_image(
polygonal_path q) /\
integral_vector x} = {a,b} /\
{x:real^2 | x
IN segment[a,b] /\
integral_vector x}
INTER
{x | x
IN path_image(
polygonal_path r) /\
integral_vector x} = {a,b}`
(CONJUNCTS_THEN SUBST1_TAC)
THENL
[FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (SET_RULE
`s
SUBSET inside(q
UNION r)
==> s = c
DIFF {a,b} /\ a
IN q /\ b
IN q /\ a
IN r /\ b
IN r /\
inside(q
UNION r)
INTER (q
UNION r) = {} /\
P a /\ P b /\ a
IN c /\ b
IN c
==> {x | x
IN c /\ P x}
INTER {x | x
IN q /\ P x} = {a,b} /\
{x | x
IN c /\ P x}
INTER {x | x
IN r /\ P x} = {a,b}`)) THEN
ASM_REWRITE_TAC[
open_segment;
INSIDE_NO_OVERLAP;
ENDS_IN_SEGMENT] THEN
ASM_MESON_TAC[
PATHSTART_IN_PATH_IMAGE;
PATHFINISH_IN_PATH_IMAGE];
ALL_TAC] THEN
SUBGOAL_THEN
`{x:real^2 | x
IN path_image(
polygonal_path q) /\
integral_vector x}
INTER
{x | x
IN path_image(
polygonal_path r) /\
integral_vector x} = {a,b}`
SUBST1_TAC THENL
[FIRST_X_ASSUM(MP_TAC o MATCH_MP (REWRITE_RULE[
IMP_CONJ]
SIMPLE_PATH_JOIN_IMP)) THEN
ASM_REWRITE_TAC[] THEN DISCH_THEN(MP_TAC o last o CONJUNCTS) THEN
MATCH_MP_TAC(SET_RULE
`P a /\ P b /\ a
IN q /\ b
IN q /\ a
IN r /\ b
IN r
==> (q
INTER r)
SUBSET {a,b}
==> {x | x
IN q /\ P x}
INTER {x | x
IN r /\ P x} = {a,b}`) THEN
ASM_MESON_TAC[
PATHSTART_IN_PATH_IMAGE;
PATHFINISH_IN_PATH_IMAGE];
ALL_TAC] THEN
SIMP_TAC[
CARD_CLAUSES;
FINITE_INSERT;
FINITE_EMPTY] THEN
ASM_REWRITE_TAC[
IN_INSERT;
NOT_IN_EMPTY] THEN CONV_TAC NUM_REDUCE_CONV THEN
MATCH_MP_TAC(REAL_ARITH
`x = y + &2 ==> &2 * x + &2 = &2 * y + &2 + &2 + &2`) THEN
REWRITE_TAC[
SEGMENT_CLOSED_OPEN] THEN
SUBGOAL_THEN `(segment(a,b)
UNION {a, b})
DIFF {a, b} = segment(a:real^2,b)`
SUBST1_TAC THENL
[MATCH_MP_TAC(SET_RULE
`~(a
IN s) /\ ~(b
IN s) ==> (s
UNION {a,b})
DIFF {a,b} = s`) THEN
REWRITE_TAC[
open_segment;
IN_DIFF] THEN SET_TAC[];
ALL_TAC] THEN
ASM_SIMP_TAC[SET_RULE
`P a /\ P b
==> {x | x
IN s
UNION {a,b} /\ P x} =
a
INSERT b
INSERT {x | x
IN s /\ P x}`] THEN
SIMP_TAC[
CARD_CLAUSES;
FINITE_BOUNDED_INTEGER_POINTS;
BOUNDED_SEGMENT;
FINITE_INSERT] THEN
ASM_REWRITE_TAC[
IN_INSERT;
IN_ELIM_THM;
ENDS_NOT_IN_SEGMENT] THEN
REWRITE_TAC[REAL_OF_NUM_ADD; ARITH_RULE `SUC(SUC n) = n + 2`]);;