--- a/src/HOL/Analysis/Fashoda_Theorem.thy Wed Apr 18 21:12:50 2018 +0100
+++ b/src/HOL/Analysis/Fashoda_Theorem.thy Thu Apr 19 14:49:08 2018 +0100
@@ -890,237 +890,4 @@
qed
qed
-(** The Following still needs to be translated. Maybe I will do that later.
-
-(* ------------------------------------------------------------------------- *)
-(* 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 RETRACTION_INJECTIVE_IMAGE_INTERVAL = prove
- (`!p:real^M->real^N a b.
- ~(interval[a,b] = {}) /\
- p continuous_on interval[a,b] /\
- (!x y. x IN interval[a,b] /\ y IN interval[a,b] /\ p x = p y ==> x = y)
- ==> ?f. f continuous_on (:real^N) /\
- IMAGE f (:real^N) SUBSET (IMAGE p (interval[a,b])) /\
- (!x. x IN (IMAGE p (interval[a,b])) ==> f x = x)`,
- REPEAT STRIP_TAC THEN
- FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [INJECTIVE_ON_LEFT_INVERSE]) THEN
- DISCH_THEN(X_CHOOSE_TAC `q:real^N->real^M`) THEN
- SUBGOAL_THEN `(q:real^N->real^M) continuous_on
- (IMAGE p (interval[a:real^M,b]))`
- ASSUME_TAC THENL
- [MATCH_MP_TAC CONTINUOUS_ON_INVERSE THEN ASM_REWRITE_TAC[COMPACT_INTERVAL];
- ALL_TAC] THEN
- MP_TAC(ISPECL [`q:real^N->real^M`;
- `IMAGE (p:real^M->real^N)
- (interval[a,b])`;
- `a:real^M`; `b:real^M`]
- TIETZE_CLOSED_INTERVAL) THEN
- ASM_SIMP_TAC[COMPACT_INTERVAL; COMPACT_CONTINUOUS_IMAGE;
- COMPACT_IMP_CLOSED] THEN
- ANTS_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
- DISCH_THEN(X_CHOOSE_THEN `r:real^N->real^M` STRIP_ASSUME_TAC) THEN
- EXISTS_TAC `(p:real^M->real^N) o (r:real^N->real^M)` THEN
- REWRITE_TAC[SUBSET; FORALL_IN_IMAGE; o_THM; IN_UNIV] THEN
- CONJ_TAC THENL [ALL_TAC; ASM SET_TAC[]] THEN
- MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN ASM_REWRITE_TAC[] THEN
- FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP(REWRITE_RULE[IMP_CONJ]
- CONTINUOUS_ON_SUBSET)) THEN ASM SET_TAC[]);;
-
-let UNBOUNDED_PATH_COMPONENTS_COMPLEMENT_HOMEOMORPHIC_INTERVAL = prove
- (`!s:real^N->bool a b:real^M.
- s homeomorphic (interval[a,b])
- ==> !x. ~(x IN s) ==> ~bounded(path_component((:real^N) DIFF s) x)`,
- REPEAT GEN_TAC THEN REWRITE_TAC[homeomorphic; homeomorphism] THEN
- REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
- MAP_EVERY X_GEN_TAC [`p':real^N->real^M`; `p:real^M->real^N`] THEN
- DISCH_TAC THEN
- SUBGOAL_THEN
- `!x y. x IN interval[a,b] /\ y IN interval[a,b] /\
- (p:real^M->real^N) x = p y ==> x = y`
- ASSUME_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
- FIRST_X_ASSUM(MP_TAC o funpow 4 CONJUNCT2) THEN
- DISCH_THEN(CONJUNCTS_THEN2 (SUBST1_TAC o SYM) ASSUME_TAC) THEN
- ASM_CASES_TAC `interval[a:real^M,b] = {}` THEN
- ASM_REWRITE_TAC[IMAGE_CLAUSES; DIFF_EMPTY; PATH_COMPONENT_UNIV;
- NOT_BOUNDED_UNIV] THEN
- ABBREV_TAC `s = (:real^N) DIFF (IMAGE p (interval[a:real^M,b]))` THEN
- X_GEN_TAC `c:real^N` THEN REPEAT STRIP_TAC THEN
- SUBGOAL_THEN `(c:real^N) IN s` ASSUME_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
- SUBGOAL_THEN `bounded((path_component s c) UNION
- (IMAGE (p:real^M->real^N) (interval[a,b])))`
- MP_TAC THENL
- [ASM_SIMP_TAC[BOUNDED_UNION; COMPACT_IMP_BOUNDED; COMPACT_IMP_BOUNDED;
- COMPACT_CONTINUOUS_IMAGE; COMPACT_INTERVAL];
- ALL_TAC] THEN
- DISCH_THEN(MP_TAC o SPEC `c:real^N` o MATCH_MP BOUNDED_SUBSET_BALL) THEN
- REWRITE_TAC[UNION_SUBSET] THEN
- DISCH_THEN(X_CHOOSE_THEN `B:real` STRIP_ASSUME_TAC) THEN
- MP_TAC(ISPECL [`p:real^M->real^N`; `a:real^M`; `b:real^M`]
- RETRACTION_INJECTIVE_IMAGE_INTERVAL) THEN
- ASM_REWRITE_TAC[SUBSET; IN_UNIV] THEN
- DISCH_THEN(X_CHOOSE_THEN `r:real^N->real^N` MP_TAC) THEN
- DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC
- (CONJUNCTS_THEN2 MP_TAC ASSUME_TAC)) THEN
- REWRITE_TAC[FORALL_IN_IMAGE; IN_UNIV] THEN DISCH_TAC THEN
- ABBREV_TAC `q = \z:real^N. if z IN path_component s c then r(z) else z` THEN
- SUBGOAL_THEN
- `(q:real^N->real^N) continuous_on
- (closure(path_component s c) UNION ((:real^N) DIFF (path_component s c)))`
- MP_TAC THENL
- [EXPAND_TAC "q" THEN MATCH_MP_TAC CONTINUOUS_ON_CASES THEN
- REWRITE_TAC[CLOSED_CLOSURE; CONTINUOUS_ON_ID; GSYM OPEN_CLOSED] THEN
- REPEAT CONJ_TAC THENL
- [MATCH_MP_TAC OPEN_PATH_COMPONENT THEN EXPAND_TAC "s" THEN
- ASM_SIMP_TAC[GSYM CLOSED_OPEN; COMPACT_IMP_CLOSED;
- COMPACT_CONTINUOUS_IMAGE; COMPACT_INTERVAL];
- ASM_MESON_TAC[CONTINUOUS_ON_SUBSET; SUBSET_UNIV];
- ALL_TAC] THEN
- X_GEN_TAC `z:real^N` THEN
- REWRITE_TAC[SET_RULE `~(z IN (s DIFF t) /\ z IN t)`] THEN
- STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
- MP_TAC(ISPECL
- [`path_component s (z:real^N)`; `path_component s (c:real^N)`]
- OPEN_INTER_CLOSURE_EQ_EMPTY) THEN
- ASM_REWRITE_TAC[GSYM DISJOINT; PATH_COMPONENT_DISJOINT] THEN ANTS_TAC THENL
- [MATCH_MP_TAC OPEN_PATH_COMPONENT THEN EXPAND_TAC "s" THEN
- ASM_SIMP_TAC[GSYM CLOSED_OPEN; COMPACT_IMP_CLOSED;
- COMPACT_CONTINUOUS_IMAGE; COMPACT_INTERVAL];
- REWRITE_TAC[DISJOINT; EXTENSION; IN_INTER; NOT_IN_EMPTY] THEN
- DISCH_THEN(MP_TAC o SPEC `z:real^N`) THEN ASM_REWRITE_TAC[] THEN
- GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [IN] THEN
- REWRITE_TAC[PATH_COMPONENT_REFL_EQ] THEN ASM SET_TAC[]];
- ALL_TAC] THEN
- SUBGOAL_THEN
- `closure(path_component s c) UNION ((:real^N) DIFF (path_component s c)) =
- (:real^N)`
- SUBST1_TAC THENL
- [MATCH_MP_TAC(SET_RULE `s SUBSET t ==> t UNION (UNIV DIFF s) = UNIV`) THEN
- REWRITE_TAC[CLOSURE_SUBSET];
- DISCH_TAC] THEN
- MP_TAC(ISPECL
- [`(\x. &2 % c - x) o
- (\x. c + B / norm(x - c) % (x - c)) o (q:real^N->real^N)`;
- `cball(c:real^N,B)`]
- BROUWER) THEN
- REWRITE_TAC[NOT_IMP; GSYM CONJ_ASSOC; COMPACT_CBALL; CONVEX_CBALL] THEN
- ASM_SIMP_TAC[CBALL_EQ_EMPTY; REAL_LT_IMP_LE; REAL_NOT_LT] THEN
- SUBGOAL_THEN `!x. ~((q:real^N->real^N) x = c)` ASSUME_TAC THENL
- [X_GEN_TAC `x:real^N` THEN EXPAND_TAC "q" THEN
- REWRITE_TAC[NORM_EQ_0; VECTOR_SUB_EQ] THEN COND_CASES_TAC THEN
- ASM SET_TAC[PATH_COMPONENT_REFL_EQ];
- ALL_TAC] THEN
- REPEAT CONJ_TAC THENL
- [MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN
- SIMP_TAC[CONTINUOUS_ON_SUB; CONTINUOUS_ON_ID; CONTINUOUS_ON_CONST] THEN
- MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN CONJ_TAC THENL
- [ASM_MESON_TAC[CONTINUOUS_ON_SUBSET; SUBSET_UNIV]; ALL_TAC] THEN
- MATCH_MP_TAC CONTINUOUS_ON_ADD THEN REWRITE_TAC[CONTINUOUS_ON_CONST] THEN
- MATCH_MP_TAC CONTINUOUS_ON_MUL THEN
- SIMP_TAC[CONTINUOUS_ON_SUB; CONTINUOUS_ON_ID; CONTINUOUS_ON_CONST] THEN
- REWRITE_TAC[o_DEF; real_div; LIFT_CMUL] THEN
- MATCH_MP_TAC CONTINUOUS_ON_CMUL THEN
- MATCH_MP_TAC(REWRITE_RULE[o_DEF] CONTINUOUS_ON_INV) THEN
- ASM_REWRITE_TAC[FORALL_IN_IMAGE; NORM_EQ_0; VECTOR_SUB_EQ] THEN
- SUBGOAL_THEN
- `(\x:real^N. lift(norm(x - c))) = (lift o norm) o (\x. x - c)`
- SUBST1_TAC THENL [REWRITE_TAC[o_DEF]; ALL_TAC] THEN
- MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN
- ASM_SIMP_TAC[CONTINUOUS_ON_SUB; CONTINUOUS_ON_ID; CONTINUOUS_ON_CONST;
- CONTINUOUS_ON_LIFT_NORM];
- REWRITE_TAC[SUBSET; FORALL_IN_IMAGE; IN_CBALL; o_THM; dist] THEN
- X_GEN_TAC `x:real^N` THEN DISCH_TAC THEN
- REWRITE_TAC[VECTOR_ARITH `c - (&2 % c - (c + x)) = x`] THEN
- REWRITE_TAC[NORM_MUL; REAL_ABS_DIV; REAL_ABS_NORM] THEN
- ASM_SIMP_TAC[REAL_DIV_RMUL; NORM_EQ_0; VECTOR_SUB_EQ] THEN
- ASM_REAL_ARITH_TAC;
- REWRITE_TAC[NOT_EXISTS_THM; TAUT `~(c /\ b) <=> c ==> ~b`] THEN
- REWRITE_TAC[IN_CBALL; o_THM; dist] THEN
- X_GEN_TAC `x:real^N` THEN DISCH_TAC THEN
- REWRITE_TAC[VECTOR_ARITH `&2 % c - (c + x') = x <=> --x' = x - c`] THEN
- ASM_CASES_TAC `(x:real^N) IN path_component s c` THENL
- [MATCH_MP_TAC(NORM_ARITH `norm(y) < B /\ norm(x) = B ==> ~(--x = y)`) THEN
- REWRITE_TAC[NORM_MUL; REAL_ABS_DIV; REAL_ABS_NORM] THEN
- ASM_SIMP_TAC[REAL_DIV_RMUL; NORM_EQ_0; VECTOR_SUB_EQ] THEN
- ASM_SIMP_TAC[REAL_ARITH `&0 < B ==> abs B = B`] THEN
- UNDISCH_TAC `path_component s c SUBSET ball(c:real^N,B)` THEN
- REWRITE_TAC[SUBSET; IN_BALL] THEN ASM_MESON_TAC[dist; NORM_SUB];
- EXPAND_TAC "q" THEN REWRITE_TAC[] THEN ASM_REWRITE_TAC[] THEN
- REWRITE_TAC[VECTOR_ARITH `--(c % x) = x <=> (&1 + c) % x = vec 0`] THEN
- ASM_REWRITE_TAC[DE_MORGAN_THM; VECTOR_SUB_EQ; VECTOR_MUL_EQ_0] THEN
- SUBGOAL_THEN `~(x:real^N = c)` ASSUME_TAC THENL
- [ASM_MESON_TAC[PATH_COMPONENT_REFL; IN]; ALL_TAC] THEN
- ASM_REWRITE_TAC[] THEN
- MATCH_MP_TAC(REAL_ARITH `&0 < x ==> ~(&1 + x = &0)`) THEN
- ASM_SIMP_TAC[REAL_LT_DIV; NORM_POS_LT; VECTOR_SUB_EQ]]]);;
-
-let PATH_CONNECTED_COMPLEMENT_HOMEOMORPHIC_INTERVAL = prove
- (`!s:real^N->bool a b:real^M.
- 2 <= dimindex(:N) /\ s homeomorphic interval[a,b]
- ==> path_connected((:real^N) DIFF s)`,
- REPEAT STRIP_TAC THEN REWRITE_TAC[PATH_CONNECTED_IFF_PATH_COMPONENT] THEN
- FIRST_ASSUM(MP_TAC o MATCH_MP
- UNBOUNDED_PATH_COMPONENTS_COMPLEMENT_HOMEOMORPHIC_INTERVAL) THEN
- ASM_REWRITE_TAC[SET_RULE `~(x IN s) <=> x IN (UNIV DIFF s)`] THEN
- ABBREV_TAC `t = (:real^N) DIFF s` THEN
- DISCH_TAC THEN MAP_EVERY X_GEN_TAC [`x:real^N`; `y:real^N`] THEN
- STRIP_TAC THEN FIRST_ASSUM(MP_TAC o MATCH_MP HOMEOMORPHIC_COMPACTNESS) THEN
- REWRITE_TAC[COMPACT_INTERVAL] THEN
- DISCH_THEN(MP_TAC o MATCH_MP COMPACT_IMP_BOUNDED) THEN
- REWRITE_TAC[BOUNDED_POS; LEFT_IMP_EXISTS_THM] THEN
- X_GEN_TAC `B:real` THEN STRIP_TAC THEN
- SUBGOAL_THEN `(?u:real^N. u IN path_component t x /\ B < norm(u)) /\
- (?v:real^N. v IN path_component t y /\ B < norm(v))`
- STRIP_ASSUME_TAC THENL
- [ASM_MESON_TAC[BOUNDED_POS; REAL_NOT_LE]; ALL_TAC] THEN
- MATCH_MP_TAC PATH_COMPONENT_TRANS THEN EXISTS_TAC `u:real^N` THEN
- CONJ_TAC THENL [ASM_MESON_TAC[IN]; ALL_TAC] THEN
- MATCH_MP_TAC PATH_COMPONENT_SYM THEN
- MATCH_MP_TAC PATH_COMPONENT_TRANS THEN EXISTS_TAC `v:real^N` THEN
- CONJ_TAC THENL [ASM_MESON_TAC[IN]; ALL_TAC] THEN
- MATCH_MP_TAC PATH_COMPONENT_OF_SUBSET THEN
- EXISTS_TAC `(:real^N) DIFF cball(vec 0,B)` THEN CONJ_TAC THENL
- [EXPAND_TAC "t" THEN MATCH_MP_TAC(SET_RULE
- `s SUBSET t ==> (u DIFF t) SUBSET (u DIFF s)`) THEN
- ASM_REWRITE_TAC[SUBSET; IN_CBALL_0];
- MP_TAC(ISPEC `cball(vec 0:real^N,B)`
- PATH_CONNECTED_COMPLEMENT_BOUNDED_CONVEX) THEN
- ASM_REWRITE_TAC[BOUNDED_CBALL; CONVEX_CBALL] THEN
- REWRITE_TAC[PATH_CONNECTED_IFF_PATH_COMPONENT] THEN
- DISCH_THEN MATCH_MP_TAC THEN
- ASM_REWRITE_TAC[IN_DIFF; IN_UNIV; IN_CBALL_0; REAL_NOT_LE]]);;
-
-(* ------------------------------------------------------------------------- *)
-(* In particular, apply all these to the special case of an arc. *)
-(* ------------------------------------------------------------------------- *)
-
-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)`,
- REWRITE_TAC[arc; path; path_image] THEN REPEAT STRIP_TAC THEN
- MATCH_MP_TAC RETRACTION_INJECTIVE_IMAGE_INTERVAL THEN
- ASM_REWRITE_TAC[INTERVAL_EQ_EMPTY_CART_1; DROP_VEC; REAL_NOT_LT; REAL_POS]);;
-
-let PATH_CONNECTED_ARC_COMPLEMENT = prove
- (`!p. 2 <= dimindex(:N) /\ arc p
- ==> path_connected((:real^N) DIFF path_image p)`,
- REWRITE_TAC[arc; path] THEN REPEAT STRIP_TAC THEN SIMP_TAC[path_image] THEN
- MP_TAC(ISPECL [`path_image p:real^N->bool`; `vec 0:real^1`; `vec 1:real^1`]
- PATH_CONNECTED_COMPLEMENT_HOMEOMORPHIC_INTERVAL) THEN
- ASM_REWRITE_TAC[path_image] THEN DISCH_THEN MATCH_MP_TAC THEN
- ONCE_REWRITE_TAC[HOMEOMORPHIC_SYM] THEN
- MATCH_MP_TAC HOMEOMORPHIC_COMPACT THEN
- EXISTS_TAC `p:real^1->real^N` THEN ASM_REWRITE_TAC[COMPACT_INTERVAL]);;
-
-let CONNECTED_ARC_COMPLEMENT = prove
- (`!p. 2 <= dimindex(:N) /\ arc p
- ==> connected((:real^N) DIFF path_image p)`,
- SIMP_TAC[PATH_CONNECTED_ARC_COMPLEMENT; PATH_CONNECTED_IMP_CONNECTED]);; *)
-
end