src/HOL/Multivariate_Analysis/Path_Connected.thy
author wenzelm
Fri, 28 Sep 2012 23:40:48 +0200
changeset 49653 03bc7afe8814
parent 48125 602dc0215954
child 49654 366d8b41ca17
permissions -rw-r--r--
tuned proofs;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
41959
b460124855b8 tuned headers;
wenzelm
parents: 39302
diff changeset
     1
(*  Title:      HOL/Multivariate_Analysis/Path_Connected.thy
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
     2
    Author:     Robert Himmelmann, TU Muenchen
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
     3
*)
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
     4
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
     5
header {* Continuous paths and path-connected sets *}
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
     6
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
     7
theory Path_Connected
37674
f86de9c00c47 convert theorem path_connected_sphere to euclidean_space class
huffman
parents: 37489
diff changeset
     8
imports Convex_Euclidean_Space
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
     9
begin
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
    10
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
    11
subsection {* Paths. *}
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
    12
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
    13
definition path :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> bool"
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
    14
  where "path g \<longleftrightarrow> continuous_on {0 .. 1} g"
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
    15
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
    16
definition pathstart :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> 'a"
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
    17
  where "pathstart g = g 0"
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
    18
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
    19
definition pathfinish :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> 'a"
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
    20
  where "pathfinish g = g 1"
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
    21
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
    22
definition path_image :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> 'a set"
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
    23
  where "path_image g = g ` {0 .. 1}"
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
    24
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
    25
