Theory HOL-Analysis.Jordan_Curve

(*  Title:      HOL/Analysis/Jordan_Curve.thy
    Authors:    LC Paulson, based on material from HOL Light
*)

section ‹The Jordan Curve Theorem and Applications›

theory Jordan_Curve
  imports Arcwise_Connected Further_Topology
begin

subsection‹Janiszewski's theorem›

lemma Janiszewski_weak:
  fixes a b::complex
  assumes "compact S" "compact T" and conST: "connected(S  T)"
      and ccS: "connected_component (- S) a b" and ccT: "connected_component (- T) a b"
    shows "connected_component (- (S  T)) a b"
proof -
  have [simp]: "a  S" "a  T" "b  S" "b  T"
    by (meson ComplD ccS ccT connected_component_in)+
  have clo: "closedin (top_of_set (S  T)) S" "closedin (top_of_set (S  T)) T"
    by (simp_all add: assms closed_subset compact_imp_closed)
  obtain g where contg: "continuous_on S g"
             and g: "x. x  S  exp (𝗂* of_real (g x)) = (x - a) /R cmod (x - a) / ((x - b) /R cmod (x - b))"
    using ccS compact S
    apply (simp add: Borsuk_maps_homotopic_in_connected_component_eq [symmetric])
    apply (subst (asm) homotopic_circlemaps_divide)
    apply (auto simp: inessential_eq_continuous_logarithm_circle)
    done
  obtain h where conth: "continuous_on T h"
             and h: "x. x  T  exp (𝗂* of_real (h x)) = (x - a) /R cmod (x - a) / ((x - b) /R cmod (x - b))"
    using ccT compact T
    apply (simp add: Borsuk_maps_homotopic_in_connected_component_eq [symmetric])
    apply (subst (asm) homotopic_circlemaps_divide)
    apply (auto simp: inessential_eq_continuous_logarithm_circle)
    done
  have "continuous_on (S  T) (λx. (x - a) /R cmod (x - a))" "continuous_on (S  T) (λx. (x - b) /R cmod (x - b))"
    by (intro continuous_intros; force)+
  moreover have "(λx. (x - a) /R cmod (x - a)) ` (S  T)  sphere 0 1" "(λx. (x - b) /R cmod (x - b)) ` (S  T)  sphere 0 1"
    by (auto simp: divide_simps)
  moreover have "g. continuous_on (S  T) g 
                     (xS  T. (x - a) /R cmod (x - a) / ((x - b) /R cmod (x - b)) = exp (𝗂*complex_of_real (g x)))"
  proof (cases "S  T = {}")
    case True
    then have "continuous_on (S  T) (λx. if x  S then g x else h x)"
      using continuous_on_cases_local [OF clo contg conth]
      by (meson disjoint_iff)
    then show ?thesis
      by (rule_tac x="(λx. if x  S then g x else h x)" in exI) (auto simp: g h)
  next
    case False
    have diffpi: "n. g x = h x + 2* of_int n*pi" if "x  S  T" for x
    proof -
      have "exp (𝗂* of_real (g x)) = exp (𝗂* of_real (h x))"
        using that by (simp add: g h)
      then obtain n where "complex_of_real (g x) = complex_of_real (h x) + 2* of_int n*complex_of_real pi"
        apply (simp add: exp_eq)
        by (metis complex_i_not_zero distrib_left mult.commute mult_cancel_left)
      then show ?thesis
        using of_real_eq_iff by (fastforce intro!: exI [where x=n])
    qed
    have contgh: "continuous_on (S  T) (λx. g x - h x)"
      by (intro continuous_intros continuous_on_subset [OF contg] continuous_on_subset [OF conth]) auto
    moreover have disc:
          "e>0. y. y  S  T  g y - h y  g x - h x  e  norm ((g y - h y) - (g x - h x))"
          if "x  S  T" for x
    proof -
      obtain nx where nx: "g x = h x + 2* of_int nx*pi"
        using x  S  T diffpi by blast
      have "2*pi  norm (g y - h y - (g x - h x))" if y: "y  S  T" and neq: "g y - h y  g x - h x" for y
      proof -
        obtain ny where ny: "g y = h y + 2* of_int ny*pi"
          using y  S  T diffpi by blast
        { assume "nx  ny"
          then have "1  ¦real_of_int ny - real_of_int nx¦"
            by linarith
          then have "(2*pi)*1  (2*pi)*¦real_of_int ny - real_of_int nx¦"
            by simp
          also have "... = ¦2*real_of_int ny*pi - 2*real_of_int nx*pi¦"
            by (simp add: algebra_simps abs_if)
          finally have "2*pi  ¦2*real_of_int ny*pi - 2*real_of_int nx*pi¦" by simp
        }
        with neq show ?thesis
          by (simp add: nx ny)
      qed
      then show ?thesis
        by (rule_tac x="2*pi" in exI) auto
    qed
    ultimately have "(λx. g x - h x) constant_on S  T"
      using continuous_discrete_range_constant [OF conST contgh] by blast
    then obtain z where z: "x. x  S  T  g x - h x = z"
      by (auto simp: constant_on_def)
    obtain w where "exp(𝗂 * of_real(h w)) = exp (𝗂 * of_real(z + h w))"
      using disc z False
      by auto (metis diff_add_cancel g h of_real_add)
    then have [simp]: "exp (𝗂* of_real z) = 1"
      by (metis cis_conv_exp cis_mult exp_not_eq_zero mult_cancel_right1)
    show ?thesis
    proof (intro exI conjI)
      show "continuous_on (S  T) (λx. if x  S then g x else z + h x)"
        by (intro continuous_intros continuous_on_cases_local [OF clo contg] conth) (use z in force)
    qed (auto simp: g h algebra_simps exp_add)
  qed
  ultimately have "homotopic_with_canon (λx. True) (S  T) (sphere 0 1)
                          (λx. (x - a) /R cmod (x - a))  (λx. (x - b) /R cmod (x - b))"
    by (subst homotopic_circlemaps_divide) (auto simp: inessential_eq_continuous_logarithm_circle)
  moreover have "compact (S  T)"
    using assms by blast
  ultimately show ?thesis
    using assms Borsuk_maps_homotopic_in_connected_component_eq by fastforce
