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: