Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
authorchaieb
Mon Mar 02 12:33:12 2009 +0000 (2009-03-02)
changeset 301966ffaa79c352c
parent 30193 391e10b42889
child 30197 7e440d357bc4
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
src/HOL/Library/Fundamental_Theorem_Algebra.thy
src/HOL/SEQ.thy
     1.1 --- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Mon Mar 02 08:26:03 2009 +0100
     1.2 +++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Mon Mar 02 12:33:12 2009 +0000
     1.3 @@ -177,151 +177,6 @@
     1.4    thus ?thesis by blast
     1.5  qed
     1.6  
     1.7 -
     1.8 -subsection{* Some theorems about Sequences*}
     1.9 -text{* Given a binary function @{text "f:: nat \<Rightarrow> 'a \<Rightarrow> 'a"}, its values are uniquely determined by a function g *}
    1.10 -
    1.11 -lemma num_Axiom: "EX! g. g 0 = e \<and> (\<forall>n. g (Suc n) = f n (g n))"
    1.12 -  unfolding Ex1_def
    1.13 -  apply (rule_tac x="nat_rec e f" in exI)
    1.14 -  apply (rule conjI)+
    1.15 -apply (rule def_nat_rec_0, simp)
    1.16 -apply (rule allI, rule def_nat_rec_Suc, simp)
    1.17 -apply (rule allI, rule impI, rule ext)
    1.18 -apply (erule conjE)
    1.19 -apply (induct_tac x)
    1.20 -apply (simp add: nat_rec_0)
    1.21 -apply (erule_tac x="n" in allE)
    1.22 -apply (simp)
    1.23 -done
    1.24 -
    1.25 -text{* for any sequence, there is a mootonic subsequence *}
    1.26 -lemma seq_monosub: "\<exists>f. subseq f \<and> monoseq (\<lambda> n. (s (f n)))"
    1.27 -proof-
    1.28 -  {assume H: "\<forall>n. \<exists>p >n. \<forall> m\<ge>p. s m \<le> s p"
    1.29 -    let ?P = "\<lambda> p n. p > n \<and> (\<forall>m \<ge> p. s m \<le> s p)"
    1.30 -    from num_Axiom[of "SOME p. ?P p 0" "\<lambda>p n. SOME p. ?P p n"]
    1.31 -    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.32 -    have "?P (f 0) 0"  unfolding f(1) some_eq_ex[of "\<lambda>p. ?P p 0"]
    1.33 -      using H apply - 
    1.34 -      apply (erule allE[where x=0], erule exE, rule_tac x="p" in exI) 
    1.35 -      unfolding order_le_less by blast 
    1.36 -    hence f0: "f 0 > 0" "\<forall>m \<ge> f 0. s m \<le> s (f 0)" by blast+
    1.37 -    {fix n
    1.38 -      have "?P (f (Suc n)) (f n)" 
    1.39 -	unfolding f(2)[rule_format, of n] some_eq_ex[of "\<lambda>p. ?P p (f n)"]
    1.40 -	using H apply - 
    1.41 -      apply (erule allE[where x="f n"], erule exE, rule_tac x="p" in exI) 
    1.42 -      unfolding order_le_less by blast 
    1.43 -    hence "f (Suc n) > f n" "\<forall>m \<ge> f (Suc n). s m \<le> s (f (Suc n))" by blast+}
    1.44 -  note fSuc = this
    1.45 -    {fix p q assume pq: "p \<ge> f q"
    1.46 -      have "s p \<le> s(f(q))"  using f0(2)[rule_format, of p] pq fSuc
    1.47 -	by (cases q, simp_all) }
    1.48 -    note pqth = this
    1.49 -    {fix q
    1.50 -      have "f (Suc q) > f q" apply (induct q) 
    1.51 -	using f0(1) fSuc(1)[of 0] apply simp by (rule fSuc(1))}
    1.52 -    note fss = this
    1.53 -    from fss have th1: "subseq f" unfolding subseq_Suc_iff ..
    1.54 -    {fix a b 
    1.55 -      have "f a \<le> f (a + b)"
    1.56 -      proof(induct b)
    1.57 -	case 0 thus ?case by simp
    1.58 -      next
    1.59 -	case (Suc b)
    1.60 -	from fSuc(1)[of "a + b"] Suc.hyps show ?case by simp
    1.61 -      qed}
    1.62 -    note fmon0 = this
    1.63 -    have "monoseq (\<lambda>n. s (f n))" 
    1.64 -    proof-
    1.65 -      {fix n
    1.66 -	have "s (f n) \<ge> s (f (Suc n))" 
    1.67 -	proof(cases n)
    1.68 -	  case 0
    1.69 -	  assume n0: "n = 0"
    1.70 -	  from fSuc(1)[of 0] have th0: "f 0 \<le> f (Suc 0)" by simp
    1.71 -	  from f0(2)[rule_format, OF th0] show ?thesis  using n0 by simp
    1.72 -	next
    1.73 -	  case (Suc m)
    1.74 -	  assume m: "n = Suc m"
    1.75 -	  from fSuc(1)[of n] m have th0: "f (Suc m) \<le> f (Suc (Suc m))" by simp
    1.76 -	  from m fSuc(2)[rule_format, OF th0] show ?thesis by simp 
    1.77 -	qed}
    1.78 -      thus "monoseq (\<lambda>n. s (f n))" unfolding monoseq_Suc by blast 
    1.79 -    qed
    1.80 -    with th1 have ?thesis by blast}
    1.81 -  moreover
    1.82 -  {fix N assume N: "\<forall>p >N. \<exists> m\<ge>p. s m > s p"
    1.83 -    {fix p assume p: "p \<ge> Suc N" 
    1.84 -      hence pN: "p > N" by arith with N obtain m where m: "m \<ge> p" "s m > s p" by blast
    1.85 -      have "m \<noteq> p" using m(2) by auto 
    1.86 -      with m have "\<exists>m>p. s p < s m" by - (rule exI[where x=m], auto)}
    1.87 -    note th0 = this
    1.88 -    let ?P = "\<lambda>m x. m > x \<and> s x < s m"
    1.89 -    from num_Axiom[of "SOME x. ?P x (Suc N)" "\<lambda>m x. SOME y. ?P y x"]
    1.90 -    obtain f where f: "f 0 = (SOME x. ?P x (Suc N))" 
    1.91 -      "\<forall>n. f (Suc n) = (SOME m. ?P m (f n))" by blast
    1.92 -    have "?P (f 0) (Suc N)"  unfolding f(1) some_eq_ex[of "\<lambda>p. ?P p (Suc N)"]
    1.93 -      using N apply - 
    1.94 -      apply (erule allE[where x="Suc N"], clarsimp)
    1.95 -      apply (rule_tac x="m" in exI)
    1.96 -      apply auto
    1.97 -      apply (subgoal_tac "Suc N \<noteq> m")
    1.98 -      apply simp
    1.99 -      apply (rule ccontr, simp)
   1.100 -      done
   1.101 -    hence f0: "f 0 > Suc N" "s (Suc N) < s (f 0)" by blast+
   1.102 -    {fix n
   1.103 -      have "f n > N \<and> ?P (f (Suc n)) (f n)"
   1.104 -	unfolding f(2)[rule_format, of n] some_eq_ex[of "\<lambda>p. ?P p (f n)"]
   1.105 -      proof (induct n)
   1.106 -	case 0 thus ?case
   1.107 -	  using f0 N apply auto 
   1.108 -	  apply (erule allE[where x="f 0"], clarsimp) 
   1.109 -	  apply (rule_tac x="m" in exI, simp)
   1.110 -	  by (subgoal_tac "f 0 \<noteq> m", auto)
   1.111 -      next
   1.112 -	case (Suc n)
   1.113 -	from Suc.hyps have Nfn: "N < f n" by blast
   1.114 -	from Suc.hyps obtain m where m: "m > f n" "s (f n) < s m" by blast
   1.115 -	with Nfn have mN: "m > N" by arith
   1.116 -	note key = Suc.hyps[unfolded some_eq_ex[of "\<lambda>p. ?P p (f n)", symmetric] f(2)[rule_format, of n, symmetric]]
   1.117 -	
   1.118 -	from key have th0: "f (Suc n) > N" by simp
   1.119 -	from N[rule_format, OF th0]
   1.120 -	obtain m' where m': "m' \<ge> f (Suc n)" "s (f (Suc n)) < s m'" by blast
   1.121 -	have "m' \<noteq> f (Suc (n))" apply (rule ccontr) using m'(2) by auto
   1.122 -	hence "m' > f (Suc n)" using m'(1) by simp
   1.123 -	with key m'(2) show ?case by auto
   1.124 -      qed}
   1.125 -    note fSuc = this
   1.126 -    {fix n
   1.127 -      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.128 -      hence "f n \<ge> Suc N" "f(Suc n) > f n" "s(f n) < s(f(Suc n))" by blast+}
   1.129 -    note thf = this
   1.130 -    have sqf: "subseq f" unfolding subseq_Suc_iff using thf by simp
   1.131 -    have "monoseq (\<lambda>n. s (f n))"  unfolding monoseq_Suc using thf
   1.132 -      apply -
   1.133 -      apply (rule disjI1)
   1.134 -      apply auto
   1.135 -      apply (rule order_less_imp_le)
   1.136 -      apply blast
   1.137 -      done
   1.138 -    then have ?thesis  using sqf by blast}
   1.139 -  ultimately show ?thesis unfolding linorder_not_less[symmetric] by blast
   1.140 -qed
   1.141 -
   1.142 -lemma seq_suble: assumes sf: "subseq f" shows "n \<le> f n"
   1.143 -proof(induct n)
   1.144 -  case 0 thus ?case by simp
   1.145 -next
   1.146 -  case (Suc n)
   1.147 -  from sf[unfolded subseq_Suc_iff, rule_format, of n] Suc.hyps
   1.148 -  have "n < f (Suc n)" by arith 
   1.149 -  thus ?case by arith
   1.150 -qed
   1.151 -
   1.152  subsection {* Fundamental theorem of algebra *}
   1.153  lemma  unimodular_reduce_norm:
   1.154    assumes md: "cmod z = 1"
   1.155 @@ -407,7 +262,6 @@
   1.156    ultimately show "\<exists>z. ?P z n" by blast
   1.157  qed
   1.158  
   1.159 -
   1.160  text{* Bolzano-Weierstrass type property for closed disc in complex plane. *}
   1.161  
   1.162  lemma metric_bound_lemma: "cmod (x - y) <= \<bar>Re x - Re y\<bar> + \<bar>Im x - Im y\<bar>"
     2.1 --- a/src/HOL/SEQ.thy	Mon Mar 02 08:26:03 2009 +0100
     2.2 +++ b/src/HOL/SEQ.thy	Mon Mar 02 12:33:12 2009 +0000
     2.3 @@ -646,8 +646,21 @@
     2.4  apply (drule LIMSEQ_minus, auto)
     2.5  done
     2.6  
     2.7 +text{* Given a binary function @{text "f:: nat \<Rightarrow> 'a \<Rightarrow> 'a"}, its values are uniquely determined by a function g *}
     2.8  
     2.9 -subsection {* Bounded Monotonic Sequences *}
    2.10 +lemma nat_function_unique: "EX! g. g 0 = e \<and> (\<forall>n. g (Suc n) = f n (g n))"
    2.11 +  unfolding Ex1_def
    2.12 +  apply (rule_tac x="nat_rec e f" in exI)
    2.13 +  apply (rule conjI)+
    2.14 +apply (rule def_nat_rec_0, simp)
    2.15 +apply (rule allI, rule def_nat_rec_Suc, simp)
    2.16 +apply (rule allI, rule impI, rule ext)
    2.17 +apply (erule conjE)
    2.18 +apply (induct_tac x)
    2.19 +apply (simp add: nat_rec_0)
    2.20 +apply (erule_tac x="n" in allE)
    2.21 +apply (simp)
    2.22 +done
    2.23  
    2.24  text{*Subsequence (alternative definition, (e.g. Hoskins)*}
    2.25  
    2.26 @@ -746,6 +759,136 @@
    2.27    qed auto
    2.28  qed
    2.29  
    2.30 +text{* for any sequence, there is a mootonic subsequence *}
    2.31 +lemma seq_monosub: "\<exists>f. subseq f \<and> monoseq (\<lambda> n. (s (f n)))"
    2.32 +proof-
    2.33 +  {assume H: "\<forall>n. \<exists>p >n. \<forall> m\<ge>p. s m \<le> s p"
    2.34 +    let ?P = "\<lambda> p n. p > n \<and> (\<forall>m \<ge> p. s m \<le> s p)"
    2.35 +    from nat_function_unique[of "SOME p. ?P p 0" "\<lambda>p n. SOME p. ?P p n"]
    2.36 +    obtain f where f: "f 0 = (SOME p. ?P p 0)" "\<forall>n. f (Suc n) = (SOME p. ?P p (f n))" by blast
    2.37 +    have "?P (f 0) 0"  unfolding f(1) some_eq_ex[of "\<lambda>p. ?P p 0"]
    2.38 +      using H apply - 
    2.39 +      apply (erule allE[where x=0], erule exE, rule_tac x="p" in exI) 
    2.40 +      unfolding order_le_less by blast 
    2.41 +    hence f0: "f 0 > 0" "\<forall>m \<ge> f 0. s m \<le> s (f 0)" by blast+
    2.42 +    {fix n
    2.43 +      have "?P (f (Suc n)) (f n)" 
    2.44 +	unfolding f(2)[rule_format, of n] some_eq_ex[of "\<lambda>p. ?P p (f n)"]
    2.45 +	using H apply - 
    2.46 +      apply (erule allE[where x="f n"], erule exE, rule_tac x="p" in exI) 
    2.47 +      unfolding order_le_less by blast 
    2.48 +    hence "f (Suc n) > f n" "\<forall>m \<ge> f (Suc n). s m \<le> s (f (Suc n))" by blast+}
    2.49 +  note fSuc = this
    2.50 +    {fix p q assume pq: "p \<ge> f q"
    2.51 +      have "s p \<le> s(f(q))"  using f0(2)[rule_format, of p] pq fSuc
    2.52 +	by (cases q, simp_all) }
    2.53 +    note pqth = this
    2.54 +    {fix q
    2.55 +      have "f (Suc q) > f q" apply (induct q) 
    2.56 +	using f0(1) fSuc(1)[of 0] apply simp by (rule fSuc(1))}
    2.57 +    note fss = this
    2.58 +    from fss have th1: "subseq f" unfolding subseq_Suc_iff ..
    2.59 +    {fix a b 
    2.60 +      have "f a \<le> f (a + b)"
    2.61 +      proof(induct b)
    2.62 +	case 0 thus ?case by simp
    2.63 +      next
    2.64 +	case (Suc b)
    2.65 +	from fSuc(1)[of "a + b"] Suc.hyps show ?case by simp
    2.66 +      qed}
    2.67 +    note fmon0 = this
    2.68 +    have "monoseq (\<lambda>n. s (f n))" 
    2.69 +    proof-
    2.70 +      {fix n
    2.71 +	have "s (f n) \<ge> s (f (Suc n))" 
    2.72 +	proof(cases n)
    2.73 +	  case 0
    2.74 +	  assume n0: "n = 0"
    2.75 +	  from fSuc(1)[of 0] have th0: "f 0 \<le> f (Suc 0)" by simp
    2.76 +	  from f0(2)[rule_format, OF th0] show ?thesis  using n0 by simp
    2.77 +	next
    2.78 +	  case (Suc m)
    2.79 +	  assume m: "n = Suc m"
    2.80 +	  from fSuc(1)[of n] m have th0: "f (Suc m) \<le> f (Suc (Suc m))" by simp
    2.81 +	  from m fSuc(2)[rule_format, OF th0] show ?thesis by simp 
    2.82 +	qed}
    2.83 +      thus "monoseq (\<lambda>n. s (f n))" unfolding monoseq_Suc by blast 
    2.84 +    qed
    2.85 +    with th1 have ?thesis by blast}
    2.86 +  moreover
    2.87 +  {fix N assume N: "\<forall>p >N. \<exists> m\<ge>p. s m > s p"
    2.88 +    {fix p assume p: "p \<ge> Suc N" 
    2.89 +      hence pN: "p > N" by arith with N obtain m where m: "m \<ge> p" "s m > s p" by blast
    2.90 +      have "m \<noteq> p" using m(2) by auto 
    2.91 +      with m have "\<exists>m>p. s p < s m" by - (rule exI[where x=m], auto)}
    2.92 +    note th0 = this
    2.93 +    let ?P = "\<lambda>m x. m > x \<and> s x < s m"
    2.94 +    from nat_function_unique[of "SOME x. ?P x (Suc N)" "\<lambda>m x. SOME y. ?P y x"]
    2.95 +    obtain f where f: "f 0 = (SOME x. ?P x (Suc N))" 
    2.96 +      "\<forall>n. f (Suc n) = (SOME m. ?P m (f n))" by blast
    2.97 +    have "?P (f 0) (Suc N)"  unfolding f(1) some_eq_ex[of "\<lambda>p. ?P p (Suc N)"]
    2.98 +      using N apply - 
    2.99 +      apply (erule allE[where x="Suc N"], clarsimp)
   2.100 +      apply (rule_tac x="m" in exI)
   2.101 +      apply auto
   2.102 +      apply (subgoal_tac "Suc N \<noteq> m")
   2.103 +      apply simp
   2.104 +      apply (rule ccontr, simp)
   2.105 +      done
   2.106 +    hence f0: "f 0 > Suc N" "s (Suc N) < s (f 0)" by blast+
   2.107 +    {fix n
   2.108 +      have "f n > N \<and> ?P (f (Suc n)) (f n)"
   2.109 +	unfolding f(2)[rule_format, of n] some_eq_ex[of "\<lambda>p. ?P p (f n)"]
   2.110 +      proof (induct n)
   2.111 +	case 0 thus ?case
   2.112 +	  using f0 N apply auto 
   2.113 +	  apply (erule allE[where x="f 0"], clarsimp) 
   2.114 +	  apply (rule_tac x="m" in exI, simp)
   2.115 +	  by (subgoal_tac "f 0 \<noteq> m", auto)
   2.116 +      next
   2.117 +	case (Suc n)
   2.118 +	from Suc.hyps have Nfn: "N < f n" by blast
   2.119 +	from Suc.hyps obtain m where m: "m > f n" "s (f n) < s m" by blast
   2.120 +	with Nfn have mN: "m > N" by arith
   2.121 +	note key = Suc.hyps[unfolded some_eq_ex[of "\<lambda>p. ?P p (f n)", symmetric] f(2)[rule_format, of n, symmetric]]
   2.122 +	
   2.123 +	from key have th0: "f (Suc n) > N" by simp
   2.124 +	from N[rule_format, OF th0]
   2.125 +	obtain m' where m': "m' \<ge> f (Suc n)" "s (f (Suc n)) < s m'" by blast
   2.126 +	have "m' \<noteq> f (Suc (n))" apply (rule ccontr) using m'(2) by auto
   2.127 +	hence "m' > f (Suc n)" using m'(1) by simp
   2.128 +	with key m'(2) show ?case by auto
   2.129 +      qed}
   2.130 +    note fSuc = this
   2.131 +    {fix n
   2.132 +      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 
   2.133 +      hence "f n \<ge> Suc N" "f(Suc n) > f n" "s(f n) < s(f(Suc n))" by blast+}
   2.134 +    note thf = this
   2.135 +    have sqf: "subseq f" unfolding subseq_Suc_iff using thf by simp
   2.136 +    have "monoseq (\<lambda>n. s (f n))"  unfolding monoseq_Suc using thf
   2.137 +      apply -
   2.138 +      apply (rule disjI1)
   2.139 +      apply auto
   2.140 +      apply (rule order_less_imp_le)
   2.141 +      apply blast
   2.142 +      done
   2.143 +    then have ?thesis  using sqf by blast}
   2.144 +  ultimately show ?thesis unfolding linorder_not_less[symmetric] by blast
   2.145 +qed
   2.146 +
   2.147 +lemma seq_suble: assumes sf: "subseq f" shows "n \<le> f n"
   2.148 +proof(induct n)
   2.149 +  case 0 thus ?case by simp
   2.150 +next
   2.151 +  case (Suc n)
   2.152 +  from sf[unfolded subseq_Suc_iff, rule_format, of n] Suc.hyps
   2.153 +  have "n < f (Suc n)" by arith 
   2.154 +  thus ?case by arith
   2.155 +qed
   2.156 +
   2.157 +subsection {* Bounded Monotonic Sequences *}
   2.158 +
   2.159 +
   2.160  text{*Bounded Sequence*}
   2.161  
   2.162  lemma BseqD: "Bseq X ==> \<exists>K. 0 < K & (\<forall>n. norm (X n) \<le> K)"