src/HOL/Analysis/Jordan_Curve.thy
author nipkow
Sat Dec 29 15:43:53 2018 +0100 (6 months ago)
changeset 69529 4ab9657b3257
parent 69508 2a4c8a2a3f8e
child 69922 4a9167f377b0
permissions -rw-r--r--
capitalize proper names in lemma names
lp15@64846
     1
(*  Title:      HOL/Analysis/Jordan_Curve.thy
lp15@64846
     2
    Authors:    LC Paulson, based on material from HOL Light
lp15@64846
     3
*)
lp15@64846
     4
lp15@64846
     5
section \<open>The Jordan Curve Theorem and Applications\<close>
lp15@64846
     6
lp15@64846
     7
theory Jordan_Curve
lp15@64846
     8
  imports Arcwise_Connected Further_Topology
lp15@64846
     9
begin
lp15@64846
    10
nipkow@67968
    11
subsection\<open>Janiszewski's theorem\<close>
lp15@64846
    12
lp15@64846
    13
lemma Janiszewski_weak:
lp15@64846
    14
  fixes a b::complex
lp15@64846
    15
  assumes "compact S" "compact T" and conST: "connected(S \<inter> T)"
lp15@64846
    16
      and ccS: "connected_component (- S) a b" and ccT: "connected_component (- T) a b"
lp15@64846
    17
    shows "connected_component (- (S \<union> T)) a b"
lp15@64846
    18
proof -
lp15@64846
    19
  have [simp]: "a \<notin> S" "a \<notin> T" "b \<notin> S" "b \<notin> T"
lp15@64846
    20
    by (meson ComplD ccS ccT connected_component_in)+
lp15@64846
    21
  have clo: "closedin (subtopology euclidean (S \<union> T)) S" "closedin (subtopology euclidean (S \<union> T)) T"
lp15@64846
    22
    by (simp_all add: assms closed_subset compact_imp_closed)
lp15@64846
    23
  obtain g where contg: "continuous_on S g"
lp15@64846
    24
             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))"
lp15@64846
    25
    using ccS \<open>compact S\<close>
lp15@64846
    26
    apply (simp add: Borsuk_maps_homotopic_in_connected_component_eq [symmetric])
lp15@64846
    27
    apply (subst (asm) homotopic_circlemaps_divide)
lp15@64846
    28
    apply (auto simp: inessential_eq_continuous_logarithm_circle)
lp15@64846
    29
    done
lp15@64846
    30
  obtain h where conth: "continuous_on T h"
lp15@64846
    31
             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))"
lp15@64846
    32
    using ccT \<open>compact T\<close>
lp15@64846
    33
    apply (simp add: Borsuk_maps_homotopic_in_connected_component_eq [symmetric])
lp15@64846
    34
    apply (subst (asm) homotopic_circlemaps_divide)
lp15@64846
    35
    apply (auto simp: inessential_eq_continuous_logarithm_circle)
lp15@64846
    36
    done
lp15@64846
    37
  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))"
lp15@64846
    38
    by (intro continuous_intros; force)+
lp15@64846
    39
  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"
lp15@64846
    40
    by (auto simp: divide_simps)
lp15@64846
    41
  moreover have "\<exists>g. continuous_on (S \<union> T) g \<and>
lp15@64846
    42
                     (\<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)))"
lp15@64846
    43
  proof (cases "S \<inter> T = {}")
lp15@64846
    44
    case True
lp15@64846
    45
    have "continuous_on (S \<union> T) (\<lambda>x. if x \<in> S then g x else h x)"
lp15@64846
    46
      apply (rule continuous_on_cases_local [OF clo contg conth])
lp15@64846
    47
      using True by auto
lp15@64846
    48
    then show ?thesis
lp15@64846
    49
      by (rule_tac x="(\<lambda>x. if x \<in> S then g x else h x)" in exI) (auto simp: g h)
lp15@64846
    50
  next
lp15@64846
    51
    case False
lp15@64846
    52
    have diffpi: "\<exists>n. g x = h x + 2* of_int n*pi" if "x \<in> S \<inter> T" for x
lp15@64846
    53
    proof -
lp15@64846
    54
      have "exp (\<i>* of_real (g x)) = exp (\<i>* of_real (h x))"
lp15@64846
    55
        using that by (simp add: g h)
lp15@64846
    56
      then obtain n where "complex_of_real (g x) = complex_of_real (h x) + 2* of_int n*complex_of_real pi"
lp15@64846
    57
        apply (auto simp: exp_eq)
lp15@64846
    58
        by (metis complex_i_not_zero distrib_left mult.commute mult_cancel_left)
lp15@64846
    59
      then show ?thesis
lp15@64846
    60
        apply (rule_tac x=n in exI)
lp15@64846
    61
        using of_real_eq_iff by fastforce
lp15@64846
    62
    qed
lp15@64846
    63
    have contgh: "continuous_on (S \<inter> T) (\<lambda>x. g x - h x)"
lp15@64846
    64
      by (intro continuous_intros continuous_on_subset [OF contg] continuous_on_subset [OF conth]) auto
lp15@64846
    65
    moreover have disc:
lp15@64846
    66
          "\<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))"
lp15@64846
    67
          if "x \<in> S \<inter> T" for x
lp15@64846
    68
    proof -
lp15@64846
    69
      obtain nx where nx: "g x = h x + 2* of_int nx*pi"
lp15@64846
    70
        using \<open>x \<in> S \<inter> T\<close> diffpi by blast
lp15@64846
    71
      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
lp15@64846
    72
      proof -
lp15@64846
    73
        obtain ny where ny: "g y = h y + 2* of_int ny*pi"
lp15@64846
    74
          using \<open>y \<in> S \<inter> T\<close> diffpi by blast
lp15@64846
    75
        { assume "nx \<noteq> ny"
lp15@64846
    76
          then have "1 \<le> \<bar>real_of_int ny - real_of_int nx\<bar>"
lp15@64846
    77
            by linarith
lp15@64846
    78
          then have "(2*pi)*1 \<le> (2*pi)*\<bar>real_of_int ny - real_of_int nx\<bar>"
lp15@64846
    79
            by simp
lp15@64846
    80
          also have "... = \<bar>2*real_of_int ny*pi - 2*real_of_int nx*pi\<bar>"
lp15@64846
    81
            by (simp add: algebra_simps abs_if)
lp15@64846
    82
          finally have "2*pi \<le> \<bar>2*real_of_int ny*pi - 2*real_of_int nx*pi\<bar>" by simp
lp15@64846
    83
        }
lp15@64846
    84
        with neq show ?thesis
lp15@64846
    85
          by (simp add: nx ny)
lp15@64846
    86
      qed
lp15@64846
    87
      then show ?thesis
lp15@64846
    88
        by (rule_tac x="2*pi" in exI) auto
lp15@64846
    89
    qed
lp15@66884
    90
    ultimately have "(\<lambda>x. g x - h x) constant_on S \<inter> T"
lp15@64846
    91
      using continuous_discrete_range_constant [OF conST contgh] by blast
lp15@66884
    92
    then obtain z where z: "\<And>x. x \<in> S \<inter> T \<Longrightarrow> g x - h x = z"
lp15@66884
    93
      by (auto simp: constant_on_def)
lp15@65064
    94
    obtain w where "exp(\<i> * of_real(h w)) = exp (\<i> * of_real(z + h w))"
lp15@64846
    95
      using disc z False
lp15@64846
    96
      by auto (metis diff_add_cancel g h of_real_add)
lp15@64846
    97
    then have [simp]: "exp (\<i>* of_real z) = 1"
lp15@64846
    98
      by (metis cis_conv_exp cis_mult exp_not_eq_zero mult_cancel_right1)
lp15@64846
    99
    show ?thesis
lp15@64846
   100
    proof (intro exI conjI)
