generalized types of many constants to work over arbitrary vector spaces;
authorhuffman
Sat Sep 16 02:40:00 2006 +0200 (2006-09-16)
changeset 205522c31dd358c21
parent 20551 ba543692bfa1
child 20553 7ced6152e52c
generalized types of many constants to work over arbitrary vector spaces;
modified theorems using Rep_star to eliminate existential quantifiers
src/HOL/Complex/CLim.thy
src/HOL/Complex/NSCA.thy
src/HOL/Hyperreal/HTranscendental.thy
src/HOL/Hyperreal/HyperDef.thy
src/HOL/Hyperreal/HyperNat.thy
src/HOL/Hyperreal/Lim.thy
src/HOL/Hyperreal/NSA.thy
src/HOL/Hyperreal/SEQ.thy
src/HOL/Hyperreal/Series.thy
src/HOL/Hyperreal/Star.thy
src/HOL/Hyperreal/Transcendental.thy
     1.1 --- a/src/HOL/Complex/CLim.thy	Sat Sep 16 02:35:58 2006 +0200
     1.2 +++ b/src/HOL/Complex/CLim.thy	Sat Sep 16 02:40:00 2006 +0200
     1.3 @@ -126,10 +126,9 @@
     1.4  apply (rule_tac x = xa in star_cases)
     1.5  apply (auto simp add: starfun star_n_diff star_of_def star_n_eq_iff
     1.6           CInfinitesimal_hcmod_iff hcmod Infinitesimal_FreeUltrafilterNat_iff)
     1.7 -apply (rule bexI [OF _ Rep_star_star_n], safe)
     1.8  apply (drule_tac x = u in spec, auto)
     1.9  apply (drule_tac x = s in spec, auto, ultra)
    1.10 -apply (drule sym, auto)
    1.11 +apply (auto)
    1.12  done
    1.13  
    1.14  lemma eq_Abs_star_ALL: "(\<forall>t. P t) = (\<forall>X. P (star_n X))"
    1.15 @@ -176,7 +175,7 @@
    1.16  apply (drule_tac x = X in spec, auto)
    1.17  apply (drule lemma_csimp [THEN complex_seq_to_hcomplex_CInfinitesimal])
    1.18  apply (simp add: CInfinitesimal_hcmod_iff star_of_def
    1.19 -            Infinitesimal_FreeUltrafilterNat_iff star_n_diff hcmod,  blast)
    1.20 +            Infinitesimal_FreeUltrafilterNat_iff star_n_diff hcmod)
    1.21  apply (drule_tac x = r in spec, clarify)
    1.22  apply (drule FreeUltrafilterNat_all, ultra)
    1.23  done
    1.24 @@ -197,10 +196,9 @@
    1.25                Infinitesimal_FreeUltrafilterNat_iff
    1.26                star_of_def star_n_eq_iff
    1.27                Infinitesimal_approx_minus [symmetric])
    1.28 -apply (rule bexI [OF _ Rep_star_star_n], safe)
    1.29  apply (drule_tac x = u in spec, auto)
    1.30  apply (drule_tac x = s in spec, auto, ultra)
    1.31 -apply (drule sym, auto)
    1.32 +apply (auto)
    1.33  done
    1.34  
    1.35  lemma lemma_CRLIM:
    1.36 @@ -242,7 +240,6 @@
    1.37  apply (drule lemma_crsimp [THEN complex_seq_to_hcomplex_CInfinitesimal])
    1.38  apply (simp add: CInfinitesimal_hcmod_iff star_of_def
    1.39               Infinitesimal_FreeUltrafilterNat_iff star_n_diff hcmod)
    1.40 -apply (auto simp add: star_of_def star_n_diff)
    1.41  apply (drule_tac x = r in spec, clarify)
    1.42  apply (drule FreeUltrafilterNat_all, ultra)
    1.43  done
     2.1 --- a/src/HOL/Complex/NSCA.thy	Sat Sep 16 02:35:58 2006 +0200
     2.2 +++ b/src/HOL/Complex/NSCA.thy	Sat Sep 16 02:40:00 2006 +0200
     2.3 @@ -656,35 +656,32 @@
     2.4  lemma hcomplex_capproxD1:
     2.5       "star_n X @c= star_n Y
     2.6        ==> star_n (%n. Re(X n)) @= star_n (%n. Re(Y n))"
     2.7 -apply (auto simp add: approx_FreeUltrafilterNat_iff)
     2.8 +apply (simp add: approx_FreeUltrafilterNat_iff2, safe)
     2.9  apply (drule capprox_minus_iff [THEN iffD1])
    2.10 -apply (auto simp add: star_n_minus star_n_add mem_cinfmal_iff [symmetric] CInfinitesimal_hcmod_iff hcmod Infinitesimal_FreeUltrafilterNat_iff2)
    2.11 -apply (drule_tac x = m in spec, ultra)
    2.12 -apply (rename_tac Z x)
    2.13 -apply (case_tac "X x")
    2.14 -apply (case_tac "Y x")
    2.15 +apply (simp add: star_n_minus star_n_add mem_cinfmal_iff [symmetric] CInfinitesimal_hcmod_iff hcmod Infinitesimal_FreeUltrafilterNat_iff2)
    2.16 +apply (drule_tac x = m in spec)
    2.17 +apply (erule ultra, rule FreeUltrafilterNat_all, clarify)
    2.18 +apply (rule_tac y="cmod (X n + - Y n)" in order_le_less_trans)
    2.19 +apply (case_tac "X n")
    2.20 +apply (case_tac "Y n")
    2.21  apply (auto simp add: complex_minus complex_add complex_mod
    2.22 -           simp del: realpow_Suc)
    2.23 -apply (rule_tac y="abs(Z x)" in order_le_less_trans)
    2.24 -apply (drule_tac t = "Z x" in sym)
    2.25 -apply (auto simp del: realpow_Suc)
    2.26 +            simp del: realpow_Suc)
    2.27  done
    2.28  
    2.29  (* same proof *)
    2.30  lemma hcomplex_capproxD2:
    2.31       "star_n X @c= star_n Y
    2.32        ==> star_n (%n. Im(X n)) @= star_n (%n. Im(Y n))"
    2.33 -apply (auto simp add: approx_FreeUltrafilterNat_iff)
    2.34 +apply (simp add: approx_FreeUltrafilterNat_iff2, safe)
    2.35  apply (drule capprox_minus_iff [THEN iffD1])
    2.36 -apply (auto simp add: star_n_minus star_n_add mem_cinfmal_iff [symmetric] CInfinitesimal_hcmod_iff hcmod Infinitesimal_FreeUltrafilterNat_iff2)
    2.37 -apply (drule_tac x = m in spec, ultra)
    2.38 -apply (rename_tac Z x)
    2.39 -apply (case_tac "X x")
    2.40 -apply (case_tac "Y x")
    2.41 -apply (auto simp add: complex_minus complex_add complex_mod simp del: realpow_Suc)
    2.42 -apply (rule_tac y="abs(Z x)" in order_le_less_trans)
    2.43 -apply (drule_tac t = "Z x" in sym)
    2.44 -apply (auto simp del: realpow_Suc)
    2.45 +apply (simp add: star_n_minus star_n_add mem_cinfmal_iff [symmetric] CInfinitesimal_hcmod_iff hcmod Infinitesimal_FreeUltrafilterNat_iff2)
    2.46 +apply (drule_tac x = m in spec)
    2.47 +apply (erule ultra, rule FreeUltrafilterNat_all, clarify)
    2.48 +apply (rule_tac y="cmod (X n + - Y n)" in order_le_less_trans)
    2.49 +apply (case_tac "X n")
    2.50 +apply (case_tac "Y n")
    2.51 +apply (auto simp add: complex_minus complex_add complex_mod
    2.52 +            simp del: realpow_Suc)
    2.53  done
    2.54  
    2.55  lemma hcomplex_capproxI:
    2.56 @@ -695,10 +692,8 @@
    2.57  apply (drule approx_minus_iff [THEN iffD1])
    2.58  apply (rule capprox_minus_iff [THEN iffD2])
    2.59  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)
    2.60 -apply (rule bexI [OF _ Rep_star_star_n], auto)
    2.61  apply (drule_tac x = "u/2" in spec)
    2.62  apply (drule_tac x = "u/2" in spec, auto, ultra)
    2.63 -apply (drule sym, drule sym)
    2.64  apply (case_tac "X x")
    2.65  apply (case_tac "Y x")
    2.66  apply (auto simp add: complex_minus complex_add complex_mod snd_conv fst_conv numeral_2_eq_2)
    2.67 @@ -725,9 +720,8 @@
    2.68       "star_n X \<in> CFinite  
    2.69        ==> star_n (%n. Re(X n)) \<in> HFinite"
    2.70  apply (auto simp add: CFinite_hcmod_iff hcmod HFinite_FreeUltrafilterNat_iff)
    2.71 -apply (rule bexI [OF _ Rep_star_star_n])
    2.72  apply (rule_tac x = u in exI, ultra)
    2.73 -apply (drule sym, case_tac "X x")
    2.74 +apply (case_tac "X x")
    2.75  apply (auto simp add: complex_mod numeral_2_eq_2 simp del: realpow_Suc)
    2.76  apply (rule ccontr, drule linorder_not_less [THEN iffD1])
    2.77  apply (drule order_less_le_trans, assumption)
    2.78 @@ -739,9 +733,8 @@
    2.79       "star_n X \<in> CFinite  
    2.80        ==> star_n (%n. Im(X n)) \<in> HFinite"
    2.81  apply (auto simp add: CFinite_hcmod_iff hcmod HFinite_FreeUltrafilterNat_iff)
    2.82 -apply (rule bexI [OF _ Rep_star_star_n])
    2.83  apply (rule_tac x = u in exI, ultra)
    2.84 -apply (drule sym, case_tac "X x")
    2.85 +apply (case_tac "X x")
    2.86  apply (auto simp add: complex_mod simp del: realpow_Suc)
    2.87  apply (rule ccontr, drule linorder_not_less [THEN iffD1])
    2.88  apply (drule order_less_le_trans, assumption)
    2.89 @@ -753,17 +746,16 @@
    2.90           star_n (%n. Im(X n)) \<in> HFinite  
    2.91        |] ==> star_n X \<in> CFinite"
    2.92  apply (auto simp add: CFinite_hcmod_iff hcmod HFinite_FreeUltrafilterNat_iff)
    2.93 -apply (rename_tac Y Z u v)
    2.94 -apply (rule bexI [OF _ Rep_star_star_n])
    2.95 +apply (rename_tac u v)
    2.96  apply (rule_tac x = "2* (u + v) " in exI)
    2.97  apply ultra
    2.98 -apply (drule sym, case_tac "X x")
    2.99 +apply (case_tac "X x")
   2.100  apply (auto simp add: complex_mod numeral_2_eq_2 simp del: realpow_Suc)
   2.101  apply (subgoal_tac "0 < u")
   2.102   prefer 2 apply arith
   2.103  apply (subgoal_tac "0 < v")
   2.104   prefer 2 apply arith
   2.105 -apply (subgoal_tac "sqrt (abs (Y x) ^ 2 + abs (Z x) ^ 2) < 2*u + 2*v")
   2.106 +apply (subgoal_tac "sqrt (abs (Re (X x)) ^ 2 + abs (Im (X x)) ^ 2) < 2*u + 2*v")
   2.107  apply (rule_tac [2] lemma_sqrt_hcomplex_capprox, auto)
   2.108  apply (simp add: power2_eq_square)
   2.109  done
   2.110 @@ -1201,7 +1193,6 @@
   2.111       "\<forall>n. cmod (X n - x) < inverse (real (Suc n)) ==>  
   2.112        star_n X - hcomplex_of_complex x \<in> CInfinitesimal"
   2.113  apply (simp add: star_n_diff CInfinitesimal_hcmod_iff star_of_def Infinitesimal_FreeUltrafilterNat_iff hcmod)
   2.114 -apply (rule bexI, auto)
   2.115  apply (auto dest: FreeUltrafilterNat_inverse_real_of_posnat FreeUltrafilterNat_all FreeUltrafilterNat_Int intro: order_less_trans FreeUltrafilterNat_subset)
   2.116  done
   2.117  
     3.1 --- a/src/HOL/Hyperreal/HTranscendental.thy	Sat Sep 16 02:35:58 2006 +0200
     3.2 +++ b/src/HOL/Hyperreal/HTranscendental.thy	Sat Sep 16 02:40:00 2006 +0200
     3.3 @@ -362,7 +362,6 @@
     3.4  lemma starfun_exp_HFinite: "x \<in> HFinite ==> ( *f* exp) x \<in> HFinite"
     3.5  apply (cases x)
     3.6  apply (auto simp add: starfun HFinite_FreeUltrafilterNat_iff)
     3.7 -apply (rule bexI [OF _ Rep_star_star_n], auto)
     3.8  apply (rule_tac x = "exp u" in exI)
     3.9  apply ultra
    3.10  done
     4.1 --- a/src/HOL/Hyperreal/HyperDef.thy	Sat Sep 16 02:35:58 2006 +0200
     4.2 +++ b/src/HOL/Hyperreal/HyperDef.thy	Sat Sep 16 02:40:00 2006 +0200
     4.3 @@ -188,6 +188,9 @@
     4.4  lemma inj_hypreal_of_real: "inj(hypreal_of_real)"
     4.5  by (rule inj_onI, simp)
     4.6  
     4.7 +lemma mem_Rep_star_iff: "(X \<in> Rep_star x) = (x = star_n X)"
     4.8 +by (cases x, simp add: star_n_def)
     4.9 +
    4.10  lemma Rep_star_star_n_iff [simp]:
    4.11    "(X \<in> Rep_star (star_n Y)) = ({n. Y n = X n} \<in> \<U>)"
    4.12  by (simp add: star_n_def)
     5.1 --- a/src/HOL/Hyperreal/HyperNat.thy	Sat Sep 16 02:35:58 2006 +0200
     5.2 +++ b/src/HOL/Hyperreal/HyperNat.thy	Sat Sep 16 02:40:00 2006 +0200
     5.3 @@ -242,27 +242,20 @@
     5.4  Free Ultrafilter*}
     5.5  
     5.6  lemma HNatInfinite_FreeUltrafilterNat:
     5.7 -     "x \<in> HNatInfinite 
     5.8 -      ==> \<exists>X \<in> Rep_star x. \<forall>u. {n. u < X n}:  FreeUltrafilterNat"
     5.9 -apply (cases x)
    5.10 -apply (auto simp add: HNatInfinite_iff SHNat_eq hypnat_of_nat_eq)
    5.11 -apply (rule bexI [OF _ Rep_star_star_n], clarify) 
    5.12 -apply (auto simp add: hypnat_of_nat_def star_n_less)
    5.13 +     "star_n X \<in> HNatInfinite ==> \<forall>u. {n. u < X n}:  FreeUltrafilterNat"
    5.14 +apply (auto simp add: HNatInfinite_iff SHNat_eq)
    5.15 +apply (drule_tac x="star_of u" in spec, simp)
    5.16 +apply (simp add: star_of_def star_n_less)
    5.17  done
    5.18  
    5.19  lemma FreeUltrafilterNat_HNatInfinite:
    5.20 -     "\<exists>X \<in> Rep_star x. \<forall>u. {n. u < X n}:  FreeUltrafilterNat
    5.21 -      ==> x \<in> HNatInfinite"
    5.22 -apply (cases x)
    5.23 -apply (auto simp add: star_n_less HNatInfinite_iff SHNat_eq hypnat_of_nat_eq)
    5.24 -apply (drule spec, ultra, auto) 
    5.25 -done
    5.26 +     "\<forall>u. {n. u < X n}:  FreeUltrafilterNat ==> star_n X \<in> HNatInfinite"
    5.27 +by (auto simp add: star_n_less HNatInfinite_iff SHNat_eq hypnat_of_nat_eq)
    5.28  
    5.29  lemma HNatInfinite_FreeUltrafilterNat_iff:
    5.30 -     "(x \<in> HNatInfinite) = 
    5.31 -      (\<exists>X \<in> Rep_star x. \<forall>u. {n. u < X n}:  FreeUltrafilterNat)"
    5.32 -by (blast intro: HNatInfinite_FreeUltrafilterNat 
    5.33 -                 FreeUltrafilterNat_HNatInfinite)
    5.34 +     "(star_n X \<in> HNatInfinite) = (\<forall>u. {n. u < X n}:  FreeUltrafilterNat)"
    5.35 +by (rule iffI [OF HNatInfinite_FreeUltrafilterNat 
    5.36 +                 FreeUltrafilterNat_HNatInfinite])
    5.37  
    5.38  lemma HNatInfinite_gt_one [simp]: "x \<in> HNatInfinite ==> (1::hypnat) < x"
    5.39  by (auto simp add: HNatInfinite_iff)
    5.40 @@ -370,10 +363,11 @@
    5.41  lemma HNatInfinite_inverse_Infinitesimal [simp]:
    5.42       "n \<in> HNatInfinite ==> inverse (hypreal_of_hypnat n) \<in> Infinitesimal"
    5.43  apply (cases n)
    5.44 -apply (auto simp add: hypreal_of_hypnat star_n_inverse 
    5.45 -      HNatInfinite_FreeUltrafilterNat_iff Infinitesimal_FreeUltrafilterNat_iff2)
    5.46 -apply (rule bexI [OF _ Rep_star_star_n], auto)
    5.47 -apply (drule_tac x = "m + 1" in spec, ultra)
    5.48 +apply (auto simp add: hypreal_of_hypnat star_n_inverse real_norm_def
    5.49 +      HNatInfinite_FreeUltrafilterNat_iff
    5.50 +      Infinitesimal_FreeUltrafilterNat_iff2)
    5.51 +apply (drule_tac x="Suc m" in spec)
    5.52 +apply (erule ultra, simp)
    5.53  done
    5.54  
    5.55  lemma HNatInfinite_hypreal_of_hypnat_gt_zero:
     6.1 --- a/src/HOL/Hyperreal/Lim.thy	Sat Sep 16 02:35:58 2006 +0200
     6.2 +++ b/src/HOL/Hyperreal/Lim.thy	Sat Sep 16 02:40:00 2006 +0200
     6.3 @@ -15,25 +15,24 @@
     6.4  text{*Standard and Nonstandard Definitions*}
     6.5  
     6.6  definition
     6.7 -  LIM :: "[real=>real,real,real] => bool"
     6.8 +  LIM :: "[real => 'a::real_normed_vector, real, 'a] => bool"
     6.9          ("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60)
    6.10    "f -- a --> L =
    6.11       (\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & \<bar>x + -a\<bar> < s
    6.12 -        --> \<bar>f x + -L\<bar> < r)"
    6.13 +        --> norm (f x + -L) < r)"
    6.14  
    6.15 -  NSLIM :: "[real=>real,real,real] => bool"
    6.16 +  NSLIM :: "[real => 'a::real_normed_vector, real, 'a] => bool"
    6.17              ("((_)/ -- (_)/ --NS> (_))" [60, 0, 60] 60)
    6.18 -  "f -- a --NS> L = (\<forall>x. (x \<noteq> hypreal_of_real a &
    6.19 -          x @= hypreal_of_real a -->
    6.20 -          ( *f* f) x @= hypreal_of_real L))"
    6.21 +  "f -- a --NS> L =
    6.22 +    (\<forall>x. (x \<noteq> star_of a & x @= star_of a --> ( *f* f) x @= star_of L))"
    6.23  
    6.24 -  isCont :: "[real=>real,real] => bool"
    6.25 +  isCont :: "[real => 'a::real_normed_vector, real] => bool"
    6.26    "isCont f a = (f -- a --> (f a))"
    6.27  
    6.28 -  isNSCont :: "[real=>real,real] => bool"
    6.29 +  isNSCont :: "[real => 'a::real_normed_vector, real] => bool"
    6.30      --{*NS definition dispenses with limit notions*}
    6.31 -  "isNSCont f a = (\<forall>y. y @= hypreal_of_real a -->
    6.32 -         ( *f* f) y @= hypreal_of_real (f a))"
    6.33 +  "isNSCont f a = (\<forall>y. y @= star_of a -->
    6.34 +         ( *f* f) y @= star_of (f a))"
    6.35  
    6.36    deriv:: "[real=>real,real,real] => bool"
    6.37      --{*Differentiation: D is derivative of function f at x*}
    6.38 @@ -79,12 +78,17 @@
    6.39  
    6.40  lemma LIM_eq:
    6.41       "f -- a --> L =
    6.42 -     (\<forall>r>0.\<exists>s>0.\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < s --> \<bar>f x - L\<bar> < r)"
    6.43 +     (\<forall>r>0.\<exists>s>0.\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < s --> norm (f x - L) < r)"
    6.44  by (simp add: LIM_def diff_minus)
    6.45  
    6.46 +lemma LIM_I:
    6.47 +     "(!!r. 0<r ==> \<exists>s>0.\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < s --> norm (f x - L) < r)
    6.48 +      ==> f -- a --> L"
    6.49 +by (simp add: LIM_eq)
    6.50 +
    6.51  lemma LIM_D:
    6.52       "[| f -- a --> L; 0<r |]
    6.53 -      ==> \<exists>s>0.\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < s --> \<bar>f x - L\<bar> < r"
    6.54 +      ==> \<exists>s>0.\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < s --> norm (f x - L) < r"
    6.55  by (simp add: LIM_eq)
    6.56  
    6.57  lemma LIM_const [simp]: "(%x. k) -- x --> k"
    6.58 @@ -93,76 +97,55 @@
    6.59  lemma LIM_add:
    6.60    assumes f: "f -- a --> L" and g: "g -- a --> M"
    6.61    shows "(%x. f x + g(x)) -- a --> (L + M)"
    6.62 -proof (unfold LIM_eq, clarify)
    6.63 +proof (rule LIM_I)
    6.64    fix r :: real
    6.65    assume r: "0 < r"
    6.66    from LIM_D [OF f half_gt_zero [OF r]]
    6.67    obtain fs
    6.68      where fs:    "0 < fs"
    6.69 -      and fs_lt: "\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < fs --> \<bar>f x - L\<bar> < r/2"
    6.70 +      and fs_lt: "\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < fs --> norm (f x - L) < r/2"
    6.71    by blast
    6.72    from LIM_D [OF g half_gt_zero [OF r]]
    6.73    obtain gs
    6.74      where gs:    "0 < gs"
    6.75 -      and gs_lt: "\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < gs --> \<bar>g x - M\<bar> < r/2"
    6.76 +      and gs_lt: "\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < gs --> norm (g x - M) < r/2"
    6.77    by blast
    6.78 -  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"
    6.79 +  show "\<exists>s>0.\<forall>x. x \<noteq> a \<and> \<bar>x-a\<bar> < s \<longrightarrow> norm (f x + g x - (L + M)) < r"
    6.80    proof (intro exI conjI strip)
    6.81      show "0 < min fs gs"  by (simp add: fs gs)
    6.82      fix x :: real
    6.83      assume "x \<noteq> a \<and> \<bar>x-a\<bar> < min fs gs"
    6.84      hence "x \<noteq> a \<and> \<bar>x-a\<bar> < fs \<and> \<bar>x-a\<bar> < gs" by simp
    6.85      with fs_lt gs_lt
    6.86 -    have "\<bar>f x - L\<bar> < r/2" and "\<bar>g x - M\<bar> < r/2" by blast+
    6.87 -    hence "\<bar>f x - L\<bar> + \<bar>g x - M\<bar> < r" by arith
    6.88 -    thus "\<bar>f x + g x - (L + M)\<bar> < r"
    6.89 -      by (blast intro: abs_diff_triangle_ineq order_le_less_trans)
    6.90 +    have "norm (f x - L) < r/2" and "norm (g x - M) < r/2" by blast+
    6.91 +    hence "norm (f x - L) + norm (g x - M) < r" by arith
    6.92 +    thus "norm (f x + g x - (L + M)) < r"
    6.93 +      by (blast intro: norm_diff_triangle_ineq order_le_less_trans)
    6.94    qed
    6.95  qed
    6.96  
    6.97 +lemma minus_diff_minus:
    6.98 +  fixes a b :: "'a::ab_group_add"
    6.99 +  shows "(- a) - (- b) = - (a - b)"
   6.100 +by simp
   6.101 +
   6.102  lemma LIM_minus: "f -- a --> L ==> (%x. -f(x)) -- a --> -L"
   6.103 -apply (simp add: LIM_eq)
   6.104 -apply (subgoal_tac "\<forall>x. \<bar>- f x + L\<bar> = \<bar>f x - L\<bar>")
   6.105 -apply (simp_all add: abs_if)
   6.106 -done
   6.107 +by (simp only: LIM_eq minus_diff_minus norm_minus_cancel)
   6.108  
   6.109  lemma LIM_add_minus:
   6.110      "[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) + -g(x)) -- x --> (l + -m)"
   6.111 -by (blast dest: LIM_add LIM_minus)
   6.112 +by (intro LIM_add LIM_minus)
   6.113  
   6.114  lemma LIM_diff:
   6.115      "[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) - g(x)) -- x --> l-m"
   6.116 -by (simp add: diff_minus LIM_add_minus)
   6.117 +by (simp only: diff_minus LIM_add LIM_minus)
   6.118  
   6.119  
   6.120  lemma LIM_const_not_eq: "k \<noteq> L ==> ~ ((%x. k) -- a --> L)"
   6.121 -proof (simp add: linorder_neq_iff LIM_eq, elim disjE)
   6.122 -  assume k: "k < L"
   6.123 -  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"
   6.124 -  proof (intro exI conjI strip)
   6.125 -    show "0 < L-k" by (simp add: k compare_rls)
   6.126 -    fix s :: real
   6.127 -    assume s: "0<s"
   6.128 -    { from s show "s/2 + a < a \<or> a < s/2 + a" by arith
   6.129 -     next
   6.130 -      from s show "\<bar>s / 2 + a - a\<bar> < s" by (simp add: abs_if)
   6.131 -     next
   6.132 -      from s show "~ \<bar>k-L\<bar> < L-k" by (simp add: abs_if) }
   6.133 -  qed
   6.134 -next
   6.135 -  assume k: "L < k"
   6.136 -  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"
   6.137 -  proof (intro exI conjI strip)
   6.138 -    show "0 < k-L" by (simp add: k compare_rls)
   6.139 -    fix s :: real
   6.140 -    assume s: "0<s"
   6.141 -    { from s show "s/2 + a < a \<or> a < s/2 + a" by arith
   6.142 -     next
   6.143 -      from s show "\<bar>s / 2 + a - a\<bar> < s" by (simp add: abs_if)
   6.144 -     next
   6.145 -      from s show "~ \<bar>k-L\<bar> < k-L" by (simp add: abs_if) }
   6.146 -  qed
   6.147 -qed
   6.148 +apply (simp add: LIM_eq)
   6.149 +apply (rule_tac x="norm (k - L)" in exI, simp, safe)
   6.150 +apply (rule_tac x="a + s/2" in exI, simp)
   6.151 +done
   6.152  
   6.153  lemma LIM_const_eq: "(%x. k) -- x --> L ==> k = L"
   6.154  apply (rule ccontr)
   6.155 @@ -175,31 +158,34 @@
   6.156  done
   6.157  
   6.158  lemma LIM_mult_zero:
   6.159 +  fixes f g :: "real \<Rightarrow> 'a::real_normed_algebra"
   6.160    assumes f: "f -- a --> 0" and g: "g -- a --> 0"
   6.161    shows "(%x. f(x) * g(x)) -- a --> 0"
   6.162 -proof (simp add: LIM_eq abs_mult, clarify)
   6.163 +proof (rule LIM_I, simp)
   6.164    fix r :: real
   6.165    assume r: "0<r"
   6.166    from LIM_D [OF f zero_less_one]
   6.167    obtain fs
   6.168      where fs:    "0 < fs"
   6.169 -      and fs_lt: "\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < fs --> \<bar>f x\<bar> < 1"
   6.170 +      and fs_lt: "\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < fs --> norm (f x) < 1"
   6.171    by auto
   6.172    from LIM_D [OF g r]
   6.173    obtain gs
   6.174      where gs:    "0 < gs"
   6.175 -      and gs_lt: "\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < gs --> \<bar>g x\<bar> < r"
   6.176 +      and gs_lt: "\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < gs --> norm (g x) < r"
   6.177    by auto
   6.178 -  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)"
   6.179 +  show "\<exists>s. 0 < s \<and> (\<forall>x. x \<noteq> a \<and> \<bar>x-a\<bar> < s \<longrightarrow> norm (f x * g x) < r)"
   6.180    proof (intro exI conjI strip)
   6.181      show "0 < min fs gs"  by (simp add: fs gs)
   6.182      fix x :: real
   6.183      assume "x \<noteq> a \<and> \<bar>x-a\<bar> < min fs gs"
   6.184      hence  "x \<noteq> a \<and> \<bar>x-a\<bar> < fs \<and> \<bar>x-a\<bar> < gs" by simp
   6.185      with fs_lt gs_lt
   6.186 -    have "\<bar>f x\<bar> < 1" and "\<bar>g x\<bar> < r" by blast+
   6.187 -    hence "\<bar>f x\<bar> * \<bar>g x\<bar> < 1*r" by (rule abs_mult_less)
   6.188 -    thus "\<bar>f x\<bar> * \<bar>g x\<bar> < r" by simp
   6.189 +    have "norm (f x) < 1" and "norm (g x) < r" by blast+
   6.190 +    hence "norm (f x) * norm (g x) < 1*r"
   6.191 +      by (rule mult_strict_mono' [OF _ _ norm_ge_zero norm_ge_zero])
   6.192 +    thus "norm (f x * g x) < r"
   6.193 +      by (simp add: order_le_less_trans [OF norm_mult_ineq])
   6.194    qed
   6.195  qed
   6.196  
   6.197 @@ -223,62 +209,71 @@
   6.198  
   6.199  text{*Standard and NS definitions of Limit*} (*NEEDS STRUCTURING*)
   6.200  lemma LIM_NSLIM:
   6.201 -      "f -- x --> L ==> f -- x --NS> L"
   6.202 -apply (simp add: LIM_def NSLIM_def approx_def)
   6.203 +      "f -- a --> L ==> f -- a --NS> L"
   6.204 +apply (simp add: LIM_def NSLIM_def approx_def, safe)
   6.205 +apply (rule_tac x="x" in star_cases)
   6.206 +apply (simp add: star_of_def star_n_minus star_n_add starfun)
   6.207  apply (simp add: Infinitesimal_FreeUltrafilterNat_iff, safe)
   6.208 -apply (rule_tac x = xa in star_cases)
   6.209 -apply (auto simp add: real_add_minus_iff starfun star_n_minus star_of_def star_n_add star_n_eq_iff)
   6.210 -apply (rule bexI [OF _ Rep_star_star_n], clarify)
   6.211 +apply (simp add: star_n_eq_iff)
   6.212  apply (drule_tac x = u in spec, clarify)
   6.213  apply (drule_tac x = s in spec, clarify)
   6.214 -apply (subgoal_tac "\<forall>n::nat. (Xa n) \<noteq> x & \<bar>(Xa n) + - x\<bar> < s --> \<bar>f (Xa n) + - L\<bar> < u")
   6.215 -prefer 2 apply blast
   6.216 -apply (drule FreeUltrafilterNat_all, ultra)
   6.217 +apply (simp only: FUFNat.Collect_not [symmetric])
   6.218 +apply (elim ultra, simp)
   6.219  done
   6.220  
   6.221  
   6.222  subsubsection{*Limit: The NS definition implies the standard definition.*}
   6.223  
   6.224 -lemma lemma_LIM: "\<forall>s>0.\<exists>xa.  xa \<noteq> x &
   6.225 -         \<bar>xa + - x\<bar> < s  & r \<le> \<bar>f xa + -L\<bar>
   6.226 -      ==> \<forall>n::nat. \<exists>xa.  xa \<noteq> x &
   6.227 -              \<bar>xa + -x\<bar> < inverse(real(Suc n)) & r \<le> \<bar>f xa + -L\<bar>"
   6.228 +lemma lemma_LIM:
   6.229 +  fixes L :: "'a::real_normed_vector"
   6.230 +  shows "\<forall>s>0. \<exists>x. x \<noteq> a \<and> \<bar>x + - a\<bar> < s \<and> \<not> norm (f x + -L) < r
   6.231 +      ==> \<forall>n::nat. \<exists>x. x \<noteq> a \<and>
   6.232 +              \<bar>x + -a\<bar> < inverse(real(Suc n)) \<and> \<not> norm (f x + -L) < r"
   6.233  apply clarify
   6.234  apply (cut_tac n1 = n in real_of_nat_Suc_gt_zero [THEN positive_imp_inverse_positive], auto)
   6.235  done
   6.236  
   6.237  lemma lemma_skolemize_LIM2:
   6.238 -     "\<forall>s>0.\<exists>xa.  xa \<noteq> x & \<bar>xa + - x\<bar> < s  & r \<le> \<bar>f xa + -L\<bar>
   6.239 -      ==> \<exists>X. \<forall>n::nat. X n \<noteq> x &
   6.240 -                \<bar>X n + -x\<bar> < inverse(real(Suc n)) & r \<le> abs(f (X n) + -L)"
   6.241 +  fixes L :: "'a::real_normed_vector"
   6.242 +  shows "\<forall>s>0. \<exists>x. x \<noteq> a \<and> \<bar>x + - a\<bar> < s \<and> \<not> norm (f x + -L) < r
   6.243 +      ==> \<exists>X. \<forall>n::nat. X n \<noteq> a \<and>
   6.244 +                \<bar>X n + -a\<bar> < inverse(real(Suc n)) \<and> \<not> norm(f (X n) + -L) < r"
   6.245  apply (drule lemma_LIM)
   6.246  apply (drule choice, blast)
   6.247  done
   6.248  
   6.249 -lemma lemma_simp: "\<forall>n. X n \<noteq> x &
   6.250 -          \<bar>X n + - x\<bar> < inverse (real(Suc n)) &
   6.251 -          r \<le> abs (f (X n) + - L) ==>
   6.252 -          \<forall>n. \<bar>X n + - x\<bar> < inverse (real(Suc n))"
   6.253 +lemma FreeUltrafilterNat_most: "\<exists>N. \<forall>n\<ge>N. P n \<Longrightarrow> {n. P n} \<in> \<U>"
   6.254 +apply (erule exE)
   6.255 +apply (rule_tac u="{n. N \<le> n}" in FUFNat.subset)
   6.256 +apply (rule cofinite_mem_FreeUltrafilterNat)
   6.257 +apply (simp add: Collect_neg_eq [symmetric])
   6.258 +apply (simp add: linorder_not_le finite_nat_segment)
   6.259 +apply fast
   6.260 +done
   6.261 +
   6.262 +lemma lemma_simp: "\<forall>n. X n \<noteq> a &
   6.263 +          \<bar>X n + - a\<bar> < inverse (real(Suc n)) &
   6.264 +          \<not> norm (f (X n) + - L) < r ==>
   6.265 +          \<forall>n. \<bar>X n + - a\<bar> < inverse (real(Suc n))"
   6.266  by auto
   6.267  
   6.268  
   6.269  text{*NSLIM => LIM*}
   6.270  
   6.271 -lemma NSLIM_LIM: "f -- x --NS> L ==> f -- x --> L"
   6.272 +lemma NSLIM_LIM: "f -- a --NS> L ==> f -- a --> L"
   6.273  apply (simp add: LIM_def NSLIM_def approx_def)
   6.274 -apply (simp add: Infinitesimal_FreeUltrafilterNat_iff, clarify)
   6.275 -apply (rule ccontr, simp)
   6.276 -apply (simp add: linorder_not_less)
   6.277 +apply (rule ccontr, simp, clarify)
   6.278  apply (drule lemma_skolemize_LIM2, safe)
   6.279  apply (drule_tac x = "star_n X" in spec)
   6.280 -apply (auto simp add: starfun star_n_minus star_of_def star_n_add star_n_eq_iff)
   6.281 -apply (drule lemma_simp [THEN real_seq_to_hypreal_Infinitesimal])
   6.282 -apply (simp add: Infinitesimal_FreeUltrafilterNat_iff star_of_def star_n_minus star_n_add star_n_eq_iff, blast)
   6.283 -apply (drule spec, drule mp, assumption)
   6.284 -apply (drule FreeUltrafilterNat_all, ultra)
   6.285 +apply (drule mp, rule conjI)
   6.286 +apply (simp add: star_of_def star_n_eq_iff)
   6.287 +apply (rule real_seq_to_hypreal_Infinitesimal, simp)
   6.288 +apply (simp add: starfun star_of_def star_n_minus star_n_add)
   6.289 +apply (simp add: Infinitesimal_FreeUltrafilterNat_iff)
   6.290 +apply (drule spec, drule (1) mp)
   6.291 +apply simp
   6.292  done
   6.293  
   6.294 -
   6.295  theorem LIM_NSLIM_iff: "(f -- x --> L) = (f -- x --NS> L)"
   6.296  by (blast intro: LIM_NSLIM NSLIM_LIM)
   6.297  
   6.298 @@ -286,12 +281,15 @@
   6.299        The properties hold for standard limits as well!*}
   6.300  
   6.301  lemma NSLIM_mult:
   6.302 -     "[| f -- x --NS> l; g -- x --NS> m |]
   6.303 +  fixes l m :: "'a::real_normed_algebra"
   6.304 +  shows "[| f -- x --NS> l; g -- x --NS> m |]
   6.305        ==> (%x. f(x) * g(x)) -- x --NS> (l * m)"
   6.306  by (auto simp add: NSLIM_def intro!: approx_mult_HFinite)
   6.307  
   6.308  lemma LIM_mult2:
   6.309 -     "[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) * g(x)) -- x --> (l * m)"
   6.310 +  fixes l m :: "'a::real_normed_algebra"
   6.311 +  shows "[| f -- x --> l; g -- x --> m |]
   6.312 +      ==> (%x. f(x) * g(x)) -- x --> (l * m)"
   6.313  by (simp add: LIM_NSLIM_iff NSLIM_mult)
   6.314  
   6.315  lemma NSLIM_add:
   6.316 @@ -325,14 +323,18 @@
   6.317  
   6.318  
   6.319  lemma NSLIM_inverse:
   6.320 -     "[| f -- a --NS> L;  L \<noteq> 0 |]
   6.321 +  fixes L :: "'a::{real_normed_div_algebra,division_by_zero}"
   6.322 +  shows "[| f -- a --NS> L;  L \<noteq> 0 |]
   6.323        ==> (%x. inverse(f(x))) -- a --NS> (inverse L)"
   6.324  apply (simp add: NSLIM_def, clarify)
   6.325  apply (drule spec)
   6.326 -apply (auto simp add: hypreal_of_real_approx_inverse)
   6.327 +apply (auto simp add: star_of_approx_inverse)
   6.328  done
   6.329  
   6.330 -lemma LIM_inverse: "[| f -- a --> L; L \<noteq> 0 |] ==> (%x. inverse(f(x))) -- a --> (inverse L)"
   6.331 +lemma LIM_inverse:
   6.332 +  fixes L :: "'a::{real_normed_div_algebra,division_by_zero}"
   6.333 +  shows "[| f -- a --> L; L \<noteq> 0 |]
   6.334 +      ==> (%x. inverse(f(x))) -- a --> (inverse L)"
   6.335  by (simp add: LIM_NSLIM_iff NSLIM_inverse)
   6.336  
   6.337  
   6.338 @@ -357,19 +359,15 @@
   6.339  apply (auto simp add: diff_minus add_assoc)
   6.340  done
   6.341  
   6.342 -lemma NSLIM_not_zero: "k \<noteq> 0 ==> ~ ((%x. k) -- x --NS> 0)"
   6.343 +lemma NSLIM_const_not_eq: "k \<noteq> L ==> ~ ((%x. k) -- x --NS> L)"
   6.344  apply (simp add: NSLIM_def)
   6.345  apply (rule_tac x = "hypreal_of_real x + epsilon" in exI)
   6.346  apply (auto intro: Infinitesimal_add_approx_self [THEN approx_sym]
   6.347              simp add: hypreal_epsilon_not_zero)
   6.348  done
   6.349  
   6.350 -lemma NSLIM_const_not_eq: "k \<noteq> L ==> ~ ((%x. k) -- x --NS> L)"
   6.351 -apply (simp add: NSLIM_def)
   6.352 -apply (rule_tac x = "hypreal_of_real x + epsilon" in exI)
   6.353 -apply (auto intro: Infinitesimal_add_approx_self [THEN approx_sym]
   6.354 -            simp add: hypreal_epsilon_not_zero)
   6.355 -done
   6.356 +lemma NSLIM_not_zero: "k \<noteq> 0 ==> ~ ((%x. k) -- x --NS> 0)"
   6.357 +by (rule NSLIM_const_not_eq)
   6.358  
   6.359  lemma NSLIM_const_eq: "(%x. k) -- x --NS> L ==> k = L"
   6.360  apply (rule ccontr)
   6.361 @@ -381,19 +379,24 @@
   6.362  apply (drule NSLIM_minus)
   6.363  apply (drule NSLIM_add, assumption)
   6.364  apply (auto dest!: NSLIM_const_eq [symmetric])
   6.365 +apply (simp add: diff_def [symmetric])
   6.366  done
   6.367  
   6.368  lemma LIM_unique2: "[| f -- x --> L; f -- x --> M |] ==> L = M"
   6.369  by (simp add: LIM_NSLIM_iff NSLIM_unique)
   6.370  
   6.371  
   6.372 -lemma NSLIM_mult_zero: "[| f -- x --NS> 0; g -- x --NS> 0 |] ==> (%x. f(x)*g(x)) -- x --NS> 0"
   6.373 +lemma NSLIM_mult_zero:
   6.374 +  fixes f g :: "real \<Rightarrow> 'a::real_normed_algebra"
   6.375 +  shows "[| f -- x --NS> 0; g -- x --NS> 0 |] ==> (%x. f(x)*g(x)) -- x --NS> 0"
   6.376  by (drule NSLIM_mult, auto)
   6.377  
   6.378  (* we can use the corresponding thm LIM_mult2 *)
   6.379  (* for standard definition of limit           *)
   6.380  
   6.381 -lemma LIM_mult_zero2: "[| f -- x --> 0; g -- x --> 0 |] ==> (%x. f(x)*g(x)) -- x --> 0"
   6.382 +lemma LIM_mult_zero2:
   6.383 +  fixes f g :: "real \<Rightarrow> 'a::real_normed_algebra"
   6.384 +  shows "[| f -- x --> 0; g -- x --> 0 |] ==> (%x. f(x)*g(x)) -- x --> 0"
   6.385  by (drule LIM_mult2, auto)
   6.386  
   6.387  
   6.388 @@ -472,7 +475,9 @@
   6.389  by (auto intro: approx_add simp add: isNSCont_isCont_iff [symmetric] isNSCont_def)
   6.390  
   6.391  text{*mult continuous*}
   6.392 -lemma isCont_mult: "[| isCont f a; isCont g a |] ==> isCont (%x. f(x) * g(x)) a"
   6.393 +lemma isCont_mult:
   6.394 +  fixes f g :: "real \<Rightarrow> 'a::real_normed_algebra"
   6.395 +  shows "[| isCont f a; isCont g a |] ==> isCont (%x. f(x) * g(x)) a"
   6.396  by (auto intro!: starfun_mult_HFinite_approx
   6.397              simp del: starfun_mult [symmetric]
   6.398              simp add: isNSCont_isCont_iff [symmetric] isNSCont_def)
   6.399 @@ -492,12 +497,15 @@
   6.400  by (auto simp add: isNSCont_isCont_iff [symmetric] isNSCont_minus)
   6.401  
   6.402  lemma isCont_inverse:
   6.403 -      "[| isCont f x; f x \<noteq> 0 |] ==> isCont (%x. inverse (f x)) x"
   6.404 +  fixes f :: "real \<Rightarrow> 'a::{real_normed_div_algebra,division_by_zero}"
   6.405 +  shows "[| isCont f x; f x \<noteq> 0 |] ==> isCont (%x. inverse (f x)) x"
   6.406  apply (simp add: isCont_def)
   6.407  apply (blast intro: LIM_inverse)
   6.408  done
   6.409  
   6.410 -lemma isNSCont_inverse: "[| isNSCont f x; f x \<noteq> 0 |] ==> isNSCont (%x. inverse (f x)) x"
   6.411 +lemma isNSCont_inverse:
   6.412 +  fixes f :: "real \<Rightarrow> 'a::{real_normed_div_algebra,division_by_zero}"
   6.413 +  shows "[| isNSCont f x; f x \<noteq> 0 |] ==> isNSCont (%x. inverse (f x)) x"
   6.414  by (auto intro: isCont_inverse simp add: isNSCont_isCont_iff)
   6.415  
   6.416  lemma isCont_diff:
   6.417 @@ -578,17 +586,15 @@
   6.418  
   6.419  lemma isUCont_isNSUCont: "isUCont f ==> isNSUCont f"
   6.420  apply (simp add: isNSUCont_def isUCont_def approx_def)
   6.421 +apply (simp add: all_star_eq starfun star_n_minus star_n_add)
   6.422  apply (simp add: Infinitesimal_FreeUltrafilterNat_iff, safe)
   6.423 -apply (rule_tac x = x in star_cases)
   6.424 -apply (rule_tac x = y in star_cases)
   6.425 -apply (auto simp add: starfun star_n_minus star_n_add)
   6.426 -apply (rule bexI [OF _ Rep_star_star_n], safe)
   6.427 +apply (rename_tac Xa Xb u)
   6.428  apply (drule_tac x = u in spec, clarify)
   6.429  apply (drule_tac x = s in spec, clarify)
   6.430  apply (subgoal_tac "\<forall>n::nat. abs ((Xa n) + - (Xb n)) < s --> abs (f (Xa n) + - f (Xb n)) < u")
   6.431  prefer 2 apply blast
   6.432  apply (erule_tac V = "\<forall>x y. \<bar>x + - y\<bar> < s --> \<bar>f x + - f y\<bar> < u" in thin_rl)
   6.433 -apply (drule FreeUltrafilterNat_all, ultra)
   6.434 +apply (erule ultra, simp)
   6.435  done
   6.436  
   6.437  lemma lemma_LIMu: "\<forall>s>0.\<exists>z y. \<bar>z + - y\<bar> < s & r \<le> \<bar>f z + -f y\<bar>
   6.438 @@ -615,17 +621,17 @@
   6.439  
   6.440  lemma isNSUCont_isUCont:
   6.441       "isNSUCont f ==> isUCont f"
   6.442 -apply (simp add: isNSUCont_def isUCont_def approx_def)
   6.443 -apply (simp add: Infinitesimal_FreeUltrafilterNat_iff, safe)
   6.444 +apply (simp add: isNSUCont_def isUCont_def approx_def, safe)
   6.445  apply (rule ccontr, simp)
   6.446  apply (simp add: linorder_not_less)
   6.447  apply (drule lemma_skolemize_LIM2u, safe)
   6.448  apply (drule_tac x = "star_n X" in spec)
   6.449  apply (drule_tac x = "star_n Y" in spec)
   6.450 -apply (simp add: starfun star_n_minus star_n_add, auto)
   6.451 -apply (drule lemma_simpu [THEN real_seq_to_hypreal_Infinitesimal2])
   6.452 -apply (simp add: Infinitesimal_FreeUltrafilterNat_iff star_n_minus star_n_add, blast)
   6.453 -apply (drule_tac x = r in spec, clarify)
   6.454 +apply (drule mp)
   6.455 +apply (rule real_seq_to_hypreal_Infinitesimal2, simp)
   6.456 +apply (simp add: all_star_eq starfun star_n_minus star_n_add)
   6.457 +apply (simp add: Infinitesimal_FreeUltrafilterNat_iff)
   6.458 +apply (drule spec, drule (1) mp)
   6.459  apply (drule FreeUltrafilterNat_all, ultra)
   6.460  done
   6.461  
   6.462 @@ -677,11 +683,6 @@
   6.463  
   6.464  subsubsection{*Alternative definition for differentiability*}
   6.465  
   6.466 -lemma LIM_I:
   6.467 -     "(!!r. 0<r ==> \<exists>s>0.\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < s --> \<bar>f x - L\<bar> < r)
   6.468 -      ==> f -- a --> L"
   6.469 -by (simp add: LIM_eq)
   6.470 -
   6.471  lemma DERIV_LIM_iff:
   6.472       "((%h. (f(a + h) - f(a)) / h) -- 0 --> D) =
   6.473        ((%x. (f(x)-f(a)) / (x-a)) -- a --> D)"
   6.474 @@ -695,14 +696,14 @@
   6.475        and s_lt: "\<forall>x. x \<noteq> 0 & \<bar>x\<bar> < s --> \<bar>(f (a + x) - f a) / x - D\<bar> < r"
   6.476    by auto
   6.477    show "\<exists>s. 0 < s \<and>
   6.478 -            (\<forall>x. x \<noteq> a \<and> \<bar>x-a\<bar> < s \<longrightarrow> \<bar>(f x - f a) / (x-a) - D\<bar> < r)"
   6.479 +            (\<forall>x. x \<noteq> a \<and> \<bar>x-a\<bar> < s \<longrightarrow> norm ((f x - f a) / (x-a) - D) < r)"
   6.480    proof (intro exI conjI strip)
   6.481      show "0 < s"  by (rule s)
   6.482    next
   6.483      fix x::real
   6.484      assume "x \<noteq> a \<and> \<bar>x-a\<bar> < s"
   6.485      with s_lt [THEN spec [where x="x-a"]]
   6.486 -    show "\<bar>(f x - f a) / (x-a) - D\<bar> < r" by auto
   6.487 +    show "norm ((f x - f a) / (x-a) - D) < r" by auto
   6.488    qed
   6.489  next
   6.490    fix r::real
   6.491 @@ -714,14 +715,14 @@
   6.492        and s_lt: "\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < s --> \<bar>(f x - f a)/(x-a) - D\<bar> < r"
   6.493    by auto
   6.494    show "\<exists>s. 0 < s \<and>
   6.495 -            (\<forall>x. x \<noteq> 0 & \<bar>x - 0\<bar> < s --> \<bar>(f (a + x) - f a) / x - D\<bar> < r)"
   6.496 +            (\<forall>x. x \<noteq> 0 & \<bar>x - 0\<bar> < s --> norm ((f (a + x) - f a) / x - D) < r)"
   6.497    proof (intro exI conjI strip)
   6.498      show "0 < s"  by (rule s)
   6.499    next
   6.500      fix x::real
   6.501      assume "x \<noteq> 0 \<and> \<bar>x - 0\<bar> < s"
   6.502      with s_lt [THEN spec [where x="x+a"]]
   6.503 -    show "\<bar>(f (a + x) - f a) / x - D\<bar> < r" by (auto simp add: add_ac)
   6.504 +    show "norm ((f (a + x) - f a) / x - D) < r" by (auto simp add: add_ac)
   6.505    qed
   6.506  qed
   6.507  
   6.508 @@ -1236,7 +1237,7 @@
   6.509  lemma f_inc_g_dec_Beq_f: "[| \<forall>n. f(n) \<le> f(Suc n);
   6.510           \<forall>n. g(Suc n) \<le> g(n);
   6.511           \<forall>n. f(n) \<le> g(n) |]
   6.512 -      ==> Bseq f"
   6.513 +      ==> Bseq (f :: nat \<Rightarrow> real)"
   6.514  apply (rule_tac k = "f 0" and K = "g 0" in BseqI2, rule allI)
   6.515  apply (induct_tac "n")
   6.516  apply (auto intro: order_trans)
   6.517 @@ -1248,7 +1249,7 @@
   6.518  lemma f_inc_g_dec_Beq_g: "[| \<forall>n. f(n) \<le> f(Suc n);
   6.519           \<forall>n. g(Suc n) \<le> g(n);
   6.520           \<forall>n. f(n) \<le> g(n) |]
   6.521 -      ==> Bseq g"
   6.522 +      ==> Bseq (g :: nat \<Rightarrow> real)"
   6.523  apply (subst Bseq_minus_iff [symmetric])
   6.524  apply (rule_tac g = "%x. - (f x)" in f_inc_g_dec_Beq_f)
   6.525  apply auto
   6.526 @@ -1282,7 +1283,7 @@
   6.527  lemma lemma_nest: "[| \<forall>n. f(n) \<le> f(Suc n);
   6.528           \<forall>n. g(Suc n) \<le> g(n);
   6.529           \<forall>n. f(n) \<le> g(n) |]
   6.530 -      ==> \<exists>l m. l \<le> m &  ((\<forall>n. f(n) \<le> l) & f ----> l) &
   6.531 +      ==> \<exists>l m :: real. l \<le> m &  ((\<forall>n. f(n) \<le> l) & f ----> l) &
   6.532                              ((\<forall>n. m \<le> g(n)) & g ----> m)"
   6.533  apply (subgoal_tac "monoseq f & monoseq g")
   6.534  prefer 2 apply (force simp add: LIMSEQ_iff monoseq_Suc)
   6.535 @@ -1299,7 +1300,7 @@
   6.536           \<forall>n. g(Suc n) \<le> g(n);
   6.537           \<forall>n. f(n) \<le> g(n);
   6.538           (%n. f(n) - g(n)) ----> 0 |]
   6.539 -      ==> \<exists>l. ((\<forall>n. f(n) \<le> l) & f ----> l) &
   6.540 +      ==> \<exists>l::real. ((\<forall>n. f(n) \<le> l) & f ----> l) &
   6.541                  ((\<forall>n. l \<le> g(n)) & g ----> l)"
   6.542  apply (drule lemma_nest, auto)
   6.543  apply (subgoal_tac "l = m")
   6.544 @@ -1414,7 +1415,7 @@
   6.545  
   6.546  subsection{*Intermediate Value Theorem: Prove Contrapositive by Bisection*}
   6.547  
   6.548 -lemma IVT: "[| f(a) \<le> y; y \<le> f(b);
   6.549 +lemma IVT: "[| f(a) \<le> (y::real); y \<le> f(b);
   6.550           a \<le> b;
   6.551           (\<forall>x. a \<le> x & x \<le> b --> isCont f x) |]
   6.552        ==> \<exists>x. a \<le> x & x \<le> b & f(x) = y"
   6.553 @@ -1441,7 +1442,7 @@
   6.554  apply (case_tac "x \<le> aa", simp_all)
   6.555  done
   6.556  
   6.557 -lemma IVT2: "[| f(b) \<le> y; y \<le> f(a);
   6.558 +lemma IVT2: "[| f(b) \<le> (y::real); y \<le> f(a);
   6.559           a \<le> b;
   6.560           (\<forall>x. a \<le> x & x \<le> b --> isCont f x)
   6.561        |] ==> \<exists>x. a \<le> x & x \<le> b & f(x) = y"
   6.562 @@ -1451,13 +1452,13 @@
   6.563  done
   6.564  
   6.565  (*HOL style here: object-level formulations*)
   6.566 -lemma IVT_objl: "(f(a) \<le> y & y \<le> f(b) & a \<le> b &
   6.567 +lemma IVT_objl: "(f(a) \<le> (y::real) & y \<le> f(b) & a \<le> b &
   6.568        (\<forall>x. a \<le> x & x \<le> b --> isCont f x))
   6.569        --> (\<exists>x. a \<le> x & x \<le> b & f(x) = y)"
   6.570  apply (blast intro: IVT)
   6.571  done
   6.572  
   6.573 -lemma IVT2_objl: "(f(b) \<le> y & y \<le> f(a) & a \<le> b &
   6.574 +lemma IVT2_objl: "(f(b) \<le> (y::real) & y \<le> f(a) & a \<le> b &
   6.575        (\<forall>x. a \<le> x & x \<le> b --> isCont f x))
   6.576        --> (\<exists>x. a \<le> x & x \<le> b & f(x) = y)"
   6.577  apply (blast intro: IVT2)
   6.578 @@ -1467,7 +1468,7 @@
   6.579  
   6.580  lemma isCont_bounded:
   6.581       "[| a \<le> b; \<forall>x. a \<le> x & x \<le> b --> isCont f x |]
   6.582 -      ==> \<exists>M. \<forall>x. a \<le> x & x \<le> b --> f(x) \<le> M"
   6.583 +      ==> \<exists>M::real. \<forall>x. a \<le> x & x \<le> b --> f(x) \<le> M"
   6.584  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)
   6.585  apply safe
   6.586  apply simp_all
   6.587 @@ -1497,7 +1498,7 @@
   6.588  by (blast intro: reals_complete)
   6.589  
   6.590  lemma isCont_has_Ub: "[| a \<le> b; \<forall>x. a \<le> x & x \<le> b --> isCont f x |]
   6.591 -         ==> \<exists>M. (\<forall>x. a \<le> x & x \<le> b --> f(x) \<le> M) &
   6.592 +         ==> \<exists>M::real. (\<forall>x. a \<le> x & x \<le> b --> f(x) \<le> M) &
   6.593                     (\<forall>N. N < M --> (\<exists>x. a \<le> x & x \<le> b & N < f(x)))"
   6.594  apply (cut_tac S = "Collect (%y. \<exists>x. a \<le> x & x \<le> b & y = f x)"
   6.595          in lemma_reals_complete)
   6.596 @@ -1513,7 +1514,7 @@
   6.597  lemma isCont_eq_Ub:
   6.598    assumes le: "a \<le> b"
   6.599        and con: "\<forall>x. a \<le> x & x \<le> b --> isCont f x"
   6.600 -  shows "\<exists>M. (\<forall>x. a \<le> x & x \<le> b --> f(x) \<le> M) &
   6.601 +  shows "\<exists>M::real. (\<forall>x. a \<le> x & x \<le> b --> f(x) \<le> M) &
   6.602               (\<exists>x. a \<le> x & x \<le> b & f(x) = M)"
   6.603  proof -
   6.604    from isCont_has_Ub [OF le con]
   6.605 @@ -1553,7 +1554,7 @@
   6.606  text{*Same theorem for lower bound*}
   6.607  
   6.608  lemma isCont_eq_Lb: "[| a \<le> b; \<forall>x. a \<le> x & x \<le> b --> isCont f x |]
   6.609 -         ==> \<exists>M. (\<forall>x. a \<le> x & x \<le> b --> M \<le> f(x)) &
   6.610 +         ==> \<exists>M::real. (\<forall>x. a \<le> x & x \<le> b --> M \<le> f(x)) &
   6.611                     (\<exists>x. a \<le> x & x \<le> b & f(x) = M)"
   6.612  apply (subgoal_tac "\<forall>x. a \<le> x & x \<le> b --> isCont (%x. - (f x)) x")
   6.613  prefer 2 apply (blast intro: isCont_minus)
   6.614 @@ -1566,7 +1567,7 @@
   6.615  text{*Another version.*}
   6.616  
   6.617  lemma isCont_Lb_Ub: "[|a \<le> b; \<forall>x. a \<le> x & x \<le> b --> isCont f x |]
   6.618 -      ==> \<exists>L M. (\<forall>x. a \<le> x & x \<le> b --> L \<le> f(x) & f(x) \<le> M) &
   6.619 +      ==> \<exists>L M::real. (\<forall>x. a \<le> x & x \<le> b --> L \<le> f(x) & f(x) \<le> M) &
   6.620            (\<forall>y. L \<le> y & y \<le> M --> (\<exists>x. a \<le> x & x \<le> b & (f(x) = y)))"
   6.621  apply (frule isCont_eq_Lb)
   6.622  apply (frule_tac [2] isCont_eq_Ub)
   6.623 @@ -1925,6 +1926,7 @@
   6.624  strict maximum at an end point, not in the middle.*}
   6.625  
   6.626  lemma lemma_isCont_inj:
   6.627 +  fixes f :: "real \<Rightarrow> real"
   6.628    assumes d: "0 < d"
   6.629        and inj [rule_format]: "\<forall>z. \<bar>z-x\<bar> \<le> d --> g(f z) = z"
   6.630        and cont: "\<forall>z. \<bar>z-x\<bar> \<le> d --> isCont f z"
   6.631 @@ -1966,7 +1968,8 @@
   6.632  text{*Similar version for lower bound.*}
   6.633  
   6.634  lemma lemma_isCont_inj2:
   6.635 -     "[|0 < d; \<forall>z. \<bar>z-x\<bar> \<le> d --> g(f z) = z;
   6.636 +  fixes f g :: "real \<Rightarrow> real"
   6.637 +  shows "[|0 < d; \<forall>z. \<bar>z-x\<bar> \<le> d --> g(f z) = z;
   6.638          \<forall>z. \<bar>z-x\<bar> \<le> d --> isCont f z |]
   6.639        ==> \<exists>z. \<bar>z-x\<bar> \<le> d & f z < f x"
   6.640  apply (insert lemma_isCont_inj
   6.641 @@ -1978,6 +1981,7 @@
   6.642  @{text "f[[x - d, x + d]]"} .*}
   6.643  
   6.644  lemma isCont_inj_range:
   6.645 +  fixes f :: "real \<Rightarrow> real"
   6.646    assumes d: "0 < d"
   6.647        and inj: "\<forall>z. \<bar>z-x\<bar> \<le> d --> g(f z) = z"
   6.648        and cont: "\<forall>z. \<bar>z-x\<bar> \<le> d --> isCont f z"
   6.649 @@ -2205,35 +2209,35 @@
   6.650    shows "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L"
   6.651  proof -
   6.652    {
   6.653 -    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)
   6.654 +    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)
   6.655      
   6.656      fix S
   6.657      assume as: "(\<forall>n. S n \<noteq> a) \<and> S ----> a"
   6.658      then have "S ----> a" by auto
   6.659 -    then have Sdef: "(\<forall>r. 0 < r --> (\<exists>no. \<forall>n. no \<le> n --> \<bar>S n + -a\<bar> < r))" by (unfold LIMSEQ_def)
   6.660 +    then have Sdef: "(\<forall>r. 0 < r --> (\<exists>no. \<forall>n. no \<le> n --> norm (S n + -a) < r))" by (unfold LIMSEQ_def)
   6.661      {
   6.662        fix r
   6.663 -      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
   6.664 +      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
   6.665        {
   6.666          assume rgz: "0 < r"
   6.667  
   6.668 -        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 
   6.669 -        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
   6.670 -        then have aux: "\<forall>x. x\<noteq>a \<and> \<bar>x + -a\<bar> < s \<longrightarrow> \<bar>X x + -L\<bar> < r" by auto
   6.671 +        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 
   6.672 +        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
   6.673 +        then have aux: "\<forall>x. x\<noteq>a \<and> \<bar>x + -a\<bar> < s \<longrightarrow> norm (X x + -L) < r" by auto
   6.674          {
   6.675            fix n
   6.676 -          from aux have "S n \<noteq> a \<and> \<bar>S n + -a\<bar> < s \<longrightarrow> \<bar>X (S n) + -L\<bar> < r" by simp
   6.677 -          with as have imp2: "\<bar>S n + -a\<bar> < s --> \<bar>X (S n) + -L\<bar> < r" by auto
   6.678 +          from aux have "S n \<noteq> a \<and> \<bar>S n + -a\<bar> < s \<longrightarrow> norm (X (S n) + -L) < r" by simp
   6.679 +          with as have imp2: "\<bar>S n + -a\<bar> < s --> norm (X (S n) + -L) < r" by auto
   6.680          }
   6.681 -        hence "\<forall>n. \<bar>S n + -a\<bar> < s --> \<bar>X (S n) + -L\<bar> < r" ..
   6.682 +        hence "\<forall>n. \<bar>S n + -a\<bar> < s --> norm (X (S n) + -L) < r" ..
   6.683          moreover
   6.684          from Sdef sdef have imp1: "\<exists>no. \<forall>n. no \<le> n --> \<bar>S n + -a\<bar> < s" by auto  
   6.685          then obtain no where "\<forall>n. no \<le> n --> \<bar>S n + -a\<bar> < s" by auto
   6.686 -        ultimately have "\<forall>n. no \<le> n \<longrightarrow> \<bar>X (S n) + -L\<bar> < r" by simp
   6.687 -        hence "\<exists>no. \<forall>n. no \<le> n \<longrightarrow> \<bar>X (S n) + -L\<bar> < r" by auto
   6.688 +        ultimately have "\<forall>n. no \<le> n \<longrightarrow> norm (X (S n) + -L) < r" by simp
   6.689 +        hence "\<exists>no. \<forall>n. no \<le> n \<longrightarrow> norm (X (S n) + -L) < r" by auto
   6.690        }
   6.691      }
   6.692 -    hence "(\<forall>r. 0 < r --> (\<exists>no. \<forall>n. no \<le> n --> \<bar>X (S n) + -L\<bar> < r))" by simp
   6.693 +    hence "(\<forall>r. 0 < r --> (\<exists>no. \<forall>n. no \<le> n --> norm (X (S n) + -L) < r))" by simp
   6.694      hence "(\<lambda>n. X (S n)) ----> L" by (fold LIMSEQ_def)
   6.695    }
   6.696    thus ?thesis by simp
   6.697 @@ -2246,12 +2250,12 @@
   6.698    shows "X -- a --> L"
   6.699  proof (rule ccontr)
   6.700    assume "\<not> (X -- a --> L)"
   6.701 -  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)
   6.702 -  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
   6.703 -  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)
   6.704 -  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
   6.705 +  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)
   6.706 +  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
   6.707 +  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)
   6.708 +  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
   6.709  
   6.710 -  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"
   6.711 +  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"
   6.712    have "?F ----> a"
   6.713    proof -
   6.714      {
   6.715 @@ -2270,10 +2274,10 @@
   6.716            "\<bar>?F n + -a\<bar> < inverse (real (Suc n))"
   6.717          proof -
   6.718            from rdef have
   6.719 -            "\<exists>x. x\<noteq>a \<and> \<bar>x + -a\<bar> < inverse (real (Suc n)) \<and> \<bar>X x + -L\<bar> \<ge> r"
   6.720 +            "\<exists>x. x\<noteq>a \<and> \<bar>x + -a\<bar> < inverse (real (Suc n)) \<and> norm (X x + -L) \<ge> r"
   6.721              by simp
   6.722            hence
   6.723 -            "(?F n)\<noteq>a \<and> \<bar>(?F n) + -a\<bar> < inverse (real (Suc n)) \<and> \<bar>X (?F n) + -L\<bar> \<ge> r"
   6.724 +            "(?F n)\<noteq>a \<and> \<bar>(?F n) + -a\<bar> < inverse (real (Suc n)) \<and> norm (X (?F n) + -L) \<ge> r"
   6.725              by (simp add: some_eq_ex [symmetric])
   6.726            thus ?thesis by simp
   6.727          qed
   6.728 @@ -2291,7 +2295,7 @@
   6.729      {
   6.730        fix n
   6.731        from rdef have
   6.732 -        "\<exists>x. x\<noteq>a \<and> \<bar>x + -a\<bar> < inverse (real (Suc n)) \<and> \<bar>X x + -L\<bar> \<ge> r"
   6.733 +        "\<exists>x. x\<noteq>a \<and> \<bar>x + -a\<bar> < inverse (real (Suc n)) \<and> norm (X x + -L) \<ge> r"
   6.734          by simp
   6.735        hence "?F n \<noteq> a" by (simp add: some_eq_ex [symmetric])
   6.736      }
   6.737 @@ -2307,15 +2311,15 @@
   6.738        obtain n where "n = no + 1" by simp
   6.739        then have nolen: "no \<le> n" by simp
   6.740          (* We prove this by showing that for any m there is an n\<ge>m such that |X (?F n) - L| \<ge> r *)
   6.741 -      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)" ..
   6.742 +      from rdef have "\<forall>s > 0. \<exists>x. (x \<noteq> a \<and> \<bar>x + -a\<bar> < s \<and> norm (X x + -L) \<ge> r)" ..
   6.743  
   6.744 -      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
   6.745 +      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
   6.746        
   6.747 -      hence "\<bar>X (?F n) + -L\<bar> \<ge> r" by (simp add: some_eq_ex [symmetric])
   6.748 -      with nolen have "\<exists>n. no \<le> n \<and> \<bar>X (?F n) + -L\<bar> \<ge> r" by auto
   6.749 +      hence "norm (X (?F n) + -L) \<ge> r" by (simp add: some_eq_ex [symmetric])
   6.750 +      with nolen have "\<exists>n. no \<le> n \<and> norm (X (?F n) + -L) \<ge> r" by auto
   6.751      }
   6.752 -    then have "(\<forall>no. \<exists>n. no \<le> n \<and> \<bar>X (?F n) + -L\<bar> \<ge> r)" by simp
   6.753 -    with rdef have "\<exists>e>0. (\<forall>no. \<exists>n. no \<le> n \<and> \<bar>X (?F n) + -L\<bar> \<ge> e)" by auto
   6.754 +    then have "(\<forall>no. \<exists>n. no \<le> n \<and> norm (X (?F n) + -L) \<ge> r)" by simp
   6.755 +    with rdef have "\<exists>e>0. (\<forall>no. \<exists>n. no \<le> n \<and> norm (X (?F n) + -L) \<ge> e)" by auto
   6.756      thus ?thesis by (unfold LIMSEQ_def, auto simp add: linorder_not_less)
   6.757    qed
   6.758    ultimately show False by simp
   6.759 @@ -2352,26 +2356,26 @@
   6.760  proof -
   6.761    have "f -- a --> L" .
   6.762    hence
   6.763 -    fd: "\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & \<bar>x + -a\<bar> < s --> \<bar>f x + -L\<bar> < r"
   6.764 +    fd: "\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & \<bar>x + -a\<bar> < s --> norm (f x + -L) < r"
   6.765      by (unfold LIM_def)
   6.766    {
   6.767      fix r::real
   6.768      assume rgz: "0 < r"
   6.769 -    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
   6.770 -    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
   6.771 -    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
   6.772 +    with fd have "\<exists>s > 0. \<forall>x. x\<noteq>a \<and> \<bar>x + -a\<bar> < s --> norm (f x + -L) < r" by simp
   6.773 +    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
   6.774 +    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
   6.775      {
   6.776        fix x::real
   6.777 -      from ax2 have nt: "(x+c)\<noteq>a \<and> \<bar>(x+c) + -a\<bar> < s \<longrightarrow> \<bar>f (x+c) + -L\<bar> < r" ..
   6.778 +      from ax2 have nt: "(x+c)\<noteq>a \<and> \<bar>(x+c) + -a\<bar> < s \<longrightarrow> norm (f (x+c) + -L) < r" ..
   6.779        moreover have "((x+c)\<noteq>a) = (x\<noteq>(a-c))" by auto
   6.780        moreover have "((x+c) + -a) = (x + -(a-c))" by simp
   6.781 -      ultimately have "x\<noteq>(a-c) \<and> \<bar>x + -(a-c)\<bar> < s \<longrightarrow> \<bar>f (x+c) + -L\<bar> < r" by simp
   6.782 +      ultimately have "x\<noteq>(a-c) \<and> \<bar>x + -(a-c)\<bar> < s \<longrightarrow> norm (f (x+c) + -L) < r" by simp
   6.783      }
   6.784 -    then have "\<forall>x. x\<noteq>(a-c) \<and> \<bar>x + -(a-c)\<bar> < s \<longrightarrow> \<bar>f (x+c) + -L\<bar> < r" ..
   6.785 -    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
   6.786 +    then have "\<forall>x. x\<noteq>(a-c) \<and> \<bar>x + -(a-c)\<bar> < s \<longrightarrow> norm (f (x+c) + -L) < r" ..
   6.787 +    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
   6.788    }
   6.789    then have
   6.790 -    "\<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
   6.791 +    "\<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
   6.792    thus ?thesis by (fold LIM_def)
   6.793  qed
   6.794  
     7.1 --- a/src/HOL/Hyperreal/NSA.thy	Sat Sep 16 02:35:58 2006 +0200
     7.2 +++ b/src/HOL/Hyperreal/NSA.thy	Sat Sep 16 02:40:00 2006 +0200
     7.3 @@ -25,7 +25,8 @@
     7.4    HInfinite :: "('a::real_normed_vector) star set"
     7.5    "HInfinite = {x. \<forall>r \<in> Reals. r < hnorm x}"
     7.6  
     7.7 -  approx :: "[hypreal, hypreal] => bool"    (infixl "@=" 50)
     7.8 +  approx :: "['a::real_normed_vector star, 'a star] => bool"
     7.9 +    (infixl "@=" 50)
    7.10      --{*the `infinitely close' relation*}
    7.11    "(x @= y) = ((x + -y) \<in> Infinitesimal)"
    7.12  
    7.13 @@ -33,10 +34,10 @@
    7.14      --{*the standard part of a hyperreal*}
    7.15    "st = (%x. @r. x \<in> HFinite & r \<in> Reals & r @= x)"
    7.16  
    7.17 -  monad     :: "hypreal => hypreal set"
    7.18 +  monad     :: "'a::real_normed_vector star => 'a star set"
    7.19    "monad x = {y. x @= y}"
    7.20  
    7.21 -  galaxy    :: "hypreal => hypreal set"
    7.22 +  galaxy    :: "'a::real_normed_vector star => 'a star set"
    7.23    "galaxy x = {y. (x + -y) \<in> HFinite}"
    7.24  
    7.25  const_syntax (xsymbols)
    7.26 @@ -609,7 +610,7 @@
    7.27  lemma approx_refl [iff]: "x @= x"
    7.28  by (simp add: approx_def Infinitesimal_def)
    7.29  
    7.30 -lemma hypreal_minus_distrib1: "-(y + -(x::hypreal)) = x + -y"
    7.31 +lemma hypreal_minus_distrib1: "-(y + -(x::'a::ab_group_add)) = x + -y"
    7.32  by (simp add: add_commute)
    7.33  
    7.34  lemma approx_sym: "x @= y ==> y @= x"
    7.35 @@ -689,7 +690,7 @@
    7.36  lemma approx_add: "[| a @= b; c @= d |] ==> a+c @= b+d"
    7.37  proof (unfold approx_def)
    7.38    assume inf: "a + - b \<in> Infinitesimal" "c + - d \<in> Infinitesimal"
    7.39 -  have "a + c + - (b + d) = (a + - b) + (c + - d)" by arith
    7.40 +  have "a + c + - (b + d) = (a + - b) + (c + - d)" by simp
    7.41    also have "... \<in> Infinitesimal" using inf by (rule Infinitesimal_add)
    7.42    finally show "a + c + - (b + d) \<in> Infinitesimal" .
    7.43  qed
    7.44 @@ -709,23 +710,38 @@
    7.45  lemma approx_add_minus: "[| a @= b; c @= d |] ==> a + -c @= b + -d"
    7.46  by (blast intro!: approx_add approx_minus)
    7.47  
    7.48 -lemma approx_mult1: "[| a @= b; c: HFinite|] ==> a*c @= b*c"
    7.49 +lemma approx_mult1:
    7.50 +  fixes a b c :: "'a::real_normed_algebra star"
    7.51 +  shows "[| a @= b; c: HFinite|] ==> a*c @= b*c"
    7.52  by (simp add: approx_def Infinitesimal_HFinite_mult minus_mult_left 
    7.53                left_distrib [symmetric] 
    7.54           del: minus_mult_left [symmetric])
    7.55  
    7.56 -lemma approx_mult2: "[|a @= b; c: HFinite|] ==> c*a @= c*b"
    7.57 -by (simp add: approx_mult1 mult_commute)
    7.58 +lemma approx_mult2:
    7.59 +  fixes a b c :: "'a::real_normed_algebra star"
    7.60 +  shows "[|a @= b; c: HFinite|] ==> c*a @= c*b"
    7.61 +by (simp add: approx_def Infinitesimal_HFinite_mult2 minus_mult_right 
    7.62 +              right_distrib [symmetric] 
    7.63 +         del: minus_mult_right [symmetric])
    7.64  
    7.65 -lemma approx_mult_subst: "[|u @= v*x; x @= y; v \<in> HFinite|] ==> u @= v*y"
    7.66 +lemma approx_mult_subst:
    7.67 +  fixes u v x y :: "'a::real_normed_algebra star"
    7.68 +  shows "[|u @= v*x; x @= y; v \<in> HFinite|] ==> u @= v*y"
    7.69  by (blast intro: approx_mult2 approx_trans)
    7.70  
    7.71 -lemma approx_mult_subst2: "[| u @= x*v; x @= y; v \<in> HFinite |] ==> u @= y*v"
    7.72 +lemma approx_mult_subst2:
    7.73 +  fixes u v x y :: "'a::real_normed_algebra star"
    7.74 +  shows "[| u @= x*v; x @= y; v \<in> HFinite |] ==> u @= y*v"
    7.75  by (blast intro: approx_mult1 approx_trans)
    7.76  
    7.77 +lemma approx_mult_subst_star_of:
    7.78 +  fixes u x y :: "'a::real_normed_algebra star"
    7.79 +  shows "[| u @= x*star_of v; x @= y |] ==> u @= y*star_of v"
    7.80 +by (auto intro: approx_mult_subst2)
    7.81 +
    7.82  lemma approx_mult_subst_SReal:
    7.83       "[| u @= x*hypreal_of_real v; x @= y |] ==> u @= y*hypreal_of_real v"
    7.84 -by (auto intro: approx_mult_subst2)
    7.85 +by (rule approx_mult_subst_star_of)
    7.86  
    7.87  lemma approx_eq_imp: "a = b ==> a @= b"
    7.88  by (simp add: approx_def)
    7.89 @@ -802,51 +818,60 @@
    7.90  apply (auto simp add: add_assoc)
    7.91  done
    7.92  
    7.93 -lemma approx_hypreal_of_real_HFinite: "x @= hypreal_of_real D ==> x \<in> HFinite"
    7.94 +lemma approx_star_of_HFinite: "x @= star_of D ==> x \<in> HFinite"
    7.95  by (rule approx_sym [THEN [2] approx_HFinite], auto)
    7.96  
    7.97 +lemma approx_hypreal_of_real_HFinite: "x @= hypreal_of_real D ==> x \<in> HFinite"
    7.98 +by (rule approx_star_of_HFinite)
    7.99 +
   7.100  lemma approx_mult_HFinite:
   7.101 -     "[|a @= b; c @= d; b: HFinite; d: HFinite|] ==> a*c @= b*d"
   7.102 +  fixes a b c d :: "'a::real_normed_algebra star"
   7.103 +  shows "[|a @= b; c @= d; b: HFinite; d: HFinite|] ==> a*c @= b*d"
   7.104  apply (rule approx_trans)
   7.105  apply (rule_tac [2] approx_mult2)
   7.106  apply (rule approx_mult1)
   7.107  prefer 2 apply (blast intro: approx_HFinite approx_sym, auto)
   7.108  done
   7.109  
   7.110 +lemma approx_mult_star_of:
   7.111 +  fixes a c :: "'a::real_normed_algebra star"
   7.112 +  shows "[|a @= star_of b; c @= star_of d |]
   7.113 +      ==> a*c @= star_of b*star_of d"
   7.114 +by (blast intro!: approx_mult_HFinite approx_star_of_HFinite HFinite_star_of)
   7.115 +
   7.116  lemma approx_mult_hypreal_of_real:
   7.117       "[|a @= hypreal_of_real b; c @= hypreal_of_real d |]
   7.118        ==> a*c @= hypreal_of_real b*hypreal_of_real d"
   7.119 -by (blast intro!: approx_mult_HFinite approx_hypreal_of_real_HFinite 
   7.120 -                  HFinite_hypreal_of_real)
   7.121 +by (rule approx_mult_star_of)
   7.122  
   7.123  lemma approx_SReal_mult_cancel_zero:
   7.124 -     "[| a \<in> Reals; a \<noteq> 0; a*x @= 0 |] ==> x @= 0"
   7.125 +     "[| (a::hypreal) \<in> Reals; a \<noteq> 0; a*x @= 0 |] ==> x @= 0"
   7.126  apply (drule SReal_inverse [THEN SReal_subset_HFinite [THEN subsetD]])
   7.127  apply (auto dest: approx_mult2 simp add: mult_assoc [symmetric])
   7.128  done
   7.129  
   7.130 -lemma approx_mult_SReal1: "[| a \<in> Reals; x @= 0 |] ==> x*a @= 0"
   7.131 +lemma approx_mult_SReal1: "[| (a::hypreal) \<in> Reals; x @= 0 |] ==> x*a @= 0"
   7.132  by (auto dest: SReal_subset_HFinite [THEN subsetD] approx_mult1)
   7.133  
   7.134 -lemma approx_mult_SReal2: "[| a \<in> Reals; x @= 0 |] ==> a*x @= 0"
   7.135 +lemma approx_mult_SReal2: "[| (a::hypreal) \<in> Reals; x @= 0 |] ==> a*x @= 0"
   7.136  by (auto dest: SReal_subset_HFinite [THEN subsetD] approx_mult2)
   7.137  
   7.138  lemma approx_mult_SReal_zero_cancel_iff [simp]:
   7.139 -     "[|a \<in> Reals; a \<noteq> 0 |] ==> (a*x @= 0) = (x @= 0)"
   7.140 +     "[|(a::hypreal) \<in> Reals; a \<noteq> 0 |] ==> (a*x @= 0) = (x @= 0)"
   7.141  by (blast intro: approx_SReal_mult_cancel_zero approx_mult_SReal2)
   7.142  
   7.143  lemma approx_SReal_mult_cancel:
   7.144 -     "[| a \<in> Reals; a \<noteq> 0; a* w @= a*z |] ==> w @= z"
   7.145 +     "[| (a::hypreal) \<in> Reals; a \<noteq> 0; a* w @= a*z |] ==> w @= z"
   7.146  apply (drule SReal_inverse [THEN SReal_subset_HFinite [THEN subsetD]])
   7.147  apply (auto dest: approx_mult2 simp add: mult_assoc [symmetric])
   7.148  done
   7.149  
   7.150  lemma approx_SReal_mult_cancel_iff1 [simp]:
   7.151 -     "[| a \<in> Reals; a \<noteq> 0|] ==> (a* w @= a*z) = (w @= z)"
   7.152 +     "[| (a::hypreal) \<in> Reals; a \<noteq> 0|] ==> (a* w @= a*z) = (w @= z)"
   7.153  by (auto intro!: approx_mult2 SReal_subset_HFinite [THEN subsetD]
   7.154           intro: approx_SReal_mult_cancel)
   7.155  
   7.156 -lemma approx_le_bound: "[| z \<le> f; f @= g; g \<le> z |] ==> f @= z"
   7.157 +lemma approx_le_bound: "[| (z::hypreal) \<le> f; f @= g; g \<le> z |] ==> f @= z"
   7.158  apply (simp add: bex_Infinitesimal_iff2 [symmetric], auto)
   7.159  apply (rule_tac x = "g+y-z" in bexI)
   7.160  apply (simp (no_asm))
   7.161 @@ -905,6 +930,10 @@
   7.162  apply simp
   7.163  done
   7.164  
   7.165 +lemma star_of_HFinite_diff_Infinitesimal:
   7.166 +     "x \<noteq> 0 ==> star_of x \<in> HFinite - Infinitesimal"
   7.167 +by simp
   7.168 +
   7.169  lemma hypreal_of_real_Infinitesimal_iff_0:
   7.170       "(hypreal_of_real x \<in> Infinitesimal) = (x=0)"
   7.171  by (rule star_of_Infinitesimal_iff_0)
   7.172 @@ -920,7 +949,8 @@
   7.173  apply simp
   7.174  done
   7.175  
   7.176 -lemma approx_SReal_not_zero: "[| y \<in> Reals; x @= y; y\<noteq> 0 |] ==> x \<noteq> 0"
   7.177 +lemma approx_SReal_not_zero:
   7.178 +  "[| (y::hypreal) \<in> Reals; x @= y; y\<noteq> 0 |] ==> x \<noteq> 0"
   7.179  apply (cut_tac x = 0 and y = y in linorder_less_linear, simp)
   7.180  apply (blast dest: approx_sym [THEN mem_infmal_iff [THEN iffD2]] SReal_not_Infinitesimal SReal_minus_not_Infinitesimal)
   7.181  done
   7.182 @@ -958,7 +988,16 @@
   7.183  
   7.184  subsection{* Uniqueness: Two Infinitely Close Reals are Equal*}
   7.185  
   7.186 -lemma SReal_approx_iff: "[|x \<in> Reals; y \<in> Reals|] ==> (x @= y) = (x = y)"
   7.187 +lemma star_of_approx_iff [simp]: "(star_of x @= star_of y) = (x = y)"
   7.188 +apply safe
   7.189 +apply (simp add: approx_def)
   7.190 +apply (simp only: star_of_minus [symmetric] star_of_add [symmetric])
   7.191 +apply (simp only: star_of_Infinitesimal_iff_0)
   7.192 +apply (simp only: diff_minus [symmetric] right_minus_eq)
   7.193 +done
   7.194 +
   7.195 +lemma SReal_approx_iff:
   7.196 +  "[|(x::hypreal) \<in> Reals; y \<in> Reals|] ==> (x @= y) = (x = y)"
   7.197  apply auto
   7.198  apply (simp add: approx_def)
   7.199  apply (drule_tac x = y in SReal_minus)
   7.200 @@ -969,23 +1008,31 @@
   7.201  done
   7.202  
   7.203  lemma number_of_approx_iff [simp]:
   7.204 -     "(number_of v @= number_of w) = (number_of v = (number_of w :: hypreal))"
   7.205 -by (auto simp add: SReal_approx_iff)
   7.206 +     "(number_of v @= (number_of w :: 'a::{number,real_normed_vector} star)) =
   7.207 +      (number_of v = (number_of w :: 'a))"
   7.208 +apply (unfold star_number_def)
   7.209 +apply (rule star_of_approx_iff)
   7.210 +done
   7.211  
   7.212  (*And also for 0 @= #nn and 1 @= #nn, #nn @= 0 and #nn @= 1.*)
   7.213 -lemma [simp]: "(0 @= number_of w) = ((number_of w :: hypreal) = 0)"
   7.214 -              "(number_of w @= 0) = ((number_of w :: hypreal) = 0)"
   7.215 -              "(1 @= number_of w) = ((number_of w :: hypreal) = 1)"
   7.216 -              "(number_of w @= 1) = ((number_of w :: hypreal) = 1)"
   7.217 -              "~ (0 @= 1)" "~ (1 @= 0)"
   7.218 -by (auto simp only: SReal_number_of SReal_approx_iff Reals_0 Reals_1)
   7.219 +lemma [simp]:
   7.220 +  "(number_of w @= (0::'a::{number,real_normed_vector} star)) =
   7.221 +   (number_of w = (0::'a))"
   7.222 +  "((0::'a::{number,real_normed_vector} star) @= number_of w) =
   7.223 +   (number_of w = (0::'a))"
   7.224 +  "(number_of w @= (1::'b::{number,one,real_normed_vector} star)) =
   7.225 +   (number_of w = (1::'b))"
   7.226 +  "((1::'b::{number,one,real_normed_vector} star) @= number_of w) =
   7.227 +   (number_of w = (1::'b))"
   7.228 +  "~ (0 @= (1::'c::{axclass_0_neq_1,real_normed_vector} star))"
   7.229 +  "~ (1 @= (0::'c::{axclass_0_neq_1,real_normed_vector} star))"
   7.230 +apply (unfold star_number_def star_zero_def star_one_def)
   7.231 +apply (unfold star_of_approx_iff)
   7.232 +by (auto intro: sym)
   7.233  
   7.234 -lemma hypreal_of_real_approx_iff [simp]:
   7.235 +lemma hypreal_of_real_approx_iff:
   7.236       "(hypreal_of_real k @= hypreal_of_real m) = (k = m)"
   7.237 -apply auto
   7.238 -apply (rule inj_hypreal_of_real [THEN injD])
   7.239 -apply (rule SReal_approx_iff [THEN iffD1], auto)
   7.240 -done
   7.241 +by (rule star_of_approx_iff)
   7.242  
   7.243  lemma hypreal_of_real_approx_number_of_iff [simp]:
   7.244       "(hypreal_of_real k @= number_of w) = (k = number_of w)"
   7.245 @@ -998,7 +1045,7 @@
   7.246    by (simp_all add:  hypreal_of_real_approx_iff [symmetric])
   7.247  
   7.248  lemma approx_unique_real:
   7.249 -     "[| r \<in> Reals; s \<in> Reals; r @= x; s @= x|] ==> r = s"
   7.250 +     "[| (r::hypreal) \<in> Reals; s \<in> Reals; r @= x; s @= x|] ==> r = s"
   7.251  by (blast intro: SReal_approx_iff [THEN iffD1] approx_trans2)
   7.252  
   7.253  
   7.254 @@ -1171,13 +1218,13 @@
   7.255  done
   7.256  
   7.257  lemma st_part_Ex:
   7.258 -     "x \<in> HFinite ==> \<exists>t \<in> Reals. x @= t"
   7.259 +     "(x::hypreal) \<in> HFinite ==> \<exists>t \<in> Reals. x @= t"
   7.260  apply (simp add: approx_def Infinitesimal_def)
   7.261  apply (drule lemma_st_part_Ex, auto)
   7.262  done
   7.263  
   7.264  text{*There is a unique real infinitely close*}
   7.265 -lemma st_part_Ex1: "x \<in> HFinite ==> EX! t. t \<in> Reals & x @= t"
   7.266 +lemma st_part_Ex1: "x \<in> HFinite ==> EX! t::hypreal. t \<in> Reals & x @= t"
   7.267  apply (drule st_part_Ex, safe)
   7.268  apply (drule_tac [2] approx_sym, drule_tac [2] approx_sym, drule_tac [2] approx_sym)
   7.269  apply (auto intro!: approx_unique_real)
   7.270 @@ -1247,6 +1294,8 @@
   7.271  done
   7.272  
   7.273  lemma approx_inverse:
   7.274 +  fixes x y :: "'a::{real_normed_div_algebra,division_by_zero} star"
   7.275 +  shows
   7.276       "[| x @= y; y \<in>  HFinite - Infinitesimal |]
   7.277        ==> inverse x @= inverse y"
   7.278  apply (frule HFinite_diff_Infinitesimal_approx, assumption)
   7.279 @@ -1259,15 +1308,20 @@
   7.280  done
   7.281  
   7.282  (*Used for NSLIM_inverse, NSLIMSEQ_inverse*)
   7.283 +lemmas star_of_approx_inverse = star_of_HFinite_diff_Infinitesimal [THEN [2] approx_inverse]
   7.284  lemmas hypreal_of_real_approx_inverse =  hypreal_of_real_HFinite_diff_Infinitesimal [THEN [2] approx_inverse]
   7.285  
   7.286  lemma inverse_add_Infinitesimal_approx:
   7.287 +  fixes x h :: "'a::{real_normed_div_algebra,division_by_zero} star"
   7.288 +  shows
   7.289       "[| x \<in> HFinite - Infinitesimal;
   7.290           h \<in> Infinitesimal |] ==> inverse(x + h) @= inverse x"
   7.291  apply (auto intro: approx_inverse approx_sym Infinitesimal_add_approx_self)
   7.292  done
   7.293  
   7.294  lemma inverse_add_Infinitesimal_approx2:
   7.295 +  fixes x h :: "'a::{real_normed_div_algebra,division_by_zero} star"
   7.296 +  shows
   7.297       "[| x \<in> HFinite - Infinitesimal;
   7.298           h \<in> Infinitesimal |] ==> inverse(h + x) @= inverse x"
   7.299  apply (rule add_commute [THEN subst])
   7.300 @@ -1275,6 +1329,8 @@
   7.301  done
   7.302  
   7.303  lemma inverse_add_Infinitesimal_approx_Infinitesimal:
   7.304 +  fixes x h :: "'a::{real_normed_div_algebra,division_by_zero} star"
   7.305 +  shows
   7.306       "[| x \<in> HFinite - Infinitesimal;
   7.307           h \<in> Infinitesimal |] ==> inverse(x + h) + -inverse x @= h"
   7.308  apply (rule approx_trans2)
   7.309 @@ -1305,7 +1361,8 @@
   7.310  by (auto simp add: HInfinite_HFinite_iff)
   7.311  
   7.312  lemma approx_HFinite_mult_cancel:
   7.313 -     "[| a: HFinite-Infinitesimal; a* w @= a*z |] ==> w @= z"
   7.314 +  fixes a w z :: "'a::{real_normed_div_algebra,division_by_zero} star"
   7.315 +  shows "[| a: HFinite-Infinitesimal; a* w @= a*z |] ==> w @= z"
   7.316  apply safe
   7.317  apply (frule HFinite_inverse, assumption)
   7.318  apply (drule not_Infinitesimal_not_zero)
   7.319 @@ -1313,7 +1370,8 @@
   7.320  done
   7.321  
   7.322  lemma approx_HFinite_mult_cancel_iff1:
   7.323 -     "a: HFinite-Infinitesimal ==> (a * w @= a * z) = (w @= z)"
   7.324 +  fixes a w z :: "'a::{real_normed_div_algebra,division_by_zero} star"
   7.325 +  shows "a: HFinite-Infinitesimal ==> (a * w @= a * z) = (w @= z)"
   7.326  by (auto intro: approx_mult2 approx_HFinite_mult_cancel)
   7.327  
   7.328  lemma HInfinite_HFinite_add_cancel:
   7.329 @@ -1376,13 +1434,13 @@
   7.330  apply (simp (no_asm) add: HInfinite_HFinite_iff)
   7.331  done
   7.332  
   7.333 -lemma approx_hrabs_disj: "abs x @= x | abs x @= -x"
   7.334 +lemma approx_hrabs_disj: "abs (x::hypreal) @= x | abs x @= -x"
   7.335  by (cut_tac x = x in hrabs_disj, auto)
   7.336  
   7.337  
   7.338  subsection{*Theorems about Monads*}
   7.339  
   7.340 -lemma monad_hrabs_Un_subset: "monad (abs x) \<le> monad(x) Un monad(-x)"
   7.341 +lemma monad_hrabs_Un_subset: "monad (abs x) \<le> monad(x::hypreal) Un monad(-x)"
   7.342  by (rule_tac x1 = x in hrabs_disj [THEN disjE], auto)
   7.343  
   7.344  lemma Infinitesimal_monad_eq: "e \<in> Infinitesimal ==> monad (x+e) = monad x"
   7.345 @@ -1398,7 +1456,7 @@
   7.346  apply (simp (no_asm) add: Infinitesimal_monad_zero_iff [symmetric])
   7.347  done
   7.348  
   7.349 -lemma monad_zero_hrabs_iff: "(x \<in> monad 0) = (abs x \<in> monad 0)"
   7.350 +lemma monad_zero_hrabs_iff: "((x::hypreal) \<in> monad 0) = (abs x \<in> monad 0)"
   7.351  apply (rule_tac x1 = x in hrabs_disj [THEN disjE])
   7.352  apply (auto simp add: monad_zero_minus_iff [symmetric])
   7.353  done
   7.354 @@ -1436,7 +1494,7 @@
   7.355  done
   7.356  
   7.357  lemma Infinitesimal_approx_hrabs:
   7.358 -     "[| x @= y; x \<in> Infinitesimal |] ==> abs x @= abs y"
   7.359 +     "[| x @= y; (x::hypreal) \<in> Infinitesimal |] ==> abs x @= abs y"
   7.360  apply (drule Infinitesimal_monad_zero_iff [THEN iffD1])
   7.361  apply (blast intro: approx_mem_monad_zero monad_zero_hrabs_iff [THEN iffD1] mem_monad_approx approx_trans3)
   7.362  done
   7.363 @@ -1449,28 +1507,28 @@
   7.364  done
   7.365  
   7.366  lemma Ball_mem_monad_gt_zero:
   7.367 -     "[| 0 < x;  x \<notin> Infinitesimal; u \<in> monad x |] ==> 0 < u"
   7.368 +     "[| 0 < (x::hypreal);  x \<notin> Infinitesimal; u \<in> monad x |] ==> 0 < u"
   7.369  apply (drule mem_monad_approx [THEN approx_sym])
   7.370  apply (erule bex_Infinitesimal_iff2 [THEN iffD2, THEN bexE])
   7.371  apply (drule_tac e = "-xa" in less_Infinitesimal_less, auto)
   7.372  done
   7.373  
   7.374  lemma Ball_mem_monad_less_zero:
   7.375 -     "[| x < 0; x \<notin> Infinitesimal; u \<in> monad x |] ==> u < 0"
   7.376 +     "[| (x::hypreal) < 0; x \<notin> Infinitesimal; u \<in> monad x |] ==> u < 0"
   7.377  apply (drule mem_monad_approx [THEN approx_sym])
   7.378  apply (erule bex_Infinitesimal_iff [THEN iffD2, THEN bexE])
   7.379  apply (cut_tac x = "-x" and e = xa in less_Infinitesimal_less, auto)
   7.380  done
   7.381  
   7.382  lemma lemma_approx_gt_zero:
   7.383 -     "[|0 < x; x \<notin> Infinitesimal; x @= y|] ==> 0 < y"
   7.384 +     "[|0 < (x::hypreal); x \<notin> Infinitesimal; x @= y|] ==> 0 < y"
   7.385  by (blast dest: Ball_mem_monad_gt_zero approx_subset_monad)
   7.386  
   7.387  lemma lemma_approx_less_zero:
   7.388 -     "[|x < 0; x \<notin> Infinitesimal; x @= y|] ==> y < 0"
   7.389 +     "[|(x::hypreal) < 0; x \<notin> Infinitesimal; x @= y|] ==> y < 0"
   7.390  by (blast dest: Ball_mem_monad_less_zero approx_subset_monad)
   7.391  
   7.392 -theorem approx_hrabs: "x @= y ==> abs x @= abs y"
   7.393 +theorem approx_hrabs: "(x::hypreal) @= y ==> abs x @= abs y"
   7.394  apply (case_tac "x \<in> Infinitesimal") 
   7.395  apply (simp add: Infinitesimal_approx_hrabs)
   7.396  apply (rule linorder_cases [of 0 x])  
   7.397 @@ -1478,20 +1536,21 @@
   7.398  apply (auto simp add: lemma_approx_less_zero [of x y] abs_of_neg)
   7.399  done
   7.400  
   7.401 -lemma approx_hrabs_zero_cancel: "abs(x) @= 0 ==> x @= 0"
   7.402 +lemma approx_hrabs_zero_cancel: "abs(x::hypreal) @= 0 ==> x @= 0"
   7.403  apply (cut_tac x = x in hrabs_disj)
   7.404  apply (auto dest: approx_minus)
   7.405  done
   7.406  
   7.407 -lemma approx_hrabs_add_Infinitesimal: "e \<in> Infinitesimal ==> abs x @= abs(x+e)"
   7.408 +lemma approx_hrabs_add_Infinitesimal:
   7.409 +  "(e::hypreal) \<in> Infinitesimal ==> abs x @= abs(x+e)"
   7.410  by (fast intro: approx_hrabs Infinitesimal_add_approx_self)
   7.411  
   7.412  lemma approx_hrabs_add_minus_Infinitesimal:
   7.413 -     "e \<in> Infinitesimal ==> abs x @= abs(x + -e)"
   7.414 +     "(e::hypreal) \<in> Infinitesimal ==> abs x @= abs(x + -e)"
   7.415  by (fast intro: approx_hrabs Infinitesimal_add_minus_approx_self)
   7.416  
   7.417  lemma hrabs_add_Infinitesimal_cancel:
   7.418 -     "[| e \<in> Infinitesimal; e' \<in> Infinitesimal;
   7.419 +     "[| (e::hypreal) \<in> Infinitesimal; e' \<in> Infinitesimal;
   7.420           abs(x+e) = abs(y+e')|] ==> abs x @= abs y"
   7.421  apply (drule_tac x = x in approx_hrabs_add_Infinitesimal)
   7.422  apply (drule_tac x = y in approx_hrabs_add_Infinitesimal)
   7.423 @@ -1499,7 +1558,7 @@
   7.424  done
   7.425  
   7.426  lemma hrabs_add_minus_Infinitesimal_cancel:
   7.427 -     "[| e \<in> Infinitesimal; e' \<in> Infinitesimal;
   7.428 +     "[| (e::hypreal) \<in> Infinitesimal; e' \<in> Infinitesimal;
   7.429           abs(x + -e) = abs(y + -e')|] ==> abs x @= abs y"
   7.430  apply (drule_tac x = x in approx_hrabs_add_minus_Infinitesimal)
   7.431  apply (drule_tac x = y in approx_hrabs_add_minus_Infinitesimal)
   7.432 @@ -1857,55 +1916,45 @@
   7.433  
   7.434  subsection{*Alternative Definitions for @{term HFinite} using Free Ultrafilter*}
   7.435  
   7.436 -lemma FreeUltrafilterNat_Rep_hypreal:
   7.437 -     "[| X \<in> Rep_star x; Y \<in> Rep_star x |]
   7.438 -      ==> {n. X n = Y n} \<in> FreeUltrafilterNat"
   7.439 -by (cases x, unfold star_n_def, auto, ultra)
   7.440 -
   7.441  lemma HFinite_FreeUltrafilterNat:
   7.442 -    "(x::hypreal) \<in> HFinite 
   7.443 -     ==> \<exists>X \<in> Rep_star x. \<exists>u. {n. abs (X n) < u} \<in> FreeUltrafilterNat"
   7.444 -apply (cases x)
   7.445 -apply (auto simp add: HFinite_def abs_less_iff minus_less_iff [of x] 
   7.446 -              star_of_def
   7.447 -              star_n_less SReal_iff star_n_minus)
   7.448 -apply (rule_tac x=X in bexI)
   7.449 -apply (rule_tac x=y in exI, ultra)
   7.450 -apply simp
   7.451 +    "star_n X \<in> HFinite 
   7.452 +     ==> \<exists>u. {n. norm (X n) < u} \<in> FreeUltrafilterNat"
   7.453 +apply (auto simp add: HFinite_def SReal_def)
   7.454 +apply (rule_tac x=r in exI)
   7.455 +apply (simp add: hnorm_def star_of_def starfun_star_n)
   7.456 +apply (simp add: star_less_def starP2_star_n)
   7.457  done
   7.458  
   7.459  lemma FreeUltrafilterNat_HFinite:
   7.460 -     "\<exists>X \<in> Rep_star x.
   7.461 -       \<exists>u. {n. abs (X n) < u} \<in> FreeUltrafilterNat
   7.462 -       ==>  (x::hypreal) \<in> HFinite"
   7.463 -apply (cases x)
   7.464 -apply (auto simp add: HFinite_def abs_less_iff minus_less_iff [of x])
   7.465 -apply (rule_tac x = "hypreal_of_real u" in bexI)
   7.466 -apply (auto simp add: star_n_less SReal_iff star_n_minus star_of_def)
   7.467 -apply ultra+
   7.468 +     "\<exists>u. {n. norm (X n) < u} \<in> FreeUltrafilterNat
   7.469 +       ==>  star_n X \<in> HFinite"
   7.470 +apply (auto simp add: HFinite_def mem_Rep_star_iff)
   7.471 +apply (rule_tac x="star_of u" in bexI)
   7.472 +apply (simp add: hnorm_def starfun_star_n star_of_def)
   7.473 +apply (simp add: star_less_def starP2_star_n)
   7.474 +apply (simp add: SReal_def)
   7.475  done
   7.476  
   7.477  lemma HFinite_FreeUltrafilterNat_iff:
   7.478 -     "((x::hypreal) \<in> HFinite) = (\<exists>X \<in> Rep_star x.
   7.479 -           \<exists>u. {n. abs (X n) < u} \<in> FreeUltrafilterNat)"
   7.480 +     "(star_n X \<in> HFinite) = (\<exists>u. {n. norm (X n) < u} \<in> FreeUltrafilterNat)"
   7.481  by (blast intro!: HFinite_FreeUltrafilterNat FreeUltrafilterNat_HFinite)
   7.482  
   7.483  
   7.484  subsection{*Alternative Definitions for @{term HInfinite} using Free Ultrafilter*}
   7.485  
   7.486 -lemma lemma_Compl_eq: "- {n. (u::real) < abs (xa n)} = {n. abs (xa n) \<le> u}"
   7.487 +lemma lemma_Compl_eq: "- {n. u < norm (xa n)} = {n. norm (xa n) \<le> u}"
   7.488  by auto
   7.489  
   7.490 -lemma lemma_Compl_eq2: "- {n. abs (xa n) < (u::real)} = {n. u \<le> abs (xa n)}"
   7.491 +lemma lemma_Compl_eq2: "- {n. norm (xa n) < u} = {n. u \<le> norm (xa n)}"
   7.492  by auto
   7.493  
   7.494  lemma lemma_Int_eq1:
   7.495 -     "{n. abs (xa n) \<le> (u::real)} Int {n. u \<le> abs (xa n)}
   7.496 -          = {n. abs(xa n) = u}"
   7.497 +     "{n. norm (xa n) \<le> u} Int {n. u \<le> norm (xa n)}
   7.498 +          = {n. norm(xa n) = u}"
   7.499  by auto
   7.500  
   7.501  lemma lemma_FreeUltrafilterNat_one:
   7.502 -     "{n. abs (xa n) = u} \<le> {n. abs (xa n) < u + (1::real)}"
   7.503 +     "{n. norm (xa n) = u} \<le> {n. norm (xa n) < u + (1::real)}"
   7.504  by auto
   7.505  
   7.506  (*-------------------------------------
   7.507 @@ -1913,87 +1962,63 @@
   7.508    ultrafilter for Infinite numbers!
   7.509   -------------------------------------*)
   7.510  lemma FreeUltrafilterNat_const_Finite:
   7.511 -     "[| xa: Rep_star x;
   7.512 -                  {n. abs (xa n) = u} \<in> FreeUltrafilterNat
   7.513 -               |] ==> (x::hypreal) \<in> HFinite"
   7.514 +     "{n. norm (X n) = u} \<in> FreeUltrafilterNat ==> star_n X \<in> HFinite"
   7.515  apply (rule FreeUltrafilterNat_HFinite)
   7.516 -apply (rule_tac x = xa in bexI)
   7.517  apply (rule_tac x = "u + 1" in exI)
   7.518 -apply (ultra, assumption)
   7.519 +apply (erule ultra, simp)
   7.520  done
   7.521  
   7.522  lemma HInfinite_FreeUltrafilterNat:
   7.523 -     "(x::hypreal) \<in> HInfinite ==> \<exists>X \<in> Rep_star x.
   7.524 -           \<forall>u. {n. u < abs (X n)} \<in> FreeUltrafilterNat"
   7.525 -apply (frule HInfinite_HFinite_iff [THEN iffD1])
   7.526 -apply (cut_tac x = x in Rep_hypreal_nonempty)
   7.527 -apply (auto simp del: Rep_hypreal_nonempty simp add: HFinite_FreeUltrafilterNat_iff Bex_def)
   7.528 -apply (drule spec)+
   7.529 -apply auto
   7.530 -apply (drule_tac x = u in spec)
   7.531 -apply (drule FreeUltrafilterNat_Compl_mem)+
   7.532 -apply (drule FreeUltrafilterNat_Int, assumption)
   7.533 -apply (simp add: lemma_Compl_eq lemma_Compl_eq2 lemma_Int_eq1)
   7.534 -apply (auto dest: FreeUltrafilterNat_const_Finite simp
   7.535 -      add: HInfinite_HFinite_iff [THEN iffD1])
   7.536 +     "star_n X \<in> HInfinite ==> \<forall>u. {n. u < norm (X n)} \<in> FreeUltrafilterNat"
   7.537 +apply (drule HInfinite_HFinite_iff [THEN iffD1])
   7.538 +apply (simp add: HFinite_FreeUltrafilterNat_iff)
   7.539 +apply (rule allI, drule_tac x="u + 1" in spec)
   7.540 +apply (drule FreeUltrafilterNat_Compl_mem)
   7.541 +apply (simp add: Collect_neg_eq [symmetric] linorder_not_less)
   7.542 +apply (erule ultra, simp)
   7.543  done
   7.544  
   7.545  lemma lemma_Int_HI:
   7.546 -     "{n. abs (Xa n) < u} Int {n. X n = Xa n} \<subseteq> {n. abs (X n) < (u::real)}"
   7.547 +     "{n. norm (Xa n) < u} Int {n. X n = Xa n} \<subseteq> {n. norm (X n) < (u::real)}"
   7.548  by auto
   7.549  
   7.550 -lemma lemma_Int_HIa: "{n. u < abs (X n)} Int {n. abs (X n) < (u::real)} = {}"
   7.551 +lemma lemma_Int_HIa: "{n. u < norm (X n)} Int {n. norm (X n) < u} = {}"
   7.552  by (auto intro: order_less_asym)
   7.553  
   7.554  lemma FreeUltrafilterNat_HInfinite:
   7.555 -     "\<exists>X \<in> Rep_star x. \<forall>u.
   7.556 -               {n. u < abs (X n)} \<in> FreeUltrafilterNat
   7.557 -               ==>  (x::hypreal) \<in> HInfinite"
   7.558 +     "\<forall>u. {n. u < norm (X n)} \<in> FreeUltrafilterNat ==> star_n X \<in> HInfinite"
   7.559  apply (rule HInfinite_HFinite_iff [THEN iffD2])
   7.560 -apply (safe, drule HFinite_FreeUltrafilterNat, auto)
   7.561 +apply (safe, drule HFinite_FreeUltrafilterNat, safe)
   7.562  apply (drule_tac x = u in spec)
   7.563 -apply (drule FreeUltrafilterNat_Rep_hypreal, assumption)
   7.564 -apply (drule_tac Y = "{n. X n = Xa n}" in FreeUltrafilterNat_Int, simp) 
   7.565 -apply (drule lemma_Int_HI [THEN [2] FreeUltrafilterNat_subset])
   7.566 -apply (drule_tac Y = "{n. abs (X n) < u}" in FreeUltrafilterNat_Int)
   7.567 -apply (auto simp add: lemma_Int_HIa)
   7.568 +apply ultra
   7.569  done
   7.570  
   7.571  lemma HInfinite_FreeUltrafilterNat_iff:
   7.572 -     "((x::hypreal) \<in> HInfinite) = (\<exists>X \<in> Rep_star x.
   7.573 -           \<forall>u. {n. u < abs (X n)} \<in> FreeUltrafilterNat)"
   7.574 +     "(star_n X \<in> HInfinite) = (\<forall>u. {n. u < norm (X n)} \<in> FreeUltrafilterNat)"
   7.575  by (blast intro!: HInfinite_FreeUltrafilterNat FreeUltrafilterNat_HInfinite)
   7.576  
   7.577  
   7.578  subsection{*Alternative Definitions for @{term Infinitesimal} using Free Ultrafilter*}
   7.579  
   7.580 +lemma ball_SReal_eq: "(\<forall>x::hypreal \<in> Reals. P x) = (\<forall>x::real. P (star_of x))"
   7.581 +by (unfold SReal_def, auto)
   7.582 +
   7.583  lemma Infinitesimal_FreeUltrafilterNat:
   7.584 -          "(x::hypreal) \<in> Infinitesimal ==> \<exists>X \<in> Rep_star x.
   7.585 -           \<forall>u. 0 < u --> {n. abs (X n) < u} \<in> FreeUltrafilterNat"
   7.586 -apply (simp add: Infinitesimal_def)
   7.587 -apply (auto simp add: abs_less_iff minus_less_iff [of x])
   7.588 -apply (cases x)
   7.589 -apply (auto, rule bexI [OF _ Rep_star_star_n], safe)
   7.590 -apply (drule star_of_less [THEN iffD2])
   7.591 -apply (drule_tac x = "hypreal_of_real u" in bspec, auto)
   7.592 -apply (auto simp add: star_n_less star_n_minus star_of_def, ultra)
   7.593 +     "star_n X \<in> Infinitesimal ==> \<forall>u>0. {n. norm (X n) < u} \<in> \<U>"
   7.594 +apply (simp add: Infinitesimal_def ball_SReal_eq)
   7.595 +apply (simp add: hnorm_def starfun_star_n star_of_def)
   7.596 +apply (simp add: star_less_def starP2_star_n)
   7.597  done
   7.598  
   7.599  lemma FreeUltrafilterNat_Infinitesimal:
   7.600 -     "\<exists>X \<in> Rep_star x.
   7.601 -            \<forall>u. 0 < u --> {n. abs (X n) < u} \<in> FreeUltrafilterNat
   7.602 -      ==> (x::hypreal) \<in> Infinitesimal"
   7.603 -apply (simp add: Infinitesimal_def)
   7.604 -apply (cases x)
   7.605 -apply (auto simp add: abs_less_iff abs_interval_iff minus_less_iff [of x])
   7.606 -apply (auto simp add: SReal_iff)
   7.607 -apply (drule_tac [!] x=y in spec) 
   7.608 -apply (auto simp add: star_n_less star_n_minus star_of_def, ultra+)
   7.609 +     "\<forall>u>0. {n. norm (X n) < u} \<in> \<U> ==> star_n X \<in> Infinitesimal"
   7.610 +apply (simp add: Infinitesimal_def ball_SReal_eq)
   7.611 +apply (simp add: hnorm_def starfun_star_n star_of_def)
   7.612 +apply (simp add: star_less_def starP2_star_n)
   7.613  done
   7.614  
   7.615  lemma Infinitesimal_FreeUltrafilterNat_iff:
   7.616 -     "((x::hypreal) \<in> Infinitesimal) = (\<exists>X \<in> Rep_star x.
   7.617 -           \<forall>u. 0 < u --> {n. abs (X n) < u} \<in> FreeUltrafilterNat)"
   7.618 +     "(star_n X \<in> Infinitesimal) = (\<forall>u>0. {n. norm (X n) < u} \<in> \<U>)"
   7.619  by (blast intro!: Infinitesimal_FreeUltrafilterNat FreeUltrafilterNat_Infinitesimal)
   7.620  
   7.621  (*------------------------------------------------------------------------
   7.622 @@ -2028,7 +2053,7 @@
   7.623  
   7.624  
   7.625  lemma Infinitesimal_hypreal_of_nat_iff:
   7.626 -     "Infinitesimal = {x. \<forall>n. abs x < inverse (hypreal_of_nat (Suc n))}"
   7.627 +     "Infinitesimal = {x. \<forall>n. hnorm x < inverse (hypreal_of_nat (Suc n))}"
   7.628  apply (simp add: Infinitesimal_def)
   7.629  apply (auto simp add: lemma_Infinitesimal2)
   7.630  done
   7.631 @@ -2098,11 +2123,9 @@
   7.632  done
   7.633  
   7.634  theorem HInfinite_omega [simp]: "omega \<in> HInfinite"
   7.635 -apply (simp add: omega_def star_n_def)
   7.636 -apply (auto intro!: FreeUltrafilterNat_HInfinite)
   7.637 -apply (rule bexI)
   7.638 -apply (rule_tac [2] lemma_starrel_refl, auto)
   7.639 -apply (simp (no_asm) add: real_of_nat_Suc diff_less_eq [symmetric] FreeUltrafilterNat_omega)
   7.640 +apply (simp add: omega_def)
   7.641 +apply (rule FreeUltrafilterNat_HInfinite)
   7.642 +apply (simp (no_asm) add: real_norm_def real_of_nat_Suc diff_less_eq [symmetric] FreeUltrafilterNat_omega)
   7.643  done
   7.644  
   7.645  (*-----------------------------------------------
   7.646 @@ -2202,27 +2225,30 @@
   7.647      |X(n) - x| < 1/n ==> [<X n>] - hypreal_of_real x| \<in> Infinitesimal
   7.648   -----------------------------------------------------*)
   7.649  lemma real_seq_to_hypreal_Infinitesimal:
   7.650 -     "\<forall>n. abs(X n + -x) < inverse(real(Suc n))
   7.651 -     ==> star_n X + -hypreal_of_real x \<in> Infinitesimal"
   7.652 +     "\<forall>n. norm(X n + -x) < inverse(real(Suc n))
   7.653 +     ==> star_n X + -star_of x \<in> Infinitesimal"
   7.654  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)
   7.655  done
   7.656  
   7.657  lemma real_seq_to_hypreal_approx:
   7.658 -     "\<forall>n. abs(X n + -x) < inverse(real(Suc n))
   7.659 -      ==> star_n X @= hypreal_of_real x"
   7.660 +     "\<forall>n. norm(X n + -x) < inverse(real(Suc n))
   7.661 +      ==> star_n X @= star_of x"
   7.662  apply (subst approx_minus_iff)
   7.663  apply (rule mem_infmal_iff [THEN subst])
   7.664  apply (erule real_seq_to_hypreal_Infinitesimal)
   7.665  done
   7.666  
   7.667  lemma real_seq_to_hypreal_approx2:
   7.668 -     "\<forall>n. abs(x + -X n) < inverse(real(Suc n))
   7.669 -               ==> star_n X @= hypreal_of_real x"
   7.670 -apply (simp add: abs_minus_add_cancel real_seq_to_hypreal_approx)
   7.671 +     "\<forall>n. norm(x + -X n) < inverse(real(Suc n))
   7.672 +               ==> star_n X @= star_of x"
   7.673 +apply (rule real_seq_to_hypreal_approx)
   7.674 +apply (subst norm_minus_cancel [symmetric])
   7.675 +apply (simp del: norm_minus_cancel)
   7.676 +apply (subst add_commute, assumption)
   7.677  done
   7.678  
   7.679  lemma real_seq_to_hypreal_Infinitesimal2:
   7.680 -     "\<forall>n. abs(X n + -Y n) < inverse(real(Suc n))
   7.681 +     "\<forall>n. norm(X n + -Y n) < inverse(real(Suc n))
   7.682        ==> star_n X + -star_n Y \<in> Infinitesimal"
   7.683  by (auto intro!: bexI
   7.684  	 dest: FreeUltrafilterNat_inverse_real_of_posnat 
     8.1 --- a/src/HOL/Hyperreal/SEQ.thy	Sat Sep 16 02:35:58 2006 +0200
     8.2 +++ b/src/HOL/Hyperreal/SEQ.thy	Sat Sep 16 02:40:00 2006 +0200
     8.3 @@ -14,13 +14,15 @@
     8.4  
     8.5  definition
     8.6  
     8.7 -  LIMSEQ :: "[nat=>real,real] => bool"    ("((_)/ ----> (_))" [60, 60] 60)
     8.8 +  LIMSEQ :: "[nat => 'a::real_normed_vector, 'a] => bool"
     8.9 +    ("((_)/ ----> (_))" [60, 60] 60)
    8.10      --{*Standard definition of convergence of sequence*}
    8.11 -  "X ----> L = (\<forall>r. 0 < r --> (\<exists>no. \<forall>n. no \<le> n --> \<bar>X n + -L\<bar> < r))"
    8.12 +  "X ----> L = (\<forall>r. 0 < r --> (\<exists>no. \<forall>n. no \<le> n --> norm (X n + -L) < r))"
    8.13  
    8.14 -  NSLIMSEQ :: "[nat=>real,real] => bool"    ("((_)/ ----NS> (_))" [60, 60] 60)
    8.15 +  NSLIMSEQ :: "[nat => 'a::real_normed_vector, 'a] => bool"
    8.16 +    ("((_)/ ----NS> (_))" [60, 60] 60)
    8.17      --{*Nonstandard definition of convergence of sequence*}
    8.18 -  "X ----NS> L = (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> hypreal_of_real L)"
    8.19 +  "X ----NS> L = (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> star_of L)"
    8.20  
    8.21    lim :: "(nat => real) => real"
    8.22      --{*Standard definition of limit using choice operator*}
    8.23 @@ -30,19 +32,19 @@
    8.24      --{*Nonstandard definition of limit using choice operator*}
    8.25    "nslim X = (SOME L. (X ----NS> L))"
    8.26  
    8.27 -  convergent :: "(nat => real) => bool"
    8.28 +  convergent :: "(nat => 'a::real_normed_vector) => bool"
    8.29      --{*Standard definition of convergence*}
    8.30    "convergent X = (\<exists>L. (X ----> L))"
    8.31  
    8.32 -  NSconvergent :: "(nat => real) => bool"
    8.33 +  NSconvergent :: "(nat => 'a::real_normed_vector) => bool"
    8.34      --{*Nonstandard definition of convergence*}
    8.35    "NSconvergent X = (\<exists>L. (X ----NS> L))"
    8.36  
    8.37 -  Bseq :: "(nat => real) => bool"
    8.38 +  Bseq :: "(nat => 'a::real_normed_vector) => bool"
    8.39      --{*Standard definition for bounded sequence*}
    8.40 -  "Bseq X = (\<exists>K>0.\<forall>n. \<bar>X n\<bar> \<le> K)"
    8.41 +  "Bseq X = (\<exists>K>0.\<forall>n. norm (X n) \<le> K)"
    8.42  
    8.43 -  NSBseq :: "(nat=>real) => bool"
    8.44 +  NSBseq :: "(nat => 'a::real_normed_vector) => bool"
    8.45      --{*Nonstandard definition for bounded sequence*}
    8.46    "NSBseq X = (\<forall>N \<in> HNatInfinite. ( *f* X) N : HFinite)"
    8.47  
    8.48 @@ -54,15 +56,16 @@
    8.49      --{*Definition of subsequence*}
    8.50    "subseq f = (\<forall>m. \<forall>n>m. (f m) < (f n))"
    8.51  
    8.52 -  Cauchy :: "(nat => real) => bool"
    8.53 +  Cauchy :: "(nat => 'a::real_normed_vector) => bool"
    8.54      --{*Standard definition of the Cauchy condition*}
    8.55 -  "Cauchy X = (\<forall>e>0. \<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. abs((X m) + -(X n)) < e)"
    8.56 +  "Cauchy X = (\<forall>e>0. \<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. norm((X m) + -(X n)) < e)"
    8.57  
    8.58 -  NSCauchy :: "(nat => real) => bool"
    8.59 +  NSCauchy :: "(nat => 'a::real_normed_vector) => bool"
    8.60      --{*Nonstandard definition*}
    8.61    "NSCauchy X = (\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite. ( *f* X) M \<approx> ( *f* X) N)"
    8.62  
    8.63  
    8.64 +declare real_norm_def [simp]
    8.65  
    8.66  text{* Example of an hypersequence (i.e. an extended standard sequence)
    8.67     whose term with an hypernatural suffix is an infinitesimal i.e.
    8.68 @@ -70,9 +73,8 @@
    8.69  
    8.70  lemma SEQ_Infinitesimal:
    8.71        "( *f* (%n::nat. inverse(real(Suc n)))) whn : Infinitesimal"
    8.72 -apply (simp add: hypnat_omega_def Infinitesimal_FreeUltrafilterNat_iff starfun)
    8.73 -apply (simp add: star_n_inverse)
    8.74 -apply (rule bexI [OF _ Rep_star_star_n])
    8.75 +apply (simp add: hypnat_omega_def starfun star_n_inverse)
    8.76 +apply (simp add: Infinitesimal_FreeUltrafilterNat_iff)
    8.77  apply (simp add: real_of_nat_Suc_gt_zero FreeUltrafilterNat_inverse_real_of_posnat)
    8.78  done
    8.79  
    8.80 @@ -80,28 +82,26 @@
    8.81  subsection{*LIMSEQ and NSLIMSEQ*}
    8.82  
    8.83  lemma LIMSEQ_iff:
    8.84 -      "(X ----> L) = (\<forall>r>0. \<exists>no. \<forall>n \<ge> no. \<bar>X n + -L\<bar> < r)"
    8.85 +      "(X ----> L) = (\<forall>r>0. \<exists>no. \<forall>n \<ge> no. norm (X n + -L) < r)"
    8.86  by (simp add: LIMSEQ_def)
    8.87  
    8.88  lemma NSLIMSEQ_iff:
    8.89 -    "(X ----NS> L) = (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> hypreal_of_real L)"
    8.90 +    "(X ----NS> L) = (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> star_of L)"
    8.91  by (simp add: NSLIMSEQ_def)
    8.92  
    8.93  
    8.94  text{*LIMSEQ ==> NSLIMSEQ*}
    8.95 -
    8.96  lemma LIMSEQ_NSLIMSEQ:
    8.97        "X ----> L ==> X ----NS> L"
    8.98 -apply (simp add: LIMSEQ_def NSLIMSEQ_def)
    8.99 -apply (auto simp add: HNatInfinite_FreeUltrafilterNat_iff)
   8.100 +apply (simp add: LIMSEQ_def NSLIMSEQ_def, safe)
   8.101  apply (rule_tac x = N in star_cases)
   8.102 +apply (simp add: HNatInfinite_FreeUltrafilterNat_iff)
   8.103  apply (rule approx_minus_iff [THEN iffD2])
   8.104  apply (auto simp add: starfun mem_infmal_iff [symmetric] star_of_def
   8.105                star_n_minus star_n_add Infinitesimal_FreeUltrafilterNat_iff)
   8.106 -apply (rule bexI [OF _ Rep_star_star_n], safe)
   8.107  apply (drule_tac x = u in spec, safe)
   8.108 -apply (drule_tac x = no in spec, fuf)
   8.109 -apply (blast dest: less_imp_le)
   8.110 +apply (drule_tac x = no in spec)
   8.111 +apply (erule ultra, simp add: less_imp_le)
   8.112  done
   8.113  
   8.114  
   8.115 @@ -148,29 +148,24 @@
   8.116  lemma HNatInfinite_NSLIMSEQ: "\<forall>n. n \<le> f n
   8.117            ==> star_n f : HNatInfinite"
   8.118  apply (auto simp add: HNatInfinite_FreeUltrafilterNat_iff)
   8.119 -apply (rule bexI [OF _ Rep_star_star_n], safe)
   8.120  apply (erule FreeUltrafilterNat_NSLIMSEQ)
   8.121  done
   8.122  
   8.123  lemma lemmaLIM:
   8.124 -     "{n. X (f n) + - L = Y n} Int {n. \<bar>Y n\<bar> < r} \<le>
   8.125 -      {n. \<bar>X (f n) + - L\<bar> < r}"
   8.126 +     "{n. X (f n) + - L = Y n} Int {n. norm (Y n) < r} \<le>
   8.127 +      {n. norm (X (f n) + - L) < r}"
   8.128  by auto
   8.129  
   8.130  lemma lemmaLIM2:
   8.131 -  "{n. \<bar>X (f n) + - L\<bar> < r} Int {n. r \<le> abs (X (f n) + - (L::real))} = {}"
   8.132 +  "{n. norm (X (f n) + - L) < r} Int {n. r \<le> norm (X (f n) + - L)} = {}"
   8.133  by auto
   8.134  
   8.135 -lemma lemmaLIM3: "[| 0 < r; \<forall>n. r \<le> \<bar>X (f n) + - L\<bar>;
   8.136 +lemma lemmaLIM3: "[| 0 < r; \<forall>n. r \<le> norm (X (f n) + - L);
   8.137             ( *f* X) (star_n f) +
   8.138 -           - hypreal_of_real  L \<approx> 0 |] ==> False"
   8.139 +           - star_of L \<approx> 0 |] ==> False"
   8.140  apply (auto simp add: starfun mem_infmal_iff [symmetric] star_of_def star_n_minus star_n_add Infinitesimal_FreeUltrafilterNat_iff)
   8.141 -apply (rename_tac "Y")
   8.142  apply (drule_tac x = r in spec, safe)
   8.143 -apply (drule FreeUltrafilterNat_Int, assumption)
   8.144 -apply (drule lemmaLIM [THEN [2] FreeUltrafilterNat_subset])
   8.145  apply (drule FreeUltrafilterNat_all)
   8.146 -apply (erule_tac V = "{n. \<bar>Y n\<bar> < r} : FreeUltrafilterNat" in thin_rl)
   8.147  apply (drule FreeUltrafilterNat_Int, assumption)
   8.148  apply (simp add: lemmaLIM2)
   8.149  done
   8.150 @@ -179,7 +174,7 @@
   8.151  apply (simp add: LIMSEQ_def NSLIMSEQ_def)
   8.152  apply (rule ccontr, simp, safe)
   8.153  txt{* skolemization step *}
   8.154 -apply (drule choice, safe)
   8.155 +apply (drule no_choice, safe)
   8.156  apply (drule_tac x = "star_n f" in bspec)
   8.157  apply (drule_tac [2] approx_minus_iff [THEN iffD1])
   8.158  apply (simp_all add: linorder_not_less)
   8.159 @@ -217,11 +212,14 @@
   8.160  by (simp add: LIMSEQ_NSLIMSEQ_iff [THEN sym] LIMSEQ_add_const)
   8.161  
   8.162  lemma NSLIMSEQ_mult:
   8.163 -      "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n * Y n) ----NS> a * b"
   8.164 +  fixes a b :: "'a::real_normed_algebra"
   8.165 +  shows "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n * Y n) ----NS> a * b"
   8.166  by (auto intro!: approx_mult_HFinite 
   8.167          simp add: NSLIMSEQ_def starfun_mult [symmetric])
   8.168  
   8.169 -lemma LIMSEQ_mult: "[| X ----> a; Y ----> b |] ==> (%n. X n * Y n) ----> a * b"
   8.170 +lemma LIMSEQ_mult:
   8.171 +  fixes a b :: "'a::real_normed_algebra"
   8.172 +  shows "[| X ----> a; Y ----> b |] ==> (%n. X n * Y n) ----> a * b"
   8.173  by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_mult)
   8.174  
   8.175  lemma NSLIMSEQ_minus: "X ----NS> a ==> (%n. -(X n)) ----NS> -a"
   8.176 @@ -266,22 +264,26 @@
   8.177  
   8.178  text{*Proof is like that of @{text NSLIM_inverse}.*}
   8.179  lemma NSLIMSEQ_inverse:
   8.180 -     "[| X ----NS> a;  a ~= 0 |] ==> (%n. inverse(X n)) ----NS> inverse(a)"
   8.181 -by (simp add: NSLIMSEQ_def starfun_inverse [symmetric] 
   8.182 -              hypreal_of_real_approx_inverse)
   8.183 +  fixes a :: "'a::{real_normed_div_algebra,division_by_zero}"
   8.184 +  shows "[| X ----NS> a;  a ~= 0 |] ==> (%n. inverse(X n)) ----NS> inverse(a)"
   8.185 +by (simp add: NSLIMSEQ_def star_of_approx_inverse)
   8.186  
   8.187  
   8.188  text{*Standard version of theorem*}
   8.189  lemma LIMSEQ_inverse:
   8.190 -     "[| X ----> a; a ~= 0 |] ==> (%n. inverse(X n)) ----> inverse(a)"
   8.191 +  fixes a :: "'a::{real_normed_div_algebra,division_by_zero}"
   8.192 +  shows "[| X ----> a; a ~= 0 |] ==> (%n. inverse(X n)) ----> inverse(a)"
   8.193  by (simp add: NSLIMSEQ_inverse LIMSEQ_NSLIMSEQ_iff)
   8.194  
   8.195  lemma NSLIMSEQ_mult_inverse:
   8.196 +  fixes a b :: "'a::{real_normed_div_algebra,field,division_by_zero}"
   8.197 +  shows
   8.198       "[| X ----NS> a;  Y ----NS> b;  b ~= 0 |] ==> (%n. X n / Y n) ----NS> a/b"
   8.199  by (simp add: NSLIMSEQ_mult NSLIMSEQ_inverse divide_inverse)
   8.200  
   8.201  lemma LIMSEQ_divide:
   8.202 -     "[| X ----> a;  Y ----> b;  b ~= 0 |] ==> (%n. X n / Y n) ----> a/b"
   8.203 +  fixes a b :: "'a::{real_normed_div_algebra,field,division_by_zero}"
   8.204 +  shows "[| X ----> a;  Y ----> b;  b ~= 0 |] ==> (%n. X n / Y n) ----> a/b"
   8.205  by (simp add: LIMSEQ_mult LIMSEQ_inverse divide_inverse)
   8.206  
   8.207  text{*Uniqueness of limit*}
   8.208 @@ -316,6 +318,7 @@
   8.209  qed
   8.210  
   8.211  lemma LIMSEQ_setprod:
   8.212 +  fixes L :: "'a \<Rightarrow> 'b::{real_normed_algebra,comm_ring_1}"
   8.213    assumes n: "\<And>n. n \<in> S \<Longrightarrow> X n ----> L n"
   8.214    shows "(\<lambda>m. \<Prod>n\<in>S. X n m) ----> (\<Prod>n\<in>S. L n)"
   8.215  proof (cases "finite S")
   8.216 @@ -455,15 +458,15 @@
   8.217  
   8.218  subsection{*Bounded Sequence*}
   8.219  
   8.220 -lemma BseqD: "Bseq X ==> \<exists>K. 0 < K & (\<forall>n. \<bar>X n\<bar> \<le> K)"
   8.221 +lemma BseqD: "Bseq X ==> \<exists>K. 0 < K & (\<forall>n. norm (X n) \<le> K)"
   8.222  by (simp add: Bseq_def)
   8.223  
   8.224 -lemma BseqI: "[| 0 < K; \<forall>n. \<bar>X n\<bar> \<le> K |] ==> Bseq X"
   8.225 +lemma BseqI: "[| 0 < K; \<forall>n. norm (X n) \<le> K |] ==> Bseq X"
   8.226  by (auto simp add: Bseq_def)
   8.227  
   8.228  lemma lemma_NBseq_def:
   8.229 -     "(\<exists>K > 0. \<forall>n. \<bar>X n\<bar> \<le> K) =
   8.230 -      (\<exists>N. \<forall>n. \<bar>X n\<bar> \<le> real(Suc N))"
   8.231 +     "(\<exists>K > 0. \<forall>n. norm (X n) \<le> K) =
   8.232 +      (\<exists>N. \<forall>n. norm (X n) \<le> real(Suc N))"
   8.233  apply auto
   8.234   prefer 2 apply force
   8.235  apply (cut_tac x = K in reals_Archimedean2, clarify)
   8.236 @@ -473,13 +476,13 @@
   8.237  done
   8.238  
   8.239  text{* alternative definition for Bseq *}
   8.240 -lemma Bseq_iff: "Bseq X = (\<exists>N. \<forall>n. \<bar>X n\<bar> \<le> real(Suc N))"
   8.241 +lemma Bseq_iff: "Bseq X = (\<exists>N. \<forall>n. norm (X n) \<le> real(Suc N))"
   8.242  apply (simp add: Bseq_def)
   8.243  apply (simp (no_asm) add: lemma_NBseq_def)
   8.244  done
   8.245  
   8.246  lemma lemma_NBseq_def2:
   8.247 -     "(\<exists>K > 0. \<forall>n. \<bar>X n\<bar> \<le> K) = (\<exists>N. \<forall>n. \<bar>X n\<bar> < real(Suc N))"
   8.248 +     "(\<exists>K > 0. \<forall>n. norm (X n) \<le> K) = (\<exists>N. \<forall>n. norm (X n) < real(Suc N))"
   8.249  apply (subst lemma_NBseq_def, auto)
   8.250  apply (rule_tac x = "Suc N" in exI)
   8.251  apply (rule_tac [2] x = N in exI)
   8.252 @@ -489,7 +492,7 @@
   8.253  done
   8.254  
   8.255  (* yet another definition for Bseq *)
   8.256 -lemma Bseq_iff1a: "Bseq X = (\<exists>N. \<forall>n. \<bar>X n\<bar> < real(Suc N))"
   8.257 +lemma Bseq_iff1a: "Bseq X = (\<exists>N. \<forall>n. norm (X n) < real(Suc N))"
   8.258  by (simp add: Bseq_def lemma_NBseq_def2)
   8.259  
   8.260  lemma NSBseqD: "[| NSBseq X;  N: HNatInfinite |] ==> ( *f* X) N : HFinite"
   8.261 @@ -500,7 +503,7 @@
   8.262  
   8.263  text{*The standard definition implies the nonstandard definition*}
   8.264  
   8.265 -lemma lemma_Bseq: "\<forall>n. \<bar>X n\<bar> \<le> K ==> \<forall>n. abs(X((f::nat=>nat) n)) \<le> K"
   8.266 +lemma lemma_Bseq: "\<forall>n. norm (X n) \<le> K ==> \<forall>n. norm(X((f::nat=>nat) n)) \<le> K"
   8.267  by auto
   8.268  
   8.269  lemma Bseq_NSBseq: "Bseq X ==> NSBseq X"
   8.270 @@ -508,7 +511,6 @@
   8.271  apply (rule_tac x = N in star_cases)
   8.272  apply (auto simp add: starfun HFinite_FreeUltrafilterNat_iff 
   8.273                        HNatInfinite_FreeUltrafilterNat_iff)
   8.274 -apply (rule bexI [OF _ Rep_star_star_n]) 
   8.275  apply (drule_tac f = Xa in lemma_Bseq)
   8.276  apply (rule_tac x = "K+1" in exI)
   8.277  apply (drule_tac P="%n. ?f n \<le> K" in FreeUltrafilterNat_all, ultra)
   8.278 @@ -525,23 +527,22 @@
   8.279     which woulid be useless.*}
   8.280  
   8.281  lemma lemmaNSBseq:
   8.282 -     "\<forall>K > 0. \<exists>n. K < \<bar>X n\<bar>
   8.283 -      ==> \<forall>N. \<exists>n. real(Suc N) < \<bar>X n\<bar>"
   8.284 +     "\<forall>K > 0. \<exists>n. K < norm (X n)
   8.285 +      ==> \<forall>N. \<exists>n. real(Suc N) < norm (X n)"
   8.286  apply safe
   8.287  apply (cut_tac n = N in real_of_nat_Suc_gt_zero, blast)
   8.288  done
   8.289  
   8.290 -lemma lemmaNSBseq2: "\<forall>K > 0. \<exists>n. K < \<bar>X n\<bar>
   8.291 -                     ==> \<exists>f. \<forall>N. real(Suc N) < \<bar>X (f N)\<bar>"
   8.292 +lemma lemmaNSBseq2: "\<forall>K > 0. \<exists>n::nat. K < norm (X n)
   8.293 +                     ==> \<exists>f. \<forall>N. real(Suc N) < norm (X (f N))"
   8.294  apply (drule lemmaNSBseq)
   8.295 -apply (drule choice, blast)
   8.296 +apply (drule no_choice, blast)
   8.297  done
   8.298  
   8.299  lemma real_seq_to_hypreal_HInfinite:
   8.300 -     "\<forall>N. real(Suc N) < \<bar>X (f N)\<bar>
   8.301 +     "\<forall>N. real(Suc N) < norm (X (f N))
   8.302        ==>  star_n (X o f) : HInfinite"
   8.303  apply (auto simp add: HInfinite_FreeUltrafilterNat_iff o_def)
   8.304 -apply (rule bexI [OF _ Rep_star_star_n], clarify)  
   8.305  apply (cut_tac u = u in FreeUltrafilterNat_nat_gt_real)
   8.306  apply (drule FreeUltrafilterNat_all)
   8.307  apply (erule FreeUltrafilterNat_Int [THEN FreeUltrafilterNat_subset])
   8.308 @@ -552,29 +553,28 @@
   8.309       defined using the skolem function  @{term "f::nat=>nat"} above*}
   8.310  
   8.311  lemma lemma_finite_NSBseq:
   8.312 -     "{n. f n \<le> Suc u & real(Suc n) < \<bar>X (f n)\<bar>} \<le>
   8.313 -      {n. f n \<le> u & real(Suc n) < \<bar>X (f n)\<bar>} Un
   8.314 -      {n. real(Suc n) < \<bar>X (Suc u)\<bar>}"
   8.315 +     "{n. f n \<le> Suc u & real(Suc n) < norm (X (f n))} \<le>
   8.316 +      {n. f n \<le> u & real(Suc n) < norm (X (f n))} Un
   8.317 +      {n. real(Suc n) < norm (X (Suc u))}"
   8.318  by (auto dest!: le_imp_less_or_eq)
   8.319  
   8.320  lemma lemma_finite_NSBseq2:
   8.321 -     "finite {n. f n \<le> (u::nat) &  real(Suc n) < \<bar>X(f n)\<bar>}"
   8.322 +     "finite {n. f n \<le> (u::nat) &  real(Suc n) < norm (X(f n))}"
   8.323  apply (induct "u")
   8.324  apply (rule_tac [2] lemma_finite_NSBseq [THEN finite_subset])
   8.325 -apply (rule_tac B = "{n. real (Suc n) < \<bar>X 0\<bar> }" in finite_subset)
   8.326 +apply (rule_tac B = "{n. real (Suc n) < norm (X 0) }" in finite_subset)
   8.327  apply (auto intro: finite_real_of_nat_less_real 
   8.328              simp add: real_of_nat_Suc less_diff_eq [symmetric])
   8.329  done
   8.330  
   8.331  lemma HNatInfinite_skolem_f:
   8.332 -     "\<forall>N. real(Suc N) < \<bar>X (f N)\<bar>
   8.333 +     "\<forall>N. real(Suc N) < norm (X (f N))
   8.334        ==> star_n f : HNatInfinite"
   8.335  apply (auto simp add: HNatInfinite_FreeUltrafilterNat_iff)
   8.336 -apply (rule bexI [OF _ Rep_star_star_n], safe)
   8.337  apply (rule ccontr, drule FreeUltrafilterNat_Compl_mem)
   8.338  apply (rule lemma_finite_NSBseq2 [THEN FreeUltrafilterNat_finite, THEN notE]) 
   8.339 -apply (subgoal_tac "{n. f n \<le> u & real (Suc n) < \<bar>X (f n)\<bar>} =
   8.340 -                    {n. f n \<le> u} \<inter> {N. real (Suc N) < \<bar>X (f N)\<bar>}")
   8.341 +apply (subgoal_tac "{n. f n \<le> u & real (Suc n) < norm (X (f n))} =
   8.342 +                    {n. f n \<le> u} \<inter> {N. real (Suc N) < norm (X (f N))}")
   8.343  apply (erule ssubst) 
   8.344   apply (auto simp add: linorder_not_less Compl_def)
   8.345  done
   8.346 @@ -600,7 +600,7 @@
   8.347  
   8.348  lemma NSconvergent_NSBseq: "NSconvergent X ==> NSBseq X"
   8.349  apply (simp add: NSconvergent_def NSBseq_def NSLIMSEQ_def)
   8.350 -apply (blast intro: HFinite_hypreal_of_real approx_sym approx_HFinite)
   8.351 +apply (blast intro: HFinite_star_of approx_sym approx_HFinite)
   8.352  done
   8.353  
   8.354  text{*Standard Version: easily now proved using equivalence of NS and
   8.355 @@ -624,10 +624,10 @@
   8.356     \<exists>U. isLub (UNIV::real set) {x. \<exists>n. X n = x} U"
   8.357  by (blast intro: reals_complete Bseq_isUb)
   8.358  
   8.359 -lemma NSBseq_isUb: "NSBseq X ==> \<exists>U. isUb UNIV {x. \<exists>n. X n = x} U"
   8.360 +lemma NSBseq_isUb: "NSBseq X ==> \<exists>U::real. isUb UNIV {x. \<exists>n. X n = x} U"
   8.361  by (simp add: Bseq_NSBseq_iff [symmetric] Bseq_isUb)
   8.362  
   8.363 -lemma NSBseq_isLub: "NSBseq X ==> \<exists>U. isLub UNIV {x. \<exists>n. X n = x} U"
   8.364 +lemma NSBseq_isLub: "NSBseq X ==> \<exists>U::real. isLub UNIV {x. \<exists>n. X n = x} U"
   8.365  by (simp add: Bseq_NSBseq_iff [symmetric] Bseq_isLub)
   8.366  
   8.367  
   8.368 @@ -686,7 +686,7 @@
   8.369  text{*A standard proof of the theorem for monotone increasing sequence*}
   8.370  
   8.371  lemma Bseq_mono_convergent:
   8.372 -     "[| Bseq X; \<forall>m. \<forall>n \<ge> m. X m \<le> X n |] ==> convergent X"
   8.373 +     "[| Bseq X; \<forall>m. \<forall>n \<ge> m. X m \<le> X n |] ==> convergent (X::nat=>real)"
   8.374  apply (simp add: convergent_def)
   8.375  apply (frule Bseq_isLub, safe)
   8.376  apply (case_tac "\<exists>m. X m = U", auto)
   8.377 @@ -705,7 +705,7 @@
   8.378  text{*Nonstandard version of the theorem*}
   8.379  
   8.380  lemma NSBseq_mono_NSconvergent:
   8.381 -     "[| NSBseq X; \<forall>m. \<forall>n \<ge> m. X m \<le> X n |] ==> NSconvergent X"
   8.382 +     "[| NSBseq X; \<forall>m. \<forall>n \<ge> m. X m \<le> X n |] ==> NSconvergent (X::nat=>real)"
   8.383  by (auto intro: Bseq_mono_convergent 
   8.384           simp add: convergent_NSconvergent_iff [symmetric] 
   8.385                     Bseq_NSBseq_iff [symmetric])
   8.386 @@ -731,26 +731,31 @@
   8.387  subsection{*A Few More Equivalence Theorems for Boundedness*}
   8.388  
   8.389  text{*alternative formulation for boundedness*}
   8.390 -lemma Bseq_iff2: "Bseq X = (\<exists>k > 0. \<exists>x. \<forall>n. \<bar>X(n) + -x\<bar> \<le> k)"
   8.391 +lemma Bseq_iff2: "Bseq X = (\<exists>k > 0. \<exists>x. \<forall>n. norm (X(n) + -x) \<le> k)"
   8.392  apply (unfold Bseq_def, safe)
   8.393 -apply (rule_tac [2] x = "k + \<bar>x\<bar> " in exI)
   8.394 +apply (rule_tac [2] x = "k + norm x" in exI)
   8.395  apply (rule_tac x = K in exI, simp)
   8.396  apply (rule exI [where x = 0], auto)
   8.397 -apply (drule_tac x=n in spec, arith)+
   8.398 +apply (erule order_less_le_trans, simp)
   8.399 +apply (drule_tac x=n in spec, fold diff_def)
   8.400 +apply (drule order_trans [OF norm_triangle_ineq2])
   8.401 +apply simp
   8.402  done
   8.403  
   8.404  text{*alternative formulation for boundedness*}
   8.405 -lemma Bseq_iff3: "Bseq X = (\<exists>k > 0. \<exists>N. \<forall>n. abs(X(n) + -X(N)) \<le> k)"
   8.406 +lemma Bseq_iff3: "Bseq X = (\<exists>k > 0. \<exists>N. \<forall>n. norm(X(n) + -X(N)) \<le> k)"
   8.407  apply safe
   8.408  apply (simp add: Bseq_def, safe)
   8.409 -apply (rule_tac x = "K + \<bar>X N\<bar> " in exI)
   8.410 +apply (rule_tac x = "K + norm (X N)" in exI)
   8.411  apply auto
   8.412 +apply (erule order_less_le_trans, simp)
   8.413  apply (rule_tac x = N in exI, safe)
   8.414 -apply (drule_tac x = n in spec, arith)
   8.415 +apply (drule_tac x = n in spec)
   8.416 +apply (rule order_trans [OF norm_triangle_ineq], simp)
   8.417  apply (auto simp add: Bseq_iff2)
   8.418  done
   8.419  
   8.420 -lemma BseqI2: "(\<forall>n. k \<le> f n & f n \<le> K) ==> Bseq f"
   8.421 +lemma BseqI2: "(\<forall>n. k \<le> f n & f n \<le> (K::real)) ==> Bseq f"
   8.422  apply (simp add: Bseq_def)
   8.423  apply (rule_tac x = " (\<bar>k\<bar> + \<bar>K\<bar>) + 1" in exI, auto)
   8.424  apply (drule_tac x = n in spec, arith)
   8.425 @@ -769,9 +774,9 @@
   8.426  done
   8.427  
   8.428  lemma lemmaCauchy2:
   8.429 -     "{n. \<forall>m n. M \<le> m & M \<le> (n::nat) --> \<bar>X m + - X n\<bar> < u} Int
   8.430 +     "{n. \<forall>m n. M \<le> m & M \<le> (n::nat) --> norm (X m + - X n) < u} Int
   8.431        {n. M \<le> xa n} Int {n. M \<le> x n} \<le>
   8.432 -      {n. abs (X (xa n) + - X (x n)) < u}"
   8.433 +      {n. norm (X (xa n) + - X (x n)) < u}"
   8.434  by blast
   8.435  
   8.436  lemma Cauchy_NSCauchy: "Cauchy X ==> NSCauchy X"
   8.437 @@ -781,7 +786,6 @@
   8.438  apply (rule approx_minus_iff [THEN iffD2])
   8.439  apply (rule mem_infmal_iff [THEN iffD1])
   8.440  apply (auto simp add: starfun star_n_minus star_n_add Infinitesimal_FreeUltrafilterNat_iff)
   8.441 -apply (rule bexI, auto)
   8.442  apply (drule spec, auto)
   8.443  apply (drule_tac M = M in lemmaCauchy1)
   8.444  apply (drule_tac M = M in lemmaCauchy1)
   8.445 @@ -795,23 +799,14 @@
   8.446  lemma NSCauchy_Cauchy: "NSCauchy X ==> Cauchy X"
   8.447  apply (auto simp add: Cauchy_def NSCauchy_def)
   8.448  apply (rule ccontr, simp)
   8.449 -apply (auto dest!: choice HNatInfinite_NSLIMSEQ simp add: all_conj_distrib)  
   8.450 +apply (auto dest!: no_choice HNatInfinite_NSLIMSEQ
   8.451 +            simp add: all_conj_distrib)
   8.452  apply (drule bspec, assumption)
   8.453  apply (drule_tac x = "star_n fa" in bspec); 
   8.454  apply (auto simp add: starfun)
   8.455  apply (drule approx_minus_iff [THEN iffD1])
   8.456  apply (drule mem_infmal_iff [THEN iffD2])
   8.457  apply (auto simp add: star_n_minus star_n_add Infinitesimal_FreeUltrafilterNat_iff)
   8.458 -apply (rename_tac "Y")
   8.459 -apply (drule_tac x = e in spec, auto)
   8.460 -apply (drule FreeUltrafilterNat_Int, assumption)
   8.461 -apply (subgoal_tac "{n. \<bar>X (f n) + - X (fa n)\<bar> < e} \<in> \<U>") 
   8.462 - prefer 2 apply (erule FreeUltrafilterNat_subset, force) 
   8.463 -apply (rule FreeUltrafilterNat_empty [THEN notE]) 
   8.464 -apply (subgoal_tac
   8.465 -         "{n. abs (X (f n) + - X (fa n)) < e} Int 
   8.466 -          {M. ~ abs (X (f M) + - X (fa M)) < e}  =  {}")
   8.467 -apply auto  
   8.468  done
   8.469  
   8.470  
   8.471 @@ -821,9 +816,13 @@
   8.472  text{*A Cauchy sequence is bounded -- this is the standard
   8.473    proof mechanization rather than the nonstandard proof*}
   8.474  
   8.475 -lemma lemmaCauchy: "\<forall>n \<ge> M. \<bar>X M + - X n\<bar> < (1::real)
   8.476 -          ==>  \<forall>n \<ge> M. \<bar>X n\<bar> < 1 + \<bar>X M\<bar>"
   8.477 -by auto
   8.478 +lemma lemmaCauchy: "\<forall>n \<ge> M. norm (X M + - X n) < (1::real)
   8.479 +          ==>  \<forall>n \<ge> M. norm (X n :: 'a::real_normed_vector) < 1 + norm (X M)"
   8.480 +apply (clarify, drule spec, drule (1) mp)
   8.481 +apply (fold diff_def, simp only: norm_minus_commute)
   8.482 +apply (drule order_le_less_trans [OF norm_triangle_ineq2])
   8.483 +apply simp
   8.484 +done
   8.485  
   8.486  lemma less_Suc_cancel_iff: "(n < Suc M) = (n \<le> M)"
   8.487  by auto
   8.488 @@ -842,7 +841,7 @@
   8.489  done
   8.490  
   8.491  lemma SUP_rabs_subseq:
   8.492 -     "\<exists>m \<le> M. \<forall>n \<le> M. \<bar>(X::nat=> real) n\<bar> \<le> \<bar>X m\<bar>"
   8.493 +     "\<exists>m::nat \<le> M. \<forall>n \<le> M. norm (X n) \<le> norm (X m)"
   8.494  by (rule SUP_subseq)
   8.495  
   8.496  lemma lemma_Nat_covered:
   8.497 @@ -853,47 +852,52 @@
   8.498  
   8.499  
   8.500  lemma lemma_trans1:
   8.501 -     "[| \<forall>n \<le> M. \<bar>(X::nat=>real) n\<bar> \<le> a;  a < b |]
   8.502 -      ==> \<forall>n \<le> M. \<bar>X n\<bar> \<le> b"
   8.503 +     "[| \<forall>n \<le> M. norm ((X::nat=>'a::real_normed_vector) n) \<le> a;  a < b |]
   8.504 +      ==> \<forall>n \<le> M. norm (X n) \<le> b"
   8.505  by (blast intro: order_le_less_trans [THEN order_less_imp_le])
   8.506  
   8.507  lemma lemma_trans2:
   8.508 -     "[| \<forall>n \<ge> M. \<bar>(X::nat=>real) n\<bar> < a; a < b |]
   8.509 -      ==> \<forall>n \<ge> M. \<bar>X n\<bar>\<le> b"
   8.510 +     "[| \<forall>n \<ge> M. norm ((X::nat=>'a::real_normed_vector) n) < a; a < b |]
   8.511 +      ==> \<forall>n \<ge> M. norm (X n) \<le> b"
   8.512  by (blast intro: order_less_trans [THEN order_less_imp_le])
   8.513  
   8.514  lemma lemma_trans3:
   8.515 -     "[| \<forall>n \<le> M. \<bar>X n\<bar> \<le> a; a = b |]
   8.516 -      ==> \<forall>n \<le> M. \<bar>X n\<bar> \<le> b"
   8.517 +     "[| \<forall>n \<le> M. norm (X n) \<le> a; a = b |]
   8.518 +      ==> \<forall>n \<le> M. norm (X n) \<le> b"
   8.519  by auto
   8.520  
   8.521 -lemma lemma_trans4: "\<forall>n \<ge> M. \<bar>(X::nat=>real) n\<bar> < a
   8.522 -              ==>  \<forall>n \<ge> M. \<bar>X n\<bar> \<le> a"
   8.523 +lemma lemma_trans4: "\<forall>n \<ge> M. norm ((X::nat=>'a::real_normed_vector) n) < a
   8.524 +              ==>  \<forall>n \<ge> M. norm (X n) \<le> a"
   8.525  by (blast intro: order_less_imp_le)
   8.526  
   8.527  
   8.528  text{*Proof is more involved than outlines sketched by various authors
   8.529   would suggest*}
   8.530  
   8.531 +lemma Bseq_Suc_imp_Bseq: "Bseq (\<lambda>n. X (Suc n)) \<Longrightarrow> Bseq X"
   8.532 +apply (unfold Bseq_def, clarify)
   8.533 +apply (rule_tac x="max K (norm (X 0))" in exI)
   8.534 +apply (simp add: order_less_le_trans [OF _ le_maxI1])
   8.535 +apply (clarify, case_tac "n", simp)
   8.536 +apply (simp add: order_trans [OF _ le_maxI1])
   8.537 +done
   8.538 +
   8.539 +lemma Bseq_shift_imp_Bseq: "Bseq (\<lambda>n. X (n + k)) \<Longrightarrow> Bseq X"
   8.540 +apply (induct k, simp_all)
   8.541 +apply (subgoal_tac "Bseq (\<lambda>n. X (n + k))", simp)
   8.542 +apply (rule Bseq_Suc_imp_Bseq, simp)
   8.543 +done
   8.544 +
   8.545  lemma Cauchy_Bseq: "Cauchy X ==> Bseq X"
   8.546 -apply (simp add: Cauchy_def Bseq_def)
   8.547 -apply (drule_tac x = 1 in spec)
   8.548 -apply (erule zero_less_one [THEN [2] impE], safe)
   8.549 -apply (drule_tac x = M in spec, simp)
   8.550 +apply (simp add: Cauchy_def)
   8.551 +apply (drule spec, drule mp, rule zero_less_one, safe)
   8.552 +apply (drule_tac x="M" in spec, simp)
   8.553  apply (drule lemmaCauchy)
   8.554 -apply (cut_tac M = M and X = X in SUP_rabs_subseq, safe)
   8.555 -apply (cut_tac x = "\<bar>X m\<bar> " and y = "1 + \<bar>X M\<bar> " in linorder_less_linear)
   8.556 -apply safe
   8.557 -apply (drule lemma_trans1, assumption)
   8.558 -apply (drule_tac [3] lemma_trans2, erule_tac [3] asm_rl)
   8.559 -apply (drule_tac [2] lemma_trans3, erule_tac [2] asm_rl)
   8.560 -apply (drule_tac [3] abs_add_one_gt_zero [THEN order_less_trans])
   8.561 -apply (drule lemma_trans4)
   8.562 -apply (drule_tac [2] lemma_trans4)
   8.563 -apply (rule_tac x = "1 + \<bar>X M\<bar> " in exI)
   8.564 -apply (rule_tac [2] x = "1 + \<bar>X M\<bar> " in exI)
   8.565 -apply (rule_tac [3] x = "\<bar>X m\<bar> " in exI)
   8.566 -apply (auto elim!: lemma_Nat_covered)
   8.567 +apply (rule_tac k="M" in Bseq_shift_imp_Bseq)
   8.568 +apply (simp add: Bseq_def)
   8.569 +apply (rule_tac x="1 + norm (X M)" in exI)
   8.570 +apply (rule conjI, rule order_less_le_trans [OF zero_less_one], simp)
   8.571 +apply (simp add: order_less_imp_le)
   8.572  done
   8.573  
   8.574  text{*A Cauchy sequence is bounded -- nonstandard version*}
   8.575 @@ -912,7 +916,7 @@
   8.576    instantiations for his 'espsilon-delta' proof(s) in this case
   8.577    since the NS formulations do not involve existential quantifiers.*}
   8.578  
   8.579 -lemma NSCauchy_NSconvergent_iff: "NSCauchy X = NSconvergent X"
   8.580 +lemma NSCauchy_NSconvergent_iff: "NSCauchy X = NSconvergent (X::nat=>real)"
   8.581  apply (simp add: NSconvergent_def NSLIMSEQ_def, safe)
   8.582  apply (frule NSCauchy_NSBseq)
   8.583  apply (auto intro: approx_trans2 simp add: NSBseq_def NSCauchy_def)
   8.584 @@ -923,7 +927,7 @@
   8.585  done
   8.586  
   8.587  text{*Standard proof for free*}
   8.588 -lemma Cauchy_convergent_iff: "Cauchy X = convergent X"
   8.589 +lemma Cauchy_convergent_iff: "Cauchy X = convergent (X::nat=>real)"
   8.590  by (simp add: NSCauchy_Cauchy_iff [symmetric] convergent_NSconvergent_iff NSCauchy_NSconvergent_iff)
   8.591  
   8.592  
   8.593 @@ -933,7 +937,7 @@
   8.594  lemma NSLIMSEQ_le:
   8.595         "[| f ----NS> l; g ----NS> m;
   8.596             \<exists>N. \<forall>n \<ge> N. f(n) \<le> g(n)
   8.597 -        |] ==> l \<le> m"
   8.598 +        |] ==> l \<le> (m::real)"
   8.599  apply (simp add: NSLIMSEQ_def, safe)
   8.600  apply (drule starfun_le_mono)
   8.601  apply (drule HNatInfinite_whn [THEN [2] bspec])+
   8.602 @@ -946,23 +950,23 @@
   8.603  (* standard version *)
   8.604  lemma LIMSEQ_le:
   8.605       "[| f ----> l; g ----> m; \<exists>N. \<forall>n \<ge> N. f(n) \<le> g(n) |]
   8.606 -      ==> l \<le> m"
   8.607 +      ==> l \<le> (m::real)"
   8.608  by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_le)
   8.609  
   8.610 -lemma LIMSEQ_le_const: "[| X ----> r; \<forall>n. a \<le> X n |] ==> a \<le> r"
   8.611 +lemma LIMSEQ_le_const: "[| X ----> (r::real); \<forall>n. a \<le> X n |] ==> a \<le> r"
   8.612  apply (rule LIMSEQ_le)
   8.613  apply (rule LIMSEQ_const, auto)
   8.614  done
   8.615  
   8.616 -lemma NSLIMSEQ_le_const: "[| X ----NS> r; \<forall>n. a \<le> X n |] ==> a \<le> r"
   8.617 +lemma NSLIMSEQ_le_const: "[| X ----NS> (r::real); \<forall>n. a \<le> X n |] ==> a \<le> r"
   8.618  by (simp add: LIMSEQ_NSLIMSEQ_iff LIMSEQ_le_const)
   8.619  
   8.620 -lemma LIMSEQ_le_const2: "[| X ----> r; \<forall>n. X n \<le> a |] ==> r \<le> a"
   8.621 +lemma LIMSEQ_le_const2: "[| X ----> (r::real); \<forall>n. X n \<le> a |] ==> r \<le> a"
   8.622  apply (rule LIMSEQ_le)
   8.623  apply (rule_tac [2] LIMSEQ_const, auto)
   8.624  done
   8.625  
   8.626 -lemma NSLIMSEQ_le_const2: "[| X ----NS> r; \<forall>n. X n \<le> a |] ==> r \<le> a"
   8.627 +lemma NSLIMSEQ_le_const2: "[| X ----NS> (r::real); \<forall>n. X n \<le> a |] ==> r \<le> a"
   8.628  by (simp add: LIMSEQ_NSLIMSEQ_iff LIMSEQ_le_const2)
   8.629  
   8.630  text{*Shift a convergent series by 1:
   8.631 @@ -970,12 +974,10 @@
   8.632    the successor of an infinite hypernatural is also infinite.*}
   8.633  
   8.634  lemma NSLIMSEQ_Suc: "f ----NS> l ==> (%n. f(Suc n)) ----NS> l"
   8.635 -apply (frule NSconvergentI [THEN NSCauchy_NSconvergent_iff [THEN iffD2]])
   8.636 -apply (auto simp add: NSCauchy_def NSLIMSEQ_def starfun_shift_one)
   8.637 -apply (drule bspec, assumption)
   8.638 -apply (drule bspec, assumption)
   8.639 -apply (drule Nats_1 [THEN [2] HNatInfinite_SHNat_add])
   8.640 -apply (blast intro: approx_trans3)
   8.641 +apply (unfold NSLIMSEQ_def, safe)
   8.642 +apply (drule_tac x="N + 1" in bspec)
   8.643 +apply (erule Nats_1 [THEN [2] HNatInfinite_SHNat_add])
   8.644 +apply (simp add: starfun_shift_one)
   8.645  done
   8.646  
   8.647  text{* standard version *}
   8.648 @@ -983,13 +985,10 @@
   8.649  by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_Suc)
   8.650  
   8.651  lemma NSLIMSEQ_imp_Suc: "(%n. f(Suc n)) ----NS> l ==> f ----NS> l"
   8.652 -apply (frule NSconvergentI [THEN NSCauchy_NSconvergent_iff [THEN iffD2]])
   8.653 -apply (auto simp add: NSCauchy_def NSLIMSEQ_def starfun_shift_one)
   8.654 -apply (drule bspec, assumption)
   8.655 -apply (drule bspec, assumption)
   8.656 -apply (frule Nats_1 [THEN [2] HNatInfinite_SHNat_diff])
   8.657 +apply (unfold NSLIMSEQ_def, safe)
   8.658  apply (drule_tac x="N - 1" in bspec) 
   8.659 -apply (auto intro: approx_trans3)
   8.660 +apply (erule Nats_1 [THEN [2] HNatInfinite_SHNat_diff])
   8.661 +apply (simp add: starfun_shift_one)
   8.662  done
   8.663  
   8.664  lemma LIMSEQ_imp_Suc: "(%n. f(Suc n)) ----> l ==> f ----> l"
   8.665 @@ -1004,30 +1003,30 @@
   8.666  by (blast intro: NSLIMSEQ_imp_Suc NSLIMSEQ_Suc)
   8.667  
   8.668  text{*A sequence tends to zero iff its abs does*}
   8.669 -lemma LIMSEQ_rabs_zero: "((%n. \<bar>f n\<bar>) ----> 0) = (f ----> 0)"
   8.670 +lemma LIMSEQ_rabs_zero: "((%n. \<bar>f n\<bar>) ----> 0) = (f ----> (0::real))"
   8.671  by (simp add: LIMSEQ_def)
   8.672  
   8.673  text{*We prove the NS version from the standard one, since the NS proof
   8.674     seems more complicated than the standard one above!*}
   8.675 -lemma NSLIMSEQ_rabs_zero: "((%n. \<bar>f n\<bar>) ----NS> 0) = (f ----NS> 0)"
   8.676 +lemma NSLIMSEQ_rabs_zero: "((%n. \<bar>f n\<bar>) ----NS> 0) = (f ----NS> (0::real))"
   8.677  by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_rabs_zero)
   8.678  
   8.679  text{*Generalization to other limits*}
   8.680 -lemma NSLIMSEQ_imp_rabs: "f ----NS> l ==> (%n. \<bar>f n\<bar>) ----NS> \<bar>l\<bar>"
   8.681 +lemma NSLIMSEQ_imp_rabs: "f ----NS> (l::real) ==> (%n. \<bar>f n\<bar>) ----NS> \<bar>l\<bar>"
   8.682  apply (simp add: NSLIMSEQ_def)
   8.683  apply (auto intro: approx_hrabs 
   8.684              simp add: starfun_abs hypreal_of_real_hrabs [symmetric])
   8.685  done
   8.686  
   8.687  text{* standard version *}
   8.688 -lemma LIMSEQ_imp_rabs: "f ----> l ==> (%n. \<bar>f n\<bar>) ----> \<bar>l\<bar>"
   8.689 +lemma LIMSEQ_imp_rabs: "f ----> (l::real) ==> (%n. \<bar>f n\<bar>) ----> \<bar>l\<bar>"
   8.690  by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_imp_rabs)
   8.691  
   8.692  text{*An unbounded sequence's inverse tends to 0*}
   8.693  
   8.694  text{* standard proof seems easier *}
   8.695  lemma LIMSEQ_inverse_zero:
   8.696 -      "\<forall>y. \<exists>N. \<forall>n \<ge> N. y < f(n) ==> (%n. inverse(f n)) ----> 0"
   8.697 +      "\<forall>y::real. \<exists>N. \<forall>n \<ge> N. y < f(n) ==> (%n. inverse(f n)) ----> 0"
   8.698  apply (simp add: LIMSEQ_def, safe)
   8.699  apply (drule_tac x = "inverse r" in spec, safe)
   8.700  apply (rule_tac x = N in exI, safe)
   8.701 @@ -1042,7 +1041,7 @@
   8.702  done
   8.703  
   8.704  lemma NSLIMSEQ_inverse_zero:
   8.705 -     "\<forall>y. \<exists>N. \<forall>n \<ge> N. y < f(n)
   8.706 +     "\<forall>y::real. \<exists>N. \<forall>n \<ge> N. y < f(n)
   8.707        ==> (%n. inverse(f n)) ----NS> 0"
   8.708  by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_zero)
   8.709  
   8.710 @@ -1090,19 +1089,22 @@
   8.711  text{* Real Powers*}
   8.712  
   8.713  lemma NSLIMSEQ_pow [rule_format]:
   8.714 -     "(X ----NS> a) --> ((%n. (X n) ^ m) ----NS> a ^ m)"
   8.715 +  fixes a :: "'a::{real_normed_algebra,recpower}"
   8.716 +  shows "(X ----NS> a) --> ((%n. (X n) ^ m) ----NS> a ^ m)"
   8.717  apply (induct "m")
   8.718 -apply (auto intro: NSLIMSEQ_mult NSLIMSEQ_const)
   8.719 +apply (auto simp add: power_Suc intro: NSLIMSEQ_mult NSLIMSEQ_const)
   8.720  done
   8.721  
   8.722 -lemma LIMSEQ_pow: "X ----> a ==> (%n. (X n) ^ m) ----> a ^ m"
   8.723 +lemma LIMSEQ_pow:
   8.724 +  fixes a :: "'a::{real_normed_algebra,recpower}"
   8.725 +  shows "X ----> a ==> (%n. (X n) ^ m) ----> a ^ m"
   8.726  by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_pow)
   8.727  
   8.728  text{*The sequence @{term "x^n"} tends to 0 if @{term "0\<le>x"} and @{term
   8.729  "x<1"}.  Proof will use (NS) Cauchy equivalence for convergence and
   8.730    also fact that bounded and monotonic sequence converges.*}
   8.731  
   8.732 -lemma Bseq_realpow: "[| 0 \<le> x; x \<le> 1 |] ==> Bseq (%n. x ^ n)"
   8.733 +lemma Bseq_realpow: "[| 0 \<le> (x::real); x \<le> 1 |] ==> Bseq (%n. x ^ n)"
   8.734  apply (simp add: Bseq_def)
   8.735  apply (rule_tac x = 1 in exI)
   8.736  apply (simp add: power_abs)
   8.737 @@ -1114,12 +1116,14 @@
   8.738  apply (cut_tac n = n and N = "Suc n" and a = x in power_decreasing, auto)
   8.739  done
   8.740  
   8.741 -lemma convergent_realpow: "[| 0 \<le> x; x \<le> 1 |] ==> convergent (%n. x ^ n)"
   8.742 +lemma convergent_realpow:
   8.743 +  "[| 0 \<le> (x::real); x \<le> 1 |] ==> convergent (%n. x ^ n)"
   8.744  by (blast intro!: Bseq_monoseq_convergent Bseq_realpow monoseq_realpow)
   8.745  
   8.746  text{* We now use NS criterion to bring proof of theorem through *}
   8.747  
   8.748 -lemma NSLIMSEQ_realpow_zero: "[| 0 \<le> x; x < 1 |] ==> (%n. x ^ n) ----NS> 0"
   8.749 +lemma NSLIMSEQ_realpow_zero:
   8.750 +  "[| 0 \<le> (x::real); x < 1 |] ==> (%n. x ^ n) ----NS> 0"
   8.751  apply (simp add: NSLIMSEQ_def)
   8.752  apply (auto dest!: convergent_realpow simp add: convergent_NSconvergent_iff)
   8.753  apply (frule NSconvergentD)
   8.754 @@ -1135,10 +1139,12 @@
   8.755  done
   8.756  
   8.757  text{* standard version *}
   8.758 -lemma LIMSEQ_realpow_zero: "[| 0 \<le> x; x < 1 |] ==> (%n. x ^ n) ----> 0"
   8.759 +lemma LIMSEQ_realpow_zero:
   8.760 +  "[| 0 \<le> (x::real); x < 1 |] ==> (%n. x ^ n) ----> 0"
   8.761  by (simp add: NSLIMSEQ_realpow_zero LIMSEQ_NSLIMSEQ_iff)
   8.762  
   8.763 -lemma LIMSEQ_divide_realpow_zero: "1 < x ==> (%n. a / (x ^ n)) ----> 0"
   8.764 +lemma LIMSEQ_divide_realpow_zero:
   8.765 +  "1 < (x::real) ==> (%n. a / (x ^ n)) ----> 0"
   8.766  apply (cut_tac a = a and x1 = "inverse x" in
   8.767          LIMSEQ_mult [OF LIMSEQ_const LIMSEQ_realpow_zero])
   8.768  apply (auto simp add: divide_inverse power_inverse)
   8.769 @@ -1147,18 +1153,18 @@
   8.770  
   8.771  text{*Limit of @{term "c^n"} for @{term"\<bar>c\<bar> < 1"}*}
   8.772  
   8.773 -lemma LIMSEQ_rabs_realpow_zero: "\<bar>c\<bar> < 1 ==> (%n. \<bar>c\<bar> ^ n) ----> 0"
   8.774 +lemma LIMSEQ_rabs_realpow_zero: "\<bar>c\<bar> < (1::real) ==> (%n. \<bar>c\<bar> ^ n) ----> 0"
   8.775  by (blast intro!: LIMSEQ_realpow_zero abs_ge_zero)
   8.776  
   8.777 -lemma NSLIMSEQ_rabs_realpow_zero: "\<bar>c\<bar> < 1 ==> (%n. \<bar>c\<bar> ^ n) ----NS> 0"
   8.778 +lemma NSLIMSEQ_rabs_realpow_zero: "\<bar>c\<bar> < (1::real) ==> (%n. \<bar>c\<bar> ^ n) ----NS> 0"
   8.779  by (simp add: LIMSEQ_rabs_realpow_zero LIMSEQ_NSLIMSEQ_iff [symmetric])
   8.780  
   8.781 -lemma LIMSEQ_rabs_realpow_zero2: "\<bar>c\<bar> < 1 ==> (%n. c ^ n) ----> 0"
   8.782 +lemma LIMSEQ_rabs_realpow_zero2: "\<bar>c\<bar> < (1::real) ==> (%n. c ^ n) ----> 0"
   8.783  apply (rule LIMSEQ_rabs_zero [THEN iffD1])
   8.784  apply (auto intro: LIMSEQ_rabs_realpow_zero simp add: power_abs)
   8.785  done
   8.786  
   8.787 -lemma NSLIMSEQ_rabs_realpow_zero2: "\<bar>c\<bar> < 1 ==> (%n. c ^ n) ----NS> 0"
   8.788 +lemma NSLIMSEQ_rabs_realpow_zero2: "\<bar>c\<bar> < (1::real) ==> (%n. c ^ n) ----NS> 0"
   8.789  by (simp add: LIMSEQ_rabs_realpow_zero2 LIMSEQ_NSLIMSEQ_iff [symmetric])
   8.790  
   8.791  subsection{*Hyperreals and Sequences*}
     9.1 --- a/src/HOL/Hyperreal/Series.thy	Sat Sep 16 02:35:58 2006 +0200
     9.2 +++ b/src/HOL/Hyperreal/Series.thy	Sat Sep 16 02:40:00 2006 +0200
     9.3 @@ -354,7 +354,7 @@
     9.4  apply (drule spec, drule (1) mp)
     9.5  apply (erule exE, rule_tac x="N" in exI, clarify)
     9.6  apply (rule_tac x="m" and y="n" in linorder_le_cases)
     9.7 -apply (subst abs_minus_commute)
     9.8 +apply (subst norm_minus_commute)
     9.9  apply (simp add: setsum_diff [symmetric])
    9.10  apply (simp add: setsum_diff [symmetric])
    9.11  done
    10.1 --- a/src/HOL/Hyperreal/Star.thy	Sat Sep 16 02:35:58 2006 +0200
    10.2 +++ b/src/HOL/Hyperreal/Star.thy	Sat Sep 16 02:40:00 2006 +0200
    10.3 @@ -38,7 +38,7 @@
    10.4     referee for the JCM Paper: let f(x) be least y such
    10.5     that  Q(x,y)
    10.6  *)
    10.7 -lemma no_choice: "\<forall>x. \<exists>y. Q x y ==> \<exists>(f :: nat => nat). \<forall>x. Q x (f x)"
    10.8 +lemma no_choice: "\<forall>x. \<exists>y. Q x y ==> \<exists>(f :: 'a => nat). \<forall>x. Q x (f x)"
    10.9  apply (rule_tac x = "%x. LEAST y. Q x y" in exI)
   10.10  apply (blast intro: LeastI)
   10.11  done
   10.12 @@ -146,11 +146,6 @@
   10.13  apply (simp add: Ifun_star_n star_n_eq_iff)
   10.14  done
   10.15  
   10.16 -lemma Rep_star_FreeUltrafilterNat:
   10.17 -     "[| X \<in> Rep_star z; Y \<in> Rep_star z |]
   10.18 -      ==> {n. X n = Y n} : FreeUltrafilterNat"
   10.19 -by (rule FreeUltrafilterNat_Rep_hypreal)
   10.20 -
   10.21  text{*Nonstandard extension of functions*}
   10.22  
   10.23  lemma starfun:
   10.24 @@ -213,7 +208,7 @@
   10.25  
   10.26  (* this is trivial, given starfun_Id *)
   10.27  lemma starfun_Idfun_approx:
   10.28 -  "x @= hypreal_of_real a ==> ( *f* (%x. x)) x @= hypreal_of_real a"
   10.29 +  "x @= star_of a ==> ( *f* (%x. x)) x @= star_of a"
   10.30  by (simp only: starfun_Id)
   10.31  
   10.32  text{*The Star-function is a (nonstandard) extension of the function*}
   10.33 @@ -243,10 +238,10 @@
   10.34  text{*extented function has same solution as its standard
   10.35     version for real arguments. i.e they are the same
   10.36     for all real arguments*}
   10.37 -lemma starfun_eq [simp]: "( *f* f) (star_of a) = star_of (f a)"
   10.38 -by (transfer, rule refl)
   10.39 +lemma starfun_eq: "( *f* f) (star_of a) = star_of (f a)"
   10.40 +by (rule starfun_star_of)
   10.41  
   10.42 -lemma starfun_approx: "( *f* f) (star_of a) @= hypreal_of_real (f a)"
   10.43 +lemma starfun_approx: "( *f* f) (star_of a) @= star_of (f a)"
   10.44  by simp
   10.45  
   10.46  (* useful for NS definition of derivatives *)
   10.47 @@ -258,7 +253,9 @@
   10.48    "( *f* (%h. f(g(x + h)))) x' = ( *f* (f o g)) (star_of x + x')"
   10.49  by (unfold o_def, rule starfun_lambda_cancel)
   10.50  
   10.51 -lemma starfun_mult_HFinite_approx: "[| ( *f* f) x @= l; ( *f* g) x @= m;
   10.52 +lemma starfun_mult_HFinite_approx:
   10.53 +  fixes l m :: "'a::real_normed_algebra star"
   10.54 +  shows "[| ( *f* f) x @= l; ( *f* g) x @= m;
   10.55                    l: HFinite; m: HFinite
   10.56                 |] ==>  ( *f* (%x. f x * g x)) x @= l * m"
   10.57  apply (drule (3) approx_mult_HFinite)
   10.58 @@ -277,10 +274,10 @@
   10.59  (* use the theorem we proved above instead          *)
   10.60  
   10.61  lemma starfun_rabs_hrabs: "*f* abs = abs"
   10.62 -by (rule hrabs_is_starext_rabs [THEN is_starext_starfun_iff [THEN iffD1], symmetric])
   10.63 +by (simp only: star_abs_def)
   10.64  
   10.65  lemma starfun_inverse_inverse [simp]: "( *f* inverse) x = inverse(x)"
   10.66 -by (unfold star_inverse_def, rule refl)
   10.67 +by (simp only: star_inverse_def)
   10.68  
   10.69  lemma starfun_inverse: "!!x. inverse (( *f* f) x) = ( *f* (%x. inverse (f x))) x"
   10.70  by (transfer, rule refl)
   10.71 @@ -312,36 +309,40 @@
   10.72     by its NS extenson. See second NS set extension below.*}
   10.73  lemma STAR_rabs_add_minus:
   10.74     "*s* {x. abs (x + - y) < r} =
   10.75 -     {x. abs(x + -hypreal_of_real y) < hypreal_of_real r}"
   10.76 +     {x. abs(x + -star_of y) < star_of r}"
   10.77  by (transfer, rule refl)
   10.78  
   10.79  lemma STAR_starfun_rabs_add_minus:
   10.80    "*s* {x. abs (f x + - y) < r} =
   10.81 -       {x. abs(( *f* f) x + -hypreal_of_real y) < hypreal_of_real r}"
   10.82 +       {x. abs(( *f* f) x + -star_of y) < star_of r}"
   10.83  by (transfer, rule refl)
   10.84  
   10.85  text{*Another characterization of Infinitesimal and one of @= relation.
   10.86     In this theory since @{text hypreal_hrabs} proved here. Maybe
   10.87     move both theorems??*}
   10.88  lemma Infinitesimal_FreeUltrafilterNat_iff2:
   10.89 -     "(x \<in> Infinitesimal) =
   10.90 -      (\<exists>X \<in> Rep_star(x).
   10.91 -        \<forall>m. {n. abs(X n) < inverse(real(Suc m))}
   10.92 +     "(star_n X \<in> Infinitesimal) =
   10.93 +      (\<forall>m. {n. norm(X n) < inverse(real(Suc m))}
   10.94                  \<in>  FreeUltrafilterNat)"
   10.95 -apply (cases x)
   10.96 -apply (auto intro!: bexI lemma_starrel_refl 
   10.97 -            simp add: Infinitesimal_hypreal_of_nat_iff star_of_def
   10.98 -     star_n_inverse star_n_abs star_n_less hypreal_of_nat_eq)
   10.99 -apply (drule_tac x = n in spec, ultra)
  10.100 +by (simp add: Infinitesimal_hypreal_of_nat_iff star_of_def
  10.101 +     hnorm_def star_of_nat_def starfun_star_n
  10.102 +     star_n_inverse star_n_less hypreal_of_nat_eq)
  10.103 +
  10.104 +lemma approx_FreeUltrafilterNat_iff: "star_n X @= star_n Y =
  10.105 +      (\<forall>r>0. {n. norm (X n + - Y n) < r} : FreeUltrafilterNat)"
  10.106 +apply (subst approx_minus_iff)
  10.107 +apply (rule mem_infmal_iff [THEN subst])
  10.108 +apply (simp add: star_n_minus star_n_add)
  10.109 +apply (simp add: Infinitesimal_FreeUltrafilterNat_iff)
  10.110  done
  10.111  
  10.112 -lemma approx_FreeUltrafilterNat_iff: "star_n X @= star_n Y =
  10.113 -      (\<forall>m. {n. abs (X n + - Y n) <
  10.114 +lemma approx_FreeUltrafilterNat_iff2: "star_n X @= star_n Y =
  10.115 +      (\<forall>m. {n. norm (X n + - Y n) <
  10.116                    inverse(real(Suc m))} : FreeUltrafilterNat)"
  10.117  apply (subst approx_minus_iff)
  10.118  apply (rule mem_infmal_iff [THEN subst])
  10.119 -apply (auto simp add: star_n_minus star_n_add Infinitesimal_FreeUltrafilterNat_iff2)
  10.120 -apply (drule_tac x = m in spec, ultra)
  10.121 +apply (simp add: star_n_minus star_n_add)
  10.122 +apply (simp add: Infinitesimal_FreeUltrafilterNat_iff2)
  10.123  done
  10.124  
  10.125  lemma inj_starfun: "inj starfun"
    11.1 --- a/src/HOL/Hyperreal/Transcendental.thy	Sat Sep 16 02:35:58 2006 +0200
    11.2 +++ b/src/HOL/Hyperreal/Transcendental.thy	Sat Sep 16 02:40:00 2006 +0200
    11.3 @@ -2540,7 +2540,8 @@
    11.4  done
    11.5  
    11.6  lemma isCont_inv_fun_inv:
    11.7 -     "[| 0 < d;  
    11.8 +  fixes f g :: "real \<Rightarrow> real"
    11.9 +  shows "[| 0 < d;  
   11.10           \<forall>z. \<bar>z - x\<bar> \<le> d --> g(f(z)) = z;  
   11.11           \<forall>z. \<bar>z - x\<bar> \<le> d --> isCont f z |]  
   11.12         ==> \<exists>e. 0 < e &  
   11.13 @@ -2555,7 +2556,7 @@
   11.14  
   11.15  text{*Bartle/Sherbert: Introduction to Real Analysis, Theorem 4.2.9, p. 110*}
   11.16  lemma LIM_fun_gt_zero:
   11.17 -     "[| f -- c --> l; 0 < l |]  
   11.18 +     "[| f -- c --> (l::real); 0 < l |]  
   11.19           ==> \<exists>r. 0 < r & (\<forall>x. x \<noteq> c & \<bar>c - x\<bar> < r --> 0 < f x)"
   11.20  apply (auto simp add: LIM_def)
   11.21  apply (drule_tac x = "l/2" in spec, safe, force)
   11.22 @@ -2564,7 +2565,7 @@
   11.23  done
   11.24  
   11.25  lemma LIM_fun_less_zero:
   11.26 -     "[| f -- c --> l; l < 0 |]  
   11.27 +     "[| f -- c --> (l::real); l < 0 |]  
   11.28        ==> \<exists>r. 0 < r & (\<forall>x. x \<noteq> c & \<bar>c - x\<bar> < r --> f x < 0)"
   11.29  apply (auto simp add: LIM_def)
   11.30  apply (drule_tac x = "-l/2" in spec, safe, force)
   11.31 @@ -2574,7 +2575,7 @@
   11.32  
   11.33  
   11.34  lemma LIM_fun_not_zero:
   11.35 -     "[| f -- c --> l; l \<noteq> 0 |] 
   11.36 +     "[| f -- c --> (l::real); l \<noteq> 0 |] 
   11.37        ==> \<exists>r. 0 < r & (\<forall>x. x \<noteq> c & \<bar>c - x\<bar> < r --> f x \<noteq> 0)"
   11.38  apply (cut_tac x = l and y = 0 in linorder_less_linear, auto)
   11.39  apply (drule LIM_fun_less_zero)