src/HOL/Library/Fundamental_Theorem_Algebra.thy
 changeset 30240 5b25fee0362c parent 29879 4425849f5db7 child 30242 aea5d7fa7ef5
1.1 --- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Wed Mar 04 10:43:39 2009 +0100
1.2 +++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Wed Mar 04 10:45:52 2009 +0100
1.3 @@ -177,151 +177,6 @@
1.4    thus ?thesis by blast
1.5  qed
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.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.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.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.160  text{* Bolzano-Weierstrass type property for closed disc in complex plane. *}
1.162  lemma metric_bound_lemma: "cmod (x - y) <= \<bar>Re x - Re y\<bar> + \<bar>Im x - Im y\<bar>"
1.163 @@ -946,90 +800,6 @@
1.164    ultimately show ?case by blast
1.165  qed simp
1.167 -subsection {* Order of polynomial roots *}
1.169 -definition
1.170 -  order :: "'a::{idom,recpower} \<Rightarrow> 'a poly \<Rightarrow> nat"
1.171 -where
1.172 -  [code del]:
1.173 -  "order a p = (LEAST n. \<not> [:-a, 1:] ^ Suc n dvd p)"
1.175 -lemma degree_power_le: "degree (p ^ n) \<le> degree p * n"
1.176 -by (induct n, simp, auto intro: order_trans degree_mult_le)
1.178 -lemma coeff_linear_power:
1.179 -  fixes a :: "'a::{comm_semiring_1,recpower}"
1.180 -  shows "coeff ([:a, 1:] ^ n) n = 1"
1.181 -apply (induct n, simp_all)
1.182 -apply (subst coeff_eq_0)
1.183 -apply (auto intro: le_less_trans degree_power_le)
1.184 -done
1.186 -lemma degree_linear_power:
1.187 -  fixes a :: "'a::{comm_semiring_1,recpower}"
1.188 -  shows "degree ([:a, 1:] ^ n) = n"
1.189 -apply (rule order_antisym)
1.190 -apply (rule ord_le_eq_trans [OF degree_power_le], simp)
1.191 -apply (rule le_degree, simp add: coeff_linear_power)
1.192 -done
1.194 -lemma order_1: "[:-a, 1:] ^ order a p dvd p"
1.195 -apply (cases "p = 0", simp)
1.196 -apply (cases "order a p", simp)
1.197 -apply (subgoal_tac "nat < (LEAST n. \<not> [:-a, 1:] ^ Suc n dvd p)")
1.198 -apply (drule not_less_Least, simp)
1.199 -apply (fold order_def, simp)
1.200 -done
1.202 -lemma order_2: "p \<noteq> 0 \<Longrightarrow> \<not> [:-a, 1:] ^ Suc (order a p) dvd p"
1.203 -unfolding order_def
1.204 -apply (rule LeastI_ex)
1.205 -apply (rule_tac x="degree p" in exI)
1.206 -apply (rule notI)
1.207 -apply (drule (1) dvd_imp_degree_le)
1.208 -apply (simp only: degree_linear_power)
1.209 -done
1.211 -lemma order:
1.212 -  "p \<noteq> 0 \<Longrightarrow> [:-a, 1:] ^ order a p dvd p \<and> \<not> [:-a, 1:] ^ Suc (order a p) dvd p"
1.213 -by (rule conjI [OF order_1 order_2])
1.215 -lemma order_degree:
1.216 -  assumes p: "p \<noteq> 0"
1.217 -  shows "order a p \<le> degree p"
1.218 -proof -
1.219 -  have "order a p = degree ([:-a, 1:] ^ order a p)"
1.220 -    by (simp only: degree_linear_power)
1.221 -  also have "\<dots> \<le> degree p"
1.222 -    using order_1 p by (rule dvd_imp_degree_le)
1.223 -  finally show ?thesis .
1.224 -qed
1.226 -lemma order_root: "poly p a = 0 \<longleftrightarrow> p = 0 \<or> order a p \<noteq> 0"
1.227 -apply (cases "p = 0", simp_all)
1.228 -apply (rule iffI)
1.229 -apply (rule ccontr, simp)
1.230 -apply (frule order_2 [where a=a], simp)
1.231 -apply (simp add: poly_eq_0_iff_dvd)
1.232 -apply (simp add: poly_eq_0_iff_dvd)
1.233 -apply (simp only: order_def)
1.234 -apply (drule not_less_Least, simp)
1.235 -done
1.237 -lemma poly_zero:
1.238 -  fixes p :: "'a::{idom,ring_char_0} poly"
1.239 -  shows "poly p = poly 0 \<longleftrightarrow> p = 0"
1.240 -apply (cases "p = 0", simp_all)
1.241 -apply (drule poly_roots_finite)
1.242 -apply (auto simp add: infinite_UNIV_char_0)
1.243 -done
1.245 -lemma poly_eq_iff:
1.246 -  fixes p q :: "'a::{idom,ring_char_0} poly"
1.247 -  shows "poly p = poly q \<longleftrightarrow> p = q"
1.248 -  using poly_zero [of "p - q"]
1.249 -  by (simp add: expand_fun_eq)
1.252  subsection{* Nullstellenstatz, degrees and divisibility of polynomials *}