lp15@64846
   101
      show "continuous_on (S \<union> T) (\<lambda>x. if x \<in> S then g x else z + h x)"
lp15@64846
   102
        apply (intro continuous_intros continuous_on_cases_local [OF clo contg] conth)
lp15@64846
   103
        using z by fastforce
lp15@64846
   104
    qed (auto simp: g h algebra_simps exp_add)
lp15@64846
   105
  qed
lp15@64846
   106
  ultimately have *: "homotopic_with (\<lambda>x. True) (S \<union> T) (sphere 0 1)
lp15@64846
   107
                          (\<lambda>x. (x - a) /\<^sub>R cmod (x - a))  (\<lambda>x. (x - b) /\<^sub>R cmod (x - b))"
lp15@64846
   108
    by (subst homotopic_circlemaps_divide) (auto simp: inessential_eq_continuous_logarithm_circle)
lp15@64846
   109
  show ?thesis
lp15@64846
   110
    apply (rule Borsuk_maps_homotopic_in_connected_component_eq [THEN iffD1])
lp15@64846
   111
    using assms by (auto simp: *)
lp15@64846
   112
qed
lp15@64846
   113
lp15@64846
   114
lp15@64846
   115
theorem Janiszewski:
eberlm@68651
   116
  fixes a b :: complex
eberlm@68651
   117
  assumes "compact S" "closed T" and conST: "connected (S \<inter> T)"
lp15@64846
   118
      and ccS: "connected_component (- S) a b" and ccT: "connected_component (- T) a b"
lp15@64846
   119
    shows "connected_component (- (S \<union> T)) a b"
lp15@64846
   120
proof -
lp15@64846
   121
  have "path_component(- T) a b"
lp15@64846
   122
    by (simp add: \<open>closed T\<close> ccT open_Compl open_path_connected_component)
lp15@64846
   123
  then obtain g where g: "path g" "path_image g \<subseteq> - T" "pathstart g = a" "pathfinish g = b"
lp15@64846
   124
    by (auto simp: path_component_def)
lp15@64846
   125
  obtain C where C: "compact C" "connected C" "a \<in> C" "b \<in> C" "C \<inter> T = {}"
lp15@64846
   126
  proof
lp15@64846
   127
    show "compact (path_image g)"
lp15@64846
   128
      by (simp add: \<open>path g\<close> compact_path_image)
lp15@64846
   129
    show "connected (path_image g)"
lp15@64846
   130
      by (simp add: \<open>path g\<close> connected_path_image)
lp15@64846
   131
  qed (use g in auto)
lp15@64846
   132
  obtain r where "0 < r" and r: "C \<union> S \<subseteq> ball 0 r"
lp15@64846
   133
    by (metis \<open>compact C\<close> \<open>compact S\<close> bounded_Un compact_imp_bounded bounded_subset_ballD)
lp15@64846
   134
  have "connected_component (- (S \<union> (T \<inter> cball 0 r \<union> sphere 0 r))) a b"
lp15@64846
   135
  proof (rule Janiszewski_weak [OF \<open>compact S\<close>])
lp15@64846
   136
    show comT': "compact ((T \<inter> cball 0 r) \<union> sphere 0 r)"
lp15@64846
   137
      by (simp add: \<open>closed T\<close> closed_Int_compact compact_Un)
lp15@64846
   138
    have "S \<inter> (T \<inter> cball 0 r \<union> sphere 0 r) = S \<inter> T"
lp15@64846
   139
      using r by auto
lp15@64846
   140
    with conST show "connected (S \<inter> (T \<inter> cball 0 r \<union> sphere 0 r))"
lp15@64846
   141
      by simp
lp15@64846
   142
    show "connected_component (- (T \<inter> cball 0 r \<union> sphere 0 r)) a b"
lp15@64846
   143
      using conST C r
lp15@64846
   144
      apply (simp add: connected_component_def)
lp15@64846
   145
      apply (rule_tac x=C in exI)
lp15@64846
   146
      by auto
lp15@64846
   147
  qed (simp add: ccS)
lp15@64846
   148
  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"
lp15@64846
   149
    by (auto simp: connected_component_def)
lp15@64846
   150
  show ?thesis
lp15@64846
   151
    unfolding connected_component_def
lp15@64846
   152
  proof (intro exI conjI)
lp15@64846
   153
    show "U \<subseteq> - (S \<union> T)"
lp15@64846
   154
      using U r \<open>0 < r\<close> \<open>a \<in> C\<close> connected_Int_frontier [of U "cball 0 r"]
lp15@64846
   155
      apply simp
lp15@64846
   156
      by (metis ball_subset_cball compl_inf disjoint_eq_subset_Compl disjoint_iff_not_equal inf.orderE inf_sup_aci(3) subsetCE)
lp15@64846
   157
  qed (auto simp: U)
lp15@64846
   158
qed
lp15@64846
   159
lp15@64846
   160
lemma Janiszewski_connected:
lp15@64846
   161
  fixes S :: "complex set"
lp15@64846
   162
  assumes ST: "compact S" "closed T" "connected(S \<inter> T)"
lp15@64846
   163
      and notST: "connected (- S)" "connected (- T)"
lp15@64846
   164
    shows "connected(- (S \<union> T))"
lp15@64846
   165
using Janiszewski [OF ST]
lp15@64846
   166
by (metis IntD1 IntD2 notST compl_sup connected_iff_connected_component)
lp15@64846
   167
eberlm@68651
   168
lp15@64846
   169
subsection\<open>The Jordan Curve theorem\<close>
lp15@64846
   170
lp15@64846
   171
lemma exists_double_arc:
lp15@64846
   172
  fixes g :: "real \<Rightarrow> 'a::real_normed_vector"
lp15@64846
   173
  assumes "simple_path g" "pathfinish g = pathstart g" "a \<in> path_image g" "b \<in> path_image g" "a \<noteq> b"
lp15@64846
   174
  obtains u d where "arc u" "arc d" "pathstart u = a" "pathfinish u = b"
lp15@64846
   175
                    "pathstart d = b" "pathfinish d = a"
lp15@64846
   176
                    "(path_image u) \<inter> (path_image d) = {a,b}"
lp15@64846
   177
                    "(path_image u) \<union> (path_image d) = path_image g"
lp15@64846
   178
proof -
lp15@64846
   179
  obtain u where u: "0 \<le> u" "u \<le> 1" "g u = a"
lp15@64846
   180
    using assms by (auto simp: path_image_def)
lp15@64846
   181
  define h where "h \<equiv> shiftpath u g"
lp15@64846
   182
  have "simple_path h"
lp15@64846
   183
    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
lp15@64846
   184
  have "pathstart h = g u"
lp15@64846
   185
    by (simp add: \<open>u \<le> 1\<close> h_def pathstart_shiftpath)
lp15@64846
   186
  have "pathfinish h = g u"
lp15@64846
   187
    by (simp add: \<open>0 \<le> u\<close> assms h_def pathfinish_shiftpath)
lp15@64846
   188
  have pihg: "path_image h = path_image g"
lp15@64846
   189
    by (simp add: \<open>0 \<le> u\<close> \<open>u \<le> 1\<close> assms h_def path_image_shiftpath)
lp15@64846
   190
  then obtain v where v: "0 \<le> v" "v \<le> 1" "h v = b"
lp15@64846
   191
    using assms by (metis (mono_tags, lifting) atLeastAtMost_iff imageE path_image_def)
lp15@64846
   192
  show ?thesis
lp15@64846
   193
  proof
lp15@64846
   194
    show "arc (subpath 0 v h)"
lp15@64846
   195
      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)
lp15@64846
   196
    show "arc (subpath v 1 h)"
lp15@64846
   197
      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)
lp15@64846
   198
    show "pathstart (subpath 0 v h) = a"
lp15@64846
   199
      by (metis \<open>pathstart h = g u\<close> pathstart_def pathstart_subpath u(3))
