src/HOL/Analysis/Path_Connected.thy
author wenzelm
Mon Mar 25 17:21:26 2019 +0100 (4 weeks ago)
changeset 69981 3dced198b9ec
parent 69939 812ce526da33
child 69986 f2d327275065
permissions -rw-r--r--
more strict AFP properties;
hoelzl@63627
     1
(*  Title:      HOL/Analysis/Path_Connected.thy
lp15@61806
     2
    Authors:    LC Paulson and Robert Himmelmann (TU Muenchen), based on material from HOL Light
huffman@36583
     3
*)
huffman@36583
     4
immler@69620
     5
section \<open>Path-Connectedness\<close>
huffman@36583
     6
huffman@36583
     7
theory Path_Connected
immler@69620
     8
  imports Starlike
huffman@36583
     9
begin
huffman@36583
    10
wenzelm@60420
    11
subsection \<open>Paths and Arcs\<close>
huffman@36583
    12
immler@67962
    13
definition%important path :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> bool"
wenzelm@53640
    14
  where "path g \<longleftrightarrow> continuous_on {0..1} g"
huffman@36583
    15
immler@67962
    16
definition%important pathstart :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> 'a"
huffman@36583
    17
  where "pathstart g = g 0"
huffman@36583
    18
immler@67962
    19
definition%important pathfinish :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> 'a"
huffman@36583
    20
  where "pathfinish g = g 1"
huffman@36583
    21
immler@67962
    22
definition%important path_image :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> 'a set"
huffman@36583
    23
  where "path_image g = g ` {0 .. 1}"
huffman@36583
    24
immler@67962
    25
definition%important reversepath :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> real \<Rightarrow> 'a"
huffman@36583
    26
  where "reversepath g = (\<lambda>x. g(1 - x))"
huffman@36583
    27
immler@67962
    28
definition%important joinpaths :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> real \<Rightarrow> 'a"
huffman@36583
    29
    (infixr "+++" 75)
huffman@36583
    30
  where "g1 +++ g2 = (\<lambda>x. if x \<le> 1/2 then g1 (2 * x) else g2 (2 * x - 1))"
huffman@36583
    31
immler@67962
    32
definition%important simple_path :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> bool"
huffman@36583
    33
  where "simple_path g \<longleftrightarrow>
paulson@60303
    34
     path g \<and> (\<forall>x\<in>{0..1}. \<forall>y\<in>{0..1}. g x = g y \<longrightarrow> x = y \<or> x = 0 \<and> y = 1 \<or> x = 1 \<and> y = 0)"
huffman@36583
    35
immler@67962
    36
definition%important arc :: "(real \<Rightarrow> 'a :: topological_space) \<Rightarrow> bool"
paulson@60303
    37
  where "arc g \<longleftrightarrow> path g \<and> inj_on g {0..1}"
huffman@36583
    38
wenzelm@49653
    39
immler@67962
    40
subsection%unimportant\<open>Invariance theorems\<close>
paulson@60303
    41
paulson@60303
    42
lemma path_eq: "path p \<Longrightarrow> (\<And>t. t \<in> {0..1} \<Longrightarrow> p t = q t) \<Longrightarrow> path q"
paulson@60303
    43
  using continuous_on_eq path_def by blast
paulson@60303
    44
lp15@68096
    45
lemma path_continuous_image: "path g \<Longrightarrow> continuous_on (path_image g) f \<Longrightarrow> path(f \<circ> g)"
paulson@60303
    46
  unfolding path_def path_image_def
paulson@60303
    47
  using continuous_on_compose by blast
paulson@60303
    48
paulson@60303
    49
lemma path_translation_eq:
paulson@60303
    50
  fixes g :: "real \<Rightarrow> 'a :: real_normed_vector"
lp15@68096
    51
  shows "path((\<lambda>x. a + x) \<circ> g) = path g"
paulson@60303
    52
proof -
lp15@68096
    53
  have g: "g = (\<lambda>x. -a + x) \<circ> ((\<lambda>x. a + x) \<circ> g)"
paulson@60303
    54
    by (rule ext) simp
paulson@60303
    55
  show ?thesis
paulson@60303
    56
    unfolding path_def
paulson@60303
    57
    apply safe
paulson@60303
    58
    apply (subst g)
paulson@60303
    59
    apply (rule continuous_on_compose)
paulson@60303
    60
    apply (auto intro: continuous_intros)
paulson@60303
    61
    done
paulson@60303
    62
qed
paulson@60303
    63
paulson@60303
    64
lemma path_linear_image_eq:
paulson@60303
    65
  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
paulson@60303
    66
   assumes "linear f" "inj f"
lp15@68096
    67
     shows "path(f \<circ> g) = path g"
paulson@60303
    68
proof -
paulson@60303
    69
  from linear_injective_left_inverse [OF assms]
paulson@60303
    70
  obtain h where h: "linear h" "h \<circ> f = id"
paulson@60303
    71
    by blast
lp15@68096
    72
  then have g: "g = h \<circ> (f \<circ> g)"
paulson@60303
    73
    by (metis comp_assoc id_comp)
paulson@60303
    74
  show ?thesis
paulson@60303
    75
    unfolding path_def
paulson@60303
    76
    using h assms
paulson@60303
    77
    by (metis g continuous_on_compose linear_continuous_on linear_conv_bounded_linear)
paulson@60303
    78
qed
paulson@60303
    79
lp15@68096
    80
lemma pathstart_translation: "pathstart((\<lambda>x. a + x) \<circ> g) = a + pathstart g"
paulson@60303
    81
  by (simp add: pathstart_def)
paulson@60303
    82
lp15@68096
    83
lemma pathstart_linear_image_eq: "linear f \<Longrightarrow> pathstart(f \<circ> g) = f(pathstart g)"
paulson@60303
    84
  by (simp add: pathstart_def)
paulson@60303
    85
lp15@68096
    86
lemma pathfinish_translation: "pathfinish((\<lambda>x. a + x) \<circ> g) = a + pathfinish g"
paulson@60303
    87
  by (simp add: pathfinish_def)
paulson@60303
    88
lp15@68096
    89
lemma pathfinish_linear_image: "linear f \<Longrightarrow> pathfinish(f \<circ> g) = f(pathfinish g)"
paulson@60303
    90
  by (simp add: pathfinish_def)
paulson@60303
    91
lp15@68096
    92
lemma path_image_translation: "path_image((\<lambda>x. a + x) \<circ> g) = (\<lambda>x. a + x) ` (path_image g)"
paulson@60303
    93
  by (simp add: image_comp path_image_def)
paulson@60303
    94
lp15@68096
    95
lemma path_image_linear_image: "linear f \<Longrightarrow> path_image(f \<circ> g) = f ` (path_image g)"
paulson@60303
    96
  by (simp add: image_comp path_image_def)
paulson@60303
    97
lp15@68096
    98
lemma reversepath_translation: "reversepath((\<lambda>x. a + x) \<circ> g) = (\<lambda>x. a + x) \<circ> reversepath g"
paulson@60303
    99
  by (rule ext) (simp add: reversepath_def)
huffman@36583
   100
lp15@68096
   101
lemma reversepath_linear_image: "linear f \<Longrightarrow> reversepath(f \<circ> g) = f \<circ> reversepath g"
paulson@60303
   102
  by (rule ext) (simp add: reversepath_def)
paulson@60303
   103
paulson@60303
   104
lemma joinpaths_translation:
lp15@68096
   105
    "((\<lambda>x. a + x) \<circ> g1) +++ ((\<lambda>x. a + x) \<circ> g2) = (\<lambda>x. a + x) \<circ> (g1 +++ g2)"
paulson@60303
   106
  by (rule ext) (simp add: joinpaths_def)
paulson@60303
   107
lp15@68096
   108
lemma joinpaths_linear_image: "linear f \<Longrightarrow> (f \<circ> g1) +++ (f \<circ> g2) = f \<circ> (g1 +++ g2)"
paulson@60303
   109
  by (rule ext) (simp add: joinpaths_def)
paulson@60303
   110
lp15@60809
   111
lemma simple_path_translation_eq:
paulson@60303
   112
  fixes g :: "real \<Rightarrow> 'a::euclidean_space"
lp15@68096
   113
  shows "simple_path((\<lambda>x. a + x) \<circ> g) = simple_path g"
paulson@60303
   114
  by (simp add: simple_path_def path_translation_eq)
paulson@60303
   115
paulson@60303
   116
lemma simple_path_linear_image_eq:
paulson@60303
   117
  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
paulson@60303
   118
  assumes "linear f" "inj f"
lp15@68096
   119
    shows "simple_path(f \<circ> g) = simple_path g"
paulson@60303
   120
  using assms inj_on_eq_iff [of f]
paulson@60303
   121
  by (auto simp: path_linear_image_eq simple_path_def path_translation_eq)
paulson@60303
   122
paulson@60303
   123
lemma arc_translation_eq:
paulson@60303
   124
  fixes g :: "real \<Rightarrow> 'a::euclidean_space"
lp15@68096
   125
  shows "arc((\<lambda>x. a + x) \<circ> g) = arc g"
paulson@60303
   126
  by (auto simp: arc_def inj_on_def path_translation_eq)
paulson@60303
   127
paulson@60303
   128
lemma arc_linear_image_eq:
paulson@60303
   129
  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
paulson@60303
   130
   assumes "linear f" "inj f"
lp15@68096
   131
     shows  "arc(f \<circ> g) = arc g"
paulson@60303
   132
  using assms inj_on_eq_iff [of f]
paulson@60303
   133
  by (auto simp: arc_def inj_on_def path_linear_image_eq)
paulson@60303
   134
nipkow@69514
   135
immler@67962
   136
subsection%unimportant\<open>Basic lemmas about paths\<close>
paulson@60303
   137
lp15@69939
   138
lemma pathin_iff_path_real [simp]: "pathin euclideanreal g \<longleftrightarrow> path g"
lp15@69939
   139
  by (simp add: pathin_def path_def)
lp15@69939
   140
lp15@64788
   141
lemma continuous_on_path: "path f \<Longrightarrow> t \<subseteq> {0..1} \<Longrightarrow> continuous_on t f"
lp15@64788
   142
  using continuous_on_subset path_def by blast
lp15@64788
   143
paulson@60303
   144
lemma arc_imp_simple_path: "arc g \<Longrightarrow> simple_path g"
paulson@60303
   145
  by (simp add: arc_def inj_on_def simple_path_def)
paulson@60303
   146
paulson@60303
   147
lemma arc_imp_path: "arc g \<Longrightarrow> path g"
paulson@60303
   148
  using arc_def by blast
paulson@60303
   149
lp15@64788
   150
lemma arc_imp_inj_on: "arc g \<Longrightarrow> inj_on g {0..1}"
lp15@64788
   151
  by (auto simp: arc_def)
lp15@64788
   152
paulson@60303
   153
lemma simple_path_imp_path: "simple_path g \<Longrightarrow> path g"
paulson@60303
   154
  using simple_path_def by blast
paulson@60303
   155
paulson@60303
   156
lemma simple_path_cases: "simple_path g \<Longrightarrow> arc g \<or> pathfinish g = pathstart g"
paulson@60303
   157
  unfolding simple_path_def arc_def inj_on_def pathfinish_def pathstart_def
lp15@68096
   158
  by force
paulson@60303
   159
paulson@60303
   160
lemma simple_path_imp_arc: "simple_path g \<Longrightarrow> pathfinish g \<noteq> pathstart g \<Longrightarrow> arc g"
paulson@60303
   161
  using simple_path_cases by auto
paulson@60303
   162
paulson@60303
   163
lemma arc_distinct_ends: "arc g \<Longrightarrow> pathfinish g \<noteq> pathstart g"
paulson@60303
   164
  unfolding arc_def inj_on_def pathfinish_def pathstart_def
paulson@60303
   165
  by fastforce
paulson@60303
   166
paulson@60303
   167
lemma arc_simple_path: "arc g \<longleftrightarrow> simple_path g \<and> pathfinish g \<noteq> pathstart g"
paulson@60303
   168
  using arc_distinct_ends arc_imp_simple_path simple_path_cases by blast
paulson@60303
   169
paulson@60303
   170
lemma simple_path_eq_arc: "pathfinish g \<noteq> pathstart g \<Longrightarrow> (simple_path g = arc g)"
paulson@60303
   171
  by (simp add: arc_simple_path)
huffman@36583
   172
lp15@66793
   173
lemma path_image_const [simp]: "path_image (\<lambda>t. a) = {a}"
lp15@66793
   174
  by (force simp: path_image_def)
lp15@66793
   175
lp15@60974
   176
lemma path_image_nonempty [simp]: "path_image g \<noteq> {}"
immler@56188
   177
  unfolding path_image_def image_is_empty box_eq_empty
wenzelm@53640
   178
  by auto
huffman@36583
   179
wenzelm@53640
   180
lemma pathstart_in_path_image[intro]: "pathstart g \<in> path_image g"
wenzelm@53640
   181
  unfolding pathstart_def path_image_def
wenzelm@53640
   182
  by auto
huffman@36583
   183
wenzelm@53640
   184
lemma pathfinish_in_path_image[intro]: "pathfinish g \<in> path_image g"
wenzelm@53640
   185
  unfolding pathfinish_def path_image_def
wenzelm@53640
   186
  by auto
wenzelm@53640
   187
wenzelm@53640
   188
lemma connected_path_image[intro]: "path g \<Longrightarrow> connected (path_image g)"
huffman@36583
   189
  unfolding path_def path_image_def
paulson@60303
   190
  using connected_continuous_image connected_Icc by blast
huffman@36583
   191
wenzelm@53640
   192
lemma compact_path_image[intro]: "path g \<Longrightarrow> compact (path_image g)"
huffman@36583
   193
  unfolding path_def path_image_def
paulson@60303
   194
  using compact_continuous_image connected_Icc by blast
huffman@36583
   195
wenzelm@53640
   196
lemma reversepath_reversepath[simp]: "reversepath (reversepath g) = g"
wenzelm@53640
   197
  unfolding reversepath_def
wenzelm@53640
   198
  by auto
huffman@36583
   199
wenzelm@53640
   200
lemma pathstart_reversepath[simp]: "pathstart (reversepath g) = pathfinish g"
wenzelm@53640
   201
  unfolding pathstart_def reversepath_def pathfinish_def
wenzelm@53640
   202
  by auto
huffman@36583
   203
wenzelm@53640
   204
lemma pathfinish_reversepath[simp]: "pathfinish (reversepath g) = pathstart g"
wenzelm@53640
   205
  unfolding pathstart_def reversepath_def pathfinish_def
wenzelm@53640
   206
  by auto
huffman@36583
   207
wenzelm@49653
   208
lemma pathstart_join[simp]: "pathstart (g1 +++ g2) = pathstart g1"
wenzelm@53640
   209
  unfolding pathstart_def joinpaths_def pathfinish_def
wenzelm@53640
   210
  by auto
huffman@36583
   211
wenzelm@49653
   212
lemma pathfinish_join[simp]: "pathfinish (g1 +++ g2) = pathfinish g2"
wenzelm@53640
   213
  unfolding pathstart_def joinpaths_def pathfinish_def
wenzelm@53640
   214
  by auto
huffman@36583
   215
wenzelm@53640
   216
lemma path_image_reversepath[simp]: "path_image (reversepath g) = path_image g"
wenzelm@49653
   217
proof -
wenzelm@53640
   218
  have *: "\<And>g. path_image (reversepath g) \<subseteq> path_image g"
wenzelm@49653
   219
    unfolding path_image_def subset_eq reversepath_def Ball_def image_iff
paulson@60303
   220
    by force
wenzelm@49653
   221
  show ?thesis
wenzelm@49653
   222
    using *[of g] *[of "reversepath g"]
wenzelm@53640
   223
    unfolding reversepath_reversepath
wenzelm@53640
   224
    by auto
wenzelm@49653
   225
qed
huffman@36583
   226
wenzelm@53640
   227
lemma path_reversepath [simp]: "path (reversepath g) \<longleftrightarrow> path g"
wenzelm@49653
   228
proof -
wenzelm@49653
   229
  have *: "\<And>g. path g \<Longrightarrow> path (reversepath g)"
wenzelm@49653
   230
    unfolding path_def reversepath_def
wenzelm@49653
   231
    apply (rule continuous_on_compose[unfolded o_def, of _ "\<lambda>x. 1 - x"])
lp15@68096
   232
    apply (auto intro: continuous_intros continuous_on_subset[of "{0..1}"])
wenzelm@49653
   233
    done
wenzelm@49653
   234
  show ?thesis
wenzelm@49653
   235
    using *[of "reversepath g"] *[of g]
wenzelm@49653
   236
    unfolding reversepath_reversepath
wenzelm@49653
   237
    by (rule iffI)
wenzelm@49653
   238
qed
wenzelm@49653
   239
paulson@60303
   240
lemma arc_reversepath:
paulson@60303
   241
  assumes "arc g" shows "arc(reversepath g)"
paulson@60303
   242
proof -
paulson@60303
   243
  have injg: "inj_on g {0..1}"
paulson@60303
   244
    using assms
paulson@60303
   245
    by (simp add: arc_def)
paulson@60303
   246
  have **: "\<And>x y::real. 1-x = 1-y \<Longrightarrow> x = y"
paulson@60303
   247
    by simp
paulson@60303
   248
  show ?thesis
lp15@68096
   249
    using assms  by (clarsimp simp: arc_def intro!: inj_onI) (simp add: inj_onD reversepath_def **)
paulson@60303
   250
qed
paulson@60303
   251
paulson@60303
   252
lemma simple_path_reversepath: "simple_path g \<Longrightarrow> simple_path (reversepath g)"
paulson@60303
   253
  apply (simp add: simple_path_def)
paulson@60303
   254
  apply (force simp: reversepath_def)
paulson@60303
   255
  done
paulson@60303
   256
wenzelm@49653
   257
lemmas reversepath_simps =
wenzelm@49653
   258
  path_reversepath path_image_reversepath pathstart_reversepath pathfinish_reversepath
huffman@36583
   259
wenzelm@49653
   260
lemma path_join[simp]:
wenzelm@49653
   261
  assumes "pathfinish g1 = pathstart g2"
wenzelm@49653
   262
  shows "path (g1 +++ g2) \<longleftrightarrow> path g1 \<and> path g2"
wenzelm@49653
   263
  unfolding path_def pathfinish_def pathstart_def
hoelzl@51478
   264
proof safe
hoelzl@51478
   265
  assume cont: "continuous_on {0..1} (g1 +++ g2)"
hoelzl@51478
   266
  have g1: "continuous_on {0..1} g1 \<longleftrightarrow> continuous_on {0..1} ((g1 +++ g2) \<circ> (\<lambda>x. x / 2))"
hoelzl@51478
   267
    by (intro continuous_on_cong refl) (auto simp: joinpaths_def)
hoelzl@51478
   268
  have g2: "continuous_on {0..1} g2 \<longleftrightarrow> continuous_on {0..1} ((g1 +++ g2) \<circ> (\<lambda>x. x / 2 + 1/2))"
wenzelm@53640
   269
    using assms
wenzelm@53640
   270
    by (intro continuous_on_cong refl) (auto simp: joinpaths_def pathfinish_def pathstart_def)
wenzelm@53640
   271
  show "continuous_on {0..1} g1" and "continuous_on {0..1} g2"
hoelzl@51481
   272
    unfolding g1 g2
hoelzl@56371
   273
    by (auto intro!: continuous_intros continuous_on_subset[OF cont] simp del: o_apply)
hoelzl@51478
   274
next
hoelzl@51478
   275
  assume g1g2: "continuous_on {0..1} g1" "continuous_on {0..1} g2"
hoelzl@51478
   276
  have 01: "{0 .. 1} = {0..1/2} \<union> {1/2 .. 1::real}"
huffman@36583
   277
    by auto
wenzelm@53640
   278
  {
wenzelm@53640
   279
    fix x :: real
wenzelm@53640
   280
    assume "0 \<le> x" and "x \<le> 1"
wenzelm@53640
   281
    then have "x \<in> (\<lambda>x. x * 2) ` {0..1 / 2}"
wenzelm@53640
   282
      by (intro image_eqI[where x="x/2"]) auto
wenzelm@53640
   283
  }
hoelzl@51478
   284
  note 1 = this
wenzelm@53640
   285
  {
wenzelm@53640
   286
    fix x :: real
wenzelm@53640
   287
    assume "0 \<le> x" and "x \<le> 1"
wenzelm@53640
   288
    then have "x \<in> (\<lambda>x. x * 2 - 1) ` {1 / 2..1}"
wenzelm@53640
   289
      by (intro image_eqI[where x="x/2 + 1/2"]) auto
wenzelm@53640
   290
  }
hoelzl@51478
   291
  note 2 = this
wenzelm@49653
   292
  show "continuous_on {0..1} (g1 +++ g2)"
wenzelm@53640
   293
    using assms
wenzelm@53640
   294
    unfolding joinpaths_def 01
hoelzl@56371
   295
    apply (intro continuous_on_cases closed_atLeastAtMost g1g2[THEN continuous_on_compose2] continuous_intros)
wenzelm@53640
   296
    apply (auto simp: field_simps pathfinish_def pathstart_def intro!: 1 2)
wenzelm@53640
   297
    done
wenzelm@49653
   298
qed
huffman@36583
   299
nipkow@69514
   300
immler@69620
   301
subsection%unimportant \<open>Path Images\<close>
paulson@60303
   302
paulson@60303
   303
lemma bounded_path_image: "path g \<Longrightarrow> bounded(path_image g)"
paulson@60303
   304
  by (simp add: compact_imp_bounded compact_path_image)
paulson@60303
   305
lp15@60809
   306
lemma closed_path_image:
paulson@60303
   307
  fixes g :: "real \<Rightarrow> 'a::t2_space"
paulson@60303
   308
  shows "path g \<Longrightarrow> closed(path_image g)"
paulson@60303
   309
  by (metis compact_path_image compact_imp_closed)
paulson@60303
   310
paulson@60303
   311
lemma connected_simple_path_image: "simple_path g \<Longrightarrow> connected(path_image g)"
paulson@60303
   312
  by (metis connected_path_image simple_path_imp_path)
paulson@60303
   313
paulson@60303
   314
lemma compact_simple_path_image: "simple_path g \<Longrightarrow> compact(path_image g)"
paulson@60303
   315
  by (metis compact_path_image simple_path_imp_path)
paulson@60303
   316
paulson@60303
   317
lemma bounded_simple_path_image: "simple_path g \<Longrightarrow> bounded(path_image g)"
paulson@60303
   318
  by (metis bounded_path_image simple_path_imp_path)
paulson@60303
   319
paulson@60303
   320
lemma closed_simple_path_image:
paulson@60303
   321
  fixes g :: "real \<Rightarrow> 'a::t2_space"
paulson@60303
   322
  shows "simple_path g \<Longrightarrow> closed(path_image g)"
paulson@60303
   323
  by (metis closed_path_image simple_path_imp_path)
paulson@60303
   324
paulson@60303
   325
lemma connected_arc_image: "arc g \<Longrightarrow> connected(path_image g)"
paulson@60303
   326
  by (metis connected_path_image arc_imp_path)
paulson@60303
   327
paulson@60303
   328
lemma compact_arc_image: "arc g \<Longrightarrow> compact(path_image g)"
paulson@60303
   329
  by (metis compact_path_image arc_imp_path)
paulson@60303
   330
paulson@60303
   331
lemma bounded_arc_image: "arc g \<Longrightarrow> bounded(path_image g)"
paulson@60303
   332
  by (metis bounded_path_image arc_imp_path)
paulson@60303
   333
paulson@60303
   334
lemma closed_arc_image:
paulson@60303
   335
  fixes g :: "real \<Rightarrow> 'a::t2_space"
paulson@60303
   336
  shows "arc g \<Longrightarrow> closed(path_image g)"
paulson@60303
   337
  by (metis closed_path_image arc_imp_path)
paulson@60303
   338
wenzelm@53640
   339
lemma path_image_join_subset: "path_image (g1 +++ g2) \<subseteq> path_image g1 \<union> path_image g2"
wenzelm@53640
   340
  unfolding path_image_def joinpaths_def
wenzelm@53640
   341
  by auto
huffman@36583
   342
huffman@36583
   343
lemma subset_path_image_join:
wenzelm@53640
   344
  assumes "path_image g1 \<subseteq> s"
wenzelm@53640
   345
    and "path_image g2 \<subseteq> s"
wenzelm@53640
   346
  shows "path_image (g1 +++ g2) \<subseteq> s"
wenzelm@53640
   347
  using path_image_join_subset[of g1 g2] and assms
wenzelm@53640
   348
  by auto
huffman@36583
   349
huffman@36583
   350
lemma path_image_join:
paulson@60303
   351
    "pathfinish g1 = pathstart g2 \<Longrightarrow> path_image(g1 +++ g2) = path_image g1 \<union> path_image g2"
paulson@60303
   352
  apply (rule subset_antisym [OF path_image_join_subset])
paulson@60303
   353
  apply (auto simp: pathfinish_def pathstart_def path_image_def joinpaths_def image_def)
paulson@60303
   354
  apply (drule sym)
paulson@60303
   355
  apply (rule_tac x="xa/2" in bexI, auto)
paulson@60303
   356
  apply (rule ccontr)
paulson@60303
   357
  apply (drule_tac x="(xa+1)/2" in bspec)
paulson@60303
   358
  apply (auto simp: field_simps)
paulson@60303
   359
  apply (drule_tac x="1/2" in bspec, auto)
paulson@60303
   360
  done
huffman@36583
   361
huffman@36583
   362
lemma not_in_path_image_join:
wenzelm@53640
   363
  assumes "x \<notin> path_image g1"
wenzelm@53640
   364
    and "x \<notin> path_image g2"
wenzelm@53640
   365
  shows "x \<notin> path_image (g1 +++ g2)"
wenzelm@53640
   366
  using assms and path_image_join_subset[of g1 g2]
wenzelm@53640
   367
  by auto
huffman@36583
   368
lp15@68096
   369
lemma pathstart_compose: "pathstart(f \<circ> p) = f(pathstart p)"
paulson@60303
   370
  by (simp add: pathstart_def)
paulson@60303
   371
lp15@68096
   372
lemma pathfinish_compose: "pathfinish(f \<circ> p) = f(pathfinish p)"
paulson@60303
   373
  by (simp add: pathfinish_def)
paulson@60303
   374
lp15@68096
   375
lemma path_image_compose: "path_image (f \<circ> p) = f ` (path_image p)"
paulson@60303
   376
  by (simp add: image_comp path_image_def)
paulson@60303
   377
lp15@68096
   378
lemma path_compose_join: "f \<circ> (p +++ q) = (f \<circ> p) +++ (f \<circ> q)"
paulson@60303
   379
  by (rule ext) (simp add: joinpaths_def)
paulson@60303
   380
lp15@68096
   381
lemma path_compose_reversepath: "f \<circ> reversepath p = reversepath(f \<circ> p)"
paulson@60303
   382
  by (rule ext) (simp add: reversepath_def)
paulson@60303
   383
lp15@61762
   384
lemma joinpaths_eq:
paulson@60303
   385
  "(\<And>t. t \<in> {0..1} \<Longrightarrow> p t = p' t) \<Longrightarrow>
