100/pick.ml

   1 (* ========================================================================= *)
   2 (* Pick's theorem.                                                           *)
   3 (* ========================================================================= *)
   4
   5 needs "Multivariate/polytope.ml";;
   6 needs "Multivariate/measure.ml";;
   7 needs "Multivariate/moretop.ml";;
   8
   9 prioritize_real();;
  10
  11 (* ------------------------------------------------------------------------- *)
  12 (* Misc lemmas.                                                              *)
  13 (* ------------------------------------------------------------------------- *)
  14
  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]);;
  19
  20 let CONVEX_HULL_3_0 = prove
  21  (`!a b:real^N.
  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]);;
  32
  33 let INTERIOR_CONVEX_HULL_3_0 = prove
  34  (`!a b:real^2.
  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
  46   ASM_REAL_ARITH_TAC);;
  47
  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)`,
  51   REPEAT STRIP_TAC THEN
  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]);;
  56
  57 let NEGLIGIBLE_SEGMENT_2 = prove
  58  (`!a b:real^2. negligible(segment[a,b])`,
  59   SIMP_TAC[COLLINEAR_IMP_NEGLIGIBLE; COLLINEAR_SEGMENT]);;
  60
  61 (* ------------------------------------------------------------------------- *)
  62 (* Decomposing an additive function on a triangle.                           *)
  63 (* ------------------------------------------------------------------------- *)
  64
  65 let TRIANGLE_DECOMPOSITION = prove
  66  (`!a b c d:real^2.
  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})`,
  72   REPEAT STRIP_TAC THEN
  73   MATCH_MP_TAC SUBSET_ANTISYM THEN REWRITE_TAC[UNION_SUBSET] THEN
  74   CONJ_TAC THENL
  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]]);;
  85
  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})) +
  99             f(convex hull {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);;
 113
 114 (* ------------------------------------------------------------------------- *)
 115 (* Vectors all of whose coordinates are integers.                            *)
 116 (* ------------------------------------------------------------------------- *)
 117
 118 let integral_vector = define
 119  `integral_vector(x:real^N) <=>
 120         !i. 1 <= i /\ i <= dimindex(:N) ==> integer(x$i)`;;
 121
 122 let INTEGRAL_VECTOR_VEC = prove
 123  (`!n. integral_vector(vec n)`,
 124   REWRITE_TAC[integral_vector; VEC_COMPONENT; INTEGER_CLOSED]);;
 125
 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]);;
 131
 132 let INTEGRAL_VECTOR_ADD = prove
 133  (`!x y:real^N.
 134         integral_vector x /\ integral_vector y ==> integral_vector(x + y)`,
 135   SIMP_TAC[integral_vector; VECTOR_ADD_COMPONENT; INTEGER_CLOSED]);;
 136
 137 let INTEGRAL_VECTOR_SUB = prove
 138  (`!x y:real^N.
 139         integral_vector x /\ integral_vector y ==> integral_vector(x - y)`,
 140   SIMP_TAC[integral_vector; VECTOR_SUB_COMPONENT; INTEGER_CLOSED]);;
 141
 142 let INTEGRAL_VECTOR_ADD_LCANCEL = prove
 143  (`!x y:real^N.
 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`]);;
 147
 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)
 157                        ==> integer(x$i) /\
 158                            (a:real^N)$i <= x$i /\ x$i <= (b:real^N)$i}` THEN
 159   CONJ_TAC THENL
 160    [MATCH_MP_TAC FINITE_CART THEN REWRITE_TAC[FINITE_INTSEG];
 161     ASM SET_TAC[]]);;
 162
 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]);;
 167
 168 (* ------------------------------------------------------------------------- *)
 169 (* Properties of a basis for the integer lattice.                            *)
 170 (* ------------------------------------------------------------------------- *)
 171
 172 let LINEAR_INTEGRAL_VECTOR = prove
 173  (`!f:real^N->real^N.
 174         linear f
 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]]);;
 194
 195 let INTEGRAL_BASIS_UNIMODULAR = prove
 196  (`!f:real^N->real^N.
 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
 201   SUBGOAL_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
 206   SUBGOAL_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];
 219     ALL_TAC] THEN
 220   SUBGOAL_THEN
 221    `!i j. 1 <= i /\ i <= dimindex(:N) /\
 222           1 <= j /\ j <= dimindex(:N)
 223           ==> integer(matrix(g:real^N->real^N)$i$j)`
 224   ASSUME_TAC THENL
 225    [ASM_SIMP_TAC[GSYM LINEAR_INTEGRAL_VECTOR] THEN ASM_MESON_TAC[];
 226     ALL_TAC] THEN
 227   SUBGOAL_THEN
 228    `det(matrix(f:real^N->real^N)) * det(matrix(g:real^N->real^N)) =
 229     det(matrix(I:real^N->real^N))`
 230   MP_TAC THENL
 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];
 233     ALL_TAC] THEN
 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]);;
 237
 238 (* ------------------------------------------------------------------------- *)
 239 (* Pick's theorem for an elementary triangle.                                *)
 240 (* ------------------------------------------------------------------------- *)
 241
 242 let PICK_ELEMENTARY_TRIANGLE_0 = prove
 243  (`!a b:real^2.
 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
 251   MAP_EVERY (fun t ->
 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[];
 264     ALL_TAC] THEN
 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];
 272     ALL_TAC] THEN
 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
 282   CONJ_TAC THENL
 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];
 291     ALL_TAC] THEN
 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
 305   MATCH_MP_TAC(TAUT
 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)`
 310     MP_TAC THENL
 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
 328     SUBGOAL_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`
 332     MP_TAC THENL
 333      [MP_TAC(SPEC `u:real` FLOOR_FRAC) THEN
 334       MP_TAC(SPEC `v:real` FLOOR_FRAC) THEN REAL_ARITH_TAC;
 335       MESON_TAC[]];
 336     REWRITE_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]);;
 342
 343 let PICK_ELEMENTARY_TRIANGLE = prove
 344  (`!a b c:real^2.
 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]);;
 355
 356 (* ------------------------------------------------------------------------- *)
 357 (* Our form of Pick's theorem holds degenerately for a flat triangle.        *)
 358 (* ------------------------------------------------------------------------- *)
 359
 360 let PICK_TRIANGLE_FLAT = prove
 361  (`!a b c:real^2.
 362         integral_vector a /\ integral_vector b /\ integral_vector c /\
 363         c IN segment[a,b]
 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 +
 369              &1 / &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];
 375     ALL_TAC] THEN
 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];
 380     ALL_TAC] THEN
 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
 384   SUBGOAL_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
 387   REWRITE_TAC[SET_RULE
 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
 393   CONJ_TAC THENL
 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
 398     SUBGOAL_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]]);;
 404
 405 (* ------------------------------------------------------------------------- *)
 406 (* Pick's theorem for a triangle.                                            *)
 407 (* ------------------------------------------------------------------------- *)
 408
 409 let PICK_TRIANGLE_ALT = prove
 410  (`!a b c:real^2.
 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 +
 417              &1 / &2`,
 418   let tac a bc =
 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];
 426       DISCH_TAC] THEN
 427     SUBGOAL_THEN(subst[bc,`bc:real^2->bool`]
 428         `convex hull {a:real^2,b,c} = convex hull bc`)
 429     ASSUME_TAC THENL
 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}`)
 433       MP_TAC THENL
 434        [SIMP_TAC[HULL_INC; IN_INSERT]; ASM SET_TAC[]];
 435       ALL_TAC] THEN
 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
 441   REPEAT GEN_TAC THEN
 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]);
 454     ALL_TAC] THEN
 455   UNDISCH_TAC `~collinear{a:real^2,b,c}` THEN
 456   MAP_EVERY
 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
 461   ASM_CASES_TAC
 462    `{x:real^2 | x IN convex hull {a, b, c} /\ integral_vector x} =
 463     {a,b,c}`
 464   THENL
 465    [ASM_SIMP_TAC[PICK_ELEMENTARY_TRIANGLE] THEN
 466     SUBGOAL_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
 478         [SET_TAC[];
 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];
 489      ALL_TAC] THEN
 490   SUBGOAL_THEN
 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];
 499     ALL_TAC] THEN
 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
 503   MP_TAC(ISPECL
 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
 510   MP_TAC(ISPECL
 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
 524     CONJ_TAC THENL
 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}`
 538   SUBST1_TAC THENL
 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);;
 544
 545 let PICK_TRIANGLE = prove
 546  (`!a b c:real^2.
 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
 559   REWRITE_TAC[SET_RULE
 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
 565   CONJ_TAC THENL
 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
 568     CONJ_TAC THENL
 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[];
 576     REWRITE_TAC[SET_RULE
 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
 581     REWRITE_TAC[SET_RULE
 582      `{x | x IN s /\ P x} INTER {x | x IN t /\ P x} =
 583       {x | x IN (s INTER t) /\ P x}`] THEN
 584     SUBGOAL_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]);;
 606
 607 (* ------------------------------------------------------------------------- *)
 608 (* Parity lemma for segment crossing a polygon.                              *)
 609 (* ------------------------------------------------------------------------- *)
 610
 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))))`,
 619   let lemma = prove
 620    (`!a b x y:real^N.
 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
 627     NORM_ARITH_TAC)
 628   and symlemma = prove
 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`;
 641                  `x:real^2`]
 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];
 660     ALL_TAC] THEN
 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];
 674     ALL_TAC] THEN
 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
 680   SUBGOAL_THEN
 681    `{c,d} INTER path_image(p ++ linepath(a:real^2,b)) = {}`
 682   ASSUME_TAC THENL
 683    [ASM_SIMP_TAC[PATH_IMAGE_JOIN; PATH_LINEPATH; PATHSTART_LINEPATH] THEN
 684     REWRITE_TAC[SET_RULE
 685      `{c,d} INTER (s UNION t) = {} <=>
 686       (~(c IN s) /\ ~(d IN s)) /\ ~(c IN t) /\ ~(d IN t)`] THEN
 687     CONJ_TAC THENL
 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[]];
 692     ALL_TAC] THEN
 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
 697    [ASM SET_TAC[];
 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[];
 702     ALL_TAC] THEN
 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]];
 720     ALL_TAC] THEN
 721   DISCH_THEN(fun th -> POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN
 722                        MP_TAC th) 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];
 737     ALL_TAC] THEN
 738   SUBGOAL_THEN
 739    `!y. y IN ball(x:real^2,e)
 740         ==> y IN segment(a,b) \/
 741             &0 < n dot (y - x) \/
 742             n dot (y - x) < &0`
 743   ASSUME_TAC THENL
 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
 760     SIMP_TAC[INSERT_AC];
 761     ALL_TAC] 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
 764   STRIP_TAC THEN
 765   SUBGOAL_THEN
 766    `~(connected_component((:real^2) DIFF path_image(p ++ linepath (a,b))) c d)`
 767   MP_TAC THENL
 768    [DISCH_TAC;
 769     ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN
 770     DISCH_THEN(MP_TAC o SPEC `path_image(p ++ linepath(a:real^2,b))` o
 771       MATCH_MP (SET_RULE
 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
 781   SUBGOAL_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`
 786   ASSUME_TAC THENL
 787    [ALL_TAC;
 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
 794     STRIP_TAC THENL
 795      [REWRITE_TAC[connected_component] THEN
 796       EXISTS_TAC `inside(path_image(p ++ linepath(a:real^2,b)))`;
 797       ASM_MESON_TAC[];
 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[];
 807     ALL_TAC] THEN
 808   MAP_EVERY X_GEN_TAC [`u:real^2`; `v:real^2`] THEN STRIP_TAC THEN
 809   UNDISCH_TAC
 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
 819   CONJ_TAC THENL
 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];
 824     ALL_TAC] THEN
 825   UNDISCH_TAC
 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
 835   CONJ_TAC THENL
 836    [ALL_TAC;
 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
 841   SUBGOAL_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`
 845   ASSUME_TAC THENL
 846    [ALL_TAC;
 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;
 851                   NOT_IN_EMPTY]] THEN
 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}`
 854   ASSUME_TAC THENL
 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];
 870     ALL_TAC] THEN
 871   UNDISCH_THEN
 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
 892          `cd INTER p = {x}
 893           ==> xd SUBSET cd
 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;
 942                        VECTOR_SUB_EQ] THEN
 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;
 950                        REAL_LT_01]];
 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
 960          `cd INTER p = {x}
 961           ==> xd SUBSET cd
 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;