lp15@64846
   200
    show "pathfinish (subpath 0 v h) = b"  "pathstart (subpath v 1 h) = b"
lp15@64846
   201
      by (simp_all add: v(3))
lp15@64846
   202
    show "pathfinish (subpath v 1 h) = a"
lp15@64846
   203
      by (metis \<open>pathfinish h = g u\<close> pathfinish_def pathfinish_subpath u(3))
lp15@64846
   204
    show "path_image (subpath 0 v h) \<inter> path_image (subpath v 1 h) = {a, b}"
lp15@64846
   205
    proof
lp15@64846
   206
      show "path_image (subpath 0 v h) \<inter> path_image (subpath v 1 h) \<subseteq> {a, b}"
lp15@64846
   207
        using v  \<open>pathfinish (subpath v 1 h) = a\<close> \<open>simple_path h\<close>
lp15@64846
   208
          apply (auto simp: simple_path_def path_image_subpath image_iff Ball_def)
lp15@64846
   209
        by (metis (full_types) less_eq_real_def less_irrefl less_le_trans)
lp15@64846
   210
      show "{a, b} \<subseteq> path_image (subpath 0 v h) \<inter> path_image (subpath v 1 h)"
lp15@64846
   211
        using v \<open>pathstart (subpath 0 v h) = a\<close> \<open>pathfinish (subpath v 1 h) = a\<close>
lp15@64846
   212
        apply (auto simp: path_image_subpath image_iff)
lp15@64846
   213
        by (metis atLeastAtMost_iff order_refl)
lp15@64846
   214
    qed
lp15@64846
   215
    show "path_image (subpath 0 v h) \<union> path_image (subpath v 1 h) = path_image g"
lp15@64846
   216
      using v apply (simp add: path_image_subpath pihg [symmetric])
lp15@64846
   217
      using path_image_def by fastforce
lp15@64846
   218
  qed
lp15@64846
   219
qed
lp15@64846
   220
lp15@64846
   221
eberlm@68651
   222
theorem%unimportant Jordan_curve:
lp15@64846
   223
  fixes c :: "real \<Rightarrow> complex"
lp15@64846
   224
  assumes "simple_path c" and loop: "pathfinish c = pathstart c"
lp15@64846
   225
  obtains inner outer where
lp15@64846
   226
                "inner \<noteq> {}" "open inner" "connected inner"
lp15@64846
   227
                "outer \<noteq> {}" "open outer" "connected outer"
lp15@64846
   228
                "bounded inner" "\<not> bounded outer" "inner \<inter> outer = {}"
lp15@64846
   229
                "inner \<union> outer = - path_image c"
lp15@64846
   230
                "frontier inner = path_image c"
lp15@64846
   231
                "frontier outer = path_image c"
lp15@64846
   232
proof -
lp15@64846
   233
  have "path c"
lp15@64846
   234
    by (simp add: assms simple_path_imp_path)
lp15@64846
   235
  have hom: "(path_image c) homeomorphic (sphere(0::complex) 1)"
lp15@64846
   236
    by (simp add: assms homeomorphic_simple_path_image_circle)
lp15@64846
   237
  with Jordan_Brouwer_separation have "\<not> connected (- (path_image c))"
lp15@64846
   238
    by fastforce
lp15@64846
   239
  then obtain inner where inner: "inner \<in> components (- path_image c)" and "bounded inner"
lp15@64846
   240
    using cobounded_has_bounded_component [of "- (path_image c)"]
lp15@64846
   241
    using \<open>\<not> connected (- path_image c)\<close> \<open>simple_path c\<close> bounded_simple_path_image by force
lp15@64846
   242
  obtain outer where outer: "outer \<in> components (- path_image c)" and "\<not> bounded outer"
lp15@64846
   243
    using cobounded_unbounded_components [of "- (path_image c)"]
lp15@64846
   244
    using \<open>path c\<close> bounded_path_image by auto
lp15@64846
   245
  show ?thesis
lp15@64846
   246
  proof
lp15@64846
   247
    show "inner \<noteq> {}"
lp15@64846
   248
      using inner in_components_nonempty by auto
lp15@64846
   249
    show "open inner"
lp15@64846
   250
      by (meson \<open>simple_path c\<close> compact_imp_closed compact_simple_path_image inner open_Compl open_components)
lp15@64846
   251
    show "connected inner"
lp15@64846
   252
      using in_components_connected inner by blast
lp15@64846
   253
    show "outer \<noteq> {}"
lp15@64846
   254
      using outer in_components_nonempty by auto
lp15@64846
   255
    show "open outer"
lp15@64846
   256
      by (meson \<open>simple_path c\<close> compact_imp_closed compact_simple_path_image outer open_Compl open_components)
lp15@64846
   257
    show "connected outer"
lp15@64846
   258
      using in_components_connected outer by blast
lp15@64846
   259
    show "inner \<inter> outer = {}"
lp15@64846
   260
      by (meson \<open>\<not> bounded outer\<close> \<open>bounded inner\<close> \<open>connected outer\<close> bounded_subset components_maximal in_components_subset inner outer)
lp15@64846
   261
    show fro_inner: "frontier inner = path_image c"
lp15@64846
   262
      by (simp add: Jordan_Brouwer_frontier [OF hom inner])
lp15@64846
   263
    show fro_outer: "frontier outer = path_image c"
lp15@64846
   264
      by (simp add: Jordan_Brouwer_frontier [OF hom outer])
lp15@64846
   265
    have False if m: "middle \<in> components (- path_image c)" and "middle \<noteq> inner" "middle \<noteq> outer" for middle
lp15@64846
   266
    proof -
lp15@64846
   267
      have "frontier middle = path_image c"
lp15@64846
   268
        by (simp add: Jordan_Brouwer_frontier [OF hom] that)
lp15@64846
   269
      have middle: "open middle" "connected middle" "middle \<noteq> {}"
lp15@64846
   270
        apply (meson \<open>simple_path c\<close> compact_imp_closed compact_simple_path_image m open_Compl open_components)
lp15@64846
   271
        using in_components_connected in_components_nonempty m by blast+
lp15@64846
   272
      obtain a0 b0 where "a0 \<in> path_image c" "b0 \<in> path_image c" "a0 \<noteq> b0"
lp15@64846
   273
        using simple_path_image_uncountable [OF \<open>simple_path c\<close>]
lp15@64846
   274
        by (metis Diff_cancel countable_Diff_eq countable_empty insert_iff subsetI subset_singleton_iff)
lp15@64846
   275
      obtain a b g where ab: "a \<in> path_image c" "b \<in> path_image c" "a \<noteq> b"
lp15@64846
   276
                     and "arc g" "pathstart g = a" "pathfinish g = b"
lp15@64846
   277
                     and pag_sub: "path_image g - {a,b} \<subseteq> middle"
lp15@64846
   278
      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)"])
lp15@64846
   279
        show "openin (subtopology euclidean (frontier middle)) (path_image c \<inter> ball a0 (dist a0 b0))"
lp15@64846
   280
             "openin (subtopology euclidean (frontier middle)) (path_image c \<inter> ball b0 (dist a0 b0))"
lp15@64846
   281
          by (simp_all add: \<open>frontier middle = path_image c\<close> openin_open_Int)
lp15@64846
   282
        show "path_image c \<inter> ball a0 (dist a0 b0) \<noteq> path_image c \<inter> ball b0 (dist a0 b0)"
lp15@64846
   283
          using \<open>a0 \<noteq> b0\<close> \<open>b0 \<in> path_image c\<close> by auto
lp15@64846
   284
        show "path_image c \<inter> ball a0 (dist a0 b0) \<noteq> {}"
lp15@64846
   285
          using \<open>a0 \<in> path_image c\<close> \<open>a0 \<noteq> b0\<close> by auto
