# HG changeset patch
# User huffman
# Date 1158367200 -7200
# Node ID 2c31dd358c2109d6c62f5cd1c28adaca949c7eca
# Parent  ba543692bfa1aaa383c25e0f6ed03da4dcdd9166
generalized types of many constants to work over arbitrary vector spaces;
modified theorems using Rep_star to eliminate existential quantifiers

diff -r ba543692bfa1 -r 2c31dd358c21 src/HOL/Complex/CLim.thy
--- a/src/HOL/Complex/CLim.thy	Sat Sep 16 02:35:58 2006 +0200
+++ b/src/HOL/Complex/CLim.thy	Sat Sep 16 02:40:00 2006 +0200
@@ -126,10 +126,9 @@
 apply (rule_tac x = xa in star_cases)
 apply (auto simp add: starfun star_n_diff star_of_def star_n_eq_iff
          CInfinitesimal_hcmod_iff hcmod Infinitesimal_FreeUltrafilterNat_iff)
-apply (rule bexI [OF _ Rep_star_star_n], safe)
 apply (drule_tac x = u in spec, auto)
 apply (drule_tac x = s in spec, auto, ultra)
-apply (drule sym, auto)
+apply (auto)
 done
 
 lemma eq_Abs_star_ALL: "(\<forall>t. P t) = (\<forall>X. P (star_n X))"
@@ -176,7 +175,7 @@
 apply (drule_tac x = X in spec, auto)
 apply (drule lemma_csimp [THEN complex_seq_to_hcomplex_CInfinitesimal])
 apply (simp add: CInfinitesimal_hcmod_iff star_of_def
-            Infinitesimal_FreeUltrafilterNat_iff star_n_diff hcmod,  blast)
+            Infinitesimal_FreeUltrafilterNat_iff star_n_diff hcmod)
 apply (drule_tac x = r in spec, clarify)
 apply (drule FreeUltrafilterNat_all, ultra)
 done
@@ -197,10 +196,9 @@
               Infinitesimal_FreeUltrafilterNat_iff
               star_of_def star_n_eq_iff
               Infinitesimal_approx_minus [symmetric])
-apply (rule bexI [OF _ Rep_star_star_n], safe)
 apply (drule_tac x = u in spec, auto)
 apply (drule_tac x = s in spec, auto, ultra)
-apply (drule sym, auto)
+apply (auto)
 done
 
 lemma lemma_CRLIM:
@@ -242,7 +240,6 @@
 apply (drule lemma_crsimp [THEN complex_seq_to_hcomplex_CInfinitesimal])
 apply (simp add: CInfinitesimal_hcmod_iff star_of_def
              Infinitesimal_FreeUltrafilterNat_iff star_n_diff hcmod)
-apply (auto simp add: star_of_def star_n_diff)
 apply (drule_tac x = r in spec, clarify)
 apply (drule FreeUltrafilterNat_all, ultra)
 done
diff -r ba543692bfa1 -r 2c31dd358c21 src/HOL/Complex/NSCA.thy
--- a/src/HOL/Complex/NSCA.thy	Sat Sep 16 02:35:58 2006 +0200
+++ b/src/HOL/Complex/NSCA.thy	Sat Sep 16 02:40:00 2006 +0200
@@ -656,35 +656,32 @@
 lemma hcomplex_capproxD1:
      "star_n X @c= star_n Y
       ==> star_n (%n. Re(X n)) @= star_n (%n. Re(Y n))"
-apply (auto simp add: approx_FreeUltrafilterNat_iff)
+apply (simp add: approx_FreeUltrafilterNat_iff2, safe)
 apply (drule capprox_minus_iff [THEN iffD1])
-apply (auto simp add: star_n_minus star_n_add mem_cinfmal_iff [symmetric] CInfinitesimal_hcmod_iff hcmod Infinitesimal_FreeUltrafilterNat_iff2)
-apply (drule_tac x = m in spec, ultra)
-apply (rename_tac Z x)
-apply (case_tac "X x")
-apply (case_tac "Y x")
+apply (simp add: star_n_minus star_n_add mem_cinfmal_iff [symmetric] CInfinitesimal_hcmod_iff hcmod Infinitesimal_FreeUltrafilterNat_iff2)
+apply (drule_tac x = m in spec)
+apply (erule ultra, rule FreeUltrafilterNat_all, clarify)
+apply (rule_tac y="cmod (X n + - Y n)" in order_le_less_trans)
+apply (case_tac "X n")
+apply (case_tac "Y n")
 apply (auto simp add: complex_minus complex_add complex_mod
-           simp del: realpow_Suc)
-apply (rule_tac y="abs(Z x)" in order_le_less_trans)
-apply (drule_tac t = "Z x" in sym)
-apply (auto simp del: realpow_Suc)
+            simp del: realpow_Suc)
 done
 
 (* same proof *)
 lemma hcomplex_capproxD2:
      "star_n X @c= star_n Y
       ==> star_n (%n. Im(X n)) @= star_n (%n. Im(Y n))"
-apply (auto simp add: approx_FreeUltrafilterNat_iff)
+apply (simp add: approx_FreeUltrafilterNat_iff2, safe)
 apply (drule capprox_minus_iff [THEN iffD1])
-apply (auto simp add: star_n_minus star_n_add mem_cinfmal_iff [symmetric] CInfinitesimal_hcmod_iff hcmod Infinitesimal_FreeUltrafilterNat_iff2)
-apply (drule_tac x = m in spec, ultra)
-apply (rename_tac Z x)
-apply (case_tac "X x")
-apply (case_tac "Y x")
-apply (auto simp add: complex_minus complex_add complex_mod simp del: realpow_Suc)
-apply (rule_tac y="abs(Z x)" in order_le_less_trans)
-apply (drule_tac t = "Z x" in sym)
-apply (auto simp del: realpow_Suc)
+apply (simp add: star_n_minus star_n_add mem_cinfmal_iff [symmetric] CInfinitesimal_hcmod_iff hcmod Infinitesimal_FreeUltrafilterNat_iff2)
+apply (drule_tac x = m in spec)
+apply (erule ultra, rule FreeUltrafilterNat_all, clarify)
+apply (rule_tac y="cmod (X n + - Y n)" in order_le_less_trans)
+apply (case_tac "X n")
+apply (case_tac "Y n")
+apply (auto simp add: complex_minus complex_add complex_mod
+            simp del: realpow_Suc)
 done
 
 lemma hcomplex_capproxI:
@@ -695,10 +692,8 @@
 apply (drule approx_minus_iff [THEN iffD1])
 apply (rule capprox_minus_iff [THEN iffD2])
 apply (auto simp add: mem_cinfmal_iff [symmetric] mem_infmal_iff [symmetric] star_n_add star_n_minus CInfinitesimal_hcmod_iff hcmod Infinitesimal_FreeUltrafilterNat_iff)
-apply (rule bexI [OF _ Rep_star_star_n], auto)
 apply (drule_tac x = "u/2" in spec)
 apply (drule_tac x = "u/2" in spec, auto, ultra)
-apply (drule sym, drule sym)
 apply (case_tac "X x")
 apply (case_tac "Y x")
 apply (auto simp add: complex_minus complex_add complex_mod snd_conv fst_conv numeral_2_eq_2)
@@ -725,9 +720,8 @@
      "star_n X \<in> CFinite  
       ==> star_n (%n. Re(X n)) \<in> HFinite"
 apply (auto simp add: CFinite_hcmod_iff hcmod HFinite_FreeUltrafilterNat_iff)
-apply (rule bexI [OF _ Rep_star_star_n])
 apply (rule_tac x = u in exI, ultra)
-apply (drule sym, case_tac "X x")
+apply (case_tac "X x")
 apply (auto simp add: complex_mod numeral_2_eq_2 simp del: realpow_Suc)
 apply (rule ccontr, drule linorder_not_less [THEN iffD1])
 apply (drule order_less_le_trans, assumption)
@@ -739,9 +733,8 @@
      "star_n X \<in> CFinite  
       ==> star_n (%n. Im(X n)) \<in> HFinite"
 apply (auto simp add: CFinite_hcmod_iff hcmod HFinite_FreeUltrafilterNat_iff)
-apply (rule bexI [OF _ Rep_star_star_n])
 apply (rule_tac x = u in exI, ultra)
-apply (drule sym, case_tac "X x")
+apply (case_tac "X x")
 apply (auto simp add: complex_mod simp del: realpow_Suc)
 apply (rule ccontr, drule linorder_not_less [THEN iffD1])
 apply (drule order_less_le_trans, assumption)
@@ -753,17 +746,16 @@
          star_n (%n. Im(X n)) \<in> HFinite  
       |] ==> star_n X \<in> CFinite"
 apply (auto simp add: CFinite_hcmod_iff hcmod HFinite_FreeUltrafilterNat_iff)
-apply (rename_tac Y Z u v)
-apply (rule bexI [OF _ Rep_star_star_n])
+apply (rename_tac u v)
 apply (rule_tac x = "2* (u + v) " in exI)
 apply ultra
-apply (drule sym, case_tac "X x")
+apply (case_tac "X x")
 apply (auto simp add: complex_mod numeral_2_eq_2 simp del: realpow_Suc)
 apply (subgoal_tac "0 < u")
  prefer 2 apply arith
 apply (subgoal_tac "0 < v")
  prefer 2 apply arith
-apply (subgoal_tac "sqrt (abs (Y x) ^ 2 + abs (Z x) ^ 2) < 2*u + 2*v")
+apply (subgoal_tac "sqrt (abs (Re (X x)) ^ 2 + abs (Im (X x)) ^ 2) < 2*u + 2*v")
 apply (rule_tac [2] lemma_sqrt_hcomplex_capprox, auto)
 apply (simp add: power2_eq_square)
 done
@@ -1201,7 +1193,6 @@
      "\<forall>n. cmod (X n - x) < inverse (real (Suc n)) ==>  
       star_n X - hcomplex_of_complex x \<in> CInfinitesimal"
 apply (simp add: star_n_diff CInfinitesimal_hcmod_iff star_of_def Infinitesimal_FreeUltrafilterNat_iff hcmod)
-apply (rule bexI, auto)
 apply (auto dest: FreeUltrafilterNat_inverse_real_of_posnat FreeUltrafilterNat_all FreeUltrafilterNat_Int intro: order_less_trans FreeUltrafilterNat_subset)
 done
 
diff -r ba543692bfa1 -r 2c31dd358c21 src/HOL/Hyperreal/HTranscendental.thy
--- a/src/HOL/Hyperreal/HTranscendental.thy	Sat Sep 16 02:35:58 2006 +0200
+++ b/src/HOL/Hyperreal/HTranscendental.thy	Sat Sep 16 02:40:00 2006 +0200
@@ -362,7 +362,6 @@
 lemma starfun_exp_HFinite: "x \<in> HFinite ==> ( *f* exp) x \<in> HFinite"
 apply (cases x)
 apply (auto simp add: starfun HFinite_FreeUltrafilterNat_iff)
-apply (rule bexI [OF _ Rep_star_star_n], auto)
 apply (rule_tac x = "exp u" in exI)
 apply ultra
 done
diff -r ba543692bfa1 -r 2c31dd358c21 src/HOL/Hyperreal/HyperDef.thy
--- a/src/HOL/Hyperreal/HyperDef.thy	Sat Sep 16 02:35:58 2006 +0200
+++ b/src/HOL/Hyperreal/HyperDef.thy	Sat Sep 16 02:40:00 2006 +0200
@@ -188,6 +188,9 @@
 lemma inj_hypreal_of_real: "inj(hypreal_of_real)"
 by (rule inj_onI, simp)
 
+lemma mem_Rep_star_iff: "(X \<in> Rep_star x) = (x = star_n X)"
+by (cases x, simp add: star_n_def)
+
 lemma Rep_star_star_n_iff [simp]:
   "(X \<in> Rep_star (star_n Y)) = ({n. Y n = X n} \<in> \<U>)"
 by (simp add: star_n_def)
diff -r ba543692bfa1 -r 2c31dd358c21 src/HOL/Hyperreal/HyperNat.thy
--- a/src/HOL/Hyperreal/HyperNat.thy	Sat Sep 16 02:35:58 2006 +0200
+++ b/src/HOL/Hyperreal/HyperNat.thy	Sat Sep 16 02:40:00 2006 +0200
@@ -242,27 +242,20 @@
 Free Ultrafilter*}
 
 lemma HNatInfinite_FreeUltrafilterNat:
-     "x \<in> HNatInfinite 
-      ==> \<exists>X \<in> Rep_star x. \<forall>u. {n. u < X n}:  FreeUltrafilterNat"
-apply (cases x)
-apply (auto simp add: HNatInfinite_iff SHNat_eq hypnat_of_nat_eq)
-apply (rule bexI [OF _ Rep_star_star_n], clarify) 
-apply (auto simp add: hypnat_of_nat_def star_n_less)
+     "star_n X \<in> HNatInfinite ==> \<forall>u. {n. u < X n}:  FreeUltrafilterNat"
+apply (auto simp add: HNatInfinite_iff SHNat_eq)
+apply (drule_tac x="star_of u" in spec, simp)
+apply (simp add: star_of_def star_n_less)
 done
 
 lemma FreeUltrafilterNat_HNatInfinite:
-     "\<exists>X \<in> Rep_star x. \<forall>u. {n. u < X n}:  FreeUltrafilterNat
-      ==> x \<in> HNatInfinite"
-apply (cases x)
-apply (auto simp add: star_n_less HNatInfinite_iff SHNat_eq hypnat_of_nat_eq)
-apply (drule spec, ultra, auto) 
-done
+     "\<forall>u. {n. u < X n}:  FreeUltrafilterNat ==> star_n X \<in> HNatInfinite"
+by (auto simp add: star_n_less HNatInfinite_iff SHNat_eq hypnat_of_nat_eq)
 
 lemma HNatInfinite_FreeUltrafilterNat_iff:
-     "(x \<in> HNatInfinite) = 
-      (\<exists>X \<in> Rep_star x. \<forall>u. {n. u < X n}:  FreeUltrafilterNat)"
-by (blast intro: HNatInfinite_FreeUltrafilterNat 
-                 FreeUltrafilterNat_HNatInfinite)
+     "(star_n X \<in> HNatInfinite) = (\<forall>u. {n. u < X n}:  FreeUltrafilterNat)"
+by (rule iffI [OF HNatInfinite_FreeUltrafilterNat 
+                 FreeUltrafilterNat_HNatInfinite])
 
 lemma HNatInfinite_gt_one [simp]: "x \<in> HNatInfinite ==> (1::hypnat) < x"
 by (auto simp add: HNatInfinite_iff)
@@ -370,10 +363,11 @@
 lemma HNatInfinite_inverse_Infinitesimal [simp]:
      "n \<in> HNatInfinite ==> inverse (hypreal_of_hypnat n) \<in> Infinitesimal"
 apply (cases n)
-apply (auto simp add: hypreal_of_hypnat star_n_inverse 
-      HNatInfinite_FreeUltrafilterNat_iff Infinitesimal_FreeUltrafilterNat_iff2)
-apply (rule bexI [OF _ Rep_star_star_n], auto)
-apply (drule_tac x = "m + 1" in spec, ultra)
+apply (auto simp add: hypreal_of_hypnat star_n_inverse real_norm_def
+      HNatInfinite_FreeUltrafilterNat_iff
+      Infinitesimal_FreeUltrafilterNat_iff2)
+apply (drule_tac x="Suc m" in spec)
+apply (erule ultra, simp)
 done
 
 lemma HNatInfinite_hypreal_of_hypnat_gt_zero:
diff -r ba543692bfa1 -r 2c31dd358c21 src/HOL/Hyperreal/Lim.thy
--- a/src/HOL/Hyperreal/Lim.thy	Sat Sep 16 02:35:58 2006 +0200
+++ b/src/HOL/Hyperreal/Lim.thy	Sat Sep 16 02:40:00 2006 +0200
@@ -15,25 +15,24 @@
 text{*Standard and Nonstandard Definitions*}
 
 definition
-  LIM :: "[real=>real,real,real] => bool"
+  LIM :: "[real => 'a::real_normed_vector, real, 'a] => bool"
         ("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60)
   "f -- a --> L =
      (\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & \<bar>x + -a\<bar> < s
-        --> \<bar>f x + -L\<bar> < r)"
+        --> norm (f x + -L) < r)"
 
-  NSLIM :: "[real=>real,real,real] => bool"
+  NSLIM :: "[real => 'a::real_normed_vector, real, 'a] => bool"
             ("((_)/ -- (_)/ --NS> (_))" [60, 0, 60] 60)
-  "f -- a --NS> L = (\<forall>x. (x \<noteq> hypreal_of_real a &
-          x @= hypreal_of_real a -->
-          ( *f* f) x @= hypreal_of_real L))"
+  "f -- a --NS> L =
+    (\<forall>x. (x \<noteq> star_of a & x @= star_of a --> ( *f* f) x @= star_of L))"
 
-  isCont :: "[real=>real,real] => bool"
+  isCont :: "[real => 'a::real_normed_vector, real] => bool"
   "isCont f a = (f -- a --> (f a))"
 
-  isNSCont :: "[real=>real,real] => bool"
+  isNSCont :: "[real => 'a::real_normed_vector, real] => bool"
     --{*NS definition dispenses with limit notions*}
-  "isNSCont f a = (\<forall>y. y @= hypreal_of_real a -->
-         ( *f* f) y @= hypreal_of_real (f a))"
+  "isNSCont f a = (\<forall>y. y @= star_of a -->
+         ( *f* f) y @= star_of (f a))"
 
   deriv:: "[real=>real,real,real] => bool"
     --{*Differentiation: D is derivative of function f at x*}
@@ -79,12 +78,17 @@
 
 lemma LIM_eq:
      "f -- a --> L =
-     (\<forall>r>0.\<exists>s>0.\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < s --> \<bar>f x - L\<bar> < r)"
+     (\<forall>r>0.\<exists>s>0.\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < s --> norm (f x - L) < r)"
 by (simp add: LIM_def diff_minus)
 
+lemma LIM_I:
+     "(!!r. 0<r ==> \<exists>s>0.\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < s --> norm (f x - L) < r)
+      ==> f -- a --> L"
+by (simp add: LIM_eq)
+
 lemma LIM_D:
      "[| f -- a --> L; 0<r |]
-      ==> \<exists>s>0.\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < s --> \<bar>f x - L\<bar> < r"
+      ==> \<exists>s>0.\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < s --> norm (f x - L) < r"
 by (simp add: LIM_eq)
 
 lemma LIM_const [simp]: "(%x. k) -- x --> k"
@@ -93,76 +97,55 @@
 lemma LIM_add:
   assumes f: "f -- a --> L" and g: "g -- a --> M"
   shows "(%x. f x + g(x)) -- a --> (L + M)"
-proof (unfold LIM_eq, clarify)
+proof (rule LIM_I)
   fix r :: real
   assume r: "0 < r"
   from LIM_D [OF f half_gt_zero [OF r]]
   obtain fs
     where fs:    "0 < fs"
-      and fs_lt: "\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < fs --> \<bar>f x - L\<bar> < r/2"
+      and fs_lt: "\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < fs --> norm (f x - L) < r/2"
   by blast
   from LIM_D [OF g half_gt_zero [OF r]]
   obtain gs
     where gs:    "0 < gs"
-      and gs_lt: "\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < gs --> \<bar>g x - M\<bar> < r/2"
+      and gs_lt: "\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < gs --> norm (g x - M) < r/2"
   by blast
-  show "\<exists>s>0.\<forall>x. x \<noteq> a \<and> \<bar>x-a\<bar> < s \<longrightarrow> \<bar>f x + g x - (L + M)\<bar> < r"
+  show "\<exists>s>0.\<forall>x. x \<noteq> a \<and> \<bar>x-a\<bar> < s \<longrightarrow> norm (f x + g x - (L + M)) < r"
   proof (intro exI conjI strip)
     show "0 < min fs gs"  by (simp add: fs gs)
     fix x :: real
     assume "x \<noteq> a \<and> \<bar>x-a\<bar> < min fs gs"
     hence "x \<noteq> a \<and> \<bar>x-a\<bar> < fs \<and> \<bar>x-a\<bar> < gs" by simp
     with fs_lt gs_lt
-    have "\<bar>f x - L\<bar> < r/2" and "\<bar>g x - M\<bar> < r/2" by blast+
-    hence "\<bar>f x - L\<bar> + \<bar>g x - M\<bar> < r" by arith
-    thus "\<bar>f x + g x - (L + M)\<bar> < r"
-      by (blast intro: abs_diff_triangle_ineq order_le_less_trans)
+    have "norm (f x - L) < r/2" and "norm (g x - M) < r/2" by blast+
+    hence "norm (f x - L) + norm (g x - M) < r" by arith
+    thus "norm (f x + g x - (L + M)) < r"
+      by (blast intro: norm_diff_triangle_ineq order_le_less_trans)
   qed
 qed
 
+lemma minus_diff_minus:
+  fixes a b :: "'a::ab_group_add"
+  shows "(- a) - (- b) = - (a - b)"
+by simp
+
 lemma LIM_minus: "f -- a --> L ==> (%x. -f(x)) -- a --> -L"
-apply (simp add: LIM_eq)
-apply (subgoal_tac "\<forall>x. \<bar>- f x + L\<bar> = \<bar>f x - L\<bar>")
-apply (simp_all add: abs_if)
-done
+by (simp only: LIM_eq minus_diff_minus norm_minus_cancel)
 
 lemma LIM_add_minus:
     "[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) + -g(x)) -- x --> (l + -m)"
-by (blast dest: LIM_add LIM_minus)
+by (intro LIM_add LIM_minus)
 
 lemma LIM_diff:
     "[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) - g(x)) -- x --> l-m"
-by (simp add: diff_minus LIM_add_minus)
+by (simp only: diff_minus LIM_add LIM_minus)
 
 
 lemma LIM_const_not_eq: "k \<noteq> L ==> ~ ((%x. k) -- a --> L)"
-proof (simp add: linorder_neq_iff LIM_eq, elim disjE)
-  assume k: "k < L"
-  show "\<exists>r>0. \<forall>s>0. (\<exists>x. (x < a \<or> a < x) \<and> \<bar>x-a\<bar> < s) \<and> \<not> \<bar>k-L\<bar> < r"
-  proof (intro exI conjI strip)
-    show "0 < L-k" by (simp add: k compare_rls)
-    fix s :: real
-    assume s: "0<s"
-    { from s show "s/2 + a < a \<or> a < s/2 + a" by arith
-     next
-      from s show "\<bar>s / 2 + a - a\<bar> < s" by (simp add: abs_if)
-     next
-      from s show "~ \<bar>k-L\<bar> < L-k" by (simp add: abs_if) }
-  qed
-next
-  assume k: "L < k"
-  show "\<exists>r>0.\<forall>s>0. (\<exists>x. (x < a \<or> a < x) \<and> \<bar>x-a\<bar> < s) \<and> \<not> \<bar>k-L\<bar> < r"
-  proof (intro exI conjI strip)
-    show "0 < k-L" by (simp add: k compare_rls)
-    fix s :: real
-    assume s: "0<s"
-    { from s show "s/2 + a < a \<or> a < s/2 + a" by arith
-     next
-      from s show "\<bar>s / 2 + a - a\<bar> < s" by (simp add: abs_if)
-     next
-      from s show "~ \<bar>k-L\<bar> < k-L" by (simp add: abs_if) }
-  qed
-qed
+apply (simp add: LIM_eq)
+apply (rule_tac x="norm (k - L)" in exI, simp, safe)
+apply (rule_tac x="a + s/2" in exI, simp)
+done
 
 lemma LIM_const_eq: "(%x. k) -- x --> L ==> k = L"
 apply (rule ccontr)
@@ -175,31 +158,34 @@
 done
 
 lemma LIM_mult_zero:
+  fixes f g :: "real \<Rightarrow> 'a::real_normed_algebra"
   assumes f: "f -- a --> 0" and g: "g -- a --> 0"
   shows "(%x. f(x) * g(x)) -- a --> 0"
-proof (simp add: LIM_eq abs_mult, clarify)
+proof (rule LIM_I, simp)
   fix r :: real
   assume r: "0<r"
   from LIM_D [OF f zero_less_one]
   obtain fs
     where fs:    "0 < fs"
-      and fs_lt: "\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < fs --> \<bar>f x\<bar> < 1"
+      and fs_lt: "\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < fs --> norm (f x) < 1"
   by auto
   from LIM_D [OF g r]
   obtain gs
     where gs:    "0 < gs"
-      and gs_lt: "\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < gs --> \<bar>g x\<bar> < r"
+      and gs_lt: "\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < gs --> norm (g x) < r"
   by auto
-  show "\<exists>s. 0 < s \<and> (\<forall>x. x \<noteq> a \<and> \<bar>x-a\<bar> < s \<longrightarrow> \<bar>f x\<bar> * \<bar>g x\<bar> < r)"
+  show "\<exists>s. 0 < s \<and> (\<forall>x. x \<noteq> a \<and> \<bar>x-a\<bar> < s \<longrightarrow> norm (f x * g x) < r)"
   proof (intro exI conjI strip)
     show "0 < min fs gs"  by (simp add: fs gs)
     fix x :: real
     assume "x \<noteq> a \<and> \<bar>x-a\<bar> < min fs gs"
     hence  "x \<noteq> a \<and> \<bar>x-a\<bar> < fs \<and> \<bar>x-a\<bar> < gs" by simp
     with fs_lt gs_lt
-    have "\<bar>f x\<bar> < 1" and "\<bar>g x\<bar> < r" by blast+
-    hence "\<bar>f x\<bar> * \<bar>g x\<bar> < 1*r" by (rule abs_mult_less)
-    thus "\<bar>f x\<bar> * \<bar>g x\<bar> < r" by simp
+    have "norm (f x) < 1" and "norm (g x) < r" by blast+
+    hence "norm (f x) * norm (g x) < 1*r"
+      by (rule mult_strict_mono' [OF _ _ norm_ge_zero norm_ge_zero])
+    thus "norm (f x * g x) < r"
+      by (simp add: order_le_less_trans [OF norm_mult_ineq])
   qed
 qed
 
@@ -223,62 +209,71 @@
 
 text{*Standard and NS definitions of Limit*} (*NEEDS STRUCTURING*)
 lemma LIM_NSLIM:
-      "f -- x --> L ==> f -- x --NS> L"
-apply (simp add: LIM_def NSLIM_def approx_def)
+      "f -- a --> L ==> f -- a --NS> L"
+apply (simp add: LIM_def NSLIM_def approx_def, safe)
+apply (rule_tac x="x" in star_cases)
+apply (simp add: star_of_def star_n_minus star_n_add starfun)
 apply (simp add: Infinitesimal_FreeUltrafilterNat_iff, safe)
-apply (rule_tac x = xa in star_cases)
-apply (auto simp add: real_add_minus_iff starfun star_n_minus star_of_def star_n_add star_n_eq_iff)
-apply (rule bexI [OF _ Rep_star_star_n], clarify)
+apply (simp add: star_n_eq_iff)
 apply (drule_tac x = u in spec, clarify)
 apply (drule_tac x = s in spec, clarify)
-apply (subgoal_tac "\<forall>n::nat. (Xa n) \<noteq> x & \<bar>(Xa n) + - x\<bar> < s --> \<bar>f (Xa n) + - L\<bar> < u")
-prefer 2 apply blast
-apply (drule FreeUltrafilterNat_all, ultra)
+apply (simp only: FUFNat.Collect_not [symmetric])
+apply (elim ultra, simp)
 done
 
 
 subsubsection{*Limit: The NS definition implies the standard definition.*}
 
-lemma lemma_LIM: "\<forall>s>0.\<exists>xa.  xa \<noteq> x &
-         \<bar>xa + - x\<bar> < s  & r \<le> \<bar>f xa + -L\<bar>
-      ==> \<forall>n::nat. \<exists>xa.  xa \<noteq> x &
-              \<bar>xa + -x\<bar> < inverse(real(Suc n)) & r \<le> \<bar>f xa + -L\<bar>"
+lemma lemma_LIM:
+  fixes L :: "'a::real_normed_vector"
+  shows "\<forall>s>0. \<exists>x. x \<noteq> a \<and> \<bar>x + - a\<bar> < s \<and> \<not> norm (f x + -L) < r
+      ==> \<forall>n::nat. \<exists>x. x \<noteq> a \<and>
+              \<bar>x + -a\<bar> < inverse(real(Suc n)) \<and> \<not> norm (f x + -L) < r"
 apply clarify
 apply (cut_tac n1 = n in real_of_nat_Suc_gt_zero [THEN positive_imp_inverse_positive], auto)
 done
 
 lemma lemma_skolemize_LIM2:
-     "\<forall>s>0.\<exists>xa.  xa \<noteq> x & \<bar>xa + - x\<bar> < s  & r \<le> \<bar>f xa + -L\<bar>
-      ==> \<exists>X. \<forall>n::nat. X n \<noteq> x &
-                \<bar>X n + -x\<bar> < inverse(real(Suc n)) & r \<le> abs(f (X n) + -L)"
+  fixes L :: "'a::real_normed_vector"
+  shows "\<forall>s>0. \<exists>x. x \<noteq> a \<and> \<bar>x + - a\<bar> < s \<and> \<not> norm (f x + -L) < r
+      ==> \<exists>X. \<forall>n::nat. X n \<noteq> a \<and>
+                \<bar>X n + -a\<bar> < inverse(real(Suc n)) \<and> \<not> norm(f (X n) + -L) < r"
 apply (drule lemma_LIM)
 apply (drule choice, blast)
 done
 
-lemma lemma_simp: "\<forall>n. X n \<noteq> x &
-          \<bar>X n + - x\<bar> < inverse (real(Suc n)) &
-          r \<le> abs (f (X n) + - L) ==>
-          \<forall>n. \<bar>X n + - x\<bar> < inverse (real(Suc n))"
+lemma FreeUltrafilterNat_most: "\<exists>N. \<forall>n\<ge>N. P n \<Longrightarrow> {n. P n} \<in> \<U>"
+apply (erule exE)
+apply (rule_tac u="{n. N \<le> n}" in FUFNat.subset)
+apply (rule cofinite_mem_FreeUltrafilterNat)
+apply (simp add: Collect_neg_eq [symmetric])
+apply (simp add: linorder_not_le finite_nat_segment)
+apply fast
+done
+
+lemma lemma_simp: "\<forall>n. X n \<noteq> a &
+          \<bar>X n + - a\<bar> < inverse (real(Suc n)) &
+          \<not> norm (f (X n) + - L) < r ==>
+          \<forall>n. \<bar>X n + - a\<bar> < inverse (real(Suc n))"
 by auto
 
 
 text{*NSLIM => LIM*}
 
-lemma NSLIM_LIM: "f -- x --NS> L ==> f -- x --> L"
+lemma NSLIM_LIM: "f -- a --NS> L ==> f -- a --> L"
 apply (simp add: LIM_def NSLIM_def approx_def)
-apply (simp add: Infinitesimal_FreeUltrafilterNat_iff, clarify)
-apply (rule ccontr, simp)
-apply (simp add: linorder_not_less)
+apply (rule ccontr, simp, clarify)
 apply (drule lemma_skolemize_LIM2, safe)
 apply (drule_tac x = "star_n X" in spec)
-apply (auto simp add: starfun star_n_minus star_of_def star_n_add star_n_eq_iff)
-apply (drule lemma_simp [THEN real_seq_to_hypreal_Infinitesimal])
-apply (simp add: Infinitesimal_FreeUltrafilterNat_iff star_of_def star_n_minus star_n_add star_n_eq_iff, blast)
-apply (drule spec, drule mp, assumption)
-apply (drule FreeUltrafilterNat_all, ultra)
+apply (drule mp, rule conjI)
+apply (simp add: star_of_def star_n_eq_iff)
+apply (rule real_seq_to_hypreal_Infinitesimal, simp)
+apply (simp add: starfun star_of_def star_n_minus star_n_add)
+apply (simp add: Infinitesimal_FreeUltrafilterNat_iff)
+apply (drule spec, drule (1) mp)
+apply simp
 done
 
-
 theorem LIM_NSLIM_iff: "(f -- x --> L) = (f -- x --NS> L)"
 by (blast intro: LIM_NSLIM NSLIM_LIM)
 
@@ -286,12 +281,15 @@
       The properties hold for standard limits as well!*}
 
 lemma NSLIM_mult:
-     "[| f -- x --NS> l; g -- x --NS> m |]
+  fixes l m :: "'a::real_normed_algebra"
+  shows "[| f -- x --NS> l; g -- x --NS> m |]
       ==> (%x. f(x) * g(x)) -- x --NS> (l * m)"
 by (auto simp add: NSLIM_def intro!: approx_mult_HFinite)
 
 lemma LIM_mult2:
-     "[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) * g(x)) -- x --> (l * m)"
+  fixes l m :: "'a::real_normed_algebra"
+  shows "[| f -- x --> l; g -- x --> m |]
+      ==> (%x. f(x) * g(x)) -- x --> (l * m)"
 by (simp add: LIM_NSLIM_iff NSLIM_mult)
 
 lemma NSLIM_add:
@@ -325,14 +323,18 @@
 
 
 lemma NSLIM_inverse:
-     "[| f -- a --NS> L;  L \<noteq> 0 |]
+  fixes L :: "'a::{real_normed_div_algebra,division_by_zero}"
+  shows "[| f -- a --NS> L;  L \<noteq> 0 |]
       ==> (%x. inverse(f(x))) -- a --NS> (inverse L)"
 apply (simp add: NSLIM_def, clarify)
 apply (drule spec)
-apply (auto simp add: hypreal_of_real_approx_inverse)
+apply (auto simp add: star_of_approx_inverse)
 done
 
-lemma LIM_inverse: "[| f -- a --> L; L \<noteq> 0 |] ==> (%x. inverse(f(x))) -- a --> (inverse L)"
+lemma LIM_inverse:
+  fixes L :: "'a::{real_normed_div_algebra,division_by_zero}"
+  shows "[| f -- a --> L; L \<noteq> 0 |]
+      ==> (%x. inverse(f(x))) -- a --> (inverse L)"
 by (simp add: LIM_NSLIM_iff NSLIM_inverse)
 
 
@@ -357,19 +359,15 @@
 apply (auto simp add: diff_minus add_assoc)
 done
 
-lemma NSLIM_not_zero: "k \<noteq> 0 ==> ~ ((%x. k) -- x --NS> 0)"
+lemma NSLIM_const_not_eq: "k \<noteq> L ==> ~ ((%x. k) -- x --NS> L)"
 apply (simp add: NSLIM_def)
 apply (rule_tac x = "hypreal_of_real x + epsilon" in exI)
 apply (auto intro: Infinitesimal_add_approx_self [THEN approx_sym]
             simp add: hypreal_epsilon_not_zero)
 done
 
-lemma NSLIM_const_not_eq: "k \<noteq> L ==> ~ ((%x. k) -- x --NS> L)"
-apply (simp add: NSLIM_def)
-apply (rule_tac x = "hypreal_of_real x + epsilon" in exI)
-apply (auto intro: Infinitesimal_add_approx_self [THEN approx_sym]
-            simp add: hypreal_epsilon_not_zero)
-done
+lemma NSLIM_not_zero: "k \<noteq> 0 ==> ~ ((%x. k) -- x --NS> 0)"
+by (rule NSLIM_const_not_eq)
 
 lemma NSLIM_const_eq: "(%x. k) -- x --NS> L ==> k = L"
 apply (rule ccontr)
@@ -381,19 +379,24 @@
 apply (drule NSLIM_minus)
 apply (drule NSLIM_add, assumption)
 apply (auto dest!: NSLIM_const_eq [symmetric])
+apply (simp add: diff_def [symmetric])
 done
 
 lemma LIM_unique2: "[| f -- x --> L; f -- x --> M |] ==> L = M"
 by (simp add: LIM_NSLIM_iff NSLIM_unique)
 
 
-lemma NSLIM_mult_zero: "[| f -- x --NS> 0; g -- x --NS> 0 |] ==> (%x. f(x)*g(x)) -- x --NS> 0"
+lemma NSLIM_mult_zero:
+  fixes f g :: "real \<Rightarrow> 'a::real_normed_algebra"
+  shows "[| f -- x --NS> 0; g -- x --NS> 0 |] ==> (%x. f(x)*g(x)) -- x --NS> 0"
 by (drule NSLIM_mult, auto)
 
 (* we can use the corresponding thm LIM_mult2 *)
 (* for standard definition of limit           *)
 
-lemma LIM_mult_zero2: "[| f -- x --> 0; g -- x --> 0 |] ==> (%x. f(x)*g(x)) -- x --> 0"
+lemma LIM_mult_zero2:
+  fixes f g :: "real \<Rightarrow> 'a::real_normed_algebra"
+  shows "[| f -- x --> 0; g -- x --> 0 |] ==> (%x. f(x)*g(x)) -- x --> 0"
 by (drule LIM_mult2, auto)
 
 
@@ -472,7 +475,9 @@
 by (auto intro: approx_add simp add: isNSCont_isCont_iff [symmetric] isNSCont_def)
 
 text{*mult continuous*}
-lemma isCont_mult: "[| isCont f a; isCont g a |] ==> isCont (%x. f(x) * g(x)) a"
+lemma isCont_mult:
+  fixes f g :: "real \<Rightarrow> 'a::real_normed_algebra"
+  shows "[| isCont f a; isCont g a |] ==> isCont (%x. f(x) * g(x)) a"
 by (auto intro!: starfun_mult_HFinite_approx
             simp del: starfun_mult [symmetric]
             simp add: isNSCont_isCont_iff [symmetric] isNSCont_def)
@@ -492,12 +497,15 @@
 by (auto simp add: isNSCont_isCont_iff [symmetric] isNSCont_minus)
 
 lemma isCont_inverse:
-      "[| isCont f x; f x \<noteq> 0 |] ==> isCont (%x. inverse (f x)) x"
+  fixes f :: "real \<Rightarrow> 'a::{real_normed_div_algebra,division_by_zero}"
+  shows "[| isCont f x; f x \<noteq> 0 |] ==> isCont (%x. inverse (f x)) x"
 apply (simp add: isCont_def)
 apply (blast intro: LIM_inverse)
 done
 
-lemma isNSCont_inverse: "[| isNSCont f x; f x \<noteq> 0 |] ==> isNSCont (%x. inverse (f x)) x"
+lemma isNSCont_inverse:
+  fixes f :: "real \<Rightarrow> 'a::{real_normed_div_algebra,division_by_zero}"
+  shows "[| isNSCont f x; f x \<noteq> 0 |] ==> isNSCont (%x. inverse (f x)) x"
 by (auto intro: isCont_inverse simp add: isNSCont_isCont_iff)
 
 lemma isCont_diff:
@@ -578,17 +586,15 @@
 
 lemma isUCont_isNSUCont: "isUCont f ==> isNSUCont f"
 apply (simp add: isNSUCont_def isUCont_def approx_def)
+apply (simp add: all_star_eq starfun star_n_minus star_n_add)
 apply (simp add: Infinitesimal_FreeUltrafilterNat_iff, safe)
-apply (rule_tac x = x in star_cases)
-apply (rule_tac x = y in star_cases)
-apply (auto simp add: starfun star_n_minus star_n_add)
-apply (rule bexI [OF _ Rep_star_star_n], safe)
+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")
 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 (drule FreeUltrafilterNat_all, ultra)
+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>
@@ -615,17 +621,17 @@
 
 lemma isNSUCont_isUCont:
      "isNSUCont f ==> isUCont f"
-apply (simp add: isNSUCont_def isUCont_def approx_def)
-apply (simp add: Infinitesimal_FreeUltrafilterNat_iff, safe)
+apply (simp add: isNSUCont_def isUCont_def approx_def, safe)
 apply (rule ccontr, simp)
 apply (simp add: linorder_not_less)
 apply (drule lemma_skolemize_LIM2u, safe)
 apply (drule_tac x = "star_n X" in spec)
 apply (drule_tac x = "star_n Y" in spec)
-apply (simp add: starfun star_n_minus star_n_add, auto)
-apply (drule lemma_simpu [THEN real_seq_to_hypreal_Infinitesimal2])
-apply (simp add: Infinitesimal_FreeUltrafilterNat_iff star_n_minus star_n_add, blast)
-apply (drule_tac x = r in spec, clarify)
+apply (drule mp)
+apply (rule real_seq_to_hypreal_Infinitesimal2, simp)
+apply (simp add: all_star_eq starfun star_n_minus star_n_add)
+apply (simp add: Infinitesimal_FreeUltrafilterNat_iff)
+apply (drule spec, drule (1) mp)
 apply (drule FreeUltrafilterNat_all, ultra)
 done
 
@@ -677,11 +683,6 @@
 
 subsubsection{*Alternative definition for differentiability*}
 