qed


theorem Janiszewski:
  fixes a b :: complex
  assumes "compact S" "closed T" and conST: "connected (S  T)"
      and ccS: "connected_component (- S) a b" and ccT: "connected_component (- T) a b"
    shows "connected_component (- (S  T)) a b"
proof -
  have "path_component(- T) a b"
    by (simp add: closed T ccT open_Compl open_path_connected_component)
  then obtain g where g: "path g" "path_image g  - T" "pathstart g = a" "pathfinish g = b"
    by (auto simp: path_component_def)
  then obtain C where C: "compact C" "connected C" "a  C" "b  C" "C  T = {}"
    by fastforce
  obtain r where "0 < r" and r: "C  S  ball 0 r"
    by (metis compact C compact S bounded_Un compact_imp_bounded bounded_subset_ballD)
  have "connected_component (- (S  (T  cball 0 r  sphere 0 r))) a b"
  proof (rule Janiszewski_weak [OF compact S])
    show comT': "compact ((T  cball 0 r)  sphere 0 r)"
      by (simp add: closed T closed_Int_compact compact_Un)
    have "S  (T  cball 0 r  sphere 0 r) = S  T"
      using r by auto
    with conST show "connected (S  (T  cball 0 r  sphere 0 r))"
      by simp
    show "connected_component (- (T  cball 0 r  sphere 0 r)) a b"
      using conST C r
      apply (simp add: connected_component_def)
      apply (rule_tac x=C in exI)
      by auto
  qed (simp add: ccS)
  then obtain U where U: "connected U" "U  - S" "U  - T  - cball 0 r" "U  - sphere 0 r" "a  U" "b  U"
    by (auto simp: connected_component_def)
  show ?thesis
    unfolding connected_component_def
  proof (intro exI conjI)
    show "U  - (S  T)"
      using U r 0 < r a  C connected_Int_frontier [of U "cball 0 r"]
      apply simp
      by (metis ball_subset_cball compl_inf disjoint_eq_subset_Compl disjoint_iff_not_equal inf.orderE inf_sup_aci(3) subsetCE)
  qed (auto simp: U)
qed

lemma Janiszewski_connected:
  fixes S :: "complex set"
  assumes ST: "compact S" "closed T" "connected(S  T)"
    and notST: "connected (- S)" "connected (- T)"
  shows "connected(- (S  T))"
  using Janiszewski [OF ST] by (metis IntD1 IntD2 notST compl_sup connected_iff_connected_component)


subsection‹The Jordan Curve theorem›

lemma exists_double_arc:
  fixes g :: "real  'a::real_normed_vector"
  assumes "simple_path g" "pathfinish g = pathstart g" "a  path_image g" "b  path_image g" "a  b"
  obtains u d where "arc u" "arc d" "pathstart u = a" "pathfinish u = b"
                    "pathstart d = b" "pathfinish d = a"
                    "(path_image u)  (path_image d) = {a,b}"
                    "(path_image u)  (path_image d) = path_image g"