lp15@64846
   286
        show "path_image c \<inter> ball b0 (dist a0 b0) \<noteq> {}"
lp15@64846
   287
          using \<open>b0 \<in> path_image c\<close> \<open>a0 \<noteq> b0\<close> by auto
lp15@64846
   288
      qed (use arc_distinct_ends arc_imp_simple_path simple_path_endless that in fastforce)
lp15@64846
   289
      obtain u d where "arc u" "arc d"
lp15@64846
   290
                   and "pathstart u = a" "pathfinish u = b" "pathstart d = b" "pathfinish d = a"
lp15@64846
   291
                   and ud_ab: "(path_image u) \<inter> (path_image d) = {a,b}"
lp15@64846
   292
                   and ud_Un: "(path_image u) \<union> (path_image d) = path_image c"
lp15@64846
   293
        using exists_double_arc [OF assms ab] by blast
lp15@64846
   294
      obtain x y where "x \<in> inner" "y \<in> outer"
lp15@64846
   295
        using \<open>inner \<noteq> {}\<close> \<open>outer \<noteq> {}\<close> by auto
lp15@64846
   296
      have "inner \<inter> middle = {}" "middle \<inter> outer = {}"
lp15@64846
   297
        using components_nonoverlap inner outer m that by blast+
lp15@64846
   298
      have "connected_component (- (path_image u \<union> path_image g \<union> (path_image d \<union> path_image g))) x y"
lp15@64846
   299
      proof (rule Janiszewski)
lp15@64846
   300
        show "compact (path_image u \<union> path_image g)"
lp15@64846
   301
          by (simp add: \<open>arc g\<close> \<open>arc u\<close> compact_Un compact_arc_image)
lp15@64846
   302
        show "closed (path_image d \<union> path_image g)"
lp15@64846
   303
          by (simp add: \<open>arc d\<close> \<open>arc g\<close> closed_Un closed_arc_image)
lp15@64846
   304
        show "connected ((path_image u \<union> path_image g) \<inter> (path_image d \<union> path_image g))"
lp15@64846
   305
          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)
lp15@64846
   306
        show "connected_component (- (path_image u \<union> path_image g)) x y"
lp15@64846
   307
          unfolding connected_component_def
lp15@64846
   308
        proof (intro exI conjI)
lp15@64846
   309
          have "connected ((inner \<union> (path_image c - path_image u)) \<union> (outer \<union> (path_image c - path_image u)))"
lp15@64846
   310
          proof (rule connected_Un)
lp15@64846
   311
            show "connected (inner \<union> (path_image c - path_image u))"
lp15@64846
   312
              apply (rule connected_intermediate_closure [OF \<open>connected inner\<close>])
lp15@64846
   313
              using fro_inner [symmetric]  apply (auto simp: closure_subset frontier_def)
lp15@64846
   314
              done
lp15@64846
   315
            show "connected (outer \<union> (path_image c - path_image u))"
lp15@64846
   316
              apply (rule connected_intermediate_closure [OF \<open>connected outer\<close>])
lp15@64846
   317
              using fro_outer [symmetric]  apply (auto simp: closure_subset frontier_def)
lp15@64846
   318
              done
lp15@64846
   319
            have "(inner \<inter> outer) \<union> (path_image c - path_image u) \<noteq> {}"
lp15@64846
   320
              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)
lp15@64846
   321
            then show "(inner \<union> (path_image c - path_image u)) \<inter> (outer \<union> (path_image c - path_image u)) \<noteq> {}"
lp15@64846
   322
              by auto
lp15@64846
   323
          qed
lp15@64846
   324
          then show "connected (inner \<union> outer \<union> (path_image c - path_image u))"
lp15@64846
   325
            by (metis sup.right_idem sup_assoc sup_commute)
lp15@64846
   326
          have "inner \<subseteq> - path_image u" "outer \<subseteq> - path_image u"
lp15@64846
   327
            using in_components_subset inner outer ud_Un by auto
lp15@64846
   328
          moreover have "inner \<subseteq> - path_image g" "outer \<subseteq> - path_image g"
lp15@64846
   329
            using \<open>inner \<inter> middle = {}\<close> \<open>inner \<subseteq> - path_image u\<close>
lp15@64846
   330
            using \<open>middle \<inter> outer = {}\<close> \<open>outer \<subseteq> - path_image u\<close> pag_sub ud_ab by fastforce+
lp15@64846
   331
          moreover have "path_image c - path_image u \<subseteq> - path_image g"
lp15@64846
   332
            using in_components_subset m pag_sub ud_ab by fastforce
lp15@64846
   333
          ultimately show "inner \<union> outer \<union> (path_image c - path_image u) \<subseteq> - (path_image u \<union> path_image g)"
lp15@64846
   334
            by force
lp15@64846
   335
          show "x \<in> inner \<union> outer \<union> (path_image c - path_image u)"
lp15@64846
   336
            by (auto simp: \<open>x \<in> inner\<close>)
lp15@64846
   337
          show "y \<in> inner \<union> outer \<union> (path_image c - path_image u)"
lp15@64846
   338
            by (auto simp: \<open>y \<in> outer\<close>)
lp15@64846
   339
        qed
lp15@64846
   340
        show "connected_component (- (path_image d \<union> path_image g)) x y"
lp15@64846
   341
          unfolding connected_component_def
lp15@64846
   342
        proof (intro exI conjI)
lp15@64846
   343
          have "connected ((inner \<union> (path_image c - path_image d)) \<union> (outer \<union> (path_image c - path_image d)))"
lp15@64846
   344
          proof (rule connected_Un)
lp15@64846
   345
            show "connected (inner \<union> (path_image c - path_image d))"
lp15@64846
   346
              apply (rule connected_intermediate_closure [OF \<open>connected inner\<close>])
lp15@64846
   347
              using fro_inner [symmetric]  apply (auto simp: closure_subset frontier_def)
lp15@64846
   348
              done
lp15@64846
   349
            show "connected (outer \<union> (path_image c - path_image d))"
lp15@64846
   350
              apply (rule connected_intermediate_closure [OF \<open>connected outer\<close>])
lp15@64846
   351
              using fro_outer [symmetric]  apply (auto simp: closure_subset frontier_def)
lp15@64846
   352
              done
lp15@64846
   353
            have "(inner \<inter> outer) \<union> (path_image c - path_image d) \<noteq> {}"
lp15@64846
   354
              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
lp15@64846
   355
            then show "(inner \<union> (path_image c - path_image d)) \<inter> (outer \<union> (path_image c - path_image d)) \<noteq> {}"
lp15@64846
   356
              by auto
lp15@64846
   357
          qed
lp15@64846
   358
          then show "connected (inner \<union> outer \<union> (path_image c - path_image d))"
lp15@64846
   359
            by (metis sup.right_idem sup_assoc sup_commute)
lp15@64846
   360
          have "inner \<subseteq> - path_image d" "outer \<subseteq> - path_image d"
lp15@64846
   361
            using in_components_subset inner outer ud_Un by auto
lp15@64846
   362
          moreover have "inner \<subseteq> - path_image g" "outer \<subseteq> - path_image g"
lp15@64846
   363
            using \<open>inner \<inter> middle = {}\<close> \<open>inner \<subseteq> - path_image d\<close>
lp15@64846
   364
            using \<open>middle \<inter> outer = {}\<close> \<open>outer \<subseteq> - path_image d\<close> pag_sub ud_ab by fastforce+
lp15@64846
   365
          moreover have "path_image c - path_image d \<subseteq> - path_image g"
lp15@64846
   366
            using in_components_subset m pag_sub ud_ab by fastforce
lp15@64846
   367
          ultimately show "inner \<union> outer \<union> (path_image c - path_image d) \<subseteq> - (path_image d \<union> path_image g)"
lp15@64846
   368
            by force
lp15@64846
   369
          show "x \<in> inner \<union> outer \<union> (path_image c - path_image d)"
lp15@64846
   370
            by (auto simp: \<open>x \<in> inner\<close>)
lp15@64846
   371
          show "y \<in> inner \<union> outer \<union> (path_image c - path_image d)"
lp15@64846
   372
            by (auto simp: \<open>y \<in> outer\<close>)
lp15@64846
   373
        qed
lp15@64846
   374
      qed
lp15@64846
   375
      then have "connected_component (- (path_image u \<union> path_image d \<union> path_image g)) x y"
lp15@64846
   376
        by (simp add: Un_ac)
nipkow@69508
   377
      moreover have "\<not>(connected_component (- (path_image c)) x y)"
lp15@64846
   378
        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)
lp15@64846
   379
      ultimately show False
lp15@64846
   380
        by (auto simp: ud_Un [symmetric] connected_component_def)
lp15@64846
   381
    qed
lp15@64846
   382
    then have "components (- path_image c) = {inner,outer}"
lp15@64846
   383
      using inner outer by blast
lp15@64846
   384
    then have "Union (components (- path_image c)) = inner \<union> outer"
lp15@64846
   385
      by simp
lp15@64846
   386
    then show "inner \<union> outer = - path_image c"
lp15@64846
   387
      by auto
lp15@64846
   388
  qed (auto simp: \<open>bounded inner\<close> \<open>\<not> bounded outer\<close>)
lp15@64846
   389
qed
lp15@64846
   390
lp15@64846
   391
eberlm@68651
   392
corollary%unimportant Jordan_disconnected:
lp15@64846
   393
  fixes c :: "real \<Rightarrow> complex"
lp15@64846
   394
  assumes "simple_path c" "pathfinish c = pathstart c"
lp15@64846
   395
    shows "\<not> connected(- path_image c)"
lp15@64846
   396
using Jordan_curve [OF assms]
lp15@64846
   397
  by (metis Jordan_Brouwer_separation assms homeomorphic_simple_path_image_circle zero_less_one)
lp15@64846
   398
lp15@64846
   399
lp15@64846
   400
corollary Jordan_inside_outside:
lp15@64846
   401
  fixes c :: "real \<Rightarrow> complex"
lp15@64846
   402
  assumes "simple_path c" "pathfinish c = pathstart c"
lp15@64846
   403
    shows "inside(path_image c) \<noteq> {} \<and>
lp15@64846
   404
          open(inside(path_image c)) \<and>
lp15@64846
   405
          connected(inside(path_image c)) \<and>
lp15@64846
   406
          outside(path_image c) \<noteq> {} \<and>
lp15@64846
   407
          open(outside(path_image c)) \<and>
lp15@64846
   408
          connected(outside(path_image c)) \<and>
lp15@64846
   409
          bounded(inside(path_image c)) \<and>
lp15@64846
   410
          \<not> bounded(outside(path_image c)) \<and>
lp15@64846
   411
          inside(path_image c) \<inter> outside(path_image c) = {} \<and>
lp15@64846
   412
          inside(path_image c) \<union> outside(path_image c) =
lp15@64846
   413
          - path_image c \<and>
lp15@64846
   414
          frontier(inside(path_image c)) = path_image c \<and>
lp15@64846
   415
          frontier(outside(path_image c)) = path_image c"
lp15@64846
   416
proof -
lp15@64846
   417
  obtain inner outer
lp15@64846
   418
    where *: "inner \<noteq> {}" "open inner" "connected inner"
lp15@64846
   419
             "outer \<noteq> {}" "open outer" "connected outer"
lp15@64846
   420
             "bounded inner" "\<not> bounded outer" "inner \<inter> outer = {}"
lp15@64846
   421
             "inner \<union> outer = - path_image c"
lp15@64846
   422
             "frontier inner = path_image c"
lp15@64846
   423
             "frontier outer = path_image c"
lp15@64846
   424
    using Jordan_curve [OF assms] by blast
lp15@64846
   425
  then have inner: "inside(path_image c) = inner"
lp15@64846
   426
    by (metis dual_order.antisym inside_subset interior_eq interior_inside_frontier)
lp15@64846
   427
  have outer: "outside(path_image c) = outer"
lp15@64846
   428
    using \<open>inner \<union> outer = - path_image c\<close> \<open>inside (path_image c) = inner\<close>
lp15@64846
   429
          outside_inside \<open>inner \<inter> outer = {}\<close> by auto
lp15@64846
   430
  show ?thesis
lp15@64846
   431
    using * by (auto simp: inner outer)
lp15@64846
   432
qed
lp15@64846
   433
lp15@64846
   434
subsubsection\<open>Triple-curve or "theta-curve" theorem\<close>
lp15@64846
   435
lp15@64846
   436
text\<open>Proof that there is no fourth component taken from
lp15@64846
   437
     Kuratowski's Topology vol 2, para 61, II.\<close>
lp15@64846
   438
lp15@64846
   439
theorem split_inside_simple_closed_curve:
lp15@64846
   440
  fixes c :: "real \<Rightarrow> complex"
lp15@64846
   441
  assumes "simple_path c1" and c1: "pathstart c1 = a" "pathfinish c1 = b"
lp15@64846
   442
      and "simple_path c2" and c2: "pathstart c2 = a" "pathfinish c2 = b"
lp15@64846
   443
      and "simple_path c"  and c: "pathstart c = a" "pathfinish c = b"
lp15@64846
   444
      and "a \<noteq> b"
lp15@64846
   445
      and c1c2: "path_image c1 \<inter> path_image c2 = {a,b}"
lp15@64846
   446
      and c1c: "path_image c1 \<inter> path_image c = {a,b}"
lp15@64846
   447
      and c2c: "path_image c2 \<inter> path_image c = {a,b}"
lp15@64846
   448
      and ne_12: "path_image c \<inter> inside(path_image c1 \<union> path_image c2) \<noteq> {}"
lp15@64846
   449
  obtains "inside(path_image c1 \<union> path_image c) \<inter> inside(path_image c2 \<union> path_image c) = {}"
lp15@64846
   450
          "inside(path_image c1 \<union> path_image c) \<union> inside(path_image c2 \<union> path_image c) \<union>
lp15@64846
   451
           (path_image c - {a,b}) = inside(path_image c1 \<union> path_image c2)"
lp15@64846
   452
proof -
lp15@64846
   453
  let ?\<Theta> = "path_image c"  let ?\<Theta>1 = "path_image c1"  let ?\<Theta>2 = "path_image c2"
lp15@64846
   454
  have sp: "simple_path (c1 +++ reversepath c2)" "simple_path (c1 +++ reversepath c)" "simple_path (c2 +++ reversepath c)"
lp15@64846
   455
    using assms by (auto simp: simple_path_join_loop_eq arc_simple_path simple_path_reversepath)
lp15@64846
   456
  then have op_in12: "open (inside (?\<Theta>1 \<union> ?\<Theta>2))"
lp15@64846
   457
     and op_out12: "open (outside (?\<Theta>1 \<union> ?\<Theta>2))"
lp15@64846
   458
     and op_in1c: "open (inside (?\<Theta>1 \<union> ?\<Theta>))"
lp15@64846
   459
     and op_in2c: "open (inside (?\<Theta>2 \<union> ?\<Theta>))"
lp15@64846
   460
     and op_out1c: "open (outside (?\<Theta>1 \<union> ?\<Theta>))"
lp15@64846
   461
     and op_out2c: "open (outside (?\<Theta>2 \<union> ?\<Theta>))"
lp15@64846
   462
     and co_in1c: "connected (inside (?\<Theta>1 \<union> ?\<Theta>))"
lp15@64846
   463
     and co_in2c: "connected (inside (?\<Theta>2 \<union> ?\<Theta>))"
lp15@64846
   464
     and co_out12c: "connected (outside (?\<Theta>1 \<union> ?\<Theta>2))"
