--- a/NEWS Wed Dec 30 11:37:29 2015 +0100
+++ b/NEWS Wed Dec 30 14:05:51 2015 +0100
@@ -504,6 +504,7 @@
notation (in topological_space) tendsto (infixr "--->" 55)
notation (in topological_space) LIMSEQ ("((_)/ ----> (_))" [60, 60] 60)
+ notation LIM ("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60)
notation NSLIMSEQ ("((_)/ ----NS> (_))" [60, 60] 60)
notation NSLIM ("((_)/ -- (_)/ --NS> (_))" [60, 0, 60] 60)
--- a/etc/abbrevs Wed Dec 30 11:37:29 2015 +0100
+++ b/etc/abbrevs Wed Dec 30 14:05:51 2015 +0100
@@ -3,6 +3,8 @@
(*prevent replacement of very long arrows*)
"===>" = "===>"
+"--->" = "\<midarrow>\<rightarrow>"
+
(*HOL-NSA*)
"--->" = "\<longlonglongrightarrow>\<^sub>N\<^sub>S"
"--->" = "\<midarrow>\<rightarrow>\<^sub>N\<^sub>S"
--- a/src/HOL/Deriv.thy Wed Dec 30 11:37:29 2015 +0100
+++ b/src/HOL/Deriv.thy Wed Dec 30 14:05:51 2015 +0100
@@ -148,12 +148,12 @@
by (simp add: has_derivative_at_within divide_inverse ac_simps)
lemma has_derivative_at:
- "(f has_derivative D) (at x) \<longleftrightarrow> (bounded_linear D \<and> (\<lambda>h. norm (f (x + h) - f x - D h) / norm h) -- 0 --> 0)"
+ "(f has_derivative D) (at x) \<longleftrightarrow> (bounded_linear D \<and> (\<lambda>h. norm (f (x + h) - f x - D h) / norm h) \<midarrow>0\<rightarrow> 0)"
unfolding has_derivative_iff_norm LIM_offset_zero_iff[of _ _ x] by simp
lemma field_has_derivative_at:
fixes x :: "'a::real_normed_field"
- shows "(f has_derivative op * D) (at x) \<longleftrightarrow> (\<lambda>h. (f (x + h) - f x) / h) -- 0 --> D"
+ shows "(f has_derivative op * D) (at x) \<longleftrightarrow> (\<lambda>h. (f (x + h) - f x) / h) \<midarrow>0\<rightarrow> D"
apply (unfold has_derivative_at)
apply (simp add: bounded_linear_mult_right)
apply (simp cong: LIM_cong add: nonzero_norm_divide [symmetric])
@@ -454,7 +454,7 @@
interpret F: bounded_linear F
using assms by (rule has_derivative_bounded_linear)
let ?r = "\<lambda>h. norm (F h) / norm h"
- have *: "?r -- 0 --> 0"
+ have *: "?r \<midarrow>0\<rightarrow> 0"
using assms unfolding has_derivative_at by simp
show "F = (\<lambda>h. 0)"
proof
@@ -599,7 +599,7 @@
lemma differentiableI: "(f has_real_derivative D) (at x within s) \<Longrightarrow> f differentiable (at x within s)"
by (force simp add: real_differentiable_def)
-lemma DERIV_def: "DERIV f x :> D \<longleftrightarrow> (\<lambda>h. (f (x + h) - f x) / h) -- 0 --> D"
+lemma DERIV_def: "DERIV f x :> D \<longleftrightarrow> (\<lambda>h. (f (x + h) - f x) / h) \<midarrow>0\<rightarrow> D"
apply (simp add: has_field_derivative_def has_derivative_at bounded_linear_mult_right LIM_zero_iff[symmetric, of _ D])
apply (subst (2) tendsto_norm_zero_iff[symmetric])
apply (rule filterlim_cong)
@@ -701,7 +701,7 @@
subsection \<open>Derivatives\<close>
-lemma DERIV_D: "DERIV f x :> D \<Longrightarrow> (\<lambda>h. (f (x + h) - f x) / h) -- 0 --> D"
+lemma DERIV_D: "DERIV f x :> D \<Longrightarrow> (\<lambda>h. (f (x + h) - f x) / h) \<midarrow>0\<rightarrow> D"
by (simp add: DERIV_def)
lemma DERIV_const [simp, derivative_intros]: "((\<lambda>x. k) has_field_derivative 0) F"
@@ -883,8 +883,8 @@
lemma DERIV_LIM_iff:
fixes f :: "'a::{real_normed_vector,inverse} \<Rightarrow> 'a" shows
- "((%h. (f(a + h) - f(a)) / h) -- 0 --> D) =
- ((%x. (f(x)-f(a)) / (x-a)) -- a --> D)"
+ "((%h. (f(a + h) - f(a)) / h) \<midarrow>0\<rightarrow> D) =
+ ((%x. (f(x)-f(a)) / (x-a)) \<midarrow>a\<rightarrow> D)"
apply (rule iffI)
apply (drule_tac k="- a" in LIM_offset)
apply simp
@@ -892,7 +892,7 @@
apply (simp add: add.commute)
done
-lemma DERIV_iff2: "(DERIV f x :> D) \<longleftrightarrow> (\<lambda>z. (f z - f x) / (z - x)) --x --> D"
+lemma DERIV_iff2: "(DERIV f x :> D) \<longleftrightarrow> (\<lambda>z. (f z - f x) / (z - x)) \<midarrow>x\<rightarrow> D"
by (simp add: DERIV_def DERIV_LIM_iff)
lemma DERIV_cong_ev: "x = y \<Longrightarrow> eventually (\<lambda>x. f x = g x) (nhds x) \<Longrightarrow> u = v \<Longrightarrow>
@@ -1485,9 +1485,9 @@
inverse ((f (g y) - x) / (g y - g x))"
by (simp add: inj)
next
- have "(\<lambda>z. (f z - f (g x)) / (z - g x)) -- g x --> D"
+ have "(\<lambda>z. (f z - f (g x)) / (z - g x)) \<midarrow>g x\<rightarrow> D"
by (rule der [unfolded DERIV_iff2])
- hence 1: "(\<lambda>z. (f z - x) / (z - g x)) -- g x --> D"
+ hence 1: "(\<lambda>z. (f z - x) / (z - g x)) \<midarrow>g x\<rightarrow> D"
using inj a b by simp
have 2: "\<exists>d>0. \<forall>y. y \<noteq> x \<and> norm (y - x) < d \<longrightarrow> g y \<noteq> g x"
proof (rule exI, safe)
@@ -1504,10 +1504,10 @@
also assume "y \<noteq> x"
finally show False by simp
qed
- have "(\<lambda>y. (f (g y) - x) / (g y - g x)) -- x --> D"
+ have "(\<lambda>y. (f (g y) - x) / (g y - g x)) \<midarrow>x\<rightarrow> D"
using cont 1 2 by (rule isCont_LIM_compose2)
thus "(\<lambda>y. inverse ((f (g y) - x) / (g y - g x)))
- -- x --> inverse D"
+ \<midarrow>x\<rightarrow> inverse D"
using neq by (rule tendsto_inverse)
qed
--- a/src/HOL/Library/Extended_Real.thy Wed Dec 30 11:37:29 2015 +0100
+++ b/src/HOL/Library/Extended_Real.thy Wed Dec 30 14:05:51 2015 +0100
@@ -3596,7 +3596,7 @@
unfolding tendsto_PInfty filterlim_at_top_dense tendsto_MInfty filterlim_at_bot_dense
using lim_ereal by (simp_all add: comp_def)
-lemma inverse_infty_ereal_tendsto_0: "inverse -- \<infinity> --> (0::ereal)"
+lemma inverse_infty_ereal_tendsto_0: "inverse \<midarrow>\<infinity>\<rightarrow> (0::ereal)"
proof -
have **: "((\<lambda>x. ereal (inverse x)) \<longlongrightarrow> ereal 0) at_infinity"
by (intro tendsto_intros tendsto_inverse_0)
@@ -3609,10 +3609,10 @@
lemma inverse_ereal_tendsto_pos:
fixes x :: ereal assumes "0 < x"
- shows "inverse -- x --> inverse x"
+ shows "inverse \<midarrow>x\<rightarrow> inverse x"
proof (cases x)
case (real r)
- with \<open>0 < x\<close> have **: "(\<lambda>x. ereal (inverse x)) -- r --> ereal (inverse r)"
+ with \<open>0 < x\<close> have **: "(\<lambda>x. ereal (inverse x)) \<midarrow>r\<rightarrow> ereal (inverse r)"
by (auto intro!: tendsto_inverse)
from real \<open>0 < x\<close> show ?thesis
by (auto simp: at_ereal tendsto_compose_filtermap[symmetric] eventually_at_filter
--- a/src/HOL/Limits.thy Wed Dec 30 11:37:29 2015 +0100
+++ b/src/HOL/Limits.thy Wed Dec 30 14:05:51 2015 +0100
@@ -1941,40 +1941,40 @@
lemma LIM_eq:
fixes a :: "'a::real_normed_vector" and L :: "'b::real_normed_vector"
- shows "f -- a --> L =
+ shows "f \<midarrow>a\<rightarrow> L =
(\<forall>r>0.\<exists>s>0.\<forall>x. x \<noteq> a & norm (x-a) < s --> norm (f x - L) < r)"
by (simp add: LIM_def dist_norm)
lemma LIM_I:
fixes a :: "'a::real_normed_vector" and L :: "'b::real_normed_vector"
shows "(!!r. 0<r ==> \<exists>s>0.\<forall>x. x \<noteq> a & norm (x-a) < s --> norm (f x - L) < r)
- ==> f -- a --> L"
+ ==> f \<midarrow>a\<rightarrow> L"
by (simp add: LIM_eq)
lemma LIM_D:
fixes a :: "'a::real_normed_vector" and L :: "'b::real_normed_vector"
- shows "[| f -- a --> L; 0<r |]
+ shows "[| f \<midarrow>a\<rightarrow> L; 0<r |]
==> \<exists>s>0.\<forall>x. x \<noteq> a & norm (x-a) < s --> norm (f x - L) < r"
by (simp add: LIM_eq)
lemma LIM_offset:
fixes a :: "'a::real_normed_vector"
- shows "f -- a --> L \<Longrightarrow> (\<lambda>x. f (x + k)) -- a - k --> L"
+ shows "f \<midarrow>a\<rightarrow> L \<Longrightarrow> (\<lambda>x. f (x + k)) \<midarrow>(a - k)\<rightarrow> L"
unfolding filtermap_at_shift[symmetric, of a k] filterlim_def filtermap_filtermap by simp
lemma LIM_offset_zero:
fixes a :: "'a::real_normed_vector"
- shows "f -- a --> L \<Longrightarrow> (\<lambda>h. f (a + h)) -- 0 --> L"
+ shows "f \<midarrow>a\<rightarrow> L \<Longrightarrow> (\<lambda>h. f (a + h)) \<midarrow>0\<rightarrow> L"
by (drule_tac k="a" in LIM_offset, simp add: add.commute)
lemma LIM_offset_zero_cancel:
fixes a :: "'a::real_normed_vector"
- shows "(\<lambda>h. f (a + h)) -- 0 --> L \<Longrightarrow> f -- a --> L"
+ shows "(\<lambda>h. f (a + h)) \<midarrow>0\<rightarrow> L \<Longrightarrow> f \<midarrow>a\<rightarrow> L"
by (drule_tac k="- a" in LIM_offset, simp)
lemma LIM_offset_zero_iff:
fixes f :: "'a :: real_normed_vector \<Rightarrow> _"
- shows "f -- a --> L \<longleftrightarrow> (\<lambda>h. f (a + h)) -- 0 --> L"
+ shows "f \<midarrow>a\<rightarrow> L \<longleftrightarrow> (\<lambda>h. f (a + h)) \<midarrow>0\<rightarrow> L"
using LIM_offset_zero_cancel[of f a L] LIM_offset_zero[of f L a] by auto
lemma LIM_zero:
@@ -1995,9 +1995,9 @@
lemma LIM_imp_LIM:
fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
fixes g :: "'a::topological_space \<Rightarrow> 'c::real_normed_vector"
- assumes f: "f -- a --> l"
+ assumes f: "f \<midarrow>a\<rightarrow> l"
assumes le: "\<And>x. x \<noteq> a \<Longrightarrow> norm (g x - m) \<le> norm (f x - l)"
- shows "g -- a --> m"
+ shows "g \<midarrow>a\<rightarrow> m"
by (rule metric_LIM_imp_LIM [OF f],
simp add: dist_norm le)
@@ -2005,23 +2005,23 @@
fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::topological_space"
assumes 1: "0 < R"
assumes 2: "\<And>x. \<lbrakk>x \<noteq> a; norm (x - a) < R\<rbrakk> \<Longrightarrow> f x = g x"
- shows "g -- a --> l \<Longrightarrow> f -- a --> l"
+ shows "g \<midarrow>a\<rightarrow> l \<Longrightarrow> f \<midarrow>a\<rightarrow> l"
by (rule metric_LIM_equal2 [OF 1 2], simp_all add: dist_norm)
lemma LIM_compose2:
fixes a :: "'a::real_normed_vector"
- assumes f: "f -- a --> b"
- assumes g: "g -- b --> c"
+ assumes f: "f \<midarrow>a\<rightarrow> b"
+ assumes g: "g \<midarrow>b\<rightarrow> c"
assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < d \<longrightarrow> f x \<noteq> b"
- shows "(\<lambda>x. g (f x)) -- a --> c"
+ shows "(\<lambda>x. g (f x)) \<midarrow>a\<rightarrow> c"
by (rule metric_LIM_compose2 [OF f g inj [folded dist_norm]])
lemma real_LIM_sandwich_zero:
fixes f g :: "'a::topological_space \<Rightarrow> real"
- assumes f: "f -- a --> 0"
+ assumes f: "f \<midarrow>a\<rightarrow> 0"
assumes 1: "\<And>x. x \<noteq> a \<Longrightarrow> 0 \<le> g x"
assumes 2: "\<And>x. x \<noteq> a \<Longrightarrow> g x \<le> f x"
- shows "g -- a --> 0"
+ shows "g \<midarrow>a\<rightarrow> 0"
proof (rule LIM_imp_LIM [OF f]) (* FIXME: use tendsto_sandwich *)
fix x assume x: "x \<noteq> a"
have "norm (g x - 0) = g x" by (simp add: 1 x)
@@ -2036,20 +2036,20 @@
lemma LIM_isCont_iff:
fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::topological_space"
- shows "(f -- a --> f a) = ((\<lambda>h. f (a + h)) -- 0 --> f a)"
+ shows "(f \<midarrow>a\<rightarrow> f a) = ((\<lambda>h. f (a + h)) \<midarrow>0\<rightarrow> f a)"
by (rule iffI [OF LIM_offset_zero LIM_offset_zero_cancel])
lemma isCont_iff:
fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::topological_space"
- shows "isCont f x = (\<lambda>h. f (x + h)) -- 0 --> f x"
+ shows "isCont f x = (\<lambda>h. f (x + h)) \<midarrow>0\<rightarrow> f x"
by (simp add: isCont_def LIM_isCont_iff)
lemma isCont_LIM_compose2:
fixes a :: "'a::real_normed_vector"
assumes f [unfolded isCont_def]: "isCont f a"
- assumes g: "g -- f a --> l"
+ assumes g: "g \<midarrow>f a\<rightarrow> l"
assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < d \<longrightarrow> f x \<noteq> f a"
- shows "(\<lambda>x. g (f x)) -- a --> l"
+ shows "(\<lambda>x. g (f x)) \<midarrow>a\<rightarrow> l"
by (rule LIM_compose2 [OF f g inj])
@@ -2403,7 +2403,7 @@
text\<open>Bartle/Sherbert: Introduction to Real Analysis, Theorem 4.2.9, p. 110\<close>
lemma LIM_fun_gt_zero:
fixes f :: "real \<Rightarrow> real"
- shows "f -- c --> l \<Longrightarrow> 0 < l \<Longrightarrow> \<exists>r. 0 < r \<and> (\<forall>x. x \<noteq> c \<and> \<bar>c - x\<bar> < r \<longrightarrow> 0 < f x)"
+ shows "f \<midarrow>c\<rightarrow> l \<Longrightarrow> 0 < l \<Longrightarrow> \<exists>r. 0 < r \<and> (\<forall>x. x \<noteq> c \<and> \<bar>c - x\<bar> < r \<longrightarrow> 0 < f x)"
apply (drule (1) LIM_D, clarify)
apply (rule_tac x = s in exI)
apply (simp add: abs_less_iff)
@@ -2411,7 +2411,7 @@
lemma LIM_fun_less_zero:
fixes f :: "real \<Rightarrow> real"
- shows "f -- c --> l \<Longrightarrow> l < 0 \<Longrightarrow> \<exists>r. 0 < r \<and> (\<forall>x. x \<noteq> c \<and> \<bar>c - x\<bar> < r \<longrightarrow> f x < 0)"
+ shows "f \<midarrow>c\<rightarrow> l \<Longrightarrow> l < 0 \<Longrightarrow> \<exists>r. 0 < r \<and> (\<forall>x. x \<noteq> c \<and> \<bar>c - x\<bar> < r \<longrightarrow> f x < 0)"
apply (drule LIM_D [where r="-l"], simp, clarify)
apply (rule_tac x = s in exI)
apply (simp add: abs_less_iff)
@@ -2419,7 +2419,7 @@
lemma LIM_fun_not_zero:
fixes f :: "real \<Rightarrow> real"
- shows "f -- c --> l \<Longrightarrow> l \<noteq> 0 \<Longrightarrow> \<exists>r. 0 < r \<and> (\<forall>x. x \<noteq> c \<and> \<bar>c - x\<bar> < r \<longrightarrow> f x \<noteq> 0)"
+ shows "f \<midarrow>c\<rightarrow> l \<Longrightarrow> l \<noteq> 0 \<Longrightarrow> \<exists>r. 0 < r \<and> (\<forall>x. x \<noteq> c \<and> \<bar>c - x\<bar> < r \<longrightarrow> f x \<noteq> 0)"
using LIM_fun_gt_zero[of f l c] LIM_fun_less_zero[of f l c] by (auto simp add: neq_iff)
end
--- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Wed Dec 30 11:37:29 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Wed Dec 30 14:05:51 2015 +0100
@@ -2552,7 +2552,7 @@
then have "\<exists>d>0. \<forall>y. y \<noteq> x \<and> cmod (y-x) < d \<longrightarrow> cmod (?pathint x y - f x * (y-x)) / cmod (y-x) < e"
using dpos by blast
}
- then have *: "(\<lambda>y. (?pathint x y - f x * (y - x)) /\<^sub>R cmod (y - x)) -- x --> 0"
+ then have *: "(\<lambda>y. (?pathint x y - f x * (y - x)) /\<^sub>R cmod (y - x)) \<midarrow>x\<rightarrow> 0"
by (simp add: Lim_at dist_norm inverse_eq_divide)
show ?thesis
apply (simp add: has_field_derivative_def has_derivative_at bounded_linear_mult_right)
@@ -5472,7 +5472,7 @@
show "(\<lambda>u. f' u / (u - w) ^ (Suc k)) contour_integrable_on \<gamma>"
by (rule contour_integral_uniform_limit [OF 1 2 leB \<gamma>]) auto
have *: "(\<lambda>n. contour_integral \<gamma> (\<lambda>x. f' x * (inverse (x - n) ^ k - inverse (x - w) ^ k) / (n - w) / k))
- --w--> contour_integral \<gamma> (\<lambda>u. f' u / (u - w) ^ (Suc k))"
+ \<midarrow>w\<rightarrow> contour_integral \<gamma> (\<lambda>u. f' u / (u - w) ^ (Suc k))"
by (rule contour_integral_uniform_limit [OF 1 2 leB \<gamma>]) auto
have **: "contour_integral \<gamma> (\<lambda>x. f' x * (inverse (x - u) ^ k - inverse (x - w) ^ k) / ((u - w) * k)) =
(f u - f w) / (u - w) / k"
--- a/src/HOL/NSA/CLim.thy Wed Dec 30 11:37:29 2015 +0100
+++ b/src/HOL/NSA/CLim.thy Wed Dec 30 14:05:51 2015 +0100
@@ -47,22 +47,22 @@
(** get this result easily now **)
lemma LIM_Re:
fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
- shows "f -- a --> L ==> (%x. Re(f x)) -- a --> Re(L)"
+ shows "f \<midarrow>a\<rightarrow> L ==> (%x. Re(f x)) \<midarrow>a\<rightarrow> Re(L)"
by (simp add: LIM_NSLIM_iff NSLIM_Re)
lemma LIM_Im:
fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
- shows "f -- a --> L ==> (%x. Im(f x)) -- a --> Im(L)"
+ shows "f \<midarrow>a\<rightarrow> L ==> (%x. Im(f x)) \<midarrow>a\<rightarrow> Im(L)"
by (simp add: LIM_NSLIM_iff NSLIM_Im)
lemma LIM_cnj:
fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
- shows "f -- a --> L ==> (%x. cnj (f x)) -- a --> cnj L"
+ shows "f \<midarrow>a\<rightarrow> L ==> (%x. cnj (f x)) \<midarrow>a\<rightarrow> cnj L"
by (simp add: LIM_eq complex_cnj_diff [symmetric] del: complex_cnj_diff)
lemma LIM_cnj_iff:
fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
- shows "((%x. cnj (f x)) -- a --> cnj L) = (f -- a --> L)"
+ shows "((%x. cnj (f x)) \<midarrow>a\<rightarrow> cnj L) = (f \<midarrow>a\<rightarrow> L)"
by (simp add: LIM_eq complex_cnj_diff [symmetric] del: complex_cnj_diff)
lemma starfun_norm: "( *f* (\<lambda>x. norm (f x))) = (\<lambda>x. hnorm (( *f* f) x))"
@@ -84,7 +84,7 @@
(** much, much easier standard proof **)
lemma CLIM_CRLIM_iff:
fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
- shows "(f -- x --> L) = ((%y. cmod(f y - L)) -- x --> 0)"
+ shows "(f \<midarrow>x\<rightarrow> L) = ((%y. cmod(f y - L)) \<midarrow>x\<rightarrow> 0)"
by (simp add: LIM_eq)
(* so this is nicer nonstandard proof *)
@@ -103,8 +103,8 @@
lemma LIM_CRLIM_Re_Im_iff:
fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
- shows "(f -- a --> L) = ((%x. Re(f x)) -- a --> Re(L) &
- (%x. Im(f x)) -- a --> Im(L))"
+ shows "(f \<midarrow>a\<rightarrow> L) = ((%x. Re(f x)) \<midarrow>a\<rightarrow> Re(L) &
+ (%x. Im(f x)) \<midarrow>a\<rightarrow> Im(L))"
by (simp add: LIM_NSLIM_iff NSLIM_NSCRLIM_Re_Im_iff)
--- a/src/HOL/NSA/HLim.thy Wed Dec 30 11:37:29 2015 +0100
+++ b/src/HOL/NSA/HLim.thy Wed Dec 30 14:05:51 2015 +0100
@@ -136,7 +136,7 @@
subsubsection \<open>Equivalence of @{term filterlim} and @{term NSLIM}\<close>
lemma LIM_NSLIM:
- assumes f: "f -- a --> L" shows "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L"
+ assumes f: "f \<midarrow>a\<rightarrow> 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 \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L" shows "f -- a --> L"
+ assumes f: "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L" shows "f \<midarrow>a\<rightarrow> 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 \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S L)"
+theorem LIM_NSLIM_iff: "(f \<midarrow>x\<rightarrow> L) = (f \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S L)"
by (blast intro: LIM_NSLIM NSLIM_LIM)
@@ -215,7 +215,7 @@
text\<open>Hence, NS continuity can be given
in terms of standard limit\<close>
-lemma isNSCont_LIM_iff: "(isNSCont f a) = (f -- a --> (f a))"
+lemma isNSCont_LIM_iff: "(isNSCont f a) = (f \<midarrow>a\<rightarrow> (f a))"
by (simp add: LIM_NSLIM_iff isNSCont_NSLIM_iff)
text\<open>Moreover, it's trivial now that NS continuity
--- a/src/HOL/Real_Vector_Spaces.thy Wed Dec 30 11:37:29 2015 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy Wed Dec 30 14:05:51 2015 +0100
@@ -1727,31 +1727,31 @@
subsubsection \<open>Limits of Functions\<close>
-lemma LIM_def: "f -- (a::'a::metric_space) --> (L::'b::metric_space) =
+lemma LIM_def: "f \<midarrow>(a::'a::metric_space)\<rightarrow> (L::'b::metric_space) =
(\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & dist x a < s
--> dist (f x) L < r)"
unfolding tendsto_iff eventually_at by simp
lemma metric_LIM_I:
"(\<And>r. 0 < r \<Longrightarrow> \<exists>s>0. \<forall>x. x \<noteq> a \<and> dist x a < s \<longrightarrow> dist (f x) L < r)
- \<Longrightarrow> f -- (a::'a::metric_space) --> (L::'b::metric_space)"
+ \<Longrightarrow> f \<midarrow>(a::'a::metric_space)\<rightarrow> (L::'b::metric_space)"
by (simp add: LIM_def)
lemma metric_LIM_D:
- "\<lbrakk>f -- (a::'a::metric_space) --> (L::'b::metric_space); 0 < r\<rbrakk>
+ "\<lbrakk>f \<midarrow>(a::'a::metric_space)\<rightarrow> (L::'b::metric_space); 0 < r\<rbrakk>
\<Longrightarrow> \<exists>s>0. \<forall>x. x \<noteq> a \<and> dist x a < s \<longrightarrow> dist (f x) L < r"
by (simp add: LIM_def)
lemma metric_LIM_imp_LIM:
- assumes f: "f -- a --> (l::'a::metric_space)"
+ assumes f: "f \<midarrow>a\<rightarrow> (l::'a::metric_space)"
assumes le: "\<And>x. x \<noteq> a \<Longrightarrow> dist (g x) m \<le> dist (f x) l"
- shows "g -- a --> (m::'b::metric_space)"
+ shows "g \<midarrow>a\<rightarrow> (m::'b::metric_space)"
by (rule metric_tendsto_imp_tendsto [OF f]) (auto simp add: eventually_at_topological le)
lemma metric_LIM_equal2:
assumes 1: "0 < R"
assumes 2: "\<And>x. \<lbrakk>x \<noteq> a; dist x a < R\<rbrakk> \<Longrightarrow> f x = g x"
- shows "g -- a --> l \<Longrightarrow> f -- (a::'a::metric_space) --> l"
+ shows "g \<midarrow>a\<rightarrow> l \<Longrightarrow> f \<midarrow>(a::'a::metric_space)\<rightarrow> l"
apply (rule topological_tendstoI)
apply (drule (2) topological_tendstoD)
apply (simp add: eventually_at, safe)
@@ -1761,19 +1761,19 @@
done
lemma metric_LIM_compose2:
- assumes f: "f -- (a::'a::metric_space) --> b"
- assumes g: "g -- b --> c"
+ assumes f: "f \<midarrow>(a::'a::metric_space)\<rightarrow> b"
+ assumes g: "g \<midarrow>b\<rightarrow> c"
assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> f x \<noteq> b"
- shows "(\<lambda>x. g (f x)) -- a --> c"
+ shows "(\<lambda>x. g (f x)) \<midarrow>a\<rightarrow> c"
using inj
by (intro tendsto_compose_eventually[OF g f]) (auto simp: eventually_at)
lemma metric_isCont_LIM_compose2:
fixes f :: "'a :: metric_space \<Rightarrow> _"
assumes f [unfolded isCont_def]: "isCont f a"
- assumes g: "g -- f a --> l"
+ assumes g: "g \<midarrow>f a\<rightarrow> l"
assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> f x \<noteq> f a"
- shows "(\<lambda>x. g (f x)) -- a --> l"
+ shows "(\<lambda>x. g (f x)) \<midarrow>a\<rightarrow> l"
by (rule metric_LIM_compose2 [OF f g inj])
subsection \<open>Complete metric spaces\<close>
--- a/src/HOL/Topological_Spaces.thy Wed Dec 30 11:37:29 2015 +0100
+++ b/src/HOL/Topological_Spaces.thy Wed Dec 30 14:05:51 2015 +0100
@@ -1204,16 +1204,16 @@
abbreviation
LIM :: "('a::topological_space \<Rightarrow> 'b::topological_space) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
- ("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60) where
- "f -- a --> L \<equiv> (f \<longlongrightarrow> L) (at a)"
+ ("((_)/ \<midarrow>(_)/\<rightarrow> (_))" [60, 0, 60] 60) where
+ "f \<midarrow>a\<rightarrow> L \<equiv> (f \<longlongrightarrow> L) (at a)"
-lemma tendsto_within_open: "a \<in> S \<Longrightarrow> open S \<Longrightarrow> (f \<longlongrightarrow> l) (at a within S) \<longleftrightarrow> (f -- a --> l)"
+lemma tendsto_within_open: "a \<in> S \<Longrightarrow> open S \<Longrightarrow> (f \<longlongrightarrow> l) (at a within S) \<longleftrightarrow> (f \<midarrow>a\<rightarrow> l)"
unfolding tendsto_def by (simp add: at_within_open[where S=S])
lemma LIM_const_not_eq[tendsto_intros]:
fixes a :: "'a::perfect_space"
fixes k L :: "'b::t2_space"
- shows "k \<noteq> L \<Longrightarrow> \<not> (\<lambda>x. k) -- a --> L"
+ shows "k \<noteq> L \<Longrightarrow> \<not> (\<lambda>x. k) \<midarrow>a\<rightarrow> L"
by (simp add: tendsto_const_iff)
lemmas LIM_not_zero = LIM_const_not_eq [where L = 0]
@@ -1221,46 +1221,46 @@
lemma LIM_const_eq:
fixes a :: "'a::perfect_space"
fixes k L :: "'b::t2_space"
- shows "(\<lambda>x. k) -- a --> L \<Longrightarrow> k = L"
+ shows "(\<lambda>x. k) \<midarrow>a\<rightarrow> L \<Longrightarrow> k = L"
by (simp add: tendsto_const_iff)
lemma LIM_unique:
fixes a :: "'a::perfect_space" and L M :: "'b::t2_space"
- shows "f -- a --> L \<Longrightarrow> f -- a --> M \<Longrightarrow> L = M"
+ shows "f \<midarrow>a\<rightarrow> L \<Longrightarrow> f \<midarrow>a\<rightarrow> M \<Longrightarrow> L = M"
using at_neq_bot by (rule tendsto_unique)
text \<open>Limits are equal for functions equal except at limit point\<close>
-lemma LIM_equal: "\<forall>x. x \<noteq> a --> (f x = g x) \<Longrightarrow> (f -- a --> l) \<longleftrightarrow> (g -- a --> l)"
+lemma LIM_equal: "\<forall>x. x \<noteq> a --> (f x = g x) \<Longrightarrow> (f \<midarrow>a\<rightarrow> l) \<longleftrightarrow> (g \<midarrow>a\<rightarrow> l)"
unfolding tendsto_def eventually_at_topological by simp
-lemma LIM_cong: "a = b \<Longrightarrow> (\<And>x. x \<noteq> b \<Longrightarrow> f x = g x) \<Longrightarrow> l = m \<Longrightarrow> (f -- a --> l) \<longleftrightarrow> (g -- b --> m)"
+lemma LIM_cong: "a = b \<Longrightarrow> (\<And>x. x \<noteq> b \<Longrightarrow> f x = g x) \<Longrightarrow> l = m \<Longrightarrow> (f \<midarrow>a\<rightarrow> l) \<longleftrightarrow> (g \<midarrow>b\<rightarrow> m)"
by (simp add: LIM_equal)
-lemma LIM_cong_limit: "f -- x --> L \<Longrightarrow> K = L \<Longrightarrow> f -- x --> K"
+lemma LIM_cong_limit: "f \<midarrow>x\<rightarrow> L \<Longrightarrow> K = L \<Longrightarrow> f \<midarrow>x\<rightarrow> K"
by simp
lemma tendsto_at_iff_tendsto_nhds:
- "g -- l --> g l \<longleftrightarrow> (g \<longlongrightarrow> g l) (nhds l)"
+ "g \<midarrow>l\<rightarrow> g l \<longleftrightarrow> (g \<longlongrightarrow> g l) (nhds l)"
unfolding tendsto_def eventually_at_filter
by (intro ext all_cong imp_cong) (auto elim!: eventually_mono)
lemma tendsto_compose:
- "g -- l --> g l \<Longrightarrow> (f \<longlongrightarrow> l) F \<Longrightarrow> ((\<lambda>x. g (f x)) \<longlongrightarrow> g l) F"
+ "g \<midarrow>l\<rightarrow> g l \<Longrightarrow> (f \<longlongrightarrow> l) F \<Longrightarrow> ((\<lambda>x. g (f x)) \<longlongrightarrow> g l) F"
unfolding tendsto_at_iff_tendsto_nhds by (rule filterlim_compose[of g])
-lemma LIM_o: "\<lbrakk>g -- l --> g l; f -- a --> l\<rbrakk> \<Longrightarrow> (g \<circ> f) -- a --> g l"
+lemma LIM_o: "\<lbrakk>g \<midarrow>l\<rightarrow> g l; f \<midarrow>a\<rightarrow> l\<rbrakk> \<Longrightarrow> (g \<circ> f) \<midarrow>a\<rightarrow> g l"
unfolding o_def by (rule tendsto_compose)
lemma tendsto_compose_eventually:
- "g -- l --> m \<Longrightarrow> (f \<longlongrightarrow> l) F \<Longrightarrow> eventually (\<lambda>x. f x \<noteq> l) F \<Longrightarrow> ((\<lambda>x. g (f x)) \<longlongrightarrow> m) F"
+ "g \<midarrow>l\<rightarrow> m \<Longrightarrow> (f \<longlongrightarrow> l) F \<Longrightarrow> eventually (\<lambda>x. f x \<noteq> l) F \<Longrightarrow> ((\<lambda>x. g (f x)) \<longlongrightarrow> m) F"
by (rule filterlim_compose[of g _ "at l"]) (auto simp add: filterlim_at)
lemma LIM_compose_eventually:
- assumes f: "f -- a --> b"
- assumes g: "g -- b --> c"
+ assumes f: "f \<midarrow>a\<rightarrow> b"
+ assumes g: "g \<midarrow>b\<rightarrow> c"
assumes inj: "eventually (\<lambda>x. f x \<noteq> b) (at a)"
- shows "(\<lambda>x. g (f x)) -- a --> c"
+ shows "(\<lambda>x. g (f x)) \<midarrow>a\<rightarrow> c"
using g f inj by (rule tendsto_compose_eventually)
lemma tendsto_compose_filtermap: "((g \<circ> f) \<longlongrightarrow> T) F \<longleftrightarrow> (g \<longlongrightarrow> T) (filtermap f F)"
@@ -1280,19 +1280,19 @@
lemma LIMSEQ_SEQ_conv1:
fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
- assumes f: "f -- a --> l"
+ assumes f: "f \<midarrow>a\<rightarrow> l"
shows "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S \<longlonglongrightarrow> a \<longrightarrow> (\<lambda>n. f (S n)) \<longlonglongrightarrow> l"
using tendsto_compose_eventually [OF f, where F=sequentially] by simp
lemma LIMSEQ_SEQ_conv2:
fixes f :: "'a::first_countable_topology \<Rightarrow> 'b::topological_space"
assumes "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S \<longlonglongrightarrow> a \<longrightarrow> (\<lambda>n. f (S n)) \<longlonglongrightarrow> l"
- shows "f -- a --> l"
+ shows "f \<midarrow>a\<rightarrow> l"
using assms unfolding tendsto_def [where l=l] by (simp add: sequentially_imp_eventually_at)
lemma LIMSEQ_SEQ_conv:
"(\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S \<longlonglongrightarrow> (a::'a::first_countable_topology) \<longrightarrow> (\<lambda>n. X (S n)) \<longlonglongrightarrow> L) =
- (X -- a --> (L::'b::topological_space))"
+ (X \<midarrow>a\<rightarrow> (L::'b::topological_space))"
using LIMSEQ_SEQ_conv2 LIMSEQ_SEQ_conv1 ..
lemma sequentially_imp_eventually_at_left:
@@ -1585,7 +1585,7 @@
continuous (at x within s) (\<lambda>x. g (f x))"
using continuous_within_compose[of x s f g] by (simp add: comp_def)
-lemma continuous_at: "continuous (at x) f \<longleftrightarrow> f -- x --> f x"
+lemma continuous_at: "continuous (at x) f \<longleftrightarrow> f \<midarrow>x\<rightarrow> f x"
using continuous_within[of x UNIV f] by simp
lemma continuous_ident[continuous_intros, simp]: "continuous (at x within S) (\<lambda>x. x)"
@@ -1601,7 +1601,7 @@
abbreviation isCont :: "('a::t2_space \<Rightarrow> 'b::topological_space) \<Rightarrow> 'a \<Rightarrow> bool" where
"isCont f a \<equiv> continuous (at a) f"
-lemma isCont_def: "isCont f a \<longleftrightarrow> f -- a --> f a"
+lemma isCont_def: "isCont f a \<longleftrightarrow> f \<midarrow>a\<rightarrow> f a"
by (rule continuous_at)
lemma continuous_at_imp_continuous_at_within: "isCont f x \<Longrightarrow> continuous (at x within s) f"
--- a/src/HOL/Transcendental.thy Wed Dec 30 11:37:29 2015 +0100
+++ b/src/HOL/Transcendental.thy Wed Dec 30 14:05:51 2015 +0100
@@ -564,19 +564,19 @@
fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
assumes k: "0 < (k::real)"
and le: "\<And>h. \<lbrakk>h \<noteq> 0; norm h < k\<rbrakk> \<Longrightarrow> norm (f h) \<le> K * norm h"
- shows "f -- 0 --> 0"
+ shows "f \<midarrow>0\<rightarrow> 0"
proof (rule tendsto_norm_zero_cancel)
- show "(\<lambda>h. norm (f h)) -- 0 --> 0"
+ show "(\<lambda>h. norm (f h)) \<midarrow>0\<rightarrow> 0"
proof (rule real_tendsto_sandwich)
show "eventually (\<lambda>h. 0 \<le> norm (f h)) (at 0)"
by simp
show "eventually (\<lambda>h. norm (f h) \<le> K * norm h) (at 0)"
using k by (auto simp add: eventually_at dist_norm le)
- show "(\<lambda>h. 0) -- (0::'a) --> (0::real)"
+ show "(\<lambda>h. 0) \<midarrow>(0::'a)\<rightarrow> (0::real)"
by (rule tendsto_const)
- have "(\<lambda>h. K * norm h) -- (0::'a) --> K * norm (0::'a)"
+ have "(\<lambda>h. K * norm h) \<midarrow>(0::'a)\<rightarrow> K * norm (0::'a)"
by (intro tendsto_intros)
- then show "(\<lambda>h. K * norm h) -- (0::'a) --> 0"
+ then show "(\<lambda>h. K * norm h) \<midarrow>(0::'a)\<rightarrow> 0"
by simp
qed
qed
@@ -586,7 +586,7 @@
assumes k: "0 < (k::real)"
assumes f: "summable f"
assumes le: "\<And>h n. \<lbrakk>h \<noteq> 0; norm h < k\<rbrakk> \<Longrightarrow> norm (g h n) \<le> f n * norm h"
- shows "(\<lambda>h. suminf (g h)) -- 0 --> 0"
+ shows "(\<lambda>h. suminf (g h)) \<midarrow>0\<rightarrow> 0"
proof (rule lemma_termdiff4 [OF k])
fix h::'a
assume "h \<noteq> 0" and "norm h < k"
@@ -615,7 +615,7 @@
assumes 1: "summable (\<lambda>n. diffs (diffs c) n * K ^ n)"
and 2: "norm x < norm K"
shows "(\<lambda>h. \<Sum>n. c n * (((x + h) ^ n - x^n) / h
- - of_nat n * x ^ (n - Suc 0))) -- 0 --> 0"
+ - of_nat n * x ^ (n - Suc 0))) \<midarrow>0\<rightarrow> 0"
proof -
from dense [OF 2]
obtain r where r1: "norm x < r" and r2: "r < norm K" by fast
@@ -682,7 +682,7 @@
unfolding DERIV_def
proof (rule LIM_zero_cancel)
show "(\<lambda>h. (suminf (\<lambda>n. c n * (x + h) ^ n) - suminf (\<lambda>n. c n * x^n)) / h
- - suminf (\<lambda>n. diffs c n * x^n)) -- 0 --> 0"
+ - suminf (\<lambda>n. diffs c n * x^n)) \<midarrow>0\<rightarrow> 0"
proof (rule LIM_equal2)
show "0 < norm K - norm x" using 4 by (simp add: less_diff_eq)
next
@@ -702,7 +702,7 @@
(\<Sum>n. c n * (((x + h) ^ n - x^n) / h - of_nat n * x ^ (n - Suc 0)))"
by (simp add: algebra_simps)
next
- show "(\<lambda>h. \<Sum>n. c n * (((x + h) ^ n - x^n) / h - of_nat n * x ^ (n - Suc 0))) -- 0 --> 0"
+ show "(\<lambda>h. \<Sum>n. c n * (((x + h) ^ n - x^n) / h - of_nat n * x ^ (n - Suc 0))) \<midarrow>0\<rightarrow> 0"
by (rule termdiffs_aux [OF 3 4])
qed
qed
@@ -4068,7 +4068,7 @@
"continuous (at x within s) f \<Longrightarrow> cos (f x) \<noteq> 0 \<Longrightarrow> continuous (at x within s) (\<lambda>x. tan (f x))"
unfolding continuous_within by (rule tendsto_tan)
-lemma LIM_cos_div_sin: "(\<lambda>x. cos(x)/sin(x)) -- pi/2 --> 0"
+lemma LIM_cos_div_sin: "(\<lambda>x. cos(x)/sin(x)) \<midarrow>pi/2\<rightarrow> 0"
by (rule LIM_cong_limit, (rule tendsto_intros)+, simp_all)
lemma lemma_tan_total: "0 < y ==> \<exists>x. 0 < x & x < pi/2 & y < tan x"
@@ -5572,7 +5572,7 @@
}
then have wnz: "\<And>w. w \<noteq> 0 \<Longrightarrow> (\<Sum>i\<le>n. c (Suc i) * w^i) = 0"
using Suc by auto
- then have "(\<lambda>h. \<Sum>i\<le>n. c (Suc i) * h^i) -- 0 --> 0"
+ then have "(\<lambda>h. \<Sum>i\<le>n. c (Suc i) * h^i) \<midarrow>0\<rightarrow> 0"
by (simp cong: LIM_cong) \<comment>\<open>the case @{term"w=0"} by continuity\<close>
then have "(\<Sum>i\<le>n. c (Suc i) * 0^i) = 0"
using isCont_polynom [of 0 "\<lambda>i. c (Suc i)" n] LIM_unique