paulson@60303
   386
   (\<And>t. t \<in> {0..1} \<Longrightarrow> q t = q' t)
paulson@60303
   387
   \<Longrightarrow>  t \<in> {0..1} \<Longrightarrow> (p +++ q) t = (p' +++ q') t"
paulson@60303
   388
  by (auto simp: joinpaths_def)
paulson@60303
   389
paulson@60303
   390
lemma simple_path_inj_on: "simple_path g \<Longrightarrow> inj_on g {0<..<1}"
paulson@60303
   391
  by (auto simp: simple_path_def path_image_def inj_on_def less_eq_real_def Ball_def)
paulson@60303
   392
paulson@60303
   393
immler@67962
   394
subsection%unimportant\<open>Simple paths with the endpoints removed\<close>
paulson@60303
   395
paulson@60303
   396
lemma simple_path_endless:
paulson@60303
   397
    "simple_path c \<Longrightarrow> path_image c - {pathstart c,pathfinish c} = c ` {0<..<1}"
paulson@60303
   398
  apply (auto simp: simple_path_def path_image_def pathstart_def pathfinish_def Ball_def Bex_def image_def)
paulson@60303
   399
  apply (metis eq_iff le_less_linear)
paulson@60303
   400
  apply (metis leD linear)
paulson@60303
   401
  using less_eq_real_def zero_le_one apply blast
paulson@60303
   402
  using less_eq_real_def zero_le_one apply blast
wenzelm@49653
   403
  done
huffman@36583
   404
paulson@60303
   405
lemma connected_simple_path_endless:
paulson@60303
   406
    "simple_path c \<Longrightarrow> connected(path_image c - {pathstart c,pathfinish c})"
paulson@60303
   407
apply (simp add: simple_path_endless)
paulson@60303
   408
apply (rule connected_continuous_image)
paulson@60303
   409
apply (meson continuous_on_subset greaterThanLessThan_subseteq_atLeastAtMost_iff le_numeral_extra(3) le_numeral_extra(4) path_def simple_path_imp_path)
paulson@60303
   410
by auto
paulson@60303
   411
paulson@60303
   412
lemma nonempty_simple_path_endless:
paulson@60303
   413
    "simple_path c \<Longrightarrow> path_image c - {pathstart c,pathfinish c} \<noteq> {}"
paulson@60303
   414
  by (simp add: simple_path_endless)
paulson@60303
   415
paulson@60303
   416
immler@67962
   417
subsection%unimportant\<open>The operations on paths\<close>
paulson@60303
   418
paulson@60303
   419
lemma path_image_subset_reversepath: "path_image(reversepath g) \<le> path_image g"
paulson@60303
   420
  by (auto simp: path_image_def reversepath_def)
paulson@60303
   421
paulson@60303
   422
lemma path_imp_reversepath: "path g \<Longrightarrow> path(reversepath g)"
paulson@60303
   423
  apply (auto simp: path_def reversepath_def)
paulson@60303
   424
  using continuous_on_compose [of "{0..1}" "\<lambda>x. 1 - x" g]
paulson@60303
   425
  apply (auto simp: continuous_on_op_minus)
paulson@60303
   426
  done
paulson@60303
   427
paulson@61204
   428
lemma half_bounded_equal: "1 \<le> x * 2 \<Longrightarrow> x * 2 \<le> 1 \<longleftrightarrow> x = (1/2::real)"
paulson@61204
   429
  by simp
paulson@60303
   430
paulson@60303
   431
lemma continuous_on_joinpaths:
paulson@60303
   432
  assumes "continuous_on {0..1} g1" "continuous_on {0..1} g2" "pathfinish g1 = pathstart g2"
paulson@60303
   433
    shows "continuous_on {0..1} (g1 +++ g2)"
paulson@60303
   434
proof -
paulson@60303
   435
  have *: "{0..1::real} = {0..1/2} \<union> {1/2..1}"
paulson@60303
   436
    by auto
paulson@60303
   437
  have gg: "g2 0 = g1 1"
paulson@60303
   438
    by (metis assms(3) pathfinish_def pathstart_def)
paulson@61204
   439
  have 1: "continuous_on {0..1/2} (g1 +++ g2)"
lp15@68096
   440
    apply (rule continuous_on_eq [of _ "g1 \<circ> (\<lambda>x. 2*x)"])
paulson@61204
   441
    apply (rule continuous_intros | simp add: joinpaths_def assms)+
paulson@60303
   442
    done
lp15@68096
   443
  have "continuous_on {1/2..1} (g2 \<circ> (\<lambda>x. 2*x-1))"
paulson@61204
   444
    apply (rule continuous_on_subset [of "{1/2..1}"])
paulson@61204
   445
    apply (rule continuous_intros | simp add: image_affinity_atLeastAtMost_diff assms)+
paulson@61204
   446
    done
paulson@61204
   447
  then have 2: "continuous_on {1/2..1} (g1 +++ g2)"
lp15@68096
   448
    apply (rule continuous_on_eq [of "{1/2..1}" "g2 \<circ> (\<lambda>x. 2*x-1)"])
paulson@61204
   449
    apply (rule assms continuous_intros | simp add: joinpaths_def mult.commute half_bounded_equal gg)+
paulson@60303
   450
    done
paulson@60303
   451
  show ?thesis
paulson@60303
   452
    apply (subst *)
lp15@62397
   453
    apply (rule continuous_on_closed_Un)
paulson@60303
   454
    using 1 2
paulson@60303
   455
    apply auto
paulson@60303
   456
    done
paulson@60303
   457
qed
paulson@60303
   458
paulson@60303
   459
lemma path_join_imp: "\<lbrakk>path g1; path g2; pathfinish g1 = pathstart g2\<rbrakk> \<Longrightarrow> path(g1 +++ g2)"
paulson@60303
   460
  by (simp add: path_join)
paulson@60303
   461
huffman@36583
   462
lemma simple_path_join_loop:
lp15@60809
   463
  assumes "arc g1" "arc g2"
lp15@60809
   464
          "pathfinish g1 = pathstart g2"  "pathfinish g2 = pathstart g1"
paulson@60303
   465
          "path_image g1 \<inter> path_image g2 \<subseteq> {pathstart g1, pathstart g2}"
paulson@60303
   466
  shows "simple_path(g1 +++ g2)"
paulson@60303
   467
proof -
paulson@60303
   468
  have injg1: "inj_on g1 {0..1}"
paulson@60303
   469
    using assms
paulson@60303
   470
    by (simp add: arc_def)
paulson@60303
   471
  have injg2: "inj_on g2 {0..1}"
paulson@60303
   472
    using assms
paulson@60303
   473
    by (simp add: arc_def)
lp15@60809
   474
  have g12: "g1 1 = g2 0"
lp15@60809
   475
   and g21: "g2 1 = g1 0"
paulson@60303
   476
   and sb:  "g1 ` {0..1} \<inter> g2 ` {0..1} \<subseteq> {g1 0, g2 0}"
paulson@60303
   477
    using assms
paulson@60303
   478
    by (simp_all add: arc_def pathfinish_def pathstart_def path_image_def)
paulson@60303
   479
  { fix x and y::real
lp15@60809
   480
    assume xyI: "x = 1 \<longrightarrow> y \<noteq> 0"
paulson@60303
   481
       and xy: "x \<le> 1" "0 \<le> y" " y * 2 \<le> 1" "\<not> x * 2 \<le> 1" "g2 (2 * x - 1) = g1 (2 * y)"
paulson@60303
   482
    have g1im: "g1 (2 * y) \<in> g1 ` {0..1} \<inter> g2 ` {0..1}"
paulson@60303
   483
      using xy
paulson@60303
   484
      apply simp
paulson@60303
   485
      apply (rule_tac x="2 * x - 1" in image_eqI, auto)
paulson@60303
   486
      done
paulson@60303
   487
    have False
lp15@60809
   488
      using subsetD [OF sb g1im] xy
paulson@60303
   489
      apply auto
paulson@60303
   490
      apply (drule inj_onD [OF injg1])
paulson@60303
   491
      using g21 [symmetric] xyI
paulson@60303
   492
      apply (auto dest: inj_onD [OF injg2])
paulson@60303
   493
      done
paulson@60303
   494
   } note * = this
paulson@60303
   495
  { fix x and y::real
paulson@60303
   496
    assume xy: "y \<le> 1" "0 \<le> x" "\<not> y * 2 \<le> 1" "x * 2 \<le> 1" "g1 (2 * x) = g2 (2 * y - 1)"
paulson@60303
   497
    have g1im: "g1 (2 * x) \<in> g1 ` {0..1} \<inter> g2 ` {0..1}"
paulson@60303
   498
      using xy
paulson@60303
   499
      apply simp
paulson@60303
   500
      apply (rule_tac x="2 * x" in image_eqI, auto)
paulson@60303
   501
      done
paulson@60303
   502
    have "x = 0 \<and> y = 1"
lp15@60809
   503
      using subsetD [OF sb g1im] xy
paulson@60303
   504
      apply auto
paulson@60303
   505
      apply (force dest: inj_onD [OF injg1])
paulson@60303
   506
      using  g21 [symmetric]
paulson@60303
   507
      apply (auto dest: inj_onD [OF injg2])
paulson@60303
   508
      done
paulson@60303
   509
   } note ** = this
paulson@60303
   510
  show ?thesis
paulson@60303
   511
    using assms
paulson@60303
   512
    apply (simp add: arc_def simple_path_def path_join, clarify)
nipkow@62390
   513
    apply (simp add: joinpaths_def split: if_split_asm)
paulson@60303
   514
    apply (force dest: inj_onD [OF injg1])
paulson@60303
   515
    apply (metis *)
paulson@60303
   516
    apply (metis **)
paulson@60303
   517
    apply (force dest: inj_onD [OF injg2])
paulson@60303
   518
    done
paulson@60303
   519
qed
paulson@60303
   520
paulson@60303
   521
lemma arc_join:
lp15@60809
   522
  assumes "arc g1" "arc g2"
paulson@60303
   523
          "pathfinish g1 = pathstart g2"
paulson@60303
   524
          "path_image g1 \<inter> path_image g2 \<subseteq> {pathstart g2}"
paulson@60303
   525
    shows "arc(g1 +++ g2)"
paulson@60303
   526
proof -
paulson@60303
   527
  have injg1: "inj_on g1 {0..1}"
paulson@60303
   528
    using assms
paulson@60303
   529
    by (simp add: arc_def)
paulson@60303
   530
  have injg2: "inj_on g2 {0..1}"
paulson@60303
   531
    using assms
paulson@60303
   532
    by (simp add: arc_def)
paulson@60303
   533
  have g11: "g1 1 = g2 0"
paulson@60303
   534
   and sb:  "g1 ` {0..1} \<inter> g2 ` {0..1} \<subseteq> {g2 0}"
paulson@60303
   535
    using assms
paulson@60303
   536
    by (simp_all add: arc_def pathfinish_def pathstart_def path_image_def)
paulson@60303
   537
  { fix x and y::real
lp15@60809
   538
    assume xy: "x \<le> 1" "0 \<le> y" " y * 2 \<le> 1" "\<not> x * 2 \<le> 1" "g2 (2 * x - 1) = g1 (2 * y)"
paulson@60303
   539
    have g1im: "g1 (2 * y) \<in> g1 ` {0..1} \<inter> g2 ` {0..1}"
paulson@60303
   540
      using xy
paulson@60303
   541
      apply simp
paulson@60303
   542
      apply (rule_tac x="2 * x - 1" in image_eqI, auto)
paulson@60303
   543
      done
paulson@60303
   544
    have False
lp15@60809
   545
      using subsetD [OF sb g1im] xy
paulson@60303
   546
      by (auto dest: inj_onD [OF injg2])
paulson@60303
   547
   } note * = this
paulson@60303
   548
  show ?thesis
paulson@60303
   549
    apply (simp add: arc_def inj_on_def)
paulson@60303
   550
    apply (clarsimp simp add: arc_imp_path assms path_join)
nipkow@62390
   551
    apply (simp add: joinpaths_def split: if_split_asm)
paulson@60303
   552
    apply (force dest: inj_onD [OF injg1])
paulson@60303
   553
    apply (metis *)
paulson@60303
   554
    apply (metis *)
paulson@60303
   555
    apply (force dest: inj_onD [OF injg2])
paulson@60303
   556
    done
paulson@60303
   557
qed
paulson@60303
   558
paulson@60303
   559
lemma reversepath_joinpaths:
paulson@60303
   560
    "pathfinish g1 = pathstart g2 \<Longrightarrow> reversepath(g1 +++ g2) = reversepath g2 +++ reversepath g1"
paulson@60303
   561
  unfolding reversepath_def pathfinish_def pathstart_def joinpaths_def
paulson@60303
   562
  by (rule ext) (auto simp: mult.commute)
paulson@60303
   563
paulson@60303
   564
immler@67962
   565
subsection%unimportant\<open>Some reversed and "if and only if" versions of joining theorems\<close>
lp15@62533
   566
hoelzl@63594
   567
lemma path_join_path_ends:
lp15@62533
   568
  fixes g1 :: "real \<Rightarrow> 'a::metric_space"
hoelzl@63594
   569
  assumes "path(g1 +++ g2)" "path g2"
lp15@62533
   570
    shows "pathfinish g1 = pathstart g2"
lp15@62533
   571
proof (rule ccontr)
wenzelm@63040
   572
  define e where "e = dist (g1 1) (g2 0)"
lp15@62533
   573
  assume Neg: "pathfinish g1 \<noteq> pathstart g2"
lp15@62533
   574
  then have "0 < dist (pathfinish g1) (pathstart g2)"
lp15@62533
   575
    by auto
lp15@62533
   576
  then have "e > 0"
hoelzl@63594
   577
    by (metis e_def pathfinish_def pathstart_def)
hoelzl@63594
   578
  then obtain d1 where "d1 > 0"
lp15@62533
   579
       and d1: "\<And>x'. \<lbrakk>x'\<in>{0..1}; norm x' < d1\<rbrakk> \<Longrightarrow> dist (g2 x') (g2 0) < e/2"
lp15@62533
   580
    using assms(2) unfolding path_def continuous_on_iff
lp15@62533
   581
    apply (drule_tac x=0 in bspec, simp)
lp15@62533
   582
    by (metis half_gt_zero_iff norm_conv_dist)
hoelzl@63594
   583
  obtain d2 where "d2 > 0"
hoelzl@63594
   584
       and d2: "\<And>x'. \<lbrakk>x'\<in>{0..1}; dist x' (1/2) < d2\<rbrakk>
lp15@62533
   585
                      \<Longrightarrow> dist ((g1 +++ g2) x') (g1 1) < e/2"
lp15@62533
   586
    using assms(1) \<open>e > 0\<close> unfolding path_def continuous_on_iff
lp15@62533
   587
    apply (drule_tac x="1/2" in bspec, simp)
lp15@62533
   588
    apply (drule_tac x="e/2" in spec)
lp15@62533
   589
    apply (force simp: joinpaths_def)
lp15@62533
   590
    done
lp15@62533
   591
  have int01_1: "min (1/2) (min d1 d2) / 2 \<in> {0..1}"
lp15@62533
   592
    using \<open>d1 > 0\<close> \<open>d2 > 0\<close> by (simp add: min_def)
lp15@62533
   593
  have dist1: "norm (min (1 / 2) (min d1 d2) / 2) < d1"
lp15@62533
   594
    using \<open>d1 > 0\<close> \<open>d2 > 0\<close> by (simp add: min_def dist_norm)
lp15@62533
   595
  have int01_2: "1/2 + min (1/2) (min d1 d2) / 4 \<in> {0..1}"
lp15@62533
   596
    using \<open>d1 > 0\<close> \<open>d2 > 0\<close> by (simp add: min_def)
lp15@62533
   597
  have dist2: "dist (1 / 2 + min (1 / 2) (min d1 d2) / 4) (1 / 2) < d2"
lp15@62533
   598
    using \<open>d1 > 0\<close> \<open>d2 > 0\<close> by (simp add: min_def dist_norm)
nipkow@69508
   599
  have [simp]: "\<not> min (1 / 2) (min d1 d2) \<le> 0"
lp15@62533
   600
    using \<open>d1 > 0\<close> \<open>d2 > 0\<close> by (simp add: min_def)
lp15@62533
   601
  have "dist (g2 (min (1 / 2) (min d1 d2) / 2)) (g1 1) < e/2"
lp15@62533
   602
       "dist (g2 (min (1 / 2) (min d1 d2) / 2)) (g2 0) < e/2"
lp15@62533
   603
    using d1 [OF int01_1 dist1] d2 [OF int01_2 dist2] by (simp_all add: joinpaths_def)
lp15@62533
   604
  then have "dist (g1 1) (g2 0) < e/2 + e/2"
lp15@62533
   605
    using dist_triangle_half_r e_def by blast
hoelzl@63594
   606
  then show False
lp15@62533
   607
    by (simp add: e_def [symmetric])
lp15@62533
   608
qed
lp15@62533
   609
hoelzl@63594
   610
lemma path_join_eq [simp]:
lp15@62533
   611
  fixes g1 :: "real \<Rightarrow> 'a::metric_space"
lp15@62533
   612
  assumes "path g1" "path g2"
lp15@62533
   613
    shows "path(g1 +++ g2) \<longleftrightarrow> pathfinish g1 = pathstart g2"
lp15@62533
   614
  using assms by (metis path_join_path_ends path_join_imp)
lp15@62533
   615
hoelzl@63594
   616
lemma simple_path_joinE:
lp15@62533
   617
  assumes "simple_path(g1 +++ g2)" and "pathfinish g1 = pathstart g2"
hoelzl@63594
   618
  obtains "arc g1" "arc g2"
lp15@62533
   619
          "path_image g1 \<inter> path_image g2 \<subseteq> {pathstart g1, pathstart g2}"
lp15@62533
   620
proof -
hoelzl@63594
   621
  have *: "\<And>x y. \<lbrakk>0 \<le> x; x \<le> 1; 0 \<le> y; y \<le> 1; (g1 +++ g2) x = (g1 +++ g2) y\<rbrakk>
lp15@62533
   622
               \<Longrightarrow> x = y \<or> x = 0 \<and> y = 1 \<or> x = 1 \<and> y = 0"
lp15@62533
   623
    using assms by (simp add: simple_path_def)
hoelzl@63594
   624
  have "path g1"
lp15@62533
   625
    using assms path_join simple_path_imp_path by blast
lp15@62533
   626
  moreover have "inj_on g1 {0..1}"
lp15@62533
   627
  proof (clarsimp simp: inj_on_def)
lp15@62533
   628
    fix x y
lp15@62533
   629
    assume "g1 x = g1 y" "0 \<le> x" "x \<le> 1" "0 \<le> y" "y \<le> 1"
lp15@62533
   630
    then show "x = y"
lp15@62533
   631
      using * [of "x/2" "y/2"] by (simp add: joinpaths_def split_ifs)
lp15@62533
   632
  qed
lp15@62533
   633
  ultimately have "arc g1"
lp15@62533
   634
    using assms  by (simp add: arc_def)
lp15@62533
   635
  have [simp]: "g2 0 = g1 1"
hoelzl@63594
   636
    using assms by (metis pathfinish_def pathstart_def)
lp15@62533
   637
  have "path g2"
lp15@62533
   638
    using assms path_join simple_path_imp_path by blast
lp15@62533
   639
  moreover have "inj_on g2 {0..1}"
lp15@62533
   640
  proof (clarsimp simp: inj_on_def)
lp15@62533
   641
    fix x y
lp15@62533
   642
    assume "g2 x = g2 y" "0 \<le> x" "x \<le> 1" "0 \<le> y" "y \<le> 1"
lp15@62533
   643
    then show "x = y"
lp15@62533
   644
      using * [of "(x + 1) / 2" "(y + 1) / 2"]
lp15@62533
   645
      by (force simp: joinpaths_def split_ifs divide_simps)
lp15@62533
   646
  qed
lp15@62533
   647
  ultimately have "arc g2"
lp15@62533
   648
    using assms  by (simp add: arc_def)
hoelzl@63594
   649
  have "g2 y = g1 0 \<or> g2 y = g1 1"
lp15@62533
   650
       if "g1 x = g2 y" "0 \<le> x" "x \<le> 1" "0 \<le> y" "y \<le> 1" for x y
lp15@62533
   651
      using * [of "x / 2" "(y + 1) / 2"] that
lp15@62533
   652
      by (auto simp: joinpaths_def split_ifs divide_simps)
lp15@62533
   653
  then have "path_image g1 \<inter> path_image g2 \<subseteq> {pathstart g1, pathstart g2}"
lp15@62533
   654
    by (fastforce simp: pathstart_def pathfinish_def path_image_def)
lp15@62533
   655
  with \<open>arc g1\<close> \<open>arc g2\<close> show ?thesis using that by blast
lp15@62533
   656
qed
lp15@62533
   657
lp15@62533
   658
lemma simple_path_join_loop_eq:
hoelzl@63594
   659
  assumes "pathfinish g2 = pathstart g1" "pathfinish g1 = pathstart g2"
lp15@62533
   660
    shows "simple_path(g1 +++ g2) \<longleftrightarrow>
lp15@62533
   661
             arc g1 \<and> arc g2 \<and> path_image g1 \<inter> path_image g2 \<subseteq> {pathstart g1, pathstart g2}"
lp15@62533
   662
by (metis assms simple_path_joinE simple_path_join_loop)
lp15@62533
   663
lp15@62533
   664
lemma arc_join_eq:
hoelzl@63594
   665
  assumes "pathfinish g1 = pathstart g2"
lp15@62533
   666
    shows "arc(g1 +++ g2) \<longleftrightarrow>
lp15@62533
   667
           arc g1 \<and> arc g2 \<and> path_image g1 \<inter> path_image g2 \<subseteq> {pathstart g2}"
lp15@62533
   668
           (is "?lhs = ?rhs")
hoelzl@63594
   669
proof
lp15@62533
   670
  assume ?lhs
lp15@62533
   671
  then have "simple_path(g1 +++ g2)" by (rule arc_imp_simple_path)
hoelzl@63594
   672
  then have *: "\<And>x y. \<lbrakk>0 \<le> x; x \<le> 1; 0 \<le> y; y \<le> 1; (g1 +++ g2) x = (g1 +++ g2) y\<rbrakk>
lp15@62533
   673
               \<Longrightarrow> x = y \<or> x = 0 \<and> y = 1 \<or> x = 1 \<and> y = 0"
lp15@62533
   674
    using assms by (simp add: simple_path_def)
lp15@62533
   675
  have False if "g1 0 = g2 u" "0 \<le> u" "u \<le> 1" for u
lp15@62533
   676
    using * [of 0 "(u + 1) / 2"] that assms arc_distinct_ends [OF \<open>?lhs\<close>]
lp15@62533
   677
    by (auto simp: joinpaths_def pathstart_def pathfinish_def split_ifs divide_simps)
nipkow@69508
   678
  then have n1: "pathstart g1 \<notin> path_image g2"
lp15@62533
   679
    unfolding pathstart_def path_image_def
lp15@62533
   680
    using atLeastAtMost_iff by blast
lp15@62533
   681
  show ?rhs using \<open>?lhs\<close>
lp15@62533
   682
    apply (rule simple_path_joinE [OF arc_imp_simple_path assms])
lp15@62533
   683
    using n1 by force
lp15@62533
   684
next
lp15@62533
   685
  assume ?rhs then show ?lhs
lp15@62533
   686
    using assms
lp15@62533
   687
    by (fastforce simp: pathfinish_def pathstart_def intro!: arc_join)
lp15@62533
   688
qed
lp15@62533
   689
hoelzl@63594
   690
lemma arc_join_eq_alt:
lp15@62533
   691
        "pathfinish g1 = pathstart g2
lp15@62533
   692
        \<Longrightarrow> (arc(g1 +++ g2) \<longleftrightarrow>
lp15@62533
   693
             arc g1 \<and> arc g2 \<and>
lp15@62533
   694
             path_image g1 \<inter> path_image g2 = {pathstart g2})"
lp15@62533
   695
using pathfinish_in_path_image by (fastforce simp: arc_join_eq)
lp15@62533
   696
lp15@62533
   697
immler@67962
   698
subsection%unimportant\<open>The joining of paths is associative\<close>
lp15@62533
   699
lp15@62533
   700
lemma path_assoc:
lp15@62533
   701
    "\<lbrakk>pathfinish p = pathstart q; pathfinish q = pathstart r\<rbrakk>
lp15@62533
   702
     \<Longrightarrow> path(p +++ (q +++ r)) \<longleftrightarrow> path((p +++ q) +++ r)"
lp15@62533
   703
by simp
lp15@62533
   704
hoelzl@63594
   705
lemma simple_path_assoc:
hoelzl@63594
   706
  assumes "pathfinish p = pathstart q" "pathfinish q = pathstart r"
lp15@62533
   707
    shows "simple_path (p +++ (q +++ r)) \<longleftrightarrow> simple_path ((p +++ q) +++ r)"
lp15@62533
   708
proof (cases "pathstart p = pathfinish r")
lp15@62533
   709
  case True show ?thesis
lp15@62533
   710
  proof
lp15@62533
   711
    assume "simple_path (p +++ q +++ r)"
lp15@62533
   712
    with assms True show "simple_path ((p +++ q) +++ r)"
hoelzl@63594
   713
      by (fastforce simp add: simple_path_join_loop_eq arc_join_eq path_image_join
lp15@62533
   714
                    dest: arc_distinct_ends [of r])
lp15@62533
   715
  next
lp15@62533
   716
    assume 0: "simple_path ((p +++ q) +++ r)"
lp15@62533
   717
    with assms True have q: "pathfinish r \<notin> path_image q"
hoelzl@63594
   718
      using arc_distinct_ends
lp15@62533
   719
      by (fastforce simp add: simple_path_join_loop_eq arc_join_eq path_image_join)
lp15@62533
   720
    have "pathstart r \<notin> path_image p"
lp15@62533
   721
      using assms
hoelzl@63594
   722
      by (metis 0 IntI arc_distinct_ends arc_join_eq_alt empty_iff insert_iff
lp15@62533
   723
              pathfinish_in_path_image pathfinish_join simple_path_joinE)
lp15@62533
   724
    with assms 0 q True show "simple_path (p +++ q +++ r)"
hoelzl@63594
   725
      by (auto simp: simple_path_join_loop_eq arc_join_eq path_image_join
lp15@62533
   726
               dest!: subsetD [OF _ IntI])
lp15@62533
   727
  qed
lp15@62533
   728
next
lp15@62533
   729
  case False
lp15@62533
   730
  { fix x :: 'a
lp15@62533
   731
    assume a: "path_image p \<inter> path_image q \<subseteq> {pathstart q}"
lp15@62533
   732
              "(path_image p \<union> path_image q) \<inter> path_image r \<subseteq> {pathstart r}"
lp15@62533
   733
              "x \<in> path_image p" "x \<in> path_image r"
lp15@62533
   734
    have "pathstart r \<in> path_image q"
lp15@62533
   735
      by (metis assms(2) pathfinish_in_path_image)
lp15@62533
   736
    with a have "x = pathstart q"
lp15@62533
   737
      by blast
lp15@62533
   738
  }
hoelzl@63594
   739
  with False assms show ?thesis
lp15@62533
   740
    by (auto simp: simple_path_eq_arc simple_path_join_loop_eq arc_join_eq path_image_join)
lp15@62533
   741
qed
lp15@62533
   742
hoelzl@63594
   743
lemma arc_assoc:
lp15@62533
   744
     "\<lbrakk>pathfinish p = pathstart q; pathfinish q = pathstart r\<rbrakk>
lp15@62533
   745
      \<Longrightarrow> arc(p +++ (q +++ r)) \<longleftrightarrow> arc((p +++ q) +++ r)"
lp15@62533
   746
by (simp add: arc_simple_path simple_path_assoc)
lp15@62533
   747
immler@67962
   748
subsubsection%unimportant\<open>Symmetry and loops\<close>
lp15@62620
   749
lp15@62620
   750
lemma path_sym:
lp15@62620
   751
    "\<lbrakk>pathfinish p = pathstart q; pathfinish q = pathstart p\<rbrakk> \<Longrightarrow> path(p +++ q) \<longleftrightarrow> path(q +++ p)"
lp15@62620
   752
  by auto
lp15@62620
   753
lp15@62620
   754
lemma simple_path_sym:
lp15@62620
   755
    "\<lbrakk>pathfinish p = pathstart q; pathfinish q = pathstart p\<rbrakk>
lp15@62620
   756
     \<Longrightarrow> simple_path(p +++ q) \<longleftrightarrow> simple_path(q +++ p)"
lp15@62620
   757
by (metis (full_types) inf_commute insert_commute simple_path_joinE simple_path_join_loop)
lp15@62620
   758
lp15@62620
   759
lemma path_image_sym:
lp15@62620
   760
    "\<lbrakk>pathfinish p = pathstart q; pathfinish q = pathstart p\<rbrakk>
lp15@62620
   761
     \<Longrightarrow> path_image(p +++ q) = path_image(q +++ p)"
lp15@62620
   762
by (simp add: path_image_join sup_commute)
lp15@62620
   763
lp15@62533
   764
nipkow@69518
   765
subsection\<open>Subpath\<close>
lp15@60809
   766
immler@67962
   767
definition%important subpath :: "real \<Rightarrow> real \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> real \<Rightarrow> 'a::real_normed_vector"
paulson@60303
   768
  where "subpath a b g \<equiv> \<lambda>x. g((b - a) * x + a)"
paulson@60303
   769
lp15@61762
   770
lemma path_image_subpath_gen:
lp15@61762
   771
  fixes g :: "_ \<Rightarrow> 'a::real_normed_vector"
paulson@60303
   772
  shows "path_image(subpath u v g) = g ` (closed_segment u v)"
haftmann@69661
   773
  by (auto simp add: closed_segment_real_eq path_image_def subpath_def)
paulson@60303
   774
lp15@61762
   775
lemma path_image_subpath:
paulson@60303
   776
  fixes g :: "real \<Rightarrow> 'a::real_normed_vector"
paulson@60303
   777
  shows "path_image(subpath u v g) = (if u \<le> v then g ` {u..v} else g ` {v..u})"
lp15@61762
   778
  by (simp add: path_image_subpath_gen closed_segment_eq_real_ivl)
paulson@60303
   779
lp15@65038
   780
lemma path_image_subpath_commute:
lp15@65038
   781
  fixes g :: "real \<Rightarrow> 'a::real_normed_vector"
lp15@65038
   782
  shows "path_image(subpath u v g) = path_image(subpath v u g)"
lp15@65038
   783
  by (simp add: path_image_subpath_gen closed_segment_eq_real_ivl)
lp15@65038
   784
paulson@60303
   785
lemma path_subpath [simp]:
paulson@60303
   786
  fixes g :: "real \<Rightarrow> 'a::real_normed_vector"
paulson@60303
   787
  assumes "path g" "u \<in> {0..1}" "v \<in> {0..1}"
paulson@60303
   788
    shows "path(subpath u v g)"
paulson@60303
   789
proof -
lp15@68096
   790
  have "continuous_on {0..1} (g \<circ> (\<lambda>x. ((v-u) * x+ u)))"
paulson@60303
   791
    apply (rule continuous_intros | simp)+
paulson@60303
   792
    apply (simp add: image_affinity_atLeastAtMost [where c=u])
paulson@60303
   793
    using assms
paulson@60303
   794
    apply (auto simp: path_def continuous_on_subset)
paulson@60303
   795
    done
paulson@60303
   796
  then show ?thesis
paulson@60303
   797
    by (simp add: path_def subpath_def)
wenzelm@49653
   798
qed
huffman@36583
   799
paulson@60303
   800
lemma pathstart_subpath [simp]: "pathstart(subpath u v g) = g(u)"
paulson@60303
   801
  by (simp add: pathstart_def subpath_def)
paulson@60303
   802
paulson@60303
   803
lemma pathfinish_subpath [simp]: "pathfinish(subpath u v g) = g(v)"
paulson@60303
   804
  by (simp add: pathfinish_def subpath_def)
paulson@60303
   805
paulson@60303
   806
lemma subpath_trivial [simp]: "subpath 0 1 g = g"
paulson@60303
   807
  by (simp add: subpath_def)
paulson@60303
   808
paulson@60303
   809
lemma subpath_reversepath: "subpath 1 0 g = reversepath g"
paulson@60303
   810
  by (simp add: reversepath_def subpath_def)
paulson@60303
   811
paulson@60303
   812
lemma reversepath_subpath: "reversepath(subpath u v g) = subpath v u g"
paulson@60303
   813
  by (simp add: reversepath_def subpath_def algebra_simps)
paulson@60303
   814
lp15@68096
   815
lemma subpath_translation: "subpath u v ((\<lambda>x. a + x) \<circ> g) = (\<lambda>x. a + x) \<circ> subpath u v g"
paulson@60303
   816
  by (rule ext) (simp add: subpath_def)
paulson@60303
   817
lp15@68096
   818
lemma subpath_linear_image: "linear f \<Longrightarrow> subpath u v (f \<circ> g) = f \<circ> subpath u v g"
paulson@60303
   819
  by (rule ext) (simp add: subpath_def)
paulson@60303
   820
lp15@60809
   821
lemma affine_ineq:
lp15@60809
   822
  fixes x :: "'a::linordered_idom"
lp15@61762
   823
  assumes "x \<le> 1" "v \<le> u"
paulson@60303
   824
    shows "v + x * u \<le> u + x * v"
paulson@60303
   825
proof -
paulson@60303
   826
  have "(1-x)*(u-v) \<ge> 0"
paulson@60303
   827
    using assms by auto
paulson@60303
   828
  then show ?thesis
paulson@60303
   829
    by (simp add: algebra_simps)
wenzelm@49653
   830
qed
huffman@36583
   831
lp15@61711
   832
lemma sum_le_prod1:
lp15@61711
   833
  fixes a::real shows "\<lbrakk>a \<le> 1; b \<le> 1\<rbrakk> \<Longrightarrow> a + b \<le> 1 + a * b"
lp15@61711
   834
by (metis add.commute affine_ineq less_eq_real_def mult.right_neutral)
lp15@61711
   835
lp15@60809
   836
lemma simple_path_subpath_eq:
paulson@60303
   837
  "simple_path(subpath u v g) \<longleftrightarrow>
paulson@60303
   838
     path(subpath u v g) \<and> u\<noteq>v \<and>
paulson@60303
   839
     (\<forall>x y. x \<in> closed_segment u v \<and> y \<in> closed_segment u v \<and> g x = g y
paulson@60303
   840
                \<longrightarrow> x = y \<or> x = u \<and> y = v \<or> x = v \<and> y = u)"
paulson@60303
   841
    (is "?lhs = ?rhs")
paulson@60303
   842
proof (rule iffI)
paulson@60303
   843
  assume ?lhs
paulson@60303
   844
  then have p: "path (\<lambda>x. g ((v - u) * x + u))"
lp15@60809
   845
        and sim: "(\<And>x y. \<lbrakk>x\<in>{0..1}; y\<in>{0..1}; g ((v - u) * x + u) = g ((v - u) * y + u)\<rbrakk>
paulson@60303
   846
                  \<Longrightarrow> x = y \<or> x = 0 \<and> y = 1 \<or> x = 1 \<and> y = 0)"
paulson@60303
   847
    by (auto simp: simple_path_def subpath_def)
paulson@60303
   848
  { fix x y
paulson@60303
   849
    assume "x \<in> closed_segment u v" "y \<in> closed_segment u v" "g x = g y"
paulson@60303
   850
    then have "x = y \<or> x = u \<and> y = v \<or> x = v \<and> y = u"
paulson@60303
   851
    using sim [of "(x-u)/(v-u)" "(y-u)/(v-u)"] p
lp15@60809
   852
    by (auto simp: closed_segment_real_eq image_affinity_atLeastAtMost divide_simps
nipkow@62390
   853
       split: if_split_asm)
paulson@60303
   854
  } moreover
paulson@60303
   855
  have "path(subpath u v g) \<and> u\<noteq>v"
paulson@60303
   856
    using sim [of "1/3" "2/3"] p
paulson@60303
   857
    by (auto simp: subpath_def)
paulson@60303
   858
  ultimately show ?rhs
paulson@60303
   859
    by metis
paulson@60303
   860
next
paulson@60303
   861
  assume ?rhs
lp15@60809
   862
  then
paulson@60303
   863
  have d1: "\<And>x y. \<lbrakk>g x = g y; u \<le> x; x \<le> v; u \<le> y; y \<le> v\<rbrakk> \<Longrightarrow> x = y \<or> x = u \<and> y = v \<or> x = v \<and> y = u"
paulson@60303
   864
   and d2: "\<And>x y. \<lbrakk>g x = g y; v \<le> x; x \<le> u; v \<le> y; y \<le> u\<rbrakk> \<Longrightarrow> x = y \<or> x = u \<and> y = v \<or> x = v \<and> y = u"
paulson@60303
   865
   and ne: "u < v \<or> v < u"
paulson@60303
   866
   and psp: "path (subpath u v g)"
paulson@60303
   867
    by (auto simp: closed_segment_real_eq image_affinity_atLeastAtMost)
paulson@60303
   868
  have [simp]: "\<And>x. u + x * v = v + x * u \<longleftrightarrow> u=v \<or> x=1"
paulson@60303
   869
    by algebra
paulson@60303
   870
  show ?lhs using psp ne
paulson@60303
   871
    unfolding simple_path_def subpath_def
paulson@60303
   872
    by (fastforce simp add: algebra_simps affine_ineq mult_left_mono crossproduct_eq dest: d1 d2)
paulson@60303
   873
qed
paulson@60303
   874
lp15@60809
   875
lemma arc_subpath_eq:
paulson@60303
   876
  "arc(subpath u v g) \<longleftrightarrow> path(subpath u v g) \<and> u\<noteq>v \<and> inj_on g (closed_segment u v)"
paulson@60303
   877
    (is "?lhs = ?rhs")
paulson@60303
   878
proof (rule iffI)
paulson@60303
   879
  assume ?lhs
paulson@60303
   880
  then have p: "path (\<lambda>x. g ((v - u) * x + u))"
lp15@60809
   881
        and sim: "(\<And>x y. \<lbrakk>x\<in>{0..1}; y\<in>{0..1}; g ((v - u) * x + u) = g ((v - u) * y + u)\<rbrakk>
paulson@60303
   882
                  \<Longrightarrow> x = y)"
paulson@60303
   883
    by (auto simp: arc_def inj_on_def subpath_def)
paulson@60303
   884
  { fix x y
paulson@60303
   885
    assume "x \<in> closed_segment u v" "y \<in> closed_segment u v" "g x = g y"
paulson@60303
   886
    then have "x = y"
paulson@60303
   887
    using sim [of "(x-u)/(v-u)" "(y-u)/(v-u)"] p
lp15@68096
   888
    by (force simp: inj_on_def closed_segment_real_eq image_affinity_atLeastAtMost divide_simps
nipkow@62390
   889
       split: if_split_asm)
paulson@60303
   890
  } moreover
paulson@60303
   891
  have "path(subpath u v g) \<and> u\<noteq>v"
paulson@60303
   892
    using sim [of "1/3" "2/3"] p
paulson@60303
   893
    by (auto simp: subpath_def)
paulson@60303
   894
  ultimately show ?rhs
lp15@60809
   895
    unfolding inj_on_def
paulson@60303
   896
    by metis
paulson@60303
   897
next
paulson@60303
   898
  assume ?rhs
lp15@60809
   899
  then
paulson@60303
   900
  have d1: "\<And>x y. \<lbrakk>g x = g y; u \<le> x; x \<le> v; u \<le> y; y \<le> v\<rbrakk> \<Longrightarrow> x = y"
paulson@60303
   901
   and d2: "\<And>x y. \<lbrakk>g x = g y; v \<le> x; x \<le> u; v \<le> y; y \<le> u\<rbrakk> \<Longrightarrow> x = y"