lp15@64846
   465
     and co_out1c: "connected (outside (?\<Theta>1 \<union> ?\<Theta>))"
lp15@64846
   466
     and co_out2c: "connected (outside (?\<Theta>2 \<union> ?\<Theta>))"
lp15@64846
   467
     and pa_c: "?\<Theta> - {pathstart c, pathfinish c} \<subseteq> - ?\<Theta>1"
lp15@64846
   468
               "?\<Theta> - {pathstart c, pathfinish c} \<subseteq> - ?\<Theta>2"
lp15@64846
   469
     and pa_c1: "?\<Theta>1 - {pathstart c1, pathfinish c1} \<subseteq> - ?\<Theta>2"
lp15@64846
   470
                "?\<Theta>1 - {pathstart c1, pathfinish c1} \<subseteq> - ?\<Theta>"
lp15@64846
   471
     and pa_c2: "?\<Theta>2 - {pathstart c2, pathfinish c2} \<subseteq> - ?\<Theta>1"
lp15@64846
   472
                "?\<Theta>2 - {pathstart c2, pathfinish c2} \<subseteq> - ?\<Theta>"
lp15@64846
   473
     and co_c: "connected(?\<Theta> - {pathstart c,pathfinish c})"
lp15@64846
   474
     and co_c1: "connected(?\<Theta>1 - {pathstart c1,pathfinish c1})"
lp15@64846
   475
     and co_c2: "connected(?\<Theta>2 - {pathstart c2,pathfinish c2})"
lp15@64846
   476
     and fr_in: "frontier(inside(?\<Theta>1 \<union> ?\<Theta>2)) = ?\<Theta>1 \<union> ?\<Theta>2"
lp15@64846
   477
              "frontier(inside(?\<Theta>2 \<union> ?\<Theta>)) = ?\<Theta>2 \<union> ?\<Theta>"
lp15@64846
   478
              "frontier(inside(?\<Theta>1 \<union> ?\<Theta>)) = ?\<Theta>1 \<union> ?\<Theta>"
lp15@64846
   479
     and fr_out: "frontier(outside(?\<Theta>1 \<union> ?\<Theta>2)) = ?\<Theta>1 \<union> ?\<Theta>2"
lp15@64846
   480
              "frontier(outside(?\<Theta>2 \<union> ?\<Theta>)) = ?\<Theta>2 \<union> ?\<Theta>"
lp15@64846
   481
              "frontier(outside(?\<Theta>1 \<union> ?\<Theta>)) = ?\<Theta>1 \<union> ?\<Theta>"
lp15@64846
   482
    using Jordan_inside_outside [of "c1 +++ reversepath c2"]
lp15@64846
   483
    using Jordan_inside_outside [of "c1 +++ reversepath c"]
lp15@64846
   484
    using Jordan_inside_outside [of "c2 +++ reversepath c"] assms
lp15@64846
   485
              apply (simp_all add: path_image_join closed_Un closed_simple_path_image open_inside open_outside)
lp15@64846
   486
      apply (blast elim: | metis connected_simple_path_endless)+
lp15@64846
   487
    done
lp15@64846
   488
  have inout_12: "inside (?\<Theta>1 \<union> ?\<Theta>2) \<inter> (?\<Theta> - {pathstart c, pathfinish c}) \<noteq> {}"
lp15@64846
   489
    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)
lp15@64846
   490
  have pi_disjoint:  "?\<Theta> \<inter> outside(?\<Theta>1 \<union> ?\<Theta>2) = {}"
lp15@64846
   491
  proof (rule ccontr)
lp15@64846
   492
    assume "?\<Theta> \<inter> outside (?\<Theta>1 \<union> ?\<Theta>2) \<noteq> {}"
lp15@64846
   493
    then show False
lp15@64846
   494
      using connectedD [OF co_c, of "inside(?\<Theta>1 \<union> ?\<Theta>2)" "outside(?\<Theta>1 \<union> ?\<Theta>2)"]
lp15@64846
   495
      using c c1c2 pa_c op_in12 op_out12 inout_12
lp15@64846
   496
      apply auto
lp15@64846
   497
      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)
lp15@64846
   498
      done
lp15@64846
   499
  qed
lp15@64846
   500
  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>)"
lp15@64846
   501
    by (metis Un_commute pi_disjoint outside_Un_outside_Un)+
lp15@64846
   502
  have pa1_disj_in2: "?\<Theta>1 \<inter> inside (?\<Theta>2 \<union> ?\<Theta>) = {}"
lp15@64846
   503
  proof (rule ccontr)
lp15@64846
   504
    assume ne: "?\<Theta>1 \<inter> inside (?\<Theta>2 \<union> ?\<Theta>) \<noteq> {}"
lp15@64846
   505
    have 1: "inside (?\<Theta> \<union> ?\<Theta>2) \<inter> ?\<Theta> = {}"
lp15@64846
   506
      by (metis (no_types) Diff_Int_distrib Diff_cancel inf_sup_absorb inf_sup_aci(3) inside_no_overlap)
lp15@64846
   507
    have 2: "outside (?\<Theta> \<union> ?\<Theta>2) \<inter> ?\<Theta> = {}"
lp15@64846
   508
      by (metis (no_types) Int_empty_right Int_left_commute inf_sup_absorb outside_no_overlap)
lp15@64846
   509
    have "outside (?\<Theta>2 \<union> ?\<Theta>) \<subseteq> outside (?\<Theta>1 \<union> ?\<Theta>2)"
lp15@64846
   510
      apply (subst Un_commute, rule outside_Un_outside_Un)
lp15@64846
   511
      using connectedD [OF co_c1, of "inside(?\<Theta>2 \<union> ?\<Theta>)" "outside(?\<Theta>2 \<union> ?\<Theta>)"]
lp15@64846
   512
        pa_c1 op_in2c op_out2c ne c1 c2c 1 2 by (auto simp: inf_sup_aci)
lp15@64846
   513
    with out_sub12
lp15@64846
   514
    have "outside(?\<Theta>1 \<union> ?\<Theta>2) = outside(?\<Theta>2 \<union> ?\<Theta>)" by blast
lp15@64846
   515
    then have "frontier(outside(?\<Theta>1 \<union> ?\<Theta>2)) = frontier(outside(?\<Theta>2 \<union> ?\<Theta>))"
lp15@64846
   516
      by simp
lp15@64846
   517
    then show False
lp15@64846
   518
      using inout_12 pi_disjoint c c1c c2c fr_out by auto
lp15@64846
   519
  qed
lp15@64846
   520
  have pa2_disj_in1: "?\<Theta>2 \<inter> inside(?\<Theta>1 \<union> ?\<Theta>) = {}"
lp15@64846
   521
  proof (rule ccontr)
lp15@64846
   522
    assume ne: "?\<Theta>2 \<inter> inside (?\<Theta>1 \<union> ?\<Theta>) \<noteq> {}"
lp15@64846
   523
    have 1: "inside (?\<Theta> \<union> ?\<Theta>1) \<inter> ?\<Theta> = {}"
lp15@64846
   524
      by (metis (no_types) Diff_Int_distrib Diff_cancel inf_sup_absorb inf_sup_aci(3) inside_no_overlap)
lp15@64846
   525
    have 2: "outside (?\<Theta> \<union> ?\<Theta>1) \<inter> ?\<Theta> = {}"
lp15@64846
   526
      by (metis (no_types) Int_empty_right Int_left_commute inf_sup_absorb outside_no_overlap)
lp15@64846
   527
    have "outside (?\<Theta>1 \<union> ?\<Theta>) \<subseteq> outside (?\<Theta>1 \<union> ?\<Theta>2)"
lp15@64846
   528
      apply (rule outside_Un_outside_Un)
lp15@64846
   529
      using connectedD [OF co_c2, of "inside(?\<Theta>1 \<union> ?\<Theta>)" "outside(?\<Theta>1 \<union> ?\<Theta>)"]
