src/HOL/Library/Fundamental_Theorem_Algebra.thy
author wenzelm
Wed Mar 08 10:50:59 2017 +0100 (2017-03-08)
changeset 65151 a7394aa4d21c
parent 63589 58aab4745e85
permissions -rw-r--r--
tuned proofs;
     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 + \<i>) < 1 \<or> cmod (z - \<i>) < 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 + \<i>) \<ge> 1" "cmod (z - \<i>) \<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 + \<i>) < 1")
   194       apply (cases "even m")
   195       apply (rule_tac x="\<i>" in exI)
   196       apply (simp add: m power_mult)
   197       apply (rule_tac x="- \<i>" in exI)
   198       apply (simp add: m power_mult)
   199       apply (cases "even m")
   200       apply (rule_tac x="- \<i>" in exI)
   201       apply (simp add: m power_mult)
   202       apply (auto simp add: m power_mult)
   203       apply (rule_tac x="\<i>" 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" "poly q x = poly p (z + x)" for 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" "norm z \<le> 1 \<Longrightarrow> norm (poly cs z) \<le> m" for z
   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: "cmod (poly (pCons c cs) 0) \<le> cmod (poly (pCons c cs) z)"
   539       if "r \<le> cmod z" for z
   540       by blast
   541     have ath: "\<And>z r. r \<le> cmod z \<or> cmod z \<le> \<bar>r\<bar>"
   542       by arith
   543     from poly_minimum_modulus_disc[of "\<bar>r\<bar>" "pCons c cs"]
   544     obtain v where v: "cmod (poly (pCons c cs) v) \<le> cmod (poly (pCons c cs) w)"
   545       if "cmod w \<le> \<bar>r\<bar>" for w
   546       by blast
   547     have "cmod (poly (pCons c cs) v) \<le> cmod (poly (pCons c cs) z)" if z: "r \<le> cmod z" for z
   548       using v[of 0] r[OF z] by simp
   549     with v ath[of r] show ?thesis
   550       by blast
   551   next
   552     case True
   553     with pCons.hyps show ?thesis
   554       by simp
   555   qed
   556 qed
   557 
   558 text \<open>Constant function (non-syntactic characterization).\<close>
   559 definition "constant f \<longleftrightarrow> (\<forall>x y. f x = f y)"
   560 
   561 lemma nonconstant_length: "\<not> constant (poly p) \<Longrightarrow> psize p \<ge> 2"
   562   by (induct p) (auto simp: constant_def psize_def)
   563 
   564 lemma poly_replicate_append: "poly (monom 1 n * p) (x::'a::comm_ring_1) = x^n * poly p x"
   565   by (simp add: poly_monom)
   566 
   567 text \<open>Decomposition of polynomial, skipping zero coefficients after the first.\<close>
   568 
   569 lemma poly_decompose_lemma:
   570   assumes nz: "\<not> (\<forall>z. z \<noteq> 0 \<longrightarrow> poly p z = (0::'a::idom))"
   571   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)"
   572   unfolding psize_def
   573   using nz
   574 proof (induct p)
   575   case 0
   576   then show ?case by simp
   577 next
   578   case (pCons c cs)
   579   show ?case
   580   proof (cases "c = 0")
   581     case True
   582     from pCons.hyps pCons.prems True show ?thesis
   583       apply auto
   584       apply (rule_tac x="k+1" in exI)
   585       apply (rule_tac x="a" in exI)
   586       apply clarsimp
   587       apply (rule_tac x="q" in exI)
   588       apply auto
   589       done
   590   next
   591     case False
   592     show ?thesis
   593       apply (rule exI[where x=0])
   594       apply (rule exI[where x=c])
   595       apply (auto simp: False)
   596       done
   597   qed
   598 qed
   599 
   600 lemma poly_decompose:
   601   assumes nc: "\<not> constant (poly p)"
   602   shows "\<exists>k a q. a \<noteq> (0::'a::idom) \<and> k \<noteq> 0 \<and>
   603                psize q + k + 1 = psize p \<and>
   604               (\<forall>z. poly p z = poly p 0 + z^k * poly (pCons a q) z)"
   605   using nc
   606 proof (induct p)
   607   case 0
   608   then show ?case
   609     by (simp add: constant_def)
   610 next
   611   case (pCons c cs)
   612   have "\<not> (\<forall>z. z \<noteq> 0 \<longrightarrow> poly cs z = 0)"
   613   proof
   614     assume "\<forall>z. z \<noteq> 0 \<longrightarrow> poly cs z = 0"
   615     then have "poly (pCons c cs) x = poly (pCons c cs) y" for x y
   616       by (cases "x = 0") auto
   617     with pCons.prems show False
   618       by (auto simp add: constant_def)
   619   qed
   620   from poly_decompose_lemma[OF this]
   621   show ?case
   622     apply clarsimp
   623     apply (rule_tac x="k+1" in exI)
   624     apply (rule_tac x="a" in exI)
   625     apply simp
   626     apply (rule_tac x="q" in exI)
   627     apply (auto simp add: psize_def split: if_splits)
   628     done
   629 qed
   630 
   631 text \<open>Fundamental theorem of algebra\<close>
   632 
   633 lemma fundamental_theorem_of_algebra:
   634   assumes nc: "\<not> constant (poly p)"
   635   shows "\<exists>z::complex. poly p z = 0"
   636   using nc
   637 proof (induct "psize p" arbitrary: p rule: less_induct)
   638   case less
   639   let ?p = "poly p"
   640   let ?ths = "\<exists>z. ?p z = 0"
   641 
   642   from nonconstant_length[OF less(2)] have n2: "psize p \<ge> 2" .
   643   from poly_minimum_modulus obtain c where c: "\<forall>w. cmod (?p c) \<le> cmod (?p w)"
   644     by blast
   645 
   646   show ?ths
   647   proof (cases "?p c = 0")
   648     case True
   649     then show ?thesis by blast
   650   next
   651     case False
   652     from poly_offset[of p c] obtain q where q: "psize q = psize p" "\<forall>x. poly q x = ?p (c + x)"
   653       by blast
   654     have False if h: "constant (poly q)"
   655     proof -
   656       from q(2) have th: "\<forall>x. poly q (x - c) = ?p x"
   657         by auto
   658       have "?p x = ?p y" for x y
   659       proof -
   660         from th have "?p x = poly q (x - c)"
   661           by auto
   662         also have "\<dots> = poly q (y - c)"
   663           using h unfolding constant_def by blast
   664         also have "\<dots> = ?p y"
   665           using th by auto
   666         finally show ?thesis .
   667       qed
   668       with less(2) show ?thesis
   669         unfolding constant_def by blast
   670     qed
   671     then have qnc: "\<not> constant (poly q)"
   672       by blast
   673     from q(2) have pqc0: "?p c = poly q 0"
   674       by simp
   675     from c pqc0 have cq0: "\<forall>w. cmod (poly q 0) \<le> cmod (?p w)"
   676       by simp
   677     let ?a0 = "poly q 0"
   678     from False pqc0 have a00: "?a0 \<noteq> 0"
   679       by simp
   680     from a00 have qr: "\<forall>z. poly q z = poly (smult (inverse ?a0) q) z * ?a0"
   681       by simp
   682     let ?r = "smult (inverse ?a0) q"
   683     have lgqr: "psize q = psize ?r"
   684       using a00
   685       unfolding psize_def degree_def
   686       by (simp add: poly_eq_iff)
   687     have False if h: "\<And>x y. poly ?r x = poly ?r y"
   688     proof -
   689       have "poly q x = poly q y" for x y
   690       proof -
   691         from qr[rule_format, of x] have "poly q x = poly ?r x * ?a0"
   692           by auto
   693         also have "\<dots> = poly ?r y * ?a0"
   694           using h by simp
   695         also have "\<dots> = poly q y"
   696           using qr[rule_format, of y] by simp
   697         finally show ?thesis .
   698       qed
   699       with qnc show ?thesis
   700         unfolding constant_def by blast
   701     qed
   702     then have rnc: "\<not> constant (poly ?r)"
   703       unfolding constant_def by blast
   704     from qr[rule_format, of 0] a00 have r01: "poly ?r 0 = 1"
   705       by auto
   706     have mrmq_eq: "cmod (poly ?r w) < 1 \<longleftrightarrow> cmod (poly q w) < cmod ?a0" for w
   707     proof -
   708       have "cmod (poly ?r w) < 1 \<longleftrightarrow> cmod (poly q w / ?a0) < 1"
   709         using qr[rule_format, of w] a00 by (simp add: divide_inverse ac_simps)
   710       also have "\<dots> \<longleftrightarrow> cmod (poly q w) < cmod ?a0"
   711         using a00 unfolding norm_divide by (simp add: field_simps)
   712       finally show ?thesis .
   713     qed
   714     from poly_decompose[OF rnc] obtain k a s where
   715       kas: "a \<noteq> 0" "k \<noteq> 0" "psize s + k + 1 = psize ?r"
   716         "\<forall>z. poly ?r z = poly ?r 0 + z^k* poly (pCons a s) z" by blast
   717     have "\<exists>w. cmod (poly ?r w) < 1"
   718     proof (cases "psize p = k + 1")
   719       case True
   720       with kas(3) lgqr[symmetric] q(1) have s0: "s = 0"
   721         by auto
   722       have hth[symmetric]: "cmod (poly ?r w) = cmod (1 + a * w ^ k)" for w
   723         using kas(4)[rule_format, of w] s0 r01 by (simp add: algebra_simps)
   724       from reduce_poly_simple[OF kas(1,2)] show ?thesis
   725         unfolding hth by blast
   726     next
   727       case False note kn = this
   728       from kn kas(3) q(1) lgqr have k1n: "k + 1 < psize p"
   729         by simp
   730       have th01: "\<not> constant (poly (pCons 1 (monom a (k - 1))))"
   731         unfolding constant_def poly_pCons poly_monom
   732         using kas(1)
   733         apply simp
   734         apply (rule exI[where x=0])
   735         apply (rule exI[where x=1])
   736         apply simp
   737         done
   738       from kas(1) kas(2) have th02: "k + 1 = psize (pCons 1 (monom a (k - 1)))"
   739         by (simp add: psize_def degree_monom_eq)
   740       from less(1) [OF k1n [simplified th02] th01]
   741       obtain w where w: "1 + w^k * a = 0"
   742         unfolding poly_pCons poly_monom
   743         using kas(2) by (cases k) (auto simp add: algebra_simps)
   744       from poly_bound_exists[of "cmod w" s] obtain m where
   745         m: "m > 0" "\<forall>z. cmod z \<le> cmod w \<longrightarrow> cmod (poly s z) \<le> m" by blast
   746       have w0: "w \<noteq> 0"
   747         using kas(2) w by (auto simp add: power_0_left)
   748       from w have "(1 + w ^ k * a) - 1 = 0 - 1"
   749         by simp
   750       then have wm1: "w^k * a = - 1"
   751         by simp
   752       have inv0: "0 < inverse (cmod w ^ (k + 1) * m)"
   753         using norm_ge_zero[of w] w0 m(1)
   754         by (simp add: inverse_eq_divide zero_less_mult_iff)
   755       with real_lbound_gt_zero[OF zero_less_one] obtain t where
   756         t: "t > 0" "t < 1" "t < inverse (cmod w ^ (k + 1) * m)" by blast
   757       let ?ct = "complex_of_real t"
   758       let ?w = "?ct * w"
   759       have "1 + ?w^k * (a + ?w * poly s ?w) = 1 + ?ct^k * (w^k * a) + ?w^k * ?w * poly s ?w"
   760         using kas(1) by (simp add: algebra_simps power_mult_distrib)
   761       also have "\<dots> = complex_of_real (1 - t^k) + ?w^k * ?w * poly s ?w"
   762         unfolding wm1 by simp
   763       finally have "cmod (1 + ?w^k * (a + ?w * poly s ?w)) =
   764         cmod (complex_of_real (1 - t^k) + ?w^k * ?w * poly s ?w)"
   765         by metis
   766       with norm_triangle_ineq[of "complex_of_real (1 - t^k)" "?w^k * ?w * poly s ?w"]
   767       have th11: "cmod (1 + ?w^k * (a + ?w * poly s ?w)) \<le> \<bar>1 - t^k\<bar> + cmod (?w^k * ?w * poly s ?w)"
   768         unfolding norm_of_real by simp
   769       have ath: "\<And>x t::real. 0 \<le> x \<Longrightarrow> x < t \<Longrightarrow> t \<le> 1 \<Longrightarrow> \<bar>1 - t\<bar> + x < 1"
   770         by arith
   771       have "t * cmod w \<le> 1 * cmod w"
   772         apply (rule mult_mono)
   773         using t(1,2)
   774         apply auto
   775         done
   776       then have tw: "cmod ?w \<le> cmod w"
   777         using t(1) by (simp add: norm_mult)
   778       from t inv0 have "t * (cmod w ^ (k + 1) * m) < 1"
   779         by (simp add: field_simps)
   780       with zero_less_power[OF t(1), of k] have th30: "t^k * (t* (cmod w ^ (k + 1) * m)) < t^k * 1"
   781         by simp
   782       have "cmod (?w^k * ?w * poly s ?w) = t^k * (t* (cmod w ^ (k + 1) * cmod (poly s ?w)))"
   783         using w0 t(1)
   784         by (simp add: algebra_simps power_mult_distrib norm_power norm_mult)
   785       then have "cmod (?w^k * ?w * poly s ?w) \<le> t^k * (t* (cmod w ^ (k + 1) * m))"
   786         using t(1,2) m(2)[rule_format, OF tw] w0
   787         by auto
   788       with th30 have th120: "cmod (?w^k * ?w * poly s ?w) < t^k"
   789         by simp
   790       from power_strict_mono[OF t(2), of k] t(1) kas(2) have th121: "t^k \<le> 1"
   791         by auto
   792       from ath[OF norm_ge_zero[of "?w^k * ?w * poly s ?w"] th120 th121]
   793       have th12: "\<bar>1 - t^k\<bar> + cmod (?w^k * ?w * poly s ?w) < 1" .
   794       from th11 th12 have "cmod (1 + ?w^k * (a + ?w * poly s ?w)) < 1"
   795         by arith
   796       then have "cmod (poly ?r ?w) < 1"
   797         unfolding kas(4)[rule_format, of ?w] r01 by simp
   798       then show ?thesis
   799         by blast
   800     qed
   801     with cq0 q(2) show ?thesis
   802       unfolding mrmq_eq not_less[symmetric] by auto
   803   qed
   804 qed
   805 
   806 text \<open>Alternative version with a syntactic notion of constant polynomial.\<close>
   807 
   808 lemma fundamental_theorem_of_algebra_alt:
   809   assumes nc: "\<not> (\<exists>a l. a \<noteq> 0 \<and> l = 0 \<and> p = pCons a l)"
   810   shows "\<exists>z. poly p z = (0::complex)"
   811   using nc
   812 proof (induct p)
   813   case 0
   814   then show ?case by simp
   815 next
   816   case (pCons c cs)
   817   show ?case
   818   proof (cases "c = 0")
   819     case True
   820     then show ?thesis by auto
   821   next
   822     case False
   823     have "\<not> constant (poly (pCons c cs))"
   824     proof
   825       assume nc: "constant (poly (pCons c cs))"
   826       from nc[unfolded constant_def, rule_format, of 0]
   827       have "\<forall>w. w \<noteq> 0 \<longrightarrow> poly cs w = 0" by auto
   828       then have "cs = 0"
   829       proof (induct cs)
   830         case 0
   831         then show ?case by simp
   832       next
   833         case (pCons d ds)
   834         show ?case
   835         proof (cases "d = 0")
   836           case True
   837           then show ?thesis
   838             using pCons.prems pCons.hyps by simp
   839         next
   840           case False
   841           from poly_bound_exists[of 1 ds] obtain m where
   842             m: "m > 0" "\<forall>z. \<forall>z. cmod z \<le> 1 \<longrightarrow> cmod (poly ds z) \<le> m" by blast
   843           have dm: "cmod d / m > 0"
   844             using False m(1) by (simp add: field_simps)
   845           from real_lbound_gt_zero[OF dm zero_less_one]
   846           obtain x where x: "x > 0" "x < cmod d / m" "x < 1"
   847             by blast
   848           let ?x = "complex_of_real x"
   849           from x have cx: "?x \<noteq> 0" "cmod ?x \<le> 1"
   850             by simp_all
   851           from pCons.prems[rule_format, OF cx(1)]
   852           have cth: "cmod (?x*poly ds ?x) = cmod d"
   853             by (simp add: eq_diff_eq[symmetric])
   854           from m(2)[rule_format, OF cx(2)] x(1)
   855           have th0: "cmod (?x*poly ds ?x) \<le> x*m"
   856             by (simp add: norm_mult)
   857           from x(2) m(1) have "x * m < cmod d"
   858             by (simp add: field_simps)
   859           with th0 have "cmod (?x*poly ds ?x) \<noteq> cmod d"
   860             by auto
   861           with cth show ?thesis
   862             by blast
   863         qed
   864       qed
   865       then show False
   866         using pCons.prems False by blast
   867     qed
   868     then show ?thesis
   869       by (rule fundamental_theorem_of_algebra)
   870   qed
   871 qed
   872 
   873 
   874 subsection \<open>Nullstellensatz, degrees and divisibility of polynomials\<close>
   875 
   876 lemma nullstellensatz_lemma:
   877   fixes p :: "complex poly"
   878   assumes "\<forall>x. poly p x = 0 \<longrightarrow> poly q x = 0"
   879     and "degree p = n"
   880     and "n \<noteq> 0"
   881   shows "p dvd (q ^ n)"
   882   using assms
   883 proof (induct n arbitrary: p q rule: nat_less_induct)
   884   fix n :: nat
   885   fix p q :: "complex poly"
   886   assume IH: "\<forall>m<n. \<forall>p q.
   887                  (\<forall>x. poly p x = (0::complex) \<longrightarrow> poly q x = 0) \<longrightarrow>
   888                  degree p = m \<longrightarrow> m \<noteq> 0 \<longrightarrow> p dvd (q ^ m)"
   889     and pq0: "\<forall>x. poly p x = 0 \<longrightarrow> poly q x = 0"
   890     and dpn: "degree p = n"
   891     and n0: "n \<noteq> 0"
   892   from dpn n0 have pne: "p \<noteq> 0" by auto
   893   show "p dvd (q ^ n)"
   894   proof (cases "\<exists>a. poly p a = 0")
   895     case True
   896     then obtain a where a: "poly p a = 0" ..
   897     have ?thesis if oa: "order a p \<noteq> 0"
   898     proof -
   899       let ?op = "order a p"
   900       from pne have ap: "([:- a, 1:] ^ ?op) dvd p" "\<not> [:- a, 1:] ^ (Suc ?op) dvd p"
   901         using order by blast+
   902       note oop = order_degree[OF pne, unfolded dpn]
   903       show ?thesis
   904       proof (cases "q = 0")
   905         case True
   906         with n0 show ?thesis by (simp add: power_0_left)
   907       next
   908         case False
   909         from pq0[rule_format, OF a, unfolded poly_eq_0_iff_dvd]
   910         obtain r where r: "q = [:- a, 1:] * r" by (rule dvdE)
   911         from ap(1) obtain s where s: "p = [:- a, 1:] ^ ?op * s"
   912           by (rule dvdE)
   913         have sne: "s \<noteq> 0"
   914           using s pne by auto
   915         show ?thesis
   916         proof (cases "degree s = 0")
   917           case True
   918           then obtain k where kpn: "s = [:k:]"
   919             by (cases s) (auto split: if_splits)
   920           from sne kpn have k: "k \<noteq> 0" by simp
   921           let ?w = "([:1/k:] * ([:-a,1:] ^ (n - ?op))) * (r ^ n)"
   922           have "q ^ n = p * ?w"
   923             apply (subst r)
   924             apply (subst s)
   925             apply (subst kpn)
   926             using k oop [of a]
   927             apply (subst power_mult_distrib)
   928             apply simp
   929             apply (subst power_add [symmetric])
   930             apply simp
   931             done
   932           then show ?thesis
   933             unfolding dvd_def by blast
   934         next
   935           case False
   936           with sne dpn s oa have dsn: "degree s < n"
   937             apply auto
   938             apply (erule ssubst)
   939             apply (simp add: degree_mult_eq degree_linear_power)
   940             done
   941           have "poly r x = 0" if h: "poly s x = 0" for x
   942           proof -
   943             have xa: "x \<noteq> a"
   944             proof
   945               assume "x = a"
   946               from h[unfolded this poly_eq_0_iff_dvd] obtain u where u: "s = [:- a, 1:] * u"
   947                 by (rule dvdE)
   948               have "p = [:- a, 1:] ^ (Suc ?op) * u"
   949                 apply (subst s)
   950                 apply (subst u)
   951                 apply (simp only: power_Suc ac_simps)
   952                 done
   953               with ap(2)[unfolded dvd_def] show False
   954                 by blast
   955             qed
   956             from h have "poly p x = 0"
   957               by (subst s) simp
   958             with pq0 have "poly q x = 0"
   959               by blast
   960             with r xa show ?thesis
   961               by auto
   962           qed
   963           with IH[rule_format, OF dsn, of s r] False have "s dvd (r ^ (degree s))"
   964             by blast
   965           then obtain u where u: "r ^ (degree s) = s * u" ..
   966           then have u': "\<And>x. poly s x * poly u x = poly r x ^ degree s"
   967             by (simp only: poly_mult[symmetric] poly_power[symmetric])
   968           let ?w = "(u * ([:-a,1:] ^ (n - ?op))) * (r ^ (n - degree s))"
   969           from oop[of a] dsn have "q ^ n = p * ?w"
   970             apply -
   971             apply (subst s)
   972             apply (subst r)
   973             apply (simp only: power_mult_distrib)
   974             apply (subst mult.assoc [where b=s])
   975             apply (subst mult.assoc [where a=u])
   976             apply (subst mult.assoc [where b=u, symmetric])
   977             apply (subst u [symmetric])
   978             apply (simp add: ac_simps power_add [symmetric])
   979             done
   980           then show ?thesis
   981             unfolding dvd_def by blast
   982         qed
   983       qed
   984     qed
   985     then show ?thesis
   986       using a order_root pne by blast
   987   next
   988     case False
   989     with fundamental_theorem_of_algebra_alt[of p]
   990     obtain c where ccs: "c \<noteq> 0" "p = pCons c 0"
   991       by blast
   992     then have pp: "poly p x = c" for x
   993       by simp
   994     let ?w = "[:1/c:] * (q ^ n)"
   995     from ccs have "(q ^ n) = (p * ?w)"
   996       by simp
   997     then show ?thesis
   998       unfolding dvd_def by blast
   999   qed
  1000 qed
  1001 
  1002 lemma nullstellensatz_univariate:
  1003   "(\<forall>x. poly p x = (0::complex) \<longrightarrow> poly q x = 0) \<longleftrightarrow>
  1004     p dvd (q ^ (degree p)) \<or> (p = 0 \<and> q = 0)"
  1005 proof -
  1006   consider "p = 0" | "p \<noteq> 0" "degree p = 0" | n where "p \<noteq> 0" "degree p = Suc n"
  1007     by (cases "degree p") auto
  1008   then show ?thesis
  1009   proof cases
  1010     case p: 1
  1011     then have eq: "(\<forall>x. poly p x = (0::complex) \<longrightarrow> poly q x = 0) \<longleftrightarrow> q = 0"
  1012       by (auto simp add: poly_all_0_iff_0)
  1013     {
  1014       assume "p dvd (q ^ (degree p))"
  1015       then obtain r where r: "q ^ (degree p) = p * r" ..
  1016       from r p have False by simp
  1017     }
  1018     with eq p show ?thesis by blast
  1019   next
  1020     case dp: 2
  1021     then obtain k where k: "p = [:k:]" "k \<noteq> 0"
  1022       by (cases p) (simp split: if_splits)
  1023     then have th1: "\<forall>x. poly p x \<noteq> 0"
  1024       by simp
  1025     from k dp(2) have "q ^ (degree p) = p * [:1/k:]"
  1026       by (simp add: one_poly_def)
  1027     then have th2: "p dvd (q ^ (degree p))" ..
  1028     from dp(1) th1 th2 show ?thesis
  1029       by blast
  1030   next
  1031     case dp: 3
  1032     have False if dvd: "p dvd (q ^ (Suc n))" and h: "poly p x = 0" "poly q x \<noteq> 0" for x
  1033     proof -
  1034       from dvd obtain u where u: "q ^ (Suc n) = p * u" ..
  1035       from h have "poly (q ^ (Suc n)) x \<noteq> 0"
  1036         by simp
  1037       with u h(1) show ?thesis
  1038         by (simp only: poly_mult) simp
  1039     qed
  1040     with dp nullstellensatz_lemma[of p q "degree p"] show ?thesis
  1041       by auto
  1042   qed
  1043 qed
  1044 
  1045 text \<open>Useful lemma\<close>
  1046 lemma constant_degree:
  1047   fixes p :: "'a::{idom,ring_char_0} poly"
  1048   shows "constant (poly p) \<longleftrightarrow> degree p = 0" (is "?lhs = ?rhs")
  1049 proof
  1050   show ?rhs if ?lhs
  1051   proof -
  1052     from that[unfolded constant_def, rule_format, of _ "0"]
  1053     have th: "poly p = poly [:poly p 0:]"
  1054       by auto
  1055     then have "p = [:poly p 0:]"
  1056       by (simp add: poly_eq_poly_eq_iff)
  1057     then have "degree p = degree [:poly p 0:]"
  1058       by simp
  1059     then show ?thesis
  1060       by simp
  1061   qed
  1062   show ?lhs if ?rhs
  1063   proof -
  1064     from that obtain k where "p = [:k:]"
  1065       by (cases p) (simp split: if_splits)
  1066     then show ?thesis
  1067       unfolding constant_def by auto
  1068   qed
  1069 qed
  1070 
  1071 text \<open>Arithmetic operations on multivariate polynomials.\<close>
  1072 
  1073 lemma mpoly_base_conv:
  1074   fixes x :: "'a::comm_ring_1"
  1075   shows "0 = poly 0 x" "c = poly [:c:] x" "x = poly [:0,1:] x"
  1076   by simp_all
  1077 
  1078 lemma mpoly_norm_conv:
  1079   fixes x :: "'a::comm_ring_1"
  1080   shows "poly [:0:] x = poly 0 x" "poly [:poly 0 y:] x = poly 0 x"
  1081   by simp_all
  1082 
  1083 lemma mpoly_sub_conv:
  1084   fixes x :: "'a::comm_ring_1"
  1085   shows "poly p x - poly q x = poly p x + -1 * poly q x"
  1086   by simp
  1087 
  1088 lemma poly_pad_rule: "poly p x = 0 \<Longrightarrow> poly (pCons 0 p) x = 0"
  1089   by simp
  1090 
  1091 lemma poly_cancel_eq_conv:
  1092   fixes x :: "'a::field"
  1093   shows "x = 0 \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> y = 0 \<longleftrightarrow> a * y - b * x = 0"
  1094   by auto
  1095 
  1096 lemma poly_divides_pad_rule:
  1097   fixes p:: "('a::comm_ring_1) poly"
  1098   assumes pq: "p dvd q"
  1099   shows "p dvd (pCons 0 q)"
  1100 proof -
  1101   have "pCons 0 q = q * [:0,1:]" by simp
  1102   then have "q dvd (pCons 0 q)" ..
  1103   with pq show ?thesis by (rule dvd_trans)
  1104 qed
  1105 
  1106 lemma poly_divides_conv0:
  1107   fixes p:: "'a::field poly"
  1108   assumes lgpq: "degree q < degree p"
  1109     and lq: "p \<noteq> 0"
  1110   shows "p dvd q \<longleftrightarrow> q = 0" (is "?lhs \<longleftrightarrow> ?rhs")
  1111 proof
  1112   assume ?rhs
  1113   then have "q = p * 0" by simp
  1114   then show ?lhs ..
  1115 next
  1116   assume l: ?lhs
  1117   show ?rhs
  1118   proof (cases "q = 0")
  1119     case True
  1120     then show ?thesis by simp
  1121   next
  1122     assume q0: "q \<noteq> 0"
  1123     from l q0 have "degree p \<le> degree q"
  1124       by (rule dvd_imp_degree_le)
  1125     with lgpq show ?thesis by simp
  1126   qed
  1127 qed
  1128 
  1129 lemma poly_divides_conv1:
  1130   fixes p :: "'a::field poly"
  1131   assumes a0: "a \<noteq> 0"
  1132     and pp': "p dvd p'"
  1133     and qrp': "smult a q - p' = r"
  1134   shows "p dvd q \<longleftrightarrow> p dvd r" (is "?lhs \<longleftrightarrow> ?rhs")
  1135 proof
  1136   from pp' obtain t where t: "p' = p * t" ..
  1137   show ?rhs if ?lhs
  1138   proof -
  1139     from that obtain u where u: "q = p * u" ..
  1140     have "r = p * (smult a u - t)"
  1141       using u qrp' [symmetric] t by (simp add: algebra_simps)
  1142     then show ?thesis ..
  1143   qed
  1144   show ?lhs if ?rhs
  1145   proof -
  1146     from that obtain u where u: "r = p * u" ..
  1147     from u [symmetric] t qrp' [symmetric] a0
  1148     have "q = p * smult (1/a) (u + t)"
  1149       by (simp add: algebra_simps)
  1150     then show ?thesis ..
  1151   qed
  1152 qed
  1153 
  1154 lemma basic_cqe_conv1:
  1155   "(\<exists>x. poly p x = 0 \<and> poly 0 x \<noteq> 0) \<longleftrightarrow> False"
  1156   "(\<exists>x. poly 0 x \<noteq> 0) \<longleftrightarrow> False"
  1157   "(\<exists>x. poly [:c:] x \<noteq> 0) \<longleftrightarrow> c \<noteq> 0"
  1158   "(\<exists>x. poly 0 x = 0) \<longleftrightarrow> True"
  1159   "(\<exists>x. poly [:c:] x = 0) \<longleftrightarrow> c = 0"
  1160   by simp_all
  1161 
  1162 lemma basic_cqe_conv2:
  1163   assumes l: "p \<noteq> 0"
  1164   shows "\<exists>x. poly (pCons a (pCons b p)) x = (0::complex)"
  1165 proof -
  1166   have False if "h \<noteq> 0" "t = 0" and "pCons a (pCons b p) = pCons h t" for h t
  1167     using l that by simp
  1168   then have th: "\<not> (\<exists> h t. h \<noteq> 0 \<and> t = 0 \<and> pCons a (pCons b p) = pCons h t)"
  1169     by blast
  1170   from fundamental_theorem_of_algebra_alt[OF th] show ?thesis
  1171     by auto
  1172 qed
  1173 
  1174 lemma  basic_cqe_conv_2b: "(\<exists>x. poly p x \<noteq> (0::complex)) \<longleftrightarrow> p \<noteq> 0"
  1175   by (metis poly_all_0_iff_0)
  1176 
  1177 lemma basic_cqe_conv3:
  1178   fixes p q :: "complex poly"
  1179   assumes l: "p \<noteq> 0"
  1180   shows "(\<exists>x. poly (pCons a p) x = 0 \<and> poly q x \<noteq> 0) \<longleftrightarrow> \<not> (pCons a p) dvd (q ^ psize p)"
  1181 proof -
  1182   from l have dp: "degree (pCons a p) = psize p"
  1183     by (simp add: psize_def)
  1184   from nullstellensatz_univariate[of "pCons a p" q] l
  1185   show ?thesis
  1186     by (metis dp pCons_eq_0_iff)
  1187 qed
  1188 
  1189 lemma basic_cqe_conv4:
  1190   fixes p q :: "complex poly"
  1191   assumes h: "\<And>x. poly (q ^ n) x = poly r x"
  1192   shows "p dvd (q ^ n) \<longleftrightarrow> p dvd r"
  1193 proof -
  1194   from h have "poly (q ^ n) = poly r"
  1195     by auto
  1196   then have "(q ^ n) = r"
  1197     by (simp add: poly_eq_poly_eq_iff)
  1198   then show "p dvd (q ^ n) \<longleftrightarrow> p dvd r"
  1199     by simp
  1200 qed
  1201 
  1202 lemma poly_const_conv:
  1203   fixes x :: "'a::comm_ring_1"
  1204   shows "poly [:c:] x = y \<longleftrightarrow> c = y"
  1205   by simp
  1206 
  1207 end