-lemma LIM_I:
-     "(!!r. 0<r ==> \<exists>s>0.\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < s --> \<bar>f x - L\<bar> < r)
-      ==> f -- a --> L"
-by (simp add: LIM_eq)
-
 lemma DERIV_LIM_iff:
      "((%h. (f(a + h) - f(a)) / h) -- 0 --> D) =
       ((%x. (f(x)-f(a)) / (x-a)) -- a --> D)"
@@ -695,14 +696,14 @@
       and s_lt: "\<forall>x. x \<noteq> 0 & \<bar>x\<bar> < s --> \<bar>(f (a + x) - f a) / x - D\<bar> < r"
   by auto
   show "\<exists>s. 0 < s \<and>
-            (\<forall>x. x \<noteq> a \<and> \<bar>x-a\<bar> < s \<longrightarrow> \<bar>(f x - f a) / (x-a) - D\<bar> < r)"
+            (\<forall>x. x \<noteq> a \<and> \<bar>x-a\<bar> < s \<longrightarrow> norm ((f x - f a) / (x-a) - D) < r)"
   proof (intro exI conjI strip)
     show "0 < s"  by (rule s)
   next
     fix x::real
     assume "x \<noteq> a \<and> \<bar>x-a\<bar> < s"
     with s_lt [THEN spec [where x="x-a"]]
-    show "\<bar>(f x - f a) / (x-a) - D\<bar> < r" by auto
+    show "norm ((f x - f a) / (x-a) - D) < r" by auto
   qed
 next
   fix r::real
@@ -714,14 +715,14 @@
       and s_lt: "\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < s --> \<bar>(f x - f a)/(x-a) - D\<bar> < r"
   by auto
   show "\<exists>s. 0 < s \<and>
-            (\<forall>x. x \<noteq> 0 & \<bar>x - 0\<bar> < s --> \<bar>(f (a + x) - f a) / x - D\<bar> < r)"
+            (\<forall>x. x \<noteq> 0 & \<bar>x - 0\<bar> < s --> norm ((f (a + x) - f a) / x - D) < r)"
   proof (intro exI conjI strip)
     show "0 < s"  by (rule s)
   next
     fix x::real
     assume "x \<noteq> 0 \<and> \<bar>x - 0\<bar> < s"
     with s_lt [THEN spec [where x="x+a"]]
-    show "\<bar>(f (a + x) - f a) / x - D\<bar> < r" by (auto simp add: add_ac)
+    show "norm ((f (a + x) - f a) / x - D) < r" by (auto simp add: add_ac)
   qed
 qed
 
@@ -1236,7 +1237,7 @@
 lemma f_inc_g_dec_Beq_f: "[| \<forall>n. f(n) \<le> f(Suc n);
          \<forall>n. g(Suc n) \<le> g(n);
          \<forall>n. f(n) \<le> g(n) |]
-      ==> Bseq f"
+      ==> Bseq (f :: nat \<Rightarrow> real)"
 apply (rule_tac k = "f 0" and K = "g 0" in BseqI2, rule allI)
 apply (induct_tac "n")
 apply (auto intro: order_trans)
@@ -1248,7 +1249,7 @@
 lemma f_inc_g_dec_Beq_g: "[| \<forall>n. f(n) \<le> f(Suc n);
          \<forall>n. g(Suc n) \<le> g(n);
          \<forall>n. f(n) \<le> g(n) |]
-      ==> Bseq g"
+      ==> Bseq (g :: nat \<Rightarrow> real)"
 apply (subst Bseq_minus_iff [symmetric])
 apply (rule_tac g = "%x. - (f x)" in f_inc_g_dec_Beq_f)
 apply auto
@@ -1282,7 +1283,7 @@
 lemma lemma_nest: "[| \<forall>n. f(n) \<le> f(Suc n);
          \<forall>n. g(Suc n) \<le> g(n);
          \<forall>n. f(n) \<le> g(n) |]
-      ==> \<exists>l m. l \<le> m &  ((\<forall>n. f(n) \<le> l) & f ----> l) &
+      ==> \<exists>l m :: real. l \<le> m &  ((\<forall>n. f(n) \<le> l) & f ----> l) &
                             ((\<forall>n. m \<le> g(n)) & g ----> m)"
 apply (subgoal_tac "monoseq f & monoseq g")
 prefer 2 apply (force simp add: LIMSEQ_iff monoseq_Suc)
@@ -1299,7 +1300,7 @@
          \<forall>n. g(Suc n) \<le> g(n);
          \<forall>n. f(n) \<le> g(n);
          (%n. f(n) - g(n)) ----> 0 |]
-      ==> \<exists>l. ((\<forall>n. f(n) \<le> l) & f ----> l) &
+      ==> \<exists>l::real. ((\<forall>n. f(n) \<le> l) & f ----> l) &
                 ((\<forall>n. l \<le> g(n)) & g ----> l)"
 apply (drule lemma_nest, auto)
 apply (subgoal_tac "l = m")
@@ -1414,7 +1415,7 @@
 
 subsection{*Intermediate Value Theorem: Prove Contrapositive by Bisection*}
 
-lemma IVT: "[| f(a) \<le> y; y \<le> f(b);
+lemma IVT: "[| f(a) \<le> (y::real); y \<le> f(b);
          a \<le> b;
          (\<forall>x. a \<le> x & x \<le> b --> isCont f x) |]
       ==> \<exists>x. a \<le> x & x \<le> b & f(x) = y"
@@ -1441,7 +1442,7 @@
 apply (case_tac "x \<le> aa", simp_all)
 done
 
-lemma IVT2: "[| f(b) \<le> y; y \<le> f(a);
+lemma IVT2: "[| f(b) \<le> (y::real); y \<le> f(a);
          a \<le> b;
          (\<forall>x. a \<le> x & x \<le> b --> isCont f x)
       |] ==> \<exists>x. a \<le> x & x \<le> b & f(x) = y"
@@ -1451,13 +1452,13 @@
 done
 
 (*HOL style here: object-level formulations*)
-lemma IVT_objl: "(f(a) \<le> y & y \<le> f(b) & a \<le> b &
+lemma IVT_objl: "(f(a) \<le> (y::real) & y \<le> f(b) & a \<le> b &
       (\<forall>x. a \<le> x & x \<le> b --> isCont f x))
       --> (\<exists>x. a \<le> x & x \<le> b & f(x) = y)"
 apply (blast intro: IVT)
 done
 
-lemma IVT2_objl: "(f(b) \<le> y & y \<le> f(a) & a \<le> b &
+lemma IVT2_objl: "(f(b) \<le> (y::real) & y \<le> f(a) & a \<le> b &
       (\<forall>x. a \<le> x & x \<le> b --> isCont f x))
       --> (\<exists>x. a \<le> x & x \<le> b & f(x) = y)"
 apply (blast intro: IVT2)
@@ -1467,7 +1468,7 @@
 
 lemma isCont_bounded:
      "[| a \<le> b; \<forall>x. a \<le> x & x \<le> b --> isCont f x |]
-      ==> \<exists>M. \<forall>x. a \<le> x & x \<le> b --> f(x) \<le> M"
+      ==> \<exists>M::real. \<forall>x. a \<le> x & x \<le> b --> f(x) \<le> M"
 apply (cut_tac P = "% (u,v) . a \<le> u & u \<le> v & v \<le> b --> (\<exists>M. \<forall>x. u \<le> x & x \<le> v --> f x \<le> M)" in lemma_BOLZANO2)
 apply safe
 apply simp_all
@@ -1497,7 +1498,7 @@
 by (blast intro: reals_complete)
 
 lemma isCont_has_Ub: "[| a \<le> b; \<forall>x. a \<le> x & x \<le> b --> isCont f x |]
-         ==> \<exists>M. (\<forall>x. a \<le> x & x \<le> b --> f(x) \<le> M) &
+         ==> \<exists>M::real. (\<forall>x. a \<le> x & x \<le> b --> f(x) \<le> M) &
                    (\<forall>N. N < M --> (\<exists>x. a \<le> x & x \<le> b & N < f(x)))"
 apply (cut_tac S = "Collect (%y. \<exists>x. a \<le> x & x \<le> b & y = f x)"
         in lemma_reals_complete)
@@ -1513,7 +1514,7 @@
 lemma isCont_eq_Ub:
   assumes le: "a \<le> b"
       and con: "\<forall>x. a \<le> x & x \<le> b --> isCont f x"
-  shows "\<exists>M. (\<forall>x. a \<le> x & x \<le> b --> f(x) \<le> M) &
+  shows "\<exists>M::real. (\<forall>x. a \<le> x & x \<le> b --> f(x) \<le> M) &
              (\<exists>x. a \<le> x & x \<le> b & f(x) = M)"
 proof -
   from isCont_has_Ub [OF le con]
@@ -1553,7 +1554,7 @@
 text{*Same theorem for lower bound*}
 
 lemma isCont_eq_Lb: "[| a \<le> b; \<forall>x. a \<le> x & x \<le> b --> isCont f x |]
-         ==> \<exists>M. (\<forall>x. a \<le> x & x \<le> b --> M \<le> f(x)) &
+         ==> \<exists>M::real. (\<forall>x. a \<le> x & x \<le> b --> M \<le> f(x)) &
                    (\<exists>x. a \<le> x & x \<le> b & f(x) = M)"
 apply (subgoal_tac "\<forall>x. a \<le> x & x \<le> b --> isCont (%x. - (f x)) x")
 prefer 2 apply (blast intro: isCont_minus)
@@ -1566,7 +1567,7 @@
 text{*Another version.*}
 
 lemma isCont_Lb_Ub: "[|a \<le> b; \<forall>x. a \<le> x & x \<le> b --> isCont f x |]
-      ==> \<exists>L M. (\<forall>x. a \<le> x & x \<le> b --> L \<le> f(x) & f(x) \<le> M) &
+      ==> \<exists>L M::real. (\<forall>x. a \<le> x & x \<le> b --> L \<le> f(x) & f(x) \<le> M) &
           (\<forall>y. L \<le> y & y \<le> M --> (\<exists>x. a \<le> x & x \<le> b & (f(x) = y)))"
 apply (frule isCont_eq_Lb)
 apply (frule_tac [2] isCont_eq_Ub)
@@ -1925,6 +1926,7 @@
 strict maximum at an end point, not in the middle.*}
 
 lemma lemma_isCont_inj:
+  fixes f :: "real \<Rightarrow> real"
   assumes d: "0 < d"
       and inj [rule_format]: "\<forall>z. \<bar>z-x\<bar> \<le> d --> g(f z) = z"
       and cont: "\<forall>z. \<bar>z-x\<bar> \<le> d --> isCont f z"
@@ -1966,7 +1968,8 @@
 text{*Similar version for lower bound.*}
 
 lemma lemma_isCont_inj2:
-     "[|0 < d; \<forall>z. \<bar>z-x\<bar> \<le> d --> g(f z) = z;
+  fixes f g :: "real \<Rightarrow> real"
+  shows "[|0 < d; \<forall>z. \<bar>z-x\<bar> \<le> d --> g(f z) = z;
         \<forall>z. \<bar>z-x\<bar> \<le> d --> isCont f z |]
       ==> \<exists>z. \<bar>z-x\<bar> \<le> d & f z < f x"
 apply (insert lemma_isCont_inj
@@ -1978,6 +1981,7 @@
 @{text "f[[x - d, x + d]]"} .*}
 
 lemma isCont_inj_range:
+  fixes f :: "real \<Rightarrow> real"
   assumes d: "0 < d"
       and inj: "\<forall>z. \<bar>z-x\<bar> \<le> d --> g(f z) = z"
       and cont: "\<forall>z. \<bar>z-x\<bar> \<le> d --> isCont f z"
@@ -2205,35 +2209,35 @@
   shows "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L"
 proof -
   {
-    from prems have Xdef: "\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & \<bar>x + -a\<bar> < s --> \<bar>X x + -L\<bar> < r" by (unfold LIM_def)
+    from prems have Xdef: "\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & \<bar>x + -a\<bar> < s --> norm (X x + -L) < r" by (unfold LIM_def)
     
     fix S
     assume as: "(\<forall>n. S n \<noteq> a) \<and> S ----> a"
     then have "S ----> a" by auto
-    then have Sdef: "(\<forall>r. 0 < r --> (\<exists>no. \<forall>n. no \<le> n --> \<bar>S n + -a\<bar> < r))" by (unfold LIMSEQ_def)
+    then have Sdef: "(\<forall>r. 0 < r --> (\<exists>no. \<forall>n. no \<le> n --> norm (S n + -a) < r))" by (unfold LIMSEQ_def)
     {
       fix r
-      from Xdef have Xdef2: "0 < r --> (\<exists>s > 0. \<forall>x. x \<noteq> a \<and> \<bar>x + -a\<bar> < s --> \<bar>X x + -L\<bar> < r)" by simp
+      from Xdef have Xdef2: "0 < r --> (\<exists>s > 0. \<forall>x. x \<noteq> a \<and> \<bar>x + -a\<bar> < s --> norm (X x + -L) < r)" by simp
       {
         assume rgz: "0 < r"
 
-        from Xdef2 rgz have "\<exists>s > 0. \<forall>x. x \<noteq> a \<and> \<bar>x + -a\<bar> < s --> \<bar>X x + -L\<bar> < r" by simp 
-        then obtain s where sdef: "s > 0 \<and> (\<forall>x. x\<noteq>a \<and> \<bar>x + -a\<bar> < s \<longrightarrow> \<bar>X x + -L\<bar> < r)" by auto
-        then have aux: "\<forall>x. x\<noteq>a \<and> \<bar>x + -a\<bar> < s \<longrightarrow> \<bar>X x + -L\<bar> < r" by auto
+        from Xdef2 rgz have "\<exists>s > 0. \<forall>x. x \<noteq> a \<and> \<bar>x + -a\<bar> < s --> norm (X x + -L) < r" by simp 
+        then obtain s where sdef: "s > 0 \<and> (\<forall>x. x\<noteq>a \<and> \<bar>x + -a\<bar> < s \<longrightarrow> norm (X x + -L) < r)" by auto
+        then have aux: "\<forall>x. x\<noteq>a \<and> \<bar>x + -a\<bar> < s \<longrightarrow> norm (X x + -L) < r" by auto
         {
           fix n
-          from aux have "S n \<noteq> a \<and> \<bar>S n + -a\<bar> < s \<longrightarrow> \<bar>X (S n) + -L\<bar> < r" by simp
-          with as have imp2: "\<bar>S n + -a\<bar> < s --> \<bar>X (S n) + -L\<bar> < r" by auto
+          from aux have "S n \<noteq> a \<and> \<bar>S n + -a\<bar> < s \<longrightarrow> norm (X (S n) + -L) < r" by simp
+          with as have imp2: "\<bar>S n + -a\<bar> < s --> norm (X (S n) + -L) < r" by auto
         }
-        hence "\<forall>n. \<bar>S n + -a\<bar> < s --> \<bar>X (S n) + -L\<bar> < r" ..
+        hence "\<forall>n. \<bar>S n + -a\<bar> < s --> norm (X (S n) + -L) < r" ..
         moreover
         from Sdef sdef have imp1: "\<exists>no. \<forall>n. no \<le> n --> \<bar>S n + -a\<bar> < s" by auto  
         then obtain no where "\<forall>n. no \<le> n --> \<bar>S n + -a\<bar> < s" by auto
-        ultimately have "\<forall>n. no \<le> n \<longrightarrow> \<bar>X (S n) + -L\<bar> < r" by simp
-        hence "\<exists>no. \<forall>n. no \<le> n \<longrightarrow> \<bar>X (S n) + -L\<bar> < r" by auto
+        ultimately have "\<forall>n. no \<le> n \<longrightarrow> norm (X (S n) + -L) < r" by simp
+        hence "\<exists>no. \<forall>n. no \<le> n \<longrightarrow> norm (X (S n) + -L) < r" by auto
       }
     }
-    hence "(\<forall>r. 0 < r --> (\<exists>no. \<forall>n. no \<le> n --> \<bar>X (S n) + -L\<bar> < r))" by simp
+    hence "(\<forall>r. 0 < r --> (\<exists>no. \<forall>n. no \<le> n --> norm (X (S n) + -L) < r))" by simp
     hence "(\<lambda>n. X (S n)) ----> L" by (fold LIMSEQ_def)
   }
   thus ?thesis by simp
@@ -2246,12 +2250,12 @@
   shows "X -- a --> L"
 proof (rule ccontr)
   assume "\<not> (X -- a --> L)"
-  hence "\<not> (\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & \<bar>x + -a\<bar> < s --> \<bar>X x + -L\<bar> < r)" by (unfold LIM_def)
-  hence "\<exists>r > 0. \<forall>s > 0. \<exists>x. \<not>(x \<noteq> a \<and> \<bar>x + -a\<bar> < s --> \<bar>X x + -L\<bar> < r)" by simp
-  hence "\<exists>r > 0. \<forall>s > 0. \<exists>x. (x \<noteq> a \<and> \<bar>x + -a\<bar> < s \<and> \<bar>X x + -L\<bar> \<ge> r)" by (simp add: linorder_not_less)
-  then obtain r where rdef: "r > 0 \<and> (\<forall>s > 0. \<exists>x. (x \<noteq> a \<and> \<bar>x + -a\<bar> < s \<and> \<bar>X x + -L\<bar> \<ge> r))" by auto
+  hence "\<not> (\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & \<bar>x + -a\<bar> < s --> norm (X x + -L) < r)" by (unfold LIM_def)
+  hence "\<exists>r > 0. \<forall>s > 0. \<exists>x. \<not>(x \<noteq> a \<and> \<bar>x + -a\<bar> < s --> norm (X x + -L) < r)" by simp
+  hence "\<exists>r > 0. \<forall>s > 0. \<exists>x. (x \<noteq> a \<and> \<bar>x + -a\<bar> < s \<and> norm (X x + -L) \<ge> r)" by (simp add: linorder_not_less)
+  then obtain r where rdef: "r > 0 \<and> (\<forall>s > 0. \<exists>x. (x \<noteq> a \<and> \<bar>x + -a\<bar> < s \<and> norm (X x + -L) \<ge> r))" by auto
 
-  let ?F = "\<lambda>n::nat. SOME x. x\<noteq>a \<and> \<bar>x + -a\<bar> < inverse (real (Suc n)) \<and> \<bar>X x + -L\<bar> \<ge> r"
+  let ?F = "\<lambda>n::nat. SOME x. x\<noteq>a \<and> \<bar>x + -a\<bar> < inverse (real (Suc n)) \<and> norm (X x + -L) \<ge> r"
   have "?F ----> a"
   proof -
     {
@@ -2270,10 +2274,10 @@
           "\<bar>?F n + -a\<bar> < inverse (real (Suc n))"
         proof -
           from rdef have
-            "\<exists>x. x\<noteq>a \<and> \<bar>x + -a\<bar> < inverse (real (Suc n)) \<and> \<bar>X x + -L\<bar> \<ge> r"
+            "\<exists>x. x\<noteq>a \<and> \<bar>x + -a\<bar> < inverse (real (Suc n)) \<and> norm (X x + -L) \<ge> r"
             by simp
           hence
-            "(?F n)\<noteq>a \<and> \<bar>(?F n) + -a\<bar> < inverse (real (Suc n)) \<and> \<bar>X (?F n) + -L\<bar> \<ge> r"
+            "(?F n)\<noteq>a \<and> \<bar>(?F n) + -a\<bar> < inverse (real (Suc n)) \<and> norm (X (?F n) + -L) \<ge> r"
             by (simp add: some_eq_ex [symmetric])
           thus ?thesis by simp
         qed
@@ -2291,7 +2295,7 @@
     {
       fix n
       from rdef have
-        "\<exists>x. x\<noteq>a \<and> \<bar>x + -a\<bar> < inverse (real (Suc n)) \<and> \<bar>X x + -L\<bar> \<ge> r"
+        "\<exists>x. x\<noteq>a \<and> \<bar>x + -a\<bar> < inverse (real (Suc n)) \<and> norm (X x + -L) \<ge> r"
         by simp
       hence "?F n \<noteq> a" by (simp add: some_eq_ex [symmetric])
     }
@@ -2307,15 +2311,15 @@
       obtain n where "n = no + 1" by simp
       then have nolen: "no \<le> n" by simp
         (* We prove this by showing that for any m there is an n\<ge>m such that |X (?F n) - L| \<ge> r *)
-      from rdef have "\<forall>s > 0. \<exists>x. (x \<noteq> a \<and> \<bar>x + -a\<bar> < s \<and> \<bar>X x + -L\<bar> \<ge> r)" ..
+      from rdef have "\<forall>s > 0. \<exists>x. (x \<noteq> a \<and> \<bar>x + -a\<bar> < s \<and> norm (X x + -L) \<ge> r)" ..
 
-      then have "\<exists>x. x\<noteq>a \<and> \<bar>x + -a\<bar> < inverse (real (Suc n)) \<and> \<bar>X x + -L\<bar> \<ge> r" by simp
+      then have "\<exists>x. x\<noteq>a \<and> \<bar>x + -a\<bar> < inverse (real (Suc n)) \<and> norm (X x + -L) \<ge> r" by simp
       
-      hence "\<bar>X (?F n) + -L\<bar> \<ge> r" by (simp add: some_eq_ex [symmetric])
-      with nolen have "\<exists>n. no \<le> n \<and> \<bar>X (?F n) + -L\<bar> \<ge> r" by auto
+      hence "norm (X (?F n) + -L) \<ge> r" by (simp add: some_eq_ex [symmetric])
+      with nolen have "\<exists>n. no \<le> n \<and> norm (X (?F n) + -L) \<ge> r" by auto
     }