lp15@64846
   530
        pa_c2 op_in1c op_out1c ne c2 c1c 1 2 by (auto simp: inf_sup_aci)
lp15@64846
   531
    with out_sub12
lp15@64846
   532
    have "outside(?\<Theta>1 \<union> ?\<Theta>2) = outside(?\<Theta>1 \<union> ?\<Theta>)"
lp15@64846
   533
      by blast
lp15@64846
   534
    then have "frontier(outside(?\<Theta>1 \<union> ?\<Theta>2)) = frontier(outside(?\<Theta>1 \<union> ?\<Theta>))"
lp15@64846
   535
      by simp
lp15@64846
   536
    then show False
lp15@64846
   537
      using inout_12 pi_disjoint c c1c c2c fr_out by auto
lp15@64846
   538
  qed
lp15@64846
   539
  have in_sub_in1: "inside(?\<Theta>1 \<union> ?\<Theta>) \<subseteq> inside(?\<Theta>1 \<union> ?\<Theta>2)"
lp15@64846
   540
    using pa2_disj_in1 out_sub12 by (auto simp: inside_outside)
lp15@64846
   541
  have in_sub_in2: "inside(?\<Theta>2 \<union> ?\<Theta>) \<subseteq> inside(?\<Theta>1 \<union> ?\<Theta>2)"
lp15@64846
   542
    using pa1_disj_in2 out_sub12 by (auto simp: inside_outside)
lp15@64846
   543
  have in_sub_out12: "inside(?\<Theta>1 \<union> ?\<Theta>) \<subseteq> outside(?\<Theta>2 \<union> ?\<Theta>)"
lp15@64846
   544
  proof
lp15@64846
   545
    fix x
lp15@64846
   546
    assume x: "x \<in> inside (?\<Theta>1 \<union> ?\<Theta>)"
lp15@64846
   547
    then have xnot: "x \<notin> ?\<Theta>"
lp15@64846
   548
      by (simp add: inside_def)
lp15@64846
   549
    obtain z where zim: "z \<in> ?\<Theta>1" and zout: "z \<in> outside(?\<Theta>2 \<union> ?\<Theta>)"
lp15@64846
   550
      apply (auto simp: outside_inside)
lp15@64846
   551
      using nonempty_simple_path_endless [OF \<open>simple_path c1\<close>]
lp15@64846
   552
      by (metis Diff_Diff_Int Diff_iff ex_in_conv c1 c1c c1c2 pa1_disj_in2)
lp15@64846
   553
    obtain e where "e > 0" and e: "ball z e \<subseteq> outside(?\<Theta>2 \<union> ?\<Theta>)"
lp15@64846
   554
      using zout op_out2c open_contains_ball_eq by blast
lp15@64846
   555
    have "z \<in> frontier (inside (?\<Theta>1 \<union> ?\<Theta>))"
lp15@64846
   556
      using zim by (auto simp: fr_in)
lp15@64846
   557
    then obtain w where w1: "w \<in> inside (?\<Theta>1 \<union> ?\<Theta>)" and dwz: "dist w z < e"
lp15@64846
   558
      using zim \<open>e > 0\<close> by (auto simp: frontier_def closure_approachable)
lp15@64846
   559
    then have w2: "w \<in> outside (?\<Theta>2 \<union> ?\<Theta>)"
lp15@64846
   560
      by (metis e dist_commute mem_ball subsetCE)
lp15@64846
   561
    then have "connected_component (- ?\<Theta>2 \<inter> - ?\<Theta>) z w"
lp15@64846
   562
      apply (simp add: connected_component_def)
lp15@64846
   563
      apply (rule_tac x = "outside(?\<Theta>2 \<union> ?\<Theta>)" in exI)
lp15@64846
   564
      using zout apply (auto simp: co_out2c)
lp15@64846
   565
       apply (simp_all add: outside_inside)
lp15@64846
   566
      done
lp15@64846
   567
    moreover have "connected_component (- ?\<Theta>2 \<inter> - ?\<Theta>) w x"
lp15@64846
   568
      unfolding connected_component_def
lp15@64846
   569
      using pa2_disj_in1 co_in1c x w1 union_with_outside by fastforce
lp15@64846
   570
    ultimately have eq: "connected_component_set (- ?\<Theta>2 \<inter> - ?\<Theta>) x =
lp15@64846
   571
                         connected_component_set (- ?\<Theta>2 \<inter> - ?\<Theta>) z"
lp15@64846
   572
      by (metis (mono_tags, lifting) connected_component_eq mem_Collect_eq)
lp15@64846
   573
    show "x \<in> outside (?\<Theta>2 \<union> ?\<Theta>)"
lp15@64846
   574
      using zout x pa2_disj_in1 by (auto simp: outside_def eq xnot)
lp15@64846
   575
  qed
lp15@64846
   576
  have in_sub_out21: "inside(?\<Theta>2 \<union> ?\<Theta>) \<subseteq> outside(?\<Theta>1 \<union> ?\<Theta>)"
lp15@64846
   577
  proof
lp15@64846
   578
    fix x
lp15@64846
   579
    assume x: "x \<in> inside (?\<Theta>2 \<union> ?\<Theta>)"
lp15@64846
   580
    then have xnot: "x \<notin> ?\<Theta>"
lp15@64846
   581
      by (simp add: inside_def)
lp15@64846
   582
    obtain z where zim: "z \<in> ?\<Theta>2" and zout: "z \<in> outside(?\<Theta>1 \<union> ?\<Theta>)"
lp15@64846
   583
      apply (auto simp: outside_inside)
lp15@64846
   584
      using nonempty_simple_path_endless [OF \<open>simple_path c2\<close>]
lp15@64846
   585
      by (metis (no_types, hide_lams) Diff_Diff_Int Diff_iff c1c2 c2 c2c ex_in_conv pa2_disj_in1)
lp15@64846
   586
    obtain e where "e > 0" and e: "ball z e \<subseteq> outside(?\<Theta>1 \<union> ?\<Theta>)"
lp15@64846
   587
      using zout op_out1c open_contains_ball_eq by blast
lp15@64846
   588
    have "z \<in> frontier (inside (?\<Theta>2 \<union> ?\<Theta>))"
lp15@64846
   589
      using zim by (auto simp: fr_in)
lp15@64846
   590
    then obtain w where w2: "w \<in> inside (?\<Theta>2 \<union> ?\<Theta>)" and dwz: "dist w z < e"
lp15@64846
   591
      using zim \<open>e > 0\<close> by (auto simp: frontier_def closure_approachable)
lp15@64846
   592
    then have w1: "w \<in> outside (?\<Theta>1 \<union> ?\<Theta>)"
lp15@64846
   593
      by (metis e dist_commute mem_ball subsetCE)
lp15@64846
   594
    then have "connected_component (- ?\<Theta>1 \<inter> - ?\<Theta>) z w"
lp15@64846
   595
      apply (simp add: connected_component_def)
lp15@64846
   596
      apply (rule_tac x = "outside(?\<Theta>1 \<union> ?\<Theta>)" in exI)
lp15@64846
   597
      using zout apply (auto simp: co_out1c)
lp15@64846
   598
       apply (simp_all add: outside_inside)
lp15@64846
   599
      done
lp15@64846
   600
    moreover have "connected_component (- ?\<Theta>1 \<inter> - ?\<Theta>) w x"
lp15@64846
   601
      unfolding connected_component_def
lp15@64846
   602
      using pa1_disj_in2 co_in2c x w2 union_with_outside by fastforce
lp15@64846
   603
    ultimately have eq: "connected_component_set (- ?\<Theta>1 \<inter> - ?\<Theta>) x =
lp15@64846
   604
                           connected_component_set (- ?\<Theta>1 \<inter> - ?\<Theta>) z"
