Theory Polygon_Jordan_Curve

theory Polygon_Jordan_Curve
imports
  "HOL-Analysis.Cartesian_Space"
  "HOL-Analysis.Path_Connected"
  "Poincare_Bendixson.Poincare_Bendixson"
  Integral_Matrix

begin

section "Polygon Definitions"
type_synonym R_to_R2 = "(real ⇒ real^2)"

definition closed_path :: "R_to_R2 ⇒ bool" where  
  "closed_path g ⟷ path g ∧ pathstart g = pathfinish g"

definition path_inside :: "R_to_R2 ⇒ (real^2) set" where
  "path_inside g = inside (path_image g)"

definition path_outside :: "R_to_R2 ⇒ (real^2) set" where
  "path_outside g = outside (path_image g)"

fun make_polygonal_path :: "(real^2) list ⇒ R_to_R2" where
  "make_polygonal_path [] = linepath 0 0"
| "make_polygonal_path [a] = linepath a a"
| "make_polygonal_path [a,b] = linepath a b"
| "make_polygonal_path (a # b # xs) = (linepath a b) +++ make_polygonal_path (b # xs)"

definition polygonal_path :: "R_to_R2 ⇒ bool" where
  "polygonal_path g ⟷ g ∈ make_polygonal_path`{xs :: (real^2) list. True}"

definition all_integral :: "(real^2) list ⇒ bool" where
  "all_integral l = (∀x ∈ set l. integral_vec x)"

definition polygon :: "R_to_R2 ⇒ bool" where
  "polygon g ⟷ polygonal_path g ∧ simple_path g ∧ closed_path g"

definition integral_polygon :: "R_to_R2 ⇒ bool" where
  "integral_polygon g ⟷
    (polygon g ∧ (∃vts. g = make_polygonal_path vts ∧ all_integral vts))"

definition make_triangle :: "real^2 ⇒ real^2 ⇒ real^2 ⇒ R_to_R2" where
  "make_triangle a b c = make_polygonal_path [a, b, c, a]"

definition polygon_of :: "R_to_R2 ⇒ (real^2) list ⇒ bool" where
  "polygon_of p vts ⟷ polygon p ∧ p = make_polygonal_path vts" 

definition good_linepath :: "real^2 ⇒ real^2 ⇒ (real^2) list ⇒ bool" where
  "good_linepath a b vts ⟷ (let p = make_polygonal_path vts in
    a ≠ b ∧ {a, b} ⊆ set vts ∧ path_image (linepath a b) ⊆ path_inside p ∪ {a, b})"

definition good_polygonal_path :: "real^2 ⇒ (real^2) list ⇒ real^2 ⇒ (real^2) list ⇒ bool" where
  "good_polygonal_path a cutvts b vts ⟷ (
    let p = make_polygonal_path vts in
    let p_cut = make_polygonal_path ([a] @ cutvts @ [b]) in
      (a ≠ b ∧ {a, b} ⊆ set vts ∧ path_image (p_cut) ⊆ path_inside p ∪ {a, b} ∧ loop_free p_cut))"

section "Jordan Curve Theorem for Polygons"

definition inside_outside :: "R_to_R2 ⇒ (real^2) set ⇒ (real^2) set ⇒ bool" where
  "inside_outside p ins outs ⟷
    (ins ≠ {} ∧ open ins ∧ connected ins ∧
    outs ≠ {} ∧ open outs ∧ connected outs ∧
    bounded ins ∧ ¬ bounded outs ∧
    ins ∩ outs = {} ∧ ins ∪ outs = - path_image p ∧
    frontier ins = path_image p ∧ frontier outs = path_image p)"

(* For our purposes, it helps to have the same result as Jordan_inside_outside_R2
   outside of the locale (and specialized to paths of our type) *)
lemma Jordan_inside_outside_real2:
  fixes p :: "real ⇒ real^2"
  assumes "simple_path p" "pathfinish p = pathstart p"
  shows "inside(path_image p) ≠ {} ∧
          open(inside(path_image p)) ∧
          connected(inside(path_image p)) ∧
          outside(path_image p) ≠ {} ∧
          open(outside(path_image p)) ∧
          connected(outside(path_image p)) ∧
          bounded(inside(path_image p)) ∧
          ¬ bounded(outside(path_image p)) ∧
          inside(path_image p) ∩ outside(path_image p) = {} ∧
          inside(path_image p) ∪ outside(path_image p) =
          - path_image p ∧
          frontier(inside(path_image p)) = path_image p ∧
          frontier(outside(path_image p)) = path_image p"
