Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
--- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy Mon Mar 02 08:26:03 2009 +0100
+++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy Mon Mar 02 12:33:12 2009 +0000
@@ -177,151 +177,6 @@
thus ?thesis by blast
qed
-
-subsection{* Some theorems about Sequences*}
-text{* Given a binary function @{text "f:: nat \<Rightarrow> 'a \<Rightarrow> 'a"}, its values are uniquely determined by a function g *}
-
-lemma num_Axiom: "EX! g. g 0 = e \<and> (\<forall>n. g (Suc n) = f n (g n))"
- unfolding Ex1_def
- apply (rule_tac x="nat_rec e f" in exI)
- apply (rule conjI)+
-apply (rule def_nat_rec_0, simp)
-apply (rule allI, rule def_nat_rec_Suc, simp)
-apply (rule allI, rule impI, rule ext)
-apply (erule conjE)
-apply (induct_tac x)
-apply (simp add: nat_rec_0)
-apply (erule_tac x="n" in allE)
-apply (simp)
-done
-
-text{* for any sequence, there is a mootonic subsequence *}
-lemma seq_monosub: "\<exists>f. subseq f \<and> monoseq (\<lambda> n. (s (f n)))"
-proof-
- {assume H: "\<forall>n. \<exists>p >n. \<forall> m\<ge>p. s m \<le> s p"
- let ?P = "\<lambda> p n. p > n \<and> (\<forall>m \<ge> p. s m \<le> s p)"
- from num_Axiom[of "SOME p. ?P p 0" "\<lambda>p n. SOME p. ?P p n"]
- obtain f where f: "f 0 = (SOME p. ?P p 0)" "\<forall>n. f (Suc n) = (SOME p. ?P p (f n))" by blast
- have "?P (f 0) 0" unfolding f(1) some_eq_ex[of "\<lambda>p. ?P p 0"]
- using H apply -
- apply (erule allE[where x=0], erule exE, rule_tac x="p" in exI)
- unfolding order_le_less by blast
- hence f0: "f 0 > 0" "\<forall>m \<ge> f 0. s m \<le> s (f 0)" by blast+
- {fix n
- have "?P (f (Suc n)) (f n)"
- unfolding f(2)[rule_format, of n] some_eq_ex[of "\<lambda>p. ?P p (f n)"]
- using H apply -
- apply (erule allE[where x="f n"], erule exE, rule_tac x="p" in exI)
- unfolding order_le_less by blast
- hence "f (Suc n) > f n" "\<forall>m \<ge> f (Suc n). s m \<le> s (f (Suc n))" by blast+}
- note fSuc = this
- {fix p q assume pq: "p \<ge> f q"
- have "s p \<le> s(f(q))" using f0(2)[rule_format, of p] pq fSuc
- by (cases q, simp_all) }
- note pqth = this
- {fix q
- have "f (Suc q) > f q" apply (induct q)
- using f0(1) fSuc(1)[of 0] apply simp by (rule fSuc(1))}
- note fss = this
- from fss have th1: "subseq f" unfolding subseq_Suc_iff ..
- {fix a b
- have "f a \<le> f (a + b)"
- proof(induct b)
- case 0 thus ?case by simp
- next
- case (Suc b)
- from fSuc(1)[of "a + b"] Suc.hyps show ?case by simp
- qed}
- note fmon0 = this
- have "monoseq (\<lambda>n. s (f n))"
- proof-
- {fix n
- have "s (f n) \<ge> s (f (Suc n))"
- proof(cases n)
- case 0
- assume n0: "n = 0"
- from fSuc(1)[of 0] have th0: "f 0 \<le> f (Suc 0)" by simp
- from f0(2)[rule_format, OF th0] show ?thesis using n0 by simp
- next
- case (Suc m)
- assume m: "n = Suc m"
- from fSuc(1)[of n] m have th0: "f (Suc m) \<le> f (Suc (Suc m))" by simp
- from m fSuc(2)[rule_format, OF th0] show ?thesis by simp
- qed}
- thus "monoseq (\<lambda>n. s (f n))" unfolding monoseq_Suc by blast
- qed
- with th1 have ?thesis by blast}
- moreover
- {fix N assume N: "\<forall>p >N. \<exists> m\<ge>p. s m > s p"
- {fix p assume p: "p \<ge> Suc N"
- hence pN: "p > N" by arith with N obtain m where m: "m \<ge> p" "s m > s p" by blast
- have "m \<noteq> p" using m(2) by auto
- with m have "\<exists>m>p. s p < s m" by - (rule exI[where x=m], auto)}
- note th0 = this
- let ?P = "\<lambda>m x. m > x \<and> s x < s m"
- from num_Axiom[of "SOME x. ?P x (Suc N)" "\<lambda>m x. SOME y. ?P y x"]
- obtain f where f: "f 0 = (SOME x. ?P x (Suc N))"
- "\<forall>n. f (Suc n) = (SOME m. ?P m (f n))" by blast
- have "?P (f 0) (Suc N)" unfolding f(1) some_eq_ex[of "\<lambda>p. ?P p (Suc N)"]
- using N apply -
- apply (erule allE[where x="Suc N"], clarsimp)
- apply (rule_tac x="m" in exI)
- apply auto
- apply (subgoal_tac "Suc N \<noteq> m")
- apply simp
- apply (rule ccontr, simp)
- done
- hence f0: "f 0 > Suc N" "s (Suc N) < s (f 0)" by blast+
- {fix n
- have "f n > N \<and> ?P (f (Suc n)) (f n)"
- unfolding f(2)[rule_format, of n] some_eq_ex[of "\<lambda>p. ?P p (f n)"]
- proof (induct n)
- case 0 thus ?case
- using f0 N apply auto
- apply (erule allE[where x="f 0"], clarsimp)
- apply (rule_tac x="m" in exI, simp)
- by (subgoal_tac "f 0 \<noteq> m", auto)
- next
- case (Suc n)
- from Suc.hyps have Nfn: "N < f n" by blast
- from Suc.hyps obtain m where m: "m > f n" "s (f n) < s m" by blast
- with Nfn have mN: "m > N" by arith
- note key = Suc.hyps[unfolded some_eq_ex[of "\<lambda>p. ?P p (f n)", symmetric] f(2)[rule_format, of n, symmetric]]
-
- from key have th0: "f (Suc n) > N" by simp
- from N[rule_format, OF th0]
- obtain m' where m': "m' \<ge> f (Suc n)" "s (f (Suc n)) < s m'" by blast
- have "m' \<noteq> f (Suc (n))" apply (rule ccontr) using m'(2) by auto
- hence "m' > f (Suc n)" using m'(1) by simp
- with key m'(2) show ?case by auto
- qed}
- note fSuc = this
- {fix n
- 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
- hence "f n \<ge> Suc N" "f(Suc n) > f n" "s(f n) < s(f(Suc n))" by blast+}
- note thf = this
- have sqf: "subseq f" unfolding subseq_Suc_iff using thf by simp
- have "monoseq (\<lambda>n. s (f n))" unfolding monoseq_Suc using thf
- apply -
- apply (rule disjI1)
- apply auto
- apply (rule order_less_imp_le)
- apply blast
- done
- then have ?thesis using sqf by blast}
- ultimately show ?thesis unfolding linorder_not_less[symmetric] by blast
-qed
-
-lemma seq_suble: assumes sf: "subseq f" shows "n \<le> f n"
-proof(induct n)
- case 0 thus ?case by simp
-next
- case (Suc n)
- from sf[unfolded subseq_Suc_iff, rule_format, of n] Suc.hyps
- have "n < f (Suc n)" by arith
- thus ?case by arith
-qed
-
subsection {* Fundamental theorem of algebra *}
lemma unimodular_reduce_norm:
assumes md: "cmod z = 1"
@@ -407,7 +262,6 @@
ultimately show "\<exists>z. ?P z n" by blast
qed
-
text{* Bolzano-Weierstrass type property for closed disc in complex plane. *}
lemma metric_bound_lemma: "cmod (x - y) <= \<bar>Re x - Re y\<bar> + \<bar>Im x - Im y\<bar>"
--- a/src/HOL/SEQ.thy Mon Mar 02 08:26:03 2009 +0100
+++ b/src/HOL/SEQ.thy Mon Mar 02 12:33:12 2009 +0000
@@ -646,8 +646,21 @@
apply (drule LIMSEQ_minus, auto)
done
+text{* Given a binary function @{text "f:: nat \<Rightarrow> 'a \<Rightarrow> 'a"}, its values are uniquely determined by a function g *}
-subsection {* Bounded Monotonic Sequences *}
+lemma nat_function_unique: "EX! g. g 0 = e \<and> (\<forall>n. g (Suc n) = f n (g n))"
+ unfolding Ex1_def
+ apply (rule_tac x="nat_rec e f" in exI)
+ apply (rule conjI)+
+apply (rule def_nat_rec_0, simp)
+apply (rule allI, rule def_nat_rec_Suc, simp)
+apply (rule allI, rule impI, rule ext)
+apply (erule conjE)
+apply (induct_tac x)
+apply (simp add: nat_rec_0)
+apply (erule_tac x="n" in allE)
+apply (simp)
+done
text{*Subsequence (alternative definition, (e.g. Hoskins)*}
@@ -746,6 +759,136 @@
qed auto
qed
+text{* for any sequence, there is a mootonic subsequence *}
+lemma seq_monosub: "\<exists>f. subseq f \<and> monoseq (\<lambda> n. (s (f n)))"
+proof-
+ {assume H: "\<forall>n. \<exists>p >n. \<forall> m\<ge>p. s m \<le> s p"
+ let ?P = "\<lambda> p n. p > n \<and> (\<forall>m \<ge> p. s m \<le> s p)"
+ from nat_function_unique[of "SOME p. ?P p 0" "\<lambda>p n. SOME p. ?P p n"]
+ obtain f where f: "f 0 = (SOME p. ?P p 0)" "\<forall>n. f (Suc n) = (SOME p. ?P p (f n))" by blast
+ have "?P (f 0) 0" unfolding f(1) some_eq_ex[of "\<lambda>p. ?P p 0"]
+ using H apply -
+ apply (erule allE[where x=0], erule exE, rule_tac x="p" in exI)
+ unfolding order_le_less by blast
+ hence f0: "f 0 > 0" "\<forall>m \<ge> f 0. s m \<le> s (f 0)" by blast+
+ {fix n
+ have "?P (f (Suc n)) (f n)"
+ unfolding f(2)[rule_format, of n] some_eq_ex[of "\<lambda>p. ?P p (f n)"]
+ using H apply -
+ apply (erule allE[where x="f n"], erule exE, rule_tac x="p" in exI)
+ unfolding order_le_less by blast
+ hence "f (Suc n) > f n" "\<forall>m \<ge> f (Suc n). s m \<le> s (f (Suc n))" by blast+}
+ note fSuc = this
+ {fix p q assume pq: "p \<ge> f q"
+ have "s p \<le> s(f(q))" using f0(2)[rule_format, of p] pq fSuc
+ by (cases q, simp_all) }
+ note pqth = this
+ {fix q
+ have "f (Suc q) > f q" apply (induct q)
+ using f0(1) fSuc(1)[of 0] apply simp by (rule fSuc(1))}
+ note fss = this
+ from fss have th1: "subseq f" unfolding subseq_Suc_iff ..
+ {fix a b
+ have "f a \<le> f (a + b)"
+ proof(induct b)
+ case 0 thus ?case by simp
+ next
+ case (Suc b)
+ from fSuc(1)[of "a + b"] Suc.hyps show ?case by simp
+ qed}
+ note fmon0 = this
+ have "monoseq (\<lambda>n. s (f n))"
+ proof-
+ {fix n
+ have "s (f n) \<ge> s (f (Suc n))"
+ proof(cases n)
+ case 0
+ assume n0: "n = 0"
+ from fSuc(1)[of 0] have th0: "f 0 \<le> f (Suc 0)" by simp
+ from f0(2)[rule_format, OF th0] show ?thesis using n0 by simp
+ next
+ case (Suc m)
+ assume m: "n = Suc m"
+ from fSuc(1)[of n] m have th0: "f (Suc m) \<le> f (Suc (Suc m))" by simp
+ from m fSuc(2)[rule_format, OF th0] show ?thesis by simp
+ qed}
+ thus "monoseq (\<lambda>n. s (f n))" unfolding monoseq_Suc by blast
+ qed
+ with th1 have ?thesis by blast}
+ moreover
+ {fix N assume N: "\<forall>p >N. \<exists> m\<ge>p. s m > s p"
+ {fix p assume p: "p \<ge> Suc N"
+ hence pN: "p > N" by arith with N obtain m where m: "m \<ge> p" "s m > s p" by blast
+ have "m \<noteq> p" using m(2) by auto
+ with m have "\<exists>m>p. s p < s m" by - (rule exI[where x=m], auto)}
+ note th0 = this
+ let ?P = "\<lambda>m x. m > x \<and> s x < s m"
+ from nat_function_unique[of "SOME x. ?P x (Suc N)" "\<lambda>m x. SOME y. ?P y x"]
+ obtain f where f: "f 0 = (SOME x. ?P x (Suc N))"
+ "\<forall>n. f (Suc n) = (SOME m. ?P m (f n))" by blast
+ have "?P (f 0) (Suc N)" unfolding f(1) some_eq_ex[of "\<lambda>p. ?P p (Suc N)"]
+ using N apply -
+ apply (erule allE[where x="Suc N"], clarsimp)
+ apply (rule_tac x="m" in exI)
+ apply auto
+ apply (subgoal_tac "Suc N \<noteq> m")
+ apply simp
+ apply (rule ccontr, simp)
+ done
+ hence f0: "f 0 > Suc N" "s (Suc N) < s (f 0)" by blast+
+ {fix n
+ have "f n > N \<and> ?P (f (Suc n)) (f n)"
+ unfolding f(2)[rule_format, of n] some_eq_ex[of "\<lambda>p. ?P p (f n)"]
+ proof (induct n)
+ case 0 thus ?case
+ using f0 N apply auto
+ apply (erule allE[where x="f 0"], clarsimp)
+ apply (rule_tac x="m" in exI, simp)
+ by (subgoal_tac "f 0 \<noteq> m", auto)
+ next
+ case (Suc n)
+ from Suc.hyps have Nfn: "N < f n" by blast
+ from Suc.hyps obtain m where m: "m > f n" "s (f n) < s m" by blast
+ with Nfn have mN: "m > N" by arith
+ note key = Suc.hyps[unfolded some_eq_ex[of "\<lambda>p. ?P p (f n)", symmetric] f(2)[rule_format, of n, symmetric]]
+
+ from key have th0: "f (Suc n) > N" by simp
+ from N[rule_format, OF th0]
+ obtain m' where m': "m' \<ge> f (Suc n)" "s (f (Suc n)) < s m'" by blast
+ have "m' \<noteq> f (Suc (n))" apply (rule ccontr) using m'(2) by auto
+ hence "m' > f (Suc n)" using m'(1) by simp
+ with key m'(2) show ?case by auto
+ qed}
+ note fSuc = this
+ {fix n
+ 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
+ hence "f n \<ge> Suc N" "f(Suc n) > f n" "s(f n) < s(f(Suc n))" by blast+}
+ note thf = this
+ have sqf: "subseq f" unfolding subseq_Suc_iff using thf by simp
+ have "monoseq (\<lambda>n. s (f n))" unfolding monoseq_Suc using thf
+ apply -
+ apply (rule disjI1)
+ apply auto
+ apply (rule order_less_imp_le)
+ apply blast
+ done
+ then have ?thesis using sqf by blast}
+ ultimately show ?thesis unfolding linorder_not_less[symmetric] by blast
+qed
+
+lemma seq_suble: assumes sf: "subseq f" shows "n \<le> f n"
+proof(induct n)
+ case 0 thus ?case by simp
+next
+ case (Suc n)
+ from sf[unfolded subseq_Suc_iff, rule_format, of n] Suc.hyps
+ have "n < f (Suc n)" by arith
+ thus ?case by arith
+qed
+
+subsection {* Bounded Monotonic Sequences *}
+
+
text{*Bounded Sequence*}
lemma BseqD: "Bseq X ==> \<exists>K. 0 < K & (\<forall>n. norm (X n) \<le> K)"