--- a/NEWS Tue Dec 29 23:20:11 2015 +0100
+++ b/NEWS Tue Dec 29 23:40:04 2015 +0100
@@ -505,6 +505,7 @@
notation (in topological_space) LIMSEQ ("((_)/ ----> (_))" [60, 60] 60)
notation NSLIMSEQ ("((_)/ ----NS> (_))" [60, 60] 60)
+ notation NSLIM ("((_)/ -- (_)/ --NS> (_))" [60, 0, 60] 60)
* The alternative notation "\<Colon>" for type and sort constraints has been
removed: in LaTeX document output it looks the same as "::".
--- a/etc/abbrevs Tue Dec 29 23:20:11 2015 +0100
+++ b/etc/abbrevs Tue Dec 29 23:40:04 2015 +0100
@@ -8,3 +8,4 @@
(*HOL-NSA*)
"---->" = "\<longlonglongrightarrow>\<^sub>N\<^sub>S"
+"---->" = "\<midarrow>\<rightarrow>\<^sub>N\<^sub>S"
--- a/src/HOL/NSA/CLim.thy Tue Dec 29 23:20:11 2015 +0100
+++ b/src/HOL/NSA/CLim.thy Tue Dec 29 23:40:04 2015 +0100
@@ -36,11 +36,11 @@
subsection{*Limit of Complex to Complex Function*}
-lemma NSLIM_Re: "f -- a --NS> L ==> (%x. Re(f x)) -- a --NS> Re(L)"
+lemma NSLIM_Re: "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L ==> (%x. Re(f x)) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S Re(L)"
by (simp add: NSLIM_def starfunC_approx_Re_Im_iff
hRe_hcomplex_of_complex)
-lemma NSLIM_Im: "f -- a --NS> L ==> (%x. Im(f x)) -- a --NS> Im(L)"
+lemma NSLIM_Im: "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L ==> (%x. Im(f x)) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S Im(L)"
by (simp add: NSLIM_def starfunC_approx_Re_Im_iff
hIm_hcomplex_of_complex)
@@ -77,7 +77,7 @@
text""
(** another equivalence result **)
lemma NSCLIM_NSCRLIM_iff:
- "(f -- x --NS> L) = ((%y. cmod(f y - L)) -- x --NS> 0)"
+ "(f \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S L) = ((%y. cmod(f y - L)) \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S 0)"
by (simp add: NSLIM_def starfun_norm
approx_approx_zero_iff [symmetric] approx_minus_iff [symmetric])
@@ -89,12 +89,12 @@
(* so this is nicer nonstandard proof *)
lemma NSCLIM_NSCRLIM_iff2:
- "(f -- x --NS> L) = ((%y. cmod(f y - L)) -- x --NS> 0)"
+ "(f \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S L) = ((%y. cmod(f y - L)) \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S 0)"
by (simp add: LIM_NSLIM_iff [symmetric] CLIM_CRLIM_iff)
lemma NSLIM_NSCRLIM_Re_Im_iff:
- "(f -- a --NS> L) = ((%x. Re(f x)) -- a --NS> Re(L) &
- (%x. Im(f x)) -- a --NS> Im(L))"
+ "(f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L) = ((%x. Re(f x)) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S Re(L) &
+ (%x. Im(f x)) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S Im(L))"
apply (auto intro: NSLIM_Re NSLIM_Im)
apply (auto simp add: NSLIM_def starfun_Re starfun_Im)
apply (auto dest!: spec)
@@ -111,7 +111,7 @@
subsection{*Continuity*}
lemma NSLIM_isContc_iff:
- "(f -- a --NS> f a) = ((%h. f(a + h)) -- 0 --NS> f a)"
+ "(f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S f a) = ((%h. f(a + h)) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S f a)"
by (rule NSLIM_h_iff)
subsection{*Functions from Complex to Reals*}
--- a/src/HOL/NSA/HDeriv.thy Tue Dec 29 23:20:11 2015 +0100
+++ b/src/HOL/NSA/HDeriv.thy Tue Dec 29 23:40:04 2015 +0100
@@ -33,10 +33,10 @@
subsection {* Derivatives *}
lemma DERIV_NS_iff:
- "(DERIV f x :> D) = ((%h. (f(x + h) - f(x))/h) -- 0 --NS> D)"
+ "(DERIV f x :> D) = ((%h. (f(x + h) - f(x))/h) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S D)"
by (simp add: DERIV_def LIM_NSLIM_iff)
-lemma NS_DERIV_D: "DERIV f x :> D ==> (%h. (f(x + h) - f(x))/h) -- 0 --NS> D"
+lemma NS_DERIV_D: "DERIV f x :> D ==> (%h. (f(x + h) - f(x))/h) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S D"
by (simp add: DERIV_def LIM_NSLIM_iff)
lemma hnorm_of_hypreal:
@@ -70,7 +70,7 @@
text{*first equivalence *}
lemma NSDERIV_NSLIM_iff:
- "(NSDERIV f x :> D) = ((%h. (f(x + h) - f(x))/h) -- 0 --NS> D)"
+ "(NSDERIV f x :> D) = ((%h. (f(x + h) - f(x))/h) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S D)"
apply (simp add: nsderiv_def NSLIM_def, auto)
apply (drule_tac x = xa in bspec)
apply (rule_tac [3] ccontr)
@@ -80,7 +80,7 @@
text{*second equivalence *}
lemma NSDERIV_NSLIM_iff2:
- "(NSDERIV f x :> D) = ((%z. (f(z) - f(x)) / (z-x)) -- x --NS> D)"
+ "(NSDERIV f x :> D) = ((%z. (f(z) - f(x)) / (z-x)) \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S D)"
by (simp add: NSDERIV_NSLIM_iff DERIV_LIM_iff LIM_NSLIM_iff [symmetric])
(* while we're at it! *)
@@ -227,15 +227,15 @@
text{*Negation of function*}
lemma NSDERIV_minus: "NSDERIV f x :> D ==> NSDERIV (%x. -(f x)) x :> -D"
proof (simp add: NSDERIV_NSLIM_iff)
- assume "(\<lambda>h. (f (x + h) - f x) / h) -- 0 --NS> D"
- hence deriv: "(\<lambda>h. - ((f(x+h) - f x) / h)) -- 0 --NS> - D"
+ assume "(\<lambda>h. (f (x + h) - f x) / h) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S D"
+ hence deriv: "(\<lambda>h. - ((f(x+h) - f x) / h)) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S - D"
by (rule NSLIM_minus)
have "\<forall>h. - ((f (x + h) - f x) / h) = (- f (x + h) + f x) / h"
by (simp add: minus_divide_left)
with deriv
- have "(\<lambda>h. (- f (x + h) + f x) / h) -- 0 --NS> - D" by simp
- then show "(\<lambda>h. (f (x + h) - f x) / h) -- 0 --NS> D \<Longrightarrow>
- (\<lambda>h. (f x - f (x + h)) / h) -- 0 --NS> - D" by simp
+ have "(\<lambda>h. (- f (x + h) + f x) / h) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S - D" by simp
+ then show "(\<lambda>h. (f (x + h) - f x) / h) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S D \<Longrightarrow>
+ (\<lambda>h. (f x - f (x + h)) / h) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S - D" by simp
qed
text{*Subtraction*}
--- a/src/HOL/NSA/HLim.thy Tue Dec 29 23:20:11 2015 +0100
+++ b/src/HOL/NSA/HLim.thy Tue Dec 29 23:40:04 2015 +0100
@@ -13,8 +13,8 @@
definition
NSLIM :: "['a::real_normed_vector => 'b::real_normed_vector, 'a, 'b] => bool"
- ("((_)/ -- (_)/ --NS> (_))" [60, 0, 60] 60) where
- "f -- a --NS> L =
+ ("((_)/ \<midarrow>(_)/\<rightarrow>\<^sub>N\<^sub>S (_))" [60, 0, 60] 60) where
+ "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L =
(\<forall>x. (x \<noteq> star_of a & x @= star_of a --> ( *f* f) x @= star_of L))"
definition
@@ -32,11 +32,11 @@
lemma NSLIM_I:
"(\<And>x. \<lbrakk>x \<noteq> star_of a; x \<approx> star_of a\<rbrakk> \<Longrightarrow> starfun f x \<approx> star_of L)
- \<Longrightarrow> f -- a --NS> L"
+ \<Longrightarrow> f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L"
by (simp add: NSLIM_def)
lemma NSLIM_D:
- "\<lbrakk>f -- a --NS> L; x \<noteq> star_of a; x \<approx> star_of a\<rbrakk>
+ "\<lbrakk>f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L; x \<noteq> star_of a; x \<approx> star_of a\<rbrakk>
\<Longrightarrow> starfun f x \<approx> star_of L"
by (simp add: NSLIM_def)
@@ -45,8 +45,8 @@
lemma NSLIM_mult:
fixes l m :: "'a::real_normed_algebra"
- shows "[| f -- x --NS> l; g -- x --NS> m |]
- ==> (%x. f(x) * g(x)) -- x --NS> (l * m)"
+ shows "[| f \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S l; g \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S m |]
+ ==> (%x. f(x) * g(x)) \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S (l * m)"
by (auto simp add: NSLIM_def intro!: approx_mult_HFinite)
lemma starfun_scaleR [simp]:
@@ -54,53 +54,53 @@
by transfer (rule refl)
lemma NSLIM_scaleR:
- "[| f -- x --NS> l; g -- x --NS> m |]
- ==> (%x. f(x) *\<^sub>R g(x)) -- x --NS> (l *\<^sub>R m)"
+ "[| f \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S l; g \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S m |]
+ ==> (%x. f(x) *\<^sub>R g(x)) \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S (l *\<^sub>R m)"
by (auto simp add: NSLIM_def intro!: approx_scaleR_HFinite)
lemma NSLIM_add:
- "[| f -- x --NS> l; g -- x --NS> m |]
- ==> (%x. f(x) + g(x)) -- x --NS> (l + m)"
+ "[| f \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S l; g \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S m |]
+ ==> (%x. f(x) + g(x)) \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S (l + m)"
by (auto simp add: NSLIM_def intro!: approx_add)
-lemma NSLIM_const [simp]: "(%x. k) -- x --NS> k"
+lemma NSLIM_const [simp]: "(%x. k) \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S k"
by (simp add: NSLIM_def)
-lemma NSLIM_minus: "f -- a --NS> L ==> (%x. -f(x)) -- a --NS> -L"
+lemma NSLIM_minus: "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L ==> (%x. -f(x)) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S -L"
by (simp add: NSLIM_def)
lemma NSLIM_diff:
- "\<lbrakk>f -- x --NS> l; g -- x --NS> m\<rbrakk> \<Longrightarrow> (\<lambda>x. f x - g x) -- x --NS> (l - m)"
+ "\<lbrakk>f \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S l; g \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S m\<rbrakk> \<Longrightarrow> (\<lambda>x. f x - g x) \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S (l - m)"
by (simp only: NSLIM_add NSLIM_minus diff_conv_add_uminus)
-lemma NSLIM_add_minus: "[| f -- x --NS> l; g -- x --NS> m |] ==> (%x. f(x) + -g(x)) -- x --NS> (l + -m)"
+lemma NSLIM_add_minus: "[| f \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S l; g \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S m |] ==> (%x. f(x) + -g(x)) \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S (l + -m)"
by (simp only: NSLIM_add NSLIM_minus)
lemma NSLIM_inverse:
fixes L :: "'a::real_normed_div_algebra"
- shows "[| f -- a --NS> L; L \<noteq> 0 |]
- ==> (%x. inverse(f(x))) -- a --NS> (inverse L)"
+ shows "[| f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L; L \<noteq> 0 |]
+ ==> (%x. inverse(f(x))) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S (inverse L)"
apply (simp add: NSLIM_def, clarify)
apply (drule spec)
apply (auto simp add: star_of_approx_inverse)
done
lemma NSLIM_zero:
- assumes f: "f -- a --NS> l" shows "(%x. f(x) - l) -- a --NS> 0"
+ assumes f: "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S l" shows "(%x. f(x) - l) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S 0"
proof -
- have "(\<lambda>x. f x - l) -- a --NS> l - l"
+ have "(\<lambda>x. f x - l) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S l - l"
by (rule NSLIM_diff [OF f NSLIM_const])
thus ?thesis by simp
qed
-lemma NSLIM_zero_cancel: "(%x. f(x) - l) -- x --NS> 0 ==> f -- x --NS> l"
+lemma NSLIM_zero_cancel: "(%x. f(x) - l) \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S 0 ==> f \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S l"
apply (drule_tac g = "%x. l" and m = l in NSLIM_add)
apply (auto simp add: add.assoc)
done
lemma NSLIM_const_not_eq:
fixes a :: "'a::real_normed_algebra_1"
- shows "k \<noteq> L \<Longrightarrow> \<not> (\<lambda>x. k) -- a --NS> L"
+ shows "k \<noteq> L \<Longrightarrow> \<not> (\<lambda>x. k) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L"
apply (simp add: NSLIM_def)
apply (rule_tac x="star_of a + of_hypreal epsilon" in exI)
apply (simp add: hypreal_epsilon_not_zero approx_def)
@@ -108,35 +108,35 @@
lemma NSLIM_not_zero:
fixes a :: "'a::real_normed_algebra_1"
- shows "k \<noteq> 0 \<Longrightarrow> \<not> (\<lambda>x. k) -- a --NS> 0"
+ shows "k \<noteq> 0 \<Longrightarrow> \<not> (\<lambda>x. k) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S 0"
by (rule NSLIM_const_not_eq)
lemma NSLIM_const_eq:
fixes a :: "'a::real_normed_algebra_1"
- shows "(\<lambda>x. k) -- a --NS> L \<Longrightarrow> k = L"
+ shows "(\<lambda>x. k) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L \<Longrightarrow> k = L"
apply (rule ccontr)
apply (blast dest: NSLIM_const_not_eq)
done
lemma NSLIM_unique:
fixes a :: "'a::real_normed_algebra_1"
- shows "\<lbrakk>f -- a --NS> L; f -- a --NS> M\<rbrakk> \<Longrightarrow> L = M"
+ shows "\<lbrakk>f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L; f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S M\<rbrakk> \<Longrightarrow> L = M"
apply (drule (1) NSLIM_diff)
apply (auto dest!: NSLIM_const_eq)
done
lemma NSLIM_mult_zero:
fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra"
- shows "[| f -- x --NS> 0; g -- x --NS> 0 |] ==> (%x. f(x)*g(x)) -- x --NS> 0"
+ shows "[| f \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S 0; g \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S 0 |] ==> (%x. f(x)*g(x)) \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S 0"
by (drule NSLIM_mult, auto)
-lemma NSLIM_self: "(%x. x) -- a --NS> a"
+lemma NSLIM_self: "(%x. x) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S a"
by (simp add: NSLIM_def)
subsubsection {* Equivalence of @{term filterlim} and @{term NSLIM} *}
lemma LIM_NSLIM:
- assumes f: "f -- a --> L" shows "f -- a --NS> L"
+ assumes f: "f -- a --> L" shows "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L"
proof (rule NSLIM_I)
fix x
assume neq: "x \<noteq> star_of a"
@@ -164,7 +164,7 @@
qed
lemma NSLIM_LIM:
- assumes f: "f -- a --NS> L" shows "f -- a --> L"
+ assumes f: "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L" shows "f -- a --> L"
proof (rule LIM_I)
fix r::real assume r: "0 < r"
have "\<exists>s>0. \<forall>x. x \<noteq> star_of a \<and> hnorm (x - star_of a) < s
@@ -190,7 +190,7 @@
by transfer
qed
-theorem LIM_NSLIM_iff: "(f -- x --> L) = (f -- x --NS> L)"
+theorem LIM_NSLIM_iff: "(f -- x --> L) = (f \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S L)"
by (blast intro: LIM_NSLIM NSLIM_LIM)
@@ -200,17 +200,17 @@
"\<lbrakk>isNSCont f a; y \<approx> star_of a\<rbrakk> \<Longrightarrow> ( *f* f) y \<approx> star_of (f a)"
by (simp add: isNSCont_def)
-lemma isNSCont_NSLIM: "isNSCont f a ==> f -- a --NS> (f a) "
+lemma isNSCont_NSLIM: "isNSCont f a ==> f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S (f a) "
by (simp add: isNSCont_def NSLIM_def)
-lemma NSLIM_isNSCont: "f -- a --NS> (f a) ==> isNSCont f a"
+lemma NSLIM_isNSCont: "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S (f a) ==> isNSCont f a"
apply (simp add: isNSCont_def NSLIM_def, auto)
apply (case_tac "y = star_of a", auto)
done
text{*NS continuity can be defined using NS Limit in
similar fashion to standard def of continuity*}
-lemma isNSCont_NSLIM_iff: "(isNSCont f a) = (f -- a --NS> (f a))"
+lemma isNSCont_NSLIM_iff: "(isNSCont f a) = (f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S (f a))"
by (blast intro: isNSCont_NSLIM NSLIM_isNSCont)
text{*Hence, NS continuity can be given
@@ -237,7 +237,7 @@
(* Prove equivalence between NS limits - *)
(* seems easier than using standard def *)
-lemma NSLIM_h_iff: "(f -- a --NS> L) = ((%h. f(a + h)) -- 0 --NS> L)"
+lemma NSLIM_h_iff: "(f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L) = ((%h. f(a + h)) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S L)"
apply (simp add: NSLIM_def, auto)
apply (drule_tac x = "star_of a + x" in spec)
apply (drule_tac [2] x = "- star_of a + x" in spec, safe, simp)
@@ -249,7 +249,7 @@
apply (auto simp add: starfun star_of_def star_n_minus star_n_add add.assoc star_n_zero_num)
done
-lemma NSLIM_isCont_iff: "(f -- a --NS> f a) = ((%h. f(a + h)) -- 0 --NS> f a)"
+lemma NSLIM_isCont_iff: "(f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S f a) = ((%h. f(a + h)) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S f a)"
by (fact NSLIM_h_iff)
lemma isNSCont_minus: "isNSCont f a ==> isNSCont (%x. - f x) a"
--- a/src/HOL/NSA/HTranscendental.thy Tue Dec 29 23:20:11 2015 +0100
+++ b/src/HOL/NSA/HTranscendental.thy Tue Dec 29 23:40:04 2015 +0100
@@ -406,7 +406,7 @@
(*
-Goalw [NSLIM_def] "(%h. ((x powr h) - 1) / h) -- 0 --NS> ln x"
+Goalw [NSLIM_def] "(%h. ((x powr h) - 1) / h) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S ln x"
*)
lemma HFinite_sin [simp]: "sumhr (0, whn, %n. sin_coeff n * x ^ n) \<in> HFinite"