A proof a the fundamental theorem of algebra
authorchaieb
Mon Feb 25 11:27:25 2008 +0100 (2008-02-25)
changeset 2612344384b5c4fc0
parent 26122 76cbf193c09d
child 26124 2514f0ade8bc
A proof a the fundamental theorem of algebra
src/HOL/Complex/Fundamental_Theorem_Algebra.thy
     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.9 +header{*Fundamental Theorem of Algebra*}
    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.214 +apply (simp add: nat_rec_0)
   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.664 +  apply (simp add: rcis_mult add_divide_distrib)
   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.1041 +	    by - (rule ext, simp add: poly_mult poly_exp poly_cmult poly_add power_add[symmetric] ring_simps power_mult_distrib[symmetric])
  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.1054 +		  by (simp add: ring_simps power_mult_distrib[symmetric] poly_mult poly_cmult poly_add poly_exp)
  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.1060 +		by (auto simp add: poly_mult poly_add poly_cmult eq_diff_eq[symmetric])}
  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.1073 +	      apply (simp add:  power_mult_distrib power_add[symmetric] poly_add poly_mult poly_exp poly_cmult mult_assoc[symmetric])
  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 [0] = 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.1176 +      by (simp add: r poly_mult poly_add poly_cmult ring_simps)
  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 [0] (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.1219 +lemma poly_divides_pad_rule: 
  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.1226 +    by - (rule ext, simp add: poly_mult poly_cmult poly_add)
  1.1227 +  thus ?thesis unfolding divides_def by blast
  1.1228 +qed
  1.1229 +
  1.1230 +lemma poly_divides_pad_const_rule: 
  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.1237 +    by - (rule ext, simp add: poly_mult poly_cmult poly_add)
  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.1282 +	 simp add: poly_add poly_mult poly_cmult poly_minus ring_simps)
  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