src/HOL/SEQ.thy
changeset 36660 1cc4ab4b7ff7
parent 36657 f376af79f6b7
child 36662 621122eeb138
     1.1 --- a/src/HOL/SEQ.thy	Tue May 04 09:56:34 2010 -0700
     1.2 +++ b/src/HOL/SEQ.thy	Tue May 04 10:06:05 2010 -0700
     1.3 @@ -13,11 +13,10 @@
     1.4  imports Limits
     1.5  begin
     1.6  
     1.7 -definition
     1.8 +abbreviation
     1.9    LIMSEQ :: "[nat \<Rightarrow> 'a::metric_space, 'a] \<Rightarrow> bool"
    1.10      ("((_)/ ----> (_))" [60, 60] 60) where
    1.11 -    --{*Standard definition of convergence of sequence*}
    1.12 -  [code del]: "X ----> L = (\<forall>r>0. \<exists>no. \<forall>n\<ge>no. dist (X n) L < r)"
    1.13 +  "X ----> L \<equiv> (X ---> L) sequentially"
    1.14  
    1.15  definition
    1.16    lim :: "(nat \<Rightarrow> 'a::metric_space) \<Rightarrow> 'a" where
    1.17 @@ -119,8 +118,8 @@
    1.18  lemma [trans]: "X=Y ==> Y ----> z ==> X ----> z"
    1.19    by simp
    1.20  
    1.21 -lemma LIMSEQ_conv_tendsto: "(X ----> L) \<longleftrightarrow> (X ---> L) sequentially"
    1.22 -unfolding LIMSEQ_def tendsto_iff eventually_sequentially ..
    1.23 +lemma LIMSEQ_def: "X ----> L = (\<forall>r>0. \<exists>no. \<forall>n\<ge>no. dist (X n) L < r)"
    1.24 +unfolding tendsto_iff eventually_sequentially ..
    1.25  
    1.26  lemma LIMSEQ_iff:
    1.27    fixes L :: "'a::real_normed_vector"
    1.28 @@ -128,10 +127,10 @@
    1.29  unfolding LIMSEQ_def dist_norm ..
    1.30  
    1.31  lemma LIMSEQ_iff_nz: "X ----> L = (\<forall>r>0. \<exists>no>0. \<forall>n\<ge>no. dist (X n) L < r)"
    1.32 -  by (auto simp add: LIMSEQ_def) (metis Suc_leD zero_less_Suc)  
    1.33 +  unfolding LIMSEQ_def by (metis Suc_leD zero_less_Suc)
    1.34  
    1.35  lemma LIMSEQ_Zfun_iff: "((\<lambda>n. X n) ----> L) = Zfun (\<lambda>n. X n - L) sequentially"
    1.36 -by (simp only: LIMSEQ_iff Zfun_def eventually_sequentially)
    1.37 +by (rule tendsto_Zfun_iff)
    1.38  
    1.39  lemma metric_LIMSEQ_I:
    1.40    "(\<And>r. 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. dist (X n) L < r) \<Longrightarrow> X ----> L"
    1.41 @@ -152,7 +151,7 @@
    1.42  by (simp add: LIMSEQ_iff)
    1.43  
    1.44  lemma LIMSEQ_const: "(\<lambda>n. k) ----> k"
    1.45 -by (simp add: LIMSEQ_def)
    1.46 +by (rule tendsto_const)
    1.47  
    1.48  lemma LIMSEQ_const_iff: "(\<lambda>n. k) ----> l \<longleftrightarrow> k = l"
    1.49  apply (safe intro!: LIMSEQ_const)
    1.50 @@ -165,7 +164,7 @@
    1.51  lemma LIMSEQ_norm:
    1.52    fixes a :: "'a::real_normed_vector"
    1.53    shows "X ----> a \<Longrightarrow> (\<lambda>n. norm (X n)) ----> norm a"
    1.54 -unfolding LIMSEQ_conv_tendsto by (rule tendsto_norm)
    1.55 +by (rule tendsto_norm)
    1.56  
    1.57  lemma LIMSEQ_ignore_initial_segment:
    1.58    "f ----> a \<Longrightarrow> (\<lambda>n. f (n + k)) ----> a"
    1.59 @@ -203,22 +202,22 @@
    1.60  lemma LIMSEQ_add:
    1.61    fixes a b :: "'a::real_normed_vector"
    1.62    shows "\<lbrakk>X ----> a; Y ----> b\<rbrakk> \<Longrightarrow> (\<lambda>n. X n + Y n) ----> a + b"
    1.63 -unfolding LIMSEQ_conv_tendsto by (rule tendsto_add)
    1.64 +by (rule tendsto_add)
    1.65  
    1.66  lemma LIMSEQ_minus:
    1.67    fixes a :: "'a::real_normed_vector"
    1.68    shows "X ----> a \<Longrightarrow> (\<lambda>n. - X n) ----> - a"
    1.69 -unfolding LIMSEQ_conv_tendsto by (rule tendsto_minus)
    1.70 +by (rule tendsto_minus)
    1.71  
    1.72  lemma LIMSEQ_minus_cancel:
    1.73    fixes a :: "'a::real_normed_vector"
    1.74    shows "(\<lambda>n. - X n) ----> - a \<Longrightarrow> X ----> a"
    1.75 -by (drule LIMSEQ_minus, simp)
    1.76 +by (rule tendsto_minus_cancel)
    1.77  
    1.78  lemma LIMSEQ_diff:
    1.79    fixes a b :: "'a::real_normed_vector"
    1.80    shows "\<lbrakk>X ----> a; Y ----> b\<rbrakk> \<Longrightarrow> (\<lambda>n. X n - Y n) ----> a - b"
    1.81 -unfolding LIMSEQ_conv_tendsto by (rule tendsto_diff)
    1.82 +by (rule tendsto_diff)
    1.83  
    1.84  lemma LIMSEQ_unique: "\<lbrakk>X ----> a; X ----> b\<rbrakk> \<Longrightarrow> a = b"
    1.85  apply (rule ccontr)
    1.86 @@ -233,16 +232,16 @@
    1.87  
    1.88  lemma (in bounded_linear) LIMSEQ:
    1.89    "X ----> a \<Longrightarrow> (\<lambda>n. f (X n)) ----> f a"
    1.90 -unfolding LIMSEQ_conv_tendsto by (rule tendsto)
    1.91 +by (rule tendsto)
    1.92  
    1.93  lemma (in bounded_bilinear) LIMSEQ:
    1.94    "\<lbrakk>X ----> a; Y ----> b\<rbrakk> \<Longrightarrow> (\<lambda>n. X n ** Y n) ----> a ** b"
    1.95 -unfolding LIMSEQ_conv_tendsto by (rule tendsto)
    1.96 +by (rule tendsto)
    1.97  
    1.98  lemma LIMSEQ_mult:
    1.99    fixes a b :: "'a::real_normed_algebra"
   1.100    shows "[| X ----> a; Y ----> b |] ==> (%n. X n * Y n) ----> a * b"
   1.101 -by (rule mult.LIMSEQ)
   1.102 +by (rule mult.tendsto)
   1.103  
   1.104  lemma increasing_LIMSEQ:
   1.105    fixes f :: "nat \<Rightarrow> real"
   1.106 @@ -287,19 +286,17 @@
   1.107  lemma Bseq_inverse:
   1.108    fixes a :: "'a::real_normed_div_algebra"
   1.109    shows "\<lbrakk>X ----> a; a \<noteq> 0\<rbrakk> \<Longrightarrow> Bseq (\<lambda>n. inverse (X n))"
   1.110 -unfolding LIMSEQ_conv_tendsto Bseq_conv_Bfun
   1.111 -by (rule Bfun_inverse)
   1.112 +unfolding Bseq_conv_Bfun by (rule Bfun_inverse)
   1.113  
   1.114  lemma LIMSEQ_inverse:
   1.115    fixes a :: "'a::real_normed_div_algebra"
   1.116    shows "\<lbrakk>X ----> a; a \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>n. inverse (X n)) ----> inverse a"
   1.117 -unfolding LIMSEQ_conv_tendsto
   1.118  by (rule tendsto_inverse)
   1.119  
   1.120  lemma LIMSEQ_divide:
   1.121    fixes a b :: "'a::real_normed_field"
   1.122    shows "\<lbrakk>X ----> a; Y ----> b; b \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>n. X n / Y n) ----> a / b"
   1.123 -by (simp add: LIMSEQ_mult LIMSEQ_inverse divide_inverse)
   1.124 +by (rule tendsto_divide)
   1.125  
   1.126  lemma LIMSEQ_pow:
   1.127    fixes a :: "'a::{power, real_normed_algebra}"
   1.128 @@ -310,7 +307,7 @@
   1.129    fixes L :: "'a \<Rightarrow> 'b::real_normed_vector"
   1.130    assumes n: "\<And>n. n \<in> S \<Longrightarrow> X n ----> L n"
   1.131    shows "(\<lambda>m. \<Sum>n\<in>S. X n m) ----> (\<Sum>n\<in>S. L n)"
   1.132 -using n unfolding LIMSEQ_conv_tendsto by (rule tendsto_setsum)
   1.133 +using assms by (rule tendsto_setsum)
   1.134  
   1.135  lemma LIMSEQ_setprod:
   1.136    fixes L :: "'a \<Rightarrow> 'b::{real_normed_algebra,comm_ring_1}"
   1.137 @@ -334,21 +331,21 @@
   1.138      by (simp add: setprod_def LIMSEQ_const)
   1.139  qed
   1.140  
   1.141 -lemma LIMSEQ_add_const:
   1.142 +lemma LIMSEQ_add_const: (* FIXME: delete *)
   1.143    fixes a :: "'a::real_normed_vector"
   1.144    shows "f ----> a ==> (%n.(f n + b)) ----> a + b"
   1.145 -by (simp add: LIMSEQ_add LIMSEQ_const)
   1.146 +by (intro tendsto_intros)
   1.147  
   1.148  (* FIXME: delete *)
   1.149  lemma LIMSEQ_add_minus:
   1.150    fixes a b :: "'a::real_normed_vector"
   1.151    shows "[| X ----> a; Y ----> b |] ==> (%n. X n + -Y n) ----> a + -b"
   1.152 -by (simp only: LIMSEQ_add LIMSEQ_minus)
   1.153 +by (intro tendsto_intros)
   1.154  
   1.155 -lemma LIMSEQ_diff_const:
   1.156 +lemma LIMSEQ_diff_const: (* FIXME: delete *)
   1.157    fixes a b :: "'a::real_normed_vector"
   1.158    shows "f ----> a ==> (%n.(f n  - b)) ----> a - b"
   1.159 -by (simp add: LIMSEQ_diff LIMSEQ_const)
   1.160 +by (intro tendsto_intros)
   1.161  
   1.162  lemma LIMSEQ_diff_approach_zero:
   1.163    fixes L :: "'a::real_normed_vector"