make (X ----> L) an abbreviation for (X ---> L) sequentially

--- a/src/HOL/Library/Product_Vector.thy	Tue May 04 09:56:34 2010 -0700
+++ b/src/HOL/Library/Product_Vector.thy	Tue May 04 10:06:05 2010 -0700
@@ -312,18 +312,6 @@
        (simp add: subsetD [OF `A \<times> B \<subseteq> S`])
 qed
 
-lemma LIMSEQ_fst: "(X ----> a) \<Longrightarrow> (\<lambda>n. fst (X n)) ----> fst a"
-unfolding LIMSEQ_conv_tendsto by (rule tendsto_fst)
-
-lemma LIMSEQ_snd: "(X ----> a) \<Longrightarrow> (\<lambda>n. snd (X n)) ----> snd a"
-unfolding LIMSEQ_conv_tendsto by (rule tendsto_snd)
-
-lemma LIMSEQ_Pair:
-  assumes "X ----> a" and "Y ----> b"
-  shows "(\<lambda>n. (X n, Y n)) ----> (a, b)"
-using assms unfolding LIMSEQ_conv_tendsto
-by (rule tendsto_Pair)
-
 lemma LIM_fst: "f -- x --> a \<Longrightarrow> (\<lambda>x. fst (f x)) -- x --> fst a"
 unfolding LIM_conv_tendsto by (rule tendsto_fst)
 
@@ -374,7 +362,7 @@
     using Cauchy_snd [OF `Cauchy X`]
     by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff)
   have "X ----> (lim (\<lambda>n. fst (X n)), lim (\<lambda>n. snd (X n)))"
-    using LIMSEQ_Pair [OF 1 2] by simp
+    using tendsto_Pair [OF 1 2] by simp
   then show "convergent X"
     by (rule convergentI)
 qed

--- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Tue May 04 09:56:34 2010 -0700
+++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Tue May 04 10:06:05 2010 -0700
@@ -313,10 +313,6 @@
 
 end
 
-lemma LIMSEQ_Cart_nth:
-  "(X ----> a) \<Longrightarrow> (\<lambda>n. X n $ i) ----> a $ i"
-unfolding LIMSEQ_conv_tendsto by (rule tendsto_Cart_nth)
-
 lemma LIM_Cart_nth:
   "(f -- x --> y) \<Longrightarrow> (\<lambda>x. f x $ i) -- x --> y $ i"
 unfolding LIM_conv_tendsto by (rule tendsto_Cart_nth)
@@ -325,11 +321,6 @@
   "Cauchy (\<lambda>n. X n) \<Longrightarrow> Cauchy (\<lambda>n. X n $ i)"
 unfolding Cauchy_def by (fast intro: le_less_trans [OF dist_nth_le])
 
-lemma LIMSEQ_vector:
-  assumes "\<And>i. (\<lambda>n. X n $ i) ----> (a $ i)"
-  shows "X ----> a"
-using assms unfolding LIMSEQ_conv_tendsto by (rule tendsto_vector)
-
 lemma Cauchy_vector:
   fixes X :: "nat \<Rightarrow> 'a::metric_space ^ 'n"
   assumes X: "\<And>i. Cauchy (\<lambda>n. X n $ i)"
@@ -371,7 +362,7 @@
     using Cauchy_Cart_nth [OF `Cauchy X`]
     by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff)
   hence "X ----> Cart_lambda (\<lambda>i. lim (\<lambda>n. X n $ i))"
-    by (simp add: LIMSEQ_vector)
+    by (simp add: tendsto_vector)
   then show "convergent X"
     by (rule convergentI)
 qed

--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue May 04 09:56:34 2010 -0700
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue May 04 10:06:05 2010 -0700
@@ -2507,15 +2507,14 @@
   ultimately have "\<exists>l\<in>closure (range f). (f ---> l) sequentially"
     using `Cauchy f` unfolding complete_def by auto
   then show "convergent f"
-    unfolding convergent_def LIMSEQ_conv_tendsto [symmetric] by auto
+    unfolding convergent_def by auto
 qed
 
 lemma complete_univ: "complete (UNIV :: 'a::complete_space set)"
 proof(simp add: complete_def, rule, rule)
   fix f :: "nat \<Rightarrow> 'a" assume "Cauchy f"
   hence "convergent f" by (rule Cauchy_convergent)
-  hence "\<exists>l. f ----> l" unfolding convergent_def .  
-  thus "\<exists>l. (f ---> l) sequentially" unfolding LIMSEQ_conv_tendsto .
+  thus "\<exists>l. f ----> l" unfolding convergent_def .  
 qed
 
 lemma complete_imp_closed: assumes "complete s" shows "closed s"

--- a/src/HOL/SEQ.thy	Tue May 04 09:56:34 2010 -0700
+++ b/src/HOL/SEQ.thy	Tue May 04 10:06:05 2010 -0700
@@ -13,11 +13,10 @@
 imports Limits
 begin
 
