--- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy Wed Mar 04 10:43:39 2009 +0100
+++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy Wed Mar 04 10:45:52 2009 +0100
@@ -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>"
@@ -946,90 +800,6 @@
ultimately show ?case by blast
qed simp
-subsection {* Order of polynomial roots *}
-
-definition
- order :: "'a::{idom,recpower} \<Rightarrow> 'a poly \<Rightarrow> nat"
-where
- [code del]:
- "order a p = (LEAST n. \<not> [:-a, 1:] ^ Suc n dvd p)"
-
-lemma degree_power_le: "degree (p ^ n) \<le> degree p * n"
-by (induct n, simp, auto intro: order_trans degree_mult_le)
-
-lemma coeff_linear_power:
- fixes a :: "'a::{comm_semiring_1,recpower}"
- shows "coeff ([:a, 1:] ^ n) n = 1"
-apply (induct n, simp_all)
-apply (subst coeff_eq_0)
-apply (auto intro: le_less_trans degree_power_le)
-done
-
-lemma degree_linear_power:
- fixes a :: "'a::{comm_semiring_1,recpower}"
- shows "degree ([:a, 1:] ^ n) = n"
-apply (rule order_antisym)
-apply (rule ord_le_eq_trans [OF degree_power_le], simp)
-apply (rule le_degree, simp add: coeff_linear_power)
-done
-
-lemma order_1: "[:-a, 1:] ^ order a p dvd p"
-apply (cases "p = 0", simp)
-apply (cases "order a p", simp)
-apply (subgoal_tac "nat < (LEAST n. \<not> [:-a, 1:] ^ Suc n dvd p)")
-apply (drule not_less_Least, simp)
-apply (fold order_def, simp)
-done
-
-lemma order_2: "p \<noteq> 0 \<Longrightarrow> \<not> [:-a, 1:] ^ Suc (order a p) dvd p"
-unfolding order_def
-apply (rule LeastI_ex)
-apply (rule_tac x="degree p" in exI)
-apply (rule notI)
-apply (drule (1) dvd_imp_degree_le)
-apply (simp only: degree_linear_power)
-done
-
-lemma order:
- "p \<noteq> 0 \<Longrightarrow> [:-a, 1:] ^ order a p dvd p \<and> \<not> [:-a, 1:] ^ Suc (order a p) dvd p"
-by (rule conjI [OF order_1 order_2])
-
-lemma order_degree:
- assumes p: "p \<noteq> 0"
- shows "order a p \<le> degree p"
-proof -
- have "order a p = degree ([:-a, 1:] ^ order a p)"
- by (simp only: degree_linear_power)
- also have "\<dots> \<le> degree p"
- using order_1 p by (rule dvd_imp_degree_le)
- finally show ?thesis .
-qed
-
-lemma order_root: "poly p a = 0 \<longleftrightarrow> p = 0 \<or> order a p \<noteq> 0"
-apply (cases "p = 0", simp_all)
-apply (rule iffI)
-apply (rule ccontr, simp)
-apply (frule order_2 [where a=a], simp)
-apply (simp add: poly_eq_0_iff_dvd)
-apply (simp add: poly_eq_0_iff_dvd)
-apply (simp only: order_def)
-apply (drule not_less_Least, simp)
-done
-
-lemma poly_zero:
- fixes p :: "'a::{idom,ring_char_0} poly"
- shows "poly p = poly 0 \<longleftrightarrow> p = 0"
-apply (cases "p = 0", simp_all)
-apply (drule poly_roots_finite)
-apply (auto simp add: infinite_UNIV_char_0)
-done
-
-lemma poly_eq_iff:
- fixes p q :: "'a::{idom,ring_char_0} poly"
- shows "poly p = poly q \<longleftrightarrow> p = q"
- using poly_zero [of "p - q"]
- by (simp add: expand_fun_eq)
-
subsection{* Nullstellenstatz, degrees and divisibility of polynomials *}