Quelle Path_Connected.thy Sprache: Isabelle

(*  Title:      HOL/Analysis/Path_Connected.thy
    Authors:    LC Paulson and Robert Himmelmann (TU Muenchen), based on material from HOL Light
*)

section \<open>Path-Connectedness\<close>

theory Path_Connected
imports
  Starlike
  T1_Spaces
begin

subsection \<open>Paths and Arcs\<close>

definition\<^marker>\<open>tag important\<close> path :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> bool"
  where "path g \ continuous_on {0..1} g"

definition\<^marker>\<open>tag important\<close> pathstart :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> 'a"
  where "pathstart g \ g 0"

definition\<^marker>\<open>tag important\<close> pathfinish :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> 'a"
  where "pathfinish g \ g 1"

definition\<^marker>\<open>tag important\<close> path_image :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> 'a set"
  where "path_image g \ g ` {0 .. 1}"

definition\<^marker>\<open>tag important\<close> reversepath :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> real \<Rightarrow> 'a"
  where "reversepath g \ (\x. g(1 - x))"

definition\<^marker>\<open>tag important\<close> joinpaths :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> real \<Rightarrow> 'a"
    (infixr \<open>+++\<close> 75)
  where "g1 +++ g2 \ (\x. if x \ 1/2 then g1 (2 * x) else g2 (2 * x - 1))"

definition\<^marker>\<open>tag important\<close> loop_free :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> bool"
  where "loop_free g \ \x\{0..1}. \y\{0..1}. g x = g y \ x = y \ x = 0 \ y = 1 \ x = 1 \ y = 0"

definition\<^marker>\<open>tag important\<close> simple_path :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> bool"
  where "simple_path g \ path g \ loop_free g"

definition\<^marker>\<open>tag important\<close> arc :: "(real \<Rightarrow> 'a :: topological_space) \<Rightarrow> bool"
  where "arc g \ path g \ inj_on g {0..1}"

subsection\<^marker>\<open>tag unimportant\<close>\<open>Invariance theorems\<close>

lemma path_eq: "path p \ (\t. t \ {0..1} \ p t = q t) \ path q"
  using continuous_on_eq path_def by blast

lemma path_continuous_image: "path g \ continuous_on (path_image g) f \ path(f \ g)"
  unfolding path_def path_image_def
  using continuous_on_compose by blast

lemma path_translation_eq:
  fixes g :: "real \ 'a :: real_normed_vector"
  shows "path((\x. a + x) \ g) = path g"
  using continuous_on_translation_eq path_def by blast

lemma path_linear_image_eq:
  fixes f :: "'a::euclidean_space \ 'b::euclidean_space"
   assumes "linear f" "inj f"
     shows "path(f \ g) = path g"
proof -
  from linear_injective_left_inverse [OF assms]
  obtain h where h: "linear h" "h \ f = id"
    by blast
  with assms show ?thesis
    by (metis comp_assoc id_comp linear_continuous_on linear_linear path_continuous_image)
qed

lemma pathstart_translation: "pathstart((\x. a + x) \ g) = a + pathstart g"
  by (simp add: pathstart_def)

lemma pathstart_linear_image_eq: "linear f \ pathstart(f \ g) = f(pathstart g)"
  by (simp add: pathstart_def)

lemma pathfinish_translation: "pathfinish((\x. a + x) \ g) = a + pathfinish g"
  by (simp add: pathfinish_def)

lemma pathfinish_linear_image: "linear f \ pathfinish(f \ g) = f(pathfinish g)"
  by (simp add: pathfinish_def)

lemma path_image_translation: "path_image((\x. a + x) \ g) = (\x. a + x) ` (path_image g)"
  by (simp add: image_comp path_image_def)

lemma path_image_linear_image: "linear f \ path_image(f \ g) = f ` (path_image g)"
  by (simp add: image_comp path_image_def)

lemma reversepath_translation: "reversepath((\x. a + x) \ g) = (\x. a + x) \ reversepath g"
  by (rule ext) (simp add: reversepath_def)

lemma reversepath_linear_image: "linear f \ reversepath(f \ g) = f \ reversepath g"
  by (rule ext) (simp add: reversepath_def)

lemma joinpaths_translation:
    "((\x. a + x) \ g1) +++ ((\x. a + x) \ g2) = (\x. a + x) \ (g1 +++ g2)"
  by (rule ext) (simp add: joinpaths_def)

lemma joinpaths_linear_image: "linear f \ (f \ g1) +++ (f \ g2) = f \ (g1 +++ g2)"
  by (rule ext) (simp add: joinpaths_def)

lemma loop_free_translation_eq:
  fixes g :: "real \ 'a::euclidean_space"
  shows "loop_free((\x. a + x) \ g) = loop_free g"
  by (simp add: loop_free_def)

lemma simple_path_translation_eq:
  fixes g :: "real \ 'a::euclidean_space"
  shows "simple_path((\x. a + x) \ g) = simple_path g"
  by (simp add: simple_path_def loop_free_translation_eq path_translation_eq)

lemma loop_free_linear_image_eq:
  fixes f :: "'a::euclidean_space \ 'b::euclidean_space"
  assumes "linear f" "inj f"
    shows "loop_free(f \ g) = loop_free g"
  using assms inj_on_eq_iff [of f] by (auto simp: loop_free_def)

lemma simple_path_linear_image_eq:
  fixes f :: "'a::euclidean_space \ 'b::euclidean_space"
  assumes "linear f" "inj f"
    shows "simple_path(f \ g) = simple_path g"
  using assms
  by (simp add: loop_free_linear_image_eq path_linear_image_eq simple_path_def)

lemma simple_pathI [intro?]:
  assumes "path p"
  assumes "\x y. 0 \ x \ x < y \ y \ 1 \ p x = p y \ x = 0 \ y = 1"
  shows   "simple_path p"
  unfolding simple_path_def loop_free_def
proof (intro ballI conjI impI)
  fix x y assume "x \ {0..1}" "y \ {0..1}" "p x = p y"
  thus "x = y \ x = 0 \ y = 1 \ x = 1 \ y = 0"
    by (metis assms(2) atLeastAtMost_iff linorder_less_linear)
qed fact+

lemma arcD: "arc p \ p x = p y \ x \ {0..1} \ y \ {0..1} \ x = y"
  by (auto simp: arc_def inj_on_def)

lemma arc_translation_eq:
  fixes g :: "real \ 'a::euclidean_space"
  shows "arc((\x. a + x) \ g) \ arc g"
  by (auto simp: arc_def inj_on_def path_translation_eq)

lemma arc_linear_image_eq:
  fixes f :: "'a::euclidean_space \ 'b::euclidean_space"
   assumes "linear f" "inj f"
     shows  "arc(f \ g) = arc g"
  using assms inj_on_eq_iff [of f]
  by (auto simp: arc_def inj_on_def path_linear_image_eq)

subsection\<^marker>\<open>tag unimportant\<close>\<open>Basic lemmas about paths\<close>

lemma path_of_real: "path complex_of_real"
  unfolding path_def by (intro continuous_intros)

lemma path_const: "path (\t. a)" for a::"'a::real_normed_vector"
  unfolding path_def by (intro continuous_intros)

lemma path_minus: "path g \ path (\t. - g t)" for g::"real\'a::real_normed_vector"
  unfolding path_def by (intro continuous_intros)

lemma path_add: "\path f; path g\ \ path (\t. f t + g t)" for f::"real\'a::real_normed_vector"
  unfolding path_def by (intro continuous_intros)

lemma path_diff: "\path f; path g\ \ path (\t. f t - g t)" for f::"real\'a::real_normed_vector"
  unfolding path_def by (intro continuous_intros)

lemma path_mult: "\path f; path g\ \ path (\t. f t * g t)" for f::"real\'a::real_normed_field"
  unfolding path_def by (intro continuous_intros)

lemma pathin_iff_path_real [simp]: "pathin euclideanreal g \ path g"
  by (simp add: pathin_def path_def)

lemma continuous_on_path: "path f \ t \ {0..1} \ continuous_on t f"
  using continuous_on_subset path_def by blast

lemma inj_on_imp_loop_free: "inj_on g {0..1} \ loop_free g"
  by (simp add: inj_onD loop_free_def)

lemma arc_imp_simple_path: "arc g \ simple_path g"
  by (simp add: arc_def inj_on_imp_loop_free simple_path_def)

lemma arc_imp_path: "arc g \ path g"
  using arc_def by blast

lemma arc_imp_inj_on: "arc g \ inj_on g {0..1}"
  by (auto simp: arc_def)

lemma simple_path_imp_path: "simple_path g \ path g"
  using simple_path_def by blast

lemma loop_free_cases: "loop_free g \ inj_on g {0..1} \ pathfinish g = pathstart g"
  by (force simp: inj_on_def loop_free_def pathfinish_def pathstart_def)

lemma simple_path_cases: "simple_path g \ arc g \ pathfinish g = pathstart g"
  using arc_def loop_free_cases simple_path_def by blast

lemma simple_path_imp_arc: "simple_path g \ pathfinish g \ pathstart g \ arc g"
  using simple_path_cases by auto