paulson@60303
   902
   and ne: "u < v \<or> v < u"
paulson@60303
   903
   and psp: "path (subpath u v g)"
paulson@60303
   904
    by (auto simp: inj_on_def closed_segment_real_eq image_affinity_atLeastAtMost)
paulson@60303
   905
  show ?lhs using psp ne
paulson@60303
   906
    unfolding arc_def subpath_def inj_on_def
paulson@60303
   907
    by (auto simp: algebra_simps affine_ineq mult_left_mono crossproduct_eq dest: d1 d2)
paulson@60303
   908
qed
paulson@60303
   909
paulson@60303
   910
lp15@60809
   911
lemma simple_path_subpath:
paulson@60303
   912
  assumes "simple_path g" "u \<in> {0..1}" "v \<in> {0..1}" "u \<noteq> v"
paulson@60303
   913
  shows "simple_path(subpath u v g)"
paulson@60303
   914
  using assms
paulson@60303
   915
  apply (simp add: simple_path_subpath_eq simple_path_imp_path)
paulson@60303
   916
  apply (simp add: simple_path_def closed_segment_real_eq image_affinity_atLeastAtMost, fastforce)
paulson@60303
   917
  done
paulson@60303
   918
paulson@60303
   919
lemma arc_simple_path_subpath:
paulson@60303
   920
    "\<lbrakk>simple_path g; u \<in> {0..1}; v \<in> {0..1}; g u \<noteq> g v\<rbrakk> \<Longrightarrow> arc(subpath u v g)"
paulson@60303
   921
  by (force intro: simple_path_subpath simple_path_imp_arc)
paulson@60303
   922
paulson@60303
   923
lemma arc_subpath_arc:
paulson@60303
   924
    "\<lbrakk>arc g; u \<in> {0..1}; v \<in> {0..1}; u \<noteq> v\<rbrakk> \<Longrightarrow> arc(subpath u v g)"
paulson@60303
   925
  by (meson arc_def arc_imp_simple_path arc_simple_path_subpath inj_onD)
paulson@60303
   926
lp15@60809
   927
lemma arc_simple_path_subpath_interior:
paulson@60303
   928
    "\<lbrakk>simple_path g; u \<in> {0..1}; v \<in> {0..1}; u \<noteq> v; \<bar>u-v\<bar> < 1\<rbrakk> \<Longrightarrow> arc(subpath u v g)"
paulson@60303
   929
    apply (rule arc_simple_path_subpath)
paulson@60303
   930
    apply (force simp: simple_path_def)+
paulson@60303
   931
    done
paulson@60303
   932
lp15@60809
   933
lemma path_image_subpath_subset:
lp15@68532
   934
    "\<lbrakk>u \<in> {0..1}; v \<in> {0..1}\<rbrakk> \<Longrightarrow> path_image(subpath u v g) \<subseteq> path_image g"
lp15@61762
   935
  apply (simp add: closed_segment_real_eq image_affinity_atLeastAtMost path_image_subpath)
paulson@60303
   936
  apply (auto simp: path_image_def)
lp15@68532
   937
  done  
paulson@60303
   938
paulson@60303
   939
lemma join_subpaths_middle: "subpath (0) ((1 / 2)) p +++ subpath ((1 / 2)) 1 p = p"
paulson@60303
   940
  by (rule ext) (simp add: joinpaths_def subpath_def divide_simps)
wenzelm@53640
   941
nipkow@69514
   942
immler@67962
   943
subsection%unimportant\<open>There is a subpath to the frontier\<close>
paulson@61518
   944
paulson@61518
   945
lemma subpath_to_frontier_explicit:
paulson@61518
   946
    fixes S :: "'a::metric_space set"
paulson@61518
   947
    assumes g: "path g" and "pathfinish g \<notin> S"
paulson@61518
   948
    obtains u where "0 \<le> u" "u \<le> 1"
paulson@61518
   949
                "\<And>x. 0 \<le> x \<and> x < u \<Longrightarrow> g x \<in> interior S"
paulson@61518
   950
                "(g u \<notin> interior S)" "(u = 0 \<or> g u \<in> closure S)"
paulson@61518
   951
proof -
paulson@61518
   952
  have gcon: "continuous_on {0..1} g"     using g by (simp add: path_def)
paulson@61518
   953
  then have com: "compact ({0..1} \<inter> {u. g u \<in> closure (- S)})"
paulson@61518
   954
    apply (simp add: Int_commute [of "{0..1}"] compact_eq_bounded_closed closed_vimage_Int [unfolded vimage_def])
paulson@61518
   955
    using compact_eq_bounded_closed apply fastforce
paulson@61518
   956
    done
paulson@61518
   957
  have "1 \<in> {u. g u \<in> closure (- S)}"
paulson@61518
   958
    using assms by (simp add: pathfinish_def closure_def)
paulson@61518
   959
  then have dis: "{0..1} \<inter> {u. g u \<in> closure (- S)} \<noteq> {}"
paulson@61518
   960
    using atLeastAtMost_iff zero_le_one by blast
paulson@61518
   961
  then obtain u where "0 \<le> u" "u \<le> 1" and gu: "g u \<in> closure (- S)"
paulson@61518
   962
                  and umin: "\<And>t. \<lbrakk>0 \<le> t; t \<le> 1; g t \<in> closure (- S)\<rbrakk> \<Longrightarrow> u \<le> t"
paulson@61518
   963
    using compact_attains_inf [OF com dis] by fastforce
paulson@61518
   964
  then have umin': "\<And>t. \<lbrakk>0 \<le> t; t \<le> 1; t < u\<rbrakk> \<Longrightarrow>  g t \<in> S"
paulson@61518
   965
    using closure_def by fastforce
