author hoelzl Mon Mar 14 14:37:37 2011 +0100 (2011-03-14) changeset 41972 8885ba629692 parent 41971 a54e8e95fe96 child 41973 15927c040731
 src/HOL/SEQ.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/SEQ.thy	Mon Mar 14 14:37:36 2011 +0100
1.2 +++ b/src/HOL/SEQ.thy	Mon Mar 14 14:37:37 2011 +0100
1.3 @@ -13,25 +13,7 @@
1.4  imports Limits RComplete
1.5  begin
1.6
1.7 -abbreviation
1.8 -  LIMSEQ :: "[nat \<Rightarrow> 'a::topological_space, 'a] \<Rightarrow> bool"
1.9 -    ("((_)/ ----> (_))" [60, 60] 60) where
1.10 -  "X ----> L \<equiv> (X ---> L) sequentially"
1.11 -
1.12 -definition
1.13 -  lim :: "(nat \<Rightarrow> 'a::metric_space) \<Rightarrow> 'a" where
1.14 -    --{*Standard definition of limit using choice operator*}
1.15 -  "lim X = (THE L. X ----> L)"
1.16 -
1.17 -definition
1.18 -  convergent :: "(nat \<Rightarrow> 'a::metric_space) \<Rightarrow> bool" where
1.19 -    --{*Standard definition of convergence*}
1.20 -  "convergent X = (\<exists>L. X ----> L)"
1.21 -
1.22 -definition
1.23 -  Bseq :: "(nat => 'a::real_normed_vector) => bool" where
1.24 -    --{*Standard definition for bounded sequence*}
1.25 -  "Bseq X = (\<exists>K>0.\<forall>n. norm (X n) \<le> K)"
1.26 +subsection {* Monotone sequences and subsequences *}
1.27
1.28  definition
1.29    monoseq :: "(nat \<Rightarrow> 'a::order) \<Rightarrow> bool" where
1.30 @@ -56,6 +38,171 @@
1.31      --{*Definition of subsequence*}
1.32    "subseq f \<longleftrightarrow> (\<forall>m. \<forall>n>m. f m < f n)"
1.33
1.34 +lemma incseq_mono: "mono f \<longleftrightarrow> incseq f"
1.35 +  unfolding mono_def incseq_def by auto
1.36 +
1.37 +lemma incseq_SucI:
1.38 +  "(\<And>n. X n \<le> X (Suc n)) \<Longrightarrow> incseq X"
1.39 +  using lift_Suc_mono_le[of X]
1.40 +  by (auto simp: incseq_def)
1.41 +
1.42 +lemma incseqD: "\<And>i j. incseq f \<Longrightarrow> i \<le> j \<Longrightarrow> f i \<le> f j"
1.43 +  by (auto simp: incseq_def)
1.44 +
1.45 +lemma incseq_SucD: "incseq A \<Longrightarrow> A i \<le> A (Suc i)"
1.46 +  using incseqD[of A i "Suc i"] by auto
1.47 +
1.48 +lemma incseq_Suc_iff: "incseq f \<longleftrightarrow> (\<forall>n. f n \<le> f (Suc n))"
1.49 +  by (auto intro: incseq_SucI dest: incseq_SucD)
1.50 +
1.51 +lemma incseq_const[simp, intro]: "incseq (\<lambda>x. k)"
1.52 +  unfolding incseq_def by auto
1.53 +
1.54 +lemma decseq_SucI:
1.55 +  "(\<And>n. X (Suc n) \<le> X n) \<Longrightarrow> decseq X"
1.56 +  using order.lift_Suc_mono_le[OF dual_order, of X]
1.57 +  by (auto simp: decseq_def)
1.58 +
1.59 +lemma decseqD: "\<And>i j. decseq f \<Longrightarrow> i \<le> j \<Longrightarrow> f j \<le> f i"
1.60 +  by (auto simp: decseq_def)
1.61 +
1.62 +lemma decseq_SucD: "decseq A \<Longrightarrow> A (Suc i) \<le> A i"
1.63 +  using decseqD[of A i "Suc i"] by auto
1.64 +
1.65 +lemma decseq_Suc_iff: "decseq f \<longleftrightarrow> (\<forall>n. f (Suc n) \<le> f n)"
1.66 +  by (auto intro: decseq_SucI dest: decseq_SucD)
1.67 +
1.68 +lemma decseq_const[simp, intro]: "decseq (\<lambda>x. k)"
1.69 +  unfolding decseq_def by auto
1.70 +
1.71 +lemma monoseq_iff: "monoseq X \<longleftrightarrow> incseq X \<or> decseq X"
1.72 +  unfolding monoseq_def incseq_def decseq_def ..
1.73 +
1.74 +lemma monoseq_Suc:
1.75 +  "monoseq X \<longleftrightarrow> (\<forall>n. X n \<le> X (Suc n)) \<or> (\<forall>n. X (Suc n) \<le> X n)"
1.76 +  unfolding monoseq_iff incseq_Suc_iff decseq_Suc_iff ..
1.77 +
1.78 +lemma monoI1: "\<forall>m. \<forall> n \<ge> m. X m \<le> X n ==> monoseq X"
1.80 +
1.81 +lemma monoI2: "\<forall>m. \<forall> n \<ge> m. X n \<le> X m ==> monoseq X"
1.83 +
1.84 +lemma mono_SucI1: "\<forall>n. X n \<le> X (Suc n) ==> monoseq X"
1.86 +
1.87 +lemma mono_SucI2: "\<forall>n. X (Suc n) \<le> X n ==> monoseq X"
1.89 +
1.90 +lemma monoseq_minus:
1.91 +  fixes a :: "nat \<Rightarrow> 'a::ordered_ab_group_add"
1.92 +  assumes "monoseq a"
1.93 +  shows "monoseq (\<lambda> n. - a n)"
1.94 +proof (cases "\<forall> m. \<forall> n \<ge> m. a m \<le> a n")
1.95 +  case True
1.96 +  hence "\<forall> m. \<forall> n \<ge> m. - a n \<le> - a m" by auto
1.97 +  thus ?thesis by (rule monoI2)
1.98 +next
1.99 +  case False
1.100 +  hence "\<forall> m. \<forall> n \<ge> m. - a m \<le> - a n" using `monoseq a`[unfolded monoseq_def] by auto
1.101 +  thus ?thesis by (rule monoI1)
1.102 +qed
1.103 +
1.104 +text{*Subsequence (alternative definition, (e.g. Hoskins)*}
1.105 +
1.106 +lemma subseq_Suc_iff: "subseq f = (\<forall>n. (f n) < (f (Suc n)))"
1.109 +apply (induct_tac k)
1.110 +apply (auto intro: less_trans)
1.111 +done
1.112 +
1.113 +text{* for any sequence, there is a monotonic subsequence *}
1.114 +lemma seq_monosub:
1.115 +  fixes s :: "nat => 'a::linorder"
1.116 +  shows "\<exists>f. subseq f \<and> monoseq (\<lambda> n. (s (f n)))"
1.117 +proof cases
1.118 +  let "?P p n" = "p > n \<and> (\<forall>m\<ge>p. s m \<le> s p)"
1.119 +  assume *: "\<forall>n. \<exists>p. ?P p n"
1.120 +  def f \<equiv> "nat_rec (SOME p. ?P p 0) (\<lambda>_ n. SOME p. ?P p n)"
1.121 +  have f_0: "f 0 = (SOME p. ?P p 0)" unfolding f_def by simp
1.122 +  have f_Suc: "\<And>i. f (Suc i) = (SOME p. ?P p (f i))" unfolding f_def nat_rec_Suc ..
1.123 +  have P_0: "?P (f 0) 0" unfolding f_0 using *[rule_format] by (rule someI2_ex) auto
1.124 +  have P_Suc: "\<And>i. ?P (f (Suc i)) (f i)" unfolding f_Suc using *[rule_format] by (rule someI2_ex) auto
1.125 +  then have "subseq f" unfolding subseq_Suc_iff by auto
1.126 +  moreover have "monoseq (\<lambda>n. s (f n))" unfolding monoseq_Suc
1.127 +  proof (intro disjI2 allI)
1.128 +    fix n show "s (f (Suc n)) \<le> s (f n)"
1.129 +    proof (cases n)
1.130 +      case 0 with P_Suc[of 0] P_0 show ?thesis by auto
1.131 +    next
1.132 +      case (Suc m)
1.133 +      from P_Suc[of n] Suc have "f (Suc m) \<le> f (Suc (Suc m))" by simp
1.134 +      with P_Suc Suc show ?thesis by simp
1.135 +    qed
1.136 +  qed
1.137 +  ultimately show ?thesis by auto
1.138 +next
1.139 +  let "?P p m" = "m < p \<and> s m < s p"
1.140 +  assume "\<not> (\<forall>n. \<exists>p>n. (\<forall>m\<ge>p. s m \<le> s p))"
1.141 +  then obtain N where N: "\<And>p. p > N \<Longrightarrow> \<exists>m>p. s p < s m" by (force simp: not_le le_less)
1.142 +  def f \<equiv> "nat_rec (SOME p. ?P p (Suc N)) (\<lambda>_ n. SOME p. ?P p n)"
1.143 +  have f_0: "f 0 = (SOME p. ?P p (Suc N))" unfolding f_def by simp
1.144 +  have f_Suc: "\<And>i. f (Suc i) = (SOME p. ?P p (f i))" unfolding f_def nat_rec_Suc ..
1.145 +  have P_0: "?P (f 0) (Suc N)"
1.146 +    unfolding f_0 some_eq_ex[of "\<lambda>p. ?P p (Suc N)"] using N[of "Suc N"] by auto
1.147 +  { fix i have "N < f i \<Longrightarrow> ?P (f (Suc i)) (f i)"
1.148 +      unfolding f_Suc some_eq_ex[of "\<lambda>p. ?P p (f i)"] using N[of "f i"] . }
1.149 +  note P' = this
1.150 +  { fix i have "N < f i \<and> ?P (f (Suc i)) (f i)"
1.151 +      by (induct i) (insert P_0 P', auto) }
1.152 +  then have "subseq f" "monoseq (\<lambda>x. s (f x))"
1.153 +    unfolding subseq_Suc_iff monoseq_Suc by (auto simp: not_le intro: less_imp_le)
1.154 +  then show ?thesis by auto
1.155 +qed
1.156 +
1.157 +lemma seq_suble: assumes sf: "subseq f" shows "n \<le> f n"
1.158 +proof(induct n)
1.159 +  case 0 thus ?case by simp
1.160 +next
1.161 +  case (Suc n)
1.162 +  from sf[unfolded subseq_Suc_iff, rule_format, of n] Suc.hyps
1.163 +  have "n < f (Suc n)" by arith
1.164 +  thus ?case by arith
1.165 +qed
1.166 +
1.167 +lemma incseq_imp_monoseq:  "incseq X \<Longrightarrow> monoseq X"
1.168 +  by (simp add: incseq_def monoseq_def)
1.169 +
1.170 +lemma decseq_imp_monoseq:  "decseq X \<Longrightarrow> monoseq X"
1.171 +  by (simp add: decseq_def monoseq_def)
1.172 +
1.173 +lemma decseq_eq_incseq:
1.174 +  fixes X :: "nat \<Rightarrow> 'a::ordered_ab_group_add" shows "decseq X = incseq (\<lambda>n. - X n)"
1.175 +  by (simp add: decseq_def incseq_def)
1.176 +
1.177 +subsection {* Defintions of limits *}
1.178 +
1.179 +abbreviation
1.180 +  LIMSEQ :: "[nat \<Rightarrow> 'a::topological_space, 'a] \<Rightarrow> bool"
1.181 +    ("((_)/ ----> (_))" [60, 60] 60) where
1.182 +  "X ----> L \<equiv> (X ---> L) sequentially"
1.183 +
1.184 +definition
1.185 +  lim :: "(nat \<Rightarrow> 'a::metric_space) \<Rightarrow> 'a" where
1.186 +    --{*Standard definition of limit using choice operator*}
1.187 +  "lim X = (THE L. X ----> L)"
1.188 +
1.189 +definition
1.190 +  convergent :: "(nat \<Rightarrow> 'a::metric_space) \<Rightarrow> bool" where
1.191 +    --{*Standard definition of convergence*}
1.192 +  "convergent X = (\<exists>L. X ----> L)"
1.193 +
1.194 +definition
1.195 +  Bseq :: "(nat => 'a::real_normed_vector) => bool" where
1.196 +    --{*Standard definition for bounded sequence*}
1.197 +  "Bseq X = (\<exists>K>0.\<forall>n. norm (X n) \<le> K)"
1.198 +
1.199  definition
1.200    Cauchy :: "(nat \<Rightarrow> 'a::metric_space) \<Rightarrow> bool" where
1.201      --{*Standard definition of the Cauchy condition*}
1.202 @@ -502,53 +649,6 @@
1.203      qed
1.204  qed
1.205
1.206 -text{*Subsequence (alternative definition, (e.g. Hoskins)*}
1.207 -
1.208 -lemma subseq_Suc_iff: "subseq f = (\<forall>n. (f n) < (f (Suc n)))"
1.211 -apply (induct_tac k)
1.212 -apply (auto intro: less_trans)
1.213 -done
1.214 -
1.215 -lemma monoseq_Suc:
1.216 -  "monoseq X \<longleftrightarrow> (\<forall>n. X n \<le> X (Suc n)) \<or> (\<forall>n. X (Suc n) \<le> X n)"
1.218 -apply (auto dest!: le_imp_less_or_eq)
1.219 -apply (auto intro!: lessI [THEN less_imp_le] dest!: less_imp_Suc_add)
1.220 -apply (induct_tac "ka")
1.221 -apply (auto intro: order_trans)
1.222 -apply (erule contrapos_np)
1.223 -apply (induct_tac "k")
1.224 -apply (auto intro: order_trans)
1.225 -done
1.226 -
1.227 -lemma monoI1: "\<forall>m. \<forall> n \<ge> m. X m \<le> X n ==> monoseq X"
1.229 -
1.230 -lemma monoI2: "\<forall>m. \<forall> n \<ge> m. X n \<le> X m ==> monoseq X"
1.232 -
1.233 -lemma mono_SucI1: "\<forall>n. X n \<le> X (Suc n) ==> monoseq X"
1.235 -
1.236 -lemma mono_SucI2: "\<forall>n. X (Suc n) \<le> X n ==> monoseq X"
1.238 -
1.239 -lemma monoseq_minus:
1.240 -  fixes a :: "nat \<Rightarrow> 'a::ordered_ab_group_add"
1.241 -  assumes "monoseq a"
1.242 -  shows "monoseq (\<lambda> n. - a n)"
1.243 -proof (cases "\<forall> m. \<forall> n \<ge> m. a m \<le> a n")
1.244 -  case True
1.245 -  hence "\<forall> m. \<forall> n \<ge> m. - a n \<le> - a m" by auto
1.246 -  thus ?thesis by (rule monoI2)
1.247 -next
1.248 -  case False
1.249 -  hence "\<forall> m. \<forall> n \<ge> m. - a m \<le> - a n" using `monoseq a`[unfolded monoseq_def] by auto
1.250 -  thus ?thesis by (rule monoI1)
1.251 -qed
1.252 -
1.253  lemma monoseq_le:
1.254    fixes a :: "nat \<Rightarrow> real"
1.255    assumes "monoseq a" and "a ----> x"
1.256 @@ -602,60 +702,6 @@
1.257    qed auto
1.258  qed
1.259
1.260 -text{* for any sequence, there is a monotonic subsequence *}
1.261 -lemma seq_monosub:
1.262 -  fixes s :: "nat => 'a::linorder"
1.263 -  shows "\<exists>f. subseq f \<and> monoseq (\<lambda> n. (s (f n)))"
1.264 -proof cases
1.265 -  let "?P p n" = "p > n \<and> (\<forall>m\<ge>p. s m \<le> s p)"
1.266 -  assume *: "\<forall>n. \<exists>p. ?P p n"
1.267 -  def f \<equiv> "nat_rec (SOME p. ?P p 0) (\<lambda>_ n. SOME p. ?P p n)"
1.268 -  have f_0: "f 0 = (SOME p. ?P p 0)" unfolding f_def by simp
1.269 -  have f_Suc: "\<And>i. f (Suc i) = (SOME p. ?P p (f i))" unfolding f_def nat_rec_Suc ..
1.270 -  have P_0: "?P (f 0) 0" unfolding f_0 using *[rule_format] by (rule someI2_ex) auto
1.271 -  have P_Suc: "\<And>i. ?P (f (Suc i)) (f i)" unfolding f_Suc using *[rule_format] by (rule someI2_ex) auto
1.272 -  then have "subseq f" unfolding subseq_Suc_iff by auto
1.273 -  moreover have "monoseq (\<lambda>n. s (f n))" unfolding monoseq_Suc
1.274 -  proof (intro disjI2 allI)
1.275 -    fix n show "s (f (Suc n)) \<le> s (f n)"
1.276 -    proof (cases n)
1.277 -      case 0 with P_Suc[of 0] P_0 show ?thesis by auto
1.278 -    next
1.279 -      case (Suc m)
1.280 -      from P_Suc[of n] Suc have "f (Suc m) \<le> f (Suc (Suc m))" by simp
1.281 -      with P_Suc Suc show ?thesis by simp
1.282 -    qed
1.283 -  qed
1.284 -  ultimately show ?thesis by auto
1.285 -next
1.286 -  let "?P p m" = "m < p \<and> s m < s p"
1.287 -  assume "\<not> (\<forall>n. \<exists>p>n. (\<forall>m\<ge>p. s m \<le> s p))"
1.288 -  then obtain N where N: "\<And>p. p > N \<Longrightarrow> \<exists>m>p. s p < s m" by (force simp: not_le le_less)
1.289 -  def f \<equiv> "nat_rec (SOME p. ?P p (Suc N)) (\<lambda>_ n. SOME p. ?P p n)"
1.290 -  have f_0: "f 0 = (SOME p. ?P p (Suc N))" unfolding f_def by simp
1.291 -  have f_Suc: "\<And>i. f (Suc i) = (SOME p. ?P p (f i))" unfolding f_def nat_rec_Suc ..
1.292 -  have P_0: "?P (f 0) (Suc N)"
1.293 -    unfolding f_0 some_eq_ex[of "\<lambda>p. ?P p (Suc N)"] using N[of "Suc N"] by auto
1.294 -  { fix i have "N < f i \<Longrightarrow> ?P (f (Suc i)) (f i)"
1.295 -      unfolding f_Suc some_eq_ex[of "\<lambda>p. ?P p (f i)"] using N[of "f i"] . }
1.296 -  note P' = this
1.297 -  { fix i have "N < f i \<and> ?P (f (Suc i)) (f i)"
1.298 -      by (induct i) (insert P_0 P', auto) }
1.299 -  then have "subseq f" "monoseq (\<lambda>x. s (f x))"
1.300 -    unfolding subseq_Suc_iff monoseq_Suc by (auto simp: not_le intro: less_imp_le)
1.301 -  then show ?thesis by auto
1.302 -qed
1.303 -
1.304 -lemma seq_suble: assumes sf: "subseq f" shows "n \<le> f n"
1.305 -proof(induct n)
1.306 -  case 0 thus ?case by simp
1.307 -next
1.308 -  case (Suc n)
1.309 -  from sf[unfolded subseq_Suc_iff, rule_format, of n] Suc.hyps
1.310 -  have "n < f (Suc n)" by arith
1.311 -  thus ?case by arith
1.312 -qed
1.313 -
1.314  lemma LIMSEQ_subseq_LIMSEQ:
1.315    "\<lbrakk> X ----> L; subseq f \<rbrakk> \<Longrightarrow> (X o f) ----> L"
1.316  apply (rule topological_tendstoI)
1.317 @@ -810,9 +856,6 @@
1.318
1.319  subsubsection{*Increasing and Decreasing Series*}
1.320
1.321 -lemma incseq_imp_monoseq:  "incseq X \<Longrightarrow> monoseq X"
1.322 -  by (simp add: incseq_def monoseq_def)
1.323 -
1.324  lemma incseq_le:
1.325    fixes X :: "nat \<Rightarrow> real"
1.326    assumes inc: "incseq X" and lim: "X ----> L" shows "X n \<le> L"
1.327 @@ -834,32 +877,6 @@
1.328      by (blast intro: eq_refl X)
1.329  qed
1.330
1.331 -lemma incseq_SucI:
1.332 -  assumes "\<And>n. X n \<le> X (Suc n)"
1.333 -  shows "incseq X" unfolding incseq_def
1.334 -proof safe
1.335 -  fix m n :: nat
1.336 -  { fix d m :: nat
1.337 -    have "X m \<le> X (m + d)"
1.338 -    proof (induct d)
1.339 -      case (Suc d)
1.340 -      also have "X (m + d) \<le> X (m + Suc d)"
1.341 -        using assms by simp
1.342 -      finally show ?case .
1.343 -    qed simp }
1.344 -  note this[of m "n - m"]
1.345 -  moreover assume "m \<le> n"
1.346 -  ultimately show "X m \<le> X n" by simp
1.347 -qed
1.348 -
1.349 -lemma decseq_imp_monoseq:  "decseq X \<Longrightarrow> monoseq X"
1.350 -  by (simp add: decseq_def monoseq_def)
1.351 -
1.352 -lemma decseq_eq_incseq:
1.353 -  fixes X :: "nat \<Rightarrow> 'a::ordered_ab_group_add" shows "decseq X = incseq (\<lambda>n. - X n)"
1.354 -  by (simp add: decseq_def incseq_def)
1.355 -
1.356 -
1.357  lemma decseq_le:
1.358    fixes X :: "nat \<Rightarrow> real" assumes dec: "decseq X" and lim: "X ----> L" shows "L \<le> X n"
1.359  proof -
```