lemma arc_distinct_ends: "arc g \ pathfinish g \ pathstart g"
  unfolding arc_def inj_on_def pathfinish_def pathstart_def
  by fastforce

lemma arc_simple_path: "arc g \ simple_path g \ pathfinish g \ pathstart g"
  using arc_distinct_ends arc_imp_simple_path simple_path_cases by blast

lemma simple_path_eq_arc: "pathfinish g \ pathstart g \ (simple_path g = arc g)"
  by (simp add: arc_simple_path)

lemma path_image_const [simp]: "path_image (\t. a) = {a}"
  by (force simp: path_image_def)

lemma path_image_nonempty [simp]: "path_image g \ {}"
  unfolding path_image_def image_is_empty box_eq_empty
  by auto

lemma pathstart_in_path_image[intro]: "pathstart g \ path_image g"
  unfolding pathstart_def path_image_def
  by auto

lemma pathfinish_in_path_image[intro]: "pathfinish g \ path_image g"
  unfolding pathfinish_def path_image_def
  by auto

lemma connected_path_image[intro]: "path g \ connected (path_image g)"
  unfolding path_def path_image_def
  using connected_continuous_image connected_Icc by blast

lemma compact_path_image[intro]: "path g \ compact (path_image g)"
  unfolding path_def path_image_def
  using compact_continuous_image connected_Icc by blast

lemma reversepath_reversepath[simp]: "reversepath (reversepath g) = g"
  unfolding reversepath_def
  by auto

lemma pathstart_reversepath[simp]: "pathstart (reversepath g) = pathfinish g"
  unfolding pathstart_def reversepath_def pathfinish_def
  by auto

lemma pathfinish_reversepath[simp]: "pathfinish (reversepath g) = pathstart g"
  unfolding pathstart_def reversepath_def pathfinish_def
  by auto

lemma reversepath_o: "reversepath g = g \ (-)1"
  by (auto simp: reversepath_def)

lemma pathstart_join[simp]: "pathstart (g1 +++ g2) = pathstart g1"
  unfolding pathstart_def joinpaths_def pathfinish_def
  by auto

lemma pathfinish_join[simp]: "pathfinish (g1 +++ g2) = pathfinish g2"
  unfolding pathstart_def joinpaths_def pathfinish_def
  by auto

lemma path_image_reversepath[simp]: "path_image (reversepath g) = path_image g"
  by (metis cancel_comm_monoid_add_class.diff_cancel diff_zero image_comp
      image_diff_atLeastAtMost path_image_def reversepath_o)

lemma path_reversepath [simp]: "path (reversepath g) \ path g"
  by (metis continuous_on_compose continuous_on_op_minus image_comp image_ident path_def path_image_def path_image_reversepath reversepath_o reversepath_reversepath)

lemma arc_reversepath:
  assumes "arc g" shows "arc(reversepath g)"
proof -
  have injg: "inj_on g {0..1}"
    using assms
    by (simp add: arc_def)
  have **: "\x y::real. 1-x = 1-y \ x = y"
    by simp
  show ?thesis
    using assms  by (clarsimp simp: arc_def intro!: inj_onI) (simp add: inj_onD reversepath_def **)
qed

lemma loop_free_reversepath:
  assumes "loop_free g" shows "loop_free(reversepath g)"
  using assms by (simp add: reversepath_def loop_free_def Ball_def) (smt (verit))

lemma simple_path_reversepath: "simple_path g \ simple_path (reversepath g)"
  by (simp add: loop_free_reversepath simple_path_def)

lemmas reversepath_simps =
  path_reversepath path_image_reversepath pathstart_reversepath pathfinish_reversepath

lemma path_join[simp]:
  assumes "pathfinish g1 = pathstart g2"
  shows "path (g1 +++ g2) \ path g1 \ path g2"
  unfolding path_def pathfinish_def pathstart_def
proof safe
  assume cont: "continuous_on {0..1} (g1 +++ g2)"
  have g1: "continuous_on {0..1} g1 \ continuous_on {0..1} ((g1 +++ g2) \ (\x. x / 2))"
    by (intro continuous_on_cong refl) (auto simp: joinpaths_def)
  have g2: "continuous_on {0..1} g2 \ continuous_on {0..1} ((g1 +++ g2) \ (\x. x / 2 + 1/2))"
    using assms
    by (intro continuous_on_cong refl) (auto simp: joinpaths_def pathfinish_def pathstart_def)
  show "continuous_on {0..1} g1" and "continuous_on {0..1} g2"
    unfolding g1 g2
    by (auto intro!: continuous_intros continuous_on_subset[OF cont] simp del: o_apply)
next
  assume g1g2: "continuous_on {0..1} g1" "continuous_on {0..1} g2"
  have 01: "{0 .. 1} = {0..1/2} \ {1/2 .. 1::real}"
    by auto
  {
    fix x :: real
    assume "0 \ x" and "x \ 1"
    then have "x \ (\x. x * 2) ` {0..1 / 2}"
      by (intro image_eqI[where x="x/2"]) auto
  }
  note 1 = this
  {
    fix x :: real
    assume "0 \ x" and "x \ 1"
    then have "x \ (\x. x * 2 - 1) ` {1 / 2..1}"
      by (intro image_eqI[where x="x/2 + 1/2"]) auto
  }
  note 2 = this
  show "continuous_on {0..1} (g1 +++ g2)"
    using assms
    unfolding joinpaths_def 01
    apply (intro continuous_on_cases closed_atLeastAtMost g1g2[THEN continuous_on_compose2] continuous_intros)
    apply (auto simp: field_simps pathfinish_def pathstart_def intro!: 1 2)
    done
qed

subsection\<^marker>\<open>tag unimportant\<close> \<open>Path Images\<close>

lemma bounded_path_image: "path g \ bounded(path_image g)"
  by (simp add: compact_imp_bounded compact_path_image)

lemma closed_path_image:
  fixes g :: "real \ 'a::t2_space"
  shows "path g \ closed(path_image g)"
  by (metis compact_path_image compact_imp_closed)

lemma connected_simple_path_image: "simple_path g \ connected(path_image g)"
  by (metis connected_path_image simple_path_imp_path)

lemma compact_simple_path_image: "simple_path g \ compact(path_image g)"
  by (metis compact_path_image simple_path_imp_path)

lemma bounded_simple_path_image: "simple_path g \ bounded(path_image g)"
  by (metis bounded_path_image simple_path_imp_path)

lemma closed_simple_path_image:
  fixes g :: "real \ 'a::t2_space"
  shows "simple_path g \ closed(path_image g)"
  by (metis closed_path_image simple_path_imp_path)

lemma connected_arc_image: "arc g \ connected(path_image g)"
  by (metis connected_path_image arc_imp_path)

lemma compact_arc_image: "arc g \ compact(path_image g)"
  by (metis compact_path_image arc_imp_path)

lemma bounded_arc_image: "arc g \ bounded(path_image g)"
  by (metis bounded_path_image arc_imp_path)

lemma closed_arc_image:
  fixes g :: "real \ 'a::t2_space"
  shows "arc g \ closed(path_image g)"
  by (metis closed_path_image arc_imp_path)

lemma path_image_join_subset: "path_image (g1 +++ g2) \ path_image g1 \ path_image g2"
  unfolding path_image_def joinpaths_def
  by auto

lemma subset_path_image_join:
  assumes "path_image g1 \ S" and "path_image g2 \ S"
  shows "path_image (g1 +++ g2) \ S"
  using path_image_join_subset[of g1 g2] and assms
  by auto

lemma path_image_join:
  assumes "pathfinish g1 = pathstart g2"
  shows "path_image(g1 +++ g2) = path_image g1 \ path_image g2"
proof -
  have "path_image g1 \ path_image (g1 +++ g2)"
  proof (clarsimp simp: path_image_def joinpaths_def)
    fix u::real
    assume "0 \ u" "u \ 1"
    then show "g1 u \ (\x. g1 (2 * x)) ` ({0..1} \ {x. x * 2 \ 1})"
      by (rule_tac x="u/2" in image_eqI) auto
  qed
  moreover
  have \<section>: "g2 u \<in> (\<lambda>x. g2 (2 * x - 1)) ` ({0..1} \<inter> {x. \<not> x * 2 \<le> 1})"
    if "0 < u" "u \ 1" for u
    using that assms
    by (rule_tac x="(u+1)/2" in image_eqI) (auto simp: field_simps pathfinish_def pathstart_def)
  have "g2 0 \ (\x. g1 (2 * x)) ` ({0..1} \ {x. x * 2 \ 1})"
    using assms
    by (rule_tac x="1/2" in image_eqI) (auto simp: pathfinish_def pathstart_def)
  then have "path_image g2 \ path_image (g1 +++ g2)"
    by (auto simp: path_image_def joinpaths_def intro!: \<section>)
  ultimately show ?thesis
    using path_image_join_subset by blast
qed

lemma not_in_path_image_join:
  assumes "x \ path_image g1" and "x \ path_image g2"
  shows "x \ path_image (g1 +++ g2)"
  using assms and path_image_join_subset[of g1 g2]
  by auto

lemma pathstart_compose: "pathstart(f \ p) = f(pathstart p)"
  by (simp add: pathstart_def)