proof -
  obtain u where u: "0  u" "u  1" "g u = a"
    using assms by (auto simp: path_image_def)
  define h where "h  shiftpath u g"
  have "simple_path h"
    using simple_path g simple_path_shiftpath 0  u u  1 assms(2) h_def by blast
  have "pathstart h = g u"
    by (simp add: u  1 h_def pathstart_shiftpath)
  have "pathfinish h = g u"
    by (simp add: 0  u assms h_def pathfinish_shiftpath)
  have pihg: "path_image h = path_image g"
    by (simp add: 0  u u  1 assms h_def path_image_shiftpath)
  then obtain v where v: "0  v" "v  1" "h v = b"
    using assms by (metis (mono_tags, lifting) atLeastAtMost_iff imageE path_image_def)
  show ?thesis
  proof
    show "arc (subpath 0 v h)"
      by (metis (no_types) pathstart h = g u simple_path h arc_simple_path_subpath a  b atLeastAtMost_iff zero_le_one order_refl pathstart_def u(3) v)
    show "arc (subpath v 1 h)"
      by (metis (no_types) pathfinish h = g u simple_path h arc_simple_path_subpath a  b atLeastAtMost_iff zero_le_one order_refl pathfinish_def u(3) v)
    show "pathstart (subpath 0 v h) = a"
      by (metis pathstart h = g u pathstart_def pathstart_subpath u(3))
    show "pathfinish (subpath 0 v h) = b"  "pathstart (subpath v 1 h) = b"
      by (simp_all add: v(3))
    show "pathfinish (subpath v 1 h) = a"
      by (metis pathfinish h = g u pathfinish_def pathfinish_subpath u(3))
    show "path_image (subpath 0 v h)  path_image (subpath v 1 h) = {a, b}"
    proof
      have "loop_free h"
        using simple_path h simple_path_def by blast
      then show "path_image (subpath 0 v h)  path_image (subpath v 1 h)  {a, b}"
        using v pathfinish (subpath v 1 h) = a
        apply (clarsimp simp add: loop_free_def path_image_subpath Ball_def)
        by (smt (verit))
      show "{a, b}  path_image (subpath 0 v h)  path_image (subpath v 1 h)"
        using v pathstart (subpath 0 v h) = a pathfinish (subpath v 1 h) = a
        by (auto simp: path_image_subpath image_iff Bex_def)
    qed
    show "path_image (subpath 0 v h)  path_image (subpath v 1 h) = path_image g"
      using v path_image_subpath pihg path_image_def
      by (metis (full_types) image_Un ivl_disj_un_two_touch(4))
  qed
qed


theoremtag unimportant› Jordan_curve:
  fixes c :: "real  complex"
  assumes "simple_path c" and loop: "pathfinish c = pathstart c"
  obtains inner outer where
                "inner  {}" "open inner" "connected inner"
                "outer  {}" "open outer" "connected outer"
                "bounded inner" "¬ bounded outer" "inner  outer = {}"
                "inner  outer = - path_image c"
                "frontier inner = path_image c"
                "frontier outer = path_image c"
proof -
  have "path c"
    by (simp add: assms simple_path_imp_path)
  have hom: "(path_image c) homeomorphic (sphere(0::complex) 1)"
    by (simp add: assms homeomorphic_simple_path_image_circle)
  with Jordan_Brouwer_separation have "¬ connected (- (path_image c))"
    by fastforce
  then obtain inner where inner: "inner  components (- path_image c)" and "bounded inner"
    using cobounded_has_bounded_component [of "- (path_image c)"]
    using ¬ connected (- path_image c) simple_path c bounded_simple_path_image by force
  obtain outer where outer: "outer  components (- path_image c)" and "¬ bounded outer"
    using cobounded_unbounded_components [of "- (path_image c)"]
    using path c bounded_path_image by auto
  show ?thesis
  proof
    show "inner  {}"
      using inner in_components_nonempty by auto
    show "open inner"
      by (meson simple_path c compact_imp_closed compact_simple_path_image inner open_Compl open_components)
    show "connected inner"
      using in_components_connected inner by blast
    show "outer  {}"
      using outer in_components_nonempty by auto
    show "open outer"
      by (meson simple_path c compact_imp_closed compact_simple_path_image outer open_Compl open_components)
    show "connected outer"
      using in_components_connected outer by blast
    show inner_outer: "inner  outer = {}"
      by (meson ¬ bounded outer bounded inner connected outer bounded_subset components_maximal in_components_subset inner outer)
    show fro_inner: "frontier inner = path_image c"
      by (simp add: Jordan_Brouwer_frontier [OF hom inner])
    show fro_outer: "frontier outer = path_image c"
      by (simp add: Jordan_Brouwer_frontier [OF hom outer])
    have False if m: "middle  components (- path_image c)" and "middle  inner" "middle  outer" for middle
    proof -
      have "frontier middle = path_image c"
        by (simp add: Jordan_Brouwer_frontier [OF hom] that)
      obtain middle: "open middle" "connected middle" "middle  {}"
        by (metis fro_inner frontier_closed in_components_maximal m open_Compl open_components)
      obtain a0 b0 where "a0  path_image c" "b0  path_image c" "a0  b0"
        using simple_path_image_uncountable [OF simple_path c]
        by (metis Diff_cancel countable_Diff_eq countable_empty insert_iff subsetI subset_singleton_iff)
      obtain a b g where ab: "a  path_image c" "b  path_image c" "a  b"
                     and g: "arc g" "pathstart g = a" "pathfinish g = b"
                     and pag_sub: "path_image g - {a,b}  middle"
      proof (rule dense_accessible_frontier_point_pairs [OF open middle connected middle, of "path_image c  ball a0 (dist a0 b0)" "path_image c  ball b0 (dist a0 b0)"])
        show "openin (top_of_set (frontier middle)) (path_image c  ball a0 (dist a0 b0))"
             "openin (top_of_set (frontier middle)) (path_image c  ball b0 (dist a0 b0))"
          by (simp_all add: frontier middle = path_image c openin_open_Int)
        show "path_image c  ball a0 (dist a0 b0)  path_image c  ball b0 (dist a0 b0)"
          using a0  b0 b0  path_image c by auto
        show "path_image c  ball a0 (dist a0 b0)  {}"
          using a0  path_image c a0  b0 by auto
        show "path_image c  ball b0 (dist a0 b0)  {}"
          using b0  path_image c a0  b0 by auto
      qed (use arc_distinct_ends arc_imp_simple_path simple_path_endless that in fastforce)
      obtain u d where "arc u" "arc d"
                   and "pathstart u = a" "pathfinish u = b" "pathstart d = b" "pathfinish d = a"
                   and ud_ab: "(path_image u)  (path_image d) = {a,b}"
                   and ud_Un: "(path_image u)  (path_image d) = path_image c"
        using exists_double_arc [OF assms ab] by blast
      obtain x y where "x  inner" "y  outer"
        using inner  {} outer  {} by auto
      have "inner  middle = {}" "middle  outer = {}"
        using components_nonoverlap inner outer m that by blast+
      have "connected_component (- (path_image u  path_image g  (path_image d  path_image g))) x y"
      proof (rule Janiszewski)
        show "compact (path_image u  path_image g)"
          by (simp add: arc g arc u compact_Un compact_arc_image)
        show "closed (path_image d  path_image g)"
          by (simp add: arc d arc g closed_Un closed_arc_image)
        show "connected ((path_image u  path_image g)  (path_image d  path_image g))"
          using ud_ab
          by (metis Un_insert_left g connected_arc_image insert_absorb pathfinish_in_path_image pathstart_in_path_image sup_bot_left sup_commute sup_inf_distrib1)
        show "connected_component (- (path_image u  path_image g)) x y"
          unfolding connected_component_def
        proof (intro exI conjI)
          have "connected ((inner  (path_image c - path_image u))  (outer  (path_image c - path_image u)))"
          proof (rule connected_Un)
            show "connected (inner  (path_image c - path_image u))"
              using connected_intermediate_closure [OF connected inner]
              by (metis Diff_subset closure_Un_frontier dual_order.refl fro_inner sup.mono sup_ge1)
            show "connected (outer  (path_image c - path_image u))"
              using connected_intermediate_closure [OF connected outer]
              by (simp add: Diff_eq closure_Un_frontier fro_outer sup_inf_distrib1)
            have "(inner  outer)  (path_image c - path_image u)  {}"
              using arc d pathfinish d = a pathstart d = b arc_imp_simple_path nonempty_simple_path_endless ud_Un ud_ab by fastforce
            then show "(inner  (path_image c - path_image u))  (outer  (path_image c - path_image u))  {}"
              by auto
          qed
          then show "connected (inner  outer  (path_image c - path_image u))"
            by (metis sup.right_idem sup_assoc sup_commute)
          have "inner  - path_image u" "outer  - path_image u"
            using in_components_subset inner outer ud_Un by auto
          moreover have "inner  - path_image g" "outer  - path_image g"
            using inner  middle = {} inner  - path_image u
            using middle  outer = {} outer  - path_image u pag_sub ud_ab by fastforce+
          moreover have "path_image c - path_image u  - path_image g"
            using in_components_subset m pag_sub ud_ab by fastforce
          ultimately show "inner  outer  (path_image c - path_image u)  - (path_image u  path_image g)"
            by force
          show "x  inner  outer  (path_image c - path_image u)"
            by (auto simp: x  inner)
          show "y  inner  outer  (path_image c - path_image u)"
            by (auto simp: y  outer)
        qed
        show "connected_component (- (path_image d  path_image g)) x y"
          unfolding connected_component_def
        proof (intro exI conjI)
          have "connected ((inner  (path_image c - path_image d))  (outer  (path_image c - path_image d)))"
          proof (rule connected_Un)
            show "connected (inner  (path_image c - path_image d))"
              using connected_intermediate_closure [OF connected inner] fro_inner
              by (simp add: closure_Un_frontier sup.coboundedI2)
            show "connected (outer  (path_image c - path_image d))"
              using connected_intermediate_closure [OF connected outer]
              by (simp add: closure_Un_frontier fro_outer sup.coboundedI2)
            have "(inner  outer)  (path_image c - path_image d)  {}"
              using arc u pathfinish u = b pathstart u = a arc_imp_simple_path nonempty_simple_path_endless ud_Un ud_ab by fastforce
            then show "(inner  (path_image c - path_image d))  (outer  (path_image c - path_image d))  {}"
              by auto
          qed
          then show "connected (inner  outer  (path_image c - path_image d))"
            by (metis sup.right_idem sup_assoc sup_commute)
          have "inner  - path_image d" "outer  - path_image d"
            using in_components_subset inner outer ud_Un by auto
          moreover have "inner  - path_image g" "outer  - path_image g"
            using inner  middle = {} inner  - path_image d
            using middle  outer = {} outer  - path_image d pag_sub ud_ab by fastforce+
          moreover have "path_image c - path_image d  - path_image g"
            using in_components_subset m pag_sub ud_ab by fastforce
          ultimately show "inner  outer  (path_image c - path_image d)  - (path_image d  path_image g)"
            by force
          show "x  inner  outer  (path_image c - path_image d)"
            by (auto simp: x  inner)
          show "y  inner  outer  (path_image c - path_image d)"
            by (auto simp: y  outer)
        qed
      qed
      then have "connected_component (- (path_image u  path_image d  path_image g)) x y"
        by (simp add: Un_ac)
      moreover have "¬(connected_component (- (path_image c)) x y)"
        by (metis (no_types, lifting) ¬ bounded outer bounded inner x  inner y  outer componentsE connected_component_eq inner mem_Collect_eq outer)
      ultimately show False
        by (auto simp: ud_Un [symmetric] connected_component_def)
    qed
    then have "components (- path_image c) = {inner,outer}"
      using inner outer by blast
    then have "Union (components (- path_image c)) = inner  outer"
      by simp
    then show "inner  outer = - path_image c"
      by auto
  qed (auto simp: bounded inner ¬ bounded outer)
qed


corollarytag unimportant› Jordan_disconnected:
  fixes c :: "real  complex"
  assumes "simple_path c" "pathfinish c = pathstart c"
  shows "¬ connected(- path_image c)"
  using Jordan_curve [OF assms]
  by (metis Jordan_Brouwer_separation assms homeomorphic_simple_path_image_circle zero_less_one)


corollary Jordan_inside_outside:
  fixes c :: "real  complex"
  assumes "simple_path c" "pathfinish c = pathstart c"
    shows "inside(path_image c)  {} 
          open(inside(path_image c)) 
          connected(inside(path_image c)) 
          outside(path_image c)  {} 
          open(outside(path_image c)) 
          connected(outside(path_image c)) 
          bounded(inside(path_image c)) 
          ¬ bounded(outside(path_image c)) 
          inside(path_image c)  outside(path_image c) = {} 
          inside(path_image c)  outside(path_image c) =
          - path_image c 
          frontier(inside(path_image c)) = path_image c 
          frontier(outside(path_image c)) = path_image c"
proof -
  obtain inner outer
    where *: "inner  {}" "open inner" "connected inner"
             "outer  {}" "open outer" "connected outer"
             "bounded inner" "¬ bounded outer" "inner  outer = {}"
             "inner  outer = - path_image c"
             "frontier inner = path_image c"
             "frontier outer = path_image c"
    using Jordan_curve [OF assms] by blast
  then have inner: "inside(path_image c) = inner"
    by (metis dual_order.antisym inside_subset interior_eq interior_inside_frontier)
  have outer: "outside(path_image c) = outer"
    using inner  outer = - path_image c inside (path_image c) = inner
          outside_inside inner  outer = {} by auto
  show ?thesis
    using * by (auto simp: inner outer)
qed

subsubsection‹Triple-curve or "theta-curve" theorem›

text‹Proof that there is no fourth component taken from
     Kuratowski's Topology vol 2, para 61, II.›

theorem split_inside_simple_closed_curve:
  fixes c :: "real  complex"
  assumes "simple_path c1" and c1: "pathstart c1 = a" "pathfinish c1 = b"
      and "simple_path c2" and c2: "pathstart c2 = a" "pathfinish c2 = b"
      and "simple_path c"  and c: "pathstart c = a" "pathfinish c = b"
      and "a  b"
      and c1c2: "path_image c1  path_image c2 = {a,b}"
      and c1c: "path_image c1  path_image c = {a,b}"
      and c2c: "path_image c2  path_image c = {a,b}"
      and ne_12: "path_image c  inside(path_image c1  path_image c2)  {}"
  obtains "inside(path_image c1  path_image c)  inside(path_image c2  path_image c) = {}"
          "inside(path_image c1  path_image c)  inside(path_image c2  path_image c) 
           (path_image c - {a,b}) = inside(path_image c1  path_image c2)"
