# HG changeset patch
# User huffman
# Date 1244007356 25200
# Node ID e37967787a4feaf76c88b3c32a28aef4f808b282
# Parent  2da6a7684e66b3eb9a0c04c6f802eedc6253c266
generalize constant uniformly_continuous_on

diff -r 2da6a7684e66 -r e37967787a4f src/HOL/Library/Topology_Euclidean_Space.thy
--- a/src/HOL/Library/Topology_Euclidean_Space.thy	Tue Jun 02 22:09:50 2009 -0700
+++ b/src/HOL/Library/Topology_Euclidean_Space.thy	Tue Jun 02 22:35:56 2009 -0700
@@ -3066,7 +3066,7 @@
 
 definition
   uniformly_continuous_on ::
-    "(real ^ 'n::finite) set \<Rightarrow> (real ^ 'n \<Rightarrow> real ^ 'm::finite) \<Rightarrow> bool" where
+    "'a::metric_space set \<Rightarrow> ('a \<Rightarrow> 'b::metric_space) \<Rightarrow> bool" where
   "uniformly_continuous_on s f \<longleftrightarrow>
         (\<forall>e>0. \<exists>d>0. \<forall>x\<in>s. \<forall> x'\<in>s. dist x' x < d
                            --> dist (f x') (f x) < e)"
@@ -3198,7 +3198,8 @@
 qed
 
 lemma uniformly_continuous_on_sequentially:
- "uniformly_continuous_on s f \<longleftrightarrow> (\<forall>x y. (\<forall>n. x n \<in> s) \<and> (\<forall>n. y n \<in> s) \<and>
+  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
+  shows "uniformly_continuous_on s f \<longleftrightarrow> (\<forall>x y. (\<forall>n. x n \<in> s) \<and> (\<forall>n. y n \<in> s) \<and>
                     ((\<lambda>n. x n - y n) ---> 0) sequentially
                     \<longrightarrow> ((\<lambda>n. f(x n) - f(y n)) ---> 0) sequentially)" (is "?lhs = ?rhs")
 proof
@@ -3226,24 +3227,25 @@
     def y \<equiv> "\<lambda>n::nat. snd (fa (inverse (real n + 1)))"
     have xyn:"\<forall>n. x n \<in> s \<and> y n \<in> s" and xy0:"\<forall>n. dist (x n) (y n) < inverse (real n + 1)" and fxy:"\<forall>n. \<not> dist (f (x n)) (f (y n)) < e"
       unfolding x_def and y_def using fa by auto
-    have *:"\<And>x (y::real^_). dist (x - y) 0 = dist x y" unfolding dist_norm by auto
+    have 1:"\<And>(x::'a) y. dist (x - y) 0 = dist x y" unfolding dist_norm by auto
+    have 2:"\<And>(x::'b) y. dist (x - y) 0 = dist x y" unfolding dist_norm by auto
     { fix e::real assume "e>0"
       then obtain N::nat where "N \<noteq> 0" and N:"0 < inverse (real N) \<and> inverse (real N) < e" unfolding real_arch_inv[of e]   by auto
       { fix n::nat assume "n\<ge>N"
 	hence "inverse (real n + 1) < inverse (real N)" using real_of_nat_ge_zero and `N\<noteq>0` by auto
 	also have "\<dots> < e" using N by auto
 	finally have "inverse (real n + 1) < e" by auto
-	hence "dist (x n - y n) 0 < e" unfolding * using xy0[THEN spec[where x=n]] by auto  }
+	hence "dist (x n - y n) 0 < e" unfolding 1 using xy0[THEN spec[where x=n]] by auto  }
       hence "\<exists>N. \<forall>n\<ge>N. dist (x n - y n) 0 < e" by auto  }
     hence "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. dist (f (x n) - f (y n)) 0 < e" using `?rhs`[THEN spec[where x=x], THEN spec[where x=y]] and xyn unfolding Lim_sequentially by auto
-    hence False unfolding * using fxy and `e>0` by auto  }
+    hence False unfolding 2 using fxy and `e>0` by auto  }
   thus ?lhs unfolding uniformly_continuous_on_def by blast
 qed
 
 text{* The usual transformation theorems. *}
 
 lemma continuous_transform_within:
-  fixes f g :: "real ^ 'n::finite \<Rightarrow> 'b::real_normed_vector"
+  fixes f g :: "'a::metric_space \<Rightarrow> 'b::metric_space"
   assumes "0 < d" "x \<in> s" "\<forall>x' \<in> s. dist x' x < d --> f x' = g x'"
           "continuous (at x within s) f"
   shows "continuous (at x within s) g"
@@ -3259,7 +3261,7 @@
 qed
 
 lemma continuous_transform_at:
-  fixes f g :: "real ^ 'n::finite \<Rightarrow> 'b::real_normed_vector"
+  fixes f g :: "'a::metric_space \<Rightarrow> 'b::metric_space"
   assumes "0 < d" "\<forall>x'. dist x' x < d --> f x' = g x'"
           "continuous (at x) f"
   shows "continuous (at x) g"
@@ -3333,9 +3335,10 @@
 
 lemma uniformly_continuous_on_const:
  "uniformly_continuous_on s (\<lambda>x. c)"
-  unfolding uniformly_continuous_on_sequentially using Lim_const[of 0] by auto
+  unfolding uniformly_continuous_on_def by simp
 
 lemma uniformly_continuous_on_cmul:
+  fixes f :: "'a::real_normed_vector \<Rightarrow> real ^ _"
   assumes "uniformly_continuous_on s f"
   shows "uniformly_continuous_on s (\<lambda>x. c *s f(x))"
 proof-
@@ -3348,25 +3351,27 @@
 qed
 
 lemma uniformly_continuous_on_neg:
- "uniformly_continuous_on s f
+  fixes f :: "'a::real_normed_vector \<Rightarrow> real ^ _" (* FIXME: generalize *)
+  shows "uniformly_continuous_on s f
          ==> uniformly_continuous_on s (\<lambda>x. -(f x))"
   using uniformly_continuous_on_cmul[of s f "-1"] unfolding pth_3 by auto
 
 lemma uniformly_continuous_on_add:
+  fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
   assumes "uniformly_continuous_on s f" "uniformly_continuous_on s g"
-  shows "uniformly_continuous_on s (\<lambda>x. f(x) + g(x) ::real^'n::finite)"
+  shows "uniformly_continuous_on s (\<lambda>x. f x + g x)"
 proof-
-  have *:"\<And>fx fy gx gy::real^'n. fx - fy + (gx - gy) = fx + gx - (fy + gy)" by auto
   {  fix x y assume "((\<lambda>n. f (x n) - f (y n)) ---> 0) sequentially"
                     "((\<lambda>n. g (x n) - g (y n)) ---> 0) sequentially"
     hence "((\<lambda>xa. f (x xa) - f (y xa) + (g (x xa) - g (y xa))) ---> 0 + 0) sequentially"
       using Lim_add[of "\<lambda> n. f (x n) - f (y n)" 0  sequentially "\<lambda> n. g (x n) - g (y n)" 0] by auto
-    hence "((\<lambda>n. f (x n) + g (x n) - (f (y n) + g (y n))) ---> 0) sequentially" unfolding Lim_sequentially and * by auto  }
+    hence "((\<lambda>n. f (x n) + g (x n) - (f (y n) + g (y n))) ---> 0) sequentially" unfolding Lim_sequentially and add_diff_add [symmetric] by auto  }
   thus ?thesis using assms unfolding uniformly_continuous_on_sequentially by auto
 qed
 
 lemma uniformly_continuous_on_sub:
- "uniformly_continuous_on s f \<Longrightarrow> uniformly_continuous_on s g
+  fixes f :: "'a::real_normed_vector \<Rightarrow> real ^ _" (* FIXME: generalize *)
+  shows "uniformly_continuous_on s f \<Longrightarrow> uniformly_continuous_on s g
            ==> uniformly_continuous_on s  (\<lambda>x. f x - g x)"
   unfolding ab_diff_minus
   using uniformly_continuous_on_add[of s f "\<lambda>x. - g x"]