1.1 --- a/src/HOL/SEQ.thy	Sat Aug 13 18:10:14 2011 -0700
     1.2 +++ b/src/HOL/SEQ.thy	Sun Aug 14 07:54:24 2011 -0700
     1.3 @@ -441,7 +441,7 @@
     1.4  lemma LIMSEQ_pow:
     1.5    fixes a :: "'a::{power, real_normed_algebra}"
     1.6    shows "X ----> a \<Longrightarrow> (\<lambda>n. (X n) ^ m) ----> a ^ m"
     1.7 -by (induct m) (simp_all add: LIMSEQ_const LIMSEQ_mult)
     1.8 +  by (rule tendsto_power)
     1.9  
    1.10  lemma LIMSEQ_setsum:
    1.11    fixes L :: "'a \<Rightarrow> 'b::real_normed_vector"
    1.12 @@ -453,23 +453,7 @@
    1.13    fixes L :: "'a \<Rightarrow> 'b::{real_normed_algebra,comm_ring_1}"
    1.14    assumes n: "\<And>n. n \<in> S \<Longrightarrow> X n ----> L n"
    1.15    shows "(\<lambda>m. \<Prod>n\<in>S. X n m) ----> (\<Prod>n\<in>S. L n)"
    1.16 -proof (cases "finite S")
    1.17 -  case True
    1.18 -  thus ?thesis using n
    1.19 -  proof (induct)
    1.20 -    case empty
    1.21 -    show ?case
    1.22 -      by (simp add: LIMSEQ_const)
    1.23 -  next
    1.24 -    case insert
    1.25 -    thus ?case
    1.26 -      by (simp add: LIMSEQ_mult)
    1.27 -  qed
    1.28 -next
    1.29 -  case False
    1.30 -  thus ?thesis
    1.31 -    by (simp add: setprod_def LIMSEQ_const)
    1.32 -qed
    1.33 +  using assms by (rule tendsto_setprod)
    1.34  
    1.35  lemma LIMSEQ_add_const: (* FIXME: delete *)
    1.36    fixes a :: "'a::real_normed_vector"
    1.37 @@ -501,13 +485,13 @@
    1.38  lemma LIMSEQ_norm_zero:
    1.39    fixes X :: "nat \<Rightarrow> 'a::real_normed_vector"
    1.40    shows "((\<lambda>n. norm (X n)) ----> 0) \<longleftrightarrow> (X ----> 0)"
    1.41 -by (simp add: LIMSEQ_iff)
    1.42 +  by (rule tendsto_norm_zero_iff)
    1.43  
    1.44  lemma LIMSEQ_rabs_zero: "((%n. \<bar>f n\<bar>) ----> 0) = (f ----> (0::real))"
    1.45 -by (simp add: LIMSEQ_iff)
    1.46 +  by (rule tendsto_rabs_zero_iff)
    1.47  
    1.48  lemma LIMSEQ_imp_rabs: "f ----> (l::real) ==> (%n. \<bar>f n\<bar>) ----> \<bar>l\<bar>"
    1.49 -by (drule LIMSEQ_norm, simp)
    1.50 +  by (rule tendsto_rabs)
    1.51  
    1.52  text{*An unbounded sequence's inverse tends to 0*}
    1.53