lemma pathfinish_compose: "pathfinish(f \ p) = f(pathfinish p)"
  by (simp add: pathfinish_def)

lemma path_image_compose: "path_image (f \ p) = f ` (path_image p)"
  by (simp add: image_comp path_image_def)

lemma path_compose_join: "f \ (p +++ q) = (f \ p) +++ (f \ q)"
  by (rule ext) (simp add: joinpaths_def)

lemma path_compose_reversepath: "f \ reversepath p = reversepath(f \ p)"
  by (rule ext) (simp add: reversepath_def)

lemma joinpaths_eq:
  "(\t. t \ {0..1} \ p t = p' t) \
   (\<And>t. t \<in> {0..1} \<Longrightarrow> q t = q' t)
   \<Longrightarrow>  t \<in> {0..1} \<Longrightarrow> (p +++ q) t = (p' +++ q') t"
  by (auto simp: joinpaths_def)

lemma loop_free_inj_on: "loop_free g \ inj_on g {0<..<1}"
  by (force simp: inj_on_def loop_free_def)

lemma simple_path_inj_on: "simple_path g \ inj_on g {0<..<1}"
  using loop_free_inj_on simple_path_def by auto

subsection\<^marker>\<open>tag unimportant\<close>\<open>Simple paths with the endpoints removed\<close>

lemma simple_path_endless:
  assumes "simple_path c"
  shows "path_image c - {pathstart c,pathfinish c} = c ` {0<..<1}" (is "?lhs = ?rhs")
proof
  show "?lhs \ ?rhs"
    using less_eq_real_def by (auto simp: path_image_def pathstart_def pathfinish_def)
  show "?rhs \ ?lhs"
    using assms
    apply (simp add: image_subset_iff path_image_def pathstart_def pathfinish_def simple_path_def loop_free_def Ball_def)
    by (smt (verit))
qed

lemma connected_simple_path_endless:
  assumes "simple_path c"
  shows "connected(path_image c - {pathstart c,pathfinish c})"
proof -
  have "continuous_on {0<..<1} c"
    using assms by (simp add: simple_path_def continuous_on_path path_def subset_iff)
  then have "connected (c ` {0<..<1})"
    using connected_Ioo connected_continuous_image by blast
  then show ?thesis
    using assms by (simp add: simple_path_endless)
qed

lemma nonempty_simple_path_endless:
    "simple_path c \ path_image c - {pathstart c,pathfinish c} \ {}"
  by (simp add: simple_path_endless)

lemma simple_path_continuous_image:
  assumes "simple_path f" "continuous_on (path_image f) g" "inj_on g (path_image f)"
  shows   "simple_path (g \ f)"
  unfolding simple_path_def
proof
  show "path (g \ f)"
    using assms unfolding simple_path_def by (intro path_continuous_image) auto
  from assms have [simp]: "g (f x) = g (f y) \ f x = f y" if "x \ {0..1}" "y \ {0..1}" for x y
    unfolding inj_on_def path_image_def using that by fastforce
  show "loop_free (g \ f)"
    using assms(1) by (auto simp: loop_free_def simple_path_def)
qed

subsection\<^marker>\<open>tag unimportant\<close>\<open>The operations on paths\<close>

lemma path_image_subset_reversepath: "path_image(reversepath g) \ path_image g"
  by simp

lemma path_imp_reversepath: "path g \ path(reversepath g)"
  by simp

lemma half_bounded_equal: "1 \ x * 2 \ x * 2 \ 1 \ x = (1/2::real)"
  by simp

lemma continuous_on_joinpaths:
  assumes "continuous_on {0..1} g1" "continuous_on {0..1} g2" "pathfinish g1 = pathstart g2"
    shows "continuous_on {0..1} (g1 +++ g2)"
  using assms path_def path_join by blast

lemma path_join_imp: "\path g1; path g2; pathfinish g1 = pathstart g2\ \ path(g1 +++ g2)"
  by simp

lemma arc_join:
  assumes "arc g1" "arc g2"
          "pathfinish g1 = pathstart g2"
          "path_image g1 \ path_image g2 \ {pathstart g2}"
    shows "arc(g1 +++ g2)"
proof -
  have injg1: "inj_on g1 {0..1}" and injg2: "inj_on g2 {0..1}"
     and g11: "g1 1 = g2 0" and sb: "g1 ` {0..1} \ g2 ` {0..1} \ {g2 0}"
    using assms
    by (auto simp: arc_def pathfinish_def pathstart_def path_image_def)
  { fix x and y::real
    assume xy: "g2 (2 * x - 1) = g1 (2 * y)" "x \ 1" "0 \ y" " y * 2 \ 1" "\ x * 2 \ 1"
    then have "g1 (2 * y) = g2 0"
      using sb by force
    then have False
      using xy inj_onD injg2 by fastforce
   } note * = this
  have "inj_on (g1 +++ g2) {0..1}"
    using inj_onD [OF injg1] inj_onD [OF injg2] *
    by (simp add: inj_on_def joinpaths_def Ball_def) (smt (verit))
  then show ?thesis
    using arc_def assms path_join_imp by blast
qed

lemma simple_path_join_loop:
  assumes "arc g1" "arc g2"
          "pathfinish g1 = pathstart g2"  "pathfinish g2 = pathstart g1"
          "path_image g1 \ path_image g2 \ {pathstart g1, pathstart g2}"
        shows "simple_path(g1 +++ g2)"
proof -
  have injg1: "inj_on g1 {0..1}" and injg2: "inj_on g2 {0..1}"
    using assms by (auto simp add: arc_def)
  have g12: "g1 1 = g2 0"
   and g21: "g2 1 = g1 0"
   and sb:  "g1 ` {0..1} \ g2 ` {0..1} \ {g1 0, g2 0}"
    using assms
    by (simp_all add: arc_def pathfinish_def pathstart_def path_image_def)
  { fix x and y::real
    assume g2_eq: "g2 (2 * x - 1) = g1 (2 * y)"
      and xyI: "x \ 1 \ y \ 0"
      and xy: "x \ 1" "0 \ y" " y * 2 \ 1" "\ x * 2 \ 1"
    then consider "g1 (2 * y) = g1 0" | "g1 (2 * y) = g2 0"
      using sb by force
    then have False
    proof cases
      case 1
      then have "y = 0"
        using xy g2_eq by (auto dest!: inj_onD [OF injg1])
      then show ?thesis
        using xy g2_eq xyI by (auto dest: inj_onD [OF injg2] simp flip: g21)
    next
      case 2
      then have "2*x = 1"
        using g2_eq g12 inj_onD [OF injg2] atLeastAtMost_iff xy(1) xy(4) by fastforce
      with xy show False by auto
    qed
  } note * = this
  have "loop_free(g1 +++ g2)"
    using inj_onD [OF injg1] inj_onD [OF injg2] *
    by (simp add: loop_free_def joinpaths_def Ball_def) (smt (verit))
  then show ?thesis
    by (simp add: arc_imp_path assms simple_path_def)
qed

lemma reversepath_joinpaths:
    "pathfinish g1 = pathstart g2 \ reversepath(g1 +++ g2) = reversepath g2 +++ reversepath g1"
  unfolding reversepath_def pathfinish_def pathstart_def joinpaths_def
  by (rule ext) (auto simp: mult.commute)

subsection\<^marker>\<open>tag unimportant\<close>\<open>Some reversed and "if and only if" versions of joining theorems\<close>

lemma path_join_path_ends:
  fixes g1 :: "real \ 'a::metric_space"
  assumes "path(g1 +++ g2)" "path g2"
    shows "pathfinish g1 = pathstart g2"
proof (rule ccontr)
  define e where "e = dist (g1 1) (g2 0)"
  assume Neg: "pathfinish g1 \ pathstart g2"
  then have "0 < dist (pathfinish g1) (pathstart g2)"
    by auto
  then have "e > 0"
    by (metis e_def pathfinish_def pathstart_def)
  then have "\e>0. \d>0. \x'\{0..1}. dist x' 0 < d \ dist (g2 x') (g2 0) < e"
    using \<open>path g2\<close> atLeastAtMost_iff zero_le_one unfolding path_def continuous_on_iff
    by blast
  then obtain d1 where "d1 > 0"
       and d1: "\x'. \x'\{0..1}; norm x' < d1\ \ dist (g2 x') (g2 0) < e/2"
    by (metis \<open>0 < e\<close> half_gt_zero_iff norm_conv_dist)
  obtain d2 where "d2 > 0"
       and d2: "\x'. \x'\{0..1}; dist x' (1/2) < d2\
                      \<Longrightarrow> dist ((g1 +++ g2) x') (g1 1) < e/2"
    using assms(1) \<open>e > 0\<close> unfolding path_def continuous_on_iff
    apply (drule_tac x="1/2" in bspec, simp)
    apply (drule_tac x="e/2" in spec, force simp: joinpaths_def)
    done
  have int01_1: "min (1/2) (min d1 d2) / 2 \ {0..1}"
    using \<open>d1 > 0\<close> \<open>d2 > 0\<close> by (simp add: min_def)
  have dist1: "norm (min (1 / 2) (min d1 d2) / 2) < d1"
    using \<open>d1 > 0\<close> \<open>d2 > 0\<close> by (simp add: min_def dist_norm)
  have int01_2: "1/2 + min (1/2) (min d1 d2) / 4 \ {0..1}"
    using \<open>d1 > 0\<close> \<open>d2 > 0\<close> by (simp add: min_def)
  have dist2: "dist (1 / 2 + min (1 / 2) (min d1 d2) / 4) (1 / 2) < d2"
    using \<open>d1 > 0\<close> \<open>d2 > 0\<close> by (simp add: min_def dist_norm)
  have [simp]: "\ min (1 / 2) (min d1 d2) \ 0"
    using \<open>d1 > 0\<close> \<open>d2 > 0\<close> by (simp add: min_def)
  have "dist (g2 (min (1 / 2) (min d1 d2) / 2)) (g1 1) < e/2"
       "dist (g2 (min (1 / 2) (min d1 d2) / 2)) (g2 0) < e/2"
    using d1 [OF int01_1 dist1] d2 [OF int01_2 dist2] by (simp_all add: joinpaths_def)
  then have "dist (g1 1) (g2 0) < e/2 + e/2"
    using dist_triangle_half_r e_def by blast
  then show False
    by (simp add: e_def [symmetric])