-    then have "(\<forall>no. \<exists>n. no \<le> n \<and> \<bar>X (?F n) + -L\<bar> \<ge> r)" by simp
-    with rdef have "\<exists>e>0. (\<forall>no. \<exists>n. no \<le> n \<and> \<bar>X (?F n) + -L\<bar> \<ge> e)" by auto
+    then have "(\<forall>no. \<exists>n. no \<le> n \<and> norm (X (?F n) + -L) \<ge> r)" by simp
+    with rdef have "\<exists>e>0. (\<forall>no. \<exists>n. no \<le> n \<and> norm (X (?F n) + -L) \<ge> e)" by auto
     thus ?thesis by (unfold LIMSEQ_def, auto simp add: linorder_not_less)
   qed
   ultimately show False by simp
@@ -2352,26 +2356,26 @@
 proof -
   have "f -- a --> L" .
   hence
-    fd: "\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & \<bar>x + -a\<bar> < s --> \<bar>f x + -L\<bar> < r"
+    fd: "\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & \<bar>x + -a\<bar> < s --> norm (f x + -L) < r"
     by (unfold LIM_def)
   {
     fix r::real
     assume rgz: "0 < r"
-    with fd have "\<exists>s > 0. \<forall>x. x\<noteq>a \<and> \<bar>x + -a\<bar> < s --> \<bar>f x + -L\<bar> < r" by simp
-    then obtain s where sgz: "s > 0" and ax: "\<forall>x. x\<noteq>a \<and> \<bar>x + -a\<bar> < s \<longrightarrow> \<bar>f x + -L\<bar> < r" by auto
-    from ax have ax2: "\<forall>x. (x+c)\<noteq>a \<and> \<bar>(x+c) + -a\<bar> < s \<longrightarrow> \<bar>f (x+c) + -L\<bar> < r" by auto
+    with fd have "\<exists>s > 0. \<forall>x. x\<noteq>a \<and> \<bar>x + -a\<bar> < s --> norm (f x + -L) < r" by simp
+    then obtain s where sgz: "s > 0" and ax: "\<forall>x. x\<noteq>a \<and> \<bar>x + -a\<bar> < s \<longrightarrow> norm (f x + -L) < r" by auto
+    from ax have ax2: "\<forall>x. (x+c)\<noteq>a \<and> \<bar>(x+c) + -a\<bar> < s \<longrightarrow> norm (f (x+c) + -L) < r" by auto
     {
       fix x::real
-      from ax2 have nt: "(x+c)\<noteq>a \<and> \<bar>(x+c) + -a\<bar> < s \<longrightarrow> \<bar>f (x+c) + -L\<bar> < r" ..
+      from ax2 have nt: "(x+c)\<noteq>a \<and> \<bar>(x+c) + -a\<bar> < s \<longrightarrow> norm (f (x+c) + -L) < r" ..
       moreover have "((x+c)\<noteq>a) = (x\<noteq>(a-c))" by auto
       moreover have "((x+c) + -a) = (x + -(a-c))" by simp
-      ultimately have "x\<noteq>(a-c) \<and> \<bar>x + -(a-c)\<bar> < s \<longrightarrow> \<bar>f (x+c) + -L\<bar> < r" by simp
+      ultimately have "x\<noteq>(a-c) \<and> \<bar>x + -(a-c)\<bar> < s \<longrightarrow> norm (f (x+c) + -L) < r" by simp
     }
-    then have "\<forall>x. x\<noteq>(a-c) \<and> \<bar>x + -(a-c)\<bar> < s \<longrightarrow> \<bar>f (x+c) + -L\<bar> < r" ..
-    with sgz have "\<exists>s > 0. \<forall>x. x\<noteq>(a-c) \<and> \<bar>x + -(a-c)\<bar> < s \<longrightarrow> \<bar>f (x+c) + -L\<bar> < r" by auto
+    then have "\<forall>x. x\<noteq>(a-c) \<and> \<bar>x + -(a-c)\<bar> < s \<longrightarrow> norm (f (x+c) + -L) < r" ..
+    with sgz have "\<exists>s > 0. \<forall>x. x\<noteq>(a-c) \<and> \<bar>x + -(a-c)\<bar> < s \<longrightarrow> norm (f (x+c) + -L) < r" by auto
   }
   then have
-    "\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> (a-c) & \<bar>x + -(a-c)\<bar> < s --> \<bar>f (x+c) + -L\<bar> < r" by simp
+    "\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> (a-c) & \<bar>x + -(a-c)\<bar> < s --> norm (f (x+c) + -L) < r" by simp
   thus ?thesis by (fold LIM_def)
 qed
 
diff -r ba543692bfa1 -r 2c31dd358c21 src/HOL/Hyperreal/NSA.thy
--- a/src/HOL/Hyperreal/NSA.thy	Sat Sep 16 02:35:58 2006 +0200
+++ b/src/HOL/Hyperreal/NSA.thy	Sat Sep 16 02:40:00 2006 +0200
@@ -25,7 +25,8 @@
   HInfinite :: "('a::real_normed_vector) star set"
   "HInfinite = {x. \<forall>r \<in> Reals. r < hnorm x}"
 
