more symbols;
authorwenzelm
Tue Dec 29 23:20:11 2015 +0100 (2015-12-29)
changeset 619706226261144d7
parent 61969 e01015e49041
child 61971 720fa884656e
more symbols;
NEWS
etc/abbrevs
src/HOL/NSA/HSEQ.thy
src/HOL/NSA/HSeries.thy
src/HOL/NSA/HTranscendental.thy
     1.1 --- a/NEWS	Tue Dec 29 23:04:53 2015 +0100
     1.2 +++ b/NEWS	Tue Dec 29 23:20:11 2015 +0100
     1.3 @@ -504,6 +504,8 @@
     1.4  
     1.5    notation (in topological_space) LIMSEQ ("((_)/ ----> (_))" [60, 60] 60)
     1.6  
     1.7 +  notation NSLIMSEQ ("((_)/ ----NS> (_))" [60, 60] 60)
     1.8 +
     1.9  * The alternative notation "\<Colon>" for type and sort constraints has been
    1.10  removed: in LaTeX document output it looks the same as "::".
    1.11  INCOMPATIBILITY, use plain "::" instead.
     2.1 --- a/etc/abbrevs	Tue Dec 29 23:04:53 2015 +0100
     2.2 +++ b/etc/abbrevs	Tue Dec 29 23:20:11 2015 +0100
     2.3 @@ -5,3 +5,6 @@
     2.4  "---->" = "---->"
     2.5  "----->" = "----->"
     2.6  "===>" = "===>"
     2.7 +
     2.8 +(*HOL-NSA*)
     2.9 +"---->" = "\<longlonglongrightarrow>\<^sub>N\<^sub>S"
     3.1 --- a/src/HOL/NSA/HSEQ.thy	Tue Dec 29 23:04:53 2015 +0100
     3.2 +++ b/src/HOL/NSA/HSEQ.thy	Tue Dec 29 23:20:11 2015 +0100
     3.3 @@ -14,19 +14,19 @@
     3.4  
     3.5  definition
     3.6    NSLIMSEQ :: "[nat => 'a::real_normed_vector, 'a] => bool"
     3.7 -    ("((_)/ ----NS> (_))" [60, 60] 60) where
     3.8 +    ("((_)/ \<longlonglongrightarrow>\<^sub>N\<^sub>S (_))" [60, 60] 60) where
     3.9      --{*Nonstandard definition of convergence of sequence*}
    3.10 -  "X ----NS> L = (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> star_of L)"
    3.11 +  "X \<longlonglongrightarrow>\<^sub>N\<^sub>S L = (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> star_of L)"
    3.12  
    3.13  definition
    3.14    nslim :: "(nat => 'a::real_normed_vector) => 'a" where
    3.15      --{*Nonstandard definition of limit using choice operator*}
    3.16 -  "nslim X = (THE L. X ----NS> L)"
    3.17 +  "nslim X = (THE L. X \<longlonglongrightarrow>\<^sub>N\<^sub>S L)"
    3.18  
    3.19  definition
    3.20    NSconvergent :: "(nat => 'a::real_normed_vector) => bool" where
    3.21      --{*Nonstandard definition of convergence*}
    3.22 -  "NSconvergent X = (\<exists>L. X ----NS> L)"
    3.23 +  "NSconvergent X = (\<exists>L. X \<longlonglongrightarrow>\<^sub>N\<^sub>S L)"
    3.24  
    3.25  definition
    3.26    NSBseq :: "(nat => 'a::real_normed_vector) => bool" where
    3.27 @@ -41,69 +41,69 @@
    3.28  subsection {* Limits of Sequences *}
    3.29  
    3.30  lemma NSLIMSEQ_iff:
    3.31 -    "(X ----NS> L) = (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> star_of L)"
    3.32 +    "(X \<longlonglongrightarrow>\<^sub>N\<^sub>S L) = (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> star_of L)"
    3.33  by (simp add: NSLIMSEQ_def)
    3.34  
    3.35  lemma NSLIMSEQ_I:
    3.36 -  "(\<And>N. N \<in> HNatInfinite \<Longrightarrow> starfun X N \<approx> star_of L) \<Longrightarrow> X ----NS> L"
    3.37 +  "(\<And>N. N \<in> HNatInfinite \<Longrightarrow> starfun X N \<approx> star_of L) \<Longrightarrow> X \<longlonglongrightarrow>\<^sub>N\<^sub>S L"
    3.38  by (simp add: NSLIMSEQ_def)
    3.39  
    3.40  lemma NSLIMSEQ_D:
    3.41 -  "\<lbrakk>X ----NS> L; N \<in> HNatInfinite\<rbrakk> \<Longrightarrow> starfun X N \<approx> star_of L"
    3.42 +  "\<lbrakk>X \<longlonglongrightarrow>\<^sub>N\<^sub>S L; N \<in> HNatInfinite\<rbrakk> \<Longrightarrow> starfun X N \<approx> star_of L"
    3.43  by (simp add: NSLIMSEQ_def)
    3.44  
    3.45 -lemma NSLIMSEQ_const: "(%n. k) ----NS> k"
    3.46 +lemma NSLIMSEQ_const: "(%n. k) \<longlonglongrightarrow>\<^sub>N\<^sub>S k"
    3.47  by (simp add: NSLIMSEQ_def)
    3.48  
    3.49  lemma NSLIMSEQ_add:
    3.50 -      "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n + Y n) ----NS> a + b"
    3.51 +      "[| X \<longlonglongrightarrow>\<^sub>N\<^sub>S a; Y \<longlonglongrightarrow>\<^sub>N\<^sub>S b |] ==> (%n. X n + Y n) \<longlonglongrightarrow>\<^sub>N\<^sub>S a + b"
    3.52  by (auto intro: approx_add simp add: NSLIMSEQ_def starfun_add [symmetric])
    3.53  
    3.54 -lemma NSLIMSEQ_add_const: "f ----NS> a ==> (%n.(f n + b)) ----NS> a + b"
    3.55 +lemma NSLIMSEQ_add_const: "f \<longlonglongrightarrow>\<^sub>N\<^sub>S a ==> (%n.(f n + b)) \<longlonglongrightarrow>\<^sub>N\<^sub>S a + b"
    3.56  by (simp only: NSLIMSEQ_add NSLIMSEQ_const)
    3.57  
    3.58  lemma NSLIMSEQ_mult:
    3.59    fixes a b :: "'a::real_normed_algebra"
    3.60 -  shows "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n * Y n) ----NS> a * b"
    3.61 +  shows "[| X \<longlonglongrightarrow>\<^sub>N\<^sub>S a; Y \<longlonglongrightarrow>\<^sub>N\<^sub>S b |] ==> (%n. X n * Y n) \<longlonglongrightarrow>\<^sub>N\<^sub>S a * b"
    3.62  by (auto intro!: approx_mult_HFinite simp add: NSLIMSEQ_def)
    3.63  
    3.64 -lemma NSLIMSEQ_minus: "X ----NS> a ==> (%n. -(X n)) ----NS> -a"
    3.65 +lemma NSLIMSEQ_minus: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S a ==> (%n. -(X n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S -a"
    3.66  by (auto simp add: NSLIMSEQ_def)
    3.67  
    3.68 -lemma NSLIMSEQ_minus_cancel: "(%n. -(X n)) ----NS> -a ==> X ----NS> a"
    3.69 +lemma NSLIMSEQ_minus_cancel: "(%n. -(X n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S -a ==> X \<longlonglongrightarrow>\<^sub>N\<^sub>S a"
    3.70  by (drule NSLIMSEQ_minus, simp)
    3.71  
    3.72  lemma NSLIMSEQ_diff:
    3.73 -     "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n - Y n) ----NS> a - b"
    3.74 +     "[| X \<longlonglongrightarrow>\<^sub>N\<^sub>S a; Y \<longlonglongrightarrow>\<^sub>N\<^sub>S b |] ==> (%n. X n - Y n) \<longlonglongrightarrow>\<^sub>N\<^sub>S a - b"
    3.75    using NSLIMSEQ_add [of X a "- Y" "- b"] by (simp add: NSLIMSEQ_minus fun_Compl_def)
    3.76  
    3.77  (* FIXME: delete *)
    3.78  lemma NSLIMSEQ_add_minus:
    3.79 -     "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n + -Y n) ----NS> a + -b"
    3.80 +     "[| X \<longlonglongrightarrow>\<^sub>N\<^sub>S a; Y \<longlonglongrightarrow>\<^sub>N\<^sub>S b |] ==> (%n. X n + -Y n) \<longlonglongrightarrow>\<^sub>N\<^sub>S a + -b"
    3.81    by (simp add: NSLIMSEQ_diff)
    3.82  
    3.83 -lemma NSLIMSEQ_diff_const: "f ----NS> a ==> (%n.(f n - b)) ----NS> a - b"
    3.84 +lemma NSLIMSEQ_diff_const: "f \<longlonglongrightarrow>\<^sub>N\<^sub>S a ==> (%n.(f n - b)) \<longlonglongrightarrow>\<^sub>N\<^sub>S a - b"
    3.85  by (simp add: NSLIMSEQ_diff NSLIMSEQ_const)
    3.86  
    3.87  lemma NSLIMSEQ_inverse:
    3.88    fixes a :: "'a::real_normed_div_algebra"
    3.89 -  shows "[| X ----NS> a;  a ~= 0 |] ==> (%n. inverse(X n)) ----NS> inverse(a)"
    3.90 +  shows "[| X \<longlonglongrightarrow>\<^sub>N\<^sub>S a;  a ~= 0 |] ==> (%n. inverse(X n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S inverse(a)"
    3.91  by (simp add: NSLIMSEQ_def star_of_approx_inverse)
    3.92  
    3.93  lemma NSLIMSEQ_mult_inverse:
    3.94    fixes a b :: "'a::real_normed_field"
    3.95    shows
    3.96 -     "[| X ----NS> a;  Y ----NS> b;  b ~= 0 |] ==> (%n. X n / Y n) ----NS> a/b"
    3.97 +     "[| X \<longlonglongrightarrow>\<^sub>N\<^sub>S a;  Y \<longlonglongrightarrow>\<^sub>N\<^sub>S b;  b ~= 0 |] ==> (%n. X n / Y n) \<longlonglongrightarrow>\<^sub>N\<^sub>S a/b"
    3.98  by (simp add: NSLIMSEQ_mult NSLIMSEQ_inverse divide_inverse)
    3.99  
   3.100  lemma starfun_hnorm: "\<And>x. hnorm (( *f* f) x) = ( *f* (\<lambda>x. norm (f x))) x"
   3.101  by transfer simp
   3.102  
   3.103 -lemma NSLIMSEQ_norm: "X ----NS> a \<Longrightarrow> (\<lambda>n. norm (X n)) ----NS> norm a"
   3.104 +lemma NSLIMSEQ_norm: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S a \<Longrightarrow> (\<lambda>n. norm (X n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S norm a"
   3.105  by (simp add: NSLIMSEQ_def starfun_hnorm [symmetric] approx_hnorm)
   3.106  
   3.107  text{*Uniqueness of limit*}
   3.108 -lemma NSLIMSEQ_unique: "[| X ----NS> a; X ----NS> b |] ==> a = b"
   3.109 +lemma NSLIMSEQ_unique: "[| X \<longlonglongrightarrow>\<^sub>N\<^sub>S a; X \<longlonglongrightarrow>\<^sub>N\<^sub>S b |] ==> a = b"
   3.110  apply (simp add: NSLIMSEQ_def)
   3.111  apply (drule HNatInfinite_whn [THEN [2] bspec])+
   3.112  apply (auto dest: approx_trans3)
   3.113 @@ -111,7 +111,7 @@
   3.114  
   3.115  lemma NSLIMSEQ_pow [rule_format]:
   3.116    fixes a :: "'a::{real_normed_algebra,power}"
   3.117 -  shows "(X ----NS> a) --> ((%n. (X n) ^ m) ----NS> a ^ m)"
   3.118 +  shows "(X \<longlonglongrightarrow>\<^sub>N\<^sub>S a) --> ((%n. (X n) ^ m) \<longlonglongrightarrow>\<^sub>N\<^sub>S a ^ m)"
   3.119  apply (induct "m")
   3.120  apply (auto simp add: power_Suc intro: NSLIMSEQ_mult NSLIMSEQ_const)
   3.121  done
   3.122 @@ -120,7 +120,7 @@
   3.123       starting with the limit comparison property for sequences.*}
   3.124  
   3.125  lemma NSLIMSEQ_le:
   3.126 -       "[| f ----NS> l; g ----NS> m;
   3.127 +       "[| f \<longlonglongrightarrow>\<^sub>N\<^sub>S l; g \<longlonglongrightarrow>\<^sub>N\<^sub>S m;
   3.128             \<exists>N. \<forall>n \<ge> N. f(n) \<le> g(n)
   3.129          |] ==> l \<le> (m::real)"
   3.130  apply (simp add: NSLIMSEQ_def, safe)
   3.131 @@ -132,37 +132,37 @@
   3.132  apply (auto intro: hypreal_of_real_le_add_Infininitesimal_cancel2)
   3.133  done
   3.134  
   3.135 -lemma NSLIMSEQ_le_const: "[| X ----NS> (r::real); \<forall>n. a \<le> X n |] ==> a \<le> r"
   3.136 +lemma NSLIMSEQ_le_const: "[| X \<longlonglongrightarrow>\<^sub>N\<^sub>S (r::real); \<forall>n. a \<le> X n |] ==> a \<le> r"
   3.137  by (erule NSLIMSEQ_le [OF NSLIMSEQ_const], auto)
   3.138  
   3.139 -lemma NSLIMSEQ_le_const2: "[| X ----NS> (r::real); \<forall>n. X n \<le> a |] ==> r \<le> a"
   3.140 +lemma NSLIMSEQ_le_const2: "[| X \<longlonglongrightarrow>\<^sub>N\<^sub>S (r::real); \<forall>n. X n \<le> a |] ==> r \<le> a"
   3.141  by (erule NSLIMSEQ_le [OF _ NSLIMSEQ_const], auto)
   3.142  
   3.143  text{*Shift a convergent series by 1:
   3.144    By the equivalence between Cauchiness and convergence and because
   3.145    the successor of an infinite hypernatural is also infinite.*}
   3.146  
   3.147 -lemma NSLIMSEQ_Suc: "f ----NS> l ==> (%n. f(Suc n)) ----NS> l"
   3.148 +lemma NSLIMSEQ_Suc: "f \<longlonglongrightarrow>\<^sub>N\<^sub>S l ==> (%n. f(Suc n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S l"
   3.149  apply (unfold NSLIMSEQ_def, safe)
   3.150  apply (drule_tac x="N + 1" in bspec)
   3.151  apply (erule HNatInfinite_add)
   3.152  apply (simp add: starfun_shift_one)
   3.153  done
   3.154  
   3.155 -lemma NSLIMSEQ_imp_Suc: "(%n. f(Suc n)) ----NS> l ==> f ----NS> l"
   3.156 +lemma NSLIMSEQ_imp_Suc: "(%n. f(Suc n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S l ==> f \<longlonglongrightarrow>\<^sub>N\<^sub>S l"
   3.157  apply (unfold NSLIMSEQ_def, safe)
   3.158  apply (drule_tac x="N - 1" in bspec) 
   3.159  apply (erule Nats_1 [THEN [2] HNatInfinite_diff])
   3.160  apply (simp add: starfun_shift_one one_le_HNatInfinite)
   3.161  done
   3.162  
   3.163 -lemma NSLIMSEQ_Suc_iff: "((%n. f(Suc n)) ----NS> l) = (f ----NS> l)"
   3.164 +lemma NSLIMSEQ_Suc_iff: "((%n. f(Suc n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S l) = (f \<longlonglongrightarrow>\<^sub>N\<^sub>S l)"
   3.165  by (blast intro: NSLIMSEQ_imp_Suc NSLIMSEQ_Suc)
   3.166  
   3.167  subsubsection {* Equivalence of @{term LIMSEQ} and @{term NSLIMSEQ} *}
   3.168  
   3.169  lemma LIMSEQ_NSLIMSEQ:
   3.170 -  assumes X: "X \<longlonglongrightarrow> L" shows "X ----NS> L"
   3.171 +  assumes X: "X \<longlonglongrightarrow> L" shows "X \<longlonglongrightarrow>\<^sub>N\<^sub>S L"
   3.172  proof (rule NSLIMSEQ_I)
   3.173    fix N assume N: "N \<in> HNatInfinite"
   3.174    have "starfun X N - star_of L \<in> Infinitesimal"
   3.175 @@ -180,7 +180,7 @@
   3.176  qed
   3.177  
   3.178  lemma NSLIMSEQ_LIMSEQ:
   3.179 -  assumes X: "X ----NS> L" shows "X \<longlonglongrightarrow> L"
   3.180 +  assumes X: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S L" shows "X \<longlonglongrightarrow> L"
   3.181  proof (rule LIMSEQ_I)
   3.182    fix r::real assume r: "0 < r"
   3.183    have "\<exists>no. \<forall>n\<ge>no. hnorm (starfun X n - star_of L) < star_of r"
   3.184 @@ -199,21 +199,21 @@
   3.185      by transfer
   3.186  qed
   3.187  
   3.188 -theorem LIMSEQ_NSLIMSEQ_iff: "(f \<longlonglongrightarrow> L) = (f ----NS> L)"
   3.189 +theorem LIMSEQ_NSLIMSEQ_iff: "(f \<longlonglongrightarrow> L) = (f \<longlonglongrightarrow>\<^sub>N\<^sub>S L)"
   3.190  by (blast intro: LIMSEQ_NSLIMSEQ NSLIMSEQ_LIMSEQ)
   3.191  
   3.192  subsubsection {* Derived theorems about @{term NSLIMSEQ} *}
   3.193  
   3.194  text{*We prove the NS version from the standard one, since the NS proof
   3.195     seems more complicated than the standard one above!*}
   3.196 -lemma NSLIMSEQ_norm_zero: "((\<lambda>n. norm (X n)) ----NS> 0) = (X ----NS> 0)"
   3.197 +lemma NSLIMSEQ_norm_zero: "((\<lambda>n. norm (X n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0) = (X \<longlonglongrightarrow>\<^sub>N\<^sub>S 0)"
   3.198  by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] tendsto_norm_zero_iff)
   3.199  
   3.200 -lemma NSLIMSEQ_rabs_zero: "((%n. \<bar>f n\<bar>) ----NS> 0) = (f ----NS> (0::real))"
   3.201 +lemma NSLIMSEQ_rabs_zero: "((%n. \<bar>f n\<bar>) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0) = (f \<longlonglongrightarrow>\<^sub>N\<^sub>S (0::real))"
   3.202  by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] tendsto_rabs_zero_iff)
   3.203  
   3.204  text{*Generalization to other limits*}
   3.205 -lemma NSLIMSEQ_imp_rabs: "f ----NS> (l::real) ==> (%n. \<bar>f n\<bar>) ----NS> \<bar>l\<bar>"
   3.206 +lemma NSLIMSEQ_imp_rabs: "f \<longlonglongrightarrow>\<^sub>N\<^sub>S (l::real) ==> (%n. \<bar>f n\<bar>) \<longlonglongrightarrow>\<^sub>N\<^sub>S \<bar>l\<bar>"
   3.207  apply (simp add: NSLIMSEQ_def)
   3.208  apply (auto intro: approx_hrabs 
   3.209              simp add: starfun_abs)
   3.210 @@ -221,28 +221,28 @@
   3.211  
   3.212  lemma NSLIMSEQ_inverse_zero:
   3.213       "\<forall>y::real. \<exists>N. \<forall>n \<ge> N. y < f(n)
   3.214 -      ==> (%n. inverse(f n)) ----NS> 0"
   3.215 +      ==> (%n. inverse(f n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0"
   3.216  by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_zero)
   3.217  
   3.218 -lemma NSLIMSEQ_inverse_real_of_nat: "(%n. inverse(real(Suc n))) ----NS> 0"
   3.219 +lemma NSLIMSEQ_inverse_real_of_nat: "(%n. inverse(real(Suc n))) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0"
   3.220  by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat del: of_nat_Suc)
   3.221  
   3.222  lemma NSLIMSEQ_inverse_real_of_nat_add:
   3.223 -     "(%n. r + inverse(real(Suc n))) ----NS> r"
   3.224 +     "(%n. r + inverse(real(Suc n))) \<longlonglongrightarrow>\<^sub>N\<^sub>S r"
   3.225  by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat_add del: of_nat_Suc)
   3.226  
   3.227  lemma NSLIMSEQ_inverse_real_of_nat_add_minus:
   3.228 -     "(%n. r + -inverse(real(Suc n))) ----NS> r"
   3.229 +     "(%n. r + -inverse(real(Suc n))) \<longlonglongrightarrow>\<^sub>N\<^sub>S r"
   3.230    using LIMSEQ_inverse_real_of_nat_add_minus by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric])
   3.231  
   3.232  lemma NSLIMSEQ_inverse_real_of_nat_add_minus_mult:
   3.233 -     "(%n. r*( 1 + -inverse(real(Suc n)))) ----NS> r"
   3.234 +     "(%n. r*( 1 + -inverse(real(Suc n)))) \<longlonglongrightarrow>\<^sub>N\<^sub>S r"
   3.235    using LIMSEQ_inverse_real_of_nat_add_minus_mult by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric])
   3.236  
   3.237  
   3.238  subsection {* Convergence *}
   3.239  
   3.240 -lemma nslimI: "X ----NS> L ==> nslim X = L"
   3.241 +lemma nslimI: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S L ==> nslim X = L"
   3.242  apply (simp add: nslim_def)
   3.243  apply (blast intro: NSLIMSEQ_unique)
   3.244  done
   3.245 @@ -250,16 +250,16 @@
   3.246  lemma lim_nslim_iff: "lim X = nslim X"
   3.247  by (simp add: lim_def nslim_def LIMSEQ_NSLIMSEQ_iff)
   3.248  
   3.249 -lemma NSconvergentD: "NSconvergent X ==> \<exists>L. (X ----NS> L)"
   3.250 +lemma NSconvergentD: "NSconvergent X ==> \<exists>L. (X \<longlonglongrightarrow>\<^sub>N\<^sub>S L)"
   3.251  by (simp add: NSconvergent_def)
   3.252  
   3.253 -lemma NSconvergentI: "(X ----NS> L) ==> NSconvergent X"
   3.254 +lemma NSconvergentI: "(X \<longlonglongrightarrow>\<^sub>N\<^sub>S L) ==> NSconvergent X"
   3.255  by (auto simp add: NSconvergent_def)
   3.256  
   3.257  lemma convergent_NSconvergent_iff: "convergent X = NSconvergent X"
   3.258  by (simp add: convergent_def NSconvergent_def LIMSEQ_NSLIMSEQ_iff)
   3.259  
   3.260 -lemma NSconvergent_NSLIMSEQ_iff: "NSconvergent X = (X ----NS> nslim X)"
   3.261 +lemma NSconvergent_NSLIMSEQ_iff: "NSconvergent X = (X \<longlonglongrightarrow>\<^sub>N\<^sub>S nslim X)"
   3.262  by (auto intro: theI NSLIMSEQ_unique simp add: NSconvergent_def nslim_def)
   3.263  
   3.264  
   3.265 @@ -360,7 +360,7 @@
   3.266     theorem and then use equivalence to "transfer" it into the
   3.267     equivalent nonstandard form if needed!*}
   3.268  
   3.269 -lemma Bmonoseq_NSLIMSEQ: "\<forall>n \<ge> m. X n = X m ==> \<exists>L. (X ----NS> L)"
   3.270 +lemma Bmonoseq_NSLIMSEQ: "\<forall>n \<ge> m. X n = X m ==> \<exists>L. (X \<longlonglongrightarrow>\<^sub>N\<^sub>S L)"
   3.271  by (auto dest!: Bmonoseq_LIMSEQ simp add: LIMSEQ_NSLIMSEQ_iff)
   3.272  
   3.273  lemma NSBseq_mono_NSconvergent:
   3.274 @@ -488,7 +488,7 @@
   3.275  text{* We now use NS criterion to bring proof of theorem through *}
   3.276  
   3.277  lemma NSLIMSEQ_realpow_zero:
   3.278 -  "[| 0 \<le> (x::real); x < 1 |] ==> (%n. x ^ n) ----NS> 0"
   3.279 +  "[| 0 \<le> (x::real); x < 1 |] ==> (%n. x ^ n) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0"
   3.280  apply (simp add: NSLIMSEQ_def)
   3.281  apply (auto dest!: convergent_realpow simp add: convergent_NSconvergent_iff)
   3.282  apply (frule NSconvergentD)
   3.283 @@ -503,10 +503,10 @@
   3.284  apply (auto simp del: star_of_mult simp add: star_of_mult [symmetric])
   3.285  done
   3.286  
   3.287 -lemma NSLIMSEQ_rabs_realpow_zero: "\<bar>c\<bar> < (1::real) ==> (%n. \<bar>c\<bar> ^ n) ----NS> 0"
   3.288 +lemma NSLIMSEQ_rabs_realpow_zero: "\<bar>c\<bar> < (1::real) ==> (%n. \<bar>c\<bar> ^ n) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0"
   3.289  by (simp add: LIMSEQ_rabs_realpow_zero LIMSEQ_NSLIMSEQ_iff [symmetric])
   3.290  
   3.291 -lemma NSLIMSEQ_rabs_realpow_zero2: "\<bar>c\<bar> < (1::real) ==> (%n. c ^ n) ----NS> 0"
   3.292 +lemma NSLIMSEQ_rabs_realpow_zero2: "\<bar>c\<bar> < (1::real) ==> (%n. c ^ n) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0"
   3.293  by (simp add: LIMSEQ_rabs_realpow_zero2 LIMSEQ_NSLIMSEQ_iff [symmetric])
   3.294  
   3.295  (***---------------------------------------------------------------
     4.1 --- a/src/HOL/NSA/HSeries.thy	Tue Dec 29 23:04:53 2015 +0100
     4.2 +++ b/src/HOL/NSA/HSeries.thy	Tue Dec 29 23:20:11 2015 +0100
     4.3 @@ -18,7 +18,7 @@
     4.4  
     4.5  definition
     4.6    NSsums  :: "[nat=>real,real] => bool"     (infixr "NSsums" 80) where
     4.7 -  "f NSsums s = (%n. setsum f {..<n}) ----NS> s"
     4.8 +  "f NSsums s = (%n. setsum f {..<n}) \<longlonglongrightarrow>\<^sub>N\<^sub>S s"
     4.9  
    4.10  definition
    4.11    NSsummable :: "(nat=>real) => bool" where
    4.12 @@ -180,7 +180,7 @@
    4.13  done
    4.14  
    4.15  text{*Terms of a convergent series tend to zero*}
    4.16 -lemma NSsummable_NSLIMSEQ_zero: "NSsummable f ==> f ----NS> 0"
    4.17 +lemma NSsummable_NSLIMSEQ_zero: "NSsummable f ==> f \<longlonglongrightarrow>\<^sub>N\<^sub>S 0"
    4.18  apply (auto simp add: NSLIMSEQ_def NSsummable_NSCauchy)
    4.19  apply (drule bspec, auto)
    4.20  apply (drule_tac x = "N + 1 " in bspec)
     5.1 --- a/src/HOL/NSA/HTranscendental.thy	Tue Dec 29 23:04:53 2015 +0100
     5.2 +++ b/src/HOL/NSA/HTranscendental.thy	Tue Dec 29 23:20:11 2015 +0100
     5.3 @@ -569,7 +569,7 @@
     5.4  apply simp
     5.5  done
     5.6  
     5.7 -lemma NSLIMSEQ_sin_pi: "(%n. real n * sin (pi / real n)) ----NS> pi"
     5.8 +lemma NSLIMSEQ_sin_pi: "(%n. real n * sin (pi / real n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S pi"
     5.9  apply (auto simp add: NSLIMSEQ_def starfun_mult [symmetric] starfunNat_real_of_nat)
    5.10  apply (rule_tac f1 = sin in starfun_o2 [THEN subst])
    5.11  apply (auto simp add: starfun_mult [symmetric] starfunNat_real_of_nat divide_inverse)
    5.12 @@ -578,7 +578,7 @@
    5.13              simp add: starfunNat_real_of_nat mult.commute divide_inverse)
    5.14  done
    5.15  
    5.16 -lemma NSLIMSEQ_cos_one: "(%n. cos (pi / real n))----NS> 1"
    5.17 +lemma NSLIMSEQ_cos_one: "(%n. cos (pi / real n))\<longlonglongrightarrow>\<^sub>N\<^sub>S 1"
    5.18  apply (simp add: NSLIMSEQ_def, auto)
    5.19  apply (rule_tac f1 = cos in starfun_o2 [THEN subst])
    5.20  apply (rule STAR_cos_Infinitesimal)
    5.21 @@ -588,7 +588,7 @@
    5.22  done
    5.23  
    5.24  lemma NSLIMSEQ_sin_cos_pi:
    5.25 -     "(%n. real n * sin (pi / real n) * cos (pi / real n)) ----NS> pi"
    5.26 +     "(%n. real n * sin (pi / real n) * cos (pi / real n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S pi"
    5.27  by (insert NSLIMSEQ_mult [OF NSLIMSEQ_sin_pi NSLIMSEQ_cos_one], simp)
    5.28  
    5.29