proof -
have good_type: "c1_on_open_R2_axioms TYPE((real, 2) vec)"
    unfolding c1_on_open_R2_axioms_def by auto
   have "inside(path_image p) ≠ {} ∧
          open(inside(path_image p)) ∧
          connected(inside(path_image p)) ∧
          outside(path_image p) ≠ {} ∧
          open(outside(path_image p)) ∧
          connected(outside(path_image p)) ∧
          bounded(inside(path_image p)) ∧
          ¬ bounded(outside(path_image p)) ∧
          inside(path_image p) ∩ outside(path_image p) = {} ∧
          inside(path_image p) ∪ outside(path_image p) =
          - path_image p ∧
          frontier(inside(path_image p)) = path_image p ∧
          frontier(outside(path_image p)) = path_image p"
    using assms c1_on_open_R2.Jordan_inside_outside_R2[of _  _ _ p]
    unfolding c1_on_open_R2_def c1_on_open_euclidean_def c1_on_open_def using good_type
    by (metis continuous_on_empty equals0D open_empty)
  then show ?thesis unfolding inside_outside_def
    using path_inside_def path_outside_def by auto
qed

lemma inside_outside_polygon:
  fixes p :: "R_to_R2"
  assumes polygon: "polygon p"
  shows "inside_outside p (path_inside p) (path_outside p)"
proof-
  have good_type: "c1_on_open_R2_axioms TYPE((real, 2) vec)"
    unfolding c1_on_open_R2_axioms_def by auto
  have "simple_path p" "pathfinish p = pathstart p" using assms polygon_def closed_path_def by auto
  then show ?thesis using Jordan_inside_outside_real2 unfolding inside_outside_def
    using path_inside_def path_outside_def by auto
qed

(* Heavily relies on Jordan_inside_outside_R2 from the existing libraries *)
lemma inside_outside_unique:
  fixes p :: "R_to_R2"
  assumes "polygon p"
  assumes io1: "inside_outside p inside1 outside1"
  assumes io2: "inside_outside p inside2 outside2"
  shows "inside1 = inside2 ∧ outside1 = outside2"
proof -
   have inner1: "inside(path_image p) = inside1"
    using dual_order.antisym inside_subset interior_eq interior_inside_frontier
    using io1 unfolding inside_outside_def
    by metis
  have inner2: "inside(path_image p) = inside2"
    using dual_order.antisym inside_subset interior_eq interior_inside_frontier
    using io2 unfolding inside_outside_def
    by metis
  have eq1: "inside1 = inside2"
    using inner1 inner2
    by auto 
  have h1: "inside1 ∪ outside1 = - path_image p"
    using io1 unfolding inside_outside_def by auto 
  have h2: "inside1 ∩ outside1 = {}"
    using io1 unfolding inside_outside_def by auto 
  have outer1: "outside(path_image p) = outside1"
    using io1 inner1 unfolding inside_outside_def
    using h1 h2 outside_inside by auto
  have h3: "inside2 ∪ outside2 = - path_image p"
    using io2 unfolding inside_outside_def by auto 
  have h4: "inside2 ∩ outside2 = {}"
    using io2 unfolding inside_outside_def by auto 
  have outer2: "outside(path_image p) = outside2"
    using io2 inner2 unfolding inside_outside_def
    using h3 h4 outside_inside by auto
  then have eq2: "outside1 = outside2"
    using outer1 outer2 by auto 
  then show ?thesis using eq1 eq2 by auto
qed

lemma polygon_jordan_curve:
  fixes p :: "R_to_R2"
  assumes "polygon p"
  obtains inside outside where
    "inside_outside p inside outside"
proof-
  have good_type: "c1_on_open_R2_axioms TYPE((real, 2) vec)"
    unfolding c1_on_open_R2_axioms_def by auto
  have "simple_path p" "pathfinish p = pathstart p" using assms polygon_def closed_path_def by auto
  then obtain inside outside where
    "inside ≠ {}" "open inside" "connected inside"
    "outside ≠ {}" "open outside" "connected outside"
    "bounded inside" "¬ bounded outside" "inside ∩ outside = {}"
    "inside ∪ outside = - path_image p"
    "frontier inside = path_image p"
    "frontier outside = path_image p"
    using c1_on_open_R2.Jordan_curve_R2[of _  _ _ p]
    unfolding c1_on_open_R2_def c1_on_open_euclidean_def c1_on_open_def using good_type
    by (metis continuous_on_empty equals0D open_empty)
  then show ?thesis
    using inside_outside_def that by auto 