qed

lemma path_join_eq [simp]:
  fixes g1 :: "real \ 'a::metric_space"
  assumes "path g1" "path g2"
    shows "path(g1 +++ g2) \ pathfinish g1 = pathstart g2"
  using assms by (metis path_join_path_ends path_join_imp)

lemma simple_path_joinE:
  assumes "simple_path(g1 +++ g2)" and "pathfinish g1 = pathstart g2"
  obtains "arc g1" "arc g2"
          "path_image g1 \ path_image g2 \ {pathstart g1, pathstart g2}"
proof -
  have *: "\x y. \0 \ x; x \ 1; 0 \ y; y \ 1; (g1 +++ g2) x = (g1 +++ g2) y\
               \<Longrightarrow> x = y \<or> x = 0 \<and> y = 1 \<or> x = 1 \<and> y = 0"
    using assms by (simp add: simple_path_def loop_free_def)
  have "path g1"
    using assms path_join simple_path_imp_path by blast
  moreover have "inj_on g1 {0..1}"
  proof (clarsimp simp: inj_on_def)
    fix x y
    assume "g1 x = g1 y" "0 \ x" "x \ 1" "0 \ y" "y \ 1"
    then show "x = y"
      using * [of "x/2" "y/2"] by (simp add: joinpaths_def split_ifs)
  qed
  ultimately have "arc g1"
    using assms  by (simp add: arc_def)
  have [simp]: "g2 0 = g1 1"
    using assms by (metis pathfinish_def pathstart_def)
  have "path g2"
    using assms path_join simple_path_imp_path by blast
  moreover have "inj_on g2 {0..1}"
  proof (clarsimp simp: inj_on_def)
    fix x y
    assume "g2 x = g2 y" "0 \ x" "x \ 1" "0 \ y" "y \ 1"
    then show "x = y"
      using * [of "(x+1) / 2" "(y+1) / 2"]
      by (force simp: joinpaths_def split_ifs field_split_simps)
  qed
  ultimately have "arc g2"
    using assms  by (simp add: arc_def)
  have "g2 y = g1 0 \ g2 y = g1 1"
       if "g1 x = g2 y" "0 \ x" "x \ 1" "0 \ y" "y \ 1" for x y
      using * [of "x / 2" "(y + 1) / 2"] that
      by (auto simp: joinpaths_def split_ifs field_split_simps)
  then have "path_image g1 \ path_image g2 \ {pathstart g1, pathstart g2}"
    by (fastforce simp: pathstart_def pathfinish_def path_image_def)
  with \<open>arc g1\<close> \<open>arc g2\<close> show ?thesis using that by blast
qed

lemma simple_path_join_loop_eq:
  assumes "pathfinish g2 = pathstart g1" "pathfinish g1 = pathstart g2"
  shows "simple_path(g1 +++ g2) \
             arc g1 \<and> arc g2 \<and> path_image g1 \<inter> path_image g2 \<subseteq> {pathstart g1, pathstart g2}"
  by (metis assms simple_path_joinE simple_path_join_loop)

lemma arc_join_eq:
  assumes "pathfinish g1 = pathstart g2"
    shows "arc(g1 +++ g2) \
           arc g1 \<and> arc g2 \<and> path_image g1 \<inter> path_image g2 \<subseteq> {pathstart g2}"
           (is "?lhs = ?rhs")
proof
  assume ?lhs then show ?rhs
    using reversepath_simps assms
    by (smt (verit, best) Int_commute arc_reversepath arc_simple_path in_mono insertE pathstart_join
          reversepath_joinpaths simple_path_joinE subsetI)
next
  assume ?rhs then show ?lhs
    using assms
    by (fastforce simp: pathfinish_def pathstart_def intro!: arc_join)
qed

lemma arc_join_eq_alt:
  "pathfinish g1 = pathstart g2
   \<Longrightarrow> arc(g1 +++ g2) \<longleftrightarrow> arc g1 \<and> arc g2 \<and> path_image g1 \<inter> path_image g2 = {pathstart g2}"
  using pathfinish_in_path_image by (fastforce simp: arc_join_eq)

subsubsection\<^marker>\<open>tag unimportant\<close>\<open>Symmetry and loops\<close>

lemma path_sym:
  "\pathfinish p = pathstart q; pathfinish q = pathstart p\ \ path(p +++ q) \ path(q +++ p)"
  by auto

lemma simple_path_sym:
  "\pathfinish p = pathstart q; pathfinish q = pathstart p\
     \<Longrightarrow> simple_path(p +++ q) \<longleftrightarrow> simple_path(q +++ p)"
  by (metis (full_types) inf_commute insert_commute simple_path_joinE simple_path_join_loop)

lemma path_image_sym:
  "\pathfinish p = pathstart q; pathfinish q = pathstart p\
     \<Longrightarrow> path_image(p +++ q) = path_image(q +++ p)"
  by (simp add: path_image_join sup_commute)

lemma simple_path_joinI:
  assumes "arc p1" "arc p2" "pathfinish p1 = pathstart p2"
  assumes "path_image p1 \ path_image p2
        \<subseteq> insert (pathstart p2) (if pathstart p1 = pathfinish p2 then {pathstart p1} else {})"
  shows   "simple_path (p1 +++ p2)"
  by (smt (verit, best) Int_commute arc_imp_simple_path arc_join assms insert_commute simple_path_join_loop simple_path_sym)

lemma simple_path_join3I:
  assumes "arc p1" "arc p2" "arc p3"
  assumes "path_image p1 \ path_image p2 \ {pathstart p2}"
  assumes "path_image p2 \ path_image p3 \ {pathstart p3}"
  assumes "path_image p1 \ path_image p3 \ {pathstart p1} \ {pathfinish p3}"
  assumes "pathfinish p1 = pathstart p2" "pathfinish p2 = pathstart p3"
  shows   "simple_path (p1 +++ p2 +++ p3)"
  using assms by (intro simple_path_joinI arc_join) (auto simp: path_image_join)

subsection\<^marker>\<open>tag unimportant\<close>\<open>The joining of paths is associative\<close>

lemma path_assoc:
  "\pathfinish p = pathstart q; pathfinish q = pathstart r\
     \<Longrightarrow> path(p +++ (q +++ r)) \<longleftrightarrow> path((p +++ q) +++ r)"
  by simp

lemma simple_path_assoc:
  assumes "pathfinish p = pathstart q" "pathfinish q = pathstart r"
    shows "simple_path (p +++ (q +++ r)) \ simple_path ((p +++ q) +++ r)"
proof (cases "pathstart p = pathfinish r")
  case True show ?thesis
  proof
    assume "simple_path (p +++ q +++ r)"
    with assms True show "simple_path ((p +++ q) +++ r)"
      by (fastforce simp add: simple_path_join_loop_eq arc_join_eq path_image_join
                    dest: arc_distinct_ends [of r])
  next
    assume 0: "simple_path ((p +++ q) +++ r)"
    with assms True have q: "pathfinish r \ path_image q"
      using arc_distinct_ends
      by (fastforce simp add: simple_path_join_loop_eq arc_join_eq path_image_join)
    have "pathstart r \ path_image p"
      using assms
      by (metis 0 IntI arc_distinct_ends arc_join_eq_alt empty_iff insert_iff
              pathfinish_in_path_image pathfinish_join simple_path_joinE)
    with assms 0 q True show "simple_path (p +++ q +++ r)"
      by (auto simp: simple_path_join_loop_eq arc_join_eq path_image_join
               dest!: subsetD [OF _ IntI])
  qed
next
  case False
  { fix x :: 'a
    assume a: "path_image p \ path_image q \ {pathstart q}"
              "(path_image p \ path_image q) \ path_image r \ {pathstart r}"
              "x \ path_image p" "x \ path_image r"
    have "pathstart r \ path_image q"
      by (metis assms(2) pathfinish_in_path_image)
    with a have "x = pathstart q"
      by blast
  }
  with False assms show ?thesis
    by (auto simp: simple_path_eq_arc simple_path_join_loop_eq arc_join_eq path_image_join)