-definition
+abbreviation
   LIMSEQ :: "[nat \<Rightarrow> 'a::metric_space, 'a] \<Rightarrow> bool"
     ("((_)/ ----> (_))" [60, 60] 60) where
-    --{*Standard definition of convergence of sequence*}
-  [code del]: "X ----> L = (\<forall>r>0. \<exists>no. \<forall>n\<ge>no. dist (X n) L < r)"
+  "X ----> L \<equiv> (X ---> L) sequentially"
 
 definition
   lim :: "(nat \<Rightarrow> 'a::metric_space) \<Rightarrow> 'a" where
@@ -119,8 +118,8 @@
 lemma [trans]: "X=Y ==> Y ----> z ==> X ----> z"
   by simp
 
-lemma LIMSEQ_conv_tendsto: "(X ----> L) \<longleftrightarrow> (X ---> L) sequentially"
-unfolding LIMSEQ_def tendsto_iff eventually_sequentially ..
+lemma LIMSEQ_def: "X ----> L = (\<forall>r>0. \<exists>no. \<forall>n\<ge>no. dist (X n) L < r)"
+unfolding tendsto_iff eventually_sequentially ..
 
 lemma LIMSEQ_iff:
   fixes L :: "'a::real_normed_vector"
@@ -128,10 +127,10 @@
 unfolding LIMSEQ_def dist_norm ..
 
 lemma LIMSEQ_iff_nz: "X ----> L = (\<forall>r>0. \<exists>no>0. \<forall>n\<ge>no. dist (X n) L < r)"
-  by (auto simp add: LIMSEQ_def) (metis Suc_leD zero_less_Suc)  
+  unfolding LIMSEQ_def by (metis Suc_leD zero_less_Suc)
 
 lemma LIMSEQ_Zfun_iff: "((\<lambda>n. X n) ----> L) = Zfun (\<lambda>n. X n - L) sequentially"
-by (simp only: LIMSEQ_iff Zfun_def eventually_sequentially)
+by (rule tendsto_Zfun_iff)
 
 lemma metric_LIMSEQ_I:
   "(\<And>r. 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. dist (X n) L < r) \<Longrightarrow> X ----> L"
@@ -152,7 +151,7 @@
 by (simp add: LIMSEQ_iff)
 
 lemma LIMSEQ_const: "(\<lambda>n. k) ----> k"
-by (simp add: LIMSEQ_def)
+by (rule tendsto_const)
 
 lemma LIMSEQ_const_iff: "(\<lambda>n. k) ----> l \<longleftrightarrow> k = l"
 apply (safe intro!: LIMSEQ_const)
@@ -165,7 +164,7 @@
 lemma LIMSEQ_norm:
   fixes a :: "'a::real_normed_vector"
   shows "X ----> a \<Longrightarrow> (\<lambda>n. norm (X n)) ----> norm a"
-unfolding LIMSEQ_conv_tendsto by (rule tendsto_norm)
+by (rule tendsto_norm)
 
 lemma LIMSEQ_ignore_initial_segment:
   "f ----> a \<Longrightarrow> (\<lambda>n. f (n + k)) ----> a"
@@ -203,22 +202,22 @@
 lemma LIMSEQ_add:
   fixes a b :: "'a::real_normed_vector"
   shows "\<lbrakk>X ----> a; Y ----> b\<rbrakk> \<Longrightarrow> (\<lambda>n. X n + Y n) ----> a + b"
-unfolding LIMSEQ_conv_tendsto by (rule tendsto_add)
+by (rule tendsto_add)
 
 lemma LIMSEQ_minus:
   fixes a :: "'a::real_normed_vector"
   shows "X ----> a \<Longrightarrow> (\<lambda>n. - X n) ----> - a"
-unfolding LIMSEQ_conv_tendsto by (rule tendsto_minus)
+by (rule tendsto_minus)
 
 lemma LIMSEQ_minus_cancel:
   fixes a :: "'a::real_normed_vector"
   shows "(\<lambda>n. - X n) ----> - a \<Longrightarrow> X ----> a"
-by (drule LIMSEQ_minus, simp)
+by (rule tendsto_minus_cancel)
 
 lemma LIMSEQ_diff:
   fixes a b :: "'a::real_normed_vector"
   shows "\<lbrakk>X ----> a; Y ----> b\<rbrakk> \<Longrightarrow> (\<lambda>n. X n - Y n) ----> a - b"
-unfolding LIMSEQ_conv_tendsto by (rule tendsto_diff)
+by (rule tendsto_diff)
 
 lemma LIMSEQ_unique: "\<lbrakk>X ----> a; X ----> b\<rbrakk> \<Longrightarrow> a = b"
 apply (rule ccontr)
@@ -233,16 +232,16 @@
 
 lemma (in bounded_linear) LIMSEQ:
   "X ----> a \<Longrightarrow> (\<lambda>n. f (X n)) ----> f a"
