# HG changeset patch
# User huffman
# Date 1272391384 25200
# Node ID e62e32e163a49d7304ebb7a29c12082d9d6a9778
# Parent  b96d9dc6accaee08df9dac0c251b9c5ed4a789be
generalize types of path operations

diff -r b96d9dc6acca -r e62e32e163a4 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Tue Apr 27 10:54:24 2010 -0700
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Tue Apr 27 11:03:04 2010 -0700
@@ -2817,41 +2817,38 @@
 
 subsection {* Paths. *}
 
-text {* TODO: Once @{const continuous_on} is generalized to arbitrary
-topological spaces, all of these concepts should be similarly generalized. *}
-
 definition
-  path :: "(real \<Rightarrow> 'a::metric_space) \<Rightarrow> bool"
+  path :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> bool"
   where "path g \<longleftrightarrow> continuous_on {0 .. 1} g"
 
 definition
-  pathstart :: "(real \<Rightarrow> 'a::metric_space) \<Rightarrow> 'a"
+  pathstart :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> 'a"
   where "pathstart g = g 0"
 
 definition
-  pathfinish :: "(real \<Rightarrow> 'a::metric_space) \<Rightarrow> 'a"
+  pathfinish :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> 'a"
   where "pathfinish g = g 1"
 
 definition
-  path_image :: "(real \<Rightarrow> 'a::metric_space) \<Rightarrow> 'a set"
+  path_image :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> 'a set"
   where "path_image g = g ` {0 .. 1}"
 
 definition
-  reversepath :: "(real \<Rightarrow> 'a::metric_space) \<Rightarrow> (real \<Rightarrow> 'a)"
+  reversepath :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> (real \<Rightarrow> 'a)"
   where "reversepath g = (\<lambda>x. g(1 - x))"
 
 definition
-  joinpaths :: "(real \<Rightarrow> 'a::metric_space) \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> (real \<Rightarrow> 'a)"
+  joinpaths :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> (real \<Rightarrow> 'a)"
     (infixr "+++" 75)
   where "g1 +++ g2 = (\<lambda>x. if x \<le> 1/2 then g1 (2 * x) else g2 (2 * x - 1))"
 
 definition
-  simple_path :: "(real \<Rightarrow> 'a::metric_space) \<Rightarrow> bool"
+  simple_path :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> bool"
   where "simple_path g \<longleftrightarrow>
   (\<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)"
 
 definition
-  injective_path :: "(real \<Rightarrow> 'a::metric_space) \<Rightarrow> bool"
+  injective_path :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> bool"
   where "injective_path g \<longleftrightarrow> (\<forall>x\<in>{0..1}. \<forall>y\<in>{0..1}. g x = g y \<longrightarrow> x = y)"
 
 subsection {* Some lemmas about these concepts. *}
@@ -3059,7 +3056,7 @@
  
 subsection {* Reparametrizing a closed curve to start at some chosen point. *}
 
-definition "shiftpath a (f::real \<Rightarrow> 'a::metric_space) =
+definition "shiftpath a (f::real \<Rightarrow> 'a::topological_space) =
   (\<lambda>x. if (a + x) \<le> 1 then f(a + x) else f(a + x - 1))"
 
 lemma pathstart_shiftpath: "a \<le> 1 \<Longrightarrow> pathstart(shiftpath a g) = g a"