qed

lemma arc_assoc:
     "\pathfinish p = pathstart q; pathfinish q = pathstart r\
      \<Longrightarrow> arc(p +++ (q +++ r)) \<longleftrightarrow> arc((p +++ q) +++ r)"
by (simp add: arc_simple_path simple_path_assoc)

subsection\<open>Subpath\<close>

definition\<^marker>\<open>tag important\<close> subpath :: "real \<Rightarrow> real \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> real \<Rightarrow> 'a::real_normed_vector"
  where "subpath a b g \ \x. g((b - a) * x + a)"

lemma path_image_subpath_gen:
  fixes g :: "_ \ 'a::real_normed_vector"
  shows "path_image(subpath u v g) = g ` (closed_segment u v)"
  by (auto simp add: closed_segment_real_eq path_image_def subpath_def)

lemma path_image_subpath:
  fixes g :: "real \ 'a::real_normed_vector"
  shows "path_image(subpath u v g) = (if u \ v then g ` {u..v} else g ` {v..u})"
  by (simp add: path_image_subpath_gen closed_segment_eq_real_ivl)

lemma path_image_subpath_commute:
  fixes g :: "real \ 'a::real_normed_vector"
  shows "path_image(subpath u v g) = path_image(subpath v u g)"
  by (simp add: path_image_subpath_gen closed_segment_eq_real_ivl)

lemma path_subpath [simp]:
  fixes g :: "real \ 'a::real_normed_vector"
  assumes "path g" "u \ {0..1}" "v \ {0..1}"
    shows "path(subpath u v g)"
proof -
  have "continuous_on {u..v} g" "continuous_on {v..u} g"
    using assms continuous_on_path by fastforce+
  then have "continuous_on {0..1} (g \ (\x. ((v-u) * x+ u)))"
    by (intro continuous_intros; simp add: image_affinity_atLeastAtMost [where c=u])
  then show ?thesis
    by (simp add: path_def subpath_def)
qed

lemma pathstart_subpath [simp]: "pathstart(subpath u v g) = g(u)"
  by (simp add: pathstart_def subpath_def)

lemma pathfinish_subpath [simp]: "pathfinish(subpath u v g) = g(v)"
  by (simp add: pathfinish_def subpath_def)

lemma subpath_trivial [simp]: "subpath 0 1 g = g"
  by (simp add: subpath_def)

lemma subpath_reversepath: "subpath 1 0 g = reversepath g"
  by (simp add: reversepath_def subpath_def)

lemma reversepath_subpath: "reversepath(subpath u v g) = subpath v u g"
  by (simp add: reversepath_def subpath_def algebra_simps)

lemma subpath_translation: "subpath u v ((\x. a + x) \ g) = (\x. a + x) \ subpath u v g"
  by (rule ext) (simp add: subpath_def)

lemma subpath_image: "subpath u v (f \ g) = f \ subpath u v g"
  by (rule ext) (simp add: subpath_def)

lemma affine_ineq:
  fixes x :: "'a::linordered_idom"
  assumes "x \ 1" "v \ u"
    shows "v + x * u \ u + x * v"
proof -
  have "(1-x)*(u-v) \ 0"
    using assms by auto
  then show ?thesis
    by (simp add: algebra_simps)
qed

lemma sum_le_prod1:
  fixes a::real shows "\a \ 1; b \ 1\ \ a + b \ 1 + a * b"
  by (metis add.commute affine_ineq mult.right_neutral)

lemma simple_path_subpath_eq:
  "simple_path(subpath u v g) \
     path(subpath u v g) \<and> u\<noteq>v \<and>
     (\<forall>x y. x \<in> closed_segment u v \<and> y \<in> closed_segment u v \<and> g x = g y
                \<longrightarrow> x = y \<or> x = u \<and> y = v \<or> x = v \<and> y = u)"
    (is "?lhs = ?rhs")
proof
  assume ?lhs
  then have p: "path (\x. g ((v - u) * x + u))"
        and sim: "(\x y. \x\{0..1}; y\{0..1}; g ((v - u) * x + u) = g ((v - u) * y + u)\
                  \<Longrightarrow> x = y \<or> x = 0 \<and> y = 1 \<or> x = 1 \<and> y = 0)"
    by (auto simp: simple_path_def loop_free_def subpath_def)
  { fix x y
    assume "x \ closed_segment u v" "y \ closed_segment u v" "g x = g y"
    then have "x = y \ x = u \ y = v \ x = v \ y = u"
      using sim [of "(x-u)/(v-u)" "(y-u)/(v-u)"] p
      by (auto split: if_split_asm simp add: closed_segment_real_eq image_affinity_atLeastAtMost)
        (simp_all add: field_split_simps)
  } moreover
  have "path(subpath u v g) \ u\v"
    using sim [of "1/3" "2/3"] p
    by (auto simp: subpath_def)
  ultimately show ?rhs
    by metis
next
  assume ?rhs
  then
  have d1: "\x y. \g x = g y; u \ x; x \ v; u \ y; y \ v\ \ x = y \ x = u \ y = v \ x = v \ y = u"
   and d2: "\x y. \g x = g y; v \ x; x \ u; v \ y; y \ u\ \ x = y \ x = u \ y = v \ x = v \ y = u"
   and ne: "u < v \ v < u"
   and psp: "path (subpath u v g)"
    by (auto simp: closed_segment_real_eq image_affinity_atLeastAtMost)
  have [simp]: "\x. u + x * v = v + x * u \ u=v \ x=1"
    by algebra
  show ?lhs using psp ne
    unfolding simple_path_def loop_free_def subpath_def
    by (fastforce simp add: algebra_simps affine_ineq mult_left_mono crossproduct_eq dest: d1 d2)
qed

lemma arc_subpath_eq:
  "arc(subpath u v g) \ path(subpath u v g) \ u\v \ inj_on g (closed_segment u v)"
  by (smt (verit, best) arc_simple_path closed_segment_commute ends_in_segment(2) inj_on_def pathfinish_subpath pathstart_subpath simple_path_subpath_eq)

lemma simple_path_subpath:
  assumes "simple_path g" "u \ {0..1}" "v \ {0..1}" "u \ v"
  shows "simple_path(subpath u v g)"
  using assms
  unfolding simple_path_subpath_eq
  by (force simp:  simple_path_def loop_free_def closed_segment_real_eq image_affinity_atLeastAtMost)

lemma arc_simple_path_subpath:
    "\simple_path g; u \ {0..1}; v \ {0..1}; g u \ g v\ \ arc(subpath u v g)"
  by (force intro: simple_path_subpath simple_path_imp_arc)

lemma arc_subpath_arc:
    "\arc g; u \ {0..1}; v \ {0..1}; u \ v\ \ arc(subpath u v g)"
  by (meson arc_def arc_imp_simple_path arc_simple_path_subpath inj_onD)

lemma arc_simple_path_subpath_interior:
    "\simple_path g; u \ {0..1}; v \ {0..1}; u \ v; \u-v\ < 1\ \ arc(subpath u v g)"
  by (force simp: simple_path_def loop_free_def intro: arc_simple_path_subpath)

lemma path_image_subpath_subset:
    "\u \ {0..1}; v \ {0..1}\ \ path_image(subpath u v g) \ path_image g"
  by (metis atLeastAtMost_iff atLeastatMost_subset_iff path_image_def path_image_subpath subset_image_iff)

lemma join_subpaths_middle: "subpath (0) ((1 / 2)) p +++ subpath ((1 / 2)) 1 p = p"
  by (rule ext) (simp add: joinpaths_def subpath_def field_split_simps)

subsection\<^marker>\<open>tag unimportant\<close>\<open>There is a subpath to the frontier\<close>

lemma subpath_to_frontier_explicit:
    fixes S :: "'a::metric_space set"
    assumes g: "path g" and "pathfinish g \ S"
    obtains u where "0 \ u" "u \ 1"
                "\x. 0 \ x \ x < u \ g x \ interior S"
                "(g u \ interior S)" "(u = 0 \ g u \ closure S)"