-unfolding LIMSEQ_conv_tendsto by (rule tendsto)
+by (rule tendsto)
 
 lemma (in bounded_bilinear) LIMSEQ:
   "\<lbrakk>X ----> a; Y ----> b\<rbrakk> \<Longrightarrow> (\<lambda>n. X n ** Y n) ----> a ** b"
-unfolding LIMSEQ_conv_tendsto by (rule tendsto)
+by (rule tendsto)
 
 lemma LIMSEQ_mult:
   fixes a b :: "'a::real_normed_algebra"
   shows "[| X ----> a; Y ----> b |] ==> (%n. X n * Y n) ----> a * b"
-by (rule mult.LIMSEQ)
+by (rule mult.tendsto)
 
 lemma increasing_LIMSEQ:
   fixes f :: "nat \<Rightarrow> real"
@@ -287,19 +286,17 @@
 lemma Bseq_inverse:
   fixes a :: "'a::real_normed_div_algebra"
   shows "\<lbrakk>X ----> a; a \<noteq> 0\<rbrakk> \<Longrightarrow> Bseq (\<lambda>n. inverse (X n))"
-unfolding LIMSEQ_conv_tendsto Bseq_conv_Bfun
-by (rule Bfun_inverse)
+unfolding Bseq_conv_Bfun by (rule Bfun_inverse)
 
 lemma LIMSEQ_inverse:
   fixes a :: "'a::real_normed_div_algebra"
   shows "\<lbrakk>X ----> a; a \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>n. inverse (X n)) ----> inverse a"
-unfolding LIMSEQ_conv_tendsto
 by (rule tendsto_inverse)
 
 lemma LIMSEQ_divide:
   fixes a b :: "'a::real_normed_field"
   shows "\<lbrakk>X ----> a; Y ----> b; b \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>n. X n / Y n) ----> a / b"
-by (simp add: LIMSEQ_mult LIMSEQ_inverse divide_inverse)
+by (rule tendsto_divide)
 
 lemma LIMSEQ_pow:
   fixes a :: "'a::{power, real_normed_algebra}"
@@ -310,7 +307,7 @@
   fixes L :: "'a \<Rightarrow> 'b::real_normed_vector"
   assumes n: "\<And>n. n \<in> S \<Longrightarrow> X n ----> L n"
   shows "(\<lambda>m. \<Sum>n\<in>S. X n m) ----> (\<Sum>n\<in>S. L n)"
-using n unfolding LIMSEQ_conv_tendsto by (rule tendsto_setsum)
+using assms by (rule tendsto_setsum)
 
 lemma LIMSEQ_setprod:
   fixes L :: "'a \<Rightarrow> 'b::{real_normed_algebra,comm_ring_1}"
@@ -334,21 +331,21 @@
     by (simp add: setprod_def LIMSEQ_const)
 qed
 
-lemma LIMSEQ_add_const:
+lemma LIMSEQ_add_const: (* FIXME: delete *)
   fixes a :: "'a::real_normed_vector"
   shows "f ----> a ==> (%n.(f n + b)) ----> a + b"
-by (simp add: LIMSEQ_add LIMSEQ_const)
+by (intro tendsto_intros)
 
 (* FIXME: delete *)
 lemma LIMSEQ_add_minus:
   fixes a b :: "'a::real_normed_vector"
   shows "[| X ----> a; Y ----> b |] ==> (%n. X n + -Y n) ----> a + -b"
-by (simp only: LIMSEQ_add LIMSEQ_minus)
+by (intro tendsto_intros)
 
-lemma LIMSEQ_diff_const:
+lemma LIMSEQ_diff_const: (* FIXME: delete *)
   fixes a b :: "'a::real_normed_vector"
   shows "f ----> a ==> (%n.(f n  - b)) ----> a - b"
-by (simp add: LIMSEQ_diff LIMSEQ_const)
+by (intro tendsto_intros)
 
 lemma LIMSEQ_diff_approach_zero:
   fixes L :: "'a::real_normed_vector"

--- a/src/HOL/Series.thy	Tue May 04 09:56:34 2010 -0700
+++ b/src/HOL/Series.thy	Tue May 04 10:06:05 2010 -0700
@@ -100,7 +100,7 @@
 
 lemma summable_sums: "summable f ==> f sums (suminf f)"
 apply (simp add: summable_def suminf_def sums_def)
-apply (blast intro: theI LIMSEQ_unique)
+apply (fast intro: theI LIMSEQ_unique)
 done
 
 lemma summable_sumr_LIMSEQ_suminf: 
@@ -701,7 +701,7 @@
     apply (auto simp add: norm_mult_ineq)
     done
   hence 2: "(\<lambda>n. setsum ?g (?S1 n) - setsum ?g (?S2 n)) ----> 0"
-    unfolding LIMSEQ_conv_tendsto tendsto_Zfun_iff diff_0_right
+    unfolding tendsto_Zfun_iff diff_0_right
     by (simp only: setsum_diff finite_S1 S2_le_S1)
 
   with 1 have "(\<lambda>n. setsum ?g (?S2 n)) ----> (\<Sum>k. a k) * (\<Sum>k. b k)"