-  approx :: "[hypreal, hypreal] => bool"    (infixl "@=" 50)
+  approx :: "['a::real_normed_vector star, 'a star] => bool"
+    (infixl "@=" 50)
     --{*the `infinitely close' relation*}
   "(x @= y) = ((x + -y) \<in> Infinitesimal)"
 
@@ -33,10 +34,10 @@
     --{*the standard part of a hyperreal*}
   "st = (%x. @r. x \<in> HFinite & r \<in> Reals & r @= x)"
 
-  monad     :: "hypreal => hypreal set"
+  monad     :: "'a::real_normed_vector star => 'a star set"
   "monad x = {y. x @= y}"
 
-  galaxy    :: "hypreal => hypreal set"
+  galaxy    :: "'a::real_normed_vector star => 'a star set"
   "galaxy x = {y. (x + -y) \<in> HFinite}"
 
 const_syntax (xsymbols)
@@ -609,7 +610,7 @@
 lemma approx_refl [iff]: "x @= x"
 by (simp add: approx_def Infinitesimal_def)
 
-lemma hypreal_minus_distrib1: "-(y + -(x::hypreal)) = x + -y"
+lemma hypreal_minus_distrib1: "-(y + -(x::'a::ab_group_add)) = x + -y"
 by (simp add: add_commute)
 
 lemma approx_sym: "x @= y ==> y @= x"
@@ -689,7 +690,7 @@
 lemma approx_add: "[| a @= b; c @= d |] ==> a+c @= b+d"
 proof (unfold approx_def)
   assume inf: "a + - b \<in> Infinitesimal" "c + - d \<in> Infinitesimal"
-  have "a + c + - (b + d) = (a + - b) + (c + - d)" by arith
+  have "a + c + - (b + d) = (a + - b) + (c + - d)" by simp
   also have "... \<in> Infinitesimal" using inf by (rule Infinitesimal_add)
   finally show "a + c + - (b + d) \<in> Infinitesimal" .
 qed
@@ -709,23 +710,38 @@
 lemma approx_add_minus: "[| a @= b; c @= d |] ==> a + -c @= b + -d"
 by (blast intro!: approx_add approx_minus)
 
-lemma approx_mult1: "[| a @= b; c: HFinite|] ==> a*c @= b*c"
+lemma approx_mult1:
+  fixes a b c :: "'a::real_normed_algebra star"
+  shows "[| a @= b; c: HFinite|] ==> a*c @= b*c"
 by (simp add: approx_def Infinitesimal_HFinite_mult minus_mult_left 
               left_distrib [symmetric] 
          del: minus_mult_left [symmetric])
 
-lemma approx_mult2: "[|a @= b; c: HFinite|] ==> c*a @= c*b"
-by (simp add: approx_mult1 mult_commute)
+lemma approx_mult2:
+  fixes a b c :: "'a::real_normed_algebra star"
+  shows "[|a @= b; c: HFinite|] ==> c*a @= c*b"
+by (simp add: approx_def Infinitesimal_HFinite_mult2 minus_mult_right 
+              right_distrib [symmetric] 
+         del: minus_mult_right [symmetric])
 
-lemma approx_mult_subst: "[|u @= v*x; x @= y; v \<in> HFinite|] ==> u @= v*y"
+lemma approx_mult_subst:
+  fixes u v x y :: "'a::real_normed_algebra star"
+  shows "[|u @= v*x; x @= y; v \<in> HFinite|] ==> u @= v*y"
 by (blast intro: approx_mult2 approx_trans)
 
-lemma approx_mult_subst2: "[| u @= x*v; x @= y; v \<in> HFinite |] ==> u @= y*v"
+lemma approx_mult_subst2:
+  fixes u v x y :: "'a::real_normed_algebra star"
+  shows "[| u @= x*v; x @= y; v \<in> HFinite |] ==> u @= y*v"
 by (blast intro: approx_mult1 approx_trans)
 
+lemma approx_mult_subst_star_of:
+  fixes u x y :: "'a::real_normed_algebra star"
+  shows "[| u @= x*star_of v; x @= y |] ==> u @= y*star_of v"
+by (auto intro: approx_mult_subst2)
+
 lemma approx_mult_subst_SReal:
      "[| u @= x*hypreal_of_real v; x @= y |] ==> u @= y*hypreal_of_real v"
-by (auto intro: approx_mult_subst2)
+by (rule approx_mult_subst_star_of)
 
 lemma approx_eq_imp: "a = b ==> a @= b"
 by (simp add: approx_def)
@@ -802,51 +818,60 @@
 apply (auto simp add: add_assoc)
 done
 
-lemma approx_hypreal_of_real_HFinite: "x @= hypreal_of_real D ==> x \<in> HFinite"
+lemma approx_star_of_HFinite: "x @= star_of D ==> x \<in> HFinite"
 by (rule approx_sym [THEN [2] approx_HFinite], auto)
 
+lemma approx_hypreal_of_real_HFinite: "x @= hypreal_of_real D ==> x \<in> HFinite"
+by (rule approx_star_of_HFinite)
+
 lemma approx_mult_HFinite:
-     "[|a @= b; c @= d; b: HFinite; d: HFinite|] ==> a*c @= b*d"
+  fixes a b c d :: "'a::real_normed_algebra star"
+  shows "[|a @= b; c @= d; b: HFinite; d: HFinite|] ==> a*c @= b*d"
 apply (rule approx_trans)
 apply (rule_tac [2] approx_mult2)
 apply (rule approx_mult1)
 prefer 2 apply (blast intro: approx_HFinite approx_sym, auto)
 done
 
+lemma approx_mult_star_of:
+  fixes a c :: "'a::real_normed_algebra star"
+  shows "[|a @= star_of b; c @= star_of d |]
+      ==> a*c @= star_of b*star_of d"
+by (blast intro!: approx_mult_HFinite approx_star_of_HFinite HFinite_star_of)
+
 lemma approx_mult_hypreal_of_real:
      "[|a @= hypreal_of_real b; c @= hypreal_of_real d |]
       ==> a*c @= hypreal_of_real b*hypreal_of_real d"
-by (blast intro!: approx_mult_HFinite approx_hypreal_of_real_HFinite 
-                  HFinite_hypreal_of_real)
+by (rule approx_mult_star_of)
 
 lemma approx_SReal_mult_cancel_zero:
-     "[| a \<in> Reals; a \<noteq> 0; a*x @= 0 |] ==> x @= 0"
+     "[| (a::hypreal) \<in> Reals; a \<noteq> 0; a*x @= 0 |] ==> x @= 0"
 apply (drule SReal_inverse [THEN SReal_subset_HFinite [THEN subsetD]])
 apply (auto dest: approx_mult2 simp add: mult_assoc [symmetric])
 done
 
-lemma approx_mult_SReal1: "[| a \<in> Reals; x @= 0 |] ==> x*a @= 0"
+lemma approx_mult_SReal1: "[| (a::hypreal) \<in> Reals; x @= 0 |] ==> x*a @= 0"
 by (auto dest: SReal_subset_HFinite [THEN subsetD] approx_mult1)
 
-lemma approx_mult_SReal2: "[| a \<in> Reals; x @= 0 |] ==> a*x @= 0"
+lemma approx_mult_SReal2: "[| (a::hypreal) \<in> Reals; x @= 0 |] ==> a*x @= 0"
 by (auto dest: SReal_subset_HFinite [THEN subsetD] approx_mult2)
 
 lemma approx_mult_SReal_zero_cancel_iff [simp]:
-     "[|a \<in> Reals; a \<noteq> 0 |] ==> (a*x @= 0) = (x @= 0)"
+     "[|(a::hypreal) \<in> Reals; a \<noteq> 0 |] ==> (a*x @= 0) = (x @= 0)"
 by (blast intro: approx_SReal_mult_cancel_zero approx_mult_SReal2)
 
 lemma approx_SReal_mult_cancel:
-     "[| a \<in> Reals; a \<noteq> 0; a* w @= a*z |] ==> w @= z"
+     "[| (a::hypreal) \<in> Reals; a \<noteq> 0; a* w @= a*z |] ==> w @= z"
 apply (drule SReal_inverse [THEN SReal_subset_HFinite [THEN subsetD]])
 apply (auto dest: approx_mult2 simp add: mult_assoc [symmetric])
 done
 
 lemma approx_SReal_mult_cancel_iff1 [simp]:
-     "[| a \<in> Reals; a \<noteq> 0|] ==> (a* w @= a*z) = (w @= z)"
+     "[| (a::hypreal) \<in> Reals; a \<noteq> 0|] ==> (a* w @= a*z) = (w @= z)"
 by (auto intro!: approx_mult2 SReal_subset_HFinite [THEN subsetD]
          intro: approx_SReal_mult_cancel)
 
-lemma approx_le_bound: "[| z \<le> f; f @= g; g \<le> z |] ==> f @= z"
+lemma approx_le_bound: "[| (z::hypreal) \<le> f; f @= g; g \<le> z |] ==> f @= z"
 apply (simp add: bex_Infinitesimal_iff2 [symmetric], auto)
 apply (rule_tac x = "g+y-z" in bexI)
 apply (simp (no_asm))
@@ -905,6 +930,10 @@
 apply simp
 done
 
+lemma star_of_HFinite_diff_Infinitesimal:
+     "x \<noteq> 0 ==> star_of x \<in> HFinite - Infinitesimal"
+by simp
+
 lemma hypreal_of_real_Infinitesimal_iff_0:
      "(hypreal_of_real x \<in> Infinitesimal) = (x=0)"
 by (rule star_of_Infinitesimal_iff_0)
@@ -920,7 +949,8 @@
 apply simp
 done
 
-lemma approx_SReal_not_zero: "[| y \<in> Reals; x @= y; y\<noteq> 0 |] ==> x \<noteq> 0"
+lemma approx_SReal_not_zero:
+  "[| (y::hypreal) \<in> Reals; x @= y; y\<noteq> 0 |] ==> x \<noteq> 0"
 apply (cut_tac x = 0 and y = y in linorder_less_linear, simp)
 apply (blast dest: approx_sym [THEN mem_infmal_iff [THEN iffD2]] SReal_not_Infinitesimal SReal_minus_not_Infinitesimal)
 done
@@ -958,7 +988,16 @@
 
 subsection{* Uniqueness: Two Infinitely Close Reals are Equal*}
 
-lemma SReal_approx_iff: "[|x \<in> Reals; y \<in> Reals|] ==> (x @= y) = (x = y)"
+lemma star_of_approx_iff [simp]: "(star_of x @= star_of y) = (x = y)"
+apply safe
+apply (simp add: approx_def)
+apply (simp only: star_of_minus [symmetric] star_of_add [symmetric])
+apply (simp only: star_of_Infinitesimal_iff_0)
+apply (simp only: diff_minus [symmetric] right_minus_eq)
+done
+
+lemma SReal_approx_iff:
+  "[|(x::hypreal) \<in> Reals; y \<in> Reals|] ==> (x @= y) = (x = y)"
 apply auto
 apply (simp add: approx_def)
 apply (drule_tac x = y in SReal_minus)
@@ -969,23 +1008,31 @@
 done
 
 lemma number_of_approx_iff [simp]:
-     "(number_of v @= number_of w) = (number_of v = (number_of w :: hypreal))"
-by (auto simp add: SReal_approx_iff)
+     "(number_of v @= (number_of w :: 'a::{number,real_normed_vector} star)) =
+      (number_of v = (number_of w :: 'a))"
+apply (unfold star_number_def)
+apply (rule star_of_approx_iff)
+done
 
 (*And also for 0 @= #nn and 1 @= #nn, #nn @= 0 and #nn @= 1.*)
-lemma [simp]: "(0 @= number_of w) = ((number_of w :: hypreal) = 0)"
-              "(number_of w @= 0) = ((number_of w :: hypreal) = 0)"
-              "(1 @= number_of w) = ((number_of w :: hypreal) = 1)"
-              "(number_of w @= 1) = ((number_of w :: hypreal) = 1)"
-              "~ (0 @= 1)" "~ (1 @= 0)"
-by (auto simp only: SReal_number_of SReal_approx_iff Reals_0 Reals_1)
+lemma [simp]:
+  "(number_of w @= (0::'a::{number,real_normed_vector} star)) =
+   (number_of w = (0::'a))"
+  "((0::'a::{number,real_normed_vector} star) @= number_of w) =
+   (number_of w = (0::'a))"
+  "(number_of w @= (1::'b::{number,one,real_normed_vector} star)) =
+   (number_of w = (1::'b))"
+  "((1::'b::{number,one,real_normed_vector} star) @= number_of w) =
+   (number_of w = (1::'b))"
+  "~ (0 @= (1::'c::{axclass_0_neq_1,real_normed_vector} star))"
+  "~ (1 @= (0::'c::{axclass_0_neq_1,real_normed_vector} star))"
+apply (unfold star_number_def star_zero_def star_one_def)
+apply (unfold star_of_approx_iff)
+by (auto intro: sym)
 
-lemma hypreal_of_real_approx_iff [simp]:
+lemma hypreal_of_real_approx_iff:
      "(hypreal_of_real k @= hypreal_of_real m) = (k = m)"
-apply auto
-apply (rule inj_hypreal_of_real [THEN injD])
-apply (rule SReal_approx_iff [THEN iffD1], auto)
-done
+by (rule star_of_approx_iff)
 
 lemma hypreal_of_real_approx_number_of_iff [simp]:
      "(hypreal_of_real k @= number_of w) = (k = number_of w)"
@@ -998,7 +1045,7 @@
   by (simp_all add:  hypreal_of_real_approx_iff [symmetric])
 
 lemma approx_unique_real:
-     "[| r \<in> Reals; s \<in> Reals; r @= x; s @= x|] ==> r = s"
+     "[| (r::hypreal) \<in> Reals; s \<in> Reals; r @= x; s @= x|] ==> r = s"
 by (blast intro: SReal_approx_iff [THEN iffD1] approx_trans2)
 
 
@@ -1171,13 +1218,13 @@
 done
 
 lemma st_part_Ex:
-     "x \<in> HFinite ==> \<exists>t \<in> Reals. x @= t"
+     "(x::hypreal) \<in> HFinite ==> \<exists>t \<in> Reals. x @= t"
 apply (simp add: approx_def Infinitesimal_def)
 apply (drule lemma_st_part_Ex, auto)
 done
 
 text{*There is a unique real infinitely close*}
-lemma st_part_Ex1: "x \<in> HFinite ==> EX! t. t \<in> Reals & x @= t"
+lemma st_part_Ex1: "x \<in> HFinite ==> EX! t::hypreal. t \<in> Reals & x @= t"
 apply (drule st_part_Ex, safe)
 apply (drule_tac [2] approx_sym, drule_tac [2] approx_sym, drule_tac [2] approx_sym)
 apply (auto intro!: approx_unique_real)
@@ -1247,6 +1294,8 @@
 done
 
 lemma approx_inverse:
+  fixes x y :: "'a::{real_normed_div_algebra,division_by_zero} star"
+  shows
      "[| x @= y; y \<in>  HFinite - Infinitesimal |]
       ==> inverse x @= inverse y"
 apply (frule HFinite_diff_Infinitesimal_approx, assumption)
@@ -1259,15 +1308,20 @@
 done
 
 (*Used for NSLIM_inverse, NSLIMSEQ_inverse*)
+lemmas star_of_approx_inverse = star_of_HFinite_diff_Infinitesimal [THEN [2] approx_inverse]
 lemmas hypreal_of_real_approx_inverse =  hypreal_of_real_HFinite_diff_Infinitesimal [THEN [2] approx_inverse]
 
 lemma inverse_add_Infinitesimal_approx:
+  fixes x h :: "'a::{real_normed_div_algebra,division_by_zero} star"
+  shows
      "[| x \<in> HFinite - Infinitesimal;
          h \<in> Infinitesimal |] ==> inverse(x + h) @= inverse x"
 apply (auto intro: approx_inverse approx_sym Infinitesimal_add_approx_self)
 done
 
 lemma inverse_add_Infinitesimal_approx2:
+  fixes x h :: "'a::{real_normed_div_algebra,division_by_zero} star"
+  shows
      "[| x \<in> HFinite - Infinitesimal;
          h \<in> Infinitesimal |] ==> inverse(h + x) @= inverse x"
 apply (rule add_commute [THEN subst])
@@ -1275,6 +1329,8 @@
 done
 
 lemma inverse_add_Infinitesimal_approx_Infinitesimal:
+  fixes x h :: "'a::{real_normed_div_algebra,division_by_zero} star"
+  shows
      "[| x \<in> HFinite - Infinitesimal;
          h \<in> Infinitesimal |] ==> inverse(x + h) + -inverse x @= h"
 apply (rule approx_trans2)
@@ -1305,7 +1361,8 @@
 by (auto simp add: HInfinite_HFinite_iff)
 
 lemma approx_HFinite_mult_cancel:
-     "[| a: HFinite-Infinitesimal; a* w @= a*z |] ==> w @= z"
+  fixes a w z :: "'a::{real_normed_div_algebra,division_by_zero} star"
+  shows "[| a: HFinite-Infinitesimal; a* w @= a*z |] ==> w @= z"
 apply safe
 apply (frule HFinite_inverse, assumption)
 apply (drule not_Infinitesimal_not_zero)
@@ -1313,7 +1370,8 @@
 done
 
 lemma approx_HFinite_mult_cancel_iff1:
-     "a: HFinite-Infinitesimal ==> (a * w @= a * z) = (w @= z)"
+  fixes a w z :: "'a::{real_normed_div_algebra,division_by_zero} star"
+  shows "a: HFinite-Infinitesimal ==> (a * w @= a * z) = (w @= z)"
 by (auto intro: approx_mult2 approx_HFinite_mult_cancel)
 
 lemma HInfinite_HFinite_add_cancel:
@@ -1376,13 +1434,13 @@
 apply (simp (no_asm) add: HInfinite_HFinite_iff)
 done
 
-lemma approx_hrabs_disj: "abs x @= x | abs x @= -x"
+lemma approx_hrabs_disj: "abs (x::hypreal) @= x | abs x @= -x"
 by (cut_tac x = x in hrabs_disj, auto)
 
 
 subsection{*Theorems about Monads*}
 
-lemma monad_hrabs_Un_subset: "monad (abs x) \<le> monad(x) Un monad(-x)"
+lemma monad_hrabs_Un_subset: "monad (abs x) \<le> monad(x::hypreal) Un monad(-x)"
 by (rule_tac x1 = x in hrabs_disj [THEN disjE], auto)
 
 lemma Infinitesimal_monad_eq: "e \<in> Infinitesimal ==> monad (x+e) = monad x"
@@ -1398,7 +1456,7 @@
 apply (simp (no_asm) add: Infinitesimal_monad_zero_iff [symmetric])
 done
 
-lemma monad_zero_hrabs_iff: "(x \<in> monad 0) = (abs x \<in> monad 0)"
+lemma monad_zero_hrabs_iff: "((x::hypreal) \<in> monad 0) = (abs x \<in> monad 0)"
 apply (rule_tac x1 = x in hrabs_disj [THEN disjE])
 apply (auto simp add: monad_zero_minus_iff [symmetric])
 done
@@ -1436,7 +1494,7 @@
 done
 
 lemma Infinitesimal_approx_hrabs:
-     "[| x @= y; x \<in> Infinitesimal |] ==> abs x @= abs y"
+     "[| x @= y; (x::hypreal) \<in> Infinitesimal |] ==> abs x @= abs y"
 apply (drule Infinitesimal_monad_zero_iff [THEN iffD1])
 apply (blast intro: approx_mem_monad_zero monad_zero_hrabs_iff [THEN iffD1] mem_monad_approx approx_trans3)
 done
@@ -1449,28 +1507,28 @@
 done
 
 lemma Ball_mem_monad_gt_zero:
-     "[| 0 < x;  x \<notin> Infinitesimal; u \<in> monad x |] ==> 0 < u"
+     "[| 0 < (x::hypreal);  x \<notin> Infinitesimal; u \<in> monad x |] ==> 0 < u"
 apply (drule mem_monad_approx [THEN approx_sym])
 apply (erule bex_Infinitesimal_iff2 [THEN iffD2, THEN bexE])
 apply (drule_tac e = "-xa" in less_Infinitesimal_less, auto)
 done
 
 lemma Ball_mem_monad_less_zero:
-     "[| x < 0; x \<notin> Infinitesimal; u \<in> monad x |] ==> u < 0"
+     "[| (x::hypreal) < 0; x \<notin> Infinitesimal; u \<in> monad x |] ==> u < 0"
 apply (drule mem_monad_approx [THEN approx_sym])
 apply (erule bex_Infinitesimal_iff [THEN iffD2, THEN bexE])
 apply (cut_tac x = "-x" and e = xa in less_Infinitesimal_less, auto)
 done
 
 lemma lemma_approx_gt_zero:
-     "[|0 < x; x \<notin> Infinitesimal; x @= y|] ==> 0 < y"
+     "[|0 < (x::hypreal); x \<notin> Infinitesimal; x @= y|] ==> 0 < y"
 by (blast dest: Ball_mem_monad_gt_zero approx_subset_monad)
 
 lemma lemma_approx_less_zero:
-     "[|x < 0; x \<notin> Infinitesimal; x @= y|] ==> y < 0"
+     "[|(x::hypreal) < 0; x \<notin> Infinitesimal; x @= y|] ==> y < 0"
 by (blast dest: Ball_mem_monad_less_zero approx_subset_monad)
 
-theorem approx_hrabs: "x @= y ==> abs x @= abs y"
+theorem approx_hrabs: "(x::hypreal) @= y ==> abs x @= abs y"
 apply (case_tac "x \<in> Infinitesimal") 
 apply (simp add: Infinitesimal_approx_hrabs)
 apply (rule linorder_cases [of 0 x])  
@@ -1478,20 +1536,21 @@
 apply (auto simp add: lemma_approx_less_zero [of x y] abs_of_neg)
 done
 
-lemma approx_hrabs_zero_cancel: "abs(x) @= 0 ==> x @= 0"
+lemma approx_hrabs_zero_cancel: "abs(x::hypreal) @= 0 ==> x @= 0"
 apply (cut_tac x = x in hrabs_disj)
 apply (auto dest: approx_minus)
 done
 
-lemma approx_hrabs_add_Infinitesimal: "e \<in> Infinitesimal ==> abs x @= abs(x+e)"
+lemma approx_hrabs_add_Infinitesimal:
+  "(e::hypreal) \<in> Infinitesimal ==> abs x @= abs(x+e)"
 by (fast intro: approx_hrabs Infinitesimal_add_approx_self)
 
 lemma approx_hrabs_add_minus_Infinitesimal:
-     "e \<in> Infinitesimal ==> abs x @= abs(x + -e)"
+     "(e::hypreal) \<in> Infinitesimal ==> abs x @= abs(x + -e)"
 by (fast intro: approx_hrabs Infinitesimal_add_minus_approx_self)
 
 lemma hrabs_add_Infinitesimal_cancel:
-     "[| e \<in> Infinitesimal; e' \<in> Infinitesimal;
+     "[| (e::hypreal) \<in> Infinitesimal; e' \<in> Infinitesimal;
          abs(x+e) = abs(y+e')|] ==> abs x @= abs y"
 apply (drule_tac x = x in approx_hrabs_add_Infinitesimal)
 apply (drule_tac x = y in approx_hrabs_add_Infinitesimal)
@@ -1499,7 +1558,7 @@
 done
 
 lemma hrabs_add_minus_Infinitesimal_cancel:
-     "[| e \<in> Infinitesimal; e' \<in> Infinitesimal;
+     "[| (e::hypreal) \<in> Infinitesimal; e' \<in> Infinitesimal;
          abs(x + -e) = abs(y + -e')|] ==> abs x @= abs y"
 apply (drule_tac x = x in approx_hrabs_add_minus_Infinitesimal)
 apply (drule_tac x = y in approx_hrabs_add_minus_Infinitesimal)
@@ -1857,55 +1916,45 @@
 
 subsection{*Alternative Definitions for @{term HFinite} using Free Ultrafilter*}
 
-lemma FreeUltrafilterNat_Rep_hypreal:
-     "[| X \<in> Rep_star x; Y \<in> Rep_star x |]
-      ==> {n. X n = Y n} \<in> FreeUltrafilterNat"
-by (cases x, unfold star_n_def, auto, ultra)
-
 lemma HFinite_FreeUltrafilterNat:
-    "(x::hypreal) \<in> HFinite 
-     ==> \<exists>X \<in> Rep_star x. \<exists>u. {n. abs (X n) < u} \<in> FreeUltrafilterNat"
-apply (cases x)
-apply (auto simp add: HFinite_def abs_less_iff minus_less_iff [of x] 
-              star_of_def
-              star_n_less SReal_iff star_n_minus)
-apply (rule_tac x=X in bexI)
-apply (rule_tac x=y in exI, ultra)
-apply simp
+    "star_n X \<in> HFinite 
+     ==> \<exists>u. {n. norm (X n) < u} \<in> FreeUltrafilterNat"
+apply (auto simp add: HFinite_def SReal_def)
+apply (rule_tac x=r in exI)
+apply (simp add: hnorm_def star_of_def starfun_star_n)
+apply (simp add: star_less_def starP2_star_n)
 done
 
 lemma FreeUltrafilterNat_HFinite:
-     "\<exists>X \<in> Rep_star x.
-       \<exists>u. {n. abs (X n) < u} \<in> FreeUltrafilterNat
-       ==>  (x::hypreal) \<in> HFinite"
-apply (cases x)
-apply (auto simp add: HFinite_def abs_less_iff minus_less_iff [of x])
-apply (rule_tac x = "hypreal_of_real u" in bexI)
-apply (auto simp add: star_n_less SReal_iff star_n_minus star_of_def)
-apply ultra+
+     "\<exists>u. {n. norm (X n) < u} \<in> FreeUltrafilterNat
+       ==>  star_n X \<in> HFinite"
+apply (auto simp add: HFinite_def mem_Rep_star_iff)
+apply (rule_tac x="star_of u" in bexI)
+apply (simp add: hnorm_def starfun_star_n star_of_def)
+apply (simp add: star_less_def starP2_star_n)
+apply (simp add: SReal_def)
 done
 
 lemma HFinite_FreeUltrafilterNat_iff:
-     "((x::hypreal) \<in> HFinite) = (\<exists>X \<in> Rep_star x.
-           \<exists>u. {n. abs (X n) < u} \<in> FreeUltrafilterNat)"
+     "(star_n X \<in> HFinite) = (\<exists>u. {n. norm (X n) < u} \<in> FreeUltrafilterNat)"
 by (blast intro!: HFinite_FreeUltrafilterNat FreeUltrafilterNat_HFinite)
 
 
 subsection{*Alternative Definitions for @{term HInfinite} using Free Ultrafilter*}
 
-lemma lemma_Compl_eq: "- {n. (u::real) < abs (xa n)} = {n. abs (xa n) \<le> u}"
+lemma lemma_Compl_eq: "- {n. u < norm (xa n)} = {n. norm (xa n) \<le> u}"
 by auto
 
-lemma lemma_Compl_eq2: "- {n. abs (xa n) < (u::real)} = {n. u \<le> abs (xa n)}"
+lemma lemma_Compl_eq2: "- {n. norm (xa n) < u} = {n. u \<le> norm (xa n)}"
 by auto
 
 lemma lemma_Int_eq1:
-     "{n. abs (xa n) \<le> (u::real)} Int {n. u \<le> abs (xa n)}
-          = {n. abs(xa n) = u}"
+     "{n. norm (xa n) \<le> u} Int {n. u \<le> norm (xa n)}
+          = {n. norm(xa n) = u}"
 by auto
 
 lemma lemma_FreeUltrafilterNat_one:
-     "{n. abs (xa n) = u} \<le> {n. abs (xa n) < u + (1::real)}"
+     "{n. norm (xa n) = u} \<le> {n. norm (xa n) < u + (1::real)}"
 by auto
 
 (*-------------------------------------
@@ -1913,87 +1962,63 @@
   ultrafilter for Infinite numbers!
  -------------------------------------*)
 lemma FreeUltrafilterNat_const_Finite:
-     "[| xa: Rep_star x;
-                  {n. abs (xa n) = u} \<in> FreeUltrafilterNat
-               |] ==> (x::hypreal) \<in> HFinite"
+     "{n. norm (X n) = u} \<in> FreeUltrafilterNat ==> star_n X \<in> HFinite"
 apply (rule FreeUltrafilterNat_HFinite)
-apply (rule_tac x = xa in bexI)
 apply (rule_tac x = "u + 1" in exI)
-apply (ultra, assumption)
+apply (erule ultra, simp)
 done
 
 lemma HInfinite_FreeUltrafilterNat:
-     "(x::hypreal) \<in> HInfinite ==> \<exists>X \<in> Rep_star x.
-           \<forall>u. {n. u < abs (X n)} \<in> FreeUltrafilterNat"
-apply (frule HInfinite_HFinite_iff [THEN iffD1])
-apply (cut_tac x = x in Rep_hypreal_nonempty)
-apply (auto simp del: Rep_hypreal_nonempty simp add: HFinite_FreeUltrafilterNat_iff Bex_def)
-apply (drule spec)+
-apply auto
-apply (drule_tac x = u in spec)
-apply (drule FreeUltrafilterNat_Compl_mem)+
-apply (drule FreeUltrafilterNat_Int, assumption)
-apply (simp add: lemma_Compl_eq lemma_Compl_eq2 lemma_Int_eq1)
-apply (auto dest: FreeUltrafilterNat_const_Finite simp
-      add: HInfinite_HFinite_iff [THEN iffD1])
+     "star_n X \<in> HInfinite ==> \<forall>u. {n. u < norm (X n)} \<in> FreeUltrafilterNat"
+apply (drule HInfinite_HFinite_iff [THEN iffD1])
+apply (simp add: HFinite_FreeUltrafilterNat_iff)
+apply (rule allI, drule_tac x="u + 1" in spec)
+apply (drule FreeUltrafilterNat_Compl_mem)
+apply (simp add: Collect_neg_eq [symmetric] linorder_not_less)
+apply (erule ultra, simp)
 done
 
 lemma lemma_Int_HI:
-     "{n. abs (Xa n) < u} Int {n. X n = Xa n} \<subseteq> {n. abs (X n) < (u::real)}"
+     "{n. norm (Xa n) < u} Int {n. X n = Xa n} \<subseteq> {n. norm (X n) < (u::real)}"
 by auto
 
-lemma lemma_Int_HIa: "{n. u < abs (X n)} Int {n. abs (X n) < (u::real)} = {}"
+lemma lemma_Int_HIa: "{n. u < norm (X n)} Int {n. norm (X n) < u} = {}"
 by (auto intro: order_less_asym)
 
 lemma FreeUltrafilterNat_HInfinite:
-     "\<exists>X \<in> Rep_star x. \<forall>u.
-               {n. u < abs (X n)} \<in> FreeUltrafilterNat
-               ==>  (x::hypreal) \<in> HInfinite"
+     "\<forall>u. {n. u < norm (X n)} \<in> FreeUltrafilterNat ==> star_n X \<in> HInfinite"
 apply (rule HInfinite_HFinite_iff [THEN iffD2])
-apply (safe, drule HFinite_FreeUltrafilterNat, auto)
+apply (safe, drule HFinite_FreeUltrafilterNat, safe)
 apply (drule_tac x = u in spec)
-apply (drule FreeUltrafilterNat_Rep_hypreal, assumption)
-apply (drule_tac Y = "{n. X n = Xa n}" in FreeUltrafilterNat_Int, simp) 
-apply (drule lemma_Int_HI [THEN [2] FreeUltrafilterNat_subset])
-apply (drule_tac Y = "{n. abs (X n) < u}" in FreeUltrafilterNat_Int)
-apply (auto simp add: lemma_Int_HIa)
+apply ultra
 done
 
 lemma HInfinite_FreeUltrafilterNat_iff:
-     "((x::hypreal) \<in> HInfinite) = (\<exists>X \<in> Rep_star x.
-           \<forall>u. {n. u < abs (X n)} \<in> FreeUltrafilterNat)"
+     "(star_n X \<in> HInfinite) = (\<forall>u. {n. u < norm (X n)} \<in> FreeUltrafilterNat)"
 by (blast intro!: HInfinite_FreeUltrafilterNat FreeUltrafilterNat_HInfinite)
 
 
 subsection{*Alternative Definitions for @{term Infinitesimal} using Free Ultrafilter*}
 
+lemma ball_SReal_eq: "(\<forall>x::hypreal \<in> Reals. P x) = (\<forall>x::real. P (star_of x))"
+by (unfold SReal_def, auto)
+
 lemma Infinitesimal_FreeUltrafilterNat:
-          "(x::hypreal) \<in> Infinitesimal ==> \<exists>X \<in> Rep_star x.
-           \<forall>u. 0 < u --> {n. abs (X n) < u} \<in> FreeUltrafilterNat"
-apply (simp add: Infinitesimal_def)
-apply (auto simp add: abs_less_iff minus_less_iff [of x])
-apply (cases x)
-apply (auto, rule bexI [OF _ Rep_star_star_n], safe)
-apply (drule star_of_less [THEN iffD2])
-apply (drule_tac x = "hypreal_of_real u" in bspec, auto)
-apply (auto simp add: star_n_less star_n_minus star_of_def, ultra)
+     "star_n X \<in> Infinitesimal ==> \<forall>u>0. {n. norm (X n) < u} \<in> \<U>"
+apply (simp add: Infinitesimal_def ball_SReal_eq)
+apply (simp add: hnorm_def starfun_star_n star_of_def)
+apply (simp add: star_less_def starP2_star_n)
 done
 
 lemma FreeUltrafilterNat_Infinitesimal:
-     "\<exists>X \<in> Rep_star x.
-            \<forall>u. 0 < u --> {n. abs (X n) < u} \<in> FreeUltrafilterNat
-      ==> (x::hypreal) \<in> Infinitesimal"
-apply (simp add: Infinitesimal_def)
-apply (cases x)
-apply (auto simp add: abs_less_iff abs_interval_iff minus_less_iff [of x])
-apply (auto simp add: SReal_iff)
-apply (drule_tac [!] x=y in spec) 
-apply (auto simp add: star_n_less star_n_minus star_of_def, ultra+)
+     "\<forall>u>0. {n. norm (X n) < u} \<in> \<U> ==> star_n X \<in> Infinitesimal"
+apply (simp add: Infinitesimal_def ball_SReal_eq)
+apply (simp add: hnorm_def starfun_star_n star_of_def)
+apply (simp add: star_less_def starP2_star_n)
 done
 
 lemma Infinitesimal_FreeUltrafilterNat_iff:
-     "((x::hypreal) \<in> Infinitesimal) = (\<exists>X \<in> Rep_star x.
-           \<forall>u. 0 < u --> {n. abs (X n) < u} \<in> FreeUltrafilterNat)"
+     "(star_n X \<in> Infinitesimal) = (\<forall>u>0. {n. norm (X n) < u} \<in> \<U>)"
 by (blast intro!: Infinitesimal_FreeUltrafilterNat FreeUltrafilterNat_Infinitesimal)
 
 (*------------------------------------------------------------------------
@@ -2028,7 +2053,7 @@
 
 
 lemma Infinitesimal_hypreal_of_nat_iff:
-     "Infinitesimal = {x. \<forall>n. abs x < inverse (hypreal_of_nat (Suc n))}"
+     "Infinitesimal = {x. \<forall>n. hnorm x < inverse (hypreal_of_nat (Suc n))}"
 apply (simp add: Infinitesimal_def)
 apply (auto simp add: lemma_Infinitesimal2)
 done
@@ -2098,11 +2123,9 @@
 done
 
 theorem HInfinite_omega [simp]: "omega \<in> HInfinite"
-apply (simp add: omega_def star_n_def)
-apply (auto intro!: FreeUltrafilterNat_HInfinite)
-apply (rule bexI)
-apply (rule_tac [2] lemma_starrel_refl, auto)
-apply (simp (no_asm) add: real_of_nat_Suc diff_less_eq [symmetric] FreeUltrafilterNat_omega)
+apply (simp add: omega_def)
+apply (rule FreeUltrafilterNat_HInfinite)
+apply (simp (no_asm) add: real_norm_def real_of_nat_Suc diff_less_eq [symmetric] FreeUltrafilterNat_omega)
 done
 
 (*-----------------------------------------------
@@ -2202,27 +2225,30 @@
     |X(n) - x| < 1/n ==> [<X n>] - hypreal_of_real x| \<in> Infinitesimal
  -----------------------------------------------------*)
 lemma real_seq_to_hypreal_Infinitesimal:
-     "\<forall>n. abs(X n + -x) < inverse(real(Suc n))
-     ==> star_n X + -hypreal_of_real x \<in> Infinitesimal"
+     "\<forall>n. norm(X n + -x) < inverse(real(Suc n))
+     ==> star_n X + -star_of x \<in> Infinitesimal"
 apply (auto intro!: bexI dest: FreeUltrafilterNat_inverse_real_of_posnat FreeUltrafilterNat_all FreeUltrafilterNat_Int intro: order_less_trans FreeUltrafilterNat_subset simp add: star_n_minus star_of_def star_n_add Infinitesimal_FreeUltrafilterNat_iff star_n_inverse)
 done
 
 lemma real_seq_to_hypreal_approx:
-     "\<forall>n. abs(X n + -x) < inverse(real(Suc n))
-      ==> star_n X @= hypreal_of_real x"
+     "\<forall>n. norm(X n + -x) < inverse(real(Suc n))
+      ==> star_n X @= star_of x"
 apply (subst approx_minus_iff)
 apply (rule mem_infmal_iff [THEN subst])
 apply (erule real_seq_to_hypreal_Infinitesimal)
 done
 
 lemma real_seq_to_hypreal_approx2:
-     "\<forall>n. abs(x + -X n) < inverse(real(Suc n))
-               ==> star_n X @= hypreal_of_real x"
-apply (simp add: abs_minus_add_cancel real_seq_to_hypreal_approx)
+     "\<forall>n. norm(x + -X n) < inverse(real(Suc n))
+               ==> star_n X @= star_of x"
+apply (rule real_seq_to_hypreal_approx)
+apply (subst norm_minus_cancel [symmetric])
+apply (simp del: norm_minus_cancel)
+apply (subst add_commute, assumption)
 done
 
 lemma real_seq_to_hypreal_Infinitesimal2:
-     "\<forall>n. abs(X n + -Y n) < inverse(real(Suc n))
+     "\<forall>n. norm(X n + -Y n) < inverse(real(Suc n))
       ==> star_n X + -star_n Y \<in> Infinitesimal"
 by (auto intro!: bexI
 	 dest: FreeUltrafilterNat_inverse_real_of_posnat 
diff -r ba543692bfa1 -r 2c31dd358c21 src/HOL/Hyperreal/SEQ.thy
--- a/src/HOL/Hyperreal/SEQ.thy	Sat Sep 16 02:35:58 2006 +0200
+++ b/src/HOL/Hyperreal/SEQ.thy	Sat Sep 16 02:40:00 2006 +0200
@@ -14,13 +14,15 @@
 
 definition
 
-  LIMSEQ :: "[nat=>real,real] => bool"    ("((_)/ ----> (_))" [60, 60] 60)
+  LIMSEQ :: "[nat => 'a::real_normed_vector, 'a] => bool"
+    ("((_)/ ----> (_))" [60, 60] 60)
     --{*Standard definition of convergence of sequence*}
-  "X ----> L = (\<forall>r. 0 < r --> (\<exists>no. \<forall>n. no \<le> n --> \<bar>X n + -L\<bar> < r))"
+  "X ----> L = (\<forall>r. 0 < r --> (\<exists>no. \<forall>n. no \<le> n --> norm (X n + -L) < r))"
 
-  NSLIMSEQ :: "[nat=>real,real] => bool"    ("((_)/ ----NS> (_))" [60, 60] 60)
+  NSLIMSEQ :: "[nat => 'a::real_normed_vector, 'a] => bool"
+    ("((_)/ ----NS> (_))" [60, 60] 60)
     --{*Nonstandard definition of convergence of sequence*}
-  "X ----NS> L = (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> hypreal_of_real L)"
+  "X ----NS> L = (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> star_of L)"
 
   lim :: "(nat => real) => real"
     --{*Standard definition of limit using choice operator*}
@@ -30,19 +32,19 @@
     --{*Nonstandard definition of limit using choice operator*}
   "nslim X = (SOME L. (X ----NS> L))"
 
-  convergent :: "(nat => real) => bool"
+  convergent :: "(nat => 'a::real_normed_vector) => bool"
     --{*Standard definition of convergence*}
   "convergent X = (\<exists>L. (X ----> L))"
 
-  NSconvergent :: "(nat => real) => bool"
+  NSconvergent :: "(nat => 'a::real_normed_vector) => bool"
     --{*Nonstandard definition of convergence*}
   "NSconvergent X = (\<exists>L. (X ----NS> L))"
 
-  Bseq :: "(nat => real) => bool"
+  Bseq :: "(nat => 'a::real_normed_vector) => bool"
     --{*Standard definition for bounded sequence*}
-  "Bseq X = (\<exists>K>0.\<forall>n. \<bar>X n\<bar> \<le> K)"
+  "Bseq X = (\<exists>K>0.\<forall>n. norm (X n) \<le> K)"
 
-  NSBseq :: "(nat=>real) => bool"
+  NSBseq :: "(nat => 'a::real_normed_vector) => bool"
     --{*Nonstandard definition for bounded sequence*}
   "NSBseq X = (\<forall>N \<in> HNatInfinite. ( *f* X) N : HFinite)"
 
@@ -54,15 +56,16 @@
     --{*Definition of subsequence*}
   "subseq f = (\<forall>m. \<forall>n>m. (f m) < (f n))"
 
-  Cauchy :: "(nat => real) => bool"
+  Cauchy :: "(nat => 'a::real_normed_vector) => bool"
     --{*Standard definition of the Cauchy condition*}
-  "Cauchy X = (\<forall>e>0. \<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. abs((X m) + -(X n)) < e)"
+  "Cauchy X = (\<forall>e>0. \<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. norm((X m) + -(X n)) < e)"
 
-  NSCauchy :: "(nat => real) => bool"
+  NSCauchy :: "(nat => 'a::real_normed_vector) => bool"
     --{*Nonstandard definition*}
   "NSCauchy X = (\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite. ( *f* X) M \<approx> ( *f* X) N)"
 
 
+declare real_norm_def [simp]
 
 text{* Example of an hypersequence (i.e. an extended standard sequence)
    whose term with an hypernatural suffix is an infinitesimal i.e.
@@ -70,9 +73,8 @@
 
 lemma SEQ_Infinitesimal:
       "( *f* (%n::nat. inverse(real(Suc n)))) whn : Infinitesimal"
-apply (simp add: hypnat_omega_def Infinitesimal_FreeUltrafilterNat_iff starfun)
-apply (simp add: star_n_inverse)
-apply (rule bexI [OF _ Rep_star_star_n])
+apply (simp add: hypnat_omega_def starfun star_n_inverse)
+apply (simp add: Infinitesimal_FreeUltrafilterNat_iff)
 apply (simp add: real_of_nat_Suc_gt_zero FreeUltrafilterNat_inverse_real_of_posnat)
 done
 
@@ -80,28 +82,26 @@
 subsection{*LIMSEQ and NSLIMSEQ*}
 
 lemma LIMSEQ_iff:
-      "(X ----> L) = (\<forall>r>0. \<exists>no. \<forall>n \<ge> no. \<bar>X n + -L\<bar> < r)"
+      "(X ----> L) = (\<forall>r>0. \<exists>no. \<forall>n \<ge> no. norm (X n + -L) < r)"
 by (simp add: LIMSEQ_def)
 
 lemma NSLIMSEQ_iff:
-    "(X ----NS> L) = (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> hypreal_of_real L)"
+    "(X ----NS> L) = (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> star_of L)"
 by (simp add: NSLIMSEQ_def)
 
 
 text{*LIMSEQ ==> NSLIMSEQ*}
-
 lemma LIMSEQ_NSLIMSEQ:
       "X ----> L ==> X ----NS> L"
-apply (simp add: LIMSEQ_def NSLIMSEQ_def)
-apply (auto simp add: HNatInfinite_FreeUltrafilterNat_iff)
+apply (simp add: LIMSEQ_def NSLIMSEQ_def, safe)
 apply (rule_tac x = N in star_cases)
+apply (simp add: HNatInfinite_FreeUltrafilterNat_iff)
 apply (rule approx_minus_iff [THEN iffD2])
 apply (auto simp add: starfun mem_infmal_iff [symmetric] star_of_def
               star_n_minus star_n_add Infinitesimal_FreeUltrafilterNat_iff)
-apply (rule bexI [OF _ Rep_star_star_n], safe)
 apply (drule_tac x = u in spec, safe)
-apply (drule_tac x = no in spec, fuf)
-apply (blast dest: less_imp_le)
+apply (drule_tac x = no in spec)
+apply (erule ultra, simp add: less_imp_le)
 done
 
 
@@ -148,29 +148,24 @@
 lemma HNatInfinite_NSLIMSEQ: "\<forall>n. n \<le> f n
           ==> star_n f : HNatInfinite"
 apply (auto simp add: HNatInfinite_FreeUltrafilterNat_iff)
-apply (rule bexI [OF _ Rep_star_star_n], safe)
 apply (erule FreeUltrafilterNat_NSLIMSEQ)
 done
 
 lemma lemmaLIM:
-     "{n. X (f n) + - L = Y n} Int {n. \<bar>Y n\<bar> < r} \<le>
-      {n. \<bar>X (f n) + - L\<bar> < r}"
+     "{n. X (f n) + - L = Y n} Int {n. norm (Y n) < r} \<le>
+      {n. norm (X (f n) + - L) < r}"
 by auto
 
 lemma lemmaLIM2:
-  "{n. \<bar>X (f n) + - L\<bar> < r} Int {n. r \<le> abs (X (f n) + - (L::real))} = {}"
+  "{n. norm (X (f n) + - L) < r} Int {n. r \<le> norm (X (f n) + - L)} = {}"
 by auto
 
-lemma lemmaLIM3: "[| 0 < r; \<forall>n. r \<le> \<bar>X (f n) + - L\<bar>;
+lemma lemmaLIM3: "[| 0 < r; \<forall>n. r \<le> norm (X (f n) + - L);
            ( *f* X) (star_n f) +
-           - hypreal_of_real  L \<approx> 0 |] ==> False"
+           - star_of L \<approx> 0 |] ==> False"
 apply (auto simp add: starfun mem_infmal_iff [symmetric] star_of_def star_n_minus star_n_add Infinitesimal_FreeUltrafilterNat_iff)
-apply (rename_tac "Y")
 apply (drule_tac x = r in spec, safe)
-apply (drule FreeUltrafilterNat_Int, assumption)
-apply (drule lemmaLIM [THEN [2] FreeUltrafilterNat_subset])
 apply (drule FreeUltrafilterNat_all)
-apply (erule_tac V = "{n. \<bar>Y n\<bar> < r} : FreeUltrafilterNat" in thin_rl)
 apply (drule FreeUltrafilterNat_Int, assumption)
 apply (simp add: lemmaLIM2)
 done
@@ -179,7 +174,7 @@
 apply (simp add: LIMSEQ_def NSLIMSEQ_def)
 apply (rule ccontr, simp, safe)
 txt{* skolemization step *}
-apply (drule choice, safe)
+apply (drule no_choice, safe)
 apply (drule_tac x = "star_n f" in bspec)
 apply (drule_tac [2] approx_minus_iff [THEN iffD1])
 apply (simp_all add: linorder_not_less)
@@ -217,11 +212,14 @@
 by (simp add: LIMSEQ_NSLIMSEQ_iff [THEN sym] LIMSEQ_add_const)
 
 lemma NSLIMSEQ_mult:
-      "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n * Y n) ----NS> a * b"
+  fixes a b :: "'a::real_normed_algebra"
+  shows "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n * Y n) ----NS> a * b"
 by (auto intro!: approx_mult_HFinite 
         simp add: NSLIMSEQ_def starfun_mult [symmetric])
 
-lemma LIMSEQ_mult: "[| X ----> a; Y ----> b |] ==> (%n. X n * Y n) ----> a * b"
+lemma LIMSEQ_mult:
+  fixes a b :: "'a::real_normed_algebra"
+  shows "[| X ----> a; Y ----> b |] ==> (%n. X n * Y n) ----> a * b"
 by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_mult)
 
 lemma NSLIMSEQ_minus: "X ----NS> a ==> (%n. -(X n)) ----NS> -a"
@@ -266,22 +264,26 @@
 
 text{*Proof is like that of @{text NSLIM_inverse}.*}
 lemma NSLIMSEQ_inverse:
-     "[| X ----NS> a;  a ~= 0 |] ==> (%n. inverse(X n)) ----NS> inverse(a)"
-by (simp add: NSLIMSEQ_def starfun_inverse [symmetric] 
-              hypreal_of_real_approx_inverse)
+  fixes a :: "'a::{real_normed_div_algebra,division_by_zero}"
+  shows "[| X ----NS> a;  a ~= 0 |] ==> (%n. inverse(X n)) ----NS> inverse(a)"
+by (simp add: NSLIMSEQ_def star_of_approx_inverse)
 
 
 text{*Standard version of theorem*}
 lemma LIMSEQ_inverse:
-     "[| X ----> a; a ~= 0 |] ==> (%n. inverse(X n)) ----> inverse(a)"
+  fixes a :: "'a::{real_normed_div_algebra,division_by_zero}"
+  shows "[| X ----> a; a ~= 0 |] ==> (%n. inverse(X n)) ----> inverse(a)"
 by (simp add: NSLIMSEQ_inverse LIMSEQ_NSLIMSEQ_iff)
 
 lemma NSLIMSEQ_mult_inverse:
+  fixes a b :: "'a::{real_normed_div_algebra,field,division_by_zero}"
+  shows
      "[| X ----NS> a;  Y ----NS> b;  b ~= 0 |] ==> (%n. X n / Y n) ----NS> a/b"
 by (simp add: NSLIMSEQ_mult NSLIMSEQ_inverse divide_inverse)
 
 lemma LIMSEQ_divide:
-     "[| X ----> a;  Y ----> b;  b ~= 0 |] ==> (%n. X n / Y n) ----> a/b"
+  fixes a b :: "'a::{real_normed_div_algebra,field,division_by_zero}"
+  shows "[| X ----> a;  Y ----> b;  b ~= 0 |] ==> (%n. X n / Y n) ----> a/b"
 by (simp add: LIMSEQ_mult LIMSEQ_inverse divide_inverse)
 
 text{*Uniqueness of limit*}
@@ -316,6 +318,7 @@
 qed
 
 lemma LIMSEQ_setprod:
+  fixes L :: "'a \<Rightarrow> 'b::{real_normed_algebra,comm_ring_1}"
   assumes n: "\<And>n. n \<in> S \<Longrightarrow> X n ----> L n"
   shows "(\<lambda>m. \<Prod>n\<in>S. X n m) ----> (\<Prod>n\<in>S. L n)"
 proof (cases "finite S")
@@ -455,15 +458,15 @@
 
 subsection{*Bounded Sequence*}
 
-lemma BseqD: "Bseq X ==> \<exists>K. 0 < K & (\<forall>n. \<bar>X n\<bar> \<le> K)"
+lemma BseqD: "Bseq X ==> \<exists>K. 0 < K & (\<forall>n. norm (X n) \<le> K)"
 by (simp add: Bseq_def)
 
-lemma BseqI: "[| 0 < K; \<forall>n. \<bar>X n\<bar> \<le> K |] ==> Bseq X"
+lemma BseqI: "[| 0 < K; \<forall>n. norm (X n) \<le> K |] ==> Bseq X"
 by (auto simp add: Bseq_def)
 
 lemma lemma_NBseq_def:
-     "(\<exists>K > 0. \<forall>n. \<bar>X n\<bar> \<le> K) =
-      (\<exists>N. \<forall>n. \<bar>X n\<bar> \<le> real(Suc N))"
+     "(\<exists>K > 0. \<forall>n. norm (X n) \<le> K) =
+      (\<exists>N. \<forall>n. norm (X n) \<le> real(Suc N))"
 apply auto
  prefer 2 apply force
 apply (cut_tac x = K in reals_Archimedean2, clarify)
@@ -473,13 +476,13 @@
 done
 
 text{* alternative definition for Bseq *}
-lemma Bseq_iff: "Bseq X = (\<exists>N. \<forall>n. \<bar>X n\<bar> \<le> real(Suc N))"
+lemma Bseq_iff: "Bseq X = (\<exists>N. \<forall>n. norm (X n) \<le> real(Suc N))"
 apply (simp add: Bseq_def)
 apply (simp (no_asm) add: lemma_NBseq_def)
 done
 
 lemma lemma_NBseq_def2:
-     "(\<exists>K > 0. \<forall>n. \<bar>X n\<bar> \<le> K) = (\<exists>N. \<forall>n. \<bar>X n\<bar> < real(Suc N))"
+     "(\<exists>K > 0. \<forall>n. norm (X n) \<le> K) = (\<exists>N. \<forall>n. norm (X n) < real(Suc N))"
 apply (subst lemma_NBseq_def, auto)
 apply (rule_tac x = "Suc N" in exI)
 apply (rule_tac [2] x = N in exI)
@@ -489,7 +492,7 @@
 done
 
 (* yet another definition for Bseq *)
-lemma Bseq_iff1a: "Bseq X = (\<exists>N. \<forall>n. \<bar>X n\<bar> < real(Suc N))"
+lemma Bseq_iff1a: "Bseq X = (\<exists>N. \<forall>n. norm (X n) < real(Suc N))"
 by (simp add: Bseq_def lemma_NBseq_def2)
 
 lemma NSBseqD: "[| NSBseq X;  N: HNatInfinite |] ==> ( *f* X) N : HFinite"
@@ -500,7 +503,7 @@
 
 text{*The standard definition implies the nonstandard definition*}
 
-lemma lemma_Bseq: "\<forall>n. \<bar>X n\<bar> \<le> K ==> \<forall>n. abs(X((f::nat=>nat) n)) \<le> K"
+lemma lemma_Bseq: "\<forall>n. norm (X n) \<le> K ==> \<forall>n. norm(X((f::nat=>nat) n)) \<le> K"
 by auto
 
 lemma Bseq_NSBseq: "Bseq X ==> NSBseq X"
@@ -508,7 +511,6 @@
 apply (rule_tac x = N in star_cases)
 apply (auto simp add: starfun HFinite_FreeUltrafilterNat_iff 
                       HNatInfinite_FreeUltrafilterNat_iff)
-apply (rule bexI [OF _ Rep_star_star_n]) 
 apply (drule_tac f = Xa in lemma_Bseq)
 apply (rule_tac x = "K+1" in exI)
 apply (drule_tac P="%n. ?f n \<le> K" in FreeUltrafilterNat_all, ultra)
@@ -525,23 +527,22 @@
    which woulid be useless.*}
 
 lemma lemmaNSBseq:
-     "\<forall>K > 0. \<exists>n. K < \<bar>X n\<bar>
-      ==> \<forall>N. \<exists>n. real(Suc N) < \<bar>X n\<bar>"
+     "\<forall>K > 0. \<exists>n. K < norm (X n)
+      ==> \<forall>N. \<exists>n. real(Suc N) < norm (X n)"
 apply safe
 apply (cut_tac n = N in real_of_nat_Suc_gt_zero, blast)
 done
 
-lemma lemmaNSBseq2: "\<forall>K > 0. \<exists>n. K < \<bar>X n\<bar>
-                     ==> \<exists>f. \<forall>N. real(Suc N) < \<bar>X (f N)\<bar>"
+lemma lemmaNSBseq2: "\<forall>K > 0. \<exists>n::nat. K < norm (X n)
+                     ==> \<exists>f. \<forall>N. real(Suc N) < norm (X (f N))"
 apply (drule lemmaNSBseq)
-apply (drule choice, blast)
+apply (drule no_choice, blast)
 done
 
 lemma real_seq_to_hypreal_HInfinite:
-     "\<forall>N. real(Suc N) < \<bar>X (f N)\<bar>
+     "\<forall>N. real(Suc N) < norm (X (f N))
       ==>  star_n (X o f) : HInfinite"
 apply (auto simp add: HInfinite_FreeUltrafilterNat_iff o_def)
-apply (rule bexI [OF _ Rep_star_star_n], clarify)  
 apply (cut_tac u = u in FreeUltrafilterNat_nat_gt_real)
 apply (drule FreeUltrafilterNat_all)
 apply (erule FreeUltrafilterNat_Int [THEN FreeUltrafilterNat_subset])
@@ -552,29 +553,28 @@
      defined using the skolem function  @{term "f::nat=>nat"} above*}
 
 lemma lemma_finite_NSBseq:
-     "{n. f n \<le> Suc u & real(Suc n) < \<bar>X (f n)\<bar>} \<le>
-      {n. f n \<le> u & real(Suc n) < \<bar>X (f n)\<bar>} Un
-      {n. real(Suc n) < \<bar>X (Suc u)\<bar>}"
+     "{n. f n \<le> Suc u & real(Suc n) < norm (X (f n))} \<le>
+      {n. f n \<le> u & real(Suc n) < norm (X (f n))} Un
+      {n. real(Suc n) < norm (X (Suc u))}"
 by (auto dest!: le_imp_less_or_eq)
 
 lemma lemma_finite_NSBseq2:
-     "finite {n. f n \<le> (u::nat) &  real(Suc n) < \<bar>X(f n)\<bar>}"
+     "finite {n. f n \<le> (u::nat) &  real(Suc n) < norm (X(f n))}"
 apply (induct "u")
 apply (rule_tac [2] lemma_finite_NSBseq [THEN finite_subset])
-apply (rule_tac B = "{n. real (Suc n) < \<bar>X 0\<bar> }" in finite_subset)
+apply (rule_tac B = "{n. real (Suc n) < norm (X 0) }" in finite_subset)
 apply (auto intro: finite_real_of_nat_less_real 
             simp add: real_of_nat_Suc less_diff_eq [symmetric])
 done
 
 lemma HNatInfinite_skolem_f:
-     "\<forall>N. real(Suc N) < \<bar>X (f N)\<bar>
+     "\<forall>N. real(Suc N) < norm (X (f N))
       ==> star_n f : HNatInfinite"
 apply (auto simp add: HNatInfinite_FreeUltrafilterNat_iff)
-apply (rule bexI [OF _ Rep_star_star_n], safe)
 apply (rule ccontr, drule FreeUltrafilterNat_Compl_mem)
 apply (rule lemma_finite_NSBseq2 [THEN FreeUltrafilterNat_finite, THEN notE]) 
-apply (subgoal_tac "{n. f n \<le> u & real (Suc n) < \<bar>X (f n)\<bar>} =
-                    {n. f n \<le> u} \<inter> {N. real (Suc N) < \<bar>X (f N)\<bar>}")
+apply (subgoal_tac "{n. f n \<le> u & real (Suc n) < norm (X (f n))} =
+                    {n. f n \<le> u} \<inter> {N. real (Suc N) < norm (X (f N))}")
 apply (erule ssubst) 
  apply (auto simp add: linorder_not_less Compl_def)
 done
@@ -600,7 +600,7 @@
 
 lemma NSconvergent_NSBseq: "NSconvergent X ==> NSBseq X"
 apply (simp add: NSconvergent_def NSBseq_def NSLIMSEQ_def)
-apply (blast intro: HFinite_hypreal_of_real approx_sym approx_HFinite)
+apply (blast intro: HFinite_star_of approx_sym approx_HFinite)
 done
 
 text{*Standard Version: easily now proved using equivalence of NS and
@@ -624,10 +624,10 @@
    \<exists>U. isLub (UNIV::real set) {x. \<exists>n. X n = x} U"
 by (blast intro: reals_complete Bseq_isUb)
 
-lemma NSBseq_isUb: "NSBseq X ==> \<exists>U. isUb UNIV {x. \<exists>n. X n = x} U"
+lemma NSBseq_isUb: "NSBseq X ==> \<exists>U::real. isUb UNIV {x. \<exists>n. X n = x} U"
 by (simp add: Bseq_NSBseq_iff [symmetric] Bseq_isUb)
 
-lemma NSBseq_isLub: "NSBseq X ==> \<exists>U. isLub UNIV {x. \<exists>n. X n = x} U"
+lemma NSBseq_isLub: "NSBseq X ==> \<exists>U::real. isLub UNIV {x. \<exists>n. X n = x} U"
 by (simp add: Bseq_NSBseq_iff [symmetric] Bseq_isLub)
 
 
@@ -686,7 +686,7 @@
 text{*A standard proof of the theorem for monotone increasing sequence*}
 
 lemma Bseq_mono_convergent:
-     "[| Bseq X; \<forall>m. \<forall>n \<ge> m. X m \<le> X n |] ==> convergent X"
+     "[| Bseq X; \<forall>m. \<forall>n \<ge> m. X m \<le> X n |] ==> convergent (X::nat=>real)"
 apply (simp add: convergent_def)
 apply (frule Bseq_isLub, safe)
 apply (case_tac "\<exists>m. X m = U", auto)
@@ -705,7 +705,7 @@
 text{*Nonstandard version of the theorem*}
 
 lemma NSBseq_mono_NSconvergent:
-     "[| NSBseq X; \<forall>m. \<forall>n \<ge> m. X m \<le> X n |] ==> NSconvergent X"
+     "[| NSBseq X; \<forall>m. \<forall>n \<ge> m. X m \<le> X n |] ==> NSconvergent (X::nat=>real)"
 by (auto intro: Bseq_mono_convergent 
          simp add: convergent_NSconvergent_iff [symmetric] 
                    Bseq_NSBseq_iff [symmetric])
@@ -731,26 +731,31 @@
 subsection{*A Few More Equivalence Theorems for Boundedness*}
 
 text{*alternative formulation for boundedness*}
-lemma Bseq_iff2: "Bseq X = (\<exists>k > 0. \<exists>x. \<forall>n. \<bar>X(n) + -x\<bar> \<le> k)"
+lemma Bseq_iff2: "Bseq X = (\<exists>k > 0. \<exists>x. \<forall>n. norm (X(n) + -x) \<le> k)"
 apply (unfold Bseq_def, safe)
-apply (rule_tac [2] x = "k + \<bar>x\<bar> " in exI)
+apply (rule_tac [2] x = "k + norm x" in exI)
 apply (rule_tac x = K in exI, simp)
 apply (rule exI [where x = 0], auto)
-apply (drule_tac x=n in spec, arith)+
+apply (erule order_less_le_trans, simp)
+apply (drule_tac x=n in spec, fold diff_def)
+apply (drule order_trans [OF norm_triangle_ineq2])
+apply simp
 done
 
 text{*alternative formulation for boundedness*}
-lemma Bseq_iff3: "Bseq X = (\<exists>k > 0. \<exists>N. \<forall>n. abs(X(n) + -X(N)) \<le> k)"
+lemma Bseq_iff3: "Bseq X = (\<exists>k > 0. \<exists>N. \<forall>n. norm(X(n) + -X(N)) \<le> k)"
 apply safe
 apply (simp add: Bseq_def, safe)
-apply (rule_tac x = "K + \<bar>X N\<bar> " in exI)
+apply (rule_tac x = "K + norm (X N)" in exI)
 apply auto
+apply (erule order_less_le_trans, simp)
 apply (rule_tac x = N in exI, safe)
-apply (drule_tac x = n in spec, arith)
+apply (drule_tac x = n in spec)
+apply (rule order_trans [OF norm_triangle_ineq], simp)
 apply (auto simp add: Bseq_iff2)
 done
 
-lemma BseqI2: "(\<forall>n. k \<le> f n & f n \<le> K) ==> Bseq f"
+lemma BseqI2: "(\<forall>n. k \<le> f n & f n \<le> (K::real)) ==> Bseq f"
 apply (simp add: Bseq_def)
 apply (rule_tac x = " (\<bar>k\<bar> + \<bar>K\<bar>) + 1" in exI, auto)
 apply (drule_tac x = n in spec, arith)
@@ -769,9 +774,9 @@
 done
 
 lemma lemmaCauchy2:
-     "{n. \<forall>m n. M \<le> m & M \<le> (n::nat) --> \<bar>X m + - X n\<bar> < u} Int
+     "{n. \<forall>m n. M \<le> m & M \<le> (n::nat) --> norm (X m + - X n) < u} Int
       {n. M \<le> xa n} Int {n. M \<le> x n} \<le>
-      {n. abs (X (xa n) + - X (x n)) < u}"
+      {n. norm (X (xa n) + - X (x n)) < u}"
 by blast
 
 lemma Cauchy_NSCauchy: "Cauchy X ==> NSCauchy X"
@@ -781,7 +786,6 @@
 apply (rule approx_minus_iff [THEN iffD2])
 apply (rule mem_infmal_iff [THEN iffD1])
 apply (auto simp add: starfun star_n_minus star_n_add Infinitesimal_FreeUltrafilterNat_iff)
-apply (rule bexI, auto)
 apply (drule spec, auto)
 apply (drule_tac M = M in lemmaCauchy1)
 apply (drule_tac M = M in lemmaCauchy1)
@@ -795,23 +799,14 @@
 lemma NSCauchy_Cauchy: "NSCauchy X ==> Cauchy X"
 apply (auto simp add: Cauchy_def NSCauchy_def)
 apply (rule ccontr, simp)
-apply (auto dest!: choice HNatInfinite_NSLIMSEQ simp add: all_conj_distrib)  
+apply (auto dest!: no_choice HNatInfinite_NSLIMSEQ
+            simp add: all_conj_distrib)
 apply (drule bspec, assumption)
 apply (drule_tac x = "star_n fa" in bspec); 
 apply (auto simp add: starfun)
 apply (drule approx_minus_iff [THEN iffD1])
 apply (drule mem_infmal_iff [THEN iffD2])
 apply (auto simp add: star_n_minus star_n_add Infinitesimal_FreeUltrafilterNat_iff)
-apply (rename_tac "Y")
-apply (drule_tac x = e in spec, auto)
-apply (drule FreeUltrafilterNat_Int, assumption)
-apply (subgoal_tac "{n. \<bar>X (f n) + - X (fa n)\<bar> < e} \<in> \<U>") 
- prefer 2 apply (erule FreeUltrafilterNat_subset, force) 
-apply (rule FreeUltrafilterNat_empty [THEN notE]) 
-apply (subgoal_tac
-         "{n. abs (X (f n) + - X (fa n)) < e} Int 
-          {M. ~ abs (X (f M) + - X (fa M)) < e}  =  {}")
-apply auto  
 done
 
 
@@ -821,9 +816,13 @@
 text{*A Cauchy sequence is bounded -- this is the standard
   proof mechanization rather than the nonstandard proof*}
 
-lemma lemmaCauchy: "\<forall>n \<ge> M. \<bar>X M + - X n\<bar> < (1::real)
-          ==>  \<forall>n \<ge> M. \<bar>X n\<bar> < 1 + \<bar>X M\<bar>"
-by auto
+lemma lemmaCauchy: "\<forall>n \<ge> M. norm (X M + - X n) < (1::real)
+          ==>  \<forall>n \<ge> M. norm (X n :: 'a::real_normed_vector) < 1 + norm (X M)"
+apply (clarify, drule spec, drule (1) mp)
+apply (fold diff_def, simp only: norm_minus_commute)
+apply (drule order_le_less_trans [OF norm_triangle_ineq2])
+apply simp
+done
 
 lemma less_Suc_cancel_iff: "(n < Suc M) = (n \<le> M)"
 by auto
@@ -842,7 +841,7 @@
 done
 
 lemma SUP_rabs_subseq:
-     "\<exists>m \<le> M. \<forall>n \<le> M. \<bar>(X::nat=> real) n\<bar> \<le> \<bar>X m\<bar>"
+     "\<exists>m::nat \<le> M. \<forall>n \<le> M. norm (X n) \<le> norm (X m)"
 by (rule SUP_subseq)
 
 lemma lemma_Nat_covered:
@@ -853,47 +852,52 @@
 
 
 lemma lemma_trans1:
-     "[| \<forall>n \<le> M. \<bar>(X::nat=>real) n\<bar> \<le> a;  a < b |]
-      ==> \<forall>n \<le> M. \<bar>X n\<bar> \<le> b"
+     "[| \<forall>n \<le> M. norm ((X::nat=>'a::real_normed_vector) n) \<le> a;  a < b |]
+      ==> \<forall>n \<le> M. norm (X n) \<le> b"
 by (blast intro: order_le_less_trans [THEN order_less_imp_le])
 
 lemma lemma_trans2:
-     "[| \<forall>n \<ge> M. \<bar>(X::nat=>real) n\<bar> < a; a < b |]
-      ==> \<forall>n \<ge> M. \<bar>X n\<bar>\<le> b"
+     "[| \<forall>n \<ge> M. norm ((X::nat=>'a::real_normed_vector) n) < a; a < b |]
+      ==> \<forall>n \<ge> M. norm (X n) \<le> b"
 by (blast intro: order_less_trans [THEN order_less_imp_le])
 
 lemma lemma_trans3:
-     "[| \<forall>n \<le> M. \<bar>X n\<bar> \<le> a; a = b |]
-      ==> \<forall>n \<le> M. \<bar>X n\<bar> \<le> b"
+     "[| \<forall>n \<le> M. norm (X n) \<le> a; a = b |]
+      ==> \<forall>n \<le> M. norm (X n) \<le> b"
 by auto
 
-lemma lemma_trans4: "\<forall>n \<ge> M. \<bar>(X::nat=>real) n\<bar> < a
-              ==>  \<forall>n \<ge> M. \<bar>X n\<bar> \<le> a"
+lemma lemma_trans4: "\<forall>n \<ge> M. norm ((X::nat=>'a::real_normed_vector) n) < a
+              ==>  \<forall>n \<ge> M. norm (X n) \<le> a"
 by (blast intro: order_less_imp_le)
 
 
 text{*Proof is more involved than outlines sketched by various authors
  would suggest*}
 
+lemma Bseq_Suc_imp_Bseq: "Bseq (\<lambda>n. X (Suc n)) \<Longrightarrow> Bseq X"
+apply (unfold Bseq_def, clarify)
+apply (rule_tac x="max K (norm (X 0))" in exI)
+apply (simp add: order_less_le_trans [OF _ le_maxI1])
+apply (clarify, case_tac "n", simp)
+apply (simp add: order_trans [OF _ le_maxI1])
+done
+
+lemma Bseq_shift_imp_Bseq: "Bseq (\<lambda>n. X (n + k)) \<Longrightarrow> Bseq X"
+apply (induct k, simp_all)
+apply (subgoal_tac "Bseq (\<lambda>n. X (n + k))", simp)
+apply (rule Bseq_Suc_imp_Bseq, simp)
+done
+
 lemma Cauchy_Bseq: "Cauchy X ==> Bseq X"
-apply (simp add: Cauchy_def Bseq_def)
-apply (drule_tac x = 1 in spec)
-apply (erule zero_less_one [THEN [2] impE], safe)
-apply (drule_tac x = M in spec, simp)
+apply (simp add: Cauchy_def)
+apply (drule spec, drule mp, rule zero_less_one, safe)
+apply (drule_tac x="M" in spec, simp)
 apply (drule lemmaCauchy)
-apply (cut_tac M = M and X = X in SUP_rabs_subseq, safe)
-apply (cut_tac x = "\<bar>X m\<bar> " and y = "1 + \<bar>X M\<bar> " in linorder_less_linear)
-apply safe
-apply (drule lemma_trans1, assumption)
-apply (drule_tac [3] lemma_trans2, erule_tac [3] asm_rl)
-apply (drule_tac [2] lemma_trans3, erule_tac [2] asm_rl)
-apply (drule_tac [3] abs_add_one_gt_zero [THEN order_less_trans])
-apply (drule lemma_trans4)
-apply (drule_tac [2] lemma_trans4)
-apply (rule_tac x = "1 + \<bar>X M\<bar> " in exI)
-apply (rule_tac [2] x = "1 + \<bar>X M\<bar> " in exI)
-apply (rule_tac [3] x = "\<bar>X m\<bar> " in exI)
-apply (auto elim!: lemma_Nat_covered)
+apply (rule_tac k="M" in Bseq_shift_imp_Bseq)
+apply (simp add: Bseq_def)
+apply (rule_tac x="1 + norm (X M)" in exI)
+apply (rule conjI, rule order_less_le_trans [OF zero_less_one], simp)
+apply (simp add: order_less_imp_le)
 done
 
 text{*A Cauchy sequence is bounded -- nonstandard version*}
@@ -912,7 +916,7 @@
   instantiations for his 'espsilon-delta' proof(s) in this case
   since the NS formulations do not involve existential quantifiers.*}
 
-lemma NSCauchy_NSconvergent_iff: "NSCauchy X = NSconvergent X"
+lemma NSCauchy_NSconvergent_iff: "NSCauchy X = NSconvergent (X::nat=>real)"
 apply (simp add: NSconvergent_def NSLIMSEQ_def, safe)
 apply (frule NSCauchy_NSBseq)
 apply (auto intro: approx_trans2 simp add: NSBseq_def NSCauchy_def)
@@ -923,7 +927,7 @@
 done
 
 text{*Standard proof for free*}
-lemma Cauchy_convergent_iff: "Cauchy X = convergent X"
+lemma Cauchy_convergent_iff: "Cauchy X = convergent (X::nat=>real)"
 by (simp add: NSCauchy_Cauchy_iff [symmetric] convergent_NSconvergent_iff NSCauchy_NSconvergent_iff)
 
 
@@ -933,7 +937,7 @@
 lemma NSLIMSEQ_le:
        "[| f ----NS> l; g ----NS> m;
            \<exists>N. \<forall>n \<ge> N. f(n) \<le> g(n)
-        |] ==> l \<le> m"
+        |] ==> l \<le> (m::real)"
 apply (simp add: NSLIMSEQ_def, safe)
 apply (drule starfun_le_mono)
 apply (drule HNatInfinite_whn [THEN [2] bspec])+
@@ -946,23 +950,23 @@
 (* standard version *)
 lemma LIMSEQ_le:
      "[| f ----> l; g ----> m; \<exists>N. \<forall>n \<ge> N. f(n) \<le> g(n) |]
-      ==> l \<le> m"
+      ==> l \<le> (m::real)"
 by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_le)
 
-lemma LIMSEQ_le_const: "[| X ----> r; \<forall>n. a \<le> X n |] ==> a \<le> r"
+lemma LIMSEQ_le_const: "[| X ----> (r::real); \<forall>n. a \<le> X n |] ==> a \<le> r"
 apply (rule LIMSEQ_le)
 apply (rule LIMSEQ_const, auto)
 done
 
-lemma NSLIMSEQ_le_const: "[| X ----NS> r; \<forall>n. a \<le> X n |] ==> a \<le> r"
+lemma NSLIMSEQ_le_const: "[| X ----NS> (r::real); \<forall>n. a \<le> X n |] ==> a \<le> r"
 by (simp add: LIMSEQ_NSLIMSEQ_iff LIMSEQ_le_const)
 
-lemma LIMSEQ_le_const2: "[| X ----> r; \<forall>n. X n \<le> a |] ==> r \<le> a"
+lemma LIMSEQ_le_const2: "[| X ----> (r::real); \<forall>n. X n \<le> a |] ==> r \<le> a"
 apply (rule LIMSEQ_le)
 apply (rule_tac [2] LIMSEQ_const, auto)
 done
 
-lemma NSLIMSEQ_le_const2: "[| X ----NS> r; \<forall>n. X n \<le> a |] ==> r \<le> a"
+lemma NSLIMSEQ_le_const2: "[| X ----NS> (r::real); \<forall>n. X n \<le> a |] ==> r \<le> a"
 by (simp add: LIMSEQ_NSLIMSEQ_iff LIMSEQ_le_const2)
 
 text{*Shift a convergent series by 1:
@@ -970,12 +974,10 @@
   the successor of an infinite hypernatural is also infinite.*}
 
 lemma NSLIMSEQ_Suc: "f ----NS> l ==> (%n. f(Suc n)) ----NS> l"
-apply (frule NSconvergentI [THEN NSCauchy_NSconvergent_iff [THEN iffD2]])
-apply (auto simp add: NSCauchy_def NSLIMSEQ_def starfun_shift_one)
-apply (drule bspec, assumption)
-apply (drule bspec, assumption)
-apply (drule Nats_1 [THEN [2] HNatInfinite_SHNat_add])
-apply (blast intro: approx_trans3)
+apply (unfold NSLIMSEQ_def, safe)
+apply (drule_tac x="N + 1" in bspec)
+apply (erule Nats_1 [THEN [2] HNatInfinite_SHNat_add])
+apply (simp add: starfun_shift_one)
 done
 
 text{* standard version *}
@@ -983,13 +985,10 @@
 by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_Suc)
 
 lemma NSLIMSEQ_imp_Suc: "(%n. f(Suc n)) ----NS> l ==> f ----NS> l"
-apply (frule NSconvergentI [THEN NSCauchy_NSconvergent_iff [THEN iffD2]])
-apply (auto simp add: NSCauchy_def NSLIMSEQ_def starfun_shift_one)
-apply (drule bspec, assumption)
-apply (drule bspec, assumption)
-apply (frule Nats_1 [THEN [2] HNatInfinite_SHNat_diff])
+apply (unfold NSLIMSEQ_def, safe)
 apply (drule_tac x="N - 1" in bspec) 
-apply (auto intro: approx_trans3)
+apply (erule Nats_1 [THEN [2] HNatInfinite_SHNat_diff])
+apply (simp add: starfun_shift_one)
 done
 
 lemma LIMSEQ_imp_Suc: "(%n. f(Suc n)) ----> l ==> f ----> l"
@@ -1004,30 +1003,30 @@
 by (blast intro: NSLIMSEQ_imp_Suc NSLIMSEQ_Suc)
 
 text{*A sequence tends to zero iff its abs does*}
-lemma LIMSEQ_rabs_zero: "((%n. \<bar>f n\<bar>) ----> 0) = (f ----> 0)"
+lemma LIMSEQ_rabs_zero: "((%n. \<bar>f n\<bar>) ----> 0) = (f ----> (0::real))"
 by (simp add: LIMSEQ_def)
 
 text{*We prove the NS version from the standard one, since the NS proof
    seems more complicated than the standard one above!*}
-lemma NSLIMSEQ_rabs_zero: "((%n. \<bar>f n\<bar>) ----NS> 0) = (f ----NS> 0)"
+lemma NSLIMSEQ_rabs_zero: "((%n. \<bar>f n\<bar>) ----NS> 0) = (f ----NS> (0::real))"
 by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_rabs_zero)
 
 text{*Generalization to other limits*}
-lemma NSLIMSEQ_imp_rabs: "f ----NS> l ==> (%n. \<bar>f n\<bar>) ----NS> \<bar>l\<bar>"
+lemma NSLIMSEQ_imp_rabs: "f ----NS> (l::real) ==> (%n. \<bar>f n\<bar>) ----NS> \<bar>l\<bar>"
 apply (simp add: NSLIMSEQ_def)
 apply (auto intro: approx_hrabs 
             simp add: starfun_abs hypreal_of_real_hrabs [symmetric])
 done
 
 text{* standard version *}
-lemma LIMSEQ_imp_rabs: "f ----> l ==> (%n. \<bar>f n\<bar>) ----> \<bar>l\<bar>"
+lemma LIMSEQ_imp_rabs: "f ----> (l::real) ==> (%n. \<bar>f n\<bar>) ----> \<bar>l\<bar>"
 by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_imp_rabs)
 
 text{*An unbounded sequence's inverse tends to 0*}
 
 text{* standard proof seems easier *}
 lemma LIMSEQ_inverse_zero:
-      "\<forall>y. \<exists>N. \<forall>n \<ge> N. y < f(n) ==> (%n. inverse(f n)) ----> 0"
+      "\<forall>y::real. \<exists>N. \<forall>n \<ge> N. y < f(n) ==> (%n. inverse(f n)) ----> 0"
 apply (simp add: LIMSEQ_def, safe)
 apply (drule_tac x = "inverse r" in spec, safe)
 apply (rule_tac x = N in exI, safe)
@@ -1042,7 +1041,7 @@
 done
 
 lemma NSLIMSEQ_inverse_zero:
-     "\<forall>y. \<exists>N. \<forall>n \<ge> N. y < f(n)
+     "\<forall>y::real. \<exists>N. \<forall>n \<ge> N. y < f(n)
       ==> (%n. inverse(f n)) ----NS> 0"
 by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_zero)
 
@@ -1090,19 +1089,22 @@
 text{* Real Powers*}
 
 lemma NSLIMSEQ_pow [rule_format]:
-     "(X ----NS> a) --> ((%n. (X n) ^ m) ----NS> a ^ m)"
+  fixes a :: "'a::{real_normed_algebra,recpower}"
+  shows "(X ----NS> a) --> ((%n. (X n) ^ m) ----NS> a ^ m)"
 apply (induct "m")
-apply (auto intro: NSLIMSEQ_mult NSLIMSEQ_const)
+apply (auto simp add: power_Suc intro: NSLIMSEQ_mult NSLIMSEQ_const)
 done
 
-lemma LIMSEQ_pow: "X ----> a ==> (%n. (X n) ^ m) ----> a ^ m"
+lemma LIMSEQ_pow:
+  fixes a :: "'a::{real_normed_algebra,recpower}"
+  shows "X ----> a ==> (%n. (X n) ^ m) ----> a ^ m"
 by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_pow)
 
 text{*The sequence @{term "x^n"} tends to 0 if @{term "0\<le>x"} and @{term
 "x<1"}.  Proof will use (NS) Cauchy equivalence for convergence and
   also fact that bounded and monotonic sequence converges.*}
 
-lemma Bseq_realpow: "[| 0 \<le> x; x \<le> 1 |] ==> Bseq (%n. x ^ n)"
+lemma Bseq_realpow: "[| 0 \<le> (x::real); x \<le> 1 |] ==> Bseq (%n. x ^ n)"
 apply (simp add: Bseq_def)
 apply (rule_tac x = 1 in exI)
 apply (simp add: power_abs)
@@ -1114,12 +1116,14 @@
 apply (cut_tac n = n and N = "Suc n" and a = x in power_decreasing, auto)
 done
 
-lemma convergent_realpow: "[| 0 \<le> x; x \<le> 1 |] ==> convergent (%n. x ^ n)"
+lemma convergent_realpow:
+  "[| 0 \<le> (x::real); x \<le> 1 |] ==> convergent (%n. x ^ n)"
 by (blast intro!: Bseq_monoseq_convergent Bseq_realpow monoseq_realpow)
 
 text{* We now use NS criterion to bring proof of theorem through *}
 
-lemma NSLIMSEQ_realpow_zero: "[| 0 \<le> x; x < 1 |] ==> (%n. x ^ n) ----NS> 0"
+lemma NSLIMSEQ_realpow_zero:
+  "[| 0 \<le> (x::real); x < 1 |] ==> (%n. x ^ n) ----NS> 0"
 apply (simp add: NSLIMSEQ_def)
 apply (auto dest!: convergent_realpow simp add: convergent_NSconvergent_iff)
 apply (frule NSconvergentD)
@@ -1135,10 +1139,12 @@
 done
 
 text{* standard version *}
-lemma LIMSEQ_realpow_zero: "[| 0 \<le> x; x < 1 |] ==> (%n. x ^ n) ----> 0"
+lemma LIMSEQ_realpow_zero:
+  "[| 0 \<le> (x::real); x < 1 |] ==> (%n. x ^ n) ----> 0"
 by (simp add: NSLIMSEQ_realpow_zero LIMSEQ_NSLIMSEQ_iff)
 
-lemma LIMSEQ_divide_realpow_zero: "1 < x ==> (%n. a / (x ^ n)) ----> 0"
+lemma LIMSEQ_divide_realpow_zero:
+  "1 < (x::real) ==> (%n. a / (x ^ n)) ----> 0"
 apply (cut_tac a = a and x1 = "inverse x" in
         LIMSEQ_mult [OF LIMSEQ_const LIMSEQ_realpow_zero])
 apply (auto simp add: divide_inverse power_inverse)
@@ -1147,18 +1153,18 @@
 
 text{*Limit of @{term "c^n"} for @{term"\<bar>c\<bar> < 1"}*}
 
-lemma LIMSEQ_rabs_realpow_zero: "\<bar>c\<bar> < 1 ==> (%n. \<bar>c\<bar> ^ n) ----> 0"
+lemma LIMSEQ_rabs_realpow_zero: "\<bar>c\<bar> < (1::real) ==> (%n. \<bar>c\<bar> ^ n) ----> 0"
 by (blast intro!: LIMSEQ_realpow_zero abs_ge_zero)
 
-lemma NSLIMSEQ_rabs_realpow_zero: "\<bar>c\<bar> < 1 ==> (%n. \<bar>c\<bar> ^ n) ----NS> 0"
+lemma NSLIMSEQ_rabs_realpow_zero: "\<bar>c\<bar> < (1::real) ==> (%n. \<bar>c\<bar> ^ n) ----NS> 0"
 by (simp add: LIMSEQ_rabs_realpow_zero LIMSEQ_NSLIMSEQ_iff [symmetric])
 
-lemma LIMSEQ_rabs_realpow_zero2: "\<bar>c\<bar> < 1 ==> (%n. c ^ n) ----> 0"
+lemma LIMSEQ_rabs_realpow_zero2: "\<bar>c\<bar> < (1::real) ==> (%n. c ^ n) ----> 0"
 apply (rule LIMSEQ_rabs_zero [THEN iffD1])
 apply (auto intro: LIMSEQ_rabs_realpow_zero simp add: power_abs)
 done
 
-lemma NSLIMSEQ_rabs_realpow_zero2: "\<bar>c\<bar> < 1 ==> (%n. c ^ n) ----NS> 0"
+lemma NSLIMSEQ_rabs_realpow_zero2: "\<bar>c\<bar> < (1::real) ==> (%n. c ^ n) ----NS> 0"
 by (simp add: LIMSEQ_rabs_realpow_zero2 LIMSEQ_NSLIMSEQ_iff [symmetric])
 
 subsection{*Hyperreals and Sequences*}
diff -r ba543692bfa1 -r 2c31dd358c21 src/HOL/Hyperreal/Series.thy
--- a/src/HOL/Hyperreal/Series.thy	Sat Sep 16 02:35:58 2006 +0200
+++ b/src/HOL/Hyperreal/Series.thy	Sat Sep 16 02:40:00 2006 +0200
@@ -354,7 +354,7 @@
 apply (drule spec, drule (1) mp)
 apply (erule exE, rule_tac x="N" in exI, clarify)
 apply (rule_tac x="m" and y="n" in linorder_le_cases)
-apply (subst abs_minus_commute)
+apply (subst norm_minus_commute)
 apply (simp add: setsum_diff [symmetric])
 apply (simp add: setsum_diff [symmetric])
 done
diff -r ba543692bfa1 -r 2c31dd358c21 src/HOL/Hyperreal/Star.thy
--- a/src/HOL/Hyperreal/Star.thy	Sat Sep 16 02:35:58 2006 +0200
+++ b/src/HOL/Hyperreal/Star.thy	Sat Sep 16 02:40:00 2006 +0200
@@ -38,7 +38,7 @@
    referee for the JCM Paper: let f(x) be least y such
    that  Q(x,y)
 *)
-lemma no_choice: "\<forall>x. \<exists>y. Q x y ==> \<exists>(f :: nat => nat). \<forall>x. Q x (f x)"
+lemma no_choice: "\<forall>x. \<exists>y. Q x y ==> \<exists>(f :: 'a => nat). \<forall>x. Q x (f x)"
 apply (rule_tac x = "%x. LEAST y. Q x y" in exI)
 apply (blast intro: LeastI)
 done
@@ -146,11 +146,6 @@
 apply (simp add: Ifun_star_n star_n_eq_iff)
 done
 
-lemma Rep_star_FreeUltrafilterNat:
-     "[| X \<in> Rep_star z; Y \<in> Rep_star z |]
-      ==> {n. X n = Y n} : FreeUltrafilterNat"
-by (rule FreeUltrafilterNat_Rep_hypreal)
-
 text{*Nonstandard extension of functions*}
 
 lemma starfun:
@@ -213,7 +208,7 @@
 
 (* this is trivial, given starfun_Id *)
 lemma starfun_Idfun_approx:
-  "x @= hypreal_of_real a ==> ( *f* (%x. x)) x @= hypreal_of_real a"
+  "x @= star_of a ==> ( *f* (%x. x)) x @= star_of a"
 by (simp only: starfun_Id)
 
 text{*The Star-function is a (nonstandard) extension of the function*}
@@ -243,10 +238,10 @@
 text{*extented function has same solution as its standard
    version for real arguments. i.e they are the same
    for all real arguments*}
-lemma starfun_eq [simp]: "( *f* f) (star_of a) = star_of (f a)"
-by (transfer, rule refl)
+lemma starfun_eq: "( *f* f) (star_of a) = star_of (f a)"
+by (rule starfun_star_of)
 
-lemma starfun_approx: "( *f* f) (star_of a) @= hypreal_of_real (f a)"
+lemma starfun_approx: "( *f* f) (star_of a) @= star_of (f a)"
 by simp
 
 (* useful for NS definition of derivatives *)
@@ -258,7 +253,9 @@
   "( *f* (%h. f(g(x + h)))) x' = ( *f* (f o g)) (star_of x + x')"
 by (unfold o_def, rule starfun_lambda_cancel)
 
-lemma starfun_mult_HFinite_approx: "[| ( *f* f) x @= l; ( *f* g) x @= m;
+lemma starfun_mult_HFinite_approx:
+  fixes l m :: "'a::real_normed_algebra star"
+  shows "[| ( *f* f) x @= l; ( *f* g) x @= m;
                   l: HFinite; m: HFinite
                |] ==>  ( *f* (%x. f x * g x)) x @= l * m"
 apply (drule (3) approx_mult_HFinite)
@@ -277,10 +274,10 @@
 (* use the theorem we proved above instead          *)
 
 lemma starfun_rabs_hrabs: "*f* abs = abs"
-by (rule hrabs_is_starext_rabs [THEN is_starext_starfun_iff [THEN iffD1], symmetric])
+by (simp only: star_abs_def)
 
 lemma starfun_inverse_inverse [simp]: "( *f* inverse) x = inverse(x)"
-by (unfold star_inverse_def, rule refl)
+by (simp only: star_inverse_def)
 
 lemma starfun_inverse: "!!x. inverse (( *f* f) x) = ( *f* (%x. inverse (f x))) x"
 by (transfer, rule refl)
@@ -312,36 +309,40 @@
    by its NS extenson. See second NS set extension below.*}
 lemma STAR_rabs_add_minus:
    "*s* {x. abs (x + - y) < r} =
-     {x. abs(x + -hypreal_of_real y) < hypreal_of_real r}"
+     {x. abs(x + -star_of y) < star_of r}"
 by (transfer, rule refl)
 
 lemma STAR_starfun_rabs_add_minus:
   "*s* {x. abs (f x + - y) < r} =
-       {x. abs(( *f* f) x + -hypreal_of_real y) < hypreal_of_real r}"
+       {x. abs(( *f* f) x + -star_of y) < star_of r}"
 by (transfer, rule refl)
 
 text{*Another characterization of Infinitesimal and one of @= relation.
    In this theory since @{text hypreal_hrabs} proved here. Maybe
    move both theorems??*}
 lemma Infinitesimal_FreeUltrafilterNat_iff2:
-     "(x \<in> Infinitesimal) =
-      (\<exists>X \<in> Rep_star(x).
-        \<forall>m. {n. abs(X n) < inverse(real(Suc m))}
+     "(star_n X \<in> Infinitesimal) =
+      (\<forall>m. {n. norm(X n) < inverse(real(Suc m))}
                 \<in>  FreeUltrafilterNat)"
-apply (cases x)
-apply (auto intro!: bexI lemma_starrel_refl 
-            simp add: Infinitesimal_hypreal_of_nat_iff star_of_def
-     star_n_inverse star_n_abs star_n_less hypreal_of_nat_eq)
-apply (drule_tac x = n in spec, ultra)
+by (simp add: Infinitesimal_hypreal_of_nat_iff star_of_def
+     hnorm_def star_of_nat_def starfun_star_n
+     star_n_inverse star_n_less hypreal_of_nat_eq)
+
+lemma approx_FreeUltrafilterNat_iff: "star_n X @= star_n Y =
+      (\<forall>r>0. {n. norm (X n + - Y n) < r} : FreeUltrafilterNat)"
+apply (subst approx_minus_iff)
+apply (rule mem_infmal_iff [THEN subst])
+apply (simp add: star_n_minus star_n_add)
+apply (simp add: Infinitesimal_FreeUltrafilterNat_iff)
 done
 
-lemma approx_FreeUltrafilterNat_iff: "star_n X @= star_n Y =
-      (\<forall>m. {n. abs (X n + - Y n) <
+lemma approx_FreeUltrafilterNat_iff2: "star_n X @= star_n Y =
+      (\<forall>m. {n. norm (X n + - Y n) <
                   inverse(real(Suc m))} : FreeUltrafilterNat)"
 apply (subst approx_minus_iff)
 apply (rule mem_infmal_iff [THEN subst])
-apply (auto simp add: star_n_minus star_n_add Infinitesimal_FreeUltrafilterNat_iff2)
-apply (drule_tac x = m in spec, ultra)
+apply (simp add: star_n_minus star_n_add)
+apply (simp add: Infinitesimal_FreeUltrafilterNat_iff2)
 done
 
 lemma inj_starfun: "inj starfun"
diff -r ba543692bfa1 -r 2c31dd358c21 src/HOL/Hyperreal/Transcendental.thy
--- a/src/HOL/Hyperreal/Transcendental.thy	Sat Sep 16 02:35:58 2006 +0200
+++ b/src/HOL/Hyperreal/Transcendental.thy	Sat Sep 16 02:40:00 2006 +0200
@@ -2540,7 +2540,8 @@
 done
 
 lemma isCont_inv_fun_inv:
-     "[| 0 < d;  
+  fixes f g :: "real \<Rightarrow> real"
+  shows "[| 0 < d;  
          \<forall>z. \<bar>z - x\<bar> \<le> d --> g(f(z)) = z;  
          \<forall>z. \<bar>z - x\<bar> \<le> d --> isCont f z |]  
        ==> \<exists>e. 0 < e &  
@@ -2555,7 +2556,7 @@
 
 text{*Bartle/Sherbert: Introduction to Real Analysis, Theorem 4.2.9, p. 110*}
 lemma LIM_fun_gt_zero:
-     "[| f -- c --> l; 0 < l |]  
+     "[| f -- c --> (l::real); 0 < l |]  
          ==> \<exists>r. 0 < r & (\<forall>x. x \<noteq> c & \<bar>c - x\<bar> < r --> 0 < f x)"
 apply (auto simp add: LIM_def)
 apply (drule_tac x = "l/2" in spec, safe, force)
@@ -2564,7 +2565,7 @@
 done
 
 lemma LIM_fun_less_zero:
-     "[| f -- c --> l; l < 0 |]  
+     "[| f -- c --> (l::real); l < 0 |]  
       ==> \<exists>r. 0 < r & (\<forall>x. x \<noteq> c & \<bar>c - x\<bar> < r --> f x < 0)"
 apply (auto simp add: LIM_def)
 apply (drule_tac x = "-l/2" in spec, safe, force)
@@ -2574,7 +2575,7 @@
 
 
 lemma LIM_fun_not_zero:
-     "[| f -- c --> l; l \<noteq> 0 |] 
+     "[| f -- c --> (l::real); l \<noteq> 0 |] 
       ==> \<exists>r. 0 < r & (\<forall>x. x \<noteq> c & \<bar>c - x\<bar> < r --> f x \<noteq> 0)"
 apply (cut_tac x = l and y = 0 in linorder_less_linear, auto)
 apply (drule LIM_fun_less_zero)