remove unneeded constant Zseq
authorhuffman
Mon May 03 20:42:58 2010 -0700 (2010-05-03)
changeset 36657f376af79f6b7
parent 36656 fec55067ae9b
child 36658 e37b4338c71f
remove unneeded constant Zseq
src/HOL/SEQ.thy
src/HOL/Series.thy
     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  
     2.1 --- a/src/HOL/Series.thy	Mon May 03 18:40:48 2010 -0700
     2.2 +++ b/src/HOL/Series.thy	Mon May 03 20:42:58 2010 -0700
     2.3 @@ -672,8 +672,8 @@
     2.4      by (rule convergentI)
     2.5    hence Cauchy: "Cauchy (\<lambda>n. setsum ?f (?S1 n))"
     2.6      by (rule convergent_Cauchy)
     2.7 -  have "Zseq (\<lambda>n. setsum ?f (?S1 n - ?S2 n))"
     2.8 -  proof (rule ZseqI, simp only: norm_setsum_f)
     2.9 +  have "Zfun (\<lambda>n. setsum ?f (?S1 n - ?S2 n)) sequentially"
    2.10 +  proof (rule ZfunI, simp only: eventually_sequentially norm_setsum_f)
    2.11      fix r :: real
    2.12      assume r: "0 < r"
    2.13      from CauchyD [OF Cauchy r] obtain N
    2.14 @@ -694,14 +694,15 @@
    2.15        finally show "setsum ?f (?S1 n - ?S2 n) < r" .
    2.16      qed
    2.17    qed
    2.18 -  hence "Zseq (\<lambda>n. setsum ?g (?S1 n - ?S2 n))"
    2.19 -    apply (rule Zseq_le [rule_format])
    2.20 +  hence "Zfun (\<lambda>n. setsum ?g (?S1 n - ?S2 n)) sequentially"
    2.21 +    apply (rule Zfun_le [rule_format])
    2.22      apply (simp only: norm_setsum_f)
    2.23      apply (rule order_trans [OF norm_setsum setsum_mono])
    2.24      apply (auto simp add: norm_mult_ineq)
    2.25      done
    2.26    hence 2: "(\<lambda>n. setsum ?g (?S1 n) - setsum ?g (?S2 n)) ----> 0"
    2.27 -    by (simp only: LIMSEQ_Zseq_iff setsum_diff finite_S1 S2_le_S1 diff_0_right)
    2.28 +    unfolding LIMSEQ_conv_tendsto tendsto_Zfun_iff diff_0_right
    2.29 +    by (simp only: setsum_diff finite_S1 S2_le_S1)
    2.30  
    2.31    with 1 have "(\<lambda>n. setsum ?g (?S2 n)) ----> (\<Sum>k. a k) * (\<Sum>k. b k)"
    2.32      by (rule LIMSEQ_diff_approach_zero2)