src/HOL/SEQ.thy
changeset 32960 69916a850301
parent 32877 6f09346c7c08
child 33042 ddf1f03a9ad9
     1.1 --- a/src/HOL/SEQ.thy	Sat Oct 17 01:05:59 2009 +0200
     1.2 +++ b/src/HOL/SEQ.thy	Sat Oct 17 14:43:18 2009 +0200
     1.3 @@ -1,9 +1,10 @@
     1.4 -(*  Title       : SEQ.thy
     1.5 -    Author      : Jacques D. Fleuriot
     1.6 -    Copyright   : 1998  University of Cambridge
     1.7 -    Description : Convergence of sequences and series
     1.8 -    Conversion to Isar and new proofs by Lawrence C Paulson, 2004
     1.9 -    Additional contributions by Jeremy Avigad and Brian Huffman
    1.10 +(*  Title:      HOL/SEQ.thy
    1.11 +    Author:     Jacques D. Fleuriot, University of Cambridge
    1.12 +    Author:     Lawrence C Paulson
    1.13 +    Author:     Jeremy Avigad
    1.14 +    Author:     Brian Huffman
    1.15 +
    1.16 +Convergence of sequences and series.
    1.17  *)
    1.18  
    1.19  header {* Sequences and Convergence *}
    1.20 @@ -337,10 +338,10 @@
    1.21      have "\<bar>f (N+k) - l\<bar> < e"
    1.22      proof (induct k)
    1.23        case 0 show ?case using N
    1.24 -	by simp   
    1.25 +        by simp   
    1.26      next
    1.27        case (Suc k) thus ?case using N inc [of "N+k"]
    1.28 -	by simp
    1.29 +        by simp
    1.30      qed 
    1.31    } note 1 = this
    1.32    { fix n
    1.33 @@ -549,11 +550,11 @@
    1.34      proof (simp add: LIMSEQ_iff)
    1.35        assume "\<forall>r>0. \<exists>no. \<forall>n\<ge>no. \<bar>f n - lim f\<bar> < r"
    1.36        hence "\<exists>no. \<forall>n\<ge>no. \<bar>f n - lim f\<bar> < lim f - x"
    1.37 -	by (metis 0)
    1.38 +        by (metis 0)
    1.39        from this obtain no where "\<forall>n\<ge>no. \<bar>f n - lim f\<bar> < lim f - x"
    1.40 -	by blast
    1.41 +        by blast
    1.42        thus "lim f \<le> x"
    1.43 -	by (metis add_cancel_end add_minus_cancel diff_def linorder_linear 
    1.44 +        by (metis add_cancel_end add_minus_cancel diff_def linorder_linear 
    1.45                    linorder_not_le minus_diff_eq abs_diff_less_iff fn_le) 
    1.46      qed
    1.47  qed
    1.48 @@ -685,45 +686,45 @@
    1.49      hence f0: "f 0 > 0" "\<forall>m \<ge> f 0. s m \<le> s (f 0)" by blast+
    1.50      {fix n
    1.51        have "?P (f (Suc n)) (f n)" 
    1.52 -	unfolding f(2)[rule_format, of n] some_eq_ex[of "\<lambda>p. ?P p (f n)"]
    1.53 -	using H apply - 
    1.54 +        unfolding f(2)[rule_format, of n] some_eq_ex[of "\<lambda>p. ?P p (f n)"]
    1.55 +        using H apply - 
    1.56        apply (erule allE[where x="f n"], erule exE, rule_tac x="p" in exI) 
    1.57        unfolding order_le_less by blast 
    1.58      hence "f (Suc n) > f n" "\<forall>m \<ge> f (Suc n). s m \<le> s (f (Suc n))" by blast+}
    1.59    note fSuc = this
    1.60      {fix p q assume pq: "p \<ge> f q"
    1.61        have "s p \<le> s(f(q))"  using f0(2)[rule_format, of p] pq fSuc
    1.62 -	by (cases q, simp_all) }
    1.63 +        by (cases q, simp_all) }
    1.64      note pqth = this
    1.65      {fix q
    1.66        have "f (Suc q) > f q" apply (induct q) 
    1.67 -	using f0(1) fSuc(1)[of 0] apply simp by (rule fSuc(1))}
    1.68 +        using f0(1) fSuc(1)[of 0] apply simp by (rule fSuc(1))}
    1.69      note fss = this
    1.70      from fss have th1: "subseq f" unfolding subseq_Suc_iff ..
    1.71      {fix a b 
    1.72        have "f a \<le> f (a + b)"
    1.73        proof(induct b)
    1.74 -	case 0 thus ?case by simp
    1.75 +        case 0 thus ?case by simp
    1.76        next
    1.77 -	case (Suc b)
    1.78 -	from fSuc(1)[of "a + b"] Suc.hyps show ?case by simp
    1.79 +        case (Suc b)
    1.80 +        from fSuc(1)[of "a + b"] Suc.hyps show ?case by simp
    1.81        qed}
    1.82      note fmon0 = this
    1.83      have "monoseq (\<lambda>n. s (f n))" 
    1.84      proof-
    1.85        {fix n
    1.86 -	have "s (f n) \<ge> s (f (Suc n))" 
    1.87 -	proof(cases n)
    1.88 -	  case 0
    1.89 -	  assume n0: "n = 0"
    1.90 -	  from fSuc(1)[of 0] have th0: "f 0 \<le> f (Suc 0)" by simp
    1.91 -	  from f0(2)[rule_format, OF th0] show ?thesis  using n0 by simp
    1.92 -	next
    1.93 -	  case (Suc m)
    1.94 -	  assume m: "n = Suc m"
    1.95 -	  from fSuc(1)[of n] m have th0: "f (Suc m) \<le> f (Suc (Suc m))" by simp
    1.96 -	  from m fSuc(2)[rule_format, OF th0] show ?thesis by simp 
    1.97 -	qed}
    1.98 +        have "s (f n) \<ge> s (f (Suc n))" 
    1.99 +        proof(cases n)
   1.100 +          case 0
   1.101 +          assume n0: "n = 0"
   1.102 +          from fSuc(1)[of 0] have th0: "f 0 \<le> f (Suc 0)" by simp
   1.103 +          from f0(2)[rule_format, OF th0] show ?thesis  using n0 by simp
   1.104 +        next
   1.105 +          case (Suc m)
   1.106 +          assume m: "n = Suc m"
   1.107 +          from fSuc(1)[of n] m have th0: "f (Suc m) \<le> f (Suc (Suc m))" by simp
   1.108 +          from m fSuc(2)[rule_format, OF th0] show ?thesis by simp 
   1.109 +        qed}
   1.110        thus "monoseq (\<lambda>n. s (f n))" unfolding monoseq_Suc by blast 
   1.111      qed
   1.112      with th1 have ?thesis by blast}
   1.113 @@ -750,26 +751,26 @@
   1.114      hence f0: "f 0 > Suc N" "s (Suc N) < s (f 0)" by blast+
   1.115      {fix n
   1.116        have "f n > N \<and> ?P (f (Suc n)) (f n)"
   1.117 -	unfolding f(2)[rule_format, of n] some_eq_ex[of "\<lambda>p. ?P p (f n)"]
   1.118 +        unfolding f(2)[rule_format, of n] some_eq_ex[of "\<lambda>p. ?P p (f n)"]
   1.119        proof (induct n)
   1.120 -	case 0 thus ?case
   1.121 -	  using f0 N apply auto 
   1.122 -	  apply (erule allE[where x="f 0"], clarsimp) 
   1.123 -	  apply (rule_tac x="m" in exI, simp)
   1.124 -	  by (subgoal_tac "f 0 \<noteq> m", auto)
   1.125 +        case 0 thus ?case
   1.126 +          using f0 N apply auto 
   1.127 +          apply (erule allE[where x="f 0"], clarsimp) 
   1.128 +          apply (rule_tac x="m" in exI, simp)
   1.129 +          by (subgoal_tac "f 0 \<noteq> m", auto)
   1.130        next
   1.131 -	case (Suc n)
   1.132 -	from Suc.hyps have Nfn: "N < f n" by blast
   1.133 -	from Suc.hyps obtain m where m: "m > f n" "s (f n) < s m" by blast
   1.134 -	with Nfn have mN: "m > N" by arith
   1.135 -	note key = Suc.hyps[unfolded some_eq_ex[of "\<lambda>p. ?P p (f n)", symmetric] f(2)[rule_format, of n, symmetric]]
   1.136 -	
   1.137 -	from key have th0: "f (Suc n) > N" by simp
   1.138 -	from N[rule_format, OF th0]
   1.139 -	obtain m' where m': "m' \<ge> f (Suc n)" "s (f (Suc n)) < s m'" by blast
   1.140 -	have "m' \<noteq> f (Suc (n))" apply (rule ccontr) using m'(2) by auto
   1.141 -	hence "m' > f (Suc n)" using m'(1) by simp
   1.142 -	with key m'(2) show ?case by auto
   1.143 +        case (Suc n)
   1.144 +        from Suc.hyps have Nfn: "N < f n" by blast
   1.145 +        from Suc.hyps obtain m where m: "m > f n" "s (f n) < s m" by blast
   1.146 +        with Nfn have mN: "m > N" by arith
   1.147 +        note key = Suc.hyps[unfolded some_eq_ex[of "\<lambda>p. ?P p (f n)", symmetric] f(2)[rule_format, of n, symmetric]]
   1.148 +        
   1.149 +        from key have th0: "f (Suc n) > N" by simp
   1.150 +        from N[rule_format, OF th0]
   1.151 +        obtain m' where m': "m' \<ge> f (Suc n)" "s (f (Suc n)) < s m'" by blast
   1.152 +        have "m' \<noteq> f (Suc (n))" apply (rule ccontr) using m'(2) by auto
   1.153 +        hence "m' > f (Suc n)" using m'(1) by simp
   1.154 +        with key m'(2) show ?case by auto
   1.155        qed}
   1.156      note fSuc = this
   1.157      {fix n