paulson@61518
   966
  { assume "u \<noteq> 0"
wenzelm@61808
   967
    then have "u > 0" using \<open>0 \<le> u\<close> by auto
paulson@61518
   968
    { fix e::real assume "e > 0"
lp15@62397
   969
      obtain d where "d>0" and d: "\<And>x'. \<lbrakk>x' \<in> {0..1}; dist x' u \<le> d\<rbrakk> \<Longrightarrow> dist (g x') (g u) < e"
lp15@62397
   970
        using continuous_onE [OF gcon _ \<open>e > 0\<close>] \<open>0 \<le> _\<close> \<open>_ \<le> 1\<close> atLeastAtMost_iff by auto
lp15@62397
   971
      have *: "dist (max 0 (u - d / 2)) u \<le> d"
wenzelm@61808
   972
        using \<open>0 \<le> u\<close> \<open>u \<le> 1\<close> \<open>d > 0\<close> by (simp add: dist_real_def)
paulson@61518
   973
      have "\<exists>y\<in>S. dist y (g u) < e"
wenzelm@61808
   974
        using \<open>0 < u\<close> \<open>u \<le> 1\<close> \<open>d > 0\<close>
paulson@61518
   975
        by (force intro: d [OF _ *] umin')
paulson@61518
   976
    }
paulson@61518
   977
    then have "g u \<in> closure S"
paulson@61518
   978
      by (simp add: frontier_def closure_approachable)
paulson@61518
   979
  }
paulson@61518
   980
  then show ?thesis
paulson@61518
   981
    apply (rule_tac u=u in that)
wenzelm@61808
   982
    apply (auto simp: \<open>0 \<le> u\<close> \<open>u \<le> 1\<close> gu interior_closure umin)
wenzelm@61808
   983
    using \<open>_ \<le> 1\<close> interior_closure umin apply fastforce
paulson@61518
   984
    done
paulson@61518
   985
qed
paulson@61518
   986
paulson@61518
   987
lemma subpath_to_frontier_strong:
paulson@61518
   988
    assumes g: "path g" and "pathfinish g \<notin> S"
paulson@61518
   989
    obtains u where "0 \<le> u" "u \<le> 1" "g u \<notin> interior S"
paulson@61518
   990
                    "u = 0 \<or> (\<forall>x. 0 \<le> x \<and> x < 1 \<longrightarrow> subpath 0 u g x \<in> interior S)  \<and>  g u \<in> closure S"
paulson@61518
   991
proof -
paulson@61518
   992
  obtain u where "0 \<le> u" "u \<le> 1"
paulson@61518
   993
             and gxin: "\<And>x. 0 \<le> x \<and> x < u \<Longrightarrow> g x \<in> interior S"
paulson@61518
   994
             and gunot: "(g u \<notin> interior S)" and u0: "(u = 0 \<or> g u \<in> closure S)"
paulson@61518
   995
    using subpath_to_frontier_explicit [OF assms] by blast
paulson@61518
   996
  show ?thesis
wenzelm@61808
   997
    apply (rule that [OF \<open>0 \<le> u\<close> \<open>u \<le> 1\<close>])
paulson@61518
   998
    apply (simp add: gunot)
wenzelm@61808
   999
    using \<open>0 \<le> u\<close> u0 by (force simp: subpath_def gxin)
paulson@61518
  1000
qed
paulson@61518
  1001
paulson@61518
  1002
lemma subpath_to_frontier:
paulson@61518
  1003
    assumes g: "path g" and g0: "pathstart g \<in> closure S" and g1: "pathfinish g \<notin> S"
paulson@61518
  1004
    obtains u where "0 \<le> u" "u \<le> 1" "g u \<in> frontier S" "(path_image(subpath 0 u g) - {g u}) \<subseteq> interior S"
paulson@61518
  1005
proof -
paulson@61518
  1006
  obtain u where "0 \<le> u" "u \<le> 1"
paulson@61518
  1007
             and notin: "g u \<notin> interior S"
paulson@61518
  1008
             and disj: "u = 0 \<or>
paulson@61518
  1009
                        (\<forall>x. 0 \<le> x \<and> x < 1 \<longrightarrow> subpath 0 u g x \<in> interior S) \<and> g u \<in> closure S"
paulson@61518
  1010
    using subpath_to_frontier_strong [OF g g1] by blast
paulson@61518
  1011
  show ?thesis
wenzelm@61808
  1012
    apply (rule that [OF \<open>0 \<le> u\<close> \<open>u \<le> 1\<close>])
paulson@61518
  1013
    apply (metis DiffI disj frontier_def g0 notin pathstart_def)
wenzelm@61808
  1014
    using \<open>0 \<le> u\<close> g0 disj
lp15@61762
  1015
    apply (simp add: path_image_subpath_gen)
paulson@61518
  1016
    apply (auto simp: closed_segment_eq_real_ivl pathstart_def pathfinish_def subpath_def)
paulson@61518
  1017
    apply (rename_tac y)
paulson@61518
  1018
    apply (drule_tac x="y/u" in spec)
nipkow@62390
  1019
    apply (auto split: if_split_asm)
paulson@61518
  1020
    done
paulson@61518
  1021
qed
paulson@61518
  1022
paulson@61518
  1023
lemma exists_path_subpath_to_frontier:
paulson@61518
  1024
    fixes S :: "'a::real_normed_vector set"
paulson@61518
  1025
    assumes "path g" "pathstart g \<in> closure S" "pathfinish g \<notin> S"
paulson@61518
  1026
    obtains h where "path h" "pathstart h = pathstart g" "path_image h \<subseteq> path_image g"
paulson@61518
  1027
                    "path_image h - {pathfinish h} \<subseteq> interior S"
paulson@61518
  1028
                    "pathfinish h \<in> frontier S"
paulson@61518
  1029
proof -
paulson@61518
  1030
  obtain u where u: "0 \<le> u" "u \<le> 1" "g u \<in> frontier S" "(path_image(subpath 0 u g) - {g u}) \<subseteq> interior S"
paulson@61518
  1031
    using subpath_to_frontier [OF assms] by blast
paulson@61518
  1032
  show ?thesis
paulson@61518
  1033
    apply (rule that [of "subpath 0 u g"])
paulson@61518
  1034
    using assms u
lp15@61762
  1035
    apply (simp_all add: path_image_subpath)
paulson@61518
  1036
    apply (simp add: pathstart_def)
paulson@61518
  1037
    apply (force simp: closed_segment_eq_real_ivl path_image_def)
paulson@61518
  1038
    done
paulson@61518
  1039
qed
paulson@61518
  1040
paulson@61518
  1041
lemma exists_path_subpath_to_frontier_closed:
paulson@61518
  1042
    fixes S :: "'a::real_normed_vector set"
paulson@61518
  1043
    assumes S: "closed S" and g: "path g" and g0: "pathstart g \<in> S" and g1: "pathfinish g \<notin> S"
paulson@61518
  1044
    obtains h where "path h" "pathstart h = pathstart g" "path_image h \<subseteq> path_image g \<inter> S"
paulson@61518
  1045
                    "pathfinish h \<in> frontier S"
paulson@61518
  1046
proof -
paulson@61518
  1047
  obtain h where h: "path h" "pathstart h = pathstart g" "path_image h \<subseteq> path_image g"
paulson@61518
  1048
                    "path_image h - {pathfinish h} \<subseteq> interior S"
paulson@61518
  1049
                    "pathfinish h \<in> frontier S"
paulson@61518
  1050
    using exists_path_subpath_to_frontier [OF g _ g1] closure_closed [OF S] g0 by auto
paulson@61518
  1051
  show ?thesis
wenzelm@61808
  1052
    apply (rule that [OF \<open>path h\<close>])
paulson@61518
  1053
    using assms h
paulson@61518
  1054
    apply auto
paulson@62087
  1055
    apply (metis Diff_single_insert frontier_subset_eq insert_iff interior_subset subset_iff)
paulson@61518
  1056
    done
paulson@61518
  1057
qed
wenzelm@49653
  1058
nipkow@69514
  1059
nipkow@69514
  1060
subsection \<open>Shift Path to Start at Some Given Point\<close>
huffman@36583
  1061
immler@67962
  1062
definition%important shiftpath :: "real \<Rightarrow> (real \<Rightarrow> 'a::topological_space) \<Rightarrow> real \<Rightarrow> 'a"
wenzelm@53640
  1063
  where "shiftpath a f = (\<lambda>x. if (a + x) \<le> 1 then f (a + x) else f (a + x - 1))"
huffman@36583
  1064
wenzelm@53640
  1065
lemma pathstart_shiftpath: "a \<le> 1 \<Longrightarrow> pathstart (shiftpath a g) = g a"
huffman@36583
  1066
  unfolding pathstart_def shiftpath_def by auto
huffman@36583
  1067
wenzelm@49653
  1068
lemma pathfinish_shiftpath:
wenzelm@53640
  1069
  assumes "0 \<le> a"
wenzelm@53640
  1070
    and "pathfinish g = pathstart g"
wenzelm@53640
  1071
  shows "pathfinish (shiftpath a g) = g a"
wenzelm@53640
  1072
  using assms
wenzelm@53640
  1073
  unfolding pathstart_def pathfinish_def shiftpath_def
huffman@36583
  1074
  by auto
huffman@36583
  1075
huffman@36583
  1076
lemma endpoints_shiftpath:
wenzelm@53640
  1077
  assumes "pathfinish g = pathstart g"
wenzelm@53640
  1078
    and "a \<in> {0 .. 1}"
wenzelm@53640
  1079
  shows "pathfinish (shiftpath a g) = g a"
wenzelm@53640
  1080
    and "pathstart (shiftpath a g) = g a"
wenzelm@53640
  1081
  using assms
wenzelm@53640
  1082
  by (auto intro!: pathfinish_shiftpath pathstart_shiftpath)
huffman@36583
  1083
huffman@36583
  1084
lemma closed_shiftpath:
wenzelm@53640
  1085
  assumes "pathfinish g = pathstart g"
wenzelm@53640
  1086
    and "a \<in> {0..1}"
wenzelm@53640
  1087
  shows "pathfinish (shiftpath a g) = pathstart (shiftpath a g)"
wenzelm@53640
  1088
  using endpoints_shiftpath[OF assms]
wenzelm@53640
  1089
  by auto
huffman@36583
  1090
huffman@36583
  1091
lemma path_shiftpath:
wenzelm@53640
  1092
  assumes "path g"
wenzelm@53640
  1093
    and "pathfinish g = pathstart g"
wenzelm@53640
  1094
    and "a \<in> {0..1}"
wenzelm@53640
  1095
  shows "path (shiftpath a g)"
wenzelm@49653
  1096
proof -
wenzelm@53640
  1097
  have *: "{0 .. 1} = {0 .. 1-a} \<union> {1-a .. 1}"
wenzelm@53640
  1098
    using assms(3) by auto
wenzelm@49653
  1099
  have **: "\<And>x. x + a = 1 \<Longrightarrow> g (x + a - 1) = g (x + a)"
wenzelm@53640
  1100
    using assms(2)[unfolded pathfinish_def pathstart_def]
wenzelm@53640
  1101
    by auto
wenzelm@49653
  1102
  show ?thesis
wenzelm@49653
  1103
    unfolding path_def shiftpath_def *
lp15@68096
  1104
  proof (rule continuous_on_closed_Un)
lp15@68096
  1105
    have contg: "continuous_on {0..1} g"
lp15@68096
  1106
      using \<open>path g\<close> path_def by blast
lp15@68096
  1107
    show "continuous_on {0..1-a} (\<lambda>x. if a + x \<le> 1 then g (a + x) else g (a + x - 1))"
lp15@68096
  1108
    proof (rule continuous_on_eq)
lp15@68096
  1109
      show "continuous_on {0..1-a} (g \<circ> (+) a)"
lp15@68096
  1110
        by (intro continuous_intros continuous_on_subset [OF contg]) (use \<open>a \<in> {0..1}\<close> in auto)
lp15@68096
  1111
    qed auto
lp15@68096
  1112
    show "continuous_on {1-a..1} (\<lambda>x. if a + x \<le> 1 then g (a + x) else g (a + x - 1))"
lp15@68096
  1113
    proof (rule continuous_on_eq)
lp15@68096
  1114
      show "continuous_on {1-a..1} (g \<circ> (+) (a - 1))"
lp15@68096
  1115
        by (intro continuous_intros continuous_on_subset [OF contg]) (use \<open>a \<in> {0..1}\<close> in auto)
lp15@68096
  1116
    qed (auto simp:  "**" add.commute add_diff_eq)
lp15@68096
  1117
  qed auto
wenzelm@49653
  1118
qed
huffman@36583
  1119
wenzelm@49653
  1120
lemma shiftpath_shiftpath:
wenzelm@53640
  1121
  assumes "pathfinish g = pathstart g"
wenzelm@53640
  1122
    and "a \<in> {0..1}"
wenzelm@53640
  1123
    and "x \<in> {0..1}"
huffman@36583
  1124
  shows "shiftpath (1 - a) (shiftpath a g) x = g x"
wenzelm@53640
  1125
  using assms
wenzelm@53640
  1126
  unfolding pathfinish_def pathstart_def shiftpath_def
wenzelm@53640
  1127
  by auto
huffman@36583
  1128
huffman@36583
  1129
lemma path_image_shiftpath:
lp15@68096
  1130
  assumes a: "a \<in> {0..1}"
wenzelm@53640
  1131
    and "pathfinish g = pathstart g"
wenzelm@53640
  1132
  shows "path_image (shiftpath a g) = path_image g"
wenzelm@49653
  1133
proof -
wenzelm@49653
  1134
  { fix x
lp15@68096
  1135
    assume g: "g 1 = g 0" "x \<in> {0..1::real}" and gne: "\<And>y. y\<in>{0..1} \<inter> {x. \<not> a + x \<le> 1} \<Longrightarrow> g x \<noteq> g (a + y - 1)"
wenzelm@49654
  1136
    then have "\<exists>y\<in>{0..1} \<inter> {x. a + x \<le> 1}. g x = g (a + y)"
wenzelm@49653
  1137
    proof (cases "a \<le> x")
wenzelm@49653
  1138
      case False
wenzelm@49654
  1139
      then show ?thesis
wenzelm@49653
  1140
        apply (rule_tac x="1 + x - a" in bexI)
lp15@68096
  1141
        using g gne[of "1 + x - a"] a
lp15@68096
  1142
        apply (force simp: field_simps)+
wenzelm@49653
  1143
        done
wenzelm@49653
  1144
    next
wenzelm@49653
  1145
      case True
wenzelm@53640
  1146
      then show ?thesis
lp15@68096
  1147
        using g a  by (rule_tac x="x - a" in bexI) (auto simp: field_simps)
wenzelm@49653
  1148
    qed
wenzelm@49653
  1149
  }
wenzelm@49654
  1150
  then show ?thesis
wenzelm@53640
  1151
    using assms
wenzelm@53640
  1152
    unfolding shiftpath_def path_image_def pathfinish_def pathstart_def
lp15@68096
  1153
    by (auto simp: image_iff)
wenzelm@49653
  1154
qed
wenzelm@49653
  1155
lp15@64788
  1156
lemma simple_path_shiftpath:
lp15@64788
  1157
  assumes "simple_path g" "pathfinish g = pathstart g" and a: "0 \<le> a" "a \<le> 1"
lp15@64788
  1158
    shows "simple_path (shiftpath a g)"
lp15@64788
  1159
  unfolding simple_path_def
lp15@64788
  1160
proof (intro conjI impI ballI)
lp15@64788
  1161
  show "path (shiftpath a g)"
lp15@64788
  1162
    by (simp add: assms path_shiftpath simple_path_imp_path)
lp15@64788
  1163
  have *: "\<And>x y. \<lbrakk>g x = g y; x \<in> {0..1}; y \<in> {0..1}\<rbrakk> \<Longrightarrow> x = y \<or> x = 0 \<and> y = 1 \<or> x = 1 \<and> y = 0"
lp15@64788
  1164
    using assms by (simp add:  simple_path_def)
lp15@64788
  1165
  show "x = y \<or> x = 0 \<and> y = 1 \<or> x = 1 \<and> y = 0"
lp15@64788
  1166
    if "x \<in> {0..1}" "y \<in> {0..1}" "shiftpath a g x = shiftpath a g y" for x y
lp15@64788
  1167
    using that a unfolding shiftpath_def
lp15@68096
  1168
    by (force split: if_split_asm dest!: *)
lp15@64788
  1169
qed
huffman@36583
  1170
nipkow@69514
  1171
nipkow@69514
  1172
subsection \<open>Straight-Line Paths\<close>
huffman@36583
  1173
immler@67962
  1174
definition%important linepath :: "'a::real_normed_vector \<Rightarrow> 'a \<Rightarrow> real \<Rightarrow> 'a"
wenzelm@49653
  1175
  where "linepath a b = (\<lambda>x. (1 - x) *\<^sub>R a + x *\<^sub>R b)"
huffman@36583
  1176
wenzelm@53640
  1177
lemma pathstart_linepath[simp]: "pathstart (linepath a b) = a"
wenzelm@53640
  1178
  unfolding pathstart_def linepath_def
wenzelm@53640
  1179
  by auto
huffman@36583
  1180
wenzelm@53640
  1181
lemma pathfinish_linepath[simp]: "pathfinish (linepath a b) = b"
wenzelm@53640
  1182
  unfolding pathfinish_def linepath_def
wenzelm@53640
  1183
  by auto
huffman@36583
  1184
eberlm@68721
  1185
lemma linepath_inner: "linepath a b x \<bullet> v = linepath (a \<bullet> v) (b \<bullet> v) x"
eberlm@68721
  1186
  by (simp add: linepath_def algebra_simps)
eberlm@68721
  1187
eberlm@68721
  1188
lemma Re_linepath': "Re (linepath a b x) = linepath (Re a) (Re b) x"
eberlm@68721
  1189
  by (simp add: linepath_def)
eberlm@68721
  1190
eberlm@68721
  1191
lemma Im_linepath': "Im (linepath a b x) = linepath (Im a) (Im b) x"
eberlm@68721
  1192
  by (simp add: linepath_def)
eberlm@68721
  1193
eberlm@68721
  1194
lemma linepath_0': "linepath a b 0 = a"
eberlm@68721
  1195
  by (simp add: linepath_def)
eberlm@68721
  1196
eberlm@68721
  1197
lemma linepath_1': "linepath a b 1 = b"
eberlm@68721
  1198
  by (simp add: linepath_def)
eberlm@68721
  1199
huffman@36583
  1200
lemma continuous_linepath_at[intro]: "continuous (at x) (linepath a b)"
wenzelm@53640
  1201
  unfolding linepath_def
wenzelm@53640
  1202
  by (intro continuous_intros)
huffman@36583
  1203
lp15@61762
  1204
lemma continuous_on_linepath [intro,continuous_intros]: "continuous_on s (linepath a b)"
wenzelm@53640
  1205
  using continuous_linepath_at
wenzelm@53640
  1206
  by (auto intro!: continuous_at_imp_continuous_on)
huffman@36583
  1207
lp15@62618
  1208
lemma path_linepath[iff]: "path (linepath a b)"
wenzelm@53640
  1209
  unfolding path_def
wenzelm@53640
  1210
  by (rule continuous_on_linepath)
huffman@36583
  1211
wenzelm@53640
  1212
lemma path_image_linepath[simp]: "path_image (linepath a b) = closed_segment a b"
wenzelm@49653
  1213
  unfolding path_image_def segment linepath_def
paulson@60303
  1214
  by auto
wenzelm@49653
  1215
wenzelm@53640
  1216
lemma reversepath_linepath[simp]: "reversepath (linepath a b) = linepath b a"
wenzelm@49653
  1217
  unfolding reversepath_def linepath_def
huffman@36583
  1218
  by auto
huffman@36583
  1219
lp15@61762
  1220
lemma linepath_0 [simp]: "linepath 0 b x = x *\<^sub>R b"
lp15@61762
  1221
  by (simp add: linepath_def)
lp15@61762
  1222
eberlm@68721
  1223
lemma linepath_cnj: "cnj (linepath a b x) = linepath (cnj a) (cnj b) x"
eberlm@68721
  1224
  by (simp add: linepath_def)
eberlm@68721
  1225
paulson@60303
  1226
lemma arc_linepath:
lp15@62618
  1227
  assumes "a \<noteq> b" shows [simp]: "arc (linepath a b)"
huffman@36583
  1228
proof -
wenzelm@53640
  1229
  {
wenzelm@53640
  1230
    fix x y :: "real"
huffman@36583
  1231
    assume "x *\<^sub>R b + y *\<^sub>R a = x *\<^sub>R a + y *\<^sub>R b"
wenzelm@53640
  1232
    then have "(x - y) *\<^sub>R a = (x - y) *\<^sub>R b"
wenzelm@53640
  1233
      by (simp add: algebra_simps)
wenzelm@53640
  1234
    with assms have "x = y"
wenzelm@53640
  1235
      by simp
wenzelm@53640
  1236
  }
wenzelm@49654
  1237
  then show ?thesis
lp15@60809
  1238
    unfolding arc_def inj_on_def
lp15@68096
  1239
    by (fastforce simp: algebra_simps linepath_def)
wenzelm@49653
  1240
qed
huffman@36583
  1241
wenzelm@53640
  1242
lemma simple_path_linepath[intro]: "a \<noteq> b \<Longrightarrow> simple_path (linepath a b)"
lp15@68096
  1243
  by (simp add: arc_imp_simple_path)
wenzelm@49653
  1244
lp15@61711
  1245
lemma linepath_trivial [simp]: "linepath a a x = a"
lp15@61711
  1246
  by (simp add: linepath_def real_vector.scale_left_diff_distrib)
lp15@61738
  1247
lp15@64394
  1248
lemma linepath_refl: "linepath a a = (\<lambda>x. a)"
lp15@64394
  1249
  by auto
lp15@64394
  1250
lp15@61711
  1251
lemma subpath_refl: "subpath a a g = linepath (g a) (g a)"
lp15@61711
  1252
  by (simp add: subpath_def linepath_def algebra_simps)
lp15@61711
  1253
lp15@62618
  1254
lemma linepath_of_real: "(linepath (of_real a) (of_real b) x) = of_real ((1 - x)*a + x*b)"
lp15@62618
  1255
  by (simp add: scaleR_conv_of_real linepath_def)
lp15@62618
  1256
lp15@62618
  1257
lemma of_real_linepath: "of_real (linepath a b x) = linepath (of_real a) (of_real b) x"
lp15@62618
  1258
  by (metis linepath_of_real mult.right_neutral of_real_def real_scaleR_def)
lp15@62618
  1259
lp15@63881
  1260
lemma inj_on_linepath:
lp15@63881
  1261
  assumes "a \<noteq> b" shows "inj_on (linepath a b) {0..1}"
lp15@63881
  1262
proof (clarsimp simp: inj_on_def linepath_def)
lp15@63881
  1263
  fix x y
lp15@63881
  1264
  assume "(1 - x) *\<^sub>R a + x *\<^sub>R b = (1 - y) *\<^sub>R a + y *\<^sub>R b" "0 \<le> x" "x \<le> 1" "0 \<le> y" "y \<le> 1"
lp15@63881
  1265
  then have "x *\<^sub>R (a - b) = y *\<^sub>R (a - b)"
lp15@63881
  1266
    by (auto simp: algebra_simps)
lp15@63881
  1267
  then show "x=y"
lp15@63881
  1268
    using assms by auto
lp15@63881
  1269
qed
lp15@63881
  1270
lp15@69144
  1271
lemma linepath_le_1:
lp15@69144
  1272
  fixes a::"'a::linordered_idom" shows "\<lbrakk>a \<le> 1; b \<le> 1; 0 \<le> u; u \<le> 1\<rbrakk> \<Longrightarrow> (1 - u) * a + u * b \<le> 1"
lp15@69144
  1273
  using mult_left_le [of a "1-u"] mult_left_le [of b u] by auto
lp15@69144
  1274
lp15@62618
  1275
immler@67962
  1276
subsection%unimportant\<open>Segments via convex hulls\<close>
lp15@62618
  1277
lp15@62618
  1278
lemma segments_subset_convex_hull:
lp15@62618
  1279
    "closed_segment a b \<subseteq> (convex hull {a,b,c})"
lp15@62618
  1280
    "closed_segment a c \<subseteq> (convex hull {a,b,c})"
lp15@62618
  1281
    "closed_segment b c \<subseteq> (convex hull {a,b,c})"
lp15@62618
  1282
    "closed_segment b a \<subseteq> (convex hull {a,b,c})"
lp15@62618
  1283
    "closed_segment c a \<subseteq> (convex hull {a,b,c})"
lp15@62618
  1284
    "closed_segment c b \<subseteq> (convex hull {a,b,c})"
lp15@62618
  1285
by (auto simp: segment_convex_hull linepath_of_real  elim!: rev_subsetD [OF _ hull_mono])
lp15@62618
  1286
lp15@62618
  1287
lemma midpoints_in_convex_hull:
lp15@62618
  1288
  assumes "x \<in> convex hull s" "y \<in> convex hull s"
lp15@62618
  1289
    shows "midpoint x y \<in> convex hull s"
lp15@62618
  1290
proof -
lp15@62618
  1291
  have "(1 - inverse(2)) *\<^sub>R x + inverse(2) *\<^sub>R y \<in> convex hull s"
lp15@68096
  1292
    by (rule convexD_alt) (use assms in auto)
lp15@62618
  1293
  then show ?thesis
lp15@62618
  1294
    by (simp add: midpoint_def algebra_simps)
lp15@62618
  1295
qed
lp15@62618
  1296
lp15@62618
  1297
lemma not_in_interior_convex_hull_3:
lp15@62618
  1298
  fixes a :: "complex"
lp15@62618
  1299
  shows "a \<notin> interior(convex hull {a,b,c})"
lp15@62618
  1300
        "b \<notin> interior(convex hull {a,b,c})"
lp15@62618
  1301
        "c \<notin> interior(convex hull {a,b,c})"
lp15@62618
  1302
  by (auto simp: card_insert_le_m1 not_in_interior_convex_hull)
lp15@62618
  1303
lp15@62618
  1304
lemma midpoint_in_closed_segment [simp]: "midpoint a b \<in> closed_segment a b"
lp15@62618
  1305
  using midpoints_in_convex_hull segment_convex_hull by blast
lp15@62618
  1306
lp15@62618
  1307
lemma midpoint_in_open_segment [simp]: "midpoint a b \<in> open_segment a b \<longleftrightarrow> a \<noteq> b"
lp15@64122
  1308
  by (simp add: open_segment_def)
lp15@64122
  1309
lp15@64122
  1310
lemma continuous_IVT_local_extremum:
lp15@64122
  1311
  fixes f :: "'a::euclidean_space \<Rightarrow> real"
lp15@64122
  1312
  assumes contf: "continuous_on (closed_segment a b) f"
lp15@64122
  1313
      and "a \<noteq> b" "f a = f b"
lp15@64122
  1314
  obtains z where "z \<in> open_segment a b"
lp15@64122
  1315
                  "(\<forall>w \<in> closed_segment a b. (f w) \<le> (f z)) \<or>
lp15@64122
  1316
                   (\<forall>w \<in> closed_segment a b. (f z) \<le> (f w))"
lp15@64122
  1317
proof -
lp15@64122
  1318
  obtain c where "c \<in> closed_segment a b" and c: "\<And>y. y \<in> closed_segment a b \<Longrightarrow> f y \<le> f c"
lp15@64122
  1319
    using continuous_attains_sup [of "closed_segment a b" f] contf by auto
lp15@64122
  1320
  obtain d where "d \<in> closed_segment a b" and d: "\<And>y. y \<in> closed_segment a b \<Longrightarrow> f d \<le> f y"
lp15@64122
  1321
    using continuous_attains_inf [of "closed_segment a b" f] contf by auto
lp15@64122
  1322
  show ?thesis
lp15@64122
  1323
  proof (cases "c \<in> open_segment a b \<or> d \<in> open_segment a b")
lp15@64122
  1324
    case True
lp15@64122
  1325
    then show ?thesis
lp15@64122
  1326
      using c d that by blast
lp15@64122
  1327
  next
lp15@64122
  1328
    case False
lp15@64122
  1329
    then have "(c = a \<or> c = b) \<and> (d = a \<or> d = b)"
lp15@64122
  1330
      by (simp add: \<open>c \<in> closed_segment a b\<close> \<open>d \<in> closed_segment a b\<close> open_segment_def)
lp15@64122
  1331
    with \<open>a \<noteq> b\<close> \<open>f a = f b\<close> c d show ?thesis
lp15@64122
  1332
      by (rule_tac z = "midpoint a b" in that) (fastforce+)
lp15@64122
  1333
  qed
lp15@64122
  1334
qed
lp15@64122
  1335
lp15@64122
  1336
text\<open>An injective map into R is also an open map w.r.T. the universe, and conversely. \<close>
lp15@64122
  1337
proposition injective_eq_1d_open_map_UNIV:
lp15@64122
  1338
  fixes f :: "real \<Rightarrow> real"
lp15@64122
  1339
  assumes contf: "continuous_on S f" and S: "is_interval S"
lp15@64122
  1340
    shows "inj_on f S \<longleftrightarrow> (\<forall>T. open T \<and> T \<subseteq> S \<longrightarrow> open(f ` T))"
lp15@64122
  1341
          (is "?lhs = ?rhs")
lp15@64122
  1342
proof safe
lp15@64122
  1343
  fix T
lp15@64122
  1344
  assume injf: ?lhs and "open T" and "T \<subseteq> S"
lp15@64122
  1345
  have "\<exists>U. open U \<and> f x \<in> U \<and> U \<subseteq> f ` T" if "x \<in> T" for x
lp15@64122
  1346
  proof -
lp15@64122
  1347
    obtain \<delta> where "\<delta> > 0" and \<delta>: "cball x \<delta> \<subseteq> T"
lp15@64122
  1348
      using \<open>open T\<close> \<open>x \<in> T\<close> open_contains_cball_eq by blast
lp15@64122
  1349
    show ?thesis
lp15@64122
  1350
    proof (intro exI conjI)
lp15@64122
  1351
      have "closed_segment (x-\<delta>) (x+\<delta>) = {x-\<delta>..x+\<delta>}"
lp15@64122
  1352
        using \<open>0 < \<delta>\<close> by (auto simp: closed_segment_eq_real_ivl)
lp15@68096
  1353
      also have "\<dots> \<subseteq> S"
lp15@64122
  1354
        using \<delta> \<open>T \<subseteq> S\<close> by (auto simp: dist_norm subset_eq)
lp15@64122
  1355
      finally have "f ` (open_segment (x-\<delta>) (x+\<delta>)) = open_segment (f (x-\<delta>)) (f (x+\<delta>))"
lp15@64122
  1356
        using continuous_injective_image_open_segment_1
lp15@64122
  1357
        by (metis continuous_on_subset [OF contf] inj_on_subset [OF injf])
lp15@64122
  1358
      then show "open (f ` {x-\<delta><..<x+\<delta>})"
lp15@64122
  1359
        using \<open>0 < \<delta>\<close> by (simp add: open_segment_eq_real_ivl)
lp15@64122
  1360
      show "f x \<in> f ` {x - \<delta><..<x + \<delta>}"
lp15@64122
  1361
        by (auto simp: \<open>\<delta> > 0\<close>)
lp15@64122
  1362
      show "f ` {x - \<delta><..<x + \<delta>} \<subseteq> f ` T"
lp15@64122
  1363
        using \<delta> by (auto simp: dist_norm subset_iff)
lp15@64122
  1364
    qed
lp15@64122
  1365
  qed
lp15@64122
  1366
  with open_subopen show "open (f ` T)"
lp15@64122
  1367
    by blast
lp15@64122
  1368
next
lp15@64122
  1369
  assume R: ?rhs
lp15@64122
  1370
  have False if xy: "x \<in> S" "y \<in> S" and "f x = f y" "x \<noteq> y" for x y
lp15@64122
  1371
  proof -
lp15@64122
  1372
    have "open (f ` open_segment x y)"
lp15@64122
  1373
      using R
lp15@64122
  1374
      by (metis S convex_contains_open_segment is_interval_convex open_greaterThanLessThan open_segment_eq_real_ivl xy)
lp15@64122
  1375
    moreover
lp15@64122
  1376
    have "continuous_on (closed_segment x y) f"
lp15@64122
  1377
      by (meson S closed_segment_subset contf continuous_on_subset is_interval_convex that)
lp15@64122
  1378
    then obtain \<xi> where "\<xi> \<in> open_segment x y"
lp15@64122
  1379
                    and \<xi>: "(\<forall>w \<in> closed_segment x y. (f w) \<le> (f \<xi>)) \<or>
lp15@64122
  1380
                            (\<forall>w \<in> closed_segment x y. (f \<xi>) \<le> (f w))"
lp15@64122
  1381
      using continuous_IVT_local_extremum [of x y f] \<open>f x = f y\<close> \<open>x \<noteq> y\<close> by blast
lp15@64122
  1382
    ultimately obtain e where "e>0" and e: "\<And>u. dist u (f \<xi>) < e \<Longrightarrow> u \<in> f ` open_segment x y"
lp15@64122
  1383
      using open_dist by (metis image_eqI)
lp15@64122
  1384
    have fin: "f \<xi> + (e/2) \<in> f ` open_segment x y" "f \<xi> - (e/2) \<in> f ` open_segment x y"
lp15@64122
  1385
      using e [of "f \<xi> + (e/2)"] e [of "f \<xi> - (e/2)"] \<open>e > 0\<close> by (auto simp: dist_norm)
lp15@64122
  1386
    show ?thesis
lp15@64122
  1387
      using \<xi> \<open>0 < e\<close> fin open_closed_segment by fastforce
lp15@64122
  1388
  qed
lp15@64122
  1389
  then show ?lhs
lp15@64122
  1390
    by (force simp: inj_on_def)
lp15@64122
  1391
qed
huffman@36583
  1392
nipkow@69514
  1393
immler@67962
  1394
subsection%unimportant \<open>Bounding a point away from a path\<close>
huffman@36583
  1395
huffman@36583
  1396
lemma not_on_path_ball:
huffman@36583
  1397
  fixes g :: "real \<Rightarrow> 'a::heine_borel"
wenzelm@53640
  1398
  assumes "path g"
lp15@68096
  1399
    and z: "z \<notin> path_image g"
wenzelm@53640
  1400
  shows "\<exists>e > 0. ball z e \<inter> path_image g = {}"
wenzelm@49653
  1401
proof -
lp15@68096
  1402
  have "closed (path_image g)"
lp15@68096
  1403
    by (simp add: \<open>path g\<close> closed_path_image)
lp15@68096
  1404
  then obtain a where "a \<in> path_image g" "\<forall>y \<in> path_image g. dist z a \<le> dist z y"
lp15@68096
  1405
    by (auto intro: distance_attains_inf[OF _ path_image_nonempty, of g z])
wenzelm@49654
  1406
  then show ?thesis
lp15@68096
  1407
    by (rule_tac x="dist z a" in exI) (use dist_commute z in auto)
wenzelm@49653
  1408
qed
huffman@36583
  1409
huffman@36583
  1410
lemma not_on_path_cball:
huffman@36583
  1411
  fixes g :: "real \<Rightarrow> 'a::heine_borel"
wenzelm@53640
  1412
  assumes "path g"
wenzelm@53640
  1413
    and "z \<notin> path_image g"
wenzelm@49653
  1414
  shows "\<exists>e>0. cball z e \<inter> (path_image g) = {}"
wenzelm@49653
  1415
proof -
wenzelm@53640
  1416
  obtain e where "ball z e \<inter> path_image g = {}" "e > 0"
wenzelm@49653
  1417
    using not_on_path_ball[OF assms] by auto
wenzelm@53640
  1418
  moreover have "cball z (e/2) \<subseteq> ball z e"
wenzelm@60420
  1419
    using \<open>e > 0\<close> by auto
wenzelm@53640
  1420
  ultimately show ?thesis
lp15@68096
  1421
    by (rule_tac x="e/2" in exI) auto
wenzelm@49653
  1422
qed
wenzelm@49653
  1423
nipkow@69518
  1424
subsection \<open>Path component\<close>
nipkow@69518
  1425
nipkow@69518
  1426
text \<open>Original formalization by Tom Hales\<close>
huffman@36583
  1427
immler@67962
  1428
definition%important "path_component s x y \<longleftrightarrow>
wenzelm@49653
  1429
  (\<exists>g. path g \<and> path_image g \<subseteq> s \<and> pathstart g = x \<and> pathfinish g = y)"
huffman@36583
  1430
immler@67962
  1431
abbreviation%important
nipkow@69518
  1432
  "path_component_set s x \<equiv> Collect (path_component s x)"
lp15@61426
  1433
wenzelm@53640
  1434
lemmas path_defs = path_def pathstart_def pathfinish_def path_image_def path_component_def
huffman@36583
  1435
wenzelm@49653
  1436
lemma path_component_mem:
wenzelm@49653
  1437
  assumes "path_component s x y"
wenzelm@53640
  1438
  shows "x \<in> s" and "y \<in> s"
wenzelm@53640
  1439
  using assms
wenzelm@53640
  1440
  unfolding path_defs
wenzelm@53640
  1441
  by auto
huffman@36583
  1442
wenzelm@49653
  1443
lemma path_component_refl:
wenzelm@49653
  1444
  assumes "x \<in> s"
wenzelm@49653
  1445
  shows "path_component s x x"
wenzelm@49653
  1446
  unfolding path_defs
wenzelm@49653
  1447
  apply (rule_tac x="\<lambda>u. x" in exI)
wenzelm@53640
  1448
  using assms
hoelzl@56371
  1449
  apply (auto intro!: continuous_intros)
wenzelm@53640
  1450
  done
huffman@36583
  1451
huffman@36583
  1452
lemma path_component_refl_eq: "path_component s x x \<longleftrightarrow> x \<in> s"
wenzelm@49653
  1453
  by (auto intro!: path_component_mem path_component_refl)
huffman@36583
  1454
huffman@36583
  1455
lemma path_component_sym: "path_component s x y \<Longrightarrow> path_component s y x"
wenzelm@49653
  1456
  unfolding path_component_def
wenzelm@49653
  1457
  apply (erule exE)
lp15@68096
  1458
  apply (rule_tac x="reversepath g" in exI, auto)
wenzelm@49653
  1459
  done
huffman@36583
  1460
wenzelm@49653
  1461
lemma path_component_trans:
lp15@61426
  1462
  assumes "path_component s x y" and "path_component s y z"
wenzelm@49653
  1463
  shows "path_component s x z"
wenzelm@49653
  1464
  using assms
wenzelm@49653
  1465
  unfolding path_component_def
wenzelm@53640
  1466
  apply (elim exE)
wenzelm@49653
  1467
  apply (rule_tac x="g +++ ga" in exI)
lp15@68096
  1468
  apply (auto simp: path_image_join)
wenzelm@49653
  1469
  done
huffman@36583
  1470
wenzelm@53640
  1471
lemma path_component_of_subset: "s \<subseteq> t \<Longrightarrow> path_component s x y \<Longrightarrow> path_component t x y"
huffman@36583
  1472
  unfolding path_component_def by auto
huffman@36583
  1473
lp15@69939
  1474
lemma path_component_linepath:
lp15@61426
  1475
    fixes s :: "'a::real_normed_vector set"
lp15@61426
  1476
    shows "closed_segment a b \<subseteq> s \<Longrightarrow> path_component s a b"
lp15@68096
  1477
  unfolding path_component_def
lp15@68096
  1478
  by (rule_tac x="linepath a b" in exI, auto)
lp15@61426
  1479
immler@67962
  1480
subsubsection%unimportant \<open>Path components as sets\<close>
huffman@36583
  1481
wenzelm@49653
  1482
lemma path_component_set:
lp15@61426
  1483
  "path_component_set s x =
wenzelm@49653
  1484
    {y. (\<exists>g. path g \<and> path_image g \<subseteq> s \<and> pathstart g = x \<and> pathfinish g = y)}"
lp15@61426
  1485
  by (auto simp: path_component_def)
huffman@36583
  1486
lp15@61426
  1487
lemma path_component_subset: "path_component_set s x \<subseteq> s"
lp15@68096
  1488
  by (auto simp: path_component_mem(2))
huffman@36583
  1489
lp15@61426
  1490
lemma path_component_eq_empty: "path_component_set s x = {} \<longleftrightarrow> x \<notin> s"
paulson@60303
  1491
  using path_component_mem path_component_refl_eq
paulson@60303
  1492
    by fastforce
huffman@36583
  1493
lp15@61426
  1494
lemma path_component_mono:
lp15@61426
  1495
     "s \<subseteq> t \<Longrightarrow> (path_component_set s x) \<subseteq> (path_component_set t x)"
lp15@61426
  1496
  by (simp add: Collect_mono path_component_of_subset)
lp15@61426
  1497
lp15@61426
  1498
lemma path_component_eq:
lp15@61426
  1499
   "y \<in> path_component_set s x \<Longrightarrow> path_component_set s y = path_component_set s x"
lp15@61426
  1500
by (metis (no_types, lifting) Collect_cong mem_Collect_eq path_component_sym path_component_trans)
lp15@61426
  1501
nipkow@69514
  1502
wenzelm@60420
  1503
subsection \<open>Path connectedness of a space\<close>
huffman@36583
  1504
immler@67962
  1505
definition%important "path_connected s \<longleftrightarrow>
wenzelm@53640
  1506
  (\<forall>x\<in>s. \<forall>y\<in>s. \<exists>g. path g \<and> path_image g \<subseteq> s \<and> pathstart g = x \<and> pathfinish g = y)"
huffman@36583
  1507
lp15@69939
  1508
lemma path_connectedin_iff_path_connected_real [simp]:
lp15@69939
  1509
     "path_connectedin euclideanreal S \<longleftrightarrow> path_connected S"
lp15@69939
  1510
  by (simp add: path_connectedin path_connected_def path_defs)
lp15@69939
  1511
huffman@36583
  1512
lemma path_connected_component: "path_connected s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>y\<in>s. path_component s x y)"
huffman@36583
  1513
  unfolding path_connected_def path_component_def by auto
huffman@36583
  1514
lp15@61426
  1515
lemma path_connected_component_set: "path_connected s \<longleftrightarrow> (\<forall>x\<in>s. path_component_set s x = s)"
lp15@61694
  1516
  unfolding path_connected_component path_component_subset
lp15@61426
  1517
  using path_component_mem by blast
lp15@61426
  1518
lp15@61426
  1519
lemma path_component_maximal:
lp15@61426
  1520
     "\<lbrakk>x \<in> t; path_connected t; t \<subseteq> s\<rbrakk> \<Longrightarrow> t \<subseteq> (path_component_set s x)"
lp15@61426
  1521
  by (metis path_component_mono path_connected_component_set)
huffman@36583
  1522
huffman@36583
  1523
lemma convex_imp_path_connected:
huffman@36583
  1524
  fixes s :: "'a::real_normed_vector set"
wenzelm@53640
  1525
  assumes "convex s"
wenzelm@53640
  1526
  shows "path_connected s"
wenzelm@49653
  1527
  unfolding path_connected_def
lp15@66793
  1528
  using assms convex_contains_segment by fastforce
huffman@36583
  1529
lp15@62620
  1530
lemma path_connected_UNIV [iff]: "path_connected (UNIV :: 'a::real_normed_vector set)"
lp15@62620
  1531
  by (simp add: convex_imp_path_connected)
lp15@62620
  1532
lp15@62620
  1533
lemma path_component_UNIV: "path_component_set UNIV x = (UNIV :: 'a::real_normed_vector set)"
lp15@62620
  1534
  using path_connected_component_set by auto
lp15@62620
  1535
wenzelm@49653
  1536
lemma path_connected_imp_connected:
lp15@64788
  1537
  assumes "path_connected S"
lp15@64788
  1538
  shows "connected S"
lp15@66793
  1539
proof (rule connectedI)
wenzelm@49653
  1540
  fix e1 e2
lp15@64788
  1541
  assume as: "open e1" "open e2" "S \<subseteq> e1 \<union> e2" "e1 \<inter> e2 \<inter> S = {}" "e1 \<inter> S \<noteq> {}" "e2 \<inter> S \<noteq> {}"
lp15@64788
  1542
  then obtain x1 x2 where obt:"x1 \<in> e1 \<inter> S" "x2 \<in> e2 \<inter> S"
wenzelm@53640
  1543
    by auto
lp15@64788
  1544
  then obtain g where g: "path g" "path_image g \<subseteq> S" "pathstart g = x1" "pathfinish g = x2"
huffman@36583
  1545
    using assms[unfolded path_connected_def,rule_format,of x1 x2] by auto
wenzelm@49653
  1546
  have *: "connected {0..1::real}"
wenzelm@49653
  1547
    by (auto intro!: convex_connected convex_real_interval)
wenzelm@49653
  1548
  have "{0..1} \<subseteq> {x \<in> {0..1}. g x \<in> e1} \<union> {x \<in> {0..1}. g x \<in> e2}"
wenzelm@49653
  1549
    using as(3) g(2)[unfolded path_defs] by blast
wenzelm@49653
  1550
  moreover have "{x \<in> {0..1}. g x \<in> e1} \<inter> {x \<in> {0..1}. g x \<in> e2} = {}"
wenzelm@53640
  1551
    using as(4) g(2)[unfolded path_defs]
wenzelm@53640
  1552
    unfolding subset_eq
wenzelm@53640
  1553
    by auto
wenzelm@49653
  1554
  moreover have "{x \<in> {0..1}. g x \<in> e1} \<noteq> {} \<and> {x \<in> {0..1}. g x \<in> e2} \<noteq> {}"
wenzelm@53640
  1555
    using g(3,4)[unfolded path_defs]
wenzelm@53640
  1556
    using obt
huffman@36583
  1557
    by (simp add: ex_in_conv [symmetric], metis zero_le_one order_refl)
wenzelm@49653
  1558
  ultimately show False
wenzelm@53640
  1559
    using *[unfolded connected_local not_ex, rule_format,
lp15@66884
  1560
      of "{0..1} \<inter> g -` e1" "{0..1} \<inter> g -` e2"]
lp15@63301
  1561
    using continuous_openin_preimage_gen[OF g(1)[unfolded path_def] as(1)]
lp15@63301
  1562
    using continuous_openin_preimage_gen[OF g(1)[unfolded path_def] as(2)]
wenzelm@49653
  1563
    by auto
wenzelm@49653
  1564
qed
huffman@36583
  1565
huffman@36583
  1566
lemma open_path_component:
lp15@64788
  1567
  fixes S :: "'a::real_normed_vector set"
lp15@64788
  1568
  assumes "open S"
lp15@64788
  1569
  shows "open (path_component_set S x)"
wenzelm@49653
  1570
  unfolding open_contains_ball
wenzelm@49653
  1571
proof
wenzelm@49653
  1572
  fix y
lp15@64788
  1573
  assume as: "y \<in> path_component_set S x"
lp15@64788
  1574
  then have "y \<in> S"
lp15@66793
  1575
    by (simp add: path_component_mem(2))
lp15@64788
  1576
  then obtain e where e: "e > 0" "ball y e \<subseteq> S"
wenzelm@53640
  1577
    using assms[unfolded open_contains_ball]
wenzelm@53640
  1578
    by auto
lp15@66793
  1579
have "\<And>u. dist y u < e \<Longrightarrow> path_component S x u"
lp15@66793
  1580
      by (metis (full_types) as centre_in_ball convex_ball convex_imp_path_connected e mem_Collect_eq mem_ball path_component_eq path_component_of_subset path_connected_component)
lp15@66793
  1581
  then show "\<exists>e > 0. ball y e \<subseteq> path_component_set S x"
lp15@66793
  1582
    using \<open>e>0\<close> by auto
wenzelm@49653
  1583
qed
huffman@36583
  1584
huffman@36583
  1585
lemma open_non_path_component:
lp15@64788
  1586
  fixes S :: "'a::real_normed_vector set"
lp15@64788
  1587
  assumes "open S"
lp15@64788
  1588
  shows "open (S - path_component_set S x)"
wenzelm@49653
  1589
  unfolding open_contains_ball
wenzelm@49653
  1590
proof
wenzelm@49653
  1591
  fix y
lp15@68096
  1592
  assume y: "y \<in> S - path_component_set S x"
lp15@64788
  1593
  then obtain e where e: "e > 0" "ball y e \<subseteq> S"
lp15@68096
  1594
    using assms openE by auto
lp15@64788
  1595
  show "\<exists>e>0. ball y e \<subseteq> S - path_component_set S x"
lp15@68096
  1596
  proof (intro exI conjI subsetI DiffI notI)
lp15@68096
  1597
    show "\<And>x. x \<in> ball y e \<Longrightarrow> x \<in> S"
lp15@68096
  1598
      using e by blast
lp15@68096
  1599
    show False if "z \<in> ball y e" "z \<in> path_component_set S x" for z
lp15@68096
  1600
    proof -
lp15@68096
  1601
      have "y \<in> path_component_set S z"
lp15@68096
  1602
        by (meson assms convex_ball convex_imp_path_connected e open_contains_ball_eq open_path_component path_component_maximal that(1))
lp15@68096
  1603
      then have "y \<in> path_component_set S x"
lp15@68096
  1604
        using path_component_eq that(2) by blast
lp15@68096
  1605
      then show False
lp15@68096
  1606
        using y by blast
lp15@68096
  1607
    qed
lp15@68096
  1608
  qed (use e in auto)
wenzelm@49653
  1609
qed
huffman@36583
  1610
huffman@36583
  1611
lemma connected_open_path_connected:
lp15@64788
  1612
  fixes S :: "'a::real_normed_vector set"
lp15@64788
  1613
  assumes "open S"
lp15@64788
  1614
    and "connected S"
lp15@64788
  1615
  shows "path_connected S"
wenzelm@49653
  1616
  unfolding path_connected_component_set
wenzelm@49653
  1617
proof (rule, rule, rule path_component_subset, rule)
wenzelm@49653
  1618
  fix x y
lp15@64788
  1619
  assume "x \<in> S" and "y \<in> S"
lp15@64788
  1620
  show "y \<in> path_component_set S x"
wenzelm@49653
  1621
  proof (rule ccontr)
wenzelm@53640
  1622
    assume "\<not> ?thesis"
lp15@64788
  1623
    moreover have "path_component_set S x \<inter> S \<noteq> {}"
lp15@64788
  1624
      using \<open>x \<in> S\<close> path_component_eq_empty path_component_subset[of S x]
wenzelm@53640
  1625
      by auto
wenzelm@49653
  1626
    ultimately
wenzelm@49653
  1627
    show False
lp15@64788
  1628
      using \<open>y \<in> S\<close> open_non_path_component[OF assms(1)] open_path_component[OF assms(1)]
wenzelm@53640
  1629
      using assms(2)[unfolded connected_def not_ex, rule_format,
lp15@64788
  1630
        of "path_component_set S x" "S - path_component_set S x"]
wenzelm@49653
  1631
      by auto
wenzelm@49653
  1632
  qed
wenzelm@49653
  1633
qed
huffman@36583
  1634
huffman@36583
  1635
lemma path_connected_continuous_image:
lp15@64788
  1636
  assumes "continuous_on S f"
lp15@64788
  1637
    and "path_connected S"
lp15@64788
  1638
  shows "path_connected (f ` S)"
wenzelm@49653
  1639
  unfolding path_connected_def
wenzelm@49653
  1640
proof (rule, rule)
wenzelm@49653
  1641
  fix x' y'
lp15@64788
  1642
  assume "x' \<in> f ` S" "y' \<in> f ` S"
lp15@64788
  1643
  then obtain x y where x: "x \<in> S" and y: "y \<in> S" and x': "x' = f x" and y': "y' = f y"
wenzelm@53640
  1644
    by auto
lp15@64788
  1645
  from x y obtain g where "path g \<and> path_image g \<subseteq> S \<and> pathstart g = x \<and> pathfinish g = y"
wenzelm@53640
  1646
    using assms(2)[unfolded path_connected_def] by fast
lp15@64788
  1647
  then show "\<exists>g. path g \<and> path_image g \<subseteq> f ` S \<and> pathstart g = x' \<and> pathfinish g = y'"
wenzelm@53640
  1648
    unfolding x' y'
wenzelm@49653
  1649
    apply (rule_tac x="f \<circ> g" in exI)
wenzelm@49653
  1650
    unfolding path_defs
hoelzl@51481
  1651
    apply (intro conjI continuous_on_compose continuous_on_subset[OF assms(1)])
hoelzl@51481
  1652
    apply auto
wenzelm@49653
  1653
    done
wenzelm@49653
  1654
qed
huffman@36583
  1655
lp15@64788
  1656
lemma path_connected_translationI:
lp15@64788
  1657
  fixes a :: "'a :: topological_group_add"
lp15@64788
  1658
  assumes "path_connected S" shows "path_connected ((\<lambda>x. a + x) ` S)"
lp15@64788
  1659
  by (intro path_connected_continuous_image assms continuous_intros)
lp15@64788
  1660
lp15@64788
  1661
lemma path_connected_translation:
lp15@64788
  1662
  fixes a :: "'a :: topological_group_add"
lp15@64788
  1663
  shows "path_connected ((\<lambda>x. a + x) ` S) = path_connected S"
lp15@64788
  1664
proof -
nipkow@67399
  1665
  have "\<forall>x y. (+) (x::'a) ` (+) (0 - x) ` y = y"
lp15@64788
  1666
    by (simp add: image_image)
lp15@64788
  1667
  then show ?thesis
lp15@64788
  1668
    by (metis (no_types) path_connected_translationI)
lp15@64788
  1669
qed
lp15@64788
  1670
lp15@64788
  1671
lemma path_connected_segment [simp]:
paulson@61518
  1672
    fixes a :: "'a::real_normed_vector"
paulson@61518
  1673
    shows "path_connected (closed_segment a b)"
paulson@61518
  1674
  by (simp add: convex_imp_path_connected)
paulson@61518
  1675
lp15@64788
  1676
lemma path_connected_open_segment [simp]:
paulson@61518
  1677
    fixes a :: "'a::real_normed_vector"
paulson@61518
  1678
    shows "path_connected (open_segment a b)"
paulson@61518
  1679
  by (simp add: convex_imp_path_connected)
paulson@61518
  1680
huffman@36583
  1681
lemma homeomorphic_path_connectedness:
lp15@68096
  1682
  "S homeomorphic T \<Longrightarrow> path_connected S \<longleftrightarrow> path_connected T"
lp15@61738
  1683
  unfolding homeomorphic_def homeomorphism_def by (metis path_connected_continuous_image)
huffman@36583
  1684
lp15@64788
  1685
lemma path_connected_empty [simp]: "path_connected {}"
huffman@36583
  1686
  unfolding path_connected_def by auto
huffman@36583
  1687
lp15@64788
  1688
lemma path_connected_singleton [simp]: "path_connected {a}"
huffman@36583
  1689
  unfolding path_connected_def pathstart_def pathfinish_def path_image_def
wenzelm@53640
  1690
  apply clarify
wenzelm@53640
  1691
  apply (rule_tac x="\<lambda>x. a" in exI)
wenzelm@53640
  1692
  apply (simp add: image_constant_conv)
huffman@36583
  1693
  apply (simp add: path_def continuous_on_const)
huffman@36583
  1694
  done
huffman@36583
  1695
wenzelm@49653
  1696
lemma path_connected_Un:
lp15@68096
  1697
  assumes "path_connected S"
lp15@68096
  1698
    and "path_connected T"
lp15@68096
  1699
    and "S \<inter> T \<noteq> {}"
lp15@68096
  1700
  shows "path_connected (S \<union> T)"
wenzelm@49653
  1701
  unfolding path_connected_component
lp15@68096
  1702
proof (intro ballI)
wenzelm@49653
  1703
  fix x y
lp15@68096
  1704
  assume x: "x \<in> S \<union> T" and y: "y \<in> S \<union> T"
lp15@68096
  1705
  from assms obtain z where z: "z \<in> S" "z \<in> T"
wenzelm@53640
  1706
    by auto
lp15@68096
  1707
  show "path_component (S \<union> T) x y"
lp15@68096
  1708
    using x y
lp15@68096
  1709
  proof safe
lp15@68096
  1710
    assume "x \<in> S" "y \<in> S"
lp15@68096
  1711
    then show "path_component (S \<union> T) x y"
lp15@68096
  1712
      by (meson Un_upper1 \<open>path_connected S\<close> path_component_of_subset path_connected_component)
lp15@68096
  1713
  next
lp15@68096
  1714
    assume "x \<in> S" "y \<in> T"
lp15@68096
  1715
    then show "path_component (S \<union> T) x y"
lp15@68096
  1716
      by (metis z assms(1-2) le_sup_iff order_refl path_component_of_subset path_component_trans path_connected_component)
lp15@68096
  1717
  next
lp15@68096
  1718
  assume "x \<in> T" "y \<in> S"
lp15@68096
  1719
    then show "path_component (S \<union> T) x y"
lp15@68096
  1720
      by (metis z assms(1-2) le_sup_iff order_refl path_component_of_subset path_component_trans path_connected_component)
lp15@68096
  1721
  next
lp15@68096
  1722
    assume "x \<in> T" "y \<in> T"
lp15@68096
  1723
    then show "path_component (S \<union> T) x y"
lp15@68096
  1724
      by (metis Un_upper1 assms(2) path_component_of_subset path_connected_component sup_commute)
lp15@68096
  1725
  qed
wenzelm@49653
  1726
qed
huffman@36583
  1727
huffman@37674
  1728
lemma path_connected_UNION:
huffman@37674
  1729
  assumes "\<And>i. i \<in> A \<Longrightarrow> path_connected (S i)"
wenzelm@49653
  1730
    and "\<And>i. i \<in> A \<Longrightarrow> z \<in> S i"
huffman@37674
  1731
  shows "path_connected (\<Union>i\<in>A. S i)"
wenzelm@49653
  1732
  unfolding path_connected_component
wenzelm@49653
  1733
proof clarify
huffman@37674
  1734
  fix x i y j
huffman@37674
  1735
  assume *: "i \<in> A" "x \<in> S i" "j \<in> A" "y \<in> S j"
wenzelm@49654
  1736
  then have "path_component (S i) x z" and "path_component (S j) z y"
huffman@37674
  1737
    using assms by (simp_all add: path_connected_component)
wenzelm@49654
  1738
  then have "path_component (\<Union>i\<in>A. S i) x z" and "path_component (\<Union>i\<in>A. S i) z y"
wenzelm@48125
  1739
    using *(1,3) by (auto elim!: path_component_of_subset [rotated])
wenzelm@49654
  1740
  then show "path_component (\<Union>i\<in>A. S i) x y"
huffman@37674
  1741
    by (rule path_component_trans)
huffman@37674
  1742
qed
huffman@36583
  1743
lp15@61426
  1744
lemma path_component_path_image_pathstart:
lp15@61426
  1745
  assumes p: "path p" and x: "x \<in> path_image p"
lp15@61426
  1746
  shows "path_component (path_image p) (pathstart p) x"
lp15@68096
  1747
proof -
lp15@68096
  1748
  obtain y where x: "x = p y" and y: "0 \<le> y" "y \<le> 1"
lp15@68096
  1749
    using x by (auto simp: path_image_def)
lp15@68096
  1750
  show ?thesis
lp15@68096
  1751
    unfolding path_component_def 
lp15@68096
  1752
  proof (intro exI conjI)
nipkow@69064
  1753
    have "continuous_on {0..1} (p \<circ> ((*) y))"
lp15@61426
  1754
      apply (rule continuous_intros)+
lp15@61426
  1755
      using p [unfolded path_def] y
lp15@61426
  1756
      apply (auto simp: mult_le_one intro: continuous_on_subset [of _ p])
lp15@61426
  1757
      done
lp15@68096
  1758
    then show "path (\<lambda>u. p (y * u))"
lp15@61426
  1759
      by (simp add: path_def)
lp15@68096
  1760
    show "path_image (\<lambda>u. p (y * u)) \<subseteq> path_image p"
lp15@68096
  1761
      using y mult_le_one by (fastforce simp: path_image_def image_iff)
lp15@68096
  1762
  qed (auto simp: pathstart_def pathfinish_def x)
lp15@61426
  1763
qed
lp15@61426
  1764
lp15@61426
  1765
lemma path_connected_path_image: "path p \<Longrightarrow> path_connected(path_image p)"
lp15@61426
  1766
  unfolding path_connected_component
lp15@61426
  1767
  by (meson path_component_path_image_pathstart path_component_sym path_component_trans)
lp15@61426
  1768
lp15@64788
  1769
lemma path_connected_path_component [simp]:
lp15@61426
  1770
   "path_connected (path_component_set s x)"
lp15@61426
  1771
proof -
lp15@61426
  1772
  { fix y z
lp15@61426
  1773
    assume pa: "path_component s x y" "path_component s x z"
lp15@61426
  1774
    then have pae: "path_component_set s x = path_component_set s y"
lp15@61426
  1775
      using path_component_eq by auto
lp15@61426
  1776
    have yz: "path_component s y z"
lp15@61426
  1777
      using pa path_component_sym path_component_trans by blast
lp15@61426
  1778
    then have "\<exists>g. path g \<and> path_image g \<subseteq> path_component_set s x \<and> pathstart g = y \<and> pathfinish g = z"
lp15@61426
  1779
      apply (simp add: path_component_def, clarify)
lp15@61426
  1780
      apply (rule_tac x=g in exI)
lp15@61426
  1781
      by (simp add: pae path_component_maximal path_connected_path_image pathstart_in_path_image)
lp15@61426
  1782
  }
lp15@61426
  1783
  then show ?thesis
lp15@61426
  1784
    by (simp add: path_connected_def)
lp15@61426
  1785
qed
lp15@61426
  1786
lp15@68532
  1787
lemma path_component: "path_component S x y \<longleftrightarrow> (\<exists>t. path_connected t \<and> t \<subseteq> S \<and> x \<in> t \<and> y \<in> t)"
lp15@61426
  1788
  apply (intro iffI)
lp15@61426
  1789
  apply (metis path_connected_path_image path_defs(5) pathfinish_in_path_image pathstart_in_path_image)
lp15@61426
  1790
  using path_component_of_subset path_connected_component by blast
lp15@61426
  1791
lp15@61426
  1792
lemma path_component_path_component [simp]:
lp15@68532
  1793
   "path_component_set (path_component_set S x) x = path_component_set S x"
lp15@68532
  1794
proof (cases "x \<in> S")
lp15@61426
  1795
  case True show ?thesis
lp15@61426
  1796
    apply (rule subset_antisym)
lp15@61426
  1797
    apply (simp add: path_component_subset)
lp15@61426
  1798
    by (simp add: True path_component_maximal path_component_refl path_connected_path_component)
lp15@61426
  1799
next
lp15@61426
  1800
  case False then show ?thesis
lp15@61426
  1801
    by (metis False empty_iff path_component_eq_empty)
lp15@61426
  1802
qed
lp15@61426
  1803
lp15@61426
  1804
lemma path_component_subset_connected_component:
lp15@68532
  1805
   "(path_component_set S x) \<subseteq> (connected_component_set S x)"
lp15@68532
  1806
proof (cases "x \<in> S")
lp15@61426
  1807
  case True show ?thesis
lp15@61426
  1808
    apply (rule connected_component_maximal)
lp15@68532
  1809
    apply (auto simp: True path_component_subset path_component_refl path_connected_imp_connected)
lp15@61426
  1810
    done
lp15@61426
  1811
next
lp15@61426
  1812
  case False then show ?thesis
lp15@61426
  1813
    using path_component_eq_empty by auto
lp15@61426
  1814
qed
wenzelm@49653
  1815
nipkow@69514
  1816
immler@67962
  1817
subsection%unimportant\<open>Lemmas about path-connectedness\<close>
lp15@62620
  1818
lp15@62620
  1819
lemma path_connected_linear_image:
lp15@62620
  1820
  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
lp15@68532
  1821
  assumes "path_connected S" "bounded_linear f"
lp15@68532
  1822
    shows "path_connected(f ` S)"
lp15@62620
  1823
by (auto simp: linear_continuous_on assms path_connected_continuous_image)
lp15@62620
  1824
lp15@68532
  1825
lemma is_interval_path_connected: "is_interval S \<Longrightarrow> path_connected S"
lp15@62620
  1826
  by (simp add: convex_imp_path_connected is_interval_convex)
lp15@62620
  1827
lp15@69939
  1828
lemma path_connectedin_path_image:
lp15@69939
  1829
  assumes "pathin X g" shows "path_connectedin X (g ` ({0..1}))"
lp15@69939
  1830
  unfolding pathin_def
lp15@69939
  1831
proof (rule path_connectedin_continuous_map_image)
lp15@69939
  1832
  show "continuous_map (subtopology euclideanreal {0..1}) X g"
lp15@69939
  1833
    using assms pathin_def by blast
lp15@69939
  1834
qed (auto simp: is_interval_1 is_interval_path_connected)
lp15@69939
  1835
lp15@69939
  1836
lemma path_connected_space_subconnected:
lp15@69939
  1837
     "path_connected_space X \<longleftrightarrow>
lp15@69939
  1838
      (\<forall>x \<in> topspace X. \<forall>y \<in> topspace X. \<exists>S. path_connectedin X S \<and> x \<in> S \<and> y \<in> S)"
lp15@69939
  1839
  unfolding path_connected_space_def Ball_def
lp15@69939
  1840
  apply (intro all_cong1 imp_cong refl, safe)
lp15@69939
  1841
  using path_connectedin_path_image apply fastforce
lp15@69939
  1842
  by (meson path_connectedin)
lp15@69939
  1843
lp15@69939
  1844
lemma connectedin_path_image: "pathin X g \<Longrightarrow> connectedin X (g ` ({0..1}))"
lp15@69939
  1845
  by (simp add: path_connectedin_imp_connectedin path_connectedin_path_image)
lp15@69939
  1846
lp15@69939
  1847
lemma compactin_path_image: "pathin X g \<Longrightarrow> compactin X (g ` ({0..1}))"
lp15@69939
  1848
  unfolding pathin_def
lp15@69939
  1849
  by (rule image_compactin [of "top_of_set {0..1}"]) auto
lp15@69939
  1850
lp15@62843
  1851
lemma linear_homeomorphism_image:
lp15@62843
  1852
  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
lp15@62620
  1853
  assumes "linear f" "inj f"
lp15@62843
  1854
    obtains g where "homeomorphism (f ` S) S g f"
lp15@62843
  1855
using linear_injective_left_inverse [OF assms]
lp15@62843
  1856
apply clarify
lp15@62843
  1857
apply (rule_tac g=g in that)
lp15@62843
  1858
using assms
lp15@62843
  1859
apply (auto simp: homeomorphism_def eq_id_iff [symmetric] image_comp comp_def linear_conv_bounded_linear linear_continuous_on)
lp15@62843
  1860
done
lp15@62843
  1861
lp15@62843
  1862
lemma linear_homeomorphic_image:
lp15@62843
  1863
  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
lp15@62843
  1864
  assumes "linear f" "inj f"
lp15@62843
  1865
    shows "S homeomorphic f ` S"
lp15@62843
  1866
by (meson homeomorphic_def homeomorphic_sym linear_homeomorphism_image [OF assms])
lp15@62620
  1867
lp15@62620
  1868
lemma path_connected_Times:
lp15@62620
  1869
  assumes "path_connected s" "path_connected t"
lp15@62620
  1870
    shows "path_connected (s \<times> t)"
lp15@62620
  1871
proof (simp add: path_connected_def Sigma_def, clarify)
lp15@62620
  1872
  fix x1 y1 x2 y2
lp15@62620
  1873
  assume "x1 \<in> s" "y1 \<in> t" "x2 \<in> s" "y2 \<in> t"
lp15@62620
  1874
  obtain g where "path g" and g: "path_image g \<subseteq> s" and gs: "pathstart g = x1" and gf: "pathfinish g = x2"
lp15@62620
  1875
    using \<open>x1 \<in> s\<close> \<open>x2 \<in> s\<close> assms by (force simp: path_connected_def)
lp15@62620
  1876
  obtain h where "path h" and h: "path_image h \<subseteq> t" and hs: "pathstart h = y1" and hf: "pathfinish h = y2"
lp15@62620
  1877
    using \<open>y1 \<in> t\<close> \<open>y2 \<in> t\<close> assms by (force simp: path_connected_def)
lp15@62620
  1878
  have "path (\<lambda>z. (x1, h z))"
lp15@62620
  1879
    using \<open>path h\<close>
lp15@62620
  1880
    apply (simp add: path_def)
lp15@62620
  1881
    apply (rule continuous_on_compose2 [where f = h])
lp15@62620
  1882
    apply (rule continuous_intros | force)+
lp15@62620
  1883
    done
lp15@62620
  1884
  moreover have "path (\<lambda>z. (g z, y2))"
lp15@62620
  1885
    using \<open>path g\<close>
lp15@62620
  1886
    apply (simp add: path_def)
lp15@62620
  1887
    apply (rule continuous_on_compose2 [where f = g])
lp15@62620
  1888
    apply (rule continuous_intros | force)+
lp15@62620
  1889
    done
lp15@62620
  1890
  ultimately have 1: "path ((\<lambda>z. (x1, h z)) +++ (\<lambda>z. (g z, y2)))"
lp15@62620
  1891
    by (metis hf gs path_join_imp pathstart_def pathfinish_def)
lp15@62620
  1892
  have "path_image ((\<lambda>z. (x1, h z)) +++ (\<lambda>z. (g z, y2))) \<subseteq> path_image (\<lambda>z. (x1, h z)) \<union> path_image (\<lambda>z. (g z, y2))"
lp15@62620
  1893
    by (rule Path_Connected.path_image_join_subset)
lp15@68096
  1894
  also have "\<dots> \<subseteq> (\<Union>x\<in>s. \<Union>x1\<in>t. {(x, x1)})"
lp15@62620
  1895
    using g h \<open>x1 \<in> s\<close> \<open>y2 \<in> t\<close> by (force simp: path_image_def)
lp15@62620
  1896
  finally have 2: "path_image ((\<lambda>z. (x1, h z)) +++ (\<lambda>z. (g z, y2))) \<subseteq> (\<Union>x\<in>s. \<Union>x1\<in>t. {(x, x1)})" .
lp15@62620
  1897
  show "\<exists>g. path g \<and> path_image g \<subseteq> (\<Union>x\<in>s. \<Union>x1\<in>t. {(x, x1)}) \<and>
lp15@62620
  1898
            pathstart g = (x1, y1) \<and> pathfinish g = (x2, y2)"
lp15@62620
  1899
    apply (intro exI conjI)
lp15@62620
  1900
       apply (rule 1)
lp15@62620
  1901
      apply (rule 2)
lp15@62620
  1902
     apply (metis hs pathstart_def pathstart_join)
lp15@62620
  1903
    by (metis gf pathfinish_def pathfinish_join)
lp15@62620
  1904
qed
lp15@62620
  1905
lp15@62620
  1906
lemma is_interval_path_connected_1:
lp15@62620
  1907
  fixes s :: "real set"
lp15@62620
  1908
  shows "is_interval s \<longleftrightarrow> path_connected s"
lp15@62620
  1909
using is_interval_connected_1 is_interval_path_connected path_connected_imp_connected by blast
lp15@62620
  1910
lp15@62620
  1911
immler@67962
  1912
subsection%unimportant\<open>Path components\<close>
lp15@66793
  1913
lp15@62948
  1914
lemma Union_path_component [simp]:
lp15@62948
  1915
   "Union {path_component_set S x |x. x \<in> S} = S"
lp15@62948
  1916
apply (rule subset_antisym)
lp15@62948
  1917
using path_component_subset apply force
lp15@62948
  1918
using path_component_refl by auto
lp15@62948
  1919
lp15@62948
  1920
lemma path_component_disjoint:
lp15@62948
  1921
   "disjnt (path_component_set S a) (path_component_set S b) \<longleftrightarrow>
lp15@62948
  1922
    (a \<notin> path_component_set S b)"
lp15@62948
  1923
apply (auto simp: disjnt_def)
lp15@62948
  1924
using path_component_eq apply fastforce
lp15@62948
  1925
using path_component_sym path_component_trans by blast
lp15@62948
  1926
lp15@62948
  1927
lemma path_component_eq_eq:
lp15@62948
  1928
   "path_component S x = path_component S y \<longleftrightarrow>
lp15@62948
  1929
        (x \<notin> S) \<and> (y \<notin> S) \<or> x \<in> S \<and> y \<in> S \<and> path_component S x y"
lp15@62948
  1930
apply (rule iffI, metis (no_types) path_component_mem(1) path_component_refl)
lp15@62948
  1931
apply (erule disjE, metis Collect_empty_eq_bot path_component_eq_empty)
lp15@62948
  1932
apply (rule ext)
lp15@62948
  1933
apply (metis path_component_trans path_component_sym)
lp15@62948
  1934
done
lp15@62948
  1935
lp15@62948
  1936
lemma path_component_unique:
lp15@62948
  1937
  assumes "x \<in> c" "c \<subseteq> S" "path_connected c"
lp15@62948
  1938
          "\<And>c'. \<lbrakk>x \<in> c'; c' \<subseteq> S; path_connected c'\<rbrakk> \<Longrightarrow> c' \<subseteq> c"
lp15@62948
  1939
   shows "path_component_set S x = c"
lp15@62948
  1940
apply (rule subset_antisym)
lp15@62948
  1941
using assms
lp15@62948
  1942
apply (metis mem_Collect_eq subsetCE path_component_eq_eq path_component_subset path_connected_path_component)
lp15@62948
  1943
by (simp add: assms path_component_maximal)
lp15@62948
  1944
lp15@62948
  1945
lemma path_component_intermediate_subset:
lp15@62948
  1946
   "path_component_set u a \<subseteq> t \<and> t \<subseteq> u
lp15@62948
  1947
        \<Longrightarrow> path_component_set t a = path_component_set u a"
lp15@62948
  1948
by (metis (no_types) path_component_mono path_component_path_component subset_antisym)
lp15@62948
  1949
lp15@62948
  1950
lemma complement_path_component_Union:
lp15@62948
  1951
  fixes x :: "'a :: topological_space"
lp15@62948
  1952
  shows "S - path_component_set S x =
lp15@62948
  1953
         \<Union>({path_component_set S y| y. y \<in> S} - {path_component_set S x})"
lp15@62948
  1954
proof -
lp15@62948
  1955
  have *: "(\<And>x. x \<in> S - {a} \<Longrightarrow> disjnt a x) \<Longrightarrow> \<Union>S - a = \<Union>(S - {a})"
lp15@62948
  1956
    for a::"'a set" and S
lp15@62948
  1957
    by (auto simp: disjnt_def)
lp15@62948
  1958
  have "\<And>y. y \<in> {path_component_set S x |x. x \<in> S} - {path_component_set S x}
lp15@62948
  1959
            \<Longrightarrow> disjnt (path_component_set S x) y"
lp15@62948
  1960
    using path_component_disjoint path_component_eq by fastforce
lp15@62948
  1961
  then have "\<Union>{path_component_set S x |x. x \<in> S} - path_component_set S x =
lp15@62948
  1962
             \<Union>({path_component_set S y |y. y \<in> S} - {path_component_set S x})"
lp15@62948
  1963
    by (meson *)
lp15@62948
  1964
  then show ?thesis by simp
lp15@62948
  1965
qed
lp15@62948
  1966
lp15@62948
  1967
lp15@69939
  1968
subsection\<open>Path components\<close>
lp15@69939
  1969
lp15@69939
  1970
definition path_component_of
lp15@69939
  1971
  where "path_component_of X x y \<equiv> \<exists>g. pathin X g \<and> g 0 = x \<and> g 1 = y"
lp15@69939
  1972
lp15@69939
  1973
abbreviation path_component_of_set
lp15@69939
  1974
  where "path_component_of_set X x \<equiv> Collect (path_component_of X x)"
lp15@69939
  1975
lp15@69939
  1976
definition path_components_of :: "'a topology \<Rightarrow> 'a set set"
lp15@69939
  1977
  where "path_components_of X \<equiv> path_component_of_set X ` topspace X"
lp15@69939
  1978
lp15@69939
  1979
lemma path_component_in_topspace:
lp15@69939
  1980
   "path_component_of X x y \<Longrightarrow> x \<in> topspace X \<and> y \<in> topspace X"
lp15@69939
  1981
  by (auto simp: path_component_of_def pathin_def continuous_map_def)
lp15@69939
  1982
lp15@69939
  1983
lemma path_component_of_refl:
lp15@69939
  1984
   "path_component_of X x x \<longleftrightarrow> x \<in> topspace X"
lp15@69939
  1985
  apply (auto simp: path_component_in_topspace)
lp15@69939
  1986
  apply (force simp: path_component_of_def pathin_const)
lp15@69939
  1987
  done
lp15@69939
  1988
lp15@69939
  1989
lemma path_component_of_sym:
lp15@69939
  1990
  assumes "path_component_of X x y"
lp15@69939
  1991
  shows "path_component_of X y x"
lp15@69939
  1992
  using assms
lp15@69939
  1993
  apply (clarsimp simp: path_component_of_def pathin_def)
lp15@69939
  1994
  apply (rule_tac x="g \<circ> (\<lambda>t. 1 - t)" in exI)
lp15@69939
  1995
  apply (auto intro!: continuous_map_compose)
lp15@69939
  1996
  apply (force simp: continuous_map_in_subtopology continuous_on_op_minus)
lp15@69939
  1997
  done
lp15@69939
  1998
lp15@69939
  1999
lemma path_component_of_sym_iff:
lp15@69939
  2000
   "path_component_of X x y \<longleftrightarrow> path_component_of X y x"
lp15@69939
  2001
  by (metis path_component_of_sym)
lp15@69939
  2002
lp15@69939
  2003
lemma path_component_of_trans:
lp15@69939
  2004
  assumes "path_component_of X x y" and "path_component_of X y z"
lp15@69939
  2005
  shows "path_component_of X x z"
lp15@69939
  2006
  unfolding path_component_of_def pathin_def
lp15@69939
  2007
proof -
lp15@69939
  2008
  let ?T01 = "top_of_set {0..1::real}"
lp15@69939
  2009
  obtain g1 g2 where g1: "continuous_map ?T01 X g1" "x = g1 0" "y = g1 1"
lp15@69939
  2010
    and g2: "continuous_map ?T01 X g2" "g2 0 = g1 1" "z = g2 1"
lp15@69939
  2011
    using assms unfolding path_component_of_def pathin_def by blast
lp15@69939
  2012
  let ?g = "\<lambda>x. if x \<le> 1/2 then (g1 \<circ> (\<lambda>t. 2 * t)) x else (g2 \<circ> (\<lambda>t. 2 * t -1)) x"
lp15@69939
  2013
  show "\<exists>g. continuous_map ?T01 X g \<and> g 0 = x \<and> g 1 = z"
lp15@69939
  2014
  proof (intro exI conjI)
lp15@69939
  2015
    show "continuous_map (subtopology euclideanreal {0..1}) X ?g"
lp15@69939
  2016
    proof (intro continuous_map_cases_le continuous_map_compose, force, force)
lp15@69939
  2017
      show "continuous_map (subtopology ?T01 {x \<in> topspace ?T01. x \<le> 1/2}) ?T01 ((*) 2)"
lp15@69939
  2018
        by (auto simp: continuous_map_in_subtopology continuous_map_from_subtopology)
lp15@69939
  2019
      have "continuous_map
lp15@69939
  2020
             (subtopology (top_of_set {0..1}) {x. 0 \<le> x \<and> x \<le> 1 \<and> 1 \<le> x * 2})
lp15@69939
  2021
             euclideanreal (\<lambda>t. 2 * t - 1)"
lp15@69939
  2022
        by (intro continuous_intros) (force intro: continuous_map_from_subtopology)
lp15@69939
  2023
      then show "continuous_map (subtopology ?T01 {x \<in> topspace ?T01. 1/2 \<le> x}) ?T01 (\<lambda>t. 2 * t - 1)"
lp15@69939
  2024
        by (force simp: continuous_map_in_subtopology)
lp15@69939
  2025
      show "(g1 \<circ> (*) 2) x = (g2 \<circ> (\<lambda>t. 2 * t - 1)) x" if "x \<in> topspace ?T01" "x = 1/2" for x
lp15@69939
  2026
        using that by (simp add: g2(2) mult.commute continuous_map_from_subtopology)
lp15@69939
  2027
    qed (auto simp: g1 g2)
lp15@69939
  2028
  qed (auto simp: g1 g2)
lp15@69939
  2029
qed
lp15@69939
  2030
lp15@69939
  2031
lp15@69939
  2032
lemma path_component_of_mono:
lp15@69939
  2033
   "\<lbrakk>path_component_of (subtopology X S) x y; S \<subseteq> T\<rbrakk> \<Longrightarrow> path_component_of (subtopology X T) x y"
lp15@69939
  2034
  unfolding path_component_of_def
lp15@69939
  2035
  by (metis subsetD pathin_subtopology)
lp15@69939
  2036
lp15@69939
  2037
lp15@69939
  2038
lemma path_component_of:
lp15@69939
  2039
  "path_component_of X x y \<longleftrightarrow> (\<exists>T. path_connectedin X T \<and> x \<in> T \<and> y \<in> T)"
lp15@69939
  2040
  apply (auto simp: path_component_of_def)
lp15@69939
  2041
  using path_connectedin_path_image apply fastforce
lp15@69939
  2042
  apply (metis path_connectedin)
lp15@69939
  2043
  done
lp15@69939
  2044
lp15@69939
  2045
lemma path_component_of_set:
lp15@69939
  2046
   "path_component_of X x y \<longleftrightarrow> (\<exists>g. pathin X g \<and> g 0 = x \<and> g 1 = y)"
lp15@69939
  2047
  by (auto simp: path_component_of_def)
lp15@69939
  2048
lp15@69939
  2049
lemma path_component_of_subset_topspace:
lp15@69939
  2050
   "Collect(path_component_of X x) \<subseteq> topspace X"
lp15@69939
  2051
  using path_component_in_topspace by fastforce
lp15@69939
  2052
lp15@69939
  2053
lemma path_component_of_eq_empty:
lp15@69939
  2054
   "Collect(path_component_of X x) = {} \<longleftrightarrow> (x \<notin> topspace X)"
lp15@69939
  2055
  using path_component_in_topspace path_component_of_refl by fastforce
lp15@69939
  2056
lp15@69939
  2057
lemma path_connected_space_iff_path_component:
lp15@69939
  2058
   "path_connected_space X \<longleftrightarrow> (\<forall>x \<in> topspace X. \<forall>y \<in> topspace X. path_component_of X x y)"
lp15@69939
  2059
  by (simp add: path_component_of path_connected_space_subconnected)
lp15@69939
  2060
lp15@69939
  2061
lemma path_connected_space_imp_path_component_of:
lp15@69939
  2062
   "\<lbrakk>path_connected_space X; a \<in> topspace X; b \<in> topspace X\<rbrakk>
lp15@69939
  2063
        \<Longrightarrow> path_component_of X a b"
lp15@69939
  2064
  by (simp add: path_connected_space_iff_path_component)
lp15@69939
  2065
lp15@69939
  2066
lemma path_connected_space_path_component_set:
lp15@69939
  2067
   "path_connected_space X \<longleftrightarrow> (\<forall>x \<in> topspace X. Collect(path_component_of X x) = topspace X)"
lp15@69939
  2068
  using path_component_of_subset_topspace path_connected_space_iff_path_component by fastforce
lp15@69939
  2069
lp15@69939
  2070
lemma path_component_of_maximal:
lp15@69939
  2071
   "\<lbrakk>path_connectedin X s; x \<in> s\<rbrakk> \<Longrightarrow> s \<subseteq> Collect(path_component_of X x)"
lp15@69939
  2072
  using path_component_of by fastforce
lp15@69939
  2073
lp15@69939
  2074
lemma path_component_of_equiv:
lp15@69939
  2075
   "path_component_of X x y \<longleftrightarrow> x \<in> topspace X \<and> y \<in> topspace X \<and> path_component_of X x = path_component_of X y"
lp15@69939
  2076
    (is "?lhs = ?rhs")
lp15@69939
  2077
proof
lp15@69939
  2078
  assume ?lhs
lp15@69939
  2079
  then show ?rhs
lp15@69939
  2080
    apply (simp add: fun_eq_iff path_component_in_topspace)
lp15@69939
  2081
    apply (meson path_component_of_sym path_component_of_trans)
lp15@69939
  2082
    done
lp15@69939
  2083
qed (simp add: path_component_of_refl)
lp15@69939
  2084
lp15@69939
  2085
lemma path_component_of_disjoint:
lp15@69939
  2086
     "disjnt (Collect (path_component_of X x)) (Collect (path_component_of X y)) \<longleftrightarrow>
lp15@69939
  2087
      ~(path_component_of X x y)"
lp15@69939
  2088
  by (force simp: disjnt_def path_component_of_eq_empty path_component_of_equiv)
lp15@69939
  2089
lp15@69939
  2090
lemma path_component_of_eq:
lp15@69939
  2091
   "path_component_of X x = path_component_of X y \<longleftrightarrow>
lp15@69939
  2092
        (x \<notin> topspace X) \<and> (y \<notin> topspace X) \<or>
lp15@69939
  2093
        x \<in> topspace X \<and> y \<in> topspace X \<and> path_component_of X x y"
lp15@69939
  2094
  by (metis Collect_empty_eq_bot path_component_of_eq_empty path_component_of_equiv)
lp15@69939
  2095
lp15@69939
  2096
lemma path_connectedin_path_component_of:
lp15@69939
  2097
  "path_connectedin X (Collect (path_component_of X x))"
lp15@69939
  2098
proof -
lp15@69939
  2099
  have "\<And>y. path_component_of X x y
lp15@69939
  2100
        \<Longrightarrow> path_component_of (subtopology X (Collect (path_component_of X x))) x y"
lp15@69939
  2101
    by (meson path_component_of path_component_of_maximal path_connectedin_subtopology)
lp15@69939
  2102
  then show ?thesis
lp15@69939
  2103
    apply (simp add: path_connectedin_def path_component_of_subset_topspace path_connected_space_iff_path_component)
lp15@69939
  2104
    by (metis Int_absorb1 mem_Collect_eq path_component_of_equiv path_component_of_subset_topspace topspace_subtopology)
lp15@69939
  2105
qed
lp15@69939
  2106
lp15@69939
  2107
lemma Union_path_components_of:
lp15@69939
  2108
     "\<Union>(path_components_of X) = topspace X"
lp15@69939
  2109
  by (auto simp: path_components_of_def path_component_of_equiv)
lp15@69939
  2110
lp15@69939
  2111
lemma path_components_of_maximal:
lp15@69939
  2112
   "\<lbrakk>C \<in> path_components_of X; path_connectedin X S; ~disjnt C S\<rbrakk> \<Longrightarrow> S \<subseteq> C"
lp15@69939
  2113
  apply (auto simp: path_components_of_def path_component_of_equiv)
lp15@69939
  2114
  using path_component_of_maximal path_connectedin_def apply fastforce
lp15@69939
  2115
  by (meson disjnt_subset2 path_component_of_disjoint path_component_of_equiv path_component_of_maximal)
lp15@69939
  2116
lp15@69939
  2117
lemma pairwise_disjoint_path_components_of:
lp15@69939
  2118
     "pairwise disjnt (path_components_of X)"
lp15@69939
  2119
  by (auto simp: path_components_of_def pairwise_def path_component_of_disjoint path_component_of_equiv)
lp15@69939
  2120
lp15@69939
  2121
lemma complement_path_components_of_Union:
lp15@69939
  2122
   "C \<in> path_components_of X
lp15@69939
  2123
        \<Longrightarrow> topspace X - C = \<Union>(path_components_of X - {C})"
lp15@69939
  2124
  by (metis Diff_cancel Diff_subset Union_path_components_of cSup_singleton diff_Union_pairwise_disjoint insert_subset pairwise_disjoint_path_components_of)
lp15@69939
  2125
lp15@69939
  2126
lemma nonempty_path_components_of:
lp15@69939
  2127
  "C \<in> path_components_of X \<Longrightarrow> (C \<noteq> {})"
lp15@69939
  2128
  apply (clarsimp simp: path_components_of_def path_component_of_eq_empty)
lp15@69939
  2129
  by (meson path_component_of_refl)
lp15@69939
  2130
lp15@69939
  2131
lemma path_components_of_subset: "C \<in> path_components_of X \<Longrightarrow> C \<subseteq> topspace X"
lp15@69939
  2132
  by (auto simp: path_components_of_def path_component_of_equiv)
lp15@69939
  2133
lp15@69939
  2134
lemma path_connectedin_path_components_of:
lp15@69939
  2135
   "C \<in> path_components_of X \<Longrightarrow> path_connectedin X C"
lp15@69939
  2136
  by (auto simp: path_components_of_def path_connectedin_path_component_of)
lp15@69939
  2137
lp15@69939
  2138
lemma path_component_in_path_components_of:
lp15@69939
  2139
  "Collect (path_component_of X a) \<in> path_components_of X \<longleftrightarrow> a \<in> topspace X"
lp15@69939
  2140
  apply (rule iffI)
lp15@69939
  2141
  using nonempty_path_components_of path_component_of_eq_empty apply fastforce
lp15@69939
  2142
  by (simp add: path_components_of_def)
lp15@69939
  2143
lp15@69939
  2144
lemma path_connectedin_Union:
lp15@69939
  2145
  assumes \<A>: "\<And>S. S \<in> \<A> \<Longrightarrow> path_connectedin X S" "\<Inter>\<A> \<noteq> {}"
lp15@69939
  2146
  shows "path_connectedin X (\<Union>\<A>)"
lp15@69939
  2147
proof -
lp15@69939
  2148
  obtain a where "\<And>S. S \<in> \<A> \<Longrightarrow> a \<in> S"
lp15@69939
  2149
    using assms by blast
lp15@69939
  2150
  then have "\<And>x. x \<in> topspace (subtopology X (\<Union>\<A>)) \<Longrightarrow> path_component_of (subtopology X (\<Union>\<A>)) a x"
lp15@69939
  2151
    apply (simp add: topspace_subtopology)
lp15@69939
  2152
    by (meson Union_upper \<A> path_component_of path_connectedin_subtopology)
lp15@69939
  2153
  then show ?thesis
lp15@69939
  2154
    using \<A> unfolding path_connectedin_def
lp15@69939
  2155
    by (metis Sup_le_iff path_component_of_equiv path_connected_space_iff_path_component)
lp15@69939
  2156
qed
lp15@69939
  2157
lp15@69939
  2158
lemma path_connectedin_Un:
lp15@69939
  2159
   "\<lbrakk>path_connectedin X S; path_connectedin X T; S \<inter> T \<noteq> {}\<rbrakk>
lp15@69939
  2160
    \<Longrightarrow> path_connectedin X (S \<union> T)"
lp15@69939
  2161
  by (blast intro: path_connectedin_Union [of "{S,T}", simplified])
lp15@69939
  2162
lp15@69939
  2163
lemma path_connected_space_iff_components_eq:
lp15@69939
  2164
  "path_connected_space X \<longleftrightarrow>
lp15@69939
  2165
    (\<forall>C \<in> path_components_of X. \<forall>C' \<in> path_components_of X. C = C')"
lp15@69939
  2166
  unfolding path_components_of_def
lp15@69939
  2167
proof (intro iffI ballI)
lp15@69939
  2168
  assume "\<forall>C \<in> path_component_of_set X ` topspace X.
lp15@69939
  2169
             \<forall>C' \<in> path_component_of_set X ` topspace X. C = C'"
lp15@69939
  2170
  then show "path_connected_space X"
lp15@69939
  2171
    using path_component_of_refl path_connected_space_iff_path_component by fastforce
lp15@69939
  2172
qed (auto simp: path_connected_space_path_component_set)
lp15@69939
  2173
lp15@69939
  2174
lemma path_components_of_eq_empty:
lp15@69939
  2175
   "path_components_of X = {} \<longleftrightarrow> topspace X = {}"
lp15@69939
  2176
  using Union_path_components_of nonempty_path_components_of by fastforce
lp15@69939
  2177
lp15@69939
  2178
lemma path_components_of_empty_space:
lp15@69939
  2179
   "topspace X = {} \<Longrightarrow> path_components_of X = {}"
lp15@69939
  2180
  by (simp add: path_components_of_eq_empty)
lp15@69939
  2181
lp15@69939
  2182
lemma path_components_of_subset_singleton:
lp15@69939
  2183
  "path_components_of X \<subseteq> {S} \<longleftrightarrow>
lp15@69939
  2184
        path_connected_space X \<and> (topspace X = {} \<or> topspace X = S)"
lp15@69939
  2185
proof (cases "topspace X = {}")
lp15@69939
  2186
  case True
lp15@69939
  2187
  then show ?thesis
lp15@69939
  2188
    by (auto simp: path_components_of_empty_space path_connected_space_topspace_empty)
lp15@69939
  2189
next
lp15@69939
  2190
  case False
lp15@69939
  2191
  have "(path_components_of X = {S}) \<longleftrightarrow> (path_connected_space X \<and> topspace X = S)"
lp15@69939
  2192
  proof (intro iffI conjI)
lp15@69939
  2193
    assume L: "path_components_of X = {S}"
lp15@69939
  2194
    then show "path_connected_space X"
lp15@69939
  2195
      by (simp add: path_connected_space_iff_components_eq)
lp15@69939
  2196
    show "topspace X = S"
lp15@69939
  2197
      by (metis L ccpo_Sup_singleton [of S] Union_path_components_of)
lp15@69939
  2198
  next
lp15@69939
  2199
    assume R: "path_connected_space X \<and> topspace X = S"
lp15@69939
  2200
    then show "path_components_of X = {S}"
lp15@69939
  2201
      using ccpo_Sup_singleton [of S]
lp15@69939
  2202
      by (metis False all_not_in_conv insert_iff mk_disjoint_insert path_component_in_path_components_of path_connected_space_iff_components_eq path_connected_space_path_component_set)
lp15@69939
  2203
  qed
lp15@69939
  2204
  with False show ?thesis
lp15@69939
  2205
    by (simp add: path_components_of_eq_empty subset_singleton_iff)
lp15@69939
  2206
qed
lp15@69939
  2207
lp15@69939
  2208
lemma path_connected_space_iff_components_subset_singleton:
lp15@69939
  2209
   "path_connected_space X \<longleftrightarrow> (\<exists>a. path_components_of X \<subseteq> {a})"
lp15@69939
  2210
  by (simp add: path_components_of_subset_singleton)
lp15@69939
  2211
lp15@69939
  2212
lemma path_components_of_eq_singleton:
lp15@69939
  2213
   "path_components_of X = {S} \<longleftrightarrow> path_connected_space X \<and> topspace X \<noteq> {} \<and> S = topspace X"
lp15@69939
  2214
  by (metis cSup_singleton insert_not_empty path_components_of_subset_singleton subset_singleton_iff)
lp15@69939
  2215
lp15@69939
  2216
lemma path_components_of_path_connected_space:
lp15@69939
  2217
   "path_connected_space X \<Longrightarrow> path_components_of X = (if topspace X = {} then {} else {topspace X})"
lp15@69939
  2218
  by (simp add: path_components_of_eq_empty path_components_of_eq_singleton)
lp15@69939
  2219
lp15@69939
  2220
lemma path_component_subset_connected_component_of:
lp15@69939
  2221
   "path_component_of_set X x \<subseteq> connected_component_of_set X x"
lp15@69939
  2222
proof (cases "x \<in> topspace X")
lp15@69939
  2223
  case True
lp15@69939
  2224
  then show ?thesis
lp15@69939
  2225
    by (simp add: connected_component_of_maximal path_component_of_refl path_connectedin_imp_connectedin path_connectedin_path_component_of)
lp15@69939
  2226
next
lp15@69939
  2227
  case False
lp15@69939
  2228
  then show ?thesis
lp15@69939
  2229
    using path_component_of_eq_empty by fastforce
lp15@69939
  2230
qed
lp15@69939
  2231
lp15@69939
  2232
lemma exists_path_component_of_superset:
lp15@69939
  2233
  assumes S: "path_connectedin X S" and ne: "topspace X \<noteq> {}"
lp15@69939
  2234
  obtains C where "C \<in> path_components_of X" "S \<subseteq> C"
lp15@69939
  2235
proof (cases "S = {}")
lp15@69939
  2236
  case True
lp15@69939
  2237
  then show ?thesis
lp15@69939
  2238
    using ne path_components_of_eq_empty that by fastforce
lp15@69939
  2239
next
lp15@69939
  2240
  case False
lp15@69939
  2241
  then obtain a where "a \<in> S"
lp15@69939
  2242
    by blast
lp15@69939
  2243
  show ?thesis
lp15@69939
  2244
  proof
lp15@69939
  2245
    show "Collect (path_component_of X a) \<in> path_components_of X"
lp15@69939
  2246
      by (meson \<open>a \<in> S\<close> S subsetD path_component_in_path_components_of path_connectedin_subset_topspace)
lp15@69939
  2247
    show "S \<subseteq> Collect (path_component_of X a)"
lp15@69939
  2248
      by (simp add: S \<open>a \<in> S\<close> path_component_of_maximal)
lp15@69939
  2249
  qed
lp15@69939
  2250
qed
lp15@69939
  2251
lp15@69939
  2252
lemma path_component_of_eq_overlap:
lp15@69939
  2253
   "path_component_of X x = path_component_of X y \<longleftrightarrow>
lp15@69939
  2254
      (x \<notin> topspace X) \<and> (y \<notin> topspace X) \<or>
lp15@69939
  2255
      Collect (path_component_of X x) \<inter> Collect (path_component_of X y) \<noteq> {}"
lp15@69939
  2256
  by (metis disjnt_def empty_iff inf_bot_right mem_Collect_eq path_component_of_disjoint path_component_of_eq path_component_of_eq_empty)
lp15@69939
  2257
lp15@69939
  2258
lemma path_component_of_nonoverlap:
lp15@69939
  2259
   "Collect (path_component_of X x) \<inter> Collect (path_component_of X y) = {} \<longleftrightarrow>
lp15@69939
  2260
    (x \<notin> topspace X) \<or> (y \<notin> topspace X) \<or>
lp15@69939
  2261
    path_component_of X x \<noteq> path_component_of X y"
lp15@69939
  2262
  by (metis inf.idem path_component_of_eq_empty path_component_of_eq_overlap)
lp15@69939
  2263
lp15@69939
  2264
lemma path_component_of_overlap:
lp15@69939
  2265
   "Collect (path_component_of X x) \<inter> Collect (path_component_of X y) \<noteq> {} \<longleftrightarrow>
lp15@69939
  2266
    x \<in> topspace X \<and> y \<in> topspace X \<and> path_component_of X x = path_component_of X y"
lp15@69939
  2267
  by (meson path_component_of_nonoverlap)
lp15@69939
  2268
lp15@69939
  2269
lemma path_components_of_disjoint:
lp15@69939
  2270
     "\<lbrakk>C \<in> path_components_of X; C' \<in> path_components_of X\<rbrakk> \<Longrightarrow> disjnt C C' \<longleftrightarrow> C \<noteq> C'"
lp15@69939
  2271
  by (auto simp: path_components_of_def path_component_of_disjoint path_component_of_equiv)
lp15@69939
  2272
lp15@69939
  2273
lemma path_components_of_overlap:
lp15@69939
  2274
    "\<lbrakk>C \<in> path_components_of X; C' \<in> path_components_of X\<rbrakk> \<Longrightarrow> C \<inter> C' \<noteq> {} \<longleftrightarrow> C = C'"
lp15@69939
  2275
  by (auto simp: path_components_of_def path_component_of_equiv)
lp15@69939
  2276
lp15@69939
  2277
lemma path_component_of_unique:
lp15@69939
  2278
   "\<lbrakk>x \<in> C; path_connectedin X C; \<And>C'. \<lbrakk>x \<in> C'; path_connectedin X C'\<rbrakk> \<Longrightarrow> C' \<subseteq> C\<rbrakk>
lp15@69939
  2279
        \<Longrightarrow> Collect (path_component_of X x) = C"
lp15@69939
  2280
  by (meson subsetD eq_iff path_component_of_maximal path_connectedin_path_component_of)
lp15@69939
  2281
lp15@69939
  2282
lemma path_component_of_discrete_topology [simp]:
lp15@69939
  2283
  "Collect (path_component_of (discrete_topology U) x) = (if x \<in> U then {x} else {})"
lp15@69939
  2284
proof -
lp15@69939
  2285
  have "\<And>C'. \<lbrakk>x \<in> C'; path_connectedin (discrete_topology U) C'\<rbrakk> \<Longrightarrow> C' \<subseteq> {x}"
lp15@69939
  2286
    by (metis path_connectedin_discrete_topology subsetD singletonD)
lp15@69939
  2287
  then have "x \<in> U \<Longrightarrow> Collect (path_component_of (discrete_topology U) x) = {x}"
lp15@69939
  2288
    by (simp add: path_component_of_unique)
lp15@69939
  2289
  then show ?thesis
lp15@69939
  2290
    using path_component_in_topspace by fastforce
lp15@69939
  2291
qed
lp15@69939
  2292
lp15@69939
  2293
lemma path_component_of_discrete_topology_iff [simp]:
lp15@69939
  2294
  "path_component_of (discrete_topology U) x y \<longleftrightarrow> x \<in> U \<and> y=x"
lp15@69939
  2295
  by (metis empty_iff insertI1 mem_Collect_eq path_component_of_discrete_topology singletonD)
lp15@69939
  2296
lp15@69939
  2297
lemma path_components_of_discrete_topology [simp]:
lp15@69939
  2298
   "path_components_of (discrete_topology U) = (\<lambda>x. {x}) ` U"
lp15@69939
  2299
  by (auto simp: path_components_of_def image_def fun_eq_iff)
lp15@69939
  2300
lp15@69939
  2301
lemma homeomorphic_map_path_component_of:
lp15@69939
  2302
  assumes f: "homeomorphic_map X Y f" and x: "x \<in> topspace X"
lp15@69939
  2303
  shows "Collect (path_component_of Y (f x)) = f ` Collect(path_component_of X x)"
lp15@69939
  2304
proof -
lp15@69939
  2305
  obtain g where g: "homeomorphic_maps X Y f g"
lp15@69939
  2306
    using f homeomorphic_map_maps by blast
lp15@69939
  2307
  show ?thesis
lp15@69939
  2308
  proof
lp15@69939
  2309
    have "Collect (path_component_of Y (f x)) \<subseteq> topspace Y"
lp15@69939
  2310
      by (simp add: path_component_of_subset_topspace)
lp15@69939
  2311
    moreover have "g ` Collect(path_component_of Y (f x)) \<subseteq> Collect (path_component_of X (g (f x)))"
lp15@69939
  2312
      using g x unfolding homeomorphic_maps_def
lp15@69939
  2313
      by (metis f homeomorphic_imp_surjective_map imageI mem_Collect_eq path_component_of_maximal path_component_of_refl path_connectedin_continuous_map_image path_connectedin_path_component_of)
lp15@69939
  2314
    ultimately show "Collect (path_component_of Y (f x)) \<subseteq> f ` Collect (path_component_of X x)"
lp15@69939
  2315
      using g x unfolding homeomorphic_maps_def continuous_map_def image_iff subset_iff
lp15@69939
  2316
      by metis
lp15@69939
  2317
    show "f ` Collect (path_component_of X x) \<subseteq> Collect (path_component_of Y (f x))"
lp15@69939
  2318
    proof (rule path_component_of_maximal)
lp15@69939
  2319
      show "path_connectedin Y (f ` Collect (path_component_of X x))"
lp15@69939
  2320
        by (meson f homeomorphic_map_path_connectedness_eq path_connectedin_path_component_of)
lp15@69939
  2321
    qed (simp add: path_component_of_refl x)
lp15@69939
  2322
  qed
lp15@69939
  2323
qed
lp15@69939
  2324
lp15@69939
  2325
lemma homeomorphic_map_path_components_of:
lp15@69939
  2326
  assumes "homeomorphic_map X Y f"
lp15@69939
  2327
  shows "path_components_of Y = (image f) ` (path_components_of X)"
lp15@69939
  2328
  unfolding path_components_of_def homeomorphic_imp_surjective_map [OF assms, symmetric]
lp15@69939
  2329
  apply safe
lp15@69939
  2330
  using assms homeomorphic_map_path_component_of apply fastforce
lp15@69939
  2331
  by (metis assms homeomorphic_map_path_component_of imageI)
lp15@69939
  2332
lp15@69939
  2333
wenzelm@60420
  2334
subsection \<open>Sphere is path-connected\<close>
hoelzl@37489
  2335
huffman@36583
  2336
lemma path_connected_punctured_universe:
huffman@37674
  2337
  assumes "2 \<le> DIM('a::euclidean_space)"
lp15@61426
  2338
  shows "path_connected (- {a::'a})"
wenzelm@49653
  2339
proof -
hoelzl@50526
  2340
  let ?A = "{x::'a. \<exists>i\<in>Basis. x \<bullet> i < a \<bullet> i}"
hoelzl@50526
  2341
  let ?B = "{x::'a. \<exists>i\<in>Basis. a \<bullet> i < x \<bullet> i}"
huffman@36583
  2342
wenzelm@49653
  2343
  have A: "path_connected ?A"
wenzelm@49653
  2344
    unfolding Collect_bex_eq
huffman@37674
  2345
  proof (rule path_connected_UNION)
hoelzl@50526
  2346
    fix i :: 'a
hoelzl@50526
  2347
    assume "i \<in> Basis"