# HG changeset patch
# User huffman
# Date 1313352297 25200
# Node ID 1d2bf1f240ac3cd70b86eab23412c0f868287e34
# Parent  ea99698c207042e9f516e18042bed0d29bfd76d4
generalize lemma convergent_subseq_convergent

diff -r ea99698c2070 -r 1d2bf1f240ac src/HOL/SEQ.thy
--- a/src/HOL/SEQ.thy	Sun Aug 14 11:44:12 2011 -0700
+++ b/src/HOL/SEQ.thy	Sun Aug 14 13:04:57 2011 -0700
@@ -691,9 +691,13 @@
 apply (blast intro: seq_suble le_trans dest!: spec) 
 done
 
+lemma convergent_subseq_convergent:
+  "\<lbrakk>convergent X; subseq f\<rbrakk> \<Longrightarrow> convergent (X o f)"
+  unfolding convergent_def by (auto intro: LIMSEQ_subseq_LIMSEQ)
+
+
 subsection {* Bounded Monotonic Sequences *}
 
-
 text{*Bounded Sequence*}
 
 lemma BseqD: "Bseq X ==> \<exists>K. 0 < K & (\<forall>n. norm (X n) \<le> K)"
@@ -1007,11 +1011,6 @@
   shows "Cauchy X = convergent X"
 by (fast intro: Cauchy_convergent convergent_Cauchy)
 
-lemma convergent_subseq_convergent:
-  fixes X :: "nat \<Rightarrow> 'a::complete_space"
-  shows "\<lbrakk> convergent X; subseq f \<rbrakk> \<Longrightarrow> convergent (X o f)"
-  by (simp add: Cauchy_subseq_Cauchy Cauchy_convergent_iff [symmetric])
-
 text {*
 Proof that Cauchy sequences converge based on the one from
 http://pirate.shu.edu/~wachsmut/ira/numseq/proofs/cauconv.html