proof -
  have gcon: "continuous_on {0..1} g"
    using g by (simp add: path_def)
  moreover have "bounded ({u. g u \ closure (- S)} \ {0..1})"
    using compact_eq_bounded_closed by fastforce
  ultimately have com: "compact ({0..1} \ {u. g u \ closure (- S)})"
    using closed_vimage_Int
    by (metis (full_types) Int_commute closed_atLeastAtMost closed_closure compact_eq_bounded_closed vimage_def)
  have "1 \ {u. g u \ closure (- S)}"
    using assms by (simp add: pathfinish_def closure_def)
  then have dis: "{0..1} \ {u. g u \ closure (- S)} \ {}"
    using atLeastAtMost_iff zero_le_one by blast
  then obtain u where "0 \ u" "u \ 1" and gu: "g u \ closure (- S)"
                  and umin: "\t. \0 \ t; t \ 1; g t \ closure (- S)\ \ u \ t"
    using compact_attains_inf [OF com dis] by fastforce
  then have umin': "\t. \0 \ t; t \ 1; t < u\ \ g t \ S"
    using closure_def by fastforce
  have \<section>: "g u \<in> closure S" if "u \<noteq> 0"
  proof -
    have "u > 0" using that \<open>0 \<le> u\<close> by auto
    { fix e::real assume "e > 0"
      obtain d where "d>0" and d: "\x'. \x' \ {0..1}; dist x' u \ d\ \ dist (g x') (g u) < e"
        using continuous_onE [OF gcon _ \<open>e > 0\<close>] \<open>0 \<le> _\<close> \<open>_ \<le> 1\<close> atLeastAtMost_iff by auto
      have *: "dist (max 0 (u - d / 2)) u \ d"
        using \<open>0 \<le> u\<close> \<open>u \<le> 1\<close> \<open>d > 0\<close> by (simp add: dist_real_def)
      have "\y\S. dist y (g u) < e"
        using \<open>0 < u\<close> \<open>u \<le> 1\<close> \<open>d > 0\<close>
        by (force intro: d [OF _ *] umin')
    }
    then show ?thesis
      by (simp add: frontier_def closure_approachable)
  qed
  show ?thesis
  proof
    show "\x. 0 \ x \ x < u \ g x \ interior S"
      using \<open>u \<le> 1\<close> interior_closure umin by fastforce
    show "g u \ interior S"
      by (simp add: gu interior_closure)
  qed (use \<open>0 \<le> u\<close> \<open>u \<le> 1\<close> \<section> in auto)
qed

lemma subpath_to_frontier_strong:
    assumes g: "path g" and "pathfinish g \ S"
    obtains u where "0 \ u" "u \ 1" "g u \ interior S"
                    "u = 0 \ (\x. 0 \ x \ x < 1 \ subpath 0 u g x \ interior S) \ g u \ closure S"
proof -
  obtain u where "0 \ u" "u \ 1"
             and gxin: "\x. 0 \ x \ x < u \ g x \ interior S"
             and gunot: "(g u \ interior S)" and u0: "(u = 0 \ g u \ closure S)"
    using subpath_to_frontier_explicit [OF assms] by blast
  show ?thesis
  proof
    show "g u \ interior S"
      using gunot by blast
  qed (use \<open>0 \<le> u\<close> \<open>u \<le> 1\<close> u0 in \<open>(force simp: subpath_def gxin)+\<close>)
qed

lemma subpath_to_frontier:
    assumes g: "path g" and g0: "pathstart g \ closure S" and g1: "pathfinish g \ S"
    obtains u where "0 \ u" "u \ 1" "g u \ frontier S" "path_image(subpath 0 u g) - {g u} \ interior S"
proof -
  obtain u where "0 \ u" "u \ 1"
             and notin: "g u \ interior S"
             and disj: "u = 0 \
                        (\<forall>x. 0 \<le> x \<and> x < 1 \<longrightarrow> subpath 0 u g x \<in> interior S) \<and> g u \<in> closure S"
                       (is "_ \ ?P")
    using subpath_to_frontier_strong [OF g g1] by blast
  show ?thesis
  proof
    show "g u \ frontier S"
      by (metis DiffI disj frontier_def g0 notin pathstart_def)
    show "path_image (subpath 0 u g) - {g u} \ interior S"
      using disj
    proof
      assume "u = 0"
      then show ?thesis
        by (simp add: path_image_subpath)
    next
      assume P: ?P
      show ?thesis
      proof (clarsimp simp add: path_image_subpath_gen)
        fix y
        assume y: "y \ closed_segment 0 u" "g y \ interior S"
        with \<open>0 \<le> u\<close> have "0 \<le> y" "y \<le> u"
          by (auto simp: closed_segment_eq_real_ivl split: if_split_asm)
        then have "y=u \ subpath 0 u g (y/u) \ interior S"
          using P less_eq_real_def by force
        then show "g y = g u"
          using y by (auto simp: subpath_def split: if_split_asm)
      qed
    qed
  qed (use \<open>0 \<le> u\<close> \<open>u \<le> 1\<close> in auto)
qed

lemma exists_path_subpath_to_frontier:
    fixes S :: "'a::real_normed_vector set"
    assumes "path g" "pathstart g \ closure S" "pathfinish g \ S"
    obtains h where "path h" "pathstart h = pathstart g" "path_image h \ path_image g"
                    "path_image h - {pathfinish h} \ interior S"
                    "pathfinish h \ frontier S"
proof -
  obtain u where u: "0 \ u" "u \ 1" "g u \ frontier S" "(path_image(subpath 0 u g) - {g u}) \ interior S"
    using subpath_to_frontier [OF assms] by blast
  show ?thesis
  proof
    show "path_image (subpath 0 u g) \ path_image g"
      by (simp add: path_image_subpath_subset u)
    show "pathstart (subpath 0 u g) = pathstart g"
      by (metis pathstart_def pathstart_subpath)
  qed (use assms u in \<open>auto simp: path_image_subpath\<close>)
qed

lemma exists_path_subpath_to_frontier_closed:
    fixes S :: "'a::real_normed_vector set"
    assumes S: "closed S" and g: "path g" and g0: "pathstart g \ S" and g1: "pathfinish g \ S"
    obtains h where "path h" "pathstart h = pathstart g" "path_image h \ path_image g \ S"
                    "pathfinish h \ frontier S"
  by (smt (verit, del_insts) Diff_iff Int_iff S closure_closed exists_path_subpath_to_frontier
      frontier_def g g0 g1 interior_subset singletonD subset_eq)

subsection \<open>Shift Path to Start at Some Given Point\<close>

definition\<^marker>\<open>tag important\<close> shiftpath :: "real \<Rightarrow> (real \<Rightarrow> 'a::topological_space) \<Rightarrow> real \<Rightarrow> 'a"
  where "shiftpath a f = (\x. if (a + x) \ 1 then f (a + x) else f (a + x - 1))"

lemma shiftpath_alt_def: "shiftpath a f = (\x. if x \ 1-a then f (a + x) else f (a + x - 1))"
  by (auto simp: shiftpath_def)

lemma pathstart_shiftpath: "a \ 1 \ pathstart (shiftpath a g) = g a"
  unfolding pathstart_def shiftpath_def by auto

lemma pathfinish_shiftpath:
  assumes "0 \ a"
    and "pathfinish g = pathstart g"
  shows "pathfinish (shiftpath a g) = g a"
  using assms
  unfolding pathstart_def pathfinish_def shiftpath_def
  by auto

lemma endpoints_shiftpath:
  assumes "pathfinish g = pathstart g"
    and "a \ {0 .. 1}"
  shows "pathfinish (shiftpath a g) = g a"
    and "pathstart (shiftpath a g) = g a"
  using assms
  by (simp_all add: pathstart_shiftpath pathfinish_shiftpath)

lemma closed_shiftpath:
  assumes "pathfinish g = pathstart g"
    and "a \ {0..1}"
  shows "pathfinish (shiftpath a g) = pathstart (shiftpath a g)"
  using endpoints_shiftpath[OF assms]
  by auto

lemma path_shiftpath:
  assumes "path g"
    and "pathfinish g = pathstart g"
    and "a \ {0..1}"
  shows "path (shiftpath a g)"
proof -
  have *: "{0 .. 1} = {0 .. 1-a} \ {1-a .. 1}"
    using assms(3) by auto
  have **: "\x. x + a = 1 \ g (x + a - 1) = g (x + a)"
    by (smt (verit, best) assms(2) pathfinish_def pathstart_def)
  show ?thesis
    unfolding path_def shiftpath_def *
  proof (rule continuous_on_closed_Un)
    have contg: "continuous_on {0..1} g"
      using \<open>path g\<close> path_def by blast
    show "continuous_on {0..1-a} (\x. if a + x \ 1 then g (a + x) else g (a + x - 1))"
    proof (rule continuous_on_eq)
      show "continuous_on {0..1-a} (g \ (+) a)"
        by (intro continuous_intros continuous_on_subset [OF contg]) (use \<open>a \<in> {0..1}\<close> in auto)
    qed auto
    show "continuous_on {1-a..1} (\x. if a + x \ 1 then g (a + x) else g (a + x - 1))"
    proof (rule continuous_on_eq)
      show "continuous_on {1-a..1} (g \ (+) (a - 1))"
        by (intro continuous_intros continuous_on_subset [OF contg]) (use \<open>a \<in> {0..1}\<close> in auto)
    qed (auto simp: "**" add.commute add_diff_eq)
  qed auto
qed

lemma shiftpath_shiftpath:
  assumes "pathfinish g = pathstart g"
    and "a \ {0..1}"
    and "x \ {0..1}"
  shows "shiftpath (1 - a) (shiftpath a g) x = g x"
  using assms
  unfolding pathfinish_def pathstart_def shiftpath_def
  by auto

lemma path_image_shiftpath:
  assumes a: "a \ {0..1}"
    and "pathfinish g = pathstart g"
  shows "path_image (shiftpath a g) = path_image g"
proof -
  { fix x
    assume g: "g 1 = g 0" "x \ {0..1::real}" and gne: "\y. y\{0..1} \ {x. \ a + x \ 1} \ g x \ g (a + y - 1)"
    then have "\y\{0..1} \ {x. a + x \ 1}. g x = g (a + y)"
    proof (cases "a \ x")
      case False
      then show ?thesis
        apply (rule_tac x="1 + x - a" in bexI)
        using g gne[of "1 + x - a"] a by (force simp: field_simps)+
    next
      case True
      then show ?thesis
        using g a  by (rule_tac x="x - a" in bexI) (auto simp: field_simps)
    qed
  }
  then show ?thesis
    using assms
    unfolding shiftpath_def path_image_def pathfinish_def pathstart_def
    by (auto simp: image_iff)
qed

lemma loop_free_shiftpath:
  assumes "loop_free g" "pathfinish g = pathstart g" and a: "0 \ a" "a \ 1"
    shows "loop_free (shiftpath a g)"
  unfolding loop_free_def
proof (intro conjI impI ballI)
  show "x = y \ x = 0 \ y = 1 \ x = 1 \ y = 0"
    if "x \ {0..1}" "y \ {0..1}" "shiftpath a g x = shiftpath a g y" for x y
    using that a assms unfolding shiftpath_def loop_free_def
    by (smt (verit, ccfv_threshold) atLeastAtMost_iff)
qed

lemma simple_path_shiftpath:
  assumes "simple_path g" "pathfinish g = pathstart g" and a: "0 \ a" "a \ 1"
  shows "simple_path (shiftpath a g)"
  using assms loop_free_shiftpath path_shiftpath simple_path_def by fastforce

subsection \<open>Straight-Line Paths\<close>

definition\<^marker>\<open>tag important\<close> linepath :: "'a::real_normed_vector \<Rightarrow> 'a \<Rightarrow> real \<Rightarrow> 'a"
  where "linepath a b = (\x. (1 - x) *\<^sub>R a + x *\<^sub>R b)"

lemma pathstart_linepath[simp]: "pathstart (linepath a b) = a"
  unfolding pathstart_def linepath_def
  by auto

lemma pathfinish_linepath[simp]: "pathfinish (linepath a b) = b"
  unfolding pathfinish_def linepath_def
  by auto

lemma linepath_inner: "linepath a b x \ v = linepath (a \ v) (b \ v) x"
  by (simp add: linepath_def algebra_simps)

lemma Re_linepath': "Re (linepath a b x) = linepath (Re a) (Re b) x"
  by (simp add: linepath_def)

lemma Im_linepath': "Im (linepath a b x) = linepath (Im a) (Im b) x"
  by (simp add: linepath_def)

lemma linepath_0': "linepath a b 0 = a"
  by (simp add: linepath_def)

lemma linepath_1': "linepath a b 1 = b"
  by (simp add: linepath_def)

lemma continuous_linepath_at[intro]: "continuous (at x) (linepath a b)"
  unfolding linepath_def
  by (intro continuous_intros)

lemma continuous_on_linepath [intro,continuous_intros]: "continuous_on s (linepath a b)"
  using continuous_linepath_at
  by (auto intro!: continuous_at_imp_continuous_on)

lemma path_linepath[iff]: "path (linepath a b)"
  unfolding path_def
  by (rule continuous_on_linepath)

lemma path_image_linepath[simp]: "path_image (linepath a b) = closed_segment a b"
  unfolding path_image_def segment linepath_def
  by auto

lemma reversepath_linepath[simp]: "reversepath (linepath a b) = linepath b a"
  unfolding reversepath_def linepath_def
  by auto

lemma linepath_0 [simp]: "linepath 0 b x = x *\<^sub>R b"
  by (simp add: linepath_def)

lemma linepath_cnj: "cnj (linepath a b x) = linepath (cnj a) (cnj b) x"
  by (simp add: linepath_def)

lemma arc_linepath:
  assumes "a \ b" shows [simp]: "arc (linepath a b)"
proof -
  {
    fix x y :: "real"
    assume "x *\<^sub>R b + y *\<^sub>R a = x *\<^sub>R a + y *\<^sub>R b"
    then have "(x - y) *\<^sub>R a = (x - y) *\<^sub>R b"
      by (simp add: algebra_simps)
    with assms have "x = y"
      by simp
  }
  then show ?thesis
    unfolding arc_def inj_on_def
    by (fastforce simp: algebra_simps linepath_def)
qed

lemma simple_path_linepath[intro]: "a \ b \ simple_path (linepath a b)"
  by (simp add: arc_imp_simple_path)

lemma linepath_trivial [simp]: "linepath a a x = a"
  by (simp add: linepath_def real_vector.scale_left_diff_distrib)

lemma linepath_refl: "linepath a a = (\x. a)"
  by auto

lemma subpath_refl: "subpath a a g = linepath (g a) (g a)"
  by (simp add: subpath_def linepath_def algebra_simps)

lemma linepath_of_real: "(linepath (of_real a) (of_real b) x) = of_real ((1 - x)*a + x*b)"
  by (simp add: scaleR_conv_of_real linepath_def)

lemma of_real_linepath: "of_real (linepath a b x) = linepath (of_real a) (of_real b) x"
  by (metis linepath_of_real mult.right_neutral of_real_def real_scaleR_def)

lemma inj_on_linepath:
  assumes "a \ b" shows "inj_on (linepath a b) {0..1}"
  using arc_imp_inj_on arc_linepath assms by blast

lemma linepath_le_1:
  fixes a::"'a::linordered_idom" shows "\a \ 1; b \ 1; 0 \ u; u \ 1\ \ (1 - u) * a + u * b \ 1"
  using mult_left_le [of a "1-u"] mult_left_le [of b u] by auto

lemma linepath_in_path:
  shows "x \ {0..1} \ linepath a b x \ closed_segment a b"
  by (auto simp: segment linepath_def)

lemma linepath_image_01: "linepath a b ` {0..1} = closed_segment a b"
  by (auto simp: segment linepath_def)

lemma linepath_in_convex_hull:
  fixes x::real
  assumes "a \ convex hull S"
    and "b \ convex hull S"
    and "0\x" "x\1"
  shows "linepath a b x \ convex hull S"
  by (meson assms atLeastAtMost_iff convex_contains_segment convex_convex_hull linepath_in_path subset_eq)

lemma Re_linepath: "Re(linepath (of_real a) (of_real b) x) = (1 - x)*a + x*b"
  by (simp add: linepath_def)

lemma Im_linepath: "Im(linepath (of_real a) (of_real b) x) = 0"
  by (simp add: linepath_def)

lemma
  assumes "x \ closed_segment y z"
  shows in_closed_segment_imp_Re_in_closed_segment: "Re x \ closed_segment (Re y) (Re z)" (is ?th1)
    and in_closed_segment_imp_Im_in_closed_segment: "Im x \ closed_segment (Im y) (Im z)" (is ?th2)
proof -
  from assms obtain t where t: "t \ {0..1}" "x = linepath y z t"
    by (metis imageE linepath_image_01)
  have "Re x = linepath (Re y) (Re z) t" "Im x = linepath (Im y) (Im z) t"
    by (simp_all add: t Re_linepath' Im_linepath')
  with t(1) show ?th1 ?th2
    using linepath_in_path[of t "Re y" "Re z"] linepath_in_path[of t "Im y" "Im z"] by simp_all
qed

lemma linepath_in_open_segment: "t \ {0<..<1} \ x \ y \ linepath x y t \ open_segment x y"
  unfolding greaterThanLessThan_iff by (metis in_segment(2) linepath_def)

lemma in_open_segment_imp_Re_in_open_segment:
  assumes "x \ open_segment y z" "Re y \ Re z"
  shows   "Re x \ open_segment (Re y) (Re z)"
proof -
  from assms obtain t where t: "t \ {0<..<1}" "x = linepath y z t"
    by (metis greaterThanLessThan_iff in_segment(2) linepath_def)
  have "Re x = linepath (Re y) (Re z) t"
    by (simp_all add: t Re_linepath')
  with t(1) show ?thesis
    using linepath_in_open_segment[of t "Re y" "Re z"] assms by auto
qed

lemma in_open_segment_imp_Im_in_open_segment:
  assumes "x \ open_segment y z" "Im y \ Im z"
  shows   "Im x \ open_segment (Im y) (Im z)"
proof -
  from assms obtain t where t: "t \ {0<..<1}" "x = linepath y z t"
    by (metis greaterThanLessThan_iff in_segment(2) linepath_def)
  have "Im x = linepath (Im y) (Im z) t"
    by (simp_all add: t Im_linepath')
  with t(1) show ?thesis
    using linepath_in_open_segment[of t "Im y" "Im z"] assms by auto
qed

lemma bounded_linear_linepath:
  assumes "bounded_linear f"
  shows   "f (linepath a b x) = linepath (f a) (f b) x"
proof -
  interpret f: bounded_linear f by fact
  show ?thesis by (simp add: linepath_def f.add f.scale)
qed

lemma bounded_linear_linepath':
  assumes "bounded_linear f"
  shows   "f \ linepath a b = linepath (f a) (f b)"
  using bounded_linear_linepath[OF assms] by (simp add: fun_eq_iff)

lemma linepath_cnj': "cnj \ linepath a b = linepath (cnj a) (cnj b)"
  by (simp add: linepath_def fun_eq_iff)

lemma differentiable_linepath [intro]: "linepath a b differentiable at x within A"
  by (auto simp: linepath_def)

lemma has_vector_derivative_linepath_within:
    "(linepath a b has_vector_derivative (b - a)) (at x within S)"
  by (force intro: derivative_eq_intros simp add: linepath_def has_vector_derivative_def algebra_simps)

lemma linepath_real_ge_left:
  fixes x y :: real
  assumes "x \ y" "t \ 0"
  shows   "linepath x y t \ x"
proof -
  have "x + 0 \ x + t *\<^sub>R (y - x)"
    using assms by (intro add_left_mono) auto
  also have "\ = linepath x y t"
    by (simp add: linepath_def algebra_simps)
  finally show ?thesis by simp
qed

lemma linepath_real_le_right:
  fixes x y :: real
  assumes "x \ y" "t \ 1"
  shows   "linepath x y t \ y"
proof -
  have "y + 0 \ y + (1 - t) *\<^sub>R (x - y)"
    using assms by (intro add_left_mono) (auto intro: mult_nonneg_nonpos)
  also have "y + (1 - t) *\<^sub>R (x - y) = linepath x y t"
    by (simp add: linepath_def algebra_simps)
  finally show ?thesis by simp
qed

lemma linepath_translate: "(+) c \ linepath a b = linepath (a + c) (b + c)"
  by (auto simp: linepath_def algebra_simps)

subsection\<^marker>\<open>tag unimportant\<close>\<open>Segments via convex hulls\<close>

lemma segments_subset_convex_hull:
    "closed_segment a b \ (convex hull {a,b,c})"
    "closed_segment a c \ (convex hull {a,b,c})"
    "closed_segment b c \ (convex hull {a,b,c})"
    "closed_segment b a \ (convex hull {a,b,c})"
    "closed_segment c a \ (convex hull {a,b,c})"
    "closed_segment c b \ (convex hull {a,b,c})"
by (auto simp: segment_convex_hull linepath_of_real  elim!: rev_subsetD [OF _ hull_mono])

lemma midpoints_in_convex_hull:
  assumes "x \ convex hull s" "y \ convex hull s"
    shows "midpoint x y \ convex hull s"
  using assms closed_segment_subset_convex_hull csegment_midpoint_subset by blast

lemma not_in_interior_convex_hull_3:
  fixes a :: "complex"
  shows "a \ interior(convex hull {a,b,c})"
        "b \ interior(convex hull {a,b,c})"
        "c \ interior(convex hull {a,b,c})"
  by (auto simp: card_insert_le_m1 not_in_interior_convex_hull)

lemma midpoint_in_closed_segment [simp]: "midpoint a b \ closed_segment a b"
  using midpoints_in_convex_hull segment_convex_hull by blast

lemma midpoint_in_open_segment [simp]: "midpoint a b \ open_segment a b \ a \ b"
  by (simp add: open_segment_def)

lemma continuous_IVT_local_extremum:
  fixes f :: "'a::euclidean_space \ real"
  assumes contf: "continuous_on (closed_segment a b) f"
      and ab: "a \ b" "f a = f b"
  obtains z where "z \ open_segment a b"
                  "(\w \ closed_segment a b. (f w) \ (f z)) \
                   (\<forall>w \<in> closed_segment a b. (f z) \<le> (f w))"
proof -
  obtain c where "c \ closed_segment a b" and c: "\y. y \ closed_segment a b \ f y \ f c"
    using continuous_attains_sup [of "closed_segment a b" f] contf by auto
  moreover
  obtain d where "d \ closed_segment a b" and d: "\y. y \ closed_segment a b \ f d \ f y"
    using continuous_attains_inf [of "closed_segment a b" f] contf by auto
  ultimately show ?thesis
    by (smt (verit) UnE ab closed_segment_eq_open empty_iff insert_iff midpoint_in_open_segment that)
qed

text\<open>An injective map into R is also an open map w.r.T. the universe, and conversely. \<close>
proposition injective_eq_1d_open_map_UNIV:
  fixes f :: "real \ real"
  assumes contf: "continuous_on S f" and S: "is_interval S"
    shows "inj_on f S \ (\T. open T \ T \ S \ open(f ` T))"
          (is "?lhs = ?rhs")
proof safe
  fix T
  assume injf: ?lhs and "open T" and "T \ S"
  have "\U. open U \ f x \ U \ U \ f ` T" if "x \ T" for x
  proof -
    obtain \<delta> where "\<delta> > 0" and \<delta>: "cball x \<delta> \<subseteq> T"
      using \<open>open T\<close> \<open>x \<in> T\<close> open_contains_cball_eq by blast
    show ?thesis
    proof (intro exI conjI)
      have "closed_segment (x-\) (x+\) = {x-\..x+\}"
        using \<open>0 < \<delta>\<close> by (auto simp: closed_segment_eq_real_ivl)
      also have "\ \ S"
        using \<delta> \<open>T \<subseteq> S\<close> by (auto simp: dist_norm subset_eq)
      finally have "f ` (open_segment (x-\) (x+\)) = open_segment (f (x-\)) (f (x+\))"
        using continuous_injective_image_open_segment_1
        by (metis continuous_on_subset [OF contf] inj_on_subset [OF injf])
      then show "open (f ` {x-\<..})"
        using \<open>0 < \<delta>\<close> by (simp add: open_segment_eq_real_ivl)
      show "f x \ f ` {x - \<..}"
        by (auto simp: \<open>\<delta> > 0\<close>)
      show "f ` {x - \<..} \ f ` T"
        using \<delta> by (auto simp: dist_norm subset_iff)
    qed
  qed
  with open_subopen show "open (f ` T)"
    by blast
next
  assume R: ?rhs
  have False if xy: "x \ S" "y \ S" and "f x = f y" "x \ y" for x y
  proof -
    have "open (f ` open_segment x y)"
      using R
      by (metis S convex_contains_open_segment is_interval_convex open_greaterThanLessThan open_segment_eq_real_ivl xy)
    moreover
    have "continuous_on (closed_segment x y) f"
      by (meson S closed_segment_subset contf continuous_on_subset is_interval_convex that)
    then obtain \<xi> where "\<xi> \<in> open_segment x y"
                    and \<xi>: "(\<forall>w \<in> closed_segment x y. (f w) \<le> (f \<xi>)) \<or>
                            (\<forall>w \<in> closed_segment x y. (f \<xi>) \<le> (f w))"
      using continuous_IVT_local_extremum [of x y f] \<open>f x = f y\<close> \<open>x \<noteq> y\<close> by blast
    ultimately obtain e where "e>0" and e: "\u. dist u (f \) < e \ u \ f ` open_segment x y"
      using open_dist by (metis image_eqI)
    have fin: "f \ + (e/2) \ f ` open_segment x y" "f \ - (e/2) \ f ` open_segment x y"
      using e [of "f \ + (e/2)"] e [of "f \ - (e/2)"] \e > 0\ by (auto simp: dist_norm)
    show ?thesis
      using \<xi> \<open>0 < e\<close> fin open_closed_segment by fastforce
  qed
  then show ?lhs
    by (force simp: inj_on_def)
qed

subsection\<^marker>\<open>tag unimportant\<close> \<open>Bounding a point away from a path\<close>

lemma not_on_path_ball:
  fixes g :: "real \ 'a::heine_borel"
  assumes "path g"
    and z: "z \ path_image g"
  shows "\e > 0. ball z e \ path_image g = {}"
proof -
  have "closed (path_image g)"
    by (simp add: \<open>path g\<close> closed_path_image)
  then obtain a where "a \ path_image g" "\y \ path_image g. dist z a \ dist z y"
    by (auto intro: distance_attains_inf[OF _ path_image_nonempty, of g z])
  then show ?thesis
    by (rule_tac x="dist z a" in exI) (use dist_commute z in auto)
qed

lemma not_on_path_cball:
  fixes g :: "real \ 'a::heine_borel"
  assumes "path g"
    and "z \ path_image g"
  shows "\e>0. cball z e \ (path_image g) = {}"
  by (smt (verit, ccfv_threshold) open_ball assms centre_in_ball inf.orderE inf_assoc
      inf_bot_right not_on_path_ball open_contains_cball_eq)

subsection \<open>Path component\<close>

text \<open>Original formalization by Tom Hales\<close>

definition\<^marker>\<open>tag important\<close> "path_component S x y \<equiv>
  (\<exists>g. path g \<and> path_image g \<subseteq> S \<and> pathstart g = x \<and> pathfinish g = y)"

abbreviation\<^marker>\<open>tag important\<close>
  "path_component_set S x \ Collect (path_component S x)"

lemmas path_defs = path_def pathstart_def pathfinish_def path_image_def path_component_def

lemma path_component_mem:
  assumes "path_component S x y"
  shows "x \ S" and "y \ S"
  using assms
  unfolding path_defs
  by auto

lemma path_component_refl:
  assumes "x \ S"
  shows "path_component S x x"
  using assms
  unfolding path_defs
  by (metis (full_types) assms continuous_on_const image_subset_iff path_image_def)

lemma path_component_refl_eq: "path_component S x x \ x \ S"
--> --------------------

--> maximum size reached

--> --------------------

quality96%

¤ Dauer der Verarbeitung: 0.38 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.