1010                        VECTOR_SUB_EQ] THEN
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;
1019                        REAL_LT_01]];
1020         REWRITE_TAC[IN_BALL; IN_INTER; IN_ELIM_THM] THEN
1021         ONCE_REWRITE_TAC[DIST_SYM] THEN ASM_REWRITE_TAC[]]]]);;
1022
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 (* ------------------------------------------------------------------------- *)
1027
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))`;;
1034
1035 let POLYGONAL_PATH_CONS_CONS = prove
1036  (`!a b p. ~(p = [])
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]);;
1041
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]);;
1052
1053 add_translation_invariants [POLYGONAL_PATH_TRANSLATION];;
1054
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
1063   CONJ_TAC THENL
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]);;
1068
1069 add_linear_invariants [POLYGONAL_PATH_LINEAR_IMAGE];;
1070
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]);;
1079
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]);;
1088
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
1103     ASM SET_TAC[]]);;
1104
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
1127   MESON_TAC[]);;
1128
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]);;
1139
1140 let PATH_IMAGE_POLYGONAL_PATH_SUBSET_CONVEX_HULL = prove
1141  (`!p. ~(p = [])
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
1157       SET_TAC[]]]);;
1158
1159 let PATH_IMAGE_POLYGONAL_PATH_SUBSET_SEGMENTS = prove
1160  (`!p x:real^N.
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)))`;
1194       `b:real^N`] THEN
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
1201       UNDISCH_TAC
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];
1218         ASM_MESON_TAC[MEM];
1219         ASM_REWRITE_TAC[];
1220         ASM SET_TAC[];
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[]]]]);;
1228
1229 (* ------------------------------------------------------------------------- *)
1230 (* Rotating the starting point to move a preferred vertex forward.           *)
1231 (* ------------------------------------------------------------------------- *)
1232
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[]);;
1239
1240 let PROPERTIES_POLYGONAL_PATH_SNOC = prove
1241  (`!p d:real^N.
1242         2 <= LENGTH p
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];
1270     ALL_TAC] THEN
1271   ASM_CASES_TAC `a:real^N = d` THENL
1272    [MATCH_MP_TAC(TAUT
1273      `(~p /\ ~p') /\ (q <=> q') ==> (p <=> p') /\ (q <=> q')`) THEN
1274     CONJ_TAC THENL
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];
1279       ALL_TAC] THEN
1280     ASM_REWRITE_TAC[] THEN
1281     W(MP_TAC o PART_MATCH (lhs o rand) SIMPLE_PATH_JOIN_LOOP_EQ o
1282      lhs o snd) THEN
1283     ANTS_TAC THENL
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
1289      rhs o snd) THEN
1290     ANTS_TAC THENL
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];
1298     MATCH_MP_TAC(TAUT
1299      `((q <=> p) /\ (q' <=> p')) /\ (p <=> p')
1300       ==> (p <=> p') /\ (q <=> q')`) THEN
1301     CONJ_TAC THENL
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];
1307       ALL_TAC] THEN
1308     W(MP_TAC o PART_MATCH (lhs o rand) ARC_JOIN_EQ o lhs o snd) THEN
1309     ANTS_TAC THENL
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
1314     ANTS_TAC THENL
1315      [SIMP_TAC[PATHSTART_POLYGONAL_PATH; PATHFINISH_LINEPATH; PATHSTART_JOIN;
1316                NOT_CONS_NIL; HD];
1317       DISCH_THEN SUBST1_TAC] THEN
1318     ASM_REWRITE_TAC[] THEN
1319     REWRITE_TAC[PATHSTART_JOIN; PATHSTART_POLYGONAL_PATH; NOT_CONS_NIL; HD]]);;
1320
1321 let PATH_IMAGE_POLYGONAL_PATH_ROTATE = prove
1322  (`!p:(real^N)list.
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
1336   DISCH_TAC 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]);;
1346
1347 let SIMPLE_PATH_POLYGONAL_PATH_ROTATE = prove
1348  (`!p:(real^N)list.
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
1362   DISCH_TAC 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]);;
1372
1373 let ROTATE_LIST_TO_FRONT_1 = prove
1374  (`!P l a:A.
1375       (!l. P(l) ==> 3 <= LENGTH l /\ LAST l = HD l) /\
1376       (!l. P(l) ==> P(APPEND (TL l) [HD(TL l)])) /\
1377       P l /\ MEM a l
1378       ==> ?l'. EL 1 l' = a /\ P l'`,
1379   let lemma0 = prove
1380      (`!P. (!i. P i /\ 0 < i ==> P(i - 1)) /\ (?k. 0 < k /\ P k)
1381              ==> P 1`,
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
1391   SUBGOAL_THEN
1392    `?i l'. 0 < i /\ i < LENGTH l' /\ P l' /\ EL i l' = (a:A)`
1393   MP_TAC THENL
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`)
1399     THENL
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`]]);;
1423
1424 let ROTATE_LIST_TO_FRONT_0 = prove
1425  (`!P l a:A.
1426       (!l. P(l) ==> 3 <= LENGTH l /\ LAST l = HD l) /\
1427       (!l. P(l) ==> P(APPEND (TL l) [HD(TL l)])) /\
1428       P l /\ MEM a 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]);;
1442
1443 (* ------------------------------------------------------------------------- *)
1444 (* We can pick a transformation to make all y coordinates distinct.          *)
1445 (* ------------------------------------------------------------------------- *)
1446
1447 let DISTINGUISHING_ROTATION_EXISTS_PAIR = prove
1448  (`!x y. ~(x = y)
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
1458   CONJ_TAC 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]);;
1466
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
1470   SUBGOAL_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)})))`
1475   MP_TAC THENL
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[]]);;
1494
1495 let DISTINGUISHING_ROTATION_EXISTS_POLYGON = prove
1496  (`!p:(real^2)list.
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)) /\
1499               f q = p`,
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[]);;
1515
1516 (* ------------------------------------------------------------------------- *)
1517 (* Proof that we can chop a polygon's inside in two.                         *)
1518 (* ------------------------------------------------------------------------- *)
1519
1520 let POLYGON_CHOP_IN_TWO = prove
1521  (`!p:(real^2)list.
1522         simple_path(polygonal_path p) /\
1523         pathfinish(polygonal_path p) = pathstart(polygonal_path p) /\
1524         5 <= LENGTH 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)
1531             ==> !x. P x` in
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]`,
1537     REPEAT GEN_TAC THEN
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];
1546       ALL_TAC] THEN
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
1551     REAL_ARITH_TAC) in
1552   MATCH_MP_TAC(MATCH_MP wlog_lemma DISTINGUISHING_ROTATION_EXISTS_POLYGON) THEN
1553   CONJ_TAC THENL
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 [];
1558     ALL_TAC] THEN
1559   X_GEN_TAC `q:(real^2)list` THEN DISCH_TAC THEN STRIP_TAC THEN
1560   SUBGOAL_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)`
1564         INF_FINITE) THEN
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
1573     ASM_REWRITE_TAC[];
1574     ALL_TAC] THEN
1575   SUBGOAL_THEN
1576    `?p:(real^2)list.
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)`
1582   MP_TAC THENL
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;
1603       ALL_TAC] THEN
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
1606      [ASM_ARITH_TAC;
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];
1628     ALL_TAC] THEN
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
1662   MP_TAC(ISPECL
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)
1671                 MP_TAC) THEN
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
1685     ASM_MESON_TAC[];
1686     ALL_TAC] 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
1693   STRIP_TAC 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
1701     ASM_MESON_TAC[];
1702     ALL_TAC] 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];
1709       ALL_TAC] THEN
1710     ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN REWRITE_TAC[] THEN
1711     STRIP_TAC THENL
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]];
1731     ALL_TAC] THEN
1732   SUBGOAL_THEN
1733    `?e. &0 < e /\
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)))
1740                           DELETE b)`
1741                 INF_FINITE) THEN
1742     ASM_SIMP_TAC[FINITE_SET_OF_LIST; FINITE_IMAGE; FINITE_DELETE] THEN
1743     ANTS_TAC THENL
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];
1747       ALL_TAC] THEN
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
1756     ASM_MESON_TAC[];
1757     ALL_TAC] 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
1761   SUBGOAL_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];
1774     ALL_TAC] THEN
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];
1782     ALL_TAC] THEN
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];
1795     ALL_TAC] THEN
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];
1799     ALL_TAC] THEN
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'}`
1808   ASSUME_TAC THENL
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
1829       ASM_REWRITE_TAC[];
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
1839         SET_TAC[];
1840         EXPAND_TAC "a'";
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
1844         SET_TAC[];
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]];
1851     ALL_TAC] THEN
1852   SUBGOAL_THEN
1853    `interior(convex hull {a,b,c}) INTER {x:real^2 | x$2 - b$2 < e} =
1854     interior(convex hull {a',b,c'})`
1855   ASSUME_TAC THENL
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];
1858     ALL_TAC] THEN
1859   SUBGOAL_THEN
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;
1875       DISCH_TAC] THEN
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;
1888     ALL_TAC] THEN
1889   SUBGOAL_THEN
1890     `path_image(polygonal_path(CONS a (CONS b (CONS c p))))
1891      SUBSET {x:real^2 | x$2 >= b$2}`
1892   MP_TAC THENL
1893    [MATCH_MP_TAC SUBSET_TRANS THEN
1894     EXISTS_TAC
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;
1901                  REAL_LE_REFL];
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
1905   SUBGOAL_THEN
1906    `(:real^2) DIFF {x | x$2 >= b$2} SUBSET
1907     outside(path_image
1908                  (linepath(a,b) ++ linepath(b,c) ++ polygonal_path(CONS c p)))`
1909   MP_TAC THENL
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
1915     DISCH_TAC] THEN
1916   ABBREV_TAC
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)))`
1920   ASSUME_TAC THENL
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;
1924     ALL_TAC] THEN
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)`];
1932     ALL_TAC] THEN
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`;
1947                 REAL_ARITH
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
1951     ASM_REAL_ARITH_TAC;
1952     ALL_TAC] 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
1956     REAL_ARITH_TAC;
1957     ALL_TAC] THEN
1958   SUBGOAL_THEN
1959    `convex hull {a':real^2,b,c'} SUBSET convex hull {a,b,c}`
1960   ASSUME_TAC THENL
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[];
1970     ALL_TAC] THEN
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
1977     ASM_REAL_ARITH_TAC;
1978     ALL_TAC] THEN
1979   SUBGOAL_THEN `~(d' IN convex hull {a':real^2,b,c'})` ASSUME_TAC THENL
1980    [ASM SET_TAC[]; ALL_TAC] THEN
1981   SUBGOAL_THEN
1982    `~(segment[d:real^2,d'] INTER frontier(convex hull {a',b,c'}) = {})`
1983   MP_TAC THENL
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]];
1989     ALL_TAC] THEN
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];
2000     ALL_TAC] THEN
2001   ASM_REWRITE_TAC[SEGMENT_CLOSED_OPEN; IN_UNION; IN_INSERT; NOT_IN_EMPTY] THEN
2002   STRIP_TAC 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
2006     REAL_ARITH_TAC;
2007     ALL_TAC] 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;
2011     ALL_TAC] THEN
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;
2017     ALL_TAC] THEN
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;
2020     ALL_TAC] THEN
2021   SUBGOAL_THEN `(x:real^2) IN (segment(b,a) UNION segment(b,c))`
2022   ASSUME_TAC THENL
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;
2032     ALL_TAC] THEN
2033   SUBGOAL_THEN
2034    `segment[d:real^2,d'] INTER path_image(polygonal_path(CONS c p)) = {}`
2035   ASSUME_TAC THENL
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];
2051     ALL_TAC] THEN
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[];
2056     ALL_TAC] THEN
2057   SUBGOAL_THEN `~(d':real^2 = d)` ASSUME_TAC THENL
2058    [ASM_MESON_TAC[IN_SEGMENT]; ALL_TAC] THEN
2059   SUBGOAL_THEN
2060    `!y:real^2. y IN segment[d,d'] /\
2061                y IN (segment (b,a) UNION segment (b,c))
2062                ==> y = x`
2063   ASSUME_TAC THENL
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];
2073       ALL_TAC] THEN
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
2077     SUBGOAL_THEN
2078      `(x:real^2) IN frontier(convex hull {a,b,c}) /\
2079       (y:real^2) IN frontier(convex hull {a,b,c})`
2080     MP_TAC THENL
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]];
2112     ALL_TAC] THEN
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
2120     MESON_TAC[];
2121     ALL_TAC] THEN
2122   SUBGOAL_THEN
2123    `(d:real^2) IN inside(path_image
2124       (linepath(a,b) ++ linepath(b,c) ++ polygonal_path(CONS c p)))`
2125   ASSUME_TAC THENL
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
2131       SUBGOAL_THEN
2132        `path_image((linepath(b:real^2,c) ++ polygonal_path(CONS c p)) ++
2133                    linepath(a,b)) =
2134         path_image(linepath(a,b) ++ linepath(b:real^2,c) ++
2135                    polygonal_path(CONS c p))`
2136       SUBST1_TAC THENL
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];
2143         ALL_TAC] THEN
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
2170           ASM_REAL_ARITH_TAC;
2171           ALL_TAC] 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
2186       SUBGOAL_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))`
2191       SUBST1_TAC THENL
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];
2197         ALL_TAC] THEN
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
2200         ANTS_TAC THENL
2201          [ALL_TAC;
2202           DISCH_THEN SUBST1_TAC THEN
2203           W(MP_TAC o PART_MATCH (lhs o rand) SIMPLE_PATH_SYM o snd) THEN
2204           ANTS_TAC THENL
2205            [ALL_TAC;
2206             DISCH_THEN SUBST1_TAC THEN
2207             W(MP_TAC o PART_MATCH (lhs o rand) (GSYM SIMPLE_PATH_ASSOC) o
2208               snd) THEN
2209             ASM_REWRITE_TAC[] THEN DISCH_THEN MATCH_MP_TAC]] THEN
2210         ASM_SIMP_TAC[GSYM SIMPLE_PATH_ASSOC;PATHSTART_JOIN;
2211                      PATHFINISH_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
2235           ASM_REAL_ARITH_TAC;
2236           ALL_TAC] 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]];
2249     ALL_TAC] THEN
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
2252   ASM_CASES_TAC
2253    `path_image(polygonal_path(CONS c p)) INTER
2254     convex hull {a,b,c} SUBSET {a:real^2,c}`
2255   THENL
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
2265     CONJ_TAC THENL
2266      [ALL_TAC;
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
2271        `t INTER s SUBSET c
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[]]];
2326     ALL_TAC] THEN
2327   SUBGOAL_THEN
2328    `?n:real^2.
2329         ~(n = vec 0) /\ orthogonal n (c - a) /\
2330         &0 < n dot (c - b)`
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];
2337       ALL_TAC] THEN
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`)
2341     THENL
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]];
2354     ALL_TAC] THEN
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];
2359     ALL_TAC] THEN
2360   SUBGOAL_THEN
2361    `!y:real^2. y IN convex hull {a,b,c} /\ ~(y = b) ==> &0 < n dot (y - b)`
2362   ASSUME_TAC THENL
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;
2374     ALL_TAC] THEN
2375   SUBGOAL_THEN
2376    `!y:real^2. y IN convex hull {a,b,c} ==> &0 <= n dot (y - b)`
2377   ASSUME_TAC THENL
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];
2381     ALL_TAC] THEN
2382   SUBGOAL_THEN
2383    `!y:real^2. y IN convex hull {a,b,c} ==> n dot (y - b) <= n dot (c - b)`
2384   ASSUME_TAC THENL
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];
2392     ALL_TAC] THEN
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];
2402       ASM SET_TAC[];
2403       SUBGOAL_THEN
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]];
2409     ALL_TAC] THEN
2410   DISCH_TAC THEN
2411   SUBGOAL_THEN
2412    `?mx:real^2.
2413       ~(mx = a) /\ ~(mx = c) /\
2414       mx IN path_image(polygonal_path(CONS c p)) INTER convex hull {a, b, c} /\
2415       (!y. y IN
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
2439     UNDISCH_TAC
2440      `segment[b:real^2,c] INTER path_image (polygonal_path (CONS c p))
2441       SUBSET {c}` THEN
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[];
2445     ALL_TAC] THEN
2446   SUBGOAL_THEN
2447    `?z:real^2. MEM z p /\
2448                z IN (convex hull {a,b,c} DIFF {a,c}) /\
2449                n dot (z - b) = m`
2450   STRIP_ASSUME_TAC THENL
2451    [ALL_TAC;
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
2461     SUBGOAL_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];
2468       ALL_TAC] THEN
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[];
2483       ALL_TAC] THEN
2484     SUBGOAL_THEN
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
2492       REWRITE_TAC[] 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[];
2504       ALL_TAC] THEN
2505     SUBGOAL_THEN `segment[b:real^2,z] SUBSET convex hull {a,b,c}`
2506     ASSUME_TAC THENL
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[];
2510       ALL_TAC] THEN
2511     SUBGOAL_THEN `segment(b:real^2,z) SUBSET convex hull {a,b,c}`
2512     ASSUME_TAC THENL
2513      [REWRITE_TAC[open_segment] THEN ASM SET_TAC[]; ALL_TAC] THEN
2514     SUBGOAL_THEN
2515      `segment(b:real^2,z) INTER path_image(polygonal_path(CONS c p)) = {}`
2516     ASSUME_TAC THENL
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];
2529       ALL_TAC] THEN
2530     SUBGOAL_THEN `segment(b:real^2,z) SUBSET interior(convex hull {a,b,c})`
2531     ASSUME_TAC THENL
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
2534       CONJ_TAC THENL
2535        [ALL_TAC;
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];
2562       ALL_TAC] THEN
2563     SUBGOAL_THEN
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
2574       CONJ_TAC THENL
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]];
2588       ALL_TAC] THEN
2589     MATCH_MP_TAC CONNECTED_COMPONENT_TRANS THEN EXISTS_TAC `y:real^2` THEN
2590     CONJ_TAC THENL
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
2646   SUBGOAL_THEN
2647    `?u v:real^2.
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]) /\
2652         n dot (u - b) <= m`
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
2656     ANTS_TAC THENL
2657      [ASM_REWRITE_TAC[LENGTH; ARITH_RULE `3 <= SUC n <=> 2 <= n`] THEN
2658       ASM SET_TAC[];
2659       ALL_TAC] 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[]];
2682     ALL_TAC] THEN
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];
2696       ALL_TAC] THEN
2697     MP_TAC(ISPECL
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 = {}))
2703           ==> u IN c`) THEN
2704     REPEAT CONJ_TAC THENL
2705      [DISCH_TAC THEN
2706       SUBGOAL_THEN `closure(segment(u:real^2,mx)) SUBSET convex hull {a,b,c}`
2707       MP_TAC THENL
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
2716        `!a b c t u.
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]];
2759       ALL_TAC] THEN
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
2766       REWRITE_TAC[MESON[]
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];
2773         REAL_ARITH_TAC;
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;
2777                      VECTOR_SUB_EQ] THEN
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]];
2781       ALL_TAC] THEN
2782     MP_TAC(ISPEC `{a:real^2,b,c}` AFFINE_INDEPENDENT_SPAN_EQ) THEN
2783     ANTS_TAC THENL
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;
2788       ALL_TAC] THEN
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
2805       UNDISCH_TAC
2806         `segment[b:real^2,c] INTER path_image(polygonal_path(CONS c p))
2807          SUBSET {c}` THEN
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[];
2815       ALL_TAC] THEN
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];
2822       ALL_TAC] THEN
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
2826       UNDISCH_TAC
2827         `segment[a:real^2,b] INTER path_image(polygonal_path(CONS c p))
2828          SUBSET {a,b}` THEN
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
2836         ASM_REAL_ARITH_TAC;
2837         ALL_TAC] 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[];
2841       ALL_TAC] THEN
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];
2848      ALL_TAC] THEN
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
2859      ASM_REAL_ARITH_TAC;
2860      ALL_TAC] THEN
2861     ASM_CASES_TAC `sx = &0` THENL
2862      [ALL_TAC;
2863       STRIP_TAC THEN
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
2873     SUBGOAL_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
2877     SUBGOAL_THEN
2878      `?q. q * (rx - r) <= rx /\
2879           q * (tx - t) <= tx /\
2880           &0 < q /\ q < &1`
2881     STRIP_ASSUME_TAC THENL
2882      [EXISTS_TAC
2883        `min (&1 / &2)
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];
2914       ALL_TAC] THEN
2915     MAP_EVERY EXISTS_TAC
2916      [`(&1 - q) * rx + q * r`;
2917       `q * s:real`;
2918       `(&1 - q) * tx + q * t:real`] THEN
2919     REWRITE_TAC[CONJ_ASSOC] THEN CONJ_TAC THENL
2920      [ALL_TAC;
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) +
2924       q * s +
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;
2941     ALL_TAC] THEN
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];
2955     ALL_TAC] THEN
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
2959   SUBGOAL_THEN
2960    `collinear {a:real^2,mx,c} /\ collinear {a,u,c}`
2961   STRIP_ASSUME_TAC THENL
2962    [SUBGOAL_THEN
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;
2975     ALL_TAC] THEN
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
2981     ASM SET_TAC[];
2982     ALL_TAC] 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
2988     ASM SET_TAC[];
2989     ALL_TAC] 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[];
2993     ALL_TAC] THEN
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]];
3001     ALL_TAC] THEN
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]];
3009     ALL_TAC] THEN
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];
3013     ALL_TAC] THEN
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];
3018     ALL_TAC] THEN
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
3022    [CONJ_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
3027       ASM_REWRITE_TAC[];
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[]];
3038     ALL_TAC] THEN
3039   STRIP_TAC THENL
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
3056     CONJ_TAC THENL
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;
3071                       REAL_MUL_LID]];
3072     UNDISCH_TAC `segment[a:real^2,c] SUBSET segment[u,v]` THEN
3073     ASM_REWRITE_TAC[SUBSET_SEGMENT]]);;
3074
3075 (* ------------------------------------------------------------------------- *)
3076 (* Hence the final Pick theorem by induction on number of polygon segments.  *)
3077 (* ------------------------------------------------------------------------- *)
3078
3079 let PICK = prove
3080  (`!p:(real^2)list.
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
3100       MESON_TAC[];
3101       ALL_TAC] 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];
3117       ALL_TAC] THEN
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
3139     SUBGOAL_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];
3155     STRIP_TAC] THEN
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
3159   SUBGOAL_THEN
3160    `?p':(real^2)list.
3161         HD p' = a /\
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
3173       ASM_ARITH_TAC;
3174       ALL_TAC] 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;
3192       ALL_TAC] THEN
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
3195      [ASM_ARITH_TAC;
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];
3217     ALL_TAC] THEN
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
3234   SUBGOAL_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
3246    [SUBGOAL_THEN
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)`
3251     MP_TAC THENL
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;
3264                   MEM] THEN
3265       MESON_TAC[];
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[];
3284       ALL_TAC] THEN
3285     STRIP_TAC THEN
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];
3294       ALL_TAC] THEN
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
3301     CONJ_TAC THENL
3302      [ASM_REWRITE_TAC[set_of_list; SET_RULE
3303        `(a INSERT s) UNION t = a INSERT (s UNION t)`];
3304       ALL_TAC] THEN
3305     CONJ_TAC THENL
3306      [REWRITE_TAC[PATHSTART_POLYGONAL_PATH; NOT_CONS_NIL; HD];
3307       ALL_TAC] THEN
3308     CONJ_TAC THENL
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];
3313       ALL_TAC] THEN
3314     SUBGOAL_THEN
3315      `polygonal_path(CONS (a:real^2) q) =
3316       linepath(a,x) ++ polygonal_path q`
3317     SUBST1_TAC THENL
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];
3328       ALL_TAC] THEN
3329     SUBGOAL_THEN
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
3333     CONJ_TAC THENL
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
3341        [SUBGOAL_THEN
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];
3349         SUBGOAL_THEN
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
3356         SUBGOAL_THEN
3357          `arc(polygonal_path q ++ polygonal_path r:real^1->real^2)`
3358         MP_TAC THENL
3359          [ALL_TAC;
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
3368       UNDISCH_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
3373       SET_TAC[]];
3374     ALL_TAC] 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];
3379     ALL_TAC] THEN
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
3383   SUBGOAL_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
3390     UNDISCH_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];
3394     ALL_TAC] THEN
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`;
3400     `MEM (a:real^2) p`;
3401     `MEM (b:real^2) p`;
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
3454   SUBGOAL_THEN
3455    `polygonal_path(CONS (b:real^2) q) = linepath(b,a) ++ polygonal_path q`
3456   SUBST_ALL_TAC THENL
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];
3463     ALL_TAC] THEN
3464   ANTS_TAC THENL
3465    [ASM_REWRITE_TAC[MEM; PATHSTART_JOIN; PATHFINISH_JOIN] THEN
3466     CONJ_TAC THENL [ASM_MESON_TAC[]; REWRITE_TAC[PATHSTART_LINEPATH]] THEN
3467     UNDISCH_TAC
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
3475      `s SUBSET i
3476       ==> c INTER i = {}
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];
3483     STRIP_TAC] THEN
3484   REWRITE_TAC[LENGTH] THEN ANTS_TAC THENL [ASM_ARITH_TAC; ALL_TAC] THEN
3485   SUBGOAL_THEN
3486    `polygonal_path(CONS (a:real^2) r) = linepath(a,b) ++ polygonal_path r`
3487   SUBST_ALL_TAC THENL
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];
3494     ALL_TAC] THEN
3495   ANTS_TAC THENL
3496    [ASM_REWRITE_TAC[MEM; PATHSTART_JOIN; PATHFINISH_JOIN] THEN
3497     CONJ_TAC THENL [ASM_MESON_TAC[]; REWRITE_TAC[PATHSTART_LINEPATH]] THEN
3498     UNDISCH_TAC
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
3505      `s SUBSET i
3506       ==> c INTER i = {}
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];
3513     STRIP_TAC] THEN
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
3522     UNDISCH_TAC
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
3534       UNDISCH_TAC
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
3544       UNDISCH_TAC
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
3555        `s SUBSET i
3556         ==> inside(q UNION r) INTER (q UNION r) = {} /\
3557             inside(q UNION r) = i /\
3558             ~(s = {})
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]];
3562     ALL_TAC] THEN
3563   REPEAT(FIRST_X_ASSUM(MP_TAC o
3564    check (free_in `measure:(real^2->bool)->real` o concl))) THEN
3565   UNDISCH_TAC
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}) =
3575     inside
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
3581   EXISTS_TAC
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
3585   CONJ_TAC THENL
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[]];
3601     ALL_TAC] THEN
3602   MATCH_MP_TAC EQ_TRANS THEN
3603   EXISTS_TAC
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
3606   CONJ_TAC THENL
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[];
3611     ALL_TAC] THEN
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
3615   SUBGOAL_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}`
3626   SUBST1_TAC THENL
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];
3645     ALL_TAC] THEN
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
3661   SUBGOAL_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)
3667   THENL
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];
3677     ALL_TAC] THEN
3678   SUBGOAL_THEN
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}`
3681   SUBST1_TAC THENL
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];
3690     ALL_TAC] THEN
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)`
3697   SUBST1_TAC THENL
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[];
3701     ALL_TAC] THEN
3702   ASM_SIMP_TAC[SET_RULE
3703    `P a /\ P b
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`]);;