author chaieb Mon Feb 25 11:27:25 2008 +0100 (2008-02-25) changeset 26123 44384b5c4fc0 parent 26122 76cbf193c09d child 26124 2514f0ade8bc
A proof a the fundamental theorem of algebra
```     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/Complex/Fundamental_Theorem_Algebra.thy	Mon Feb 25 11:27:25 2008 +0100
1.3 @@ -0,0 +1,1370 @@
1.4 +(*  Title:       Fundamental_Theorem_Algebra.thy
1.5 +    ID:          \$Id\$
1.6 +    Author:      Amine Chaieb
1.7 +*)
1.8 +
1.10 +
1.11 +theory Fundamental_Theorem_Algebra
1.12 +  imports  Univ_Poly Complex
1.13 +begin
1.14 +
1.15 +section {* Square root of complex numbers *}
1.16 +definition csqrt :: "complex \<Rightarrow> complex" where
1.17 +"csqrt z = (if Im z = 0 then
1.18 +            if 0 \<le> Re z then Complex (sqrt(Re z)) 0
1.19 +            else Complex 0 (sqrt(- Re z))
1.20 +           else Complex (sqrt((cmod z + Re z) /2))
1.21 +                        ((Im z / abs(Im z)) * sqrt((cmod z - Re z) /2)))"
1.22 +
1.23 +lemma csqrt: "csqrt z ^ 2 = z"
1.24 +proof-
1.25 +  obtain x y where xy: "z = Complex x y" by (cases z, simp_all)
1.26 +  {assume y0: "y = 0"
1.27 +    {assume x0: "x \<ge> 0"
1.28 +      then have ?thesis using y0 xy real_sqrt_pow2[OF x0]
1.29 +	by (simp add: csqrt_def power2_eq_square)}
1.30 +    moreover
1.31 +    {assume "\<not> x \<ge> 0" hence x0: "- x \<ge> 0" by arith
1.32 +      then have ?thesis using y0 xy real_sqrt_pow2[OF x0]
1.33 +	by (simp add: csqrt_def power2_eq_square) }
1.34 +    ultimately have ?thesis by blast}
1.35 +  moreover
1.36 +  {assume y0: "y\<noteq>0"
1.37 +    {fix x y
1.38 +      let ?z = "Complex x y"
1.39 +      from abs_Re_le_cmod[of ?z] have tha: "abs x \<le> cmod ?z" by auto
1.40 +      hence "cmod ?z - x \<ge> 0" "cmod ?z + x \<ge> 0" by (cases "x \<ge> 0", arith+)
1.41 +      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) }
1.42 +    note th = this
1.43 +    have sq4: "\<And>x::real. x^2 / 4 = (x / 2) ^ 2"
1.44 +      by (simp add: power2_eq_square)
1.45 +    from th[of x y]
1.46 +    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
1.47 +    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"
1.48 +      unfolding power2_eq_square by simp
1.49 +    have "sqrt 4 = sqrt (2^2)" by simp
1.50 +    hence sqrt4: "sqrt 4 = 2" by (simp only: real_sqrt_abs)
1.51 +    have th2: "2 *(y * sqrt ((sqrt (x * x + y * y) - x) * (sqrt (x * x + y * y) + x) / 4)) / \<bar>y\<bar> = y"
1.52 +      using iffD2[OF real_sqrt_pow2_iff sum_power2_ge_zero[of x y]] y0
1.53 +      unfolding power2_eq_square
1.54 +      by (simp add: ring_simps real_sqrt_divide sqrt4)
1.55 +     from y0 xy have ?thesis  apply (simp add: csqrt_def power2_eq_square)
1.56 +       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])
1.57 +      using th1 th2  ..}
1.58 +  ultimately show ?thesis by blast
1.59 +qed
1.60 +
1.61 +
1.62 +section{* More lemmas about module of complex numbers *}
1.63 +
1.64 +lemma complex_of_real_power: "complex_of_real x ^ n = complex_of_real (x^n)"
1.65 +  by (induct n, auto)
1.66 +
1.67 +lemma cmod_pos: "cmod z \<ge> 0" by simp
1.68 +lemma complex_mod_triangle_ineq: "cmod (z + w) \<le> cmod z + cmod w"
1.69 +  using complex_mod_triangle_ineq2[of z w] by (simp add: ring_simps)
1.70 +
1.71 +lemma cmod_mult: "cmod (z*w) = cmod z * cmod w"
1.72 +proof-
1.73 +  from rcis_Ex[of z] rcis_Ex[of w]
1.74 +  obtain rz az rw aw where z: "z = rcis rz az" and w: "w = rcis rw aw"  by blast
1.75 +  thus ?thesis by (simp add: rcis_mult abs_mult)
1.76 +qed
1.77 +
1.78 +lemma cmod_divide: "cmod (z/w) = cmod z / cmod w"
1.79 +proof-
1.80 +  from rcis_Ex[of z] rcis_Ex[of w]
1.81 +  obtain rz az rw aw where z: "z = rcis rz az" and w: "w = rcis rw aw"  by blast
1.82 +  thus ?thesis by (simp add: rcis_divide)
1.83 +qed
1.84 +
1.85 +lemma cmod_inverse: "cmod (inverse z) = inverse (cmod z)"
1.86 +  using cmod_divide[of 1 z] by (simp add: inverse_eq_divide)
1.87 +
1.88 +lemma cmod_uminus: "cmod (- z) = cmod z"
1.89 +  unfolding cmod_def by simp
1.90 +lemma cmod_abs_norm: "\<bar>cmod w - cmod z\<bar> \<le> cmod (w - z)"
1.91 +proof-
1.92 +  have ath: "\<And>(a::real) b x. a - b <= x \<Longrightarrow> b - a <= x ==> abs(a - b) <= x"
1.93 +    by arith
1.94 +  from complex_mod_triangle_ineq2[of "w - z" z]
1.95 +  have th1: "cmod w - cmod z \<le> cmod (w - z)" by simp
1.96 +  from complex_mod_triangle_ineq2[of "- (w - z)" "w"]
1.97 +  have th2: "cmod z - cmod w \<le> cmod (w - z)" using cmod_uminus [of "w - z"]
1.98 +    by simp
1.99 +  from ath[OF th1 th2] show ?thesis .
1.100 +qed
1.101 +
1.102 +lemma cmod_power: "cmod (z ^n) = cmod z ^ n" by (induct n, auto simp add: cmod_mult)
1.103 +lemma real_down2: "(0::real) < d1 \<Longrightarrow> 0 < d2 ==> EX e. 0 < e & e < d1 & e < d2"
1.104 +  apply ferrack apply arith done
1.105 +
1.106 +lemma cmod_complex_of_real: "cmod (complex_of_real x) = \<bar>x\<bar>"
1.107 +  unfolding cmod_def by auto
1.108 +
1.109 +
1.110 +text{* The triangle inequality for cmod *}
1.111 +lemma complex_mod_triangle_sub: "cmod w \<le> cmod (w + z) + norm z"
1.112 +  using complex_mod_triangle_ineq2[of "w + z" "-z"] by auto
1.113 +
1.114 +section{* Basic lemmas about complex polynomials *}
1.115 +
1.116 +lemma poly_bound_exists:
1.117 +  shows "\<exists>m. m > 0 \<and> (\<forall>z. cmod z <= r \<longrightarrow> cmod (poly p z) \<le> m)"
1.118 +proof(induct p)
1.119 +  case Nil thus ?case by (rule exI[where x=1], simp)
1.120 +next
1.121 +  case (Cons c cs)
1.122 +  from Cons.hyps obtain m where m: "\<forall>z. cmod z \<le> r \<longrightarrow> cmod (poly cs z) \<le> m"
1.123 +    by blast
1.124 +  let ?k = " 1 + cmod c + \<bar>r * m\<bar>"
1.125 +  have kp: "?k > 0" using abs_ge_zero[of "r*m"] cmod_pos[of c] by arith
1.126 +  {fix z
1.127 +    assume H: "cmod z \<le> r"
1.128 +    from m H have th: "cmod (poly cs z) \<le> m" by blast
1.129 +    from H have rp: "r \<ge> 0" using cmod_pos[of z] by arith
1.130 +    have "cmod (poly (c # cs) z) \<le> cmod c + cmod (z* poly cs z)"
1.131 +      using complex_mod_triangle_ineq[of c "z* poly cs z"] by simp
1.132 +    also have "\<dots> \<le> cmod c + r*m" using mult_mono[OF H th rp cmod_pos[of "poly cs z"]] by (simp add: cmod_mult)
1.133 +    also have "\<dots> \<le> ?k" by simp
1.134 +    finally have "cmod (poly (c # cs) z) \<le> ?k" .}
1.135 +  with kp show ?case by blast
1.136 +qed
1.137 +
1.138 +
1.139 +text{* Offsetting the variable in a polynomial gives another of same degree *}
1.140 +  (* FIXME : Lemma holds also in locale --- fix it laster *)
1.141 +lemma  poly_offset_lemma:
1.142 +  shows "\<exists>b q. (length q = length p) \<and> (\<forall>x. poly (b#q) (x::complex) = (a + x) * poly p x)"
1.143 +proof(induct p)
1.144 +  case Nil thus ?case by simp
1.145 +next
1.146 +  case (Cons c cs)
1.147 +  from Cons.hyps obtain b q where
1.148 +    bq: "length q = length cs" "\<forall>x. poly (b # q) x = (a + x) * poly cs x"
1.149 +    by blast
1.150 +  let ?b = "a*c"
1.151 +  let ?q = "(b+c)#q"
1.152 +  have lg: "length ?q = length (c#cs)" using bq(1) by simp
1.153 +  {fix x
1.154 +    from bq(2)[rule_format, of x]
1.155 +    have "x*poly (b # q) x = x*((a + x) * poly cs x)" by simp
1.156 +    hence "poly (?b# ?q) x = (a + x) * poly (c # cs) x"
1.157 +      by (simp add: ring_simps)}
1.158 +  with lg  show ?case by blast
1.159 +qed
1.160 +
1.161 +    (* FIXME : This one too*)
1.162 +lemma poly_offset: "\<exists> q. length q = length p \<and> (\<forall>x. poly q (x::complex) = poly p (a + x))"
1.163 +proof (induct p)
1.164 +  case Nil thus ?case by simp
1.165 +next
1.166 +  case (Cons c cs)
1.167 +  from Cons.hyps obtain q where q: "length q = length cs" "\<forall>x. poly q x = poly cs (a + x)" by blast
1.168 +  from poly_offset_lemma[of q a] obtain b p where
1.169 +    bp: "length p = length q" "\<forall>x. poly (b # p) x = (a + x) * poly q x"
1.170 +    by blast
1.171 +  thus ?case using q bp by - (rule exI[where x="(c + b)#p"], simp)
1.172 +qed
1.173 +
1.174 +text{* An alternative useful formulation of completeness of the reals *}
1.175 +lemma real_sup_exists: assumes ex: "\<exists>x. P x" and bz: "\<exists>z. \<forall>x. P x \<longrightarrow> x < z"
1.176 +  shows "\<exists>(s::real). \<forall>y. (\<exists>x. P x \<and> y < x) \<longleftrightarrow> y < s"
1.177 +proof-
1.178 +  from ex bz obtain x Y where x: "P x" and Y: "\<And>x. P x \<Longrightarrow> x < Y"  by blast
1.179 +  from ex have thx:"\<exists>x. x \<in> Collect P" by blast
1.180 +  from bz have thY: "\<exists>Y. isUb UNIV (Collect P) Y"
1.181 +    by(auto simp add: isUb_def isLub_def setge_def setle_def leastP_def Ball_def order_le_less)
1.182 +  from reals_complete[OF thx thY] obtain L where L: "isLub UNIV (Collect P) L"
1.183 +    by blast
1.184 +  from Y[OF x] have xY: "x < Y" .
1.185 +  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)
1.186 +  from Y have Y': "\<forall>x. P x \<longrightarrow> x \<le> Y"
1.187 +    apply (clarsimp, atomize (full)) by auto
1.188 +  from L Y' have "L \<le> Y" by (auto simp add: isUb_def isLub_def setge_def setle_def leastP_def Ball_def)
1.189 +  {fix y
1.190 +    {fix z assume z: "P z" "y < z"
1.191 +      from L' z have "y < L" by auto }
1.192 +    moreover
1.193 +    {assume yL: "y < L" "\<forall>z. P z \<longrightarrow> \<not> y < z"
1.194 +      hence nox: "\<forall>z. P z \<longrightarrow> y \<ge> z" by auto
1.195 +      from nox L have "y \<ge> L" by (auto simp add: isUb_def isLub_def setge_def setle_def leastP_def Ball_def)
1.196 +      with yL(1) have False  by arith}
1.197 +    ultimately have "(\<exists>x. P x \<and> y < x) \<longleftrightarrow> y < L" by blast}
1.198 +  thus ?thesis by blast
1.199 +qed
1.200 +
1.201 +
1.202 +section{* Some theorems about Sequences*}
1.203 +text{* Given a binary function @{text "f:: nat \<Rightarrow> 'a \<Rightarrow> 'a"}, its values are uniquely determined by a function g *}
1.204 +
1.205 +lemma num_Axiom: "EX! g. g 0 = e \<and> (\<forall>n. g (Suc n) = f n (g n))"
1.206 +  unfolding Ex1_def
1.207 +  apply (rule_tac x="nat_rec e f" in exI)
1.208 +  apply (rule conjI)+
1.209 +apply (rule def_nat_rec_0, simp)
1.210 +apply (rule allI, rule def_nat_rec_Suc, simp)
1.211 +apply (rule allI, rule impI, rule ext)
1.212 +apply (erule conjE)
1.213 +apply (induct_tac x)
1.215 +apply (erule_tac x="n" in allE)
1.216 +apply (simp)
1.217 +done
1.218 +
1.219 + text{* An equivalent formulation of monotony -- Not used here, but might be useful *}
1.220 +lemma mono_Suc: "mono f = (\<forall>n. (f n :: 'a :: order) \<le> f (Suc n))"
1.221 +unfolding mono_def
1.222 +proof auto
1.223 +  fix A B :: nat
1.224 +  assume H: "\<forall>n. f n \<le> f (Suc n)" "A \<le> B"
1.225 +  hence "\<exists>k. B = A + k" apply -  apply (thin_tac "\<forall>n. f n \<le> f (Suc n)")
1.226 +    by presburger
1.227 +  then obtain k where k: "B = A + k" by blast
1.228 +  {fix a k
1.229 +    have "f a \<le> f (a + k)"
1.230 +    proof (induct k)
1.231 +      case 0 thus ?case by simp
1.232 +    next
1.233 +      case (Suc k)
1.234 +      from Suc.hyps H(1)[rule_format, of "a + k"] show ?case by simp
1.235 +    qed}
1.236 +  with k show "f A \<le> f B" by blast
1.237 +qed
1.238 +
1.239 +text{* for any sequence, there is a mootonic subsequence *}
1.240 +lemma seq_monosub: "\<exists>f. subseq f \<and> monoseq (\<lambda> n. (s (f n)))"
1.241 +proof-
1.242 +  {assume H: "\<forall>n. \<exists>p >n. \<forall> m\<ge>p. s m \<le> s p"
1.243 +    let ?P = "\<lambda> p n. p > n \<and> (\<forall>m \<ge> p. s m \<le> s p)"
1.244 +    from num_Axiom[of "SOME p. ?P p 0" "\<lambda>p n. SOME p. ?P p n"]
1.245 +    obtain f where f: "f 0 = (SOME p. ?P p 0)" "\<forall>n. f (Suc n) = (SOME p. ?P p (f n))" by blast
1.246 +    have "?P (f 0) 0"  unfolding f(1) some_eq_ex[of "\<lambda>p. ?P p 0"]
1.247 +      using H apply -
1.248 +      apply (erule allE[where x=0], erule exE, rule_tac x="p" in exI)
1.249 +      unfolding order_le_less by blast
1.250 +    hence f0: "f 0 > 0" "\<forall>m \<ge> f 0. s m \<le> s (f 0)" by blast+
1.251 +    {fix n
1.252 +      have "?P (f (Suc n)) (f n)"
1.253 +	unfolding f(2)[rule_format, of n] some_eq_ex[of "\<lambda>p. ?P p (f n)"]
1.254 +	using H apply -
1.255 +      apply (erule allE[where x="f n"], erule exE, rule_tac x="p" in exI)
1.256 +      unfolding order_le_less by blast
1.257 +    hence "f (Suc n) > f n" "\<forall>m \<ge> f (Suc n). s m \<le> s (f (Suc n))" by blast+}
1.258 +  note fSuc = this
1.259 +    {fix p q assume pq: "p \<ge> f q"
1.260 +      have "s p \<le> s(f(q))"  using f0(2)[rule_format, of p] pq fSuc
1.261 +	by (cases q, simp_all) }
1.262 +    note pqth = this
1.263 +    {fix q
1.264 +      have "f (Suc q) > f q" apply (induct q)
1.265 +	using f0(1) fSuc(1)[of 0] apply simp by (rule fSuc(1))}
1.266 +    note fss = this
1.267 +    from fss have th1: "subseq f" unfolding subseq_Suc_iff ..
1.268 +    {fix a b
1.269 +      have "f a \<le> f (a + b)"
1.270 +      proof(induct b)
1.271 +	case 0 thus ?case by simp
1.272 +      next
1.273 +	case (Suc b)
1.274 +	from fSuc(1)[of "a + b"] Suc.hyps show ?case by simp
1.275 +      qed}
1.276 +    note fmon0 = this
1.277 +    have "monoseq (\<lambda>n. s (f n))"
1.278 +    proof-
1.279 +      {fix n
1.280 +	have "s (f n) \<ge> s (f (Suc n))"
1.281 +	proof(cases n)
1.282 +	  case 0
1.283 +	  assume n0: "n = 0"
1.284 +	  from fSuc(1)[of 0] have th0: "f 0 \<le> f (Suc 0)" by simp
1.285 +	  from f0(2)[rule_format, OF th0] show ?thesis  using n0 by simp
1.286 +	next
1.287 +	  case (Suc m)
1.288 +	  assume m: "n = Suc m"
1.289 +	  from fSuc(1)[of n] m have th0: "f (Suc m) \<le> f (Suc (Suc m))" by simp
1.290 +	  from m fSuc(2)[rule_format, OF th0] show ?thesis by simp
1.291 +	qed}
1.292 +      thus "monoseq (\<lambda>n. s (f n))" unfolding monoseq_Suc by blast
1.293 +    qed
1.294 +    with th1 have ?thesis by blast}
1.295 +  moreover
1.296 +  {fix N assume N: "\<forall>p >N. \<exists> m\<ge>p. s m > s p"
1.297 +    {fix p assume p: "p \<ge> Suc N"
1.298 +      hence pN: "p > N" by arith with N obtain m where m: "m \<ge> p" "s m > s p" by blast
1.299 +      have "m \<noteq> p" using m(2) by auto
1.300 +      with m have "\<exists>m>p. s p < s m" by - (rule exI[where x=m], auto)}
1.301 +    note th0 = this
1.302 +    let ?P = "\<lambda>m x. m > x \<and> s x < s m"
1.303 +    from num_Axiom[of "SOME x. ?P x (Suc N)" "\<lambda>m x. SOME y. ?P y x"]
1.304 +    obtain f where f: "f 0 = (SOME x. ?P x (Suc N))"
1.305 +      "\<forall>n. f (Suc n) = (SOME m. ?P m (f n))" by blast
1.306 +    have "?P (f 0) (Suc N)"  unfolding f(1) some_eq_ex[of "\<lambda>p. ?P p (Suc N)"]
1.307 +      using N apply -
1.308 +      apply (erule allE[where x="Suc N"], clarsimp)
1.309 +      apply (rule_tac x="m" in exI)
1.310 +      apply auto
1.311 +      apply (subgoal_tac "Suc N \<noteq> m")
1.312 +      apply simp
1.313 +      apply (rule ccontr, simp)
1.314 +      done
1.315 +    hence f0: "f 0 > Suc N" "s (Suc N) < s (f 0)" by blast+
1.316 +    {fix n
1.317 +      have "f n > N \<and> ?P (f (Suc n)) (f n)"
1.318 +	unfolding f(2)[rule_format, of n] some_eq_ex[of "\<lambda>p. ?P p (f n)"]
1.319 +      proof (induct n)
1.320 +	case 0 thus ?case
1.321 +	  using f0 N apply auto
1.322 +	  apply (erule allE[where x="f 0"], clarsimp)
1.323 +	  apply (rule_tac x="m" in exI, simp)
1.324 +	  by (subgoal_tac "f 0 \<noteq> m", auto)
1.325 +      next
1.326 +	case (Suc n)
1.327 +	from Suc.hyps have Nfn: "N < f n" by blast
1.328 +	from Suc.hyps obtain m where m: "m > f n" "s (f n) < s m" by blast
1.329 +	with Nfn have mN: "m > N" by arith
1.330 +	note key = Suc.hyps[unfolded some_eq_ex[of "\<lambda>p. ?P p (f n)", symmetric] f(2)[rule_format, of n, symmetric]]
1.331 +
1.332 +	from key have th0: "f (Suc n) > N" by simp
1.333 +	from N[rule_format, OF th0]
1.334 +	obtain m' where m': "m' \<ge> f (Suc n)" "s (f (Suc n)) < s m'" by blast
1.335 +	have "m' \<noteq> f (Suc (n))" apply (rule ccontr) using m'(2) by auto
1.336 +	hence "m' > f (Suc n)" using m'(1) by simp
1.337 +	with key m'(2) show ?case by auto
1.338 +      qed}
1.339 +    note fSuc = this
1.340 +    {fix n
1.341 +      have "f n \<ge> Suc N \<and> f(Suc n) > f n \<and> s(f n) < s(f(Suc n))" using fSuc[of n] by auto
1.342 +      hence "f n \<ge> Suc N" "f(Suc n) > f n" "s(f n) < s(f(Suc n))" by blast+}
1.343 +    note thf = this
1.344 +    have sqf: "subseq f" unfolding subseq_Suc_iff using thf by simp
1.345 +    have "monoseq (\<lambda>n. s (f n))"  unfolding monoseq_Suc using thf
1.346 +      apply -
1.347 +      apply (rule disjI1)
1.348 +      apply auto
1.349 +      apply (rule order_less_imp_le)
1.350 +      apply blast
1.351 +      done
1.352 +    then have ?thesis  using sqf by blast}
1.353 +  ultimately show ?thesis unfolding linorder_not_less[symmetric] by blast
1.354 +qed
1.355 +
1.356 +lemma seq_suble: assumes sf: "subseq f" shows "n \<le> f n"
1.357 +proof(induct n)
1.358 +  case 0 thus ?case by simp
1.359 +next
1.360 +  case (Suc n)
1.361 +  from sf[unfolded subseq_Suc_iff, rule_format, of n] Suc.hyps
1.362 +  have "n < f (Suc n)" by arith
1.363 +  thus ?case by arith
1.364 +qed
1.365 +
1.366 +section {* Fundamental theorem of algebra *}
1.367 +lemma  unimodular_reduce_norm:
1.368 +  assumes md: "cmod z = 1"
1.369 +  shows "cmod (z + 1) < 1 \<or> cmod (z - 1) < 1 \<or> cmod (z + ii) < 1 \<or> cmod (z - ii) < 1"
1.370 +proof-
1.371 +  obtain x y where z: "z = Complex x y " by (cases z, auto)
1.372 +  from md z have xy: "x^2 + y^2 = 1" by (simp add: cmod_def)
1.373 +  {assume C: "cmod (z + 1) \<ge> 1" "cmod (z - 1) \<ge> 1" "cmod (z + ii) \<ge> 1" "cmod (z - ii) \<ge> 1"
1.374 +    from C z xy have "2*x \<le> 1" "2*x \<ge> -1" "2*y \<le> 1" "2*y \<ge> -1"
1.375 +      by (simp_all add: cmod_def power2_eq_square ring_simps)
1.376 +    hence "abs (2*x) \<le> 1" "abs (2*y) \<le> 1" by simp_all
1.377 +    hence "(abs (2 * x))^2 <= 1^2" "(abs (2 * y)) ^2 <= 1^2"
1.378 +      by - (rule power_mono, simp, simp)+
1.379 +    hence th0: "4*x^2 \<le> 1" "4*y^2 \<le> 1"
1.380 +      by (simp_all  add: power2_abs power_mult_distrib)
1.381 +    from add_mono[OF th0] xy have False by simp }
1.382 +  thus ?thesis unfolding linorder_not_le[symmetric] by blast
1.383 +qed
1.384 +
1.385 +text{* Hence we can always reduce modulus of 1 + b z^n if nonzero *}
1.386 +lemma reduce_poly_simple:
1.387 + assumes b: "b \<noteq> 0" and n: "n\<noteq>0"
1.388 +  shows "\<exists>z. cmod (1 + b * z^n) < 1"
1.389 +using n
1.390 +proof(induct n rule: nat_less_induct)
1.391 +  fix n
1.392 +  assume IH: "\<forall>m<n. m \<noteq> 0 \<longrightarrow> (\<exists>z. cmod (1 + b * z ^ m) < 1)" and n: "n \<noteq> 0"
1.393 +  let ?P = "\<lambda>z n. cmod (1 + b * z ^ n) < 1"
1.394 +  {assume e: "even n"
1.395 +    hence "\<exists>m. n = 2*m" by presburger
1.396 +    then obtain m where m: "n = 2*m" by blast
1.397 +    from n m have "m\<noteq>0" "m < n" by presburger+
1.398 +    with IH[rule_format, of m] obtain z where z: "?P z m" by blast
1.399 +    from z have "?P (csqrt z) n" by (simp add: m power_mult csqrt)
1.400 +    hence "\<exists>z. ?P z n" ..}
1.401 +  moreover
1.402 +  {assume o: "odd n"
1.403 +    from b have b': "b^2 \<noteq> 0" unfolding power2_eq_square by simp
1.404 +    have "Im (inverse b) * (Im (inverse b) * \<bar>Im b * Im b + Re b * Re b\<bar>) +
1.405 +    Re (inverse b) * (Re (inverse b) * \<bar>Im b * Im b + Re b * Re b\<bar>) =
1.406 +    ((Re (inverse b))^2 + (Im (inverse b))^2) * \<bar>Im b * Im b + Re b * Re b\<bar>" by algebra
1.407 +    also have "\<dots> = cmod (inverse b) ^2 * cmod b ^ 2"
1.408 +      apply (simp add: cmod_def) using realpow_two_le_add_order[of "Re b" "Im b"]
1.409 +      by (simp add: power2_eq_square)
1.410 +    finally
1.411 +    have th0: "Im (inverse b) * (Im (inverse b) * \<bar>Im b * Im b + Re b * Re b\<bar>) +
1.412 +    Re (inverse b) * (Re (inverse b) * \<bar>Im b * Im b + Re b * Re b\<bar>) =
1.413 +    1"
1.414 +      apply (simp add: power2_eq_square cmod_mult[symmetric] cmod_inverse[symmetric])
1.415 +      using right_inverse[OF b']
1.416 +      by (simp add: power2_eq_square[symmetric] power_inverse[symmetric] ring_simps)
1.417 +    have th0: "cmod (complex_of_real (cmod b) / b) = 1"
1.418 +      apply (simp add: complex_Re_mult cmod_def power2_eq_square Re_complex_of_real Im_complex_of_real divide_inverse ring_simps )
1.419 +      by (simp add: real_sqrt_mult[symmetric] th0)
1.420 +    from o have "\<exists>m. n = Suc (2*m)" by presburger+
1.421 +    then obtain m where m: "n = Suc (2*m)" by blast
1.422 +    from unimodular_reduce_norm[OF th0] o
1.423 +    have "\<exists>v. cmod (complex_of_real (cmod b) / b + v^n) < 1"
1.424 +      apply (cases "cmod (complex_of_real (cmod b) / b + 1) < 1", rule_tac x="1" in exI, simp)
1.425 +      apply (cases "cmod (complex_of_real (cmod b) / b - 1) < 1", rule_tac x="-1" in exI, simp add: diff_def)
1.426 +      apply (cases "cmod (complex_of_real (cmod b) / b + ii) < 1")
1.427 +      apply (cases "even m", rule_tac x="ii" in exI, simp add: m power_mult)
1.428 +      apply (rule_tac x="- ii" in exI, simp add: m power_mult)
1.429 +      apply (cases "even m", rule_tac x="- ii" in exI, simp add: m power_mult diff_def)
1.430 +      apply (rule_tac x="ii" in exI, simp add: m power_mult diff_def)
1.431 +      done
1.432 +    then obtain v where v: "cmod (complex_of_real (cmod b) / b + v^n) < 1" by blast
1.433 +    let ?w = "v / complex_of_real (root n (cmod b))"
1.434 +    from odd_real_root_pow[OF o, of "cmod b"]
1.435 +    have th1: "?w ^ n = v^n / complex_of_real (cmod b)"
1.436 +      by (simp add: power_divide complex_of_real_power)
1.437 +    have th2:"cmod (complex_of_real (cmod b) / b) = 1" using b by (simp add: cmod_divide)
1.438 +    hence th3: "cmod (complex_of_real (cmod b) / b) \<ge> 0" by simp
1.439 +    have th4: "cmod (complex_of_real (cmod b) / b) *
1.440 +   cmod (1 + b * (v ^ n / complex_of_real (cmod b)))
1.441 +   < cmod (complex_of_real (cmod b) / b) * 1"
1.442 +      apply (simp only: cmod_mult[symmetric] right_distrib)
1.443 +      using b v by (simp add: th2)
1.444 +
1.445 +    from mult_less_imp_less_left[OF th4 th3]
1.446 +    have "?P ?w n" unfolding th1 .
1.447 +    hence "\<exists>z. ?P z n" .. }
1.448 +  ultimately show "\<exists>z. ?P z n" by blast
1.449 +qed
1.450 +
1.451 +
1.452 +text{* Bolzano-Weierstrass type property for closed disc in complex plane. *}
1.453 +
1.454 +lemma metric_bound_lemma: "cmod (x - y) <= \<bar>Re x - Re y\<bar> + \<bar>Im x - Im y\<bar>"
1.455 +  using real_sqrt_sum_squares_triangle_ineq[of "Re x - Re y" 0 0 "Im x - Im y" ]
1.456 +  unfolding cmod_def by simp
1.457 +
1.458 +lemma bolzano_weierstrass_complex_disc:
1.459 +  assumes r: "\<forall>n. cmod (s n) \<le> r"
1.460 +  shows "\<exists>f z. subseq f \<and> (\<forall>e >0. \<exists>N. \<forall>n \<ge> N. cmod (s (f n) - z) < e)"
1.461 +proof-
1.462 +  from seq_monosub[of "Re o s"]
1.463 +  obtain f g where f: "subseq f" "monoseq (\<lambda>n. Re (s (f n)))"
1.464 +    unfolding o_def by blast
1.465 +  from seq_monosub[of "Im o s o f"]
1.466 +  obtain g where g: "subseq g" "monoseq (\<lambda>n. Im (s(f(g n))))" unfolding o_def by blast
1.467 +  let ?h = "f o g"
1.468 +  from r[rule_format, of 0] have rp: "r \<ge> 0" using cmod_pos[of "s 0"] by arith
1.469 +  have th:"\<forall>n. r + 1 \<ge> \<bar> Re (s n)\<bar>"
1.470 +  proof
1.471 +    fix n
1.472 +    from abs_Re_le_cmod[of "s n"] r[rule_format, of n]  show "\<bar>Re (s n)\<bar> \<le> r + 1" by arith
1.473 +  qed
1.474 +  have conv1: "convergent (\<lambda>n. Re (s ( f n)))"
1.475 +    apply (rule Bseq_monoseq_convergent)
1.476 +    apply (simp add: Bseq_def)
1.477 +    apply (rule exI[where x= "r + 1"])
1.478 +    using th rp apply simp
1.479 +    using f(2) .
1.480 +  have th:"\<forall>n. r + 1 \<ge> \<bar> Im (s n)\<bar>"
1.481 +  proof
1.482 +    fix n
1.483 +    from abs_Im_le_cmod[of "s n"] r[rule_format, of n]  show "\<bar>Im (s n)\<bar> \<le> r + 1" by arith
1.484 +  qed
1.485 +
1.486 +  have conv2: "convergent (\<lambda>n. Im (s (f (g n))))"
1.487 +    apply (rule Bseq_monoseq_convergent)
1.488 +    apply (simp add: Bseq_def)
1.489 +    apply (rule exI[where x= "r + 1"])
1.490 +    using th rp apply simp
1.491 +    using g(2) .
1.492 +
1.493 +  from conv1[unfolded convergent_def] obtain x where "LIMSEQ (\<lambda>n. Re (s (f n))) x"
1.494 +    by blast
1.495 +  hence  x: "\<forall>r>0. \<exists>n0. \<forall>n\<ge>n0. \<bar> Re (s (f n)) - x \<bar> < r"
1.496 +    unfolding LIMSEQ_def real_norm_def .
1.497 +
1.498 +  from conv2[unfolded convergent_def] obtain y where "LIMSEQ (\<lambda>n. Im (s (f (g n)))) y"
1.499 +    by blast
1.500 +  hence  y: "\<forall>r>0. \<exists>n0. \<forall>n\<ge>n0. \<bar> Im (s (f (g n))) - y \<bar> < r"
1.501 +    unfolding LIMSEQ_def real_norm_def .
1.502 +  let ?w = "Complex x y"
1.503 +  from f(1) g(1) have hs: "subseq ?h" unfolding subseq_def by auto
1.504 +  {fix e assume ep: "e > (0::real)"
1.505 +    hence e2: "e/2 > 0" by simp
1.506 +    from x[rule_format, OF e2] y[rule_format, OF e2]
1.507 +    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
1.508 +    {fix n assume nN12: "n \<ge> N1 + N2"
1.509 +      hence nN1: "g n \<ge> N1" and nN2: "n \<ge> N2" using seq_suble[OF g(1), of n] by arith+
1.510 +      from add_strict_mono[OF N1[rule_format, OF nN1] N2[rule_format, OF nN2]]
1.511 +      have "cmod (s (?h n) - ?w) < e"
1.512 +	using metric_bound_lemma[of "s (f (g n))" ?w] by simp }
1.513 +    hence "\<exists>N. \<forall>n\<ge>N. cmod (s (?h n) - ?w) < e" by blast }
1.514 +  with hs show ?thesis  by blast
1.515 +qed
1.516 +
1.517 +text{* Polynomial is continuous. *}
1.518 +
1.519 +lemma poly_cont:
1.520 +  assumes ep: "e > 0"
1.521 +  shows "\<exists>d >0. \<forall>w. 0 < cmod (w - z) \<and> cmod (w - z) < d \<longrightarrow> cmod (poly p w - poly p z) < e"
1.522 +proof-
1.523 +  from poly_offset[of p z] obtain q where q: "length q = length p" "\<And>x. poly q x = poly p (z + x)" by blast
1.524 +  {fix w
1.525 +    note q(2)[of "w - z", simplified]}
1.526 +  note th = this
1.527 +  show ?thesis unfolding th[symmetric]
1.528 +  proof(induct q)
1.529 +    case Nil thus ?case  using ep by auto
1.530 +  next
1.531 +    case (Cons c cs)
1.532 +    from poly_bound_exists[of 1 "cs"]
1.533 +    obtain m where m: "m > 0" "\<And>z. cmod z \<le> 1 \<Longrightarrow> cmod (poly cs z) \<le> m" by blast
1.534 +    from ep m(1) have em0: "e/m > 0" by (simp add: field_simps)
1.535 +    have one0: "1 > (0::real)"  by arith
1.536 +    from real_lbound_gt_zero[OF one0 em0]
1.537 +    obtain d where d: "d >0" "d < 1" "d < e / m" by blast
1.538 +    from d(1,3) m(1) have dm: "d*m > 0" "d*m < e"
1.539 +      by (simp_all add: field_simps real_mult_order)
1.540 +    show ?case
1.541 +      proof(rule ex_forward[OF real_lbound_gt_zero[OF one0 em0]], clarsimp simp add: cmod_mult)
1.542 +	fix d w
1.543 +	assume H: "d > 0" "d < 1" "d < e/m" "w\<noteq>z" "cmod (w-z) < d"
1.544 +	hence d1: "cmod (w-z) \<le> 1" "d \<ge> 0" by simp_all
1.545 +	from H(3) m(1) have dme: "d*m < e" by (simp add: field_simps)
1.546 +	from H have th: "cmod (w-z) \<le> d" by simp
1.547 +	from mult_mono[OF th m(2)[OF d1(1)] d1(2) cmod_pos] dme
1.548 +	show "cmod (w - z) * cmod (poly cs (w - z)) < e" by simp
1.549 +      qed
1.550 +    qed
1.551 +qed
1.552 +
1.553 +text{* Hence a polynomial attains minimum on a closed disc
1.554 +  in the complex plane. *}
1.555 +lemma  poly_minimum_modulus_disc:
1.556 +  "\<exists>z. \<forall>w. cmod w \<le> r \<longrightarrow> cmod (poly p z) \<le> cmod (poly p w)"
1.557 +proof-
1.558 +  {assume "\<not> r \<ge> 0" hence ?thesis unfolding linorder_not_le
1.559 +      apply -
1.560 +      apply (rule exI[where x=0])
1.561 +      apply auto
1.562 +      apply (subgoal_tac "cmod w < 0")
1.563 +      apply simp
1.564 +      apply arith
1.565 +      done }
1.566 +  moreover
1.567 +  {assume rp: "r \<ge> 0"
1.568 +    from rp have "cmod 0 \<le> r \<and> cmod (poly p 0) = - (- cmod (poly p 0))" by simp
1.569 +    hence mth1: "\<exists>x z. cmod z \<le> r \<and> cmod (poly p z) = - x"  by blast
1.570 +    {fix x z
1.571 +      assume H: "cmod z \<le> r" "cmod (poly p z) = - x" "\<not>x < 1"
1.572 +      hence "- x < 0 " by arith
1.573 +      with H(2) cmod_pos[of "poly p z"]  have False by simp }
1.574 +    then have mth2: "\<exists>z. \<forall>x. (\<exists>z. cmod z \<le> r \<and> cmod (poly p z) = - x) \<longrightarrow> x < z" by blast
1.575 +    from real_sup_exists[OF mth1 mth2] obtain s where
1.576 +      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
1.577 +    let ?m = "-s"
1.578 +    {fix y
1.579 +      from s[rule_format, of "-y"] have
1.580 +    "(\<exists>z x. cmod z \<le> r \<and> -(- cmod (poly p z)) < y) \<longleftrightarrow> ?m < y"
1.581 +	unfolding minus_less_iff[of y ] equation_minus_iff by blast }
1.582 +    note s1 = this[unfolded minus_minus]
1.583 +    from s1[of ?m] have s1m: "\<And>z x. cmod z \<le> r \<Longrightarrow> cmod (poly p z) \<ge> ?m"
1.584 +      by auto
1.585 +    {fix n::nat
1.586 +      from s1[rule_format, of "?m + 1/real (Suc n)"]
1.587 +      have "\<exists>z. cmod z \<le> r \<and> cmod (poly p z) < - s + 1 / real (Suc n)"
1.588 +	by simp}
1.589 +    hence th: "\<forall>n. \<exists>z. cmod z \<le> r \<and> cmod (poly p z) < - s + 1 / real (Suc n)" ..
1.590 +    from choice[OF th] obtain g where
1.591 +      g: "\<forall>n. cmod (g n) \<le> r" "\<forall>n. cmod (poly p (g n)) <?m+1 /real(Suc n)"
1.592 +      by blast
1.593 +    from bolzano_weierstrass_complex_disc[OF g(1)]
1.594 +    obtain f z where fz: "subseq f" "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. cmod (g (f n) - z) < e"
1.595 +      by blast
1.596 +    {fix w
1.597 +      assume wr: "cmod w \<le> r"
1.598 +      let ?e = "\<bar>cmod (poly p z) - ?m\<bar>"
1.599 +      {assume e: "?e > 0"
1.600 +	hence e2: "?e/2 > 0" by simp
1.601 +	from poly_cont[OF e2, of z p] obtain d where
1.602 +	  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
1.603 +	{fix w assume w: "cmod (w - z) < d"
1.604 +	  have "cmod(poly p w - poly p z) < ?e / 2"
1.605 +	    using d(2)[rule_format, of w] w e by (cases "w=z", simp_all)}
1.606 +	note th1 = this
1.607 +
1.608 +	from fz(2)[rule_format, OF d(1)] obtain N1 where
1.609 +	  N1: "\<forall>n\<ge>N1. cmod (g (f n) - z) < d" by blast
1.610 +	from reals_Archimedean2[of "2/?e"] obtain N2::nat where
1.611 +	  N2: "2/?e < real N2" by blast
1.612 +	have th2: "cmod(poly p (g(f(N1 + N2))) - poly p z) < ?e/2"
1.613 +	  using N1[rule_format, of "N1 + N2"] th1 by simp
1.614 +	{fix a b e2 m :: real
1.615 +	have "a < e2 \<Longrightarrow> abs(b - m) < e2 \<Longrightarrow> 2 * e2 <= abs(b - m) + a
1.616 +          ==> False" by arith}
1.617 +      note th0 = this
1.618 +      have ath:
1.619 +	"\<And>m x e. m <= x \<Longrightarrow>  x < m + e ==> abs(x - m::real) < e" by arith
1.620 +      from s1m[OF g(1)[rule_format]]
1.621 +      have th31: "?m \<le> cmod(poly p (g (f (N1 + N2))))" .
1.622 +      from seq_suble[OF fz(1), of "N1+N2"]
1.623 +      have th00: "real (Suc (N1+N2)) \<le> real (Suc (f (N1+N2)))" by simp
1.624 +      have th000: "0 \<le> (1::real)" "(1::real) \<le> 1" "real (Suc (N1+N2)) > 0"
1.625 +	using N2 by auto
1.626 +      from frac_le[OF th000 th00] have th00: "?m +1 / real (Suc (f (N1 + N2))) \<le> ?m + 1 / real (Suc (N1 + N2))" by simp
1.627 +      from g(2)[rule_format, of "f (N1 + N2)"]
1.628 +      have th01:"cmod (poly p (g (f (N1 + N2)))) < - s + 1 / real (Suc (f (N1 + N2)))" .
1.629 +      from order_less_le_trans[OF th01 th00]
1.630 +      have th32: "cmod(poly p (g (f (N1 + N2)))) < ?m + (1/ real(Suc (N1 + N2)))" .
1.631 +      from N2 have "2/?e < real (Suc (N1 + N2))" by arith
1.632 +      with e2 less_imp_inverse_less[of "2/?e" "real (Suc (N1 + N2))"]
1.633 +      have "?e/2 > 1/ real (Suc (N1 + N2))" by (simp add: inverse_eq_divide)
1.634 +      with ath[OF th31 th32]
1.635 +      have thc1:"\<bar>cmod(poly p (g (f (N1 + N2)))) - ?m\<bar>< ?e/2" by arith
1.636 +      have ath2: "\<And>(a::real) b c m. \<bar>a - b\<bar> <= c ==> \<bar>b - m\<bar> <= \<bar>a - m\<bar> + c"
1.637 +	by arith
1.638 +      have th22: "\<bar>cmod (poly p (g (f (N1 + N2)))) - cmod (poly p z)\<bar>
1.639 +\<le> cmod (poly p (g (f (N1 + N2))) - poly p z)"
1.640 +	by (simp add: cmod_abs_norm)
1.641 +      from ath2[OF th22, of ?m]
1.642 +      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
1.643 +      from th0[OF th2 thc1 thc2] have False .}
1.644 +      hence "?e = 0" by auto
1.645 +      then have "cmod (poly p z) = ?m" by simp
1.646 +      with s1m[OF wr]
1.647 +      have "cmod (poly p z) \<le> cmod (poly p w)" by simp }
1.648 +    hence ?thesis by blast}
1.649 +  ultimately show ?thesis by blast
1.650 +qed
1.651 +
1.652 +lemma "(rcis (sqrt (abs r)) (a/2)) ^ 2 = rcis (abs r) a"
1.653 +  unfolding power2_eq_square
1.654 +  apply (simp add: rcis_mult)
1.655 +  apply (simp add: power2_eq_square[symmetric])
1.656 +  done
1.657 +
1.658 +lemma cispi: "cis pi = -1"
1.659 +  unfolding cis_def
1.660 +  by simp
1.661 +
1.662 +lemma "(rcis (sqrt (abs r)) ((pi + a)/2)) ^ 2 = rcis (- abs r) a"
1.663 +  unfolding power2_eq_square
1.665 +  apply (simp add: power2_eq_square[symmetric] rcis_def cispi cis_mult[symmetric])
1.666 +  done
1.667 +
1.668 +text {* Nonzero polynomial in z goes to infinity as z does. *}
1.669 +
1.670 +instance complex::idom_char_0 by (intro_classes)
1.671 +instance complex :: recpower_idom_char_0 by intro_classes
1.672 +
1.673 +lemma poly_infinity:
1.674 +  assumes ex: "list_ex (\<lambda>c. c \<noteq> 0) p"
1.675 +  shows "\<exists>r. \<forall>z. r \<le> cmod z \<longrightarrow> d \<le> cmod (poly (a#p) z)"
1.676 +using ex
1.677 +proof(induct p arbitrary: a d)
1.678 +  case (Cons c cs a d)
1.679 +  {assume H: "list_ex (\<lambda>c. c\<noteq>0) cs"
1.680 +    with Cons.hyps obtain r where r: "\<forall>z. r \<le> cmod z \<longrightarrow> d + cmod a \<le> cmod (poly (c # cs) z)" by blast
1.681 +    let ?r = "1 + \<bar>r\<bar>"
1.682 +    {fix z assume h: "1 + \<bar>r\<bar> \<le> cmod z"
1.683 +      have r0: "r \<le> cmod z" using h by arith
1.684 +      from r[rule_format, OF r0]
1.685 +      have th0: "d + cmod a \<le> 1 * cmod(poly (c#cs) z)" by arith
1.686 +      from h have z1: "cmod z \<ge> 1" by arith
1.687 +      from order_trans[OF th0 mult_right_mono[OF z1 cmod_pos[of "poly (c#cs) z"]]]
1.688 +      have th1: "d \<le> cmod(z * poly (c#cs) z) - cmod a"
1.689 +	unfolding cmod_mult by (simp add: ring_simps)
1.690 +      from complex_mod_triangle_sub[of "z * poly (c#cs) z" a]
1.691 +      have th2: "cmod(z * poly (c#cs) z) - cmod a \<le> cmod (poly (a#c#cs) z)"
1.692 +	by (simp add: diff_le_eq ring_simps)
1.693 +      from th1 th2 have "d \<le> cmod (poly (a#c#cs) z)"  by arith}
1.694 +    hence ?case by blast}
1.695 +  moreover
1.696 +  {assume cs0: "\<not> (list_ex (\<lambda>c. c \<noteq> 0) cs)"
1.697 +    with Cons.prems have c0: "c \<noteq> 0" by simp
1.698 +    from cs0 have cs0': "list_all (\<lambda>c. c = 0) cs"
1.699 +      by (auto simp add: list_all_iff list_ex_iff)
1.700 +    {fix z
1.701 +      assume h: "(\<bar>d\<bar> + cmod a) / cmod c \<le> cmod z"
1.702 +      from c0 have "cmod c > 0" by simp
1.703 +      from h c0 have th0: "\<bar>d\<bar> + cmod a \<le> cmod (z*c)"
1.704 +	by (simp add: field_simps cmod_mult)
1.705 +      have ath: "\<And>mzh mazh ma. mzh <= mazh + ma ==> abs(d) + ma <= mzh ==> d <= mazh" by arith
1.706 +      from complex_mod_triangle_sub[of "z*c" a ]
1.707 +      have th1: "cmod (z * c) \<le> cmod (a + z * c) + cmod a"
1.708 +	by (simp add: ring_simps)
1.709 +      from ath[OF th1 th0] have "d \<le> cmod (poly (a # c # cs) z)"
1.710 +	using poly_0[OF cs0'] by simp}
1.711 +    then have ?case  by blast}
1.712 +  ultimately show ?case by blast
1.713 +qed simp
1.714 +
1.715 +text {* Hence polynomial's modulus attains its minimum somewhere. *}
1.716 +lemma poly_minimum_modulus:
1.717 +  "\<exists>z.\<forall>w. cmod (poly p z) \<le> cmod (poly p w)"
1.718 +proof(induct p)
1.719 +  case (Cons c cs)
1.720 +  {assume cs0: "list_ex (\<lambda>c. c \<noteq> 0) cs"
1.721 +    from poly_infinity[OF cs0, of "cmod (poly (c#cs) 0)" c]
1.722 +    obtain r where r: "\<And>z. r \<le> cmod z \<Longrightarrow> cmod (poly (c # cs) 0) \<le> cmod (poly (c # cs) z)" by blast
1.723 +    have ath: "\<And>z r. r \<le> cmod z \<or> cmod z \<le> \<bar>r\<bar>" by arith
1.724 +    from poly_minimum_modulus_disc[of "\<bar>r\<bar>" "c#cs"]
1.725 +    obtain v where v: "\<And>w. cmod w \<le> \<bar>r\<bar> \<Longrightarrow> cmod (poly (c # cs) v) \<le> cmod (poly (c # cs) w)" by blast
1.726 +    {fix z assume z: "r \<le> cmod z"
1.727 +      from v[of 0] r[OF z]
1.728 +      have "cmod (poly (c # cs) v) \<le> cmod (poly (c # cs) z)"
1.729 +	by simp }
1.730 +    note v0 = this
1.731 +    from v0 v ath[of r] have ?case by blast}
1.732 +  moreover
1.733 +  {assume cs0: "\<not> (list_ex (\<lambda>c. c\<noteq>0) cs)"
1.734 +    hence th:"list_all (\<lambda>c. c = 0) cs" by (simp add: list_all_iff list_ex_iff)
1.735 +    from poly_0[OF th] Cons.hyps have ?case by simp}
1.736 +  ultimately show ?case by blast
1.737 +qed simp
1.738 +
1.739 +text{* Constant function (non-syntactic characterization). *}
1.740 +definition "constant f = (\<forall>x y. f x = f y)"
1.741 +
1.742 +lemma nonconstant_length: "\<not> (constant (poly p)) \<Longrightarrow> length p \<ge> 2"
1.743 +  unfolding constant_def
1.744 +  apply (induct p, auto)
1.745 +  apply (unfold not_less[symmetric])
1.746 +  apply simp
1.747 +  apply (rule ccontr)
1.748 +  apply auto
1.749 +  done
1.750 +
1.751 +lemma poly_replicate_append:
1.752 +  "poly ((replicate n 0)@p) (x::'a::{recpower, comm_ring}) = x^n * poly p x"
1.753 +  by(induct n, auto simp add: power_Suc ring_simps)
1.754 +
1.755 +text {* Decomposition of polynomial, skipping zero coefficients
1.756 +  after the first.  *}
1.757 +
1.758 +lemma poly_decompose_lemma:
1.759 + assumes nz: "\<not>(\<forall>z. z\<noteq>0 \<longrightarrow> poly p z = (0::'a::{recpower,idom}))"
1.760 +  shows "\<exists>k a q. a\<noteq>0 \<and> Suc (length q + k) = length p \<and>
1.761 +                 (\<forall>z. poly p z = z^k * poly (a#q) z)"
1.762 +using nz
1.763 +proof(induct p)
1.764 +  case Nil thus ?case by simp
1.765 +next
1.766 +  case (Cons c cs)
1.767 +  {assume c0: "c = 0"
1.768 +
1.769 +    from Cons.hyps Cons.prems c0 have ?case apply auto
1.770 +      apply (rule_tac x="k+1" in exI)
1.771 +      apply (rule_tac x="a" in exI, clarsimp)
1.772 +      apply (rule_tac x="q" in exI)
1.773 +      by (auto simp add: power_Suc)}
1.774 +  moreover
1.775 +  {assume c0: "c\<noteq>0"
1.776 +    hence ?case apply-
1.777 +      apply (rule exI[where x=0])
1.778 +      apply (rule exI[where x=c], clarsimp)
1.779 +      apply (rule exI[where x=cs])
1.780 +      apply auto
1.781 +      done}
1.782 +  ultimately show ?case by blast
1.783 +qed
1.784 +
1.785 +lemma poly_decompose:
1.786 +  assumes nc: "~constant(poly p)"
1.787 +  shows "\<exists>k a q. a\<noteq>(0::'a::{recpower,idom}) \<and> k\<noteq>0 \<and>
1.788 +               length q + k + 1 = length p \<and>
1.789 +              (\<forall>z. poly p z = poly p 0 + z^k * poly (a#q) z)"
1.790 +using nc
1.791 +proof(induct p)
1.792 +  case Nil thus ?case by (simp add: constant_def)
1.793 +next
1.794 +  case (Cons c cs)
1.795 +  {assume C:"\<forall>z. z \<noteq> 0 \<longrightarrow> poly cs z = 0"
1.796 +    {fix x y
1.797 +      from C have "poly (c#cs) x = poly (c#cs) y" by (cases "x=0", auto)}
1.798 +    with Cons.prems have False by (auto simp add: constant_def)}
1.799 +  hence th: "\<not> (\<forall>z. z \<noteq> 0 \<longrightarrow> poly cs z = 0)" ..
1.800 +  from poly_decompose_lemma[OF th]
1.801 +  show ?case
1.802 +    apply clarsimp
1.803 +    apply (rule_tac x="k+1" in exI)
1.804 +    apply (rule_tac x="a" in exI)
1.805 +    apply simp
1.806 +    apply (rule_tac x="q" in exI)
1.807 +    apply (auto simp add: power_Suc)
1.808 +    done
1.809 +qed
1.810 +
1.811 +text{* Fundamental theorem of algebral *}
1.812 +
1.813 +lemma fundamental_theorem_of_algebra:
1.814 +  assumes nc: "~constant(poly p)"
1.815 +  shows "\<exists>z::complex. poly p z = 0"
1.816 +using nc
1.817 +proof(induct n\<equiv> "length p" arbitrary: p rule: nat_less_induct)
1.818 +  fix n fix p :: "complex list"
1.819 +  let ?p = "poly p"
1.820 +  assume H: "\<forall>m<n. \<forall>p. \<not> constant (poly p) \<longrightarrow> m = length p \<longrightarrow> (\<exists>(z::complex). poly p z = 0)" and nc: "\<not> constant ?p" and n: "n = length p"
1.821 +  let ?ths = "\<exists>z. ?p z = 0"
1.822 +
1.823 +  from nonconstant_length[OF nc] have n2: "n\<ge> 2" by (simp add: n)
1.824 +  from poly_minimum_modulus obtain c where
1.825 +    c: "\<forall>w. cmod (?p c) \<le> cmod (?p w)" by blast
1.826 +  {assume pc: "?p c = 0" hence ?ths by blast}
1.827 +  moreover
1.828 +  {assume pc0: "?p c \<noteq> 0"
1.829 +    from poly_offset[of p c] obtain q where
1.830 +      q: "length q = length p" "\<forall>x. poly q x = ?p (c+x)" by blast
1.831 +    {assume h: "constant (poly q)"
1.832 +      from q(2) have th: "\<forall>x. poly q (x - c) = ?p x" by auto
1.833 +      {fix x y
1.834 +	from th have "?p x = poly q (x - c)" by auto
1.835 +	also have "\<dots> = poly q (y - c)"
1.836 +	  using h unfolding constant_def by blast
1.837 +	also have "\<dots> = ?p y" using th by auto
1.838 +	finally have "?p x = ?p y" .}
1.839 +      with nc have False unfolding constant_def by blast }
1.840 +    hence qnc: "\<not> constant (poly q)" by blast
1.841 +    from q(2) have pqc0: "?p c = poly q 0" by simp
1.842 +    from c pqc0 have cq0: "\<forall>w. cmod (poly q 0) \<le> cmod (?p w)" by simp
1.843 +    let ?a0 = "poly q 0"
1.844 +    from pc0 pqc0 have a00: "?a0 \<noteq> 0" by simp
1.845 +    from a00
1.846 +    have qr: "\<forall>z. poly q z = poly (map (op * (inverse ?a0)) q) z * ?a0"
1.847 +      by (simp add: poly_cmult_map)
1.848 +    let ?r = "map (op * (inverse ?a0)) q"
1.849 +    have lgqr: "length q = length ?r" by simp
1.850 +    {assume h: "\<And>x y. poly ?r x = poly ?r y"
1.851 +      {fix x y
1.852 +	from qr[rule_format, of x]
1.853 +	have "poly q x = poly ?r x * ?a0" by auto
1.854 +	also have "\<dots> = poly ?r y * ?a0" using h by simp
1.855 +	also have "\<dots> = poly q y" using qr[rule_format, of y] by simp
1.856 +	finally have "poly q x = poly q y" .}
1.857 +      with qnc have False unfolding constant_def by blast}
1.858 +    hence rnc: "\<not> constant (poly ?r)" unfolding constant_def by blast
1.859 +    from qr[rule_format, of 0] a00  have r01: "poly ?r 0 = 1" by auto
1.860 +    {fix w
1.861 +      have "cmod (poly ?r w) < 1 \<longleftrightarrow> cmod (poly q w / ?a0) < 1"
1.862 +	using qr[rule_format, of w] a00 by simp
1.863 +      also have "\<dots> \<longleftrightarrow> cmod (poly q w) < cmod ?a0"
1.864 +	using a00 unfolding cmod_divide by (simp add: field_simps)
1.865 +      finally have "cmod (poly ?r w) < 1 \<longleftrightarrow> cmod (poly q w) < cmod ?a0" .}
1.866 +    note mrmq_eq = this
1.867 +    from poly_decompose[OF rnc] obtain k a s where
1.868 +      kas: "a\<noteq>0" "k\<noteq>0" "length s + k + 1 = length ?r"
1.869 +      "\<forall>z. poly ?r z = poly ?r 0 + z^k* poly (a#s) z" by blast
1.870 +    {assume "k + 1 = n"
1.871 +      with kas(3) lgqr[symmetric] q(1) n[symmetric] have s0:"s=[]" by auto
1.872 +      {fix w
1.873 +	have "cmod (poly ?r w) = cmod (1 + a * w ^ k)"
1.874 +	  using kas(4)[rule_format, of w] s0 r01 by (simp add: ring_simps)}
1.875 +      note hth = this [symmetric]
1.876 +	from reduce_poly_simple[OF kas(1,2)]
1.877 +      have "\<exists>w. cmod (poly ?r w) < 1" unfolding hth by blast}
1.878 +    moreover
1.879 +    {assume kn: "k+1 \<noteq> n"
1.880 +      from kn kas(3) q(1) n[symmetric] have k1n: "k + 1 < n" by simp
1.881 +      have th01: "\<not> constant (poly (1#((replicate (k - 1) 0)@[a])))"
1.882 +	unfolding constant_def poly_Nil poly_Cons poly_replicate_append
1.883 +	using kas(1) apply simp
1.884 +	by (rule exI[where x=0], rule exI[where x=1], simp)
1.885 +      from kas(2) have th02: "k+1 = length (1#((replicate (k - 1) 0)@[a]))"
1.886 +	by simp
1.887 +      from H[rule_format, OF k1n th01 th02]
1.888 +      obtain w where w: "1 + w^k * a = 0"
1.889 +	unfolding poly_Nil poly_Cons poly_replicate_append
1.890 +	using kas(2) by (auto simp add: power_Suc[symmetric, of _ "k - Suc 0"]
1.891 +	  mult_assoc[of _ _ a, symmetric])
1.892 +      from poly_bound_exists[of "cmod w" s] obtain m where
1.893 +	m: "m > 0" "\<forall>z. cmod z \<le> cmod w \<longrightarrow> cmod (poly s z) \<le> m" by blast
1.894 +      have w0: "w\<noteq>0" using kas(2) w by (auto simp add: power_0_left)
1.895 +      from w have "(1 + w ^ k * a) - 1 = 0 - 1" by simp
1.896 +      then have wm1: "w^k * a = - 1" by simp
1.897 +      have inv0: "0 < inverse (cmod w ^ (k + 1) * m)"
1.898 +	using cmod_pos[of w] w0 m(1)
1.899 +	  by (simp add: inverse_eq_divide zero_less_mult_iff)
1.900 +      with real_down2[OF zero_less_one] obtain t where
1.901 +	t: "t > 0" "t < 1" "t < inverse (cmod w ^ (k + 1) * m)" by blast
1.902 +      let ?ct = "complex_of_real t"
1.903 +      let ?w = "?ct * w"
1.904 +      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: ring_simps power_mult_distrib)
1.905 +      also have "\<dots> = complex_of_real (1 - t^k) + ?w^k * ?w * poly s ?w"
1.906 +	unfolding wm1 by (simp)
1.907 +      finally have "cmod (1 + ?w^k * (a + ?w * poly s ?w)) = cmod (complex_of_real (1 - t^k) + ?w^k * ?w * poly s ?w)"
1.908 +	apply -
1.909 +	apply (rule cong[OF refl[of cmod]])
1.910 +	apply assumption
1.911 +	done
1.912 +      with complex_mod_triangle_ineq[of "complex_of_real (1 - t^k)" "?w^k * ?w * poly s ?w"]
1.913 +      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 cmod_complex_of_real by simp
1.914 +      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
1.915 +      have "t *cmod w \<le> 1 * cmod w" apply (rule mult_mono) using t(1,2) by auto
1.916 +      then have tw: "cmod ?w \<le> cmod w" using t(1) by (simp add: cmod_mult)
1.917 +      from t inv0 have "t* (cmod w ^ (k + 1) * m) < 1"
1.918 +	by (simp add: inverse_eq_divide field_simps)
1.919 +      with zero_less_power[OF t(1), of k]
1.920 +      have th30: "t^k * (t* (cmod w ^ (k + 1) * m)) < t^k * 1"
1.921 +	apply - apply (rule mult_strict_left_mono) by simp_all
1.922 +      have "cmod (?w^k * ?w * poly s ?w) = t^k * (t* (cmod w ^ (k+1) * cmod (poly s ?w)))"  using w0 t(1)
1.923 +	by (simp add: ring_simps power_mult_distrib cmod_complex_of_real cmod_power cmod_mult)
1.924 +      then have "cmod (?w^k * ?w * poly s ?w) \<le> t^k * (t* (cmod w ^ (k + 1) * m))"
1.925 +	using t(1,2) m(2)[rule_format, OF tw] w0
1.926 +	apply (simp only: )
1.927 +	apply auto
1.928 +	apply (rule mult_mono, simp_all add: cmod_pos)+
1.929 +	apply (simp add: zero_le_mult_iff zero_le_power)
1.930 +	done
1.931 +      with th30 have th120: "cmod (?w^k * ?w * poly s ?w) < t^k" by simp
1.932 +      from power_strict_mono[OF t(2), of k] t(1) kas(2) have th121: "t^k \<le> 1"
1.933 +	by auto
1.934 +      from ath[OF cmod_pos[of "?w^k * ?w * poly s ?w"] th120 th121]
1.935 +      have th12: "\<bar>1 - t^k\<bar> + cmod (?w^k * ?w * poly s ?w) < 1" .
1.936 +      from th11 th12
1.937 +      have "cmod (1 + ?w^k * (a + ?w * poly s ?w)) < 1"  by arith
1.938 +      then have "cmod (poly ?r ?w) < 1"
1.939 +	unfolding kas(4)[rule_format, of ?w] r01 by simp
1.940 +      then have "\<exists>w. cmod (poly ?r w) < 1" by blast}
1.941 +    ultimately have cr0_contr: "\<exists>w. cmod (poly ?r w) < 1" by blast
1.942 +    from cr0_contr cq0 q(2)
1.943 +    have ?ths unfolding mrmq_eq not_less[symmetric] by auto}
1.944 +  ultimately show ?ths by blast
1.945 +qed
1.946 +
1.947 +text {* Alternative version with a syntactic notion of constant polynomial. *}
1.948 +
1.949 +lemma fundamental_theorem_of_algebra_alt:
1.950 +  assumes nc: "~(\<exists>a l. a\<noteq> 0 \<and> list_all(\<lambda>b. b = 0) l \<and> p = a#l)"
1.951 +  shows "\<exists>z. poly p z = (0::complex)"
1.952 +using nc
1.953 +proof(induct p)
1.954 +  case (Cons c cs)
1.955 +  {assume "c=0" hence ?case by auto}
1.956 +  moreover
1.957 +  {assume c0: "c\<noteq>0"
1.958 +    {assume nc: "constant (poly (c#cs))"
1.959 +      from nc[unfolded constant_def, rule_format, of 0]
1.960 +      have "\<forall>w. w \<noteq> 0 \<longrightarrow> poly cs w = 0" by auto
1.961 +      hence "list_all (\<lambda>c. c=0) cs"
1.962 +	proof(induct cs)
1.963 +	  case (Cons d ds)
1.964 +	  {assume "d=0" hence ?case using Cons.prems Cons.hyps by simp}
1.965 +	  moreover
1.966 +	  {assume d0: "d\<noteq>0"
1.967 +	    from poly_bound_exists[of 1 ds] obtain m where
1.968 +	      m: "m > 0" "\<forall>z. \<forall>z. cmod z \<le> 1 \<longrightarrow> cmod (poly ds z) \<le> m" by blast
1.969 +	    have dm: "cmod d / m > 0" using d0 m(1) by (simp add: field_simps)
1.970 +	    from real_down2[OF dm zero_less_one] obtain x where
1.971 +	      x: "x > 0" "x < cmod d / m" "x < 1" by blast
1.972 +	    let ?x = "complex_of_real x"
1.973 +	    from x have cx: "?x \<noteq> 0"  "cmod ?x \<le> 1" by simp_all
1.974 +	    from Cons.prems[rule_format, OF cx(1)]
1.975 +	    have cth: "cmod (?x*poly ds ?x) = cmod d" by (simp add: eq_diff_eq[symmetric])
1.976 +	    from m(2)[rule_format, OF cx(2)] x(1)
1.977 +	    have th0: "cmod (?x*poly ds ?x) \<le> x*m"
1.978 +	      by (simp add: cmod_mult)
1.979 +	    from x(2) m(1) have "x*m < cmod d" by (simp add: field_simps)
1.980 +	    with th0 have "cmod (?x*poly ds ?x) \<noteq> cmod d" by auto
1.981 +	    with cth  have ?case by blast}
1.982 +	  ultimately show ?case by blast
1.983 +	qed simp}
1.984 +      then have nc: "\<not> constant (poly (c#cs))" using Cons.prems c0
1.985 +	by blast
1.986 +      from fundamental_theorem_of_algebra[OF nc] have ?case .}
1.987 +  ultimately show ?case by blast
1.988 +qed simp
1.989 +
1.990 +section{* Nullstellenstatz, degrees and divisibility of polynomials *}
1.991 +
1.992 +lemma nullstellensatz_lemma:
1.993 +  fixes p :: "complex list"
1.994 +  assumes "\<forall>x. poly p x = 0 \<longrightarrow> poly q x = 0"
1.995 +  and "degree p = n" and "n \<noteq> 0"
1.996 +  shows "p divides (pexp q n)"
1.997 +using prems
1.998 +proof(induct n arbitrary: p q rule: nat_less_induct)
1.999 +  fix n::nat fix p q :: "complex list"
1.1000 +  assume IH: "\<forall>m<n. \<forall>p q.
1.1001 +                 (\<forall>x. poly p x = (0::complex) \<longrightarrow> poly q x = 0) \<longrightarrow>
1.1002 +                 degree p = m \<longrightarrow> m \<noteq> 0 \<longrightarrow> p divides (q %^ m)"
1.1003 +    and pq0: "\<forall>x. poly p x = 0 \<longrightarrow> poly q x = 0"
1.1004 +    and dpn: "degree p = n" and n0: "n \<noteq> 0"
1.1005 +  let ?ths = "p divides (q %^ n)"
1.1006 +  {fix a assume a: "poly p a = 0"
1.1007 +    {assume p0: "poly p = poly []"
1.1008 +      hence ?ths unfolding divides_def  using pq0 n0
1.1009 +	apply - apply (rule exI[where x="[]"], rule ext)
1.1010 +	by (auto simp add: poly_mult poly_exp)}
1.1011 +    moreover
1.1012 +    {assume p0: "poly p \<noteq> poly []"
1.1013 +      and oa: "order  a p \<noteq> 0"
1.1014 +      from p0 have pne: "p \<noteq> []" by auto
1.1015 +      let ?op = "order a p"
1.1016 +      from p0 have ap: "([- a, 1] %^ ?op) divides p"
1.1017 +	"\<not> pexp [- a, 1] (Suc ?op) divides p" using order by blast+
1.1018 +      note oop = order_degree[OF p0, unfolded dpn]
1.1019 +      {assume q0: "q = []"
1.1020 +	hence ?ths using n0 unfolding divides_def
1.1021 +	  apply simp
1.1022 +	  apply (rule exI[where x="[]"], rule ext)
1.1023 +	  by (simp add: divides_def poly_exp poly_mult)}
1.1024 +      moreover
1.1025 +      {assume q0: "q\<noteq>[]"
1.1026 +	from pq0[rule_format, OF a, unfolded poly_linear_divides] q0
1.1027 +	obtain r where r: "q = pmult [- a, 1] r" by blast
1.1028 +	from ap[unfolded divides_def] obtain s where
1.1029 +	  s: "poly p = poly (pmult (pexp [- a, 1] ?op) s)" by blast
1.1030 +	have s0: "poly s \<noteq> poly []"
1.1031 +	  using s p0 by (simp add: poly_entire)
1.1032 +	hence pns0: "poly (pnormalize s) \<noteq> poly []" and sne: "s\<noteq>[]" by auto
1.1033 +	{assume ds0: "degree s = 0"
1.1034 +	  from ds0 pns0 have "\<exists>k. pnormalize s = [k]" unfolding degree_def
1.1035 +	    by (cases "pnormalize s", auto)
1.1036 +	  then obtain k where kpn: "pnormalize s = [k]" by blast
1.1037 +	  from pns0[unfolded poly_zero] kpn have k: "k \<noteq>0" "poly s = poly [k]"
1.1038 +	    using poly_normalize[of s] by simp_all
1.1039 +	  let ?w = "pmult (pmult [1/k] (pexp [-a,1] (n - ?op))) (pexp r n)"
1.1040 +	  from k r s oop have "poly (pexp q n) = poly (pmult p ?w)"
1.1042 +	  hence ?ths unfolding divides_def by blast}
1.1043 +	moreover
1.1044 +	{assume ds0: "degree s \<noteq> 0"
1.1045 +	  from ds0 s0 dpn degree_unique[OF s, unfolded linear_pow_mul_degree] oa
1.1046 +	    have dsn: "degree s < n" by auto
1.1047 +	    {fix x assume h: "poly s x = 0"
1.1048 +	      {assume xa: "x = a"
1.1049 +		from h[unfolded xa poly_linear_divides] sne obtain u where
1.1050 +		  u: "s = pmult [- a, 1] u" by blast
1.1051 +		have "poly p = poly (pmult (pexp [- a, 1] (Suc ?op)) u)"
1.1052 +		  unfolding s u
1.1053 +		  apply (rule ext)
1.1055 +		with ap(2)[unfolded divides_def] have False by blast}
1.1056 +	      note xa = this
1.1057 +	      from h s have "poly p x = 0" by (simp add: poly_mult)
1.1058 +	      with pq0 have "poly q x = 0" by blast
1.1059 +	      with r xa have "poly r x = 0"
1.1061 +	    note impth = this
1.1062 +	    from IH[rule_format, OF dsn, of s r] impth ds0
1.1063 +	    have "s divides (pexp r (degree s))" by blast
1.1064 +	    then obtain u where u: "poly (pexp r (degree s)) = poly (pmult s u)"
1.1065 +	      unfolding divides_def by blast
1.1066 +	    hence u': "\<And>x. poly s x * poly u x = poly r x ^ degree s"
1.1067 +	      by (simp add: poly_mult[symmetric] poly_exp[symmetric])
1.1068 +	    let ?w = "pmult (pmult u (pexp [-a,1] (n - ?op))) (pexp r (n - degree s))"
1.1069 +	    from u' s r oop[of a] dsn have "poly (pexp q n) = poly (pmult p ?w)"
1.1070 +	      apply - apply (rule ext)
1.1071 +	      apply (simp only:  power_mult_distrib power_add[symmetric] poly_add poly_mult poly_exp poly_cmult ring_simps)
1.1072 +
1.1074 +	      done
1.1075 +	    hence ?ths unfolding divides_def by blast}
1.1076 +      ultimately have ?ths by blast }
1.1077 +      ultimately have ?ths by blast}
1.1078 +    ultimately have ?ths using a order_root by blast}
1.1079 +  moreover
1.1080 +  {assume exa: "\<not> (\<exists>a. poly p a = 0)"
1.1081 +    from fundamental_theorem_of_algebra_alt[of p] exa obtain c cs where
1.1082 +      ccs: "c\<noteq>0" "list_all (\<lambda>c. c = 0) cs" "p = c#cs" by blast
1.1083 +
1.1084 +    from poly_0[OF ccs(2)] ccs(3)
1.1085 +    have pp: "\<And>x. poly p x =  c" by simp
1.1086 +    let ?w = "pmult [1/c] (pexp q n)"
1.1087 +    from pp ccs(1)
1.1088 +    have "poly (pexp q n) = poly (pmult p ?w) "
1.1089 +      apply - apply (rule ext)
1.1090 +      unfolding poly_mult_assoc[symmetric] by (simp add: poly_mult)
1.1091 +    hence ?ths unfolding divides_def by blast}
1.1092 +  ultimately show ?ths by blast
1.1093 +qed
1.1094 +
1.1095 +lemma nullstellensatz_univariate:
1.1096 +  "(\<forall>x. poly p x = (0::complex) \<longrightarrow> poly q x = 0) \<longleftrightarrow>
1.1097 +    p divides (q %^ (degree p)) \<or> (poly p = poly [] \<and> poly q = poly [])"
1.1098 +proof-
1.1099 +  {assume pe: "poly p = poly []"
1.1100 +    hence eq: "(\<forall>x. poly p x = (0::complex) \<longrightarrow> poly q x = 0) \<longleftrightarrow> poly q = poly []"
1.1101 +      apply auto
1.1102 +      by (rule ext, simp)
1.1103 +    {assume "p divides (pexp q (degree p))"
1.1104 +      then obtain r where r: "poly (pexp q (degree p)) = poly (pmult p r)"
1.1105 +	unfolding divides_def by blast
1.1106 +      from cong[OF r refl] pe degree_unique[OF pe]
1.1107 +      have False by (simp add: poly_mult degree_def)}
1.1108 +    with eq pe have ?thesis by blast}
1.1109 +  moreover
1.1110 +  {assume pe: "poly p \<noteq> poly []"
1.1111 +    have p0: "poly  = poly []" by (rule ext, simp)
1.1112 +    {assume dp: "degree p = 0"
1.1113 +      then obtain k where "pnormalize p = [k]" using pe poly_normalize[of p]
1.1114 +	unfolding degree_def by (cases "pnormalize p", auto)
1.1115 +      hence k: "pnormalize p = [k]" "poly p = poly [k]" "k\<noteq>0"
1.1116 +	using pe poly_normalize[of p] by (auto simp add: p0)
1.1117 +      hence th1: "\<forall>x. poly p x \<noteq> 0" by simp
1.1118 +      from k(2,3) dp have "poly (pexp q (degree p)) = poly (pmult p [1/k]) "
1.1119 +	by - (rule ext, simp add: poly_mult poly_exp)
1.1120 +      hence th2: "p divides (pexp q (degree p))" unfolding divides_def by blast
1.1121 +      from th1 th2 pe have ?thesis by blast}
1.1122 +    moreover
1.1123 +    {assume dp: "degree p \<noteq> 0"
1.1124 +      then obtain n where n: "degree p = Suc n " by (cases "degree p", auto)
1.1125 +      {assume "p divides (pexp q (Suc n))"
1.1126 +	then obtain u where u: "poly (pexp q (Suc n)) = poly (pmult p u)"
1.1127 +	  unfolding divides_def by blast
1.1128 +	hence u' :"\<And>x. poly (pexp q (Suc n)) x = poly (pmult p u) x" by simp_all
1.1129 +	{fix x assume h: "poly p x = 0" "poly q x \<noteq> 0"
1.1130 +	  hence "poly (pexp q (Suc n)) x \<noteq> 0" by (simp only: poly_exp) simp
1.1131 +	  hence False using u' h(1) by (simp only: poly_mult poly_exp) simp}}
1.1132 +	with n nullstellensatz_lemma[of p q "degree p"] dp
1.1133 +	have ?thesis by auto}
1.1134 +    ultimately have ?thesis by blast}
1.1135 +  ultimately show ?thesis by blast
1.1136 +qed
1.1137 +
1.1138 +text{* Useful lemma *}
1.1139 +
1.1140 +lemma (in idom_char_0) constant_degree: "constant (poly p) \<longleftrightarrow> degree p = 0" (is "?lhs = ?rhs")
1.1141 +proof
1.1142 +  assume l: ?lhs
1.1143 +  from l[unfolded constant_def, rule_format, of _ "zero"]
1.1144 +  have th: "poly p = poly [poly p 0]" apply - by (rule ext, simp)
1.1145 +  from degree_unique[OF th] show ?rhs by (simp add: degree_def)
1.1146 +next
1.1147 +  assume r: ?rhs
1.1148 +  from r have "pnormalize p = [] \<or> (\<exists>k. pnormalize p = [k])"
1.1149 +    unfolding degree_def by (cases "pnormalize p", auto)
1.1150 +  then show ?lhs unfolding constant_def poly_normalize[of p, symmetric]
1.1151 +    by (auto simp del: poly_normalize)
1.1152 +qed
1.1153 +
1.1154 +(* It would be nicer to prove this without using algebraic closure...        *)
1.1155 +
1.1156 +lemma divides_degree_lemma: assumes dpn: "degree (p::complex list) = n"
1.1157 +  shows "n \<le> degree (p *** q) \<or> poly (p *** q) = poly []"
1.1158 +  using dpn
1.1159 +proof(induct n arbitrary: p q)
1.1160 +  case 0 thus ?case by simp
1.1161 +next
1.1162 +  case (Suc n p q)
1.1163 +  from Suc.prems fundamental_theorem_of_algebra[of p] constant_degree[of p]
1.1164 +  obtain a where a: "poly p a = 0" by auto
1.1165 +  then obtain r where r: "p = pmult [-a, 1] r" unfolding poly_linear_divides
1.1166 +    using Suc.prems by (auto simp add: degree_def)
1.1167 +  {assume h: "poly (pmult r q) = poly []"
1.1168 +    hence "poly (pmult p q) = poly []" using r
1.1169 +      apply - apply (rule ext)  by (auto simp add: poly_entire poly_mult poly_add poly_cmult) hence ?case by blast}
1.1170 +  moreover
1.1171 +  {assume h: "poly (pmult r q) \<noteq> poly []"
1.1172 +    hence r0: "poly r \<noteq> poly []" and q0: "poly q \<noteq> poly []"
1.1173 +      by (auto simp add: poly_entire)
1.1174 +    have eq: "poly (pmult p q) = poly (pmult [-a, 1] (pmult r q))"
1.1175 +      apply - apply (rule ext)
1.1177 +    from linear_mul_degree[OF h, of "- a"]
1.1178 +    have dqe: "degree (pmult p q) = degree (pmult r q) + 1"
1.1179 +      unfolding degree_unique[OF eq] .
1.1180 +    from linear_mul_degree[OF r0, of "- a", unfolded r[symmetric]] r Suc.prems
1.1181 +    have dr: "degree r = n" by auto
1.1182 +    from  Suc.hyps[OF dr, of q] have "Suc n \<le> degree (pmult p q)"
1.1183 +      unfolding dqe using h by (auto simp del: poly.simps)
1.1184 +    hence ?case by blast}
1.1185 +  ultimately show ?case by blast
1.1186 +qed
1.1187 +
1.1188 +lemma divides_degree: assumes pq: "p divides (q:: complex list)"
1.1189 +  shows "degree p \<le> degree q \<or> poly q = poly []"
1.1190 +using pq  divides_degree_lemma[OF refl, of p]
1.1191 +apply (auto simp add: divides_def poly_entire)
1.1192 +apply atomize
1.1193 +apply (erule_tac x="qa" in allE, auto)
1.1194 +apply (subgoal_tac "degree q = degree (p *** qa)", simp)
1.1195 +apply (rule degree_unique, simp)
1.1196 +done
1.1197 +
1.1198 +(* Arithmetic operations on multivariate polynomials.                        *)
1.1199 +
1.1200 +lemma mpoly_base_conv:
1.1201 +  "(0::complex) \<equiv> poly [] x" "c \<equiv> poly [c] x" "x \<equiv> poly [0,1] x" by simp_all
1.1202 +
1.1203 +lemma mpoly_norm_conv:
1.1204 +  "poly  (x::complex) \<equiv> poly [] x" "poly [poly [] y] x \<equiv> poly [] x" by simp_all
1.1205 +
1.1206 +lemma mpoly_sub_conv:
1.1207 +  "poly p (x::complex) - poly q x \<equiv> poly p x + -1 * poly q x"
1.1208 +  by (simp add: diff_def)
1.1209 +
1.1210 +lemma poly_pad_rule: "poly p x = 0 ==> poly (0#p) x = (0::complex)" by simp
1.1211 +
1.1212 +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
1.1213 +
1.1214 +lemma resolve_eq_raw:  "poly [] x \<equiv> 0" "poly [c] x \<equiv> (c::complex)" by auto
1.1215 +lemma  resolve_eq_then: "(P \<Longrightarrow> (Q \<equiv> Q1)) \<Longrightarrow> (\<not>P \<Longrightarrow> (Q \<equiv> Q2))
1.1216 +  \<Longrightarrow> Q \<equiv> P \<and> Q1 \<or> \<not>P\<and> Q2" apply (atomize (full)) by blast
1.1217 +lemma expand_ex_beta_conv: "list_ex P [c] \<equiv> P c" by simp
1.1218 +
1.1220 +  fixes p q :: "complex list"
1.1221 +  assumes pq: "p divides q"
1.1222 +  shows "p divides ((0::complex)#q)"
1.1223 +proof-
1.1224 +  from pq obtain r where r: "poly q = poly (p *** r)" unfolding divides_def by blast
1.1225 +  hence "poly (0#q) = poly (p *** ([0,1] *** r))"
1.1227 +  thus ?thesis unfolding divides_def by blast
1.1228 +qed
1.1229 +
1.1231 +  fixes p q :: "complex list"
1.1232 +  assumes pq: "p divides q"
1.1233 +  shows "p divides (a %* q)"
1.1234 +proof-
1.1235 +  from pq obtain r where r: "poly q = poly (p *** r)" unfolding divides_def by blast
1.1236 +  hence "poly (a %* q) = poly (p *** (a %* r))"
1.1238 +  thus ?thesis unfolding divides_def by blast
1.1239 +qed
1.1240 +
1.1241 +
1.1242 +lemma poly_divides_conv0:
1.1243 +  fixes p :: "complex list"
1.1244 +  assumes lgpq: "length q < length p" and lq:"last p \<noteq> 0"
1.1245 +  shows "p divides q \<equiv> (\<not> (list_ex (\<lambda>c. c \<noteq> 0) q))" (is "?lhs \<equiv> ?rhs")
1.1246 +proof-
1.1247 +  {assume r: ?rhs
1.1248 +    hence eq: "poly q = poly []" unfolding poly_zero
1.1249 +      by (simp add: list_all_iff list_ex_iff)
1.1250 +    hence "poly q = poly (p *** [])" by - (rule ext, simp add: poly_mult)
1.1251 +    hence ?lhs unfolding divides_def  by blast}
1.1252 +  moreover
1.1253 +  {assume l: ?lhs
1.1254 +    have ath: "\<And>lq lp dq::nat. lq < lp ==> lq \<noteq> 0 \<Longrightarrow> dq <= lq - 1 ==> dq < lp - 1"
1.1255 +      by arith
1.1256 +    {assume q0: "length q = 0"
1.1257 +      hence "q = []" by simp
1.1258 +      hence ?rhs by simp}
1.1259 +    moreover
1.1260 +    {assume lgq0: "length q \<noteq> 0"
1.1261 +      from pnormalize_length[of q] have dql: "degree q \<le> length q - 1"
1.1262 +	unfolding degree_def by simp
1.1263 +      from ath[OF lgpq lgq0 dql, unfolded pnormal_degree[OF lq, symmetric]] divides_degree[OF l] have "poly q = poly []" by auto
1.1264 +      hence ?rhs unfolding poly_zero by (simp add: list_all_iff list_ex_iff)}
1.1265 +    ultimately have ?rhs by blast }
1.1266 +  ultimately show "?lhs \<equiv> ?rhs" by - (atomize (full), blast)
1.1267 +qed
1.1268 +
1.1269 +lemma poly_divides_conv1:
1.1270 +  assumes a0: "a\<noteq> (0::complex)" and pp': "(p::complex list) divides p'"
1.1271 +  and qrp': "\<And>x. a * poly q x - poly p' x \<equiv> poly r x"
1.1272 +  shows "p divides q \<equiv> p divides (r::complex list)" (is "?lhs \<equiv> ?rhs")
1.1273 +proof-
1.1274 +  {
1.1275 +  from pp' obtain t where t: "poly p' = poly (p *** t)"
1.1276 +    unfolding divides_def by blast
1.1277 +  {assume l: ?lhs
1.1278 +    then obtain u where u: "poly q = poly (p *** u)" unfolding divides_def by blast
1.1279 +     have "poly r = poly (p *** ((a %* u) +++ (-- t)))"
1.1280 +       using u qrp' t
1.1281 +       by - (rule ext,
1.1283 +     then have ?rhs unfolding divides_def by blast}
1.1284 +  moreover
1.1285 +  {assume r: ?rhs
1.1286 +    then obtain u where u: "poly r = poly (p *** u)" unfolding divides_def by blast
1.1287 +    from u t qrp' a0 have "poly q = poly (p *** ((1/a) %* (u +++ t)))"
1.1288 +      by - (rule ext, atomize (full), simp add: poly_mult poly_add poly_cmult field_simps)
1.1289 +    hence ?lhs  unfolding divides_def by blast}
1.1290 +  ultimately have "?lhs = ?rhs" by blast }
1.1291 +thus "?lhs \<equiv> ?rhs"  by - (atomize(full), blast)
1.1292 +qed
1.1293 +
1.1294 +lemma basic_cqe_conv1:
1.1295 +  "(\<exists>x. poly p x = 0 \<and> poly [] x \<noteq> 0) \<equiv> False"
1.1296 +  "(\<exists>x. poly [] x \<noteq> 0) \<equiv> False"
1.1297 +  "(\<exists>x. poly [c] x \<noteq> 0) \<equiv> c\<noteq>0"
1.1298 +  "(\<exists>x. poly [] x = 0) \<equiv> True"
1.1299 +  "(\<exists>x. poly [c] x = 0) \<equiv> c = 0" by simp_all
1.1300 +
1.1301 +lemma basic_cqe_conv2:
1.1302 +  assumes l:"last (a#b#p) \<noteq> 0"
1.1303 +  shows "(\<exists>x. poly (a#b#p) x = (0::complex)) \<equiv> True"
1.1304 +proof-
1.1305 +  {fix h t
1.1306 +    assume h: "h\<noteq>0" "list_all (\<lambda>c. c=(0::complex)) t"  "a#b#p = h#t"
1.1307 +    hence "list_all (\<lambda>c. c= 0) (b#p)" by simp
1.1308 +    moreover have "last (b#p) \<in> set (b#p)" by simp
1.1309 +    ultimately have "last (b#p) = 0" by (simp add: list_all_iff)
1.1310 +    with l have False by simp}
1.1311 +  hence th: "\<not> (\<exists> h t. h\<noteq>0 \<and> list_all (\<lambda>c. c=0) t \<and> a#b#p = h#t)"
1.1312 +    by blast
1.1313 +  from fundamental_theorem_of_algebra_alt[OF th]
1.1314 +  show "(\<exists>x. poly (a#b#p) x = (0::complex)) \<equiv> True" by auto
1.1315 +qed
1.1316 +
1.1317 +lemma  basic_cqe_conv_2b: "(\<exists>x. poly p x \<noteq> (0::complex)) \<equiv> (list_ex (\<lambda>c. c \<noteq> 0) p)"
1.1318 +proof-
1.1319 +  have "\<not> (list_ex (\<lambda>c. c \<noteq> 0) p) \<longleftrightarrow> poly p = poly []"
1.1320 +    by (simp add: poly_zero list_all_iff list_ex_iff)
1.1321 +  also have "\<dots> \<longleftrightarrow> (\<not> (\<exists>x. poly p x \<noteq> 0))" by (auto intro: ext)
1.1322 +  finally show "(\<exists>x. poly p x \<noteq> (0::complex)) \<equiv> (list_ex (\<lambda>c. c \<noteq> 0) p)"
1.1323 +    by - (atomize (full), blast)
1.1324 +qed
1.1325 +
1.1326 +lemma basic_cqe_conv3:
1.1327 +  fixes p q :: "complex list"
1.1328 +  assumes l: "last (a#p) \<noteq> 0"
1.1329 +  shows "(\<exists>x. poly (a#p) x =0 \<and> poly q x \<noteq> 0) \<equiv> \<not> ((a#p) divides (q %^ (length p)))"
1.1330 +proof-
1.1331 +  note np = pnormalize_eq[OF l]
1.1332 +  {assume "poly (a#p) = poly []" hence False using l
1.1333 +      unfolding poly_zero apply (auto simp add: list_all_iff del: last.simps)
1.1334 +      apply (cases p, simp_all) done}
1.1335 +  then have p0: "poly (a#p) \<noteq> poly []"  by blast
1.1336 +  from np have dp:"degree (a#p) = length p" by (simp add: degree_def)
1.1337 +  from nullstellensatz_univariate[of "a#p" q] p0 dp
1.1338 +  show "(\<exists>x. poly (a#p) x =0 \<and> poly q x \<noteq> 0) \<equiv> \<not> ((a#p) divides (q %^ (length p)))"
1.1339 +    by - (atomize (full), auto)
1.1340 +qed
1.1341 +
1.1342 +lemma basic_cqe_conv4:
1.1343 +  fixes p q :: "complex list"
1.1344 +  assumes h: "\<And>x. poly (q %^ n) x \<equiv> poly r x"
1.1345 +  shows "p divides (q %^ n) \<equiv> p divides r"
1.1346 +proof-
1.1347 +  from h have "poly (q %^ n) = poly r" by (auto intro: ext)
1.1348 +  thus "p divides (q %^ n) \<equiv> p divides r" unfolding divides_def by simp
1.1349 +qed
1.1350 +
1.1351 +lemma pmult_Cons_Cons: "((a::complex)#b#p) *** q = (a %*q) +++ (0#((b#p) *** q))"
1.1352 +  by simp
1.1353 +
1.1354 +lemma elim_neg_conv: "- z \<equiv> (-1) * (z::complex)" by simp
1.1355 +lemma eqT_intr: "PROP P \<Longrightarrow> (True \<Longrightarrow> PROP P )" "PROP P \<Longrightarrow> True" by blast+
1.1356 +lemma negate_negate_rule: "Trueprop P \<equiv> \<not> P \<equiv> False" by (atomize (full), auto)
1.1357 +lemma last_simps: "last [x] = x" "last (x#y#ys) = last (y#ys)" by simp_all
1.1358 +lemma length_simps: "length [] = 0" "length (x#y#xs) = length xs + 2" "length [x] = 1" by simp_all
1.1359 +
1.1360 +lemma complex_entire: "(z::complex) \<noteq> 0 \<and> w \<noteq> 0 \<equiv> z*w \<noteq> 0" by simp
1.1361 +lemma resolve_eq_ne: "(P \<equiv> True) \<equiv> (\<not>P \<equiv> False)" "(P \<equiv> False) \<equiv> (\<not>P \<equiv> True)"
1.1362 +  by (atomize (full)) simp_all
1.1363 +lemma cqe_conv1: "poly [] x = 0 \<longleftrightarrow> True"  by simp
1.1364 +lemma cqe_conv2: "(p \<Longrightarrow> (q \<equiv> r)) \<equiv> ((p \<and> q) \<equiv> (p \<and> r))"  (is "?l \<equiv> ?r")
1.1365 +proof
1.1366 +  assume "p \<Longrightarrow> q \<equiv> r" thus "p \<and> q \<equiv> p \<and> r" apply - apply (atomize (full)) by blast
1.1367 +next
1.1368 +  assume "p \<and> q \<equiv> p \<and> r" "p"
1.1369 +  thus "q \<equiv> r" apply - apply (atomize (full)) apply blast done
1.1370 +qed
1.1371 +lemma poly_const_conv: "poly [c] (x::complex) = y \<longleftrightarrow> c = y" by simp
1.1372 +
1.1373 +end
1.1374 \ No newline at end of file
```