add lemmas for monotone sequences
authorhoelzl
Mon Mar 14 14:37:37 2011 +0100 (2011-03-14)
changeset 419728885ba629692
parent 41971 a54e8e95fe96
child 41973 15927c040731
add lemmas for monotone sequences
src/HOL/SEQ.thy
     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.79 +by (simp add: monoseq_def)
    1.80 +
    1.81 +lemma monoI2: "\<forall>m. \<forall> n \<ge> m. X n \<le> X m ==> monoseq X"
    1.82 +by (simp add: monoseq_def)
    1.83 +
    1.84 +lemma mono_SucI1: "\<forall>n. X n \<le> X (Suc n) ==> monoseq X"
    1.85 +by (simp add: monoseq_Suc)
    1.86 +
    1.87 +lemma mono_SucI2: "\<forall>n. X (Suc n) \<le> X n ==> monoseq X"
    1.88 +by (simp add: monoseq_Suc)
    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.107 +apply (simp add: subseq_def)
   1.108 +apply (auto dest!: less_imp_Suc_add)
   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.209 -apply (simp add: subseq_def)
   1.210 -apply (auto dest!: less_imp_Suc_add)
   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.217 -apply (simp add: monoseq_def)
   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.228 -by (simp add: monoseq_def)
   1.229 -
   1.230 -lemma monoI2: "\<forall>m. \<forall> n \<ge> m. X n \<le> X m ==> monoseq X"
   1.231 -by (simp add: monoseq_def)
   1.232 -
   1.233 -lemma mono_SucI1: "\<forall>n. X n \<le> X (Suc n) ==> monoseq X"
   1.234 -by (simp add: monoseq_Suc)
   1.235 -
   1.236 -lemma mono_SucI2: "\<forall>n. X (Suc n) \<le> X n ==> monoseq X"
   1.237 -by (simp add: monoseq_Suc)
   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 -