src/HOL/Library/Fundamental_Theorem_Algebra.thy
author paulson <lp15@cam.ac.uk>
Mon Feb 22 14:37:56 2016 +0000 (2016-02-22)
changeset 62379 340738057c8c
parent 62128 3201ddb00097
child 63060 293ede07b775
permissions -rw-r--r--
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
     1 (* Author: Amine Chaieb, TU Muenchen *)
     2 
     3 section \<open>Fundamental Theorem of Algebra\<close>
     4 
     5 theory Fundamental_Theorem_Algebra
     6 imports Polynomial Complex_Main
     7 begin
     8 
     9 subsection \<open>More lemmas about module of complex numbers\<close>
    10 
    11 text \<open>The triangle inequality for cmod\<close>
    12 
    13 lemma complex_mod_triangle_sub: "cmod w \<le> cmod (w + z) + norm z"
    14   using complex_mod_triangle_ineq2[of "w + z" "-z"] by auto
    15 
    16 
    17 subsection \<open>Basic lemmas about polynomials\<close>
    18 
    19 lemma poly_bound_exists:
    20   fixes p :: "'a::{comm_semiring_0,real_normed_div_algebra} poly"
    21   shows "\<exists>m. m > 0 \<and> (\<forall>z. norm z \<le> r \<longrightarrow> norm (poly p z) \<le> m)"
    22 proof (induct p)
    23   case 0
    24   then show ?case by (rule exI[where x=1]) simp
    25 next
    26   case (pCons c cs)
    27   from pCons.hyps obtain m where m: "\<forall>z. norm z \<le> r \<longrightarrow> norm (poly cs z) \<le> m"
    28     by blast
    29   let ?k = " 1 + norm c + \<bar>r * m\<bar>"
    30   have kp: "?k > 0"
    31     using abs_ge_zero[of "r*m"] norm_ge_zero[of c] by arith
    32   have "norm (poly (pCons c cs) z) \<le> ?k" if H: "norm z \<le> r" for z
    33   proof -
    34     from m H have th: "norm (poly cs z) \<le> m"
    35       by blast
    36     from H have rp: "r \<ge> 0"
    37       using norm_ge_zero[of z] by arith
    38     have "norm (poly (pCons c cs) z) \<le> norm c + norm (z * poly cs z)"
    39       using norm_triangle_ineq[of c "z* poly cs z"] by simp
    40     also have "\<dots> \<le> norm c + r * m"
    41       using mult_mono[OF H th rp norm_ge_zero[of "poly cs z"]]
    42       by (simp add: norm_mult)
    43     also have "\<dots> \<le> ?k"
    44       by simp
    45     finally show ?thesis .
    46   qed
    47   with kp show ?case by blast
    48 qed
    49 
    50 
    51 text \<open>Offsetting the variable in a polynomial gives another of same degree\<close>
    52 
    53 definition offset_poly :: "'a::comm_semiring_0 poly \<Rightarrow> 'a \<Rightarrow> 'a poly"
    54   where "offset_poly p h = fold_coeffs (\<lambda>a q. smult h q + pCons a q) p 0"
    55 
    56 lemma offset_poly_0: "offset_poly 0 h = 0"
    57   by (simp add: offset_poly_def)
    58 
    59 lemma offset_poly_pCons:
    60   "offset_poly (pCons a p) h =
    61     smult h (offset_poly p h) + pCons a (offset_poly p h)"
    62   by (cases "p = 0 \<and> a = 0") (auto simp add: offset_poly_def)
    63 
    64 lemma offset_poly_single: "offset_poly [:a:] h = [:a:]"
    65   by (simp add: offset_poly_pCons offset_poly_0)
    66 
    67 lemma poly_offset_poly: "poly (offset_poly p h) x = poly p (h + x)"
    68   apply (induct p)
    69   apply (simp add: offset_poly_0)
    70   apply (simp add: offset_poly_pCons algebra_simps)
    71   done
    72 
    73 lemma offset_poly_eq_0_lemma: "smult c p + pCons a p = 0 \<Longrightarrow> p = 0"
    74   by (induct p arbitrary: a) (simp, force)
    75 
    76 lemma offset_poly_eq_0_iff: "offset_poly p h = 0 \<longleftrightarrow> p = 0"
    77   apply (safe intro!: offset_poly_0)
    78   apply (induct p)
    79   apply simp
    80   apply (simp add: offset_poly_pCons)
    81   apply (frule offset_poly_eq_0_lemma, simp)
    82   done
    83 
    84 lemma degree_offset_poly: "degree (offset_poly p h) = degree p"
    85   apply (induct p)
    86   apply (simp add: offset_poly_0)
    87   apply (case_tac "p = 0")
    88   apply (simp add: offset_poly_0 offset_poly_pCons)
    89   apply (simp add: offset_poly_pCons)
    90   apply (subst degree_add_eq_right)
    91   apply (rule le_less_trans [OF degree_smult_le])
    92   apply (simp add: offset_poly_eq_0_iff)
    93   apply (simp add: offset_poly_eq_0_iff)
    94   done
    95 
    96 definition "psize p = (if p = 0 then 0 else Suc (degree p))"
    97 
    98 lemma psize_eq_0_iff [simp]: "psize p = 0 \<longleftrightarrow> p = 0"
    99   unfolding psize_def by simp
   100 
   101 lemma poly_offset:
   102   fixes p :: "'a::comm_ring_1 poly"
   103   shows "\<exists>q. psize q = psize p \<and> (\<forall>x. poly q x = poly p (a + x))"
   104 proof (intro exI conjI)
   105   show "psize (offset_poly p a) = psize p"
   106     unfolding psize_def
   107     by (simp add: offset_poly_eq_0_iff degree_offset_poly)
   108   show "\<forall>x. poly (offset_poly p a) x = poly p (a + x)"
   109     by (simp add: poly_offset_poly)
   110 qed
   111 
   112 text \<open>An alternative useful formulation of completeness of the reals\<close>
   113 lemma real_sup_exists:
   114   assumes ex: "\<exists>x. P x"
   115     and bz: "\<exists>z. \<forall>x. P x \<longrightarrow> x < z"
   116   shows "\<exists>s::real. \<forall>y. (\<exists>x. P x \<and> y < x) \<longleftrightarrow> y < s"
   117 proof
   118   from bz have "bdd_above (Collect P)"
   119     by (force intro: less_imp_le)
   120   then show "\<forall>y. (\<exists>x. P x \<and> y < x) \<longleftrightarrow> y < Sup (Collect P)"
   121     using ex bz by (subst less_cSup_iff) auto
   122 qed
   123 
   124 
   125 subsection \<open>Fundamental theorem of algebra\<close>
   126 
   127 lemma unimodular_reduce_norm:
   128   assumes md: "cmod z = 1"
   129   shows "cmod (z + 1) < 1 \<or> cmod (z - 1) < 1 \<or> cmod (z + ii) < 1 \<or> cmod (z - ii) < 1"
   130 proof -
   131   obtain x y where z: "z = Complex x y "
   132     by (cases z) auto
   133   from md z have xy: "x\<^sup>2 + y\<^sup>2 = 1"
   134     by (simp add: cmod_def)
   135   have False if "cmod (z + 1) \<ge> 1" "cmod (z - 1) \<ge> 1" "cmod (z + ii) \<ge> 1" "cmod (z - ii) \<ge> 1"
   136   proof -
   137     from that z xy have "2 * x \<le> 1" "2 * x \<ge> -1" "2 * y \<le> 1" "2 * y \<ge> -1"
   138       by (simp_all add: cmod_def power2_eq_square algebra_simps)
   139     then have "\<bar>2 * x\<bar> \<le> 1" "\<bar>2 * y\<bar> \<le> 1"
   140       by simp_all
   141     then have "\<bar>2 * x\<bar>\<^sup>2 \<le> 1\<^sup>2" "\<bar>2 * y\<bar>\<^sup>2 \<le> 1\<^sup>2"
   142       by - (rule power_mono, simp, simp)+
   143     then have th0: "4 * x\<^sup>2 \<le> 1" "4 * y\<^sup>2 \<le> 1"
   144       by (simp_all add: power_mult_distrib)
   145     from add_mono[OF th0] xy show ?thesis
   146       by simp
   147   qed
   148   then show ?thesis
   149     unfolding linorder_not_le[symmetric] by blast
   150 qed
   151 
   152 text \<open>Hence we can always reduce modulus of \<open>1 + b z^n\<close> if nonzero\<close>
   153 lemma reduce_poly_simple:
   154   assumes b: "b \<noteq> 0"
   155     and n: "n \<noteq> 0"
   156   shows "\<exists>z. cmod (1 + b * z^n) < 1"
   157   using n
   158 proof (induct n rule: nat_less_induct)
   159   fix n
   160   assume IH: "\<forall>m<n. m \<noteq> 0 \<longrightarrow> (\<exists>z. cmod (1 + b * z ^ m) < 1)"
   161   assume n: "n \<noteq> 0"
   162   let ?P = "\<lambda>z n. cmod (1 + b * z ^ n) < 1"
   163   show "\<exists>z. ?P z n"
   164   proof cases
   165     assume "even n"
   166     then have "\<exists>m. n = 2 * m"
   167       by presburger
   168     then obtain m where m: "n = 2 * m"
   169       by blast
   170     from n m have "m \<noteq> 0" "m < n"
   171       by presburger+
   172     with IH[rule_format, of m] obtain z where z: "?P z m"
   173       by blast
   174     from z have "?P (csqrt z) n"
   175       by (simp add: m power_mult)
   176     then show ?thesis ..
   177   next
   178     assume "odd n"
   179     then have "\<exists>m. n = Suc (2 * m)"
   180       by presburger+
   181     then obtain m where m: "n = Suc (2 * m)"
   182       by blast
   183     have th0: "cmod (complex_of_real (cmod b) / b) = 1"
   184       using b by (simp add: norm_divide)
   185     from unimodular_reduce_norm[OF th0] \<open>odd n\<close>
   186     have "\<exists>v. cmod (complex_of_real (cmod b) / b + v^n) < 1"
   187       apply (cases "cmod (complex_of_real (cmod b) / b + 1) < 1")
   188       apply (rule_tac x="1" in exI)
   189       apply simp
   190       apply (cases "cmod (complex_of_real (cmod b) / b - 1) < 1")
   191       apply (rule_tac x="-1" in exI)
   192       apply simp
   193       apply (cases "cmod (complex_of_real (cmod b) / b + ii) < 1")
   194       apply (cases "even m")
   195       apply (rule_tac x="ii" in exI)
   196       apply (simp add: m power_mult)
   197       apply (rule_tac x="- ii" in exI)
   198       apply (simp add: m power_mult)
   199       apply (cases "even m")
   200       apply (rule_tac x="- ii" in exI)
   201       apply (simp add: m power_mult)
   202       apply (auto simp add: m power_mult)
   203       apply (rule_tac x="ii" in exI)
   204       apply (auto simp add: m power_mult)
   205       done
   206     then obtain v where v: "cmod (complex_of_real (cmod b) / b + v^n) < 1"
   207       by blast
   208     let ?w = "v / complex_of_real (root n (cmod b))"
   209     from odd_real_root_pow[OF \<open>odd n\<close>, of "cmod b"]
   210     have th1: "?w ^ n = v^n / complex_of_real (cmod b)"
   211       by (simp add: power_divide of_real_power[symmetric])
   212     have th2:"cmod (complex_of_real (cmod b) / b) = 1"
   213       using b by (simp add: norm_divide)
   214     then have th3: "cmod (complex_of_real (cmod b) / b) \<ge> 0"
   215       by simp
   216     have th4: "cmod (complex_of_real (cmod b) / b) *
   217         cmod (1 + b * (v ^ n / complex_of_real (cmod b))) <
   218         cmod (complex_of_real (cmod b) / b) * 1"
   219       apply (simp only: norm_mult[symmetric] distrib_left)
   220       using b v
   221       apply (simp add: th2)
   222       done
   223     from mult_left_less_imp_less[OF th4 th3]
   224     have "?P ?w n" unfolding th1 .
   225     then show ?thesis ..
   226   qed
   227 qed
   228 
   229 text \<open>Bolzano-Weierstrass type property for closed disc in complex plane.\<close>
   230 
   231 lemma metric_bound_lemma: "cmod (x - y) \<le> \<bar>Re x - Re y\<bar> + \<bar>Im x - Im y\<bar>"
   232   using real_sqrt_sum_squares_triangle_ineq[of "Re x - Re y" 0 0 "Im x - Im y"]
   233   unfolding cmod_def by simp
   234 
   235 lemma bolzano_weierstrass_complex_disc:
   236   assumes r: "\<forall>n. cmod (s n) \<le> r"
   237   shows "\<exists>f z. subseq f \<and> (\<forall>e >0. \<exists>N. \<forall>n \<ge> N. cmod (s (f n) - z) < e)"
   238 proof -
   239   from seq_monosub[of "Re \<circ> s"]
   240   obtain f where f: "subseq f" "monoseq (\<lambda>n. Re (s (f n)))"
   241     unfolding o_def by blast
   242   from seq_monosub[of "Im \<circ> s \<circ> f"]
   243   obtain g where g: "subseq g" "monoseq (\<lambda>n. Im (s (f (g n))))"
   244     unfolding o_def by blast
   245   let ?h = "f \<circ> g"
   246   from r[rule_format, of 0] have rp: "r \<ge> 0"
   247     using norm_ge_zero[of "s 0"] by arith
   248   have th: "\<forall>n. r + 1 \<ge> \<bar>Re (s n)\<bar>"
   249   proof
   250     fix n
   251     from abs_Re_le_cmod[of "s n"] r[rule_format, of n]
   252     show "\<bar>Re (s n)\<bar> \<le> r + 1" by arith
   253   qed
   254   have conv1: "convergent (\<lambda>n. Re (s (f n)))"
   255     apply (rule Bseq_monoseq_convergent)
   256     apply (simp add: Bseq_def)
   257     apply (metis gt_ex le_less_linear less_trans order.trans th)
   258     apply (rule f(2))
   259     done
   260   have th: "\<forall>n. r + 1 \<ge> \<bar>Im (s n)\<bar>"
   261   proof
   262     fix n
   263     from abs_Im_le_cmod[of "s n"] r[rule_format, of n]
   264     show "\<bar>Im (s n)\<bar> \<le> r + 1"
   265       by arith
   266   qed
   267 
   268   have conv2: "convergent (\<lambda>n. Im (s (f (g n))))"
   269     apply (rule Bseq_monoseq_convergent)
   270     apply (simp add: Bseq_def)
   271     apply (metis gt_ex le_less_linear less_trans order.trans th)
   272     apply (rule g(2))
   273     done
   274 
   275   from conv1[unfolded convergent_def] obtain x where "LIMSEQ (\<lambda>n. Re (s (f n))) x"
   276     by blast
   277   then have x: "\<forall>r>0. \<exists>n0. \<forall>n\<ge>n0. \<bar>Re (s (f n)) - x\<bar> < r"
   278     unfolding LIMSEQ_iff real_norm_def .
   279 
   280   from conv2[unfolded convergent_def] obtain y where "LIMSEQ (\<lambda>n. Im (s (f (g n)))) y"
   281     by blast
   282   then have y: "\<forall>r>0. \<exists>n0. \<forall>n\<ge>n0. \<bar>Im (s (f (g n))) - y\<bar> < r"
   283     unfolding LIMSEQ_iff real_norm_def .
   284   let ?w = "Complex x y"
   285   from f(1) g(1) have hs: "subseq ?h"
   286     unfolding subseq_def by auto
   287   have "\<exists>N. \<forall>n\<ge>N. cmod (s (?h n) - ?w) < e" if "e > 0" for e
   288   proof -
   289     from that have e2: "e/2 > 0"
   290       by simp
   291     from x[rule_format, OF e2] y[rule_format, OF e2]
   292     obtain N1 N2 where N1: "\<forall>n\<ge>N1. \<bar>Re (s (f n)) - x\<bar> < e / 2"
   293       and N2: "\<forall>n\<ge>N2. \<bar>Im (s (f (g n))) - y\<bar> < e / 2"
   294       by blast
   295     have "cmod (s (?h n) - ?w) < e" if "n \<ge> N1 + N2" for n
   296     proof -
   297       from that have nN1: "g n \<ge> N1" and nN2: "n \<ge> N2"
   298         using seq_suble[OF g(1), of n] by arith+
   299       from add_strict_mono[OF N1[rule_format, OF nN1] N2[rule_format, OF nN2]]
   300       show ?thesis
   301         using metric_bound_lemma[of "s (f (g n))" ?w] by simp
   302     qed
   303     then show ?thesis by blast
   304   qed
   305   with hs show ?thesis by blast
   306 qed
   307 
   308 text \<open>Polynomial is continuous.\<close>
   309 
   310 lemma poly_cont:
   311   fixes p :: "'a::{comm_semiring_0,real_normed_div_algebra} poly"
   312   assumes ep: "e > 0"
   313   shows "\<exists>d >0. \<forall>w. 0 < norm (w - z) \<and> norm (w - z) < d \<longrightarrow> norm (poly p w - poly p z) < e"
   314 proof -
   315   obtain q where q: "degree q = degree p" "\<And>x. poly q x = poly p (z + x)"
   316   proof
   317     show "degree (offset_poly p z) = degree p"
   318       by (rule degree_offset_poly)
   319     show "\<And>x. poly (offset_poly p z) x = poly p (z + x)"
   320       by (rule poly_offset_poly)
   321   qed
   322   have th: "\<And>w. poly q (w - z) = poly p w"
   323     using q(2)[of "w - z" for w] by simp
   324   show ?thesis unfolding th[symmetric]
   325   proof (induct q)
   326     case 0
   327     then show ?case
   328       using ep by auto
   329   next
   330     case (pCons c cs)
   331     from poly_bound_exists[of 1 "cs"]
   332     obtain m where m: "m > 0" "\<And>z. norm z \<le> 1 \<Longrightarrow> norm (poly cs z) \<le> m"
   333       by blast
   334     from ep m(1) have em0: "e/m > 0"
   335       by (simp add: field_simps)
   336     have one0: "1 > (0::real)"
   337       by arith
   338     from real_lbound_gt_zero[OF one0 em0]
   339     obtain d where d: "d > 0" "d < 1" "d < e / m"
   340       by blast
   341     from d(1,3) m(1) have dm: "d * m > 0" "d * m < e"
   342       by (simp_all add: field_simps)
   343     show ?case
   344     proof (rule ex_forward[OF real_lbound_gt_zero[OF one0 em0]], clarsimp simp add: norm_mult)
   345       fix d w
   346       assume H: "d > 0" "d < 1" "d < e/m" "w \<noteq> z" "norm (w - z) < d"
   347       then have d1: "norm (w-z) \<le> 1" "d \<ge> 0"
   348         by simp_all
   349       from H(3) m(1) have dme: "d*m < e"
   350         by (simp add: field_simps)
   351       from H have th: "norm (w - z) \<le> d"
   352         by simp
   353       from mult_mono[OF th m(2)[OF d1(1)] d1(2) norm_ge_zero] dme
   354       show "norm (w - z) * norm (poly cs (w - z)) < e"
   355         by simp
   356     qed
   357   qed
   358 qed
   359 
   360 text \<open>Hence a polynomial attains minimum on a closed disc
   361   in the complex plane.\<close>
   362 lemma poly_minimum_modulus_disc: "\<exists>z. \<forall>w. cmod w \<le> r \<longrightarrow> cmod (poly p z) \<le> cmod (poly p w)"
   363 proof -
   364   show ?thesis
   365   proof (cases "r \<ge> 0")
   366     case False
   367     then show ?thesis
   368       by (metis norm_ge_zero order.trans)
   369   next
   370     case True
   371     then have "cmod 0 \<le> r \<and> cmod (poly p 0) = - (- cmod (poly p 0))"
   372       by simp
   373     then have mth1: "\<exists>x z. cmod z \<le> r \<and> cmod (poly p z) = - x"
   374       by blast
   375     have False if "cmod z \<le> r" "cmod (poly p z) = - x" "\<not> x < 1" for x z
   376     proof -
   377       from that have "- x < 0 "
   378         by arith
   379       with that(2) norm_ge_zero[of "poly p z"] show ?thesis
   380         by simp
   381     qed
   382     then have mth2: "\<exists>z. \<forall>x. (\<exists>z. cmod z \<le> r \<and> cmod (poly p z) = - x) \<longrightarrow> x < z"
   383       by blast
   384     from real_sup_exists[OF mth1 mth2] obtain s where
   385       s: "\<forall>y. (\<exists>x. (\<exists>z. cmod z \<le> r \<and> cmod (poly p z) = - x) \<and> y < x) \<longleftrightarrow> y < s"
   386       by blast
   387     let ?m = "- s"
   388     have s1[unfolded minus_minus]:
   389       "(\<exists>z x. cmod z \<le> r \<and> - (- cmod (poly p z)) < y) \<longleftrightarrow> ?m < y" for y
   390       using s[rule_format, of "-y"]
   391       unfolding minus_less_iff[of y] equation_minus_iff by blast
   392     from s1[of ?m] have s1m: "\<And>z x. cmod z \<le> r \<Longrightarrow> cmod (poly p z) \<ge> ?m"
   393       by auto
   394     have "\<exists>z. cmod z \<le> r \<and> cmod (poly p z) < - s + 1 / real (Suc n)" for n
   395       using s1[rule_format, of "?m + 1/real (Suc n)"] by simp
   396     then have th: "\<forall>n. \<exists>z. cmod z \<le> r \<and> cmod (poly p z) < - s + 1 / real (Suc n)" ..
   397     from choice[OF th] obtain g where
   398         g: "\<forall>n. cmod (g n) \<le> r" "\<forall>n. cmod (poly p (g n)) <?m + 1 /real(Suc n)"
   399       by blast
   400     from bolzano_weierstrass_complex_disc[OF g(1)]
   401     obtain f z where fz: "subseq f" "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. cmod (g (f n) - z) < e"
   402       by blast
   403     {
   404       fix w
   405       assume wr: "cmod w \<le> r"
   406       let ?e = "\<bar>cmod (poly p z) - ?m\<bar>"
   407       {
   408         assume e: "?e > 0"
   409         then have e2: "?e/2 > 0"
   410           by simp
   411         from poly_cont[OF e2, of z p] obtain d where
   412             d: "d > 0" "\<forall>w. 0<cmod (w - z)\<and> cmod(w - z) < d \<longrightarrow> cmod(poly p w - poly p z) < ?e/2"
   413           by blast
   414         have th1: "cmod(poly p w - poly p z) < ?e / 2" if w: "cmod (w - z) < d" for w
   415           using d(2)[rule_format, of w] w e by (cases "w = z") simp_all
   416         from fz(2) d(1) obtain N1 where N1: "\<forall>n\<ge>N1. cmod (g (f n) - z) < d"
   417           by blast
   418         from reals_Archimedean2[of "2/?e"] obtain N2 :: nat where N2: "2/?e < real N2"
   419           by blast
   420         have th2: "cmod (poly p (g (f (N1 + N2))) - poly p z) < ?e/2"
   421           using N1[rule_format, of "N1 + N2"] th1 by simp
   422         have th0: "a < e2 \<Longrightarrow> \<bar>b - m\<bar> < e2 \<Longrightarrow> 2 * e2 \<le> \<bar>b - m\<bar> + a \<Longrightarrow> False"
   423           for a b e2 m :: real
   424           by arith
   425         have ath: "m \<le> x \<Longrightarrow> x < m + e \<Longrightarrow> \<bar>x - m\<bar> < e" for m x e :: real
   426           by arith
   427         from s1m[OF g(1)[rule_format]] have th31: "?m \<le> cmod(poly p (g (f (N1 + N2))))" .
   428         from seq_suble[OF fz(1), of "N1 + N2"]
   429         have th00: "real (Suc (N1 + N2)) \<le> real (Suc (f (N1 + N2)))"
   430           by simp
   431         have th000: "0 \<le> (1::real)" "(1::real) \<le> 1" "real (Suc (N1 + N2)) > 0"
   432           using N2 by auto
   433         from frac_le[OF th000 th00]
   434         have th00: "?m + 1 / real (Suc (f (N1 + N2))) \<le> ?m + 1 / real (Suc (N1 + N2))"
   435           by simp
   436         from g(2)[rule_format, of "f (N1 + N2)"]
   437         have th01:"cmod (poly p (g (f (N1 + N2)))) < - s + 1 / real (Suc (f (N1 + N2)))" .
   438         from order_less_le_trans[OF th01 th00]
   439         have th32: "cmod (poly p (g (f (N1 + N2)))) < ?m + (1/ real(Suc (N1 + N2)))" .
   440         from N2 have "2/?e < real (Suc (N1 + N2))"
   441           by arith
   442         with e2 less_imp_inverse_less[of "2/?e" "real (Suc (N1 + N2))"]
   443         have "?e/2 > 1/ real (Suc (N1 + N2))"
   444           by (simp add: inverse_eq_divide)
   445         with ath[OF th31 th32] have thc1: "\<bar>cmod (poly p (g (f (N1 + N2)))) - ?m\<bar> < ?e/2"
   446           by arith
   447         have ath2: "\<bar>a - b\<bar> \<le> c \<Longrightarrow> \<bar>b - m\<bar> \<le> \<bar>a - m\<bar> + c" for a b c m :: real
   448           by arith
   449         have th22: "\<bar>cmod (poly p (g (f (N1 + N2)))) - cmod (poly p z)\<bar> \<le>
   450             cmod (poly p (g (f (N1 + N2))) - poly p z)"
   451           by (simp add: norm_triangle_ineq3)
   452         from ath2[OF th22, of ?m]
   453         have thc2: "2 * (?e/2) \<le>
   454             \<bar>cmod(poly p (g (f (N1 + N2)))) - ?m\<bar> + cmod (poly p (g (f (N1 + N2))) - poly p z)"
   455           by simp
   456         from th0[OF th2 thc1 thc2] have False .
   457       }
   458       then have "?e = 0"
   459         by auto
   460       then have "cmod (poly p z) = ?m"
   461         by simp
   462       with s1m[OF wr] have "cmod (poly p z) \<le> cmod (poly p w)"
   463         by simp
   464     }
   465     then show ?thesis by blast
   466   qed
   467 qed
   468 
   469 text \<open>Nonzero polynomial in z goes to infinity as z does.\<close>
   470 
   471 lemma poly_infinity:
   472   fixes p:: "'a::{comm_semiring_0,real_normed_div_algebra} poly"
   473   assumes ex: "p \<noteq> 0"
   474   shows "\<exists>r. \<forall>z. r \<le> norm z \<longrightarrow> d \<le> norm (poly (pCons a p) z)"
   475   using ex
   476 proof (induct p arbitrary: a d)
   477   case 0
   478   then show ?case by simp
   479 next
   480   case (pCons c cs a d)
   481   show ?case
   482   proof (cases "cs = 0")
   483     case False
   484     with pCons.hyps obtain r where r: "\<forall>z. r \<le> norm z \<longrightarrow> d + norm a \<le> norm (poly (pCons c cs) z)"
   485       by blast
   486     let ?r = "1 + \<bar>r\<bar>"
   487     have "d \<le> norm (poly (pCons a (pCons c cs)) z)" if "1 + \<bar>r\<bar> \<le> norm z" for z
   488     proof -
   489       have r0: "r \<le> norm z"
   490         using that by arith
   491       from r[rule_format, OF r0] have th0: "d + norm a \<le> 1 * norm(poly (pCons c cs) z)"
   492         by arith
   493       from that have z1: "norm z \<ge> 1"
   494         by arith
   495       from order_trans[OF th0 mult_right_mono[OF z1 norm_ge_zero[of "poly (pCons c cs) z"]]]
   496       have th1: "d \<le> norm(z * poly (pCons c cs) z) - norm a"
   497         unfolding norm_mult by (simp add: algebra_simps)
   498       from norm_diff_ineq[of "z * poly (pCons c cs) z" a]
   499       have th2: "norm (z * poly (pCons c cs) z) - norm a \<le> norm (poly (pCons a (pCons c cs)) z)"
   500         by (simp add: algebra_simps)
   501       from th1 th2 show ?thesis
   502         by arith
   503     qed
   504     then show ?thesis by blast
   505   next
   506     case True
   507     with pCons.prems have c0: "c \<noteq> 0"
   508       by simp
   509     have "d \<le> norm (poly (pCons a (pCons c cs)) z)"
   510       if h: "(\<bar>d\<bar> + norm a) / norm c \<le> norm z" for z :: 'a
   511     proof -
   512       from c0 have "norm c > 0"
   513         by simp
   514       from h c0 have th0: "\<bar>d\<bar> + norm a \<le> norm (z * c)"
   515         by (simp add: field_simps norm_mult)
   516       have ath: "\<And>mzh mazh ma. mzh \<le> mazh + ma \<Longrightarrow> \<bar>d\<bar> + ma \<le> mzh \<Longrightarrow> d \<le> mazh"
   517         by arith
   518       from norm_diff_ineq[of "z * c" a] have th1: "norm (z * c) \<le> norm (a + z * c) + norm a"
   519         by (simp add: algebra_simps)
   520       from ath[OF th1 th0] show ?thesis
   521         using True by simp
   522     qed
   523     then show ?thesis by blast
   524   qed
   525 qed
   526 
   527 text \<open>Hence polynomial's modulus attains its minimum somewhere.\<close>
   528 lemma poly_minimum_modulus: "\<exists>z.\<forall>w. cmod (poly p z) \<le> cmod (poly p w)"
   529 proof (induct p)
   530   case 0
   531   then show ?case by simp
   532 next
   533   case (pCons c cs)
   534   show ?case
   535   proof (cases "cs = 0")
   536     case False
   537     from poly_infinity[OF False, of "cmod (poly (pCons c cs) 0)" c]
   538     obtain r where r: "\<And>z. r \<le> cmod z \<Longrightarrow> cmod (poly (pCons c cs) 0) \<le> cmod (poly (pCons c cs) z)"
   539       by blast
   540     have ath: "\<And>z r. r \<le> cmod z \<or> cmod z \<le> \<bar>r\<bar>"
   541       by arith
   542     from poly_minimum_modulus_disc[of "\<bar>r\<bar>" "pCons c cs"]
   543     obtain v where v: "\<And>w. cmod w \<le> \<bar>r\<bar> \<Longrightarrow> cmod (poly (pCons c cs) v) \<le> cmod (poly (pCons c cs) w)"
   544       by blast
   545     have "cmod (poly (pCons c cs) v) \<le> cmod (poly (pCons c cs) z)" if z: "r \<le> cmod z" for z
   546       using v[of 0] r[OF z] by simp
   547     with v ath[of r] show ?thesis
   548       by blast
   549   next
   550     case True
   551     with pCons.hyps show ?thesis
   552       by simp
   553   qed
   554 qed
   555 
   556 text \<open>Constant function (non-syntactic characterization).\<close>
   557 definition "constant f \<longleftrightarrow> (\<forall>x y. f x = f y)"
   558 
   559 lemma nonconstant_length: "\<not> constant (poly p) \<Longrightarrow> psize p \<ge> 2"
   560   by (induct p) (auto simp: constant_def psize_def)
   561 
   562 lemma poly_replicate_append: "poly (monom 1 n * p) (x::'a::comm_ring_1) = x^n * poly p x"
   563   by (simp add: poly_monom)
   564 
   565 text \<open>Decomposition of polynomial, skipping zero coefficients after the first.\<close>
   566 
   567 lemma poly_decompose_lemma:
   568   assumes nz: "\<not> (\<forall>z. z \<noteq> 0 \<longrightarrow> poly p z = (0::'a::idom))"
   569   shows "\<exists>k a q. a \<noteq> 0 \<and> Suc (psize q + k) = psize p \<and> (\<forall>z. poly p z = z^k * poly (pCons a q) z)"
   570   unfolding psize_def
   571   using nz
   572 proof (induct p)
   573   case 0
   574   then show ?case by simp
   575 next
   576   case (pCons c cs)
   577   show ?case
   578   proof (cases "c = 0")
   579     case True
   580     from pCons.hyps pCons.prems True show ?thesis
   581       apply auto
   582       apply (rule_tac x="k+1" in exI)
   583       apply (rule_tac x="a" in exI)
   584       apply clarsimp
   585       apply (rule_tac x="q" in exI)
   586       apply auto
   587       done
   588   next
   589     case False
   590     show ?thesis
   591       apply (rule exI[where x=0])
   592       apply (rule exI[where x=c])
   593       apply (auto simp: False)
   594       done
   595   qed
   596 qed
   597 
   598 lemma poly_decompose:
   599   assumes nc: "\<not> constant (poly p)"
   600   shows "\<exists>k a q. a \<noteq> (0::'a::idom) \<and> k \<noteq> 0 \<and>
   601                psize q + k + 1 = psize p \<and>
   602               (\<forall>z. poly p z = poly p 0 + z^k * poly (pCons a q) z)"
   603   using nc
   604 proof (induct p)
   605   case 0
   606   then show ?case
   607     by (simp add: constant_def)
   608 next
   609   case (pCons c cs)
   610   have "\<not> (\<forall>z. z \<noteq> 0 \<longrightarrow> poly cs z = 0)"
   611   proof
   612     assume "\<forall>z. z \<noteq> 0 \<longrightarrow> poly cs z = 0"
   613     then have "poly (pCons c cs) x = poly (pCons c cs) y" for x y
   614       by (cases "x = 0") auto
   615     with pCons.prems show False
   616       by (auto simp add: constant_def)
   617   qed
   618   from poly_decompose_lemma[OF this]
   619   show ?case
   620     apply clarsimp
   621     apply (rule_tac x="k+1" in exI)
   622     apply (rule_tac x="a" in exI)
   623     apply simp
   624     apply (rule_tac x="q" in exI)
   625     apply (auto simp add: psize_def split: if_splits)
   626     done
   627 qed
   628 
   629 text \<open>Fundamental theorem of algebra\<close>
   630 
   631 lemma fundamental_theorem_of_algebra:
   632   assumes nc: "\<not> constant (poly p)"
   633   shows "\<exists>z::complex. poly p z = 0"
   634   using nc
   635 proof (induct "psize p" arbitrary: p rule: less_induct)
   636   case less
   637   let ?p = "poly p"
   638   let ?ths = "\<exists>z. ?p z = 0"
   639 
   640   from nonconstant_length[OF less(2)] have n2: "psize p \<ge> 2" .
   641   from poly_minimum_modulus obtain c where c: "\<forall>w. cmod (?p c) \<le> cmod (?p w)"
   642     by blast
   643 
   644   show ?ths
   645   proof (cases "?p c = 0")
   646     case True
   647     then show ?thesis by blast
   648   next
   649     case False
   650     from poly_offset[of p c] obtain q where q: "psize q = psize p" "\<forall>x. poly q x = ?p (c + x)"
   651       by blast
   652     have False if h: "constant (poly q)"
   653     proof -
   654       from q(2) have th: "\<forall>x. poly q (x - c) = ?p x"
   655         by auto
   656       have "?p x = ?p y" for x y
   657       proof -
   658         from th have "?p x = poly q (x - c)"
   659           by auto
   660         also have "\<dots> = poly q (y - c)"
   661           using h unfolding constant_def by blast
   662         also have "\<dots> = ?p y"
   663           using th by auto
   664         finally show ?thesis .
   665       qed
   666       with less(2) show ?thesis
   667         unfolding constant_def by blast
   668     qed
   669     then have qnc: "\<not> constant (poly q)"
   670       by blast
   671     from q(2) have pqc0: "?p c = poly q 0"
   672       by simp
   673     from c pqc0 have cq0: "\<forall>w. cmod (poly q 0) \<le> cmod (?p w)"
   674       by simp
   675     let ?a0 = "poly q 0"
   676     from False pqc0 have a00: "?a0 \<noteq> 0"
   677       by simp
   678     from a00 have qr: "\<forall>z. poly q z = poly (smult (inverse ?a0) q) z * ?a0"
   679       by simp
   680     let ?r = "smult (inverse ?a0) q"
   681     have lgqr: "psize q = psize ?r"
   682       using a00
   683       unfolding psize_def degree_def
   684       by (simp add: poly_eq_iff)
   685     have False if h: "\<And>x y. poly ?r x = poly ?r y"
   686     proof -
   687       have "poly q x = poly q y" for x y
   688       proof -
   689         from qr[rule_format, of x] have "poly q x = poly ?r x * ?a0"
   690           by auto
   691         also have "\<dots> = poly ?r y * ?a0"
   692           using h by simp
   693         also have "\<dots> = poly q y"
   694           using qr[rule_format, of y] by simp
   695         finally show ?thesis .
   696       qed
   697       with qnc show ?thesis
   698         unfolding constant_def by blast
   699     qed
   700     then have rnc: "\<not> constant (poly ?r)"
   701       unfolding constant_def by blast
   702     from qr[rule_format, of 0] a00 have r01: "poly ?r 0 = 1"
   703       by auto
   704     have mrmq_eq: "cmod (poly ?r w) < 1 \<longleftrightarrow> cmod (poly q w) < cmod ?a0" for w
   705     proof -
   706       have "cmod (poly ?r w) < 1 \<longleftrightarrow> cmod (poly q w / ?a0) < 1"
   707         using qr[rule_format, of w] a00 by (simp add: divide_inverse ac_simps)
   708       also have "\<dots> \<longleftrightarrow> cmod (poly q w) < cmod ?a0"
   709         using a00 unfolding norm_divide by (simp add: field_simps)
   710       finally show ?thesis .
   711     qed
   712     from poly_decompose[OF rnc] obtain k a s where
   713       kas: "a \<noteq> 0" "k \<noteq> 0" "psize s + k + 1 = psize ?r"
   714         "\<forall>z. poly ?r z = poly ?r 0 + z^k* poly (pCons a s) z" by blast
   715     have "\<exists>w. cmod (poly ?r w) < 1"
   716     proof (cases "psize p = k + 1")
   717       case True
   718       with kas(3) lgqr[symmetric] q(1) have s0: "s = 0"
   719         by auto
   720       have hth[symmetric]: "cmod (poly ?r w) = cmod (1 + a * w ^ k)" for w
   721         using kas(4)[rule_format, of w] s0 r01 by (simp add: algebra_simps)
   722       from reduce_poly_simple[OF kas(1,2)] show ?thesis
   723         unfolding hth by blast
   724     next
   725       case False note kn = this
   726       from kn kas(3) q(1) lgqr have k1n: "k + 1 < psize p"
   727         by simp
   728       have th01: "\<not> constant (poly (pCons 1 (monom a (k - 1))))"
   729         unfolding constant_def poly_pCons poly_monom
   730         using kas(1)
   731         apply simp
   732         apply (rule exI[where x=0])
   733         apply (rule exI[where x=1])
   734         apply simp
   735         done
   736       from kas(1) kas(2) have th02: "k + 1 = psize (pCons 1 (monom a (k - 1)))"
   737         by (simp add: psize_def degree_monom_eq)
   738       from less(1) [OF k1n [simplified th02] th01]
   739       obtain w where w: "1 + w^k * a = 0"
   740         unfolding poly_pCons poly_monom
   741         using kas(2) by (cases k) (auto simp add: algebra_simps)
   742       from poly_bound_exists[of "cmod w" s] obtain m where
   743         m: "m > 0" "\<forall>z. cmod z \<le> cmod w \<longrightarrow> cmod (poly s z) \<le> m" by blast
   744       have w0: "w \<noteq> 0"
   745         using kas(2) w by (auto simp add: power_0_left)
   746       from w have "(1 + w ^ k * a) - 1 = 0 - 1"
   747         by simp
   748       then have wm1: "w^k * a = - 1"
   749         by simp
   750       have inv0: "0 < inverse (cmod w ^ (k + 1) * m)"
   751         using norm_ge_zero[of w] w0 m(1)
   752         by (simp add: inverse_eq_divide zero_less_mult_iff)
   753       with real_lbound_gt_zero[OF zero_less_one] obtain t where
   754         t: "t > 0" "t < 1" "t < inverse (cmod w ^ (k + 1) * m)" by blast
   755       let ?ct = "complex_of_real t"
   756       let ?w = "?ct * w"
   757       have "1 + ?w^k * (a + ?w * poly s ?w) = 1 + ?ct^k * (w^k * a) + ?w^k * ?w * poly s ?w"
   758         using kas(1) by (simp add: algebra_simps power_mult_distrib)
   759       also have "\<dots> = complex_of_real (1 - t^k) + ?w^k * ?w * poly s ?w"
   760         unfolding wm1 by simp
   761       finally have "cmod (1 + ?w^k * (a + ?w * poly s ?w)) =
   762         cmod (complex_of_real (1 - t^k) + ?w^k * ?w * poly s ?w)"
   763         by metis
   764       with norm_triangle_ineq[of "complex_of_real (1 - t^k)" "?w^k * ?w * poly s ?w"]
   765       have th11: "cmod (1 + ?w^k * (a + ?w * poly s ?w)) \<le> \<bar>1 - t^k\<bar> + cmod (?w^k * ?w * poly s ?w)"
   766         unfolding norm_of_real by simp
   767       have ath: "\<And>x t::real. 0 \<le> x \<Longrightarrow> x < t \<Longrightarrow> t \<le> 1 \<Longrightarrow> \<bar>1 - t\<bar> + x < 1"
   768         by arith
   769       have "t * cmod w \<le> 1 * cmod w"
   770         apply (rule mult_mono)
   771         using t(1,2)
   772         apply auto
   773         done
   774       then have tw: "cmod ?w \<le> cmod w"
   775         using t(1) by (simp add: norm_mult)
   776       from t inv0 have "t * (cmod w ^ (k + 1) * m) < 1"
   777         by (simp add: field_simps)
   778       with zero_less_power[OF t(1), of k] have th30: "t^k * (t* (cmod w ^ (k + 1) * m)) < t^k * 1"
   779         by simp
   780       have "cmod (?w^k * ?w * poly s ?w) = t^k * (t* (cmod w ^ (k + 1) * cmod (poly s ?w)))"
   781         using w0 t(1)
   782         by (simp add: algebra_simps power_mult_distrib norm_power norm_mult)
   783       then have "cmod (?w^k * ?w * poly s ?w) \<le> t^k * (t* (cmod w ^ (k + 1) * m))"
   784         using t(1,2) m(2)[rule_format, OF tw] w0
   785         by auto
   786       with th30 have th120: "cmod (?w^k * ?w * poly s ?w) < t^k"
   787         by simp
   788       from power_strict_mono[OF t(2), of k] t(1) kas(2) have th121: "t^k \<le> 1"
   789         by auto
   790       from ath[OF norm_ge_zero[of "?w^k * ?w * poly s ?w"] th120 th121]
   791       have th12: "\<bar>1 - t^k\<bar> + cmod (?w^k * ?w * poly s ?w) < 1" .
   792       from th11 th12 have "cmod (1 + ?w^k * (a + ?w * poly s ?w)) < 1"
   793         by arith
   794       then have "cmod (poly ?r ?w) < 1"
   795         unfolding kas(4)[rule_format, of ?w] r01 by simp
   796       then show ?thesis
   797         by blast
   798     qed
   799     with cq0 q(2) show ?thesis
   800       unfolding mrmq_eq not_less[symmetric] by auto
   801   qed
   802 qed
   803 
   804 text \<open>Alternative version with a syntactic notion of constant polynomial.\<close>
   805 
   806 lemma fundamental_theorem_of_algebra_alt:
   807   assumes nc: "\<not> (\<exists>a l. a \<noteq> 0 \<and> l = 0 \<and> p = pCons a l)"
   808   shows "\<exists>z. poly p z = (0::complex)"
   809   using nc
   810 proof (induct p)
   811   case 0
   812   then show ?case by simp
   813 next
   814   case (pCons c cs)
   815   show ?case
   816   proof (cases "c = 0")
   817     case True
   818     then show ?thesis by auto
   819   next
   820     case False
   821     have "\<not> constant (poly (pCons c cs))"
   822     proof
   823       assume nc: "constant (poly (pCons c cs))"
   824       from nc[unfolded constant_def, rule_format, of 0]
   825       have "\<forall>w. w \<noteq> 0 \<longrightarrow> poly cs w = 0" by auto
   826       then have "cs = 0"
   827       proof (induct cs)
   828         case 0
   829         then show ?case by simp
   830       next
   831         case (pCons d ds)
   832         show ?case
   833         proof (cases "d = 0")
   834           case True
   835           then show ?thesis
   836             using pCons.prems pCons.hyps by simp
   837         next
   838           case False
   839           from poly_bound_exists[of 1 ds] obtain m where
   840             m: "m > 0" "\<forall>z. \<forall>z. cmod z \<le> 1 \<longrightarrow> cmod (poly ds z) \<le> m" by blast
   841           have dm: "cmod d / m > 0"
   842             using False m(1) by (simp add: field_simps)
   843           from real_lbound_gt_zero[OF dm zero_less_one]
   844           obtain x where x: "x > 0" "x < cmod d / m" "x < 1"
   845             by blast
   846           let ?x = "complex_of_real x"
   847           from x have cx: "?x \<noteq> 0" "cmod ?x \<le> 1"
   848             by simp_all
   849           from pCons.prems[rule_format, OF cx(1)]
   850           have cth: "cmod (?x*poly ds ?x) = cmod d"
   851             by (simp add: eq_diff_eq[symmetric])
   852           from m(2)[rule_format, OF cx(2)] x(1)
   853           have th0: "cmod (?x*poly ds ?x) \<le> x*m"
   854             by (simp add: norm_mult)
   855           from x(2) m(1) have "x * m < cmod d"
   856             by (simp add: field_simps)
   857           with th0 have "cmod (?x*poly ds ?x) \<noteq> cmod d"
   858             by auto
   859           with cth show ?thesis
   860             by blast
   861         qed
   862       qed
   863       then show False
   864         using pCons.prems False by blast
   865     qed
   866     then show ?thesis
   867       by (rule fundamental_theorem_of_algebra)
   868   qed
   869 qed
   870 
   871 
   872 subsection \<open>Nullstellensatz, degrees and divisibility of polynomials\<close>
   873 
   874 lemma nullstellensatz_lemma:
   875   fixes p :: "complex poly"
   876   assumes "\<forall>x. poly p x = 0 \<longrightarrow> poly q x = 0"
   877     and "degree p = n"
   878     and "n \<noteq> 0"
   879   shows "p dvd (q ^ n)"
   880   using assms
   881 proof (induct n arbitrary: p q rule: nat_less_induct)
   882   fix n :: nat
   883   fix p q :: "complex poly"
   884   assume IH: "\<forall>m<n. \<forall>p q.
   885                  (\<forall>x. poly p x = (0::complex) \<longrightarrow> poly q x = 0) \<longrightarrow>
   886                  degree p = m \<longrightarrow> m \<noteq> 0 \<longrightarrow> p dvd (q ^ m)"
   887     and pq0: "\<forall>x. poly p x = 0 \<longrightarrow> poly q x = 0"
   888     and dpn: "degree p = n"
   889     and n0: "n \<noteq> 0"
   890   from dpn n0 have pne: "p \<noteq> 0" by auto
   891   show "p dvd (q ^ n)"
   892   proof (cases "\<exists>a. poly p a = 0")
   893     case True
   894     then obtain a where a: "poly p a = 0" ..
   895     have ?thesis if oa: "order a p \<noteq> 0"
   896     proof -
   897       let ?op = "order a p"
   898       from pne have ap: "([:- a, 1:] ^ ?op) dvd p" "\<not> [:- a, 1:] ^ (Suc ?op) dvd p"
   899         using order by blast+
   900       note oop = order_degree[OF pne, unfolded dpn]
   901       show ?thesis
   902       proof (cases "q = 0")
   903         case True
   904         with n0 show ?thesis by (simp add: power_0_left)
   905       next
   906         case False
   907         from pq0[rule_format, OF a, unfolded poly_eq_0_iff_dvd]
   908         obtain r where r: "q = [:- a, 1:] * r" by (rule dvdE)
   909         from ap(1) obtain s where s: "p = [:- a, 1:] ^ ?op * s"
   910           by (rule dvdE)
   911         have sne: "s \<noteq> 0"
   912           using s pne by auto
   913         show ?thesis
   914         proof (cases "degree s = 0")
   915           case True
   916           then obtain k where kpn: "s = [:k:]"
   917             by (cases s) (auto split: if_splits)
   918           from sne kpn have k: "k \<noteq> 0" by simp
   919           let ?w = "([:1/k:] * ([:-a,1:] ^ (n - ?op))) * (r ^ n)"
   920           have "q ^ n = p * ?w"
   921             apply (subst r)
   922             apply (subst s)
   923             apply (subst kpn)
   924             using k oop [of a]
   925             apply (subst power_mult_distrib)
   926             apply simp
   927             apply (subst power_add [symmetric])
   928             apply simp
   929             done
   930           then show ?thesis
   931             unfolding dvd_def by blast
   932         next
   933           case False
   934           with sne dpn s oa have dsn: "degree s < n"
   935             apply auto
   936             apply (erule ssubst)
   937             apply (simp add: degree_mult_eq degree_linear_power)
   938             done
   939           have "poly r x = 0" if h: "poly s x = 0" for x
   940           proof -
   941             have xa: "x \<noteq> a"
   942             proof
   943               assume "x = a"
   944               from h[unfolded this poly_eq_0_iff_dvd] obtain u where u: "s = [:- a, 1:] * u"
   945                 by (rule dvdE)
   946               have "p = [:- a, 1:] ^ (Suc ?op) * u"
   947                 apply (subst s)
   948                 apply (subst u)
   949                 apply (simp only: power_Suc ac_simps)
   950                 done
   951               with ap(2)[unfolded dvd_def] show False
   952                 by blast
   953             qed
   954             from h have "poly p x = 0"
   955               by (subst s) simp
   956             with pq0 have "poly q x = 0"
   957               by blast
   958             with r xa show ?thesis
   959               by auto
   960           qed
   961           with IH[rule_format, OF dsn, of s r] False have "s dvd (r ^ (degree s))"
   962             by blast
   963           then obtain u where u: "r ^ (degree s) = s * u" ..
   964           then have u': "\<And>x. poly s x * poly u x = poly r x ^ degree s"
   965             by (simp only: poly_mult[symmetric] poly_power[symmetric])
   966           let ?w = "(u * ([:-a,1:] ^ (n - ?op))) * (r ^ (n - degree s))"
   967           from oop[of a] dsn have "q ^ n = p * ?w"
   968             apply -
   969             apply (subst s)
   970             apply (subst r)
   971             apply (simp only: power_mult_distrib)
   972             apply (subst mult.assoc [where b=s])
   973             apply (subst mult.assoc [where a=u])
   974             apply (subst mult.assoc [where b=u, symmetric])
   975             apply (subst u [symmetric])
   976             apply (simp add: ac_simps power_add [symmetric])
   977             done
   978           then show ?thesis
   979             unfolding dvd_def by blast
   980         qed
   981       qed
   982     qed
   983     then show ?thesis
   984       using a order_root pne by blast
   985   next
   986     case False
   987     with fundamental_theorem_of_algebra_alt[of p]
   988     obtain c where ccs: "c \<noteq> 0" "p = pCons c 0"
   989       by blast
   990     then have pp: "poly p x = c" for x
   991       by simp
   992     let ?w = "[:1/c:] * (q ^ n)"
   993     from ccs have "(q ^ n) = (p * ?w)"
   994       by simp
   995     then show ?thesis
   996       unfolding dvd_def by blast
   997   qed
   998 qed
   999 
  1000 lemma nullstellensatz_univariate:
  1001   "(\<forall>x. poly p x = (0::complex) \<longrightarrow> poly q x = 0) \<longleftrightarrow>
  1002     p dvd (q ^ (degree p)) \<or> (p = 0 \<and> q = 0)"
  1003 proof -
  1004   consider "p = 0" | "p \<noteq> 0" "degree p = 0" | n where "p \<noteq> 0" "degree p = Suc n"
  1005     by (cases "degree p") auto
  1006   then show ?thesis
  1007   proof cases
  1008     case p: 1
  1009     then have eq: "(\<forall>x. poly p x = (0::complex) \<longrightarrow> poly q x = 0) \<longleftrightarrow> q = 0"
  1010       by (auto simp add: poly_all_0_iff_0)
  1011     {
  1012       assume "p dvd (q ^ (degree p))"
  1013       then obtain r where r: "q ^ (degree p) = p * r" ..
  1014       from r p have False by simp
  1015     }
  1016     with eq p show ?thesis by blast
  1017   next
  1018     case dp: 2
  1019     then obtain k where k: "p = [:k:]" "k \<noteq> 0"
  1020       by (cases p) (simp split: if_splits)
  1021     then have th1: "\<forall>x. poly p x \<noteq> 0"
  1022       by simp
  1023     from k dp(2) have "q ^ (degree p) = p * [:1/k:]"
  1024       by (simp add: one_poly_def)
  1025     then have th2: "p dvd (q ^ (degree p))" ..
  1026     from dp(1) th1 th2 show ?thesis
  1027       by blast
  1028   next
  1029     case dp: 3
  1030     have False if dvd: "p dvd (q ^ (Suc n))" and h: "poly p x = 0" "poly q x \<noteq> 0" for x
  1031     proof -
  1032       from dvd obtain u where u: "q ^ (Suc n) = p * u" ..
  1033       from h have "poly (q ^ (Suc n)) x \<noteq> 0"
  1034         by simp
  1035       with u h(1) show ?thesis
  1036         by (simp only: poly_mult) simp
  1037     qed
  1038     with dp nullstellensatz_lemma[of p q "degree p"] show ?thesis
  1039       by auto
  1040   qed
  1041 qed
  1042 
  1043 text \<open>Useful lemma\<close>
  1044 lemma constant_degree:
  1045   fixes p :: "'a::{idom,ring_char_0} poly"
  1046   shows "constant (poly p) \<longleftrightarrow> degree p = 0" (is "?lhs = ?rhs")
  1047 proof
  1048   show ?rhs if ?lhs
  1049   proof -
  1050     from that[unfolded constant_def, rule_format, of _ "0"]
  1051     have th: "poly p = poly [:poly p 0:]"
  1052       by auto
  1053     then have "p = [:poly p 0:]"
  1054       by (simp add: poly_eq_poly_eq_iff)
  1055     then have "degree p = degree [:poly p 0:]"
  1056       by simp
  1057     then show ?thesis
  1058       by simp
  1059   qed
  1060   show ?lhs if ?rhs
  1061   proof -
  1062     from that obtain k where "p = [:k:]"
  1063       by (cases p) (simp split: if_splits)
  1064     then show ?thesis
  1065       unfolding constant_def by auto
  1066   qed
  1067 qed
  1068 
  1069 text \<open>Arithmetic operations on multivariate polynomials.\<close>
  1070 
  1071 lemma mpoly_base_conv:
  1072   fixes x :: "'a::comm_ring_1"
  1073   shows "0 = poly 0 x" "c = poly [:c:] x" "x = poly [:0,1:] x"
  1074   by simp_all
  1075 
  1076 lemma mpoly_norm_conv:
  1077   fixes x :: "'a::comm_ring_1"
  1078   shows "poly [:0:] x = poly 0 x" "poly [:poly 0 y:] x = poly 0 x"
  1079   by simp_all
  1080 
  1081 lemma mpoly_sub_conv:
  1082   fixes x :: "'a::comm_ring_1"
  1083   shows "poly p x - poly q x = poly p x + -1 * poly q x"
  1084   by simp
  1085 
  1086 lemma poly_pad_rule: "poly p x = 0 \<Longrightarrow> poly (pCons 0 p) x = 0"
  1087   by simp
  1088 
  1089 lemma poly_cancel_eq_conv:
  1090   fixes x :: "'a::field"
  1091   shows "x = 0 \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> y = 0 \<longleftrightarrow> a * y - b * x = 0"
  1092   by auto
  1093 
  1094 lemma poly_divides_pad_rule:
  1095   fixes p:: "('a::comm_ring_1) poly"
  1096   assumes pq: "p dvd q"
  1097   shows "p dvd (pCons 0 q)"
  1098 proof -
  1099   have "pCons 0 q = q * [:0,1:]" by simp
  1100   then have "q dvd (pCons 0 q)" ..
  1101   with pq show ?thesis by (rule dvd_trans)
  1102 qed
  1103 
  1104 lemma poly_divides_conv0:
  1105   fixes p:: "'a::field poly"
  1106   assumes lgpq: "degree q < degree p"
  1107     and lq: "p \<noteq> 0"
  1108   shows "p dvd q \<longleftrightarrow> q = 0" (is "?lhs \<longleftrightarrow> ?rhs")
  1109 proof
  1110   assume ?rhs
  1111   then have "q = p * 0" by simp
  1112   then show ?lhs ..
  1113 next
  1114   assume l: ?lhs
  1115   show ?rhs
  1116   proof (cases "q = 0")
  1117     case True
  1118     then show ?thesis by simp
  1119   next
  1120     assume q0: "q \<noteq> 0"
  1121     from l q0 have "degree p \<le> degree q"
  1122       by (rule dvd_imp_degree_le)
  1123     with lgpq show ?thesis by simp
  1124   qed
  1125 qed
  1126 
  1127 lemma poly_divides_conv1:
  1128   fixes p :: "'a::field poly"
  1129   assumes a0: "a \<noteq> 0"
  1130     and pp': "p dvd p'"
  1131     and qrp': "smult a q - p' = r"
  1132   shows "p dvd q \<longleftrightarrow> p dvd r" (is "?lhs \<longleftrightarrow> ?rhs")
  1133 proof
  1134   from pp' obtain t where t: "p' = p * t" ..
  1135   show ?rhs if ?lhs
  1136   proof -
  1137     from that obtain u where u: "q = p * u" ..
  1138     have "r = p * (smult a u - t)"
  1139       using u qrp' [symmetric] t by (simp add: algebra_simps)
  1140     then show ?thesis ..
  1141   qed
  1142   show ?lhs if ?rhs
  1143   proof -
  1144     from that obtain u where u: "r = p * u" ..
  1145     from u [symmetric] t qrp' [symmetric] a0
  1146     have "q = p * smult (1/a) (u + t)"
  1147       by (simp add: algebra_simps)
  1148     then show ?thesis ..
  1149   qed
  1150 qed
  1151 
  1152 lemma basic_cqe_conv1:
  1153   "(\<exists>x. poly p x = 0 \<and> poly 0 x \<noteq> 0) \<longleftrightarrow> False"
  1154   "(\<exists>x. poly 0 x \<noteq> 0) \<longleftrightarrow> False"
  1155   "(\<exists>x. poly [:c:] x \<noteq> 0) \<longleftrightarrow> c \<noteq> 0"
  1156   "(\<exists>x. poly 0 x = 0) \<longleftrightarrow> True"
  1157   "(\<exists>x. poly [:c:] x = 0) \<longleftrightarrow> c = 0"
  1158   by simp_all
  1159 
  1160 lemma basic_cqe_conv2:
  1161   assumes l: "p \<noteq> 0"
  1162   shows "\<exists>x. poly (pCons a (pCons b p)) x = (0::complex)"
  1163 proof -
  1164   have False if "h \<noteq> 0" "t = 0" and "pCons a (pCons b p) = pCons h t" for h t
  1165     using l that by simp
  1166   then have th: "\<not> (\<exists> h t. h \<noteq> 0 \<and> t = 0 \<and> pCons a (pCons b p) = pCons h t)"
  1167     by blast
  1168   from fundamental_theorem_of_algebra_alt[OF th] show ?thesis
  1169     by auto
  1170 qed
  1171 
  1172 lemma  basic_cqe_conv_2b: "(\<exists>x. poly p x \<noteq> (0::complex)) \<longleftrightarrow> p \<noteq> 0"
  1173   by (metis poly_all_0_iff_0)
  1174 
  1175 lemma basic_cqe_conv3:
  1176   fixes p q :: "complex poly"
  1177   assumes l: "p \<noteq> 0"
  1178   shows "(\<exists>x. poly (pCons a p) x = 0 \<and> poly q x \<noteq> 0) \<longleftrightarrow> \<not> (pCons a p) dvd (q ^ psize p)"
  1179 proof -
  1180   from l have dp: "degree (pCons a p) = psize p"
  1181     by (simp add: psize_def)
  1182   from nullstellensatz_univariate[of "pCons a p" q] l
  1183   show ?thesis
  1184     by (metis dp pCons_eq_0_iff)
  1185 qed
  1186 
  1187 lemma basic_cqe_conv4:
  1188   fixes p q :: "complex poly"
  1189   assumes h: "\<And>x. poly (q ^ n) x = poly r x"
  1190   shows "p dvd (q ^ n) \<longleftrightarrow> p dvd r"
  1191 proof -
  1192   from h have "poly (q ^ n) = poly r"
  1193     by auto
  1194   then have "(q ^ n) = r"
  1195     by (simp add: poly_eq_poly_eq_iff)
  1196   then show "p dvd (q ^ n) \<longleftrightarrow> p dvd r"
  1197     by simp
  1198 qed
  1199 
  1200 lemma poly_const_conv:
  1201   fixes x :: "'a::comm_ring_1"
  1202   shows "poly [:c:] x = y \<longleftrightarrow> c = y"
  1203   by simp
  1204 
  1205 end