1 (* ========================================================================= *)
3 (* ========================================================================= *)
5 needs "Multivariate/polytope.ml";;
6 needs "Multivariate/measure.ml";;
7 needs "Multivariate/moretop.ml";;
11 (* ------------------------------------------------------------------------- *)
13 (* ------------------------------------------------------------------------- *)
15 let COLLINEAR_IMP_NEGLIGIBLE = prove
16 (`!s:real^2->bool. collinear s ==> negligible s`,
17 REWRITE_TAC[COLLINEAR_AFFINE_HULL] THEN
18 MESON_TAC[NEGLIGIBLE_AFFINE_HULL_2; NEGLIGIBLE_SUBSET]);;
20 let CONVEX_HULL_3_0 = prove
22 convex hull {vec 0,a,b} =
23 {x % a + y % b | &0 <= x /\ &0 <= y /\ x + y <= &1}`,
24 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[SET_RULE `{c,a,b} = {a,b,c}`] THEN
25 REWRITE_TAC[CONVEX_HULL_3; EXTENSION; IN_ELIM_THM] THEN
26 X_GEN_TAC `y:real^N` THEN
27 AP_TERM_TAC THEN REWRITE_TAC[FUN_EQ_THM] THEN X_GEN_TAC `x:real` THEN
28 AP_TERM_TAC THEN REWRITE_TAC[FUN_EQ_THM] THEN X_GEN_TAC `y:real` THEN
29 REWRITE_TAC[VECTOR_MUL_RZERO; VECTOR_ADD_RID] THEN
30 EQ_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THENL
31 [ASM_ARITH_TAC; EXISTS_TAC `&1 - x - y` THEN ASM_ARITH_TAC]);;
33 let INTERIOR_CONVEX_HULL_3_0 = prove
35 ~(collinear {vec 0,a,b})
36 ==> interior(convex hull {vec 0,a,b}) =
37 {x % a + y % b | &0 < x /\ &0 < y /\ x + y < &1}`,
38 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[SET_RULE `{c,a,b} = {a,b,c}`] THEN
39 STRIP_TAC THEN ASM_SIMP_TAC[INTERIOR_CONVEX_HULL_3] THEN
40 REWRITE_TAC[TAUT `a /\ x = &1 /\ b <=> x = &1 /\ a /\ b`] THEN
41 REWRITE_TAC[VECTOR_MUL_RZERO; VECTOR_ADD_RID] THEN
42 REWRITE_TAC[REAL_ARITH `x + y + z = &1 <=> &1 - x - y = z`; UNWIND_THM1] THEN
43 REWRITE_TAC[EXTENSION; IN_ELIM_THM] THEN
44 GEN_TAC THEN REPEAT(AP_TERM_TAC THEN ABS_TAC) THEN
45 EQ_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
48 let MEASURE_CONVEX_HULL_2_TRIVIAL = prove
49 (`(!a:real^2. measure(convex hull {a}) = &0) /\
50 (!a b:real^2. measure(convex hull {a,b}) = &0)`,
52 MATCH_MP_TAC MEASURE_EQ_0 THEN
53 MATCH_MP_TAC COLLINEAR_IMP_NEGLIGIBLE THEN
54 REWRITE_TAC[GSYM SEGMENT_CONVEX_HULL; CONVEX_HULL_SING] THEN
55 REWRITE_TAC[COLLINEAR_SING; COLLINEAR_SEGMENT]);;
57 let NEGLIGIBLE_SEGMENT_2 = prove
58 (`!a b:real^2. negligible(segment[a,b])`,
59 SIMP_TAC[COLLINEAR_IMP_NEGLIGIBLE; COLLINEAR_SEGMENT]);;
61 (* ------------------------------------------------------------------------- *)
62 (* Decomposing an additive function on a triangle. *)
63 (* ------------------------------------------------------------------------- *)
65 let TRIANGLE_DECOMPOSITION = prove
67 d IN convex hull {a,b,c}
68 ==> (convex hull {a,b,c} =
69 convex hull {d,b,c} UNION
70 convex hull {d,a,c} UNION
71 convex hull {d,a,b})`,
73 MATCH_MP_TAC SUBSET_ANTISYM THEN REWRITE_TAC[UNION_SUBSET] THEN
75 [REWRITE_TAC[SUBSET] THEN X_GEN_TAC `x:real^2` THEN DISCH_TAC THEN
76 MP_TAC(ISPECL [`{a:real^2,b,c}`; `d:real^2`; `x:real^2`]
77 IN_CONVEX_HULL_EXCHANGE) THEN
78 ASM_REWRITE_TAC[EXISTS_IN_INSERT; NOT_IN_EMPTY; IN_UNION] THEN
79 REPEAT(MATCH_MP_TAC MONO_OR THEN CONJ_TAC) THEN
80 SPEC_TAC(`x:real^2`,`x:real^2`) THEN REWRITE_TAC[GSYM SUBSET] THEN
81 MATCH_MP_TAC HULL_MONO THEN SET_TAC[];
82 SIMP_TAC[SUBSET_HULL; CONVEX_CONVEX_HULL] THEN
83 REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET] THEN
84 ASM_SIMP_TAC[HULL_INC; IN_INSERT]]);;
86 let TRIANGLE_ADDITIVE_DECOMPOSITION = prove
87 (`!f:(real^2->bool)->real a b c d.
88 (!s t. compact s /\ compact t
89 ==> f(s UNION t) = f(s) + f(t) - f(s INTER t)) /\
90 ~(a = b) /\ ~(a = c) /\ ~(b = c) /\
91 ~affine_dependent {a,b,c} /\ d IN convex hull {a,b,c}
92 ==> f(convex hull {a,b,c}) =
93 (f(convex hull {a,b,d}) +
94 f(convex hull {a,c,d}) +
95 f(convex hull {b,c,d})) -
96 (f(convex hull {a,d}) +
97 f(convex hull {b,d}) +
98 f(convex hull {c,d})) +
100 REPEAT STRIP_TAC THEN
101 FIRST_ASSUM(SUBST1_TAC o MATCH_MP TRIANGLE_DECOMPOSITION) THEN
102 ASM (CONV_TAC o GEN_SIMPLIFY_CONV TOP_DEPTH_SQCONV (basic_ss []) 5)
103 [COMPACT_UNION; COMPACT_INTER; COMPACT_CONVEX_HULL;
104 FINITE_IMP_COMPACT; FINITE_INSERT; FINITE_EMPTY;
105 UNION_OVER_INTER] THEN
106 MP_TAC(ISPECL [`{a:real^2,b,c}`; `d:real^2`]
107 CONVEX_HULL_EXCHANGE_INTER) THEN
108 ASM_REWRITE_TAC[] THEN
109 SIMP_TAC[INSERT_SUBSET; EMPTY_SUBSET; IN_INSERT; NOT_IN_EMPTY;
110 SET_RULE `s SUBSET u /\ t SUBSET u ==> (s INTER t) SUBSET u`] THEN
111 ASM_REWRITE_TAC[INSERT_INTER; IN_INSERT; NOT_IN_EMPTY; INTER_EMPTY] THEN
112 DISCH_TAC THEN REWRITE_TAC[INSERT_AC] THEN REAL_ARITH_TAC);;
114 (* ------------------------------------------------------------------------- *)
115 (* Vectors all of whose coordinates are integers. *)
116 (* ------------------------------------------------------------------------- *)
118 let integral_vector = define
119 `integral_vector(x:real^N) <=>
120 !i. 1 <= i /\ i <= dimindex(:N) ==> integer(x$i)`;;
122 let INTEGRAL_VECTOR_VEC = prove
123 (`!n. integral_vector(vec n)`,
124 REWRITE_TAC[integral_vector; VEC_COMPONENT; INTEGER_CLOSED]);;
126 let INTEGRAL_VECTOR_STDBASIS = prove
127 (`!i. integral_vector(basis i:real^N)`,
128 REWRITE_TAC[integral_vector] THEN
129 REPEAT STRIP_TAC THEN ASM_SIMP_TAC[BASIS_COMPONENT] THEN
130 COND_CASES_TAC THEN REWRITE_TAC[INTEGER_CLOSED]);;
132 let INTEGRAL_VECTOR_ADD = prove
134 integral_vector x /\ integral_vector y ==> integral_vector(x + y)`,
135 SIMP_TAC[integral_vector; VECTOR_ADD_COMPONENT; INTEGER_CLOSED]);;
137 let INTEGRAL_VECTOR_SUB = prove
139 integral_vector x /\ integral_vector y ==> integral_vector(x - y)`,
140 SIMP_TAC[integral_vector; VECTOR_SUB_COMPONENT; INTEGER_CLOSED]);;
142 let INTEGRAL_VECTOR_ADD_LCANCEL = prove
144 integral_vector x ==> (integral_vector(x + y) <=> integral_vector y)`,
145 MESON_TAC[INTEGRAL_VECTOR_ADD; INTEGRAL_VECTOR_SUB;
146 VECTOR_ARITH `(x + y) - x:real^N = y`]);;
148 let FINITE_BOUNDED_INTEGER_POINTS = prove
149 (`!s:real^N->bool. bounded s ==> FINITE {x | x IN s /\ integral_vector x}`,
150 REPEAT STRIP_TAC THEN
151 FIRST_ASSUM(MP_TAC o MATCH_MP BOUNDED_SUBSET_CLOSED_INTERVAL) THEN
152 REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
153 MAP_EVERY X_GEN_TAC [`a:real^N`; `b:real^N`] THEN
154 REWRITE_TAC[SUBSET; IN_INTERVAL; integral_vector] THEN DISCH_TAC THEN
155 MATCH_MP_TAC FINITE_SUBSET THEN
156 EXISTS_TAC `{x:real^N | !i. 1 <= i /\ i <= dimindex(:N)
158 (a:real^N)$i <= x$i /\ x$i <= (b:real^N)$i}` THEN
160 [MATCH_MP_TAC FINITE_CART THEN REWRITE_TAC[FINITE_INTSEG];
163 let FINITE_TRIANGLE_INTEGER_POINTS = prove
164 (`!a b c:real^N. FINITE {x | x IN convex hull {a,b,c} /\ integral_vector x}`,
165 REPEAT GEN_TAC THEN MATCH_MP_TAC FINITE_BOUNDED_INTEGER_POINTS THEN
166 SIMP_TAC[FINITE_IMP_BOUNDED_CONVEX_HULL; FINITE_INSERT; FINITE_EMPTY]);;
168 (* ------------------------------------------------------------------------- *)
169 (* Properties of a basis for the integer lattice. *)
170 (* ------------------------------------------------------------------------- *)
172 let LINEAR_INTEGRAL_VECTOR = prove
175 ==> ((!x. integral_vector x ==> integral_vector(f x)) <=>
176 (!i j. 1 <= i /\ i <= dimindex(:N) /\
177 1 <= j /\ j <= dimindex(:N)
178 ==> integer(matrix f$i$j)))`,
179 REPEAT STRIP_TAC THEN
180 FIRST_ASSUM(fun th -> ONCE_REWRITE_TAC[GSYM(MATCH_MP MATRIX_WORKS th)]) THEN
181 ABBREV_TAC `M = matrix(f:real^N->real^N)` THEN
182 SIMP_TAC[integral_vector; matrix_vector_mul; LAMBDA_BETA] THEN
183 EQ_TAC THEN REPEAT GEN_TAC THEN DISCH_TAC THENL
184 [MAP_EVERY X_GEN_TAC [`i:num`; `j:num`] THEN STRIP_TAC THEN
185 FIRST_X_ASSUM(MP_TAC o SPEC `basis j:real^N`) THEN
186 REWRITE_TAC[GSYM integral_vector; INTEGRAL_VECTOR_STDBASIS] THEN
187 DISCH_THEN(MP_TAC o SPEC `i:num`) THEN ASM_REWRITE_TAC[] THEN
188 ASM_SIMP_TAC[BASIS_COMPONENT; COND_RAND; COND_RATOR] THEN
189 ASM_REWRITE_TAC[REAL_MUL_RZERO; SUM_DELTA; IN_NUMSEG; REAL_MUL_RID];
190 X_GEN_TAC `x:real^N` THEN DISCH_TAC THEN
191 X_GEN_TAC `i:num` THEN STRIP_TAC THEN
192 MATCH_MP_TAC INTEGER_SUM THEN
193 ASM_SIMP_TAC[INTEGER_CLOSED; IN_NUMSEG]]);;
195 let INTEGRAL_BASIS_UNIMODULAR = prove
197 linear f /\ IMAGE f integral_vector = integral_vector
198 ==> abs(det(matrix f)) = &1`,
199 REWRITE_TAC[GSYM SUBSET_ANTISYM_EQ; SUBSET; FORALL_IN_IMAGE] THEN
200 REWRITE_TAC[IN_IMAGE] THEN REWRITE_TAC[IN] THEN REPEAT STRIP_TAC THEN
202 `!i j. 1 <= i /\ i <= dimindex(:N) /\
203 1 <= j /\ j <= dimindex(:N)
204 ==> integer(matrix(f:real^N->real^N)$i$j)`
205 ASSUME_TAC THENL [ASM_SIMP_TAC[GSYM LINEAR_INTEGRAL_VECTOR]; ALL_TAC] THEN
207 `?g:real^N->real^N. linear g /\ (!x. g(f x) = x) /\ (!y. f(g y) = y)`
208 STRIP_ASSUME_TAC THENL
209 [MATCH_MP_TAC LINEAR_BIJECTIVE_LEFT_RIGHT_INVERSE THEN ASM_SIMP_TAC[] THEN
210 MATCH_MP_TAC(TAUT `(b ==> a) /\ b ==> a /\ b`) THEN CONJ_TAC THENL
211 [ASM_MESON_TAC[LINEAR_SURJECTIVE_IMP_INJECTIVE]; ALL_TAC] THEN
212 SUBGOAL_THEN `!y. y:real^N IN span(IMAGE f (:real^N))` MP_TAC THENL
213 [ALL_TAC; ASM_SIMP_TAC[SPAN_LINEAR_IMAGE; SPAN_UNIV] THEN SET_TAC[]] THEN
214 GEN_TAC THEN GEN_REWRITE_TAC LAND_CONV [GSYM BASIS_EXPANSION] THEN
215 MATCH_MP_TAC SPAN_VSUM THEN REWRITE_TAC[FINITE_NUMSEG; IN_NUMSEG] THEN
216 X_GEN_TAC `k:num` THEN STRIP_TAC THEN MATCH_MP_TAC SPAN_MUL THEN
217 MATCH_MP_TAC SPAN_SUPERSET THEN REWRITE_TAC[IN_IMAGE; IN_UNIV] THEN
218 ASM_MESON_TAC[INTEGRAL_VECTOR_STDBASIS];
221 `!i j. 1 <= i /\ i <= dimindex(:N) /\
222 1 <= j /\ j <= dimindex(:N)
223 ==> integer(matrix(g:real^N->real^N)$i$j)`
225 [ASM_SIMP_TAC[GSYM LINEAR_INTEGRAL_VECTOR] THEN ASM_MESON_TAC[];
228 `det(matrix(f:real^N->real^N)) * det(matrix(g:real^N->real^N)) =
229 det(matrix(I:real^N->real^N))`
231 [ASM_SIMP_TAC[GSYM DET_MUL; GSYM MATRIX_COMPOSE] THEN
232 REPEAT AP_TERM_TAC THEN ASM_REWRITE_TAC[FUN_EQ_THM; o_THM; I_THM];
234 DISCH_THEN(MP_TAC o AP_TERM `abs:real->real`) THEN
235 REWRITE_TAC[MATRIX_I; DET_I; REAL_ABS_NUM] THEN
236 ASM_SIMP_TAC[INTEGER_DET; INTEGER_ABS_MUL_EQ_1]);;
238 (* ------------------------------------------------------------------------- *)
239 (* Pick's theorem for an elementary triangle. *)
240 (* ------------------------------------------------------------------------- *)
242 let PICK_ELEMENTARY_TRIANGLE_0 = prove
244 {x | x IN convex hull {vec 0,a,b} /\ integral_vector x} = {vec 0,a,b}
245 ==> measure(convex hull {vec 0,a,b}) =
246 if collinear {vec 0,a,b} then &0 else &1 / &2`,
247 REPEAT GEN_TAC THEN COND_CASES_TAC THEN
248 ASM_SIMP_TAC[MEASURE_EQ_0; COLLINEAR_IMP_NEGLIGIBLE;
249 COLLINEAR_CONVEX_HULL_COLLINEAR] THEN
250 POP_ASSUM MP_TAC THEN
252 ASM_CASES_TAC t THENL [ASM_REWRITE_TAC[INSERT_AC; COLLINEAR_2]; ALL_TAC])
253 [`a:real^2 = vec 0`; `b:real^2 = vec 0`; `a:real^2 = b`] THEN
254 DISCH_TAC THEN SUBGOAL_THEN `independent {a:real^2,b}` ASSUME_TAC THENL
255 [UNDISCH_TAC `~collinear{vec 0:real^2, a, b}` THEN
256 REWRITE_TAC[independent; CONTRAPOS_THM] THEN
257 REWRITE_TAC[dependent; EXISTS_IN_INSERT; NOT_IN_EMPTY] THEN STRIP_TAC THENL
258 [ONCE_REWRITE_TAC[SET_RULE `{c,a,b} = {c,b,a}`]; ALL_TAC] THEN
259 ASM_SIMP_TAC[COLLINEAR_3_AFFINE_HULL] THEN
260 ASM_SIMP_TAC[AFFINE_HULL_EQ_SPAN; HULL_INC; IN_INSERT] THEN
261 FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP
262 (SET_RULE `a IN s ==> s SUBSET t ==> a IN t`)) THEN
263 MATCH_MP_TAC SPAN_MONO THEN SET_TAC[];
265 SUBGOAL_THEN `span{a,b} = (:real^2)` ASSUME_TAC THENL
266 [MP_TAC(ISPECL [`(:real^2)`; `{a:real^2,b}`] CARD_EQ_DIM) THEN
267 ASM_REWRITE_TAC[SUBSET_UNIV; SUBSET; EXTENSION; IN_ELIM_THM; IN_UNIV] THEN
268 DISCH_THEN MATCH_MP_TAC THEN
269 REWRITE_TAC[HAS_SIZE; FINITE_INSERT; FINITE_EMPTY] THEN
270 SIMP_TAC[CARD_CLAUSES; FINITE_INSERT; FINITE_EMPTY; IN_INSERT] THEN
271 ASM_REWRITE_TAC[NOT_IN_EMPTY; DIM_UNIV; DIMINDEX_2; ARITH];
273 REWRITE_TAC[GSYM SUBSET_ANTISYM_EQ; SUBSET; FORALL_IN_INSERT;
274 FORALL_IN_GSPEC] THEN
275 REWRITE_TAC[IN_ELIM_THM; NOT_IN_EMPTY; IN_INSERT] THEN STRIP_TAC THEN
276 MP_TAC(ISPEC `\x:real^2. transp(vector[a;b]:real^2^2) ** x`
277 INTEGRAL_BASIS_UNIMODULAR) THEN
278 REWRITE_TAC[MATRIX_OF_MATRIX_VECTOR_MUL; MATRIX_VECTOR_MUL_LINEAR] THEN
279 REWRITE_TAC[DET_2; MEASURE_TRIANGLE; VECTOR_2; DET_TRANSP; VEC_COMPONENT] THEN
280 ANTS_TAC THENL [ALL_TAC; REAL_ARITH_TAC] THEN
281 MATCH_MP_TAC SUBSET_ANTISYM THEN REWRITE_TAC[SUBSET; FORALL_IN_IMAGE] THEN
283 [REWRITE_TAC[IN] THEN
284 SIMP_TAC[LINEAR_INTEGRAL_VECTOR; MATRIX_VECTOR_MUL_LINEAR; LAMBDA_BETA;
285 MATRIX_OF_MATRIX_VECTOR_MUL; transp; DIMINDEX_2; ARITH] THEN
286 MAP_EVERY UNDISCH_TAC
287 [`integral_vector(a:real^2)`; `integral_vector(b:real^2)`] THEN
288 REWRITE_TAC[integral_vector; IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN
289 REWRITE_TAC[IMP_IMP; FORALL_2; DIMINDEX_2; VECTOR_2] THEN
290 REWRITE_TAC[CONJ_ACI];
292 REWRITE_TAC[IN_IMAGE] THEN REWRITE_TAC[IN] THEN
293 X_GEN_TAC `x:real^2` THEN DISCH_TAC THEN REWRITE_TAC[EXISTS_VECTOR_2] THEN
294 REWRITE_TAC[MATRIX_VECTOR_COLUMN; TRANSP_TRANSP] THEN
295 REWRITE_TAC[DIMINDEX_2; VSUM_2; VECTOR_2; integral_vector; FORALL_2] THEN
296 SUBGOAL_THEN `(x:real^2) IN span{a,b}` MP_TAC THENL
297 [ASM_REWRITE_TAC[IN_UNIV]; ALL_TAC] THEN
298 REWRITE_TAC[SPAN_2; IN_UNIV; IN_ELIM_THM] THEN
299 MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `u:real` THEN
300 MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `v:real` THEN
301 DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
302 FIRST_ASSUM(MP_TAC o SPEC `frac u % a + frac v % b:real^2`) THEN
303 FIRST_X_ASSUM(MP_TAC o SPEC
304 `(&1 - frac u) % a + (&1 - frac v) % b:real^2`) THEN
306 `b' /\ (b' ==> b) /\ (a \/ a') /\ (c \/ c' ==> x)
307 ==> (a /\ b ==> c) ==> (a' /\ b' ==> c') ==> x`) THEN
308 REPEAT CONJ_TAC THENL
309 [SUBGOAL_THEN `integral_vector(floor u % a + floor v % b:real^2)`
311 [MAP_EVERY UNDISCH_TAC
312 [`integral_vector(a:real^2)`; `integral_vector(b:real^2)`] THEN
313 SIMP_TAC[integral_vector; DIMINDEX_2; FORALL_2;
314 VECTOR_ADD_COMPONENT; VECTOR_MUL_COMPONENT] THEN
315 SIMP_TAC[FLOOR; INTEGER_CLOSED];
316 UNDISCH_TAC `integral_vector(x:real^2)` THEN REWRITE_TAC[IMP_IMP] THEN
317 DISCH_THEN(MP_TAC o MATCH_MP INTEGRAL_VECTOR_SUB) THEN
318 ASM_REWRITE_TAC[VECTOR_ARITH
319 `(x % a + y % b) - (u % a + v % b) = (x - u) % a + (y - v) % b`] THEN
320 MATCH_MP_TAC EQ_IMP THEN AP_TERM_TAC THEN BINOP_TAC THEN
321 AP_THM_TAC THEN AP_TERM_TAC THEN
322 REWRITE_TAC[REAL_ARITH `u - x:real = y <=> u = x + y`] THEN
323 REWRITE_TAC[GSYM FLOOR_FRAC]];
324 REWRITE_TAC[VECTOR_ARITH
325 `(&1 - u) % a + (&1 - v) % b = (a + b) - (u % a + v % b)`] THEN
326 ASM_SIMP_TAC[INTEGRAL_VECTOR_ADD; INTEGRAL_VECTOR_SUB];
327 REWRITE_TAC[CONVEX_HULL_3_0; IN_ELIM_THM] THEN
329 `&0 <= frac u /\ &0 <= frac v /\ frac u + frac v <= &1 \/
330 &0 <= &1 - frac u /\ &0 <= &1 - frac v /\
331 (&1 - frac u) + (&1 - frac v) <= &1`
333 [MP_TAC(SPEC `u:real` FLOOR_FRAC) THEN
334 MP_TAC(SPEC `v:real` FLOOR_FRAC) THEN REAL_ARITH_TAC;
337 [VECTOR_ARITH `x % a + y % b = a <=> (x - &1) % a + y % b = vec 0`;
338 VECTOR_ARITH `x % a + y % b = b <=> x % a + (y - &1) % b = vec 0`] THEN
339 ASM_SIMP_TAC[INDEPENDENT_2; GSYM REAL_FRAC_EQ_0] THEN
340 MP_TAC(SPEC `u:real` FLOOR_FRAC) THEN
341 MP_TAC(SPEC `v:real` FLOOR_FRAC) THEN REAL_ARITH_TAC]);;
343 let PICK_ELEMENTARY_TRIANGLE = prove
345 {x | x IN convex hull {a,b,c} /\ integral_vector x} = {a,b,c}
346 ==> measure(convex hull {a,b,c}) =
347 if collinear {a,b,c} then &0 else &1 / &2`,
348 REPEAT GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP (SET_RULE
349 `s = t ==> (!x. x IN s <=> x IN t) /\ s = t`)) THEN
350 REWRITE_TAC[IMP_CONJ] THEN DISCH_THEN(MP_TAC o SPEC `a:real^2`) THEN
351 REWRITE_TAC[IN_INSERT; IN_ELIM_THM] THEN
352 GEOM_ORIGIN_TAC `a:real^2`THEN
353 SIMP_TAC[INTEGRAL_VECTOR_ADD_LCANCEL; VECTOR_ADD_RID] THEN
354 REWRITE_TAC[PICK_ELEMENTARY_TRIANGLE_0]);;
356 (* ------------------------------------------------------------------------- *)
357 (* Our form of Pick's theorem holds degenerately for a flat triangle. *)
358 (* ------------------------------------------------------------------------- *)
360 let PICK_TRIANGLE_FLAT = prove
362 integral_vector a /\ integral_vector b /\ integral_vector c /\
364 ==> measure(convex hull {a,b,c}) =
365 &(CARD {x | x IN convex hull {a,b,c} /\ integral_vector x}) -
366 (&(CARD {x | x IN convex hull {b,c} /\ integral_vector x}) +
367 &(CARD {x | x IN convex hull {a,c} /\ integral_vector x}) +
368 &(CARD {x | x IN convex hull {a,b} /\ integral_vector x})) / &2 +
370 REPEAT STRIP_TAC THEN REWRITE_TAC[GSYM SEGMENT_CONVEX_HULL] THEN
371 SUBGOAL_THEN `convex hull {a:real^2,b,c} = segment[a,b]` SUBST1_TAC THENL
372 [REWRITE_TAC[SEGMENT_CONVEX_HULL] THEN MATCH_MP_TAC CONVEX_HULLS_EQ THEN
373 ASM_REWRITE_TAC[GSYM SEGMENT_CONVEX_HULL; INSERT_SUBSET; EMPTY_SUBSET] THEN
374 SIMP_TAC[ENDS_IN_SEGMENT; HULL_INC; IN_INSERT];
376 SUBGOAL_THEN `measure(segment[a:real^2,b]) = &0` SUBST1_TAC THENL
377 [MATCH_MP_TAC MEASURE_EQ_0 THEN
378 MATCH_MP_TAC COLLINEAR_IMP_NEGLIGIBLE THEN
379 REWRITE_TAC[COLLINEAR_SEGMENT];
381 REWRITE_TAC[REAL_ARITH
382 `&0 = c - (a + b + c) / &2 + &1 / &2 <=> a + b = c + &1`] THEN
383 REWRITE_TAC[REAL_OF_NUM_ADD; REAL_OF_NUM_EQ] THEN
385 `segment[a:real^2,b] = segment[b,c] UNION segment[a,c]`
386 SUBST1_TAC THENL [ASM_MESON_TAC[SEGMENT_SYM; UNION_SEGMENT]; ALL_TAC] THEN
388 `{x | x IN (s UNION t) /\ P x} =
389 {x | x IN s /\ P x} UNION {x | x IN t /\ P x}`] THEN
390 SIMP_TAC[CARD_UNION_GEN; FINITE_BOUNDED_INTEGER_POINTS; BOUNDED_SEGMENT] THEN
391 MATCH_MP_TAC(ARITH_RULE
392 `z:num <= x /\ z = 1 ==> x + y = (x + y) - z + 1`) THEN
394 [MATCH_MP_TAC CARD_SUBSET THEN
395 SIMP_TAC[FINITE_BOUNDED_INTEGER_POINTS; BOUNDED_SEGMENT] THEN SET_TAC[];
396 REWRITE_TAC[SET_RULE `{x | x IN s /\ P x} INTER {x | x IN t /\ P x} =
397 {x | x IN (s INTER t) /\ P x}`] THEN
399 `segment[b:real^2,c] INTER segment[a,c] = {c}`
400 SUBST1_TAC THENL [ASM_MESON_TAC[INTER_SEGMENT; SEGMENT_SYM]; ALL_TAC] THEN
401 SUBGOAL_THEN `{x:real^2 | x IN {c} /\ integral_vector x} = {c}`
402 SUBST1_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
403 SIMP_TAC[CARD_CLAUSES; FINITE_EMPTY; ARITH; NOT_IN_EMPTY]]);;
405 (* ------------------------------------------------------------------------- *)
406 (* Pick's theorem for a triangle. *)
407 (* ------------------------------------------------------------------------- *)
409 let PICK_TRIANGLE_ALT = prove
411 integral_vector a /\ integral_vector b /\ integral_vector c
412 ==> measure(convex hull {a,b,c}) =
413 &(CARD {x | x IN convex hull {a,b,c} /\ integral_vector x}) -
414 (&(CARD {x | x IN convex hull {b,c} /\ integral_vector x}) +
415 &(CARD {x | x IN convex hull {a,c} /\ integral_vector x}) +
416 &(CARD {x | x IN convex hull {a,b} /\ integral_vector x})) / &2 +
419 MATCH_MP_TAC CARD_PSUBSET THEN
420 REWRITE_TAC[FINITE_TRIANGLE_INTEGER_POINTS] THEN
421 REWRITE_TAC[PSUBSET] THEN CONJ_TAC THENL
422 [MATCH_MP_TAC(SET_RULE
423 `s SUBSET t ==> {x | x IN s /\ P x} SUBSET {x | x IN t /\ P x}`) THEN
424 MATCH_MP_TAC HULL_MINIMAL THEN REWRITE_TAC[CONVEX_CONVEX_HULL] THEN
425 ASM_SIMP_TAC[INSERT_SUBSET; EMPTY_SUBSET; IN_INSERT; HULL_INC];
427 SUBGOAL_THEN(subst[bc,`bc:real^2->bool`]
428 `convex hull {a:real^2,b,c} = convex hull bc`)
430 [MATCH_MP_TAC CONVEX_HULLS_EQ THEN
431 ASM_SIMP_TAC[HULL_INC; IN_INSERT; INSERT_SUBSET; EMPTY_SUBSET] THEN
432 SUBGOAL_THEN(subst [a,`x:real^2`] `x IN convex hull {a:real^2,b,c}`)
434 [SIMP_TAC[HULL_INC; IN_INSERT]; ASM SET_TAC[]];
436 MP_TAC(ISPECL [`{a:real^2,b,c}`; a]
437 EXTREME_POINT_OF_CONVEX_HULL_AFFINE_INDEPENDENT) THEN
438 ASM_REWRITE_TAC[IN_INSERT] THEN
439 DISCH_THEN(MP_TAC o MATCH_MP EXTREME_POINT_OF_CONVEX_HULL) THEN
440 ASM_REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY] in
442 WF_INDUCT_TAC `CARD {x:real^2 | x IN convex hull {a,b,c} /\
443 integral_vector x}` THEN
444 ASM_CASES_TAC `collinear{a:real^2,b,c}` THENL
445 [FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [COLLINEAR_BETWEEN_CASES]) THEN
446 REWRITE_TAC[BETWEEN_IN_SEGMENT] THEN REPEAT STRIP_TAC THENL
447 [MP_TAC(ISPECL [`b:real^2`; `c:real^2`; `a:real^2`] PICK_TRIANGLE_FLAT);
448 MP_TAC(ISPECL [`a:real^2`; `c:real^2`; `b:real^2`] PICK_TRIANGLE_FLAT);
449 MP_TAC(ISPECL [`a:real^2`; `b:real^2`; `c:real^2`]
450 PICK_TRIANGLE_FLAT)] THEN
451 (ANTS_TAC THENL [ASM_MESON_TAC[SEGMENT_SYM]; ALL_TAC] THEN
452 REWRITE_TAC[SET_RULE `{x | x IN s /\ P x} = s INTER P`] THEN
453 REWRITE_TAC[INSERT_AC; REAL_ADD_AC]);
455 UNDISCH_TAC `~collinear{a:real^2,b,c}` THEN
457 (fun t -> ASM_CASES_TAC t THENL
458 [ASM_REWRITE_TAC[INSERT_AC; COLLINEAR_2]; ALL_TAC])
459 [`a:real^2 = b`; `a:real^2 = c`; `b:real^2 = c`] THEN
460 DISCH_TAC THEN STRIP_TAC THEN
462 `{x:real^2 | x IN convex hull {a, b, c} /\ integral_vector x} =
465 [ASM_SIMP_TAC[PICK_ELEMENTARY_TRIANGLE] THEN
467 `{x | x IN convex hull {b,c} /\ integral_vector x} = {b,c} /\
468 {x | x IN convex hull {a,c} /\ integral_vector x} = {a,c} /\
469 {x | x IN convex hull {a,b} /\ integral_vector x} = {a:real^2,b}`
470 (REPEAT_TCL CONJUNCTS_THEN SUBST1_TAC) THENL
471 [REPEAT CONJ_TAC THEN
472 (FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (SET_RULE
473 `{x | x IN cs /\ P x} = s
474 ==> t SUBSET s /\ t SUBSET ct /\ ct SUBSET cs /\
475 (s DIFF t) INTER ct = {}
476 ==> {x | x IN ct /\ P x} = t`)) THEN
477 REPEAT CONJ_TAC THENL
479 MATCH_ACCEPT_TAC HULL_SUBSET;
480 MATCH_MP_TAC HULL_MONO THEN SET_TAC[];
481 ASM_REWRITE_TAC[INSERT_DIFF; IN_INSERT; NOT_IN_EMPTY; EMPTY_DIFF] THEN
482 MATCH_MP_TAC(SET_RULE `~(x IN s) ==> {x} INTER s = {}`) THEN
483 REWRITE_TAC[GSYM SEGMENT_CONVEX_HULL; GSYM BETWEEN_IN_SEGMENT] THEN
484 DISCH_THEN(MP_TAC o MATCH_MP BETWEEN_IMP_COLLINEAR) THEN
485 UNDISCH_TAC `~collinear{a:real^2,b,c}` THEN REWRITE_TAC[INSERT_AC]]);
486 SIMP_TAC[CARD_CLAUSES; FINITE_INSERT; FINITE_EMPTY] THEN
487 ASM_REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY] THEN
488 CONV_TAC NUM_REDUCE_CONV THEN CONV_TAC REAL_RAT_REDUCE_CONV];
491 `?d:real^2. d IN convex hull {a, b, c} /\ integral_vector d /\
492 ~(d = a) /\ ~(d = b) /\ ~(d = c)`
493 STRIP_ASSUME_TAC THENL
494 [FIRST_X_ASSUM(MP_TAC o MATCH_MP (SET_RULE
495 `~(s = t) ==> t SUBSET s ==> ?d. d IN s /\ ~(d IN t)`)) THEN
496 REWRITE_TAC[SUBSET; FORALL_IN_INSERT; IN_ELIM_THM] THEN
497 ASM_SIMP_TAC[IN_INSERT; NOT_IN_EMPTY; DE_MORGAN_THM; GSYM CONJ_ASSOC] THEN
498 DISCH_THEN MATCH_MP_TAC THEN SIMP_TAC[HULL_INC; IN_INSERT];
500 FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE RAND_CONV
501 [COLLINEAR_3_EQ_AFFINE_DEPENDENT]) THEN
502 ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
504 [`measure:(real^2->bool)->real`;
505 `a:real^2`; `b:real^2`; `c:real^2`; `d:real^2`]
506 TRIANGLE_ADDITIVE_DECOMPOSITION) THEN
507 SIMP_TAC[MEASURE_UNION; MEASURABLE_COMPACT] THEN
508 ASM_REWRITE_TAC[] THEN DISCH_THEN SUBST1_TAC THEN
509 REWRITE_TAC[MEASURE_CONVEX_HULL_2_TRIVIAL; REAL_ADD_RID; REAL_SUB_RZERO] THEN
511 [`\s. &(CARD {x:real^2 | x IN s /\ integral_vector x})`;
512 `a:real^2`; `b:real^2`; `c:real^2`; `d:real^2`]
513 TRIANGLE_ADDITIVE_DECOMPOSITION) THEN
514 ASM_REWRITE_TAC[] THEN ANTS_TAC THENL
515 [REWRITE_TAC[SET_RULE `{x | x IN (s UNION t) /\ P x} =
516 {x | x IN s /\ P x} UNION {x | x IN t /\ P x}`;
517 SET_RULE `{x | x IN (s INTER t) /\ P x} =
518 {x | x IN s /\ P x} INTER {x | x IN t /\ P x}`] THEN
519 REPEAT STRIP_TAC THEN
520 REWRITE_TAC[REAL_ARITH `x:real = y + z - w <=> x + w = y + z`] THEN
521 REWRITE_TAC[REAL_OF_NUM_ADD; REAL_OF_NUM_EQ] THEN
522 MATCH_MP_TAC(ARITH_RULE
523 `x:num = (y + z) - w /\ w <= z ==> x + w = y + z`) THEN
525 [MATCH_MP_TAC CARD_UNION_GEN;
526 MATCH_MP_TAC CARD_SUBSET THEN REWRITE_TAC[INTER_SUBSET]] THEN
527 ASM_SIMP_TAC[FINITE_BOUNDED_INTEGER_POINTS; COMPACT_IMP_BOUNDED];
528 DISCH_THEN SUBST1_TAC] THEN
529 FIRST_X_ASSUM(fun th ->
530 MP_TAC(ISPECL [`a:real^2`; `b:real^2`; `d:real^2`] th) THEN
531 MP_TAC(ISPECL [`a:real^2`; `c:real^2`; `d:real^2`] th) THEN
532 MP_TAC(ISPECL [`b:real^2`; `c:real^2`; `d:real^2`] th)) THEN
533 ASM_REWRITE_TAC[] THEN
534 ANTS_TAC THENL [tac `a:real^2` `{b:real^2,c,d}`; DISCH_THEN SUBST1_TAC] THEN
535 ANTS_TAC THENL [tac `b:real^2` `{a:real^2,c,d}`; DISCH_THEN SUBST1_TAC] THEN
536 ANTS_TAC THENL [tac `c:real^2` `{a:real^2,b,d}`; DISCH_THEN SUBST1_TAC] THEN
537 SUBGOAL_THEN `{x:real^2 | x IN convex hull {d} /\ integral_vector x} = {d}`
539 [REWRITE_TAC[CONVEX_HULL_SING] THEN ASM SET_TAC[]; ALL_TAC] THEN
540 SIMP_TAC[CARD_CLAUSES; FINITE_RULES; NOT_IN_EMPTY] THEN
541 CONV_TAC NUM_REDUCE_CONV THEN
542 REWRITE_TAC[SET_RULE `{x | x IN s /\ P x} = s INTER P`] THEN
543 REWRITE_TAC[INSERT_AC] THEN REAL_ARITH_TAC);;
545 let PICK_TRIANGLE = prove
547 integral_vector a /\ integral_vector b /\ integral_vector c
548 ==> measure(convex hull {a,b,c}) =
549 if collinear {a,b,c} then &0
550 else &(CARD {x | x IN interior(convex hull {a,b,c}) /\
551 integral_vector x}) +
552 &(CARD {x | x IN frontier(convex hull {a,b,c}) /\
553 integral_vector x}) / &2 - &1`,
554 REPEAT STRIP_TAC THEN COND_CASES_TAC THEN
555 ASM_SIMP_TAC[MEASURE_EQ_0; COLLINEAR_IMP_NEGLIGIBLE;
556 COLLINEAR_CONVEX_HULL_COLLINEAR] THEN
557 ASM_SIMP_TAC[PICK_TRIANGLE_ALT] THEN
558 REWRITE_TAC[INTERIOR_OF_TRIANGLE; FRONTIER_OF_TRIANGLE] THEN
560 `{x | x IN (s DIFF t) /\ P x} =
561 {x | x IN s /\ P x} DIFF {x | x IN t /\ P x}`] THEN
562 MATCH_MP_TAC(REAL_ARITH
563 `i + c = s /\ ccc = c + &3
564 ==> s - ccc / &2 + &1 / &2 = i + c / &2 - &1`) THEN
566 [REWRITE_TAC[REAL_OF_NUM_ADD; REAL_OF_NUM_EQ] THEN
567 MATCH_MP_TAC(ARITH_RULE `y:num <= x /\ x - y = z ==> z + y = x`) THEN
569 [MATCH_MP_TAC CARD_SUBSET; MATCH_MP_TAC(GSYM CARD_DIFF)] THEN
570 ASM_SIMP_TAC[FINITE_BOUNDED_INTEGER_POINTS;
571 FINITE_IMP_BOUNDED_CONVEX_HULL; FINITE_INSERT; FINITE_EMPTY] THEN
572 MATCH_MP_TAC(SET_RULE
573 `s SUBSET t ==> {x | x IN s /\ P x} SUBSET {x | x IN t /\ P x}`) THEN
574 REWRITE_TAC[UNION_SUBSET; SEGMENT_CONVEX_HULL] THEN
575 REPEAT CONJ_TAC THEN MATCH_MP_TAC HULL_MONO THEN SET_TAC[];
577 `{x | x IN (s UNION t) /\ P x} =
578 {x | x IN s /\ P x} UNION {x | x IN t /\ P x}`] THEN
579 SIMP_TAC[CARD_UNION_GEN; FINITE_BOUNDED_INTEGER_POINTS;
580 FINITE_INTER; FINITE_UNION; BOUNDED_SEGMENT; UNION_OVER_INTER] THEN
582 `{x | x IN s /\ P x} INTER {x | x IN t /\ P x} =
583 {x | x IN (s INTER t) /\ P x}`] THEN
585 `segment[b:real^2,c] INTER segment [c,a] = {c} /\
586 segment[a,b] INTER segment [b,c] = {b} /\
587 segment[a,b] INTER segment [c,a] = {a}`
588 (REPEAT_TCL CONJUNCTS_THEN SUBST1_TAC) THENL
589 [ASM_MESON_TAC[INTER_SEGMENT; SEGMENT_SYM; INSERT_AC]; ALL_TAC] THEN
590 ASM_SIMP_TAC[SET_RULE `P a ==> {x | x IN {a} /\ P x} = {a}`] THEN
591 ASM_CASES_TAC `b:real^2 = a` THENL
592 [ASM_MESON_TAC[COLLINEAR_2; INSERT_AC]; ALL_TAC] THEN
593 ASM_SIMP_TAC[SET_RULE `~(a = b) ==> {b} INTER {a} = {}`] THEN
594 REWRITE_TAC[REAL_OF_NUM_ADD; REAL_OF_NUM_EQ] THEN
595 REWRITE_TAC[NOT_IN_EMPTY; EMPTY_GSPEC; CARD_CLAUSES; SUB_0] THEN
596 MATCH_MP_TAC(ARITH_RULE
597 `c:num <= ca /\ a <= ab /\ b <= bc /\
598 bc' + ac' + ab' + a + b + c = ab + bc + ca + 3
599 ==> bc' + ac' + ab' = (ab + (bc + ca) - c) - (b + a) + 3`) THEN
600 ASM_SIMP_TAC[CARD_SUBSET; SING_SUBSET; IN_ELIM_THM; ENDS_IN_SEGMENT;
601 FINITE_BOUNDED_INTEGER_POINTS; BOUNDED_SEGMENT] THEN
602 SIMP_TAC[NOT_IN_EMPTY; EMPTY_GSPEC; CARD_CLAUSES; FINITE_INSERT;
603 FINITE_EMPTY] THEN CONV_TAC NUM_REDUCE_CONV THEN
604 REWRITE_TAC[SET_RULE `{x | x IN s /\ P x} = s INTER P`] THEN
605 REWRITE_TAC[SEGMENT_CONVEX_HULL; INSERT_AC] THEN ARITH_TAC]);;
607 (* ------------------------------------------------------------------------- *)
608 (* Parity lemma for segment crossing a polygon. *)
609 (* ------------------------------------------------------------------------- *)
611 let PARITY_LEMMA = prove
612 (`!a b c d p x:real^2.
613 simple_path(p ++ linepath(a,b)) /\
614 pathstart p = b /\ pathfinish p = a /\
615 segment(a,b) INTER segment(c,d) = {x} /\
616 segment[c,d] INTER path_image p = {}
617 ==> (c IN inside(path_image(p ++ linepath(a,b))) <=>
618 d IN outside(path_image(p ++ linepath(a,b))))`,
621 collinear{y,a,b} /\ between x (a,b) /\
622 dist(y,x) < dist(x,b) /\ dist(y,x) < dist(x,a)
623 ==> y IN segment(a,b)`,
624 REPEAT STRIP_TAC THEN MATCH_MP_TAC COLLINEAR_DIST_IN_OPEN_SEGMENT THEN
625 ASM_REWRITE_TAC[] THEN
626 REPEAT(POP_ASSUM MP_TAC) THEN REWRITE_TAC[between; DIST_SYM] THEN
629 (`(!n. P(--n) <=> P (n)) /\ (!n. &0 < n dot x ==> P n)
630 ==> !n:real^N. ~(n dot x = &0) ==> P n`,
631 STRIP_TAC THEN GEN_TAC THEN
632 REWRITE_TAC[REAL_ARITH `~(x = &0) <=> &0 < x \/ &0 < --x`] THEN
633 REWRITE_TAC[GSYM DOT_LNEG] THEN ASM_MESON_TAC[]) in
634 REPEAT STRIP_TAC THEN
635 MP_TAC(ISPECL [`p:real^1->real^2`; `linepath(a:real^2,b)`]
636 SIMPLE_PATH_JOIN_LOOP_EQ) THEN
637 FIRST_ASSUM(MP_TAC o MATCH_MP SIMPLE_PATH_IMP_PATH) THEN
638 ASM_SIMP_TAC[PATH_JOIN; PATHSTART_LINEPATH; PATHFINISH_LINEPATH] THEN
639 DISCH_THEN(ASSUME_TAC o CONJUNCT1) THEN STRIP_TAC THEN
640 MP_TAC(ISPECL [`(a:real^2) INSERT b INSERT c INSERT d INSERT path_image p`;
642 DISTANCE_ATTAINS_INF) THEN
643 REWRITE_TAC[FORALL_IN_INSERT] THEN
644 ONCE_REWRITE_TAC[SET_RULE `a INSERT b INSERT c INSERT d INSERT s =
645 {a,b,c,d} UNION s`] THEN
646 ASM_SIMP_TAC[CLOSED_UNION; FINITE_IMP_CLOSED; CLOSED_PATH_IMAGE;
647 FINITE_INSERT; FINITE_EMPTY] THEN
648 ANTS_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
649 DISCH_THEN(X_CHOOSE_THEN `cp:real^2` MP_TAC) THEN
650 DISJ_CASES_TAC(NORM_ARITH `cp = x \/ &0 < dist(x:real^2,cp)`) THENL
651 [FIRST_X_ASSUM SUBST_ALL_TAC THEN
652 MATCH_MP_TAC(TAUT `~a ==> a /\ b ==> c`) THEN
653 FIRST_ASSUM(MP_TAC o MATCH_MP (SET_RULE `a = {x} ==> x IN a`)) THEN
654 REWRITE_TAC[open_segment; IN_DIFF; IN_UNION; IN_INSERT; NOT_IN_EMPTY;
655 IN_INTER; DE_MORGAN_THM] THEN
656 STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
657 FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (SET_RULE
658 `p INTER s SUBSET u ==> x IN (s DIFF u) ==> ~(x IN p)`)) THEN
659 ASM_REWRITE_TAC[IN_DIFF; IN_INSERT; NOT_IN_EMPTY; PATH_IMAGE_LINEPATH];
661 ABBREV_TAC `e = dist(x:real^2,cp)` THEN FIRST_X_ASSUM(K ALL_TAC o SYM) THEN
662 DISCH_THEN(STRIP_ASSUME_TAC o CONJUNCT2) THEN
663 RULE_ASSUM_TAC(REWRITE_RULE[ARC_LINEPATH_EQ]) THEN
664 MP_TAC(ISPECL [`a:real^2`; `b:real^2`; `c:real^2`; `d:real^2`]
665 FINITE_INTER_COLLINEAR_OPEN_SEGMENTS) THEN
666 MP_TAC(ISPECL [`a:real^2`; `b:real^2`; `d:real^2`; `c:real^2`]
667 FINITE_INTER_COLLINEAR_OPEN_SEGMENTS) THEN
668 SUBST1_TAC(MESON[SEGMENT_SYM] `segment(d:real^2,c) = segment(c,d)`) THEN
669 ASM_REWRITE_TAC[FINITE_SING; NOT_INSERT_EMPTY] THEN REPEAT DISCH_TAC THEN
670 SUBGOAL_THEN `~(a IN segment[c:real^2,d]) /\ ~(b IN segment[c,d])`
671 STRIP_ASSUME_TAC THENL
672 [ASM_MESON_TAC[PATHSTART_IN_PATH_IMAGE; PATHFINISH_IN_PATH_IMAGE;
673 IN_INTER; NOT_IN_EMPTY];
675 SUBGOAL_THEN `~(c:real^2 = a) /\ ~(c = b) /\ ~(d = a) /\ ~(d = b)`
676 STRIP_ASSUME_TAC THENL [ASM_MESON_TAC[ENDS_IN_SEGMENT]; ALL_TAC] THEN
677 SUBGOAL_THEN `x IN segment(a:real^2,b) /\ x IN segment(c,d)` MP_TAC THENL
678 [ASM SET_TAC[]; ALL_TAC] THEN
679 REWRITE_TAC[IN_OPEN_SEGMENT_ALT] THEN STRIP_TAC THEN
681 `{c,d} INTER path_image(p ++ linepath(a:real^2,b)) = {}`
683 [ASM_SIMP_TAC[PATH_IMAGE_JOIN; PATH_LINEPATH; PATHSTART_LINEPATH] THEN
685 `{c,d} INTER (s UNION t) = {} <=>
686 (~(c IN s) /\ ~(d IN s)) /\ ~(c IN t) /\ ~(d IN t)`] THEN
688 [ASM_MESON_TAC[ENDS_IN_SEGMENT; IN_INTER; NOT_IN_EMPTY];
689 REWRITE_TAC[PATH_IMAGE_LINEPATH; GSYM BETWEEN_IN_SEGMENT] THEN
690 CONJ_TAC THEN DISCH_THEN(ASSUME_TAC o MATCH_MP BETWEEN_IMP_COLLINEAR) THEN
691 RULE_ASSUM_TAC(REWRITE_RULE[INSERT_AC]) THEN ASM_MESON_TAC[]];
693 MP_TAC(ISPEC `b - x:real^2` ORTHOGONAL_TO_VECTOR_EXISTS) THEN
694 REWRITE_TAC[DIMINDEX_2; LE_REFL; LEFT_IMP_EXISTS_THM] THEN
695 X_GEN_TAC `n:real^2` THEN STRIP_TAC THEN
696 SUBGOAL_THEN `(x:real^2) IN segment(a,b) /\ x IN segment(c,d)` MP_TAC THENL
698 SIMP_TAC[IN_OPEN_SEGMENT_ALT; GSYM BETWEEN_IN_SEGMENT] THEN STRIP_TAC] THEN
699 SUBGOAL_THEN `~collinear{a:real^2, b, c, d}` ASSUME_TAC THENL
700 [UNDISCH_TAC `~collinear{a:real^2,b,c}` THEN REWRITE_TAC[CONTRAPOS_THM] THEN
701 MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ_ALT] COLLINEAR_SUBSET) THEN SET_TAC[];
703 SUBGOAL_THEN `~(n dot (d - x:real^2) = &0)` MP_TAC THENL
704 [REWRITE_TAC[GSYM orthogonal] THEN DISCH_TAC THEN
705 MP_TAC(SPECL [`n:real^2`; `d - x:real^2`; `b - x:real^2`]
706 ORTHOGONAL_TO_ORTHOGONAL_2D) THEN
707 ANTS_TAC THENL [ASM_MESON_TAC[ORTHOGONAL_SYM]; ALL_TAC] THEN
708 REWRITE_TAC[GSYM COLLINEAR_3] THEN DISCH_TAC THEN
709 UNDISCH_TAC `~collinear{a:real^2, b, c, d}` THEN ASM_REWRITE_TAC[] THEN
710 ONCE_REWRITE_TAC[SET_RULE `{a,b,c,d} = {b,d,a,c}`] THEN
711 ASM_SIMP_TAC[COLLINEAR_4_3] THEN CONJ_TAC THENL
712 [MATCH_MP_TAC COLLINEAR_SUBSET THEN EXISTS_TAC `{b:real^2,x,a,d}` THEN
713 CONJ_TAC THENL [ASM_SIMP_TAC[COLLINEAR_4_3]; SET_TAC[]] THEN
714 ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {c,b,a}`] THEN
715 ASM_SIMP_TAC[BETWEEN_IMP_COLLINEAR];
716 MATCH_MP_TAC COLLINEAR_SUBSET THEN EXISTS_TAC `{d:real^2,x,b,c}` THEN
717 CONJ_TAC THENL [ASM_SIMP_TAC[COLLINEAR_4_3]; SET_TAC[]] THEN
718 ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {c,b,a}`] THEN
719 ASM_SIMP_TAC[BETWEEN_IMP_COLLINEAR]];
721 DISCH_THEN(fun th -> POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN
723 SPEC_TAC(`n:real^2`,`n:real^2`) THEN
724 MATCH_MP_TAC symlemma THEN CONJ_TAC THENL
725 [REWRITE_TAC[ORTHOGONAL_RNEG; VECTOR_NEG_EQ_0]; ALL_TAC] THEN
726 GEN_TAC THEN DISCH_TAC THEN STRIP_TAC THEN
727 SUBGOAL_THEN `n dot (c - x:real^2) < &0` ASSUME_TAC THENL
728 [UNDISCH_TAC `&0 < n dot (d - x:real^2)` THEN
729 SUBGOAL_THEN `(x:real^2) IN segment(c,d)` MP_TAC THENL
730 [ASM SET_TAC[]; ALL_TAC] THEN
731 ASM_REWRITE_TAC[IN_SEGMENT] THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
732 REWRITE_TAC[VECTOR_ARITH
733 `d - ((&1 - u) % c + u % d):real^N = (&1 - u) % (d - c) /\
734 c - ((&1 - u) % c + u % d) = --u % (d - c)`] THEN
735 REWRITE_TAC[DOT_RMUL; REAL_MUL_LNEG; REAL_ARITH `--x < &0 <=> &0 < x`] THEN
736 ASM_SIMP_TAC[REAL_LT_MUL_EQ; REAL_SUB_LT];
739 `!y. y IN ball(x:real^2,e)
740 ==> y IN segment(a,b) \/
741 &0 < n dot (y - x) \/
744 [REWRITE_TAC[IN_BALL] THEN REPEAT STRIP_TAC THEN
745 MATCH_MP_TAC(TAUT `(~c /\ ~b ==> a) ==> a \/ b \/ c`) THEN
746 REWRITE_TAC[REAL_ARITH `~(x < &0) /\ ~(&0 < x) <=> x = &0`] THEN
747 REWRITE_TAC[GSYM orthogonal] THEN DISCH_TAC THEN
748 MP_TAC(SPECL [`n:real^2`; `y - x:real^2`; `b - x:real^2`]
749 ORTHOGONAL_TO_ORTHOGONAL_2D) THEN
750 ANTS_TAC THENL [ASM_MESON_TAC[ORTHOGONAL_SYM]; ALL_TAC] THEN
751 REWRITE_TAC[GSYM COLLINEAR_3] THEN DISCH_TAC THEN
752 MATCH_MP_TAC lemma THEN EXISTS_TAC `x:real^2` THEN
753 ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
754 [ALL_TAC; ASM_MESON_TAC[REAL_LTE_TRANS; DIST_SYM]] THEN
755 ONCE_REWRITE_TAC[SET_RULE `{y,a,b} = {a,b,y}`] THEN
756 MATCH_MP_TAC COLLINEAR_3_TRANS THEN EXISTS_TAC `x:real^2` THEN
757 ASM_REWRITE_TAC[] THEN UNDISCH_TAC `collinear{y:real^2, x, b}` THEN
758 MP_TAC(MATCH_MP BETWEEN_IMP_COLLINEAR (ASSUME
759 `between (x:real^2) (a,b)`)) THEN
762 MP_TAC(SPEC `p ++ linepath(a:real^2,b)` JORDAN_INSIDE_OUTSIDE) THEN
763 ASM_REWRITE_TAC[PATHFINISH_JOIN; PATHSTART_JOIN; PATHFINISH_LINEPATH] THEN
766 `~(connected_component((:real^2) DIFF path_image(p ++ linepath (a,b))) c d)`
769 ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN
770 DISCH_THEN(MP_TAC o SPEC `path_image(p ++ linepath(a:real^2,b))` o
772 `~(x IN s <=> y IN t)
773 ==> !p. s UNION t = (:real^2) DIFF p /\ {x,y} INTER p = {}
774 ==> x IN s /\ y IN s \/ x IN t /\ y IN t`)) THEN
775 ASM_REWRITE_TAC[connected_component] THEN
776 ASM_REWRITE_TAC[SET_RULE `t SUBSET UNIV DIFF s <=> t INTER s = {}`] THEN
777 ASM_MESON_TAC[INSIDE_NO_OVERLAP; OUTSIDE_NO_OVERLAP]] THEN
778 MP_TAC(SPEC `p ++ linepath(a:real^2,b)` JORDAN_DISCONNECTED) THEN
779 ASM_REWRITE_TAC[PATHFINISH_JOIN; PATHSTART_JOIN; PATHFINISH_LINEPATH] THEN
780 REWRITE_TAC[CONNECTED_IFF_CONNECTED_COMPONENT] THEN
782 `!u v. u IN inside(path_image(p ++ linepath(a,b))) /\
783 v IN outside(path_image(p ++ linepath(a,b)))
784 ==> connected_component
785 ((:real^2) DIFF path_image (p ++ linepath (a,b))) u v`
788 MAP_EVERY X_GEN_TAC [`u:real^2`; `v:real^2`] THEN
789 GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV)
790 [SYM(ASSUME `inside (path_image (p ++ linepath (a,b))) UNION
791 outside (path_image (p ++ linepath (a,b))) =
792 (:real^2) DIFF path_image (p ++ linepath (a,b))`)] THEN
793 REWRITE_TAC[IN_UNION; CONNECTED_IFF_CONNECTED_COMPONENT] THEN
795 [REWRITE_TAC[connected_component] THEN
796 EXISTS_TAC `inside(path_image(p ++ linepath(a:real^2,b)))`;
798 ASM_MESON_TAC[CONNECTED_COMPONENT_SYM];
799 REWRITE_TAC[connected_component] THEN
800 EXISTS_TAC `outside(path_image(p ++ linepath(a:real^2,b)))`] THEN
801 ASM_REWRITE_TAC[SET_RULE `s SUBSET UNIV DIFF t <=> s INTER t = {}`] THEN
802 REWRITE_TAC[OUTSIDE_NO_OVERLAP; INSIDE_NO_OVERLAP]] THEN
803 SUBGOAL_THEN `(x:real^2) IN path_image(p ++ linepath(a,b))` ASSUME_TAC THENL
804 [ASM_SIMP_TAC[PATHSTART_LINEPATH; PATH_IMAGE_JOIN; PATH_LINEPATH] THEN
805 REWRITE_TAC[IN_UNION; PATH_IMAGE_LINEPATH] THEN DISJ2_TAC THEN
806 RULE_ASSUM_TAC(REWRITE_RULE[open_segment]) THEN ASM SET_TAC[];
808 MAP_EVERY X_GEN_TAC [`u:real^2`; `v:real^2`] THEN STRIP_TAC THEN
810 `frontier(inside(path_image(p ++ linepath(a:real^2,b)))) =
811 path_image(p ++ linepath(a,b))` THEN
812 REWRITE_TAC[EXTENSION] THEN
813 DISCH_THEN(MP_TAC o SPEC `x:real^2`) THEN ASM_REWRITE_TAC[frontier] THEN
814 REWRITE_TAC[IN_DIFF; CLOSURE_APPROACHABLE] THEN
815 DISCH_THEN(MP_TAC o SPEC `e:real` o CONJUNCT1) THEN
816 ASM_REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
817 X_GEN_TAC `w:real^2` THEN STRIP_TAC THEN
818 MATCH_MP_TAC CONNECTED_COMPONENT_TRANS THEN EXISTS_TAC `w:real^2` THEN
820 [REWRITE_TAC[connected_component] THEN
821 EXISTS_TAC `inside(path_image(p ++ linepath(a:real^2,b)))` THEN
822 ASM_REWRITE_TAC[SET_RULE `s SUBSET UNIV DIFF t <=> s INTER t = {}`] THEN
823 REWRITE_TAC[INSIDE_NO_OVERLAP];
826 `frontier(outside(path_image(p ++ linepath(a:real^2,b)))) =
827 path_image(p ++ linepath(a,b))` THEN
828 REWRITE_TAC[EXTENSION] THEN
829 DISCH_THEN(MP_TAC o SPEC `x:real^2`) THEN ASM_REWRITE_TAC[frontier] THEN
830 REWRITE_TAC[IN_DIFF; CLOSURE_APPROACHABLE] THEN
831 DISCH_THEN(MP_TAC o SPEC `e:real` o CONJUNCT1) THEN
832 ASM_REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
833 X_GEN_TAC `z:real^2` THEN STRIP_TAC THEN
834 MATCH_MP_TAC CONNECTED_COMPONENT_TRANS THEN EXISTS_TAC `z:real^2` THEN
837 REWRITE_TAC[connected_component] THEN
838 EXISTS_TAC `outside(path_image(p ++ linepath(a:real^2,b)))` THEN
839 ASM_REWRITE_TAC[SET_RULE `s SUBSET UNIV DIFF t <=> s INTER t = {}`] THEN
840 REWRITE_TAC[OUTSIDE_NO_OVERLAP]] THEN
842 `!y. dist(y,x) < e /\ ~(y IN path_image(p ++ linepath (a,b)))
843 ==> connected_component
844 ((:real^2) DIFF path_image(p ++ linepath(a,b))) c y`
847 MATCH_MP_TAC CONNECTED_COMPONENT_TRANS THEN EXISTS_TAC `c:real^2` THEN
848 CONJ_TAC THENL [MATCH_MP_TAC CONNECTED_COMPONENT_SYM; ALL_TAC] THEN
849 FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN
850 ASM_MESON_TAC[INSIDE_NO_OVERLAP; OUTSIDE_NO_OVERLAP; IN_INTER;
852 X_GEN_TAC `y:real^2` THEN STRIP_TAC THEN
853 SUBGOAL_THEN `segment[c,d] INTER path_image(p ++ linepath(a,b)) = {x:real^2}`
855 [MATCH_MP_TAC(SET_RULE
856 `{c,d} INTER p = {} /\ (segment[c,d] DIFF {c,d}) INTER p = {x}
857 ==> segment[c,d] INTER p = {x}`) THEN
858 ASM_SIMP_TAC[PATH_IMAGE_JOIN; PATHSTART_LINEPATH; PATH_LINEPATH] THEN
859 MATCH_MP_TAC(SET_RULE
860 `cd INTER p = {} /\ l INTER (cd DIFF {c,d}) = {x}
861 ==> (cd DIFF {c,d}) INTER (p UNION l) = {x}`) THEN
862 ASM_REWRITE_TAC[GSYM open_segment; PATH_IMAGE_LINEPATH] THEN
863 MATCH_MP_TAC(SET_RULE
864 `~(a IN segment[c,d]) /\ ~(b IN segment[c,d]) /\
865 segment(a,b) INTER segment(c,d) = {x} /\
866 segment(a,b) = segment[a,b] DIFF {a,b} /\
867 segment(c,d) = segment[c,d] DIFF {c,d}
868 ==> segment[a,b] INTER segment(c,d) = {x}`) THEN
869 ASM_REWRITE_TAC[] THEN REWRITE_TAC[open_segment];
872 `!y. y IN ball(x:real^2,e)
873 ==> y IN segment(a,b) \/ &0 < n dot (y - x) \/ n dot (y - x) < &0`
874 (MP_TAC o SPEC `y:real^2`) THEN
875 REWRITE_TAC[IN_BALL] THEN ONCE_REWRITE_TAC[DIST_SYM] THEN
876 ASM_REWRITE_TAC[] THEN
877 DISCH_THEN(REPEAT_TCL DISJ_CASES_THEN MP_TAC) THENL
878 [MATCH_MP_TAC(TAUT `~p ==> p ==> q`) THEN
879 UNDISCH_TAC `~(y IN path_image(p ++ linepath(a:real^2,b)))` THEN
880 ASM_SIMP_TAC[PATHSTART_LINEPATH; PATH_IMAGE_JOIN; PATH_LINEPATH] THEN
881 SIMP_TAC[CONTRAPOS_THM; open_segment; IN_DIFF; IN_UNION;
882 PATH_IMAGE_LINEPATH];
883 DISCH_TAC THEN MATCH_MP_TAC CONNECTED_COMPONENT_TRANS THEN
884 EXISTS_TAC `d:real^2` THEN ASM_REWRITE_TAC[] THEN
885 MATCH_MP_TAC CONNECTED_COMPONENT_TRANS THEN
886 EXISTS_TAC `x + min (&1 / &2) (e / &2 / norm(d - x)) % (d - x):real^2` THEN
887 REWRITE_TAC[connected_component] THEN CONJ_TAC THENL
888 [EXISTS_TAC `segment[x:real^2,d] DELETE x` THEN
889 SIMP_TAC[CONVEX_SEMIOPEN_SEGMENT; CONVEX_CONNECTED] THEN
890 ASM_REWRITE_TAC[IN_DELETE; ENDS_IN_SEGMENT] THEN REPEAT CONJ_TAC THENL
891 [FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP (SET_RULE
894 ==> (xd DELETE x) SUBSET (UNIV DIFF p)`)) THEN
895 REWRITE_TAC[SUBSET_SEGMENT; ENDS_IN_SEGMENT] THEN
896 UNDISCH_TAC `segment (a,b) INTER segment (c,d) = {x:real^2}` THEN
897 REWRITE_TAC[open_segment] THEN SET_TAC[];
898 REWRITE_TAC[IN_SEGMENT; VECTOR_ARITH
899 `x + a % (y - x):real^N = (&1 - a) % x + a % y`] THEN
900 EXISTS_TAC `min (&1 / &2) (e / &2 / norm(d - x:real^2))` THEN
901 REWRITE_TAC[] THEN CONJ_TAC THENL [ALL_TAC; REAL_ARITH_TAC] THEN
902 REWRITE_TAC[REAL_LE_MIN] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
903 ASM_SIMP_TAC[REAL_LE_DIV; REAL_POS; NORM_POS_LE; REAL_LT_IMP_LE];
904 ASM_REWRITE_TAC[VECTOR_MUL_EQ_0; VECTOR_SUB_EQ;
905 VECTOR_ARITH `x + a:real^N = x <=> a = vec 0`] THEN
906 MATCH_MP_TAC(REAL_ARITH `&0 < x ==> ~(min (&1 / &2) x = &0)`) THEN
907 MATCH_MP_TAC REAL_LT_DIV THEN ASM_REWRITE_TAC[REAL_HALF] THEN
908 ASM_REWRITE_TAC[NORM_POS_LT; VECTOR_SUB_EQ]];
909 EXISTS_TAC `ball(x,e) INTER {w:real^2 | &0 < n dot (w - x)}` THEN
910 REPEAT CONJ_TAC THENL
911 [MATCH_MP_TAC CONVEX_CONNECTED THEN MATCH_MP_TAC CONVEX_INTER THEN
912 REWRITE_TAC[CONVEX_BALL; DOT_RSUB; REAL_SUB_LT] THEN
913 REWRITE_TAC[GSYM real_gt; CONVEX_HALFSPACE_GT];
914 ASM_SIMP_TAC[PATHSTART_LINEPATH; PATH_IMAGE_JOIN; PATH_LINEPATH] THEN
915 MATCH_MP_TAC(SET_RULE
916 `p SUBSET (UNIV DIFF b) /\ l INTER w = {}
917 ==> (b INTER w) SUBSET (UNIV DIFF (p UNION l))`) THEN
918 ASM_REWRITE_TAC[SUBSET; IN_DIFF; IN_UNIV; IN_BALL; REAL_NOT_LT] THEN
919 MATCH_MP_TAC(SET_RULE
920 `!t. t INTER u = {} /\ s SUBSET t ==> s INTER u = {}`) THEN
921 EXISTS_TAC `affine hull {x:real^2,b}` THEN CONJ_TAC THENL
922 [REWRITE_TAC[AFFINE_HULL_2; FORALL_IN_GSPEC; SET_RULE
923 `s INTER t = {} <=> !x. x IN s ==> ~(x IN t)`] THEN
924 REWRITE_TAC[IN_ELIM_THM] THEN
925 SIMP_TAC[REAL_ARITH `u + v = &1 <=> u = &1 - v`] THEN
926 REWRITE_TAC[DOT_RMUL; VECTOR_ARITH
927 `((&1 - v) % x + v % b) - x:real^N = v % (b - x)`] THEN
928 RULE_ASSUM_TAC(REWRITE_RULE[orthogonal]) THEN
929 ONCE_REWRITE_TAC[DOT_SYM] THEN
930 ASM_REWRITE_TAC[REAL_MUL_RZERO; REAL_LT_REFL];
931 REWRITE_TAC[PATH_IMAGE_LINEPATH; SEGMENT_CONVEX_HULL] THEN
932 SIMP_TAC[SUBSET_HULL; AFFINE_IMP_CONVEX; AFFINE_AFFINE_HULL] THEN
933 REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET] THEN
934 SIMP_TAC[HULL_INC; IN_INSERT] THEN
935 ASM_SIMP_TAC[GSYM COLLINEAR_3_AFFINE_HULL] THEN
936 ONCE_REWRITE_TAC[SET_RULE `{x,b,a} = {a,x,b}`] THEN
937 MATCH_MP_TAC BETWEEN_IMP_COLLINEAR THEN ASM_REWRITE_TAC[]];
938 REWRITE_TAC[IN_BALL; IN_INTER; IN_ELIM_THM; dist] THEN
939 REWRITE_TAC[NORM_ARITH `norm(x - (x + a):real^N) = norm a`] THEN
940 REWRITE_TAC[VECTOR_ARITH `(x + a) - x:real^N = a`] THEN CONJ_TAC THENL
941 [ASM_SIMP_TAC[NORM_MUL; GSYM REAL_LT_RDIV_EQ; NORM_POS_LT;
943 MATCH_MP_TAC(REAL_ARITH
944 `&0 < x /\ x < e ==> abs(min (&1 / &2) x) < e`) THEN
945 ASM_SIMP_TAC[REAL_LT_DIV; REAL_HALF; NORM_POS_LT; VECTOR_SUB_EQ;
946 REAL_LT_DIV2_EQ] THEN ASM_REAL_ARITH_TAC;
947 REWRITE_TAC[DOT_RMUL] THEN MATCH_MP_TAC REAL_LT_MUL THEN
948 ASM_REWRITE_TAC[REAL_LT_MIN] THEN
949 ASM_SIMP_TAC[REAL_LT_DIV; REAL_HALF; NORM_POS_LT; VECTOR_SUB_EQ;
951 REWRITE_TAC[IN_BALL; IN_INTER; IN_ELIM_THM] THEN
952 ONCE_REWRITE_TAC[DIST_SYM] THEN ASM_REWRITE_TAC[]]];
953 DISCH_TAC THEN MATCH_MP_TAC CONNECTED_COMPONENT_TRANS THEN
954 EXISTS_TAC `x + min (&1 / &2) (e / &2 / norm(c - x)) % (c - x):real^2` THEN
955 REWRITE_TAC[connected_component] THEN CONJ_TAC THENL
956 [EXISTS_TAC `segment[x:real^2,c] DELETE x` THEN
957 SIMP_TAC[CONVEX_SEMIOPEN_SEGMENT; CONVEX_CONNECTED] THEN
958 ASM_REWRITE_TAC[IN_DELETE; ENDS_IN_SEGMENT] THEN REPEAT CONJ_TAC THENL
959 [FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP (SET_RULE
962 ==> (xd DELETE x) SUBSET (UNIV DIFF p)`)) THEN
963 REWRITE_TAC[SUBSET_SEGMENT; ENDS_IN_SEGMENT] THEN
964 UNDISCH_TAC `segment (a,b) INTER segment (c,d) = {x:real^2}` THEN
965 REWRITE_TAC[open_segment] THEN SET_TAC[];
966 REWRITE_TAC[IN_SEGMENT; VECTOR_ARITH
967 `x + a % (y - x):real^N = (&1 - a) % x + a % y`] THEN
968 EXISTS_TAC `min (&1 / &2) (e / &2 / norm(c - x:real^2))` THEN
969 REWRITE_TAC[] THEN CONJ_TAC THENL [ALL_TAC; REAL_ARITH_TAC] THEN
970 REWRITE_TAC[REAL_LE_MIN] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
971 ASM_SIMP_TAC[REAL_LE_DIV; REAL_POS; NORM_POS_LE; REAL_LT_IMP_LE];
972 ASM_REWRITE_TAC[VECTOR_MUL_EQ_0; VECTOR_SUB_EQ;
973 VECTOR_ARITH `x + a:real^N = x <=> a = vec 0`] THEN
974 MATCH_MP_TAC(REAL_ARITH `&0 < x ==> ~(min (&1 / &2) x = &0)`) THEN
975 MATCH_MP_TAC REAL_LT_DIV THEN ASM_REWRITE_TAC[REAL_HALF] THEN
976 ASM_REWRITE_TAC[NORM_POS_LT; VECTOR_SUB_EQ]];
977 EXISTS_TAC `ball(x,e) INTER {w:real^2 | n dot (w - x) < &0}` THEN
978 REPEAT CONJ_TAC THENL
979 [MATCH_MP_TAC CONVEX_CONNECTED THEN MATCH_MP_TAC CONVEX_INTER THEN
980 REWRITE_TAC[CONVEX_BALL; DOT_RSUB; REAL_ARITH `a - b < &0 <=> a < b`;
981 CONVEX_HALFSPACE_LT];
982 ASM_SIMP_TAC[PATHSTART_LINEPATH; PATH_IMAGE_JOIN; PATH_LINEPATH] THEN
983 MATCH_MP_TAC(SET_RULE
984 `p SUBSET (UNIV DIFF b) /\ l INTER w = {}
985 ==> (b INTER w) SUBSET (UNIV DIFF (p UNION l))`) THEN
986 ASM_REWRITE_TAC[SUBSET; IN_DIFF; IN_UNIV; IN_BALL; REAL_NOT_LT] THEN
987 MATCH_MP_TAC(SET_RULE
988 `!t. t INTER u = {} /\ s SUBSET t ==> s INTER u = {}`) THEN
989 EXISTS_TAC `affine hull {x:real^2,b}` THEN CONJ_TAC THENL
990 [REWRITE_TAC[AFFINE_HULL_2; FORALL_IN_GSPEC; SET_RULE
991 `s INTER t = {} <=> !x. x IN s ==> ~(x IN t)`] THEN
992 REWRITE_TAC[IN_ELIM_THM] THEN
993 SIMP_TAC[REAL_ARITH `u + v = &1 <=> u = &1 - v`] THEN
994 REWRITE_TAC[DOT_RMUL; VECTOR_ARITH
995 `((&1 - v) % x + v % b) - x:real^N = v % (b - x)`] THEN
996 RULE_ASSUM_TAC(REWRITE_RULE[orthogonal]) THEN
997 ONCE_REWRITE_TAC[DOT_SYM] THEN
998 ASM_REWRITE_TAC[REAL_MUL_RZERO; REAL_LT_REFL];
999 REWRITE_TAC[PATH_IMAGE_LINEPATH; SEGMENT_CONVEX_HULL] THEN
1000 SIMP_TAC[SUBSET_HULL; AFFINE_IMP_CONVEX; AFFINE_AFFINE_HULL] THEN
1001 REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET] THEN
1002 SIMP_TAC[HULL_INC; IN_INSERT] THEN
1003 ASM_SIMP_TAC[GSYM COLLINEAR_3_AFFINE_HULL] THEN
1004 ONCE_REWRITE_TAC[SET_RULE `{x,b,a} = {a,x,b}`] THEN
1005 MATCH_MP_TAC BETWEEN_IMP_COLLINEAR THEN ASM_REWRITE_TAC[]];
1006 REWRITE_TAC[IN_BALL; IN_INTER; IN_ELIM_THM; dist] THEN
1007 REWRITE_TAC[NORM_ARITH `norm(x - (x + a):real^N) = norm a`] THEN
1008 REWRITE_TAC[VECTOR_ARITH `(x + a) - x:real^N = a`] THEN CONJ_TAC THENL
1009 [ASM_SIMP_TAC[NORM_MUL; GSYM REAL_LT_RDIV_EQ; NORM_POS_LT;
1011 MATCH_MP_TAC(REAL_ARITH
1012 `&0 < x /\ x < e ==> abs(min (&1 / &2) x) < e`) THEN
1013 ASM_SIMP_TAC[REAL_LT_DIV; REAL_HALF; NORM_POS_LT; VECTOR_SUB_EQ;
1014 REAL_LT_DIV2_EQ] THEN ASM_REAL_ARITH_TAC;
1015 REWRITE_TAC[DOT_RMUL; REAL_ARITH `x * y < &0 <=> &0 < x * --y`] THEN
1016 MATCH_MP_TAC REAL_LT_MUL THEN ASM_REWRITE_TAC[REAL_LT_MIN] THEN
1017 ASM_REWRITE_TAC[REAL_ARITH `&0 < --x <=> x < &0`] THEN
1018 ASM_SIMP_TAC[REAL_LT_DIV; REAL_HALF; NORM_POS_LT; VECTOR_SUB_EQ;
1020 REWRITE_TAC[IN_BALL; IN_INTER; IN_ELIM_THM] THEN
1021 ONCE_REWRITE_TAC[DIST_SYM] THEN ASM_REWRITE_TAC[]]]]);;
1023 (* ------------------------------------------------------------------------- *)
1024 (* Polygonal path; 0 in the empty case is just for linear invariance. *)
1025 (* Note that we *are* forced to assume non-emptiness for translation. *)
1026 (* ------------------------------------------------------------------------- *)
1028 let polygonal_path = define
1029 `polygonal_path[] = linepath(vec 0,vec 0) /\
1030 polygonal_path[a] = linepath(a,a) /\
1031 polygonal_path [a;b] = linepath(a,b) /\
1032 polygonal_path (CONS a (CONS b (CONS c l))) =
1033 linepath(a,b) ++ polygonal_path(CONS b (CONS c l))`;;
1035 let POLYGONAL_PATH_CONS_CONS = prove
1037 ==> polygonal_path(CONS a (CONS b p)) =
1038 linepath(a,b) ++ polygonal_path(CONS b p)`,
1039 GEN_TAC THEN GEN_TAC THEN LIST_INDUCT_TAC THEN
1040 REWRITE_TAC[polygonal_path]);;
1042 let POLYGONAL_PATH_TRANSLATION = prove
1043 (`!a b p. polygonal_path (MAP (\x. a + x) (CONS b p)) =
1044 (\x. a + x) o (polygonal_path (CONS b p))`,
1045 GEN_TAC THEN ONCE_REWRITE_TAC[SWAP_FORALL_THM] THEN
1046 MATCH_MP_TAC list_INDUCT THEN
1047 REWRITE_TAC[MAP; polygonal_path; LINEPATH_TRANSLATION] THEN
1048 ONCE_REWRITE_TAC[SWAP_FORALL_THM] THEN
1049 MATCH_MP_TAC list_INDUCT THEN
1050 ASM_SIMP_TAC[MAP; polygonal_path; LINEPATH_TRANSLATION] THEN
1051 REWRITE_TAC[JOINPATHS_TRANSLATION]);;
1053 add_translation_invariants [POLYGONAL_PATH_TRANSLATION];;
1055 let POLYGONAL_PATH_LINEAR_IMAGE = prove
1056 (`!f p. linear f ==> polygonal_path (MAP f p) = f o polygonal_path p`,
1057 REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN GEN_TAC THEN DISCH_TAC THEN
1058 MATCH_MP_TAC list_INDUCT THEN
1059 REWRITE_TAC[polygonal_path; MAP] THEN CONJ_TAC THENL
1060 [REWRITE_TAC[LINEPATH_REFL; o_DEF; FUN_EQ_THM] THEN ASM_MESON_TAC[LINEAR_0];
1061 ONCE_REWRITE_TAC[SWAP_FORALL_THM]] THEN
1062 MATCH_MP_TAC list_INDUCT THEN REWRITE_TAC[polygonal_path; MAP] THEN
1064 [ASM_MESON_TAC[LINEPATH_LINEAR_IMAGE];
1065 ONCE_REWRITE_TAC[SWAP_FORALL_THM]] THEN
1066 MATCH_MP_TAC list_INDUCT THEN REWRITE_TAC[polygonal_path; MAP] THEN
1067 ASM_SIMP_TAC[GSYM JOINPATHS_LINEAR_IMAGE; GSYM LINEPATH_LINEAR_IMAGE]);;
1069 add_linear_invariants [POLYGONAL_PATH_LINEAR_IMAGE];;
1071 let PATHSTART_POLYGONAL_PATH = prove
1072 (`!p. pathstart(polygonal_path p) = if p = [] then vec 0 else HD p`,
1073 MATCH_MP_TAC list_INDUCT THEN
1074 REWRITE_TAC[polygonal_path; PATHSTART_LINEPATH] THEN
1075 GEN_TAC THEN MATCH_MP_TAC list_INDUCT THEN
1076 REWRITE_TAC[polygonal_path; PATHSTART_LINEPATH; NOT_CONS_NIL; HD] THEN
1077 GEN_TAC THEN MATCH_MP_TAC list_INDUCT THEN
1078 REWRITE_TAC[polygonal_path; PATHSTART_LINEPATH; HD; PATHSTART_JOIN]);;
1080 let PATHFINISH_POLYGONAL_PATH = prove
1081 (`!p. pathfinish(polygonal_path p) = if p = [] then vec 0 else LAST p`,
1082 MATCH_MP_TAC list_INDUCT THEN
1083 REWRITE_TAC[polygonal_path; PATHFINISH_LINEPATH] THEN
1084 GEN_TAC THEN MATCH_MP_TAC list_INDUCT THEN
1085 REWRITE_TAC[polygonal_path; PATHFINISH_LINEPATH; NOT_CONS_NIL; LAST] THEN
1086 GEN_TAC THEN MATCH_MP_TAC list_INDUCT THEN
1087 REWRITE_TAC[polygonal_path; PATHFINISH_LINEPATH; PATHFINISH_JOIN]);;
1089 let VERTICES_IN_PATH_IMAGE_POLYGONAL_PATH = prove
1090 (`!p:(real^N)list. set_of_list p SUBSET path_image (polygonal_path p)`,
1091 MATCH_MP_TAC list_INDUCT THEN REWRITE_TAC[set_of_list; EMPTY_SUBSET] THEN
1092 GEN_TAC THEN MATCH_MP_TAC list_INDUCT THEN
1093 REWRITE_TAC[set_of_list; polygonal_path; PATH_IMAGE_LINEPATH] THEN
1094 REWRITE_TAC[SEGMENT_REFL; INSERT_AC; SUBSET_REFL] THEN
1095 GEN_TAC THEN MATCH_MP_TAC list_INDUCT THEN
1096 REWRITE_TAC[set_of_list; polygonal_path] THEN CONJ_TAC THENL
1097 [REWRITE_TAC[PATH_IMAGE_LINEPATH; INSERT_SUBSET; ENDS_IN_SEGMENT] THEN
1098 REWRITE_TAC[EMPTY_SUBSET];
1099 REPEAT GEN_TAC THEN REPLICATE_TAC 3 DISCH_TAC THEN
1100 ONCE_REWRITE_TAC[INSERT_SUBSET] THEN
1101 SIMP_TAC[PATH_IMAGE_JOIN; PATHFINISH_LINEPATH; PATHSTART_POLYGONAL_PATH;
1102 HD; NOT_CONS_NIL; IN_UNION; ENDS_IN_SEGMENT; PATH_IMAGE_LINEPATH] THEN
1105 let ARC_POLYGONAL_PATH_IMP_DISTINCT = prove
1106 (`!p:(real^N)list. arc(polygonal_path p) ==> PAIRWISE (\x y. ~(x = y)) p`,
1107 MATCH_MP_TAC list_INDUCT THEN
1108 REWRITE_TAC[polygonal_path; ARC_LINEPATH_EQ] THEN
1109 X_GEN_TAC `a:real^N` THEN MATCH_MP_TAC list_INDUCT THEN
1110 REWRITE_TAC[polygonal_path; ARC_LINEPATH_EQ] THEN
1111 X_GEN_TAC `b:real^N` THEN
1112 MATCH_MP_TAC list_INDUCT THEN
1113 REWRITE_TAC[polygonal_path; ARC_LINEPATH_EQ] THEN CONJ_TAC THENL
1114 [REWRITE_TAC[PAIRWISE; ALL]; ALL_TAC] THEN
1115 MAP_EVERY X_GEN_TAC [`c:real^N`; `p:(real^N)list`] THEN
1116 REPLICATE_TAC 3 DISCH_TAC THEN
1117 SIMP_TAC[ARC_JOIN_EQ; PATHFINISH_LINEPATH; PATHSTART_POLYGONAL_PATH;
1118 HD; NOT_CONS_NIL; ARC_LINEPATH_EQ] THEN
1119 STRIP_TAC THEN ONCE_REWRITE_TAC[PAIRWISE] THEN
1120 ASM_SIMP_TAC[] THEN REWRITE_TAC[ALL] THEN
1121 FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [SUBSET]) THEN
1122 DISCH_THEN(MP_TAC o SPEC `a:real^N`) THEN
1123 ASM_REWRITE_TAC[IN_INTER; IN_SING; ENDS_IN_SEGMENT; PATH_IMAGE_LINEPATH] THEN
1124 DISCH_THEN(MP_TAC o MATCH_MP (ONCE_REWRITE_RULE[GSYM CONTRAPOS_THM]
1125 (REWRITE_RULE[SUBSET] VERTICES_IN_PATH_IMAGE_POLYGONAL_PATH))) THEN
1126 ASM_REWRITE_TAC[IN_SET_OF_LIST; MEM; DE_MORGAN_THM; GSYM ALL_MEM] THEN
1129 let PATH_POLYGONAL_PATH = prove
1130 (`!p:(real^N)list. path(polygonal_path p)`,
1131 MATCH_MP_TAC list_INDUCT THEN
1132 REWRITE_TAC[polygonal_path; PATH_LINEPATH] THEN
1133 GEN_TAC THEN MATCH_MP_TAC list_INDUCT THEN
1134 REWRITE_TAC[polygonal_path; PATH_LINEPATH] THEN
1135 GEN_TAC THEN MATCH_MP_TAC list_INDUCT THEN
1136 REWRITE_TAC[polygonal_path; PATH_LINEPATH] THEN
1137 SIMP_TAC[PATH_JOIN; PATHFINISH_LINEPATH; PATHSTART_POLYGONAL_PATH;
1138 NOT_CONS_NIL; HD; PATH_LINEPATH]);;
1140 let PATH_IMAGE_POLYGONAL_PATH_SUBSET_CONVEX_HULL = prove
1142 ==> path_image(polygonal_path p) SUBSET convex hull (set_of_list p)`,
1143 MATCH_MP_TAC list_INDUCT THEN REWRITE_TAC[] THEN GEN_TAC THEN
1144 MATCH_MP_TAC list_INDUCT THEN REWRITE_TAC[NOT_CONS_NIL] THEN CONJ_TAC THENL
1145 [REWRITE_TAC[polygonal_path; PATH_IMAGE_LINEPATH; set_of_list] THEN
1146 REWRITE_TAC[SEGMENT_REFL; CONVEX_HULL_SING] THEN SET_TAC[];
1147 GEN_TAC THEN MATCH_MP_TAC list_INDUCT THEN
1148 REWRITE_TAC[polygonal_path] THEN CONJ_TAC THENL
1149 [REWRITE_TAC[polygonal_path; PATH_IMAGE_LINEPATH; set_of_list] THEN
1150 REWRITE_TAC[SEGMENT_CONVEX_HULL; SUBSET_REFL];
1151 REPEAT STRIP_TAC THEN MATCH_MP_TAC SUBSET_PATH_IMAGE_JOIN THEN
1152 REWRITE_TAC[PATH_IMAGE_LINEPATH; SEGMENT_CONVEX_HULL; set_of_list] THEN
1153 SIMP_TAC[HULL_MONO; INSERT_SUBSET; EMPTY_SUBSET; IN_INSERT] THEN
1154 FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP
1155 (REWRITE_RULE[IMP_CONJ] SUBSET_TRANS)) THEN
1156 MATCH_MP_TAC HULL_MONO THEN REWRITE_TAC[set_of_list] THEN
1159 let PATH_IMAGE_POLYGONAL_PATH_SUBSET_SEGMENTS = prove
1161 arc(polygonal_path p) /\ 3 <= LENGTH p /\
1162 x IN path_image(polygonal_path p)
1163 ==> ?a b. MEM a p /\ MEM b p /\ x IN segment[a,b] /\
1164 segment[a,b] SUBSET path_image(polygonal_path p) /\
1165 ~(pathstart(polygonal_path p) IN segment[a,b] /\
1166 pathfinish(polygonal_path p) IN segment[a,b])`,
1167 MATCH_MP_TAC list_INDUCT THEN REWRITE_TAC[LENGTH; ARITH] THEN
1168 X_GEN_TAC `a:real^N` THEN
1169 MATCH_MP_TAC list_INDUCT THEN REWRITE_TAC[LENGTH; ARITH] THEN
1170 X_GEN_TAC `b:real^N` THEN
1171 MATCH_MP_TAC list_INDUCT THEN REWRITE_TAC[LENGTH; ARITH] THEN
1172 X_GEN_TAC `c:real^N` THEN X_GEN_TAC `p:(real^N)list` THEN
1173 REPEAT DISCH_TAC THEN REWRITE_TAC[polygonal_path] THEN
1174 X_GEN_TAC `x:real^N` THEN
1175 REWRITE_TAC[PATHSTART_JOIN; PATHFINISH_JOIN] THEN
1176 SIMP_TAC[PATH_IMAGE_JOIN; PATHFINISH_LINEPATH; PATHSTART_POLYGONAL_PATH;
1177 ARC_JOIN_EQ; NOT_CONS_NIL; HD] THEN
1178 REWRITE_TAC[PATHSTART_LINEPATH; PATH_IMAGE_LINEPATH; ARC_LINEPATH] THEN
1179 REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
1180 GEN_REWRITE_TAC LAND_CONV [IN_UNION] THEN STRIP_TAC THENL
1181 [MAP_EVERY EXISTS_TAC [`a:real^N`; `b:real^N`] THEN
1182 ASM_REWRITE_TAC[MEM; SUBSET_UNION; ENDS_IN_SEGMENT] THEN
1183 FIRST_X_ASSUM(CONJUNCTS_THEN MP_TAC) THEN
1184 DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
1185 DISCH_THEN(MP_TAC o MATCH_MP ARC_DISTINCT_ENDS) THEN
1186 REWRITE_TAC[PATHSTART_POLYGONAL_PATH; HD; NOT_CONS_NIL] THEN
1187 DISCH_TAC THEN REWRITE_TAC[ARC_LINEPATH_EQ] THEN DISCH_TAC THEN
1188 MATCH_MP_TAC(SET_RULE
1189 `!p b. (s INTER p) SUBSET {b} /\
1190 x IN p /\ b IN s /\ ~(x = b)
1191 ==> ~(x IN s)`) THEN
1192 MAP_EVERY EXISTS_TAC
1193 [`path_image(polygonal_path (CONS (b:real^N) (CONS c p)))`;
1195 ASM_REWRITE_TAC[ENDS_IN_SEGMENT; PATHFINISH_IN_PATH_IMAGE];
1196 FIRST_X_ASSUM(MP_TAC o SPEC `x:real^N`) THEN
1197 ASM_REWRITE_TAC[ARITH_RULE `3 <= SUC(SUC p) <=> ~(p = 0)`] THEN
1198 REWRITE_TAC[LENGTH_EQ_NIL] THEN ASM_CASES_TAC `p:(real^N)list = []` THENL
1199 [ASM_REWRITE_TAC[LENGTH; polygonal_path] THEN
1200 REWRITE_TAC[PATHFINISH_LINEPATH; PATH_IMAGE_LINEPATH] THEN
1202 `x IN path_image(polygonal_path (CONS (b:real^N) (CONS c p)))` THEN
1203 ASM_REWRITE_TAC[polygonal_path; PATH_IMAGE_LINEPATH] THEN
1204 DISCH_TAC THEN MAP_EVERY EXISTS_TAC [`b:real^N`; `c:real^N`] THEN
1205 ASM_REWRITE_TAC[MEM; SUBSET_UNION; ENDS_IN_SEGMENT] THEN
1206 FIRST_X_ASSUM(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
1207 ASM_REWRITE_TAC[polygonal_path; PATH_IMAGE_LINEPATH] THEN
1208 REWRITE_TAC[ARC_LINEPATH_EQ] THEN
1209 MP_TAC(ISPECL [`a:real^N`; `b:real^N`] ENDS_IN_SEGMENT) THEN
1210 FIRST_ASSUM(MP_TAC o MATCH_MP ARC_DISTINCT_ENDS) THEN
1211 REWRITE_TAC[PATHSTART_LINEPATH; PATHFINISH_LINEPATH] THEN SET_TAC[];
1212 ASM_REWRITE_TAC[LENGTH_EQ_NIL] THEN
1213 MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `d:real^N` THEN
1214 MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `e:real^N` THEN
1215 REWRITE_TAC[PATHSTART_POLYGONAL_PATH; NOT_CONS_NIL; HD] THEN
1216 REPEAT STRIP_TAC THENL
1217 [ASM_MESON_TAC[MEM];
1221 FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (SET_RULE
1222 `(sab INTER p) SUBSET {b}
1223 ==> !sde a. sde SUBSET p /\
1224 ~(b IN sde) /\ d IN sde /\ a IN sde /\ a IN sab
1225 ==> F`) o el 2 o CONJUNCTS) THEN
1226 MAP_EVERY EXISTS_TAC [`segment[d:real^N,e]`; `a:real^N`] THEN
1227 ASM_REWRITE_TAC[ENDS_IN_SEGMENT] THEN ASM_MESON_TAC[]]]]);;
1229 (* ------------------------------------------------------------------------- *)
1230 (* Rotating the starting point to move a preferred vertex forward. *)
1231 (* ------------------------------------------------------------------------- *)
1233 let SET_OF_LIST_POLYGONAL_PATH_ROTATE = prove
1234 (`!p. ~(p = []) ==> set_of_list(CONS (LAST p) (BUTLAST p)) = set_of_list p`,
1235 REPEAT STRIP_TAC THEN
1236 FIRST_X_ASSUM(fun th -> GEN_REWRITE_TAC (RAND_CONV o RAND_CONV)
1237 [GSYM(MATCH_MP APPEND_BUTLAST_LAST th)]) THEN
1238 REWRITE_TAC[SET_OF_LIST_APPEND; set_of_list] THEN SET_TAC[]);;
1240 let PROPERTIES_POLYGONAL_PATH_SNOC = prove
1243 ==> path_image(polygonal_path(APPEND p [d])) =
1244 path_image(polygonal_path p ++ linepath(LAST p,d)) /\
1245 (arc(polygonal_path(APPEND p [d])) <=>
1246 arc(polygonal_path p ++ linepath(LAST p,d))) /\
1247 (simple_path(polygonal_path(APPEND p [d])) <=>
1248 simple_path(polygonal_path p ++ linepath(LAST p,d)))`,
1249 MATCH_MP_TAC list_INDUCT THEN REWRITE_TAC[LENGTH; ARITH] THEN
1250 X_GEN_TAC `a:real^N` THEN MATCH_MP_TAC list_INDUCT THEN
1251 REWRITE_TAC[LENGTH; ARITH] THEN X_GEN_TAC `b:real^N` THEN
1252 MATCH_MP_TAC list_INDUCT THEN CONJ_TAC THENL
1253 [REWRITE_TAC[APPEND; polygonal_path; LAST; NOT_CONS_NIL]; ALL_TAC] THEN
1254 MAP_EVERY X_GEN_TAC [`c:real^N`; `p:(real^N)list`] THEN REPEAT DISCH_TAC THEN
1255 X_GEN_TAC `d:real^N` THEN DISCH_TAC THEN REWRITE_TAC[APPEND] THEN
1256 ONCE_REWRITE_TAC[LAST] THEN REWRITE_TAC[NOT_CONS_NIL] THEN
1257 ONCE_REWRITE_TAC[polygonal_path] THEN
1258 FIRST_X_ASSUM(MP_TAC o SPEC `d:real^N`) THEN POP_ASSUM_LIST(K ALL_TAC) THEN
1259 REWRITE_TAC[APPEND; LENGTH; ARITH_RULE `2 <= SUC(SUC n)`] THEN
1260 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
1261 SIMP_TAC[GSYM ARC_ASSOC; GSYM SIMPLE_PATH_ASSOC; PATHSTART_JOIN;
1262 PATHFINISH_JOIN; PATHSTART_POLYGONAL_PATH;
1263 PATHFINISH_POLYGONAL_PATH;
1264 PATHSTART_LINEPATH; PATHFINISH_LINEPATH; NOT_CONS_NIL; HD] THEN
1265 DISCH_TAC THEN CONJ_TAC THENL
1266 [ASM_SIMP_TAC[PATH_IMAGE_JOIN; PATHSTART_JOIN; PATHFINISH_JOIN;
1267 PATHSTART_POLYGONAL_PATH; PATHFINISH_POLYGONAL_PATH;
1268 PATHSTART_LINEPATH; PATHFINISH_LINEPATH; NOT_CONS_NIL; HD] THEN
1269 REWRITE_TAC[UNION_ACI];
1271 ASM_CASES_TAC `a:real^N = d` THENL
1273 `(~p /\ ~p') /\ (q <=> q') ==> (p <=> p') /\ (q <=> q')`) THEN
1275 [REWRITE_TAC[ARC_SIMPLE_PATH; PATHSTART_JOIN; PATHFINISH_JOIN] THEN
1276 REWRITE_TAC[PATHSTART_LINEPATH; PATHFINISH_LINEPATH] THEN
1277 ASM_REWRITE_TAC[PATHFINISH_POLYGONAL_PATH; NOT_CONS_NIL; LAST;
1278 APPEND_EQ_NIL; LAST_APPEND];
1280 ASM_REWRITE_TAC[] THEN
1281 W(MP_TAC o PART_MATCH (lhs o rand) SIMPLE_PATH_JOIN_LOOP_EQ o
1284 [REWRITE_TAC[PATHSTART_POLYGONAL_PATH; PATHFINISH_LINEPATH] THEN
1285 REWRITE_TAC[PATHFINISH_POLYGONAL_PATH; PATHSTART_LINEPATH] THEN
1286 REWRITE_TAC[NOT_CONS_NIL; HD; LAST; LAST_APPEND; APPEND_EQ_NIL];
1287 DISCH_THEN SUBST1_TAC] THEN
1288 W(MP_TAC o PART_MATCH (lhs o rand) SIMPLE_PATH_JOIN_LOOP_EQ o
1291 [REWRITE_TAC[PATHSTART_JOIN; PATHFINISH_JOIN; PATHSTART_LINEPATH;
1292 PATHFINISH_LINEPATH; PATHSTART_POLYGONAL_PATH;
1293 PATHFINISH_POLYGONAL_PATH] THEN
1294 REWRITE_TAC[NOT_CONS_NIL; HD; LAST; LAST_APPEND; APPEND_EQ_NIL];
1295 DISCH_THEN SUBST1_TAC] THEN
1296 ASM_REWRITE_TAC[] THEN
1297 REWRITE_TAC[PATHSTART_JOIN; PATHSTART_POLYGONAL_PATH; NOT_CONS_NIL; HD];
1299 `((q <=> p) /\ (q' <=> p')) /\ (p <=> p')
1300 ==> (p <=> p') /\ (q <=> q')`) THEN
1302 [CONJ_TAC THEN MATCH_MP_TAC SIMPLE_PATH_EQ_ARC THEN
1303 REWRITE_TAC[PATHSTART_JOIN; PATHFINISH_JOIN; PATHSTART_LINEPATH;
1304 PATHFINISH_LINEPATH; PATHSTART_POLYGONAL_PATH;
1305 PATHFINISH_POLYGONAL_PATH] THEN
1306 ASM_REWRITE_TAC[NOT_CONS_NIL; HD; LAST; LAST_APPEND; APPEND_EQ_NIL];
1308 W(MP_TAC o PART_MATCH (lhs o rand) ARC_JOIN_EQ o lhs o snd) THEN
1310 [REWRITE_TAC[PATHSTART_POLYGONAL_PATH; PATHFINISH_LINEPATH] THEN
1311 REWRITE_TAC[NOT_CONS_NIL; HD];
1312 DISCH_THEN SUBST1_TAC] THEN
1313 W(MP_TAC o PART_MATCH (lhs o rand) ARC_JOIN_EQ o rhs o snd) THEN
1315 [SIMP_TAC[PATHSTART_POLYGONAL_PATH; PATHFINISH_LINEPATH; PATHSTART_JOIN;
1317 DISCH_THEN SUBST1_TAC] THEN
1318 ASM_REWRITE_TAC[] THEN
1319 REWRITE_TAC[PATHSTART_JOIN; PATHSTART_POLYGONAL_PATH; NOT_CONS_NIL; HD]]);;
1321 let PATH_IMAGE_POLYGONAL_PATH_ROTATE = prove
1323 2 <= LENGTH p /\ LAST p = HD p
1324 ==> path_image(polygonal_path(APPEND (TL p) [HD(TL p)])) =
1325 path_image(polygonal_path p)`,
1326 MATCH_MP_TAC list_INDUCT THEN REWRITE_TAC[LENGTH; ARITH] THEN
1327 X_GEN_TAC `a:real^N` THEN
1328 MATCH_MP_TAC list_INDUCT THEN REWRITE_TAC[LENGTH; ARITH] THEN
1329 X_GEN_TAC `b:real^N` THEN REWRITE_TAC[HD; TL] THEN
1330 MATCH_MP_TAC list_INDUCT THEN REWRITE_TAC[LENGTH; ARITH] THEN CONJ_TAC THENL
1331 [REWRITE_TAC[LAST; APPEND; NOT_CONS_NIL] THEN MESON_TAC[]; ALL_TAC] THEN
1332 MAP_EVERY X_GEN_TAC [`c:real^N`; `p:(real^N)list`] THEN
1333 REPLICATE_TAC 3 (DISCH_THEN(K ALL_TAC)) THEN
1334 DISCH_THEN(MP_TAC o CONJUNCT2) THEN
1335 REWRITE_TAC[LAST; NOT_CONS_NIL] THEN ONCE_REWRITE_TAC[GSYM LAST] THEN
1337 SIMP_TAC[PROPERTIES_POLYGONAL_PATH_SNOC; LENGTH;
1338 ARITH_RULE `2 <= SUC(SUC n)`] THEN
1339 ONCE_REWRITE_TAC[LAST] THEN ASM_REWRITE_TAC[NOT_CONS_NIL] THEN
1340 GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [polygonal_path] THEN
1341 RULE_ASSUM_TAC(REWRITE_RULE[LAST]) THEN
1342 ASM_SIMP_TAC[PATH_IMAGE_JOIN; PATHSTART_LINEPATH; PATHFINISH_LINEPATH;
1343 PATHSTART_POLYGONAL_PATH; PATHFINISH_POLYGONAL_PATH;
1344 LAST; NOT_CONS_NIL; HD] THEN
1345 REWRITE_TAC[UNION_ACI]);;
1347 let SIMPLE_PATH_POLYGONAL_PATH_ROTATE = prove
1349 2 <= LENGTH p /\ LAST p = HD p
1350 ==> (simple_path(polygonal_path(APPEND (TL p) [HD(TL p)])) =
1351 simple_path(polygonal_path p))`,
1352 MATCH_MP_TAC list_INDUCT THEN REWRITE_TAC[LENGTH; ARITH] THEN
1353 X_GEN_TAC `a:real^N` THEN
1354 MATCH_MP_TAC list_INDUCT THEN REWRITE_TAC[LENGTH; ARITH] THEN
1355 X_GEN_TAC `b:real^N` THEN REWRITE_TAC[HD; TL] THEN
1356 MATCH_MP_TAC list_INDUCT THEN REWRITE_TAC[LENGTH; ARITH] THEN CONJ_TAC THENL
1357 [REWRITE_TAC[LAST; APPEND; NOT_CONS_NIL] THEN MESON_TAC[]; ALL_TAC] THEN
1358 MAP_EVERY X_GEN_TAC [`c:real^N`; `p:(real^N)list`] THEN
1359 REPLICATE_TAC 3 (DISCH_THEN(K ALL_TAC)) THEN
1360 DISCH_THEN(MP_TAC o CONJUNCT2) THEN
1361 REWRITE_TAC[LAST; NOT_CONS_NIL] THEN ONCE_REWRITE_TAC[GSYM LAST] THEN
1363 SIMP_TAC[PROPERTIES_POLYGONAL_PATH_SNOC; LENGTH;
1364 ARITH_RULE `2 <= SUC(SUC n)`] THEN
1365 ONCE_REWRITE_TAC[LAST] THEN ASM_REWRITE_TAC[NOT_CONS_NIL] THEN
1366 GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [polygonal_path] THEN
1367 RULE_ASSUM_TAC(REWRITE_RULE[LAST]) THEN
1368 ASM_SIMP_TAC[SIMPLE_PATH_JOIN_LOOP_EQ; PATHSTART_LINEPATH;
1369 PATHFINISH_LINEPATH; PATHSTART_POLYGONAL_PATH;
1370 PATHFINISH_POLYGONAL_PATH; LAST; NOT_CONS_NIL; HD] THEN
1371 REWRITE_TAC[INSERT_AC; INTER_ACI; CONJ_ACI]);;
1373 let ROTATE_LIST_TO_FRONT_1 = prove
1375 (!l. P(l) ==> 3 <= LENGTH l /\ LAST l = HD l) /\
1376 (!l. P(l) ==> P(APPEND (TL l) [HD(TL l)])) /\
1378 ==> ?l'. EL 1 l' = a /\ P l'`,
1380 (`!P. (!i. P i /\ 0 < i ==> P(i - 1)) /\ (?k. 0 < k /\ P k)
1382 REPEAT STRIP_TAC THEN
1383 SUBGOAL_THEN `!i:num. i < k ==> P(k - i)` MP_TAC THENL
1384 [INDUCT_TAC THEN ASM_REWRITE_TAC[SUB_0] THEN DISCH_TAC THEN
1385 REWRITE_TAC[ARITH_RULE `k - SUC i = k - i - 1`] THEN
1386 FIRST_X_ASSUM MATCH_MP_TAC THEN
1387 CONJ_TAC THEN TRY(FIRST_X_ASSUM MATCH_MP_TAC) THEN ASM_ARITH_TAC;
1388 DISCH_THEN(MP_TAC o SPEC `k - 1`) THEN
1389 ASM_SIMP_TAC[ARITH_RULE `0 < k ==> k - 1 < k /\ k - (k - 1) = 1`]]) in
1390 REPEAT STRIP_TAC THEN
1392 `?i l'. 0 < i /\ i < LENGTH l' /\ P l' /\ EL i l' = (a:A)`
1394 [SUBGOAL_THEN `~(l:A list = [])` ASSUME_TAC THENL
1395 [ASM_MESON_TAC[LENGTH; ARITH_RULE `~(3 <= 0)`]; ALL_TAC] THEN
1396 FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [MEM_EXISTS_EL]) THEN
1397 DISCH_THEN(X_CHOOSE_THEN `i:num` STRIP_ASSUME_TAC) THEN
1398 DISJ_CASES_THEN2 SUBST_ALL_TAC ASSUME_TAC (ARITH_RULE `i = 0 \/ 0 < i`)
1400 [EXISTS_TAC `LENGTH(l:A list) - 2` THEN
1401 EXISTS_TAC `(APPEND (TL l) [HD(TL l):A])` THEN
1402 ASM_SIMP_TAC[LENGTH_APPEND; LENGTH_TL; EL_APPEND] THEN
1403 REWRITE_TAC[LT_REFL; LENGTH; SUB_REFL; EL; HD] THEN
1404 SUBGOAL_THEN `3 <= LENGTH(l:A list)` ASSUME_TAC THENL
1405 [ASM_MESON_TAC[]; ALL_TAC] THEN
1406 REPLICATE_TAC 2 (CONJ_TAC THENL [ASM_ARITH_TAC; ALL_TAC]) THEN
1407 ASM_SIMP_TAC[ARITH_RULE `3 <= n ==> n - 2 < n - 1`] THEN
1408 ASM_SIMP_TAC[EL_TL; ARITH_RULE `3 <= n ==> n - 2 + 1 = n - 1`] THEN
1409 ASM_MESON_TAC[LAST_EL];
1410 MAP_EVERY EXISTS_TAC [`i:num`; `l:A list`] THEN ASM_REWRITE_TAC[]];
1411 REWRITE_TAC[RIGHT_EXISTS_AND_THM] THEN
1412 DISCH_THEN(MP_TAC o MATCH_MP (ONCE_REWRITE_RULE[IMP_CONJ_ALT] lemma0)) THEN
1413 ANTS_TAC THENL [ALL_TAC; MESON_TAC[]] THEN X_GEN_TAC `k:num` THEN
1414 DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
1415 DISCH_THEN(X_CHOOSE_THEN `m:A list` STRIP_ASSUME_TAC) THEN
1416 EXISTS_TAC `APPEND (TL m) [HD(TL m):A]` THEN
1417 SUBGOAL_THEN `~(m:A list = [])` ASSUME_TAC THENL
1418 [ASM_MESON_TAC[LENGTH; ARITH_RULE `~(3 <= 0)`]; ALL_TAC] THEN
1419 ASM_SIMP_TAC[LENGTH_APPEND; LENGTH_TL; EL_APPEND] THEN
1420 ASM_REWRITE_TAC[LENGTH] THEN CONJ_TAC THENL [ASM_ARITH_TAC; ALL_TAC] THEN
1421 COND_CASES_TAC THENL [ALL_TAC; ASM_ARITH_TAC] THEN
1422 ASM_SIMP_TAC[EL_TL; ARITH_RULE `0 < k ==> k - 1 + 1 = k`]]);;
1424 let ROTATE_LIST_TO_FRONT_0 = prove
1426 (!l. P(l) ==> 3 <= LENGTH l /\ LAST l = HD l) /\
1427 (!l. P(l) ==> P(APPEND (TL l) [HD(TL l)])) /\
1429 ==> ?l'. HD l' = a /\ P l'`,
1430 REPEAT STRIP_TAC THEN
1431 MP_TAC(ISPECL [`P:A list->bool`; `l:A list`; `a:A`]
1432 ROTATE_LIST_TO_FRONT_1) THEN
1433 ASM_REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN X_GEN_TAC `l':A list` THEN
1434 STRIP_TAC THEN EXISTS_TAC `APPEND (TL l') [HD(TL l'):A]` THEN
1435 ASM_SIMP_TAC[] THEN UNDISCH_TAC `EL 1 l' = (a:A)` THEN
1436 SUBGOAL_THEN `3 <= LENGTH(l':A list)` MP_TAC THENL
1437 [ASM_MESON_TAC[]; ALL_TAC] THEN
1438 SPEC_TAC(`l':A list`,`p:A list`) THEN
1439 MATCH_MP_TAC list_INDUCT THEN REWRITE_TAC[LENGTH; ARITH] THEN
1440 GEN_TAC THEN MATCH_MP_TAC list_INDUCT THEN REWRITE_TAC[LENGTH; ARITH] THEN
1441 REWRITE_TAC[APPEND; HD; TL; num_CONV `1`; EL]);;
1443 (* ------------------------------------------------------------------------- *)
1444 (* We can pick a transformation to make all y coordinates distinct. *)
1445 (* ------------------------------------------------------------------------- *)
1447 let DISTINGUISHING_ROTATION_EXISTS_PAIR = prove
1449 ==> FINITE {t | &0 <= t /\ t < &2 * pi /\
1450 (rotate2d t x)$2 = (rotate2d t y)$2}`,
1451 REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[GSYM REAL_SUB_0] THEN
1452 ONCE_REWRITE_TAC[GSYM VECTOR_SUB_COMPONENT] THEN
1453 ONCE_REWRITE_TAC[GSYM ROTATE2D_SUB] THEN
1454 REWRITE_TAC[GSYM IM_DEF; GSYM real; GSYM ARG_EQ_0_PI] THEN
1455 REWRITE_TAC[FINITE_UNION; SET_RULE
1456 `{x | p x /\ q x /\ (r x \/ s x)} =
1457 {x | p x /\ q x /\ r x} UNION {x | p x /\ q x /\ s x}`] THEN
1459 MATCH_MP_TAC(MESON[FINITE_SING; FINITE_SUBSET]
1460 `(?a. s SUBSET {a}) ==> FINITE s`) THEN
1461 MATCH_MP_TAC(SET_RULE
1462 `(!x y. x IN s /\ y IN s ==> x = y) ==> ?a. s SUBSET {a}`) THEN
1463 REWRITE_TAC[IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN
1464 MATCH_MP_TAC ARG_ROTATE2D_UNIQUE_2PI THEN EXISTS_TAC `x - y:complex` THEN
1465 ASM_REWRITE_TAC[COMPLEX_SUB_0]);;
1467 let DISTINGUISHING_ROTATION_EXISTS = prove
1468 (`!s. FINITE s ==> ?t. pairwise (\x y. ~(x$2 = y$2)) (IMAGE (rotate2d t) s)`,
1469 REPEAT STRIP_TAC THEN
1471 `INFINITE ({t | &0 <= t /\ t < &2 * pi} DIFF
1472 UNIONS (IMAGE (\(x,y). {t | &0 <= t /\ t < &2 * pi /\
1473 (rotate2d t x)$2 = (rotate2d t y)$2})
1474 ({(x,y) | x IN s /\ y IN s /\ ~(x = y)})))`
1476 [MATCH_MP_TAC INFINITE_DIFF_FINITE THEN
1477 REWRITE_TAC[INFINITE; FINITE_REAL_INTERVAL; REAL_NOT_LE] THEN
1478 CONJ_TAC THENL [MP_TAC PI_POS THEN REAL_ARITH_TAC; ALL_TAC] THEN
1479 REWRITE_TAC[FINITE_UNIONS] THEN CONJ_TAC THENL
1480 [MATCH_MP_TAC FINITE_IMAGE THEN MATCH_MP_TAC FINITE_SUBSET THEN
1481 EXISTS_TAC `{(x:real^2,y:real^2) | x IN s /\ y IN s}` THEN
1482 ASM_SIMP_TAC[FINITE_PRODUCT_DEPENDENT] THEN SET_TAC[];
1483 REWRITE_TAC[FORALL_IN_IMAGE; FORALL_IN_GSPEC] THEN
1484 ASM_SIMP_TAC[DISTINGUISHING_ROTATION_EXISTS_PAIR]];
1485 DISCH_THEN(MP_TAC o MATCH_MP (MESON[FINITE_EMPTY; INFINITE]
1486 `INFINITE s ==> ~(s = {})`)) THEN
1487 REWRITE_TAC[GSYM MEMBER_NOT_EMPTY; IN_DIFF; IN_ELIM_THM] THEN
1488 MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `t:real` THEN
1489 DISCH_THEN(CONJUNCTS_THEN2 STRIP_ASSUME_TAC MP_TAC) THEN
1490 REWRITE_TAC[UNIONS_IMAGE; EXISTS_IN_GSPEC] THEN
1491 REWRITE_TAC[pairwise; IN_ELIM_THM] THEN
1492 REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM; FORALL_IN_IMAGE] THEN
1493 ASM_REWRITE_TAC[ROTATE2D_EQ] THEN MESON_TAC[]]);;
1495 let DISTINGUISHING_ROTATION_EXISTS_POLYGON = prove
1497 ?f q. (?g. orthogonal_transformation g /\ f = MAP g) /\
1498 (!x y. MEM x q /\ MEM y q /\ ~(x = y) ==> ~(x$2 = y$2)) /\
1500 GEN_TAC THEN MP_TAC(ISPEC
1501 `set_of_list(p:(real^2)list)` DISTINGUISHING_ROTATION_EXISTS) THEN
1502 REWRITE_TAC[FINITE_SET_OF_LIST; pairwise] THEN
1503 REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM; FORALL_IN_IMAGE] THEN
1504 REWRITE_TAC[IN_SET_OF_LIST; ROTATE2D_EQ] THEN
1505 REWRITE_TAC[IMP_IMP; RIGHT_IMP_FORALL_THM; GSYM CONJ_ASSOC] THEN
1506 DISCH_THEN(X_CHOOSE_THEN `t:real` STRIP_ASSUME_TAC) THEN
1507 EXISTS_TAC `MAP (rotate2d(--t))` THEN
1508 EXISTS_TAC `MAP (rotate2d t) p` THEN
1509 REWRITE_TAC[GSYM MAP_o; o_DEF; GSYM ROTATE2D_ADD] THEN
1510 REWRITE_TAC[REAL_ADD_LINV; ROTATE2D_ZERO; MAP_ID] THEN
1511 CONJ_TAC THENL [MESON_TAC[ORTHOGONAL_TRANSFORMATION_ROTATE2D]; ALL_TAC] THEN
1512 REWRITE_TAC[GSYM IN_SET_OF_LIST; SET_OF_LIST_MAP] THEN
1513 REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM; FORALL_IN_IMAGE] THEN
1514 ASM_REWRITE_TAC[IN_SET_OF_LIST; ROTATE2D_EQ] THEN ASM_MESON_TAC[]);;
1516 (* ------------------------------------------------------------------------- *)
1517 (* Proof that we can chop a polygon's inside in two. *)
1518 (* ------------------------------------------------------------------------- *)
1520 let POLYGON_CHOP_IN_TWO = prove
1522 simple_path(polygonal_path p) /\
1523 pathfinish(polygonal_path p) = pathstart(polygonal_path p) /\
1525 ==> ?a b. ~(a = b) /\ MEM a p /\ MEM b p /\
1526 segment(a,b) SUBSET inside(path_image(polygonal_path p))`,
1527 let wlog_lemma = MESON[]
1528 `(!x. ?f:A->A y. transform f /\ nice y /\ f y = x)
1529 ==> !P. (!f x. transform f ==> (P(f x) <=> P x)) /\
1530 (!x. nice x ==> P x)
1532 let between_lemma = prove
1533 (`!a c u v m:real^N.
1534 collinear {a,c,u,v,m} /\ m IN segment[u,v] /\ m IN segment(a,c)
1535 ==> u IN segment(a,c) \/ v IN segment(a,c) \/
1536 segment[a,c] SUBSET segment[u,v]`,
1538 ONCE_REWRITE_TAC[IMP_CONJ] THEN REWRITE_TAC[COLLINEAR_AFFINE_HULL] THEN
1539 REWRITE_TAC[INSERT_SUBSET; LEFT_IMP_EXISTS_THM; EMPTY_SUBSET] THEN
1540 MAP_EVERY X_GEN_TAC [`origin:real^N`; `dir:real^N`] THEN
1541 GEOM_ORIGIN_TAC `origin:real^N` THEN
1542 REWRITE_TAC[AFFINE_HULL_2; VECTOR_MUL_RZERO; VECTOR_ADD_LID] THEN
1543 REWRITE_TAC[IN_ELIM_THM] THEN REPEAT GEN_TAC THEN STRIP_TAC THEN
1544 ASM_REWRITE_TAC[] THEN ASM_CASES_TAC `dir:real^N = vec 0` THENL
1545 [ASM_REWRITE_TAC[VECTOR_MUL_RZERO; SEGMENT_REFL; SUBSET_REFL];
1547 REWRITE_TAC[SUBSET_SEGMENT] THEN
1548 ASM_SIMP_TAC[SEGMENT_SCALAR_MULTIPLE; IN_ELIM_THM] THEN
1549 ASM_REWRITE_TAC[VECTOR_MUL_RCANCEL] THEN
1550 REWRITE_TAC[ONCE_REWRITE_RULE[CONJ_SYM] UNWIND_THM1] THEN
1552 MATCH_MP_TAC(MATCH_MP wlog_lemma DISTINGUISHING_ROTATION_EXISTS_POLYGON) THEN
1554 [REWRITE_TAC[MESON[] `(!x y. (?z. P z /\ x = f z) ==> Q x y) <=>
1555 (!z y. P z ==> Q (f z) y)`] THEN
1556 REWRITE_TAC[ORTHOGONAL_TRANSFORMATION] THEN
1557 GEOM_TRANSFORM_TAC [];
1559 X_GEN_TAC `q:(real^2)list` THEN DISCH_TAC THEN STRIP_TAC THEN
1561 `?b:real^2. MEM b q /\ !d. MEM d q ==> b$2 <= d$2`
1562 STRIP_ASSUME_TAC THENL
1563 [MP_TAC(ISPEC `IMAGE (\x:real^2. x$2) (set_of_list q)`
1565 SIMP_TAC[FINITE_SET_OF_LIST; FINITE_IMAGE] THEN
1566 REWRITE_TAC[IMAGE_EQ_EMPTY; SET_OF_LIST_EQ_EMPTY] THEN
1567 UNDISCH_TAC `5 <= LENGTH(q:(real^2)list)` THEN
1568 ASM_CASES_TAC `q:(real^2)list = []` THEN
1569 ASM_REWRITE_TAC[LENGTH; ARITH; FORALL_IN_IMAGE] THEN DISCH_TAC THEN
1570 REWRITE_TAC[IN_IMAGE; LEFT_AND_EXISTS_THM; IN_SET_OF_LIST] THEN
1571 MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `b:real^2` THEN
1572 DISCH_THEN(CONJUNCTS_THEN2 STRIP_ASSUME_TAC MP_TAC) THEN
1577 EL 1 p = b /\ LAST p = HD p /\
1578 LENGTH p = LENGTH q /\ set_of_list p = set_of_list q /\
1579 path_image(polygonal_path p) = path_image(polygonal_path q) /\
1580 simple_path(polygonal_path p) /\
1581 pathfinish(polygonal_path p) = pathstart(polygonal_path p)`
1583 [MATCH_MP_TAC ROTATE_LIST_TO_FRONT_1 THEN EXISTS_TAC `q:(real^2)list` THEN
1584 ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
1585 [REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN ASM_ARITH_TAC; ALL_TAC] THEN
1586 MAP_EVERY UNDISCH_TAC
1587 [`pathfinish(polygonal_path(q:(real^2)list)) =
1588 pathstart(polygonal_path q)`;
1589 `5 <= LENGTH(q:(real^2)list)`] THEN
1590 ASM_CASES_TAC `q:(real^2)list = []` THEN
1591 ASM_REWRITE_TAC[LENGTH; ARITH] THEN
1592 ASM_REWRITE_TAC[PATHSTART_POLYGONAL_PATH; PATHFINISH_POLYGONAL_PATH] THEN
1593 DISCH_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
1594 X_GEN_TAC `l:(real^2)list` THEN
1595 REWRITE_TAC[APPEND_EQ_NIL; NOT_CONS_NIL] THEN
1596 ASM_CASES_TAC `l:(real^2)list = []` THENL
1597 [ASM_MESON_TAC[LENGTH_EQ_NIL]; ALL_TAC] THEN
1598 ASM_REWRITE_TAC[] THEN DISCH_THEN(STRIP_ASSUME_TAC o GSYM) THEN
1599 ASM_REWRITE_TAC[] THEN
1600 SUBGOAL_THEN `~(TL l:(real^2)list = [])` ASSUME_TAC THENL
1601 [DISCH_THEN(MP_TAC o AP_TERM `LENGTH:(real^2)list->num`) THEN
1602 ASM_SIMP_TAC[LENGTH; LENGTH_TL] THEN ASM_ARITH_TAC;
1604 ASM_SIMP_TAC[LAST_APPEND; LENGTH_APPEND; LENGTH_TL; NOT_CONS_NIL] THEN
1605 ASM_REWRITE_TAC[LAST; HD_APPEND; LENGTH] THEN REPEAT CONJ_TAC THENL
1607 MAP_EVERY UNDISCH_TAC
1608 [`HD(l:(real^2)list) = LAST l`; `5 <= LENGTH(q:(real^2)list)`;
1609 `~(l:(real^2)list = [])`] THEN
1610 ASM_REWRITE_TAC[] THEN
1611 SPEC_TAC(`l:(real^2)list`,`l:(real^2)list`) THEN
1612 LIST_INDUCT_TAC THEN REWRITE_TAC[HD; TL; APPEND] THEN
1613 REWRITE_TAC[SET_OF_LIST_APPEND; set_of_list] THEN
1614 REPEAT STRIP_TAC THEN MATCH_MP_TAC(SET_RULE
1615 `a IN s /\ b IN s ==> s UNION {a} = b INSERT s`) THEN
1616 ASM_REWRITE_TAC[LAST] THEN ONCE_ASM_REWRITE_TAC[] THEN
1617 REWRITE_TAC[LAST] THEN UNDISCH_TAC `5 <= LENGTH(CONS (h:real^2) t)` THEN
1618 COND_CASES_TAC THEN ASM_REWRITE_TAC[LENGTH; ARITH] THEN
1619 REWRITE_TAC[IN_SET_OF_LIST; MEM_EXISTS_EL; LENGTH] THEN
1620 DISCH_TAC THEN CONJ_TAC THENL
1621 [EXISTS_TAC `0` THEN REWRITE_TAC[EL] THEN ASM_ARITH_TAC;
1622 EXISTS_TAC `LENGTH(t:(real^2)list) - 1` THEN
1623 ASM_SIMP_TAC[LAST_EL] THEN ASM_ARITH_TAC];
1624 MATCH_MP_TAC PATH_IMAGE_POLYGONAL_PATH_ROTATE THEN
1625 ASM_REWRITE_TAC[] THEN ASM_ARITH_TAC;
1626 MP_TAC(ISPEC `l:(real^2)list` SIMPLE_PATH_POLYGONAL_PATH_ROTATE) THEN
1627 ASM_REWRITE_TAC[] THEN DISCH_THEN MATCH_MP_TAC THEN ASM_ARITH_TAC];
1629 UNDISCH_THEN `pathfinish(polygonal_path(q:(real^2)list)) =
1630 pathstart(polygonal_path q)` (K ALL_TAC) THEN
1631 UNDISCH_THEN `simple_path(polygonal_path(q:(real^2)list))` (K ALL_TAC) THEN
1632 DISCH_THEN(X_CHOOSE_THEN `r:(real^2)list` MP_TAC) THEN
1633 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
1634 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
1635 DISCH_THEN(CONJUNCTS_THEN2 (SUBST_ALL_TAC o SYM) MP_TAC) THEN
1636 GEN_REWRITE_TAC (LAND_CONV o LAND_CONV) [EXTENSION] THEN
1637 REWRITE_TAC[IN_SET_OF_LIST] THEN DISCH_THEN(CONJUNCTS_THEN2
1638 (fun th -> REWRITE_TAC[GSYM th] THEN
1639 RULE_ASSUM_TAC(REWRITE_RULE[GSYM th])) MP_TAC) THEN
1640 DISCH_THEN(CONJUNCTS_THEN2 (SUBST_ALL_TAC o SYM) STRIP_ASSUME_TAC) THEN
1641 UNDISCH_THEN `MEM (b:real^2) r` (K ALL_TAC) THEN
1642 POP_ASSUM_LIST(MP_TAC o end_itlist CONJ o rev) THEN
1643 SPEC_TAC(`r:(real^2)list`,`r:(real^2)list`) THEN
1644 MATCH_MP_TAC list_INDUCT THEN REWRITE_TAC[LENGTH; ARITH] THEN
1645 X_GEN_TAC `a:real^2` THEN
1646 MATCH_MP_TAC list_INDUCT THEN REWRITE_TAC[LENGTH; ARITH] THEN
1647 X_GEN_TAC `b':real^2` THEN
1648 MATCH_MP_TAC list_INDUCT THEN REWRITE_TAC[LENGTH; ARITH] THEN
1649 X_GEN_TAC `c:real^2` THEN X_GEN_TAC `p:(real^2)list` THEN
1650 REPLICATE_TAC 3 (DISCH_THEN(K ALL_TAC)) THEN
1651 REWRITE_TAC[num_CONV `1`; EL; HD; TL] THEN
1652 ASM_CASES_TAC `b':real^2 = b` THEN ASM_REWRITE_TAC[] THEN
1653 POP_ASSUM(K ALL_TAC) THEN
1654 REWRITE_TAC[ARITH_RULE `5 <= SUC(SUC(SUC n)) <=> ~(n = 0) /\ 2 <= n`] THEN
1655 ASM_CASES_TAC `p:(real^2)list = []` THEN ASM_REWRITE_TAC[LENGTH_EQ_NIL] THEN
1656 ASM_SIMP_TAC[POLYGONAL_PATH_CONS_CONS; LAST; NOT_CONS_NIL] THEN
1657 REWRITE_TAC[PATHSTART_JOIN; PATHSTART_LINEPATH] THEN
1658 REPLICATE_TAC 2 (DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
1659 FIRST_X_ASSUM(MP_TAC o SPEC `b:real^2`) THEN
1660 REWRITE_TAC[MESON[MEM] `MEM b (CONS a (CONS b l))`] THEN
1661 DISCH_THEN(ASSUME_TAC o GSYM) THEN STRIP_TAC THEN
1663 [`linepath(a:real^2,b)`;
1664 `polygonal_path(CONS (b:real^2) (CONS c p))`]
1665 SIMPLE_PATH_JOIN_IMP) THEN
1666 ASM_SIMP_TAC[POLYGONAL_PATH_CONS_CONS] THEN
1667 REWRITE_TAC[PATHFINISH_LINEPATH; PATHSTART_JOIN; PATHSTART_LINEPATH] THEN
1668 REWRITE_TAC[ARC_LINEPATH_EQ] THEN
1669 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
1670 DISCH_THEN(CONJUNCTS_THEN2 (fun th -> ASSUME_TAC th THEN MP_TAC th)
1672 SIMP_TAC[ARC_JOIN_EQ; PATHFINISH_LINEPATH; PATHSTART_POLYGONAL_PATH;
1673 NOT_CONS_NIL; HD] THEN
1674 REWRITE_TAC[ARC_LINEPATH_EQ; GSYM CONJ_ASSOC; PATH_IMAGE_LINEPATH] THEN
1675 SIMP_TAC[PATH_IMAGE_JOIN; PATHFINISH_LINEPATH; PATHSTART_POLYGONAL_PATH;
1676 HD; NOT_CONS_NIL] THEN
1677 REWRITE_TAC[SET_RULE `s INTER (t UNION u) SUBSET v <=>
1678 s INTER t SUBSET v /\ s INTER u SUBSET v`] THEN
1679 ASM_CASES_TAC `a:real^2 = c` THENL
1680 [DISCH_THEN(MP_TAC o CONJUNCT1) THEN
1681 ASM_REWRITE_TAC[PATH_IMAGE_LINEPATH; SEGMENT_SYM; INTER_ACI] THEN
1682 DISCH_THEN(MP_TAC o MATCH_MP (REWRITE_RULE [IMP_CONJ_ALT]
1683 FINITE_SUBSET)) THEN
1684 REWRITE_TAC[FINITE_SEGMENT; FINITE_INSERT; FINITE_EMPTY] THEN
1687 REWRITE_TAC[PATH_IMAGE_LINEPATH] THEN STRIP_TAC THEN STRIP_TAC THEN
1688 MP_TAC(ISPEC `CONS (b:real^2) (CONS c p)`
1689 ARC_POLYGONAL_PATH_IMP_DISTINCT) THEN
1690 ASM_SIMP_TAC[POLYGONAL_PATH_CONS_CONS] THEN
1691 REWRITE_TAC[PAIRWISE; ALL] THEN REWRITE_TAC[GSYM ALL_MEM] THEN
1692 REWRITE_TAC[MESON[] `(!x. P x ==> ~(a = x)) <=> ~(P a)`] THEN
1694 SUBGOAL_THEN `(b:real^2)$2 < (a:real^2)$2 /\
1695 (b:real^2)$2 < (c:real^2)$2 /\
1696 (!v. MEM v p ==> (b:real^2)$2 < (v:real^2)$2)`
1697 STRIP_ASSUME_TAC THENL
1698 [REPEAT STRIP_TAC THEN REWRITE_TAC[REAL_LT_LE] THEN
1699 CONV_TAC(ONCE_DEPTH_CONV SYM_CONV) THEN
1700 CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[MEM] THEN
1703 SUBGOAL_THEN `~collinear{a:real^2,b,c}` ASSUME_TAC THENL
1704 [REWRITE_TAC[COLLINEAR_BETWEEN_CASES; BETWEEN_IN_SEGMENT] THEN
1705 SUBGOAL_THEN `FINITE(segment[a:real^2,b] INTER segment[b,c])` MP_TAC THENL
1706 [MATCH_MP_TAC FINITE_SUBSET THEN
1707 EXISTS_TAC `{a:real^2,b}` THEN ASM_REWRITE_TAC[] THEN
1708 REWRITE_TAC[FINITE_INSERT; FINITE_EMPTY];
1710 ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN REWRITE_TAC[] THEN
1712 [SUBGOAL_THEN `segment[a:real^2,b] INTER segment[b,c] = segment[a,b]`
1713 (fun th -> ASM_REWRITE_TAC[FINITE_SEGMENT; th]) THEN
1714 REWRITE_TAC[SET_RULE `s INTER t = s <=> s SUBSET t`] THEN
1715 ASM_REWRITE_TAC[SUBSET_SEGMENT; ENDS_IN_SEGMENT];
1716 DISCH_TAC THEN UNDISCH_TAC `b IN segment[c:real^2,a]` THEN
1717 ASM_REWRITE_TAC[SEGMENT_CLOSED_OPEN; IN_UNION; IN_INSERT] THEN
1718 ASM_REWRITE_TAC[IN_SEGMENT; NOT_IN_EMPTY] THEN
1719 DISCH_THEN(X_CHOOSE_THEN `u:real` MP_TAC) THEN
1720 REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
1721 DISCH_THEN(MP_TAC o AP_TERM `\x:real^2. x$2`) THEN
1722 REWRITE_TAC[VECTOR_ADD_COMPONENT; VECTOR_MUL_COMPONENT] THEN
1723 MATCH_MP_TAC(REAL_ARITH
1724 `(&1 - u) * b < (&1 - u) * c /\ u * b < u * a
1725 ==> ~(b = (&1 - u) * c + u * a)`) THEN
1726 ASM_SIMP_TAC[REAL_LT_LMUL_EQ; REAL_SUB_LT];
1727 SUBGOAL_THEN `segment[a:real^2,b] INTER segment[b,c] = segment[b,c]`
1728 (fun th -> ASM_REWRITE_TAC[FINITE_SEGMENT; th]) THEN
1729 REWRITE_TAC[SET_RULE `s INTER t = t <=> t SUBSET s`] THEN
1730 ASM_REWRITE_TAC[SUBSET_SEGMENT; ENDS_IN_SEGMENT]];
1734 e <= (a:real^2)$2 - (b:real^2)$2 /\
1735 e <= (c:real^2)$2 - (b:real^2)$2 /\
1736 !v. MEM v p ==> e <= (v:real^2)$2 - (b:real^2)$2`
1737 STRIP_ASSUME_TAC THENL
1738 [MP_TAC(ISPEC `IMAGE (\v. (v:real^2)$2 - (b:real^2)$2)
1739 (set_of_list(CONS a (CONS b (CONS c p)))
1742 ASM_SIMP_TAC[FINITE_SET_OF_LIST; FINITE_IMAGE; FINITE_DELETE] THEN
1744 [REWRITE_TAC[IMAGE_EQ_EMPTY] THEN
1745 REWRITE_TAC[set_of_list; GSYM MEMBER_NOT_EMPTY] THEN
1746 EXISTS_TAC `a:real^2` THEN ASM_REWRITE_TAC[IN_DELETE; IN_INSERT];
1748 REWRITE_TAC[FORALL_IN_IMAGE] THEN REWRITE_TAC[IN_IMAGE] THEN
1749 ASM_REWRITE_TAC[set_of_list; FORALL_IN_INSERT; IMP_CONJ; IN_DELETE] THEN
1750 DISCH_THEN(X_CHOOSE_THEN `d:real^2` MP_TAC) THEN
1751 DISCH_THEN(CONJUNCTS_THEN2 SUBST1_TAC STRIP_ASSUME_TAC) THEN
1752 DISCH_TAC THEN DISCH_TAC THEN REWRITE_TAC[IN_SET_OF_LIST] THEN
1753 DISCH_TAC THEN EXISTS_TAC `(d:real^2)$2 - (b:real^2)$2` THEN
1754 ASM_REWRITE_TAC[REAL_SUB_LT] THEN
1755 RULE_ASSUM_TAC(REWRITE_RULE[IN_INSERT; IN_SET_OF_LIST]) THEN
1758 MAP_EVERY ABBREV_TAC
1759 [`a':real^2 = (&1 - e / (a$2 - b$2)) % b + e / (a$2 - b$2) % a`;
1760 `c':real^2 = (&1 - e / (c$2 - b$2)) % b + e / (c$2 - b$2) % c`] THEN
1762 `a' IN segment[b:real^2,a] /\ c' IN segment[b,c]`
1763 STRIP_ASSUME_TAC THENL
1764 [MAP_EVERY EXPAND_TAC ["a'"; "c'"] THEN
1765 REWRITE_TAC[IN_SEGMENT] THEN
1766 REWRITE_TAC[VECTOR_ARITH
1767 `(&1 - u) % a + u % b = (&1 - v) % a + v % b <=>
1768 (u - v) % (b - a) = vec 0`] THEN
1769 ASM_REWRITE_TAC[VECTOR_MUL_EQ_0; VECTOR_SUB_EQ; REAL_SUB_0] THEN
1770 ONCE_REWRITE_TAC[TAUT `p /\ q /\ r <=> r /\ p /\ q`] THEN
1771 REWRITE_TAC[UNWIND_THM1] THEN
1772 ASM_SIMP_TAC[REAL_LT_IMP_LE; REAL_LE_DIV; REAL_SUB_LE;
1773 REAL_LE_LDIV_EQ; REAL_SUB_LT; REAL_MUL_LID];
1775 SUBGOAL_THEN `~(a':real^2 = b) /\ ~(c':real^2 = b)` STRIP_ASSUME_TAC THENL
1776 [MAP_EVERY EXPAND_TAC ["a'"; "c'"] THEN
1777 REWRITE_TAC[VECTOR_ARITH
1778 `(&1 - u) % a + u % b = a <=> u % (b - a) = vec 0`] THEN
1779 ASM_REWRITE_TAC[VECTOR_MUL_EQ_0; VECTOR_SUB_EQ] THEN
1780 ASM_SIMP_TAC[REAL_EQ_LDIV_EQ; REAL_SUB_LT] THEN
1781 ASM_SIMP_TAC[REAL_MUL_LZERO; REAL_LT_IMP_NZ];
1783 SUBGOAL_THEN `~collinear{a':real^2,b,c'}` ASSUME_TAC THENL
1784 [UNDISCH_TAC `~collinear{a:real^2,b,c}` THEN
1785 REWRITE_TAC[CONTRAPOS_THM] THEN ONCE_REWRITE_TAC[COLLINEAR_3] THEN
1786 MAP_EVERY EXPAND_TAC ["a'"; "c'"] THEN
1787 REWRITE_TAC[VECTOR_ARITH `((&1 - u) % b + u % a) - b = u % (a - b)`] THEN
1788 REWRITE_TAC[GSYM DOT_CAUCHY_SCHWARZ_EQUAL; DOT_LMUL; DOT_RMUL] THEN
1789 MATCH_MP_TAC(REAL_FIELD
1790 `~(a = &0) /\ ~(c = &0)
1791 ==> (a * c * x) pow 2 = (a * a * y) * (c * c * z)
1792 ==> x pow 2 = y * z`) THEN
1793 ASM_SIMP_TAC[REAL_EQ_LDIV_EQ; REAL_SUB_LT] THEN
1794 ASM_SIMP_TAC[REAL_MUL_LZERO; REAL_LT_IMP_NZ];
1796 SUBGOAL_THEN `~(a':real^2 = c')` ASSUME_TAC THENL
1797 [DISCH_TAC THEN UNDISCH_TAC `~collinear{a':real^2,b,c'}` THEN
1798 ASM_REWRITE_TAC[INSERT_AC; COLLINEAR_2];
1800 SUBGOAL_THEN `~affine_dependent{a':real^2,b,c'}` ASSUME_TAC THENL
1801 [ASM_MESON_TAC[AFFINE_DEPENDENT_IMP_COLLINEAR_3]; ALL_TAC] THEN
1802 MP_TAC(ISPEC `{a':real^2,b,c'}` INTERIOR_CONVEX_HULL_EQ_EMPTY) THEN
1803 REWRITE_TAC[DIMINDEX_2; HAS_SIZE; ARITH; FINITE_INSERT; FINITE_EMPTY] THEN
1804 SIMP_TAC[CARD_CLAUSES; FINITE_INSERT; FINITE_EMPTY] THEN
1805 ASM_REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY; ARITH] THEN DISCH_TAC THEN
1806 SUBGOAL_THEN `convex hull {a,b,c} INTER {x:real^2 | x$2 - b$2 <= e} =
1807 convex hull {a',b,c'}`
1809 [MATCH_MP_TAC SUBSET_ANTISYM THEN CONJ_TAC THENL
1810 [ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {b,a,c}`] THEN
1811 REWRITE_TAC[CONVEX_HULL_3_ALT] THEN
1812 REWRITE_TAC[SUBSET; IN_INTER; FORALL_IN_GSPEC; IMP_CONJ] THEN
1813 REWRITE_TAC[IN_ELIM_THM; VECTOR_ARITH
1814 `a + x:real^N = a + y <=> x = y`] THEN
1815 MAP_EVERY X_GEN_TAC [`s:real`; `t:real`] THEN
1816 REPLICATE_TAC 3 DISCH_TAC THEN MAP_EVERY EXPAND_TAC ["a'"; "c'"] THEN
1817 REWRITE_TAC[VECTOR_ARITH
1818 `((&1 - u) % b + u % a) - b:real^N = u % (a - b)`] THEN
1819 REWRITE_TAC[VECTOR_ADD_COMPONENT; VECTOR_MUL_COMPONENT] THEN
1820 REWRITE_TAC[REAL_ADD_SUB; VECTOR_SUB_COMPONENT] THEN STRIP_TAC THEN
1821 EXISTS_TAC `(s * ((a:real^2)$2 - (b:real^2)$2)) / e` THEN
1822 EXISTS_TAC `(t * ((c:real^2)$2 - (b:real^2)$2)) / e` THEN
1823 ASM_SIMP_TAC[REAL_LE_DIV; REAL_LE_MUL; REAL_SUB_LT; REAL_LT_IMP_LE] THEN
1824 REWRITE_TAC[REAL_ARITH `a / e + b / e:real = (a + b) / e`] THEN
1825 ASM_SIMP_TAC[REAL_LE_LDIV_EQ; REAL_MUL_LID] THEN
1826 REWRITE_TAC[VECTOR_MUL_ASSOC] THEN BINOP_TAC THEN
1827 AP_THM_TAC THEN AP_TERM_TAC THEN MATCH_MP_TAC(REAL_FIELD
1828 `y < x /\ &0 < e ==> s = (s * (x - y)) / e * e / (x - y)`) THEN
1830 MATCH_MP_TAC HULL_MINIMAL THEN
1831 REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET; IN_INTER; IN_ELIM_THM] THEN
1832 ASM_SIMP_TAC[HULL_INC; IN_INSERT; REAL_SUB_REFL; REAL_LT_IMP_LE] THEN
1833 SIMP_TAC[REAL_LE_SUB_RADD; CONVEX_INTER; CONVEX_HALFSPACE_COMPONENT_LE;
1834 CONVEX_CONVEX_HULL] THEN
1835 REPEAT CONJ_TAC THENL
1836 [UNDISCH_TAC `a' IN segment[b:real^2,a]` THEN
1837 SPEC_TAC(`a':real^2`,`x:real^2`) THEN REWRITE_TAC[GSYM SUBSET] THEN
1838 REWRITE_TAC[SEGMENT_CONVEX_HULL] THEN MATCH_MP_TAC HULL_MONO THEN
1841 UNDISCH_TAC `c' IN segment[b:real^2,c]` THEN
1842 SPEC_TAC(`c':real^2`,`x:real^2`) THEN REWRITE_TAC[GSYM SUBSET] THEN
1843 REWRITE_TAC[SEGMENT_CONVEX_HULL] THEN MATCH_MP_TAC HULL_MONO THEN
1845 EXPAND_TAC "c'"] THEN
1846 REWRITE_TAC[VECTOR_ADD_COMPONENT; VECTOR_MUL_COMPONENT] THEN
1847 REWRITE_TAC[REAL_ARITH
1848 `(&1 - u) * b + u * a <= e + b <=> (a - b) * u <= e`] THEN
1849 ASM_SIMP_TAC[REAL_DIV_LMUL; REAL_LT_IMP_NZ; REAL_SUB_LT] THEN
1850 REWRITE_TAC[REAL_LE_REFL]];
1853 `interior(convex hull {a,b,c}) INTER {x:real^2 | x$2 - b$2 < e} =
1854 interior(convex hull {a',b,c'})`
1856 [REWRITE_TAC[REAL_LT_SUB_RADD; GSYM INTERIOR_HALFSPACE_COMPONENT_LE] THEN
1857 ASM_REWRITE_TAC[GSYM INTERIOR_INTER; GSYM REAL_LE_SUB_RADD];
1860 `?d:real^2. d IN interior(convex hull {a',b,c'}) /\ ~(d$1 = b$1)`
1861 STRIP_ASSUME_TAC THENL
1862 [UNDISCH_TAC `~(interior(convex hull {a':real^2,b,c'}) = {})` THEN
1863 REWRITE_TAC[GSYM MEMBER_NOT_EMPTY; LEFT_IMP_EXISTS_THM] THEN
1864 X_GEN_TAC `x:real^2` THEN DISCH_TAC THEN
1865 ASM_CASES_TAC `(x:real^2)$1 = (b:real^2)$1` THENL
1866 [ALL_TAC; EXISTS_TAC `x:real^2` THEN ASM_REWRITE_TAC[]] THEN
1867 FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [IN_INTERIOR]) THEN
1868 DISCH_THEN(X_CHOOSE_THEN `k:real` MP_TAC) THEN
1869 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN REWRITE_TAC[SUBSET] THEN
1870 DISCH_THEN(fun th -> ASSUME_TAC th THEN MP_TAC th) THEN
1871 DISCH_THEN(MP_TAC o SPEC `x + k / &2 % basis 1:real^2`) THEN ANTS_TAC THENL
1872 [REWRITE_TAC[IN_BALL; NORM_ARITH `dist(x,x + e) = norm e`] THEN
1873 SIMP_TAC[NORM_MUL; NORM_BASIS; DIMINDEX_GE_1; ARITH] THEN
1874 UNDISCH_TAC `&0 < k` THEN REAL_ARITH_TAC;
1876 EXISTS_TAC `x + k / &2 % basis 1:real^2` THEN
1877 REWRITE_TAC[VECTOR_ADD_COMPONENT; VECTOR_MUL_COMPONENT] THEN
1878 ASM_SIMP_TAC[BASIS_COMPONENT; DIMINDEX_GE_1; ARITH; REAL_MUL_RID] THEN
1879 ASM_SIMP_TAC[REAL_ARITH `&0 < k ==> ~(b + k / &2 = b)`] THEN
1880 REWRITE_TAC[IN_INTERIOR] THEN EXISTS_TAC `k / &2` THEN
1881 ASM_REWRITE_TAC[REAL_HALF; SUBSET] THEN X_GEN_TAC `y:real^2` THEN
1882 REWRITE_TAC[IN_BALL] THEN DISCH_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN
1883 REWRITE_TAC[IN_BALL] THEN MATCH_MP_TAC(NORM_ARITH
1884 `!a. dist(x + a,y) < k / &2 /\ norm(a) = k / &2 ==> dist(x,y) < k`) THEN
1885 EXISTS_TAC `k / &2 % basis 1:real^2` THEN ASM_REWRITE_TAC[NORM_MUL] THEN
1886 SIMP_TAC[NORM_BASIS; DIMINDEX_GE_1; LE_REFL] THEN
1887 UNDISCH_TAC `&0 < k` THEN REAL_ARITH_TAC;
1890 `path_image(polygonal_path(CONS a (CONS b (CONS c p))))
1891 SUBSET {x:real^2 | x$2 >= b$2}`
1893 [MATCH_MP_TAC SUBSET_TRANS THEN
1895 `convex hull(set_of_list(CONS (a:real^2) (CONS b (CONS c p))))` THEN
1896 SIMP_TAC[PATH_IMAGE_POLYGONAL_PATH_SUBSET_CONVEX_HULL; NOT_CONS_NIL] THEN
1897 MATCH_MP_TAC HULL_MINIMAL THEN
1898 REWRITE_TAC[CONVEX_HALFSPACE_COMPONENT_GE] THEN
1899 REWRITE_TAC[set_of_list; INSERT_SUBSET; IN_ELIM_THM; EMPTY_SUBSET] THEN
1900 ASM_SIMP_TAC[SUBSET; IN_SET_OF_LIST; real_ge; IN_ELIM_THM; REAL_LT_IMP_LE;
1902 GEN_REWRITE_TAC LAND_CONV [SUBSET] THEN
1903 ASM_SIMP_TAC[POLYGONAL_PATH_CONS_CONS; NOT_CONS_NIL] THEN
1904 REWRITE_TAC[IN_ELIM_THM; real_ge] THEN DISCH_TAC] THEN
1906 `(:real^2) DIFF {x | x$2 >= b$2} SUBSET
1908 (linepath(a,b) ++ linepath(b,c) ++ polygonal_path(CONS c p)))`
1910 [MATCH_MP_TAC OUTSIDE_SUBSET_CONVEX THEN
1911 REWRITE_TAC[CONVEX_HALFSPACE_COMPONENT_GE] THEN
1912 ASM_REWRITE_TAC[SUBSET; real_ge; IN_ELIM_THM];
1913 REWRITE_TAC[SUBSET; real_ge; IN_ELIM_THM; IN_UNIV;
1914 IN_DIFF; REAL_NOT_LE] THEN
1917 `d':real^2 = d - (&1 + (d:real^2)$2 - (b:real^2)$2) % basis 2` THEN
1918 SUBGOAL_THEN `(d':real^2) IN outside(path_image
1919 (linepath(a,b) ++ linepath(b,c) ++ polygonal_path(CONS c p)))`
1921 [FIRST_X_ASSUM MATCH_MP_TAC THEN EXPAND_TAC "d'" THEN
1922 REWRITE_TAC[VECTOR_SUB_COMPONENT; VECTOR_MUL_COMPONENT] THEN
1923 SIMP_TAC[BASIS_COMPONENT; DIMINDEX_2; ARITH] THEN REAL_ARITH_TAC;
1925 SUBGOAL_THEN `(a':real^2)$2 - (b:real^2)$2 = e /\
1926 (c':real^2)$2 - (b:real^2)$2 = e`
1927 STRIP_ASSUME_TAC THENL
1928 [MAP_EVERY EXPAND_TAC ["a'"; "c'"] THEN
1929 REWRITE_TAC[VECTOR_ADD_COMPONENT; VECTOR_MUL_COMPONENT] THEN
1930 REWRITE_TAC[REAL_ARITH `((&1 - u) * b + u * a) - b = u * (a - b)`] THEN
1931 ASM_SIMP_TAC[REAL_DIV_RMUL; REAL_ARITH `b < a ==> ~(a - b = &0)`];
1933 SUBGOAL_THEN `(b:real^2)$2 < (d:real^2)$2 /\ (d:real^2)$2 < (b:real^2)$2 + e`
1934 STRIP_ASSUME_TAC THENL
1935 [UNDISCH_TAC `(d:real^2) IN interior(convex hull {a',b,c'})` THEN
1936 ASM_SIMP_TAC[INTERIOR_CONVEX_HULL_3_MINIMAL] THEN
1937 REWRITE_TAC[IN_ELIM_THM; LEFT_IMP_EXISTS_THM] THEN
1938 MAP_EVERY X_GEN_TAC [`r:real`; `s:real`; `t:real`] THEN
1939 REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
1940 DISCH_THEN(SUBST1_TAC o SYM) THEN
1941 REWRITE_TAC[VECTOR_ADD_COMPONENT; VECTOR_MUL_COMPONENT] THEN
1942 RULE_ASSUM_TAC(REWRITE_RULE[REAL_EQ_SUB_RADD]) THEN ASM_REWRITE_TAC[] THEN
1943 FIRST_ASSUM(SUBST1_TAC o MATCH_MP (REAL_ARITH
1944 `r + s + t = &1 ==> s = &1 - (r + t)`)) THEN
1945 REWRITE_TAC[REAL_ARITH
1946 `b < r * x + (&1 - (r + t)) * b + t * x <=> (r + t) * b < (r + t) * x`;
1948 `r * (e + b) + (&1 - (r + t)) * b + t * (e + b) < b + e <=>
1949 (r + t) * e < &1 * e`] THEN
1950 ASM_SIMP_TAC[REAL_LT_LMUL_EQ; REAL_LT_ADD; REAL_LT_RMUL_EQ] THEN
1953 SUBGOAL_THEN `(d':real^2)$2 + &1 = (b:real^2)$2` ASSUME_TAC THENL
1954 [EXPAND_TAC "d'" THEN REWRITE_TAC[VECTOR_SUB_COMPONENT] THEN
1955 SIMP_TAC[VECTOR_MUL_COMPONENT; BASIS_COMPONENT; DIMINDEX_2; ARITH] THEN
1959 `convex hull {a':real^2,b,c'} SUBSET convex hull {a,b,c}`
1961 [MATCH_MP_TAC HULL_MINIMAL THEN
1962 REWRITE_TAC[CONVEX_CONVEX_HULL; INSERT_SUBSET; EMPTY_SUBSET] THEN
1963 SIMP_TAC[HULL_INC; IN_INSERT] THEN CONJ_TAC THENL
1964 [UNDISCH_TAC `(a':real^2) IN segment[b,a]` THEN
1965 SPEC_TAC(`a':real^2`,`x:real^2`);
1966 UNDISCH_TAC `(c':real^2) IN segment[b,c]` THEN
1967 SPEC_TAC(`c':real^2`,`x:real^2`)] THEN
1968 REWRITE_TAC[GSYM SUBSET] THEN REWRITE_TAC[SEGMENT_CONVEX_HULL] THEN
1969 MATCH_MP_TAC HULL_MONO THEN SET_TAC[];
1971 SUBGOAL_THEN `~(d' IN convex hull {a:real^2,b,c})` ASSUME_TAC THENL
1972 [MATCH_MP_TAC(SET_RULE
1973 `!t. s SUBSET t /\ ~(x IN t) ==> ~(x IN s)`) THEN
1974 EXISTS_TAC `{x | (x:real^2)$2 >= (b:real^2)$2}` THEN
1975 SIMP_TAC[SUBSET_HULL; CONVEX_HALFSPACE_COMPONENT_GE] THEN
1976 ASM_REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET; IN_ELIM_THM; real_ge] THEN
1979 SUBGOAL_THEN `~(d' IN convex hull {a':real^2,b,c'})` ASSUME_TAC THENL
1980 [ASM SET_TAC[]; ALL_TAC] THEN
1982 `~(segment[d:real^2,d'] INTER frontier(convex hull {a',b,c'}) = {})`
1984 [MATCH_MP_TAC CONNECTED_INTER_FRONTIER THEN
1985 REWRITE_TAC[CONNECTED_SEGMENT; GSYM MEMBER_NOT_EMPTY] THEN CONJ_TAC THENL
1986 [EXISTS_TAC `d:real^2` THEN REWRITE_TAC[ENDS_IN_SEGMENT; IN_INTER] THEN
1987 ASM_MESON_TAC[INTERIOR_SUBSET; SUBSET];
1988 EXISTS_TAC `d':real^2` THEN ASM_REWRITE_TAC[ENDS_IN_SEGMENT; IN_DIFF]];
1990 GEN_REWRITE_TAC LAND_CONV [GSYM MEMBER_NOT_EMPTY] THEN
1991 DISCH_THEN(X_CHOOSE_THEN `x:real^2` MP_TAC) THEN REWRITE_TAC[IN_INTER] THEN
1992 ASM_CASES_TAC `x:real^2 = d` THENL
1993 [ASM_REWRITE_TAC[IN_DIFF; frontier]; ALL_TAC] THEN
1994 ASM_CASES_TAC `x:real^2 = d'` THENL
1995 [ASM_REWRITE_TAC[IN_DIFF; frontier] THEN
1996 SUBGOAL_THEN `closure(convex hull {a':real^2,b,c'}) = convex hull {a',b,c'}`
1997 (fun th -> ASM_REWRITE_TAC[th]) THEN
1998 MATCH_MP_TAC CLOSURE_CLOSED THEN MATCH_MP_TAC COMPACT_IMP_CLOSED THEN
1999 MESON_TAC[COMPACT_CONVEX_HULL; FINITE_IMP_COMPACT; FINITE_RULES];
2001 ASM_REWRITE_TAC[SEGMENT_CLOSED_OPEN; IN_UNION; IN_INSERT; NOT_IN_EMPTY] THEN
2003 SUBGOAL_THEN `(d':real^2)$1 = (d:real^2)$1` ASSUME_TAC THENL
2004 [EXPAND_TAC "d'" THEN REWRITE_TAC[VECTOR_SUB_COMPONENT] THEN
2005 SIMP_TAC[VECTOR_MUL_COMPONENT; BASIS_COMPONENT; DIMINDEX_2; ARITH] THEN
2008 SUBGOAL_THEN `(x:real^2)$1 = (d:real^2)$1` ASSUME_TAC THENL
2009 [MP_TAC(ISPECL [`d:real^2`; `d':real^2`; `x:real^2`] SEGMENT_VERTICAL) THEN
2010 ASM_REWRITE_TAC[SEGMENT_CLOSED_OPEN; IN_UNION] THEN ASM_REAL_ARITH_TAC;
2012 SUBGOAL_THEN `~(x:real^2 = b)` ASSUME_TAC THENL
2013 [ASM_MESON_TAC[]; ALL_TAC] THEN
2014 SUBGOAL_THEN `(x:real^2)$2 < (b:real^2)$2 + e` ASSUME_TAC THENL
2015 [MP_TAC(ISPECL [`d:real^2`; `d':real^2`; `x:real^2`] SEGMENT_VERTICAL) THEN
2016 ASM_REWRITE_TAC[SEGMENT_CLOSED_OPEN; IN_UNION] THEN ASM_REAL_ARITH_TAC;
2018 SUBGOAL_THEN `~(x:real^2 = a) /\ ~(x = c)` STRIP_ASSUME_TAC THENL
2019 [REWRITE_TAC[CART_EQ; DIMINDEX_2; FORALL_2] THEN ASM_REAL_ARITH_TAC;
2021 SUBGOAL_THEN `(x:real^2) IN (segment(b,a) UNION segment(b,c))`
2023 [UNDISCH_TAC `(x:real^2) IN frontier(convex hull {a':real^2,b,c'})` THEN
2024 ASM_SIMP_TAC[open_segment; IN_UNION; IN_DIFF; IN_INSERT; NOT_IN_EMPTY] THEN
2025 REWRITE_TAC[FRONTIER_OF_TRIANGLE] THEN MATCH_MP_TAC(SET_RULE
2026 `~(x IN u) /\ s SUBSET s' /\ t SUBSET t'
2027 ==> x IN (s UNION t UNION u) ==> x IN s' \/ x IN t'`) THEN
2028 ASM_REWRITE_TAC[SUBSET_SEGMENT; ENDS_IN_SEGMENT] THEN DISCH_TAC THEN
2029 MP_TAC(ISPECL [`c':real^2`; `a':real^2`; `x:real^2`]
2030 SEGMENT_HORIZONTAL) THEN
2031 ASM_REWRITE_TAC[] THEN ASM_REAL_ARITH_TAC;
2034 `segment[d:real^2,d'] INTER path_image(polygonal_path(CONS c p)) = {}`
2036 [MATCH_MP_TAC(SET_RULE
2037 `!u. t SUBSET u /\ s INTER u = {} ==> s INTER t = {}`) THEN
2038 EXISTS_TAC `{x:real^2 | x$2 >= (b:real^2)$2 + e}` THEN CONJ_TAC THENL
2039 [MATCH_MP_TAC SUBSET_TRANS THEN
2040 EXISTS_TAC `convex hull(set_of_list(CONS c p)) :real^2->bool` THEN
2041 SIMP_TAC[PATH_IMAGE_POLYGONAL_PATH_SUBSET_CONVEX_HULL; NOT_CONS_NIL] THEN
2042 MATCH_MP_TAC HULL_MINIMAL THEN
2043 REWRITE_TAC[CONVEX_HALFSPACE_COMPONENT_GE;
2044 set_of_list; INSERT_SUBSET] THEN
2045 REWRITE_TAC[SUBSET; IN_SET_OF_LIST; IN_ELIM_THM] THEN
2046 ASM_SIMP_TAC[real_ge; REAL_ARITH `b + e <= x <=> e <= x - b`];
2047 REWRITE_TAC[SET_RULE `s INTER t = {} <=> !x. x IN s ==> ~(x IN t)`] THEN
2048 X_GEN_TAC `y:real^2` THEN DISCH_TAC THEN
2049 MP_TAC(ISPECL[`d:real^2`; `d':real^2`; `y:real^2`] SEGMENT_VERTICAL) THEN
2050 ASM_REWRITE_TAC[IN_ELIM_THM; real_ge] THEN ASM_REAL_ARITH_TAC];
2052 SUBGOAL_THEN `(d:real^2) IN interior(convex hull {a,b,c})` ASSUME_TAC THENL
2053 [UNDISCH_TAC `(d:real^2) IN interior(convex hull {a', b, c'})` THEN
2054 SPEC_TAC(`d:real^2`,`d:real^2`) THEN REWRITE_TAC[GSYM SUBSET] THEN
2055 MATCH_MP_TAC SUBSET_INTERIOR THEN ASM_REWRITE_TAC[];
2057 SUBGOAL_THEN `~(d':real^2 = d)` ASSUME_TAC THENL
2058 [ASM_MESON_TAC[IN_SEGMENT]; ALL_TAC] THEN
2060 `!y:real^2. y IN segment[d,d'] /\
2061 y IN (segment (b,a) UNION segment (b,c))
2064 [GEN_TAC THEN STRIP_TAC THEN
2065 SUBGOAL_THEN `collinear {d:real^2,x,y}` MP_TAC THENL
2066 [REWRITE_TAC[COLLINEAR_AFFINE_HULL] THEN
2067 MAP_EVERY EXISTS_TAC [`d:real^2`; `d':real^2`] THEN
2068 REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET] THEN
2069 REPEAT CONJ_TAC THEN MATCH_MP_TAC
2070 (REWRITE_RULE[SUBSET] CONVEX_HULL_SUBSET_AFFINE_HULL) THEN
2071 ASM_REWRITE_TAC[GSYM SEGMENT_CONVEX_HULL; ENDS_IN_SEGMENT] THEN
2072 ASM_REWRITE_TAC[SEGMENT_CLOSED_OPEN; IN_UNION];
2074 REWRITE_TAC[COLLINEAR_BETWEEN_CASES; BETWEEN_IN_SEGMENT] THEN
2075 ASM_SIMP_TAC[SEGMENT_CLOSED_OPEN; IN_UNION; IN_INSERT; NOT_IN_EMPTY] THEN
2076 ASM_CASES_TAC `x:real^2 = y` THEN ASM_REWRITE_TAC[] THEN
2078 `(x:real^2) IN frontier(convex hull {a,b,c}) /\
2079 (y:real^2) IN frontier(convex hull {a,b,c})`
2081 [REWRITE_TAC[FRONTIER_OF_TRIANGLE] THEN
2082 REWRITE_TAC[SEGMENT_CLOSED_OPEN; IN_UNION] THEN
2083 RULE_ASSUM_TAC(REWRITE_RULE[IN_UNION]) THEN ASM_MESON_TAC[SEGMENT_SYM];
2084 REWRITE_TAC[frontier; IN_DIFF]] THEN
2085 ASM_CASES_TAC `y:real^2 = d` THEN ASM_REWRITE_TAC[] THEN
2086 REPEAT STRIP_TAC THENL
2087 [MAP_EVERY UNDISCH_TAC
2088 [`(d:real^2) IN segment (x,y)`;
2089 `(y:real^2) IN segment [d,d']`;
2090 `(x:real^2) IN segment(d,d')`] THEN
2091 ASM_REWRITE_TAC[IN_SEGMENT] THEN
2092 REPLICATE_TAC 2 (STRIP_TAC THEN ASM_REWRITE_TAC[]) THEN
2093 ASM_REWRITE_TAC[VECTOR_MUL_EQ_0; VECTOR_SUB_EQ; VECTOR_ARITH
2094 `d = (&1 - w) % ((&1 - u) % d + u % d') + w % ((&1 - v) % d + v % d') <=>
2095 ((&1 - w) * u + w * v) % (d' - d) = vec 0`] THEN
2096 DISCH_THEN(CHOOSE_THEN MP_TAC) THEN
2097 REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
2098 ASM_SIMP_TAC[REAL_SUB_LE; REAL_LE_MUL; REAL_LT_IMP_LE; REAL_ARITH
2099 `&0 <= x /\ &0 <= y ==> (x + y = &0 <=> x = &0 /\ y = &0)`] THEN
2100 REWRITE_TAC[REAL_ENTIRE] THEN ASM_REAL_ARITH_TAC;
2101 UNDISCH_TAC `~(x IN interior(convex hull {a:real^2, b, c}))` THEN
2102 UNDISCH_TAC `x IN segment (y:real^2,d)` THEN
2103 SPEC_TAC(`x:real^2`,`x:real^2`) THEN ASM_REWRITE_TAC[GSYM SUBSET] THEN
2104 ONCE_REWRITE_TAC[SEGMENT_SYM] THEN
2105 MATCH_MP_TAC IN_INTERIOR_CLOSURE_CONVEX_SEGMENT THEN
2106 ASM_REWRITE_TAC[CONVEX_CONVEX_HULL];
2107 UNDISCH_TAC `~(y IN interior(convex hull {a:real^2, b, c}))` THEN
2108 UNDISCH_TAC `y IN segment (d:real^2,x)` THEN
2109 SPEC_TAC(`y:real^2`,`y:real^2`) THEN ASM_REWRITE_TAC[GSYM SUBSET] THEN
2110 MATCH_MP_TAC IN_INTERIOR_CLOSURE_CONVEX_SEGMENT THEN
2111 ASM_REWRITE_TAC[CONVEX_CONVEX_HULL]];
2113 SUBGOAL_THEN `pathfinish(polygonal_path p) = (a:real^2)` ASSUME_TAC THENL
2114 [ASM_REWRITE_TAC[PATHFINISH_POLYGONAL_PATH]; ALL_TAC] THEN
2115 SUBGOAL_THEN `segment(a:real^2,b) INTER segment(b,c) = {}` ASSUME_TAC THENL
2116 [UNDISCH_TAC `segment[a:real^2,b] INTER segment[b,c] SUBSET {a, b}` THEN
2117 REWRITE_TAC[SUBSET; EXTENSION; IN_INTER; NOT_IN_EMPTY] THEN
2118 MATCH_MP_TAC MONO_FORALL THEN
2119 REWRITE_TAC[open_segment; IN_DIFF; IN_INSERT; NOT_IN_EMPTY] THEN
2123 `(d:real^2) IN inside(path_image
2124 (linepath(a,b) ++ linepath(b,c) ++ polygonal_path(CONS c p)))`
2126 [UNDISCH_TAC `x IN segment(b:real^2,a) UNION segment (b,c)` THEN
2127 REWRITE_TAC[IN_UNION] THEN STRIP_TAC THENL
2128 [MP_TAC(ISPECL [`a:real^2`; `b:real^2`; `d:real^2`; `d':real^2`;
2129 `linepath(b:real^2,c) ++ polygonal_path(CONS c p)`;
2130 `x:real^2`] PARITY_LEMMA) THEN
2132 `path_image((linepath(b:real^2,c) ++ polygonal_path(CONS c p)) ++
2134 path_image(linepath(a,b) ++ linepath(b:real^2,c) ++
2135 polygonal_path(CONS c p))`
2137 [MATCH_MP_TAC PATH_IMAGE_SYM THEN
2138 REWRITE_TAC[PATHSTART_JOIN; PATHFINISH_JOIN] THEN
2139 REWRITE_TAC[PATHSTART_LINEPATH; PATHFINISH_LINEPATH] THEN
2140 UNDISCH_TAC `pathfinish(linepath(a,b) ++
2141 linepath (b,c) ++ polygonal_path(CONS c p)):real^2 = a` THEN
2142 ASM_REWRITE_TAC[PATHFINISH_JOIN; PATHFINISH_POLYGONAL_PATH];
2144 ASM_REWRITE_TAC[] THEN DISCH_THEN MATCH_MP_TAC THEN REPEAT CONJ_TAC THENL
2145 [W(MP_TAC o PART_MATCH (lhs o rand) SIMPLE_PATH_SYM o snd) THEN
2146 ASM_REWRITE_TAC[PATHSTART_JOIN; PATHFINISH_JOIN] THEN
2147 ASM_REWRITE_TAC[PATHSTART_LINEPATH; PATHFINISH_LINEPATH] THEN
2148 REWRITE_TAC[PATHFINISH_POLYGONAL_PATH] THEN
2149 ASM_REWRITE_TAC[NOT_CONS_NIL; LAST];
2150 REWRITE_TAC[PATHSTART_JOIN; PATHSTART_LINEPATH];
2151 REWRITE_TAC[PATHFINISH_JOIN; PATHFINISH_POLYGONAL_PATH] THEN
2152 ASM_REWRITE_TAC[NOT_CONS_NIL; LAST];
2153 MATCH_MP_TAC(SET_RULE
2154 `x IN s /\ x IN t /\ (!y. y IN s /\ y IN t ==> y = x)
2155 ==> s INTER t = {x}`) THEN
2156 SUBST1_TAC(ISPECL[`a:real^2`; `b:real^2`] (CONJUNCT2 SEGMENT_SYM)) THEN
2157 ASM_REWRITE_TAC[] THEN
2158 RULE_ASSUM_TAC(REWRITE_RULE[SEGMENT_CLOSED_OPEN]) THEN ASM SET_TAC[];
2159 SIMP_TAC[PATH_IMAGE_JOIN; PATHFINISH_LINEPATH; PATH_IMAGE_LINEPATH;
2160 PATHSTART_POLYGONAL_PATH; NOT_CONS_NIL; HD] THEN
2161 ASM_REWRITE_TAC[SET_RULE `s INTER (t UNION u) = {} <=>
2162 s INTER t = {} /\ s INTER u = {}`] THEN
2163 REWRITE_TAC[EXTENSION; IN_INTER; NOT_IN_EMPTY] THEN
2164 X_GEN_TAC `y:real^2` THEN
2165 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
2166 SUBGOAL_THEN `(y:real^2)$1 = (d:real^2)$1` ASSUME_TAC THENL
2167 [MP_TAC(ISPECL [`d:real^2`; `d':real^2`; `y:real^2`]
2168 SEGMENT_VERTICAL) THEN
2169 ASM_REWRITE_TAC[SEGMENT_CLOSED_OPEN; IN_UNION] THEN
2172 ASM_REWRITE_TAC[SEGMENT_CLOSED_OPEN; IN_UNION;
2173 IN_INSERT; NOT_IN_EMPTY] THEN
2174 ASM_CASES_TAC `y:real^2 = b` THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
2175 RULE_ASSUM_TAC(SUBS[ISPECL [`a:real^2`; `b:real^2`]
2176 (CONJUNCT2 SEGMENT_SYM)]) THEN
2177 ASM_CASES_TAC `y:real^2 = c` THENL [ALL_TAC; ASM SET_TAC[]] THEN
2178 UNDISCH_THEN `y:real^2 = c` SUBST_ALL_TAC THEN
2179 MP_TAC(ISPECL [`d:real^2`; `d':real^2`; `c:real^2`]
2180 SEGMENT_VERTICAL) THEN
2181 ASM_REWRITE_TAC[SEGMENT_CLOSED_OPEN; IN_UNION] THEN
2182 ASM_REAL_ARITH_TAC];
2183 MP_TAC(ISPECL [`b:real^2`; `c:real^2`; `d:real^2`; `d':real^2`;
2184 `polygonal_path(CONS c p) ++ linepath(a:real^2,b)`;
2185 `x:real^2`] PARITY_LEMMA) THEN
2187 `path_image((polygonal_path (CONS c p) ++ linepath (a,b)) ++
2188 linepath(b:real^2,c)) =
2189 path_image(linepath(a,b) ++ linepath(b:real^2,c) ++
2190 polygonal_path(CONS c p))`
2192 [ASM_SIMP_TAC[PATH_IMAGE_JOIN; PATHSTART_JOIN; PATHFINISH_JOIN;
2193 PATHSTART_LINEPATH; PATHFINISH_LINEPATH;
2194 PATHSTART_POLYGONAL_PATH; PATHFINISH_POLYGONAL_PATH;
2195 NOT_CONS_NIL; HD; LAST] THEN
2196 REWRITE_TAC[UNION_ACI];
2198 ASM_REWRITE_TAC[] THEN DISCH_THEN MATCH_MP_TAC THEN REPEAT CONJ_TAC THENL
2199 [W(MP_TAC o PART_MATCH (lhs o rand) (GSYM SIMPLE_PATH_ASSOC) o snd) THEN
2202 DISCH_THEN SUBST1_TAC THEN
2203 W(MP_TAC o PART_MATCH (lhs o rand) SIMPLE_PATH_SYM o snd) THEN
2206 DISCH_THEN SUBST1_TAC THEN
2207 W(MP_TAC o PART_MATCH (lhs o rand) (GSYM SIMPLE_PATH_ASSOC) o
2209 ASM_REWRITE_TAC[] THEN DISCH_THEN MATCH_MP_TAC]] THEN
2210 ASM_SIMP_TAC[GSYM SIMPLE_PATH_ASSOC;PATHSTART_JOIN;
2212 PATHSTART_LINEPATH; PATHFINISH_LINEPATH;
2213 PATHSTART_POLYGONAL_PATH; PATHFINISH_POLYGONAL_PATH;
2214 NOT_CONS_NIL; HD; LAST];
2215 REWRITE_TAC[PATHSTART_JOIN; PATHSTART_POLYGONAL_PATH] THEN
2216 REWRITE_TAC[NOT_CONS_NIL; HD];
2217 REWRITE_TAC[PATHFINISH_JOIN; PATHFINISH_LINEPATH];
2218 MATCH_MP_TAC(SET_RULE
2219 `x IN s /\ x IN t /\ (!y. y IN s /\ y IN t ==> y = x)
2220 ==> s INTER t = {x}`) THEN
2221 SUBST1_TAC(ISPECL[`a:real^2`; `b:real^2`] (CONJUNCT2 SEGMENT_SYM)) THEN
2222 ASM_REWRITE_TAC[] THEN
2223 RULE_ASSUM_TAC(REWRITE_RULE[SEGMENT_CLOSED_OPEN]) THEN ASM SET_TAC[];
2224 ASM_SIMP_TAC[PATH_IMAGE_JOIN; PATHSTART_LINEPATH; NOT_CONS_NIL; HD;
2225 PATH_IMAGE_LINEPATH; PATHFINISH_POLYGONAL_PATH; LAST] THEN
2226 ASM_REWRITE_TAC[SET_RULE `s INTER (t UNION u) = {} <=>
2227 s INTER t = {} /\ s INTER u = {}`] THEN
2228 REWRITE_TAC[EXTENSION; IN_INTER; NOT_IN_EMPTY] THEN
2229 X_GEN_TAC `y:real^2` THEN
2230 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
2231 SUBGOAL_THEN `(y:real^2)$1 = (d:real^2)$1` ASSUME_TAC THENL
2232 [MP_TAC(ISPECL [`d:real^2`; `d':real^2`; `y:real^2`]
2233 SEGMENT_VERTICAL) THEN
2234 ASM_REWRITE_TAC[SEGMENT_CLOSED_OPEN; IN_UNION] THEN
2237 ASM_REWRITE_TAC[SEGMENT_CLOSED_OPEN; IN_UNION;
2238 IN_INSERT; NOT_IN_EMPTY] THEN
2239 ASM_CASES_TAC `y:real^2 = b` THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
2240 RULE_ASSUM_TAC(SUBS[ISPECL [`a:real^2`; `b:real^2`]
2241 (CONJUNCT2 SEGMENT_SYM)]) THEN
2242 ONCE_REWRITE_TAC[SEGMENT_SYM] THEN
2243 ASM_CASES_TAC `y:real^2 = a` THENL [ALL_TAC; ASM SET_TAC[]] THEN
2244 UNDISCH_THEN `y:real^2 = a` SUBST_ALL_TAC THEN
2245 MP_TAC(ISPECL [`d:real^2`; `d':real^2`; `a:real^2`]
2246 SEGMENT_VERTICAL) THEN
2247 ASM_REWRITE_TAC[SEGMENT_CLOSED_OPEN; IN_UNION] THEN
2248 ASM_REAL_ARITH_TAC]];
2250 SUBGOAL_THEN `~affine_dependent{a:real^2,b,c}` ASSUME_TAC THENL
2251 [ASM_MESON_TAC[AFFINE_DEPENDENT_IMP_COLLINEAR_3]; ALL_TAC] THEN
2253 `path_image(polygonal_path(CONS c p)) INTER
2254 convex hull {a,b,c} SUBSET {a:real^2,c}`
2256 [MAP_EVERY EXISTS_TAC [`a:real^2`; `c:real^2`] THEN
2257 ASM_REWRITE_TAC[MEM] THEN X_GEN_TAC `y:real^2` THEN DISCH_TAC THEN
2258 MATCH_MP_TAC INSIDE_SAME_COMPONENT THEN
2259 EXISTS_TAC `d:real^2` THEN ASM_REWRITE_TAC[] THEN
2260 REWRITE_TAC[connected_component] THEN
2261 EXISTS_TAC `segment[d:real^2,y]` THEN
2262 REWRITE_TAC[CONNECTED_SEGMENT; ENDS_IN_SEGMENT] THEN
2263 MATCH_MP_TAC SUBSET_TRANS THEN EXISTS_TAC
2264 `convex hull {a:real^2,b,c} DIFF (segment[a,b] UNION segment[b,c])` THEN
2267 SIMP_TAC[PATH_IMAGE_JOIN; PATHSTART_JOIN; PATHFINISH_LINEPATH;
2268 PATHSTART_LINEPATH; PATHSTART_POLYGONAL_PATH; NOT_CONS_NIL; HD] THEN
2269 REWRITE_TAC[PATH_IMAGE_LINEPATH] THEN
2270 FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (SET_RULE
2272 ==> c SUBSET (a UNION b)
2273 ==> s DIFF (a UNION b) SUBSET UNIV DIFF (a UNION b UNION t)`)) THEN
2274 REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET; IN_UNION; ENDS_IN_SEGMENT]] THEN
2275 REWRITE_TAC[SEGMENT_CONVEX_HULL] THEN MATCH_MP_TAC HULL_MINIMAL THEN
2276 REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET] THEN REPEAT CONJ_TAC THENL
2277 [REWRITE_TAC[IN_DIFF] THEN CONJ_TAC THENL
2278 [ASM_MESON_TAC[INTERIOR_SUBSET; SUBSET]; ALL_TAC] THEN
2279 SUBGOAL_THEN `~(d IN frontier(convex hull {a:real^2,b,c}))` MP_TAC THENL
2280 [ASM_REWRITE_TAC[frontier; IN_DIFF];
2281 REWRITE_TAC[FRONTIER_OF_TRIANGLE; SEGMENT_CONVEX_HULL] THEN SET_TAC[]];
2282 REWRITE_TAC[IN_DIFF; IN_UNION] THEN REPEAT STRIP_TAC THENL
2283 [UNDISCH_TAC `y IN segment(a:real^2,c)` THEN
2284 REWRITE_TAC[open_segment; IN_DIFF; SEGMENT_CONVEX_HULL] THEN
2285 MATCH_MP_TAC(SET_RULE `s SUBSET t ==> x IN s /\ P x ==> x IN t`) THEN
2286 MATCH_MP_TAC HULL_MONO THEN SET_TAC[];
2287 UNDISCH_TAC `~collinear{a:real^2,b,c}` THEN REWRITE_TAC[] THEN
2288 ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {b,a,c}`] THEN
2289 MATCH_MP_TAC COLLINEAR_3_TRANS THEN EXISTS_TAC `y:real^2` THEN
2290 MAP_EVERY UNDISCH_TAC
2291 [`y IN convex hull {a:real^2, b}`; `y IN segment(a:real^2,c)`] THEN
2292 REWRITE_TAC[open_segment; GSYM SEGMENT_CONVEX_HULL; IN_DIFF] THEN
2293 REWRITE_TAC[DE_MORGAN_THM; IN_INSERT; NOT_IN_EMPTY] THEN
2294 DISCH_THEN(CONJUNCTS_THEN2 MP_TAC STRIP_ASSUME_TAC) THEN
2295 ASM_REWRITE_TAC[IMP_IMP; GSYM BETWEEN_IN_SEGMENT] THEN
2296 DISCH_THEN(CONJUNCTS_THEN(MP_TAC o
2297 MATCH_MP BETWEEN_IMP_COLLINEAR)) THEN
2298 REWRITE_TAC[INSERT_AC; IMP_IMP];
2299 UNDISCH_TAC `~collinear{a:real^2,b,c}` THEN REWRITE_TAC[] THEN
2300 ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {b,c,a}`] THEN
2301 MATCH_MP_TAC COLLINEAR_3_TRANS THEN EXISTS_TAC `y:real^2` THEN
2302 MAP_EVERY UNDISCH_TAC
2303 [`y IN convex hull {b:real^2, c}`; `y IN segment(a:real^2,c)`] THEN
2304 REWRITE_TAC[open_segment; GSYM SEGMENT_CONVEX_HULL; IN_DIFF] THEN
2305 REWRITE_TAC[DE_MORGAN_THM; IN_INSERT; NOT_IN_EMPTY] THEN
2306 DISCH_THEN(CONJUNCTS_THEN2 MP_TAC STRIP_ASSUME_TAC) THEN
2307 ASM_REWRITE_TAC[IMP_IMP; GSYM BETWEEN_IN_SEGMENT] THEN
2308 DISCH_THEN(CONJUNCTS_THEN(MP_TAC o
2309 MATCH_MP BETWEEN_IMP_COLLINEAR)) THEN
2310 REWRITE_TAC[INSERT_AC; IMP_IMP]];
2311 REWRITE_TAC[SET_RULE
2312 `s DIFF (t UNION u) = (s DIFF t) INTER (s DIFF u)`] THEN
2313 MATCH_MP_TAC CONVEX_INTER THEN CONJ_TAC THENL
2314 [MP_TAC(ISPECL [`convex hull {a:real^2,b,c}`; `convex hull{a:real^2,b}`]
2315 FACE_OF_STILLCONVEX) THEN
2316 REWRITE_TAC[CONVEX_CONVEX_HULL] THEN MATCH_MP_TAC(TAUT
2317 `p ==> (p <=> q /\ r /\ s) ==> r`) THEN
2318 ASM_SIMP_TAC[FACE_OF_CONVEX_HULL_AFFINE_INDEPENDENT] THEN
2319 EXISTS_TAC `{a:real^2,b}` THEN SET_TAC[];
2320 MP_TAC(ISPECL [`convex hull {a:real^2,b,c}`; `convex hull{b:real^2,c}`]
2321 FACE_OF_STILLCONVEX) THEN
2322 REWRITE_TAC[CONVEX_CONVEX_HULL] THEN MATCH_MP_TAC(TAUT
2323 `p ==> (p <=> q /\ r /\ s) ==> r`) THEN
2324 ASM_SIMP_TAC[FACE_OF_CONVEX_HULL_AFFINE_INDEPENDENT] THEN
2325 EXISTS_TAC `{b:real^2,c}` THEN SET_TAC[]]];
2329 ~(n = vec 0) /\ orthogonal n (c - a) /\
2331 STRIP_ASSUME_TAC THENL
2332 [SUBGOAL_THEN `?n:real^2. ~(n = vec 0) /\ orthogonal n (c - a)`
2333 STRIP_ASSUME_TAC THENL
2334 [ONCE_REWRITE_TAC[ORTHOGONAL_SYM] THEN
2335 MATCH_MP_TAC ORTHOGONAL_TO_VECTOR_EXISTS THEN
2336 REWRITE_TAC[DIMINDEX_2; LE_REFL];
2338 REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC (REAL_ARITH
2339 `&0 < n dot (c - b) \/ &0 < --(n dot (c - b)) \/
2340 (n:real^2) dot (c - b) = &0`)
2342 [EXISTS_TAC `n:real^2` THEN ASM_REWRITE_TAC[];
2343 EXISTS_TAC `--n:real^2` THEN ASM_REWRITE_TAC[DOT_LNEG] THEN
2344 ASM_REWRITE_TAC[VECTOR_NEG_EQ_0; ORTHOGONAL_LNEG];
2345 UNDISCH_TAC `~collinear{a:real^2,b,c}` THEN
2346 ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {a,c,b}`] THEN
2347 MATCH_MP_TAC(TAUT `p ==> ~p ==> q`) THEN
2348 ONCE_REWRITE_TAC[COLLINEAR_3] THEN
2349 MATCH_MP_TAC ORTHOGONAL_TO_ORTHOGONAL_2D THEN
2350 EXISTS_TAC `n:real^2` THEN
2351 ONCE_REWRITE_TAC[GSYM ORTHOGONAL_RNEG] THEN
2352 ASM_REWRITE_TAC[VECTOR_NEG_SUB] THEN
2353 ASM_REWRITE_TAC[orthogonal]];
2355 SUBGOAL_THEN `n dot (a - b:real^2) = n dot (c - b)` ASSUME_TAC THENL
2356 [REWRITE_TAC[DOT_RSUB; real_sub; REAL_EQ_ADD_RCANCEL] THEN
2357 ONCE_REWRITE_TAC[REAL_ARITH `x = y <=> y - x = &0`] THEN
2358 ASM_REWRITE_TAC[GSYM DOT_RSUB; GSYM orthogonal];
2361 `!y:real^2. y IN convex hull {a,b,c} /\ ~(y = b) ==> &0 < n dot (y - b)`
2363 [REWRITE_TAC[CONVEX_HULL_3_ALT; FORALL_IN_GSPEC; IMP_CONJ] THEN
2364 REWRITE_TAC[VECTOR_ARITH
2365 `(a + u % (b - a) + v % (c - a)) - b =
2366 (&1 - u - v) % (a - b) + v % (c - b)`] THEN
2367 ASM_REWRITE_TAC[DOT_RADD; DOT_RMUL] THEN
2368 MAP_EVERY X_GEN_TAC [`r:real`; `s:real`] THEN REPEAT STRIP_TAC THEN
2369 REWRITE_TAC[REAL_ARITH `(&1 - u - v) * x + v * x = (&1 - u) * x`] THEN
2370 MATCH_MP_TAC REAL_LT_MUL THEN ASM_REWRITE_TAC[] THEN
2371 ASM_CASES_TAC `r = &1 /\ s = &0` THENL [ALL_TAC; ASM_REAL_ARITH_TAC] THEN
2372 UNDISCH_TAC `~(a + r % (b - a) + s % (c - a):real^2 = b)` THEN
2373 ASM_REWRITE_TAC[REAL_LT_REFL; REAL_SUB_LT] THEN VECTOR_ARITH_TAC;
2376 `!y:real^2. y IN convex hull {a,b,c} ==> &0 <= n dot (y - b)`
2378 [GEN_TAC THEN ASM_CASES_TAC `y:real^2 = b` THEN
2379 ASM_REWRITE_TAC[VECTOR_SUB_REFL; DOT_RZERO; REAL_LE_REFL] THEN
2380 ASM_MESON_TAC[REAL_LT_IMP_LE];
2383 `!y:real^2. y IN convex hull {a,b,c} ==> n dot (y - b) <= n dot (c - b)`
2385 [REWRITE_TAC[CONVEX_HULL_3_ALT; FORALL_IN_GSPEC] THEN
2386 REWRITE_TAC[VECTOR_ARITH
2387 `(a + u % (b - a) + v % (c - a)) - b =
2388 (&1 - u - v) % (a - b) + v % (c - b)`] THEN
2389 ASM_REWRITE_TAC[DOT_RADD; DOT_RMUL; REAL_ARITH
2390 `(&1 - u - v) * x + v * x <= x <=> &0 <= u * x`] THEN
2391 ASM_SIMP_TAC[REAL_LE_MUL; REAL_LT_IMP_LE];
2393 MP_TAC(ISPECL [`\x:real^2. n dot (x - b)`;
2394 `path_image (polygonal_path(CONS c p)) INTER convex hull {a:real^2,b,c}`]
2395 CONTINUOUS_ATTAINS_INF) THEN
2396 REWRITE_TAC[] THEN ANTS_TAC THENL
2397 [REPEAT CONJ_TAC THENL
2398 [MATCH_MP_TAC COMPACT_INTER THEN
2399 SIMP_TAC[COMPACT_PATH_IMAGE; PATH_POLYGONAL_PATH] THEN
2400 SIMP_TAC[COMPACT_CONVEX_HULL; FINITE_IMP_COMPACT;
2401 FINITE_INSERT; FINITE_EMPTY];
2404 `(\x:real^2. n dot (x - b)) = (\x. n dot x) o (\x. x - b)`
2405 SUBST1_TAC THENL [REWRITE_TAC[o_DEF]; ALL_TAC] THEN
2406 REWRITE_TAC[o_ASSOC] THEN MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN
2407 REWRITE_TAC[CONTINUOUS_ON_LIFT_DOT] THEN
2408 SIMP_TAC[CONTINUOUS_ON_SUB; CONTINUOUS_ON_CONST; CONTINUOUS_ON_ID]];
2413 ~(mx = a) /\ ~(mx = c) /\
2414 mx IN path_image(polygonal_path(CONS c p)) INTER convex hull {a, b, c} /\
2416 path_image(polygonal_path(CONS c p)) INTER convex hull {a, b, c}
2417 ==> n dot (mx - b) <= n dot (y - b))`
2418 STRIP_ASSUME_TAC THENL
2419 [FIRST_X_ASSUM(X_CHOOSE_THEN `mx:real^2` STRIP_ASSUME_TAC) THEN
2420 SUBGOAL_THEN `n dot (mx - b:real^2) <= n dot (c - b)` MP_TAC THENL
2421 [ASM SET_TAC[]; ALL_TAC] THEN
2422 GEN_REWRITE_TAC LAND_CONV [REAL_LE_LT] THEN STRIP_TAC THENL
2423 [EXISTS_TAC `mx:real^2` THEN ASM_MESON_TAC[REAL_LT_REFL]; ALL_TAC] THEN
2424 UNDISCH_TAC `~(path_image(polygonal_path(CONS c p)) INTER
2425 convex hull {a, b, c} SUBSET {a:real^2, c})` THEN
2426 REWRITE_TAC[SUBSET; NOT_FORALL_THM; NOT_IMP; IN_INSERT; NOT_IN_EMPTY] THEN
2427 MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `my:real^2` THEN
2428 REWRITE_TAC[DE_MORGAN_THM] THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
2429 X_GEN_TAC `y:real^2` THEN REWRITE_TAC[IN_INTER] THEN STRIP_TAC THEN
2430 MATCH_MP_TAC REAL_LE_TRANS THEN
2431 EXISTS_TAC `n dot (mx - b:real^2)` THEN CONJ_TAC THENL
2432 [ASM_REWRITE_TAC[] THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM SET_TAC[];
2433 FIRST_X_ASSUM MATCH_MP_TAC THEN ASM SET_TAC[]];
2434 FIRST_X_ASSUM(CHOOSE_THEN (K ALL_TAC))] THEN
2435 ABBREV_TAC `m = (n:real^2) dot (mx - b)` THEN
2436 SUBGOAL_THEN `&0 < m` ASSUME_TAC THENL
2437 [EXPAND_TAC "m" THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
2438 CONJ_TAC THENL [ASM SET_TAC[]; DISCH_THEN SUBST_ALL_TAC] THEN
2440 `segment[b:real^2,c] INTER path_image (polygonal_path (CONS c p))
2442 REWRITE_TAC[SUBSET; IN_INTER] THEN
2443 DISCH_THEN(MP_TAC o SPEC `b:real^2`) THEN
2444 ASM_REWRITE_TAC[IN_SING; ENDS_IN_SEGMENT] THEN ASM SET_TAC[];
2447 `?z:real^2. MEM z p /\
2448 z IN (convex hull {a,b,c} DIFF {a,c}) /\
2450 STRIP_ASSUME_TAC THENL
2452 MAP_EVERY EXISTS_TAC [`b:real^2`; `z:real^2`] THEN
2453 ASM_REWRITE_TAC[MEM] THEN
2454 MATCH_MP_TAC(TAUT `p /\ (p ==> q) ==> p /\ q`) THEN
2455 CONJ_TAC THENL [ASM_MESON_TAC[REAL_LT_REFL]; DISCH_TAC] THEN
2456 X_GEN_TAC `w:real^2` THEN DISCH_TAC THEN
2457 MATCH_MP_TAC INSIDE_SAME_COMPONENT THEN
2458 EXISTS_TAC `d:real^2` THEN ASM_REWRITE_TAC[] THEN
2459 SUBGOAL_THEN `~(z:real^2 = a) /\ ~(z = c)` STRIP_ASSUME_TAC THENL
2460 [ASM SET_TAC[]; ALL_TAC] THEN
2462 `(z:real^2) IN path_image(polygonal_path(CONS c p)) /\
2463 (z:real^2) IN path_image(polygonal_path p)`
2464 STRIP_ASSUME_TAC THENL
2465 [CONJ_TAC THEN MATCH_MP_TAC
2466 (REWRITE_RULE[SUBSET] VERTICES_IN_PATH_IMAGE_POLYGONAL_PATH) THEN
2467 ASM_REWRITE_TAC[IN_SET_OF_LIST; MEM];
2469 SUBGOAL_THEN `~(z IN segment[a:real^2,b]) /\ ~(z IN segment[b,c])`
2470 STRIP_ASSUME_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
2471 SUBGOAL_THEN `~collinear{b:real^2,a,z} /\ ~collinear{b,c,z}`
2472 STRIP_ASSUME_TAC THENL
2473 [ASM_SIMP_TAC[COLLINEAR_3_AFFINE_HULL] THEN
2474 MATCH_MP_TAC(SET_RULE
2475 `!c. x IN c /\ ~(x IN (a INTER c)) /\ ~(x IN (b INTER c))
2476 ==> ~(x IN a) /\ ~(x IN b)`) THEN
2477 EXISTS_TAC `convex hull {a:real^2,b,c}` THEN
2478 CONJ_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
2479 ASM_SIMP_TAC[GSYM AFFINE_INDEPENDENT_CONVEX_AFFINE_HULL;
2480 INSERT_SUBSET; EMPTY_SUBSET; IN_INSERT] THEN
2481 ASM_REWRITE_TAC[GSYM SEGMENT_CONVEX_HULL] THEN
2482 ONCE_REWRITE_TAC[SEGMENT_SYM] THEN ASM_REWRITE_TAC[];
2485 `segment(b:real^2,z) INTER segment[a,b] = {} /\
2486 segment(b,z) INTER segment[b,c] = {}`
2487 STRIP_ASSUME_TAC THENL
2488 [REWRITE_TAC[EXTENSION; IN_INTER; NOT_IN_EMPTY] THEN
2489 CONJ_TAC THEN X_GEN_TAC `v:real^2` THEN STRIP_TAC THENL
2490 [UNDISCH_TAC `~collinear{b:real^2,a,z}`;
2491 UNDISCH_TAC `~collinear{b:real^2,c,z}`] THEN
2493 ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {b,a,c}`] THEN
2494 MATCH_MP_TAC COLLINEAR_3_TRANS THEN
2495 EXISTS_TAC `v:real^2` THEN
2496 UNDISCH_TAC `v IN segment(b:real^2,z)` THEN
2497 REWRITE_TAC[open_segment; IN_DIFF; IN_INSERT; NOT_IN_EMPTY] THEN
2498 REWRITE_TAC[DE_MORGAN_THM; IMP_CONJ] THENL
2499 [UNDISCH_TAC `v IN segment[a:real^2,b]`;
2500 UNDISCH_TAC `v IN segment[b:real^2,c]`] THEN
2501 ONCE_REWRITE_TAC[IMP_IMP] THEN REWRITE_TAC[GSYM BETWEEN_IN_SEGMENT] THEN
2502 DISCH_THEN(CONJUNCTS_THEN(MP_TAC o MATCH_MP BETWEEN_IMP_COLLINEAR)) THEN
2503 REWRITE_TAC[INSERT_AC] THEN SIMP_TAC[];
2505 SUBGOAL_THEN `segment[b:real^2,z] SUBSET convex hull {a,b,c}`
2507 [REWRITE_TAC[SEGMENT_CONVEX_HULL] THEN MATCH_MP_TAC HULL_MINIMAL THEN
2508 REWRITE_TAC[CONVEX_CONVEX_HULL; INSERT_SUBSET; EMPTY_SUBSET] THEN
2509 SIMP_TAC[HULL_INC; IN_INSERT] THEN ASM SET_TAC[];
2511 SUBGOAL_THEN `segment(b:real^2,z) SUBSET convex hull {a,b,c}`
2513 [REWRITE_TAC[open_segment] THEN ASM SET_TAC[]; ALL_TAC] THEN
2515 `segment(b:real^2,z) INTER path_image(polygonal_path(CONS c p)) = {}`
2517 [REWRITE_TAC[EXTENSION; IN_INTER; NOT_IN_EMPTY] THEN
2518 X_GEN_TAC `v:real^2` THEN STRIP_TAC THEN
2519 SUBGOAL_THEN `m <= n dot (v - b:real^2)` MP_TAC THENL
2520 [FIRST_X_ASSUM MATCH_MP_TAC THEN ASM SET_TAC[]; ALL_TAC] THEN
2521 REWRITE_TAC[REAL_NOT_LE] THEN
2522 UNDISCH_TAC `v IN segment(b:real^2,z)` THEN REWRITE_TAC[IN_SEGMENT] THEN
2523 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
2524 DISCH_THEN(X_CHOOSE_THEN `t:real` STRIP_ASSUME_TAC) THEN
2525 ASM_REWRITE_TAC[DOT_RMUL; VECTOR_ARITH
2526 `((&1 - t) % a + t % b) - a:real^N = t % (b - a)`] THEN
2527 ONCE_REWRITE_TAC[REAL_ARITH `t * m < m <=> &0 < m * (&1 - t)`] THEN
2528 MATCH_MP_TAC REAL_LT_MUL THEN ASM_REWRITE_TAC[REAL_SUB_LT];
2530 SUBGOAL_THEN `segment(b:real^2,z) SUBSET interior(convex hull {a,b,c})`
2532 [MATCH_MP_TAC SUBSET_TRANS THEN EXISTS_TAC
2533 `(convex hull {a:real^2,b,c}) DIFF frontier(convex hull {a,b,c})` THEN
2536 REWRITE_TAC[frontier] THEN MATCH_MP_TAC(SET_RULE
2537 `s SUBSET u ==> s DIFF (u DIFF t) SUBSET t`) THEN
2538 REWRITE_TAC[CLOSURE_SUBSET]] THEN
2539 REWRITE_TAC[FRONTIER_OF_TRIANGLE] THEN MATCH_MP_TAC(SET_RULE
2540 `s INTER a = {} /\ s INTER b = {} /\ s INTER c = {} /\ s SUBSET u
2541 ==> s SUBSET u DIFF (a UNION b UNION c)`) THEN
2542 ASM_REWRITE_TAC[] THEN
2543 REWRITE_TAC[EXTENSION; IN_INTER; NOT_IN_EMPTY] THEN
2544 X_GEN_TAC `v:real^2` THEN REWRITE_TAC[IN_SEGMENT] THEN
2545 DISCH_THEN(CONJUNCTS_THEN2
2546 (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) MP_TAC) THEN
2547 DISCH_THEN(X_CHOOSE_THEN `s:real` STRIP_ASSUME_TAC) THEN
2548 ASM_REWRITE_TAC[NOT_EXISTS_THM] THEN X_GEN_TAC `t:real` THEN
2549 REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
2550 DISCH_THEN(MP_TAC o AP_TERM `\x:real^2. n dot (x - b)`) THEN
2551 REWRITE_TAC[VECTOR_ARITH
2552 `((&1 - u) % c + u % a) - b =
2553 (&1 - u) % (c - b) + u % (a - b)`] THEN
2554 ASM_REWRITE_TAC[VECTOR_SUB_REFL; VECTOR_ADD_LID; VECTOR_MUL_RZERO] THEN
2555 ASM_REWRITE_TAC[DOT_RADD; DOT_RMUL] THEN MATCH_MP_TAC(REAL_ARITH
2556 `&0 < m * (&1 - t) /\ m <= x ==> ~((&1 - s) * x + s * x = t * m)`) THEN
2557 ASM_SIMP_TAC[REAL_LT_MUL; REAL_SUB_LT] THEN
2558 FIRST_X_ASSUM MATCH_MP_TAC THEN
2559 SIMP_TAC[IN_INTER; IN_INSERT; HULL_INC] THEN MATCH_MP_TAC
2560 (REWRITE_RULE[SUBSET] VERTICES_IN_PATH_IMAGE_POLYGONAL_PATH) THEN
2561 REWRITE_TAC[set_of_list; IN_INSERT];
2564 `?y:real^2. y IN segment(b,z) /\ y IN interior(convex hull {a',b,c'})`
2565 STRIP_ASSUME_TAC THENL
2566 [REWRITE_TAC[INTER; GSYM(ASSUME
2567 `interior(convex hull {a, b, c}) INTER {x:real^2 | x$2 - b$2 < e} =
2568 interior(convex hull {a', b, c'})`)] THEN
2569 REWRITE_TAC[IN_ELIM_THM] THEN MATCH_MP_TAC(SET_RULE
2570 `(?y. y IN s /\ P y) /\ s SUBSET t
2571 ==> ?y. y IN s /\ y IN t /\ P y`) THEN
2572 ASM_REWRITE_TAC[] THEN ASM_REWRITE_TAC[IN_SEGMENT] THEN EXISTS_TAC
2573 `b + min (&1 / &2) (e / &2 / norm(z - b)) % (z - b):real^2` THEN
2575 [EXISTS_TAC `min (&1 / &2) (e / &2 / norm (z - b:real^2))` THEN
2576 REPEAT CONJ_TAC THENL [ALL_TAC; REAL_ARITH_TAC; VECTOR_ARITH_TAC] THEN
2577 REWRITE_TAC[REAL_LT_MIN] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
2578 ASM_SIMP_TAC[REAL_HALF; REAL_LT_DIV; NORM_POS_LT; VECTOR_SUB_EQ];
2579 REWRITE_TAC[VECTOR_ADD_COMPONENT; REAL_ADD_SUB] THEN
2580 MATCH_MP_TAC(REAL_ARITH
2581 `abs(x$2) <= norm x /\ norm x <= e / &2 /\ &0 < e ==> x$2 < e`) THEN
2582 SIMP_TAC[COMPONENT_LE_NORM; DIMINDEX_2; ARITH] THEN
2583 ASM_REWRITE_TAC[NORM_MUL] THEN
2584 ASM_SIMP_TAC[GSYM REAL_LE_RDIV_EQ; NORM_POS_LT; VECTOR_SUB_EQ] THEN
2585 MATCH_MP_TAC(REAL_ARITH `&0 <= x ==> abs(min (&1 / &2) x) <= x`) THEN
2586 MATCH_MP_TAC REAL_LT_IMP_LE THEN MATCH_MP_TAC REAL_LT_DIV THEN
2587 ASM_REWRITE_TAC[REAL_HALF; NORM_POS_LT; VECTOR_SUB_EQ]];
2589 MATCH_MP_TAC CONNECTED_COMPONENT_TRANS THEN EXISTS_TAC `y:real^2` THEN
2591 [REWRITE_TAC[connected_component] THEN
2592 EXISTS_TAC `interior(convex hull {a':real^2,b,c'})` THEN
2593 ASM_REWRITE_TAC[] THEN
2594 SIMP_TAC[CONVEX_CONNECTED; CONVEX_INTERIOR; CONVEX_CONVEX_HULL] THEN
2595 SIMP_TAC[PATH_IMAGE_JOIN; PATHSTART_JOIN; PATHSTART_LINEPATH;
2596 PATHFINISH_LINEPATH; PATHSTART_POLYGONAL_PATH; NOT_CONS_NIL; HD] THEN
2597 REWRITE_TAC[SET_RULE `s SUBSET UNIV DIFF (a UNION b UNION c) <=>
2598 s INTER a = {} /\ s INTER b = {} /\ s INTER c = {}`] THEN
2599 REPEAT CONJ_TAC THENL
2600 [MATCH_MP_TAC(SET_RULE
2601 `!t. s SUBSET t /\ t INTER u = {} ==> s INTER u = {}`) THEN
2602 EXISTS_TAC `interior(convex hull {a:real^2,b,c})` THEN
2603 ASM_SIMP_TAC[SUBSET_INTERIOR] THEN
2604 MP_TAC(ISPECL [`a:real^2`; `b:real^2`; `c:real^2`]
2605 FRONTIER_OF_TRIANGLE) THEN
2606 REWRITE_TAC[PATH_IMAGE_LINEPATH; frontier] THEN
2607 MATCH_MP_TAC(SET_RULE
2608 `!s. i SUBSET s /\ s SUBSET c
2609 ==> c DIFF i = a UNION b ==> i INTER a = {}`) THEN
2610 EXISTS_TAC `convex hull {a:real^2,b,c}` THEN
2611 REWRITE_TAC[INTERIOR_SUBSET; CLOSURE_SUBSET];
2612 MATCH_MP_TAC(SET_RULE
2613 `!t. s SUBSET t /\ t INTER u = {} ==> s INTER u = {}`) THEN
2614 EXISTS_TAC `interior(convex hull {a:real^2,b,c})` THEN
2615 ASM_SIMP_TAC[SUBSET_INTERIOR] THEN
2616 MP_TAC(ISPECL [`a:real^2`; `b:real^2`; `c:real^2`]
2617 FRONTIER_OF_TRIANGLE) THEN
2618 REWRITE_TAC[PATH_IMAGE_LINEPATH; frontier] THEN
2619 MATCH_MP_TAC(SET_RULE
2620 `!s. i SUBSET s /\ s SUBSET c
2621 ==> c DIFF i = a UNION b UNION d ==> i INTER b = {}`) THEN
2622 EXISTS_TAC `convex hull {a:real^2,b,c}` THEN
2623 REWRITE_TAC[INTERIOR_SUBSET; CLOSURE_SUBSET];
2624 MATCH_MP_TAC(SET_RULE
2625 `!t. s SUBSET t /\ u INTER t = {} ==> s INTER u = {}`) THEN
2626 EXISTS_TAC `{x | (x:real^2)$2 - (b:real^2)$2 < e}` THEN
2627 CONJ_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
2628 REWRITE_TAC[SET_RULE `s INTER t = {} <=> s SUBSET (UNIV DIFF t)`] THEN
2629 REWRITE_TAC[SUBSET; IN_DIFF; IN_ELIM_THM; REAL_NOT_LT; IN_UNIV] THEN
2630 MP_TAC(ISPEC `CONS (c:real^2) p`
2631 PATH_IMAGE_POLYGONAL_PATH_SUBSET_CONVEX_HULL) THEN
2632 REWRITE_TAC[NOT_CONS_NIL] THEN
2633 MATCH_MP_TAC(SET_RULE
2634 `t SUBSET {x | P x} ==> s SUBSET t ==> !x. x IN s ==> P x`) THEN
2635 REWRITE_TAC[REAL_ARITH `e <= x - b <=> x >= b + e`] THEN
2636 SIMP_TAC[SUBSET_HULL; CONVEX_HALFSPACE_COMPONENT_GE] THEN
2637 REWRITE_TAC[set_of_list; REAL_ARITH `x >= b + e <=> e <= x - b`] THEN
2638 ASM_REWRITE_TAC[INSERT_SUBSET; IN_ELIM_THM] THEN
2639 ASM_REWRITE_TAC[SUBSET; IN_SET_OF_LIST; IN_ELIM_THM]];
2640 REWRITE_TAC[connected_component] THEN
2641 EXISTS_TAC `segment(b:real^2,z)` THEN ASM_REWRITE_TAC[] THEN
2642 REWRITE_TAC[CONNECTED_SEGMENT] THEN
2643 SIMP_TAC[PATH_IMAGE_JOIN; PATHSTART_JOIN; PATHSTART_LINEPATH;
2644 PATHFINISH_LINEPATH; PATHSTART_POLYGONAL_PATH; NOT_CONS_NIL; HD] THEN
2645 REWRITE_TAC[PATH_IMAGE_LINEPATH] THEN ASM SET_TAC[]]] THEN
2648 MEM u (CONS c p) /\ MEM v (CONS c p) /\
2649 mx IN segment[u,v] /\
2650 segment[u,v] SUBSET path_image(polygonal_path(CONS c p)) /\
2651 ~(a IN segment[u,v] /\ c IN segment[u,v]) /\
2653 STRIP_ASSUME_TAC THENL
2654 [MP_TAC(ISPECL [`CONS (c:real^2) p`; `mx:real^2`]
2655 PATH_IMAGE_POLYGONAL_PATH_SUBSET_SEGMENTS) THEN
2657 [ASM_REWRITE_TAC[LENGTH; ARITH_RULE `3 <= SUC n <=> 2 <= n`] THEN
2660 REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
2661 MAP_EVERY X_GEN_TAC [`u:real^2`; `v:real^2`] THEN
2662 ASM_REWRITE_TAC[PATHSTART_POLYGONAL_PATH; PATHFINISH_POLYGONAL_PATH] THEN
2663 ASM_REWRITE_TAC[NOT_CONS_NIL; LAST; HD] THEN STRIP_TAC THEN
2664 SUBGOAL_THEN `n dot (u - b) <= m \/ n dot (v - b:real^2) <= m`
2665 STRIP_ASSUME_TAC THENL
2666 [REWRITE_TAC[GSYM REAL_NOT_LT; GSYM DE_MORGAN_THM] THEN STRIP_TAC THEN
2667 UNDISCH_TAC `n dot (mx - b:real^2) = m` THEN
2668 UNDISCH_TAC `(mx:real^2) IN segment[u,v]` THEN
2669 REWRITE_TAC[IN_SEGMENT] THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
2670 REWRITE_TAC[VECTOR_ARITH
2671 `((&1 - u) % x + u % y) - a:real^N =
2672 (&1 - u) % (x - a) + u % (y - a)`] THEN
2673 MATCH_MP_TAC(REAL_ARITH `--x < --m ==> ~(x = m)`) THEN
2674 REWRITE_TAC[GSYM DOT_LNEG] THEN REWRITE_TAC[DOT_RADD; DOT_RMUL] THEN
2675 MATCH_MP_TAC REAL_CONVEX_BOUND_LT THEN
2676 ASM_REWRITE_TAC[DOT_LNEG; REAL_LT_NEG2] THEN ASM_REAL_ARITH_TAC;
2677 MAP_EVERY EXISTS_TAC [`u:real^2`; `v:real^2`] THEN ASM_REWRITE_TAC[] THEN
2678 ONCE_REWRITE_TAC[CONJ_SYM] THEN ASM_REWRITE_TAC[];
2679 MAP_EVERY EXISTS_TAC [`v:real^2`; `u:real^2`] THEN
2680 ONCE_REWRITE_TAC[SEGMENT_SYM] THEN ASM_REWRITE_TAC[] THEN
2681 ONCE_REWRITE_TAC[CONJ_SYM] THEN ASM_REWRITE_TAC[]];
2683 ASM_CASES_TAC `n dot (u - b:real^2) < n dot (c - b)` THENL
2684 [SUBGOAL_THEN `~(u:real^2 = a) /\ ~(u = c)` STRIP_ASSUME_TAC THENL
2685 [ASM_MESON_TAC[REAL_LT_REFL]; ALL_TAC] THEN
2686 UNDISCH_TAC `MEM (u:real^2) (CONS c p)` THEN
2687 ASM_REWRITE_TAC[MEM] THEN DISCH_TAC THEN EXISTS_TAC `u:real^2` THEN
2688 ASM_REWRITE_TAC[IN_DIFF; IN_INSERT; NOT_IN_EMPTY] THEN
2689 ASM_CASES_TAC `mx:real^2 = u` THENL [ASM SET_TAC[]; ALL_TAC] THEN
2690 MATCH_MP_TAC(TAUT `(a ==> b) /\ a ==> a /\ b`) THEN CONJ_TAC THENL
2691 [DISCH_TAC THEN ASM_REWRITE_TAC[GSYM REAL_LE_ANTISYM] THEN
2692 FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[IN_INTER] THEN
2693 MATCH_MP_TAC(REWRITE_RULE[SUBSET]
2694 VERTICES_IN_PATH_IMAGE_POLYGONAL_PATH) THEN
2695 ASM_REWRITE_TAC[IN_SET_OF_LIST; MEM];
2698 [`segment(u:real^2,mx)`; `convex hull {a:real^2,b,c}`]
2699 CONNECTED_INTER_FRONTIER) THEN
2700 REWRITE_TAC[CONNECTED_SEGMENT] THEN MATCH_MP_TAC(SET_RULE
2701 `(s SUBSET c ==> u IN c) /\ s INTER f = {} /\ ~(s INTER c = {})
2702 ==> (~(s INTER c = {}) /\ ~(s DIFF c = {}) ==> ~(s INTER f = {}))
2704 REPEAT CONJ_TAC THENL
2706 SUBGOAL_THEN `closure(segment(u:real^2,mx)) SUBSET convex hull {a,b,c}`
2708 [MATCH_MP_TAC CLOSURE_MINIMAL THEN ASM_REWRITE_TAC[] THEN
2709 MATCH_MP_TAC COMPACT_IMP_CLOSED THEN
2710 MATCH_MP_TAC COMPACT_CONVEX_HULL THEN
2711 SIMP_TAC[FINITE_IMP_COMPACT; FINITE_INSERT; FINITE_EMPTY];
2712 ASM_REWRITE_TAC[SUBSET; CLOSURE_SEGMENT] THEN
2713 DISCH_THEN MATCH_MP_TAC THEN REWRITE_TAC[ENDS_IN_SEGMENT]];
2714 REWRITE_TAC[FRONTIER_OF_TRIANGLE] THEN
2715 MATCH_MP_TAC(SET_RULE
2717 s SUBSET t /\ t SUBSET u /\
2718 a IN ca /\ c IN ca /\
2719 ab INTER u SUBSET {a,b} /\ bc INTER u SUBSET {c} /\
2720 ~(b IN u) /\ s INTER ca = {}
2721 ==> s INTER (ab UNION bc UNION ca) = {}`) THEN
2722 MAP_EVERY EXISTS_TAC
2723 [`a:real^2`; `b:real^2`; `c:real^2`; `segment[u:real^2,v]`;
2724 `path_image(polygonal_path(CONS (c:real^2) p))`] THEN
2725 ASM_REWRITE_TAC[ENDS_IN_SEGMENT; SUBSET_SEGMENT] THEN CONJ_TAC THENL
2726 [MP_TAC(ISPEC `CONS (c:real^2) p`
2727 PATH_IMAGE_POLYGONAL_PATH_SUBSET_CONVEX_HULL) THEN
2728 REWRITE_TAC[NOT_CONS_NIL] THEN MATCH_MP_TAC(SET_RULE
2729 `~(x IN t) ==> s SUBSET t ==> ~(x IN s)`) THEN
2730 MATCH_MP_TAC(SET_RULE
2731 `!t. ~(b IN t) /\ s SUBSET t ==> ~(b IN s)`) THEN
2732 EXISTS_TAC `{x:real^2 | (x:real^2)$2 >= (b:real^2)$2 + e}` THEN
2733 ASM_REWRITE_TAC[IN_ELIM_THM; real_ge; REAL_NOT_LE; REAL_LT_ADDR] THEN
2734 MATCH_MP_TAC HULL_MINIMAL THEN
2735 REWRITE_TAC[GSYM real_ge; CONVEX_HALFSPACE_COMPONENT_GE] THEN
2736 REWRITE_TAC[SUBSET; set_of_list; FORALL_IN_INSERT; IN_ELIM_THM] THEN
2737 ASM_REWRITE_TAC[IN_SET_OF_LIST; REAL_ARITH
2738 `x >= b + e <=> e <= x - b`];
2739 REWRITE_TAC[EXTENSION; IN_INTER; NOT_IN_EMPTY] THEN
2740 X_GEN_TAC `y:real^2` THEN REWRITE_TAC[IN_SEGMENT] THEN
2741 DISCH_THEN(CONJUNCTS_THEN MP_TAC) THEN
2742 DISCH_THEN(X_CHOOSE_THEN `s:real` STRIP_ASSUME_TAC) THEN
2743 ASM_REWRITE_TAC[NOT_EXISTS_THM] THEN X_GEN_TAC `t:real` THEN
2744 REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
2745 DISCH_THEN(MP_TAC o AP_TERM `\x:real^2. n dot (x - b)`) THEN
2746 REWRITE_TAC[VECTOR_ARITH
2747 `((&1 - u) % c + u % a) - b =
2748 (&1 - u) % (c - b) + u % (a - b)`] THEN
2749 ASM_REWRITE_TAC[DOT_RADD; DOT_RMUL] THEN MATCH_MP_TAC(REAL_ARITH
2750 `(&1 - t) * a < (&1 - t) * m /\ t * b <= t * m
2751 ==> ~((&1 - s) * m + s * m = (&1 - t) * a + t * b)`) THEN
2752 ASM_SIMP_TAC[REAL_LT_LMUL; REAL_SUB_LT] THEN
2753 MATCH_MP_TAC REAL_LE_LMUL THEN
2754 CONJ_TAC THENL [ASM_REAL_ARITH_TAC; FIRST_X_ASSUM MATCH_MP_TAC] THEN
2755 SIMP_TAC[IN_INTER; HULL_INC; IN_INSERT] THEN
2756 MATCH_MP_TAC(REWRITE_RULE[SUBSET]
2757 VERTICES_IN_PATH_IMAGE_POLYGONAL_PATH) THEN
2758 REWRITE_TAC[set_of_list; IN_INSERT]];
2760 ASM_CASES_TAC `mx IN interior(convex hull {a:real^2,b,c})` THENL
2761 [UNDISCH_TAC `mx IN interior(convex hull {a:real^2,b,c})` THEN
2762 REWRITE_TAC[IN_INTERIOR_CBALL; SUBSET; IN_CBALL] THEN
2763 DISCH_THEN(X_CHOOSE_THEN `ee:real` STRIP_ASSUME_TAC) THEN
2764 REWRITE_TAC[GSYM MEMBER_NOT_EMPTY; IN_INTER] THEN
2765 ONCE_REWRITE_TAC[SEGMENT_SYM] THEN ASM_REWRITE_TAC[IN_SEGMENT] THEN
2767 `(?x. (?u. P u /\ Q u /\ x = f u) /\ R x) <=>
2768 (?u. P u /\ Q u /\ R(f u))`] THEN
2769 EXISTS_TAC `min (&1 / &2) (ee / norm(u - mx:real^2))` THEN
2770 REPEAT CONJ_TAC THENL
2771 [MATCH_MP_TAC(REAL_ARITH `&0 < x ==> &0 < min (&1 / &2) x`) THEN
2772 ASM_SIMP_TAC[REAL_LT_DIV; NORM_POS_LT; VECTOR_SUB_EQ];
2774 FIRST_X_ASSUM MATCH_MP_TAC THEN REWRITE_TAC[dist; VECTOR_ARITH
2775 `a - ((&1 - u) % a + u % b):real^N = u % (a - b)`] THEN
2776 ASM_SIMP_TAC[NORM_MUL; GSYM REAL_LE_RDIV_EQ; NORM_POS_LT;
2778 REWRITE_TAC[NORM_SUB] THEN MATCH_MP_TAC(REAL_ARITH
2779 `&0 < x ==> abs(min (&1 / &2) x) <= x`) THEN
2780 ASM_SIMP_TAC[REAL_LT_DIV; NORM_POS_LT; VECTOR_SUB_EQ]];
2782 MP_TAC(ISPEC `{a:real^2,b,c}` AFFINE_INDEPENDENT_SPAN_EQ) THEN
2784 [ASM_REWRITE_TAC[] THEN
2785 SIMP_TAC[CARD_CLAUSES; FINITE_INSERT; FINITE_EMPTY] THEN
2786 ASM_REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY; DIMINDEX_2] THEN
2787 CONV_TAC NUM_REDUCE_CONV;
2789 GEN_REWRITE_TAC LAND_CONV [EXTENSION] THEN
2790 REWRITE_TAC[AFFINE_HULL_3; IN_UNIV] THEN
2791 DISCH_THEN(MP_TAC o SPEC `u:real^2`) THEN
2792 REWRITE_TAC[IN_ELIM_THM; LEFT_IMP_EXISTS_THM] THEN
2793 MAP_EVERY X_GEN_TAC [`r:real`; `s:real`; `t:real`] THEN STRIP_TAC THEN
2794 SUBGOAL_THEN `mx IN convex hull {a:real^2,b,c}` MP_TAC THENL
2795 [ASM SET_TAC[]; ALL_TAC] THEN
2796 ONCE_REWRITE_TAC[SEGMENT_SYM] THEN REWRITE_TAC[CONVEX_HULL_3] THEN
2797 REWRITE_TAC[GSYM MEMBER_NOT_EMPTY; IN_ELIM_THM] THEN
2798 ONCE_REWRITE_TAC[INTER_COMM] THEN
2799 REWRITE_TAC[IN_INTER; EXISTS_IN_GSPEC] THEN
2800 REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
2801 MAP_EVERY X_GEN_TAC [`rx:real`; `sx:real`; `tx:real`] THEN
2802 ASM_CASES_TAC `rx = &0` THENL
2803 [ASM_REWRITE_TAC[REAL_LE_REFL; REAL_ADD_LID] THEN
2804 REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_LID] THEN STRIP_TAC THEN
2806 `segment[b:real^2,c] INTER path_image(polygonal_path(CONS c p))
2808 REWRITE_TAC[SUBSET] THEN
2809 DISCH_THEN(MP_TAC o SPEC `mx:real^2`) THEN
2810 MATCH_MP_TAC(TAUT `~q /\ p ==> (p ==> q) ==> r`) THEN
2811 REWRITE_TAC[IN_SING] THEN CONJ_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
2812 REWRITE_TAC[IN_INTER; SEGMENT_CONVEX_HULL] THEN
2813 CONJ_TAC THENL [ALL_TAC; ASM SET_TAC[]] THEN
2814 REWRITE_TAC[CONVEX_HULL_2; IN_ELIM_THM] THEN ASM_MESON_TAC[];
2816 ASM_CASES_TAC `rx = &1` THENL
2817 [ASM_REWRITE_TAC[] THEN
2818 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
2819 SUBGOAL_THEN `sx = &0 /\ tx = &0` ASSUME_TAC THENL
2820 [ASM_REAL_ARITH_TAC; ASM_REWRITE_TAC[]] THEN
2821 ASM_REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_MUL_LID; VECTOR_ADD_RID];
2823 ASM_CASES_TAC `tx = &0` THENL
2824 [ASM_REWRITE_TAC[REAL_LE_REFL; REAL_ADD_RID] THEN
2825 REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_RID] THEN STRIP_TAC THEN
2827 `segment[a:real^2,b] INTER path_image(polygonal_path(CONS c p))
2829 REWRITE_TAC[SUBSET] THEN
2830 DISCH_THEN(MP_TAC o SPEC `mx:real^2`) THEN
2831 MATCH_MP_TAC(TAUT `~q /\ p ==> (p ==> q) ==> r`) THEN CONJ_TAC THENL
2832 [REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY; DE_MORGAN_THM] THEN
2833 CONJ_TAC THENL [ASM_MESON_TAC[]; DISCH_THEN SUBST_ALL_TAC] THEN
2834 UNDISCH_TAC `n dot (b - b:real^2) = m` THEN
2835 REWRITE_TAC[VECTOR_SUB_REFL; DOT_RZERO] THEN
2838 REWRITE_TAC[IN_INTER; SEGMENT_CONVEX_HULL] THEN
2839 CONJ_TAC THENL [ALL_TAC; ASM SET_TAC[]] THEN
2840 REWRITE_TAC[CONVEX_HULL_2; IN_ELIM_THM] THEN ASM_MESON_TAC[];
2842 ASM_CASES_TAC `tx = &1` THENL
2843 [ASM_REWRITE_TAC[] THEN
2844 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
2845 SUBGOAL_THEN `sx = &0 /\ rx = &0` ASSUME_TAC THENL
2846 [ASM_REAL_ARITH_TAC; ASM_REWRITE_TAC[]] THEN
2847 ASM_REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_MUL_LID; VECTOR_ADD_LID];
2849 ASM_CASES_TAC `sx = &1` THENL
2850 [ASM_REWRITE_TAC[] THEN
2851 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
2852 SUBGOAL_THEN `rx = &0 /\ tx = &0` ASSUME_TAC THENL
2853 [ASM_REAL_ARITH_TAC; ASM_REWRITE_TAC[]] THEN
2854 ASM_REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_MUL_LID; VECTOR_ADD_LID;
2855 VECTOR_ADD_RID] THEN
2856 DISCH_THEN SUBST_ALL_TAC THEN
2857 UNDISCH_TAC `n dot (b - b:real^2) = m` THEN
2858 REWRITE_TAC[VECTOR_SUB_REFL; DOT_RZERO] THEN
2861 ASM_CASES_TAC `sx = &0` THENL
2864 UNDISCH_TAC `~(mx IN interior(convex hull {a:real^2, b, c}))` THEN
2865 MATCH_MP_TAC(TAUT `p ==> ~p ==> q`) THEN
2866 ASM_SIMP_TAC[INTERIOR_CONVEX_HULL_3] THEN
2867 REWRITE_TAC[IN_ELIM_THM] THEN
2868 MAP_EVERY EXISTS_TAC [`rx:real`; `sx:real`; `tx:real`] THEN
2869 REWRITE_TAC[] THEN ASM_REAL_ARITH_TAC] THEN
2870 UNDISCH_THEN `sx = &0` SUBST_ALL_TAC THEN
2871 REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_LID; REAL_LE_REFL] THEN
2872 REWRITE_TAC[REAL_ADD_LID] THEN STRIP_TAC THEN
2874 `&0 < rx /\ rx < &1 /\ &0 < tx /\ tx < &1`
2875 STRIP_ASSUME_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC] THEN
2876 ASM_REWRITE_TAC[IN_SEGMENT] THEN
2878 `?q. q * (rx - r) <= rx /\
2879 q * (tx - t) <= tx /\
2881 STRIP_ASSUME_TAC THENL
2884 (min (if rx:real = r then &1 / &2 else rx / abs(rx - r))
2885 (if tx:real = t then &1 / &2 else tx / abs(tx - t)))` THEN
2886 REWRITE_TAC[REAL_LT_MIN; REAL_MIN_LT] THEN
2887 CONV_TAC REAL_RAT_REDUCE_CONV THEN REPEAT CONJ_TAC THENL
2888 [ASM_CASES_TAC `r:real = rx` THENL
2889 [ASM_REWRITE_TAC[REAL_SUB_REFL; REAL_MUL_RZERO]; ALL_TAC] THEN
2890 MATCH_MP_TAC(REAL_ARITH `abs x <= a ==> x <= a`) THEN
2891 REWRITE_TAC[REAL_ABS_MUL] THEN
2892 ASM_SIMP_TAC[GSYM REAL_LE_RDIV_EQ; REAL_ARITH
2893 `~(x = y) ==> &0 < abs(x - y)`] THEN
2894 MATCH_MP_TAC(REAL_ARITH
2895 `&0 <= a /\ &0 <= x /\ &0 <= b ==> abs(min a (min x b)) <= x`) THEN
2896 CONV_TAC REAL_RAT_REDUCE_CONV THEN
2897 COND_CASES_TAC THEN ASM_SIMP_TAC[REAL_LE_DIV; REAL_ABS_POS] THEN
2898 CONV_TAC REAL_RAT_REDUCE_CONV;
2899 ASM_CASES_TAC `t:real = tx` THENL
2900 [ASM_REWRITE_TAC[REAL_SUB_REFL; REAL_MUL_RZERO]; ALL_TAC] THEN
2901 MATCH_MP_TAC(REAL_ARITH `abs x <= a ==> x <= a`) THEN
2902 REWRITE_TAC[REAL_ABS_MUL] THEN
2903 ASM_SIMP_TAC[GSYM REAL_LE_RDIV_EQ; REAL_ARITH
2904 `~(x = y) ==> &0 < abs(x - y)`] THEN
2905 MATCH_MP_TAC(REAL_ARITH
2906 `&0 <= a /\ &0 <= x /\ &0 <= b ==> abs(min a (min b x)) <= x`) THEN
2907 CONV_TAC REAL_RAT_REDUCE_CONV THEN
2908 COND_CASES_TAC THEN ASM_SIMP_TAC[REAL_LE_DIV; REAL_ABS_POS] THEN
2909 CONV_TAC REAL_RAT_REDUCE_CONV;
2910 COND_CASES_TAC THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
2911 MATCH_MP_TAC REAL_LT_DIV THEN ASM_REAL_ARITH_TAC;
2912 COND_CASES_TAC THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
2913 MATCH_MP_TAC REAL_LT_DIV THEN ASM_REAL_ARITH_TAC];
2915 MAP_EVERY EXISTS_TAC
2916 [`(&1 - q) * rx + q * r`;
2918 `(&1 - q) * tx + q * t:real`] THEN
2919 REWRITE_TAC[CONJ_ASSOC] THEN CONJ_TAC THENL
2921 EXISTS_TAC `q:real` THEN ASM_REWRITE_TAC[] THEN VECTOR_ARITH_TAC] THEN
2922 REWRITE_TAC[REAL_ARITH
2923 `((&1 - q) * rx + q * r) +
2925 ((&1 - q) * tx + q * t) =
2926 (rx + tx) + q * ((r + s + t) - (rx + tx))`] THEN
2927 ASM_REWRITE_TAC[] THEN CONJ_TAC THENL [ALL_TAC; REAL_ARITH_TAC] THEN
2928 REWRITE_TAC[REAL_ARITH
2929 `&0 <= (&1 - q) * r + q * s <=> q * (r - s) <= r`] THEN
2930 ASM_REWRITE_TAC[] THEN MATCH_MP_TAC REAL_LE_MUL THEN
2931 ASM_SIMP_TAC[REAL_LT_IMP_LE] THEN
2932 UNDISCH_TAC `n dot (u - b:real^2) < n dot (c - b)` THEN
2933 ASM_REWRITE_TAC[VECTOR_ARITH
2934 `(r % a + s % b + t % c) - b =
2935 r % (a - b) + t % (c - b) + ((r + s + t) - &1) % b`] THEN
2936 REWRITE_TAC[REAL_SUB_REFL; VECTOR_MUL_LZERO; VECTOR_ADD_RID] THEN
2937 ASM_REWRITE_TAC[DOT_RADD; DOT_RMUL] THEN
2938 REWRITE_TAC[REAL_ARITH
2939 `r * x + s * x < x <=> &0 < (&1 - r - s) * x`] THEN
2940 ASM_SIMP_TAC[REAL_LT_MUL_EQ] THEN ASM_REAL_ARITH_TAC;
2942 SUBGOAL_THEN `n dot (u - b) = m /\ n dot (c - b) = m` MP_TAC THENL
2943 [MATCH_MP_TAC(REAL_ARITH
2944 `!mx. n dot (u - b) <= m /\
2945 ~(n dot (u - b) < n dot (c - b)) /\
2946 n dot (mx - b) = m /\
2947 n dot (mx - b) <= n dot (c - b)
2948 ==> n dot (u - b) = m /\ n dot (c - b) = m`) THEN
2949 EXISTS_TAC `mx:real^2` THEN ASM_REWRITE_TAC[] THEN
2950 FIRST_X_ASSUM MATCH_MP_TAC THEN
2951 SIMP_TAC[IN_INTER; HULL_INC; IN_INSERT] THEN
2952 MATCH_MP_TAC(REWRITE_RULE[SUBSET]
2953 VERTICES_IN_PATH_IMAGE_POLYGONAL_PATH) THEN
2954 REWRITE_TAC[set_of_list; IN_INSERT];
2956 DISCH_THEN(CONJUNCTS_THEN
2957 (fun th -> SUBST_ALL_TAC th THEN ASSUME_TAC th)) THEN
2958 MAP_EVERY (C UNDISCH_THEN (K ALL_TAC)) [`m <= m`; `~(m < m)`] THEN
2960 `collinear {a:real^2,mx,c} /\ collinear {a,u,c}`
2961 STRIP_ASSUME_TAC THENL
2963 `!y:real^2. n dot (y - b) = m ==> collinear {a,y,c}`
2964 (fun th -> CONJ_TAC THEN MATCH_MP_TAC th THEN ASM_REWRITE_TAC[]) THEN
2965 X_GEN_TAC `y:real^2` THEN DISCH_TAC THEN
2966 ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {a,c,b}`] THEN
2967 ONCE_REWRITE_TAC[COLLINEAR_3] THEN
2968 MATCH_MP_TAC ORTHOGONAL_TO_ORTHOGONAL_2D THEN
2969 EXISTS_TAC `n:real^2` THEN ASM_REWRITE_TAC[] THEN
2970 ONCE_REWRITE_TAC[GSYM ORTHOGONAL_RNEG] THEN
2971 ASM_REWRITE_TAC[VECTOR_NEG_SUB] THEN
2972 MAP_EVERY UNDISCH_TAC
2973 [`n dot (y - b:real^2) = m`; `n dot (c - b:real^2) = m`] THEN
2974 REWRITE_TAC[orthogonal; DOT_RSUB] THEN REAL_ARITH_TAC;
2976 ASM_CASES_TAC `mx:real^2 = u` THENL
2977 [UNDISCH_THEN `mx:real^2 = u` SUBST_ALL_TAC THEN
2978 UNDISCH_TAC `MEM (u:real^2) (CONS c p)` THEN
2979 ASM_REWRITE_TAC[MEM] THEN DISCH_TAC THEN EXISTS_TAC `u:real^2` THEN
2980 ASM_REWRITE_TAC[IN_DIFF; IN_INSERT; NOT_IN_EMPTY] THEN
2983 ASM_CASES_TAC `mx:real^2 = v` THENL
2984 [UNDISCH_THEN `mx:real^2 = v` SUBST_ALL_TAC THEN
2985 UNDISCH_TAC `MEM (v:real^2) (CONS c p)` THEN
2986 ASM_REWRITE_TAC[MEM] THEN DISCH_TAC THEN EXISTS_TAC `v:real^2` THEN
2987 ASM_REWRITE_TAC[IN_DIFF; IN_INSERT; NOT_IN_EMPTY] THEN
2990 SUBGOAL_THEN `collinear {a:real^2,c,mx,u}` ASSUME_TAC THENL
2991 [ASM_SIMP_TAC[COLLINEAR_4_3] THEN
2992 ONCE_REWRITE_TAC[SET_RULE `{a,c,b} = {a,b,c}`] THEN ASM_REWRITE_TAC[];
2994 SUBGOAL_THEN `collinear {a:real^2,u,v}` ASSUME_TAC THENL
2995 [MATCH_MP_TAC COLLINEAR_3_TRANS THEN EXISTS_TAC `mx:real^2` THEN
2996 ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
2997 [MATCH_MP_TAC COLLINEAR_SUBSET THEN
2998 EXISTS_TAC `{a:real^2,c,mx,u}` THEN ASM_REWRITE_TAC[] THEN SET_TAC[];
2999 MATCH_MP_TAC BETWEEN_IMP_COLLINEAR THEN
3000 ASM_REWRITE_TAC[BETWEEN_IN_SEGMENT]];
3002 SUBGOAL_THEN `collinear {c:real^2,u,v}` ASSUME_TAC THENL
3003 [MATCH_MP_TAC COLLINEAR_3_TRANS THEN EXISTS_TAC `mx:real^2` THEN
3004 ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
3005 [MATCH_MP_TAC COLLINEAR_SUBSET THEN
3006 EXISTS_TAC `{a:real^2,c,mx,u}` THEN ASM_REWRITE_TAC[] THEN SET_TAC[];
3007 MATCH_MP_TAC BETWEEN_IMP_COLLINEAR THEN
3008 ASM_REWRITE_TAC[BETWEEN_IN_SEGMENT]];
3010 ASM_CASES_TAC `u:real^2 = v` THENL
3011 [UNDISCH_THEN `u:real^2 = v` SUBST_ALL_TAC THEN
3012 ASM_MESON_TAC[SEGMENT_REFL; IN_SING];
3014 SUBGOAL_THEN `collinear {a:real^2,v,c}` ASSUME_TAC THENL
3015 [MATCH_MP_TAC COLLINEAR_3_TRANS THEN EXISTS_TAC `u:real^2` THEN
3016 RULE_ASSUM_TAC(REWRITE_RULE[INSERT_AC]) THEN
3017 ASM_REWRITE_TAC[INSERT_AC];
3019 MP_TAC(ISPECL [`a:real^2`; `c:real^2`; `u:real^2`; `v:real^2`;
3020 `mx:real^2`] between_lemma) THEN
3021 ASM_REWRITE_TAC[] THEN ANTS_TAC THENL
3023 [W(MP_TAC o PART_MATCH (lhs o rand) COLLINEAR_TRIPLES o snd) THEN
3024 ASM_REWRITE_TAC[FORALL_IN_INSERT; NOT_IN_EMPTY] THEN
3025 DISCH_THEN SUBST1_TAC THEN
3026 ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {a,c,b}`] THEN
3028 ASM_REWRITE_TAC[open_segment; IN_DIFF; IN_INSERT; NOT_IN_EMPTY] THEN
3029 MP_TAC(ISPECL [`{a:real^2,b,c}`; `{a:real^2,c}`]
3030 AFFINE_INDEPENDENT_CONVEX_AFFINE_HULL) THEN
3031 ASM_REWRITE_TAC[SEGMENT_CONVEX_HULL] THEN
3032 ANTS_TAC THENL [SET_TAC[]; DISCH_THEN SUBST1_TAC] THEN
3033 REWRITE_TAC[IN_INTER] THEN CONJ_TAC THENL [ALL_TAC; ASM SET_TAC[]] THEN
3034 ASM_SIMP_TAC[GSYM COLLINEAR_3_AFFINE_HULL] THEN
3035 MATCH_MP_TAC COLLINEAR_SUBSET THEN
3036 EXISTS_TAC `{a:real^2,c,mx,u}` THEN
3037 ASM_REWRITE_TAC[] THEN SET_TAC[]];
3040 [EXISTS_TAC `u:real^2` THEN
3041 MP_TAC(ASSUME `u IN segment(a:real^2,c)`) THEN
3042 REWRITE_TAC[open_segment; IN_DIFF; IN_INSERT; NOT_IN_EMPTY] THEN
3043 REWRITE_TAC[DE_MORGAN_THM] THEN STRIP_TAC THEN
3044 UNDISCH_TAC `MEM (u:real^2) (CONS c p)` THEN
3045 ASM_REWRITE_TAC[MEM] THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
3046 UNDISCH_TAC `(u:real^2) IN segment[a,c]` THEN
3047 REWRITE_TAC[SEGMENT_CONVEX_HULL] THEN
3048 SPEC_TAC(`u:real^2`,`u:real^2`) THEN REWRITE_TAC[GSYM SUBSET] THEN
3049 MATCH_MP_TAC HULL_MONO THEN SET_TAC[];
3050 EXISTS_TAC `v:real^2` THEN
3051 MP_TAC(ASSUME `v IN segment(a:real^2,c)`) THEN
3052 REWRITE_TAC[open_segment; IN_DIFF; IN_INSERT; NOT_IN_EMPTY] THEN
3053 REWRITE_TAC[DE_MORGAN_THM] THEN STRIP_TAC THEN
3054 UNDISCH_TAC `MEM (v:real^2) (CONS c p)` THEN
3055 ASM_REWRITE_TAC[MEM] THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
3057 [UNDISCH_TAC `(v:real^2) IN segment[a,c]` THEN
3058 REWRITE_TAC[SEGMENT_CONVEX_HULL] THEN
3059 SPEC_TAC(`v:real^2`,`v:real^2`) THEN REWRITE_TAC[GSYM SUBSET] THEN
3060 MATCH_MP_TAC HULL_MONO THEN SET_TAC[];
3061 UNDISCH_TAC `collinear {a:real^2, v, c}` THEN
3062 ONCE_REWRITE_TAC[SET_RULE `{a,v,c} = {a,c,v}`] THEN
3063 ASM_SIMP_TAC[COLLINEAR_3_AFFINE_HULL] THEN
3064 REWRITE_TAC[AFFINE_HULL_2; IN_ELIM_THM] THEN
3065 STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
3066 REWRITE_TAC[VECTOR_ARITH
3067 `(u % a + v % c) - b:real^N =
3068 u % (a - b) + v % (c - b) + ((u + v) - &1) % b`] THEN
3069 ASM_REWRITE_TAC[DOT_RADD; DOT_RMUL; REAL_SUB_REFL] THEN
3070 ASM_REWRITE_TAC[REAL_MUL_LZERO; REAL_ADD_RID; GSYM REAL_ADD_RDISTRIB;
3072 UNDISCH_TAC `segment[a:real^2,c] SUBSET segment[u,v]` THEN
3073 ASM_REWRITE_TAC[SUBSET_SEGMENT]]);;
3075 (* ------------------------------------------------------------------------- *)
3076 (* Hence the final Pick theorem by induction on number of polygon segments. *)
3077 (* ------------------------------------------------------------------------- *)
3081 (!x. MEM x p ==> integral_vector x) /\
3082 simple_path (polygonal_path p) /\
3083 pathfinish (polygonal_path p) = pathstart (polygonal_path p)
3084 ==> measure(inside(path_image(polygonal_path p))) =
3085 &(CARD {x | x IN inside(path_image(polygonal_path p)) /\
3086 integral_vector x}) +
3087 &(CARD {x | x IN path_image(polygonal_path p) /\
3088 integral_vector x}) / &2 - &1`,
3089 GEN_TAC THEN WF_INDUCT_TAC `LENGTH(p:(real^2)list)` THEN DISJ_CASES_TAC
3090 (ARITH_RULE `LENGTH(p:(real^2)list) <= 4 \/ 5 <= LENGTH p`) THENL
3091 [UNDISCH_TAC `LENGTH(p:(real^2)list) <= 4` THEN
3092 POP_ASSUM(K ALL_TAC) THEN SPEC_TAC(`p:(real^2)list`,`p:(real^2)list`) THEN
3093 MATCH_MP_TAC list_INDUCT THEN
3094 REWRITE_TAC[polygonal_path; SIMPLE_PATH_LINEPATH_EQ] THEN
3095 X_GEN_TAC `a:real^2` THEN MATCH_MP_TAC list_INDUCT THEN
3096 REWRITE_TAC[polygonal_path; SIMPLE_PATH_LINEPATH_EQ] THEN
3097 X_GEN_TAC `b:real^2` THEN MATCH_MP_TAC list_INDUCT THEN CONJ_TAC THENL
3098 [REWRITE_TAC[polygonal_path; SIMPLE_PATH_LINEPATH_EQ;
3099 PATHSTART_LINEPATH; PATHFINISH_LINEPATH] THEN
3102 X_GEN_TAC `c:real^2` THEN MATCH_MP_TAC list_INDUCT THEN CONJ_TAC THENL
3103 [REPLICATE_TAC 4 (DISCH_THEN(K ALL_TAC)) THEN
3104 REWRITE_TAC[polygonal_path] THEN
3105 REWRITE_TAC[PATHSTART_JOIN; PATHFINISH_JOIN; PATHSTART_LINEPATH;
3106 PATHFINISH_LINEPATH] THEN
3107 ASM_CASES_TAC `c:real^2 = a` THEN ASM_REWRITE_TAC[] THEN
3108 ASM_SIMP_TAC[SIMPLE_PATH_JOIN_LOOP_EQ; PATHSTART_LINEPATH;
3109 PATHFINISH_LINEPATH] THEN
3110 REWRITE_TAC[ARC_LINEPATH_EQ] THEN
3111 REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
3112 REWRITE_TAC[PATH_IMAGE_LINEPATH] THEN
3113 SUBST1_TAC(ISPECL [`b:real^2`; `a:real^2`] (CONJUNCT1 SEGMENT_SYM)) THEN
3114 REWRITE_TAC[INTER_IDEMPOT] THEN DISCH_THEN(MP_TAC o MATCH_MP
3115 (REWRITE_RULE[IMP_CONJ_ALT] FINITE_SUBSET)) THEN
3116 ASM_REWRITE_TAC[FINITE_SEGMENT; FINITE_INSERT; FINITE_EMPTY];
3118 X_GEN_TAC `d:real^2` THEN MATCH_MP_TAC list_INDUCT THEN CONJ_TAC THENL
3119 [REPLICATE_TAC 5 (DISCH_THEN(K ALL_TAC));
3120 REWRITE_TAC[LENGTH; ARITH_RULE `~(SUC(SUC(SUC(SUC(SUC n)))) <= 4)`]] THEN
3121 REWRITE_TAC[polygonal_path; PATHSTART_JOIN; PATHFINISH_JOIN] THEN
3122 REWRITE_TAC[GSYM IN_SET_OF_LIST; set_of_list] THEN
3123 REWRITE_TAC[FORALL_IN_INSERT; NOT_IN_EMPTY] THEN
3124 REWRITE_TAC[PATHSTART_LINEPATH; PATHFINISH_LINEPATH] THEN
3125 ASM_CASES_TAC `d:real^2 = a` THEN ASM_REWRITE_TAC[] THEN
3126 FIRST_X_ASSUM SUBST1_TAC THEN
3127 DISCH_THEN(CONJUNCTS_THEN2 STRIP_ASSUME_TAC MP_TAC) THEN
3128 SIMP_TAC[SIMPLE_PATH_JOIN_LOOP_EQ; PATH_IMAGE_JOIN; PATHSTART_LINEPATH;
3129 ARC_JOIN_EQ; PATHSTART_JOIN; PATHFINISH_JOIN; PATHFINISH_LINEPATH] THEN
3130 REWRITE_TAC[PATH_IMAGE_LINEPATH] THEN REWRITE_TAC[INSIDE_OF_TRIANGLE] THEN
3131 REWRITE_TAC[GSYM FRONTIER_OF_TRIANGLE] THEN
3132 SIMP_TAC[MEASURE_INTERIOR; NEGLIGIBLE_CONVEX_FRONTIER;
3133 CONVEX_CONVEX_HULL; FINITE_IMP_BOUNDED_CONVEX_HULL;
3134 FINITE_INSERT; FINITE_EMPTY] THEN
3135 ASM_SIMP_TAC[PICK_TRIANGLE] THEN
3136 COND_CASES_TAC THEN ASM_REWRITE_TAC[ARC_LINEPATH_EQ] THEN
3137 MATCH_MP_TAC(TAUT `~p ==> p ==> q`) THEN REWRITE_TAC[UNION_OVER_INTER] THEN
3138 REWRITE_TAC[UNION_SUBSET] THEN STRIP_TAC THEN
3140 `segment[b:real^2,c] INTER segment [c,a] = segment[b,c] \/
3141 segment[b,c] INTER segment [c,a] = segment[c,a] \/
3142 segment[a,b] INTER segment [b,c] = segment[b,c]`
3143 (REPEAT_TCL DISJ_CASES_THEN SUBST_ALL_TAC) THENL
3144 [REWRITE_TAC[SET_RULE `s INTER t = s <=> s SUBSET t`;
3145 SET_RULE `s INTER t = t <=> t SUBSET s`] THEN
3146 FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [COLLINEAR_BETWEEN_CASES]) THEN
3147 REWRITE_TAC[SUBSET_SEGMENT; BETWEEN_IN_SEGMENT; ENDS_IN_SEGMENT] THEN
3148 REWRITE_TAC[SEGMENT_SYM; DISJ_ACI];
3149 UNDISCH_TAC `segment [b,c] SUBSET {c:real^2}`;
3150 UNDISCH_TAC `segment [c,a] SUBSET {c:real^2}`;
3151 UNDISCH_TAC `segment [b,c] SUBSET {a:real^2, b}`] THEN
3152 DISCH_THEN(MP_TAC o MATCH_MP
3153 (REWRITE_RULE[IMP_CONJ_ALT] FINITE_SUBSET)) THEN
3154 ASM_REWRITE_TAC[FINITE_SEGMENT; FINITE_INSERT; FINITE_EMPTY];
3156 MP_TAC(ISPEC `p:(real^2)list` POLYGON_CHOP_IN_TWO) THEN
3157 ASM_REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
3158 MAP_EVERY X_GEN_TAC [`a:real^2`;`b:real^2`] THEN STRIP_TAC THEN
3162 LENGTH p' = LENGTH p /\
3163 path_image(polygonal_path p') = path_image(polygonal_path p) /\
3164 set_of_list p' = set_of_list p /\
3165 simple_path(polygonal_path p') /\
3166 pathfinish(polygonal_path p') = pathstart(polygonal_path p')`
3167 STRIP_ASSUME_TAC THENL
3168 [MATCH_MP_TAC ROTATE_LIST_TO_FRONT_0 THEN
3169 EXISTS_TAC `p:(real^2)list` THEN ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
3170 [ASM_SIMP_TAC[ARITH_RULE `5 <= p ==> 3 <= p`] THEN
3171 REWRITE_TAC[PATHSTART_POLYGONAL_PATH; PATHFINISH_POLYGONAL_PATH] THEN
3172 GEN_TAC THEN COND_CASES_TAC THEN ASM_SIMP_TAC[LENGTH] THEN
3175 MAP_EVERY UNDISCH_TAC
3176 [`pathfinish(polygonal_path(p:(real^2)list)) =
3177 pathstart(polygonal_path p)`;
3178 `5 <= LENGTH(p:(real^2)list)`] THEN
3179 ASM_CASES_TAC `p:(real^2)list = []` THEN
3180 ASM_REWRITE_TAC[LENGTH; ARITH] THEN
3181 ASM_REWRITE_TAC[PATHSTART_POLYGONAL_PATH; PATHFINISH_POLYGONAL_PATH] THEN
3182 DISCH_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
3183 X_GEN_TAC `l:(real^2)list` THEN
3184 REWRITE_TAC[APPEND_EQ_NIL; NOT_CONS_NIL] THEN
3185 ASM_CASES_TAC `l:(real^2)list = []` THENL
3186 [ASM_MESON_TAC[LENGTH_EQ_NIL]; ALL_TAC] THEN
3187 ASM_REWRITE_TAC[] THEN DISCH_THEN(STRIP_ASSUME_TAC o GSYM) THEN
3188 ASM_REWRITE_TAC[] THEN
3189 SUBGOAL_THEN `~(TL l:(real^2)list = [])` ASSUME_TAC THENL
3190 [DISCH_THEN(MP_TAC o AP_TERM `LENGTH:(real^2)list->num`) THEN
3191 ASM_SIMP_TAC[LENGTH; LENGTH_TL] THEN ASM_ARITH_TAC;
3193 ASM_SIMP_TAC[LAST_APPEND; LENGTH_APPEND; LENGTH_TL; NOT_CONS_NIL] THEN
3194 ASM_REWRITE_TAC[LAST; HD_APPEND; LENGTH] THEN REPEAT CONJ_TAC THENL
3196 MATCH_MP_TAC PATH_IMAGE_POLYGONAL_PATH_ROTATE THEN
3197 ASM_REWRITE_TAC[] THEN ASM_ARITH_TAC;
3198 MAP_EVERY UNDISCH_TAC
3199 [`HD(l:(real^2)list) = LAST l`; `5 <= LENGTH(p:(real^2)list)`;
3200 `~(l:(real^2)list = [])`] THEN
3201 ASM_REWRITE_TAC[] THEN
3202 SPEC_TAC(`l:(real^2)list`,`l:(real^2)list`) THEN
3203 LIST_INDUCT_TAC THEN REWRITE_TAC[HD; TL; APPEND] THEN
3204 REWRITE_TAC[SET_OF_LIST_APPEND; set_of_list] THEN
3205 REPEAT STRIP_TAC THEN MATCH_MP_TAC(SET_RULE
3206 `a IN s /\ b IN s ==> s UNION {a} = b INSERT s`) THEN
3207 ASM_REWRITE_TAC[LAST] THEN ONCE_ASM_REWRITE_TAC[] THEN
3208 REWRITE_TAC[LAST] THEN UNDISCH_TAC `5 <= LENGTH(CONS (h:real^2) t)` THEN
3209 COND_CASES_TAC THEN ASM_REWRITE_TAC[LENGTH; ARITH] THEN
3210 REWRITE_TAC[IN_SET_OF_LIST; MEM_EXISTS_EL; LENGTH] THEN
3211 DISCH_TAC THEN CONJ_TAC THENL
3212 [EXISTS_TAC `0` THEN REWRITE_TAC[EL] THEN ASM_ARITH_TAC;
3213 EXISTS_TAC `LENGTH(t:(real^2)list) - 1` THEN
3214 ASM_SIMP_TAC[LAST_EL] THEN ASM_ARITH_TAC];
3215 MP_TAC(ISPEC `l:(real^2)list` SIMPLE_PATH_POLYGONAL_PATH_ROTATE) THEN
3216 ASM_REWRITE_TAC[] THEN DISCH_THEN MATCH_MP_TAC THEN ASM_ARITH_TAC];
3218 SUBGOAL_THEN `!x:real^2. MEM x p <=> MEM x p'`
3219 (fun th -> REWRITE_TAC[th] THEN
3220 RULE_ASSUM_TAC(REWRITE_RULE[th]))
3221 THENL [ASM_REWRITE_TAC[GSYM IN_SET_OF_LIST]; ALL_TAC] THEN
3222 MAP_EVERY (C UNDISCH_THEN (SUBST_ALL_TAC o SYM))
3223 [`set_of_list(p':(real^2)list) = set_of_list p`;
3224 `path_image(polygonal_path(p':(real^2)list)) =
3225 path_image (polygonal_path p)`;
3226 `LENGTH(p':(real^2)list) = LENGTH(p:(real^2)list)`] THEN
3227 MAP_EVERY (C UNDISCH_THEN (K ALL_TAC))
3228 [`simple_path(polygonal_path(p:(real^2)list))`;
3229 `pathfinish(polygonal_path(p:(real^2)list)) =
3230 pathstart(polygonal_path p)`] THEN
3231 POP_ASSUM_LIST(MP_TAC o end_itlist CONJ o rev) THEN
3232 SPEC_TAC(`p':(real^2)list`,`p:(real^2)list`) THEN
3233 GEN_TAC THEN STRIP_TAC THEN
3235 `?q r. 2 <= LENGTH q /\ 2 <= LENGTH r /\
3236 LENGTH q + LENGTH r = LENGTH p + 1 /\
3237 set_of_list q UNION set_of_list r = set_of_list p /\
3238 pathstart(polygonal_path q) = pathstart(polygonal_path p) /\
3239 pathfinish(polygonal_path q) = (b:real^2) /\
3240 pathstart(polygonal_path r) = b /\
3241 pathfinish(polygonal_path r) = pathfinish(polygonal_path p) /\
3242 simple_path(polygonal_path q ++ polygonal_path r) /\
3243 path_image(polygonal_path q ++ polygonal_path r) =
3244 path_image(polygonal_path p)`
3245 STRIP_ASSUME_TAC THENL
3247 `simple_path(polygonal_path p) /\
3248 2 <= LENGTH p /\ MEM (b:real^2) p /\
3249 ~(pathstart(polygonal_path p) = b) /\
3250 ~(pathfinish(polygonal_path p) = b)`
3252 [ASM_SIMP_TAC[ARITH_RULE `5 <= p ==> 2 <= p`] THEN
3253 ASM_REWRITE_TAC[PATHSTART_POLYGONAL_PATH; CONJ_ASSOC] THEN
3254 COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[MEM];
3255 POP_ASSUM_LIST(K ALL_TAC)] THEN
3256 WF_INDUCT_TAC `LENGTH(p:(real^2)list)` THEN POP_ASSUM MP_TAC THEN
3257 SPEC_TAC(`p:(real^2)list`,`p:(real^2)list`) THEN
3258 MATCH_MP_TAC list_INDUCT THEN REWRITE_TAC[LENGTH; ARITH] THEN
3259 X_GEN_TAC `a:real^2` THEN
3260 MATCH_MP_TAC list_INDUCT THEN REWRITE_TAC[LENGTH; ARITH] THEN
3261 X_GEN_TAC `x:real^2` THEN
3262 MATCH_MP_TAC list_INDUCT THEN CONJ_TAC THENL
3263 [REWRITE_TAC[polygonal_path; PATHSTART_LINEPATH; PATHFINISH_LINEPATH;
3266 REWRITE_TAC[LENGTH; ARITH]] THEN
3267 MAP_EVERY X_GEN_TAC [`y:real^2`; `l:(real^2)list`] THEN
3268 REPLICATE_TAC 3 (DISCH_THEN(K ALL_TAC)) THEN DISCH_TAC THEN
3269 REWRITE_TAC[polygonal_path] THEN
3270 REWRITE_TAC[PATHSTART_JOIN; PATHFINISH_JOIN] THEN
3271 REWRITE_TAC[PATHSTART_LINEPATH; PATHFINISH_LINEPATH] THEN
3272 ONCE_REWRITE_TAC[MEM] THEN
3273 ASM_CASES_TAC `a:real^2 = b` THEN ASM_REWRITE_TAC[] THEN
3274 ONCE_REWRITE_TAC[MEM] THEN
3275 ASM_CASES_TAC `x:real^2 = b` THEN ASM_REWRITE_TAC[] THENL
3276 [FIRST_X_ASSUM(K ALL_TAC o check is_forall o concl) THEN STRIP_TAC THEN
3277 EXISTS_TAC `[a:real^2;b]` THEN
3278 EXISTS_TAC `CONS (b:real^2) (CONS y l)` THEN
3279 ASM_REWRITE_TAC[polygonal_path; LENGTH] THEN
3280 REWRITE_TAC[PATHSTART_POLYGONAL_PATH; NOT_CONS_NIL; HD] THEN
3281 REWRITE_TAC[PATHSTART_LINEPATH; PATHFINISH_LINEPATH] THEN
3282 REPEAT(CONJ_TAC THENL [ARITH_TAC; ALL_TAC]) THEN
3283 REWRITE_TAC[set_of_list] THEN SET_TAC[];
3286 FIRST_X_ASSUM(MP_TAC o SPEC `CONS (x:real^2) (CONS y l)`) THEN
3287 REWRITE_TAC[LENGTH; ARITH_RULE `n < SUC n`] THEN ANTS_TAC THENL
3288 [REWRITE_TAC[ARITH_RULE `2 <= SUC(SUC n)`] THEN
3289 ONCE_REWRITE_TAC[MEM] THEN ASM_REWRITE_TAC[] THEN
3290 FIRST_ASSUM(MP_TAC o MATCH_MP (REWRITE_RULE[IMP_CONJ]
3291 SIMPLE_PATH_JOIN_IMP)) THEN
3292 ASM_REWRITE_TAC[PATHSTART_POLYGONAL_PATH; NOT_CONS_NIL; HD] THEN
3293 SIMP_TAC[PATHFINISH_LINEPATH; ARC_IMP_SIMPLE_PATH];
3295 REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
3296 MAP_EVERY X_GEN_TAC [`q:(real^2)list`; `r:(real^2)list`] THEN
3297 STRIP_TAC THEN MAP_EVERY EXISTS_TAC
3298 [`CONS (a:real^2) q`; `r:(real^2)list`] THEN
3299 ASM_REWRITE_TAC[LENGTH; NOT_CONS_NIL; HD] THEN
3300 REPLICATE_TAC 2 (CONJ_TAC THENL [ASM_ARITH_TAC; ALL_TAC]) THEN
3302 [ASM_REWRITE_TAC[set_of_list; SET_RULE
3303 `(a INSERT s) UNION t = a INSERT (s UNION t)`];
3306 [REWRITE_TAC[PATHSTART_POLYGONAL_PATH; NOT_CONS_NIL; HD];
3309 [UNDISCH_TAC `pathfinish(polygonal_path q) = (b:real^2)` THEN
3310 REWRITE_TAC[PATHFINISH_POLYGONAL_PATH; LAST; NOT_CONS_NIL] THEN
3311 UNDISCH_TAC `2 <= LENGTH(q:(real^2)list)` THEN
3312 COND_CASES_TAC THEN ASM_REWRITE_TAC[LENGTH; ARITH];
3315 `polygonal_path(CONS (a:real^2) q) =
3316 linepath(a,x) ++ polygonal_path q`
3318 [MAP_EVERY UNDISCH_TAC
3319 [`pathstart(polygonal_path q) =
3320 pathstart(polygonal_path (CONS (x:real^2) (CONS y l)))`;
3321 `2 <= LENGTH(q:(real^2)list)`] THEN
3322 SPEC_TAC(`q:(real^2)list`,`q:(real^2)list`) THEN
3323 POP_ASSUM_LIST(K ALL_TAC) THEN
3324 MATCH_MP_TAC list_INDUCT THEN REWRITE_TAC[LENGTH; ARITH] THEN
3325 GEN_TAC THEN MATCH_MP_TAC list_INDUCT THEN
3326 REWRITE_TAC[LENGTH; ARITH; polygonal_path] THEN
3327 SIMP_TAC[PATHSTART_POLYGONAL_PATH; HD; NOT_CONS_NIL];
3330 `pathstart(polygonal_path(CONS x (CONS y l))) = (x:real^2)`
3331 (fun th -> SUBST_ALL_TAC th THEN ASSUME_TAC th) THENL
3332 [REWRITE_TAC[PATHSTART_POLYGONAL_PATH; NOT_CONS_NIL; HD]; ALL_TAC] THEN
3334 [W(MP_TAC o PART_MATCH (rand o rand) SIMPLE_PATH_ASSOC o snd) THEN
3335 ASM_REWRITE_TAC[PATHSTART_LINEPATH; PATHFINISH_LINEPATH] THEN
3336 REWRITE_TAC[PATHSTART_POLYGONAL_PATH; NOT_CONS_NIL; HD] THEN
3337 DISCH_THEN(SUBST1_TAC o SYM) THEN
3338 UNDISCH_TAC `simple_path(linepath(a:real^2,x) ++
3339 polygonal_path (CONS x (CONS y l)))` THEN
3340 ASM_CASES_TAC `pathfinish(polygonal_path r) = (a:real^2)` THENL
3342 `pathfinish(polygonal_path(CONS (x:real^2) (CONS y l))) = a`
3343 ASSUME_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
3344 ASM_SIMP_TAC[SIMPLE_PATH_JOIN_LOOP_EQ; PATHFINISH_LINEPATH;
3345 PATHSTART_JOIN; PATHFINISH_JOIN; PATHSTART_LINEPATH] THEN
3346 STRIP_TAC THEN MATCH_MP_TAC SIMPLE_PATH_IMP_ARC THEN
3347 ASM_REWRITE_TAC[PATHSTART_JOIN; PATHFINISH_JOIN] THEN
3348 ASM_MESON_TAC[ARC_LINEPATH_EQ];
3350 `~(pathfinish(polygonal_path(CONS (x:real^2) (CONS y l))) = a)`
3351 ASSUME_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
3352 ASM_SIMP_TAC[SIMPLE_PATH_EQ_ARC; PATHSTART_JOIN; PATHSTART_LINEPATH;
3353 PATHFINISH_JOIN] THEN
3354 ASM_SIMP_TAC[ARC_JOIN_EQ; PATHFINISH_LINEPATH; PATHSTART_JOIN] THEN
3355 REWRITE_TAC[ARC_LINEPATH_EQ] THEN STRIP_TAC THEN
3357 `arc(polygonal_path q ++ polygonal_path r:real^1->real^2)`
3360 ASM_SIMP_TAC[ARC_JOIN_EQ; PATHFINISH_LINEPATH; PATHSTART_JOIN]] THEN
3361 MATCH_MP_TAC SIMPLE_PATH_IMP_ARC THEN
3362 ASM_REWRITE_TAC[PATHSTART_JOIN; PATHFINISH_JOIN] THEN
3363 FIRST_X_ASSUM(MP_TAC o MATCH_MP ARC_DISTINCT_ENDS) THEN
3364 REWRITE_TAC[PATHSTART_POLYGONAL_PATH; HD; NOT_CONS_NIL]];
3365 ASM_SIMP_TAC[PATH_IMAGE_JOIN; PATHFINISH_JOIN; PATHFINISH_LINEPATH] THEN
3366 SIMP_TAC[PATH_IMAGE_JOIN; PATHFINISH_LINEPATH; NOT_CONS_NIL; HD;
3367 PATHSTART_POLYGONAL_PATH] THEN
3369 `path_image(polygonal_path q ++ polygonal_path r) =
3370 path_image(polygonal_path(CONS (x:real^2) (CONS y l)))`
3371 (SUBST1_TAC o SYM) THEN
3372 ASM_SIMP_TAC[PATH_IMAGE_JOIN; PATHFINISH_JOIN; PATHFINISH_LINEPATH] THEN
3375 SUBGOAL_THEN `pathstart(polygonal_path p) = (a:real^2)` SUBST_ALL_TAC THENL
3376 [UNDISCH_TAC `5 <= LENGTH(p:(real^2)list)` THEN
3377 REWRITE_TAC[PATHSTART_POLYGONAL_PATH] THEN
3378 COND_CASES_TAC THEN ASM_REWRITE_TAC[LENGTH; ARITH];
3380 UNDISCH_THEN `pathfinish (polygonal_path p) = (a:real^2)` SUBST_ALL_TAC THEN
3381 UNDISCH_THEN `path_image(polygonal_path q ++ polygonal_path r):real^2->bool =
3382 path_image(polygonal_path p)` (SUBST_ALL_TAC o SYM) THEN
3384 `(!x:real^2. MEM x q ==> integral_vector x) /\
3385 (!x:real^2. MEM x r ==> integral_vector x)`
3386 STRIP_ASSUME_TAC THENL
3387 [REWRITE_TAC[GSYM IN_SET_OF_LIST] THEN REPEAT STRIP_TAC THEN
3388 FIRST_X_ASSUM MATCH_MP_TAC THEN
3389 ASM_REWRITE_TAC[GSYM IN_SET_OF_LIST; IN_UNION] THEN
3391 `(set_of_list q UNION set_of_list r):real^2->bool = set_of_list p`
3392 (SUBST_ALL_TAC o SYM) THEN
3393 ASM_REWRITE_TAC[IN_UNION];
3395 ABBREV_TAC `n = LENGTH(p:(real^2)list)` THEN
3396 SUBGOAL_THEN `integral_vector(a:real^2) /\ integral_vector(b:real^2)`
3397 STRIP_ASSUME_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
3398 MAP_EVERY (C UNDISCH_THEN (K ALL_TAC))
3399 [`!x:real^2. MEM x p ==> integral_vector x`;
3402 `HD p = (a:real^2)`;
3403 `(set_of_list q UNION set_of_list r):real^2->bool = set_of_list p`;
3404 `simple_path(polygonal_path p :real^1->real^2)`] THEN
3405 SUBGOAL_THEN `3 <= LENGTH(q:(real^2)list)` ASSUME_TAC THENL
3406 [REPEAT(FIRST_X_ASSUM(K ALL_TAC o check is_forall o concl)) THEN
3407 REPEAT(POP_ASSUM MP_TAC) THEN
3408 SPEC_TAC(`q:(real^2)list`,`q:(real^2)list`) THEN
3409 MATCH_MP_TAC list_INDUCT THEN REWRITE_TAC[LENGTH; ARITH] THEN
3410 X_GEN_TAC `a0:real^2` THEN
3411 MATCH_MP_TAC list_INDUCT THEN REWRITE_TAC[LENGTH; ARITH] THEN
3412 X_GEN_TAC `a1:real^2` THEN MATCH_MP_TAC list_INDUCT THEN
3413 REWRITE_TAC[LENGTH; ARITH; ARITH_RULE `3 <= SUC(SUC(SUC n))`] THEN
3414 REWRITE_TAC[polygonal_path; PATHSTART_LINEPATH; PATHFINISH_LINEPATH] THEN
3415 REPEAT STRIP_TAC THEN
3416 UNDISCH_THEN `a0:real^2 = a` SUBST_ALL_TAC THEN
3417 UNDISCH_THEN `a1:real^2 = b` SUBST_ALL_TAC THEN
3418 UNDISCH_TAC `segment(a:real^2,b) SUBSET
3419 inside(path_image(linepath(a,b) ++ polygonal_path r))` THEN
3420 ASM_SIMP_TAC[PATH_IMAGE_JOIN; PATH_IMAGE_LINEPATH; PATHFINISH_LINEPATH] THEN
3421 MATCH_MP_TAC(SET_RULE
3422 `inside(s' UNION t) INTER (s' UNION t) = {} /\ ~(s = {}) /\ s SUBSET s'
3423 ==> ~(s SUBSET inside(s' UNION t))`) THEN
3424 REWRITE_TAC[INSIDE_NO_OVERLAP] THEN
3425 ASM_REWRITE_TAC[SEGMENT_OPEN_SUBSET_CLOSED; SEGMENT_EQ_EMPTY];
3426 UNDISCH_THEN `2 <= LENGTH(q:(real^2)list)` (K ALL_TAC)] THEN
3427 SUBGOAL_THEN `3 <= LENGTH(r:(real^2)list)` ASSUME_TAC THENL
3428 [REPEAT(FIRST_X_ASSUM(K ALL_TAC o check is_forall o concl)) THEN
3429 REPEAT(POP_ASSUM MP_TAC) THEN
3430 SPEC_TAC(`r:(real^2)list`,`r:(real^2)list`) THEN
3431 MATCH_MP_TAC list_INDUCT THEN REWRITE_TAC[LENGTH; ARITH] THEN
3432 X_GEN_TAC `a0:real^2` THEN
3433 MATCH_MP_TAC list_INDUCT THEN REWRITE_TAC[LENGTH; ARITH] THEN
3434 X_GEN_TAC `a1:real^2` THEN MATCH_MP_TAC list_INDUCT THEN
3435 REWRITE_TAC[LENGTH; ARITH; ARITH_RULE `3 <= SUC(SUC(SUC n))`] THEN
3436 REWRITE_TAC[polygonal_path; PATHSTART_LINEPATH; PATHFINISH_LINEPATH] THEN
3437 REPEAT STRIP_TAC THEN
3438 UNDISCH_THEN `a0:real^2 = b` SUBST_ALL_TAC THEN
3439 UNDISCH_THEN `a1:real^2 = a` SUBST_ALL_TAC THEN
3440 UNDISCH_TAC `segment(a:real^2,b) SUBSET
3441 inside(path_image(polygonal_path q ++ linepath(b,a)))` THEN
3442 ASM_SIMP_TAC[PATH_IMAGE_JOIN; PATH_IMAGE_LINEPATH; PATHSTART_LINEPATH] THEN
3443 ONCE_REWRITE_TAC[CONJUNCT1 SEGMENT_SYM] THEN
3444 MATCH_MP_TAC(SET_RULE
3445 `inside(t UNION s') INTER (t UNION s') = {} /\ ~(s = {}) /\ s SUBSET s'
3446 ==> ~(s SUBSET inside(t UNION s'))`) THEN
3447 REWRITE_TAC[INSIDE_NO_OVERLAP] THEN
3448 ASM_REWRITE_TAC[SEGMENT_OPEN_SUBSET_CLOSED; SEGMENT_EQ_EMPTY];
3449 UNDISCH_THEN `2 <= LENGTH(r:(real^2)list)` (K ALL_TAC)] THEN
3450 FIRST_X_ASSUM(fun th ->
3451 MP_TAC(ISPEC `CONS (a:real^2) r` th) THEN
3452 MP_TAC(ISPEC `CONS (b:real^2) q` th)) THEN
3453 REWRITE_TAC[LENGTH] THEN ANTS_TAC THENL [ASM_ARITH_TAC; ALL_TAC] THEN
3455 `polygonal_path(CONS (b:real^2) q) = linepath(b,a) ++ polygonal_path q`
3457 [POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN
3458 SPEC_TAC(`q:(real^2)list`,`q:(real^2)list`) THEN
3459 MATCH_MP_TAC list_INDUCT THEN REWRITE_TAC[LENGTH; ARITH] THEN
3460 GEN_TAC THEN MATCH_MP_TAC list_INDUCT THEN
3461 REWRITE_TAC[LENGTH; ARITH; polygonal_path] THEN
3462 SIMP_TAC[PATHSTART_POLYGONAL_PATH; HD; NOT_CONS_NIL];
3465 [ASM_REWRITE_TAC[MEM; PATHSTART_JOIN; PATHFINISH_JOIN] THEN
3466 CONJ_TAC THENL [ASM_MESON_TAC[]; REWRITE_TAC[PATHSTART_LINEPATH]] THEN
3468 `simple_path(polygonal_path q ++ polygonal_path r :real^1->real^2)` THEN
3469 ASM_SIMP_TAC[SIMPLE_PATH_JOIN_LOOP_EQ; PATHSTART_LINEPATH;
3470 PATHFINISH_LINEPATH; ARC_LINEPATH_EQ] THEN
3471 STRIP_TAC THEN REWRITE_TAC[PATH_IMAGE_LINEPATH] THEN
3472 ONCE_REWRITE_TAC[SEGMENT_SYM] THEN
3473 REWRITE_TAC[SEGMENT_CLOSED_OPEN] THEN
3474 FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (SET_RULE
3477 ==> (s UNION {a,b}) INTER c SUBSET {b,a}`)) THEN
3478 ASM_SIMP_TAC[PATH_IMAGE_JOIN] THEN
3479 MATCH_MP_TAC(SET_RULE
3480 `inside(s UNION t) INTER (s UNION t) = {}
3481 ==> s INTER inside(s UNION t) = {}`) THEN
3482 REWRITE_TAC[INSIDE_NO_OVERLAP];
3484 REWRITE_TAC[LENGTH] THEN ANTS_TAC THENL [ASM_ARITH_TAC; ALL_TAC] THEN
3486 `polygonal_path(CONS (a:real^2) r) = linepath(a,b) ++ polygonal_path r`
3488 [POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN
3489 SPEC_TAC(`r:(real^2)list`,`r:(real^2)list`) THEN
3490 MATCH_MP_TAC list_INDUCT THEN REWRITE_TAC[LENGTH; ARITH] THEN
3491 GEN_TAC THEN MATCH_MP_TAC list_INDUCT THEN
3492 REWRITE_TAC[LENGTH; ARITH; polygonal_path] THEN
3493 SIMP_TAC[PATHSTART_POLYGONAL_PATH; HD; NOT_CONS_NIL];
3496 [ASM_REWRITE_TAC[MEM; PATHSTART_JOIN; PATHFINISH_JOIN] THEN
3497 CONJ_TAC THENL [ASM_MESON_TAC[]; REWRITE_TAC[PATHSTART_LINEPATH]] THEN
3499 `simple_path(polygonal_path q ++ polygonal_path r :real^1->real^2)` THEN
3500 ASM_SIMP_TAC[SIMPLE_PATH_JOIN_LOOP_EQ; PATHSTART_LINEPATH;
3501 PATHFINISH_LINEPATH; ARC_LINEPATH_EQ] THEN
3502 STRIP_TAC THEN REWRITE_TAC[PATH_IMAGE_LINEPATH] THEN
3503 REWRITE_TAC[SEGMENT_CLOSED_OPEN] THEN
3504 FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (SET_RULE
3507 ==> (s UNION {a,b}) INTER c SUBSET {a,b}`)) THEN
3508 ASM_SIMP_TAC[PATH_IMAGE_JOIN] THEN
3509 MATCH_MP_TAC(SET_RULE
3510 `inside(s UNION t) INTER (s UNION t) = {}
3511 ==> t INTER inside(s UNION t) = {}`) THEN
3512 REWRITE_TAC[INSIDE_NO_OVERLAP];
3514 MP_TAC(ISPECL [`polygonal_path q:real^1->real^2`;
3515 `reversepath(polygonal_path r):real^1->real^2`;
3516 `linepath(a:real^2,b)`; `a:real^2`; `b:real^2`]
3517 SPLIT_INSIDE_SIMPLE_CLOSED_CURVE) THEN
3518 REWRITE_TAC[] THEN ANTS_TAC THENL
3519 [ASM_REWRITE_TAC[PATHSTART_LINEPATH; PATHFINISH_LINEPATH;
3520 PATHSTART_REVERSEPATH; PATHFINISH_REVERSEPATH;
3521 SIMPLE_PATH_LINEPATH_EQ] THEN
3523 `simple_path(polygonal_path q ++ polygonal_path r :real^1->real^2)` THEN
3524 ASM_SIMP_TAC[SIMPLE_PATH_JOIN_LOOP_EQ; PATH_IMAGE_LINEPATH] THEN
3525 ASM_SIMP_TAC[PATH_IMAGE_REVERSEPATH; ARC_IMP_SIMPLE_PATH;
3526 SIMPLE_PATH_REVERSEPATH] THEN
3527 STRIP_TAC THEN REPEAT CONJ_TAC THENL
3528 [MATCH_MP_TAC(SET_RULE
3529 `s INTER t SUBSET {a,b} /\
3530 a IN s /\ b IN s /\ a IN t /\ b IN t
3531 ==> s INTER t = {a,b}`) THEN
3532 ASM_MESON_TAC[PATHSTART_IN_PATH_IMAGE; PATHFINISH_IN_PATH_IMAGE];
3533 REWRITE_TAC[SEGMENT_CLOSED_OPEN] THEN
3535 `segment(a:real^2,b) SUBSET
3536 inside(path_image(polygonal_path q ++ polygonal_path r))` THEN
3537 ASM_SIMP_TAC[PATH_IMAGE_JOIN] THEN MATCH_MP_TAC(SET_RULE
3538 `a IN t /\ b IN t /\ inside(t UNION u) INTER (t UNION u) = {}
3539 ==> s SUBSET inside(t UNION u)
3540 ==> t INTER (s UNION {a,b}) = {a,b}`) THEN
3541 REWRITE_TAC[INSIDE_NO_OVERLAP] THEN
3542 ASM_MESON_TAC[PATHSTART_IN_PATH_IMAGE; PATHFINISH_IN_PATH_IMAGE];
3543 REWRITE_TAC[SEGMENT_CLOSED_OPEN] THEN
3545 `segment(a:real^2,b) SUBSET
3546 inside(path_image(polygonal_path q ++ polygonal_path r))` THEN
3547 ASM_SIMP_TAC[PATH_IMAGE_JOIN] THEN MATCH_MP_TAC(SET_RULE
3548 `a IN u /\ b IN u /\ inside(t UNION u) INTER (t UNION u) = {}
3549 ==> s SUBSET inside(t UNION u)
3550 ==> u INTER (s UNION {a,b}) = {a,b}`) THEN
3551 REWRITE_TAC[INSIDE_NO_OVERLAP] THEN
3552 ASM_MESON_TAC[PATHSTART_IN_PATH_IMAGE; PATHFINISH_IN_PATH_IMAGE];
3553 REWRITE_TAC[SEGMENT_CLOSED_OPEN] THEN
3554 FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (SET_RULE
3556 ==> inside(q UNION r) INTER (q UNION r) = {} /\
3557 inside(q UNION r) = i /\
3559 ==> ~((s UNION {a,b}) INTER inside(q UNION r) = {})`)) THEN
3560 ASM_REWRITE_TAC[INSIDE_NO_OVERLAP; SEGMENT_EQ_EMPTY] THEN
3561 ASM_SIMP_TAC[PATH_IMAGE_JOIN]];
3563 REPEAT(FIRST_X_ASSUM(MP_TAC o
3564 check (free_in `measure:(real^2->bool)->real` o concl))) THEN
3566 `segment(a:real^2,b) SUBSET
3567 inside(path_image (polygonal_path q ++ polygonal_path r))` THEN
3568 ASM_SIMP_TAC[PATH_IMAGE_JOIN; PATHSTART_LINEPATH; PATHFINISH_LINEPATH] THEN
3569 REWRITE_TAC[PATH_IMAGE_REVERSEPATH; PATH_IMAGE_LINEPATH] THEN
3570 SUBST1_TAC(ISPECL [`b:real^2`; `a:real^2`] (CONJUNCT1 SEGMENT_SYM)) THEN
3571 REPEAT STRIP_TAC THEN SUBST1_TAC(SYM(ASSUME
3572 `inside(path_image(polygonal_path q) UNION segment [a,b]) UNION
3573 inside(path_image(polygonal_path r) UNION segment [a,b]) UNION
3574 (segment [a:real^2,b] DIFF {a, b}) =
3576 (path_image(polygonal_path q) UNION path_image(polygonal_path r))`)) THEN
3577 REWRITE_TAC[SET_RULE
3578 `{x | x IN (s UNION t) /\ P x} =
3579 {x | x IN s /\ P x} UNION {x | x IN t /\ P x}`] THEN
3580 MATCH_MP_TAC EQ_TRANS THEN
3582 `measure(inside(path_image(polygonal_path q) UNION segment[a:real^2,b])) +
3583 measure(inside(path_image (polygonal_path r) UNION segment [a,b]) UNION
3584 segment [a,b] DIFF {a, b})` THEN
3586 [MATCH_MP_TAC MEASURE_NEGLIGIBLE_UNION THEN REPEAT CONJ_TAC THENL
3587 [MATCH_MP_TAC MEASURABLE_INSIDE THEN
3588 MATCH_MP_TAC COMPACT_UNION THEN
3589 SIMP_TAC[COMPACT_PATH_IMAGE; COMPACT_SEGMENT; PATH_POLYGONAL_PATH];
3590 MATCH_MP_TAC MEASURABLE_UNION THEN CONJ_TAC THENL
3591 [MATCH_MP_TAC MEASURABLE_INSIDE THEN
3592 MATCH_MP_TAC COMPACT_UNION THEN
3593 SIMP_TAC[COMPACT_PATH_IMAGE; COMPACT_SEGMENT; PATH_POLYGONAL_PATH];
3594 MATCH_MP_TAC MEASURABLE_DIFF THEN CONJ_TAC THEN
3595 MATCH_MP_TAC MEASURABLE_COMPACT THEN REWRITE_TAC[COMPACT_SEGMENT] THEN
3596 MATCH_MP_TAC FINITE_IMP_COMPACT THEN
3597 REWRITE_TAC[FINITE_INSERT; FINITE_EMPTY]];
3598 ASM_REWRITE_TAC[UNION_OVER_INTER; UNION_EMPTY] THEN
3599 MATCH_MP_TAC NEGLIGIBLE_SUBSET THEN EXISTS_TAC `segment[a:real^2,b]` THEN
3600 REWRITE_TAC[NEGLIGIBLE_SEGMENT_2] THEN SET_TAC[]];
3602 MATCH_MP_TAC EQ_TRANS THEN
3604 `measure(inside(path_image(polygonal_path q) UNION segment[a:real^2,b])) +
3605 measure(inside(path_image(polygonal_path r) UNION segment[a,b]))` THEN
3607 [AP_TERM_TAC THEN MATCH_MP_TAC MEASURE_NEGLIGIBLE_SYMDIFF THEN
3608 MATCH_MP_TAC NEGLIGIBLE_SUBSET THEN
3609 EXISTS_TAC `segment[a:real^2,b]` THEN
3610 REWRITE_TAC[NEGLIGIBLE_SEGMENT_2] THEN SET_TAC[];
3612 REWRITE_TAC[GSYM REAL_OF_NUM_ADD] THEN
3613 ONCE_REWRITE_TAC[SET_RULE `s UNION segment[a,b] = segment[a,b] UNION s`] THEN
3614 ASM_REWRITE_TAC[] THEN
3616 `CARD({x | x IN inside(segment[a,b] UNION path_image(polygonal_path q)) /\
3617 integral_vector x} UNION
3618 {x | x IN inside(segment[a,b] UNION path_image(polygonal_path r)) /\
3619 integral_vector x} UNION
3620 {x | x IN segment[a,b] DIFF {a, b} /\ integral_vector x}) =
3621 CARD {x | x IN inside(segment[a,b] UNION path_image(polygonal_path q)) /\
3622 integral_vector x} +
3623 CARD {x | x IN inside(segment[a,b] UNION path_image(polygonal_path r)) /\
3624 integral_vector x} +
3625 CARD {x:real^2 | x IN segment[a,b] DIFF {a, b} /\ integral_vector x}`
3627 [(CONV_TAC o GEN_SIMPLIFY_CONV TOP_DEPTH_SQCONV (basic_ss []) 5)
3628 [CARD_UNION_GEN; FINITE_BOUNDED_INTEGER_POINTS; FINITE_UNION;
3629 BOUNDED_INSIDE; BOUNDED_UNION; BOUNDED_SEGMENT;
3630 BOUNDED_PATH_IMAGE; BOUNDED_DIFF; PATH_POLYGONAL_PATH] THEN
3631 MATCH_MP_TAC(ARITH_RULE
3632 `pr = 0 /\ qrp = 0 ==> (q + (r + p) - pr) - qrp = q + r + p`) THEN
3633 REWRITE_TAC[UNION_OVER_INTER] THEN
3634 REWRITE_TAC[SET_RULE
3635 `{x | x IN s /\ P x} INTER {x | x IN t /\ P x} =
3636 {x | x IN (s INTER t) /\ P x}`] THEN
3637 RULE_ASSUM_TAC(ONCE_REWRITE_RULE
3638 [SET_RULE `s UNION segment[a,b] = segment[a,b] UNION s`]) THEN
3639 ASM_REWRITE_TAC[NOT_IN_EMPTY; EMPTY_GSPEC; UNION_EMPTY] THEN CONJ_TAC THEN
3640 MATCH_MP_TAC(MESON[CARD_CLAUSES] `s = {} ==> CARD s = 0`) THEN
3641 MATCH_MP_TAC(SET_RULE
3642 `inside(s UNION t) INTER (s UNION t) = {}
3643 ==> {x | x IN inside(s UNION t) INTER (s DIFF ab) /\ P x} = {}`) THEN
3644 REWRITE_TAC[INSIDE_NO_OVERLAP];
3646 REWRITE_TAC[GSYM REAL_OF_NUM_ADD] THEN MATCH_MP_TAC(REAL_ARITH
3647 `q + r = &2 * x + y + &2
3648 ==> (iq + q / &2 - &1) + (ir + r / &2 - &1) =
3649 ((iq + ir + x) + y / &2 - &1)`) THEN
3650 REWRITE_TAC[SET_RULE
3651 `{x | x IN (s UNION t) /\ P x} =
3652 {x | x IN s /\ P x} UNION {x | x IN t /\ P x}`] THEN
3653 (CONV_TAC o GEN_SIMPLIFY_CONV TOP_DEPTH_SQCONV (basic_ss []) 5)
3654 [CARD_UNION_GEN; FINITE_BOUNDED_INTEGER_POINTS; BOUNDED_SEGMENT;
3655 BOUNDED_PATH_IMAGE; PATH_POLYGONAL_PATH; GSYM REAL_OF_NUM_SUB;
3656 INTER_SUBSET; CARD_SUBSET; ARITH_RULE `x:num <= y ==> x <= y + z`] THEN
3657 REWRITE_TAC[GSYM REAL_OF_NUM_ADD] THEN MATCH_MP_TAC(REAL_ARITH
3658 `&2 * ab + qr = &2 * x + qab + rab + &2
3659 ==> ((ab + q) - qab) + ((ab + r) - rab) =
3660 &2 * x + ((q + r) - qr) + &2`) THEN
3662 `{x | x IN segment[a,b] /\ integral_vector x} INTER
3663 {x | x IN path_image(polygonal_path q) /\ integral_vector x} = {a,b} /\
3664 {x:real^2 | x IN segment[a,b] /\ integral_vector x} INTER
3665 {x | x IN path_image(polygonal_path r) /\ integral_vector x} = {a,b}`
3666 (CONJUNCTS_THEN SUBST1_TAC)
3668 [FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (SET_RULE
3669 `s SUBSET inside(q UNION r)
3670 ==> s = c DIFF {a,b} /\ a IN q /\ b IN q /\ a IN r /\ b IN r /\
3671 inside(q UNION r) INTER (q UNION r) = {} /\
3672 P a /\ P b /\ a IN c /\ b IN c
3673 ==> {x | x IN c /\ P x} INTER {x | x IN q /\ P x} = {a,b} /\
3674 {x | x IN c /\ P x} INTER {x | x IN r /\ P x} = {a,b}`)) THEN
3675 ASM_REWRITE_TAC[open_segment; INSIDE_NO_OVERLAP; ENDS_IN_SEGMENT] THEN
3676 ASM_MESON_TAC[PATHSTART_IN_PATH_IMAGE; PATHFINISH_IN_PATH_IMAGE];
3679 `{x:real^2 | x IN path_image(polygonal_path q) /\ integral_vector x} INTER
3680 {x | x IN path_image(polygonal_path r) /\ integral_vector x} = {a,b}`
3682 [FIRST_X_ASSUM(MP_TAC o MATCH_MP (REWRITE_RULE[IMP_CONJ]
3683 SIMPLE_PATH_JOIN_IMP)) THEN
3684 ASM_REWRITE_TAC[] THEN DISCH_THEN(MP_TAC o last o CONJUNCTS) THEN
3685 MATCH_MP_TAC(SET_RULE
3686 `P a /\ P b /\ a IN q /\ b IN q /\ a IN r /\ b IN r
3687 ==> (q INTER r) SUBSET {a,b}
3688 ==> {x | x IN q /\ P x} INTER {x | x IN r /\ P x} = {a,b}`) THEN
3689 ASM_MESON_TAC[PATHSTART_IN_PATH_IMAGE; PATHFINISH_IN_PATH_IMAGE];
3691 SIMP_TAC[CARD_CLAUSES; FINITE_INSERT; FINITE_EMPTY] THEN
3692 ASM_REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY] THEN CONV_TAC NUM_REDUCE_CONV THEN
3693 MATCH_MP_TAC(REAL_ARITH
3694 `x = y + &2 ==> &2 * x + &2 = &2 * y + &2 + &2 + &2`) THEN
3695 REWRITE_TAC[SEGMENT_CLOSED_OPEN] THEN
3696 SUBGOAL_THEN `(segment(a,b) UNION {a, b}) DIFF {a, b} = segment(a:real^2,b)`
3698 [MATCH_MP_TAC(SET_RULE
3699 `~(a IN s) /\ ~(b IN s) ==> (s UNION {a,b}) DIFF {a,b} = s`) THEN
3700 REWRITE_TAC[open_segment; IN_DIFF] THEN SET_TAC[];
3702 ASM_SIMP_TAC[SET_RULE
3704 ==> {x | x IN s UNION {a,b} /\ P x} =
3705 a INSERT b INSERT {x | x IN s /\ P x}`] THEN
3706 SIMP_TAC[CARD_CLAUSES; FINITE_BOUNDED_INTEGER_POINTS;
3707 BOUNDED_SEGMENT; FINITE_INSERT] THEN
3708 ASM_REWRITE_TAC[IN_INSERT; IN_ELIM_THM; ENDS_NOT_IN_SEGMENT] THEN
3709 REWRITE_TAC[REAL_OF_NUM_ADD; ARITH_RULE `SUC(SUC n) = n + 2`]);;