proof -
  let  = "path_image c"  let ?Θ1 = "path_image c1"  let ?Θ2 = "path_image c2"
  have sp: "simple_path (c1 +++ reversepath c2)" "simple_path (c1 +++ reversepath c)" "simple_path (c2 +++ reversepath c)"
    using assms by (auto simp: simple_path_join_loop_eq arc_simple_path simple_path_reversepath)
  then have op_in12: "open (inside (?Θ1  ?Θ2))"
     and op_out12: "open (outside (?Θ1  ?Θ2))"
     and op_in1c: "open (inside (?Θ1  ))"
     and op_in2c: "open (inside (?Θ2  ))"
     and op_out1c: "open (outside (?Θ1  ))"
     and op_out2c: "open (outside (?Θ2  ))"
     and co_in1c: "connected (inside (?Θ1  ))"
     and co_in2c: "connected (inside (?Θ2  ))"
     and co_out12c: "connected (outside (?Θ1  ?Θ2))"
     and co_out1c: "connected (outside (?Θ1  ))"
     and co_out2c: "connected (outside (?Θ2  ))"
     and pa_c: " - {pathstart c, pathfinish c}  - ?Θ1"
               " - {pathstart c, pathfinish c}  - ?Θ2"
     and pa_c1: "?Θ1 - {pathstart c1, pathfinish c1}  - ?Θ2"
                "?Θ1 - {pathstart c1, pathfinish c1}  - "
     and pa_c2: "?Θ2 - {pathstart c2, pathfinish c2}  - ?Θ1"
                "?Θ2 - {pathstart c2, pathfinish c2}  - "
     and co_c: "connected( - {pathstart c,pathfinish c})"
     and co_c1: "connected(?Θ1 - {pathstart c1,pathfinish c1})"
     and co_c2: "connected(?Θ2 - {pathstart c2,pathfinish c2})"
     and fr_in: "frontier(inside(?Θ1  ?Θ2)) = ?Θ1  ?Θ2"
              "frontier(inside(?Θ2  )) = ?Θ2  "
              "frontier(inside(?Θ1  )) = ?Θ1  "
     and fr_out: "frontier(outside(?Θ1  ?Θ2)) = ?Θ1  ?Θ2"
              "frontier(outside(?Θ2  )) = ?Θ2  "
              "frontier(outside(?Θ1  )) = ?Θ1  "
    using Jordan_inside_outside [of "c1 +++ reversepath c2"]
    using Jordan_inside_outside [of "c1 +++ reversepath c"]
    using Jordan_inside_outside [of "c2 +++ reversepath c"] assms
              apply (simp_all add: path_image_join closed_Un closed_simple_path_image open_inside open_outside)
      apply (blast | metis connected_simple_path_endless)+
    done
  have inout_12: "inside (?Θ1  ?Θ2)  ( - {pathstart c, pathfinish c})  {}"
    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)
  have pi_disjoint:  "  outside(?Θ1  ?Θ2) = {}"
  proof (rule ccontr)
    assume "  outside (?Θ1  ?Θ2)  {}"
    then show False
      using connectedD [OF co_c, of "inside(?Θ1  ?Θ2)" "outside(?Θ1  ?Θ2)"]
      using c c1c2 pa_c op_in12 op_out12 inout_12
      apply clarsimp
      by (smt (verit, ccfv_threshold) Diff_Int_distrib Diff_cancel Diff_empty Int_assoc inf_sup_absorb inf_sup_aci(1) outside_no_overlap)
  qed
  have out_sub12: "outside(?Θ1  ?Θ2)  outside(?Θ1  )" "outside(?Θ1  ?Θ2)  outside(?Θ2  )"
    by (metis Un_commute pi_disjoint outside_Un_outside_Un)+
  have pa1_disj_in2: "?Θ1  inside (?Θ2  ) = {}"
  proof (rule ccontr)
    assume ne: "?Θ1  inside (?Θ2  )  {}"
    have 1: "inside (  ?Θ2)   = {}"
      by (metis (no_types) Diff_Int_distrib Diff_cancel inf_sup_absorb inf_sup_aci(3) inside_no_overlap)
    have 2: "outside (  ?Θ2)   = {}"
      by (metis (no_types) Int_empty_right Int_left_commute inf_sup_absorb outside_no_overlap)
    have "path_image c1  outside (path_image c2  path_image c) = {}"
      using connectedD [OF co_c1, of "inside(?Θ2  )" "outside(?Θ2  )"]
        pa_c1 op_in2c op_out2c ne c1 c2c 1 2 by (auto simp: inf_sup_aci)
    then have "outside (?Θ2  )  outside (?Θ1  ?Θ2)"
      by (metis outside_Un_outside_Un sup_commute)
    with out_sub12
    have "outside(?Θ1  ?Θ2) = outside(?Θ2  )" by blast
    then have "frontier(outside(?Θ1  ?Θ2)) = frontier(outside(?Θ2  ))"
      by simp
    then show False
      using inout_12 pi_disjoint c c1c c2c fr_out by auto
  qed
  have pa2_disj_in1: "?Θ2  inside(?Θ1  ) = {}"
  proof (rule ccontr)
    assume ne: "?Θ2  inside (?Θ1  )  {}"
    have 1: "inside (  ?Θ1)   = {}"
      by (metis (no_types) Diff_Int_distrib Diff_cancel inf_sup_absorb inf_sup_aci(3) inside_no_overlap)
    have 2: "outside (  ?Θ1)   = {}"
      by (metis (no_types) Int_empty_right Int_left_commute inf_sup_absorb outside_no_overlap)
    have "outside (?Θ1  )  outside (?Θ1  ?Θ2)"
      apply (rule outside_Un_outside_Un)
      using connectedD [OF co_c2, of "inside(?Θ1  )" "outside(?Θ1  )"]
        pa_c2 op_in1c op_out1c ne c2 c1c 1 2 by (auto simp: inf_sup_aci)
    with out_sub12
    have "outside(?Θ1  ?Θ2) = outside(?Θ1  )"
      by blast
    then have "frontier(outside(?Θ1  ?Θ2)) = frontier(outside(?Θ1  ))"
      by simp
    then show False
      using inout_12 pi_disjoint c c1c c2c fr_out by auto
  qed
  have in_sub_in1: "inside(?Θ1  )  inside(?Θ1  ?Θ2)"
    using pa2_disj_in1 out_sub12 by (auto simp: inside_outside)
  have in_sub_in2: "inside(?Θ2  )  inside(?Θ1  ?Θ2)"
    using pa1_disj_in2 out_sub12 by (auto simp: inside_outside)
  have in_sub_out12: "inside(?Θ1  )  outside(?Θ2  )"
  proof
    fix x
    assume x: "x  inside (?Θ1  )"
    then have xnot: "x  "
      by (simp add: inside_def)
    obtain z where zim: "z  ?Θ1" and zout: "z  outside(?Θ2  )"
      unfolding outside_inside
      using nonempty_simple_path_endless [OF simple_path c1] c1 c1c c1c2 pa1_disj_in2 by auto
    obtain e where "e > 0" and e: "ball z e  outside(?Θ2  )"
      using zout op_out2c open_contains_ball_eq by blast
    have "z  frontier (inside (?Θ1  ))"
      using zim by (auto simp: fr_in)
    then obtain w where w1: "w  inside (?Θ1  )" and dwz: "dist w z < e"
      using zim e > 0 by (auto simp: frontier_def closure_approachable)
    then have w2: "w  outside (?Θ2  )"
      by (metis e dist_commute mem_ball subsetCE)
    then have "connected_component (- ?Θ2  - ) z w"
      unfolding connected_component_def
      by (metis co_out2c compl_sup inside_Un_outside sup_ge2 zout)
    moreover have "connected_component (- ?Θ2  - ) w x"
      unfolding connected_component_def
      using pa2_disj_in1 co_in1c x w1 union_with_outside by fastforce
    ultimately have eq: "connected_component_set (- ?Θ2  - ) x =
                         connected_component_set (- ?Θ2  - ) z"
      by (metis (mono_tags, lifting) connected_component_eq mem_Collect_eq)
    show "x  outside (?Θ2  )"
      using zout x pa2_disj_in1 by (auto simp: outside_def eq xnot)
  qed
  have in_sub_out21: "inside(?Θ2  )  outside(?Θ1  )"
  proof
    fix x
    assume x: "x  inside (?Θ2  )"
    then have xnot: "x  "
      by (simp add: inside_def)
    obtain z where zim: "z  ?Θ2" and zout: "z  outside(?Θ1  )"
      unfolding outside_inside
      using nonempty_simple_path_endless [OF simple_path c2] c1c2 c2 c2c pa2_disj_in1 by auto
    obtain e where "e > 0" and e: "ball z e  outside(?Θ1  )"
      using zout op_out1c open_contains_ball_eq by blast
    have "z  frontier (inside (?Θ2  ))"
      using zim by (auto simp: fr_in)
    then obtain w where w2: "w  inside (?Θ2  )" and dwz: "dist w z < e"
      using zim e > 0 by (auto simp: frontier_def closure_approachable)
    then have w1: "w  outside (?Θ1  )"
      by (metis e dist_commute mem_ball subsetCE)
    then have "connected_component (- ?Θ1  - ) z w"
      unfolding connected_component_def
      by (metis Compl_Un co_out1c inside_Un_outside sup_ge2 zout)
    moreover have "connected_component (- ?Θ1  - ) w x"
      unfolding connected_component_def
      using pa1_disj_in2 co_in2c x w2 union_with_outside by fastforce
    ultimately have eq: "connected_component_set (- ?Θ1  - ) x =
                           connected_component_set (- ?Θ1  - ) z"
      by (metis (no_types, lifting) connected_component_eq mem_Collect_eq)
    show "x  outside (?Θ1  )"
      using zout x pa1_disj_in2 by (auto simp: outside_def eq xnot)
  qed
  show ?thesis
  proof
    show "inside (?Θ1  )  inside (?Θ2  ) = {}"
      by (metis Int_Un_distrib in_sub_out12 bot_eq_sup_iff disjoint_eq_subset_Compl outside_inside)
    have *: "outside (?Θ1  )  outside (?Θ2  )  outside (?Θ1  ?Θ2)"
    proof (rule components_maximal)
      show out_in: "outside (?Θ1  ?Θ2)  components (- (?Θ1  ?Θ2))"
        unfolding outside_in_components co_out12c
        using co_out12c fr_out(1) by force
      have conn_U: "connected (- (closure (inside (?Θ1  ))  closure (inside (?Θ2  ))))"
      proof (rule Janiszewski_connected, simp_all)
        show "bounded (inside (?Θ1  ))"
          by (simp add: simple_path c1 simple_path c bounded_inside bounded_simple_path_image)
        have if1: "- (inside (?Θ1  )  frontier (inside (?Θ1  ))) = - ?Θ1  -   - inside (?Θ1  )"
          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))
        then show "connected (- closure (inside (?Θ1  )))"
          by (metis Compl_Un outside_inside co_out1c closure_Un_frontier)
        have if2: "- (inside (?Θ2  )  frontier (inside (?Θ2  ))) = - ?Θ2  -   - inside (?Θ2  )"
          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(3) closure_Un_frontier fr_out(2))
        then show "connected (- closure (inside (?Θ2  )))"
          by (metis Compl_Un outside_inside co_out2c closure_Un_frontier)
        have "connected()"
          by (metis simple_path c connected_simple_path_image)
        moreover
        have "closure (inside (?Θ1  ))  closure (inside (?Θ2  )) = "
          (is "?lhs = ?rhs")
        proof
          show "?lhs  ?rhs"
          proof clarify
            fix x
            assume x: "x  closure (inside (?Θ1  ))" "x  closure (inside (?Θ2  ))"
            then have "x  inside (?Θ1  )"
              by (meson closure_iff_nhds_not_empty in_sub_out12 inside_Int_outside op_in1c)
            with fr_in x show "x  "
              by (metis c1c c1c2 closure_Un_frontier pa1_disj_in2 Int_iff Un_iff insert_disjoint(2) insert_subset subsetI subset_antisym)
          qed
          show "?rhs  ?lhs"
            using if1 if2 closure_Un_frontier by fastforce
        qed
        ultimately
        show "connected (closure (inside (?Θ1  ))  closure (inside (?Θ2  )))"
          by auto
      qed
      show "connected (outside (?Θ1  )  outside (?Θ2  ))"
        using fr_in conn_U  by (simp add: closure_Un_frontier outside_inside Un_commute)
      show "outside (?Θ1  )  outside (?Θ2  )  - (?Θ1  ?Θ2)"
        by clarify (metis Diff_Compl Diff_iff Un_iff inf_sup_absorb outside_inside)
      show "outside (?Θ1  ?Θ2) 
            (outside (?Θ1  )  outside (?Θ2  ))  {}"
        by (metis Int_assoc out_in inf.orderE out_sub12(1) out_sub12(2) outside_in_components)
    qed
    show "inside (?Θ1  )  inside (?Θ2  )  ( - {a, b}) = inside (?Θ1  ?Θ2)"
      (is "?lhs = ?rhs")
    proof
      have " path_image c - {a, b}  inside (path_image c1  path_image c2)"
        using c1c c2c inside_outside pi_disjoint by fastforce
      then show "?lhs  ?rhs"
        by (simp add: in_sub_in1 in_sub_in2)
      have "inside (?Θ1  ?Θ2)  inside (?Θ1  )  inside (?Θ2  )  ()"
        using Compl_anti_mono [OF *] by (force simp: inside_outside)
      moreover have "inside (?Θ1  ?Θ2)  -{a,b}"
        using c1 union_with_outside by fastforce
      ultimately show "?rhs  ?lhs" by auto
    qed
  qed
qed

end