Jordan Curve Theorem
authorpaulson <lp15@cam.ac.uk>
Mon Jan 09 14:40:31 2017 +0000 (2017-01-09)
changeset 64846de4e3df6693d
parent 64845 e5d4bc2016a6
child 64847 54f5afc9c413
Jordan Curve Theorem
NEWS
src/HOL/Analysis/Analysis.thy
src/HOL/Analysis/Further_Topology.thy
src/HOL/Analysis/Jordan_Curve.thy
     1.1 --- a/NEWS	Mon Jan 09 14:00:13 2017 +0000
     1.2 +++ b/NEWS	Mon Jan 09 14:40:31 2017 +0000
     1.3 @@ -65,6 +65,9 @@
     1.4      with type class annotations. As a result, the tactic that derives
     1.5      it no longer fails on nested datatypes. Slight INCOMPATIBILITY.
     1.6  
     1.7 +* Session HOL-Analysis: more material involving arcs, paths, covering spaces,
     1.8 +innessential maps, retracts. Major results include the Jordan Curve Theorem.
     1.9 +
    1.10  * The theorem in Permutations has been renamed:
    1.11    bij_swap_ompose_bij ~> bij_swap_compose_bij
    1.12  
     2.1 --- a/src/HOL/Analysis/Analysis.thy	Mon Jan 09 14:00:13 2017 +0000
     2.2 +++ b/src/HOL/Analysis/Analysis.thy	Mon Jan 09 14:40:31 2017 +0000
     2.3 @@ -11,8 +11,7 @@
     2.4    Function_Topology
     2.5    Weierstrass_Theorems
     2.6    Polytope
     2.7 -  Further_Topology
     2.8 -  Arcwise_Connected
     2.9 +  Jordan_Curve
    2.10    Poly_Roots
    2.11    Conformal_Mappings
    2.12    Generalised_Binomial_Theorem
     3.1 --- a/src/HOL/Analysis/Further_Topology.thy	Mon Jan 09 14:00:13 2017 +0000
     3.2 +++ b/src/HOL/Analysis/Further_Topology.thy	Mon Jan 09 14:40:31 2017 +0000
     3.3 @@ -3543,7 +3543,7 @@
     3.4    fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
     3.5    assumes hom: "homotopic_with (\<lambda>x. True) S (sphere 0 1) f g" and conth: "continuous_on S h"
     3.6        and hin: "\<And>x. x \<in> S \<Longrightarrow> h x \<in> sphere 0 1"
     3.7 -    shows "homotopic_with (\<lambda>x. True) S (sphere 0 1) (\<lambda>x. f x*h x) (\<lambda>x. g x*h x)"
     3.8 +    shows "homotopic_with (\<lambda>x. True) S (sphere 0 1) (\<lambda>x. f x * h x) (\<lambda>x. g x * h x)"
     3.9  proof -
    3.10    obtain k where contk: "continuous_on ({0..1::real} \<times> S) k"
    3.11               and kim: "k ` ({0..1} \<times> S) \<subseteq> sphere 0 1"
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Analysis/Jordan_Curve.thy	Mon Jan 09 14:40:31 2017 +0000
     4.3 @@ -0,0 +1,673 @@
     4.4 +(*  Title:      HOL/Analysis/Jordan_Curve.thy
     4.5 +    Authors:    LC Paulson, based on material from HOL Light
     4.6 +*)
     4.7 +
     4.8 +section \<open>The Jordan Curve Theorem and Applications\<close>
     4.9 +
    4.10 +theory Jordan_Curve
    4.11 +  imports Arcwise_Connected Further_Topology
    4.12 +
    4.13 +begin
    4.14 +
    4.15 +subsection\<open>Janiszewski's theorem.\<close>
    4.16 +
    4.17 +lemma Janiszewski_weak:
    4.18 +  fixes a b::complex
    4.19 +  assumes "compact S" "compact T" and conST: "connected(S \<inter> T)"
    4.20 +      and ccS: "connected_component (- S) a b" and ccT: "connected_component (- T) a b"
    4.21 +    shows "connected_component (- (S \<union> T)) a b"
    4.22 +proof -
    4.23 +  have [simp]: "a \<notin> S" "a \<notin> T" "b \<notin> S" "b \<notin> T"
    4.24 +    by (meson ComplD ccS ccT connected_component_in)+
    4.25 +  have clo: "closedin (subtopology euclidean (S \<union> T)) S" "closedin (subtopology euclidean (S \<union> T)) T"
    4.26 +    by (simp_all add: assms closed_subset compact_imp_closed)
    4.27 +  obtain g where contg: "continuous_on S g"
    4.28 +             and g: "\<And>x. x \<in> S \<Longrightarrow> exp (\<i>* of_real (g x)) = (x - a) /\<^sub>R cmod (x - a) / ((x - b) /\<^sub>R cmod (x - b))"
    4.29 +    using ccS \<open>compact S\<close>
    4.30 +    apply (simp add: Borsuk_maps_homotopic_in_connected_component_eq [symmetric])
    4.31 +    apply (subst (asm) homotopic_circlemaps_divide)
    4.32 +    apply (auto simp: inessential_eq_continuous_logarithm_circle)
    4.33 +    done
    4.34 +  obtain h where conth: "continuous_on T h"
    4.35 +             and h: "\<And>x. x \<in> T \<Longrightarrow> exp (\<i>* of_real (h x)) = (x - a) /\<^sub>R cmod (x - a) / ((x - b) /\<^sub>R cmod (x - b))"
    4.36 +    using ccT \<open>compact T\<close>
    4.37 +    apply (simp add: Borsuk_maps_homotopic_in_connected_component_eq [symmetric])
    4.38 +    apply (subst (asm) homotopic_circlemaps_divide)
    4.39 +    apply (auto simp: inessential_eq_continuous_logarithm_circle)
    4.40 +    done
    4.41 +  have "continuous_on (S \<union> T) (\<lambda>x. (x - a) /\<^sub>R cmod (x - a))" "continuous_on (S \<union> T) (\<lambda>x. (x - b) /\<^sub>R cmod (x - b))"
    4.42 +    by (intro continuous_intros; force)+
    4.43 +  moreover have "(\<lambda>x. (x - a) /\<^sub>R cmod (x - a)) ` (S \<union> T) \<subseteq> sphere 0 1" "(\<lambda>x. (x - b) /\<^sub>R cmod (x - b)) ` (S \<union> T) \<subseteq> sphere 0 1"
    4.44 +    by (auto simp: divide_simps)
    4.45 +  moreover have "\<exists>g. continuous_on (S \<union> T) g \<and>
    4.46 +                     (\<forall>x\<in>S \<union> T. (x - a) /\<^sub>R cmod (x - a) / ((x - b) /\<^sub>R cmod (x - b)) = exp (\<i>*complex_of_real (g x)))"
    4.47 +  proof (cases "S \<inter> T = {}")
    4.48 +    case True
    4.49 +    have "continuous_on (S \<union> T) (\<lambda>x. if x \<in> S then g x else h x)"
    4.50 +      apply (rule continuous_on_cases_local [OF clo contg conth])
    4.51 +      using True by auto
    4.52 +    then show ?thesis
    4.53 +      by (rule_tac x="(\<lambda>x. if x \<in> S then g x else h x)" in exI) (auto simp: g h)
    4.54 +  next
    4.55 +    case False
    4.56 +    have diffpi: "\<exists>n. g x = h x + 2* of_int n*pi" if "x \<in> S \<inter> T" for x
    4.57 +    proof -
    4.58 +      have "exp (\<i>* of_real (g x)) = exp (\<i>* of_real (h x))"
    4.59 +        using that by (simp add: g h)
    4.60 +      then obtain n where "complex_of_real (g x) = complex_of_real (h x) + 2* of_int n*complex_of_real pi"
    4.61 +        apply (auto simp: exp_eq)
    4.62 +        by (metis complex_i_not_zero distrib_left mult.commute mult_cancel_left)
    4.63 +      then show ?thesis
    4.64 +        apply (rule_tac x=n in exI)
    4.65 +        using of_real_eq_iff by fastforce
    4.66 +    qed
    4.67 +    have contgh: "continuous_on (S \<inter> T) (\<lambda>x. g x - h x)"
    4.68 +      by (intro continuous_intros continuous_on_subset [OF contg] continuous_on_subset [OF conth]) auto
    4.69 +    moreover have disc:
    4.70 +          "\<exists>e>0. \<forall>y. y \<in> S \<inter> T \<and> g y - h y \<noteq> g x - h x \<longrightarrow> e \<le> norm ((g y - h y) - (g x - h x))"
    4.71 +          if "x \<in> S \<inter> T" for x
    4.72 +    proof -
    4.73 +      obtain nx where nx: "g x = h x + 2* of_int nx*pi"
    4.74 +        using \<open>x \<in> S \<inter> T\<close> diffpi by blast
    4.75 +      have "2*pi \<le> norm (g y - h y - (g x - h x))" if y: "y \<in> S \<inter> T" and neq: "g y - h y \<noteq> g x - h x" for y
    4.76 +      proof -
    4.77 +        obtain ny where ny: "g y = h y + 2* of_int ny*pi"
    4.78 +          using \<open>y \<in> S \<inter> T\<close> diffpi by blast
    4.79 +        { assume "nx \<noteq> ny"
    4.80 +          then have "1 \<le> \<bar>real_of_int ny - real_of_int nx\<bar>"
    4.81 +            by linarith
    4.82 +          then have "(2*pi)*1 \<le> (2*pi)*\<bar>real_of_int ny - real_of_int nx\<bar>"
    4.83 +            by simp
    4.84 +          also have "... = \<bar>2*real_of_int ny*pi - 2*real_of_int nx*pi\<bar>"
    4.85 +            by (simp add: algebra_simps abs_if)
    4.86 +          finally have "2*pi \<le> \<bar>2*real_of_int ny*pi - 2*real_of_int nx*pi\<bar>" by simp
    4.87 +        }
    4.88 +        with neq show ?thesis
    4.89 +          by (simp add: nx ny)
    4.90 +      qed
    4.91 +      then show ?thesis
    4.92 +        by (rule_tac x="2*pi" in exI) auto
    4.93 +    qed
    4.94 +    ultimately obtain z where z: "\<And>x. x \<in> S \<inter> T \<Longrightarrow> g x - h x = z"
    4.95 +      using continuous_discrete_range_constant [OF conST contgh] by blast
    4.96 +    obtain w where "exp(ii* of_real(h w)) = exp (ii* of_real(z + h w))"
    4.97 +      using disc z False
    4.98 +      by auto (metis diff_add_cancel g h of_real_add)
    4.99 +    then have [simp]: "exp (\<i>* of_real z) = 1"
   4.100 +      by (metis cis_conv_exp cis_mult exp_not_eq_zero mult_cancel_right1)
   4.101 +    show ?thesis
   4.102 +    proof (intro exI conjI)
   4.103 +      show "continuous_on (S \<union> T) (\<lambda>x. if x \<in> S then g x else z + h x)"
   4.104 +        apply (intro continuous_intros continuous_on_cases_local [OF clo contg] conth)
   4.105 +        using z by fastforce
   4.106 +    qed (auto simp: g h algebra_simps exp_add)
   4.107 +  qed
   4.108 +  ultimately have *: "homotopic_with (\<lambda>x. True) (S \<union> T) (sphere 0 1)
   4.109 +                          (\<lambda>x. (x - a) /\<^sub>R cmod (x - a))  (\<lambda>x. (x - b) /\<^sub>R cmod (x - b))"
   4.110 +    by (subst homotopic_circlemaps_divide) (auto simp: inessential_eq_continuous_logarithm_circle)
   4.111 +  show ?thesis
   4.112 +    apply (rule Borsuk_maps_homotopic_in_connected_component_eq [THEN iffD1])
   4.113 +    using assms by (auto simp: *)
   4.114 +qed
   4.115 +
   4.116 +
   4.117 +theorem Janiszewski:
   4.118 +  fixes a b::complex
   4.119 +  assumes "compact S" "closed T" and conST: "connected(S \<inter> T)"
   4.120 +      and ccS: "connected_component (- S) a b" and ccT: "connected_component (- T) a b"
   4.121 +    shows "connected_component (- (S \<union> T)) a b"
   4.122 +proof -
   4.123 +  have "path_component(- T) a b"
   4.124 +    by (simp add: \<open>closed T\<close> ccT open_Compl open_path_connected_component)
   4.125 +  then obtain g where g: "path g" "path_image g \<subseteq> - T" "pathstart g = a" "pathfinish g = b"
   4.126 +    by (auto simp: path_component_def)
   4.127 +  obtain C where C: "compact C" "connected C" "a \<in> C" "b \<in> C" "C \<inter> T = {}"
   4.128 +  proof
   4.129 +    show "compact (path_image g)"
   4.130 +      by (simp add: \<open>path g\<close> compact_path_image)
   4.131 +    show "connected (path_image g)"
   4.132 +      by (simp add: \<open>path g\<close> connected_path_image)
   4.133 +  qed (use g in auto)
   4.134 +  obtain r where "0 < r" and r: "C \<union> S \<subseteq> ball 0 r"
   4.135 +    by (metis \<open>compact C\<close> \<open>compact S\<close> bounded_Un compact_imp_bounded bounded_subset_ballD)
   4.136 +  have "connected_component (- (S \<union> (T \<inter> cball 0 r \<union> sphere 0 r))) a b"
   4.137 +  proof (rule Janiszewski_weak [OF \<open>compact S\<close>])
   4.138 +    show comT': "compact ((T \<inter> cball 0 r) \<union> sphere 0 r)"
   4.139 +      by (simp add: \<open>closed T\<close> closed_Int_compact compact_Un)
   4.140 +    have "S \<inter> (T \<inter> cball 0 r \<union> sphere 0 r) = S \<inter> T"
   4.141 +      using r by auto
   4.142 +    with conST show "connected (S \<inter> (T \<inter> cball 0 r \<union> sphere 0 r))"
   4.143 +      by simp
   4.144 +    show "connected_component (- (T \<inter> cball 0 r \<union> sphere 0 r)) a b"
   4.145 +      using conST C r
   4.146 +      apply (simp add: connected_component_def)
   4.147 +      apply (rule_tac x=C in exI)
   4.148 +      by auto
   4.149 +  qed (simp add: ccS)
   4.150 +  then obtain U where U: "connected U" "U \<subseteq> - S" "U \<subseteq> - T \<union> - cball 0 r" "U \<subseteq> - sphere 0 r" "a \<in> U" "b \<in> U"
   4.151 +    by (auto simp: connected_component_def)
   4.152 +  show ?thesis
   4.153 +    unfolding connected_component_def
   4.154 +  proof (intro exI conjI)
   4.155 +    show "U \<subseteq> - (S \<union> T)"
   4.156 +      using U r \<open>0 < r\<close> \<open>a \<in> C\<close> connected_Int_frontier [of U "cball 0 r"]
   4.157 +      apply simp
   4.158 +      by (metis ball_subset_cball compl_inf disjoint_eq_subset_Compl disjoint_iff_not_equal inf.orderE inf_sup_aci(3) subsetCE)
   4.159 +  qed (auto simp: U)
   4.160 +qed
   4.161 +
   4.162 +lemma Janiszewski_connected:
   4.163 +  fixes S :: "complex set"
   4.164 +  assumes ST: "compact S" "closed T" "connected(S \<inter> T)"
   4.165 +      and notST: "connected (- S)" "connected (- T)"
   4.166 +    shows "connected(- (S \<union> T))"
   4.167 +using Janiszewski [OF ST]
   4.168 +by (metis IntD1 IntD2 notST compl_sup connected_iff_connected_component)
   4.169 +
   4.170 +subsection\<open>The Jordan Curve theorem\<close>
   4.171 +
   4.172 +lemma exists_double_arc:
   4.173 +  fixes g :: "real \<Rightarrow> 'a::real_normed_vector"
   4.174 +  assumes "simple_path g" "pathfinish g = pathstart g" "a \<in> path_image g" "b \<in> path_image g" "a \<noteq> b"
   4.175 +  obtains u d where "arc u" "arc d" "pathstart u = a" "pathfinish u = b"
   4.176 +                    "pathstart d = b" "pathfinish d = a"
   4.177 +                    "(path_image u) \<inter> (path_image d) = {a,b}"
   4.178 +                    "(path_image u) \<union> (path_image d) = path_image g"
   4.179 +proof -
   4.180 +  obtain u where u: "0 \<le> u" "u \<le> 1" "g u = a"
   4.181 +    using assms by (auto simp: path_image_def)
   4.182 +  define h where "h \<equiv> shiftpath u g"
   4.183 +  have "simple_path h"
   4.184 +    using \<open>simple_path g\<close> simple_path_shiftpath \<open>0 \<le> u\<close> \<open>u \<le> 1\<close> assms(2) h_def by blast
   4.185 +  have "pathstart h = g u"
   4.186 +    by (simp add: \<open>u \<le> 1\<close> h_def pathstart_shiftpath)
   4.187 +  have "pathfinish h = g u"
   4.188 +    by (simp add: \<open>0 \<le> u\<close> assms h_def pathfinish_shiftpath)
   4.189 +  have pihg: "path_image h = path_image g"
   4.190 +    by (simp add: \<open>0 \<le> u\<close> \<open>u \<le> 1\<close> assms h_def path_image_shiftpath)
   4.191 +  then obtain v where v: "0 \<le> v" "v \<le> 1" "h v = b"
   4.192 +    using assms by (metis (mono_tags, lifting) atLeastAtMost_iff imageE path_image_def)
   4.193 +  show ?thesis
   4.194 +  proof
   4.195 +    show "arc (subpath 0 v h)"
   4.196 +      by (metis (no_types) \<open>pathstart h = g u\<close> \<open>simple_path h\<close> arc_simple_path_subpath \<open>a \<noteq> b\<close> atLeastAtMost_iff zero_le_one order_refl pathstart_def u(3) v)
   4.197 +    show "arc (subpath v 1 h)"
   4.198 +      by (metis (no_types) \<open>pathfinish h = g u\<close> \<open>simple_path h\<close> arc_simple_path_subpath \<open>a \<noteq> b\<close> atLeastAtMost_iff zero_le_one order_refl pathfinish_def u(3) v)
   4.199 +    show "pathstart (subpath 0 v h) = a"
   4.200 +      by (metis \<open>pathstart h = g u\<close> pathstart_def pathstart_subpath u(3))
   4.201 +    show "pathfinish (subpath 0 v h) = b"  "pathstart (subpath v 1 h) = b"
   4.202 +      by (simp_all add: v(3))
   4.203 +    show "pathfinish (subpath v 1 h) = a"
   4.204 +      by (metis \<open>pathfinish h = g u\<close> pathfinish_def pathfinish_subpath u(3))
   4.205 +    show "path_image (subpath 0 v h) \<inter> path_image (subpath v 1 h) = {a, b}"
   4.206 +    proof
   4.207 +      show "path_image (subpath 0 v h) \<inter> path_image (subpath v 1 h) \<subseteq> {a, b}"
   4.208 +        using v  \<open>pathfinish (subpath v 1 h) = a\<close> \<open>simple_path h\<close>
   4.209 +          apply (auto simp: simple_path_def path_image_subpath image_iff Ball_def)
   4.210 +        by (metis (full_types) less_eq_real_def less_irrefl less_le_trans)
   4.211 +      show "{a, b} \<subseteq> path_image (subpath 0 v h) \<inter> path_image (subpath v 1 h)"
   4.212 +        using v \<open>pathstart (subpath 0 v h) = a\<close> \<open>pathfinish (subpath v 1 h) = a\<close>
   4.213 +        apply (auto simp: path_image_subpath image_iff)
   4.214 +        by (metis atLeastAtMost_iff order_refl)
   4.215 +    qed
   4.216 +    show "path_image (subpath 0 v h) \<union> path_image (subpath v 1 h) = path_image g"
   4.217 +      using v apply (simp add: path_image_subpath pihg [symmetric])
   4.218 +      using path_image_def by fastforce
   4.219 +  qed
   4.220 +qed
   4.221 +
   4.222 +
   4.223 +theorem Jordan_curve:
   4.224 +  fixes c :: "real \<Rightarrow> complex"
   4.225 +  assumes "simple_path c" and loop: "pathfinish c = pathstart c"
   4.226 +  obtains inner outer where
   4.227 +                "inner \<noteq> {}" "open inner" "connected inner"
   4.228 +                "outer \<noteq> {}" "open outer" "connected outer"
   4.229 +                "bounded inner" "\<not> bounded outer" "inner \<inter> outer = {}"
   4.230 +                "inner \<union> outer = - path_image c"
   4.231 +                "frontier inner = path_image c"
   4.232 +                "frontier outer = path_image c"
   4.233 +proof -
   4.234 +  have "path c"
   4.235 +    by (simp add: assms simple_path_imp_path)
   4.236 +  have hom: "(path_image c) homeomorphic (sphere(0::complex) 1)"
   4.237 +    by (simp add: assms homeomorphic_simple_path_image_circle)
   4.238 +  with Jordan_Brouwer_separation have "\<not> connected (- (path_image c))"
   4.239 +    by fastforce
   4.240 +  then obtain inner where inner: "inner \<in> components (- path_image c)" and "bounded inner"
   4.241 +    using cobounded_has_bounded_component [of "- (path_image c)"]
   4.242 +    using \<open>\<not> connected (- path_image c)\<close> \<open>simple_path c\<close> bounded_simple_path_image by force
   4.243 +  obtain outer where outer: "outer \<in> components (- path_image c)" and "\<not> bounded outer"
   4.244 +    using cobounded_unbounded_components [of "- (path_image c)"]
   4.245 +    using \<open>path c\<close> bounded_path_image by auto
   4.246 +  show ?thesis
   4.247 +  proof
   4.248 +    show "inner \<noteq> {}"
   4.249 +      using inner in_components_nonempty by auto
   4.250 +    show "open inner"
   4.251 +      by (meson \<open>simple_path c\<close> compact_imp_closed compact_simple_path_image inner open_Compl open_components)
   4.252 +    show "connected inner"
   4.253 +      using in_components_connected inner by blast
   4.254 +    show "outer \<noteq> {}"
   4.255 +      using outer in_components_nonempty by auto
   4.256 +    show "open outer"
   4.257 +      by (meson \<open>simple_path c\<close> compact_imp_closed compact_simple_path_image outer open_Compl open_components)
   4.258 +    show "connected outer"
   4.259 +      using in_components_connected outer by blast
   4.260 +    show "inner \<inter> outer = {}"
   4.261 +      by (meson \<open>\<not> bounded outer\<close> \<open>bounded inner\<close> \<open>connected outer\<close> bounded_subset components_maximal in_components_subset inner outer)
   4.262 +    show fro_inner: "frontier inner = path_image c"
   4.263 +      by (simp add: Jordan_Brouwer_frontier [OF hom inner])
   4.264 +    show fro_outer: "frontier outer = path_image c"
   4.265 +      by (simp add: Jordan_Brouwer_frontier [OF hom outer])
   4.266 +    have False if m: "middle \<in> components (- path_image c)" and "middle \<noteq> inner" "middle \<noteq> outer" for middle
   4.267 +    proof -
   4.268 +      have "frontier middle = path_image c"
   4.269 +        by (simp add: Jordan_Brouwer_frontier [OF hom] that)
   4.270 +      have middle: "open middle" "connected middle" "middle \<noteq> {}"
   4.271 +        apply (meson \<open>simple_path c\<close> compact_imp_closed compact_simple_path_image m open_Compl open_components)
   4.272 +        using in_components_connected in_components_nonempty m by blast+
   4.273 +      obtain a0 b0 where "a0 \<in> path_image c" "b0 \<in> path_image c" "a0 \<noteq> b0"
   4.274 +        using simple_path_image_uncountable [OF \<open>simple_path c\<close>]
   4.275 +        by (metis Diff_cancel countable_Diff_eq countable_empty insert_iff subsetI subset_singleton_iff)
   4.276 +      obtain a b g where ab: "a \<in> path_image c" "b \<in> path_image c" "a \<noteq> b"
   4.277 +                     and "arc g" "pathstart g = a" "pathfinish g = b"
   4.278 +                     and pag_sub: "path_image g - {a,b} \<subseteq> middle"
   4.279 +      proof (rule dense_accessible_frontier_point_pairs [OF \<open>open middle\<close> \<open>connected middle\<close>, of "path_image c \<inter> ball a0 (dist a0 b0)" "path_image c \<inter> ball b0 (dist a0 b0)"])
   4.280 +        show "openin (subtopology euclidean (frontier middle)) (path_image c \<inter> ball a0 (dist a0 b0))"
   4.281 +             "openin (subtopology euclidean (frontier middle)) (path_image c \<inter> ball b0 (dist a0 b0))"
   4.282 +          by (simp_all add: \<open>frontier middle = path_image c\<close> openin_open_Int)
   4.283 +        show "path_image c \<inter> ball a0 (dist a0 b0) \<noteq> path_image c \<inter> ball b0 (dist a0 b0)"
   4.284 +          using \<open>a0 \<noteq> b0\<close> \<open>b0 \<in> path_image c\<close> by auto
   4.285 +        show "path_image c \<inter> ball a0 (dist a0 b0) \<noteq> {}"
   4.286 +          using \<open>a0 \<in> path_image c\<close> \<open>a0 \<noteq> b0\<close> by auto
   4.287 +        show "path_image c \<inter> ball b0 (dist a0 b0) \<noteq> {}"
   4.288 +          using \<open>b0 \<in> path_image c\<close> \<open>a0 \<noteq> b0\<close> by auto
   4.289 +      qed (use arc_distinct_ends arc_imp_simple_path simple_path_endless that in fastforce)
   4.290 +      obtain u d where "arc u" "arc d"
   4.291 +                   and "pathstart u = a" "pathfinish u = b" "pathstart d = b" "pathfinish d = a"
   4.292 +                   and ud_ab: "(path_image u) \<inter> (path_image d) = {a,b}"
   4.293 +                   and ud_Un: "(path_image u) \<union> (path_image d) = path_image c"
   4.294 +        using exists_double_arc [OF assms ab] by blast
   4.295 +      obtain x y where "x \<in> inner" "y \<in> outer"
   4.296 +        using \<open>inner \<noteq> {}\<close> \<open>outer \<noteq> {}\<close> by auto
   4.297 +      have "inner \<inter> middle = {}" "middle \<inter> outer = {}"
   4.298 +        using components_nonoverlap inner outer m that by blast+
   4.299 +      have "connected_component (- (path_image u \<union> path_image g \<union> (path_image d \<union> path_image g))) x y"
   4.300 +      proof (rule Janiszewski)
   4.301 +        show "compact (path_image u \<union> path_image g)"
   4.302 +          by (simp add: \<open>arc g\<close> \<open>arc u\<close> compact_Un compact_arc_image)
   4.303 +        show "closed (path_image d \<union> path_image g)"
   4.304 +          by (simp add: \<open>arc d\<close> \<open>arc g\<close> closed_Un closed_arc_image)
   4.305 +        show "connected ((path_image u \<union> path_image g) \<inter> (path_image d \<union> path_image g))"
   4.306 +          by (metis Un_Diff_cancel \<open>arc g\<close> \<open>path_image u \<inter> path_image d = {a, b}\<close> \<open>pathfinish g = b\<close> \<open>pathstart g = a\<close> connected_arc_image insert_Diff1 pathfinish_in_path_image pathstart_in_path_image sup_bot.right_neutral sup_commute sup_inf_distrib1)
   4.307 +        show "connected_component (- (path_image u \<union> path_image g)) x y"
   4.308 +          unfolding connected_component_def
   4.309 +        proof (intro exI conjI)
   4.310 +          have "connected ((inner \<union> (path_image c - path_image u)) \<union> (outer \<union> (path_image c - path_image u)))"
   4.311 +          proof (rule connected_Un)
   4.312 +            show "connected (inner \<union> (path_image c - path_image u))"
   4.313 +              apply (rule connected_intermediate_closure [OF \<open>connected inner\<close>])
   4.314 +              using fro_inner [symmetric]  apply (auto simp: closure_subset frontier_def)
   4.315 +              done
   4.316 +            show "connected (outer \<union> (path_image c - path_image u))"
   4.317 +              apply (rule connected_intermediate_closure [OF \<open>connected outer\<close>])
   4.318 +              using fro_outer [symmetric]  apply (auto simp: closure_subset frontier_def)
   4.319 +              done
   4.320 +            have "(inner \<inter> outer) \<union> (path_image c - path_image u) \<noteq> {}"
   4.321 +              by (metis \<open>arc d\<close>  ud_ab Diff_Int Diff_cancel Un_Diff \<open>inner \<inter> outer = {}\<close> \<open>pathfinish d = a\<close> \<open>pathstart d = b\<close> arc_simple_path insert_commute nonempty_simple_path_endless sup_bot_left ud_Un)
   4.322 +            then show "(inner \<union> (path_image c - path_image u)) \<inter> (outer \<union> (path_image c - path_image u)) \<noteq> {}"
   4.323 +              by auto
   4.324 +          qed
   4.325 +          then show "connected (inner \<union> outer \<union> (path_image c - path_image u))"
   4.326 +            by (metis sup.right_idem sup_assoc sup_commute)
   4.327 +          have "inner \<subseteq> - path_image u" "outer \<subseteq> - path_image u"
   4.328 +            using in_components_subset inner outer ud_Un by auto
   4.329 +          moreover have "inner \<subseteq> - path_image g" "outer \<subseteq> - path_image g"
   4.330 +            using \<open>inner \<inter> middle = {}\<close> \<open>inner \<subseteq> - path_image u\<close>
   4.331 +            using \<open>middle \<inter> outer = {}\<close> \<open>outer \<subseteq> - path_image u\<close> pag_sub ud_ab by fastforce+
   4.332 +          moreover have "path_image c - path_image u \<subseteq> - path_image g"
   4.333 +            using in_components_subset m pag_sub ud_ab by fastforce
   4.334 +          ultimately show "inner \<union> outer \<union> (path_image c - path_image u) \<subseteq> - (path_image u \<union> path_image g)"
   4.335 +            by force
   4.336 +          show "x \<in> inner \<union> outer \<union> (path_image c - path_image u)"
   4.337 +            by (auto simp: \<open>x \<in> inner\<close>)
   4.338 +          show "y \<in> inner \<union> outer \<union> (path_image c - path_image u)"
   4.339 +            by (auto simp: \<open>y \<in> outer\<close>)
   4.340 +        qed
   4.341 +        show "connected_component (- (path_image d \<union> path_image g)) x y"
   4.342 +          unfolding connected_component_def
   4.343 +        proof (intro exI conjI)
   4.344 +          have "connected ((inner \<union> (path_image c - path_image d)) \<union> (outer \<union> (path_image c - path_image d)))"
   4.345 +          proof (rule connected_Un)
   4.346 +            show "connected (inner \<union> (path_image c - path_image d))"
   4.347 +              apply (rule connected_intermediate_closure [OF \<open>connected inner\<close>])
   4.348 +              using fro_inner [symmetric]  apply (auto simp: closure_subset frontier_def)
   4.349 +              done
   4.350 +            show "connected (outer \<union> (path_image c - path_image d))"
   4.351 +              apply (rule connected_intermediate_closure [OF \<open>connected outer\<close>])
   4.352 +              using fro_outer [symmetric]  apply (auto simp: closure_subset frontier_def)
   4.353 +              done
   4.354 +            have "(inner \<inter> outer) \<union> (path_image c - path_image d) \<noteq> {}"
   4.355 +              using \<open>arc u\<close> \<open>pathfinish u = b\<close> \<open>pathstart u = a\<close> arc_imp_simple_path nonempty_simple_path_endless ud_Un ud_ab by fastforce
   4.356 +            then show "(inner \<union> (path_image c - path_image d)) \<inter> (outer \<union> (path_image c - path_image d)) \<noteq> {}"
   4.357 +              by auto
   4.358 +          qed
   4.359 +          then show "connected (inner \<union> outer \<union> (path_image c - path_image d))"
   4.360 +            by (metis sup.right_idem sup_assoc sup_commute)
   4.361 +          have "inner \<subseteq> - path_image d" "outer \<subseteq> - path_image d"
   4.362 +            using in_components_subset inner outer ud_Un by auto
   4.363 +          moreover have "inner \<subseteq> - path_image g" "outer \<subseteq> - path_image g"
   4.364 +            using \<open>inner \<inter> middle = {}\<close> \<open>inner \<subseteq> - path_image d\<close>
   4.365 +            using \<open>middle \<inter> outer = {}\<close> \<open>outer \<subseteq> - path_image d\<close> pag_sub ud_ab by fastforce+
   4.366 +          moreover have "path_image c - path_image d \<subseteq> - path_image g"
   4.367 +            using in_components_subset m pag_sub ud_ab by fastforce
   4.368 +          ultimately show "inner \<union> outer \<union> (path_image c - path_image d) \<subseteq> - (path_image d \<union> path_image g)"
   4.369 +            by force
   4.370 +          show "x \<in> inner \<union> outer \<union> (path_image c - path_image d)"
   4.371 +            by (auto simp: \<open>x \<in> inner\<close>)
   4.372 +          show "y \<in> inner \<union> outer \<union> (path_image c - path_image d)"
   4.373 +            by (auto simp: \<open>y \<in> outer\<close>)
   4.374 +        qed
   4.375 +      qed
   4.376 +      then have "connected_component (- (path_image u \<union> path_image d \<union> path_image g)) x y"
   4.377 +        by (simp add: Un_ac)
   4.378 +      moreover have "~(connected_component (- (path_image c)) x y)"
   4.379 +        by (metis (no_types, lifting) \<open>\<not> bounded outer\<close> \<open>bounded inner\<close> \<open>x \<in> inner\<close> \<open>y \<in> outer\<close> componentsE connected_component_eq inner mem_Collect_eq outer)
   4.380 +      ultimately show False
   4.381 +        by (auto simp: ud_Un [symmetric] connected_component_def)
   4.382 +    qed
   4.383 +    then have "components (- path_image c) = {inner,outer}"
   4.384 +      using inner outer by blast
   4.385 +    then have "Union (components (- path_image c)) = inner \<union> outer"
   4.386 +      by simp
   4.387 +    then show "inner \<union> outer = - path_image c"
   4.388 +      by auto
   4.389 +  qed (auto simp: \<open>bounded inner\<close> \<open>\<not> bounded outer\<close>)
   4.390 +qed
   4.391 +
   4.392 +
   4.393 +corollary Jordan_disconnected:
   4.394 +  fixes c :: "real \<Rightarrow> complex"
   4.395 +  assumes "simple_path c" "pathfinish c = pathstart c"
   4.396 +    shows "\<not> connected(- path_image c)"
   4.397 +using Jordan_curve [OF assms]
   4.398 +  by (metis Jordan_Brouwer_separation assms homeomorphic_simple_path_image_circle zero_less_one)
   4.399 +
   4.400 +
   4.401 +corollary Jordan_inside_outside:
   4.402 +  fixes c :: "real \<Rightarrow> complex"
   4.403 +  assumes "simple_path c" "pathfinish c = pathstart c"
   4.404 +    shows "inside(path_image c) \<noteq> {} \<and>
   4.405 +          open(inside(path_image c)) \<and>
   4.406 +          connected(inside(path_image c)) \<and>
   4.407 +          outside(path_image c) \<noteq> {} \<and>
   4.408 +          open(outside(path_image c)) \<and>
   4.409 +          connected(outside(path_image c)) \<and>
   4.410 +          bounded(inside(path_image c)) \<and>
   4.411 +          \<not> bounded(outside(path_image c)) \<and>
   4.412 +          inside(path_image c) \<inter> outside(path_image c) = {} \<and>
   4.413 +          inside(path_image c) \<union> outside(path_image c) =
   4.414 +          - path_image c \<and>
   4.415 +          frontier(inside(path_image c)) = path_image c \<and>
   4.416 +          frontier(outside(path_image c)) = path_image c"
   4.417 +proof -
   4.418 +  obtain inner outer
   4.419 +    where *: "inner \<noteq> {}" "open inner" "connected inner"
   4.420 +             "outer \<noteq> {}" "open outer" "connected outer"
   4.421 +             "bounded inner" "\<not> bounded outer" "inner \<inter> outer = {}"
   4.422 +             "inner \<union> outer = - path_image c"
   4.423 +             "frontier inner = path_image c"
   4.424 +             "frontier outer = path_image c"
   4.425 +    using Jordan_curve [OF assms] by blast
   4.426 +  then have inner: "inside(path_image c) = inner"
   4.427 +    by (metis dual_order.antisym inside_subset interior_eq interior_inside_frontier)
   4.428 +  have outer: "outside(path_image c) = outer"
   4.429 +    using \<open>inner \<union> outer = - path_image c\<close> \<open>inside (path_image c) = inner\<close>
   4.430 +          outside_inside \<open>inner \<inter> outer = {}\<close> by auto
   4.431 +  show ?thesis
   4.432 +    using * by (auto simp: inner outer)
   4.433 +qed
   4.434 +
   4.435 +subsubsection\<open>Triple-curve or "theta-curve" theorem\<close>
   4.436 +
   4.437 +text\<open>Proof that there is no fourth component taken from
   4.438 +     Kuratowski's Topology vol 2, para 61, II.\<close>
   4.439 +
   4.440 +theorem split_inside_simple_closed_curve:
   4.441 +  fixes c :: "real \<Rightarrow> complex"
   4.442 +  assumes "simple_path c1" and c1: "pathstart c1 = a" "pathfinish c1 = b"
   4.443 +      and "simple_path c2" and c2: "pathstart c2 = a" "pathfinish c2 = b"
   4.444 +      and "simple_path c"  and c: "pathstart c = a" "pathfinish c = b"
   4.445 +      and "a \<noteq> b"
   4.446 +      and c1c2: "path_image c1 \<inter> path_image c2 = {a,b}"
   4.447 +      and c1c: "path_image c1 \<inter> path_image c = {a,b}"
   4.448 +      and c2c: "path_image c2 \<inter> path_image c = {a,b}"
   4.449 +      and ne_12: "path_image c \<inter> inside(path_image c1 \<union> path_image c2) \<noteq> {}"
   4.450 +  obtains "inside(path_image c1 \<union> path_image c) \<inter> inside(path_image c2 \<union> path_image c) = {}"
   4.451 +          "inside(path_image c1 \<union> path_image c) \<union> inside(path_image c2 \<union> path_image c) \<union>
   4.452 +           (path_image c - {a,b}) = inside(path_image c1 \<union> path_image c2)"
   4.453 +proof -
   4.454 +  let ?\<Theta> = "path_image c"  let ?\<Theta>1 = "path_image c1"  let ?\<Theta>2 = "path_image c2"
   4.455 +  have sp: "simple_path (c1 +++ reversepath c2)" "simple_path (c1 +++ reversepath c)" "simple_path (c2 +++ reversepath c)"
   4.456 +    using assms by (auto simp: simple_path_join_loop_eq arc_simple_path simple_path_reversepath)
   4.457 +  then have op_in12: "open (inside (?\<Theta>1 \<union> ?\<Theta>2))"
   4.458 +     and op_out12: "open (outside (?\<Theta>1 \<union> ?\<Theta>2))"
   4.459 +     and op_in1c: "open (inside (?\<Theta>1 \<union> ?\<Theta>))"
   4.460 +     and op_in2c: "open (inside (?\<Theta>2 \<union> ?\<Theta>))"
   4.461 +     and op_out1c: "open (outside (?\<Theta>1 \<union> ?\<Theta>))"
   4.462 +     and op_out2c: "open (outside (?\<Theta>2 \<union> ?\<Theta>))"
   4.463 +     and co_in1c: "connected (inside (?\<Theta>1 \<union> ?\<Theta>))"
   4.464 +     and co_in2c: "connected (inside (?\<Theta>2 \<union> ?\<Theta>))"
   4.465 +     and co_out12c: "connected (outside (?\<Theta>1 \<union> ?\<Theta>2))"
   4.466 +     and co_out1c: "connected (outside (?\<Theta>1 \<union> ?\<Theta>))"
   4.467 +     and co_out2c: "connected (outside (?\<Theta>2 \<union> ?\<Theta>))"
   4.468 +     and pa_c: "?\<Theta> - {pathstart c, pathfinish c} \<subseteq> - ?\<Theta>1"
   4.469 +               "?\<Theta> - {pathstart c, pathfinish c} \<subseteq> - ?\<Theta>2"
   4.470 +     and pa_c1: "?\<Theta>1 - {pathstart c1, pathfinish c1} \<subseteq> - ?\<Theta>2"
   4.471 +                "?\<Theta>1 - {pathstart c1, pathfinish c1} \<subseteq> - ?\<Theta>"
   4.472 +     and pa_c2: "?\<Theta>2 - {pathstart c2, pathfinish c2} \<subseteq> - ?\<Theta>1"
   4.473 +                "?\<Theta>2 - {pathstart c2, pathfinish c2} \<subseteq> - ?\<Theta>"
   4.474 +     and co_c: "connected(?\<Theta> - {pathstart c,pathfinish c})"
   4.475 +     and co_c1: "connected(?\<Theta>1 - {pathstart c1,pathfinish c1})"
   4.476 +     and co_c2: "connected(?\<Theta>2 - {pathstart c2,pathfinish c2})"
   4.477 +     and fr_in: "frontier(inside(?\<Theta>1 \<union> ?\<Theta>2)) = ?\<Theta>1 \<union> ?\<Theta>2"
   4.478 +              "frontier(inside(?\<Theta>2 \<union> ?\<Theta>)) = ?\<Theta>2 \<union> ?\<Theta>"
   4.479 +              "frontier(inside(?\<Theta>1 \<union> ?\<Theta>)) = ?\<Theta>1 \<union> ?\<Theta>"
   4.480 +     and fr_out: "frontier(outside(?\<Theta>1 \<union> ?\<Theta>2)) = ?\<Theta>1 \<union> ?\<Theta>2"
   4.481 +              "frontier(outside(?\<Theta>2 \<union> ?\<Theta>)) = ?\<Theta>2 \<union> ?\<Theta>"
   4.482 +              "frontier(outside(?\<Theta>1 \<union> ?\<Theta>)) = ?\<Theta>1 \<union> ?\<Theta>"
   4.483 +    using Jordan_inside_outside [of "c1 +++ reversepath c2"]
   4.484 +    using Jordan_inside_outside [of "c1 +++ reversepath c"]
   4.485 +    using Jordan_inside_outside [of "c2 +++ reversepath c"] assms
   4.486 +              apply (simp_all add: path_image_join closed_Un closed_simple_path_image open_inside open_outside)
   4.487 +      apply (blast elim: | metis connected_simple_path_endless)+
   4.488 +    done
   4.489 +  have inout_12: "inside (?\<Theta>1 \<union> ?\<Theta>2) \<inter> (?\<Theta> - {pathstart c, pathfinish c}) \<noteq> {}"
   4.490 +    by (metis (no_types, lifting) c c1c ne_12 Diff_Int_distrib Diff_empty Int_empty_right Int_left_commute inf_sup_absorb inf_sup_aci(1) inside_no_overlap)
   4.491 +  have pi_disjoint:  "?\<Theta> \<inter> outside(?\<Theta>1 \<union> ?\<Theta>2) = {}"
   4.492 +  proof (rule ccontr)
   4.493 +    assume "?\<Theta> \<inter> outside (?\<Theta>1 \<union> ?\<Theta>2) \<noteq> {}"
   4.494 +    then show False
   4.495 +      using connectedD [OF co_c, of "inside(?\<Theta>1 \<union> ?\<Theta>2)" "outside(?\<Theta>1 \<union> ?\<Theta>2)"]
   4.496 +      using c c1c2 pa_c op_in12 op_out12 inout_12
   4.497 +      apply auto
   4.498 +      apply (metis Un_Diff_cancel2 Un_iff compl_sup disjoint_insert(1) inf_commute inf_compl_bot_left2 inside_Un_outside mk_disjoint_insert sup_inf_absorb)
   4.499 +      done
   4.500 +  qed
   4.501 +  have out_sub12: "outside(?\<Theta>1 \<union> ?\<Theta>2) \<subseteq> outside(?\<Theta>1 \<union> ?\<Theta>)" "outside(?\<Theta>1 \<union> ?\<Theta>2) \<subseteq> outside(?\<Theta>2 \<union> ?\<Theta>)"
   4.502 +    by (metis Un_commute pi_disjoint outside_Un_outside_Un)+
   4.503 +  have pa1_disj_in2: "?\<Theta>1 \<inter> inside (?\<Theta>2 \<union> ?\<Theta>) = {}"
   4.504 +  proof (rule ccontr)
   4.505 +    assume ne: "?\<Theta>1 \<inter> inside (?\<Theta>2 \<union> ?\<Theta>) \<noteq> {}"
   4.506 +    have 1: "inside (?\<Theta> \<union> ?\<Theta>2) \<inter> ?\<Theta> = {}"
   4.507 +      by (metis (no_types) Diff_Int_distrib Diff_cancel inf_sup_absorb inf_sup_aci(3) inside_no_overlap)
   4.508 +    have 2: "outside (?\<Theta> \<union> ?\<Theta>2) \<inter> ?\<Theta> = {}"
   4.509 +      by (metis (no_types) Int_empty_right Int_left_commute inf_sup_absorb outside_no_overlap)
   4.510 +    have "outside (?\<Theta>2 \<union> ?\<Theta>) \<subseteq> outside (?\<Theta>1 \<union> ?\<Theta>2)"
   4.511 +      apply (subst Un_commute, rule outside_Un_outside_Un)
   4.512 +      using connectedD [OF co_c1, of "inside(?\<Theta>2 \<union> ?\<Theta>)" "outside(?\<Theta>2 \<union> ?\<Theta>)"]
   4.513 +        pa_c1 op_in2c op_out2c ne c1 c2c 1 2 by (auto simp: inf_sup_aci)
   4.514 +    with out_sub12
   4.515 +    have "outside(?\<Theta>1 \<union> ?\<Theta>2) = outside(?\<Theta>2 \<union> ?\<Theta>)" by blast
   4.516 +    then have "frontier(outside(?\<Theta>1 \<union> ?\<Theta>2)) = frontier(outside(?\<Theta>2 \<union> ?\<Theta>))"
   4.517 +      by simp
   4.518 +    then show False
   4.519 +      using inout_12 pi_disjoint c c1c c2c fr_out by auto
   4.520 +  qed
   4.521 +  have pa2_disj_in1: "?\<Theta>2 \<inter> inside(?\<Theta>1 \<union> ?\<Theta>) = {}"
   4.522 +  proof (rule ccontr)
   4.523 +    assume ne: "?\<Theta>2 \<inter> inside (?\<Theta>1 \<union> ?\<Theta>) \<noteq> {}"
   4.524 +    have 1: "inside (?\<Theta> \<union> ?\<Theta>1) \<inter> ?\<Theta> = {}"
   4.525 +      by (metis (no_types) Diff_Int_distrib Diff_cancel inf_sup_absorb inf_sup_aci(3) inside_no_overlap)
   4.526 +    have 2: "outside (?\<Theta> \<union> ?\<Theta>1) \<inter> ?\<Theta> = {}"
   4.527 +      by (metis (no_types) Int_empty_right Int_left_commute inf_sup_absorb outside_no_overlap)
   4.528 +    have "outside (?\<Theta>1 \<union> ?\<Theta>) \<subseteq> outside (?\<Theta>1 \<union> ?\<Theta>2)"
   4.529 +      apply (rule outside_Un_outside_Un)
   4.530 +      using connectedD [OF co_c2, of "inside(?\<Theta>1 \<union> ?\<Theta>)" "outside(?\<Theta>1 \<union> ?\<Theta>)"]
   4.531 +        pa_c2 op_in1c op_out1c ne c2 c1c 1 2 by (auto simp: inf_sup_aci)
   4.532 +    with out_sub12
   4.533 +    have "outside(?\<Theta>1 \<union> ?\<Theta>2) = outside(?\<Theta>1 \<union> ?\<Theta>)"
   4.534 +      by blast
   4.535 +    then have "frontier(outside(?\<Theta>1 \<union> ?\<Theta>2)) = frontier(outside(?\<Theta>1 \<union> ?\<Theta>))"
   4.536 +      by simp
   4.537 +    then show False
   4.538 +      using inout_12 pi_disjoint c c1c c2c fr_out by auto
   4.539 +  qed
   4.540 +  have in_sub_in1: "inside(?\<Theta>1 \<union> ?\<Theta>) \<subseteq> inside(?\<Theta>1 \<union> ?\<Theta>2)"
   4.541 +    using pa2_disj_in1 out_sub12 by (auto simp: inside_outside)
   4.542 +  have in_sub_in2: "inside(?\<Theta>2 \<union> ?\<Theta>) \<subseteq> inside(?\<Theta>1 \<union> ?\<Theta>2)"
   4.543 +    using pa1_disj_in2 out_sub12 by (auto simp: inside_outside)
   4.544 +  have in_sub_out12: "inside(?\<Theta>1 \<union> ?\<Theta>) \<subseteq> outside(?\<Theta>2 \<union> ?\<Theta>)"
   4.545 +  proof
   4.546 +    fix x
   4.547 +    assume x: "x \<in> inside (?\<Theta>1 \<union> ?\<Theta>)"
   4.548 +    then have xnot: "x \<notin> ?\<Theta>"
   4.549 +      by (simp add: inside_def)
   4.550 +    obtain z where zim: "z \<in> ?\<Theta>1" and zout: "z \<in> outside(?\<Theta>2 \<union> ?\<Theta>)"
   4.551 +      apply (auto simp: outside_inside)
   4.552 +      using nonempty_simple_path_endless [OF \<open>simple_path c1\<close>]
   4.553 +      by (metis Diff_Diff_Int Diff_iff ex_in_conv c1 c1c c1c2 pa1_disj_in2)
   4.554 +    obtain e where "e > 0" and e: "ball z e \<subseteq> outside(?\<Theta>2 \<union> ?\<Theta>)"
   4.555 +      using zout op_out2c open_contains_ball_eq by blast
   4.556 +    have "z \<in> frontier (inside (?\<Theta>1 \<union> ?\<Theta>))"
   4.557 +      using zim by (auto simp: fr_in)
   4.558 +    then obtain w where w1: "w \<in> inside (?\<Theta>1 \<union> ?\<Theta>)" and dwz: "dist w z < e"
   4.559 +      using zim \<open>e > 0\<close> by (auto simp: frontier_def closure_approachable)
   4.560 +    then have w2: "w \<in> outside (?\<Theta>2 \<union> ?\<Theta>)"
   4.561 +      by (metis e dist_commute mem_ball subsetCE)
   4.562 +    then have "connected_component (- ?\<Theta>2 \<inter> - ?\<Theta>) z w"
   4.563 +      apply (simp add: connected_component_def)
   4.564 +      apply (rule_tac x = "outside(?\<Theta>2 \<union> ?\<Theta>)" in exI)
   4.565 +      using zout apply (auto simp: co_out2c)
   4.566 +       apply (simp_all add: outside_inside)
   4.567 +      done
   4.568 +    moreover have "connected_component (- ?\<Theta>2 \<inter> - ?\<Theta>) w x"
   4.569 +      unfolding connected_component_def
   4.570 +      using pa2_disj_in1 co_in1c x w1 union_with_outside by fastforce
   4.571 +    ultimately have eq: "connected_component_set (- ?\<Theta>2 \<inter> - ?\<Theta>) x =
   4.572 +                         connected_component_set (- ?\<Theta>2 \<inter> - ?\<Theta>) z"
   4.573 +      by (metis (mono_tags, lifting) connected_component_eq mem_Collect_eq)
   4.574 +    show "x \<in> outside (?\<Theta>2 \<union> ?\<Theta>)"
   4.575 +      using zout x pa2_disj_in1 by (auto simp: outside_def eq xnot)
   4.576 +  qed
   4.577 +  have in_sub_out21: "inside(?\<Theta>2 \<union> ?\<Theta>) \<subseteq> outside(?\<Theta>1 \<union> ?\<Theta>)"
   4.578 +  proof
   4.579 +    fix x
   4.580 +    assume x: "x \<in> inside (?\<Theta>2 \<union> ?\<Theta>)"
   4.581 +    then have xnot: "x \<notin> ?\<Theta>"
   4.582 +      by (simp add: inside_def)
   4.583 +    obtain z where zim: "z \<in> ?\<Theta>2" and zout: "z \<in> outside(?\<Theta>1 \<union> ?\<Theta>)"
   4.584 +      apply (auto simp: outside_inside)
   4.585 +      using nonempty_simple_path_endless [OF \<open>simple_path c2\<close>]
   4.586 +      by (metis (no_types, hide_lams) Diff_Diff_Int Diff_iff c1c2 c2 c2c ex_in_conv pa2_disj_in1)
   4.587 +    obtain e where "e > 0" and e: "ball z e \<subseteq> outside(?\<Theta>1 \<union> ?\<Theta>)"
   4.588 +      using zout op_out1c open_contains_ball_eq by blast
   4.589 +    have "z \<in> frontier (inside (?\<Theta>2 \<union> ?\<Theta>))"
   4.590 +      using zim by (auto simp: fr_in)
   4.591 +    then obtain w where w2: "w \<in> inside (?\<Theta>2 \<union> ?\<Theta>)" and dwz: "dist w z < e"
   4.592 +      using zim \<open>e > 0\<close> by (auto simp: frontier_def closure_approachable)
   4.593 +    then have w1: "w \<in> outside (?\<Theta>1 \<union> ?\<Theta>)"
   4.594 +      by (metis e dist_commute mem_ball subsetCE)
   4.595 +    then have "connected_component (- ?\<Theta>1 \<inter> - ?\<Theta>) z w"
   4.596 +      apply (simp add: connected_component_def)
   4.597 +      apply (rule_tac x = "outside(?\<Theta>1 \<union> ?\<Theta>)" in exI)
   4.598 +      using zout apply (auto simp: co_out1c)
   4.599 +       apply (simp_all add: outside_inside)
   4.600 +      done
   4.601 +    moreover have "connected_component (- ?\<Theta>1 \<inter> - ?\<Theta>) w x"
   4.602 +      unfolding connected_component_def
   4.603 +      using pa1_disj_in2 co_in2c x w2 union_with_outside by fastforce
   4.604 +    ultimately have eq: "connected_component_set (- ?\<Theta>1 \<inter> - ?\<Theta>) x =
   4.605 +                           connected_component_set (- ?\<Theta>1 \<inter> - ?\<Theta>) z"
   4.606 +      by (metis (no_types, lifting) connected_component_eq mem_Collect_eq)
   4.607 +    show "x \<in> outside (?\<Theta>1 \<union> ?\<Theta>)"
   4.608 +      using zout x pa1_disj_in2 by (auto simp: outside_def eq xnot)
   4.609 +  qed
   4.610 +  show ?thesis
   4.611 +  proof
   4.612 +    show "inside (?\<Theta>1 \<union> ?\<Theta>) \<inter> inside (?\<Theta>2 \<union> ?\<Theta>) = {}"
   4.613 +      by (metis Int_Un_distrib in_sub_out12 bot_eq_sup_iff disjoint_eq_subset_Compl outside_inside)
   4.614 +    have *: "outside (?\<Theta>1 \<union> ?\<Theta>) \<inter> outside (?\<Theta>2 \<union> ?\<Theta>) \<subseteq> outside (?\<Theta>1 \<union> ?\<Theta>2)"
   4.615 +    proof (rule components_maximal)
   4.616 +      show out_in: "outside (?\<Theta>1 \<union> ?\<Theta>2) \<in> components (- (?\<Theta>1 \<union> ?\<Theta>2))"
   4.617 +        apply (simp only: outside_in_components co_out12c)
   4.618 +        by (metis bounded_empty fr_out(1) frontier_empty unbounded_outside)
   4.619 +      have conn_U: "connected (- (closure (inside (?\<Theta>1 \<union> ?\<Theta>)) \<union> closure (inside (?\<Theta>2 \<union> ?\<Theta>))))"
   4.620 +      proof (rule Janiszewski_connected, simp_all)
   4.621 +        show "bounded (inside (?\<Theta>1 \<union> ?\<Theta>))"
   4.622 +          by (simp add: \<open>simple_path c1\<close> \<open>simple_path c\<close> bounded_inside bounded_simple_path_image)
   4.623 +        have if1: "- (inside (?\<Theta>1 \<union> ?\<Theta>) \<union> frontier (inside (?\<Theta>1 \<union> ?\<Theta>))) = - ?\<Theta>1 \<inter> - ?\<Theta> \<inter> - inside (?\<Theta>1 \<union> ?\<Theta>)"
   4.624 +          by (metis (no_types, lifting) Int_commute Jordan_inside_outside c c1 compl_sup path_image_join path_image_reversepath pathfinish_join pathfinish_reversepath pathstart_join pathstart_reversepath sp(2) closure_Un_frontier fr_out(3))
   4.625 +        then show "connected (- closure (inside (?\<Theta>1 \<union> ?\<Theta>)))"
   4.626 +          by (metis Compl_Un outside_inside co_out1c closure_Un_frontier)
   4.627 +        have if2: "- (inside (?\<Theta>2 \<union> ?\<Theta>) \<union> frontier (inside (?\<Theta>2 \<union> ?\<Theta>))) = - ?\<Theta>2 \<inter> - ?\<Theta> \<inter> - inside (?\<Theta>2 \<union> ?\<Theta>)"
   4.628 +          by (metis (no_types, lifting) Int_commute Jordan_inside_outside c c2 compl_sup path_image_join path_image_reversepath pathfinish_join pathfinish_reversepath pathstart_join pathstart_reversepath sp closure_Un_frontier fr_out(2))
   4.629 +        then show "connected (- closure (inside (?\<Theta>2 \<union> ?\<Theta>)))"
   4.630 +          by (metis Compl_Un outside_inside co_out2c closure_Un_frontier)
   4.631 +        have "connected(?\<Theta>)"
   4.632 +          by (metis \<open>simple_path c\<close> connected_simple_path_image)
   4.633 +        moreover
   4.634 +        have "closure (inside (?\<Theta>1 \<union> ?\<Theta>)) \<inter> closure (inside (?\<Theta>2 \<union> ?\<Theta>)) = ?\<Theta>"
   4.635 +          (is "?lhs = ?rhs")
   4.636 +        proof
   4.637 +          show "?lhs \<subseteq> ?rhs"
   4.638 +          proof clarify
   4.639 +            fix x
   4.640 +            assume x: "x \<in> closure (inside (?\<Theta>1 \<union> ?\<Theta>))" "x \<in> closure (inside (?\<Theta>2 \<union> ?\<Theta>))"
   4.641 +            then have "x \<notin> inside (?\<Theta>1 \<union> ?\<Theta>)"
   4.642 +              by (meson closure_iff_nhds_not_empty in_sub_out12 inside_Int_outside op_in1c)
   4.643 +            with fr_in x show "x \<in> ?\<Theta>"
   4.644 +              by (metis c1c c1c2 closure_Un_frontier pa1_disj_in2 Int_iff Un_iff insert_disjoint(2) insert_subset subsetI subset_antisym)
   4.645 +          qed
   4.646 +          show "?rhs \<subseteq> ?lhs"
   4.647 +            using if1 if2 closure_Un_frontier by fastforce
   4.648 +        qed
   4.649 +        ultimately
   4.650 +        show "connected (closure (inside (?\<Theta>1 \<union> ?\<Theta>)) \<inter> closure (inside (?\<Theta>2 \<union> ?\<Theta>)))"
   4.651 +          by auto
   4.652 +      qed
   4.653 +      show "connected (outside (?\<Theta>1 \<union> ?\<Theta>) \<inter> outside (?\<Theta>2 \<union> ?\<Theta>))"
   4.654 +        using fr_in conn_U  by (simp add: closure_Un_frontier outside_inside Un_commute)
   4.655 +      show "outside (?\<Theta>1 \<union> ?\<Theta>) \<inter> outside (?\<Theta>2 \<union> ?\<Theta>) \<subseteq> - (?\<Theta>1 \<union> ?\<Theta>2)"
   4.656 +        by clarify (metis Diff_Compl Diff_iff Un_iff inf_sup_absorb outside_inside)
   4.657 +      show "outside (?\<Theta>1 \<union> ?\<Theta>2) \<inter>
   4.658 +            (outside (?\<Theta>1 \<union> ?\<Theta>) \<inter> outside (?\<Theta>2 \<union> ?\<Theta>)) \<noteq> {}"
   4.659 +        by (metis Int_assoc out_in inf.orderE out_sub12(1) out_sub12(2) outside_in_components)
   4.660 +    qed
   4.661 +    show "inside (?\<Theta>1 \<union> ?\<Theta>) \<union> inside (?\<Theta>2 \<union> ?\<Theta>) \<union> (?\<Theta> - {a, b}) = inside (?\<Theta>1 \<union> ?\<Theta>2)"
   4.662 +      (is "?lhs = ?rhs")
   4.663 +    proof
   4.664 +      show "?lhs \<subseteq> ?rhs"
   4.665 +        apply (simp add: in_sub_in1 in_sub_in2)
   4.666 +        using c1c c2c inside_outside pi_disjoint by fastforce
   4.667 +      have "inside (?\<Theta>1 \<union> ?\<Theta>2) \<subseteq> inside (?\<Theta>1 \<union> ?\<Theta>) \<union> inside (?\<Theta>2 \<union> ?\<Theta>) \<union> (?\<Theta>)"
   4.668 +        using Compl_anti_mono [OF *] by (force simp: inside_outside)
   4.669 +      moreover have "inside (?\<Theta>1 \<union> ?\<Theta>2) \<subseteq> -{a,b}"
   4.670 +        using c1 union_with_outside by fastforce
   4.671 +      ultimately show "?rhs \<subseteq> ?lhs" by auto
   4.672 +    qed
   4.673 +  qed
   4.674 +qed
   4.675 +
   4.676 +end