--- 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)"
--- 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: