src/HOL/SEQ.thy
changeset 31392 69570155ddf8
parent 31355 3d18766ddc4b
child 31403 0baaad47cef2
     1.1 --- a/src/HOL/SEQ.thy	Tue Jun 02 15:37:59 2009 -0700
     1.2 +++ b/src/HOL/SEQ.thy	Tue Jun 02 17:03:22 2009 -0700
     1.3 @@ -13,10 +13,6 @@
     1.4  begin
     1.5  
     1.6  definition
     1.7 -  sequentially :: "nat filter" where
     1.8 -  [code del]: "sequentially = Abs_filter (\<lambda>P. \<exists>N. \<forall>n\<ge>N. P n)"
     1.9 -
    1.10 -definition
    1.11    Zseq :: "[nat \<Rightarrow> 'a::real_normed_vector] \<Rightarrow> bool" where
    1.12      --{*Standard definition of sequence converging to zero*}
    1.13    [code del]: "Zseq X = (\<forall>r>0. \<exists>no. \<forall>n\<ge>no. norm (X n) < r)"
    1.14 @@ -71,24 +67,6 @@
    1.15    [code del]: "Cauchy X = (\<forall>e>0. \<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. dist (X m) (X n) < e)"
    1.16  
    1.17  
    1.18 -subsection {* Sequentially *}
    1.19 -
    1.20 -lemma eventually_sequentially:
    1.21 -  "eventually P sequentially \<longleftrightarrow> (\<exists>N. \<forall>n\<ge>N. P n)"
    1.22 -unfolding sequentially_def
    1.23 -apply (rule eventually_Abs_filter)
    1.24 -apply simp
    1.25 -apply (clarify, rule_tac x=N in exI, simp)
    1.26 -apply (clarify, rename_tac M N)
    1.27 -apply (rule_tac x="max M N" in exI, simp)
    1.28 -done
    1.29 -
    1.30 -lemma Zseq_conv_Zfun: "Zseq X \<longleftrightarrow> Zfun X sequentially"
    1.31 -unfolding Zseq_def Zfun_def eventually_sequentially ..
    1.32 -
    1.33 -lemma LIMSEQ_conv_tendsto: "(X ----> L) \<longleftrightarrow> tendsto X L sequentially"
    1.34 -unfolding LIMSEQ_def tendsto_def eventually_sequentially ..
    1.35 -
    1.36  subsection {* Bounded Sequences *}
    1.37  
    1.38  lemma BseqI': assumes K: "\<And>n. norm (X n) \<le> K" shows "Bseq X"
    1.39 @@ -150,6 +128,9 @@
    1.40    "\<lbrakk>Zseq X; 0 < r\<rbrakk> \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. norm (X n) < r"
    1.41  unfolding Zseq_def by simp
    1.42  
    1.43 +lemma Zseq_conv_Zfun: "Zseq X \<longleftrightarrow> Zfun X sequentially"
    1.44 +unfolding Zseq_def Zfun_def eventually_sequentially ..
    1.45 +
    1.46  lemma Zseq_zero: "Zseq (\<lambda>n. 0)"
    1.47  unfolding Zseq_def by simp
    1.48  
    1.49 @@ -212,6 +193,9 @@
    1.50  
    1.51  subsection {* Limits of Sequences *}
    1.52  
    1.53 +lemma LIMSEQ_conv_tendsto: "(X ----> L) \<longleftrightarrow> tendsto X L sequentially"
    1.54 +unfolding LIMSEQ_def tendsto_def eventually_sequentially ..
    1.55 +
    1.56  lemma LIMSEQ_iff:
    1.57    fixes L :: "'a::real_normed_vector"
    1.58    shows "(X ----> L) = (\<forall>r>0. \<exists>no. \<forall>n \<ge> no. norm (X n - L) < r)"