definition reversepath :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> (real \<Rightarrow> 'a)"
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
    26
  where "reversepath g = (\<lambda>x. g(1 - x))"
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
    27
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
    28
definition joinpaths :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> (real \<Rightarrow> 'a)"
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
    29
    (infixr "+++" 75)
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
    30
  where "g1 +++ g2 = (\<lambda>x. if x \<le> 1/2 then g1 (2 * x) else g2 (2 * x - 1))"
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
    31
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
    32
definition simple_path :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> bool"
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
    33
  where "simple_path g \<longleftrightarrow>
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
    34
    (\<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)"
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
    35
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
    36
definition injective_path :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> bool"
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
    37
  where "injective_path g \<longleftrightarrow> (\<forall>x\<in>{0..1}. \<forall>y\<in>{0..1}. g x = g y \<longrightarrow> x = y)"
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
    38
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
    39
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
    40
subsection {* Some lemmas about these concepts. *}
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
    41
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
    42
lemma injective_imp_simple_path: "injective_path g \<Longrightarrow> simple_path g"
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
    43
  unfolding injective_path_def simple_path_def by auto
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
    44
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
    45
lemma path_image_nonempty: "path_image g \<noteq> {}"
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
    46
  unfolding path_image_def image_is_empty interval_eq_empty by auto 
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
    47
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
    48
lemma pathstart_in_path_image[intro]: "(pathstart g) \<in> path_image g"
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
    49
  unfolding pathstart_def path_image_def by auto
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
    50
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
    51
lemma pathfinish_in_path_image[intro]: "(pathfinish g) \<in> path_image g"
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
    52
  unfolding pathfinish_def path_image_def by auto
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
    53
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
    54
lemma connected_path_image[intro]: "path g \<Longrightarrow> connected(path_image g)"
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
    55
  unfolding path_def path_image_def
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
    56
  apply (erule connected_continuous_image)
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
    57
  apply (rule convex_connected, rule convex_real_interval)
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
    58
  done
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
    59
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
    60
lemma compact_path_image[intro]: "path g \<Longrightarrow> compact(path_image g)"
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
    61
  unfolding path_def path_image_def
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36583
diff changeset
    62
  by (erule compact_continuous_image, rule compact_interval)
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
    63
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
    64
lemma reversepath_reversepath[simp]: "reversepath(reversepath g) = g"
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
    65
  unfolding reversepath_def by auto
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
    66
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
    67
lemma pathstart_reversepath[simp]: "pathstart(reversepath g) = pathfinish g"
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
    68
  unfolding pathstart_def reversepath_def pathfinish_def by auto
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
    69
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
    70
lemma pathfinish_reversepath[simp]: "pathfinish(reversepath g) = pathstart g"
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
    71
  unfolding pathstart_def reversepath_def pathfinish_def by auto
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
    72
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
    73
lemma pathstart_join[simp]: "pathstart (g1 +++ g2) = pathstart g1"
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
    74
  unfolding pathstart_def joinpaths_def pathfinish_def by auto
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
    75
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
    76
lemma pathfinish_join[simp]: "pathfinish (g1 +++ g2) = pathfinish g2"
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
    77
  unfolding pathstart_def joinpaths_def pathfinish_def by auto
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
    78
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
    79
lemma path_image_reversepath[simp]: "path_image(reversepath g) = path_image g"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
    80
proof -
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
    81
  have *: "\<And>g. path_image(reversepath g) \<subseteq> path_image g"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
    82
    unfolding path_image_def subset_eq reversepath_def Ball_def image_iff
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
    83
    apply(rule,rule,erule bexE)
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
    84
    apply(rule_tac x="1 - xa" in bexI)
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
    85
    apply auto
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
    86
    done
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
    87
  show ?thesis
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
    88
    using *[of g] *[of "reversepath g"]
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
    89
    unfolding reversepath_reversepath by auto
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
    90
qed
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
    91
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
    92
lemma path_reversepath[simp]: "path (reversepath g) \<longleftrightarrow> path g"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
    93
proof -
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
    94
  have *: "\<And>g. path g \<Longrightarrow> path (reversepath g)"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
    95
    unfolding path_def reversepath_def
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
    96
    apply (rule continuous_on_compose[unfolded o_def, of _ "\<lambda>x. 1 - x"])
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
    97
    apply (intro continuous_on_intros)
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
    98
    apply (rule continuous_on_subset[of "{0..1}"], assumption)
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
    99
    apply auto
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   100
    done
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   101
  show ?thesis
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   102
    using *[of "reversepath g"] *[of g]
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   103
    unfolding reversepath_reversepath
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   104
    by (rule iffI)
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   105
qed
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   106
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   107
lemmas reversepath_simps =
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   108
  path_reversepath path_image_reversepath pathstart_reversepath pathfinish_reversepath
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   109
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   110
lemma path_join[simp]:
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   111
  assumes "pathfinish g1 = pathstart g2"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   112
  shows "path (g1 +++ g2) \<longleftrightarrow> path g1 \<and> path g2"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   113
  unfolding path_def pathfinish_def pathstart_def
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   114
  apply rule defer
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   115
  apply(erule conjE)
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   116
proof -
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   117
  assume as: "continuous_on {0..1} (g1 +++ g2)"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   118
  have *: "g1 = (\<lambda>x. g1 (2 *\<^sub>R x)) \<circ> (\<lambda>x. (1/2) *\<^sub>R x)"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   119
      "g2 = (\<lambda>x. g2 (2 *\<^sub>R x - 1)) \<circ> (\<lambda>x. (1/2) *\<^sub>R (x + 1))"
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   120
    unfolding o_def by (auto simp add: add_divide_distrib)
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   121
  have "op *\<^sub>R (1 / 2) ` {0::real..1} \<subseteq> {0..1}"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   122
    "(\<lambda>x. (1 / 2) *\<^sub>R (x + 1)) ` {(0::real)..1} \<subseteq> {0..1}"
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   123
    by auto
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   124
  then show "continuous_on {0..1} g1 \<and> continuous_on {0..1} g2"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   125
    apply -
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   126
    apply rule
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   127
    apply (subst *) defer
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   128
    apply (subst *)
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   129
    apply (rule_tac[!] continuous_on_compose)
44531
1d477a2b1572 replace some continuous_on lemmas with more general versions
huffman
parents: 44170
diff changeset
   130
    apply (intro continuous_on_intros) defer
1d477a2b1572 replace some continuous_on lemmas with more general versions
huffman
parents: 44170
diff changeset
   131
    apply (intro continuous_on_intros)
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   132
    apply (rule_tac[!] continuous_on_eq[of _ "g1 +++ g2"]) defer prefer 3
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   133
    apply (rule_tac[1-2] continuous_on_subset[of "{0 .. 1}"])
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   134
    apply (rule as, assumption, rule as, assumption)
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   135
    apply rule defer
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   136
    apply rule
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   137
  proof -
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   138
    fix x
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   139
    assume "x \<in> op *\<^sub>R (1 / 2) ` {0::real..1}"
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   140
    hence "x \<le> 1 / 2" unfolding image_iff by auto
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   141
    thus "(g1 +++ g2) x = g1 (2 *\<^sub>R x)" unfolding joinpaths_def by auto
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   142
  next
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   143
    fix x
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   144
    assume "x \<in> (\<lambda>x. (1 / 2) *\<^sub>R (x + 1)) ` {0::real..1}"
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   145
    hence "x \<ge> 1 / 2" unfolding image_iff by auto
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   146
    thus "(g1 +++ g2) x = g2 (2 *\<^sub>R x - 1)"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   147
    proof (cases "x = 1 / 2")
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   148
      case True
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   149
      hence "x = (1/2) *\<^sub>R 1" by auto
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   150
      thus ?thesis
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   151
        unfolding joinpaths_def
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   152
        using assms[unfolded pathstart_def pathfinish_def]
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   153
        by (auto simp add: mult_ac)
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   154
    qed (auto simp add:le_less joinpaths_def)
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   155
  qed
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   156
next
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   157
  assume as:"continuous_on {0..1} g1" "continuous_on {0..1} g2"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   158
  have *: "{0 .. 1::real} = {0.. (1/2)*\<^sub>R 1} \<union> {(1/2) *\<^sub>R 1 .. 1}" by auto
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   159
  have **: "op *\<^sub>R 2 ` {0..(1 / 2) *\<^sub>R 1} = {0..1::real}"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   160
    apply (rule set_eqI, rule)
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   161
    unfolding image_iff
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   162
    defer
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   163
    apply (rule_tac x="(1/2)*\<^sub>R x" in bexI)
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   164
    apply auto
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   165
    done
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   166
  have ***: "(\<lambda>x. 2 *\<^sub>R x - 1) ` {(1 / 2) *\<^sub>R 1..1} = {0..1::real}"
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   167
    apply (auto simp add: image_def)
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   168
    apply (rule_tac x="(x + 1) / 2" in bexI)
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   169
    apply (auto simp add: add_divide_distrib)
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   170
    done
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   171
  show "continuous_on {0..1} (g1 +++ g2)"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   172
    unfolding *
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   173
    apply (rule continuous_on_union)
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   174
    apply (rule closed_real_atLeastAtMost)+
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   175
  proof -
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   176
    show "continuous_on {0..(1 / 2) *\<^sub>R 1} (g1 +++ g2)"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   177
      apply (rule continuous_on_eq[of _ "\<lambda>x. g1 (2 *\<^sub>R x)"]) defer
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   178
      unfolding o_def[THEN sym]
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   179
      apply (rule continuous_on_compose)
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   180
      apply (intro continuous_on_intros)
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   181
      unfolding **
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   182
      apply (rule as(1))
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   183
      unfolding joinpaths_def
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   184
      apply auto
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   185
      done
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   186
  next
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   187
    show "continuous_on {(1/2)*\<^sub>R1..1} (g1 +++ g2)"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   188
      apply (rule continuous_on_eq[of _ "g2 \<circ> (\<lambda>x. 2 *\<^sub>R x - 1)"]) defer
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   189
      apply (rule continuous_on_compose)
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   190
      apply (intro continuous_on_intros)
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   191
      unfolding *** o_def joinpaths_def
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   192
      apply (rule as(2))
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   193
      using assms[unfolded pathstart_def pathfinish_def]
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   194
      apply (auto simp add: mult_ac)  
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   195
      done
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   196
  qed
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   197
qed
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   198
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   199
lemma path_image_join_subset: "path_image(g1 +++ g2) \<subseteq> (path_image g1 \<union> path_image g2)"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   200
proof
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   201
  fix x
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   202
  assume "x \<in> path_image (g1 +++ g2)"
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   203
  then obtain y where y:"y\<in>{0..1}" "x = (if y \<le> 1 / 2 then g1 (2 *\<^sub>R y) else g2 (2 *\<^sub>R y - 1))"
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   204
    unfolding path_image_def image_iff joinpaths_def by auto
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   205
  thus "x \<in> path_image g1 \<union> path_image g2"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   206
    apply (cases "y \<le> 1/2")
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   207
    apply (rule_tac UnI1) defer
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   208
    apply (rule_tac UnI2)
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   209
    unfolding y(2) path_image_def
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   210
    using y(1)
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   211
    apply (auto intro!: imageI)
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   212
    done
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   213
qed
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   214
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   215
lemma subset_path_image_join:
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   216
  assumes "path_image g1 \<subseteq> s" "path_image g2 \<subseteq> s"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   217
  shows "path_image(g1 +++ g2) \<subseteq> s"
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   218
  using path_image_join_subset[of g1 g2] and assms by auto
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   219
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   220
lemma path_image_join:
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   221
  assumes "path g1" "path g2" "pathfinish g1 = pathstart g2"
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   222
  shows "path_image(g1 +++ g2) = (path_image g1) \<union> (path_image g2)"
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   223
  apply (rule, rule path_image_join_subset, rule)
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   224
  unfolding Un_iff
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   225
proof (erule disjE)
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   226
  fix x
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   227
  assume "x \<in> path_image g1"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   228
  then obtain y where y: "y\<in>{0..1}" "x = g1 y"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   229
    unfolding path_image_def image_iff by auto
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   230
  thus "x \<in> path_image (g1 +++ g2)"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   231
    unfolding joinpaths_def path_image_def image_iff
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   232
    apply (rule_tac x="(1/2) *\<^sub>R y" in bexI)
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   233
    apply auto
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   234
    done
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   235
next
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   236
  fix x
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   237
  assume "x \<in> path_image g2"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   238
  then obtain y where y: "y\<in>{0..1}" "x = g2 y"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   239
    unfolding path_image_def image_iff by auto
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   240
  then show "x \<in> path_image (g1 +++ g2)"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   241
    unfolding joinpaths_def path_image_def image_iff
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   242
    apply(rule_tac x="(1/2) *\<^sub>R (y + 1)" in bexI)
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   243
    using assms(3)[unfolded pathfinish_def pathstart_def]
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   244
    apply (auto simp add: add_divide_distrib) 
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   245
    done
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   246
qed
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   247
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   248
lemma not_in_path_image_join:
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   249
  assumes "x \<notin> path_image g1" "x \<notin> path_image g2"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   250
  shows "x \<notin> path_image(g1 +++ g2)"
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   251
  using assms and path_image_join_subset[of g1 g2] by auto
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   252
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   253
lemma simple_path_reversepath:
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   254
  assumes "simple_path g"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   255
  shows "simple_path (reversepath g)"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   256
  using assms
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   257
  unfolding simple_path_def reversepath_def
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   258
  apply -
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   259
  apply (rule ballI)+
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   260
  apply (erule_tac x="1-x" in ballE, erule_tac x="1-y" in ballE)
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   261
  apply auto
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   262
  done
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   263
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   264
lemma simple_path_join_loop:
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   265
  assumes "injective_path g1" "injective_path g2" "pathfinish g2 = pathstart g1"
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   266
    "(path_image g1 \<inter> path_image g2) \<subseteq> {pathstart g1,pathstart g2}"
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   267
  shows "simple_path(g1 +++ g2)"
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   268
  unfolding simple_path_def
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   269
proof ((rule ballI)+, rule impI)
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   270
  let ?g = "g1 +++ g2"
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   271
  note inj = assms(1,2)[unfolded injective_path_def, rule_format]
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   272
  fix x y :: real
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   273
  assume xy: "x \<in> {0..1}" "y \<in> {0..1}" "?g x = ?g y"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   274
  show "x = y \<or> x = 0 \<and> y = 1 \<or> x = 1 \<and> y = 0"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   275
  proof (case_tac "x \<le> 1/2", case_tac[!] "y \<le> 1/2", unfold not_le)
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   276
    assume as: "x \<le> 1 / 2" "y \<le> 1 / 2"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   277
    hence "g1 (2 *\<^sub>R x) = g1 (2 *\<^sub>R y)"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   278
      using xy(3) unfolding joinpaths_def by auto
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   279
    moreover
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   280
    have "2 *\<^sub>R x \<in> {0..1}" "2 *\<^sub>R y \<in> {0..1}" using xy(1,2) as
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   281
      by auto
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   282
    ultimately
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   283
    show ?thesis using inj(1)[of "2*\<^sub>R x" "2*\<^sub>R y"] by auto
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   284
  next
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   285
    assume as:"x > 1 / 2" "y > 1 / 2"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   286
    hence "g2 (2 *\<^sub>R x - 1) = g2 (2 *\<^sub>R y - 1)"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   287
      using xy(3) unfolding joinpaths_def by auto
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   288
    moreover
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   289
    have "2 *\<^sub>R x - 1 \<in> {0..1}" "2 *\<^sub>R y - 1 \<in> {0..1}"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   290
      using xy(1,2) as by auto
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   291
    ultimately
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   292
    show ?thesis using inj(2)[of "2*\<^sub>R x - 1" "2*\<^sub>R y - 1"] by auto
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   293
  next
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   294
    assume as:"x \<le> 1 / 2" "y > 1 / 2"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   295
    hence "?g x \<in> path_image g1" "?g y \<in> path_image g2"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   296
      unfolding path_image_def joinpaths_def
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   297
      using xy(1,2) by auto
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   298
    moreover
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   299
      have "?g y \<noteq> pathstart g2" using as(2) unfolding pathstart_def joinpaths_def
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   300
      using inj(2)[of "2 *\<^sub>R y - 1" 0] and xy(2)
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   301
      by (auto simp add: field_simps)
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   302
    ultimately
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   303
    have *:"?g x = pathstart g1" using assms(4) unfolding xy(3) by auto
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   304
    hence "x = 0" unfolding pathstart_def joinpaths_def using as(1) and xy(1)
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   305
      using inj(1)[of "2 *\<^sub>R x" 0] by auto
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   306
    moreover
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   307
    have "y = 1" using * unfolding xy(3) assms(3)[THEN sym]
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   308
      unfolding joinpaths_def pathfinish_def using as(2) and xy(2)
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   309
      using inj(2)[of "2 *\<^sub>R y - 1" 1] by auto
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   310
    ultimately show ?thesis by auto
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   311
  next
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   312
    assume as: "x > 1 / 2" "y \<le> 1 / 2"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   313
    hence "?g x \<in> path_image g2" "?g y \<in> path_image g1"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   314
      unfolding path_image_def joinpaths_def
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   315
      using xy(1,2) by auto
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   316
    moreover
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   317
      have "?g x \<noteq> pathstart g2" using as(1) unfolding pathstart_def joinpaths_def
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   318
      using inj(2)[of "2 *\<^sub>R x - 1" 0] and xy(1)
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   319
      by (auto simp add: field_simps)
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   320
    ultimately
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   321
    have *: "?g y = pathstart g1" using assms(4) unfolding xy(3) by auto
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   322
    hence "y = 0" unfolding pathstart_def joinpaths_def using as(2) and xy(2)
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   323
      using inj(1)[of "2 *\<^sub>R y" 0] by auto
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   324
    moreover
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   325
    have "x = 1" using * unfolding xy(3)[THEN sym] assms(3)[THEN sym]
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   326
      unfolding joinpaths_def pathfinish_def using as(1) and xy(1)
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   327
      using inj(2)[of "2 *\<^sub>R x - 1" 1] by auto
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   328
    ultimately show ?thesis by auto
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   329
  qed
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   330
qed
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   331
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   332
lemma injective_path_join:
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   333
  assumes "injective_path g1" "injective_path g2" "pathfinish g1 = pathstart g2"
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   334
    "(path_image g1 \<inter> path_image g2) \<subseteq> {pathstart g2}"
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   335
  shows "injective_path(g1 +++ g2)"
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   336
  unfolding injective_path_def
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   337
proof (rule, rule, rule)
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   338
  let ?g = "g1 +++ g2"
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   339
  note inj = assms(1,2)[unfolded injective_path_def, rule_format]
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   340
  fix x y
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   341
  assume xy: "x \<in> {0..1}" "y \<in> {0..1}" "(g1 +++ g2) x = (g1 +++ g2) y"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   342
  show "x = y"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   343
  proof (cases "x \<le> 1/2", case_tac[!] "y \<le> 1/2", unfold not_le)
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   344
    assume "x \<le> 1 / 2" "y \<le> 1 / 2"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   345
    thus ?thesis using inj(1)[of "2*\<^sub>R x" "2*\<^sub>R y"] and xy
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   346
      unfolding joinpaths_def by auto
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   347
  next
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   348
    assume "x > 1 / 2" "y > 1 / 2"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   349
    thus ?thesis using inj(2)[of "2*\<^sub>R x - 1" "2*\<^sub>R y - 1"] and xy
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   350
      unfolding joinpaths_def by auto
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   351
  next
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   352
    assume as: "x \<le> 1 / 2" "y > 1 / 2"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   353
    hence "?g x \<in> path_image g1" "?g y \<in> path_image g2"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   354
      unfolding path_image_def joinpaths_def
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   355
      using xy(1,2) by auto
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   356
    hence "?g x = pathfinish g1" "?g y = pathstart g2"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   357
      using assms(4) unfolding assms(3) xy(3) by auto
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   358
    thus ?thesis
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   359
      using as and inj(1)[of "2 *\<^sub>R x" 1] inj(2)[of "2 *\<^sub>R y - 1" 0] and xy(1,2)
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   360
      unfolding pathstart_def pathfinish_def joinpaths_def
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   361
      by auto
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   362
  next
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   363
    assume as:"x > 1 / 2" "y \<le> 1 / 2" 
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   364
    hence "?g x \<in> path_image g2" "?g y \<in> path_image g1"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   365
      unfolding path_image_def joinpaths_def
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   366
      using xy(1,2) by auto
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   367
    hence "?g x = pathstart g2" "?g y = pathfinish g1"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   368
      using assms(4) unfolding assms(3) xy(3) by auto
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   369
    thus ?thesis using as and inj(2)[of "2 *\<^sub>R x - 1" 0] inj(1)[of "2 *\<^sub>R y" 1] and xy(1,2)
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   370
      unfolding pathstart_def pathfinish_def joinpaths_def
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   371
      by auto
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   372
  qed
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   373
qed
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   374
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   375
lemmas join_paths_simps = path_join path_image_join pathstart_join pathfinish_join
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   376
 
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   377
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   378
subsection {* Reparametrizing a closed curve to start at some chosen point. *}
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   379
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   380
definition "shiftpath a (f::real \<Rightarrow> 'a::topological_space) =
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   381
  (\<lambda>x. if (a + x) \<le> 1 then f(a + x) else f(a + x - 1))"
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   382
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   383
lemma pathstart_shiftpath: "a \<le> 1 \<Longrightarrow> pathstart(shiftpath a g) = g a"
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   384
  unfolding pathstart_def shiftpath_def by auto
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   385
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   386
lemma pathfinish_shiftpath:
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   387
  assumes "0 \<le> a" "pathfinish g = pathstart g"
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   388
  shows "pathfinish(shiftpath a g) = g a"
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   389
  using assms unfolding pathstart_def pathfinish_def shiftpath_def
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   390
  by auto
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   391
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   392
lemma endpoints_shiftpath:
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   393
  assumes "pathfinish g = pathstart g" "a \<in> {0 .. 1}" 
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   394
  shows "pathfinish(shiftpath a g) = g a" "pathstart(shiftpath a g) = g a"
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   395
  using assms by(auto intro!:pathfinish_shiftpath pathstart_shiftpath)
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   396
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   397
lemma closed_shiftpath:
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   398
  assumes "pathfinish g = pathstart g" "a \<in> {0..1}"
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   399
  shows "pathfinish(shiftpath a g) = pathstart(shiftpath a g)"
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   400
  using endpoints_shiftpath[OF assms] by auto
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   401
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   402
lemma path_shiftpath:
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   403
  assumes "path g" "pathfinish g = pathstart g" "a \<in> {0..1}"
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   404
  shows "path(shiftpath a g)"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   405
proof -
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   406
  have *: "{0 .. 1} = {0 .. 1-a} \<union> {1-a .. 1}" using assms(3) by auto
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   407
  have **: "\<And>x. x + a = 1 \<Longrightarrow> g (x + a - 1) = g (x + a)"
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   408
    using assms(2)[unfolded pathfinish_def pathstart_def] by auto
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   409
  show ?thesis
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   410
    unfolding path_def shiftpath_def *
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   411
    apply (rule continuous_on_union)
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   412
    apply (rule closed_real_atLeastAtMost)+
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   413
    apply (rule continuous_on_eq[of _ "g \<circ> (\<lambda>x. a + x)"]) prefer 3
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   414
    apply (rule continuous_on_eq[of _ "g \<circ> (\<lambda>x. a - 1 + x)"]) defer prefer 3
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   415
    apply (rule continuous_on_intros)+ prefer 2
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   416
    apply (rule continuous_on_intros)+
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   417
    apply (rule_tac[1-2] continuous_on_subset[OF assms(1)[unfolded path_def]])
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   418
    using assms(3) and **
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   419
    apply (auto, auto simp add: field_simps)
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   420
    done
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   421
qed
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   422
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   423
lemma shiftpath_shiftpath:
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   424
  assumes "pathfinish g = pathstart g" "a \<in> {0..1}" "x \<in> {0..1}" 
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   425
  shows "shiftpath (1 - a) (shiftpath a g) x = g x"
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   426
  using assms unfolding pathfinish_def pathstart_def shiftpath_def by auto
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   427
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   428
lemma path_image_shiftpath:
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   429
  assumes "a \<in> {0..1}" "pathfinish g = pathstart g"
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   430
  shows "path_image(shiftpath a g) = path_image g"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   431
proof -
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   432
  { fix x
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   433
    assume as:"g 1 = g 0" "x \<in> {0..1::real}" " \<forall>y\<in>{0..1} \<inter> {x. \<not> a + x \<le> 1}. g x \<noteq> g (a + y - 1)" 
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   434
    hence "\<exists>y\<in>{0..1} \<inter> {x. a + x \<le> 1}. g x = g (a + y)"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   435
    proof (cases "a \<le> x")
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   436
      case False
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   437
      thus ?thesis
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   438
        apply (rule_tac x="1 + x - a" in bexI)
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   439
        using as(1,2) and as(3)[THEN bspec[where x="1 + x - a"]] and assms(1)
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   440
        apply (auto simp add: field_simps atomize_not)
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   441
        done
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   442
    next
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   443
      case True
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   444
      thus ?thesis using as(1-2) and assms(1) apply(rule_tac x="x - a" in bexI)
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   445
        by(auto simp add: field_simps)
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   446
    qed
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   447
  }
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   448
  thus ?thesis
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   449
    using assms unfolding shiftpath_def path_image_def pathfinish_def pathstart_def
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   450
    by(auto simp add: image_iff)
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   451
qed
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   452
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   453
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   454
subsection {* Special case of straight-line paths. *}
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   455
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   456
definition linepath :: "'a::real_normed_vector \<Rightarrow> 'a \<Rightarrow> real \<Rightarrow> 'a"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   457
  where "linepath a b = (\<lambda>x. (1 - x) *\<^sub>R a + x *\<^sub>R b)"
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   458
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   459
lemma pathstart_linepath[simp]: "pathstart(linepath a b) = a"
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   460
  unfolding pathstart_def linepath_def by auto
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   461
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   462
lemma pathfinish_linepath[simp]: "pathfinish(linepath a b) = b"
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   463
  unfolding pathfinish_def linepath_def by auto
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   464
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   465
lemma continuous_linepath_at[intro]: "continuous (at x) (linepath a b)"
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   466
  unfolding linepath_def by (intro continuous_intros)
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   467
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   468
lemma continuous_on_linepath[intro]: "continuous_on s (linepath a b)"
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   469
  using continuous_linepath_at by(auto intro!: continuous_at_imp_continuous_on)
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   470
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   471
lemma path_linepath[intro]: "path(linepath a b)"
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   472
  unfolding path_def by(rule continuous_on_linepath)
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   473
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   474
lemma path_image_linepath[simp]: "path_image(linepath a b) = (closed_segment a b)"
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   475
  unfolding path_image_def segment linepath_def
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   476
  apply (rule set_eqI, rule) defer
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   477
  unfolding mem_Collect_eq image_iff
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   478
  apply(erule exE)
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   479
  apply(rule_tac x="u *\<^sub>R 1" in bexI)
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   480
  apply auto
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   481
  done
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   482
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   483
lemma reversepath_linepath[simp]: "reversepath(linepath a b) = linepath b a"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   484
  unfolding reversepath_def linepath_def
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   485
  by auto
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   486
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   487
lemma injective_path_linepath:
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   488
  assumes "a \<noteq> b"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   489
  shows "injective_path (linepath a b)"
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   490
proof -
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   491
  { fix x y :: "real"
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   492
    assume "x *\<^sub>R b + y *\<^sub>R a = x *\<^sub>R a + y *\<^sub>R b"
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   493
    hence "(x - y) *\<^sub>R a = (x - y) *\<^sub>R b" by (simp add: algebra_simps)
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   494
    with assms have "x = y" by simp }
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   495
  thus ?thesis
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   496
    unfolding injective_path_def linepath_def
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   497
    by (auto simp add: algebra_simps)
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   498
qed
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   499
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   500
lemma simple_path_linepath[intro]: "a \<noteq> b \<Longrightarrow> simple_path(linepath a b)"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   501
  by(auto intro!: injective_imp_simple_path injective_path_linepath)
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   502
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   503
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   504
subsection {* Bounding a point away from a path. *}
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   505
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   506
lemma not_on_path_ball:
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   507
  fixes g :: "real \<Rightarrow> 'a::heine_borel"
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   508
  assumes "path g" "z \<notin> path_image g"
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   509
  shows "\<exists>e > 0. ball z e \<inter> (path_image g) = {}"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   510
proof -
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   511
  obtain a where "a \<in> path_image g" "\<forall>y \<in> path_image g. dist z a \<le> dist z y"
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   512
    using distance_attains_inf[OF _ path_image_nonempty, of g z]
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   513
    using compact_path_image[THEN compact_imp_closed, OF assms(1)] by auto
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   514
  thus ?thesis
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   515
    apply (rule_tac x="dist z a" in exI)
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   516
    using assms(2)
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   517
    apply (auto intro!: dist_pos_lt)
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   518
    done
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   519
qed
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   520
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   521
lemma not_on_path_cball:
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   522
  fixes g :: "real \<Rightarrow> 'a::heine_borel"
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   523
  assumes "path g" "z \<notin> path_image g"
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   524
  shows "\<exists>e>0. cball z e \<inter> (path_image g) = {}"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   525
proof -
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   526
  obtain e where "ball z e \<inter> path_image g = {}" "e>0"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   527
    using not_on_path_ball[OF assms] by auto
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   528
  moreover have "cball z (e/2) \<subseteq> ball z e" using `e>0` by auto
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   529
  ultimately show ?thesis apply(rule_tac x="e/2" in exI) by auto
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   530
qed
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   531
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   532
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   533
subsection {* Path component, considered as a "joinability" relation (from Tom Hales). *}
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   534
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   535
definition "path_component s x y \<longleftrightarrow>
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   536
  (\<exists>g. path g \<and> path_image g \<subseteq> s \<and> pathstart g = x \<and> pathfinish g = y)"
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   537
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   538
lemmas path_defs = path_def pathstart_def pathfinish_def path_image_def path_component_def 
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   539
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   540
lemma path_component_mem:
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   541
  assumes "path_component s x y"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   542
  shows "x \<in> s" "y \<in> s"
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   543
  using assms unfolding path_defs by auto
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   544
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   545
lemma path_component_refl:
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   546
  assumes "x \<in> s"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   547
  shows "path_component s x x"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   548
  unfolding path_defs
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   549
  apply (rule_tac x="\<lambda>u. x" in exI)
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   550
  using assms apply (auto intro!:continuous_on_intros) done
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   551
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   552
lemma path_component_refl_eq: "path_component s x x \<longleftrightarrow> x \<in> s"
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   553
  by (auto intro!: path_component_mem path_component_refl)
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   554
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   555
lemma path_component_sym: "path_component s x y \<Longrightarrow> path_component s y x"
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   556
  using assms
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   557
  unfolding path_component_def
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   558
  apply (erule exE)
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   559
  apply (rule_tac x="reversepath g" in exI)
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   560
  apply auto
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   561
  done
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   562
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   563
lemma path_component_trans:
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   564
  assumes "path_component s x y" "path_component s y z"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   565
  shows "path_component s x z"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   566
  using assms
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   567
  unfolding path_component_def
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   568
  apply -
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   569
  apply (erule exE)+
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   570
  apply (rule_tac x="g +++ ga" in exI)
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   571
  apply (auto simp add: path_image_join)
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   572
  done
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   573
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   574
lemma path_component_of_subset: "s \<subseteq> t \<Longrightarrow>  path_component s x y \<Longrightarrow> path_component t x y"
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   575
  unfolding path_component_def by auto
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   576
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   577
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   578
subsection {* Can also consider it as a set, as the name suggests. *}
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   579
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   580
lemma path_component_set:
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   581
  "{y. path_component s x y} =
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   582
    {y. (\<exists>g. path g \<and> path_image g \<subseteq> s \<and> pathstart g = x \<and> pathfinish g = y)}"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   583
  apply (rule set_eqI)
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   584
  unfolding mem_Collect_eq
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   585
  unfolding path_component_def
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   586
  apply auto
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   587
  done
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   588
44170
510ac30f44c0 make Multivariate_Analysis work with separate set type
huffman
parents: 41959
diff changeset
   589
lemma path_component_subset: "{y. path_component s x y} \<subseteq> s"
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   590
  apply (rule, rule path_component_mem(2))
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   591
  apply auto
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   592
  done
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   593
44170
510ac30f44c0 make Multivariate_Analysis work with separate set type
huffman
parents: 41959
diff changeset
   594
lemma path_component_eq_empty: "{y. path_component s x y} = {} \<longleftrightarrow> x \<notin> s"
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   595
  apply rule
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   596
  apply (drule equals0D[of _ x]) defer
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   597
  apply (rule equals0I)
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   598
  unfolding mem_Collect_eq
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   599
  apply (drule path_component_mem(1))
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   600
  using path_component_refl
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   601
  apply auto
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   602
  done
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   603
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   604
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   605
subsection {* Path connectedness of a space. *}
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   606
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   607
definition "path_connected s \<longleftrightarrow>
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   608
  (\<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)"
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   609
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   610
lemma path_connected_component: "path_connected s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>y\<in>s. path_component s x y)"
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   611
  unfolding path_connected_def path_component_def by auto
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   612
44170
510ac30f44c0 make Multivariate_Analysis work with separate set type
huffman
parents: 41959
diff changeset
   613
lemma path_connected_component_set: "path_connected s \<longleftrightarrow> (\<forall>x\<in>s. {y. path_component s x y} = s)" 
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   614
  unfolding path_connected_component
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   615
  apply (rule, rule, rule, rule path_component_subset) 
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   616
  unfolding subset_eq mem_Collect_eq Ball_def
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   617
  apply auto
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   618
  done
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   619
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   620
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   621
subsection {* Some useful lemmas about path-connectedness. *}
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   622
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   623
lemma convex_imp_path_connected:
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   624
  fixes s :: "'a::real_normed_vector set"
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   625
  assumes "convex s" shows "path_connected s"
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   626
  unfolding path_connected_def
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   627
  apply (rule, rule, rule_tac x = "linepath x y" in exI)
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   628
  unfolding path_image_linepath
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   629
  using assms [unfolded convex_contains_segment]
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   630
  apply auto
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   631
  done
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   632
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   633
lemma path_connected_imp_connected:
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   634
  assumes "path_connected s"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   635
  shows "connected s"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   636
  unfolding connected_def not_ex
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   637
  apply (rule, rule, rule ccontr)
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   638
  unfolding not_not
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   639
  apply (erule conjE)+
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   640
proof -
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   641
  fix e1 e2
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   642
  assume as: "open e1" "open e2" "s \<subseteq> e1 \<union> e2" "e1 \<inter> e2 \<inter> s = {}" "e1 \<inter> s \<noteq> {}" "e2 \<inter> s \<noteq> {}"
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   643
  then obtain x1 x2 where obt:"x1\<in>e1\<inter>s" "x2\<in>e2\<inter>s" by auto
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   644
  then obtain g where g:"path g" "path_image g \<subseteq> s" "pathstart g = x1" "pathfinish g = x2"
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   645
    using assms[unfolded path_connected_def,rule_format,of x1 x2] by auto
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   646
  have *: "connected {0..1::real}"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   647
    by (auto intro!: convex_connected convex_real_interval)
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   648
  have "{0..1} \<subseteq> {x \<in> {0..1}. g x \<in> e1} \<union> {x \<in> {0..1}. g x \<in> e2}"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   649
    using as(3) g(2)[unfolded path_defs] by blast
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   650
  moreover have "{x \<in> {0..1}. g x \<in> e1} \<inter> {x \<in> {0..1}. g x \<in> e2} = {}"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   651
    using as(4) g(2)[unfolded path_defs] unfolding subset_eq by auto 
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   652
  moreover have "{x \<in> {0..1}. g x \<in> e1} \<noteq> {} \<and> {x \<in> {0..1}. g x \<in> e2} \<noteq> {}"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   653
    using g(3,4)[unfolded path_defs] using obt
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   654
    by (simp add: ex_in_conv [symmetric], metis zero_le_one order_refl)
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   655
  ultimately show False
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   656
    using *[unfolded connected_local not_ex, rule_format, of "{x\<in>{0..1}. g x \<in> e1}" "{x\<in>{0..1}. g x \<in> e2}"]
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   657
    using continuous_open_in_preimage[OF g(1)[unfolded path_def] as(1)]
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   658
    using continuous_open_in_preimage[OF g(1)[unfolded path_def] as(2)]
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   659
    by auto
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   660
qed
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   661
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   662
lemma open_path_component:
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   663
  fixes s :: "'a::real_normed_vector set" (*TODO: generalize to metric_space*)
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   664
  assumes "open s"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   665
  shows "open {y. path_component s x y}"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   666
  unfolding open_contains_ball
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   667
proof
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   668
  fix y
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   669
  assume as: "y \<in> {y. path_component s x y}"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   670
  hence "y \<in> s"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   671
    apply -
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   672
    apply (rule path_component_mem(2))
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   673
    unfolding mem_Collect_eq
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   674
    apply auto
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   675
    done
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   676
  then obtain e where e:"e>0" "ball y e \<subseteq> s"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   677
    using assms[unfolded open_contains_ball] by auto
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   678
  show "\<exists>e > 0. ball y e \<subseteq> {y. path_component s x y}"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   679
    apply (rule_tac x=e in exI)
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   680
    apply (rule,rule `e>0`, rule)
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   681
    unfolding mem_ball mem_Collect_eq
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   682
  proof -
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   683
    fix z
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   684
    assume "dist y z < e"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   685
    thus "path_component s x z"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   686
      apply (rule_tac path_component_trans[of _ _ y]) defer
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   687
      apply (rule path_component_of_subset[OF e(2)])
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   688
      apply (rule convex_imp_path_connected[OF convex_ball, unfolded path_connected_component, rule_format])
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   689
      using `e>0` as
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   690
      apply auto
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   691
      done
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   692
  qed
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   693
qed
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   694
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   695
lemma open_non_path_component:
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   696
  fixes s :: "'a::real_normed_vector set" (*TODO: generalize to metric_space*)
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   697
  assumes "open s"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   698
  shows "open(s - {y. path_component s x y})"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   699
  unfolding open_contains_ball
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   700
proof
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   701
  fix y
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   702
  assume as: "y\<in>s - {y. path_component s x y}"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   703
  then obtain e where e:"e>0" "ball y e \<subseteq> s"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   704
    using assms [unfolded open_contains_ball] by auto
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   705
  show "\<exists>e>0. ball y e \<subseteq> s - {y. path_component s x y}"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   706
    apply (rule_tac x=e in exI)
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   707
    apply (rule, rule `e>0`, rule, rule) defer
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   708
  proof (rule ccontr)
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   709
    fix z
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   710
    assume "z \<in> ball y e" "\<not> z \<notin> {y. path_component s x y}"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   711
    hence "y \<in> {y. path_component s x y}"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   712
      unfolding not_not mem_Collect_eq using `e>0`
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   713
      apply -
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   714
      apply (rule path_component_trans, assumption)
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   715
      apply (rule path_component_of_subset[OF e(2)])
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   716
      apply (rule convex_imp_path_connected[OF convex_ball, unfolded path_connected_component, rule_format])
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   717
      apply auto
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   718
      done
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   719
    thus False using as by auto
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   720
  qed (insert e(2), auto)
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   721
qed
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   722
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   723
lemma connected_open_path_connected:
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   724
  fixes s :: "'a::real_normed_vector set" (*TODO: generalize to metric_space*)
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   725
  assumes "open s" "connected s"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   726
  shows "path_connected s"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   727
  unfolding path_connected_component_set
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   728
proof (rule, rule, rule path_component_subset, rule)
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   729
  fix x y
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   730
  assume "x \<in> s" "y \<in> s"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   731
  show "y \<in> {y. path_component s x y}"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   732
  proof (rule ccontr)
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   733
    assume "y \<notin> {y. path_component s x y}"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   734
    moreover
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   735
    have "{y. path_component s x y} \<inter> s \<noteq> {}"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   736
      using `x\<in>s` path_component_eq_empty path_component_subset[of s x] by auto
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   737
    ultimately
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   738
    show False
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   739
      using `y\<in>s` open_non_path_component[OF assms(1)] open_path_component[OF assms(1)]
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   740
      using assms(2)[unfolded connected_def not_ex, rule_format, of"{y. path_component s x y}" "s - {y. path_component s x y}"]
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   741
      by auto
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   742
  qed
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   743
qed
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   744
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   745
lemma path_connected_continuous_image:
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   746
  assumes "continuous_on s f" "path_connected s"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   747
  shows "path_connected (f ` s)"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   748
  unfolding path_connected_def
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   749
proof (rule, rule)
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   750
  fix x' y'
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   751
  assume "x' \<in> f ` s" "y' \<in> f ` s"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   752
  then obtain x y where xy: "x\<in>s" "y\<in>s" "x' = f x" "y' = f y" by auto
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   753
  guess g using assms(2)[unfolded path_connected_def, rule_format, OF xy(1,2)] ..
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   754
  thus "\<exists>g. path g \<and> path_image g \<subseteq> f ` s \<and> pathstart g = x' \<and> pathfinish g = y'"
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   755
    unfolding xy
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   756
    apply (rule_tac x="f \<circ> g" in exI)
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   757
    unfolding path_defs
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   758
    using assms(1)
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   759
    apply (auto intro!: continuous_on_compose continuous_on_subset[of _ _ "g ` {0..1}"])
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   760
    done
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   761
qed
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   762
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   763
lemma homeomorphic_path_connectedness:
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   764
  "s homeomorphic t \<Longrightarrow> (path_connected s \<longleftrightarrow> path_connected t)"
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   765
  unfolding homeomorphic_def homeomorphism_def
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   766
  apply (erule exE|erule conjE)+  
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   767
  apply rule
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   768
  apply (drule_tac f=f in path_connected_continuous_image) prefer 3
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   769
  apply (drule_tac f=g in path_connected_continuous_image)
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   770
  apply auto
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   771
  done
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   772
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   773
lemma path_connected_empty: "path_connected {}"
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   774
  unfolding path_connected_def by auto
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   775
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   776
lemma path_connected_singleton: "path_connected {a}"
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   777
  unfolding path_connected_def pathstart_def pathfinish_def path_image_def
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   778
  apply (clarify, rule_tac x="\<lambda>x. a" in exI, simp add: image_constant_conv)
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   779
  apply (simp add: path_def continuous_on_const)
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   780
  done
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   781
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   782
lemma path_connected_Un:
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   783
  assumes "path_connected s" "path_connected t" "s \<inter> t \<noteq> {}"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   784
  shows "path_connected (s \<union> t)"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   785
  unfolding path_connected_component
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   786
proof (rule, rule)
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   787
  fix x y
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   788
  assume as: "x \<in> s \<union> t" "y \<in> s \<union> t"
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   789
  from assms(3) obtain z where "z \<in> s \<inter> t" by auto
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   790
  thus "path_component (s \<union> t) x y"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   791
    using as and assms(1-2)[unfolded path_connected_component]
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   792
    apply - 
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   793
    apply (erule_tac[!] UnE)+
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   794
    apply (rule_tac[2-3] path_component_trans[of _ _ z])
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   795
    apply (auto simp add:path_component_of_subset [OF Un_upper1] path_component_of_subset[OF Un_upper2])
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   796
    done
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   797
qed
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   798
37674
f86de9c00c47 convert theorem path_connected_sphere to euclidean_space class
huffman
parents: 37489
diff changeset
   799
lemma path_connected_UNION:
f86de9c00c47 convert theorem path_connected_sphere to euclidean_space class
huffman
parents: 37489
diff changeset
   800
  assumes "\<And>i. i \<in> A \<Longrightarrow> path_connected (S i)"
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   801
    and "\<And>i. i \<in> A \<Longrightarrow> z \<in> S i"
37674
f86de9c00c47 convert theorem path_connected_sphere to euclidean_space class
huffman
parents: 37489
diff changeset
   802
  shows "path_connected (\<Union>i\<in>A. S i)"
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   803
  unfolding path_connected_component
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   804
proof clarify
37674
f86de9c00c47 convert theorem path_connected_sphere to euclidean_space class
huffman
parents: 37489
diff changeset
   805
  fix x i y j
f86de9c00c47 convert theorem path_connected_sphere to euclidean_space class
huffman
parents: 37489
diff changeset
   806
  assume *: "i \<in> A" "x \<in> S i" "j \<in> A" "y \<in> S j"
f86de9c00c47 convert theorem path_connected_sphere to euclidean_space class
huffman
parents: 37489
diff changeset
   807
  hence "path_component (S i) x z" and "path_component (S j) z y"
f86de9c00c47 convert theorem path_connected_sphere to euclidean_space class
huffman
parents: 37489
diff changeset
   808
    using assms by (simp_all add: path_connected_component)
f86de9c00c47 convert theorem path_connected_sphere to euclidean_space class
huffman
parents: 37489
diff changeset
   809
  hence "path_component (\<Union>i\<in>A. S i) x z" and "path_component (\<Union>i\<in>A. S i) z y"
48125
602dc0215954 tuned proofs -- prefer direct "rotated" instead of old-style COMP;
wenzelm
parents: 44647
diff changeset
   810
    using *(1,3) by (auto elim!: path_component_of_subset [rotated])
37674
f86de9c00c47 convert theorem path_connected_sphere to euclidean_space class
huffman
parents: 37489
diff changeset
   811
  thus "path_component (\<Union>i\<in>A. S i) x y"
f86de9c00c47 convert theorem path_connected_sphere to euclidean_space class
huffman
parents: 37489
diff changeset
   812
    by (rule path_component_trans)
f86de9c00c47 convert theorem path_connected_sphere to euclidean_space class
huffman
parents: 37489
diff changeset
   813
qed
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   814
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   815
37674
f86de9c00c47 convert theorem path_connected_sphere to euclidean_space class
huffman
parents: 37489
diff changeset
   816
subsection {* sphere is path-connected. *}
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36583
diff changeset
   817
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   818
lemma path_connected_punctured_universe:
37674
f86de9c00c47 convert theorem path_connected_sphere to euclidean_space class
huffman
parents: 37489
diff changeset
   819
  assumes "2 \<le> DIM('a::euclidean_space)"
f86de9c00c47 convert theorem path_connected_sphere to euclidean_space class
huffman
parents: 37489
diff changeset
   820
  shows "path_connected((UNIV::'a::euclidean_space set) - {a})"
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   821
proof -
37674
f86de9c00c47 convert theorem path_connected_sphere to euclidean_space class
huffman
parents: 37489
diff changeset
   822
  let ?A = "{x::'a. \<exists>i\<in>{..<DIM('a)}. x $$ i < a $$ i}"
f86de9c00c47 convert theorem path_connected_sphere to euclidean_space class
huffman
parents: 37489
diff changeset
   823
  let ?B = "{x::'a. \<exists>i\<in>{..<DIM('a)}. a $$ i < x $$ i}"
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   824
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   825
  have A: "path_connected ?A"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   826
    unfolding Collect_bex_eq
37674
f86de9c00c47 convert theorem path_connected_sphere to euclidean_space class
huffman
parents: 37489
diff changeset
   827
  proof (rule path_connected_UNION)
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   828
    fix i
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   829
    assume "i \<in> {..<DIM('a)}"
37674
f86de9c00c47 convert theorem path_connected_sphere to euclidean_space class
huffman
parents: 37489
diff changeset
   830
    thus "(\<chi>\<chi> i. a $$ i - 1) \<in> {x::'a. x $$ i < a $$ i}" by simp
f86de9c00c47 convert theorem path_connected_sphere to euclidean_space class
huffman
parents: 37489
diff changeset
   831
    show "path_connected {x. x $$ i < a $$ i}" unfolding euclidean_component_def
f86de9c00c47 convert theorem path_connected_sphere to euclidean_space class
huffman
parents: 37489
diff changeset
   832
      by (rule convex_imp_path_connected [OF convex_halfspace_lt])
f86de9c00c47 convert theorem path_connected_sphere to euclidean_space class
huffman
parents: 37489
diff changeset
   833
  qed
f86de9c00c47 convert theorem path_connected_sphere to euclidean_space class
huffman
parents: 37489
diff changeset
   834
  have B: "path_connected ?B" unfolding Collect_bex_eq
f86de9c00c47 convert theorem path_connected_sphere to euclidean_space class
huffman
parents: 37489
diff changeset
   835
  proof (rule path_connected_UNION)
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   836
    fix i
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   837
    assume "i \<in> {..<DIM('a)}"
37674
f86de9c00c47 convert theorem path_connected_sphere to euclidean_space class
huffman
parents: 37489
diff changeset
   838
    thus "(\<chi>\<chi> i. a $$ i + 1) \<in> {x::'a. a $$ i < x $$ i}" by simp
f86de9c00c47 convert theorem path_connected_sphere to euclidean_space class
huffman
parents: 37489
diff changeset
   839
    show "path_connected {x. a $$ i < x $$ i}" unfolding euclidean_component_def
f86de9c00c47 convert theorem path_connected_sphere to euclidean_space class
huffman
parents: 37489
diff changeset
   840
      by (rule convex_imp_path_connected [OF convex_halfspace_gt])
f86de9c00c47 convert theorem path_connected_sphere to euclidean_space class
huffman
parents: 37489
diff changeset
   841
  qed
f86de9c00c47 convert theorem path_connected_sphere to euclidean_space class
huffman
parents: 37489
diff changeset
   842
  from assms have "1 < DIM('a)" by auto
f86de9c00c47 convert theorem path_connected_sphere to euclidean_space class
huffman
parents: 37489
diff changeset
   843
  hence "a + basis 0 - basis 1 \<in> ?A \<inter> ?B" by auto
f86de9c00c47 convert theorem path_connected_sphere to euclidean_space class
huffman
parents: 37489
diff changeset
   844
  hence "?A \<inter> ?B \<noteq> {}" by fast
f86de9c00c47 convert theorem path_connected_sphere to euclidean_space class
huffman
parents: 37489
diff changeset
   845
  with A B have "path_connected (?A \<union> ?B)"
f86de9c00c47 convert theorem path_connected_sphere to euclidean_space class
huffman
parents: 37489
diff changeset
   846
    by (rule path_connected_Un)
f86de9c00c47 convert theorem path_connected_sphere to euclidean_space class
huffman
parents: 37489
diff changeset
   847
  also have "?A \<union> ?B = {x. \<exists>i\<in>{..<DIM('a)}. x $$ i \<noteq> a $$ i}"
f86de9c00c47 convert theorem path_connected_sphere to euclidean_space class
huffman
parents: 37489
diff changeset
   848
    unfolding neq_iff bex_disj_distrib Collect_disj_eq ..
f86de9c00c47 convert theorem path_connected_sphere to euclidean_space class
huffman
parents: 37489
diff changeset
   849
  also have "\<dots> = {x. x \<noteq> a}"
f86de9c00c47 convert theorem path_connected_sphere to euclidean_space class
huffman
parents: 37489
diff changeset
   850
    unfolding Bex_def euclidean_eq [where 'a='a] by simp
f86de9c00c47 convert theorem path_connected_sphere to euclidean_space class
huffman
parents: 37489
diff changeset
   851
  also have "\<dots> = UNIV - {a}" by auto
f86de9c00c47 convert theorem path_connected_sphere to euclidean_space class
huffman
parents: 37489
diff changeset
   852
  finally show ?thesis .
f86de9c00c47 convert theorem path_connected_sphere to euclidean_space class
huffman
parents: 37489
diff changeset
   853
qed
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   854
37674
f86de9c00c47 convert theorem path_connected_sphere to euclidean_space class
huffman
parents: 37489
diff changeset
   855
lemma path_connected_sphere:
f86de9c00c47 convert theorem path_connected_sphere to euclidean_space class
huffman
parents: 37489
diff changeset
   856
  assumes "2 \<le> DIM('a::euclidean_space)"
f86de9c00c47 convert theorem path_connected_sphere to euclidean_space class
huffman
parents: 37489
diff changeset
   857
  shows "path_connected {x::'a::euclidean_space. norm(x - a) = r}"
f86de9c00c47 convert theorem path_connected_sphere to euclidean_space class
huffman
parents: 37489
diff changeset
   858
proof (rule linorder_cases [of r 0])
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   859
  assume "r < 0"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   860
  hence "{x::'a. norm(x - a) = r} = {}" by auto
37674
f86de9c00c47 convert theorem path_connected_sphere to euclidean_space class
huffman
parents: 37489
diff changeset
   861
  thus ?thesis using path_connected_empty by simp
f86de9c00c47 convert theorem path_connected_sphere to euclidean_space class
huffman
parents: 37489
diff changeset
   862
next
f86de9c00c47 convert theorem path_connected_sphere to euclidean_space class
huffman
parents: 37489
diff changeset
   863
  assume "r = 0"
f86de9c00c47 convert theorem path_connected_sphere to euclidean_space class
huffman
parents: 37489
diff changeset
   864
  thus ?thesis using path_connected_singleton by simp
f86de9c00c47 convert theorem path_connected_sphere to euclidean_space class
huffman
parents: 37489
diff changeset
   865
next
f86de9c00c47 convert theorem path_connected_sphere to euclidean_space class
huffman
parents: 37489
diff changeset
   866
  assume r: "0 < r"
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   867
  hence *: "{x::'a. norm(x - a) = r} = (\<lambda>x. a + r *\<^sub>R x) ` {x. norm x = 1}"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   868
    apply -
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   869
    apply (rule set_eqI, rule)
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   870
    unfolding image_iff
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   871
    apply (rule_tac x="(1/r) *\<^sub>R (x - a)" in bexI)
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   872
    unfolding mem_Collect_eq norm_scaleR
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   873
    apply (auto simp add: scaleR_right_diff_distrib)
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   874
    done
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   875
  have **: "{x::'a. norm x = 1} = (\<lambda>x. (1/norm x) *\<^sub>R x) ` (UNIV - {0})"
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   876
    apply (rule set_eqI,rule)
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   877
    unfolding image_iff
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   878
    apply (rule_tac x=x in bexI)
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   879
    unfolding mem_Collect_eq
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   880
    apply (auto split:split_if_asm)
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   881
    done
44647
e4de7750cdeb modernize lemmas about 'continuous' and 'continuous_on';
huffman
parents: 44531
diff changeset
   882
  have "continuous_on (UNIV - {0}) (\<lambda>x::'a. 1 / norm x)"
e4de7750cdeb modernize lemmas about 'continuous' and 'continuous_on';
huffman
parents: 44531
diff changeset
   883
    unfolding field_divide_inverse by (simp add: continuous_on_intros)
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   884
  thus ?thesis unfolding * ** using path_connected_punctured_universe[OF assms]
49653
03bc7afe8814 tuned proofs;
wenzelm
parents: 48125
diff changeset
   885
    by (auto intro!: path_connected_continuous_image continuous_on_intros)
37674
f86de9c00c47 convert theorem path_connected_sphere to euclidean_space class
huffman
parents: 37489
diff changeset
   886
qed
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   887
37674
f86de9c00c47 convert theorem path_connected_sphere to euclidean_space class
huffman
parents: 37489
diff changeset
   888
lemma connected_sphere: "2 \<le> DIM('a::euclidean_space) \<Longrightarrow> connected {x::'a. norm(x - a) = r}"
36583
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   889
  using path_connected_sphere path_connected_imp_connected by auto
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   890
68ce5760c585 move path-related stuff into new theory file
huffman
parents:
diff changeset
   891
end