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.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
```