author nipkow Thu Feb 12 18:14:43 2009 +0100 (2009-02-12) changeset 29879 4425849f5db7 parent 29878 06efd6e731c6 child 29880 3dee8ff45d3d
Moved FTA into Lib and cleaned it up a little.
 src/HOL/Complex_Main.thy file | annotate | diff | revisions src/HOL/Finite_Set.thy file | annotate | diff | revisions src/HOL/Fundamental_Theorem_Algebra.thy file | annotate | diff | revisions src/HOL/IsaMakefile file | annotate | diff | revisions src/HOL/Library/Fundamental_Theorem_Algebra.thy file | annotate | diff | revisions src/HOL/Library/Library.thy file | annotate | diff | revisions src/HOL/Library/Univ_Poly.thy file | annotate | diff | revisions src/HOL/Nat.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Complex_Main.thy	Wed Feb 11 11:22:42 2009 -0800
1.2 +++ b/src/HOL/Complex_Main.thy	Thu Feb 12 18:14:43 2009 +0100
1.3 @@ -4,7 +4,7 @@
1.4  imports
1.5    Main
1.6    Real
1.7 -  Fundamental_Theorem_Algebra
1.8 +  Complex
1.9    Log
1.10    Ln
1.11    Taylor
```
```     2.1 --- a/src/HOL/Finite_Set.thy	Wed Feb 11 11:22:42 2009 -0800
2.2 +++ b/src/HOL/Finite_Set.thy	Thu Feb 12 18:14:43 2009 +0100
2.3 @@ -2029,6 +2029,19 @@
2.4    show False by simp (blast dest: Suc_neq_Zero surjD)
2.5  qed
2.6
2.7 +lemma infinite_UNIV_char_0:
2.8 +  "\<not> finite (UNIV::'a::semiring_char_0 set)"
2.9 +proof
2.10 +  assume "finite (UNIV::'a set)"
2.11 +  with subset_UNIV have "finite (range of_nat::'a set)"
2.12 +    by (rule finite_subset)
2.13 +  moreover have "inj (of_nat::nat \<Rightarrow> 'a)"
2.14 +    by (simp add: inj_on_def)
2.15 +  ultimately have "finite (UNIV::nat set)"
2.16 +    by (rule finite_imageD)
2.17 +  then show "False"
2.18 +    by (simp add: infinite_UNIV_nat)
2.19 +qed
2.20
2.21  subsection{* A fold functional for non-empty sets *}
2.22
```
```     3.1 --- a/src/HOL/Fundamental_Theorem_Algebra.thy	Wed Feb 11 11:22:42 2009 -0800
3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
3.3 @@ -1,1396 +0,0 @@
3.4 -(* Author: Amine Chaieb, TU Muenchen *)
3.5 -
3.7 -
3.8 -theory Fundamental_Theorem_Algebra
3.9 -imports Polynomial Complex
3.10 -begin
3.11 -
3.12 -subsection {* Square root of complex numbers *}
3.13 -definition csqrt :: "complex \<Rightarrow> complex" where
3.14 -"csqrt z = (if Im z = 0 then
3.15 -            if 0 \<le> Re z then Complex (sqrt(Re z)) 0
3.16 -            else Complex 0 (sqrt(- Re z))
3.17 -           else Complex (sqrt((cmod z + Re z) /2))
3.18 -                        ((Im z / abs(Im z)) * sqrt((cmod z - Re z) /2)))"
3.19 -
3.20 -lemma csqrt[algebra]: "csqrt z ^ 2 = z"
3.21 -proof-
3.22 -  obtain x y where xy: "z = Complex x y" by (cases z)
3.23 -  {assume y0: "y = 0"
3.24 -    {assume x0: "x \<ge> 0"
3.25 -      then have ?thesis using y0 xy real_sqrt_pow2[OF x0]
3.26 -	by (simp add: csqrt_def power2_eq_square)}
3.27 -    moreover
3.28 -    {assume "\<not> x \<ge> 0" hence x0: "- x \<ge> 0" by arith
3.29 -      then have ?thesis using y0 xy real_sqrt_pow2[OF x0]
3.30 -	by (simp add: csqrt_def power2_eq_square) }
3.31 -    ultimately have ?thesis by blast}
3.32 -  moreover
3.33 -  {assume y0: "y\<noteq>0"
3.34 -    {fix x y
3.35 -      let ?z = "Complex x y"
3.36 -      from abs_Re_le_cmod[of ?z] have tha: "abs x \<le> cmod ?z" by auto
3.37 -      hence "cmod ?z - x \<ge> 0" "cmod ?z + x \<ge> 0" by arith+
3.38 -      hence "(sqrt (x * x + y * y) + x) / 2 \<ge> 0" "(sqrt (x * x + y * y) - x) / 2 \<ge> 0" by (simp_all add: power2_eq_square) }
3.39 -    note th = this
3.40 -    have sq4: "\<And>x::real. x^2 / 4 = (x / 2) ^ 2"
3.41 -      by (simp add: power2_eq_square)
3.42 -    from th[of x y]
3.43 -    have sq4': "sqrt (((sqrt (x * x + y * y) + x)^2 / 4)) = (sqrt (x * x + y * y) + x) / 2" "sqrt (((sqrt (x * x + y * y) - x)^2 / 4)) = (sqrt (x * x + y * y) - x) / 2" unfolding sq4 by simp_all
3.44 -    then have th1: "sqrt ((sqrt (x * x + y * y) + x) * (sqrt (x * x + y * y) + x) / 4) - sqrt ((sqrt (x * x + y * y) - x) * (sqrt (x * x + y * y) - x) / 4) = x"
3.45 -      unfolding power2_eq_square by simp
3.46 -    have "sqrt 4 = sqrt (2^2)" by simp
3.47 -    hence sqrt4: "sqrt 4 = 2" by (simp only: real_sqrt_abs)
3.48 -    have th2: "2 *(y * sqrt ((sqrt (x * x + y * y) - x) * (sqrt (x * x + y * y) + x) / 4)) / \<bar>y\<bar> = y"
3.49 -      using iffD2[OF real_sqrt_pow2_iff sum_power2_ge_zero[of x y]] y0
3.50 -      unfolding power2_eq_square
3.51 -      by (simp add: algebra_simps real_sqrt_divide sqrt4)
3.52 -     from y0 xy have ?thesis  apply (simp add: csqrt_def power2_eq_square)
3.53 -       apply (simp add: real_sqrt_sum_squares_mult_ge_zero[of x y] real_sqrt_pow2[OF th(1)[of x y], unfolded power2_eq_square] real_sqrt_pow2[OF th(2)[of x y], unfolded power2_eq_square] real_sqrt_mult[symmetric])
3.54 -      using th1 th2  ..}
3.55 -  ultimately show ?thesis by blast
3.56 -qed
3.57 -
3.58 -
3.59 -subsection{* More lemmas about module of complex numbers *}
3.60 -
3.61 -lemma complex_of_real_power: "complex_of_real x ^ n = complex_of_real (x^n)"
3.62 -  by (rule of_real_power [symmetric])
3.63 -
3.64 -lemma real_down2: "(0::real) < d1 \<Longrightarrow> 0 < d2 ==> EX e. 0 < e & e < d1 & e < d2"
3.65 -  apply (rule exI[where x = "min d1 d2 / 2"])
3.66 -  by (simp add: field_simps min_def)
3.67 -
3.68 -text{* The triangle inequality for cmod *}
3.69 -lemma complex_mod_triangle_sub: "cmod w \<le> cmod (w + z) + norm z"
3.70 -  using complex_mod_triangle_ineq2[of "w + z" "-z"] by auto
3.71 -
3.72 -subsection{* Basic lemmas about complex polynomials *}
3.73 -
3.74 -lemma poly_bound_exists:
3.75 -  shows "\<exists>m. m > 0 \<and> (\<forall>z. cmod z <= r \<longrightarrow> cmod (poly p z) \<le> m)"
3.76 -proof(induct p)
3.77 -  case 0 thus ?case by (rule exI[where x=1], simp)
3.78 -next
3.79 -  case (pCons c cs)
3.80 -  from pCons.hyps obtain m where m: "\<forall>z. cmod z \<le> r \<longrightarrow> cmod (poly cs z) \<le> m"
3.81 -    by blast
3.82 -  let ?k = " 1 + cmod c + \<bar>r * m\<bar>"
3.83 -  have kp: "?k > 0" using abs_ge_zero[of "r*m"] norm_ge_zero[of c] by arith
3.84 -  {fix z
3.85 -    assume H: "cmod z \<le> r"
3.86 -    from m H have th: "cmod (poly cs z) \<le> m" by blast
3.87 -    from H have rp: "r \<ge> 0" using norm_ge_zero[of z] by arith
3.88 -    have "cmod (poly (pCons c cs) z) \<le> cmod c + cmod (z* poly cs z)"
3.89 -      using norm_triangle_ineq[of c "z* poly cs z"] by simp
3.90 -    also have "\<dots> \<le> cmod c + r*m" using mult_mono[OF H th rp norm_ge_zero[of "poly cs z"]] by (simp add: norm_mult)
3.91 -    also have "\<dots> \<le> ?k" by simp
3.92 -    finally have "cmod (poly (pCons c cs) z) \<le> ?k" .}
3.93 -  with kp show ?case by blast
3.94 -qed
3.95 -
3.96 -
3.97 -text{* Offsetting the variable in a polynomial gives another of same degree *}
3.98 -
3.99 -definition
3.100 -  "offset_poly p h = poly_rec 0 (\<lambda>a p q. smult h q + pCons a q) p"
3.101 -
3.102 -lemma offset_poly_0: "offset_poly 0 h = 0"
3.103 -  unfolding offset_poly_def by (simp add: poly_rec_0)
3.104 -
3.105 -lemma offset_poly_pCons:
3.106 -  "offset_poly (pCons a p) h =
3.107 -    smult h (offset_poly p h) + pCons a (offset_poly p h)"
3.108 -  unfolding offset_poly_def by (simp add: poly_rec_pCons)
3.109 -
3.110 -lemma offset_poly_single: "offset_poly [:a:] h = [:a:]"
3.111 -by (simp add: offset_poly_pCons offset_poly_0)
3.112 -
3.113 -lemma poly_offset_poly: "poly (offset_poly p h) x = poly p (h + x)"
3.114 -apply (induct p)
3.116 -apply (simp add: offset_poly_pCons algebra_simps)
3.117 -done
3.118 -
3.119 -lemma offset_poly_eq_0_lemma: "smult c p + pCons a p = 0 \<Longrightarrow> p = 0"
3.120 -by (induct p arbitrary: a, simp, force)
3.121 -
3.122 -lemma offset_poly_eq_0_iff: "offset_poly p h = 0 \<longleftrightarrow> p = 0"
3.123 -apply (safe intro!: offset_poly_0)
3.124 -apply (induct p, simp)
3.126 -apply (frule offset_poly_eq_0_lemma, simp)
3.127 -done
3.128 -
3.129 -lemma degree_offset_poly: "degree (offset_poly p h) = degree p"
3.130 -apply (induct p)
3.132 -apply (case_tac "p = 0")
3.133 -apply (simp add: offset_poly_0 offset_poly_pCons)
3.136 -apply (rule le_less_trans [OF degree_smult_le])
3.139 -done
3.140 -
3.141 -definition
3.142 -  "psize p = (if p = 0 then 0 else Suc (degree p))"
3.143 -
3.144 -lemma psize_eq_0_iff [simp]: "psize p = 0 \<longleftrightarrow> p = 0"
3.145 -  unfolding psize_def by simp
3.146 -
3.147 -lemma poly_offset: "\<exists> q. psize q = psize p \<and> (\<forall>x. poly q (x::complex) = poly p (a + x))"
3.148 -proof (intro exI conjI)
3.149 -  show "psize (offset_poly p a) = psize p"
3.150 -    unfolding psize_def
3.151 -    by (simp add: offset_poly_eq_0_iff degree_offset_poly)
3.152 -  show "\<forall>x. poly (offset_poly p a) x = poly p (a + x)"
3.153 -    by (simp add: poly_offset_poly)
3.154 -qed
3.155 -
3.156 -text{* An alternative useful formulation of completeness of the reals *}
3.157 -lemma real_sup_exists: assumes ex: "\<exists>x. P x" and bz: "\<exists>z. \<forall>x. P x \<longrightarrow> x < z"
3.158 -  shows "\<exists>(s::real). \<forall>y. (\<exists>x. P x \<and> y < x) \<longleftrightarrow> y < s"
3.159 -proof-
3.160 -  from ex bz obtain x Y where x: "P x" and Y: "\<And>x. P x \<Longrightarrow> x < Y"  by blast
3.161 -  from ex have thx:"\<exists>x. x \<in> Collect P" by blast
3.162 -  from bz have thY: "\<exists>Y. isUb UNIV (Collect P) Y"
3.163 -    by(auto simp add: isUb_def isLub_def setge_def setle_def leastP_def Ball_def order_le_less)
3.164 -  from reals_complete[OF thx thY] obtain L where L: "isLub UNIV (Collect P) L"
3.165 -    by blast
3.166 -  from Y[OF x] have xY: "x < Y" .
3.167 -  from L have L': "\<forall>x. P x \<longrightarrow> x \<le> L" by (auto simp add: isUb_def isLub_def setge_def setle_def leastP_def Ball_def)
3.168 -  from Y have Y': "\<forall>x. P x \<longrightarrow> x \<le> Y"
3.169 -    apply (clarsimp, atomize (full)) by auto
3.170 -  from L Y' have "L \<le> Y" by (auto simp add: isUb_def isLub_def setge_def setle_def leastP_def Ball_def)
3.171 -  {fix y
3.172 -    {fix z assume z: "P z" "y < z"
3.173 -      from L' z have "y < L" by auto }
3.174 -    moreover
3.175 -    {assume yL: "y < L" "\<forall>z. P z \<longrightarrow> \<not> y < z"
3.176 -      hence nox: "\<forall>z. P z \<longrightarrow> y \<ge> z" by auto
3.177 -      from nox L have "y \<ge> L" by (auto simp add: isUb_def isLub_def setge_def setle_def leastP_def Ball_def)
3.178 -      with yL(1) have False  by arith}
3.179 -    ultimately have "(\<exists>x. P x \<and> y < x) \<longleftrightarrow> y < L" by blast}
3.180 -  thus ?thesis by blast
3.181 -qed
3.182 -
3.183 -
3.184 -subsection{* Some theorems about Sequences*}
3.185 -text{* Given a binary function @{text "f:: nat \<Rightarrow> 'a \<Rightarrow> 'a"}, its values are uniquely determined by a function g *}
3.186 -
3.187 -lemma num_Axiom: "EX! g. g 0 = e \<and> (\<forall>n. g (Suc n) = f n (g n))"
3.188 -  unfolding Ex1_def
3.189 -  apply (rule_tac x="nat_rec e f" in exI)
3.190 -  apply (rule conjI)+
3.191 -apply (rule def_nat_rec_0, simp)
3.192 -apply (rule allI, rule def_nat_rec_Suc, simp)
3.193 -apply (rule allI, rule impI, rule ext)
3.194 -apply (erule conjE)
3.195 -apply (induct_tac x)
3.197 -apply (erule_tac x="n" in allE)
3.198 -apply (simp)
3.199 -done
3.200 -
3.201 - text{* An equivalent formulation of monotony -- Not used here, but might be useful *}
3.202 -lemma mono_Suc: "mono f = (\<forall>n. (f n :: 'a :: order) \<le> f (Suc n))"
3.203 -unfolding mono_def
3.204 -proof auto
3.205 -  fix A B :: nat
3.206 -  assume H: "\<forall>n. f n \<le> f (Suc n)" "A \<le> B"
3.207 -  hence "\<exists>k. B = A + k" apply -  apply (thin_tac "\<forall>n. f n \<le> f (Suc n)")
3.208 -    by presburger
3.209 -  then obtain k where k: "B = A + k" by blast
3.210 -  {fix a k
3.211 -    have "f a \<le> f (a + k)"
3.212 -    proof (induct k)
3.213 -      case 0 thus ?case by simp
3.214 -    next
3.215 -      case (Suc k)
3.216 -      from Suc.hyps H(1)[rule_format, of "a + k"] show ?case by simp
3.217 -    qed}
3.218 -  with k show "f A \<le> f B" by blast
3.219 -qed
3.220 -
3.221 -text{* for any sequence, there is a mootonic subsequence *}
3.222 -lemma seq_monosub: "\<exists>f. subseq f \<and> monoseq (\<lambda> n. (s (f n)))"
3.223 -proof-
3.224 -  {assume H: "\<forall>n. \<exists>p >n. \<forall> m\<ge>p. s m \<le> s p"
3.225 -    let ?P = "\<lambda> p n. p > n \<and> (\<forall>m \<ge> p. s m \<le> s p)"
3.226 -    from num_Axiom[of "SOME p. ?P p 0" "\<lambda>p n. SOME p. ?P p n"]
3.227 -    obtain f where f: "f 0 = (SOME p. ?P p 0)" "\<forall>n. f (Suc n) = (SOME p. ?P p (f n))" by blast
3.228 -    have "?P (f 0) 0"  unfolding f(1) some_eq_ex[of "\<lambda>p. ?P p 0"]
3.229 -      using H apply -
3.230 -      apply (erule allE[where x=0], erule exE, rule_tac x="p" in exI)
3.231 -      unfolding order_le_less by blast
3.232 -    hence f0: "f 0 > 0" "\<forall>m \<ge> f 0. s m \<le> s (f 0)" by blast+
3.233 -    {fix n
3.234 -      have "?P (f (Suc n)) (f n)"
3.235 -	unfolding f(2)[rule_format, of n] some_eq_ex[of "\<lambda>p. ?P p (f n)"]
3.236 -	using H apply -
3.237 -      apply (erule allE[where x="f n"], erule exE, rule_tac x="p" in exI)
3.238 -      unfolding order_le_less by blast
3.239 -    hence "f (Suc n) > f n" "\<forall>m \<ge> f (Suc n). s m \<le> s (f (Suc n))" by blast+}
3.240 -  note fSuc = this
3.241 -    {fix p q assume pq: "p \<ge> f q"
3.242 -      have "s p \<le> s(f(q))"  using f0(2)[rule_format, of p] pq fSuc
3.243 -	by (cases q, simp_all) }
3.244 -    note pqth = this
3.245 -    {fix q
3.246 -      have "f (Suc q) > f q" apply (induct q)
3.247 -	using f0(1) fSuc(1)[of 0] apply simp by (rule fSuc(1))}
3.248 -    note fss = this
3.249 -    from fss have th1: "subseq f" unfolding subseq_Suc_iff ..
3.250 -    {fix a b
3.251 -      have "f a \<le> f (a + b)"
3.252 -      proof(induct b)
3.253 -	case 0 thus ?case by simp
3.254 -      next
3.255 -	case (Suc b)
3.256 -	from fSuc(1)[of "a + b"] Suc.hyps show ?case by simp
3.257 -      qed}
3.258 -    note fmon0 = this
3.259 -    have "monoseq (\<lambda>n. s (f n))"
3.260 -    proof-
3.261 -      {fix n
3.262 -	have "s (f n) \<ge> s (f (Suc n))"
3.263 -	proof(cases n)
3.264 -	  case 0
3.265 -	  assume n0: "n = 0"
3.266 -	  from fSuc(1)[of 0] have th0: "f 0 \<le> f (Suc 0)" by simp
3.267 -	  from f0(2)[rule_format, OF th0] show ?thesis  using n0 by simp
3.268 -	next
3.269 -	  case (Suc m)
3.270 -	  assume m: "n = Suc m"
3.271 -	  from fSuc(1)[of n] m have th0: "f (Suc m) \<le> f (Suc (Suc m))" by simp
3.272 -	  from m fSuc(2)[rule_format, OF th0] show ?thesis by simp
3.273 -	qed}
3.274 -      thus "monoseq (\<lambda>n. s (f n))" unfolding monoseq_Suc by blast
3.275 -    qed
3.276 -    with th1 have ?thesis by blast}
3.277 -  moreover
3.278 -  {fix N assume N: "\<forall>p >N. \<exists> m\<ge>p. s m > s p"
3.279 -    {fix p assume p: "p \<ge> Suc N"
3.280 -      hence pN: "p > N" by arith with N obtain m where m: "m \<ge> p" "s m > s p" by blast
3.281 -      have "m \<noteq> p" using m(2) by auto
3.282 -      with m have "\<exists>m>p. s p < s m" by - (rule exI[where x=m], auto)}
3.283 -    note th0 = this
3.284 -    let ?P = "\<lambda>m x. m > x \<and> s x < s m"
3.285 -    from num_Axiom[of "SOME x. ?P x (Suc N)" "\<lambda>m x. SOME y. ?P y x"]
3.286 -    obtain f where f: "f 0 = (SOME x. ?P x (Suc N))"
3.287 -      "\<forall>n. f (Suc n) = (SOME m. ?P m (f n))" by blast
3.288 -    have "?P (f 0) (Suc N)"  unfolding f(1) some_eq_ex[of "\<lambda>p. ?P p (Suc N)"]
3.289 -      using N apply -
3.290 -      apply (erule allE[where x="Suc N"], clarsimp)
3.291 -      apply (rule_tac x="m" in exI)
3.292 -      apply auto
3.293 -      apply (subgoal_tac "Suc N \<noteq> m")
3.294 -      apply simp
3.295 -      apply (rule ccontr, simp)
3.296 -      done
3.297 -    hence f0: "f 0 > Suc N" "s (Suc N) < s (f 0)" by blast+
3.298 -    {fix n
3.299 -      have "f n > N \<and> ?P (f (Suc n)) (f n)"
3.300 -	unfolding f(2)[rule_format, of n] some_eq_ex[of "\<lambda>p. ?P p (f n)"]
3.301 -      proof (induct n)
3.302 -	case 0 thus ?case
3.303 -	  using f0 N apply auto
3.304 -	  apply (erule allE[where x="f 0"], clarsimp)
3.305 -	  apply (rule_tac x="m" in exI, simp)
3.306 -	  by (subgoal_tac "f 0 \<noteq> m", auto)
3.307 -      next
3.308 -	case (Suc n)
3.309 -	from Suc.hyps have Nfn: "N < f n" by blast
3.310 -	from Suc.hyps obtain m where m: "m > f n" "s (f n) < s m" by blast
3.311 -	with Nfn have mN: "m > N" by arith
3.312 -	note key = Suc.hyps[unfolded some_eq_ex[of "\<lambda>p. ?P p (f n)", symmetric] f(2)[rule_format, of n, symmetric]]
3.313 -
3.314 -	from key have th0: "f (Suc n) > N" by simp
3.315 -	from N[rule_format, OF th0]
3.316 -	obtain m' where m': "m' \<ge> f (Suc n)" "s (f (Suc n)) < s m'" by blast
3.317 -	have "m' \<noteq> f (Suc (n))" apply (rule ccontr) using m'(2) by auto
3.318 -	hence "m' > f (Suc n)" using m'(1) by simp
3.319 -	with key m'(2) show ?case by auto
3.320 -      qed}
3.321 -    note fSuc = this
3.322 -    {fix n
3.323 -      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
3.324 -      hence "f n \<ge> Suc N" "f(Suc n) > f n" "s(f n) < s(f(Suc n))" by blast+}
3.325 -    note thf = this
3.326 -    have sqf: "subseq f" unfolding subseq_Suc_iff using thf by simp
3.327 -    have "monoseq (\<lambda>n. s (f n))"  unfolding monoseq_Suc using thf
3.328 -      apply -
3.329 -      apply (rule disjI1)
3.330 -      apply auto
3.331 -      apply (rule order_less_imp_le)
3.332 -      apply blast
3.333 -      done
3.334 -    then have ?thesis  using sqf by blast}
3.335 -  ultimately show ?thesis unfolding linorder_not_less[symmetric] by blast
3.336 -qed
3.337 -
3.338 -lemma seq_suble: assumes sf: "subseq f" shows "n \<le> f n"
3.339 -proof(induct n)
3.340 -  case 0 thus ?case by simp
3.341 -next
3.342 -  case (Suc n)
3.343 -  from sf[unfolded subseq_Suc_iff, rule_format, of n] Suc.hyps
3.344 -  have "n < f (Suc n)" by arith
3.345 -  thus ?case by arith
3.346 -qed
3.347 -
3.348 -subsection {* Fundamental theorem of algebra *}
3.349 -lemma  unimodular_reduce_norm:
3.350 -  assumes md: "cmod z = 1"
3.351 -  shows "cmod (z + 1) < 1 \<or> cmod (z - 1) < 1 \<or> cmod (z + ii) < 1 \<or> cmod (z - ii) < 1"
3.352 -proof-
3.353 -  obtain x y where z: "z = Complex x y " by (cases z, auto)
3.354 -  from md z have xy: "x^2 + y^2 = 1" by (simp add: cmod_def)
3.355 -  {assume C: "cmod (z + 1) \<ge> 1" "cmod (z - 1) \<ge> 1" "cmod (z + ii) \<ge> 1" "cmod (z - ii) \<ge> 1"
3.356 -    from C z xy have "2*x \<le> 1" "2*x \<ge> -1" "2*y \<le> 1" "2*y \<ge> -1"
3.357 -      by (simp_all add: cmod_def power2_eq_square algebra_simps)
3.358 -    hence "abs (2*x) \<le> 1" "abs (2*y) \<le> 1" by simp_all
3.359 -    hence "(abs (2 * x))^2 <= 1^2" "(abs (2 * y)) ^2 <= 1^2"
3.360 -      by - (rule power_mono, simp, simp)+
3.361 -    hence th0: "4*x^2 \<le> 1" "4*y^2 \<le> 1"
3.362 -      by (simp_all  add: power2_abs power_mult_distrib)
3.363 -    from add_mono[OF th0] xy have False by simp }
3.364 -  thus ?thesis unfolding linorder_not_le[symmetric] by blast
3.365 -qed
3.366 -
3.367 -text{* Hence we can always reduce modulus of @{text "1 + b z^n"} if nonzero *}
3.368 -lemma reduce_poly_simple:
3.369 - assumes b: "b \<noteq> 0" and n: "n\<noteq>0"
3.370 -  shows "\<exists>z. cmod (1 + b * z^n) < 1"
3.371 -using n
3.372 -proof(induct n rule: nat_less_induct)
3.373 -  fix n
3.374 -  assume IH: "\<forall>m<n. m \<noteq> 0 \<longrightarrow> (\<exists>z. cmod (1 + b * z ^ m) < 1)" and n: "n \<noteq> 0"
3.375 -  let ?P = "\<lambda>z n. cmod (1 + b * z ^ n) < 1"
3.376 -  {assume e: "even n"
3.377 -    hence "\<exists>m. n = 2*m" by presburger
3.378 -    then obtain m where m: "n = 2*m" by blast
3.379 -    from n m have "m\<noteq>0" "m < n" by presburger+
3.380 -    with IH[rule_format, of m] obtain z where z: "?P z m" by blast
3.381 -    from z have "?P (csqrt z) n" by (simp add: m power_mult csqrt)
3.382 -    hence "\<exists>z. ?P z n" ..}
3.383 -  moreover
3.384 -  {assume o: "odd n"
3.385 -    from b have b': "b^2 \<noteq> 0" unfolding power2_eq_square by simp
3.386 -    have "Im (inverse b) * (Im (inverse b) * \<bar>Im b * Im b + Re b * Re b\<bar>) +
3.387 -    Re (inverse b) * (Re (inverse b) * \<bar>Im b * Im b + Re b * Re b\<bar>) =
3.388 -    ((Re (inverse b))^2 + (Im (inverse b))^2) * \<bar>Im b * Im b + Re b * Re b\<bar>" by algebra
3.389 -    also have "\<dots> = cmod (inverse b) ^2 * cmod b ^ 2"
3.390 -      apply (simp add: cmod_def) using realpow_two_le_add_order[of "Re b" "Im b"]
3.391 -      by (simp add: power2_eq_square)
3.392 -    finally
3.393 -    have th0: "Im (inverse b) * (Im (inverse b) * \<bar>Im b * Im b + Re b * Re b\<bar>) +
3.394 -    Re (inverse b) * (Re (inverse b) * \<bar>Im b * Im b + Re b * Re b\<bar>) =
3.395 -    1"
3.396 -      apply (simp add: power2_eq_square norm_mult[symmetric] norm_inverse[symmetric])
3.397 -      using right_inverse[OF b']
3.398 -      by (simp add: power2_eq_square[symmetric] power_inverse[symmetric] algebra_simps)
3.399 -    have th0: "cmod (complex_of_real (cmod b) / b) = 1"
3.400 -      apply (simp add: complex_Re_mult cmod_def power2_eq_square Re_complex_of_real Im_complex_of_real divide_inverse algebra_simps )
3.401 -      by (simp add: real_sqrt_mult[symmetric] th0)
3.402 -    from o have "\<exists>m. n = Suc (2*m)" by presburger+
3.403 -    then obtain m where m: "n = Suc (2*m)" by blast
3.404 -    from unimodular_reduce_norm[OF th0] o
3.405 -    have "\<exists>v. cmod (complex_of_real (cmod b) / b + v^n) < 1"
3.406 -      apply (cases "cmod (complex_of_real (cmod b) / b + 1) < 1", rule_tac x="1" in exI, simp)
3.407 -      apply (cases "cmod (complex_of_real (cmod b) / b - 1) < 1", rule_tac x="-1" in exI, simp add: diff_def)
3.408 -      apply (cases "cmod (complex_of_real (cmod b) / b + ii) < 1")
3.409 -      apply (cases "even m", rule_tac x="ii" in exI, simp add: m power_mult)
3.410 -      apply (rule_tac x="- ii" in exI, simp add: m power_mult)
3.411 -      apply (cases "even m", rule_tac x="- ii" in exI, simp add: m power_mult diff_def)
3.412 -      apply (rule_tac x="ii" in exI, simp add: m power_mult diff_def)
3.413 -      done
3.414 -    then obtain v where v: "cmod (complex_of_real (cmod b) / b + v^n) < 1" by blast
3.415 -    let ?w = "v / complex_of_real (root n (cmod b))"
3.416 -    from odd_real_root_pow[OF o, of "cmod b"]
3.417 -    have th1: "?w ^ n = v^n / complex_of_real (cmod b)"
3.418 -      by (simp add: power_divide complex_of_real_power)
3.419 -    have th2:"cmod (complex_of_real (cmod b) / b) = 1" using b by (simp add: norm_divide)
3.420 -    hence th3: "cmod (complex_of_real (cmod b) / b) \<ge> 0" by simp
3.421 -    have th4: "cmod (complex_of_real (cmod b) / b) *
3.422 -   cmod (1 + b * (v ^ n / complex_of_real (cmod b)))
3.423 -   < cmod (complex_of_real (cmod b) / b) * 1"
3.424 -      apply (simp only: norm_mult[symmetric] right_distrib)
3.425 -      using b v by (simp add: th2)
3.426 -
3.427 -    from mult_less_imp_less_left[OF th4 th3]
3.428 -    have "?P ?w n" unfolding th1 .
3.429 -    hence "\<exists>z. ?P z n" .. }
3.430 -  ultimately show "\<exists>z. ?P z n" by blast
3.431 -qed
3.432 -
3.433 -
3.434 -text{* Bolzano-Weierstrass type property for closed disc in complex plane. *}
3.435 -
3.436 -lemma metric_bound_lemma: "cmod (x - y) <= \<bar>Re x - Re y\<bar> + \<bar>Im x - Im y\<bar>"
3.437 -  using real_sqrt_sum_squares_triangle_ineq[of "Re x - Re y" 0 0 "Im x - Im y" ]
3.438 -  unfolding cmod_def by simp
3.439 -
3.440 -lemma bolzano_weierstrass_complex_disc:
3.441 -  assumes r: "\<forall>n. cmod (s n) \<le> r"
3.442 -  shows "\<exists>f z. subseq f \<and> (\<forall>e >0. \<exists>N. \<forall>n \<ge> N. cmod (s (f n) - z) < e)"
3.443 -proof-
3.444 -  from seq_monosub[of "Re o s"]
3.445 -  obtain f g where f: "subseq f" "monoseq (\<lambda>n. Re (s (f n)))"
3.446 -    unfolding o_def by blast
3.447 -  from seq_monosub[of "Im o s o f"]
3.448 -  obtain g where g: "subseq g" "monoseq (\<lambda>n. Im (s(f(g n))))" unfolding o_def by blast
3.449 -  let ?h = "f o g"
3.450 -  from r[rule_format, of 0] have rp: "r \<ge> 0" using norm_ge_zero[of "s 0"] by arith
3.451 -  have th:"\<forall>n. r + 1 \<ge> \<bar> Re (s n)\<bar>"
3.452 -  proof
3.453 -    fix n
3.454 -    from abs_Re_le_cmod[of "s n"] r[rule_format, of n]  show "\<bar>Re (s n)\<bar> \<le> r + 1" by arith
3.455 -  qed
3.456 -  have conv1: "convergent (\<lambda>n. Re (s ( f n)))"
3.457 -    apply (rule Bseq_monoseq_convergent)
3.458 -    apply (simp add: Bseq_def)
3.459 -    apply (rule exI[where x= "r + 1"])
3.460 -    using th rp apply simp
3.461 -    using f(2) .
3.462 -  have th:"\<forall>n. r + 1 \<ge> \<bar> Im (s n)\<bar>"
3.463 -  proof
3.464 -    fix n
3.465 -    from abs_Im_le_cmod[of "s n"] r[rule_format, of n]  show "\<bar>Im (s n)\<bar> \<le> r + 1" by arith
3.466 -  qed
3.467 -
3.468 -  have conv2: "convergent (\<lambda>n. Im (s (f (g n))))"
3.469 -    apply (rule Bseq_monoseq_convergent)
3.470 -    apply (simp add: Bseq_def)
3.471 -    apply (rule exI[where x= "r + 1"])
3.472 -    using th rp apply simp
3.473 -    using g(2) .
3.474 -
3.475 -  from conv1[unfolded convergent_def] obtain x where "LIMSEQ (\<lambda>n. Re (s (f n))) x"
3.476 -    by blast
3.477 -  hence  x: "\<forall>r>0. \<exists>n0. \<forall>n\<ge>n0. \<bar> Re (s (f n)) - x \<bar> < r"
3.478 -    unfolding LIMSEQ_def real_norm_def .
3.479 -
3.480 -  from conv2[unfolded convergent_def] obtain y where "LIMSEQ (\<lambda>n. Im (s (f (g n)))) y"
3.481 -    by blast
3.482 -  hence  y: "\<forall>r>0. \<exists>n0. \<forall>n\<ge>n0. \<bar> Im (s (f (g n))) - y \<bar> < r"
3.483 -    unfolding LIMSEQ_def real_norm_def .
3.484 -  let ?w = "Complex x y"
3.485 -  from f(1) g(1) have hs: "subseq ?h" unfolding subseq_def by auto
3.486 -  {fix e assume ep: "e > (0::real)"
3.487 -    hence e2: "e/2 > 0" by simp
3.488 -    from x[rule_format, OF e2] y[rule_format, OF e2]
3.489 -    obtain N1 N2 where N1: "\<forall>n\<ge>N1. \<bar>Re (s (f n)) - x\<bar> < e / 2" and N2: "\<forall>n\<ge>N2. \<bar>Im (s (f (g n))) - y\<bar> < e / 2" by blast
3.490 -    {fix n assume nN12: "n \<ge> N1 + N2"
3.491 -      hence nN1: "g n \<ge> N1" and nN2: "n \<ge> N2" using seq_suble[OF g(1), of n] by arith+
3.492 -      from add_strict_mono[OF N1[rule_format, OF nN1] N2[rule_format, OF nN2]]
3.493 -      have "cmod (s (?h n) - ?w) < e"
3.494 -	using metric_bound_lemma[of "s (f (g n))" ?w] by simp }
3.495 -    hence "\<exists>N. \<forall>n\<ge>N. cmod (s (?h n) - ?w) < e" by blast }
3.496 -  with hs show ?thesis  by blast
3.497 -qed
3.498 -
3.499 -text{* Polynomial is continuous. *}
3.500 -
3.501 -lemma poly_cont:
3.502 -  assumes ep: "e > 0"
3.503 -  shows "\<exists>d >0. \<forall>w. 0 < cmod (w - z) \<and> cmod (w - z) < d \<longrightarrow> cmod (poly p w - poly p z) < e"
3.504 -proof-
3.505 -  obtain q where q: "degree q = degree p" "\<And>x. poly q x = poly p (z + x)"
3.506 -  proof
3.507 -    show "degree (offset_poly p z) = degree p"
3.508 -      by (rule degree_offset_poly)
3.509 -    show "\<And>x. poly (offset_poly p z) x = poly p (z + x)"
3.510 -      by (rule poly_offset_poly)
3.511 -  qed
3.512 -  {fix w
3.513 -    note q(2)[of "w - z", simplified]}
3.514 -  note th = this
3.515 -  show ?thesis unfolding th[symmetric]
3.516 -  proof(induct q)
3.517 -    case 0 thus ?case  using ep by auto
3.518 -  next
3.519 -    case (pCons c cs)
3.520 -    from poly_bound_exists[of 1 "cs"]
3.521 -    obtain m where m: "m > 0" "\<And>z. cmod z \<le> 1 \<Longrightarrow> cmod (poly cs z) \<le> m" by blast
3.522 -    from ep m(1) have em0: "e/m > 0" by (simp add: field_simps)
3.523 -    have one0: "1 > (0::real)"  by arith
3.524 -    from real_lbound_gt_zero[OF one0 em0]
3.525 -    obtain d where d: "d >0" "d < 1" "d < e / m" by blast
3.526 -    from d(1,3) m(1) have dm: "d*m > 0" "d*m < e"
3.527 -      by (simp_all add: field_simps real_mult_order)
3.528 -    show ?case
3.529 -      proof(rule ex_forward[OF real_lbound_gt_zero[OF one0 em0]], clarsimp simp add: norm_mult)
3.530 -	fix d w
3.531 -	assume H: "d > 0" "d < 1" "d < e/m" "w\<noteq>z" "cmod (w-z) < d"
3.532 -	hence d1: "cmod (w-z) \<le> 1" "d \<ge> 0" by simp_all
3.533 -	from H(3) m(1) have dme: "d*m < e" by (simp add: field_simps)
3.534 -	from H have th: "cmod (w-z) \<le> d" by simp
3.535 -	from mult_mono[OF th m(2)[OF d1(1)] d1(2) norm_ge_zero] dme
3.536 -	show "cmod (w - z) * cmod (poly cs (w - z)) < e" by simp
3.537 -      qed
3.538 -    qed
3.539 -qed
3.540 -
3.541 -text{* Hence a polynomial attains minimum on a closed disc
3.542 -  in the complex plane. *}
3.543 -lemma  poly_minimum_modulus_disc:
3.544 -  "\<exists>z. \<forall>w. cmod w \<le> r \<longrightarrow> cmod (poly p z) \<le> cmod (poly p w)"
3.545 -proof-
3.546 -  {assume "\<not> r \<ge> 0" hence ?thesis unfolding linorder_not_le
3.547 -      apply -
3.548 -      apply (rule exI[where x=0])
3.549 -      apply auto
3.550 -      apply (subgoal_tac "cmod w < 0")
3.551 -      apply simp
3.552 -      apply arith
3.553 -      done }
3.554 -  moreover
3.555 -  {assume rp: "r \<ge> 0"
3.556 -    from rp have "cmod 0 \<le> r \<and> cmod (poly p 0) = - (- cmod (poly p 0))" by simp
3.557 -    hence mth1: "\<exists>x z. cmod z \<le> r \<and> cmod (poly p z) = - x"  by blast
3.558 -    {fix x z
3.559 -      assume H: "cmod z \<le> r" "cmod (poly p z) = - x" "\<not>x < 1"
3.560 -      hence "- x < 0 " by arith
3.561 -      with H(2) norm_ge_zero[of "poly p z"]  have False by simp }
3.562 -    then have mth2: "\<exists>z. \<forall>x. (\<exists>z. cmod z \<le> r \<and> cmod (poly p z) = - x) \<longrightarrow> x < z" by blast
3.563 -    from real_sup_exists[OF mth1 mth2] obtain s where
3.564 -      s: "\<forall>y. (\<exists>x. (\<exists>z. cmod z \<le> r \<and> cmod (poly p z) = - x) \<and> y < x) \<longleftrightarrow>(y < s)" by blast
3.565 -    let ?m = "-s"
3.566 -    {fix y
3.567 -      from s[rule_format, of "-y"] have
3.568 -    "(\<exists>z x. cmod z \<le> r \<and> -(- cmod (poly p z)) < y) \<longleftrightarrow> ?m < y"
3.569 -	unfolding minus_less_iff[of y ] equation_minus_iff by blast }
3.570 -    note s1 = this[unfolded minus_minus]
3.571 -    from s1[of ?m] have s1m: "\<And>z x. cmod z \<le> r \<Longrightarrow> cmod (poly p z) \<ge> ?m"
3.572 -      by auto
3.573 -    {fix n::nat
3.574 -      from s1[rule_format, of "?m + 1/real (Suc n)"]
3.575 -      have "\<exists>z. cmod z \<le> r \<and> cmod (poly p z) < - s + 1 / real (Suc n)"
3.576 -	by simp}
3.577 -    hence th: "\<forall>n. \<exists>z. cmod z \<le> r \<and> cmod (poly p z) < - s + 1 / real (Suc n)" ..
3.578 -    from choice[OF th] obtain g where
3.579 -      g: "\<forall>n. cmod (g n) \<le> r" "\<forall>n. cmod (poly p (g n)) <?m+1 /real(Suc n)"
3.580 -      by blast
3.581 -    from bolzano_weierstrass_complex_disc[OF g(1)]
3.582 -    obtain f z where fz: "subseq f" "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. cmod (g (f n) - z) < e"
3.583 -      by blast
3.584 -    {fix w
3.585 -      assume wr: "cmod w \<le> r"
3.586 -      let ?e = "\<bar>cmod (poly p z) - ?m\<bar>"
3.587 -      {assume e: "?e > 0"
3.588 -	hence e2: "?e/2 > 0" by simp
3.589 -	from poly_cont[OF e2, of z p] obtain d where
3.590 -	  d: "d>0" "\<forall>w. 0<cmod (w - z)\<and> cmod(w - z) < d \<longrightarrow> cmod(poly p w - poly p z) < ?e/2" by blast
3.591 -	{fix w assume w: "cmod (w - z) < d"
3.592 -	  have "cmod(poly p w - poly p z) < ?e / 2"
3.593 -	    using d(2)[rule_format, of w] w e by (cases "w=z", simp_all)}
3.594 -	note th1 = this
3.595 -
3.596 -	from fz(2)[rule_format, OF d(1)] obtain N1 where
3.597 -	  N1: "\<forall>n\<ge>N1. cmod (g (f n) - z) < d" by blast
3.598 -	from reals_Archimedean2[of "2/?e"] obtain N2::nat where
3.599 -	  N2: "2/?e < real N2" by blast
3.600 -	have th2: "cmod(poly p (g(f(N1 + N2))) - poly p z) < ?e/2"
3.601 -	  using N1[rule_format, of "N1 + N2"] th1 by simp
3.602 -	{fix a b e2 m :: real
3.603 -	have "a < e2 \<Longrightarrow> abs(b - m) < e2 \<Longrightarrow> 2 * e2 <= abs(b - m) + a
3.604 -          ==> False" by arith}
3.605 -      note th0 = this
3.606 -      have ath:
3.607 -	"\<And>m x e. m <= x \<Longrightarrow>  x < m + e ==> abs(x - m::real) < e" by arith
3.608 -      from s1m[OF g(1)[rule_format]]
3.609 -      have th31: "?m \<le> cmod(poly p (g (f (N1 + N2))))" .
3.610 -      from seq_suble[OF fz(1), of "N1+N2"]
3.611 -      have th00: "real (Suc (N1+N2)) \<le> real (Suc (f (N1+N2)))" by simp
3.612 -      have th000: "0 \<le> (1::real)" "(1::real) \<le> 1" "real (Suc (N1+N2)) > 0"
3.613 -	using N2 by auto
3.614 -      from frac_le[OF th000 th00] have th00: "?m +1 / real (Suc (f (N1 + N2))) \<le> ?m + 1 / real (Suc (N1 + N2))" by simp
3.615 -      from g(2)[rule_format, of "f (N1 + N2)"]
3.616 -      have th01:"cmod (poly p (g (f (N1 + N2)))) < - s + 1 / real (Suc (f (N1 + N2)))" .
3.617 -      from order_less_le_trans[OF th01 th00]
3.618 -      have th32: "cmod(poly p (g (f (N1 + N2)))) < ?m + (1/ real(Suc (N1 + N2)))" .
3.619 -      from N2 have "2/?e < real (Suc (N1 + N2))" by arith
3.620 -      with e2 less_imp_inverse_less[of "2/?e" "real (Suc (N1 + N2))"]
3.621 -      have "?e/2 > 1/ real (Suc (N1 + N2))" by (simp add: inverse_eq_divide)
3.622 -      with ath[OF th31 th32]
3.623 -      have thc1:"\<bar>cmod(poly p (g (f (N1 + N2)))) - ?m\<bar>< ?e/2" by arith
3.624 -      have ath2: "\<And>(a::real) b c m. \<bar>a - b\<bar> <= c ==> \<bar>b - m\<bar> <= \<bar>a - m\<bar> + c"
3.625 -	by arith
3.626 -      have th22: "\<bar>cmod (poly p (g (f (N1 + N2)))) - cmod (poly p z)\<bar>
3.627 -\<le> cmod (poly p (g (f (N1 + N2))) - poly p z)"
3.628 -	by (simp add: norm_triangle_ineq3)
3.629 -      from ath2[OF th22, of ?m]
3.630 -      have thc2: "2*(?e/2) \<le> \<bar>cmod(poly p (g (f (N1 + N2)))) - ?m\<bar> + cmod (poly p (g (f (N1 + N2))) - poly p z)" by simp
3.631 -      from th0[OF th2 thc1 thc2] have False .}
3.632 -      hence "?e = 0" by auto
3.633 -      then have "cmod (poly p z) = ?m" by simp
3.634 -      with s1m[OF wr]
3.635 -      have "cmod (poly p z) \<le> cmod (poly p w)" by simp }
3.636 -    hence ?thesis by blast}
3.637 -  ultimately show ?thesis by blast
3.638 -qed
3.639 -
3.640 -lemma "(rcis (sqrt (abs r)) (a/2)) ^ 2 = rcis (abs r) a"
3.641 -  unfolding power2_eq_square
3.642 -  apply (simp add: rcis_mult)
3.643 -  apply (simp add: power2_eq_square[symmetric])
3.644 -  done
3.645 -
3.646 -lemma cispi: "cis pi = -1"
3.647 -  unfolding cis_def
3.648 -  by simp
3.649 -
3.650 -lemma "(rcis (sqrt (abs r)) ((pi + a)/2)) ^ 2 = rcis (- abs r) a"
3.651 -  unfolding power2_eq_square
3.653 -  apply (simp add: power2_eq_square[symmetric] rcis_def cispi cis_mult[symmetric])
3.654 -  done
3.655 -
3.656 -text {* Nonzero polynomial in z goes to infinity as z does. *}
3.657 -
3.658 -lemma poly_infinity:
3.659 -  assumes ex: "p \<noteq> 0"
3.660 -  shows "\<exists>r. \<forall>z. r \<le> cmod z \<longrightarrow> d \<le> cmod (poly (pCons a p) z)"
3.661 -using ex
3.662 -proof(induct p arbitrary: a d)
3.663 -  case (pCons c cs a d)
3.664 -  {assume H: "cs \<noteq> 0"
3.665 -    with pCons.hyps obtain r where r: "\<forall>z. r \<le> cmod z \<longrightarrow> d + cmod a \<le> cmod (poly (pCons c cs) z)" by blast
3.666 -    let ?r = "1 + \<bar>r\<bar>"
3.667 -    {fix z assume h: "1 + \<bar>r\<bar> \<le> cmod z"
3.668 -      have r0: "r \<le> cmod z" using h by arith
3.669 -      from r[rule_format, OF r0]
3.670 -      have th0: "d + cmod a \<le> 1 * cmod(poly (pCons c cs) z)" by arith
3.671 -      from h have z1: "cmod z \<ge> 1" by arith
3.672 -      from order_trans[OF th0 mult_right_mono[OF z1 norm_ge_zero[of "poly (pCons c cs) z"]]]
3.673 -      have th1: "d \<le> cmod(z * poly (pCons c cs) z) - cmod a"
3.674 -	unfolding norm_mult by (simp add: algebra_simps)
3.675 -      from complex_mod_triangle_sub[of "z * poly (pCons c cs) z" a]
3.676 -      have th2: "cmod(z * poly (pCons c cs) z) - cmod a \<le> cmod (poly (pCons a (pCons c cs)) z)"
3.677 -	by (simp add: diff_le_eq algebra_simps)
3.678 -      from th1 th2 have "d \<le> cmod (poly (pCons a (pCons c cs)) z)"  by arith}
3.679 -    hence ?case by blast}
3.680 -  moreover
3.681 -  {assume cs0: "\<not> (cs \<noteq> 0)"
3.682 -    with pCons.prems have c0: "c \<noteq> 0" by simp
3.683 -    from cs0 have cs0': "cs = 0" by simp
3.684 -    {fix z
3.685 -      assume h: "(\<bar>d\<bar> + cmod a) / cmod c \<le> cmod z"
3.686 -      from c0 have "cmod c > 0" by simp
3.687 -      from h c0 have th0: "\<bar>d\<bar> + cmod a \<le> cmod (z*c)"
3.688 -	by (simp add: field_simps norm_mult)
3.689 -      have ath: "\<And>mzh mazh ma. mzh <= mazh + ma ==> abs(d) + ma <= mzh ==> d <= mazh" by arith
3.690 -      from complex_mod_triangle_sub[of "z*c" a ]
3.691 -      have th1: "cmod (z * c) \<le> cmod (a + z * c) + cmod a"
3.692 -	by (simp add: algebra_simps)
3.693 -      from ath[OF th1 th0] have "d \<le> cmod (poly (pCons a (pCons c cs)) z)"
3.694 -        using cs0' by simp}
3.695 -    then have ?case  by blast}
3.696 -  ultimately show ?case by blast
3.697 -qed simp
3.698 -
3.699 -text {* Hence polynomial's modulus attains its minimum somewhere. *}
3.700 -lemma poly_minimum_modulus:
3.701 -  "\<exists>z.\<forall>w. cmod (poly p z) \<le> cmod (poly p w)"
3.702 -proof(induct p)
3.703 -  case (pCons c cs)
3.704 -  {assume cs0: "cs \<noteq> 0"
3.705 -    from poly_infinity[OF cs0, of "cmod (poly (pCons c cs) 0)" c]
3.706 -    obtain r where r: "\<And>z. r \<le> cmod z \<Longrightarrow> cmod (poly (pCons c cs) 0) \<le> cmod (poly (pCons c cs) z)" by blast
3.707 -    have ath: "\<And>z r. r \<le> cmod z \<or> cmod z \<le> \<bar>r\<bar>" by arith
3.708 -    from poly_minimum_modulus_disc[of "\<bar>r\<bar>" "pCons c cs"]
3.709 -    obtain v where v: "\<And>w. cmod w \<le> \<bar>r\<bar> \<Longrightarrow> cmod (poly (pCons c cs) v) \<le> cmod (poly (pCons c cs) w)" by blast
3.710 -    {fix z assume z: "r \<le> cmod z"
3.711 -      from v[of 0] r[OF z]
3.712 -      have "cmod (poly (pCons c cs) v) \<le> cmod (poly (pCons c cs) z)"
3.713 -	by simp }
3.714 -    note v0 = this
3.715 -    from v0 v ath[of r] have ?case by blast}
3.716 -  moreover
3.717 -  {assume cs0: "\<not> (cs \<noteq> 0)"
3.718 -    hence th:"cs = 0" by simp
3.719 -    from th pCons.hyps have ?case by simp}
3.720 -  ultimately show ?case by blast
3.721 -qed simp
3.722 -
3.723 -text{* Constant function (non-syntactic characterization). *}
3.724 -definition "constant f = (\<forall>x y. f x = f y)"
3.725 -
3.726 -lemma nonconstant_length: "\<not> (constant (poly p)) \<Longrightarrow> psize p \<ge> 2"
3.727 -  unfolding constant_def psize_def
3.728 -  apply (induct p, auto)
3.729 -  done
3.730 -
3.731 -lemma poly_replicate_append:
3.732 -  "poly (monom 1 n * p) (x::'a::{recpower, comm_ring_1}) = x^n * poly p x"
3.733 -  by (simp add: poly_monom)
3.734 -
3.735 -text {* Decomposition of polynomial, skipping zero coefficients
3.736 -  after the first.  *}
3.737 -
3.738 -lemma poly_decompose_lemma:
3.739 - assumes nz: "\<not>(\<forall>z. z\<noteq>0 \<longrightarrow> poly p z = (0::'a::{recpower,idom}))"
3.740 -  shows "\<exists>k a q. a\<noteq>0 \<and> Suc (psize q + k) = psize p \<and>
3.741 -                 (\<forall>z. poly p z = z^k * poly (pCons a q) z)"
3.742 -unfolding psize_def
3.743 -using nz
3.744 -proof(induct p)
3.745 -  case 0 thus ?case by simp
3.746 -next
3.747 -  case (pCons c cs)
3.748 -  {assume c0: "c = 0"
3.749 -    from pCons.hyps pCons.prems c0 have ?case apply auto
3.750 -      apply (rule_tac x="k+1" in exI)
3.751 -      apply (rule_tac x="a" in exI, clarsimp)
3.752 -      apply (rule_tac x="q" in exI)
3.753 -      by (auto simp add: power_Suc)}
3.754 -  moreover
3.755 -  {assume c0: "c\<noteq>0"
3.756 -    hence ?case apply-
3.757 -      apply (rule exI[where x=0])
3.758 -      apply (rule exI[where x=c], clarsimp)
3.759 -      apply (rule exI[where x=cs])
3.760 -      apply auto
3.761 -      done}
3.762 -  ultimately show ?case by blast
3.763 -qed
3.764 -
3.765 -lemma poly_decompose:
3.766 -  assumes nc: "~constant(poly p)"
3.767 -  shows "\<exists>k a q. a\<noteq>(0::'a::{recpower,idom}) \<and> k\<noteq>0 \<and>
3.768 -               psize q + k + 1 = psize p \<and>
3.769 -              (\<forall>z. poly p z = poly p 0 + z^k * poly (pCons a q) z)"
3.770 -using nc
3.771 -proof(induct p)
3.772 -  case 0 thus ?case by (simp add: constant_def)
3.773 -next
3.774 -  case (pCons c cs)
3.775 -  {assume C:"\<forall>z. z \<noteq> 0 \<longrightarrow> poly cs z = 0"
3.776 -    {fix x y
3.777 -      from C have "poly (pCons c cs) x = poly (pCons c cs) y" by (cases "x=0", auto)}
3.778 -    with pCons.prems have False by (auto simp add: constant_def)}
3.779 -  hence th: "\<not> (\<forall>z. z \<noteq> 0 \<longrightarrow> poly cs z = 0)" ..
3.780 -  from poly_decompose_lemma[OF th]
3.781 -  show ?case
3.782 -    apply clarsimp
3.783 -    apply (rule_tac x="k+1" in exI)
3.784 -    apply (rule_tac x="a" in exI)
3.785 -    apply simp
3.786 -    apply (rule_tac x="q" in exI)
3.787 -    apply (auto simp add: power_Suc)
3.788 -    apply (auto simp add: psize_def split: if_splits)
3.789 -    done
3.790 -qed
3.791 -
3.792 -text{* Fundamental theorem of algebral *}
3.793 -
3.794 -lemma fundamental_theorem_of_algebra:
3.795 -  assumes nc: "~constant(poly p)"
3.796 -  shows "\<exists>z::complex. poly p z = 0"
3.797 -using nc
3.798 -proof(induct n\<equiv> "psize p" arbitrary: p rule: nat_less_induct)
3.799 -  fix n fix p :: "complex poly"
3.800 -  let ?p = "poly p"
3.801 -  assume H: "\<forall>m<n. \<forall>p. \<not> constant (poly p) \<longrightarrow> m = psize p \<longrightarrow> (\<exists>(z::complex). poly p z = 0)" and nc: "\<not> constant ?p" and n: "n = psize p"
3.802 -  let ?ths = "\<exists>z. ?p z = 0"
3.803 -
3.804 -  from nonconstant_length[OF nc] have n2: "n\<ge> 2" by (simp add: n)
3.805 -  from poly_minimum_modulus obtain c where
3.806 -    c: "\<forall>w. cmod (?p c) \<le> cmod (?p w)" by blast
3.807 -  {assume pc: "?p c = 0" hence ?ths by blast}
3.808 -  moreover
3.809 -  {assume pc0: "?p c \<noteq> 0"
3.810 -    from poly_offset[of p c] obtain q where
3.811 -      q: "psize q = psize p" "\<forall>x. poly q x = ?p (c+x)" by blast
3.812 -    {assume h: "constant (poly q)"
3.813 -      from q(2) have th: "\<forall>x. poly q (x - c) = ?p x" by auto
3.814 -      {fix x y
3.815 -	from th have "?p x = poly q (x - c)" by auto
3.816 -	also have "\<dots> = poly q (y - c)"
3.817 -	  using h unfolding constant_def by blast
3.818 -	also have "\<dots> = ?p y" using th by auto
3.819 -	finally have "?p x = ?p y" .}
3.820 -      with nc have False unfolding constant_def by blast }
3.821 -    hence qnc: "\<not> constant (poly q)" by blast
3.822 -    from q(2) have pqc0: "?p c = poly q 0" by simp
3.823 -    from c pqc0 have cq0: "\<forall>w. cmod (poly q 0) \<le> cmod (?p w)" by simp
3.824 -    let ?a0 = "poly q 0"
3.825 -    from pc0 pqc0 have a00: "?a0 \<noteq> 0" by simp
3.826 -    from a00
3.827 -    have qr: "\<forall>z. poly q z = poly (smult (inverse ?a0) q) z * ?a0"
3.828 -      by simp
3.829 -    let ?r = "smult (inverse ?a0) q"
3.830 -    have lgqr: "psize q = psize ?r"
3.831 -      using a00 unfolding psize_def degree_def
3.832 -      by (simp add: expand_poly_eq)
3.833 -    {assume h: "\<And>x y. poly ?r x = poly ?r y"
3.834 -      {fix x y
3.835 -	from qr[rule_format, of x]
3.836 -	have "poly q x = poly ?r x * ?a0" by auto
3.837 -	also have "\<dots> = poly ?r y * ?a0" using h by simp
3.838 -	also have "\<dots> = poly q y" using qr[rule_format, of y] by simp
3.839 -	finally have "poly q x = poly q y" .}
3.840 -      with qnc have False unfolding constant_def by blast}
3.841 -    hence rnc: "\<not> constant (poly ?r)" unfolding constant_def by blast
3.842 -    from qr[rule_format, of 0] a00  have r01: "poly ?r 0 = 1" by auto
3.843 -    {fix w
3.844 -      have "cmod (poly ?r w) < 1 \<longleftrightarrow> cmod (poly q w / ?a0) < 1"
3.845 -	using qr[rule_format, of w] a00 by (simp add: divide_inverse mult_ac)
3.846 -      also have "\<dots> \<longleftrightarrow> cmod (poly q w) < cmod ?a0"
3.847 -	using a00 unfolding norm_divide by (simp add: field_simps)
3.848 -      finally have "cmod (poly ?r w) < 1 \<longleftrightarrow> cmod (poly q w) < cmod ?a0" .}
3.849 -    note mrmq_eq = this
3.850 -    from poly_decompose[OF rnc] obtain k a s where
3.851 -      kas: "a\<noteq>0" "k\<noteq>0" "psize s + k + 1 = psize ?r"
3.852 -      "\<forall>z. poly ?r z = poly ?r 0 + z^k* poly (pCons a s) z" by blast
3.853 -    {assume "k + 1 = n"
3.854 -      with kas(3) lgqr[symmetric] q(1) n[symmetric] have s0:"s=0" by auto
3.855 -      {fix w
3.856 -	have "cmod (poly ?r w) = cmod (1 + a * w ^ k)"
3.857 -	  using kas(4)[rule_format, of w] s0 r01 by (simp add: algebra_simps)}
3.858 -      note hth = this [symmetric]
3.859 -	from reduce_poly_simple[OF kas(1,2)]
3.860 -      have "\<exists>w. cmod (poly ?r w) < 1" unfolding hth by blast}
3.861 -    moreover
3.862 -    {assume kn: "k+1 \<noteq> n"
3.863 -      from kn kas(3) q(1) n[symmetric] lgqr have k1n: "k + 1 < n" by simp
3.864 -      have th01: "\<not> constant (poly (pCons 1 (monom a (k - 1))))"
3.865 -	unfolding constant_def poly_pCons poly_monom
3.866 -	using kas(1) apply simp
3.867 -	by (rule exI[where x=0], rule exI[where x=1], simp)
3.868 -      from kas(1) kas(2) have th02: "k+1 = psize (pCons 1 (monom a (k - 1)))"
3.869 -	by (simp add: psize_def degree_monom_eq)
3.870 -      from H[rule_format, OF k1n th01 th02]
3.871 -      obtain w where w: "1 + w^k * a = 0"
3.872 -	unfolding poly_pCons poly_monom
3.873 -	using kas(2) by (cases k, auto simp add: algebra_simps)
3.874 -      from poly_bound_exists[of "cmod w" s] obtain m where
3.875 -	m: "m > 0" "\<forall>z. cmod z \<le> cmod w \<longrightarrow> cmod (poly s z) \<le> m" by blast
3.876 -      have w0: "w\<noteq>0" using kas(2) w by (auto simp add: power_0_left)
3.877 -      from w have "(1 + w ^ k * a) - 1 = 0 - 1" by simp
3.878 -      then have wm1: "w^k * a = - 1" by simp
3.879 -      have inv0: "0 < inverse (cmod w ^ (k + 1) * m)"
3.880 -	using norm_ge_zero[of w] w0 m(1)
3.881 -	  by (simp add: inverse_eq_divide zero_less_mult_iff)
3.882 -      with real_down2[OF zero_less_one] obtain t where
3.883 -	t: "t > 0" "t < 1" "t < inverse (cmod w ^ (k + 1) * m)" by blast
3.884 -      let ?ct = "complex_of_real t"
3.885 -      let ?w = "?ct * w"
3.886 -      have "1 + ?w^k * (a + ?w * poly s ?w) = 1 + ?ct^k * (w^k * a) + ?w^k * ?w * poly s ?w" using kas(1) by (simp add: algebra_simps power_mult_distrib)
3.887 -      also have "\<dots> = complex_of_real (1 - t^k) + ?w^k * ?w * poly s ?w"
3.888 -	unfolding wm1 by (simp)
3.889 -      finally have "cmod (1 + ?w^k * (a + ?w * poly s ?w)) = cmod (complex_of_real (1 - t^k) + ?w^k * ?w * poly s ?w)"
3.890 -	apply -
3.891 -	apply (rule cong[OF refl[of cmod]])
3.892 -	apply assumption
3.893 -	done
3.894 -      with norm_triangle_ineq[of "complex_of_real (1 - t^k)" "?w^k * ?w * poly s ?w"]
3.895 -      have th11: "cmod (1 + ?w^k * (a + ?w * poly s ?w)) \<le> \<bar>1 - t^k\<bar> + cmod (?w^k * ?w * poly s ?w)" unfolding norm_of_real by simp
3.896 -      have ath: "\<And>x (t::real). 0\<le> x \<Longrightarrow> x < t \<Longrightarrow> t\<le>1 \<Longrightarrow> \<bar>1 - t\<bar> + x < 1" by arith
3.897 -      have "t *cmod w \<le> 1 * cmod w" apply (rule mult_mono) using t(1,2) by auto
3.898 -      then have tw: "cmod ?w \<le> cmod w" using t(1) by (simp add: norm_mult)
3.899 -      from t inv0 have "t* (cmod w ^ (k + 1) * m) < 1"
3.900 -	by (simp add: inverse_eq_divide field_simps)
3.901 -      with zero_less_power[OF t(1), of k]
3.902 -      have th30: "t^k * (t* (cmod w ^ (k + 1) * m)) < t^k * 1"
3.903 -	apply - apply (rule mult_strict_left_mono) by simp_all
3.904 -      have "cmod (?w^k * ?w * poly s ?w) = t^k * (t* (cmod w ^ (k+1) * cmod (poly s ?w)))"  using w0 t(1)
3.905 -	by (simp add: algebra_simps power_mult_distrib norm_of_real norm_power norm_mult)
3.906 -      then have "cmod (?w^k * ?w * poly s ?w) \<le> t^k * (t* (cmod w ^ (k + 1) * m))"
3.907 -	using t(1,2) m(2)[rule_format, OF tw] w0
3.908 -	apply (simp only: )
3.909 -	apply auto
3.910 -	apply (rule mult_mono, simp_all add: norm_ge_zero)+
3.911 -	apply (simp add: zero_le_mult_iff zero_le_power)
3.912 -	done
3.913 -      with th30 have th120: "cmod (?w^k * ?w * poly s ?w) < t^k" by simp
3.914 -      from power_strict_mono[OF t(2), of k] t(1) kas(2) have th121: "t^k \<le> 1"
3.915 -	by auto
3.916 -      from ath[OF norm_ge_zero[of "?w^k * ?w * poly s ?w"] th120 th121]
3.917 -      have th12: "\<bar>1 - t^k\<bar> + cmod (?w^k * ?w * poly s ?w) < 1" .
3.918 -      from th11 th12
3.919 -      have "cmod (1 + ?w^k * (a + ?w * poly s ?w)) < 1"  by arith
3.920 -      then have "cmod (poly ?r ?w) < 1"
3.921 -	unfolding kas(4)[rule_format, of ?w] r01 by simp
3.922 -      then have "\<exists>w. cmod (poly ?r w) < 1" by blast}
3.923 -    ultimately have cr0_contr: "\<exists>w. cmod (poly ?r w) < 1" by blast
3.924 -    from cr0_contr cq0 q(2)
3.925 -    have ?ths unfolding mrmq_eq not_less[symmetric] by auto}
3.926 -  ultimately show ?ths by blast
3.927 -qed
3.928 -
3.929 -text {* Alternative version with a syntactic notion of constant polynomial. *}
3.930 -
3.931 -lemma fundamental_theorem_of_algebra_alt:
3.932 -  assumes nc: "~(\<exists>a l. a\<noteq> 0 \<and> l = 0 \<and> p = pCons a l)"
3.933 -  shows "\<exists>z. poly p z = (0::complex)"
3.934 -using nc
3.935 -proof(induct p)
3.936 -  case (pCons c cs)
3.937 -  {assume "c=0" hence ?case by auto}
3.938 -  moreover
3.939 -  {assume c0: "c\<noteq>0"
3.940 -    {assume nc: "constant (poly (pCons c cs))"
3.941 -      from nc[unfolded constant_def, rule_format, of 0]
3.942 -      have "\<forall>w. w \<noteq> 0 \<longrightarrow> poly cs w = 0" by auto
3.943 -      hence "cs = 0"
3.944 -	proof(induct cs)
3.945 -	  case (pCons d ds)
3.946 -	  {assume "d=0" hence ?case using pCons.prems pCons.hyps by simp}
3.947 -	  moreover
3.948 -	  {assume d0: "d\<noteq>0"
3.949 -	    from poly_bound_exists[of 1 ds] obtain m where
3.950 -	      m: "m > 0" "\<forall>z. \<forall>z. cmod z \<le> 1 \<longrightarrow> cmod (poly ds z) \<le> m" by blast
3.951 -	    have dm: "cmod d / m > 0" using d0 m(1) by (simp add: field_simps)
3.952 -	    from real_down2[OF dm zero_less_one] obtain x where
3.953 -	      x: "x > 0" "x < cmod d / m" "x < 1" by blast
3.954 -	    let ?x = "complex_of_real x"
3.955 -	    from x have cx: "?x \<noteq> 0"  "cmod ?x \<le> 1" by simp_all
3.956 -	    from pCons.prems[rule_format, OF cx(1)]
3.957 -	    have cth: "cmod (?x*poly ds ?x) = cmod d" by (simp add: eq_diff_eq[symmetric])
3.958 -	    from m(2)[rule_format, OF cx(2)] x(1)
3.959 -	    have th0: "cmod (?x*poly ds ?x) \<le> x*m"
3.960 -	      by (simp add: norm_mult)
3.961 -	    from x(2) m(1) have "x*m < cmod d" by (simp add: field_simps)
3.962 -	    with th0 have "cmod (?x*poly ds ?x) \<noteq> cmod d" by auto
3.963 -	    with cth  have ?case by blast}
3.964 -	  ultimately show ?case by blast
3.965 -	qed simp}
3.966 -      then have nc: "\<not> constant (poly (pCons c cs))" using pCons.prems c0
3.967 -	by blast
3.968 -      from fundamental_theorem_of_algebra[OF nc] have ?case .}
3.969 -  ultimately show ?case by blast
3.970 -qed simp
3.971 -
3.972 -subsection {* Order of polynomial roots *}
3.973 -
3.974 -definition
3.975 -  order :: "'a::{idom,recpower} \<Rightarrow> 'a poly \<Rightarrow> nat"
3.976 -where
3.977 -  [code del]:
3.978 -  "order a p = (LEAST n. \<not> [:-a, 1:] ^ Suc n dvd p)"
3.979 -
3.980 -lemma degree_power_le: "degree (p ^ n) \<le> degree p * n"
3.981 -by (induct n, simp, auto intro: order_trans degree_mult_le)
3.982 -
3.983 -lemma coeff_linear_power:
3.984 -  fixes a :: "'a::{comm_semiring_1,recpower}"
3.985 -  shows "coeff ([:a, 1:] ^ n) n = 1"
3.986 -apply (induct n, simp_all)
3.987 -apply (subst coeff_eq_0)
3.988 -apply (auto intro: le_less_trans degree_power_le)
3.989 -done
3.990 -
3.991 -lemma degree_linear_power:
3.992 -  fixes a :: "'a::{comm_semiring_1,recpower}"
3.993 -  shows "degree ([:a, 1:] ^ n) = n"
3.994 -apply (rule order_antisym)
3.995 -apply (rule ord_le_eq_trans [OF degree_power_le], simp)
3.996 -apply (rule le_degree, simp add: coeff_linear_power)
3.997 -done
3.998 -
3.999 -lemma order_1: "[:-a, 1:] ^ order a p dvd p"
3.1000 -apply (cases "p = 0", simp)
3.1001 -apply (cases "order a p", simp)
3.1002 -apply (subgoal_tac "nat < (LEAST n. \<not> [:-a, 1:] ^ Suc n dvd p)")
3.1003 -apply (drule not_less_Least, simp)
3.1004 -apply (fold order_def, simp)
3.1005 -done
3.1006 -
3.1007 -lemma order_2: "p \<noteq> 0 \<Longrightarrow> \<not> [:-a, 1:] ^ Suc (order a p) dvd p"
3.1008 -unfolding order_def
3.1009 -apply (rule LeastI_ex)
3.1010 -apply (rule_tac x="degree p" in exI)
3.1011 -apply (rule notI)
3.1012 -apply (drule (1) dvd_imp_degree_le)
3.1013 -apply (simp only: degree_linear_power)
3.1014 -done
3.1015 -
3.1016 -lemma order:
3.1017 -  "p \<noteq> 0 \<Longrightarrow> [:-a, 1:] ^ order a p dvd p \<and> \<not> [:-a, 1:] ^ Suc (order a p) dvd p"
3.1018 -by (rule conjI [OF order_1 order_2])
3.1019 -
3.1020 -lemma order_degree:
3.1021 -  assumes p: "p \<noteq> 0"
3.1022 -  shows "order a p \<le> degree p"
3.1023 -proof -
3.1024 -  have "order a p = degree ([:-a, 1:] ^ order a p)"
3.1025 -    by (simp only: degree_linear_power)
3.1026 -  also have "\<dots> \<le> degree p"
3.1027 -    using order_1 p by (rule dvd_imp_degree_le)
3.1028 -  finally show ?thesis .
3.1029 -qed
3.1030 -
3.1031 -lemma order_root: "poly p a = 0 \<longleftrightarrow> p = 0 \<or> order a p \<noteq> 0"
3.1032 -apply (cases "p = 0", simp_all)
3.1033 -apply (rule iffI)
3.1034 -apply (rule ccontr, simp)
3.1035 -apply (frule order_2 [where a=a], simp)
3.1038 -apply (simp only: order_def)
3.1039 -apply (drule not_less_Least, simp)
3.1040 -done
3.1041 -
3.1042 -lemma UNIV_nat_infinite:
3.1043 -  "\<not> finite (UNIV :: nat set)" (is "\<not> finite ?U")
3.1044 -proof
3.1045 -  assume "finite ?U"
3.1046 -  moreover have "Suc (Max ?U) \<in> ?U" ..
3.1047 -  ultimately have "Suc (Max ?U) \<le> Max ?U" by (rule Max_ge)
3.1048 -  then show "False" by simp
3.1049 -qed
3.1050 -
3.1051 -lemma UNIV_char_0_infinite:
3.1052 -  "\<not> finite (UNIV::'a::semiring_char_0 set)"
3.1053 -proof
3.1054 -  assume "finite (UNIV::'a set)"
3.1055 -  with subset_UNIV have "finite (range of_nat::'a set)"
3.1056 -    by (rule finite_subset)
3.1057 -  moreover have "inj (of_nat::nat \<Rightarrow> 'a)"
3.1058 -    by (simp add: inj_on_def)
3.1059 -  ultimately have "finite (UNIV::nat set)"
3.1060 -    by (rule finite_imageD)
3.1061 -  then show "False"
3.1062 -    by (simp add: UNIV_nat_infinite)
3.1063 -qed
3.1064 -
3.1065 -lemma poly_zero:
3.1066 -  fixes p :: "'a::{idom,ring_char_0} poly"
3.1067 -  shows "poly p = poly 0 \<longleftrightarrow> p = 0"
3.1068 -apply (cases "p = 0", simp_all)
3.1069 -apply (drule poly_roots_finite)
3.1070 -apply (auto simp add: UNIV_char_0_infinite)
3.1071 -done
3.1072 -
3.1073 -lemma poly_eq_iff:
3.1074 -  fixes p q :: "'a::{idom,ring_char_0} poly"
3.1075 -  shows "poly p = poly q \<longleftrightarrow> p = q"
3.1076 -  using poly_zero [of "p - q"]
3.1077 -  by (simp add: expand_fun_eq)
3.1078 -
3.1079 -
3.1080 -subsection{* Nullstellenstatz, degrees and divisibility of polynomials *}
3.1081 -
3.1082 -lemma nullstellensatz_lemma:
3.1083 -  fixes p :: "complex poly"
3.1084 -  assumes "\<forall>x. poly p x = 0 \<longrightarrow> poly q x = 0"
3.1085 -  and "degree p = n" and "n \<noteq> 0"
3.1086 -  shows "p dvd (q ^ n)"
3.1087 -using prems
3.1088 -proof(induct n arbitrary: p q rule: nat_less_induct)
3.1089 -  fix n::nat fix p q :: "complex poly"
3.1090 -  assume IH: "\<forall>m<n. \<forall>p q.
3.1091 -                 (\<forall>x. poly p x = (0::complex) \<longrightarrow> poly q x = 0) \<longrightarrow>
3.1092 -                 degree p = m \<longrightarrow> m \<noteq> 0 \<longrightarrow> p dvd (q ^ m)"
3.1093 -    and pq0: "\<forall>x. poly p x = 0 \<longrightarrow> poly q x = 0"
3.1094 -    and dpn: "degree p = n" and n0: "n \<noteq> 0"
3.1095 -  from dpn n0 have pne: "p \<noteq> 0" by auto
3.1096 -  let ?ths = "p dvd (q ^ n)"
3.1097 -  {fix a assume a: "poly p a = 0"
3.1098 -    {assume oa: "order a p \<noteq> 0"
3.1099 -      let ?op = "order a p"
3.1100 -      from pne have ap: "([:- a, 1:] ^ ?op) dvd p"
3.1101 -	"\<not> [:- a, 1:] ^ (Suc ?op) dvd p" using order by blast+
3.1102 -      note oop = order_degree[OF pne, unfolded dpn]
3.1103 -      {assume q0: "q = 0"
3.1104 -	hence ?ths using n0
3.1105 -          by (simp add: power_0_left)}
3.1106 -      moreover
3.1107 -      {assume q0: "q \<noteq> 0"
3.1108 -	from pq0[rule_format, OF a, unfolded poly_eq_0_iff_dvd]
3.1109 -	obtain r where r: "q = [:- a, 1:] * r" by (rule dvdE)
3.1110 -	from ap(1) obtain s where
3.1111 -	  s: "p = [:- a, 1:] ^ ?op * s" by (rule dvdE)
3.1112 -	have sne: "s \<noteq> 0"
3.1113 -	  using s pne by auto
3.1114 -	{assume ds0: "degree s = 0"
3.1115 -	  from ds0 have "\<exists>k. s = [:k:]"
3.1116 -            by (cases s, simp split: if_splits)
3.1117 -	  then obtain k where kpn: "s = [:k:]" by blast
3.1118 -          from sne kpn have k: "k \<noteq> 0" by simp
3.1119 -	  let ?w = "([:1/k:] * ([:-a,1:] ^ (n - ?op))) * (r ^ n)"
3.1120 -          from k oop [of a] have "q ^ n = p * ?w"
3.1121 -            apply -
3.1122 -            apply (subst r, subst s, subst kpn)
3.1123 -            apply (subst power_mult_distrib, simp)
3.1124 -            apply (subst power_add [symmetric], simp)
3.1125 -            done
3.1126 -	  hence ?ths unfolding dvd_def by blast}
3.1127 -	moreover
3.1128 -	{assume ds0: "degree s \<noteq> 0"
3.1129 -	  from ds0 sne dpn s oa
3.1130 -	    have dsn: "degree s < n" apply auto
3.1131 -              apply (erule ssubst)
3.1132 -              apply (simp add: degree_mult_eq degree_linear_power)
3.1133 -              done
3.1134 -	    {fix x assume h: "poly s x = 0"
3.1135 -	      {assume xa: "x = a"
3.1136 -		from h[unfolded xa poly_eq_0_iff_dvd] obtain u where
3.1137 -		  u: "s = [:- a, 1:] * u" by (rule dvdE)
3.1138 -		have "p = [:- a, 1:] ^ (Suc ?op) * u"
3.1139 -                  by (subst s, subst u, simp only: power_Suc mult_ac)
3.1140 -		with ap(2)[unfolded dvd_def] have False by blast}
3.1141 -	      note xa = this
3.1142 -	      from h have "poly p x = 0" by (subst s, simp)
3.1143 -	      with pq0 have "poly q x = 0" by blast
3.1144 -	      with r xa have "poly r x = 0"
3.1146 -	    note impth = this
3.1147 -	    from IH[rule_format, OF dsn, of s r] impth ds0
3.1148 -	    have "s dvd (r ^ (degree s))" by blast
3.1149 -	    then obtain u where u: "r ^ (degree s) = s * u" ..
3.1150 -	    hence u': "\<And>x. poly s x * poly u x = poly r x ^ degree s"
3.1151 -              by (simp only: poly_mult[symmetric] poly_power[symmetric])
3.1152 -	    let ?w = "(u * ([:-a,1:] ^ (n - ?op))) * (r ^ (n - degree s))"
3.1153 -	    from oop[of a] dsn have "q ^ n = p * ?w"
3.1154 -              apply -
3.1155 -              apply (subst s, subst r)
3.1156 -              apply (simp only: power_mult_distrib)
3.1157 -              apply (subst mult_assoc [where b=s])
3.1158 -              apply (subst mult_assoc [where a=u])
3.1159 -              apply (subst mult_assoc [where b=u, symmetric])
3.1160 -              apply (subst u [symmetric])
3.1162 -              done
3.1163 -	    hence ?ths unfolding dvd_def by blast}
3.1164 -      ultimately have ?ths by blast }
3.1165 -      ultimately have ?ths by blast}
3.1166 -    then have ?ths using a order_root pne by blast}
3.1167 -  moreover
3.1168 -  {assume exa: "\<not> (\<exists>a. poly p a = 0)"
3.1169 -    from fundamental_theorem_of_algebra_alt[of p] exa obtain c where
3.1170 -      ccs: "c\<noteq>0" "p = pCons c 0" by blast
3.1171 -
3.1172 -    then have pp: "\<And>x. poly p x =  c" by simp
3.1173 -    let ?w = "[:1/c:] * (q ^ n)"
3.1174 -    from ccs
3.1175 -    have "(q ^ n) = (p * ?w) "
3.1176 -      by (simp add: smult_smult)
3.1177 -    hence ?ths unfolding dvd_def by blast}
3.1178 -  ultimately show ?ths by blast
3.1179 -qed
3.1180 -
3.1181 -lemma nullstellensatz_univariate:
3.1182 -  "(\<forall>x. poly p x = (0::complex) \<longrightarrow> poly q x = 0) \<longleftrightarrow>
3.1183 -    p dvd (q ^ (degree p)) \<or> (p = 0 \<and> q = 0)"
3.1184 -proof-
3.1185 -  {assume pe: "p = 0"
3.1186 -    hence eq: "(\<forall>x. poly p x = (0::complex) \<longrightarrow> poly q x = 0) \<longleftrightarrow> q = 0"
3.1187 -      apply auto
3.1188 -      apply (rule poly_zero [THEN iffD1])
3.1189 -      by (rule ext, simp)
3.1190 -    {assume "p dvd (q ^ (degree p))"
3.1191 -      then obtain r where r: "q ^ (degree p) = p * r" ..
3.1192 -      from r pe have False by simp}
3.1193 -    with eq pe have ?thesis by blast}
3.1194 -  moreover
3.1195 -  {assume pe: "p \<noteq> 0"
3.1196 -    {assume dp: "degree p = 0"
3.1197 -      then obtain k where k: "p = [:k:]" "k\<noteq>0" using pe
3.1198 -        by (cases p, simp split: if_splits)
3.1199 -      hence th1: "\<forall>x. poly p x \<noteq> 0" by simp
3.1200 -      from k dp have "q ^ (degree p) = p * [:1/k:]"
3.1201 -        by (simp add: one_poly_def)
3.1202 -      hence th2: "p dvd (q ^ (degree p))" ..
3.1203 -      from th1 th2 pe have ?thesis by blast}
3.1204 -    moreover
3.1205 -    {assume dp: "degree p \<noteq> 0"
3.1206 -      then obtain n where n: "degree p = Suc n " by (cases "degree p", auto)
3.1207 -      {assume "p dvd (q ^ (Suc n))"
3.1208 -	then obtain u where u: "q ^ (Suc n) = p * u" ..
3.1209 -	{fix x assume h: "poly p x = 0" "poly q x \<noteq> 0"
3.1210 -	  hence "poly (q ^ (Suc n)) x \<noteq> 0" by simp
3.1211 -	  hence False using u h(1) by (simp only: poly_mult) simp}}
3.1212 -	with n nullstellensatz_lemma[of p q "degree p"] dp
3.1213 -	have ?thesis by auto}
3.1214 -    ultimately have ?thesis by blast}
3.1215 -  ultimately show ?thesis by blast
3.1216 -qed
3.1217 -
3.1218 -text{* Useful lemma *}
3.1219 -
3.1220 -lemma constant_degree:
3.1221 -  fixes p :: "'a::{idom,ring_char_0} poly"
3.1222 -  shows "constant (poly p) \<longleftrightarrow> degree p = 0" (is "?lhs = ?rhs")
3.1223 -proof
3.1224 -  assume l: ?lhs
3.1225 -  from l[unfolded constant_def, rule_format, of _ "0"]
3.1226 -  have th: "poly p = poly [:poly p 0:]" apply - by (rule ext, simp)
3.1227 -  then have "p = [:poly p 0:]" by (simp add: poly_eq_iff)
3.1228 -  then have "degree p = degree [:poly p 0:]" by simp
3.1229 -  then show ?rhs by simp
3.1230 -next
3.1231 -  assume r: ?rhs
3.1232 -  then obtain k where "p = [:k:]"
3.1233 -    by (cases p, simp split: if_splits)
3.1234 -  then show ?lhs unfolding constant_def by auto
3.1235 -qed
3.1236 -
3.1237 -lemma divides_degree: assumes pq: "p dvd (q:: complex poly)"
3.1238 -  shows "degree p \<le> degree q \<or> q = 0"
3.1239 -apply (cases "q = 0", simp_all)
3.1240 -apply (erule dvd_imp_degree_le [OF pq])
3.1241 -done
3.1242 -
3.1243 -(* Arithmetic operations on multivariate polynomials.                        *)
3.1244 -
3.1245 -lemma mpoly_base_conv:
3.1246 -  "(0::complex) \<equiv> poly 0 x" "c \<equiv> poly [:c:] x" "x \<equiv> poly [:0,1:] x" by simp_all
3.1247 -
3.1248 -lemma mpoly_norm_conv:
3.1249 -  "poly [:0:] (x::complex) \<equiv> poly 0 x" "poly [:poly 0 y:] x \<equiv> poly 0 x" by simp_all
3.1250 -
3.1251 -lemma mpoly_sub_conv:
3.1252 -  "poly p (x::complex) - poly q x \<equiv> poly p x + -1 * poly q x"
3.1253 -  by (simp add: diff_def)
3.1254 -
3.1255 -lemma poly_pad_rule: "poly p x = 0 ==> poly (pCons 0 p) x = (0::complex)" by simp
3.1256 -
3.1257 -lemma poly_cancel_eq_conv: "p = (0::complex) \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> (q = 0) \<equiv> (a * q - b * p = 0)" apply (atomize (full)) by auto
3.1258 -
3.1259 -lemma resolve_eq_raw:  "poly 0 x \<equiv> 0" "poly [:c:] x \<equiv> (c::complex)" by auto
3.1260 -lemma  resolve_eq_then: "(P \<Longrightarrow> (Q \<equiv> Q1)) \<Longrightarrow> (\<not>P \<Longrightarrow> (Q \<equiv> Q2))
3.1261 -  \<Longrightarrow> Q \<equiv> P \<and> Q1 \<or> \<not>P\<and> Q2" apply (atomize (full)) by blast
3.1262 -
3.1264 -  fixes p q :: "complex poly"
3.1265 -  assumes pq: "p dvd q"
3.1266 -  shows "p dvd (pCons (0::complex) q)"
3.1267 -proof-
3.1268 -  have "pCons 0 q = q * [:0,1:]" by simp
3.1269 -  then have "q dvd (pCons 0 q)" ..
3.1270 -  with pq show ?thesis by (rule dvd_trans)
3.1271 -qed
3.1272 -
3.1274 -  fixes p q :: "complex poly"
3.1275 -  assumes pq: "p dvd q"
3.1276 -  shows "p dvd (smult a q)"
3.1277 -proof-
3.1278 -  have "smult a q = q * [:a:]" by simp
3.1279 -  then have "q dvd smult a q" ..
3.1280 -  with pq show ?thesis by (rule dvd_trans)
3.1281 -qed
3.1282 -
3.1283 -
3.1284 -lemma poly_divides_conv0:
3.1285 -  fixes p :: "complex poly"
3.1286 -  assumes lgpq: "degree q < degree p" and lq:"p \<noteq> 0"
3.1287 -  shows "p dvd q \<equiv> q = 0" (is "?lhs \<equiv> ?rhs")
3.1288 -proof-
3.1289 -  {assume r: ?rhs
3.1290 -    hence "q = p * 0" by simp
3.1291 -    hence ?lhs ..}
3.1292 -  moreover
3.1293 -  {assume l: ?lhs
3.1294 -    {assume q0: "q = 0"
3.1295 -      hence ?rhs by simp}
3.1296 -    moreover
3.1297 -    {assume q0: "q \<noteq> 0"
3.1298 -      from l q0 have "degree p \<le> degree q"
3.1299 -        by (rule dvd_imp_degree_le)
3.1300 -      with lgpq have ?rhs by simp }
3.1301 -    ultimately have ?rhs by blast }
3.1302 -  ultimately show "?lhs \<equiv> ?rhs" by - (atomize (full), blast)
3.1303 -qed
3.1304 -
3.1305 -lemma poly_divides_conv1:
3.1306 -  assumes a0: "a\<noteq> (0::complex)" and pp': "(p::complex poly) dvd p'"
3.1307 -  and qrp': "smult a q - p' \<equiv> r"
3.1308 -  shows "p dvd q \<equiv> p dvd (r::complex poly)" (is "?lhs \<equiv> ?rhs")
3.1309 -proof-
3.1310 -  {
3.1311 -  from pp' obtain t where t: "p' = p * t" ..
3.1312 -  {assume l: ?lhs
3.1313 -    then obtain u where u: "q = p * u" ..
3.1314 -     have "r = p * (smult a u - t)"
3.1315 -       using u qrp' [symmetric] t by (simp add: algebra_simps mult_smult_right)
3.1316 -     then have ?rhs ..}
3.1317 -  moreover
3.1318 -  {assume r: ?rhs
3.1319 -    then obtain u where u: "r = p * u" ..
3.1320 -    from u [symmetric] t qrp' [symmetric] a0
3.1321 -    have "q = p * smult (1/a) (u + t)"
3.1322 -      by (simp add: algebra_simps mult_smult_right smult_smult)
3.1323 -    hence ?lhs ..}
3.1324 -  ultimately have "?lhs = ?rhs" by blast }
3.1325 -thus "?lhs \<equiv> ?rhs"  by - (atomize(full), blast)
3.1326 -qed
3.1327 -
3.1328 -lemma basic_cqe_conv1:
3.1329 -  "(\<exists>x. poly p x = 0 \<and> poly 0 x \<noteq> 0) \<equiv> False"
3.1330 -  "(\<exists>x. poly 0 x \<noteq> 0) \<equiv> False"
3.1331 -  "(\<exists>x. poly [:c:] x \<noteq> 0) \<equiv> c\<noteq>0"
3.1332 -  "(\<exists>x. poly 0 x = 0) \<equiv> True"
3.1333 -  "(\<exists>x. poly [:c:] x = 0) \<equiv> c = 0" by simp_all
3.1334 -
3.1335 -lemma basic_cqe_conv2:
3.1336 -  assumes l:"p \<noteq> 0"
3.1337 -  shows "(\<exists>x. poly (pCons a (pCons b p)) x = (0::complex)) \<equiv> True"
3.1338 -proof-
3.1339 -  {fix h t
3.1340 -    assume h: "h\<noteq>0" "t=0"  "pCons a (pCons b p) = pCons h t"
3.1341 -    with l have False by simp}
3.1342 -  hence th: "\<not> (\<exists> h t. h\<noteq>0 \<and> t=0 \<and> pCons a (pCons b p) = pCons h t)"
3.1343 -    by blast
3.1344 -  from fundamental_theorem_of_algebra_alt[OF th]
3.1345 -  show "(\<exists>x. poly (pCons a (pCons b p)) x = (0::complex)) \<equiv> True" by auto
3.1346 -qed
3.1347 -
3.1348 -lemma  basic_cqe_conv_2b: "(\<exists>x. poly p x \<noteq> (0::complex)) \<equiv> (p \<noteq> 0)"
3.1349 -proof-
3.1350 -  have "p = 0 \<longleftrightarrow> poly p = poly 0"
3.1351 -    by (simp add: poly_zero)
3.1352 -  also have "\<dots> \<longleftrightarrow> (\<not> (\<exists>x. poly p x \<noteq> 0))" by (auto intro: ext)
3.1353 -  finally show "(\<exists>x. poly p x \<noteq> (0::complex)) \<equiv> p \<noteq> 0"
3.1354 -    by - (atomize (full), blast)
3.1355 -qed
3.1356 -
3.1357 -lemma basic_cqe_conv3:
3.1358 -  fixes p q :: "complex poly"
3.1359 -  assumes l: "p \<noteq> 0"
3.1360 -  shows "(\<exists>x. poly (pCons a p) x = 0 \<and> poly q x \<noteq> 0) \<equiv> \<not> ((pCons a p) dvd (q ^ (psize p)))"
3.1361 -proof-
3.1362 -  from l have dp:"degree (pCons a p) = psize p" by (simp add: psize_def)
3.1363 -  from nullstellensatz_univariate[of "pCons a p" q] l
3.1364 -  show "(\<exists>x. poly (pCons a p) x = 0 \<and> poly q x \<noteq> 0) \<equiv> \<not> ((pCons a p) dvd (q ^ (psize p)))"
3.1365 -    unfolding dp
3.1366 -    by - (atomize (full), auto)
3.1367 -qed
3.1368 -
3.1369 -lemma basic_cqe_conv4:
3.1370 -  fixes p q :: "complex poly"
3.1371 -  assumes h: "\<And>x. poly (q ^ n) x \<equiv> poly r x"
3.1372 -  shows "p dvd (q ^ n) \<equiv> p dvd r"
3.1373 -proof-
3.1374 -  from h have "poly (q ^ n) = poly r" by (auto intro: ext)
3.1375 -  then have "(q ^ n) = r" by (simp add: poly_eq_iff)
3.1376 -  thus "p dvd (q ^ n) \<equiv> p dvd r" by simp
3.1377 -qed
3.1378 -
3.1379 -lemma pmult_Cons_Cons: "(pCons (a::complex) (pCons b p) * q = (smult a q) + (pCons 0 (pCons b p * q)))"
3.1380 -  by simp
3.1381 -
3.1382 -lemma elim_neg_conv: "- z \<equiv> (-1) * (z::complex)" by simp
3.1383 -lemma eqT_intr: "PROP P \<Longrightarrow> (True \<Longrightarrow> PROP P )" "PROP P \<Longrightarrow> True" by blast+
3.1384 -lemma negate_negate_rule: "Trueprop P \<equiv> \<not> P \<equiv> False" by (atomize (full), auto)
3.1385 -
3.1386 -lemma complex_entire: "(z::complex) \<noteq> 0 \<and> w \<noteq> 0 \<equiv> z*w \<noteq> 0" by simp
3.1387 -lemma resolve_eq_ne: "(P \<equiv> True) \<equiv> (\<not>P \<equiv> False)" "(P \<equiv> False) \<equiv> (\<not>P \<equiv> True)"
3.1388 -  by (atomize (full)) simp_all
3.1389 -lemma cqe_conv1: "poly 0 x = 0 \<longleftrightarrow> True"  by simp
3.1390 -lemma cqe_conv2: "(p \<Longrightarrow> (q \<equiv> r)) \<equiv> ((p \<and> q) \<equiv> (p \<and> r))"  (is "?l \<equiv> ?r")
3.1391 -proof
3.1392 -  assume "p \<Longrightarrow> q \<equiv> r" thus "p \<and> q \<equiv> p \<and> r" apply - apply (atomize (full)) by blast
3.1393 -next
3.1394 -  assume "p \<and> q \<equiv> p \<and> r" "p"
3.1395 -  thus "q \<equiv> r" apply - apply (atomize (full)) apply blast done
3.1396 -qed
3.1397 -lemma poly_const_conv: "poly [:c:] (x::complex) = y \<longleftrightarrow> c = y" by simp
3.1398 -
3.1399 -end
```
```     4.1 --- a/src/HOL/IsaMakefile	Wed Feb 11 11:22:42 2009 -0800
4.2 +++ b/src/HOL/IsaMakefile	Thu Feb 12 18:14:43 2009 +0100
4.3 @@ -270,7 +270,6 @@
4.4  \$(OUT)/HOL: ROOT.ML \$(MAIN_DEPENDENCIES) \
4.5    Complex_Main.thy \
4.6    Complex.thy \
4.7 -  Fundamental_Theorem_Algebra.thy \
4.8    Deriv.thy \
4.9    Fact.thy \
4.10    FrechetDeriv.thy \
4.11 @@ -317,6 +316,7 @@
4.12    Library/Executable_Set.thy Library/Infinite_Set.thy			\
4.13    Library/FuncSet.thy Library/Permutations.thy Library/Determinants.thy\
4.14    Library/Finite_Cartesian_Product.thy \
4.15 +  Library/Fundamental_Theorem_Algebra.thy \
4.17    Library/Multiset.thy Library/Permutation.thy	\
4.18    Library/Primes.thy Library/Pocklington.thy Library/Quotient.thy	\
```
```     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Thu Feb 12 18:14:43 2009 +0100
5.3 @@ -0,0 +1,1353 @@
5.4 +(* Author: Amine Chaieb, TU Muenchen *)
5.5 +
5.7 +
5.8 +theory Fundamental_Theorem_Algebra
5.9 +imports Polynomial Complex
5.10 +begin
5.11 +
5.12 +subsection {* Square root of complex numbers *}
5.13 +definition csqrt :: "complex \<Rightarrow> complex" where
5.14 +"csqrt z = (if Im z = 0 then
5.15 +            if 0 \<le> Re z then Complex (sqrt(Re z)) 0
5.16 +            else Complex 0 (sqrt(- Re z))
5.17 +           else Complex (sqrt((cmod z + Re z) /2))
5.18 +                        ((Im z / abs(Im z)) * sqrt((cmod z - Re z) /2)))"
5.19 +
5.20 +lemma csqrt[algebra]: "csqrt z ^ 2 = z"
5.21 +proof-
5.22 +  obtain x y where xy: "z = Complex x y" by (cases z)
5.23 +  {assume y0: "y = 0"
5.24 +    {assume x0: "x \<ge> 0"
5.25 +      then have ?thesis using y0 xy real_sqrt_pow2[OF x0]
5.26 +	by (simp add: csqrt_def power2_eq_square)}
5.27 +    moreover
5.28 +    {assume "\<not> x \<ge> 0" hence x0: "- x \<ge> 0" by arith
5.29 +      then have ?thesis using y0 xy real_sqrt_pow2[OF x0]
5.30 +	by (simp add: csqrt_def power2_eq_square) }
5.31 +    ultimately have ?thesis by blast}
5.32 +  moreover
5.33 +  {assume y0: "y\<noteq>0"
5.34 +    {fix x y
5.35 +      let ?z = "Complex x y"
5.36 +      from abs_Re_le_cmod[of ?z] have tha: "abs x \<le> cmod ?z" by auto
5.37 +      hence "cmod ?z - x \<ge> 0" "cmod ?z + x \<ge> 0" by arith+
5.38 +      hence "(sqrt (x * x + y * y) + x) / 2 \<ge> 0" "(sqrt (x * x + y * y) - x) / 2 \<ge> 0" by (simp_all add: power2_eq_square) }
5.39 +    note th = this
5.40 +    have sq4: "\<And>x::real. x^2 / 4 = (x / 2) ^ 2"
5.41 +      by (simp add: power2_eq_square)
5.42 +    from th[of x y]
5.43 +    have sq4': "sqrt (((sqrt (x * x + y * y) + x)^2 / 4)) = (sqrt (x * x + y * y) + x) / 2" "sqrt (((sqrt (x * x + y * y) - x)^2 / 4)) = (sqrt (x * x + y * y) - x) / 2" unfolding sq4 by simp_all
5.44 +    then have th1: "sqrt ((sqrt (x * x + y * y) + x) * (sqrt (x * x + y * y) + x) / 4) - sqrt ((sqrt (x * x + y * y) - x) * (sqrt (x * x + y * y) - x) / 4) = x"
5.45 +      unfolding power2_eq_square by simp
5.46 +    have "sqrt 4 = sqrt (2^2)" by simp
5.47 +    hence sqrt4: "sqrt 4 = 2" by (simp only: real_sqrt_abs)
5.48 +    have th2: "2 *(y * sqrt ((sqrt (x * x + y * y) - x) * (sqrt (x * x + y * y) + x) / 4)) / \<bar>y\<bar> = y"
5.49 +      using iffD2[OF real_sqrt_pow2_iff sum_power2_ge_zero[of x y]] y0
5.50 +      unfolding power2_eq_square
5.51 +      by (simp add: algebra_simps real_sqrt_divide sqrt4)
5.52 +     from y0 xy have ?thesis  apply (simp add: csqrt_def power2_eq_square)
5.53 +       apply (simp add: real_sqrt_sum_squares_mult_ge_zero[of x y] real_sqrt_pow2[OF th(1)[of x y], unfolded power2_eq_square] real_sqrt_pow2[OF th(2)[of x y], unfolded power2_eq_square] real_sqrt_mult[symmetric])
5.54 +      using th1 th2  ..}
5.55 +  ultimately show ?thesis by blast
5.56 +qed
5.57 +
5.58 +
5.59 +subsection{* More lemmas about module of complex numbers *}
5.60 +
5.61 +lemma complex_of_real_power: "complex_of_real x ^ n = complex_of_real (x^n)"
5.62 +  by (rule of_real_power [symmetric])
5.63 +
5.64 +lemma real_down2: "(0::real) < d1 \<Longrightarrow> 0 < d2 ==> EX e. 0 < e & e < d1 & e < d2"
5.65 +  apply (rule exI[where x = "min d1 d2 / 2"])
5.66 +  by (simp add: field_simps min_def)
5.67 +
5.68 +text{* The triangle inequality for cmod *}
5.69 +lemma complex_mod_triangle_sub: "cmod w \<le> cmod (w + z) + norm z"
5.70 +  using complex_mod_triangle_ineq2[of "w + z" "-z"] by auto
5.71 +
5.72 +subsection{* Basic lemmas about complex polynomials *}
5.73 +
5.74 +lemma poly_bound_exists:
5.75 +  shows "\<exists>m. m > 0 \<and> (\<forall>z. cmod z <= r \<longrightarrow> cmod (poly p z) \<le> m)"
5.76 +proof(induct p)
5.77 +  case 0 thus ?case by (rule exI[where x=1], simp)
5.78 +next
5.79 +  case (pCons c cs)
5.80 +  from pCons.hyps obtain m where m: "\<forall>z. cmod z \<le> r \<longrightarrow> cmod (poly cs z) \<le> m"
5.81 +    by blast
5.82 +  let ?k = " 1 + cmod c + \<bar>r * m\<bar>"
5.83 +  have kp: "?k > 0" using abs_ge_zero[of "r*m"] norm_ge_zero[of c] by arith
5.84 +  {fix z
5.85 +    assume H: "cmod z \<le> r"
5.86 +    from m H have th: "cmod (poly cs z) \<le> m" by blast
5.87 +    from H have rp: "r \<ge> 0" using norm_ge_zero[of z] by arith
5.88 +    have "cmod (poly (pCons c cs) z) \<le> cmod c + cmod (z* poly cs z)"
5.89 +      using norm_triangle_ineq[of c "z* poly cs z"] by simp
5.90 +    also have "\<dots> \<le> cmod c + r*m" using mult_mono[OF H th rp norm_ge_zero[of "poly cs z"]] by (simp add: norm_mult)
5.91 +    also have "\<dots> \<le> ?k" by simp
5.92 +    finally have "cmod (poly (pCons c cs) z) \<le> ?k" .}
5.93 +  with kp show ?case by blast
5.94 +qed
5.95 +
5.96 +
5.97 +text{* Offsetting the variable in a polynomial gives another of same degree *}
5.98 +
5.99 +definition
5.100 +  "offset_poly p h = poly_rec 0 (\<lambda>a p q. smult h q + pCons a q) p"
5.101 +
5.102 +lemma offset_poly_0: "offset_poly 0 h = 0"
5.103 +  unfolding offset_poly_def by (simp add: poly_rec_0)
5.104 +
5.105 +lemma offset_poly_pCons:
5.106 +  "offset_poly (pCons a p) h =
5.107 +    smult h (offset_poly p h) + pCons a (offset_poly p h)"
5.108 +  unfolding offset_poly_def by (simp add: poly_rec_pCons)
5.109 +
5.110 +lemma offset_poly_single: "offset_poly [:a:] h = [:a:]"
5.111 +by (simp add: offset_poly_pCons offset_poly_0)
5.112 +
5.113 +lemma poly_offset_poly: "poly (offset_poly p h) x = poly p (h + x)"
5.114 +apply (induct p)
5.116 +apply (simp add: offset_poly_pCons algebra_simps)
5.117 +done
5.118 +
5.119 +lemma offset_poly_eq_0_lemma: "smult c p + pCons a p = 0 \<Longrightarrow> p = 0"
5.120 +by (induct p arbitrary: a, simp, force)
5.121 +
5.122 +lemma offset_poly_eq_0_iff: "offset_poly p h = 0 \<longleftrightarrow> p = 0"
5.123 +apply (safe intro!: offset_poly_0)
5.124 +apply (induct p, simp)
5.126 +apply (frule offset_poly_eq_0_lemma, simp)
5.127 +done
5.128 +
5.129 +lemma degree_offset_poly: "degree (offset_poly p h) = degree p"
5.130 +apply (induct p)
5.132 +apply (case_tac "p = 0")
5.133 +apply (simp add: offset_poly_0 offset_poly_pCons)
5.136 +apply (rule le_less_trans [OF degree_smult_le])
5.139 +done
5.140 +
5.141 +definition
5.142 +  "psize p = (if p = 0 then 0 else Suc (degree p))"
5.143 +
5.144 +lemma psize_eq_0_iff [simp]: "psize p = 0 \<longleftrightarrow> p = 0"
5.145 +  unfolding psize_def by simp
5.146 +
5.147 +lemma poly_offset: "\<exists> q. psize q = psize p \<and> (\<forall>x. poly q (x::complex) = poly p (a + x))"
5.148 +proof (intro exI conjI)
5.149 +  show "psize (offset_poly p a) = psize p"
5.150 +    unfolding psize_def
5.151 +    by (simp add: offset_poly_eq_0_iff degree_offset_poly)
5.152 +  show "\<forall>x. poly (offset_poly p a) x = poly p (a + x)"
5.153 +    by (simp add: poly_offset_poly)
5.154 +qed
5.155 +
5.156 +text{* An alternative useful formulation of completeness of the reals *}
5.157 +lemma real_sup_exists: assumes ex: "\<exists>x. P x" and bz: "\<exists>z. \<forall>x. P x \<longrightarrow> x < z"
5.158 +  shows "\<exists>(s::real). \<forall>y. (\<exists>x. P x \<and> y < x) \<longleftrightarrow> y < s"
5.159 +proof-
5.160 +  from ex bz obtain x Y where x: "P x" and Y: "\<And>x. P x \<Longrightarrow> x < Y"  by blast
5.161 +  from ex have thx:"\<exists>x. x \<in> Collect P" by blast
5.162 +  from bz have thY: "\<exists>Y. isUb UNIV (Collect P) Y"
5.163 +    by(auto simp add: isUb_def isLub_def setge_def setle_def leastP_def Ball_def order_le_less)
5.164 +  from reals_complete[OF thx thY] obtain L where L: "isLub UNIV (Collect P) L"
5.165 +    by blast
5.166 +  from Y[OF x] have xY: "x < Y" .
5.167 +  from L have L': "\<forall>x. P x \<longrightarrow> x \<le> L" by (auto simp add: isUb_def isLub_def setge_def setle_def leastP_def Ball_def)
5.168 +  from Y have Y': "\<forall>x. P x \<longrightarrow> x \<le> Y"
5.169 +    apply (clarsimp, atomize (full)) by auto
5.170 +  from L Y' have "L \<le> Y" by (auto simp add: isUb_def isLub_def setge_def setle_def leastP_def Ball_def)
5.171 +  {fix y
5.172 +    {fix z assume z: "P z" "y < z"
5.173 +      from L' z have "y < L" by auto }
5.174 +    moreover
5.175 +    {assume yL: "y < L" "\<forall>z. P z \<longrightarrow> \<not> y < z"
5.176 +      hence nox: "\<forall>z. P z \<longrightarrow> y \<ge> z" by auto
5.177 +      from nox L have "y \<ge> L" by (auto simp add: isUb_def isLub_def setge_def setle_def leastP_def Ball_def)
5.178 +      with yL(1) have False  by arith}
5.179 +    ultimately have "(\<exists>x. P x \<and> y < x) \<longleftrightarrow> y < L" by blast}
5.180 +  thus ?thesis by blast
5.181 +qed
5.182 +
5.183 +
5.184 +subsection{* Some theorems about Sequences*}
5.185 +text{* Given a binary function @{text "f:: nat \<Rightarrow> 'a \<Rightarrow> 'a"}, its values are uniquely determined by a function g *}
5.186 +
5.187 +lemma num_Axiom: "EX! g. g 0 = e \<and> (\<forall>n. g (Suc n) = f n (g n))"
5.188 +  unfolding Ex1_def
5.189 +  apply (rule_tac x="nat_rec e f" in exI)
5.190 +  apply (rule conjI)+
5.191 +apply (rule def_nat_rec_0, simp)
5.192 +apply (rule allI, rule def_nat_rec_Suc, simp)
5.193 +apply (rule allI, rule impI, rule ext)
5.194 +apply (erule conjE)
5.195 +apply (induct_tac x)
5.197 +apply (erule_tac x="n" in allE)
5.198 +apply (simp)
5.199 +done
5.200 +
5.201 +text{* for any sequence, there is a mootonic subsequence *}
5.202 +lemma seq_monosub: "\<exists>f. subseq f \<and> monoseq (\<lambda> n. (s (f n)))"
5.203 +proof-
5.204 +  {assume H: "\<forall>n. \<exists>p >n. \<forall> m\<ge>p. s m \<le> s p"
5.205 +    let ?P = "\<lambda> p n. p > n \<and> (\<forall>m \<ge> p. s m \<le> s p)"
5.206 +    from num_Axiom[of "SOME p. ?P p 0" "\<lambda>p n. SOME p. ?P p n"]
5.207 +    obtain f where f: "f 0 = (SOME p. ?P p 0)" "\<forall>n. f (Suc n) = (SOME p. ?P p (f n))" by blast
5.208 +    have "?P (f 0) 0"  unfolding f(1) some_eq_ex[of "\<lambda>p. ?P p 0"]
5.209 +      using H apply -
5.210 +      apply (erule allE[where x=0], erule exE, rule_tac x="p" in exI)
5.211 +      unfolding order_le_less by blast
5.212 +    hence f0: "f 0 > 0" "\<forall>m \<ge> f 0. s m \<le> s (f 0)" by blast+
5.213 +    {fix n
5.214 +      have "?P (f (Suc n)) (f n)"
5.215 +	unfolding f(2)[rule_format, of n] some_eq_ex[of "\<lambda>p. ?P p (f n)"]
5.216 +	using H apply -
5.217 +      apply (erule allE[where x="f n"], erule exE, rule_tac x="p" in exI)
5.218 +      unfolding order_le_less by blast
5.219 +    hence "f (Suc n) > f n" "\<forall>m \<ge> f (Suc n). s m \<le> s (f (Suc n))" by blast+}
5.220 +  note fSuc = this
5.221 +    {fix p q assume pq: "p \<ge> f q"
5.222 +      have "s p \<le> s(f(q))"  using f0(2)[rule_format, of p] pq fSuc
5.223 +	by (cases q, simp_all) }
5.224 +    note pqth = this
5.225 +    {fix q
5.226 +      have "f (Suc q) > f q" apply (induct q)
5.227 +	using f0(1) fSuc(1)[of 0] apply simp by (rule fSuc(1))}
5.228 +    note fss = this
5.229 +    from fss have th1: "subseq f" unfolding subseq_Suc_iff ..
5.230 +    {fix a b
5.231 +      have "f a \<le> f (a + b)"
5.232 +      proof(induct b)
5.233 +	case 0 thus ?case by simp
5.234 +      next
5.235 +	case (Suc b)
5.236 +	from fSuc(1)[of "a + b"] Suc.hyps show ?case by simp
5.237 +      qed}
5.238 +    note fmon0 = this
5.239 +    have "monoseq (\<lambda>n. s (f n))"
5.240 +    proof-
5.241 +      {fix n
5.242 +	have "s (f n) \<ge> s (f (Suc n))"
5.243 +	proof(cases n)
5.244 +	  case 0
5.245 +	  assume n0: "n = 0"
5.246 +	  from fSuc(1)[of 0] have th0: "f 0 \<le> f (Suc 0)" by simp
5.247 +	  from f0(2)[rule_format, OF th0] show ?thesis  using n0 by simp
5.248 +	next
5.249 +	  case (Suc m)
5.250 +	  assume m: "n = Suc m"
5.251 +	  from fSuc(1)[of n] m have th0: "f (Suc m) \<le> f (Suc (Suc m))" by simp
5.252 +	  from m fSuc(2)[rule_format, OF th0] show ?thesis by simp
5.253 +	qed}
5.254 +      thus "monoseq (\<lambda>n. s (f n))" unfolding monoseq_Suc by blast
5.255 +    qed
5.256 +    with th1 have ?thesis by blast}
5.257 +  moreover
5.258 +  {fix N assume N: "\<forall>p >N. \<exists> m\<ge>p. s m > s p"
5.259 +    {fix p assume p: "p \<ge> Suc N"
5.260 +      hence pN: "p > N" by arith with N obtain m where m: "m \<ge> p" "s m > s p" by blast
5.261 +      have "m \<noteq> p" using m(2) by auto
5.262 +      with m have "\<exists>m>p. s p < s m" by - (rule exI[where x=m], auto)}
5.263 +    note th0 = this
5.264 +    let ?P = "\<lambda>m x. m > x \<and> s x < s m"
5.265 +    from num_Axiom[of "SOME x. ?P x (Suc N)" "\<lambda>m x. SOME y. ?P y x"]
5.266 +    obtain f where f: "f 0 = (SOME x. ?P x (Suc N))"
5.267 +      "\<forall>n. f (Suc n) = (SOME m. ?P m (f n))" by blast
5.268 +    have "?P (f 0) (Suc N)"  unfolding f(1) some_eq_ex[of "\<lambda>p. ?P p (Suc N)"]
5.269 +      using N apply -
5.270 +      apply (erule allE[where x="Suc N"], clarsimp)
5.271 +      apply (rule_tac x="m" in exI)
5.272 +      apply auto
5.273 +      apply (subgoal_tac "Suc N \<noteq> m")
5.274 +      apply simp
5.275 +      apply (rule ccontr, simp)
5.276 +      done
5.277 +    hence f0: "f 0 > Suc N" "s (Suc N) < s (f 0)" by blast+
5.278 +    {fix n
5.279 +      have "f n > N \<and> ?P (f (Suc n)) (f n)"
5.280 +	unfolding f(2)[rule_format, of n] some_eq_ex[of "\<lambda>p. ?P p (f n)"]
5.281 +      proof (induct n)
5.282 +	case 0 thus ?case
5.283 +	  using f0 N apply auto
5.284 +	  apply (erule allE[where x="f 0"], clarsimp)
5.285 +	  apply (rule_tac x="m" in exI, simp)
5.286 +	  by (subgoal_tac "f 0 \<noteq> m", auto)
5.287 +      next
5.288 +	case (Suc n)
5.289 +	from Suc.hyps have Nfn: "N < f n" by blast
5.290 +	from Suc.hyps obtain m where m: "m > f n" "s (f n) < s m" by blast
5.291 +	with Nfn have mN: "m > N" by arith
5.292 +	note key = Suc.hyps[unfolded some_eq_ex[of "\<lambda>p. ?P p (f n)", symmetric] f(2)[rule_format, of n, symmetric]]
5.293 +
5.294 +	from key have th0: "f (Suc n) > N" by simp
5.295 +	from N[rule_format, OF th0]
5.296 +	obtain m' where m': "m' \<ge> f (Suc n)" "s (f (Suc n)) < s m'" by blast
5.297 +	have "m' \<noteq> f (Suc (n))" apply (rule ccontr) using m'(2) by auto
5.298 +	hence "m' > f (Suc n)" using m'(1) by simp
5.299 +	with key m'(2) show ?case by auto
5.300 +      qed}
5.301 +    note fSuc = this
5.302 +    {fix n
5.303 +      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
5.304 +      hence "f n \<ge> Suc N" "f(Suc n) > f n" "s(f n) < s(f(Suc n))" by blast+}
5.305 +    note thf = this
5.306 +    have sqf: "subseq f" unfolding subseq_Suc_iff using thf by simp
5.307 +    have "monoseq (\<lambda>n. s (f n))"  unfolding monoseq_Suc using thf
5.308 +      apply -
5.309 +      apply (rule disjI1)
5.310 +      apply auto
5.311 +      apply (rule order_less_imp_le)
5.312 +      apply blast
5.313 +      done
5.314 +    then have ?thesis  using sqf by blast}
5.315 +  ultimately show ?thesis unfolding linorder_not_less[symmetric] by blast
5.316 +qed
5.317 +
5.318 +lemma seq_suble: assumes sf: "subseq f" shows "n \<le> f n"
5.319 +proof(induct n)
5.320 +  case 0 thus ?case by simp
5.321 +next
5.322 +  case (Suc n)
5.323 +  from sf[unfolded subseq_Suc_iff, rule_format, of n] Suc.hyps
5.324 +  have "n < f (Suc n)" by arith
5.325 +  thus ?case by arith
5.326 +qed
5.327 +
5.328 +subsection {* Fundamental theorem of algebra *}
5.329 +lemma  unimodular_reduce_norm:
5.330 +  assumes md: "cmod z = 1"
5.331 +  shows "cmod (z + 1) < 1 \<or> cmod (z - 1) < 1 \<or> cmod (z + ii) < 1 \<or> cmod (z - ii) < 1"
5.332 +proof-
5.333 +  obtain x y where z: "z = Complex x y " by (cases z, auto)
5.334 +  from md z have xy: "x^2 + y^2 = 1" by (simp add: cmod_def)
5.335 +  {assume C: "cmod (z + 1) \<ge> 1" "cmod (z - 1) \<ge> 1" "cmod (z + ii) \<ge> 1" "cmod (z - ii) \<ge> 1"
5.336 +    from C z xy have "2*x \<le> 1" "2*x \<ge> -1" "2*y \<le> 1" "2*y \<ge> -1"
5.337 +      by (simp_all add: cmod_def power2_eq_square algebra_simps)
5.338 +    hence "abs (2*x) \<le> 1" "abs (2*y) \<le> 1" by simp_all
5.339 +    hence "(abs (2 * x))^2 <= 1^2" "(abs (2 * y)) ^2 <= 1^2"
5.340 +      by - (rule power_mono, simp, simp)+
5.341 +    hence th0: "4*x^2 \<le> 1" "4*y^2 \<le> 1"
5.342 +      by (simp_all  add: power2_abs power_mult_distrib)
5.343 +    from add_mono[OF th0] xy have False by simp }
5.344 +  thus ?thesis unfolding linorder_not_le[symmetric] by blast
5.345 +qed
5.346 +
5.347 +text{* Hence we can always reduce modulus of @{text "1 + b z^n"} if nonzero *}
5.348 +lemma reduce_poly_simple:
5.349 + assumes b: "b \<noteq> 0" and n: "n\<noteq>0"
5.350 +  shows "\<exists>z. cmod (1 + b * z^n) < 1"
5.351 +using n
5.352 +proof(induct n rule: nat_less_induct)
5.353 +  fix n
5.354 +  assume IH: "\<forall>m<n. m \<noteq> 0 \<longrightarrow> (\<exists>z. cmod (1 + b * z ^ m) < 1)" and n: "n \<noteq> 0"
5.355 +  let ?P = "\<lambda>z n. cmod (1 + b * z ^ n) < 1"
5.356 +  {assume e: "even n"
5.357 +    hence "\<exists>m. n = 2*m" by presburger
5.358 +    then obtain m where m: "n = 2*m" by blast
5.359 +    from n m have "m\<noteq>0" "m < n" by presburger+
5.360 +    with IH[rule_format, of m] obtain z where z: "?P z m" by blast
5.361 +    from z have "?P (csqrt z) n" by (simp add: m power_mult csqrt)
5.362 +    hence "\<exists>z. ?P z n" ..}
5.363 +  moreover
5.364 +  {assume o: "odd n"
5.365 +    from b have b': "b^2 \<noteq> 0" unfolding power2_eq_square by simp
5.366 +    have "Im (inverse b) * (Im (inverse b) * \<bar>Im b * Im b + Re b * Re b\<bar>) +
5.367 +    Re (inverse b) * (Re (inverse b) * \<bar>Im b * Im b + Re b * Re b\<bar>) =
5.368 +    ((Re (inverse b))^2 + (Im (inverse b))^2) * \<bar>Im b * Im b + Re b * Re b\<bar>" by algebra
5.369 +    also have "\<dots> = cmod (inverse b) ^2 * cmod b ^ 2"
5.370 +      apply (simp add: cmod_def) using realpow_two_le_add_order[of "Re b" "Im b"]
5.371 +      by (simp add: power2_eq_square)
5.372 +    finally
5.373 +    have th0: "Im (inverse b) * (Im (inverse b) * \<bar>Im b * Im b + Re b * Re b\<bar>) +
5.374 +    Re (inverse b) * (Re (inverse b) * \<bar>Im b * Im b + Re b * Re b\<bar>) =
5.375 +    1"
5.376 +      apply (simp add: power2_eq_square norm_mult[symmetric] norm_inverse[symmetric])
5.377 +      using right_inverse[OF b']
5.378 +      by (simp add: power2_eq_square[symmetric] power_inverse[symmetric] algebra_simps)
5.379 +    have th0: "cmod (complex_of_real (cmod b) / b) = 1"
5.380 +      apply (simp add: complex_Re_mult cmod_def power2_eq_square Re_complex_of_real Im_complex_of_real divide_inverse algebra_simps )
5.381 +      by (simp add: real_sqrt_mult[symmetric] th0)
5.382 +    from o have "\<exists>m. n = Suc (2*m)" by presburger+
5.383 +    then obtain m where m: "n = Suc (2*m)" by blast
5.384 +    from unimodular_reduce_norm[OF th0] o
5.385 +    have "\<exists>v. cmod (complex_of_real (cmod b) / b + v^n) < 1"
5.386 +      apply (cases "cmod (complex_of_real (cmod b) / b + 1) < 1", rule_tac x="1" in exI, simp)
5.387 +      apply (cases "cmod (complex_of_real (cmod b) / b - 1) < 1", rule_tac x="-1" in exI, simp add: diff_def)
5.388 +      apply (cases "cmod (complex_of_real (cmod b) / b + ii) < 1")
5.389 +      apply (cases "even m", rule_tac x="ii" in exI, simp add: m power_mult)
5.390 +      apply (rule_tac x="- ii" in exI, simp add: m power_mult)
5.391 +      apply (cases "even m", rule_tac x="- ii" in exI, simp add: m power_mult diff_def)
5.392 +      apply (rule_tac x="ii" in exI, simp add: m power_mult diff_def)
5.393 +      done
5.394 +    then obtain v where v: "cmod (complex_of_real (cmod b) / b + v^n) < 1" by blast
5.395 +    let ?w = "v / complex_of_real (root n (cmod b))"
5.396 +    from odd_real_root_pow[OF o, of "cmod b"]
5.397 +    have th1: "?w ^ n = v^n / complex_of_real (cmod b)"
5.398 +      by (simp add: power_divide complex_of_real_power)
5.399 +    have th2:"cmod (complex_of_real (cmod b) / b) = 1" using b by (simp add: norm_divide)
5.400 +    hence th3: "cmod (complex_of_real (cmod b) / b) \<ge> 0" by simp
5.401 +    have th4: "cmod (complex_of_real (cmod b) / b) *
5.402 +   cmod (1 + b * (v ^ n / complex_of_real (cmod b)))
5.403 +   < cmod (complex_of_real (cmod b) / b) * 1"
5.404 +      apply (simp only: norm_mult[symmetric] right_distrib)
5.405 +      using b v by (simp add: th2)
5.406 +
5.407 +    from mult_less_imp_less_left[OF th4 th3]
5.408 +    have "?P ?w n" unfolding th1 .
5.409 +    hence "\<exists>z. ?P z n" .. }
5.410 +  ultimately show "\<exists>z. ?P z n" by blast
5.411 +qed
5.412 +
5.413 +
5.414 +text{* Bolzano-Weierstrass type property for closed disc in complex plane. *}
5.415 +
5.416 +lemma metric_bound_lemma: "cmod (x - y) <= \<bar>Re x - Re y\<bar> + \<bar>Im x - Im y\<bar>"
5.417 +  using real_sqrt_sum_squares_triangle_ineq[of "Re x - Re y" 0 0 "Im x - Im y" ]
5.418 +  unfolding cmod_def by simp
5.419 +
5.420 +lemma bolzano_weierstrass_complex_disc:
5.421 +  assumes r: "\<forall>n. cmod (s n) \<le> r"
5.422 +  shows "\<exists>f z. subseq f \<and> (\<forall>e >0. \<exists>N. \<forall>n \<ge> N. cmod (s (f n) - z) < e)"
5.423 +proof-
5.424 +  from seq_monosub[of "Re o s"]
5.425 +  obtain f g where f: "subseq f" "monoseq (\<lambda>n. Re (s (f n)))"
5.426 +    unfolding o_def by blast
5.427 +  from seq_monosub[of "Im o s o f"]
5.428 +  obtain g where g: "subseq g" "monoseq (\<lambda>n. Im (s(f(g n))))" unfolding o_def by blast
5.429 +  let ?h = "f o g"
5.430 +  from r[rule_format, of 0] have rp: "r \<ge> 0" using norm_ge_zero[of "s 0"] by arith
5.431 +  have th:"\<forall>n. r + 1 \<ge> \<bar> Re (s n)\<bar>"
5.432 +  proof
5.433 +    fix n
5.434 +    from abs_Re_le_cmod[of "s n"] r[rule_format, of n]  show "\<bar>Re (s n)\<bar> \<le> r + 1" by arith
5.435 +  qed
5.436 +  have conv1: "convergent (\<lambda>n. Re (s ( f n)))"
5.437 +    apply (rule Bseq_monoseq_convergent)
5.438 +    apply (simp add: Bseq_def)
5.439 +    apply (rule exI[where x= "r + 1"])
5.440 +    using th rp apply simp
5.441 +    using f(2) .
5.442 +  have th:"\<forall>n. r + 1 \<ge> \<bar> Im (s n)\<bar>"
5.443 +  proof
5.444 +    fix n
5.445 +    from abs_Im_le_cmod[of "s n"] r[rule_format, of n]  show "\<bar>Im (s n)\<bar> \<le> r + 1" by arith
5.446 +  qed
5.447 +
5.448 +  have conv2: "convergent (\<lambda>n. Im (s (f (g n))))"
5.449 +    apply (rule Bseq_monoseq_convergent)
5.450 +    apply (simp add: Bseq_def)
5.451 +    apply (rule exI[where x= "r + 1"])
5.452 +    using th rp apply simp
5.453 +    using g(2) .
5.454 +
5.455 +  from conv1[unfolded convergent_def] obtain x where "LIMSEQ (\<lambda>n. Re (s (f n))) x"
5.456 +    by blast
5.457 +  hence  x: "\<forall>r>0. \<exists>n0. \<forall>n\<ge>n0. \<bar> Re (s (f n)) - x \<bar> < r"
5.458 +    unfolding LIMSEQ_def real_norm_def .
5.459 +
5.460 +  from conv2[unfolded convergent_def] obtain y where "LIMSEQ (\<lambda>n. Im (s (f (g n)))) y"
5.461 +    by blast
5.462 +  hence  y: "\<forall>r>0. \<exists>n0. \<forall>n\<ge>n0. \<bar> Im (s (f (g n))) - y \<bar> < r"
5.463 +    unfolding LIMSEQ_def real_norm_def .
5.464 +  let ?w = "Complex x y"
5.465 +  from f(1) g(1) have hs: "subseq ?h" unfolding subseq_def by auto
5.466 +  {fix e assume ep: "e > (0::real)"
5.467 +    hence e2: "e/2 > 0" by simp
5.468 +    from x[rule_format, OF e2] y[rule_format, OF e2]
5.469 +    obtain N1 N2 where N1: "\<forall>n\<ge>N1. \<bar>Re (s (f n)) - x\<bar> < e / 2" and N2: "\<forall>n\<ge>N2. \<bar>Im (s (f (g n))) - y\<bar> < e / 2" by blast
5.470 +    {fix n assume nN12: "n \<ge> N1 + N2"
5.471 +      hence nN1: "g n \<ge> N1" and nN2: "n \<ge> N2" using seq_suble[OF g(1), of n] by arith+
5.472 +      from add_strict_mono[OF N1[rule_format, OF nN1] N2[rule_format, OF nN2]]
5.473 +      have "cmod (s (?h n) - ?w) < e"
5.474 +	using metric_bound_lemma[of "s (f (g n))" ?w] by simp }
5.475 +    hence "\<exists>N. \<forall>n\<ge>N. cmod (s (?h n) - ?w) < e" by blast }
5.476 +  with hs show ?thesis  by blast
5.477 +qed
5.478 +
5.479 +text{* Polynomial is continuous. *}
5.480 +
5.481 +lemma poly_cont:
5.482 +  assumes ep: "e > 0"
5.483 +  shows "\<exists>d >0. \<forall>w. 0 < cmod (w - z) \<and> cmod (w - z) < d \<longrightarrow> cmod (poly p w - poly p z) < e"
5.484 +proof-
5.485 +  obtain q where q: "degree q = degree p" "\<And>x. poly q x = poly p (z + x)"
5.486 +  proof
5.487 +    show "degree (offset_poly p z) = degree p"
5.488 +      by (rule degree_offset_poly)
5.489 +    show "\<And>x. poly (offset_poly p z) x = poly p (z + x)"
5.490 +      by (rule poly_offset_poly)
5.491 +  qed
5.492 +  {fix w
5.493 +    note q(2)[of "w - z", simplified]}
5.494 +  note th = this
5.495 +  show ?thesis unfolding th[symmetric]
5.496 +  proof(induct q)
5.497 +    case 0 thus ?case  using ep by auto
5.498 +  next
5.499 +    case (pCons c cs)
5.500 +    from poly_bound_exists[of 1 "cs"]
5.501 +    obtain m where m: "m > 0" "\<And>z. cmod z \<le> 1 \<Longrightarrow> cmod (poly cs z) \<le> m" by blast
5.502 +    from ep m(1) have em0: "e/m > 0" by (simp add: field_simps)
5.503 +    have one0: "1 > (0::real)"  by arith
5.504 +    from real_lbound_gt_zero[OF one0 em0]
5.505 +    obtain d where d: "d >0" "d < 1" "d < e / m" by blast
5.506 +    from d(1,3) m(1) have dm: "d*m > 0" "d*m < e"
5.507 +      by (simp_all add: field_simps real_mult_order)
5.508 +    show ?case
5.509 +      proof(rule ex_forward[OF real_lbound_gt_zero[OF one0 em0]], clarsimp simp add: norm_mult)
5.510 +	fix d w
5.511 +	assume H: "d > 0" "d < 1" "d < e/m" "w\<noteq>z" "cmod (w-z) < d"
5.512 +	hence d1: "cmod (w-z) \<le> 1" "d \<ge> 0" by simp_all
5.513 +	from H(3) m(1) have dme: "d*m < e" by (simp add: field_simps)
5.514 +	from H have th: "cmod (w-z) \<le> d" by simp
5.515 +	from mult_mono[OF th m(2)[OF d1(1)] d1(2) norm_ge_zero] dme
5.516 +	show "cmod (w - z) * cmod (poly cs (w - z)) < e" by simp
5.517 +      qed
5.518 +    qed
5.519 +qed
5.520 +
5.521 +text{* Hence a polynomial attains minimum on a closed disc
5.522 +  in the complex plane. *}
5.523 +lemma  poly_minimum_modulus_disc:
5.524 +  "\<exists>z. \<forall>w. cmod w \<le> r \<longrightarrow> cmod (poly p z) \<le> cmod (poly p w)"
5.525 +proof-
5.526 +  {assume "\<not> r \<ge> 0" hence ?thesis unfolding linorder_not_le
5.527 +      apply -
5.528 +      apply (rule exI[where x=0])
5.529 +      apply auto
5.530 +      apply (subgoal_tac "cmod w < 0")
5.531 +      apply simp
5.532 +      apply arith
5.533 +      done }
5.534 +  moreover
5.535 +  {assume rp: "r \<ge> 0"
5.536 +    from rp have "cmod 0 \<le> r \<and> cmod (poly p 0) = - (- cmod (poly p 0))" by simp
5.537 +    hence mth1: "\<exists>x z. cmod z \<le> r \<and> cmod (poly p z) = - x"  by blast
5.538 +    {fix x z
5.539 +      assume H: "cmod z \<le> r" "cmod (poly p z) = - x" "\<not>x < 1"
5.540 +      hence "- x < 0 " by arith
5.541 +      with H(2) norm_ge_zero[of "poly p z"]  have False by simp }
5.542 +    then have mth2: "\<exists>z. \<forall>x. (\<exists>z. cmod z \<le> r \<and> cmod (poly p z) = - x) \<longrightarrow> x < z" by blast
5.543 +    from real_sup_exists[OF mth1 mth2] obtain s where
5.544 +      s: "\<forall>y. (\<exists>x. (\<exists>z. cmod z \<le> r \<and> cmod (poly p z) = - x) \<and> y < x) \<longleftrightarrow>(y < s)" by blast
5.545 +    let ?m = "-s"
5.546 +    {fix y
5.547 +      from s[rule_format, of "-y"] have
5.548 +    "(\<exists>z x. cmod z \<le> r \<and> -(- cmod (poly p z)) < y) \<longleftrightarrow> ?m < y"
5.549 +	unfolding minus_less_iff[of y ] equation_minus_iff by blast }
5.550 +    note s1 = this[unfolded minus_minus]
5.551 +    from s1[of ?m] have s1m: "\<And>z x. cmod z \<le> r \<Longrightarrow> cmod (poly p z) \<ge> ?m"
5.552 +      by auto
5.553 +    {fix n::nat
5.554 +      from s1[rule_format, of "?m + 1/real (Suc n)"]
5.555 +      have "\<exists>z. cmod z \<le> r \<and> cmod (poly p z) < - s + 1 / real (Suc n)"
5.556 +	by simp}
5.557 +    hence th: "\<forall>n. \<exists>z. cmod z \<le> r \<and> cmod (poly p z) < - s + 1 / real (Suc n)" ..
5.558 +    from choice[OF th] obtain g where
5.559 +      g: "\<forall>n. cmod (g n) \<le> r" "\<forall>n. cmod (poly p (g n)) <?m+1 /real(Suc n)"
5.560 +      by blast
5.561 +    from bolzano_weierstrass_complex_disc[OF g(1)]
5.562 +    obtain f z where fz: "subseq f" "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. cmod (g (f n) - z) < e"
5.563 +      by blast
5.564 +    {fix w
5.565 +      assume wr: "cmod w \<le> r"
5.566 +      let ?e = "\<bar>cmod (poly p z) - ?m\<bar>"
5.567 +      {assume e: "?e > 0"
5.568 +	hence e2: "?e/2 > 0" by simp
5.569 +	from poly_cont[OF e2, of z p] obtain d where
5.570 +	  d: "d>0" "\<forall>w. 0<cmod (w - z)\<and> cmod(w - z) < d \<longrightarrow> cmod(poly p w - poly p z) < ?e/2" by blast
5.571 +	{fix w assume w: "cmod (w - z) < d"
5.572 +	  have "cmod(poly p w - poly p z) < ?e / 2"
5.573 +	    using d(2)[rule_format, of w] w e by (cases "w=z", simp_all)}
5.574 +	note th1 = this
5.575 +
5.576 +	from fz(2)[rule_format, OF d(1)] obtain N1 where
5.577 +	  N1: "\<forall>n\<ge>N1. cmod (g (f n) - z) < d" by blast
5.578 +	from reals_Archimedean2[of "2/?e"] obtain N2::nat where
5.579 +	  N2: "2/?e < real N2" by blast
5.580 +	have th2: "cmod(poly p (g(f(N1 + N2))) - poly p z) < ?e/2"
5.581 +	  using N1[rule_format, of "N1 + N2"] th1 by simp
5.582 +	{fix a b e2 m :: real
5.583 +	have "a < e2 \<Longrightarrow> abs(b - m) < e2 \<Longrightarrow> 2 * e2 <= abs(b - m) + a
5.584 +          ==> False" by arith}
5.585 +      note th0 = this
5.586 +      have ath:
5.587 +	"\<And>m x e. m <= x \<Longrightarrow>  x < m + e ==> abs(x - m::real) < e" by arith
5.588 +      from s1m[OF g(1)[rule_format]]
5.589 +      have th31: "?m \<le> cmod(poly p (g (f (N1 + N2))))" .
5.590 +      from seq_suble[OF fz(1), of "N1+N2"]
5.591 +      have th00: "real (Suc (N1+N2)) \<le> real (Suc (f (N1+N2)))" by simp
5.592 +      have th000: "0 \<le> (1::real)" "(1::real) \<le> 1" "real (Suc (N1+N2)) > 0"
5.593 +	using N2 by auto
5.594 +      from frac_le[OF th000 th00] have th00: "?m +1 / real (Suc (f (N1 + N2))) \<le> ?m + 1 / real (Suc (N1 + N2))" by simp
5.595 +      from g(2)[rule_format, of "f (N1 + N2)"]
5.596 +      have th01:"cmod (poly p (g (f (N1 + N2)))) < - s + 1 / real (Suc (f (N1 + N2)))" .
5.597 +      from order_less_le_trans[OF th01 th00]
5.598 +      have th32: "cmod(poly p (g (f (N1 + N2)))) < ?m + (1/ real(Suc (N1 + N2)))" .
5.599 +      from N2 have "2/?e < real (Suc (N1 + N2))" by arith
5.600 +      with e2 less_imp_inverse_less[of "2/?e" "real (Suc (N1 + N2))"]
5.601 +      have "?e/2 > 1/ real (Suc (N1 + N2))" by (simp add: inverse_eq_divide)
5.602 +      with ath[OF th31 th32]
5.603 +      have thc1:"\<bar>cmod(poly p (g (f (N1 + N2)))) - ?m\<bar>< ?e/2" by arith
5.604 +      have ath2: "\<And>(a::real) b c m. \<bar>a - b\<bar> <= c ==> \<bar>b - m\<bar> <= \<bar>a - m\<bar> + c"
5.605 +	by arith
5.606 +      have th22: "\<bar>cmod (poly p (g (f (N1 + N2)))) - cmod (poly p z)\<bar>
5.607 +\<le> cmod (poly p (g (f (N1 + N2))) - poly p z)"
5.608 +	by (simp add: norm_triangle_ineq3)
5.609 +      from ath2[OF th22, of ?m]
5.610 +      have thc2: "2*(?e/2) \<le> \<bar>cmod(poly p (g (f (N1 + N2)))) - ?m\<bar> + cmod (poly p (g (f (N1 + N2))) - poly p z)" by simp
5.611 +      from th0[OF th2 thc1 thc2] have False .}
5.612 +      hence "?e = 0" by auto
5.613 +      then have "cmod (poly p z) = ?m" by simp
5.614 +      with s1m[OF wr]
5.615 +      have "cmod (poly p z) \<le> cmod (poly p w)" by simp }
5.616 +    hence ?thesis by blast}
5.617 +  ultimately show ?thesis by blast
5.618 +qed
5.619 +
5.620 +lemma "(rcis (sqrt (abs r)) (a/2)) ^ 2 = rcis (abs r) a"
5.621 +  unfolding power2_eq_square
5.622 +  apply (simp add: rcis_mult)
5.623 +  apply (simp add: power2_eq_square[symmetric])
5.624 +  done
5.625 +
5.626 +lemma cispi: "cis pi = -1"
5.627 +  unfolding cis_def
5.628 +  by simp
5.629 +
5.630 +lemma "(rcis (sqrt (abs r)) ((pi + a)/2)) ^ 2 = rcis (- abs r) a"
5.631 +  unfolding power2_eq_square
5.633 +  apply (simp add: power2_eq_square[symmetric] rcis_def cispi cis_mult[symmetric])
5.634 +  done
5.635 +
5.636 +text {* Nonzero polynomial in z goes to infinity as z does. *}
5.637 +
5.638 +lemma poly_infinity:
5.639 +  assumes ex: "p \<noteq> 0"
5.640 +  shows "\<exists>r. \<forall>z. r \<le> cmod z \<longrightarrow> d \<le> cmod (poly (pCons a p) z)"
5.641 +using ex
5.642 +proof(induct p arbitrary: a d)
5.643 +  case (pCons c cs a d)
5.644 +  {assume H: "cs \<noteq> 0"
5.645 +    with pCons.hyps obtain r where r: "\<forall>z. r \<le> cmod z \<longrightarrow> d + cmod a \<le> cmod (poly (pCons c cs) z)" by blast
5.646 +    let ?r = "1 + \<bar>r\<bar>"
5.647 +    {fix z assume h: "1 + \<bar>r\<bar> \<le> cmod z"
5.648 +      have r0: "r \<le> cmod z" using h by arith
5.649 +      from r[rule_format, OF r0]
5.650 +      have th0: "d + cmod a \<le> 1 * cmod(poly (pCons c cs) z)" by arith
5.651 +      from h have z1: "cmod z \<ge> 1" by arith
5.652 +      from order_trans[OF th0 mult_right_mono[OF z1 norm_ge_zero[of "poly (pCons c cs) z"]]]
5.653 +      have th1: "d \<le> cmod(z * poly (pCons c cs) z) - cmod a"
5.654 +	unfolding norm_mult by (simp add: algebra_simps)
5.655 +      from complex_mod_triangle_sub[of "z * poly (pCons c cs) z" a]
5.656 +      have th2: "cmod(z * poly (pCons c cs) z) - cmod a \<le> cmod (poly (pCons a (pCons c cs)) z)"
5.657 +	by (simp add: diff_le_eq algebra_simps)
5.658 +      from th1 th2 have "d \<le> cmod (poly (pCons a (pCons c cs)) z)"  by arith}
5.659 +    hence ?case by blast}
5.660 +  moreover
5.661 +  {assume cs0: "\<not> (cs \<noteq> 0)"
5.662 +    with pCons.prems have c0: "c \<noteq> 0" by simp
5.663 +    from cs0 have cs0': "cs = 0" by simp
5.664 +    {fix z
5.665 +      assume h: "(\<bar>d\<bar> + cmod a) / cmod c \<le> cmod z"
5.666 +      from c0 have "cmod c > 0" by simp
5.667 +      from h c0 have th0: "\<bar>d\<bar> + cmod a \<le> cmod (z*c)"
5.668 +	by (simp add: field_simps norm_mult)
5.669 +      have ath: "\<And>mzh mazh ma. mzh <= mazh + ma ==> abs(d) + ma <= mzh ==> d <= mazh" by arith
5.670 +      from complex_mod_triangle_sub[of "z*c" a ]
5.671 +      have th1: "cmod (z * c) \<le> cmod (a + z * c) + cmod a"
5.672 +	by (simp add: algebra_simps)
5.673 +      from ath[OF th1 th0] have "d \<le> cmod (poly (pCons a (pCons c cs)) z)"
5.674 +        using cs0' by simp}
5.675 +    then have ?case  by blast}
5.676 +  ultimately show ?case by blast
5.677 +qed simp
5.678 +
5.679 +text {* Hence polynomial's modulus attains its minimum somewhere. *}
5.680 +lemma poly_minimum_modulus:
5.681 +  "\<exists>z.\<forall>w. cmod (poly p z) \<le> cmod (poly p w)"
5.682 +proof(induct p)
5.683 +  case (pCons c cs)
5.684 +  {assume cs0: "cs \<noteq> 0"
5.685 +    from poly_infinity[OF cs0, of "cmod (poly (pCons c cs) 0)" c]
5.686 +    obtain r where r: "\<And>z. r \<le> cmod z \<Longrightarrow> cmod (poly (pCons c cs) 0) \<le> cmod (poly (pCons c cs) z)" by blast
5.687 +    have ath: "\<And>z r. r \<le> cmod z \<or> cmod z \<le> \<bar>r\<bar>" by arith
5.688 +    from poly_minimum_modulus_disc[of "\<bar>r\<bar>" "pCons c cs"]
5.689 +    obtain v where v: "\<And>w. cmod w \<le> \<bar>r\<bar> \<Longrightarrow> cmod (poly (pCons c cs) v) \<le> cmod (poly (pCons c cs) w)" by blast
5.690 +    {fix z assume z: "r \<le> cmod z"
5.691 +      from v[of 0] r[OF z]
5.692 +      have "cmod (poly (pCons c cs) v) \<le> cmod (poly (pCons c cs) z)"
5.693 +	by simp }
5.694 +    note v0 = this
5.695 +    from v0 v ath[of r] have ?case by blast}
5.696 +  moreover
5.697 +  {assume cs0: "\<not> (cs \<noteq> 0)"
5.698 +    hence th:"cs = 0" by simp
5.699 +    from th pCons.hyps have ?case by simp}
5.700 +  ultimately show ?case by blast
5.701 +qed simp
5.702 +
5.703 +text{* Constant function (non-syntactic characterization). *}
5.704 +definition "constant f = (\<forall>x y. f x = f y)"
5.705 +
5.706 +lemma nonconstant_length: "\<not> (constant (poly p)) \<Longrightarrow> psize p \<ge> 2"
5.707 +  unfolding constant_def psize_def
5.708 +  apply (induct p, auto)
5.709 +  done
5.710 +
5.711 +lemma poly_replicate_append:
5.712 +  "poly (monom 1 n * p) (x::'a::{recpower, comm_ring_1}) = x^n * poly p x"
5.713 +  by (simp add: poly_monom)
5.714 +
5.715 +text {* Decomposition of polynomial, skipping zero coefficients
5.716 +  after the first.  *}
5.717 +
5.718 +lemma poly_decompose_lemma:
5.719 + assumes nz: "\<not>(\<forall>z. z\<noteq>0 \<longrightarrow> poly p z = (0::'a::{recpower,idom}))"
5.720 +  shows "\<exists>k a q. a\<noteq>0 \<and> Suc (psize q + k) = psize p \<and>
5.721 +                 (\<forall>z. poly p z = z^k * poly (pCons a q) z)"
5.722 +unfolding psize_def
5.723 +using nz
5.724 +proof(induct p)
5.725 +  case 0 thus ?case by simp
5.726 +next
5.727 +  case (pCons c cs)
5.728 +  {assume c0: "c = 0"
5.729 +    from pCons.hyps pCons.prems c0 have ?case apply auto
5.730 +      apply (rule_tac x="k+1" in exI)
5.731 +      apply (rule_tac x="a" in exI, clarsimp)
5.732 +      apply (rule_tac x="q" in exI)
5.733 +      by (auto simp add: power_Suc)}
5.734 +  moreover
5.735 +  {assume c0: "c\<noteq>0"
5.736 +    hence ?case apply-
5.737 +      apply (rule exI[where x=0])
5.738 +      apply (rule exI[where x=c], clarsimp)
5.739 +      apply (rule exI[where x=cs])
5.740 +      apply auto
5.741 +      done}
5.742 +  ultimately show ?case by blast
5.743 +qed
5.744 +
5.745 +lemma poly_decompose:
5.746 +  assumes nc: "~constant(poly p)"
5.747 +  shows "\<exists>k a q. a\<noteq>(0::'a::{recpower,idom}) \<and> k\<noteq>0 \<and>
5.748 +               psize q + k + 1 = psize p \<and>
5.749 +              (\<forall>z. poly p z = poly p 0 + z^k * poly (pCons a q) z)"
5.750 +using nc
5.751 +proof(induct p)
5.752 +  case 0 thus ?case by (simp add: constant_def)
5.753 +next
5.754 +  case (pCons c cs)
5.755 +  {assume C:"\<forall>z. z \<noteq> 0 \<longrightarrow> poly cs z = 0"
5.756 +    {fix x y
5.757 +      from C have "poly (pCons c cs) x = poly (pCons c cs) y" by (cases "x=0", auto)}
5.758 +    with pCons.prems have False by (auto simp add: constant_def)}
5.759 +  hence th: "\<not> (\<forall>z. z \<noteq> 0 \<longrightarrow> poly cs z = 0)" ..
5.760 +  from poly_decompose_lemma[OF th]
5.761 +  show ?case
5.762 +    apply clarsimp
5.763 +    apply (rule_tac x="k+1" in exI)
5.764 +    apply (rule_tac x="a" in exI)
5.765 +    apply simp
5.766 +    apply (rule_tac x="q" in exI)
5.767 +    apply (auto simp add: power_Suc)
5.768 +    apply (auto simp add: psize_def split: if_splits)
5.769 +    done
5.770 +qed
5.771 +
5.772 +text{* Fundamental theorem of algebral *}
5.773 +
5.774 +lemma fundamental_theorem_of_algebra:
5.775 +  assumes nc: "~constant(poly p)"
5.776 +  shows "\<exists>z::complex. poly p z = 0"
5.777 +using nc
5.778 +proof(induct n\<equiv> "psize p" arbitrary: p rule: nat_less_induct)
5.779 +  fix n fix p :: "complex poly"
5.780 +  let ?p = "poly p"
5.781 +  assume H: "\<forall>m<n. \<forall>p. \<not> constant (poly p) \<longrightarrow> m = psize p \<longrightarrow> (\<exists>(z::complex). poly p z = 0)" and nc: "\<not> constant ?p" and n: "n = psize p"
5.782 +  let ?ths = "\<exists>z. ?p z = 0"
5.783 +
5.784 +  from nonconstant_length[OF nc] have n2: "n\<ge> 2" by (simp add: n)
5.785 +  from poly_minimum_modulus obtain c where
5.786 +    c: "\<forall>w. cmod (?p c) \<le> cmod (?p w)" by blast
5.787 +  {assume pc: "?p c = 0" hence ?ths by blast}
5.788 +  moreover
5.789 +  {assume pc0: "?p c \<noteq> 0"
5.790 +    from poly_offset[of p c] obtain q where
5.791 +      q: "psize q = psize p" "\<forall>x. poly q x = ?p (c+x)" by blast
5.792 +    {assume h: "constant (poly q)"
5.793 +      from q(2) have th: "\<forall>x. poly q (x - c) = ?p x" by auto
5.794 +      {fix x y
5.795 +	from th have "?p x = poly q (x - c)" by auto
5.796 +	also have "\<dots> = poly q (y - c)"
5.797 +	  using h unfolding constant_def by blast
5.798 +	also have "\<dots> = ?p y" using th by auto
5.799 +	finally have "?p x = ?p y" .}
5.800 +      with nc have False unfolding constant_def by blast }
5.801 +    hence qnc: "\<not> constant (poly q)" by blast
5.802 +    from q(2) have pqc0: "?p c = poly q 0" by simp
5.803 +    from c pqc0 have cq0: "\<forall>w. cmod (poly q 0) \<le> cmod (?p w)" by simp
5.804 +    let ?a0 = "poly q 0"
5.805 +    from pc0 pqc0 have a00: "?a0 \<noteq> 0" by simp
5.806 +    from a00
5.807 +    have qr: "\<forall>z. poly q z = poly (smult (inverse ?a0) q) z * ?a0"
5.808 +      by simp
5.809 +    let ?r = "smult (inverse ?a0) q"
5.810 +    have lgqr: "psize q = psize ?r"
5.811 +      using a00 unfolding psize_def degree_def
5.812 +      by (simp add: expand_poly_eq)
5.813 +    {assume h: "\<And>x y. poly ?r x = poly ?r y"
5.814 +      {fix x y
5.815 +	from qr[rule_format, of x]
5.816 +	have "poly q x = poly ?r x * ?a0" by auto
5.817 +	also have "\<dots> = poly ?r y * ?a0" using h by simp
5.818 +	also have "\<dots> = poly q y" using qr[rule_format, of y] by simp
5.819 +	finally have "poly q x = poly q y" .}
5.820 +      with qnc have False unfolding constant_def by blast}
5.821 +    hence rnc: "\<not> constant (poly ?r)" unfolding constant_def by blast
5.822 +    from qr[rule_format, of 0] a00  have r01: "poly ?r 0 = 1" by auto
5.823 +    {fix w
5.824 +      have "cmod (poly ?r w) < 1 \<longleftrightarrow> cmod (poly q w / ?a0) < 1"
5.825 +	using qr[rule_format, of w] a00 by (simp add: divide_inverse mult_ac)
5.826 +      also have "\<dots> \<longleftrightarrow> cmod (poly q w) < cmod ?a0"
5.827 +	using a00 unfolding norm_divide by (simp add: field_simps)
5.828 +      finally have "cmod (poly ?r w) < 1 \<longleftrightarrow> cmod (poly q w) < cmod ?a0" .}
5.829 +    note mrmq_eq = this
5.830 +    from poly_decompose[OF rnc] obtain k a s where
5.831 +      kas: "a\<noteq>0" "k\<noteq>0" "psize s + k + 1 = psize ?r"
5.832 +      "\<forall>z. poly ?r z = poly ?r 0 + z^k* poly (pCons a s) z" by blast
5.833 +    {assume "k + 1 = n"
5.834 +      with kas(3) lgqr[symmetric] q(1) n[symmetric] have s0:"s=0" by auto
5.835 +      {fix w
5.836 +	have "cmod (poly ?r w) = cmod (1 + a * w ^ k)"
5.837 +	  using kas(4)[rule_format, of w] s0 r01 by (simp add: algebra_simps)}
5.838 +      note hth = this [symmetric]
5.839 +	from reduce_poly_simple[OF kas(1,2)]
5.840 +      have "\<exists>w. cmod (poly ?r w) < 1" unfolding hth by blast}
5.841 +    moreover
5.842 +    {assume kn: "k+1 \<noteq> n"
5.843 +      from kn kas(3) q(1) n[symmetric] lgqr have k1n: "k + 1 < n" by simp
5.844 +      have th01: "\<not> constant (poly (pCons 1 (monom a (k - 1))))"
5.845 +	unfolding constant_def poly_pCons poly_monom
5.846 +	using kas(1) apply simp
5.847 +	by (rule exI[where x=0], rule exI[where x=1], simp)
5.848 +      from kas(1) kas(2) have th02: "k+1 = psize (pCons 1 (monom a (k - 1)))"
5.849 +	by (simp add: psize_def degree_monom_eq)
5.850 +      from H[rule_format, OF k1n th01 th02]
5.851 +      obtain w where w: "1 + w^k * a = 0"
5.852 +	unfolding poly_pCons poly_monom
5.853 +	using kas(2) by (cases k, auto simp add: algebra_simps)
5.854 +      from poly_bound_exists[of "cmod w" s] obtain m where
5.855 +	m: "m > 0" "\<forall>z. cmod z \<le> cmod w \<longrightarrow> cmod (poly s z) \<le> m" by blast
5.856 +      have w0: "w\<noteq>0" using kas(2) w by (auto simp add: power_0_left)
5.857 +      from w have "(1 + w ^ k * a) - 1 = 0 - 1" by simp
5.858 +      then have wm1: "w^k * a = - 1" by simp
5.859 +      have inv0: "0 < inverse (cmod w ^ (k + 1) * m)"
5.860 +	using norm_ge_zero[of w] w0 m(1)
5.861 +	  by (simp add: inverse_eq_divide zero_less_mult_iff)
5.862 +      with real_down2[OF zero_less_one] obtain t where
5.863 +	t: "t > 0" "t < 1" "t < inverse (cmod w ^ (k + 1) * m)" by blast
5.864 +      let ?ct = "complex_of_real t"
5.865 +      let ?w = "?ct * w"
5.866 +      have "1 + ?w^k * (a + ?w * poly s ?w) = 1 + ?ct^k * (w^k * a) + ?w^k * ?w * poly s ?w" using kas(1) by (simp add: algebra_simps power_mult_distrib)
5.867 +      also have "\<dots> = complex_of_real (1 - t^k) + ?w^k * ?w * poly s ?w"
5.868 +	unfolding wm1 by (simp)
5.869 +      finally have "cmod (1 + ?w^k * (a + ?w * poly s ?w)) = cmod (complex_of_real (1 - t^k) + ?w^k * ?w * poly s ?w)"
5.870 +	apply -
5.871 +	apply (rule cong[OF refl[of cmod]])
5.872 +	apply assumption
5.873 +	done
5.874 +      with norm_triangle_ineq[of "complex_of_real (1 - t^k)" "?w^k * ?w * poly s ?w"]
5.875 +      have th11: "cmod (1 + ?w^k * (a + ?w * poly s ?w)) \<le> \<bar>1 - t^k\<bar> + cmod (?w^k * ?w * poly s ?w)" unfolding norm_of_real by simp
5.876 +      have ath: "\<And>x (t::real). 0\<le> x \<Longrightarrow> x < t \<Longrightarrow> t\<le>1 \<Longrightarrow> \<bar>1 - t\<bar> + x < 1" by arith
5.877 +      have "t *cmod w \<le> 1 * cmod w" apply (rule mult_mono) using t(1,2) by auto
5.878 +      then have tw: "cmod ?w \<le> cmod w" using t(1) by (simp add: norm_mult)
5.879 +      from t inv0 have "t* (cmod w ^ (k + 1) * m) < 1"
5.880 +	by (simp add: inverse_eq_divide field_simps)
5.881 +      with zero_less_power[OF t(1), of k]
5.882 +      have th30: "t^k * (t* (cmod w ^ (k + 1) * m)) < t^k * 1"
5.883 +	apply - apply (rule mult_strict_left_mono) by simp_all
5.884 +      have "cmod (?w^k * ?w * poly s ?w) = t^k * (t* (cmod w ^ (k+1) * cmod (poly s ?w)))"  using w0 t(1)
5.885 +	by (simp add: algebra_simps power_mult_distrib norm_of_real norm_power norm_mult)
5.886 +      then have "cmod (?w^k * ?w * poly s ?w) \<le> t^k * (t* (cmod w ^ (k + 1) * m))"
5.887 +	using t(1,2) m(2)[rule_format, OF tw] w0
5.888 +	apply (simp only: )
5.889 +	apply auto
5.890 +	apply (rule mult_mono, simp_all add: norm_ge_zero)+
5.891 +	apply (simp add: zero_le_mult_iff zero_le_power)
5.892 +	done
5.893 +      with th30 have th120: "cmod (?w^k * ?w * poly s ?w) < t^k" by simp
5.894 +      from power_strict_mono[OF t(2), of k] t(1) kas(2) have th121: "t^k \<le> 1"
5.895 +	by auto
5.896 +      from ath[OF norm_ge_zero[of "?w^k * ?w * poly s ?w"] th120 th121]
5.897 +      have th12: "\<bar>1 - t^k\<bar> + cmod (?w^k * ?w * poly s ?w) < 1" .
5.898 +      from th11 th12
5.899 +      have "cmod (1 + ?w^k * (a + ?w * poly s ?w)) < 1"  by arith
5.900 +      then have "cmod (poly ?r ?w) < 1"
5.901 +	unfolding kas(4)[rule_format, of ?w] r01 by simp
5.902 +      then have "\<exists>w. cmod (poly ?r w) < 1" by blast}
5.903 +    ultimately have cr0_contr: "\<exists>w. cmod (poly ?r w) < 1" by blast
5.904 +    from cr0_contr cq0 q(2)
5.905 +    have ?ths unfolding mrmq_eq not_less[symmetric] by auto}
5.906 +  ultimately show ?ths by blast
5.907 +qed
5.908 +
5.909 +text {* Alternative version with a syntactic notion of constant polynomial. *}
5.910 +
5.911 +lemma fundamental_theorem_of_algebra_alt:
5.912 +  assumes nc: "~(\<exists>a l. a\<noteq> 0 \<and> l = 0 \<and> p = pCons a l)"
5.913 +  shows "\<exists>z. poly p z = (0::complex)"
5.914 +using nc
5.915 +proof(induct p)
5.916 +  case (pCons c cs)
5.917 +  {assume "c=0" hence ?case by auto}
5.918 +  moreover
5.919 +  {assume c0: "c\<noteq>0"
5.920 +    {assume nc: "constant (poly (pCons c cs))"
5.921 +      from nc[unfolded constant_def, rule_format, of 0]
5.922 +      have "\<forall>w. w \<noteq> 0 \<longrightarrow> poly cs w = 0" by auto
5.923 +      hence "cs = 0"
5.924 +	proof(induct cs)
5.925 +	  case (pCons d ds)
5.926 +	  {assume "d=0" hence ?case using pCons.prems pCons.hyps by simp}
5.927 +	  moreover
5.928 +	  {assume d0: "d\<noteq>0"
5.929 +	    from poly_bound_exists[of 1 ds] obtain m where
5.930 +	      m: "m > 0" "\<forall>z. \<forall>z. cmod z \<le> 1 \<longrightarrow> cmod (poly ds z) \<le> m" by blast
5.931 +	    have dm: "cmod d / m > 0" using d0 m(1) by (simp add: field_simps)
5.932 +	    from real_down2[OF dm zero_less_one] obtain x where
5.933 +	      x: "x > 0" "x < cmod d / m" "x < 1" by blast
5.934 +	    let ?x = "complex_of_real x"
5.935 +	    from x have cx: "?x \<noteq> 0"  "cmod ?x \<le> 1" by simp_all
5.936 +	    from pCons.prems[rule_format, OF cx(1)]
5.937 +	    have cth: "cmod (?x*poly ds ?x) = cmod d" by (simp add: eq_diff_eq[symmetric])
5.938 +	    from m(2)[rule_format, OF cx(2)] x(1)
5.939 +	    have th0: "cmod (?x*poly ds ?x) \<le> x*m"
5.940 +	      by (simp add: norm_mult)
5.941 +	    from x(2) m(1) have "x*m < cmod d" by (simp add: field_simps)
5.942 +	    with th0 have "cmod (?x*poly ds ?x) \<noteq> cmod d" by auto
5.943 +	    with cth  have ?case by blast}
5.944 +	  ultimately show ?case by blast
5.945 +	qed simp}
5.946 +      then have nc: "\<not> constant (poly (pCons c cs))" using pCons.prems c0
5.947 +	by blast
5.948 +      from fundamental_theorem_of_algebra[OF nc] have ?case .}
5.949 +  ultimately show ?case by blast
5.950 +qed simp
5.951 +
5.952 +subsection {* Order of polynomial roots *}
5.953 +
5.954 +definition
5.955 +  order :: "'a::{idom,recpower} \<Rightarrow> 'a poly \<Rightarrow> nat"
5.956 +where
5.957 +  [code del]:
5.958 +  "order a p = (LEAST n. \<not> [:-a, 1:] ^ Suc n dvd p)"
5.959 +
5.960 +lemma degree_power_le: "degree (p ^ n) \<le> degree p * n"
5.961 +by (induct n, simp, auto intro: order_trans degree_mult_le)
5.962 +
5.963 +lemma coeff_linear_power:
5.964 +  fixes a :: "'a::{comm_semiring_1,recpower}"
5.965 +  shows "coeff ([:a, 1:] ^ n) n = 1"
5.966 +apply (induct n, simp_all)
5.967 +apply (subst coeff_eq_0)
5.968 +apply (auto intro: le_less_trans degree_power_le)
5.969 +done
5.970 +
5.971 +lemma degree_linear_power:
5.972 +  fixes a :: "'a::{comm_semiring_1,recpower}"
5.973 +  shows "degree ([:a, 1:] ^ n) = n"
5.974 +apply (rule order_antisym)
5.975 +apply (rule ord_le_eq_trans [OF degree_power_le], simp)
5.976 +apply (rule le_degree, simp add: coeff_linear_power)
5.977 +done
5.978 +
5.979 +lemma order_1: "[:-a, 1:] ^ order a p dvd p"
5.980 +apply (cases "p = 0", simp)
5.981 +apply (cases "order a p", simp)
5.982 +apply (subgoal_tac "nat < (LEAST n. \<not> [:-a, 1:] ^ Suc n dvd p)")
5.983 +apply (drule not_less_Least, simp)
5.984 +apply (fold order_def, simp)
5.985 +done
5.986 +
5.987 +lemma order_2: "p \<noteq> 0 \<Longrightarrow> \<not> [:-a, 1:] ^ Suc (order a p) dvd p"
5.988 +unfolding order_def
5.989 +apply (rule LeastI_ex)
5.990 +apply (rule_tac x="degree p" in exI)
5.991 +apply (rule notI)
5.992 +apply (drule (1) dvd_imp_degree_le)
5.993 +apply (simp only: degree_linear_power)
5.994 +done
5.995 +
5.996 +lemma order:
5.997 +  "p \<noteq> 0 \<Longrightarrow> [:-a, 1:] ^ order a p dvd p \<and> \<not> [:-a, 1:] ^ Suc (order a p) dvd p"
5.998 +by (rule conjI [OF order_1 order_2])
5.999 +
5.1000 +lemma order_degree:
5.1001 +  assumes p: "p \<noteq> 0"
5.1002 +  shows "order a p \<le> degree p"
5.1003 +proof -
5.1004 +  have "order a p = degree ([:-a, 1:] ^ order a p)"
5.1005 +    by (simp only: degree_linear_power)
5.1006 +  also have "\<dots> \<le> degree p"
5.1007 +    using order_1 p by (rule dvd_imp_degree_le)
5.1008 +  finally show ?thesis .
5.1009 +qed
5.1010 +
5.1011 +lemma order_root: "poly p a = 0 \<longleftrightarrow> p = 0 \<or> order a p \<noteq> 0"
5.1012 +apply (cases "p = 0", simp_all)
5.1013 +apply (rule iffI)
5.1014 +apply (rule ccontr, simp)
5.1015 +apply (frule order_2 [where a=a], simp)
5.1018 +apply (simp only: order_def)
5.1019 +apply (drule not_less_Least, simp)
5.1020 +done
5.1021 +
5.1022 +lemma poly_zero:
5.1023 +  fixes p :: "'a::{idom,ring_char_0} poly"
5.1024 +  shows "poly p = poly 0 \<longleftrightarrow> p = 0"
5.1025 +apply (cases "p = 0", simp_all)
5.1026 +apply (drule poly_roots_finite)
5.1027 +apply (auto simp add: infinite_UNIV_char_0)
5.1028 +done
5.1029 +
5.1030 +lemma poly_eq_iff:
5.1031 +  fixes p q :: "'a::{idom,ring_char_0} poly"
5.1032 +  shows "poly p = poly q \<longleftrightarrow> p = q"
5.1033 +  using poly_zero [of "p - q"]
5.1034 +  by (simp add: expand_fun_eq)
5.1035 +
5.1036 +
5.1037 +subsection{* Nullstellenstatz, degrees and divisibility of polynomials *}
5.1038 +
5.1039 +lemma nullstellensatz_lemma:
5.1040 +  fixes p :: "complex poly"
5.1041 +  assumes "\<forall>x. poly p x = 0 \<longrightarrow> poly q x = 0"
5.1042 +  and "degree p = n" and "n \<noteq> 0"
5.1043 +  shows "p dvd (q ^ n)"
5.1044 +using prems
5.1045 +proof(induct n arbitrary: p q rule: nat_less_induct)
5.1046 +  fix n::nat fix p q :: "complex poly"
5.1047 +  assume IH: "\<forall>m<n. \<forall>p q.
5.1048 +                 (\<forall>x. poly p x = (0::complex) \<longrightarrow> poly q x = 0) \<longrightarrow>
5.1049 +                 degree p = m \<longrightarrow> m \<noteq> 0 \<longrightarrow> p dvd (q ^ m)"
5.1050 +    and pq0: "\<forall>x. poly p x = 0 \<longrightarrow> poly q x = 0"
5.1051 +    and dpn: "degree p = n" and n0: "n \<noteq> 0"
5.1052 +  from dpn n0 have pne: "p \<noteq> 0" by auto
5.1053 +  let ?ths = "p dvd (q ^ n)"
5.1054 +  {fix a assume a: "poly p a = 0"
5.1055 +    {assume oa: "order a p \<noteq> 0"
5.1056 +      let ?op = "order a p"
5.1057 +      from pne have ap: "([:- a, 1:] ^ ?op) dvd p"
5.1058 +	"\<not> [:- a, 1:] ^ (Suc ?op) dvd p" using order by blast+
5.1059 +      note oop = order_degree[OF pne, unfolded dpn]
5.1060 +      {assume q0: "q = 0"
5.1061 +	hence ?ths using n0
5.1062 +          by (simp add: power_0_left)}
5.1063 +      moreover
5.1064 +      {assume q0: "q \<noteq> 0"
5.1065 +	from pq0[rule_format, OF a, unfolded poly_eq_0_iff_dvd]
5.1066 +	obtain r where r: "q = [:- a, 1:] * r" by (rule dvdE)
5.1067 +	from ap(1) obtain s where
5.1068 +	  s: "p = [:- a, 1:] ^ ?op * s" by (rule dvdE)
5.1069 +	have sne: "s \<noteq> 0"
5.1070 +	  using s pne by auto
5.1071 +	{assume ds0: "degree s = 0"
5.1072 +	  from ds0 have "\<exists>k. s = [:k:]"
5.1073 +            by (cases s, simp split: if_splits)
5.1074 +	  then obtain k where kpn: "s = [:k:]" by blast
5.1075 +          from sne kpn have k: "k \<noteq> 0" by simp
5.1076 +	  let ?w = "([:1/k:] * ([:-a,1:] ^ (n - ?op))) * (r ^ n)"
5.1077 +          from k oop [of a] have "q ^ n = p * ?w"
5.1078 +            apply -
5.1079 +            apply (subst r, subst s, subst kpn)
5.1080 +            apply (subst power_mult_distrib, simp)
5.1081 +            apply (subst power_add [symmetric], simp)
5.1082 +            done
5.1083 +	  hence ?ths unfolding dvd_def by blast}
5.1084 +	moreover
5.1085 +	{assume ds0: "degree s \<noteq> 0"
5.1086 +	  from ds0 sne dpn s oa
5.1087 +	    have dsn: "degree s < n" apply auto
5.1088 +              apply (erule ssubst)
5.1089 +              apply (simp add: degree_mult_eq degree_linear_power)
5.1090 +              done
5.1091 +	    {fix x assume h: "poly s x = 0"
5.1092 +	      {assume xa: "x = a"
5.1093 +		from h[unfolded xa poly_eq_0_iff_dvd] obtain u where
5.1094 +		  u: "s = [:- a, 1:] * u" by (rule dvdE)
5.1095 +		have "p = [:- a, 1:] ^ (Suc ?op) * u"
5.1096 +                  by (subst s, subst u, simp only: power_Suc mult_ac)
5.1097 +		with ap(2)[unfolded dvd_def] have False by blast}
5.1098 +	      note xa = this
5.1099 +	      from h have "poly p x = 0" by (subst s, simp)
5.1100 +	      with pq0 have "poly q x = 0" by blast
5.1101 +	      with r xa have "poly r x = 0"
5.1103 +	    note impth = this
5.1104 +	    from IH[rule_format, OF dsn, of s r] impth ds0
5.1105 +	    have "s dvd (r ^ (degree s))" by blast
5.1106 +	    then obtain u where u: "r ^ (degree s) = s * u" ..
5.1107 +	    hence u': "\<And>x. poly s x * poly u x = poly r x ^ degree s"
5.1108 +              by (simp only: poly_mult[symmetric] poly_power[symmetric])
5.1109 +	    let ?w = "(u * ([:-a,1:] ^ (n - ?op))) * (r ^ (n - degree s))"
5.1110 +	    from oop[of a] dsn have "q ^ n = p * ?w"
5.1111 +              apply -
5.1112 +              apply (subst s, subst r)
5.1113 +              apply (simp only: power_mult_distrib)
5.1114 +              apply (subst mult_assoc [where b=s])
5.1115 +              apply (subst mult_assoc [where a=u])
5.1116 +              apply (subst mult_assoc [where b=u, symmetric])
5.1117 +              apply (subst u [symmetric])
5.1119 +              done
5.1120 +	    hence ?ths unfolding dvd_def by blast}
5.1121 +      ultimately have ?ths by blast }
5.1122 +      ultimately have ?ths by blast}
5.1123 +    then have ?ths using a order_root pne by blast}
5.1124 +  moreover
5.1125 +  {assume exa: "\<not> (\<exists>a. poly p a = 0)"
5.1126 +    from fundamental_theorem_of_algebra_alt[of p] exa obtain c where
5.1127 +      ccs: "c\<noteq>0" "p = pCons c 0" by blast
5.1128 +
5.1129 +    then have pp: "\<And>x. poly p x =  c" by simp
5.1130 +    let ?w = "[:1/c:] * (q ^ n)"
5.1131 +    from ccs
5.1132 +    have "(q ^ n) = (p * ?w) "
5.1133 +      by (simp add: smult_smult)
5.1134 +    hence ?ths unfolding dvd_def by blast}
5.1135 +  ultimately show ?ths by blast
5.1136 +qed
5.1137 +
5.1138 +lemma nullstellensatz_univariate:
5.1139 +  "(\<forall>x. poly p x = (0::complex) \<longrightarrow> poly q x = 0) \<longleftrightarrow>
5.1140 +    p dvd (q ^ (degree p)) \<or> (p = 0 \<and> q = 0)"
5.1141 +proof-
5.1142 +  {assume pe: "p = 0"
5.1143 +    hence eq: "(\<forall>x. poly p x = (0::complex) \<longrightarrow> poly q x = 0) \<longleftrightarrow> q = 0"
5.1144 +      apply auto
5.1145 +      apply (rule poly_zero [THEN iffD1])
5.1146 +      by (rule ext, simp)
5.1147 +    {assume "p dvd (q ^ (degree p))"
5.1148 +      then obtain r where r: "q ^ (degree p) = p * r" ..
5.1149 +      from r pe have False by simp}
5.1150 +    with eq pe have ?thesis by blast}
5.1151 +  moreover
5.1152 +  {assume pe: "p \<noteq> 0"
5.1153 +    {assume dp: "degree p = 0"
5.1154 +      then obtain k where k: "p = [:k:]" "k\<noteq>0" using pe
5.1155 +        by (cases p, simp split: if_splits)
5.1156 +      hence th1: "\<forall>x. poly p x \<noteq> 0" by simp
5.1157 +      from k dp have "q ^ (degree p) = p * [:1/k:]"
5.1158 +        by (simp add: one_poly_def)
5.1159 +      hence th2: "p dvd (q ^ (degree p))" ..
5.1160 +      from th1 th2 pe have ?thesis by blast}
5.1161 +    moreover
5.1162 +    {assume dp: "degree p \<noteq> 0"
5.1163 +      then obtain n where n: "degree p = Suc n " by (cases "degree p", auto)
5.1164 +      {assume "p dvd (q ^ (Suc n))"
5.1165 +	then obtain u where u: "q ^ (Suc n) = p * u" ..
5.1166 +	{fix x assume h: "poly p x = 0" "poly q x \<noteq> 0"
5.1167 +	  hence "poly (q ^ (Suc n)) x \<noteq> 0" by simp
5.1168 +	  hence False using u h(1) by (simp only: poly_mult) simp}}
5.1169 +	with n nullstellensatz_lemma[of p q "degree p"] dp
5.1170 +	have ?thesis by auto}
5.1171 +    ultimately have ?thesis by blast}
5.1172 +  ultimately show ?thesis by blast
5.1173 +qed
5.1174 +
5.1175 +text{* Useful lemma *}
5.1176 +
5.1177 +lemma constant_degree:
5.1178 +  fixes p :: "'a::{idom,ring_char_0} poly"
5.1179 +  shows "constant (poly p) \<longleftrightarrow> degree p = 0" (is "?lhs = ?rhs")
5.1180 +proof
5.1181 +  assume l: ?lhs
5.1182 +  from l[unfolded constant_def, rule_format, of _ "0"]
5.1183 +  have th: "poly p = poly [:poly p 0:]" apply - by (rule ext, simp)
5.1184 +  then have "p = [:poly p 0:]" by (simp add: poly_eq_iff)
5.1185 +  then have "degree p = degree [:poly p 0:]" by simp
5.1186 +  then show ?rhs by simp
5.1187 +next
5.1188 +  assume r: ?rhs
5.1189 +  then obtain k where "p = [:k:]"
5.1190 +    by (cases p, simp split: if_splits)
5.1191 +  then show ?lhs unfolding constant_def by auto
5.1192 +qed
5.1193 +
5.1194 +lemma divides_degree: assumes pq: "p dvd (q:: complex poly)"
5.1195 +  shows "degree p \<le> degree q \<or> q = 0"
5.1196 +apply (cases "q = 0", simp_all)
5.1197 +apply (erule dvd_imp_degree_le [OF pq])
5.1198 +done
5.1199 +
5.1200 +(* Arithmetic operations on multivariate polynomials.                        *)
5.1201 +
5.1202 +lemma mpoly_base_conv:
5.1203 +  "(0::complex) \<equiv> poly 0 x" "c \<equiv> poly [:c:] x" "x \<equiv> poly [:0,1:] x" by simp_all
5.1204 +
5.1205 +lemma mpoly_norm_conv:
5.1206 +  "poly [:0:] (x::complex) \<equiv> poly 0 x" "poly [:poly 0 y:] x \<equiv> poly 0 x" by simp_all
5.1207 +
5.1208 +lemma mpoly_sub_conv:
5.1209 +  "poly p (x::complex) - poly q x \<equiv> poly p x + -1 * poly q x"
5.1210 +  by (simp add: diff_def)
5.1211 +
5.1212 +lemma poly_pad_rule: "poly p x = 0 ==> poly (pCons 0 p) x = (0::complex)" by simp
5.1213 +
5.1214 +lemma poly_cancel_eq_conv: "p = (0::complex) \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> (q = 0) \<equiv> (a * q - b * p = 0)" apply (atomize (full)) by auto
5.1215 +
5.1216 +lemma resolve_eq_raw:  "poly 0 x \<equiv> 0" "poly [:c:] x \<equiv> (c::complex)" by auto
5.1217 +lemma  resolve_eq_then: "(P \<Longrightarrow> (Q \<equiv> Q1)) \<Longrightarrow> (\<not>P \<Longrightarrow> (Q \<equiv> Q2))
5.1218 +  \<Longrightarrow> Q \<equiv> P \<and> Q1 \<or> \<not>P\<and> Q2" apply (atomize (full)) by blast
5.1219 +
5.1221 +  fixes p q :: "complex poly"
5.1222 +  assumes pq: "p dvd q"
5.1223 +  shows "p dvd (pCons (0::complex) q)"
5.1224 +proof-
5.1225 +  have "pCons 0 q = q * [:0,1:]" by simp
5.1226 +  then have "q dvd (pCons 0 q)" ..
5.1227 +  with pq show ?thesis by (rule dvd_trans)
5.1228 +qed
5.1229 +
5.1231 +  fixes p q :: "complex poly"
5.1232 +  assumes pq: "p dvd q"
5.1233 +  shows "p dvd (smult a q)"
5.1234 +proof-
5.1235 +  have "smult a q = q * [:a:]" by simp
5.1236 +  then have "q dvd smult a q" ..
5.1237 +  with pq show ?thesis by (rule dvd_trans)
5.1238 +qed
5.1239 +
5.1240 +
5.1241 +lemma poly_divides_conv0:
5.1242 +  fixes p :: "complex poly"
5.1243 +  assumes lgpq: "degree q < degree p" and lq:"p \<noteq> 0"
5.1244 +  shows "p dvd q \<equiv> q = 0" (is "?lhs \<equiv> ?rhs")
5.1245 +proof-
5.1246 +  {assume r: ?rhs
5.1247 +    hence "q = p * 0" by simp
5.1248 +    hence ?lhs ..}
5.1249 +  moreover
5.1250 +  {assume l: ?lhs
5.1251 +    {assume q0: "q = 0"
5.1252 +      hence ?rhs by simp}
5.1253 +    moreover
5.1254 +    {assume q0: "q \<noteq> 0"
5.1255 +      from l q0 have "degree p \<le> degree q"
5.1256 +        by (rule dvd_imp_degree_le)
5.1257 +      with lgpq have ?rhs by simp }
5.1258 +    ultimately have ?rhs by blast }
5.1259 +  ultimately show "?lhs \<equiv> ?rhs" by - (atomize (full), blast)
5.1260 +qed
5.1261 +
5.1262 +lemma poly_divides_conv1:
5.1263 +  assumes a0: "a\<noteq> (0::complex)" and pp': "(p::complex poly) dvd p'"
5.1264 +  and qrp': "smult a q - p' \<equiv> r"
5.1265 +  shows "p dvd q \<equiv> p dvd (r::complex poly)" (is "?lhs \<equiv> ?rhs")
5.1266 +proof-
5.1267 +  {
5.1268 +  from pp' obtain t where t: "p' = p * t" ..
5.1269 +  {assume l: ?lhs
5.1270 +    then obtain u where u: "q = p * u" ..
5.1271 +     have "r = p * (smult a u - t)"
5.1272 +       using u qrp' [symmetric] t by (simp add: algebra_simps mult_smult_right)
5.1273 +     then have ?rhs ..}
5.1274 +  moreover
5.1275 +  {assume r: ?rhs
5.1276 +    then obtain u where u: "r = p * u" ..
5.1277 +    from u [symmetric] t qrp' [symmetric] a0
5.1278 +    have "q = p * smult (1/a) (u + t)"
5.1279 +      by (simp add: algebra_simps mult_smult_right smult_smult)
5.1280 +    hence ?lhs ..}
5.1281 +  ultimately have "?lhs = ?rhs" by blast }
5.1282 +thus "?lhs \<equiv> ?rhs"  by - (atomize(full), blast)
5.1283 +qed
5.1284 +
5.1285 +lemma basic_cqe_conv1:
5.1286 +  "(\<exists>x. poly p x = 0 \<and> poly 0 x \<noteq> 0) \<equiv> False"
5.1287 +  "(\<exists>x. poly 0 x \<noteq> 0) \<equiv> False"
5.1288 +  "(\<exists>x. poly [:c:] x \<noteq> 0) \<equiv> c\<noteq>0"
5.1289 +  "(\<exists>x. poly 0 x = 0) \<equiv> True"
5.1290 +  "(\<exists>x. poly [:c:] x = 0) \<equiv> c = 0" by simp_all
5.1291 +
5.1292 +lemma basic_cqe_conv2:
5.1293 +  assumes l:"p \<noteq> 0"
5.1294 +  shows "(\<exists>x. poly (pCons a (pCons b p)) x = (0::complex)) \<equiv> True"
5.1295 +proof-
5.1296 +  {fix h t
5.1297 +    assume h: "h\<noteq>0" "t=0"  "pCons a (pCons b p) = pCons h t"
5.1298 +    with l have False by simp}
5.1299 +  hence th: "\<not> (\<exists> h t. h\<noteq>0 \<and> t=0 \<and> pCons a (pCons b p) = pCons h t)"
5.1300 +    by blast
5.1301 +  from fundamental_theorem_of_algebra_alt[OF th]
5.1302 +  show "(\<exists>x. poly (pCons a (pCons b p)) x = (0::complex)) \<equiv> True" by auto
5.1303 +qed
5.1304 +
5.1305 +lemma  basic_cqe_conv_2b: "(\<exists>x. poly p x \<noteq> (0::complex)) \<equiv> (p \<noteq> 0)"
5.1306 +proof-
5.1307 +  have "p = 0 \<longleftrightarrow> poly p = poly 0"
5.1308 +    by (simp add: poly_zero)
5.1309 +  also have "\<dots> \<longleftrightarrow> (\<not> (\<exists>x. poly p x \<noteq> 0))" by (auto intro: ext)
5.1310 +  finally show "(\<exists>x. poly p x \<noteq> (0::complex)) \<equiv> p \<noteq> 0"
5.1311 +    by - (atomize (full), blast)
5.1312 +qed
5.1313 +
5.1314 +lemma basic_cqe_conv3:
5.1315 +  fixes p q :: "complex poly"
5.1316 +  assumes l: "p \<noteq> 0"
5.1317 +  shows "(\<exists>x. poly (pCons a p) x = 0 \<and> poly q x \<noteq> 0) \<equiv> \<not> ((pCons a p) dvd (q ^ (psize p)))"
5.1318 +proof-
5.1319 +  from l have dp:"degree (pCons a p) = psize p" by (simp add: psize_def)
5.1320 +  from nullstellensatz_univariate[of "pCons a p" q] l
5.1321 +  show "(\<exists>x. poly (pCons a p) x = 0 \<and> poly q x \<noteq> 0) \<equiv> \<not> ((pCons a p) dvd (q ^ (psize p)))"
5.1322 +    unfolding dp
5.1323 +    by - (atomize (full), auto)
5.1324 +qed
5.1325 +
5.1326 +lemma basic_cqe_conv4:
5.1327 +  fixes p q :: "complex poly"
5.1328 +  assumes h: "\<And>x. poly (q ^ n) x \<equiv> poly r x"
5.1329 +  shows "p dvd (q ^ n) \<equiv> p dvd r"
5.1330 +proof-
5.1331 +  from h have "poly (q ^ n) = poly r" by (auto intro: ext)
5.1332 +  then have "(q ^ n) = r" by (simp add: poly_eq_iff)
5.1333 +  thus "p dvd (q ^ n) \<equiv> p dvd r" by simp
5.1334 +qed
5.1335 +
5.1336 +lemma pmult_Cons_Cons: "(pCons (a::complex) (pCons b p) * q = (smult a q) + (pCons 0 (pCons b p * q)))"
5.1337 +  by simp
5.1338 +
5.1339 +lemma elim_neg_conv: "- z \<equiv> (-1) * (z::complex)" by simp
5.1340 +lemma eqT_intr: "PROP P \<Longrightarrow> (True \<Longrightarrow> PROP P )" "PROP P \<Longrightarrow> True" by blast+
5.1341 +lemma negate_negate_rule: "Trueprop P \<equiv> \<not> P \<equiv> False" by (atomize (full), auto)
5.1342 +
5.1343 +lemma complex_entire: "(z::complex) \<noteq> 0 \<and> w \<noteq> 0 \<equiv> z*w \<noteq> 0" by simp
5.1344 +lemma resolve_eq_ne: "(P \<equiv> True) \<equiv> (\<not>P \<equiv> False)" "(P \<equiv> False) \<equiv> (\<not>P \<equiv> True)"
5.1345 +  by (atomize (full)) simp_all
5.1346 +lemma cqe_conv1: "poly 0 x = 0 \<longleftrightarrow> True"  by simp
5.1347 +lemma cqe_conv2: "(p \<Longrightarrow> (q \<equiv> r)) \<equiv> ((p \<and> q) \<equiv> (p \<and> r))"  (is "?l \<equiv> ?r")
5.1348 +proof
5.1349 +  assume "p \<Longrightarrow> q \<equiv> r" thus "p \<and> q \<equiv> p \<and> r" apply - apply (atomize (full)) by blast
5.1350 +next
5.1351 +  assume "p \<and> q \<equiv> p \<and> r" "p"
5.1352 +  thus "q \<equiv> r" apply - apply (atomize (full)) apply blast done
5.1353 +qed
5.1354 +lemma poly_const_conv: "poly [:c:] (x::complex) = y \<longleftrightarrow> c = y" by simp
5.1355 +
5.1356 +end
```
```     6.1 --- a/src/HOL/Library/Library.thy	Wed Feb 11 11:22:42 2009 -0800
6.2 +++ b/src/HOL/Library/Library.thy	Thu Feb 12 18:14:43 2009 +0100
6.3 @@ -23,6 +23,7 @@
6.4    Float
6.5    Formal_Power_Series
6.6    FuncSet
6.7 +  Fundamental_Theorem_Algebra
6.8    Infinite_Set
6.9    ListVector
6.10    Mapping
```
```     7.1 --- a/src/HOL/Library/Univ_Poly.thy	Wed Feb 11 11:22:42 2009 -0800
7.2 +++ b/src/HOL/Library/Univ_Poly.thy	Thu Feb 12 18:14:43 2009 +0100
7.3 @@ -344,26 +344,6 @@
7.4  apply (erule_tac x="x" in allE, clarsimp)
7.5  by (case_tac "n=length p", auto simp add: order_le_less)
7.6
7.7 -lemma UNIV_nat_infinite: "\<not> finite (UNIV :: nat set)"
7.8 -  unfolding finite_conv_nat_seg_image
7.9 -proof(auto simp add: expand_set_eq image_iff)
7.10 -  fix n::nat and f:: "nat \<Rightarrow> nat"
7.11 -  let ?N = "{i. i < n}"
7.12 -  let ?fN = "f ` ?N"
7.13 -  let ?y = "Max ?fN + 1"
7.14 -  from nat_seg_image_imp_finite[of "?fN" "f" n]
7.15 -  have thfN: "finite ?fN" by simp
7.16 -  {assume "n =0" hence "\<exists>x. \<forall>xa<n. x \<noteq> f xa" by auto}
7.17 -  moreover
7.18 -  {assume nz: "n \<noteq> 0"
7.19 -    hence thne: "?fN \<noteq> {}" by (auto simp add: neq0_conv)
7.20 -    have "\<forall>x\<in> ?fN. Max ?fN \<ge> x" using nz Max_ge_iff[OF thfN thne] by auto
7.21 -    hence "\<forall>x\<in> ?fN. ?y > x" by auto
7.22 -    hence "?y \<notin> ?fN" by auto
7.23 -    hence "\<exists>x. \<forall>xa<n. x \<noteq> f xa" by auto }
7.24 -  ultimately show "\<exists>x. \<forall>xa<n. x \<noteq> f xa" by blast
7.25 -qed
7.26 -
7.27  lemma (in ring_char_0) UNIV_ring_char_0_infinte:
7.28    "\<not> (finite (UNIV:: 'a set))"
7.29  proof
7.30 @@ -374,7 +354,7 @@
7.31      then show "finite (of_nat ` UNIV :: 'a set)" using F by (rule finite_subset)
7.32      show "inj (of_nat :: nat \<Rightarrow> 'a)" by (simp add: inj_on_def)
7.33    qed
7.34 -  with UNIV_nat_infinite show False ..
7.35 +  with infinite_UNIV_nat show False ..
7.36  qed
7.37
7.38  lemma (in idom_char_0) poly_roots_finite: "(poly p \<noteq> poly []) =
```
```     8.1 --- a/src/HOL/Nat.thy	Wed Feb 11 11:22:42 2009 -0800
8.2 +++ b/src/HOL/Nat.thy	Thu Feb 12 18:14:43 2009 +0100
8.3 @@ -1367,6 +1367,9 @@
8.4
8.5  end
8.6
8.7 +lemma mono_iff_le_Suc: "mono f = (\<forall>n. f n \<le> f (Suc n))"
8.8 +unfolding mono_def
8.9 +by (auto intro:lift_Suc_mono_le[of f])
8.10
8.11  lemma mono_nat_linear_lb:
8.12    "(!!m n::nat. m<n \<Longrightarrow> f m < f n) \<Longrightarrow> f(m)+k \<le> f(m+k)"
```