REPEAT GEN_TAC THEN STRIP_TAC THEN
MAP_EVERY (MP_TAC o C ISPEC
JORDAN_INSIDE_OUTSIDE)
[`(
c1 ++
reversepath c2):real^1->real^2`;
`(
c1 ++
reversepath c):real^1->real^2`;
`(c2 ++
reversepath c):real^1->real^2`] THEN
ASM_SIMP_TAC[
PATHSTART_JOIN;
PATHFINISH_JOIN;
PATHSTART_REVERSEPATH;
PATHFINISH_REVERSEPATH;
SIMPLE_PATH_JOIN_LOOP;
SIMPLE_PATH_IMP_ARC;
PATH_IMAGE_JOIN;
SIMPLE_PATH_IMP_PATH;
PATH_IMAGE_REVERSEPATH;
SIMPLE_PATH_REVERSEPATH;
ARC_REVERSEPATH;
SUBSET_REFL] THEN
REPLICATE_TAC 3 STRIP_TAC THEN
SUBGOAL_THEN
`
path_image(c:real^1->real^2)
INTER
outside(
path_image c1 UNION path_image c2) = {}`
ASSUME_TAC THENL
[MATCH_MP_TAC(TAUT `(~p ==> F) ==> p`) THEN DISCH_TAC THEN
SUBGOAL_THEN
`
connected(
path_image(c:real^1->real^2)
DIFF
{
pathstart c,
pathfinish c})`
MP_TAC THENL [ASM_SIMP_TAC[
CONNECTED_SIMPLE_PATH_ENDLESS]; ALL_TAC] THEN
ASM_REWRITE_TAC[
connected] THEN
MAP_EVERY EXISTS_TAC
[`
inside(
path_image c1 UNION path_image c2):real^2->bool`;
`
outside(
path_image c1 UNION path_image c2):real^2->bool`] THEN
ASM_REWRITE_TAC[] THEN ASM SET_TAC[];
ALL_TAC] THEN
SUBGOAL_THEN
`
outside(
path_image c1 UNION path_image c2)
SUBSET
outside(
path_image c1 UNION path_image (c:real^1->real^2)) /\
outside(
path_image c1 UNION path_image c2)
SUBSET
outside(
path_image c2
UNION path_image c)`
STRIP_ASSUME_TAC THENL
[CONJ_TAC THENL
[ALL_TAC; GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [
UNION_COMM]] THEN
MATCH_MP_TAC
OUTSIDE_UNION_OUTSIDE_UNION THEN ASM_REWRITE_TAC[] THEN
ONCE_REWRITE_TAC[
UNION_COMM] THEN ASM_REWRITE_TAC[];
ALL_TAC] THEN
SUBGOAL_THEN
`
path_image(c1:real^1->real^2)
INTER
inside(
path_image c2
UNION path_image c) = {}`
ASSUME_TAC THENL
[MATCH_MP_TAC(TAUT `(~p ==> F) ==> p`) THEN DISCH_TAC THEN
SUBGOAL_THEN
`
frontier(
outside(
path_image c1 UNION path_image c2)):real^2->bool =
frontier(
outside(
path_image c2
UNION path_image c))`
MP_TAC THENL
[AP_TERM_TAC THEN MATCH_MP_TAC
SUBSET_ANTISYM THEN ASM_REWRITE_TAC[] THEN
GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [
UNION_COMM] THEN
MATCH_MP_TAC
OUTSIDE_UNION_OUTSIDE_UNION THEN
MATCH_MP_TAC(TAUT `(~p ==> F) ==> p`) THEN DISCH_TAC THEN
SUBGOAL_THEN
`
connected(
path_image(c1:real^1->real^2)
DIFF
{
pathstart c1,
pathfinish c1})`
MP_TAC THENL [ASM_SIMP_TAC[
CONNECTED_SIMPLE_PATH_ENDLESS]; ALL_TAC] THEN
ASM_REWRITE_TAC[
connected] THEN
MAP_EVERY EXISTS_TAC
[`
inside(
path_image c2
UNION path_image c):real^2->bool`;
`
outside(
path_image c2
UNION path_image c):real^2->bool`] THEN
ASM_REWRITE_TAC[] THEN ASM SET_TAC[];
MP_TAC(ISPEC `c:real^1->real^2`
NONEMPTY_SIMPLE_PATH_ENDLESS) THEN
ASM_REWRITE_TAC[] THEN ASM SET_TAC[]];
ALL_TAC] THEN
SUBGOAL_THEN
`
path_image(c2:real^1->real^2)
INTER
inside(
path_image c1 UNION path_image c) = {}`
ASSUME_TAC THENL
[MATCH_MP_TAC(TAUT `(~p ==> F) ==> p`) THEN DISCH_TAC THEN
SUBGOAL_THEN
`
frontier(
outside(
path_image c1 UNION path_image c2)):real^2->bool =
frontier(
outside(
path_image c1 UNION path_image c))`
MP_TAC THENL
[AP_TERM_TAC THEN MATCH_MP_TAC
SUBSET_ANTISYM THEN ASM_REWRITE_TAC[] THEN
MATCH_MP_TAC
OUTSIDE_UNION_OUTSIDE_UNION THEN
MATCH_MP_TAC(TAUT `(~p ==> F) ==> p`) THEN DISCH_TAC THEN
SUBGOAL_THEN
`
connected(
path_image(c2:real^1->real^2)
DIFF
{
pathstart c2,
pathfinish c2})`
MP_TAC THENL [ASM_SIMP_TAC[
CONNECTED_SIMPLE_PATH_ENDLESS]; ALL_TAC] THEN
ASM_REWRITE_TAC[
connected] THEN
MAP_EVERY EXISTS_TAC
[`
inside(
path_image c1 UNION path_image c):real^2->bool`;
`
outside(
path_image c1 UNION path_image c):real^2->bool`] THEN
ASM_REWRITE_TAC[] THEN ASM SET_TAC[];
MP_TAC(ISPEC `c:real^1->real^2`
NONEMPTY_SIMPLE_PATH_ENDLESS) THEN
ASM_REWRITE_TAC[] THEN ASM SET_TAC[]];
ALL_TAC] THEN
SUBGOAL_THEN
`
inside(
path_image c1 UNION path_image (c:real^1->real^2))
SUBSET
inside(
path_image c1 UNION path_image c2) /\
inside(
path_image c2
UNION path_image (c:real^1->real^2))
SUBSET
inside(
path_image c1 UNION path_image c2)`
STRIP_ASSUME_TAC THENL
[CONJ_TAC THEN REWRITE_TAC[
INSIDE_OUTSIDE] THEN
REWRITE_TAC[SET_RULE `
UNIV DIFF t
SUBSET UNIV DIFF s <=> s
SUBSET t`] THENL
[ALL_TAC; GEN_REWRITE_TAC (LAND_CONV o LAND_CONV) [
UNION_COMM]] THEN
MATCH_MP_TAC(SET_RULE
`out1
SUBSET out2 /\ c2
DIFF (
c1 UNION c)
SUBSET out2
==> (
c1 UNION c2)
UNION out1
SUBSET (
c1 UNION c)
UNION out2`) THEN
ASM_REWRITE_TAC[] THEN
REWRITE_TAC[
OUTSIDE_INSIDE] THEN ASM SET_TAC[];
ALL_TAC] THEN
SUBGOAL_THEN
`
inside(
path_image c1 UNION path_image c :real^2->bool)
SUBSET
outside(
path_image c2
UNION path_image c) /\
inside(
path_image c2
UNION path_image c)
SUBSET
outside(
path_image c1 UNION path_image c)`
STRIP_ASSUME_TAC THENL
[REWRITE_TAC[
SUBSET] THEN CONJ_TAC THEN
X_GEN_TAC `x:real^2` THEN DISCH_TAC THENL
[SUBGOAL_THEN `?z:real^2. z
IN path_image c1 /\
z
IN outside(
path_image c2
UNION path_image c)`
(CHOOSE_THEN (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THENL
[REWRITE_TAC[
OUTSIDE_INSIDE;
IN_DIFF;
IN_UNION;
IN_UNIV] THEN
MP_TAC(ISPEC `c1:real^1->real^2`
NONEMPTY_SIMPLE_PATH_ENDLESS) THEN
ASM_REWRITE_TAC[] THEN ASM SET_TAC[];
ALL_TAC] THEN
DISCH_THEN(fun
th -> ASSUME_TAC
th THEN MP_TAC
th) THEN
REWRITE_TAC[
OUTSIDE;
IN_ELIM_THM; CONTRAPOS_THM] THEN
MATCH_MP_TAC EQ_IMP THEN AP_TERM_TAC THEN
MATCH_MP_TAC
CONNECTED_COMPONENT_EQ THEN REWRITE_TAC[
IN] THEN
MP_TAC(ASSUME
`open(
outside(
path_image c2
UNION path_image c):real^2->bool)`) THEN
REWRITE_TAC[
OPEN_CONTAINS_BALL] THEN
DISCH_THEN(MP_TAC o SPEC `z:real^2`) THEN ASM_REWRITE_TAC[] THEN
DISCH_THEN(X_CHOOSE_THEN `e:real` STRIP_ASSUME_TAC) THEN
MP_TAC(ASSUME
`
frontier(
inside(
path_image c1 UNION path_image c):real^2->bool) =
path_image c1 UNION path_image c`) THEN
GEN_REWRITE_TAC LAND_CONV [
EXTENSION] THEN
DISCH_THEN(MP_TAC o SPEC `z:real^2`) THEN REWRITE_TAC[
frontier] THEN
ASM_SIMP_TAC[
IN_UNION;
IN_DIFF;
CLOSURE_APPROACHABLE;
IN_ELIM_THM] THEN
DISCH_THEN(MP_TAC o SPEC `e:real` o CONJUNCT1) THEN
ASM_REWRITE_TAC[
LEFT_IMP_EXISTS_THM] THEN
X_GEN_TAC `w:real^2` THEN STRIP_TAC THEN
MATCH_MP_TAC
CONNECTED_COMPONENT_TRANS THEN EXISTS_TAC `w:real^2` THEN
REWRITE_TAC[
connected_component] THEN CONJ_TAC THENL
[EXISTS_TAC
`
outside(
path_image c2
UNION path_image c:real^2->bool)` THEN
ASM_REWRITE_TAC[SET_RULE `s
SUBSET UNIV DIFF t <=> s
INTER t = {}`;
OUTSIDE_NO_OVERLAP] THEN
FIRST_X_ASSUM(MATCH_MP_TAC o GEN_REWRITE_RULE I [
SUBSET]) THEN
ASM_REWRITE_TAC[ONCE_REWRITE_RULE[
DIST_SYM]
IN_BALL];
EXISTS_TAC `
inside(
path_image c1 UNION path_image c:real^2->bool)` THEN
ASM_REWRITE_TAC[] THEN
MATCH_MP_TAC(SET_RULE
`
inside(
c1 UNION c)
INTER (
c1 UNION c) = {} /\
c2
INTER inside(
c1 UNION c) = {}
==>
inside(
c1 UNION c)
SUBSET UNIV DIFF (c2
UNION c)`) THEN
ASM_REWRITE_TAC[
INSIDE_NO_OVERLAP]];
SUBGOAL_THEN `?z:real^2. z
IN path_image c2 /\
z
IN outside(
path_image c1 UNION path_image c)`
(CHOOSE_THEN (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THENL
[REWRITE_TAC[
OUTSIDE_INSIDE;
IN_DIFF;
IN_UNION;
IN_UNIV] THEN
MP_TAC(ISPEC `c2:real^1->real^2`
NONEMPTY_SIMPLE_PATH_ENDLESS) THEN
ASM_REWRITE_TAC[] THEN ASM SET_TAC[];
ALL_TAC] THEN
DISCH_THEN(fun
th -> ASSUME_TAC
th THEN MP_TAC
th) THEN
REWRITE_TAC[
OUTSIDE;
IN_ELIM_THM; CONTRAPOS_THM] THEN
MATCH_MP_TAC EQ_IMP THEN AP_TERM_TAC THEN
MATCH_MP_TAC
CONNECTED_COMPONENT_EQ THEN REWRITE_TAC[
IN] THEN
MP_TAC(ASSUME
`open(
outside(
path_image c1 UNION path_image c):real^2->bool)`) THEN
REWRITE_TAC[
OPEN_CONTAINS_BALL] THEN
DISCH_THEN(MP_TAC o SPEC `z:real^2`) THEN ASM_REWRITE_TAC[] THEN
DISCH_THEN(X_CHOOSE_THEN `e:real` STRIP_ASSUME_TAC) THEN
MP_TAC(ASSUME
`
frontier(
inside(
path_image c2
UNION path_image c):real^2->bool) =
path_image c2
UNION path_image c`) THEN
GEN_REWRITE_TAC LAND_CONV [
EXTENSION] THEN
DISCH_THEN(MP_TAC o SPEC `z:real^2`) THEN REWRITE_TAC[
frontier] THEN
ASM_SIMP_TAC[
IN_UNION;
IN_DIFF;
CLOSURE_APPROACHABLE;
IN_ELIM_THM] THEN
DISCH_THEN(MP_TAC o SPEC `e:real` o CONJUNCT1) THEN
ASM_REWRITE_TAC[
LEFT_IMP_EXISTS_THM] THEN
X_GEN_TAC `w:real^2` THEN STRIP_TAC THEN
MATCH_MP_TAC
CONNECTED_COMPONENT_TRANS THEN EXISTS_TAC `w:real^2` THEN
REWRITE_TAC[
connected_component] THEN CONJ_TAC THENL
[EXISTS_TAC
`
outside(
path_image c1 UNION path_image c:real^2->bool)` THEN
ASM_REWRITE_TAC[SET_RULE `s
SUBSET UNIV DIFF t <=> s
INTER t = {}`;
OUTSIDE_NO_OVERLAP] THEN
FIRST_X_ASSUM(MATCH_MP_TAC o GEN_REWRITE_RULE I [
SUBSET]) THEN
ASM_REWRITE_TAC[ONCE_REWRITE_RULE[
DIST_SYM]
IN_BALL];
EXISTS_TAC `
inside(
path_image c2
UNION path_image c:real^2->bool)` THEN
ASM_REWRITE_TAC[] THEN
MATCH_MP_TAC(SET_RULE
`
inside(c2
UNION c)
INTER (c2
UNION c) = {} /\
c1 INTER inside(c2
UNION c) = {}
==>
inside(c2
UNION c)
SUBSET UNIV DIFF (
c1 UNION c)`) THEN
ASM_REWRITE_TAC[
INSIDE_NO_OVERLAP]]];
ALL_TAC] THEN
CONJ_TAC THENL
[MATCH_MP_TAC(SET_RULE
`!u. s
SUBSET u /\ t
INTER u = {} ==> s
INTER t = {}`) THEN
EXISTS_TAC `
outside(
path_image c2
UNION path_image c):real^2->bool` THEN
ASM_REWRITE_TAC[
INSIDE_INTER_OUTSIDE];
ALL_TAC] THEN
SUBGOAL_THEN
`!x:real^2. ~(x
IN path_image c) /\
x
IN inside(
path_image c1 UNION path_image c2) /\
~(x
IN inside(
path_image c1 UNION path_image c)) /\
~(x
IN inside(
path_image c2
UNION path_image c)) ==> F`
ASSUME_TAC THENL [ALL_TAC; ASM SET_TAC[]] THEN
X_GEN_TAC `z:real^2` THEN STRIP_TAC THEN
SUBGOAL_THEN `~((z:real^2)
IN (
path_image c1 UNION path_image c2))`
MP_TAC THENL
[ASM_MESON_TAC[
INSIDE_NO_OVERLAP;
NOT_IN_EMPTY;
IN_INTER];
PURE_REWRITE_TAC[
IN_UNION; DE_MORGAN_THM] THEN STRIP_TAC] THEN
MAP_EVERY (MP_TAC o C ISPEC
INSIDE_UNION_OUTSIDE)
[`
path_image c1 UNION path_image c:real^2->bool`;
`
path_image c2
UNION path_image c:real^2->bool`] THEN
PURE_REWRITE_TAC[IMP_IMP] THEN REWRITE_TAC[
EXTENSION;
IN_UNION] THEN
REWRITE_TAC[
AND_FORALL_THM] THEN DISCH_THEN(MP_TAC o SPEC `z:real^2`) THEN
ASM_REWRITE_TAC[
IN_UNIV;
IN_DIFF;
IN_UNION] THEN STRIP_TAC THEN
MP_TAC(ASSUME
`~(
outside(
path_image c1 UNION path_image c2:real^2->bool) = {})`) THEN
GEN_REWRITE_TAC LAND_CONV [GSYM
MEMBER_NOT_EMPTY] THEN
DISCH_THEN(X_CHOOSE_TAC `w:real^2`) THEN
SUBGOAL_THEN `(w:real^2)
IN outside(
path_image c1 UNION path_image c) /\
w
IN outside(
path_image c2
UNION path_image c)`
STRIP_ASSUME_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
SUBGOAL_THEN
`~((w:real^2)
IN (
path_image c1 UNION path_image c2)) /\
~(w
IN path_image c1 UNION path_image c)`
MP_TAC THENL
[ASM_MESON_TAC[
OUTSIDE_NO_OVERLAP;
NOT_IN_EMPTY;
IN_INTER];
PURE_REWRITE_TAC[
IN_UNION;
CONJ_ACI; DE_MORGAN_THM] THEN STRIP_TAC] THEN
MAP_EVERY (MP_TAC o C ISPEC
INSIDE_INTER_OUTSIDE)
[`
path_image c1 UNION path_image c2:real^2->bool`;
`
path_image c1 UNION path_image c:real^2->bool`;
`
path_image c2
UNION path_image c:real^2->bool`] THEN
PURE_REWRITE_TAC[IMP_IMP] THEN
REWRITE_TAC[
EXTENSION;
IN_INTER;
NOT_IN_EMPTY] THEN
REWRITE_TAC[
AND_FORALL_THM] THEN DISCH_THEN(MP_TAC o SPEC `w:real^2`) THEN
ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
MP_TAC(ISPEC
`
outside(
path_image c2
UNION path_image c):real^2->bool`
CONNECTED_OPEN_ARC_CONNECTED) THEN
ASM_REWRITE_TAC[] THEN
DISCH_THEN(MP_TAC o SPECL [`z:real^2`; `w:real^2`]) THEN
ASM_REWRITE_TAC[] THEN
DISCH_THEN(DISJ_CASES_THEN MP_TAC) THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
DISCH_THEN(X_CHOOSE_THEN `g1:real^1->real^2` STRIP_ASSUME_TAC) THEN
MP_TAC(ISPEC
`
outside(
path_image c1 UNION path_image c):real^2->bool`
CONNECTED_OPEN_ARC_CONNECTED) THEN
ASM_REWRITE_TAC[] THEN
DISCH_THEN(MP_TAC o SPECL [`z:real^2`; `w:real^2`]) THEN
ASM_REWRITE_TAC[] THEN
DISCH_THEN(DISJ_CASES_THEN MP_TAC) THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
DISCH_THEN(X_CHOOSE_THEN `g2:real^1->real^2` STRIP_ASSUME_TAC) THEN
SUBGOAL_THEN
`?h.
arc h /\
pathstart h = (z:real^2) /\
path_image h
DELETE pathfinish h
SUBSET
inside(
path_image c1 UNION path_image c2)
INTER
outside(
path_image c1 UNION path_image c)
INTER
outside(
path_image c2
UNION path_image c) /\
pathfinish h
IN path_image c1 /\
~(
pathfinish h
IN path_image c2)`
(X_CHOOSE_THEN `gzx:real^1->real^2` STRIP_ASSUME_TAC) THENL
[MP_TAC(ISPECL
[`g1:real^1->real^2`;
`
inside(
path_image c1 UNION path_image c2)
INTER
outside(
path_image c1 UNION path_image c)
INTER
outside(
path_image c2
UNION path_image c):real^2->bool`]
SUBPATH_TO_FRONTIER) THEN
ASM_SIMP_TAC[
ARC_IMP_PATH;
IN_INTER;
INTERIOR_INTER;
INTERIOR_OPEN] THEN
DISCH_THEN(X_CHOOSE_THEN `u:real^1` STRIP_ASSUME_TAC) THEN
ABBREV_TAC `h:real^1->real^2 =
subpath (
vec 0) u g1` THEN
EXISTS_TAC `h:real^1->real^2` THEN ASM_REWRITE_TAC[] THEN
EXPAND_TAC "h" THEN
REWRITE_TAC[
PATHSTART_SUBPATH;
PATHFINISH_SUBPATH] THEN
MATCH_MP_TAC(TAUT `b /\ (c ==> a) /\ c ==> a /\ b /\ c`) THEN
CONJ_TAC THENL [ASM_MESON_TAC[
pathstart]; ALL_TAC] THEN CONJ_TAC THENL
[DISCH_TAC THEN MATCH_MP_TAC
ARC_SIMPLE_PATH_SUBPATH THEN
ASM_SIMP_TAC[
ENDS_IN_UNIT_INTERVAL;
ARC_IMP_SIMPLE_PATH] THEN
DISCH_THEN(SUBST_ALL_TAC o SYM) THEN
MP_TAC(ISPEC `
path_image c1 UNION path_image c2:real^2->bool`
INSIDE_NO_OVERLAP) THEN
REWRITE_TAC[GSYM
MEMBER_NOT_EMPTY] THEN
EXISTS_TAC `
pathstart(g1:real^1->real^2)` THEN
ASM_REWRITE_TAC[
IN_INTER] THEN
REWRITE_TAC[
IN_UNION] THEN DISJ1_TAC THEN ASM_MESON_TAC[
pathstart];
ALL_TAC] THEN
UNDISCH_TAC
`(
pathfinish h:real^2)
IN
frontier
(
inside (
path_image c1 UNION path_image c2)
INTER
outside (
path_image c1 UNION path_image c)
INTER
outside (
path_image c2
UNION path_image c))` THEN
EXPAND_TAC "h" THEN REWRITE_TAC[
PATHFINISH_SUBPATH] THEN
DISCH_THEN(MP_TAC o MATCH_MP (REWRITE_RULE[
SUBSET]
FRONTIER_INTER_SUBSET)) THEN ASM_REWRITE_TAC[] THEN
MP_TAC(ASSUME
`(
path_image g1:real^2->bool)
SUBSET
outside(
path_image c2
UNION path_image c)`) THEN
DISCH_THEN(MP_TAC o SPEC `(g1:real^1->real^2) u` o
REWRITE_RULE[
SUBSET]) THEN
GEN_REWRITE_TAC (LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV) [
path_image] THEN
REWRITE_TAC[
IN_IMAGE] THEN ANTS_TAC THENL [ASM_MESON_TAC[]; DISCH_TAC] THEN
MP_TAC(ISPEC `
path_image c2
UNION path_image c:real^2->bool`
OUTSIDE_NO_OVERLAP) THEN
GEN_REWRITE_TAC LAND_CONV [
EXTENSION] THEN
DISCH_THEN(MP_TAC o SPEC `(g1:real^1->real^2) u`) THEN
ASM_REWRITE_TAC[
IN_INTER;
IN_UNION;
NOT_IN_EMPTY; DE_MORGAN_THM] THEN
STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
DISCH_THEN(DISJ_CASES_THEN2 ACCEPT_TAC MP_TAC) THEN
DISCH_THEN(MP_TAC o MATCH_MP (REWRITE_RULE[
SUBSET]
FRONTIER_INTER_SUBSET)) THEN ASM_REWRITE_TAC[] THEN
ASM_REWRITE_TAC[
IN_UNION];
ABBREV_TAC `x:real^2 =
pathfinish gzx`] THEN
SUBGOAL_THEN
`?h.
arc h /\
pathstart h = (w:real^2) /\
path_image h
DELETE pathfinish h
SUBSET
outside(
path_image c1 UNION path_image c2) /\
pathfinish h
IN path_image c1 /\
~(
pathfinish h
IN path_image c2)`
(X_CHOOSE_THEN `gwx:real^1->real^2` STRIP_ASSUME_TAC) THENL
[MP_TAC(ISPECL
[`
reversepath g1:real^1->real^2`;
`
outside(
path_image c1 UNION path_image c2):real^2->bool`]
SUBPATH_TO_FRONTIER) THEN
ASM_SIMP_TAC[
ARC_IMP_PATH;
IN_INTER;
INTERIOR_INTER;
INTERIOR_OPEN;
PATH_REVERSEPATH;
PATHSTART_REVERSEPATH;
PATHFINISH_REVERSEPATH] THEN
ANTS_TAC THENL
[ASM_MESON_TAC[
INSIDE_INTER_OUTSIDE;
IN_INTER;
NOT_IN_EMPTY];
ALL_TAC] THEN
DISCH_THEN(X_CHOOSE_THEN `u:real^1` STRIP_ASSUME_TAC) THEN
ABBREV_TAC `h:real^1->real^2 =
subpath (
vec 0) u (
reversepath g1)` THEN
EXISTS_TAC `h:real^1->real^2` THEN ASM_REWRITE_TAC[] THEN
EXPAND_TAC "h" THEN
REWRITE_TAC[
PATHSTART_SUBPATH;
PATHFINISH_SUBPATH] THEN
MATCH_MP_TAC(TAUT `b /\ (c ==> a) /\ c ==> a /\ b /\ c`) THEN
CONJ_TAC THENL
[ASM_MESON_TAC[
pathstart;
PATHSTART_REVERSEPATH]; ALL_TAC] THEN
CONJ_TAC THENL
[DISCH_TAC THEN MATCH_MP_TAC
ARC_SIMPLE_PATH_SUBPATH THEN
ASM_SIMP_TAC[
ENDS_IN_UNIT_INTERVAL;
ARC_IMP_SIMPLE_PATH;
SIMPLE_PATH_REVERSEPATH] THEN
DISCH_THEN(SUBST_ALL_TAC o SYM) THEN
MP_TAC(ISPEC `
path_image c1 UNION path_image c2:real^2->bool`
OUTSIDE_NO_OVERLAP) THEN
REWRITE_TAC[GSYM
MEMBER_NOT_EMPTY] THEN
EXISTS_TAC `
pathstart(
reversepath g1:real^1->real^2)` THEN
ASM_REWRITE_TAC[
IN_INTER] THEN CONJ_TAC THENL
[ASM_REWRITE_TAC[
PATHSTART_REVERSEPATH];
REWRITE_TAC[
IN_UNION] THEN DISJ1_TAC THEN ASM_MESON_TAC[
pathstart]];
ALL_TAC] THEN
UNDISCH_TAC
`(
pathfinish h:real^2)
IN path_image c1 UNION path_image c2` THEN
EXPAND_TAC "h" THEN REWRITE_TAC[
PATHFINISH_SUBPATH] THEN
MP_TAC(ASSUME
`(
path_image g1:real^2->bool)
SUBSET
outside(
path_image c2
UNION path_image c)`) THEN
DISCH_THEN(MP_TAC o SPEC `
reversepath (g1:real^1->real^2) u` o
REWRITE_RULE[
SUBSET]) THEN
ANTS_TAC THENL
[ONCE_REWRITE_TAC[GSYM
PATH_IMAGE_REVERSEPATH] THEN
REWRITE_TAC[
path_image;
IN_IMAGE] THEN ASM_MESON_TAC[];
DISCH_TAC] THEN
MP_TAC(ISPEC `
path_image c2
UNION path_image c:real^2->bool`
OUTSIDE_NO_OVERLAP) THEN
GEN_REWRITE_TAC LAND_CONV [
EXTENSION] THEN
DISCH_THEN(MP_TAC o SPEC `
reversepath (g1:real^1->real^2) u`) THEN
ASM_REWRITE_TAC[
IN_INTER;
IN_UNION;
NOT_IN_EMPTY; DE_MORGAN_THM] THEN
CONV_TAC TAUT;
ABBREV_TAC `x':real^2 =
pathfinish gwx`] THEN
SUBGOAL_THEN
`?h.
arc h /\
pathstart h = (z:real^2) /\
path_image h
DELETE pathfinish h
SUBSET
inside(
path_image c1 UNION path_image c2)
INTER
outside(
path_image c1 UNION path_image c)
INTER
outside(
path_image c2
UNION path_image c) /\
pathfinish h
IN path_image c2 /\
~(
pathfinish h
IN path_image c1)`
(X_CHOOSE_THEN `gzy:real^1->real^2` STRIP_ASSUME_TAC) THENL
[MP_TAC(ISPECL
[`g2:real^1->real^2`;
`
inside(
path_image c1 UNION path_image c2)
INTER
outside(
path_image c1 UNION path_image c)
INTER
outside(
path_image c2
UNION path_image c):real^2->bool`]
SUBPATH_TO_FRONTIER) THEN
ASM_SIMP_TAC[
ARC_IMP_PATH;
IN_INTER;
INTERIOR_INTER;
INTERIOR_OPEN] THEN
DISCH_THEN(X_CHOOSE_THEN `u:real^1` STRIP_ASSUME_TAC) THEN
ABBREV_TAC `h:real^1->real^2 =
subpath (
vec 0) u g2` THEN
EXISTS_TAC `h:real^1->real^2` THEN ASM_REWRITE_TAC[] THEN
EXPAND_TAC "h" THEN
REWRITE_TAC[
PATHSTART_SUBPATH;
PATHFINISH_SUBPATH] THEN
MATCH_MP_TAC(TAUT `b /\ (c ==> a) /\ c ==> a /\ b /\ c`) THEN
CONJ_TAC THENL [ASM_MESON_TAC[
pathstart]; ALL_TAC] THEN CONJ_TAC THENL
[DISCH_TAC THEN MATCH_MP_TAC
ARC_SIMPLE_PATH_SUBPATH THEN
ASM_SIMP_TAC[
ENDS_IN_UNIT_INTERVAL;
ARC_IMP_SIMPLE_PATH] THEN
DISCH_THEN(SUBST_ALL_TAC o SYM) THEN
MP_TAC(ISPEC `
path_image c1 UNION path_image c2:real^2->bool`
INSIDE_NO_OVERLAP) THEN
REWRITE_TAC[GSYM
MEMBER_NOT_EMPTY] THEN
EXISTS_TAC `
pathstart(g2:real^1->real^2)` THEN
ASM_REWRITE_TAC[
IN_INTER] THEN
REWRITE_TAC[
IN_UNION] THEN DISJ1_TAC THEN ASM_MESON_TAC[
pathstart];
ALL_TAC] THEN
UNDISCH_TAC
`(
pathfinish h:real^2)
IN
frontier
(
inside (
path_image c1 UNION path_image c2)
INTER
outside (
path_image c1 UNION path_image c)
INTER
outside (
path_image c2
UNION path_image c))` THEN
EXPAND_TAC "h" THEN REWRITE_TAC[
PATHFINISH_SUBPATH] THEN
DISCH_THEN(MP_TAC o MATCH_MP (REWRITE_RULE[
SUBSET]
FRONTIER_INTER_SUBSET)) THEN ASM_REWRITE_TAC[] THEN
MP_TAC(ASSUME
`(
path_image g2:real^2->bool)
SUBSET
outside(
path_image c1 UNION path_image c)`) THEN
DISCH_THEN(MP_TAC o SPEC `(g2:real^1->real^2) u` o
REWRITE_RULE[
SUBSET]) THEN
GEN_REWRITE_TAC (LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV) [
path_image] THEN
REWRITE_TAC[
IN_IMAGE] THEN ANTS_TAC THENL [ASM_MESON_TAC[]; DISCH_TAC] THEN
MP_TAC(ISPEC `
path_image c1 UNION path_image c:real^2->bool`
OUTSIDE_NO_OVERLAP) THEN
GEN_REWRITE_TAC LAND_CONV [
EXTENSION] THEN
DISCH_THEN(MP_TAC o SPEC `(g2:real^1->real^2) u`) THEN
ASM_REWRITE_TAC[
IN_INTER;
IN_UNION;
NOT_IN_EMPTY; DE_MORGAN_THM] THEN
STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
DISCH_THEN(DISJ_CASES_THEN2 ACCEPT_TAC MP_TAC) THEN
DISCH_THEN(MP_TAC o MATCH_MP (REWRITE_RULE[
SUBSET]
FRONTIER_INTER_SUBSET)) THEN ASM_REWRITE_TAC[] THEN
ASM_REWRITE_TAC[
IN_UNION];
ABBREV_TAC `y:real^2 =
pathfinish gzy`] THEN
SUBGOAL_THEN
`?h.
arc h /\
pathstart h = (w:real^2) /\
path_image h
DELETE pathfinish h
SUBSET
outside(
path_image c1 UNION path_image c2) /\
pathfinish h
IN path_image c2 /\
~(
pathfinish h
IN path_image c1)`
(X_CHOOSE_THEN `gwy:real^1->real^2` STRIP_ASSUME_TAC) THENL
[MP_TAC(ISPECL
[`
reversepath g2:real^1->real^2`;
`
outside(
path_image c1 UNION path_image c2):real^2->bool`]
SUBPATH_TO_FRONTIER) THEN
ASM_SIMP_TAC[
ARC_IMP_PATH;
IN_INTER;
INTERIOR_INTER;
INTERIOR_OPEN;
PATH_REVERSEPATH;
PATHSTART_REVERSEPATH;
PATHFINISH_REVERSEPATH] THEN
ANTS_TAC THENL
[ASM_MESON_TAC[
INSIDE_INTER_OUTSIDE;
IN_INTER;
NOT_IN_EMPTY];
ALL_TAC] THEN
DISCH_THEN(X_CHOOSE_THEN `u:real^1` STRIP_ASSUME_TAC) THEN
ABBREV_TAC `h:real^1->real^2 =
subpath (
vec 0) u (
reversepath g2)` THEN
EXISTS_TAC `h:real^1->real^2` THEN ASM_REWRITE_TAC[] THEN
EXPAND_TAC "h" THEN
REWRITE_TAC[
PATHSTART_SUBPATH;
PATHFINISH_SUBPATH] THEN
MATCH_MP_TAC(TAUT `b /\ (c ==> a) /\ c ==> a /\ b /\ c`) THEN
CONJ_TAC THENL
[ASM_MESON_TAC[
pathstart;
PATHSTART_REVERSEPATH]; ALL_TAC] THEN
CONJ_TAC THENL
[DISCH_TAC THEN MATCH_MP_TAC
ARC_SIMPLE_PATH_SUBPATH THEN
ASM_SIMP_TAC[
ENDS_IN_UNIT_INTERVAL;
ARC_IMP_SIMPLE_PATH;
SIMPLE_PATH_REVERSEPATH] THEN
DISCH_THEN(SUBST_ALL_TAC o SYM) THEN
MP_TAC(ISPEC `
path_image c1 UNION path_image c2:real^2->bool`
OUTSIDE_NO_OVERLAP) THEN
REWRITE_TAC[GSYM
MEMBER_NOT_EMPTY] THEN
EXISTS_TAC `
pathstart(
reversepath g2:real^1->real^2)` THEN
ASM_REWRITE_TAC[
IN_INTER] THEN CONJ_TAC THENL
[ASM_REWRITE_TAC[
PATHSTART_REVERSEPATH];
REWRITE_TAC[
IN_UNION] THEN DISJ2_TAC THEN ASM_MESON_TAC[
pathstart]];
ALL_TAC] THEN
UNDISCH_TAC
`(
pathfinish h:real^2)
IN path_image c1 UNION path_image c2` THEN
EXPAND_TAC "h" THEN REWRITE_TAC[
PATHFINISH_SUBPATH] THEN
MP_TAC(ASSUME
`(
path_image g2:real^2->bool)
SUBSET
outside(
path_image c1 UNION path_image c)`) THEN
DISCH_THEN(MP_TAC o SPEC `
reversepath (g2:real^1->real^2) u` o
REWRITE_RULE[
SUBSET]) THEN
ANTS_TAC THENL
[ONCE_REWRITE_TAC[GSYM
PATH_IMAGE_REVERSEPATH] THEN
REWRITE_TAC[
path_image;
IN_IMAGE] THEN ASM_MESON_TAC[];
DISCH_TAC] THEN
MP_TAC(ISPEC `
path_image c1 UNION path_image c:real^2->bool`
OUTSIDE_NO_OVERLAP) THEN
GEN_REWRITE_TAC LAND_CONV [
EXTENSION] THEN
DISCH_THEN(MP_TAC o SPEC `
reversepath (g2:real^1->real^2) u`) THEN
ASM_REWRITE_TAC[
IN_INTER;
IN_UNION;
NOT_IN_EMPTY; DE_MORGAN_THM] THEN
CONV_TAC TAUT;
ABBREV_TAC `y':real^2 =
pathfinish gwy`] THEN
MP_TAC(ISPECL [`
reversepath gzx:real^1->real^2`; `gzy:real^1->real^2`]
ARC_CONNECTED_TRANS) THEN
ASM_SIMP_TAC[
ARC_REVERSEPATH;
PATHSTART_REVERSEPATH;
PATHFINISH_REVERSEPATH;
PATH_IMAGE_REVERSEPATH; NOT_IMP] THEN
CONJ_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
DISCH_THEN(X_CHOOSE_THEN `xy:real^1->real^2` STRIP_ASSUME_TAC) THEN
SUBGOAL_THEN
`(
path_image xy
DIFF {x:real^2,y})
SUBSET
inside(
path_image c1 UNION path_image c2)
INTER
outside(
path_image c1 UNION path_image c)
INTER
outside(
path_image c2
UNION path_image c)`
ASSUME_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
SUBGOAL_THEN
`~(((
path_image xy):real^2->bool)
INTER
inside(
path_image c1 UNION path_image c2)
INTER
outside(
path_image c1 UNION path_image c)
INTER
outside(
path_image c2
UNION path_image c) = {})`
ASSUME_TAC THENL
[MATCH_MP_TAC(SET_RULE
`!x y. ~(s
DIFF {x,y} = {}) /\ s
DIFF {x,y}
SUBSET t
==> ~(s
INTER t = {})`) THEN
MAP_EVERY EXISTS_TAC [`x:real^2`; `y:real^2`] THEN ASM_REWRITE_TAC[] THEN
ASM_MESON_TAC[
NONEMPTY_SIMPLE_PATH_ENDLESS;
ARC_IMP_SIMPLE_PATH];
ALL_TAC] THEN
MP_TAC(ISPECL [`
reversepath gwy:real^1->real^2`; `gwx:real^1->real^2`]
ARC_CONNECTED_TRANS) THEN
ASM_SIMP_TAC[
ARC_REVERSEPATH;
PATHSTART_REVERSEPATH;
PATHFINISH_REVERSEPATH;
PATH_IMAGE_REVERSEPATH; NOT_IMP] THEN
CONJ_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
DISCH_THEN(X_CHOOSE_THEN `y'x':real^1->real^2` STRIP_ASSUME_TAC) THEN
SUBGOAL_THEN
`(
path_image y'x'
DIFF {x':real^2,y'})
SUBSET
outside(
path_image c1 UNION path_image c2)`
ASSUME_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
SUBGOAL_THEN
`?xy'.
arc xy' /\
pathstart xy' = x /\
pathfinish xy' = (y':real^2) /\
(
path_image xy'
DELETE x)
SUBSET
(
inside (
path_image c1 UNION path_image c2)
INTER
outside (
path_image c1 UNION path_image c)
INTER
outside (
path_image c2
UNION path_image c))
UNION
(
path_image c2
DIFF {a,b}) /\
~(
path_image xy'
INTER
inside(
path_image c1 UNION path_image c2)
INTER
outside(
path_image c1 UNION path_image c)
INTER
outside(
path_image c2
UNION path_image c) = {})`
STRIP_ASSUME_TAC THENL
[ASM_CASES_TAC `y':real^2 = y` THENL
[UNDISCH_THEN `y':real^2 = y` SUBST_ALL_TAC THEN
EXISTS_TAC `xy:real^1->real^2` THEN ASM_REWRITE_TAC[] THEN
MATCH_MP_TAC(SET_RULE
`!y. p
DIFF {x,y}
SUBSET i /\ y
IN j
==> p
DELETE x
SUBSET (i
UNION j)`) THEN
EXISTS_TAC `y:real^2` THEN ASM_REWRITE_TAC[
IN_DIFF] THEN ASM SET_TAC[];
ALL_TAC] THEN
MP_TAC(ISPECL [`c2:real^1->real^2`; `y:real^2`; `y':real^2`]
EXISTS_SUBARC_OF_ARC_NOENDS) THEN
ASM_SIMP_TAC[
SIMPLE_PATH_IMP_ARC; NOT_IMP] THEN
ANTS_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
DISCH_THEN(X_CHOOSE_THEN `yy':real^1->real^2` STRIP_ASSUME_TAC) THEN
EXISTS_TAC `xy ++ yy':real^1->real^2` THEN
ASM_REWRITE_TAC[
PATHSTART_JOIN;
PATHFINISH_JOIN] THEN CONJ_TAC THENL
[MATCH_MP_TAC
ARC_JOIN THEN ASM_REWRITE_TAC[] THEN ASM SET_TAC[];
ASM_SIMP_TAC[
PATH_IMAGE_JOIN;
ARC_IMP_PATH] THEN
ASM_SIMP_TAC[SET_RULE
`~(a
INTER c = {}) ==> ~((a
UNION b)
INTER c = {})`] THEN
MATCH_MP_TAC(SET_RULE
`s
SUBSET (y
INSERT t) ==> s
DELETE y
SUBSET t`) THEN ASM SET_TAC[]];
ALL_TAC] THEN
SUBGOAL_THEN
`~((
path_image y'x':real^2->bool)
INTER
outside(
path_image c1 UNION path_image c2) = {})`
ASSUME_TAC THENL
[MP_TAC(ISPEC `y'x':real^1->real^2`
NONEMPTY_SIMPLE_PATH_ENDLESS) THEN
ASM_SIMP_TAC[
ARC_IMP_SIMPLE_PATH] THEN ASM SET_TAC[];
ALL_TAC] THEN
SUBGOAL_THEN
`?y'x.
arc y'x /\
pathstart y'x = y' /\
pathfinish y'x = (x:real^2) /\
~(
path_image y'x
INTER
outside(
path_image c1 UNION path_image c2) = {}) /\
(
path_image y'x
DELETE y')
SUBSET
outside(
path_image c1 UNION path_image c2)
UNION
(
path_image c1 DIFF {a,b})`
STRIP_ASSUME_TAC THENL
[ASM_CASES_TAC `x':real^2 = x` THENL
[UNDISCH_THEN `x':real^2 = x` SUBST_ALL_TAC THEN
EXISTS_TAC `y'x':real^1->real^2` THEN ASM_REWRITE_TAC[] THEN
MATCH_MP_TAC(SET_RULE
`!y. p
DIFF {x,y}
SUBSET i /\ y
IN j
==> p
DELETE x
SUBSET (i
UNION j)`) THEN
EXISTS_TAC `x:real^2` THEN ASM_REWRITE_TAC[
IN_DIFF] THEN ASM SET_TAC[];
ALL_TAC] THEN
MP_TAC(ISPECL [`c1:real^1->real^2`; `x':real^2`; `x:real^2`]
EXISTS_SUBARC_OF_ARC_NOENDS) THEN
ASM_SIMP_TAC[
SIMPLE_PATH_IMP_ARC; NOT_IMP] THEN
ANTS_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
DISCH_THEN(X_CHOOSE_THEN `x'x:real^1->real^2` STRIP_ASSUME_TAC) THEN
EXISTS_TAC `y'x' ++ x'x:real^1->real^2` THEN
ASM_REWRITE_TAC[
PATHSTART_JOIN;
PATHFINISH_JOIN] THEN
ASM_SIMP_TAC[
PATH_IMAGE_JOIN;
ARC_IMP_PATH] THEN REPEAT CONJ_TAC THENL
[MATCH_MP_TAC
ARC_JOIN THEN ASM_REWRITE_TAC[] THEN ASM SET_TAC[];
ASM SET_TAC[];
ASM SET_TAC[]];
ALL_TAC] THEN
SUBGOAL_THEN
`?j.
simple_path j /\
pathstart j = x /\
pathfinish j = (x:real^2) /\
~(
path_image j
INTER
inside(
path_image c1 UNION path_image c2) = {}) /\
~(
path_image j
INTER
outside(
path_image c1 UNION path_image c2) = {}) /\
path_image j
SUBSET
(
inside(
path_image c1 UNION path_image c2)
INTER
outside(
path_image c1 UNION path_image c)
INTER
outside(
path_image c2
UNION path_image c))
UNION
outside(
path_image c1 UNION path_image c2)
UNION
((
path_image c1 UNION path_image c2)
DIFF {a,b})`
STRIP_ASSUME_TAC THENL
[EXISTS_TAC `xy' ++ y'x:real^1->real^2` THEN
ASM_REWRITE_TAC[
PATHSTART_JOIN;
PATHFINISH_JOIN] THEN
ASM_SIMP_TAC[
PATH_IMAGE_JOIN;
ARC_IMP_PATH] THEN
CONJ_TAC THENL [ALL_TAC; ASM SET_TAC[]] THEN
MATCH_MP_TAC
SIMPLE_PATH_JOIN_LOOP THEN ASM_REWRITE_TAC[] THEN
FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP (SET_RULE
`xy
DELETE x
SUBSET s
==> !t. yx
DELETE y
SUBSET t /\ s
INTER t = {}
==> xy
INTER yx
SUBSET {x,y}`)) THEN
EXISTS_TAC `
outside(
path_image c1 UNION path_image c2)
UNION
path_image c1 DIFF {a:real^2, b}` THEN
ASM_REWRITE_TAC[] THEN
MP_TAC(ISPEC `
path_image c1 UNION path_image c2:real^2->bool`
INSIDE_NO_OVERLAP) THEN
MP_TAC(ISPEC `
path_image c1 UNION path_image c2:real^2->bool`
INSIDE_INTER_OUTSIDE) THEN
ASM SET_TAC[];
ALL_TAC] THEN
SUBGOAL_THEN `~((a:real^2)
IN path_image j)` ASSUME_TAC THENL
[FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (SET_RULE
`s
SUBSET t ==> ~(a
IN t) ==> ~(a
IN s)`)) THEN
MATCH_MP_TAC(SET_RULE
`~(a
IN s) /\ ~(a
IN t)
==> ~(a
IN ((s
INTER s'
INTER s'')
UNION t
UNION (u
DIFF {a,b})))`) THEN
MAP_EVERY (MP_TAC o ISPEC `
path_image c1 UNION path_image c2:real^2->bool`)
[
OUTSIDE_NO_OVERLAP;
INSIDE_NO_OVERLAP] THEN
REWRITE_TAC[IMP_IMP] THEN MATCH_MP_TAC MONO_AND THEN
ASM SET_TAC[];
ALL_TAC] THEN
SUBGOAL_THEN
`?u v. ~(u = {}) /\ open u /\
connected u /\
~(v = {}) /\ open v /\
connected v /\
u
INTER v = {} /\ u
UNION v = (:real^2)
DIFF path_image j /\
frontier u =
path_image j /\
frontier v =
path_image j /\
a
IN u`
STRIP_ASSUME_TAC THENL
[MP_TAC(ISPEC `j:real^1->real^2`
JORDAN_CURVE_THEOREM) THEN
ASM_REWRITE_TAC[
LEFT_IMP_EXISTS_THM] THEN
MAP_EVERY X_GEN_TAC [`u:real^2->bool`; `v:real^2->bool`] THEN
STRIP_TAC THEN
SUBGOAL_THEN `(a:real^2)
IN u \/ (a:real^2)
IN v` MP_TAC THENL
[ASM SET_TAC[]; ALL_TAC] THEN
STRIP_TAC THENL
[MAP_EVERY EXISTS_TAC [`u:real^2->bool`; `v:real^2->bool`];
MAP_EVERY EXISTS_TAC [`v:real^2->bool`; `u:real^2->bool`]] THEN
ASM_REWRITE_TAC[] THEN
ONCE_REWRITE_TAC[
INTER_COMM;
UNION_COMM] THEN ASM_REWRITE_TAC[];
ALL_TAC] THEN
SUBGOAL_THEN
`~(v
INTER inside(
path_image c1 UNION path_image c2) = {}) /\
~((v:real^2->bool)
INTER outside(
path_image c1 UNION path_image c2) = {})`
STRIP_ASSUME_TAC THENL
[CONJ_TAC THENL
[UNDISCH_TAC
`~((
path_image j:real^2->bool)
INTER
inside(
path_image c1 UNION path_image c2) = {})` THEN
REWRITE_TAC[GSYM
MEMBER_NOT_EMPTY;
IN_INTER] THEN
SUBST1_TAC(SYM(ASSUME `
frontier v:real^2->bool =
path_image j`)) THEN
DISCH_THEN(X_CHOOSE_THEN `p:real^2` MP_TAC) THEN
DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
REWRITE_TAC[
frontier;
IN_DIFF;
CLOSURE_APPROACHABLE] THEN
MP_TAC(GEN_REWRITE_RULE I [
OPEN_CONTAINS_BALL] (ASSUME
`open(
inside(
path_image c1 UNION path_image c2):real^2->bool)`)) THEN
DISCH_THEN(MP_TAC o SPEC `p:real^2`) THEN ONCE_REWRITE_TAC[
DIST_SYM] THEN
ASM_REWRITE_TAC[
SUBSET;
IN_BALL] THEN ASM_MESON_TAC[];
UNDISCH_TAC
`~((
path_image j:real^2->bool)
INTER
outside(
path_image c1 UNION path_image c2) = {})` THEN
REWRITE_TAC[GSYM
MEMBER_NOT_EMPTY;
IN_INTER] THEN
SUBST1_TAC(SYM(ASSUME `
frontier v:real^2->bool =
path_image j`)) THEN
DISCH_THEN(X_CHOOSE_THEN `p:real^2` MP_TAC) THEN
DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
REWRITE_TAC[
frontier;
IN_DIFF;
CLOSURE_APPROACHABLE] THEN
MP_TAC(GEN_REWRITE_RULE I [
OPEN_CONTAINS_BALL] (ASSUME
`open(
outside(
path_image c1 UNION path_image c2):real^2->bool)`)) THEN
DISCH_THEN(MP_TAC o SPEC `p:real^2`) THEN ONCE_REWRITE_TAC[
DIST_SYM] THEN
ASM_REWRITE_TAC[
SUBSET;
IN_BALL] THEN ASM_MESON_TAC[]];
ALL_TAC] THEN
SUBGOAL_THEN
`~((v:real^2->bool)
INTER (
path_image c1 UNION path_image c2) = {})`
MP_TAC THENL
[MP_TAC(ASSUME `
connected(v:real^2->bool)`) THEN
REWRITE_TAC[
connected; CONTRAPOS_THM] THEN DISCH_TAC THEN
MAP_EVERY EXISTS_TAC
[`
inside(
path_image c1 UNION path_image c2):real^2->bool`;
`
outside(
path_image c1 UNION path_image c2):real^2->bool`] THEN
ASM_REWRITE_TAC[] THEN ASM SET_TAC[];
GEN_REWRITE_TAC LAND_CONV [GSYM
MEMBER_NOT_EMPTY]] THEN
REWRITE_TAC[
IN_INTER;
IN_UNION] THEN
DISCH_THEN(X_CHOOSE_THEN `p:real^2` (CONJUNCTS_THEN ASSUME_TAC)) THEN
SUBGOAL_THEN `~(p:real^2 = a)` ASSUME_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
FIRST_X_ASSUM DISJ_CASES_TAC THENL
[SUBGOAL_THEN
`~((u:real^2->bool)
INTER inside(
path_image c1 UNION path_image c) = {})`
ASSUME_TAC THENL
[MP_TAC(ASSUME `open(u:real^2->bool)`) THEN
REWRITE_TAC[
OPEN_CONTAINS_BALL;
SUBSET;
IN_BALL] THEN
DISCH_THEN(MP_TAC o SPEC `a:real^2`) THEN ASM_REWRITE_TAC[] THEN
ONCE_REWRITE_TAC[
DIST_SYM] THEN
SUBGOAL_THEN
`(a:real^2)
IN frontier(
inside(
path_image c1 UNION path_image c))`
MP_TAC THENL [ASM SET_TAC[]; REWRITE_TAC[
frontier;
IN_DIFF]] THEN
REWRITE_TAC[
CLOSURE_APPROACHABLE; GSYM
MEMBER_NOT_EMPTY;
IN_INTER] THEN
MESON_TAC[];
ALL_TAC] THEN
SUBGOAL_THEN
`~((v:real^2->bool)
INTER inside(
path_image c1 UNION path_image c) = {})`
ASSUME_TAC THENL
[MP_TAC(ASSUME `open(v:real^2->bool)`) THEN
REWRITE_TAC[
OPEN_CONTAINS_BALL;
SUBSET;
IN_BALL] THEN
DISCH_THEN(MP_TAC o SPEC `p:real^2`) THEN ASM_REWRITE_TAC[] THEN
ONCE_REWRITE_TAC[
DIST_SYM] THEN
SUBGOAL_THEN
`(p:real^2)
IN frontier(
inside(
path_image c1 UNION path_image c))`
MP_TAC THENL [ASM SET_TAC[]; REWRITE_TAC[
frontier;
IN_DIFF]] THEN
REWRITE_TAC[
CLOSURE_APPROACHABLE; GSYM
MEMBER_NOT_EMPTY;
IN_INTER] THEN
MESON_TAC[];
ALL_TAC] THEN
MP_TAC(ASSUME
`
connected(
inside(
path_image c1 UNION path_image c):real^2->bool)`) THEN
REWRITE_TAC[
connected] THEN
MAP_EVERY EXISTS_TAC [`u:real^2->bool`; `v:real^2->bool`] THEN
ASM_REWRITE_TAC[GSYM
INTER_ASSOC;
INTER_EMPTY] THEN
FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (SET_RULE
`j
SUBSET t ==> s
INTER t = {} ==> s
SUBSET UNIV DIFF j`)) THEN
MATCH_MP_TAC(SET_RULE
`!x. s
INTER t2 = {} /\ u
SUBSET t2 /\
x
INTER v = {} /\ s
SUBSET x
==> s
INTER
(
t1 INTER t2
INTER t3
UNION u
UNION (v
DIFF w)) = {}`) THEN
EXISTS_TAC `
inside(
path_image c1 UNION path_image c2:real^2->bool)` THEN
ASM_REWRITE_TAC[
INSIDE_INTER_OUTSIDE;
INSIDE_NO_OVERLAP];
SUBGOAL_THEN
`~((u:real^2->bool)
INTER inside(
path_image c2
UNION path_image c) = {})`
ASSUME_TAC THENL
[MP_TAC(ASSUME `open(u:real^2->bool)`) THEN
REWRITE_TAC[
OPEN_CONTAINS_BALL;
SUBSET;
IN_BALL] THEN
DISCH_THEN(MP_TAC o SPEC `a:real^2`) THEN ASM_REWRITE_TAC[] THEN
ONCE_REWRITE_TAC[
DIST_SYM] THEN
SUBGOAL_THEN
`(a:real^2)
IN frontier(
inside(
path_image c2
UNION path_image c))`
MP_TAC THENL [ASM SET_TAC[]; REWRITE_TAC[
frontier;
IN_DIFF]] THEN
REWRITE_TAC[
CLOSURE_APPROACHABLE; GSYM
MEMBER_NOT_EMPTY;
IN_INTER] THEN
MESON_TAC[];
ALL_TAC] THEN
SUBGOAL_THEN
`~((v:real^2->bool)
INTER inside(
path_image c2
UNION path_image c) = {})`
ASSUME_TAC THENL
[MP_TAC(ASSUME `open(v:real^2->bool)`) THEN
REWRITE_TAC[
OPEN_CONTAINS_BALL;
SUBSET;
IN_BALL] THEN
DISCH_THEN(MP_TAC o SPEC `p:real^2`) THEN ASM_REWRITE_TAC[] THEN
ONCE_REWRITE_TAC[
DIST_SYM] THEN
SUBGOAL_THEN
`(p:real^2)
IN frontier(
inside(
path_image c2
UNION path_image c))`
MP_TAC THENL [ASM SET_TAC[]; REWRITE_TAC[
frontier;
IN_DIFF]] THEN
REWRITE_TAC[
CLOSURE_APPROACHABLE; GSYM
MEMBER_NOT_EMPTY;
IN_INTER] THEN
MESON_TAC[];
ALL_TAC] THEN
MP_TAC(ASSUME
`
connected(
inside(
path_image c2
UNION path_image c):real^2->bool)`) THEN
REWRITE_TAC[
connected] THEN
MAP_EVERY EXISTS_TAC [`u:real^2->bool`; `v:real^2->bool`] THEN
ASM_REWRITE_TAC[GSYM
INTER_ASSOC;
INTER_EMPTY] THEN
FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (SET_RULE
`j
SUBSET t ==> s
INTER t = {} ==> s
SUBSET UNIV DIFF j`)) THEN
MATCH_MP_TAC(SET_RULE
`!x. s
INTER t3 = {} /\ u
SUBSET t3 /\
x
INTER v = {} /\ s
SUBSET x
==> s
INTER
(
t1 INTER t2
INTER t3
UNION u
UNION (v
DIFF w)) = {}`) THEN
EXISTS_TAC `
inside(
path_image c1 UNION path_image c2:real^2->bool)` THEN
ASM_REWRITE_TAC[
INSIDE_INTER_OUTSIDE;
INSIDE_NO_OVERLAP]]);;