src/HOL/SEQ.thy
 changeset 41367 1b65137d598c parent 40811 ab0a8cc7976a child 41972 8885ba629692
```     1.1 --- a/src/HOL/SEQ.thy	Tue Dec 21 14:18:45 2010 +0100
1.2 +++ b/src/HOL/SEQ.thy	Tue Dec 21 14:50:53 2010 +0100
1.3 @@ -34,27 +34,27 @@
1.4    "Bseq X = (\<exists>K>0.\<forall>n. norm (X n) \<le> K)"
1.5
1.6  definition
1.7 -  monoseq :: "(nat=>real)=>bool" where
1.8 -    --{*Definition of monotonicity.
1.9 -        The use of disjunction here complicates proofs considerably.
1.10 -        One alternative is to add a Boolean argument to indicate the direction.
1.11 +  monoseq :: "(nat \<Rightarrow> 'a::order) \<Rightarrow> bool" where
1.12 +    --{*Definition of monotonicity.
1.13 +        The use of disjunction here complicates proofs considerably.
1.14 +        One alternative is to add a Boolean argument to indicate the direction.
1.15          Another is to develop the notions of increasing and decreasing first.*}
1.16    "monoseq X = ((\<forall>m. \<forall>n\<ge>m. X m \<le> X n) | (\<forall>m. \<forall>n\<ge>m. X n \<le> X m))"
1.17
1.18  definition
1.19 -  incseq :: "(nat=>real)=>bool" where
1.20 +  incseq :: "(nat \<Rightarrow> 'a::order) \<Rightarrow> bool" where
1.21      --{*Increasing sequence*}
1.22 -  "incseq X = (\<forall>m. \<forall>n\<ge>m. X m \<le> X n)"
1.23 +  "incseq X \<longleftrightarrow> (\<forall>m. \<forall>n\<ge>m. X m \<le> X n)"
1.24
1.25  definition
1.26 -  decseq :: "(nat=>real)=>bool" where
1.27 -    --{*Increasing sequence*}
1.28 -  "decseq X = (\<forall>m. \<forall>n\<ge>m. X n \<le> X m)"
1.29 +  decseq :: "(nat \<Rightarrow> 'a::order) \<Rightarrow> bool" where
1.30 +    --{*Decreasing sequence*}
1.31 +  "decseq X \<longleftrightarrow> (\<forall>m. \<forall>n\<ge>m. X n \<le> X m)"
1.32
1.33  definition
1.34 -  subseq :: "(nat => nat) => bool" where
1.35 +  subseq :: "(nat \<Rightarrow> nat) \<Rightarrow> bool" where
1.36      --{*Definition of subsequence*}
1.37 -  "subseq f = (\<forall>m. \<forall>n>m. (f m) < (f n))"
1.38 +  "subseq f \<longleftrightarrow> (\<forall>m. \<forall>n>m. f m < f n)"
1.39
1.40  definition
1.41    Cauchy :: "(nat \<Rightarrow> 'a::metric_space) \<Rightarrow> bool" where
1.42 @@ -502,22 +502,6 @@
1.43      qed
1.44  qed
1.45
1.46 -text{* Given a binary function @{text "f:: nat \<Rightarrow> 'a \<Rightarrow> 'a"}, its values are uniquely determined by a function g *}
1.47 -
1.48 -lemma nat_function_unique: "EX! g. g 0 = e \<and> (\<forall>n. g (Suc n) = f n (g n))"
1.49 -  unfolding Ex1_def
1.50 -  apply (rule_tac x="nat_rec e f" in exI)
1.51 -  apply (rule conjI)+
1.52 -apply (rule def_nat_rec_0, simp)
1.53 -apply (rule allI, rule def_nat_rec_Suc, simp)
1.54 -apply (rule allI, rule impI, rule ext)
1.55 -apply (erule conjE)
1.56 -apply (induct_tac x)
1.57 -apply simp
1.58 -apply (erule_tac x="n" in allE)
1.59 -apply (simp)
1.60 -done
1.61 -
1.62  text{*Subsequence (alternative definition, (e.g. Hoskins)*}
1.63
1.64  lemma subseq_Suc_iff: "subseq f = (\<forall>n. (f n) < (f (Suc n)))"
1.65 @@ -528,8 +512,7 @@
1.66  done
1.67
1.68  lemma monoseq_Suc:
1.69 -   "monoseq X = ((\<forall>n. X n \<le> X (Suc n))
1.70 -                 | (\<forall>n. X (Suc n) \<le> X n))"
1.71 +  "monoseq X \<longleftrightarrow> (\<forall>n. X n \<le> X (Suc n)) \<or> (\<forall>n. X (Suc n) \<le> X n)"
1.73  apply (auto dest!: le_imp_less_or_eq)
1.74  apply (auto intro!: lessI [THEN less_imp_le] dest!: less_imp_Suc_add)
1.75 @@ -552,7 +535,9 @@
1.76  lemma mono_SucI2: "\<forall>n. X (Suc n) \<le> X n ==> monoseq X"
1.78
1.79 -lemma monoseq_minus: assumes "monoseq a"
1.80 +lemma monoseq_minus:
1.81 +  fixes a :: "nat \<Rightarrow> 'a::ordered_ab_group_add"
1.82 +  assumes "monoseq a"
1.83    shows "monoseq (\<lambda> n. - a n)"
1.84  proof (cases "\<forall> m. \<forall> n \<ge> m. a m \<le> a n")
1.85    case True
1.86 @@ -564,7 +549,9 @@
1.87    thus ?thesis by (rule monoI1)
1.88  qed
1.89
1.90 -lemma monoseq_le: assumes "monoseq a" and "a ----> x"
1.91 +lemma monoseq_le:
1.92 +  fixes a :: "nat \<Rightarrow> real"
1.93 +  assumes "monoseq a" and "a ----> x"
1.94    shows "((\<forall> n. a n \<le> x) \<and> (\<forall>m. \<forall>n\<ge>m. a m \<le> a n)) \<or>
1.95           ((\<forall> n. x \<le> a n) \<and> (\<forall>m. \<forall>n\<ge>m. a n \<le> a m))"
1.96  proof -
1.97 @@ -615,121 +602,48 @@
1.98    qed auto
1.99  qed
1.100
1.101 -text{* for any sequence, there is a mootonic subsequence *}
1.102 -lemma seq_monosub: "\<exists>f. subseq f \<and> monoseq (\<lambda> n. (s (f n)))"
1.103 -proof-
1.104 -  {assume H: "\<forall>n. \<exists>p >n. \<forall> m\<ge>p. s m \<le> s p"
1.105 -    let ?P = "\<lambda> p n. p > n \<and> (\<forall>m \<ge> p. s m \<le> s p)"
1.106 -    from nat_function_unique[of "SOME p. ?P p 0" "\<lambda>p n. SOME p. ?P p n"]
1.107 -    obtain f where f: "f 0 = (SOME p. ?P p 0)" "\<forall>n. f (Suc n) = (SOME p. ?P p (f n))" by blast
1.108 -    have "?P (f 0) 0"  unfolding f(1) some_eq_ex[of "\<lambda>p. ?P p 0"]
1.109 -      using H apply -
1.110 -      apply (erule allE[where x=0], erule exE, rule_tac x="p" in exI)
1.111 -      unfolding order_le_less by blast
1.112 -    hence f0: "f 0 > 0" "\<forall>m \<ge> f 0. s m \<le> s (f 0)" by blast+
1.113 -    {fix n
1.114 -      have "?P (f (Suc n)) (f n)"
1.115 -        unfolding f(2)[rule_format, of n] some_eq_ex[of "\<lambda>p. ?P p (f n)"]
1.116 -        using H apply -
1.117 -      apply (erule allE[where x="f n"], erule exE, rule_tac x="p" in exI)
1.118 -      unfolding order_le_less by blast
1.119 -    hence "f (Suc n) > f n" "\<forall>m \<ge> f (Suc n). s m \<le> s (f (Suc n))" by blast+}
1.120 -  note fSuc = this
1.121 -    {fix p q assume pq: "p \<ge> f q"
1.122 -      have "s p \<le> s(f(q))"  using f0(2)[rule_format, of p] pq fSuc
1.123 -        by (cases q, simp_all) }
1.124 -    note pqth = this
1.125 -    {fix q
1.126 -      have "f (Suc q) > f q" apply (induct q)
1.127 -        using f0(1) fSuc(1)[of 0] apply simp by (rule fSuc(1))}
1.128 -    note fss = this
1.129 -    from fss have th1: "subseq f" unfolding subseq_Suc_iff ..
1.130 -    {fix a b
1.131 -      have "f a \<le> f (a + b)"
1.132 -      proof(induct b)
1.133 -        case 0 thus ?case by simp
1.134 -      next
1.135 -        case (Suc b)
1.136 -        from fSuc(1)[of "a + b"] Suc.hyps show ?case by simp
1.137 -      qed}
1.138 -    note fmon0 = this
1.139 -    have "monoseq (\<lambda>n. s (f n))"
1.140 -    proof-
1.141 -      {fix n
1.142 -        have "s (f n) \<ge> s (f (Suc n))"
1.143 -        proof(cases n)
1.144 -          case 0
1.145 -          assume n0: "n = 0"
1.146 -          from fSuc(1)[of 0] have th0: "f 0 \<le> f (Suc 0)" by simp
1.147 -          from f0(2)[rule_format, OF th0] show ?thesis  using n0 by simp
1.148 -        next
1.149 -          case (Suc m)
1.150 -          assume m: "n = Suc m"
1.151 -          from fSuc(1)[of n] m have th0: "f (Suc m) \<le> f (Suc (Suc m))" by simp
1.152 -          from m fSuc(2)[rule_format, OF th0] show ?thesis by simp
1.153 -        qed}
1.154 -      thus "monoseq (\<lambda>n. s (f n))" unfolding monoseq_Suc by blast
1.155 +text{* for any sequence, there is a monotonic subsequence *}
1.156 +lemma seq_monosub:
1.157 +  fixes s :: "nat => 'a::linorder"
1.158 +  shows "\<exists>f. subseq f \<and> monoseq (\<lambda> n. (s (f n)))"
1.159 +proof cases
1.160 +  let "?P p n" = "p > n \<and> (\<forall>m\<ge>p. s m \<le> s p)"
1.161 +  assume *: "\<forall>n. \<exists>p. ?P p n"
1.162 +  def f \<equiv> "nat_rec (SOME p. ?P p 0) (\<lambda>_ n. SOME p. ?P p n)"
1.163 +  have f_0: "f 0 = (SOME p. ?P p 0)" unfolding f_def by simp
1.164 +  have f_Suc: "\<And>i. f (Suc i) = (SOME p. ?P p (f i))" unfolding f_def nat_rec_Suc ..
1.165 +  have P_0: "?P (f 0) 0" unfolding f_0 using *[rule_format] by (rule someI2_ex) auto
1.166 +  have P_Suc: "\<And>i. ?P (f (Suc i)) (f i)" unfolding f_Suc using *[rule_format] by (rule someI2_ex) auto
1.167 +  then have "subseq f" unfolding subseq_Suc_iff by auto
1.168 +  moreover have "monoseq (\<lambda>n. s (f n))" unfolding monoseq_Suc
1.169 +  proof (intro disjI2 allI)
1.170 +    fix n show "s (f (Suc n)) \<le> s (f n)"
1.171 +    proof (cases n)
1.172 +      case 0 with P_Suc[of 0] P_0 show ?thesis by auto
1.173 +    next
1.174 +      case (Suc m)
1.175 +      from P_Suc[of n] Suc have "f (Suc m) \<le> f (Suc (Suc m))" by simp
1.176 +      with P_Suc Suc show ?thesis by simp
1.177      qed
1.178 -    with th1 have ?thesis by blast}
1.179 -  moreover
1.180 -  {fix N assume N: "\<forall>p >N. \<exists> m\<ge>p. s m > s p"
1.181 -    {fix p assume p: "p \<ge> Suc N"
1.182 -      hence pN: "p > N" by arith with N obtain m where m: "m \<ge> p" "s m > s p" by blast
1.183 -      have "m \<noteq> p" using m(2) by auto
1.184 -      with m have "\<exists>m>p. s p < s m" by - (rule exI[where x=m], auto)}
1.185 -    note th0 = this
1.186 -    let ?P = "\<lambda>m x. m > x \<and> s x < s m"
1.187 -    from nat_function_unique[of "SOME x. ?P x (Suc N)" "\<lambda>m x. SOME y. ?P y x"]
1.188 -    obtain f where f: "f 0 = (SOME x. ?P x (Suc N))"
1.189 -      "\<forall>n. f (Suc n) = (SOME m. ?P m (f n))" by blast
1.190 -    have "?P (f 0) (Suc N)"  unfolding f(1) some_eq_ex[of "\<lambda>p. ?P p (Suc N)"]
1.191 -      using N apply -
1.192 -      apply (erule allE[where x="Suc N"], clarsimp)
1.193 -      apply (rule_tac x="m" in exI)
1.194 -      apply auto
1.195 -      apply (subgoal_tac "Suc N \<noteq> m")
1.196 -      apply simp
1.197 -      apply (rule ccontr, simp)
1.198 -      done
1.199 -    hence f0: "f 0 > Suc N" "s (Suc N) < s (f 0)" by blast+
1.200 -    {fix n
1.201 -      have "f n > N \<and> ?P (f (Suc n)) (f n)"
1.202 -        unfolding f(2)[rule_format, of n] some_eq_ex[of "\<lambda>p. ?P p (f n)"]
1.203 -      proof (induct n)
1.204 -        case 0 thus ?case
1.205 -          using f0 N apply auto
1.206 -          apply (erule allE[where x="f 0"], clarsimp)
1.207 -          apply (rule_tac x="m" in exI, simp)
1.208 -          by (subgoal_tac "f 0 \<noteq> m", auto)
1.209 -      next
1.210 -        case (Suc n)
1.211 -        from Suc.hyps have Nfn: "N < f n" by blast
1.212 -        from Suc.hyps obtain m where m: "m > f n" "s (f n) < s m" by blast
1.213 -        with Nfn have mN: "m > N" by arith
1.214 -        note key = Suc.hyps[unfolded some_eq_ex[of "\<lambda>p. ?P p (f n)", symmetric] f(2)[rule_format, of n, symmetric]]
1.215 -
1.216 -        from key have th0: "f (Suc n) > N" by simp
1.217 -        from N[rule_format, OF th0]
1.218 -        obtain m' where m': "m' \<ge> f (Suc n)" "s (f (Suc n)) < s m'" by blast
1.219 -        have "m' \<noteq> f (Suc (n))" apply (rule ccontr) using m'(2) by auto
1.220 -        hence "m' > f (Suc n)" using m'(1) by simp
1.221 -        with key m'(2) show ?case by auto
1.222 -      qed}
1.223 -    note fSuc = this
1.224 -    {fix n
1.225 -      have "f n \<ge> Suc N \<and> f(Suc n) > f n \<and> s(f n) < s(f(Suc n))" using fSuc[of n] by auto
1.226 -      hence "f n \<ge> Suc N" "f(Suc n) > f n" "s(f n) < s(f(Suc n))" by blast+}
1.227 -    note thf = this
1.228 -    have sqf: "subseq f" unfolding subseq_Suc_iff using thf by simp
1.229 -    have "monoseq (\<lambda>n. s (f n))"  unfolding monoseq_Suc using thf
1.230 -      apply -
1.231 -      apply (rule disjI1)
1.232 -      apply auto
1.233 -      apply (rule order_less_imp_le)
1.234 -      apply blast
1.235 -      done
1.236 -    then have ?thesis  using sqf by blast}
1.237 -  ultimately show ?thesis unfolding linorder_not_less[symmetric] by blast
1.238 +  qed
1.239 +  ultimately show ?thesis by auto
1.240 +next
1.241 +  let "?P p m" = "m < p \<and> s m < s p"
1.242 +  assume "\<not> (\<forall>n. \<exists>p>n. (\<forall>m\<ge>p. s m \<le> s p))"
1.243 +  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.244 +  def f \<equiv> "nat_rec (SOME p. ?P p (Suc N)) (\<lambda>_ n. SOME p. ?P p n)"
1.245 +  have f_0: "f 0 = (SOME p. ?P p (Suc N))" unfolding f_def by simp
1.246 +  have f_Suc: "\<And>i. f (Suc i) = (SOME p. ?P p (f i))" unfolding f_def nat_rec_Suc ..
1.247 +  have P_0: "?P (f 0) (Suc N)"
1.248 +    unfolding f_0 some_eq_ex[of "\<lambda>p. ?P p (Suc N)"] using N[of "Suc N"] by auto
1.249 +  { fix i have "N < f i \<Longrightarrow> ?P (f (Suc i)) (f i)"
1.250 +      unfolding f_Suc some_eq_ex[of "\<lambda>p. ?P p (f i)"] using N[of "f i"] . }
1.251 +  note P' = this
1.252 +  { fix i have "N < f i \<and> ?P (f (Suc i)) (f i)"
1.253 +      by (induct i) (insert P_0 P', auto) }
1.254 +  then have "subseq f" "monoseq (\<lambda>x. s (f x))"
1.255 +    unfolding subseq_Suc_iff monoseq_Suc by (auto simp: not_le intro: less_imp_le)
1.256 +  then show ?thesis by auto
1.257  qed
1.258
1.259  lemma seq_suble: assumes sf: "subseq f" shows "n \<le> f n"
1.260 @@ -738,7 +652,7 @@
1.261  next
1.262    case (Suc n)
1.263    from sf[unfolded subseq_Suc_iff, rule_format, of n] Suc.hyps
1.264 -  have "n < f (Suc n)" by arith
1.265 +  have "n < f (Suc n)" by arith
1.266    thus ?case by arith
1.267  qed
1.268
1.269 @@ -887,7 +801,7 @@
1.271
1.272  text{*Main monotonicity theorem*}
1.273 -lemma Bseq_monoseq_convergent: "[| Bseq X; monoseq X |] ==> convergent X"
1.274 +lemma Bseq_monoseq_convergent: "[| Bseq X; monoseq X |] ==> convergent (X::nat\<Rightarrow>real)"
1.275  apply (simp add: monoseq_def, safe)
1.276  apply (rule_tac [2] convergent_minus_iff [THEN ssubst])
1.277  apply (drule_tac [2] Bseq_minus_iff [THEN ssubst])
1.278 @@ -897,9 +811,11 @@
1.279  subsubsection{*Increasing and Decreasing Series*}
1.280
1.281  lemma incseq_imp_monoseq:  "incseq X \<Longrightarrow> monoseq X"
1.282 -  by (simp add: incseq_def monoseq_def)
1.283 +  by (simp add: incseq_def monoseq_def)
1.284
1.285 -lemma incseq_le: assumes inc: "incseq X" and lim: "X ----> L" shows "X n \<le> L"
1.286 +lemma incseq_le:
1.287 +  fixes X :: "nat \<Rightarrow> real"
1.288 +  assumes inc: "incseq X" and lim: "X ----> L" shows "X n \<le> L"
1.289    using monoseq_le [OF incseq_imp_monoseq [OF inc] lim]
1.290  proof
1.291    assume "(\<forall>n. X n \<le> L) \<and> (\<forall>m n. m \<le> n \<longrightarrow> X m \<le> X n)"
1.292 @@ -939,11 +855,13 @@
1.293  lemma decseq_imp_monoseq:  "decseq X \<Longrightarrow> monoseq X"
1.294    by (simp add: decseq_def monoseq_def)
1.295
1.296 -lemma decseq_eq_incseq: "decseq X = incseq (\<lambda>n. - X n)"
1.297 +lemma decseq_eq_incseq:
1.298 +  fixes X :: "nat \<Rightarrow> 'a::ordered_ab_group_add" shows "decseq X = incseq (\<lambda>n. - X n)"
1.299    by (simp add: decseq_def incseq_def)
1.300
1.301
1.302 -lemma decseq_le: assumes dec: "decseq X" and lim: "X ----> L" shows "L \<le> X n"
1.303 +lemma decseq_le:
1.304 +  fixes X :: "nat \<Rightarrow> real" assumes dec: "decseq X" and lim: "X ----> L" shows "L \<le> X n"
1.305  proof -
1.306    have inc: "incseq (\<lambda>n. - X n)" using dec