qed

lemma connected_component_image:
  fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space"
  assumes "linear f" "bij f"
  shows " f ` (connected_component_set S x) = connected_component_set (f ` S) (f x)"
proof - 
  have conn: "⋀S. connected S ⟹ connected (f ` S)"
    by (simp add: assms(1) connected_linear_image)
  then have h1: "⋀T. T ∈ {T. connected T ∧ x ∈ T ∧ T ⊆ S} ⟹ f ` T ∈ {T. connected T ∧ (f x) ∈ T ∧ T ⊆ (f ` S)}"
    by auto
  then have subset1: "f ` connected_component_set S x ⊆ connected_component_set (f ` S) (f x)"
    using connected_component_Union   
    by (smt (verit, ccfv_threshold) assms(2) bij_is_inj connected_component_eq_empty connected_component_maximal connected_component_refl_eq connected_component_subset connected_connected_component image_is_empty inj_image_mem_iff mem_Collect_eq) have "⋀S. connected (f ` S) ⟹ connected S"
    using assms  connected_continuous_image assms linear_continuous_on linear_conv_bounded_linear
   bij_is_inj homeomorphism_def linear_homeomorphism_image
    by (smt (verit, del_insts))
  then have h2: "⋀T. f ` T ∈ {T. connected T ∧ (f x) ∈ T ∧ T ⊆ (f ` S)} ⟹ T ∈ {T. connected T ∧ x ∈ T ∧ T ⊆ S}"
    by (simp add: assms(2) bij_is_inj image_subset_iff inj_image_mem_iff subsetI)
    then have subset2: "connected_component_set (f ` S) (f x) ⊆ f ` connected_component_set S x"
    using connected_component_Union[of S x] connected_component_Union[of "f`S" "f x"]
    by (smt (verit, del_insts) assms(2) bij_is_inj connected_component_eq_empty connected_component_maximal connected_component_refl_eq connected_component_subset connected_connected_component image_mono inj_image_mem_iff mem_Collect_eq subset_imageE)
  show "f ` (connected_component_set S x) = connected_component_set (f ` S) (f x)"
    using subset1 subset2 by auto
qed

lemma bounded_map:
  fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space"
  assumes "linear f" "bij f"
  shows "bounded (f ` S) = bounded S"
proof - 
  have h1: "bounded S ⟹ bounded (f ` S)"
    using assms 
    using bounded_linear_image linear_conv_bounded_linear by blast
  have "bounded_linear f"
    using linear_conv_bounded_linear assms by auto 
  then have "bounded_linear (inv f)"
    using assms unfolding bij_def 
    by (smt (verit, ccfv_threshold) bij_betw_def bij_betw_subset dim_image_eq inv_equality linear_conv_bounded_linear linear_surjective_isomorphism subset_UNIV)
  then have h2: "bounded (f ` S) ⟹ bounded S"
    using assms 
    by (metis bij_is_inj bounded_linear_image image_inv_f_f)
  then show ?thesis
    using assms h1 h2 by auto
qed

lemma inside_bijective_linear_image:
  fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space"
  fixes c :: "real ⇒ 'a"
  assumes c_simple:"path c"
  assumes "linear f" "bij f"
  shows "inside (f ` (path_image c)) = f ` (inside(path_image c))" 