lp15@64846
   605
      by (metis (no_types, lifting) connected_component_eq mem_Collect_eq)
lp15@64846
   606
    show "x \<in> outside (?\<Theta>1 \<union> ?\<Theta>)"
lp15@64846
   607
      using zout x pa1_disj_in2 by (auto simp: outside_def eq xnot)
lp15@64846
   608
  qed
lp15@64846
   609
  show ?thesis
lp15@64846
   610
  proof
lp15@64846
   611
    show "inside (?\<Theta>1 \<union> ?\<Theta>) \<inter> inside (?\<Theta>2 \<union> ?\<Theta>) = {}"
lp15@64846
   612
      by (metis Int_Un_distrib in_sub_out12 bot_eq_sup_iff disjoint_eq_subset_Compl outside_inside)
lp15@64846
   613
    have *: "outside (?\<Theta>1 \<union> ?\<Theta>) \<inter> outside (?\<Theta>2 \<union> ?\<Theta>) \<subseteq> outside (?\<Theta>1 \<union> ?\<Theta>2)"
lp15@64846
   614
    proof (rule components_maximal)
lp15@64846
   615
      show out_in: "outside (?\<Theta>1 \<union> ?\<Theta>2) \<in> components (- (?\<Theta>1 \<union> ?\<Theta>2))"
lp15@64846
   616
        apply (simp only: outside_in_components co_out12c)
lp15@64846
   617
        by (metis bounded_empty fr_out(1) frontier_empty unbounded_outside)
lp15@64846
   618
      have conn_U: "connected (- (closure (inside (?\<Theta>1 \<union> ?\<Theta>)) \<union> closure (inside (?\<Theta>2 \<union> ?\<Theta>))))"
lp15@64846
   619
      proof (rule Janiszewski_connected, simp_all)
lp15@64846
   620
        show "bounded (inside (?\<Theta>1 \<union> ?\<Theta>))"
lp15@64846
   621
          by (simp add: \<open>simple_path c1\<close> \<open>simple_path c\<close> bounded_inside bounded_simple_path_image)
lp15@64846
   622
        have if1: "- (inside (?\<Theta>1 \<union> ?\<Theta>) \<union> frontier (inside (?\<Theta>1 \<union> ?\<Theta>))) = - ?\<Theta>1 \<inter> - ?\<Theta> \<inter> - inside (?\<Theta>1 \<union> ?\<Theta>)"
lp15@64846
   623
          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))
lp15@64846
   624
        then show "connected (- closure (inside (?\<Theta>1 \<union> ?\<Theta>)))"
lp15@64846
   625
          by (metis Compl_Un outside_inside co_out1c closure_Un_frontier)
lp15@64846
   626
        have if2: "- (inside (?\<Theta>2 \<union> ?\<Theta>) \<union> frontier (inside (?\<Theta>2 \<union> ?\<Theta>))) = - ?\<Theta>2 \<inter> - ?\<Theta> \<inter> - inside (?\<Theta>2 \<union> ?\<Theta>)"
lp15@64846
   627
          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))
lp15@64846
   628
        then show "connected (- closure (inside (?\<Theta>2 \<union> ?\<Theta>)))"
lp15@64846
   629
          by (metis Compl_Un outside_inside co_out2c closure_Un_frontier)
lp15@64846
   630
        have "connected(?\<Theta>)"
lp15@64846
   631
          by (metis \<open>simple_path c\<close> connected_simple_path_image)
lp15@64846
   632
        moreover
lp15@64846
   633
        have "closure (inside (?\<Theta>1 \<union> ?\<Theta>)) \<inter> closure (inside (?\<Theta>2 \<union> ?\<Theta>)) = ?\<Theta>"
lp15@64846
   634
          (is "?lhs = ?rhs")
lp15@64846
   635
        proof
lp15@64846
   636
          show "?lhs \<subseteq> ?rhs"
lp15@64846
   637
          proof clarify
lp15@64846
   638
            fix x
lp15@64846
   639
            assume x: "x \<in> closure (inside (?\<Theta>1 \<union> ?\<Theta>))" "x \<in> closure (inside (?\<Theta>2 \<union> ?\<Theta>))"
lp15@64846
   640
            then have "x \<notin> inside (?\<Theta>1 \<union> ?\<Theta>)"
lp15@64846
   641
              by (meson closure_iff_nhds_not_empty in_sub_out12 inside_Int_outside op_in1c)
lp15@64846
   642
            with fr_in x show "x \<in> ?\<Theta>"
lp15@64846
   643
              by (metis c1c c1c2 closure_Un_frontier pa1_disj_in2 Int_iff Un_iff insert_disjoint(2) insert_subset subsetI subset_antisym)
lp15@64846
   644
          qed
lp15@64846
   645
          show "?rhs \<subseteq> ?lhs"
lp15@64846
   646
            using if1 if2 closure_Un_frontier by fastforce
lp15@64846
   647
        qed
lp15@64846
   648
        ultimately
lp15@64846
   649
        show "connected (closure (inside (?\<Theta>1 \<union> ?\<Theta>)) \<inter> closure (inside (?\<Theta>2 \<union> ?\<Theta>)))"
lp15@64846
   650
          by auto
lp15@64846
   651
      qed
lp15@64846
   652
      show "connected (outside (?\<Theta>1 \<union> ?\<Theta>) \<inter> outside (?\<Theta>2 \<union> ?\<Theta>))"
lp15@64846
   653
        using fr_in conn_U  by (simp add: closure_Un_frontier outside_inside Un_commute)
lp15@64846
   654
      show "outside (?\<Theta>1 \<union> ?\<Theta>) \<inter> outside (?\<Theta>2 \<union> ?\<Theta>) \<subseteq> - (?\<Theta>1 \<union> ?\<Theta>2)"
lp15@64846
   655
        by clarify (metis Diff_Compl Diff_iff Un_iff inf_sup_absorb outside_inside)
lp15@64846
   656
      show "outside (?\<Theta>1 \<union> ?\<Theta>2) \<inter>
lp15@64846
   657
            (outside (?\<Theta>1 \<union> ?\<Theta>) \<inter> outside (?\<Theta>2 \<union> ?\<Theta>)) \<noteq> {}"
lp15@64846
   658
        by (metis Int_assoc out_in inf.orderE out_sub12(1) out_sub12(2) outside_in_components)
lp15@64846
   659
    qed
lp15@64846
   660
    show "inside (?\<Theta>1 \<union> ?\<Theta>) \<union> inside (?\<Theta>2 \<union> ?\<Theta>) \<union> (?\<Theta> - {a, b}) = inside (?\<Theta>1 \<union> ?\<Theta>2)"
lp15@64846
   661
      (is "?lhs = ?rhs")
lp15@64846
   662
    proof
lp15@64846
   663
      show "?lhs \<subseteq> ?rhs"
lp15@64846
   664
        apply (simp add: in_sub_in1 in_sub_in2)
lp15@64846
   665
        using c1c c2c inside_outside pi_disjoint by fastforce
lp15@64846
   666
      have "inside (?\<Theta>1 \<union> ?\<Theta>2) \<subseteq> inside (?\<Theta>1 \<union> ?\<Theta>) \<union> inside (?\<Theta>2 \<union> ?\<Theta>) \<union> (?\<Theta>)"
lp15@64846
   667
        using Compl_anti_mono [OF *] by (force simp: inside_outside)
lp15@64846
   668
      moreover have "inside (?\<Theta>1 \<union> ?\<Theta>2) \<subseteq> -{a,b}"
lp15@64846
   669
        using c1 union_with_outside by fastforce
lp15@64846
   670
      ultimately show "?rhs \<subseteq> ?lhs" by auto
lp15@64846
   671
    qed
lp15@64846
   672
  qed
lp15@64846
   673
qed
lp15@64846
   674
lp15@64846
   675
end