# HG changeset patch
# User huffman
# Date 1159399588 -7200
# Node ID 09cf0e407a455f7d1a1e7be07b7830f2379330e7
# Parent  93271c59d211f94e8a3c3e0f03629b208cdd3a2b
generalize type of is(NS)UCont

diff -r 93271c59d211 -r 09cf0e407a45 src/HOL/Complex/CLim.thy
--- a/src/HOL/Complex/CLim.thy	Thu Sep 28 00:57:36 2006 +0200
+++ b/src/HOL/Complex/CLim.thy	Thu Sep 28 01:26:28 2006 +0200
@@ -67,6 +67,12 @@
   isNSContCR :: "[complex=>real,complex] => bool"
   "isNSContCR == isNSCont"
 
+  isUContc :: "(complex=>complex) => bool"
+  "isUContc == isUCont"
+
+  isNSUContc :: "(complex=>complex) => bool"
+  "isNSUContc == isNSUCont"
+
 
 lemma CLIM_def:
   "f -- a --C> L =
@@ -112,6 +118,17 @@
 			   ( *f* f) y @= hypreal_of_real (f a))"
 by (rule isNSCont_def)
 
+lemma isUContc_def:
+  "isUContc f =  (\<forall>r. 0 < r -->
+		      (\<exists>s. 0 < s & (\<forall>x y. cmod(x - y) < s
+			    --> cmod(f x - f y) < r)))"
+by (rule isUCont_def)
+
+lemma isNSUContc_def:
+  "isNSUContc f = (\<forall>x y. x @= y --> ( *f* f) x @= ( *f* f) y)"
+by (rule isNSUCont_def)
+
+
 definition
 
   (* differentiation: D is derivative of function f at x *)
@@ -134,16 +151,6 @@
   "f NSCdifferentiable x = (\<exists>D. NSCDERIV f x :> D)"
 
 
-  isUContc :: "(complex=>complex) => bool"
-  "isUContc f =  (\<forall>r. 0 < r -->
-		      (\<exists>s. 0 < s & (\<forall>x y. cmod(x - y) < s
-			    --> cmod(f x - f y) < r)))"
-
-  isNSUContc :: "(complex=>complex) => bool"
-  "isNSUContc f = (\<forall>x y. x @= y --> ( *f* f) x @= ( *f* f) y)"
-
-
-
 subsection{*Limit of Complex to Complex Function*}
 
 lemma NSCLIM_NSCRLIM_Re: "f -- a --NSC> L ==> (%x. Re(f x)) -- a --NSCR> Re(L)"
diff -r 93271c59d211 -r 09cf0e407a45 src/HOL/Hyperreal/Lim.thy
--- a/src/HOL/Hyperreal/Lim.thy	Thu Sep 28 00:57:36 2006 +0200
+++ b/src/HOL/Hyperreal/Lim.thy	Thu Sep 28 01:26:28 2006 +0200
@@ -56,10 +56,10 @@
   "increment f x h = (@inc. f NSdifferentiable x &
            inc = ( *f* f)(hypreal_of_real x + h) - hypreal_of_real (f x))"
 
-  isUCont :: "(real=>real) => bool"
-  "isUCont f =  (\<forall>r > 0. \<exists>s > 0. \<forall>x y. \<bar>x - y\<bar> < s --> \<bar>f x - f y\<bar> < r)"
+  isUCont :: "['a::real_normed_vector => 'b::real_normed_vector] => bool"
+  "isUCont f = (\<forall>r>0. \<exists>s>0. \<forall>x y. norm (x - y) < s \<longrightarrow> norm (f x - f y) < r)"
 
-  isNSUCont :: "(real=>real) => bool"
+  isNSUCont :: "['a::real_normed_vector => 'b::real_normed_vector] => bool"
   "isNSUCont f = (\<forall>x y. x @= y --> ( *f* f) x @= ( *f* f) y)"
 
 
@@ -608,32 +608,32 @@
 apply (rename_tac Xa Xb u)
 apply (drule_tac x = u in spec, clarify)
 apply (drule_tac x = s in spec, clarify)
-apply (subgoal_tac "\<forall>n::nat. abs ((Xa n) - (Xb n)) < s --> abs (f (Xa n) - f (Xb n)) < u")
+apply (subgoal_tac "\<forall>n::nat. norm ((Xa n) - (Xb n)) < s --> norm (f (Xa n) - f (Xb n)) < u")
 prefer 2 apply blast
-apply (erule_tac V = "\<forall>x y. \<bar>x - y\<bar> < s --> \<bar>f x - f y\<bar> < u" in thin_rl)
+apply (erule_tac V = "\<forall>x y. norm (x - y) < s --> norm (f x - f y) < u" in thin_rl)
 apply (erule ultra, simp)
 done
 
-lemma lemma_LIMu: "\<forall>s>0.\<exists>z y. \<bar>z - y\<bar> < s & r \<le> \<bar>f z - f y\<bar>
-      ==> \<forall>n::nat. \<exists>z y. \<bar>z - y\<bar> < inverse(real(Suc n)) & r \<le> \<bar>f z - f y\<bar>"
+lemma lemma_LIMu: "\<forall>s>0.\<exists>z y. norm (z - y) < s & r \<le> norm (f z - f y)
+      ==> \<forall>n::nat. \<exists>z y. norm (z - y) < inverse(real(Suc n)) & r \<le> norm (f z - f y)"
 apply clarify
 apply (cut_tac n1 = n
        in real_of_nat_Suc_gt_zero [THEN positive_imp_inverse_positive], auto)
 done
 
 lemma lemma_skolemize_LIM2u:
-     "\<forall>s>0.\<exists>z y. \<bar>z - y\<bar> < s  & r \<le> \<bar>f z - f y\<bar>
+     "\<forall>s>0.\<exists>z y. norm (z - y) < s  & r \<le> norm (f z - f y)
       ==> \<exists>X Y. \<forall>n::nat.
-               abs(X n - Y n) < inverse(real(Suc n)) &
-               r \<le> abs(f (X n) - f (Y n))"
+               norm (X n - Y n) < inverse(real(Suc n)) &
+               r \<le> norm (f (X n) - f (Y n))"
 apply (drule lemma_LIMu)
 apply (drule choice, safe)
 apply (drule choice, blast)
 done
 
-lemma lemma_simpu: "\<forall>n. \<bar>X n - Y n\<bar> < inverse (real(Suc n)) &
-          r \<le> abs (f (X n) - f(Y n)) ==>
-          \<forall>n. \<bar>X n - Y n\<bar> < inverse (real(Suc n))"
+lemma lemma_simpu: "\<forall>n. norm (X n - Y n) < inverse (real(Suc n)) &
+          r \<le> norm (f (X n) - f(Y n)) ==>
+          \<forall>n. norm (X n - Y n) < inverse (real(Suc n))"
 by auto
 
 lemma isNSUCont_isUCont: