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