proof - 
  have set1: "{x. x ∉ f ` path_image c} =  f ` {x. x ∉ path_image c}"
    using assms path_image_compose unfolding bij_def 
    by (smt (verit, best) UNIV_I imageE inj_image_mem_iff mem_Collect_eq subsetI subset_antisym)
  have linear_inv: "linear (inv f)"
    using assms 
    by (metis bij_imp_bij_inv bij_is_inj inv_o_cancel linear_injective_left_inverse o_inv_o_cancel)
  have bij_inv: "bij (inv f)"
    using assms 
    using bij_imp_bij_inv by blast
  have inset1: "⋀x. x ∈ {x. bounded (connected_component_set (- f ` path_image c) x)} ⟹ x ∈ f ` {x. bounded (connected_component_set (- path_image c) x)}"
  proof -
    fix x
    assume *: "x ∈ {x. bounded (connected_component_set (- f ` path_image c) x)}"
    have "inj f"
        using assms(3) bij_betw_imp_inj_on by blast
    then show "x ∈ f ` {x. bounded (connected_component_set (- path_image c) x)}"
      using * connected_component_image[OF linear_inv bij_inv]
        by (smt (z3) ‹⋀x S. inv f ` connected_component_set S x = connected_component_set (inv f ` S) (inv f x)› ‹bij (inv f)› ‹linear (inv f)› ‹x ∈ {x. bounded (connected_component_set (- f ` path_image c) x)}› bij_image_Compl_eq bounded_map connected_component_eq_empty image_empty image_inv_f_f mem_Collect_eq)
  qed
  have inset2: "⋀x. x ∈ f ` {x. bounded (connected_component_set (- path_image c) x)} ⟹ x ∈ {x. bounded (connected_component_set (- f ` path_image c) x)}"
  proof - 
    fix x
    assume "x ∈ f ` {x. bounded (connected_component_set (- path_image c) x)}"
    then obtain x1 where "x = f x1" "x1 ∈ {x. bounded (connected_component_set (- path_image c) x)}"
      by auto
    then show "x ∈ {x. bounded (connected_component_set (- f ` path_image c) x)}" 
      using bounded_map[OF assms(2) assms(3)] connected_component_image[OF assms(2) assms(3)]
      by (metis assms(3) bij_image_Compl_eq mem_Collect_eq)
  qed
  have set2: "f ` {x. bounded (connected_component_set (- path_image c) x)} = {x. bounded (connected_component_set (- f ` path_image c) x)}"
    using inset1 inset2 by auto
  have inset1: "⋀x. x ∈ f ` {x. x ∉ path_image c ∧ bounded (connected_component_set (- path_image c) x)} ⟹ 
    x∈ {x. x ∉ f ` path_image c ∧ bounded (connected_component_set (- f ` path_image c) x)}"
  proof - 
    fix x
    assume "x ∈ f ` {x. x ∉ path_image c ∧ bounded (connected_component_set (- path_image c) x)}" 
    then show "x∈ {x. x ∉ f ` path_image c ∧ bounded (connected_component_set (- f ` path_image c) x)}"
      by (metis (no_types, lifting) image_iff mem_Collect_eq set1 set2)
  qed
  have inset2: "⋀x. x∈ {x. x ∉ f ` path_image c ∧ bounded (connected_component_set (- f ` path_image c) x)} ⟹
    x ∈ f ` {x. x ∉ path_image c ∧ bounded (connected_component_set (- path_image c) x)}"
  proof - 
    fix x
    assume " x∈ {x. x ∉ f ` path_image c ∧ bounded (connected_component_set (- f ` path_image c) x)}"
    then show "x ∈ f ` {x. x ∉ path_image c ∧ bounded (connected_component_set (- path_image c) x)}"
      by (smt (verit, best) image_iff mem_Collect_eq set2)
  qed
  have same_set: "{x. x ∉ f ` path_image c ∧ bounded (connected_component_set (- f ` path_image c) x)} =
    f ` {x. x ∉ path_image c ∧ bounded (connected_component_set (- path_image c) x)}"
    using inset1 inset2 
    by blast
  have ins1: "⋀x. x ∈ inside (f ` path_image c) ⟹ x ∈ f ` inside (path_image c)"
  proof - 
    fix x
    assume *: "x ∈ inside (f ` path_image c)"
    show "x ∈ f ` inside (path_image c)"
      by (metis (no_types) * same_set inside_def)
  qed
  then have "inside (f ` (path_image c)) ⊆ f ` (inside(path_image c))"
    by auto
  have ins2: "⋀xa. xa ∈ inside (path_image c) ⟹ f xa ∈ inside (f ` path_image c)"
  proof - 
    fix xa
    assume *: "xa ∈ inside (path_image c)"
    show "f xa ∈ inside (f ` path_image c)"
      by (metis (no_types, lifting) * same_set assms(3) bij_def inj_image_mem_iff inside_def mem_Collect_eq)
  qed
  then have "f ` (inside(path_image c)) ⊆ inside (f ` (path_image c)) "
    by auto
  show ?thesis
  using ins1 ins2 by auto 
qed

lemma bij_image_intersection:
  assumes "path_image c1 ∩ path_image c2 = S"
  assumes "bij f"
  assumes "c ∈ path_image (f ∘ c1) ∩ path_image (f ∘ c2)"
  shows "c ∈ f ` S"
  proof - 
    have "c ∈ f ` path_image c1 ∩ f ` path_image c2"
      using assms path_image_compose[of f  c1] path_image_compose[of f c2]
      by auto
    then obtain w where c_is: "w ∈ path_image c1 ∧ w ∈ path_image c2 ∧ c = f w"
      using assms unfolding bij_def inj_def surj_def 
      by auto
    then have "w ∈ S"
      using assms by auto
    then show "c ∈ f ` S"
    using c_is by auto 
qed

(* inspired by a proof in Poincare_Bendixson, but still requires some work *)
theorem (in c1_on_open_R2) split_inside_simple_closed_curve_locale:
  fixes c :: "real ⇒ 'a"
  assumes c1_simple:"simple_path c1" and c1_start: "pathstart c1 = a" and c1_end: "pathfinish c1 = b"
  assumes c2_simple: "simple_path c2" and c2_start: "pathstart c2 = a" and c2_end: "pathfinish c2 = b"
  assumes c_simple: "simple_path c" and c_start: "pathstart c = a" and c_end: "pathfinish c = b"
  assumes a_neq_b: "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 ?cc1 = "(complex_of ∘ c1)"
  let ?cc2 = "(complex_of ∘ c2)"
  let ?cc = "(complex_of ∘ c)"
  have cc1_simple:"simple_path ?cc1"
    using bij_betw_imp_inj_on c1_simple complex_of_bij
    using simple_path_linear_image_eq[OF complex_of_linear]
    by blast
  have cc1_start:"pathstart ?cc1 = (complex_of a)"
    using c1_start by (simp add:pathstart_compose)
  have cc1_end:"pathfinish ?cc1 = (complex_of b)"
    using c1_end by (simp add: pathfinish_compose)
  have cc2_simple:"simple_path ?cc2"
    using c2_simple complex_of_bij bij_betw_imp_inj_on
    using simple_path_linear_image_eq[OF complex_of_linear]
    by blast
  have cc2_start:"pathstart ?cc2 = (complex_of a)"
    using c2_start by (simp add:pathstart_compose)
  have cc2_end:"pathfinish ?cc2 = (complex_of b)"
    using c2_end by (simp add: pathfinish_compose)
  have cc_simple:"simple_path ?cc" using c_simple complex_of_bij
    using bij_betw_imp_inj_on
    using simple_path_linear_image_eq[OF complex_of_linear]
    by blast
  have cc_start:"pathstart ?cc = (complex_of a)"
    using c_start by (simp add:pathstart_compose)
  have cc_end:"pathfinish ?cc = (complex_of b)"
    using c_end by (simp add: pathfinish_compose)
  have ca_neq_cb: "complex_of a ≠ complex_of b"
    using a_neq_b 
    by (meson bij_betw_imp_inj_on complex_of_bij inj_eq)
  have image_set_eq1: "{complex_of a, complex_of b} ⊆ path_image ?cc1 ∩ path_image ?cc2"
    using c1c2 path_image_compose[of complex_of  c1] path_image_compose[of complex_of c2]
    by auto
  have image_set_eq2: "⋀c. c ∈ path_image ?cc1 ∩ path_image ?cc2 ⟹ c ∈{complex_of a, complex_of b}"
   using bij_image_intersection[of c1 c2 "{a, b}" "complex_of"] 
    using c1c2 complex_of_bij by auto
  have cc1c2: "path_image ?cc1 ∩ path_image ?cc2 = {(complex_of a),(complex_of b)}"
    using image_set_eq1 image_set_eq2 by auto
  have image_set_eq1: "{complex_of a, complex_of b} ⊆ path_image ?cc1 ∩ path_image ?cc"
    using c1c path_image_compose[of complex_of c1] path_image_compose[of complex_of c]
    by auto
  have image_set_eq2: "⋀c. c ∈ path_image ?cc1 ∩ path_image ?cc ⟹ c ∈{complex_of a, complex_of b}"
   using bij_image_intersection[of c1 c "{a, b}" "complex_of"] 
    using c1c complex_of_bij by auto
  have cc1c: "path_image ?cc1 ∩ path_image ?cc = {(complex_of a),(complex_of b)}" 
    using image_set_eq1 image_set_eq2 by auto
  have image_set_eq1: "{complex_of a, complex_of b} ⊆ path_image ?cc2 ∩ path_image ?cc"
    using c2c path_image_compose[of complex_of c2] path_image_compose[of complex_of c]
    by auto
  have image_set_eq2: "⋀c. c ∈ path_image ?cc2 ∩ path_image ?cc ⟹ c ∈{complex_of a, complex_of b}"
   using bij_image_intersection[of c2 c "{a, b}" "complex_of"] 
    using c2c complex_of_bij by auto
  have cc2c: "path_image ?cc2 ∩ path_image ?cc = {(complex_of a),(complex_of b)}"
    using image_set_eq1 image_set_eq2 by auto

  (* show there exists a path where the union of the two path images is that path*)
  let ?j = "c1 +++ (reversepath c)"
  let ?cj = "?cc1 +++ (reversepath ?cc)"
  have cj_and_j: "path_image ?cj = complex_of ` (path_image ?j)"
    by (metis path_compose_join path_compose_reversepath path_image_compose)
  have "pathstart (reversepath c) = b"
    using c_end
    by auto 
  then have j_path: "path (c1 +++ (reversepath c))"
    using c1_end c1_simple c_simple unfolding simple_path_def path_def
    by (metis continuous_on_joinpaths path_def path_reversepath)
  then have "path ?j ∧ path_image ?j = path_image c1 ∪ path_image c" 
    using ‹pathstart (reversepath c) = b› c1_end path_image_join path_image_reversepath by blast
  then have "inside(path_image c1 ∪ path_image c) = inside(path_image ?j)"
    by auto
  have "pathstart (reversepath ?cc) = complex_of b"
    using cc_end
    by auto 
  then have cj_path: "path ?cj"
    using cc1_end cc1_simple cc_simple unfolding simple_path_def path_def
    by (metis continuous_on_joinpaths path_def path_reversepath)
  then have "path ?cj ∧ path_image ?cj = path_image ?cc1 ∪ path_image ?cc" 
    by (metis ‹pathstart (reversepath (complex_of ∘ c)) = complex_of b› cc1_end path_image_join path_image_reversepath)
  then have ins_cj: "inside(path_image ?cc1 ∪ path_image ?cc) = inside (path_image ?cj)"
    by auto
  have "inside(path_image ?cj) = complex_of ` (inside(path_image ?j))"
    using inside_bijective_linear_image[of ?j "complex_of"] j_path
    using cj_and_j complex_of_bij complex_of_linear by presburger
  then have i1: "inside(path_image ?cc1 ∪ path_image ?cc) = complex_of ` (inside(path_image c1 ∪ path_image c))" using complex_of_real_of unfolding image_comp
    using cj_and_j 
    by (simp add: ins_cj ‹inside (path_image c1 ∪ path_image c) = inside (path_image (c1 +++ reversepath c))›) 
 
  (* Very similar to the proof of i1 *)
  let ?j2 = "c2 +++ (reversepath c)"
  let ?cj2 = "?cc2 +++ (reversepath ?cc)"
  have cj2_and_j2: "path_image ?cj2 = complex_of ` (path_image ?j2)"
    by (metis path_compose_join path_compose_reversepath path_image_compose)
  have "pathstart (reversepath c) = b"
    using c_end by auto 
  then have j2_path: "path (c2 +++ (reversepath c))"
    using c2_end c2_simple c_simple unfolding simple_path_def path_def
    by (metis continuous_on_joinpaths path_def path_reversepath)
  then have "path ?j2 ∧ path_image ?j2 = path_image c2 ∪ path_image c"
    using ‹pathstart (reversepath c) = b› c2_end path_image_join path_image_reversepath by blast 
  then have "inside(path_image c2 ∪ path_image c) = inside(path_image ?j2)"
    by auto
  have "pathstart (reversepath ?cc) = complex_of b"
    using cc_end by auto 
  then have cj2_path: "path ?cj2"
    using cc2_end cc2_simple cc_simple unfolding simple_path_def path_def
    by (metis continuous_on_joinpaths path_def path_reversepath)
  then have "path ?cj2 ∧ path_image ?cj2 = path_image ?cc2 ∪ path_image ?cc" 
    by (metis ‹pathstart (reversepath (complex_of ∘ c)) = complex_of b› cc2_end path_image_join path_image_reversepath)
  then have ins_cj2: "inside(path_image ?cc2 ∪ path_image ?cc) = inside (path_image ?cj2)"
    by auto
  have "inside(path_image ?cj2) = complex_of ` (inside(path_image ?j2))"
    using inside_bijective_linear_image[of ?j2 "complex_of"] j2_path
    using cj2_and_j2 complex_of_bij complex_of_linear
    by presburger
  then have i2: "inside (path_image (complex_of ∘ c2) ∪ path_image (complex_of ∘ c))
        = complex_of ` inside (path_image c2 ∪ path_image c)"
    using cj2_and_j2 
    by (simp add: ins_cj2 ‹inside (path_image c2 ∪ path_image c) = inside (path_image (c2 +++ reversepath c))›) 

  (* Very similar to the proof of i1 *)
  let ?j3 = "c2 +++ (reversepath c1)"
  let ?cj3 = "?cc2 +++ (reversepath ?cc1)"
  have cj3_and_j3: "path_image ?cj3 = complex_of ` (path_image ?j3)"
    by (metis path_compose_join path_compose_reversepath path_image_compose)
  have "pathstart (reversepath c1) = b"
    using c1_end by auto 
  then have j3_path: "path (c2 +++ (reversepath c1))"
    using c2_end c2_simple c1_simple unfolding simple_path_def path_def
    by (metis continuous_on_joinpaths path_def path_reversepath)
  then have path_j3: "path ?j3 ∧ path_image ?j3 = path_image c2 ∪ path_image c1"
    using ‹pathstart (reversepath c1) = b› c2_end path_image_join path_image_reversepath by blast 
   then have "inside(path_image c2 ∪ path_image c1) = inside(path_image ?j3)"
    by auto
  have "pathstart (reversepath ?cc1) = complex_of b"
    using cc1_end by auto 
  then have cj3_path: "path ?cj3"
    using cc2_end cc2_simple cc1_simple unfolding simple_path_def path_def
    by (metis continuous_on_joinpaths path_def path_reversepath)
  then have path_cj3: "path ?cj3 ∧ path_image ?cj3 = path_image ?cc2 ∪ path_image ?cc1"  
    by (metis ‹pathstart (reversepath (complex_of ∘ c1)) = complex_of b› cc2_end path_image_join path_image_reversepath)
  then have ins_cj3: "inside(path_image ?cc2 ∪ path_image ?cc1) = inside (path_image ?cj3)"
    by auto
  have "inside(path_image ?cj3) = complex_of ` (inside(path_image ?j3))"
    using inside_bijective_linear_image[of ?j3 "complex_of"] j3_path
    using cj3_and_j3 complex_of_bij complex_of_linear
    by presburger
  then have i3: "inside (path_image (complex_of ∘ c1) ∪ path_image (complex_of ∘ c2))
      = complex_of ` inside (path_image c1 ∪ path_image c2)" 
    by (simp add: path_cj3 path_j3 sup_commute)
  obtain y where y_prop: "y ∈ path_image c ∩ inside (path_image c1 ∪ path_image c2)"
    using ne_12 by auto 
  then have y_in1: "complex_of y ∈ path_image ?cc"
    by (metis IntD1 image_eqI path_image_compose)
  have y_in2: "complex_of y ∈ complex_of ` (inside (path_image c1 ∪ path_image c2))"
    using y_prop by auto 
  then have cne_12: "path_image ?cc ∩ inside(path_image ?cc1 ∪ path_image ?cc2) ≠ {}"
    using ne_12 y_in1 y_in2 i3 by force
  obtain for_reals: "inside(path_image ?cc1 ∪ path_image ?cc) ∩ inside(path_image ?cc2 ∪ path_image ?cc) = {}"
          "inside(path_image ?cc1 ∪ path_image ?cc) ∪ inside(path_image ?cc2 ∪ path_image ?cc) ∪
           (path_image ?cc - {complex_of a, complex_of b}) = inside(path_image ?cc1 ∪ path_image ?cc2)"
    using split_inside_simple_closed_curve[OF cc1_simple cc1_start cc1_end cc2_simple cc2_start
      cc2_end cc_simple cc_start cc_end ca_neq_cb cc1c2 cc1c cc2c cne_12]
    by auto
  let ?rin1 = "real_of ` inside(path_image ?cc1 ∪ path_image ?cc)"
  let ?rin2 = "real_of ` inside(path_image ?cc2 ∪ path_image ?cc)"
  
  have h1: "inside(path_image c1 ∪ path_image c) ∩ inside(path_image c2 ∪ path_image c) ≠ {} ⟹ False"
  proof-
    assume "inside(path_image c1 ∪ path_image c) ∩ inside(path_image c2 ∪ path_image c) ≠ {}"
    then obtain a where a_prop: "a ∈ inside(path_image c1 ∪ path_image c) ∧ a ∈ inside(path_image c2 ∪ path_image c)"
      by auto
    have in1: "complex_of a ∈ inside (path_image (complex_of ∘ c1) ∪ path_image (complex_of ∘ c))"
      using a_prop i1 by auto
    have in2: "complex_of a ∈ inside (path_image (complex_of ∘ c2) ∪ path_image (complex_of ∘ c))"
      using a_prop i2 by auto
    show "False" using in1 in2 for_reals(1) by auto
  qed
  have h: "path_image (complex_of ∘ c) - {complex_of a, complex_of b} = complex_of ` (path_image c) - complex_of `{a,b}"
    using path_image_compose by auto
  have "complex_of ` path_image c - complex_of ` {a, b} = complex_of ` (path_image c - {a, b})"
  proof - 
    have "⋀x. x ∈ (complex_of ` path_image c - complex_of ` {a, b}) ⟷ x ∈ complex_of ` (path_image c - {a, b})"
      using Diff_iff bij_betw_imp_inj_on complex_of_bij image_iff inj_eq by (smt (z3))
    then show ?thesis by blast
  qed
  then have "path_image (complex_of ∘ c) - {complex_of a, complex_of b} = complex_of ` (path_image c - {a,b})"
    using h by simp
  then have h2: "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-
    have "⋀x . x ∈ inside(path_image c1 ∪ path_image c2) ⟷ complex_of x ∈ complex_of ` inside (path_image c1 ∪ path_image c2)"
      using i3 by (metis bij_betw_imp_inj_on complex_of_bij image_iff inj_eq)
    then have in_iff: "⋀x. x ∈ inside(path_image c1 ∪ path_image c2) ⟷ complex_of x ∈ inside (path_image (complex_of ∘ c1) ∪ path_image (complex_of ∘ c)) ∪
        inside (path_image (complex_of ∘ c2) ∪ path_image (complex_of ∘ c)) ∪
        (path_image (complex_of ∘ c) - {complex_of a, complex_of b})"
      using for_reals(2)
      using i3 by presburger
    have "⋀x. complex_of x ∈ inside (path_image (complex_of ∘ c1) ∪ path_image (complex_of ∘ c)) ∪
        inside (path_image (complex_of ∘ c2) ∪ path_image (complex_of ∘ c)) ∪
        (path_image (complex_of ∘ c) - {complex_of a, complex_of b})
        ⟷ complex_of x ∈ inside (path_image (complex_of ∘ c1) ∪ path_image (complex_of ∘ c))
          ∨ complex_of x ∈ inside (path_image (complex_of ∘ c2) ∪ path_image (complex_of ∘ c))
          ∨ complex_of x ∈ (path_image (complex_of ∘ c) - {complex_of a, complex_of b})"
      by blast
    then have "⋀x. complex_of x ∈ inside (path_image (complex_of ∘ c1) ∪ path_image (complex_of ∘ c)) ∪
        inside (path_image (complex_of ∘ c2) ∪ path_image (complex_of ∘ c)) ∪
        (path_image (complex_of ∘ c) - {complex_of a, complex_of b})
        ⟷ x ∈ inside(path_image c1 ∪ path_image c) ∪ inside(path_image c2 ∪ path_image c) ∪
           (path_image c - {a,b})"
      using i1 i2 i3 Un_iff ‹path_image (complex_of ∘ c) - {complex_of a, complex_of b} = complex_of ` (path_image c - {a, b})› bij_betw_imp_inj_on complex_of_bij image_iff inj_def
      by (smt (verit, best))
    then have "⋀x. x ∈ inside(path_image c1 ∪ path_image c2) ⟷ x ∈ (inside(path_image c1 ∪ path_image c) ∪ inside(path_image c2 ∪ path_image c) ∪
          (path_image c - {a,b}))"
      using in_iff by meson
    then show ?thesis by auto
qed
  show ?thesis using that h1 h2 by auto 
qed

lemma split_inside_simple_closed_curve_real2:
  fixes c :: "real ⇒ real^2"
  assumes c1_simple:"simple_path c1" and c1_start: "pathstart c1 = a" and c1_end: "pathfinish c1 = b"
  assumes c2_simple: "simple_path c2" and c2_start: "pathstart c2 = a" and c2_end: "pathfinish c2 = b"
  assumes c_simple: "simple_path c" and c_start: "pathstart c = a" and c_end: "pathfinish c = b"
  assumes a_neq_b: "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 - 
  have good_type: "c1_on_open_R2_axioms TYPE((real, 2) vec)"
    unfolding c1_on_open_R2_axioms_def by auto
  then show ?thesis
    using c1_on_open_R2.split_inside_simple_closed_curve_locale[of _ _ _ c1 a b c2 c] assms
    unfolding c1_on_open_R2_def c1_on_open_euclidean_def c1_on_open_def 
    using good_type that by blast
qed

end