src/HOL/SEQ.thy
changeset 36657 f376af79f6b7
parent 36625 2ba6525f9905
child 36660 1cc4ab4b7ff7
     1.1 --- a/src/HOL/SEQ.thy	Mon May 03 18:40:48 2010 -0700
     1.2 +++ b/src/HOL/SEQ.thy	Mon May 03 20:42:58 2010 -0700
     1.3 @@ -14,11 +14,6 @@
     1.4  begin
     1.5  
     1.6  definition
     1.7 -  Zseq :: "[nat \<Rightarrow> 'a::real_normed_vector] \<Rightarrow> bool" where
     1.8 -    --{*Standard definition of sequence converging to zero*}
     1.9 -  [code del]: "Zseq X = (\<forall>r>0. \<exists>no. \<forall>n\<ge>no. norm (X n) < r)"
    1.10 -
    1.11 -definition
    1.12    LIMSEQ :: "[nat \<Rightarrow> 'a::metric_space, 'a] \<Rightarrow> bool"
    1.13      ("((_)/ ----> (_))" [60, 60] 60) where
    1.14      --{*Standard definition of convergence of sequence*}
    1.15 @@ -119,79 +114,6 @@
    1.16  done
    1.17  
    1.18  
    1.19 -subsection {* Sequences That Converge to Zero *}
    1.20 -
    1.21 -lemma ZseqI:
    1.22 -  "(\<And>r. 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. norm (X n) < r) \<Longrightarrow> Zseq X"
    1.23 -unfolding Zseq_def by simp
    1.24 -
    1.25 -lemma ZseqD:
    1.26 -  "\<lbrakk>Zseq X; 0 < r\<rbrakk> \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. norm (X n) < r"
    1.27 -unfolding Zseq_def by simp
    1.28 -
    1.29 -lemma Zseq_conv_Zfun: "Zseq X \<longleftrightarrow> Zfun X sequentially"
    1.30 -unfolding Zseq_def Zfun_def eventually_sequentially ..
    1.31 -
    1.32 -lemma Zseq_zero: "Zseq (\<lambda>n. 0)"
    1.33 -unfolding Zseq_def by simp
    1.34 -
    1.35 -lemma Zseq_const_iff: "Zseq (\<lambda>n. k) = (k = 0)"
    1.36 -unfolding Zseq_def by force
    1.37 -
    1.38 -lemma Zseq_norm_iff: "Zseq (\<lambda>n. norm (X n)) = Zseq (\<lambda>n. X n)"
    1.39 -unfolding Zseq_def by simp
    1.40 -
    1.41 -lemma Zseq_imp_Zseq:
    1.42 -  assumes X: "Zseq X"
    1.43 -  assumes Y: "\<And>n. norm (Y n) \<le> norm (X n) * K"
    1.44 -  shows "Zseq (\<lambda>n. Y n)"
    1.45 -using X Y Zfun_imp_Zfun [of X sequentially Y K]
    1.46 -unfolding Zseq_conv_Zfun by simp
    1.47 -
    1.48 -lemma Zseq_le: "\<lbrakk>Zseq Y; \<forall>n. norm (X n) \<le> norm (Y n)\<rbrakk> \<Longrightarrow> Zseq X"
    1.49 -by (erule_tac K="1" in Zseq_imp_Zseq, simp)
    1.50 -
    1.51 -lemma Zseq_add:
    1.52 -  "Zseq X \<Longrightarrow> Zseq Y \<Longrightarrow> Zseq (\<lambda>n. X n + Y n)"
    1.53 -unfolding Zseq_conv_Zfun by (rule Zfun_add)
    1.54 -
    1.55 -lemma Zseq_minus: "Zseq X \<Longrightarrow> Zseq (\<lambda>n. - X n)"
    1.56 -unfolding Zseq_def by simp
    1.57 -
    1.58 -lemma Zseq_diff: "\<lbrakk>Zseq X; Zseq Y\<rbrakk> \<Longrightarrow> Zseq (\<lambda>n. X n - Y n)"
    1.59 -by (simp only: diff_minus Zseq_add Zseq_minus)
    1.60 -
    1.61 -lemma (in bounded_linear) Zseq:
    1.62 -  "Zseq X \<Longrightarrow> Zseq (\<lambda>n. f (X n))"
    1.63 -unfolding Zseq_conv_Zfun by (rule Zfun)
    1.64 -
    1.65 -lemma (in bounded_bilinear) Zseq:
    1.66 -  "Zseq X \<Longrightarrow> Zseq Y \<Longrightarrow> Zseq (\<lambda>n. X n ** Y n)"
    1.67 -unfolding Zseq_conv_Zfun by (rule Zfun)
    1.68 -
    1.69 -lemma (in bounded_bilinear) Zseq_prod_Bseq:
    1.70 -  "Zseq X \<Longrightarrow> Bseq Y \<Longrightarrow> Zseq (\<lambda>n. X n ** Y n)"
    1.71 -unfolding Zseq_conv_Zfun Bseq_conv_Bfun
    1.72 -by (rule Zfun_prod_Bfun)
    1.73 -
    1.74 -lemma (in bounded_bilinear) Bseq_prod_Zseq:
    1.75 -  "Bseq X \<Longrightarrow> Zseq Y \<Longrightarrow> Zseq (\<lambda>n. X n ** Y n)"
    1.76 -unfolding Zseq_conv_Zfun Bseq_conv_Bfun
    1.77 -by (rule Bfun_prod_Zfun)
    1.78 -
    1.79 -lemma (in bounded_bilinear) Zseq_left:
    1.80 -  "Zseq X \<Longrightarrow> Zseq (\<lambda>n. X n ** a)"
    1.81 -by (rule bounded_linear_left [THEN bounded_linear.Zseq])
    1.82 -
    1.83 -lemma (in bounded_bilinear) Zseq_right:
    1.84 -  "Zseq X \<Longrightarrow> Zseq (\<lambda>n. a ** X n)"
    1.85 -by (rule bounded_linear_right [THEN bounded_linear.Zseq])
    1.86 -
    1.87 -lemmas Zseq_mult = mult.Zseq
    1.88 -lemmas Zseq_mult_right = mult.Zseq_right
    1.89 -lemmas Zseq_mult_left = mult.Zseq_left
    1.90 -
    1.91 -
    1.92  subsection {* Limits of Sequences *}
    1.93  
    1.94  lemma [trans]: "X=Y ==> Y ----> z ==> X ----> z"
    1.95 @@ -208,8 +130,8 @@
    1.96  lemma LIMSEQ_iff_nz: "X ----> L = (\<forall>r>0. \<exists>no>0. \<forall>n\<ge>no. dist (X n) L < r)"
    1.97    by (auto simp add: LIMSEQ_def) (metis Suc_leD zero_less_Suc)  
    1.98  
    1.99 -lemma LIMSEQ_Zseq_iff: "((\<lambda>n. X n) ----> L) = Zseq (\<lambda>n. X n - L)"
   1.100 -by (simp only: LIMSEQ_iff Zseq_def)
   1.101 +lemma LIMSEQ_Zfun_iff: "((\<lambda>n. X n) ----> L) = Zfun (\<lambda>n. X n - L) sequentially"
   1.102 +by (simp only: LIMSEQ_iff Zfun_def eventually_sequentially)
   1.103  
   1.104  lemma metric_LIMSEQ_I:
   1.105    "(\<And>r. 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. dist (X n) L < r) \<Longrightarrow> X ----> L"
   1.106 @@ -1380,7 +1302,7 @@
   1.107    fixes x :: "'a::{real_normed_algebra_1}"
   1.108    shows "norm x < 1 \<Longrightarrow> (\<lambda>n. x ^ n) ----> 0"
   1.109  apply (drule LIMSEQ_realpow_zero [OF norm_ge_zero])
   1.110 -apply (simp only: LIMSEQ_Zseq_iff, erule Zseq_le)
   1.111 +apply (simp only: LIMSEQ_Zfun_iff, erule Zfun_le)
   1.112  apply (simp add: power_abs norm_power_ineq)
   1.113  done
   1.114