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.43
1.44  lemma LIMSEQ_const: "(\<lambda>n. k) ----> k"
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.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.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.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.146 +by (intro tendsto_intros)
1.147
1.148  (* FIXME: delete *)
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"
```