(* ========================================================================= *) (* Results connected with topological dimension. *) (* *) (* At the moment this is just Brouwer's fixpoint theorem. The proof is from *) (* Kuhn: "some combinatorial lemmas in topology", IBM J. v4. (1960) p. 518 *) (* See "http://www.research.ibm.com/journal/rd/045/ibmrd0405K.pdf". *) (* *) (* The script below is quite messy, but at least we avoid formalizing any *) (* topological machinery; we don't even use barycentric subdivision; this is *) (* the big advantage of Kuhn's proof over the usual Sperner's lemma one. *) (* *) (* (c) Copyright, John Harrison 1998-2008 *) (* ========================================================================= *) needs "Multivariate/topology.ml";; needs "Multivariate/paths.ml";;let BROUWER_COMPACTNESS_LEMMA =prove (`!f:real^M->real^N s. compact s /\ f continuous_on s /\ ~(?x. x IN s /\ (f x = vec 0)) ==> ?d. &0 < d /\ !x. x IN s ==> d <= norm(f x)`,(* ------------------------------------------------------------------------- *) (* The key "counting" observation, somewhat abstracted. *) (* ------------------------------------------------------------------------- *)let KUHN_LABELLING_LEMMA =prove (`!f:real^N->real^N P Q. (!x. P x ==> P (f x)) ==> (!x. P x ==> (!i. Q i ==> &0 <= x$i /\ x$i <= &1)) ==> ?l. (!x i. l x i <= 1) /\ (!x i. P x /\ Q i /\ (x$i = &0) ==> (l x i = 0)) /\ (!x i. P x /\ Q i /\ (x$i = &1) ==> (l x i = 1)) /\ (!x i. P x /\ Q i /\ (l x i = 0) ==> x$i <= f(x)$i) /\ (!x i. P x /\ Q i /\ (l x i = 1) ==> f(x)$i <= x$i)`,(* ------------------------------------------------------------------------- *) (* The odd/even result for faces of complete vertices, generalized. *) (* ------------------------------------------------------------------------- *) (* ------------------------------------------------------------------------- *) (* Combine this with the basic counting lemma. *) (* ------------------------------------------------------------------------- *)let KUHN_COUNTING_LEMMA =prove (`!face:F->S->bool faces simplices comp comp' bnd. FINITE faces /\ FINITE simplices /\ (!f. f IN faces /\ bnd f ==> (CARD {s | s IN simplices /\ face f s} = 1)) /\ (!f. f IN faces /\ ~bnd f ==> (CARD {s | s IN simplices /\ face f s} = 2)) /\ (!s. s IN simplices /\ comp s ==> (CARD {f | f IN faces /\ face f s /\ comp' f} = 1)) /\ (!s. s IN simplices /\ ~comp s ==> (CARD {f | f IN faces /\ face f s /\ comp' f} = 0) \/ (CARD {f | f IN faces /\ face f s /\ comp' f} = 2)) ==> ODD(CARD {f | f IN faces /\ comp' f /\ bnd f}) ==> ODD(CARD {s | s IN simplices /\ comp s})`,(* ------------------------------------------------------------------------- *) (* We use the following notion of ordering rather than pointwise indexing. *) (* ------------------------------------------------------------------------- *)let KUHN_COMPLETE_LEMMA =prove (`!face:(A->bool)->(A->bool)->bool simplices rl bnd n. FINITE simplices /\ (!f s. face f s <=> ?a. a IN s /\ (f = s DELETE a)) /\ (!s. s IN simplices ==> s HAS_SIZE (n + 2) /\ (IMAGE rl s) SUBSET 0..n+1) /\ (!f. f IN {f | ?s. s IN simplices /\ face f s} /\ bnd f ==> (CARD {s | s IN simplices /\ face f s} = 1)) /\ (!f. f IN {f | ?s. s IN simplices /\ face f s} /\ ~bnd f ==> (CARD {s | s IN simplices /\ face f s} = 2)) ==> ODD(CARD {f | f IN {f | ?s. s IN simplices /\ face f s} /\ (IMAGE rl f = 0..n) /\ bnd f}) ==> ODD(CARD {s | s IN simplices /\ (IMAGE rl s = 0..n+1)})`,let kle = new_definition `kle n x y <=> ?k. k SUBSET 1..n /\ (!j. y(j) = x(j) + (if j IN k then 1 else 0))`;;let POINTWISE_MINIMAL,POINTWISE_MAXIMAL = (CONJ_PAIR o prove) (`(!s:(num->num)->bool. FINITE s ==> ~(s = {}) /\ (!x y. x IN s /\ y IN s ==> (!j. x(j) <= y(j)) \/ (!j. y(j) <= x(j))) ==> ?a. a IN s /\ !x. x IN s ==> !j. a(j) <= x(j)) /\ (!s:(num->num)->bool. FINITE s ==> ~(s = {}) /\ (!x y. x IN s /\ y IN s ==> (!j. x(j) <= y(j)) \/ (!j. y(j) <= x(j))) ==> ?a. a IN s /\ !x. x IN s ==> !j. x(j) <= a(j))`, CONJ_TAC THEN (MATCH_MP_TAC FINITE_INDUCT_STRONG THEN REWRITE_TAC[NOT_INSERT_EMPTY] THEN MAP_EVERY X_GEN_TAC [`a:num->num`; `s:(num->num)->bool`] THEN ASM_CASES_TAC `s:(num->num)->bool = {}` THEN ASM_REWRITE_TAC[] THENL [REWRITE_TAC[IN_SING] THEN MESON_TAC[LE_REFL]; ALL_TAC] THEN DISCH_THEN(CONJUNCTS_THEN2 MP_TAC STRIP_ASSUME_TAC) THEN DISCH_THEN(fun th -> STRIP_TAC THEN MP_TAC th) THEN ANTS_TAC THENL [ASM_MESON_TAC[IN_INSERT]; ALL_TAC] THEN DISCH_THEN(X_CHOOSE_THEN `b:num->num` STRIP_ASSUME_TAC) THEN FIRST_X_ASSUM(MP_TAC o SPECL [`a:num->num`; `b:num->num`]) THEN ASM_REWRITE_TAC[IN_INSERT] THEN ASM_MESON_TAC[LE_CASES; LE_TRANS]));;let KLE_ANTISYM =prove (`!n x y. kle n x y /\ kle n y x <=> (x = y)`,let KLE_IMP_POINTWISE =prove (`!n x y. kle n x y ==> !j. x(j) <= y(j)`,let POINTWISE_ANTISYM =prove (`!x y:num->num. (!j. x(j) <= y(j)) /\ (!j. y(j) <= x(j)) <=> (x = y)`,let KLE_TRANS =prove (`!x y z n. kle n x y /\ kle n y z /\ (kle n x z \/ kle n z x) ==> kle n x z`,let KLE_STRICT =prove (`!n x y. kle n x y /\ ~(x = y) ==> (!j. x(j) <= y(j)) /\ (?k. 1 <= k /\ k <= n /\ x(k) < y(k))`,let KLE_TRANS_1 =prove (`!n x y. kle n x y ==> !j. x j <= y j /\ y j <= x j + 1`,let KLE_TRANS_2 =prove (`!a b c. kle n a b /\ kle n b c /\ (!j. c j <= a j + 1) ==> kle n a c`,let KLE_BETWEEN_R =prove (`!a b c x. kle n a b /\ kle n b c /\ kle n a x /\ kle n c x ==> kle n b x`,let KLE_BETWEEN_L =prove (`!a b c x. kle n a b /\ kle n b c /\ kle n x a /\ kle n x c ==> kle n x b`,(* ------------------------------------------------------------------------- *) (* Kuhn's notion of a simplex (my reformulation to avoid so much indexing). *) (* ------------------------------------------------------------------------- *)let KLE_ADJACENT =prove (`!a b x k. 1 <= k /\ k <= n /\ (!j. b(j) = if j = k then a(j) + 1 else a(j)) /\ kle n a x /\ kle n x b ==> (x = a) \/ (x = b)`,(* ------------------------------------------------------------------------- *) (* The lemmas about simplices that we need. *) (* ------------------------------------------------------------------------- *) (* ------------------------------------------------------------------------- *) (* Hence another step towards concreteness. *) (* ------------------------------------------------------------------------- *)let ksimplex = new_definition `ksimplex p n s <=> s HAS_SIZE (n + 1) /\ (!x j. x IN s ==> x(j) <= p) /\ (!x j. x IN s /\ ~(1 <= j /\ j <= n) ==> (x j = p)) /\ (!x y. x IN s /\ y IN s ==> kle n x y \/ kle n y x)`;;(* ------------------------------------------------------------------------- *) (* Reduced labelling. *) (* ------------------------------------------------------------------------- *)let KUHN_SIMPLEX_LEMMA =prove (`!p n. (!s. ksimplex p (n + 1) s ==> (IMAGE rl s SUBSET 0..n+1)) /\ ODD(CARD{f | (?s a. ksimplex p (n + 1) s /\ a IN s /\ (f = s DELETE a)) /\ (IMAGE rl f = 0 .. n) /\ ((?j. 1 <= j /\ j <= n + 1 /\ !x. x IN f ==> (x j = 0)) \/ (?j. 1 <= j /\ j <= n + 1 /\ !x. x IN f ==> (x j = p)))}) ==> ODD(CARD {s | s IN {s | ksimplex p (n + 1) s} /\ (IMAGE rl s = 0..n+1)})`,let reduced = new_definition `reduced label n (x:num->num) = @k. k <= n /\ (!i. 1 <= i /\ i < k + 1 ==> (label x i = 0)) /\ ((k = n) \/ ~(label x (k + 1) = 0))`;;let REDUCED_LABELLING =prove (`!label x n. reduced label n x <= n /\ (!i. 1 <= i /\ i < reduced label n x + 1 ==> (label x i = 0)) /\ ((reduced label n x = n) \/ ~(label x (reduced label n x + 1) = 0))`,let REDUCED_LABELLING_UNIQUE =prove (`!label x n. r <= n /\ (!i. 1 <= i /\ i < r + 1 ==> (label x i = 0)) /\ ((r = n) \/ ~(label x (r + 1) = 0)) ==> (reduced label n x = r)`,let REDUCED_LABELLING_0 =prove (`!label n x j. 1 <= j /\ j <= n /\ (label x j = 0) ==> ~(reduced label n x = j - 1)`,let REDUCED_LABELLING_1 =prove (`!label n x j. 1 <= j /\ j <= n /\ ~(label x j = 0) ==> reduced label n x < j`,let REDUCED_LABELLING_SUC =prove (`!lab n x. ~(reduced lab (n + 1) x = n + 1) ==> (reduced lab (n + 1) x = reduced lab n x)`,(* ------------------------------------------------------------------------- *) (* Hence we get just about the nice induction. *) (* ------------------------------------------------------------------------- *)let COMPLETE_FACE_TOP =prove (`!lab f n. (!x j. x IN f /\ 1 <= j /\ j <= n + 1 /\ (x j = 0) ==> (lab x j = 0)) /\ (!x j. x IN f /\ 1 <= j /\ j <= n + 1 /\ (x j = p) ==> (lab x j = 1)) ==> ((IMAGE (reduced lab (n + 1)) f = 0..n) /\ ((?j. 1 <= j /\ j <= n + 1 /\ !x. x IN f ==> (x j = 0)) \/ (?j. 1 <= j /\ j <= n + 1 /\ !x. x IN f ==> (x j = p))) <=> (IMAGE (reduced lab (n + 1)) f = 0..n) /\ (!x. x IN f ==> (x (n + 1) = p)))`,(* ------------------------------------------------------------------------- *) (* And so we get the final combinatorial result. *) (* ------------------------------------------------------------------------- *)let KUHN_INDUCTION =prove (`!p n. 0 < p /\ (!x j. (!j. x(j) <= p) /\ 1 <= j /\ j <= n + 1 /\ (x j = 0) ==> (lab x j = 0)) /\ (!x j. (!j. x(j) <= p) /\ 1 <= j /\ j <= n + 1 /\ (x j = p) ==> (lab x j = 1)) ==> ODD(CARD {f | ksimplex p n f /\ (IMAGE (reduced lab n) f = 0..n)}) ==> ODD(CARD {s | ksimplex p (n + 1) s /\ (IMAGE (reduced lab (n + 1)) s = 0..n+1)})`,let KSIMPLEX_0 =prove (`ksimplex p 0 s <=> (s = {(\x. p)})`,let REDUCE_LABELLING_0 =prove (`!lab x. reduced lab 0 x = 0`,(* ------------------------------------------------------------------------- *) (* The main result for the unit cube. *) (* ------------------------------------------------------------------------- *)let KUHN_LEMMA =prove (`!n p label. 0 < p /\ 0 < n /\ (!x. (!i. 1 <= i /\ i <= n ==> x(i) <= p) ==> !i. 1 <= i /\ i <= n ==> (label x i = 0) \/ (label x i = 1)) /\ (!x. (!i. 1 <= i /\ i <= n ==> x(i) <= p) ==> !i. 1 <= i /\ i <= n /\ (x i = 0) ==> (label x i = 0)) /\ (!x. (!i. 1 <= i /\ i <= n ==> x(i) <= p) ==> !i. 1 <= i /\ i <= n /\ (x i = p) ==> (label x i = 1)) ==> ?q. (!i. 1 <= i /\ i <= n ==> q(i) < p) /\ (!i. 1 <= i /\ i <= n ==> ?r s. (!j. 1 <= j /\ j <= n ==> q(j) <= r(j) /\ r(j) <= q(j) + 1) /\ (!j. 1 <= j /\ j <= n ==> q(j) <= s(j) /\ s(j) <= q(j) + 1) /\ ~(label r i = label s i))`,(* ------------------------------------------------------------------------- *) (* Retractions. *) (* ------------------------------------------------------------------------- *) parse_as_infix("retract_of",(12,"right"));;let BROUWER_CUBE =prove (`!f:real^N->real^N. f continuous_on (interval [vec 0,vec 1]) /\ IMAGE f (interval [vec 0,vec 1]) SUBSET (interval [vec 0,vec 1]) ==> ?x. x IN interval[vec 0,vec 1] /\ (f x = x)`,let retraction = new_definition `retraction (s,t) (r:real^N->real^N) <=> t SUBSET s /\ r continuous_on s /\ (IMAGE r s SUBSET t) /\ (!x. x IN t ==> (r x = x))`;;let retract_of = new_definition `t retract_of s <=> ?r. retraction (s,t) r`;;let RETRACTION =prove (`!s t r. retraction (s,t) r <=> t SUBSET s /\ r continuous_on s /\ IMAGE r s = t /\ (!x. x IN t ==> r x = x)`,let RETRACT_OF_IMP_EXTENSIBLE =prove (`!f:real^M->real^N u s t. s retract_of t /\ f continuous_on s /\ IMAGE f s SUBSET u ==> ?g. g continuous_on t /\ IMAGE g t SUBSET u /\ (!x. x IN s ==> g x = f x)`,let RETRACT_OF_TRANSLATION =prove (`!a t s:real^N->bool. t retract_of s ==> (IMAGE (\x. a + x) t) retract_of (IMAGE (\x. a + x) s)`,add_translation_invariants [RETRACT_OF_TRANSLATION_EQ];;let RETRACT_OF_TRANSLATION_EQ =prove (`!a t s:real^N->bool. (IMAGE (\x. a + x) t) retract_of (IMAGE (\x. a + x) s) <=> t retract_of s`,let RETRACT_OF_INJECTIVE_LINEAR_IMAGE =prove (`!f:real^M->real^N s t. linear f /\ (!x y. f x = f y ==> x = y) /\ t retract_of s ==> (IMAGE f t) retract_of (IMAGE f s)`,add_linear_invariants [RETRACT_OF_LINEAR_IMAGE_EQ];;let RETRACT_OF_LINEAR_IMAGE_EQ =prove (`!f:real^M->real^N s t. linear f /\ (!x y. f x = f y ==> x = y) /\ (!y. ?x. f x = y) ==> ((IMAGE f t) retract_of (IMAGE f s) <=> t retract_of s)`,let RETRACTION_REFL =prove (`!s. retraction (s,s) (\x. x)`,let RETRACT_OF_REFL =prove (`!s. s retract_of s`,let RETRACT_OF_EMPTY =prove (`(!s:real^N->bool. {} retract_of s <=> s = {}) /\ (!s:real^N->bool. s retract_of {} <=> s = {})`,let RETRACTION_o =prove (`!f g s t u:real^N->bool. retraction (s,t) f /\ retraction (t,u) g ==> retraction (s,u) (g o f)`,let RETRACT_OF_CONTRACTIBLE =prove (`!s t:real^N->bool. contractible t /\ s retract_of t ==> contractible s`,let RETRACT_OF_COMPACT =prove (`!s t:real^N->bool. compact t /\ s retract_of t ==> compact s`,let RETRACT_OF_CLOSED =prove (`!s t. closed t /\ s retract_of t ==> closed t`,let RETRACT_OF_CONNECTED =prove (`!s t:real^N->bool. connected t /\ s retract_of t ==> connected s`,let RETRACT_OF_HOMOTOPICALLY_TRIVIAL =prove (`!s t:real^N->bool u:real^M->bool. t retract_of s /\ (!f g. f continuous_on u /\ IMAGE f u SUBSET s /\ g continuous_on u /\ IMAGE g u SUBSET s ==> homotopic_with (\x. T) (u,s) f g) ==> (!f g. f continuous_on u /\ IMAGE f u SUBSET t /\ g continuous_on u /\ IMAGE g u SUBSET t ==> homotopic_with (\x. T) (u,t) f g)`,let RETRACT_OF_HOMOTOPICALLY_TRIVIAL_NULL =prove (`!s t:real^N->bool u:real^M->bool. t retract_of s /\ (!f. f continuous_on u /\ IMAGE f u SUBSET s ==> ?c. homotopic_with (\x. T) (u,s) f (\x. c)) ==> (!f. f continuous_on u /\ IMAGE f u SUBSET t ==> ?c. homotopic_with (\x. T) (u,t) f (\x. c))`,let RETRACT_OF_COHOMOTOPICALLY_TRIVIAL =prove (`!s t:real^N->bool u:real^M->bool. t retract_of s /\ (!f g. f continuous_on s /\ IMAGE f s SUBSET u /\ g continuous_on s /\ IMAGE g s SUBSET u ==> homotopic_with (\x. T) (s,u) f g) ==> (!f g. f continuous_on t /\ IMAGE f t SUBSET u /\ g continuous_on t /\ IMAGE g t SUBSET u ==> homotopic_with (\x. T) (t,u) f g)`,let RETRACT_OF_COHOMOTOPICALLY_TRIVIAL_NULL =prove (`!s t:real^N->bool u:real^M->bool. t retract_of s /\ (!f. f continuous_on s /\ IMAGE f s SUBSET u ==> ?c. homotopic_with (\x. T) (s,u) f (\x. c)) ==> (!f. f continuous_on t /\ IMAGE f t SUBSET u ==> ?c. homotopic_with (\x. T) (t,u) f (\x. c))`,let RETRACT_OF_LOCALLY_CONNECTED =prove (`!s t:real^N->bool. s retract_of t /\ locally connected t ==> locally connected s`,let RETRACT_OF_LOCALLY_PATH_CONNECTED =prove (`!s t:real^N->bool. s retract_of t /\ locally path_connected t ==> locally path_connected s`,let RETRACT_OF_LOCALLY_COMPACT =prove (`!s t:real^N->bool. locally compact s /\ t retract_of s ==> locally compact t`,(* ------------------------------------------------------------------------- *) (* A neighbourhood retract is an ANR for Euclidean space. *) (* ------------------------------------------------------------------------- *)let ABSOLUTE_RETRACTION_CONVEX_CLOSED_RELATIVE =prove (`!s:real^N->bool t. convex s /\ closed s /\ ~(s = {}) /\ s SUBSET t ==> ?r. retraction (t,s) r /\ !x. x IN (affine hull s) DIFF (relative_interior s) ==> r(x) IN relative_frontier s`,let NEIGHBOURHOOD_RETRACT_IMP_ANR =prove (`!s:real^M->bool s':real^N->bool t u. s retract_of t /\ open t /\ s homeomorphic s' /\ s' SUBSET u ==> ?t'. open_in (subtopology euclidean u) t' /\ s' retract_of t'`,let NEIGHBOURHOOD_RETRACT_IMP_ANR_UNIV =prove (`!s:real^M->bool s':real^N->bool t. s retract_of t /\ open t /\ s homeomorphic s' ==> ?t'. open t' /\ s' retract_of t'`,(* ------------------------------------------------------------------------- *) (* Likewise for ARs, at least given closedness. *) (* ------------------------------------------------------------------------- *)let HOMEOMORPHIC_ANRNESS =prove (`!s:real^M->bool t:real^N->bool. s homeomorphic t ==> ((?u. open u /\ s retract_of u) <=> (?u. open u /\ t retract_of u))`,let ABSOLUTE_RETRACT_IMP_AR_GEN =prove (`!s:real^M->bool s':real^N->bool t u. s retract_of t /\ convex t /\ closed t /\ ~(t = {}) /\ s homeomorphic s' /\ closed_in (subtopology euclidean u) s' ==> s' retract_of u`,let ABSOLUTE_RETRACT_IMP_AR =prove (`!s s'. s retract_of (:real^M) /\ s homeomorphic s' /\ closed s' ==> s' retract_of (:real^N)`,(* ------------------------------------------------------------------------- *) (* More retract properties including connection of complements. *) (* ------------------------------------------------------------------------- *)let HOMEOMORPHIC_COMPACT_ARNESS =prove (`!s s'. s homeomorphic s' ==> (compact s /\ s retract_of (:real^M) <=> compact s' /\ s' retract_of (:real^N))`,let ABSOLUTE_RETRACT_HOMEOMORPHIC_CONVEX_COMPACT =prove (`!s:real^N->bool t u:real^M->bool. s homeomorphic u /\ ~(s = {}) /\ s SUBSET t /\ convex u /\ compact u ==> s retract_of t`,let RELATIVE_BOUNDARY_RETRACT_OF_PUNCTURED_AFFINE_HULL =prove (`!s a:real^N. convex s /\ compact s /\ a IN relative_interior s ==> (s DIFF relative_interior s) retract_of ((affine hull s) DELETE a)`,let RELATIVE_FRONTIER_RETRACT_OF_PUNCTURED_AFFINE_HULL =prove (`!s a:real^N. convex s /\ bounded s /\ a IN relative_interior s ==> relative_frontier s retract_of (affine hull s) DELETE a`,let ANR_RELATIVE_FRONTIER_CONVEX =prove (`!s:real^N->bool. bounded s /\ convex s ==> ?t. open t /\ (relative_frontier s) retract_of t`,let FRONTIER_RETRACT_OF_PUNCTURED_UNIVERSE =prove (`!s a. convex s /\ bounded s /\ a IN interior s ==> (frontier s) retract_of ((:real^N) DELETE a)`,let RETRACT_OF_PCROSS =prove (`!s:real^M->bool s' t:real^N->bool t'. s retract_of s' /\ t retract_of t' ==> (s PCROSS t) retract_of (s' PCROSS t')`,let LOCALLY_CONNECTED_SPHERE_GEN =prove (`!s:real^N->bool. bounded s /\ convex s ==> locally connected (relative_frontier s)`,let LOCALLY_PATH_CONNECTED_SPHERE =prove (`!a:real^N r. locally path_connected (sphere(a,r))`,(* ------------------------------------------------------------------------- *) (* Extending a function into an ANR. *) (* ------------------------------------------------------------------------- *)let LOCALLY_CONNECTED_SPHERE =prove (`!a:real^N r. locally connected(sphere(a,r))`,let NEIGHBOURHOOD_EXTENSION_INTO_ANR_LOCAL =prove (`!f:real^M->real^N c s t u. f continuous_on c /\ IMAGE f c SUBSET t /\ open u /\ t retract_of u /\ closed_in (subtopology euclidean s) c ==> ?v g. c SUBSET v /\ open_in (subtopology euclidean s) v /\ g continuous_on v /\ IMAGE g v SUBSET t /\ !x. x IN c ==> g x = f x`,(* ------------------------------------------------------------------------- *) (* Borsuk homotopy extension thorem. It's only this late so we can use the *) (* concept of retraction, essentially that the range is an ANR. *) (* ------------------------------------------------------------------------- *)let NEIGHBOURHOOD_EXTENSION_INTO_ANR =prove (`!f:real^M->real^N s t u. f continuous_on s /\ IMAGE f s SUBSET t /\ open u /\ t retract_of u /\ closed s ==> ?v g. s SUBSET v /\ open v /\ g continuous_on v /\ IMAGE g v SUBSET t /\ !x. x IN s ==> g x = f x`,"V"] THEN REWRITE_TAC[UNION_SUBSET] THEN REWRITE_TAC[SUBSET; FORALL_IN_GSPEC] THEN ASM_SIMP_TAC[IN_ELIM_THM; IN_UNIV] THEN ASM SET_TAC[]; ALL_TAC] THEN ABBREV_TAC `s' = {x | ?u. u IN interval[vec 0,vec 1] /\ ~((pastecart (u:real^1) (x:real^M)) IN V)}` THEN SUBGOAL_THEN `closed(s':real^M->bool)` ASSUME_TAC THENL [EXPAND_TAC "s'" THEN REWRITE_TAC[SET_RULE `~(x IN s) <=> x IN (UNIV DIFF s)`] THEN MATCH_MP_TAC CLOSED_COMPACT_PROJECTION THEN ASM_REWRITE_TAC[GSYM OPEN_CLOSED; COMPACT_INTERVAL]; ALL_TAC] THEN MP_TAC(ISPECL [`s:real^M->bool`; `s':real^M->bool`; `vec 1:real^1`; `vec 0:real^1`] URYSOHN) THEN ASM_REWRITE_TAC[] THEN ANTS_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN ONCE_REWRITE_TAC[SEGMENT_SYM] THEN REWRITE_TAC[SEGMENT_1; DROP_VEC; REAL_POS] THEN DISCH_THEN(X_CHOOSE_THEN `a:real^M->real^1` STRIP_ASSUME_TAC) THEN FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [retract_of]) THEN REWRITE_TAC[retraction; LEFT_IMP_EXISTS_THM] THEN X_GEN_TAC `r:real^N->real^N` THEN STRIP_TAC THEN EXISTS_TAC `(r:real^N->real^N) o (\x. (k:real^(1,M)finite_sum->real^N) (pastecart (a x) x))` THEN REWRITE_TAC[o_THM; IMAGE_o] THEN CONJ_TAC THENL [ALL_TAC; ASM SET_TAC[]] THEN MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN CONJ_TAC THENL [GEN_REWRITE_TAC LAND_CONV [GSYM o_DEF] THEN MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN CONJ_TAC THENL [MATCH_MP_TAC CONTINUOUS_ON_PASTECART THEN REWRITE_TAC[CONTINUOUS_ON_ID] THEN ASM_MESON_TAC[CONTINUOUS_ON_SUBSET; SUBSET_UNIV]; ASM_MESON_TAC[CONTINUOUS_ON_SUBSET; SUBSET_UNIV]]; FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REWRITE_RULE[IMP_CONJ] CONTINUOUS_ON_SUBSET)) THEN ASM SET_TAC[]]);;let BORSUK_HOMOTOPY_EXTENSION =prove (`!f:real^M->real^N g s t u v. closed s /\ closed t /\ u retract_of v /\ open v /\ f continuous_on t /\ IMAGE f t SUBSET u /\ g continuous_on s /\ IMAGE g s SUBSET u /\ homotopic_with (\x. T) (s,u) f g ==> ?g'. g' continuous_on t /\ IMAGE g' t SUBSET u /\ !x. x IN s ==> g'(x) = g(x)`,let NULLHOMOTOPIC_INTO_ANR_EXTENSION =prove (`!f:real^M->real^N s t u. closed s /\ f continuous_on s /\ ~(s = {}) /\ IMAGE f s SUBSET t /\ open u /\ t retract_of u ==> ((?c. homotopic_with (\x. T) (s,t) f (\x. c)) <=> (?g. g continuous_on (:real^M) /\ IMAGE g (:real^M) SUBSET t /\ !x. x IN s ==> g x = f x))`,let NULLHOMOTOPIC_INTO_RELATIVE_FRONTIER_EXTENSION =prove (`!f:real^M->real^N s t. closed s /\ f continuous_on s /\ ~(s = {}) /\ IMAGE f s SUBSET relative_frontier t /\ convex t /\ bounded t ==> ((?c. homotopic_with (\x. T) (s,relative_frontier t) f (\x. c)) <=> (?g. g continuous_on (:real^M) /\ IMAGE g (:real^M) SUBSET relative_frontier t /\ !x. x IN s ==> g x = f x))`,let NULLHOMOTOPIC_INTO_SPHERE_EXTENSION =prove (`!f:real^M->real^N s a r. closed s /\ f continuous_on s /\ ~(s = {}) /\ IMAGE f s SUBSET sphere(a,r) ==> ((?c. homotopic_with (\x. T) (s,sphere(a,r)) f (\x. c)) <=> (?g. g continuous_on (:real^M) /\ IMAGE g (:real^M) SUBSET sphere(a,r) /\ !x. x IN s ==> g x = f x))`,(* ------------------------------------------------------------------------- *) (* Preservation of fixpoints under (more general notion of) retraction. *) (* ------------------------------------------------------------------------- *)let ABSOLUTE_RETRACT_CONTRACTIBLE_ANR =prove (`!s t. closed s /\ contractible s /\ ~(s = {}) /\ s retract_of t /\ open t ==> s retract_of (:real^N)`,let INVERTIBLE_FIXPOINT_PROPERTY =prove (`!s:real^M->bool t:real^N->bool i r. i continuous_on t /\ IMAGE i t SUBSET s /\ r continuous_on s /\ IMAGE r s SUBSET t /\ (!y. y IN t ==> (r(i(y)) = y)) ==> (!f. f continuous_on s /\ IMAGE f s SUBSET s ==> ?x. x IN s /\ (f x = x)) ==> !g. g continuous_on t /\ IMAGE g t SUBSET t ==> ?y. y IN t /\ (g y = y)`,let HOMEOMORPHIC_FIXPOINT_PROPERTY =prove (`!s t. s homeomorphic t ==> ((!f. f continuous_on s /\ IMAGE f s SUBSET s ==> ?x. x IN s /\ (f x = x)) <=> (!g. g continuous_on t /\ IMAGE g t SUBSET t ==> ?y. y IN t /\ (g y = y)))`,(* ------------------------------------------------------------------------- *) (* So the Brouwer theorem for any set with nonempty interior. *) (* ------------------------------------------------------------------------- *)let RETRACT_FIXPOINT_PROPERTY =prove (`!s t:real^N->bool. t retract_of s /\ (!f. f continuous_on s /\ IMAGE f s SUBSET s ==> ?x. x IN s /\ (f x = x)) ==> !g. g continuous_on t /\ IMAGE g t SUBSET t ==> ?y. y IN t /\ (g y = y)`,(* ------------------------------------------------------------------------- *) (* And in particular for a closed ball. *) (* ------------------------------------------------------------------------- *)let BROUWER_WEAK =prove (`!f:real^N->real^N s. compact s /\ convex s /\ ~(interior s = {}) /\ f continuous_on s /\ IMAGE f s SUBSET s ==> ?x. x IN s /\ f x = x`,(* ------------------------------------------------------------------------- *) (* Still more general form; could derive this directly without using the *) (* rather involved HOMEOMORPHIC_CONVEX_COMPACT theorem, just using *) (* a scaling and translation to put the set inside the unit cube. *) (* ------------------------------------------------------------------------- *)let BROUWER_BALL =prove (`!f:real^N->real^N a e. &0 < e /\ f continuous_on cball(a,e) /\ IMAGE f (cball(a,e)) SUBSET (cball(a,e)) ==> ?x. x IN cball(a,e) /\ (f x = x)`,(* ------------------------------------------------------------------------- *) (* So we get the no-retraction theorem, first for a ball, then more general. *) (* ------------------------------------------------------------------------- *)let BROUWER =prove (`!f:real^N->real^N s. compact s /\ convex s /\ ~(s = {}) /\ f continuous_on s /\ IMAGE f s SUBSET s ==> ?x. x IN s /\ f x = x`,let NO_RETRACTION_CBALL =prove (`!a:real^N e. &0 < e ==> ~(sphere(a,e) retract_of cball(a,e))`,let NO_RETRACTION_FRONTIER_BOUNDED =prove (`!s:real^N->bool. bounded s /\ ~(interior s = {}) ==> ~((frontier s) retract_of s)`,(* ------------------------------------------------------------------------- *) (* Similarly we get noncontractibility of a non-trivial sphere. *) (* ------------------------------------------------------------------------- *)let COMPACT_SUBSET_FRONTIER_RETRACTION =prove (`!f:real^N->real^N s. compact s /\ f continuous_on s /\ (!x. x IN frontier s ==> f x = x) ==> s SUBSET IMAGE f s`,(* ------------------------------------------------------------------------- *) (* We also get fixpoint properties for suitable ANRs. *) (* ------------------------------------------------------------------------- *)let CONTRACTIBLE_SPHERE =prove (`!a:real^N r. contractible(sphere(a,r)) <=> r <= &0`,let BROUWER_INESSENTIAL_ANR =prove (`!f:real^N->real^N s t. compact s /\ ~(s = {}) /\ s retract_of t /\ open t /\ f continuous_on s /\ IMAGE f s SUBSET s /\ (?a. homotopic_with (\x. T) (s,s) f (\x. a)) ==> ?x. x IN s /\ f x = x`,let BROUWER_CONTRACTIBLE_ANR =prove (`!f:real^N->real^N s t. compact s /\ contractible s /\ ~(s = {}) /\ s retract_of t /\ open t /\ f continuous_on s /\ IMAGE f s SUBSET s ==> ?x. x IN s /\ f x = x`,(* ------------------------------------------------------------------------- *) (* Some other related fixed-point theorems. *) (* ------------------------------------------------------------------------- *)let FIXED_POINT_INESSENTIAL_SPHERE_MAP =prove (`!f a:real^N r c. &0 < r /\ homotopic_with (\x. T) (sphere(a,r),sphere(a,r)) f (\x. c) ==> ?x. x IN sphere(a,r) /\ f x = x`,(* ------------------------------------------------------------------------- *) (* Bijections between intervals. *) (* ------------------------------------------------------------------------- *)let SCHAUDER_UNIV =prove (`!f:real^N->real^N. f continuous_on (:real^N) /\ bounded (IMAGE f (:real^N)) ==> ?x. f x = x`,let interval_bij = new_definition `interval_bij (a:real^N,b:real^N) (u:real^N,v:real^N) (x:real^N) = (lambda i. u$i + (x$i - a$i) / (b$i - a$i) * (v$i - u$i)):real^N`;;let INTERVAL_BIJ_AFFINE =prove (`interval_bij (a,b) (u,v) = \x. (lambda i. (v$i - u$i) / (b$i - a$i) * x$i) + (lambda i. u$i - (v$i - u$i) / (b$i - a$i) * a$i)`,let CONTINUOUS_INTERVAL_BIJ =prove (`!a b u v x. (interval_bij (a:real^N,b:real^N) (u:real^N,v:real^N)) continuous at x`,let IN_INTERVAL_INTERVAL_BIJ =prove (`!a b u v x:real^N. x IN interval[a,b] /\ ~(interval[u,v] = {}) ==> (interval_bij (a,b) (u,v) x) IN interval[u,v]`,(* ------------------------------------------------------------------------- *) (* Fashoda meet theorem. *) (* ------------------------------------------------------------------------- *)let INTERVAL_BIJ_BIJ =prove (`!a b u v x:real^N. (!i. 1 <= i /\ i <= dimindex(:N) ==> a$i < b$i /\ u$i < v$i) ==> interval_bij (a,b) (u,v) (interval_bij (u,v) (a,b) x) = x`,let INFNORM_EQ_1_2 =prove (`infnorm (x:real^2) = &1 <=> abs(x$1) <= &1 /\ abs(x$2) <= &1 /\ (x$1 = -- &1 \/ x$1 = &1 \/ x$2 = -- &1 \/ x$2 = &1)`,let INFNORM_EQ_1_IMP =prove (`infnorm (x:real^2) = &1 ==> abs(x$1) <= &1 /\ abs(x$2) <= &1`,"negatex"] THEN REWRITE_TAC[VECTOR_2] THENL [DISCH_THEN(MP_TAC o MATCH_MP (REAL_ARITH `--x = -- &1 ==> &0 < x`)); DISCH_THEN(MP_TAC o MATCH_MP (REAL_ARITH `--x = &1 ==> x < &0`)); DISCH_THEN(MP_TAC o MATCH_MP (REAL_ARITH `x = -- &1 ==> x < &0`)); DISCH_THEN(MP_TAC o MATCH_MP (REAL_ARITH `x = &1 ==> &0 < x`))] THEN W(fun (_,w) -> FIRST_X_ASSUM(fun th -> MP_TAC(PART_MATCH (lhs o rand) th (lhand w)))) THEN (ANTS_TAC THENL [REWRITE_TAC[VECTOR_SUB_EQ; ARITH] THEN FIRST_X_ASSUM MATCH_MP_TAC THEN FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [IN_INTERVAL]) THEN ASM_SIMP_TAC[SUBSET; FORALL_IN_IMAGE; IN_INTERVAL_1] THEN SIMP_TAC[IN_INTERVAL; DIMINDEX_2; FORALL_2; VEC_COMPONENT; ARITH; VECTOR_NEG_COMPONENT; DROP_NEG; DROP_VEC; LIFT_DROP] THEN REAL_ARITH_TAC; DISCH_THEN SUBST1_TAC]) THEN ASM_SIMP_TAC[VECTOR_SUB_COMPONENT; DIMINDEX_2; ARITH; LIFT_NEG; LIFT_NUM] THENL [MATCH_MP_TAC(REAL_ARITH `abs(x$1) <= &1 /\ abs(x$2) <= &1 ==> ~(&0 < -- &1 - x$1)`); MATCH_MP_TAC(REAL_ARITH `abs(x$1) <= &1 /\ abs(x$2) <= &1 ==> ~(&1 - x$1 < &0)`); MATCH_MP_TAC(REAL_ARITH `abs(x$1) <= &1 /\ abs(x$2) <= &1 ==> ~(x$2 - -- &1 < &0)`); MATCH_MP_TAC(REAL_ARITH `abs(x$1) <= &1 /\ abs(x$2) <= &1 ==> ~(&0 < x$2 - &1)`)] THEN (SUBGOAL_THEN `!z:real^2. abs(z$1) <= &1 /\ abs(z$2) <= &1 <=> z IN interval[--vec 1,vec 1]` (fun th -> REWRITE_TAC[th]) THENL [SIMP_TAC[IN_INTERVAL; DIMINDEX_2; FORALL_2; VEC_COMPONENT; ARITH; VECTOR_NEG_COMPONENT; DROP_NEG; DROP_VEC; LIFT_DROP] THEN REAL_ARITH_TAC; ALL_TAC]) THEN FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (SET_RULE `IMAGE f s SUBSET t ==> x IN s ==> f x IN t`)) THEN REWRITE_TAC[IN_INTERVAL_1; DROP_NEG; DROP_VEC; LIFT_DROP] THEN ASM_REWRITE_TAC[REAL_BOUNDS_LE]);;let FASHODA_UNIT =prove (`!f:real^1->real^2 g:real^1->real^2. IMAGE f (interval[--vec 1,vec 1]) SUBSET interval[--vec 1,vec 1] /\ IMAGE g (interval[--vec 1,vec 1]) SUBSET interval[--vec 1,vec 1] /\ f continuous_on interval[--vec 1,vec 1] /\ g continuous_on interval[--vec 1,vec 1] /\ f(--vec 1)$1 = -- &1 /\ f(vec 1)$1 = &1 /\ g(--vec 1)$2 = -- &1 /\ g(vec 1)$2 = &1 ==> ?s t. s IN interval[--vec 1,vec 1] /\ t IN interval[--vec 1,vec 1] /\ f(s) = g(t)`,let FASHODA_UNIT_PATH =prove (`!f:real^1->real^2 g:real^1->real^2. path f /\ path g /\ path_image f SUBSET interval[--vec 1,vec 1] /\ path_image g SUBSET interval[--vec 1,vec 1] /\ (pathstart f)$1 = -- &1 /\ (pathfinish f)$1 = &1 /\ (pathstart g)$2 = -- &1 /\ (pathfinish g)$2 = &1 ==> ?z. z IN path_image f /\ z IN path_image g`,(* ------------------------------------------------------------------------- *) (* Some slightly ad hoc lemmas I use below *) (* ------------------------------------------------------------------------- *) (* ------------------------------------------------------------------------- *) (* Useful Fashoda corollary pointed out to me by Tom Hales. *) (* ------------------------------------------------------------------------- *)let FASHODA =prove (`!f g a b:real^2. path f /\ path g /\ path_image f SUBSET interval[a,b] /\ path_image g SUBSET interval[a,b] /\ (pathstart f)$1 = a$1 /\ (pathfinish f)$1 = b$1 /\ (pathstart g)$2 = a$2 /\ (pathfinish g)$2 = b$2 ==> ?z. z IN path_image f /\ z IN path_image g`,(* ------------------------------------------------------------------------- *) (* Complement in dimension N >= 2 of set homeomorphic to any interval in *) (* any dimension is (path-)connected. This naively generalizes the argument *) (* in Ryuji Maehara's paper "The Jordan curve theorem via the Brouwer *) (* fixed point theorem", American Mathematical Monthly 1984. *) (* ------------------------------------------------------------------------- *)let FASHODA_INTERLACE =prove (`!f g a b:real^2. path f /\ path g /\ path_image f SUBSET interval[a,b] /\ path_image g SUBSET interval[a,b] /\ (pathstart f)$2 = a$2 /\ (pathfinish f)$2 = a$2 /\ (pathstart g)$2 = a$2 /\ (pathfinish g)$2 = a$2 /\ (pathstart f)$1 < (pathstart g)$1 /\ (pathstart g)$1 < (pathfinish f)$1 /\ (pathfinish f)$1 < (pathfinish g)$1 ==> ?z. z IN path_image f /\ z IN path_image g`,let UNBOUNDED_COMPONENTS_COMPLEMENT_ABSOLUTE_RETRACT =prove (`!s c. compact s /\ s retract_of (:real^N) /\ c IN components((:real^N) DIFF s) ==> ~bounded c`,let CONNECTED_COMPLEMENT_ABSOLUTE_RETRACT =prove (`!s. 2 <= dimindex(:N) /\ compact s /\ s retract_of (:real^N) ==> connected((:real^N) DIFF s)`,let PATH_CONNECTED_COMPLEMENT_ABSOLUTE_RETRACT =prove (`!s:real^N->bool. 2 <= dimindex(:N) /\ compact s /\ s retract_of (:real^N) ==> path_connected((:real^N) DIFF s)`,(* ------------------------------------------------------------------------- *) (* In particular, apply all these to the special case of an arc. *) (* ------------------------------------------------------------------------- *)let PATH_CONNECTED_COMPLEMENT_HOMEOMORPHIC_CONVEX_COMPACT =prove (`!s:real^N->bool t:real^M->bool. 2 <= dimindex(:N) /\ s homeomorphic t /\ convex t /\ compact t ==> path_connected((:real^N) DIFF s)`,let RETRACTION_ARC =prove (`!p. arc p ==> ?f. f continuous_on (:real^N) /\ IMAGE f (:real^N) SUBSET path_image p /\ (!x. x IN path_image p ==> f x = x)`,(* ------------------------------------------------------------------------- *) (* The Jordan curve theorem, again approximately following Maehara. *) (* ------------------------------------------------------------------------- *)let INSIDE_ARC_EMPTY =prove (`!p:real^1->real^N. arc p ==> inside(path_image p) = {}`,"n"] THEN SIMP_TAC[BASIS_COMPONENT; VECTOR_MUL_COMPONENT; DIMINDEX_2; ARITH] THEN REWRITE_TAC[midpoint; VECTOR_ADD_COMPONENT; VECTOR_MUL_COMPONENT] THEN ASM_REWRITE_TAC[] THEN CONV_TAC REAL_RAT_REDUCE_CONV; ALL_TAC] THEN SUBGOAL_THEN `(y:real^2)$2 = ((p:real^2)$2 + (q:real^2)$2) / &2` ASSUME_TAC THENL [EXPAND_TAC "y" THEN REWRITE_TAC[midpoint; VECTOR_ADD_COMPONENT; VECTOR_MUL_COMPONENT] THEN REAL_ARITH_TAC; ALL_TAC] THEN SUBGOAL_THEN `(n:real^2)$2 = &2` ASSUME_TAC THENL [EXPAND_TAC "n" THEN SIMP_TAC[BASIS_COMPONENT; VECTOR_MUL_COMPONENT; DIMINDEX_2; ARITH] THEN REAL_ARITH_TAC; ALL_TAC] THEN SUBGOAL_THEN `(b:real^2)$2 <= (q:real^2)$2` ASSUME_TAC THENL [ASM_MESON_TAC[IN_UNION]; ALL_TAC] THEN SUBGOAL_THEN `((abs((q:real^2)$2) <= &9 / &5 /\ abs(q$2) < &2) /\ q IN interval[--vector[&1; &9 / &5],vector[&1; &9 / &5]] /\ q IN interval[--vector[&1; &2],vector[&1; &2]]) /\ ((abs((b:real^2)$2) <= &9 / &5 /\ abs(b$2) < &2) /\ b IN interval[--vector[&1; &9 / &5],vector[&1; &9 / &5]] /\ b IN interval[--vector[&1; &2],vector[&1; &2]])` STRIP_ASSUME_TAC THENL [CONJ_TAC THEN MATCH_MP_TAC(TAUT `a /\ (a ==> b) ==> a /\ b`) THEN (CONJ_TAC THENL [ASM_MESON_TAC[IN_UNION]; ALL_TAC]) THEN ASM_REWRITE_TAC[IN_INTERVAL; FORALL_2; DIMINDEX_2; VECTOR_2; VECTOR_NEG_COMPONENT] THEN REAL_ARITH_TAC; ALL_TAC] THEN SUBGOAL_THEN `path_image(h:real^1->real^2) SUBSET interval[--vector[&1; &9 / &5],vector[&1; &9 / &5]] /\ path_image h SUBSET interval[--vector[&1; &2],vector[&1; &2]] /\ path_image l SUBSET interval[--vector[&1; &9 / &5],vector[&1; &9 / &5]] /\ path_image(l:real^1->real^2) SUBSET interval[--vector[&1; &2],vector[&1; &2]] /\ ~(basis 1 IN path_image h) /\ ~(basis 1 IN path_image l) /\ ~(--basis 1 IN path_image h) /\ ~(--basis 1 IN path_image l)` STRIP_ASSUME_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN SUBGOAL_THEN `(n:real^2) IN interval[--vector[&1; &2],vector[&1; &2]] /\ (--n) IN interval[--vector[&1; &2],vector[&1; &2]]` STRIP_ASSUME_TAC THENL [ASM_REWRITE_TAC[IN_INTERVAL; DIMINDEX_2; FORALL_2; VECTOR_2; VECTOR_NEG_COMPONENT] THEN CONV_TAC REAL_RAT_REDUCE_CONV; ALL_TAC] THEN SUBGOAL_THEN `(q:real^2)$2 < (y:real^2)$2 /\ (y:real^2)$2 < (p:real^2)$2 /\ (q:real^2)$2 <= (y:real^2)$2 /\ (y:real^2)$2 <= (p:real^2)$2` STRIP_ASSUME_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC] THEN REWRITE_TAC[SYM(ASSUME `path_image(U ++ D):real^2->bool = path_image U UNION path_image D`)] THEN ASM_REWRITE_TAC[] THEN SUBGOAL_THEN `(y:real^2) IN K` ASSUME_TAC THENL [EXPAND_TAC "K" THEN REWRITE_TAC[IN_UNIV; IN_DIFF] THEN ASM_REWRITE_TAC[IN_UNION; DE_MORGAN_THM] THEN ASM_MESON_TAC[REAL_NOT_LE]; ASM_REWRITE_TAC[]] THEN SUBGOAL_THEN `(n:real^2) IN K` ASSUME_TAC THENL [EXPAND_TAC "K" THEN ASM_REWRITE_TAC[IN_DIFF; IN_UNIV] THEN ASM_MESON_TAC[REAL_ARITH `~(abs x < x)`]; ASM_REWRITE_TAC[]] THEN MATCH_MP_TAC(TAUT `(a /\ b ==> c) /\ b /\ a /\ d ==> a /\ b /\ c /\ d`) THEN CONJ_TAC THENL [MESON_TAC[CONNECTED_COMPONENT_NONOVERLAP]; ALL_TAC] THEN SUBGOAL_THEN `(y:real^2) IN interval[--vector [&1; &9 / &5],vector [&1; &9 / &5]] /\ (y:real^2) IN interval[--vector [&1; &2],vector [&1; &2]]` STRIP_ASSUME_TAC THENL [REWRITE_TAC[IN_INTERVAL; FORALL_2; DIMINDEX_2; VECTOR_2; VECTOR_NEG_COMPONENT] THEN ASM_REAL_ARITH_TAC; ALL_TAC] THEN SUBGOAL_THEN `((:real^2) DIFF interval[--vector [&1; &9 / &5],vector [&1; &9 / &5]]) SUBSET connected_component K n /\ ((:real^2) DIFF interval[--vector [&1; &2],vector [&1; &2]]) SUBSET connected_component K n` STRIP_ASSUME_TAC THENL [MATCH_MP_TAC(SET_RULE `i SUBSET j /\ UNIV DIFF i SUBSET s ==> UNIV DIFF i SUBSET s /\ UNIV DIFF j SUBSET s`) THEN REWRITE_TAC[SUBSET_INTERVAL; DIMINDEX_2; FORALL_2; VECTOR_2; VECTOR_NEG_COMPONENT] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN MATCH_MP_TAC CONNECTED_COMPONENT_MAXIMAL THEN SIMP_TAC[CONNECTED_COMPLEMENT_BOUNDED_CONVEX; LE_REFL; DIMINDEX_2; BOUNDED_INTERVAL; CONVEX_INTERVAL] THEN EXPAND_TAC "K" THEN ASM_REWRITE_TAC[SET_RULE `UNIV DIFF s SUBSET UNIV DIFF t <=> t SUBSET s`; UNION_SUBSET] THEN ASM_REWRITE_TAC[IN_UNIV; IN_DIFF; IN_INTERVAL; FORALL_2; DIMINDEX_2; VECTOR_2; VECTOR_NEG_COMPONENT] THEN CONV_TAC REAL_RAT_REDUCE_CONV; ALL_TAC] THEN SUBGOAL_THEN `~bounded(connected_component K (n:real^2))` ASSUME_TAC THENL [MATCH_MP_TAC COBOUNDED_IMP_UNBOUNDED THEN MATCH_MP_TAC BOUNDED_SUBSET THEN EXISTS_TAC `interval[--vector[&1; &2]:real^2,vector [&1; &2]]` THEN ONCE_REWRITE_TAC[SET_RULE `UNIV DIFF s SUBSET t <=> UNIV DIFF t SUBSET s`] THEN ASM_REWRITE_TAC[BOUNDED_INTERVAL]; ASM_REWRITE_TAC[]] THEN SUBGOAL_THEN `bounded(connected_component K (y:real^2))` ASSUME_TAC THENL [REWRITE_TAC[bounded] THEN EXISTS_TAC `&4` THEN X_GEN_TAC `z:real^2` THEN REWRITE_TAC[GSYM REAL_NOT_LT] THEN ASM_SIMP_TAC[GSYM OPEN_PATH_CONNECTED_COMPONENT] THEN REWRITE_TAC[path_component; IN] THEN DISCH_THEN(X_CHOOSE_THEN `i:real^1->real^2` STRIP_ASSUME_TAC) THEN STRIP_TAC THEN MP_TAC(ISPECL [`i:real^1->real^2`; `interval[--vector[&1; &2]:real^2,vector[&1; &2]]`] EXISTS_PATH_SUBPATH_TO_FRONTIER_CLOSED) THEN ASM_REWRITE_TAC[CLOSED_INTERVAL; NOT_IMP; SUBSET_INTER; GSYM CONJ_ASSOC] THEN CONJ_TAC THENL [REWRITE_TAC[IN_INTERVAL; VECTOR_2; DIMINDEX_2; FORALL_2; VECTOR_NEG_COMPONENT; GSYM REAL_ABS_BOUNDS] THEN STRIP_TAC THEN UNDISCH_TAC `&4 < norm(z:real^2)` THEN REWRITE_TAC[REAL_NOT_LT] THEN W(MP_TAC o PART_MATCH lhand NORM_LE_L1 o lhand o snd) THEN REWRITE_TAC[DIMINDEX_2; SUM_2] THEN ASM_REAL_ARITH_TAC; REWRITE_TAC[IN_DIFF; FRONTIER_CLOSED_INTERVAL; IN_INTERVAL; FORALL_2; DIMINDEX_2; VECTOR_2; VECTOR_NEG_COMPONENT] THEN DISCH_THEN(X_CHOOSE_THEN `j:real^1->real^2` MP_TAC) THEN REPEAT(DISCH_THEN(CONJUNCTS_THEN2 STRIP_ASSUME_TAC MP_TAC)) THEN ASM_REWRITE_TAC[REAL_LT_LE; REAL_ARITH `x:real = i$j <=> i$j = x`] THEN REWRITE_TAC[GSYM DE_MORGAN_THM; GSYM DISJ_ASSOC] THEN DISCH_TAC] THEN SUBGOAL_THEN `path_image(j:real^1->real^2) SUBSET K` ASSUME_TAC THENL [ASM_MESON_TAC[SUBSET_TRANS]; ALL_TAC] THEN SUBGOAL_THEN `~(pathfinish(j):real^2 = basis 1) /\ ~(pathfinish(j):real^2 = --basis 1)` STRIP_ASSUME_TAC THENL [REPEAT STRIP_TAC THEN UNDISCH_THEN `path_image(j:real^1->real^2) SUBSET K` (MP_TAC o SPEC `pathfinish(j):real^2` o REWRITE_RULE[SUBSET]) THEN ASM_REWRITE_TAC[PATHFINISH_IN_PATH_IMAGE] THEN EXPAND_TAC "K" THEN ASM_REWRITE_TAC[IN_DIFF; IN_UNIV; IN_UNION]; ALL_TAC] THEN SUBGOAL_THEN `?e:real^1->real^2. path e /\ pathstart e = y /\ ((pathfinish e)$2 = -- &2 \/ (pathfinish e)$2 = &2) /\ path_image e SUBSET K /\ path_image e SUBSET interval[--vector [&1; &2],vector [&1; &2]]` MP_TAC THENL [FIRST_X_ASSUM(DISJ_CASES_THEN STRIP_ASSUME_TAC) THENL [UNDISCH_TAC `~((pathfinish j):real^2 = --basis 1)` THEN SIMP_TAC[CART_EQ; DIMINDEX_2; FORALL_2; BASIS_COMPONENT; VECTOR_NEG_COMPONENT; ARITH] THEN ASM_REWRITE_TAC[] THEN DISCH_THEN(DISJ_CASES_TAC o MATCH_MP (REAL_ARITH `~(x = -- &0) ==> x < &0 \/ &0 < x`)) THENL [EXISTS_TAC `(j:real^1->real^2) ++ linepath(pathfinish j,--vector [&1; &2])` THEN ASM_SIMP_TAC[PATH_JOIN; PATHSTART_JOIN; PATHFINISH_JOIN; PATH_LINEPATH; PATHSTART_LINEPATH; PATHFINISH_LINEPATH; PATH_IMAGE_JOIN] THEN REWRITE_TAC[VECTOR_2; VECTOR_NEG_COMPONENT] THEN REWRITE_TAC[UNION_SUBSET; PATH_IMAGE_LINEPATH] THEN ONCE_REWRITE_TAC[AC CONJ_ACI `(a /\ b) /\ c /\ d <=> (a /\ c) /\ b /\ d`] THEN CONJ_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN EXPAND_TAC "K" THEN MATCH_MP_TAC(SET_RULE `(!x. x IN s ==> x IN t /\ ~(x IN u)) ==> s SUBSET (UNIV DIFF u) /\ s SUBSET t`) THEN X_GEN_TAC `x:real^2` THEN DISCH_TAC THEN MP_TAC(ISPECL [`pathfinish(j:real^1->real^2)`; `--vector[&1; &2]:real^2`; `x:real^2`] SEGMENT_VERTICAL) THEN ASM_SIMP_TAC[VECTOR_NEG_COMPONENT; VECTOR_2; IN_INTERVAL; FORALL_2; DIMINDEX_2] THEN DISCH_TAC THEN CONJ_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC] THEN DISCH_TAC THEN UNDISCH_THEN `!z:real^2. z IN path_image U UNION path_image D /\ z$1 = -- &1 <=> z = --basis 1` (MP_TAC o SPEC `x:real^2`) THEN ASM_REWRITE_TAC[] THEN ASM_SIMP_TAC[CART_EQ; DIMINDEX_2; FORALL_2; BASIS_COMPONENT; VECTOR_NEG_COMPONENT; ARITH; REAL_NEG_0] THEN ASM_REAL_ARITH_TAC; EXISTS_TAC `(j:real^1->real^2) ++ linepath(pathfinish j,vector [-- &1; &2])` THEN ASM_SIMP_TAC[PATH_JOIN; PATHSTART_JOIN; PATHFINISH_JOIN; PATH_LINEPATH; PATHSTART_LINEPATH; PATHFINISH_LINEPATH; PATH_IMAGE_JOIN] THEN REWRITE_TAC[VECTOR_2; VECTOR_NEG_COMPONENT] THEN REWRITE_TAC[UNION_SUBSET; PATH_IMAGE_LINEPATH] THEN ONCE_REWRITE_TAC[AC CONJ_ACI `(a /\ b) /\ c /\ d <=> (a /\ c) /\ b /\ d`] THEN CONJ_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN EXPAND_TAC "K" THEN MATCH_MP_TAC(SET_RULE `(!x. x IN s ==> x IN t /\ ~(x IN u)) ==> s SUBSET (UNIV DIFF u) /\ s SUBSET t`) THEN X_GEN_TAC `x:real^2` THEN DISCH_TAC THEN MP_TAC(ISPECL [`pathfinish(j:real^1->real^2)`; `vector[-- &1; &2]:real^2`; `x:real^2`] SEGMENT_VERTICAL) THEN ASM_SIMP_TAC[VECTOR_NEG_COMPONENT; VECTOR_2; IN_INTERVAL; FORALL_2; DIMINDEX_2] THEN DISCH_TAC THEN CONJ_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC] THEN DISCH_TAC THEN UNDISCH_THEN `!z:real^2. z IN path_image U UNION path_image D /\ z$1 = -- &1 <=> z = --basis 1` (MP_TAC o SPEC `x:real^2`) THEN ASM_REWRITE_TAC[] THEN ASM_SIMP_TAC[CART_EQ; DIMINDEX_2; FORALL_2; BASIS_COMPONENT; VECTOR_NEG_COMPONENT; ARITH; REAL_NEG_0] THEN ASM_REAL_ARITH_TAC]; UNDISCH_TAC `~((pathfinish j):real^2 = basis 1)` THEN SIMP_TAC[CART_EQ; DIMINDEX_2; FORALL_2; BASIS_COMPONENT; VECTOR_NEG_COMPONENT; ARITH] THEN ASM_REWRITE_TAC[] THEN DISCH_THEN(DISJ_CASES_TAC o MATCH_MP (REAL_ARITH `~(x = &0) ==> x < &0 \/ &0 < x`)) THENL [EXISTS_TAC `(j:real^1->real^2) ++ linepath(pathfinish j,vector [&1; -- &2])` THEN ASM_SIMP_TAC[PATH_JOIN; PATHSTART_JOIN; PATHFINISH_JOIN; PATH_LINEPATH; PATHSTART_LINEPATH; PATHFINISH_LINEPATH; PATH_IMAGE_JOIN] THEN REWRITE_TAC[VECTOR_2; VECTOR_NEG_COMPONENT] THEN REWRITE_TAC[UNION_SUBSET; PATH_IMAGE_LINEPATH] THEN ONCE_REWRITE_TAC[AC CONJ_ACI `(a /\ b) /\ c /\ d <=> (a /\ c) /\ b /\ d`] THEN CONJ_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN EXPAND_TAC "K" THEN MATCH_MP_TAC(SET_RULE `(!x. x IN s ==> x IN t /\ ~(x IN u)) ==> s SUBSET (UNIV DIFF u) /\ s SUBSET t`) THEN X_GEN_TAC `x:real^2` THEN DISCH_TAC THEN MP_TAC(ISPECL [`pathfinish(j:real^1->real^2)`; `vector[&1; -- &2]:real^2`; `x:real^2`] SEGMENT_VERTICAL) THEN ASM_SIMP_TAC[VECTOR_NEG_COMPONENT; VECTOR_2; IN_INTERVAL; FORALL_2; DIMINDEX_2] THEN DISCH_TAC THEN CONJ_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC] THEN DISCH_TAC THEN UNDISCH_THEN `!z:real^2. z IN path_image U UNION path_image D /\ z$1 = &1 <=> z = basis 1` (MP_TAC o SPEC `x:real^2`) THEN ASM_REWRITE_TAC[] THEN ASM_SIMP_TAC[CART_EQ; DIMINDEX_2; FORALL_2; BASIS_COMPONENT; VECTOR_NEG_COMPONENT; ARITH; REAL_NEG_0] THEN ASM_REAL_ARITH_TAC; EXISTS_TAC `(j:real^1->real^2) ++ linepath(pathfinish j,vector [&1; &2])` THEN ASM_SIMP_TAC[PATH_JOIN; PATHSTART_JOIN; PATHFINISH_JOIN; PATH_LINEPATH; PATHSTART_LINEPATH; PATHFINISH_LINEPATH; PATH_IMAGE_JOIN] THEN REWRITE_TAC[VECTOR_2; VECTOR_NEG_COMPONENT] THEN REWRITE_TAC[UNION_SUBSET; PATH_IMAGE_LINEPATH] THEN ONCE_REWRITE_TAC[AC CONJ_ACI `(a /\ b) /\ c /\ d <=> (a /\ c) /\ b /\ d`] THEN CONJ_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN EXPAND_TAC "K" THEN MATCH_MP_TAC(SET_RULE `(!x. x IN s ==> x IN t /\ ~(x IN u)) ==> s SUBSET (UNIV DIFF u) /\ s SUBSET t`) THEN X_GEN_TAC `x:real^2` THEN DISCH_TAC THEN MP_TAC(ISPECL [`pathfinish(j:real^1->real^2)`; `vector[&1; &2]:real^2`; `x:real^2`] SEGMENT_VERTICAL) THEN ASM_SIMP_TAC[VECTOR_NEG_COMPONENT; VECTOR_2; IN_INTERVAL; FORALL_2; DIMINDEX_2] THEN DISCH_TAC THEN CONJ_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC] THEN DISCH_TAC THEN UNDISCH_THEN `!z:real^2. z IN path_image U UNION path_image D /\ z$1 = &1 <=> z = basis 1` (MP_TAC o SPEC `x:real^2`) THEN ASM_REWRITE_TAC[] THEN ASM_SIMP_TAC[CART_EQ; DIMINDEX_2; FORALL_2; BASIS_COMPONENT; VECTOR_NEG_COMPONENT; ARITH; REAL_NEG_0] THEN ASM_REAL_ARITH_TAC]; EXISTS_TAC `j:real^1->real^2` THEN ASM_REWRITE_TAC[]; EXISTS_TAC `j:real^1->real^2` THEN ASM_REWRITE_TAC[]]; FIRST_X_ASSUM(K ALL_TAC o check (is_disj o concl))] THEN STRIP_TAC THENL [MP_TAC(ISPECL [`reversepath(D:real^1->real^2)`; `reversepath e ++ linepath(y,p) ++ reversepath h ++ linepath(t:real^2,vector[t$1;&2])`; `--vector[&1; &2]:real^2`; `vector[&1; &2]:real^2`] FASHODA) THEN ASM_SIMP_TAC [PATH_REVERSEPATH; ARC_IMP_PATH; PATH_JOIN; PATH_LINEPATH; PATHSTART_LINEPATH; PATHFINISH_LINEPATH; PATHSTART_REVERSEPATH; PATHFINISH_REVERSEPATH; PATH_IMAGE_JOIN; PATHSTART_JOIN; PATHFINISH_JOIN; PATH_IMAGE_REVERSEPATH] THEN SIMP_TAC[VECTOR_2; VECTOR_NEG_COMPONENT; BASIS_COMPONENT; DIMINDEX_2; ARITH; NOT_IMP; GSYM CONJ_ASSOC] THEN CONJ_TAC THENL [ASM_SIMP_TAC[UNION_SUBSET; PATH_IMAGE_LINEPATH; SEGMENT_CONVEX_HULL; SUBSET_HULL; CONVEX_INTERVAL; INSERT_SUBSET; EMPTY_SUBSET] THEN REWRITE_TAC[IN_INTERVAL; DIMINDEX_2; FORALL_2; VECTOR_NEG_COMPONENT; VECTOR_2] THEN CONV_TAC REAL_RAT_REDUCE_CONV; DISCH_THEN(X_CHOOSE_THEN `x:real^2` (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN REWRITE_TAC[DE_MORGAN_THM; IN_UNION] THEN REPEAT CONJ_TAC THENL [ASM SET_TAC[]; REWRITE_TAC[PATH_IMAGE_LINEPATH] THEN DISCH_TAC THEN MP_TAC(ISPECL [`y:real^2`; `p:real^2`; `x:real^2`] SEGMENT_VERTICAL) THEN ASM_REWRITE_TAC[] THEN UNDISCH_THEN `!z:real^2. z$2 <= (p:real^2)$2 /\ z$1 = &0 /\ z IN path_image D ==> z$2 <= (q:real^2)$2` (MP_TAC o SPEC `x:real^2`) THEN ASM_REWRITE_TAC[] THEN ASM_REAL_ARITH_TAC; DISCH_TAC THEN UNDISCH_THEN `path_image(h:real^1->real^2) SUBSET (path_image U) DIFF {pathstart U, pathfinish U}` (MP_TAC o SPEC `x:real^2` o REWRITE_RULE[SUBSET]) THEN ASM_REWRITE_TAC[] THEN ASM SET_TAC[]; REWRITE_TAC[PATH_IMAGE_LINEPATH] THEN DISCH_TAC THEN MP_TAC(ISPECL [`t:real^2`; `vector[&0;&2]:real^2`; `x:real^2`] SEGMENT_VERTICAL) THEN ASM_REWRITE_TAC[VECTOR_2] THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN ASM_CASES_TAC `x:real^2 = t` THENL [ASM_MESON_TAC[]; UNDISCH_TAC `~(x:real^2 = t)`] THEN ASM_REWRITE_TAC[CART_EQ; DIMINDEX_2; FORALL_2] THEN UNDISCH_THEN `!z:real^2. z$1 = &0 /\ z IN path_image U UNION path_image D ==> z$2 <= (t:real^2)$2` (MP_TAC o SPEC `x:real^2`) THEN ASM_REWRITE_TAC[IN_UNION] THEN ASM_REAL_ARITH_TAC]]; MP_TAC(ISPECL [`U:real^1->real^2`; `linepath(vector[b$1; -- &2],b) ++ reversepath l ++ linepath(q:real^2,y) ++ e`; `--vector[&1; &2]:real^2`; `vector[&1; &2]:real^2`] FASHODA) THEN ASM_SIMP_TAC [PATH_REVERSEPATH; ARC_IMP_PATH; PATH_JOIN; PATH_LINEPATH; PATHSTART_LINEPATH; PATHFINISH_LINEPATH; PATHSTART_REVERSEPATH; PATHFINISH_REVERSEPATH; PATH_IMAGE_JOIN; PATHSTART_JOIN; PATHFINISH_JOIN; PATH_IMAGE_REVERSEPATH] THEN SIMP_TAC[VECTOR_2; VECTOR_NEG_COMPONENT; BASIS_COMPONENT; DIMINDEX_2; ARITH; NOT_IMP; GSYM CONJ_ASSOC] THEN CONJ_TAC THENL [ASM_SIMP_TAC[UNION_SUBSET; PATH_IMAGE_LINEPATH; SEGMENT_CONVEX_HULL; SUBSET_HULL; CONVEX_INTERVAL; INSERT_SUBSET; EMPTY_SUBSET] THEN REWRITE_TAC[IN_INTERVAL; DIMINDEX_2; FORALL_2; VECTOR_NEG_COMPONENT; VECTOR_2] THEN CONV_TAC REAL_RAT_REDUCE_CONV; DISCH_THEN(X_CHOOSE_THEN `x:real^2` (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN REWRITE_TAC[DE_MORGAN_THM; IN_UNION] THEN REPEAT CONJ_TAC THENL [REWRITE_TAC[PATH_IMAGE_LINEPATH] THEN DISCH_TAC THEN MP_TAC(ISPECL [`vector[&0; -- &2]:real^2`; `b:real^2`; `x:real^2`] SEGMENT_VERTICAL) THEN ASM_REWRITE_TAC[VECTOR_2] THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN ASM_CASES_TAC `x:real^2 = b` THENL [ASM_MESON_TAC[]; UNDISCH_TAC `~(x:real^2 = b)`] THEN ASM_REWRITE_TAC[CART_EQ; DIMINDEX_2; FORALL_2] THEN UNDISCH_THEN `!z:real^2. z$1 = &0 /\ z IN path_image U ==> (p:real^2)$2 <= z$2` (MP_TAC o SPEC `x:real^2`) THEN ASM_REWRITE_TAC[] THEN ASM_REAL_ARITH_TAC; DISCH_TAC THEN UNDISCH_THEN `path_image(l:real^1->real^2) SUBSET (path_image D) DIFF {pathstart D, pathfinish D}` (MP_TAC o SPEC `x:real^2` o REWRITE_RULE[SUBSET]) THEN ASM_REWRITE_TAC[] THEN ASM SET_TAC[]; REWRITE_TAC[PATH_IMAGE_LINEPATH] THEN DISCH_TAC THEN MP_TAC(ISPECL [`q:real^2`; `y:real^2`; `x:real^2`] SEGMENT_VERTICAL) THEN ASM_REWRITE_TAC[] THEN UNDISCH_THEN `!z:real^2. z$1 = &0 /\ z IN path_image U ==> (p:real^2)$2 <= z$2` (MP_TAC o SPEC `x:real^2`) THEN ASM_REWRITE_TAC[] THEN ASM_REAL_ARITH_TAC; ASM SET_TAC[]]]]; ASM_REWRITE_TAC[]] THEN SUBGOAL_THEN `!x:real^2. x IN K /\ ~bounded(connected_component K x) ==> connected_component K x = connected_component K n` ASSUME_TAC THENL [X_GEN_TAC `z:real^2` THEN DISCH_TAC THEN MATCH_MP_TAC COBOUNDED_UNIQUE_UNBOUNDED_COMPONENT THEN ASM_REWRITE_TAC[DIMINDEX_2; LE_REFL] THEN EXPAND_TAC "K" THEN REWRITE_TAC[SET_RULE `UNIV DIFF (UNIV DIFF s) = s`] THEN ASM_SIMP_TAC[COMPACT_PATH_IMAGE; COMPACT_IMP_BOUNDED; SIMPLE_PATH_IMP_PATH]; ALL_TAC] THEN SUBGOAL_THEN `!x:real^2. x IN K ==> frontier(connected_component K x) = path_image U UNION path_image D` ASSUME_TAC THENL [X_GEN_TAC `x:real^2` THEN DISCH_TAC THEN REWRITE_TAC[frontier] THEN ASM_SIMP_TAC[OPEN_CONNECTED_COMPONENT; INTERIOR_OPEN] THEN MATCH_MP_TAC(SET_RULE `s SUBSET t /\ ~(s PSUBSET t) ==> s = t`) THEN CONJ_TAC THENL [REWRITE_TAC[SUBSET; IN_DIFF] THEN X_GEN_TAC `w:real^2` THEN ASM_CASES_TAC `(w:real^2) IN K` THENL [ALL_TAC; ASM SET_TAC[]] THEN ASM_SIMP_TAC[IN_CLOSURE_CONNECTED_COMPONENT] THEN CONV_TAC TAUT; DISCH_TAC] THEN SUBGOAL_THEN `?A:real^1->real^2. arc A /\ (closure (connected_component K x) DIFF connected_component K x) SUBSET path_image A /\ path_image A SUBSET path_image(U) UNION path_image(D)` STRIP_ASSUME_TAC THENL [SUBST1_TAC(SYM(ASSUME `path_image(U ++ D:real^1->real^2) = path_image U UNION path_image D`)) THEN MATCH_MP_TAC EXISTS_ARC_PSUBSET_SIMPLE_PATH THEN ASM_REWRITE_TAC[] THEN ASM_SIMP_TAC[CLOSED_DIFF; CLOSED_CLOSURE; OPEN_CONNECTED_COMPONENT]; ALL_TAC] THEN MP_TAC(ISPEC `A:real^1->real^2` RETRACTION_ARC) THEN ASM_REWRITE_TAC[] THEN DISCH_THEN(X_CHOOSE_THEN `rr:real^2->real^2` STRIP_ASSUME_TAC) THEN ASM_CASES_TAC `bounded(connected_component K (x:real^2))` THENL [MP_TAC(ISPECL [`connected_component K (x:real^2)`; `path_image(A:real^1->real^2)`; `rr:real^2->real^2`] FRONTIER_SUBSET_RETRACTION) THEN ASM_REWRITE_TAC[NOT_IMP; GSYM CONJ_ASSOC] THEN ASM_SIMP_TAC[frontier; INTERIOR_OPEN; OPEN_CONNECTED_COMPONENT] THEN CONJ_TAC THENL [ASM_MESON_TAC[CONTINUOUS_ON_SUBSET; SUBSET_UNIV]; ALL_TAC] THEN CONJ_TAC THENL [ASM SET_TAC[]; REWRITE_TAC[SUBSET]] THEN DISCH_THEN(MP_TAC o SPEC `x:real^2`) THEN GEN_REWRITE_TAC (LAND_CONV o LAND_CONV) [IN] THEN ASM_REWRITE_TAC[CONNECTED_COMPONENT_REFL_EQ] THEN DISCH_TAC THEN UNDISCH_TAC `(x:real^2) IN K` THEN UNDISCH_TAC `path_image(A:real^1->real^2) SUBSET path_image U UNION path_image D` THEN REWRITE_TAC[SUBSET] THEN EXPAND_TAC "K" THEN REWRITE_TAC[IN_UNIV; IN_DIFF] THEN DISCH_THEN(MP_TAC o SPEC `x:real^2`) THEN ASM_REWRITE_TAC[]; MP_TAC(ISPECL [`(:real^2) DIFF (connected_component K (x:real^2))`; `path_image(A:real^1->real^2)`; `rr:real^2->real^2`] FRONTIER_SUBSET_RETRACTION) THEN ASM_REWRITE_TAC[FRONTIER_COMPLEMENT; NOT_IMP; GSYM CONJ_ASSOC] THEN UNDISCH_THEN `!x:real^2. x IN K /\ ~bounded (connected_component K x) ==> connected_component K x = connected_component K n` (MP_TAC o SPEC `x:real^2`) THEN ASM_REWRITE_TAC[] THEN DISCH_THEN SUBST_ALL_TAC THEN REPEAT CONJ_TAC THENL [MATCH_MP_TAC BOUNDED_SUBSET THEN EXISTS_TAC `interval[--vector[&1; &2]:real^2,vector [&1; &2]]` THEN ONCE_REWRITE_TAC[SET_RULE `UNIV DIFF s SUBSET t <=> UNIV DIFF t SUBSET s`] THEN ASM_REWRITE_TAC[BOUNDED_INTERVAL]; REWRITE_TAC[frontier] THEN FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP (SET_RULE `s DIFF t SUBSET u ==> t' = t ==> s DIFF t' SUBSET u`)) THEN MATCH_MP_TAC INTERIOR_OPEN THEN MATCH_MP_TAC OPEN_CONNECTED_COMPONENT THEN ASM_REWRITE_TAC[]; MATCH_MP_TAC CONTINUOUS_ON_SUBSET THEN EXISTS_TAC `(:real^2)` THEN ASM_REWRITE_TAC[SUBSET_UNIV]; MATCH_MP_TAC(SET_RULE `IMAGE f UNIV SUBSET s ==> IMAGE f t SUBSET s`) THEN ASM_REWRITE_TAC[]; UNDISCH_TAC `path_image(A:real^1->real^2) SUBSET path_image U UNION path_image D` THEN MATCH_MP_TAC(SET_RULE `!y. y IN c /\ ~(y IN p) ==> a SUBSET p ==> ~(c SUBSET a)`) THEN EXISTS_TAC `y:real^2` THEN REWRITE_TAC[IN_DIFF; IN_UNIV] THEN CONJ_TAC THENL [DISCH_THEN(MP_TAC o MATCH_MP CONNECTED_COMPONENT_EQ) THEN DISCH_THEN SUBST_ALL_TAC THEN ASM_MESON_TAC[]; UNDISCH_TAC `(y:real^2) IN K` THEN EXPAND_TAC "K" THEN REWRITE_TAC[IN_UNIV; IN_DIFF] THEN ASM_REWRITE_TAC[]]]]; ALL_TAC] THEN CONJ_TAC THENL [ALL_TAC; ASM_MESON_TAC[]] THEN MATCH_MP_TAC SUBSET_ANTISYM THEN REWRITE_TAC[UNION_SUBSET; CONNECTED_COMPONENT_SUBSET] THEN REWRITE_TAC[SUBSET; IN_UNION; IN_ELIM_THM] THEN X_GEN_TAC `x:real^2` THEN DISCH_THEN(fun th -> ASSUME_TAC th THEN MP_TAC(MATCH_MP CONNECTED_COMPONENT_REFL th)) THEN GEN_REWRITE_TAC LAND_CONV [GSYM IN] THEN ASM_CASES_TAC `connected_component K (x:real^2) = connected_component K y` THEN ASM_REWRITE_TAC[] THEN SIMP_TAC[] THEN ASM_CASES_TAC `connected_component K (x:real^2) = connected_component K n` THEN ASM_REWRITE_TAC[] THEN SIMP_TAC[] THEN DISCH_TAC THEN MATCH_MP_TAC(TAUT `F ==> p`) THEN SUBGOAL_THEN `bounded(connected_component K (x:real^2))` ASSUME_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN ABBREV_TAC `bp = (linepath(n:real^2,t) ++ h) ++ linepath(p,q) ++ (l ++ linepath(b,--n))` THEN SUBGOAL_THEN `path_image bp SUBSET ((path_image U UNION path_image D) DIFF {--basis 1:real^2,basis 1}) UNION (connected_component K n) UNION (connected_component K y)` (LABEL_TAC "*") THENL [EXPAND_TAC "bp" THEN REPEAT(MATCH_MP_TAC SUBSET_PATH_IMAGE_JOIN THEN CONJ_TAC) THEN REPEAT CONJ_TAC THENL [MATCH_MP_TAC(SET_RULE `(path_image(linepath(n,t)) DELETE t) SUBSET nn /\ t IN uu DIFF kk ==> path_image(linepath(n,t)) SUBSET ((uu UNION dd) DIFF kk) UNION nn UNION yy`) THEN ASM_REWRITE_TAC[IN_DIFF; IN_INSERT; NOT_IN_EMPTY] THEN CONJ_TAC THENL [ALL_TAC; SIMP_TAC[CART_EQ; FORALL_2; DIMINDEX_2; BASIS_COMPONENT; VECTOR_NEG_COMPONENT; ARITH; REAL_NEG_0] THEN ASM_REWRITE_TAC[] THEN CONV_TAC REAL_RAT_REDUCE_CONV] THEN MATCH_MP_TAC CONNECTED_COMPONENT_MAXIMAL THEN SIMP_TAC[CONVEX_CONNECTED; PATH_IMAGE_LINEPATH; CONVEX_SEMIOPEN_SEGMENT; IN_DELETE; ENDS_IN_SEGMENT] THEN CONJ_TAC THENL [DISCH_THEN(MP_TAC o AP_TERM `\z:real^2. z$2`) THEN ASM_REWRITE_TAC[] THEN ASM_REAL_ARITH_TAC; ALL_TAC] THEN REWRITE_TAC[SUBSET; IN_DELETE] THEN X_GEN_TAC `w:real^2` THEN STRIP_TAC THEN MP_TAC(ISPECL [`n:real^2`; `t:real^2`; `w:real^2`] SEGMENT_VERTICAL) THEN ASM_REWRITE_TAC[] THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN UNDISCH_TAC `~(w:real^2 = t)` THEN ASM_REWRITE_TAC[CART_EQ; FORALL_2; DIMINDEX_2; IMP_IMP] THEN DISCH_THEN(MP_TAC o MATCH_MP (REAL_ARITH `~(w = t) /\ (&2 <= w /\ w <= t \/ t <= w /\ w <= &2) ==> abs(t) < &2 ==> t < w`)) THEN MATCH_MP_TAC(TAUT `a /\ (~c ==> ~b) ==> (a ==> b) ==> c`) THEN CONJ_TAC THENL [FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[IN_UNION]; EXPAND_TAC "K" THEN ASM_REWRITE_TAC[IN_DIFF; IN_UNIV; REAL_NOT_LT] THEN ASM_MESON_TAC[]]; MATCH_MP_TAC SUBSET_TRANS THEN EXISTS_TAC `path_image U DIFF {pathstart U:real^2, pathfinish U}` THEN ASM_REWRITE_TAC[] THEN CONV_TAC SET_RULE; MATCH_MP_TAC(SET_RULE `(p IN uu /\ q IN dd /\ ~(p IN kk) /\ ~(q IN kk)) /\ (path_image(linepath(p,q)) DIFF {p,q}) SUBSET yy ==> path_image(linepath(p,q)) SUBSET ((uu UNION dd) DIFF kk) UNION nn UNION yy`) THEN ASM_REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY] THEN CONJ_TAC THENL [SIMP_TAC[CART_EQ; FORALL_2; DIMINDEX_2; BASIS_COMPONENT; VECTOR_NEG_COMPONENT; ARITH; REAL_NEG_0] THEN ASM_REWRITE_TAC[] THEN CONV_TAC REAL_RAT_REDUCE_CONV; ALL_TAC] THEN MATCH_MP_TAC CONNECTED_COMPONENT_MAXIMAL THEN REWRITE_TAC[PATH_IMAGE_LINEPATH; GSYM open_segment] THEN REWRITE_TAC[CONNECTED_SEGMENT] THEN EXPAND_TAC "y" THEN REWRITE_TAC[MIDPOINT_IN_SEGMENT] THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[open_segment; SUBSET; IN_DIFF; IN_INSERT; NOT_IN_EMPTY] THEN X_GEN_TAC `w:real^2` THEN REWRITE_TAC[DE_MORGAN_THM] THEN STRIP_TAC THEN MP_TAC(ISPECL [`p:real^2`; `q:real^2`; `w:real^2`] SEGMENT_VERTICAL) THEN ASM_REWRITE_TAC[] THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN MAP_EVERY UNDISCH_TAC [`~(w:real^2 = p)`; `~(w:real^2 = q)`] THEN ASM_REWRITE_TAC[CART_EQ; FORALL_2; DIMINDEX_2; IMP_IMP] THEN DISCH_THEN(MP_TAC o MATCH_MP (REAL_ARITH `(~(w = q) /\ ~(w = p)) /\ (p <= w /\ w <= q \/ q <= w /\ w <= p) ==> q < p ==> q < w /\ w < p`)) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN MAP_EVERY (C UNDISCH_THEN (MP_TAC o SPEC `w:real^2`)) [`!z:real^2. z$2 <= (p:real^2)$2 /\ z$1 = &0 /\ z IN path_image D ==> z$2 <= (q:real^2)$2`; `!z:real^2. z$1 = &0 /\ z IN path_image U ==> (p:real^2)$2 <= z$2`] THEN ASM_REWRITE_TAC[GSYM REAL_NOT_LT] THEN DISCH_TAC THEN EXPAND_TAC "K" THEN ASM_REWRITE_TAC[IN_DIFF; IN_UNIV; IN_UNION] THEN MATCH_MP_TAC(TAUT `~p ==> ~(~p /\ q) ==> ~q`) THEN ASM_REAL_ARITH_TAC; MATCH_MP_TAC SUBSET_TRANS THEN EXISTS_TAC `path_image D DIFF {pathstart D:real^2, pathfinish D}` THEN ASM_REWRITE_TAC[] THEN CONV_TAC SET_RULE; MATCH_MP_TAC(SET_RULE `(path_image(linepath(b,n)) DELETE b) SUBSET nn /\ b IN dd DIFF kk ==> path_image(linepath(b,n)) SUBSET ((uu UNION dd) DIFF kk) UNION nn UNION yy`) THEN ASM_REWRITE_TAC[IN_DIFF; IN_INSERT; NOT_IN_EMPTY] THEN CONJ_TAC THENL [ALL_TAC; SIMP_TAC[CART_EQ; FORALL_2; DIMINDEX_2; BASIS_COMPONENT; VECTOR_NEG_COMPONENT; ARITH; REAL_NEG_0] THEN ASM_REWRITE_TAC[] THEN CONV_TAC REAL_RAT_REDUCE_CONV] THEN SUBGOAL_THEN `connected_component K (n:real^2) = connected_component K (--n)` SUBST1_TAC THENL [CONV_TAC SYM_CONV THEN MATCH_MP_TAC CONNECTED_COMPONENT_EQ THEN MATCH_MP_TAC(REWRITE_RULE[SUBSET] (ASSUME `(:real^2) DIFF interval[--vector [&1; &9 / &5],vector [&1; &9 / &5]] SUBSET connected_component K n`)) THEN ASM_REWRITE_TAC[IN_UNIV; IN_DIFF; IN_INTERVAL; DIMINDEX_2; FORALL_2; VECTOR_NEG_COMPONENT; VECTOR_2] THEN CONV_TAC REAL_RAT_REDUCE_CONV; ALL_TAC] THEN MATCH_MP_TAC CONNECTED_COMPONENT_MAXIMAL THEN SIMP_TAC[CONVEX_CONNECTED; PATH_IMAGE_LINEPATH; CONVEX_SEMIOPEN_SEGMENT; IN_DELETE; ENDS_IN_SEGMENT] THEN CONJ_TAC THENL [DISCH_THEN(MP_TAC o AP_TERM `\z:real^2. z$2`) THEN ASM_REWRITE_TAC[VECTOR_NEG_COMPONENT] THEN ASM_REAL_ARITH_TAC; ALL_TAC] THEN REWRITE_TAC[SUBSET; IN_DELETE] THEN X_GEN_TAC `w:real^2` THEN STRIP_TAC THEN MP_TAC(ISPECL [`b:real^2`; `--n:real^2`; `w:real^2`] SEGMENT_VERTICAL) THEN ASM_REWRITE_TAC[VECTOR_NEG_COMPONENT; REAL_NEG_0] THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN UNDISCH_TAC `~(w:real^2 = b)` THEN ASM_REWRITE_TAC[CART_EQ; FORALL_2; DIMINDEX_2; IMP_IMP] THEN DISCH_THEN(MP_TAC o MATCH_MP (REAL_ARITH `~(w = b) /\ (b <= w /\ w <= -- &2 \/ -- &2 <= w /\ w <= b) ==> abs(b) < &2 ==> w < b`)) THEN MATCH_MP_TAC(TAUT `a /\ (~c ==> ~b) ==> (a ==> b) ==> c`) THEN CONJ_TAC THENL [FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[IN_UNION]; EXPAND_TAC "K" THEN ASM_REWRITE_TAC[IN_DIFF; IN_UNIV; IN_UNION; REAL_NOT_LT] THEN ASM_CASES_TAC `(w:real^2) IN path_image D` THEN ASM_REWRITE_TAC[] THENL [ASM_MESON_TAC[]; DISCH_TAC] THEN UNDISCH_TAC `!z. z$1 = &0 /\ z IN path_image U ==> (p:real^2)$2 <= (z:real^2)$2` THEN DISCH_THEN(MP_TAC o SPEC `w:real^2`) THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC(REAL_ARITH `!q. b <= q /\ q < p ==> p <= w ==> b <= w`) THEN EXISTS_TAC `(q:real^2)$2` THEN ASM_MESON_TAC[]]]; ALL_TAC] THEN SUBGOAL_THEN `path(bp:real^1->real^2)` ASSUME_TAC THENL [EXPAND_TAC "bp" THEN REPEAT(MATCH_MP_TAC PATH_JOIN_IMP THEN REPEAT CONJ_TAC THEN ASM_REWRITE_TAC[PATHSTART_LINEPATH; PATHFINISH_LINEPATH]) THEN ASM_REWRITE_TAC[PATH_LINEPATH; PATHSTART_JOIN; PATHFINISH_JOIN; PATHSTART_LINEPATH; PATHFINISH_LINEPATH]; ALL_TAC] THEN SUBGOAL_THEN `(?d1. &0 < d1 /\ cball(--basis 1,d1) SUBSET ((:real^2) DIFF path_image bp)) /\ (?d2. &0 < d2 /\ cball(basis 1,d2) SUBSET ((:real^2) DIFF path_image bp))` STRIP_ASSUME_TAC THENL [CONJ_TAC THEN MATCH_MP_TAC(REWRITE_RULE[RIGHT_IMP_FORALL_THM; IMP_IMP] (fst(EQ_IMP_RULE(SPEC_ALL OPEN_CONTAINS_CBALL)))) THEN REWRITE_TAC[GSYM closed; IN_DIFF; IN_UNIV] THEN (CONJ_TAC THENL [ASM_MESON_TAC[COMPACT_IMP_CLOSED; COMPACT_PATH_IMAGE]; ALL_TAC]) THEN FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (SET_RULE `bp SUBSET s ==> ~(x IN s) ==> ~(x IN bp)`)) THEN ASM_REWRITE_TAC[IN_UNION; IN_DIFF; IN_INSERT] THEN MATCH_MP_TAC(SET_RULE `(!x. connected_component k x SUBSET k) /\ ~(a IN k) /\ ~(b IN k) ==> ~(a IN connected_component k x \/ b IN connected_component k y)`) THEN REWRITE_TAC[CONNECTED_COMPONENT_SUBSET] THEN EXPAND_TAC "K" THEN REWRITE_TAC[IN_UNIV; IN_DIFF] THEN ASM_REWRITE_TAC[]; ALL_TAC] THEN SUBGOAL_THEN `--(basis 1) IN frontier(connected_component K (x:real^2)) /\ (basis 1) IN frontier(connected_component K x)` MP_TAC THENL [ASM_SIMP_TAC[]; ALL_TAC] THEN REWRITE_TAC[frontier] THEN ASM_SIMP_TAC[OPEN_CONNECTED_COMPONENT; INTERIOR_OPEN] THEN REWRITE_TAC[IN_DIFF] THEN DISCH_THEN(CONJUNCTS_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC)) THEN REWRITE_TAC[CLOSURE_APPROACHABLE] THEN DISCH_THEN(MP_TAC o SPEC `d2:real`) THEN ASM_REWRITE_TAC[] THEN DISCH_THEN(X_CHOOSE_THEN `w2:real^2` STRIP_ASSUME_TAC) THEN DISCH_THEN(MP_TAC o SPEC `d1:real`) THEN ASM_REWRITE_TAC[] THEN DISCH_THEN(X_CHOOSE_THEN `w1:real^2` STRIP_ASSUME_TAC) THEN SUBGOAL_THEN `(w1:real^2) IN interval[--vector [&1; &2],vector [&1; &2]] /\ (w2:real^2) IN interval[--vector [&1; &2],vector [&1; &2]]` STRIP_ASSUME_TAC THENL [CONJ_TAC THEN MATCH_MP_TAC(SET_RULE `!n j. j SUBSET i /\ (:real^N) DIFF j SUBSET n /\ ~(w IN n) ==> w IN i`) THEN EXISTS_TAC `connected_component K (n:real^2)` THEN EXISTS_TAC `interval[--vector [&1; &9 / &5]:real^2,vector [&1; &9 / &5]]` THEN ASM_REWRITE_TAC[SUBSET_INTERVAL; DIMINDEX_2; FORALL_2; VECTOR_2; VECTOR_NEG_COMPONENT] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN ASM_MESON_TAC[CONNECTED_COMPONENT_EQ]; ALL_TAC] THEN SUBGOAL_THEN `?br. path br /\ path_image br SUBSET connected_component K x /\ pathstart br = w1 /\ pathfinish br = (w2:real^2)` STRIP_ASSUME_TAC THENL [MP_TAC(ISPEC `connected_component K (x:real^2)` path_connected) THEN ASM_SIMP_TAC[PATH_CONNECTED_EQ_CONNECTED; OPEN_CONNECTED_COMPONENT] THEN REWRITE_TAC[CONNECTED_CONNECTED_COMPONENT] THEN DISCH_THEN MATCH_MP_TAC THEN ASM_REWRITE_TAC[]; ALL_TAC] THEN SUBGOAL_THEN `pathstart bp = n:real^2 /\ pathfinish bp = (--n:real^2)` STRIP_ASSUME_TAC THENL [EXPAND_TAC "bp" THEN REWRITE_TAC[PATHSTART_JOIN; PATHFINISH_JOIN] THEN REWRITE_TAC[PATHSTART_LINEPATH; PATHFINISH_LINEPATH]; ALL_TAC] THEN MP_TAC(ISPECL [`linepath(--basis 1:real^2,w1) ++ br ++ linepath(w2,basis 1)`; `reversepath bp:real^1->real^2`; `--vector[&1; &2]:real^2`; `vector[&1; &2]:real^2`] FASHODA) THEN ASM_SIMP_TAC[PATH_JOIN; PATH_LINEPATH; PATH_REVERSEPATH; PATHSTART_REVERSEPATH; PATHFINISH_REVERSEPATH; PATHSTART_LINEPATH; PATHFINISH_LINEPATH; PATHSTART_JOIN; PATHFINISH_JOIN; PATH_IMAGE_JOIN; PATH_IMAGE_REVERSEPATH] THEN SUBST1_TAC(SYM(ASSUME `&2 % basis 2:real^2 = n`)) THEN SIMP_TAC[BASIS_COMPONENT; VECTOR_2; VECTOR_NEG_COMPONENT; DIMINDEX_2; ARITH; VECTOR_MUL_COMPONENT] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN REWRITE_TAC[NOT_IMP; UNION_SUBSET; GSYM CONJ_ASSOC] THEN REWRITE_TAC[PATH_IMAGE_LINEPATH; SEGMENT_CONVEX_HULL] THEN SIMP_TAC[SUBSET_HULL; CONVEX_INTERVAL] THEN ASM_REWRITE_TAC[SET_RULE `{a,b} SUBSET s <=> a IN s /\ b IN s`] THEN SIMP_TAC[IN_INTERVAL; DIMINDEX_2; FORALL_2; VECTOR_2; BASIS_COMPONENT; ARITH; VECTOR_NEG_COMPONENT] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN REPEAT CONJ_TAC THENL [MATCH_MP_TAC SUBSET_TRANS THEN EXISTS_TAC `connected_component K (x:real^2)` THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC(SET_RULE `!n j. j SUBSET i /\ (:real^N) DIFF j SUBSET n /\ c INTER n = {} ==> c SUBSET i`) THEN EXISTS_TAC `connected_component K (n:real^2)` THEN EXISTS_TAC `interval[--vector [&1; &9 / &5]:real^2,vector [&1; &9 / &5]]` THEN ASM_REWRITE_TAC[SUBSET_INTERVAL; DIMINDEX_2; FORALL_2; VECTOR_2; VECTOR_NEG_COMPONENT] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN ASM_REWRITE_TAC[CONNECTED_COMPONENT_NONOVERLAP]; EXPAND_TAC "bp" THEN REPEAT(MATCH_MP_TAC SUBSET_PATH_IMAGE_JOIN THEN CONJ_TAC) THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[PATH_IMAGE_LINEPATH; SEGMENT_CONVEX_HULL] THEN SIMP_TAC[SUBSET_HULL; CONVEX_INTERVAL] THEN ASM_REWRITE_TAC[SET_RULE `{a,b} SUBSET s <=> a IN s /\ b IN s`] THEN SUBST1_TAC(SYM(ASSUME `&2 % basis 2:real^2 = n`)) THEN SIMP_TAC[BASIS_COMPONENT; VECTOR_2; VECTOR_NEG_COMPONENT; DIMINDEX_2; ARITH; VECTOR_MUL_COMPONENT; IN_INTERVAL; FORALL_2] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN ASM SET_TAC[]; ALL_TAC] THEN DISCH_THEN(X_CHOOSE_THEN `w:real^2` (CONJUNCTS_THEN2 MP_TAC ASSUME_TAC)) THEN REWRITE_TAC[IN_UNION; DE_MORGAN_THM] THEN REPEAT CONJ_TAC THENL [UNDISCH_TAC `cball(--basis 1,d1) SUBSET (:real^2) DIFF path_image bp` THEN REWRITE_TAC[SUBSET; IN_DIFF; IN_UNIV] THEN DISCH_THEN(MP_TAC o SPEC `w:real^2`) THEN ASM_REWRITE_TAC[CONTRAPOS_THM] THEN SPEC_TAC(`w:real^2`,`u:real^2`) THEN REWRITE_TAC[GSYM SUBSET] THEN SIMP_TAC[SUBSET_HULL; CONVEX_CBALL] THEN REWRITE_TAC[SET_RULE `{a,b} SUBSET s <=> a IN s /\ b IN s`] THEN ASM_SIMP_TAC[CENTRE_IN_CBALL; REAL_LT_IMP_LE] THEN REWRITE_TAC[IN_CBALL] THEN ASM_MESON_TAC[REAL_LT_IMP_LE; DIST_SYM]; ALL_TAC; UNDISCH_TAC `cball(basis 1,d2) SUBSET (:real^2) DIFF path_image bp` THEN REWRITE_TAC[SUBSET; IN_DIFF; IN_UNIV] THEN DISCH_THEN(MP_TAC o SPEC `w:real^2`) THEN ASM_REWRITE_TAC[CONTRAPOS_THM] THEN SPEC_TAC(`w:real^2`,`u:real^2`) THEN REWRITE_TAC[GSYM SUBSET] THEN SIMP_TAC[SUBSET_HULL; CONVEX_CBALL] THEN REWRITE_TAC[SET_RULE `{a,b} SUBSET s <=> a IN s /\ b IN s`] THEN ASM_SIMP_TAC[CENTRE_IN_CBALL; REAL_LT_IMP_LE] THEN REWRITE_TAC[IN_CBALL] THEN ASM_MESON_TAC[REAL_LT_IMP_LE; DIST_SYM]] THEN FIRST_X_ASSUM(MP_TAC o C MATCH_MP (ASSUME `(w:real^2) IN path_image bp`) o GEN_REWRITE_RULE I [SUBSET]) THEN FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (SET_RULE `br SUBSET k ==> s INTER k = {} ==> w IN s ==> ~(w IN br)`)) THEN MATCH_MP_TAC(SET_RULE `xx SUBSET (UNIV DIFF du) /\ nn INTER xx = {} /\ yy INTER xx = {} ==> ((du DIFF ee) UNION nn UNION yy) INTER xx = {}`) THEN ASM_REWRITE_TAC[CONNECTED_COMPONENT_NONOVERLAP] THEN MATCH_MP_TAC SUBSET_TRANS THEN EXISTS_TAC `K:real^2->bool` THEN REWRITE_TAC[CONNECTED_COMPONENT_SUBSET] THEN EXPAND_TAC "K" THEN MATCH_MP_TAC(SET_RULE `s = t ==> s SUBSET t`) THEN AP_TERM_TAC THEN ASM_REWRITE_TAC[]);;let JORDAN_CURVE_THEOREM =prove (`!c:real^1->real^2. simple_path c /\ pathfinish c = pathstart c ==> ?ins out. ~(ins = {}) /\ open ins /\ connected ins /\ ~(out = {}) /\ open out /\ connected out /\ bounded ins /\ ~bounded out /\ ins INTER out = {} /\ ins UNION out = (:real^2) DIFF path_image c /\ frontier ins = path_image c /\ frontier out = path_image c`,let JORDAN_DISCONNECTED =prove (`!c. simple_path c /\ pathfinish c = pathstart c ==> ~connected((:real^2) DIFF path_image c)`,(* ------------------------------------------------------------------------- *) (* Splitting the inside of a closed curve into two with a cut across it. *) (* The hardest part, that there is no third component inside the original *) (* curve, is taken from Whyburn's, "Topological Analysis" (1.4 on p31). *) (* ------------------------------------------------------------------------- *)let JORDAN_INSIDE_OUTSIDE =prove (`!c:real^1->real^2. simple_path c /\ pathfinish c = pathstart c ==> ~(inside(path_image c) = {}) /\ open(inside(path_image c)) /\ connected(inside(path_image c)) /\ ~(outside(path_image c) = {}) /\ open(outside(path_image c)) /\ connected(outside(path_image c)) /\ bounded(inside(path_image c)) /\ ~bounded(outside(path_image c)) /\ inside(path_image c) INTER outside(path_image c) = {} /\ inside(path_image c) UNION outside(path_image c) = (:real^2) DIFF path_image c /\ frontier(inside(path_image c)) = path_image c /\ frontier(outside(path_image c)) = path_image c`,let SPLIT_INSIDE_SIMPLE_CLOSED_CURVE =prove (`!c1 c2 c a b:real^2. ~(a = b) /\ simple_path c1 /\ pathstart c1 = a /\ pathfinish c1 = b /\ simple_path c2 /\ pathstart c2 = a /\ pathfinish c2 = b /\ simple_path c /\ pathstart c = a /\ pathfinish c = b /\ path_image c1 INTER path_image c2 = {a,b} /\ path_image c1 INTER path_image c = {a,b} /\ path_image c2 INTER path_image c = {a,b} /\ ~(path_image c INTER inside(path_image c1 UNION path_image c2) = {}) ==> inside(path_image c1 UNION path_image c) INTER inside(path_image c2 UNION path_image c) = {} /\ inside(path_image c1 UNION path_image c) UNION inside(path_image c2 UNION path_image c) UNION (path_image c DIFF {a,b}) = inside(path_image c1 UNION path_image c2)`,