generalized monoseq, decseq and incseq; simplified proof for seq_monosub
authorhoelzl
Tue Dec 21 14:50:53 2010 +0100 (2010-12-21)
changeset 413671b65137d598c
parent 41362 3cb30e525ee9
child 41368 8afa26855137
generalized monoseq, decseq and incseq; simplified proof for seq_monosub
src/HOL/SEQ.thy
     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.72  apply (simp add: monoseq_def)
    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.77  by (simp add: monoseq_Suc)
    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.270  by (simp add: Bseq_def)
   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
   1.307      by (simp add: decseq_eq_incseq)
   1.308 @@ -1220,7 +1138,7 @@
   1.309  apply (auto dest: power_mono)
   1.310  done
   1.311  
   1.312 -lemma monoseq_realpow: "[| 0 \<le> x; x \<le> 1 |] ==> monoseq (%n. x ^ n)"
   1.313 +lemma monoseq_realpow: fixes x :: real shows "[| 0 \<le> x; x \<le> 1 |] ==> monoseq (%n. x ^ n)"
   1.314  apply (clarify intro!: mono_SucI2)
   1.315  apply (cut_tac n = n and N = "Suc n" and a = x in power_decreasing, auto)
   1.316  done