src/HOL/Computational_Algebra/Polynomial.thy
author wenzelm
Sun Nov 26 21:08:32 2017 +0100 (17 months ago)
changeset 67091 1393c2340eec
parent 66806 a4e82b58d833
child 67369 7360fe6bb423
permissions -rw-r--r--
more symbols;
     1 (*  Title:      HOL/Computational_Algebra/Polynomial.thy
     2     Author:     Brian Huffman
     3     Author:     Clemens Ballarin
     4     Author:     Amine Chaieb
     5     Author:     Florian Haftmann
     6 *)
     7 
     8 section \<open>Polynomials as type over a ring structure\<close>
     9 
    10 theory Polynomial
    11 imports
    12   HOL.Deriv
    13   "HOL-Library.More_List"
    14   "HOL-Library.Infinite_Set"
    15   Factorial_Ring
    16 begin
    17 
    18 subsection \<open>Auxiliary: operations for lists (later) representing coefficients\<close>
    19 
    20 definition cCons :: "'a::zero \<Rightarrow> 'a list \<Rightarrow> 'a list"  (infixr "##" 65)
    21   where "x ## xs = (if xs = [] \<and> x = 0 then [] else x # xs)"
    22 
    23 lemma cCons_0_Nil_eq [simp]: "0 ## [] = []"
    24   by (simp add: cCons_def)
    25 
    26 lemma cCons_Cons_eq [simp]: "x ## y # ys = x # y # ys"
    27   by (simp add: cCons_def)
    28 
    29 lemma cCons_append_Cons_eq [simp]: "x ## xs @ y # ys = x # xs @ y # ys"
    30   by (simp add: cCons_def)
    31 
    32 lemma cCons_not_0_eq [simp]: "x \<noteq> 0 \<Longrightarrow> x ## xs = x # xs"
    33   by (simp add: cCons_def)
    34 
    35 lemma strip_while_not_0_Cons_eq [simp]:
    36   "strip_while (\<lambda>x. x = 0) (x # xs) = x ## strip_while (\<lambda>x. x = 0) xs"
    37 proof (cases "x = 0")
    38   case False
    39   then show ?thesis by simp
    40 next
    41   case True
    42   show ?thesis
    43   proof (induct xs rule: rev_induct)
    44     case Nil
    45     with True show ?case by simp
    46   next
    47     case (snoc y ys)
    48     then show ?case
    49       by (cases "y = 0") (simp_all add: append_Cons [symmetric] del: append_Cons)
    50   qed
    51 qed
    52 
    53 lemma tl_cCons [simp]: "tl (x ## xs) = xs"
    54   by (simp add: cCons_def)
    55 
    56 
    57 subsection \<open>Definition of type \<open>poly\<close>\<close>
    58 
    59 typedef (overloaded) 'a poly = "{f :: nat \<Rightarrow> 'a::zero. \<forall>\<^sub>\<infinity> n. f n = 0}"
    60   morphisms coeff Abs_poly
    61   by (auto intro!: ALL_MOST)
    62 
    63 setup_lifting type_definition_poly
    64 
    65 lemma poly_eq_iff: "p = q \<longleftrightarrow> (\<forall>n. coeff p n = coeff q n)"
    66   by (simp add: coeff_inject [symmetric] fun_eq_iff)
    67 
    68 lemma poly_eqI: "(\<And>n. coeff p n = coeff q n) \<Longrightarrow> p = q"
    69   by (simp add: poly_eq_iff)
    70 
    71 lemma MOST_coeff_eq_0: "\<forall>\<^sub>\<infinity> n. coeff p n = 0"
    72   using coeff [of p] by simp
    73 
    74 
    75 subsection \<open>Degree of a polynomial\<close>
    76 
    77 definition degree :: "'a::zero poly \<Rightarrow> nat"
    78   where "degree p = (LEAST n. \<forall>i>n. coeff p i = 0)"
    79 
    80 lemma coeff_eq_0:
    81   assumes "degree p < n"
    82   shows "coeff p n = 0"
    83 proof -
    84   have "\<exists>n. \<forall>i>n. coeff p i = 0"
    85     using MOST_coeff_eq_0 by (simp add: MOST_nat)
    86   then have "\<forall>i>degree p. coeff p i = 0"
    87     unfolding degree_def by (rule LeastI_ex)
    88   with assms show ?thesis by simp
    89 qed
    90 
    91 lemma le_degree: "coeff p n \<noteq> 0 \<Longrightarrow> n \<le> degree p"
    92   by (erule contrapos_np, rule coeff_eq_0, simp)
    93 
    94 lemma degree_le: "\<forall>i>n. coeff p i = 0 \<Longrightarrow> degree p \<le> n"
    95   unfolding degree_def by (erule Least_le)
    96 
    97 lemma less_degree_imp: "n < degree p \<Longrightarrow> \<exists>i>n. coeff p i \<noteq> 0"
    98   unfolding degree_def by (drule not_less_Least, simp)
    99 
   100 
   101 subsection \<open>The zero polynomial\<close>
   102 
   103 instantiation poly :: (zero) zero
   104 begin
   105 
   106 lift_definition zero_poly :: "'a poly"
   107   is "\<lambda>_. 0"
   108   by (rule MOST_I) simp
   109 
   110 instance ..
   111 
   112 end
   113 
   114 lemma coeff_0 [simp]: "coeff 0 n = 0"
   115   by transfer rule
   116 
   117 lemma degree_0 [simp]: "degree 0 = 0"
   118   by (rule order_antisym [OF degree_le le0]) simp
   119 
   120 lemma leading_coeff_neq_0:
   121   assumes "p \<noteq> 0"
   122   shows "coeff p (degree p) \<noteq> 0"
   123 proof (cases "degree p")
   124   case 0
   125   from \<open>p \<noteq> 0\<close> obtain n where "coeff p n \<noteq> 0"
   126     by (auto simp add: poly_eq_iff)
   127   then have "n \<le> degree p"
   128     by (rule le_degree)
   129   with \<open>coeff p n \<noteq> 0\<close> and \<open>degree p = 0\<close> show "coeff p (degree p) \<noteq> 0"
   130     by simp
   131 next
   132   case (Suc n)
   133   from \<open>degree p = Suc n\<close> have "n < degree p"
   134     by simp
   135   then have "\<exists>i>n. coeff p i \<noteq> 0"
   136     by (rule less_degree_imp)
   137   then obtain i where "n < i" and "coeff p i \<noteq> 0"
   138     by blast
   139   from \<open>degree p = Suc n\<close> and \<open>n < i\<close> have "degree p \<le> i"
   140     by simp
   141   also from \<open>coeff p i \<noteq> 0\<close> have "i \<le> degree p"
   142     by (rule le_degree)
   143   finally have "degree p = i" .
   144   with \<open>coeff p i \<noteq> 0\<close> show "coeff p (degree p) \<noteq> 0" by simp
   145 qed
   146 
   147 lemma leading_coeff_0_iff [simp]: "coeff p (degree p) = 0 \<longleftrightarrow> p = 0"
   148   by (cases "p = 0") (simp_all add: leading_coeff_neq_0)
   149 
   150 lemma eq_zero_or_degree_less:
   151   assumes "degree p \<le> n" and "coeff p n = 0"
   152   shows "p = 0 \<or> degree p < n"
   153 proof (cases n)
   154   case 0
   155   with \<open>degree p \<le> n\<close> and \<open>coeff p n = 0\<close> have "coeff p (degree p) = 0"
   156     by simp
   157   then have "p = 0" by simp
   158   then show ?thesis ..
   159 next
   160   case (Suc m)
   161   from \<open>degree p \<le> n\<close> have "\<forall>i>n. coeff p i = 0"
   162     by (simp add: coeff_eq_0)
   163   with \<open>coeff p n = 0\<close> have "\<forall>i\<ge>n. coeff p i = 0"
   164     by (simp add: le_less)
   165   with \<open>n = Suc m\<close> have "\<forall>i>m. coeff p i = 0"
   166     by (simp add: less_eq_Suc_le)
   167   then have "degree p \<le> m"
   168     by (rule degree_le)
   169   with \<open>n = Suc m\<close> have "degree p < n"
   170     by (simp add: less_Suc_eq_le)
   171   then show ?thesis ..
   172 qed
   173 
   174 lemma coeff_0_degree_minus_1: "coeff rrr dr = 0 \<Longrightarrow> degree rrr \<le> dr \<Longrightarrow> degree rrr \<le> dr - 1"
   175   using eq_zero_or_degree_less by fastforce
   176 
   177 
   178 subsection \<open>List-style constructor for polynomials\<close>
   179 
   180 lift_definition pCons :: "'a::zero \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
   181   is "\<lambda>a p. case_nat a (coeff p)"
   182   by (rule MOST_SucD) (simp add: MOST_coeff_eq_0)
   183 
   184 lemmas coeff_pCons = pCons.rep_eq
   185 
   186 lemma coeff_pCons_0 [simp]: "coeff (pCons a p) 0 = a"
   187   by transfer simp
   188 
   189 lemma coeff_pCons_Suc [simp]: "coeff (pCons a p) (Suc n) = coeff p n"
   190   by (simp add: coeff_pCons)
   191 
   192 lemma degree_pCons_le: "degree (pCons a p) \<le> Suc (degree p)"
   193   by (rule degree_le) (simp add: coeff_eq_0 coeff_pCons split: nat.split)
   194 
   195 lemma degree_pCons_eq: "p \<noteq> 0 \<Longrightarrow> degree (pCons a p) = Suc (degree p)"
   196   apply (rule order_antisym [OF degree_pCons_le])
   197   apply (rule le_degree, simp)
   198   done
   199 
   200 lemma degree_pCons_0: "degree (pCons a 0) = 0"
   201   apply (rule order_antisym [OF _ le0])
   202   apply (rule degree_le, simp add: coeff_pCons split: nat.split)
   203   done
   204 
   205 lemma degree_pCons_eq_if [simp]: "degree (pCons a p) = (if p = 0 then 0 else Suc (degree p))"
   206   apply (cases "p = 0", simp_all)
   207   apply (rule order_antisym [OF _ le0])
   208   apply (rule degree_le, simp add: coeff_pCons split: nat.split)
   209   apply (rule order_antisym [OF degree_pCons_le])
   210   apply (rule le_degree, simp)
   211   done
   212 
   213 lemma pCons_0_0 [simp]: "pCons 0 0 = 0"
   214   by (rule poly_eqI) (simp add: coeff_pCons split: nat.split)
   215 
   216 lemma pCons_eq_iff [simp]: "pCons a p = pCons b q \<longleftrightarrow> a = b \<and> p = q"
   217 proof safe
   218   assume "pCons a p = pCons b q"
   219   then have "coeff (pCons a p) 0 = coeff (pCons b q) 0"
   220     by simp
   221   then show "a = b"
   222     by simp
   223 next
   224   assume "pCons a p = pCons b q"
   225   then have "coeff (pCons a p) (Suc n) = coeff (pCons b q) (Suc n)" for n
   226     by simp
   227   then show "p = q"
   228     by (simp add: poly_eq_iff)
   229 qed
   230 
   231 lemma pCons_eq_0_iff [simp]: "pCons a p = 0 \<longleftrightarrow> a = 0 \<and> p = 0"
   232   using pCons_eq_iff [of a p 0 0] by simp
   233 
   234 lemma pCons_cases [cases type: poly]:
   235   obtains (pCons) a q where "p = pCons a q"
   236 proof
   237   show "p = pCons (coeff p 0) (Abs_poly (\<lambda>n. coeff p (Suc n)))"
   238     by transfer
   239       (simp_all add: MOST_inj[where f=Suc and P="\<lambda>n. p n = 0" for p] fun_eq_iff Abs_poly_inverse
   240         split: nat.split)
   241 qed
   242 
   243 lemma pCons_induct [case_names 0 pCons, induct type: poly]:
   244   assumes zero: "P 0"
   245   assumes pCons: "\<And>a p. a \<noteq> 0 \<or> p \<noteq> 0 \<Longrightarrow> P p \<Longrightarrow> P (pCons a p)"
   246   shows "P p"
   247 proof (induct p rule: measure_induct_rule [where f=degree])
   248   case (less p)
   249   obtain a q where "p = pCons a q" by (rule pCons_cases)
   250   have "P q"
   251   proof (cases "q = 0")
   252     case True
   253     then show "P q" by (simp add: zero)
   254   next
   255     case False
   256     then have "degree (pCons a q) = Suc (degree q)"
   257       by (rule degree_pCons_eq)
   258     with \<open>p = pCons a q\<close> have "degree q < degree p"
   259       by simp
   260     then show "P q"
   261       by (rule less.hyps)
   262   qed
   263   have "P (pCons a q)"
   264   proof (cases "a \<noteq> 0 \<or> q \<noteq> 0")
   265     case True
   266     with \<open>P q\<close> show ?thesis by (auto intro: pCons)
   267   next
   268     case False
   269     with zero show ?thesis by simp
   270   qed
   271   with \<open>p = pCons a q\<close> show ?case
   272     by simp
   273 qed
   274 
   275 lemma degree_eq_zeroE:
   276   fixes p :: "'a::zero poly"
   277   assumes "degree p = 0"
   278   obtains a where "p = pCons a 0"
   279 proof -
   280   obtain a q where p: "p = pCons a q"
   281     by (cases p)
   282   with assms have "q = 0"
   283     by (cases "q = 0") simp_all
   284   with p have "p = pCons a 0"
   285     by simp
   286   then show thesis ..
   287 qed
   288 
   289 
   290 subsection \<open>Quickcheck generator for polynomials\<close>
   291 
   292 quickcheck_generator poly constructors: "0 :: _ poly", pCons
   293 
   294 
   295 subsection \<open>List-style syntax for polynomials\<close>
   296 
   297 syntax "_poly" :: "args \<Rightarrow> 'a poly"  ("[:(_):]")
   298 translations
   299   "[:x, xs:]" \<rightleftharpoons> "CONST pCons x [:xs:]"
   300   "[:x:]" \<rightleftharpoons> "CONST pCons x 0"
   301   "[:x:]" \<leftharpoondown> "CONST pCons x (_constrain 0 t)"
   302 
   303 
   304 subsection \<open>Representation of polynomials by lists of coefficients\<close>
   305 
   306 primrec Poly :: "'a::zero list \<Rightarrow> 'a poly"
   307   where
   308     [code_post]: "Poly [] = 0"
   309   | [code_post]: "Poly (a # as) = pCons a (Poly as)"
   310 
   311 lemma Poly_replicate_0 [simp]: "Poly (replicate n 0) = 0"
   312   by (induct n) simp_all
   313 
   314 lemma Poly_eq_0: "Poly as = 0 \<longleftrightarrow> (\<exists>n. as = replicate n 0)"
   315   by (induct as) (auto simp add: Cons_replicate_eq)
   316 
   317 lemma Poly_append_replicate_zero [simp]: "Poly (as @ replicate n 0) = Poly as"
   318   by (induct as) simp_all
   319 
   320 lemma Poly_snoc_zero [simp]: "Poly (as @ [0]) = Poly as"
   321   using Poly_append_replicate_zero [of as 1] by simp
   322 
   323 lemma Poly_cCons_eq_pCons_Poly [simp]: "Poly (a ## p) = pCons a (Poly p)"
   324   by (simp add: cCons_def)
   325 
   326 lemma Poly_on_rev_starting_with_0 [simp]: "hd as = 0 \<Longrightarrow> Poly (rev (tl as)) = Poly (rev as)"
   327   by (cases as) simp_all
   328 
   329 lemma degree_Poly: "degree (Poly xs) \<le> length xs"
   330   by (induct xs) simp_all
   331 
   332 lemma coeff_Poly_eq [simp]: "coeff (Poly xs) = nth_default 0 xs"
   333   by (induct xs) (simp_all add: fun_eq_iff coeff_pCons split: nat.splits)
   334 
   335 definition coeffs :: "'a poly \<Rightarrow> 'a::zero list"
   336   where "coeffs p = (if p = 0 then [] else map (\<lambda>i. coeff p i) [0 ..< Suc (degree p)])"
   337 
   338 lemma coeffs_eq_Nil [simp]: "coeffs p = [] \<longleftrightarrow> p = 0"
   339   by (simp add: coeffs_def)
   340 
   341 lemma not_0_coeffs_not_Nil: "p \<noteq> 0 \<Longrightarrow> coeffs p \<noteq> []"
   342   by simp
   343 
   344 lemma coeffs_0_eq_Nil [simp]: "coeffs 0 = []"
   345   by simp
   346 
   347 lemma coeffs_pCons_eq_cCons [simp]: "coeffs (pCons a p) = a ## coeffs p"
   348 proof -
   349   have *: "\<forall>m\<in>set ms. m > 0 \<Longrightarrow> map (case_nat x f) ms = map f (map (\<lambda>n. n - 1) ms)"
   350     for ms :: "nat list" and f :: "nat \<Rightarrow> 'a" and x :: "'a"
   351     by (induct ms) (auto split: nat.split)
   352   show ?thesis
   353     by (simp add: * coeffs_def upt_conv_Cons coeff_pCons map_decr_upt del: upt_Suc)
   354 qed
   355 
   356 lemma length_coeffs: "p \<noteq> 0 \<Longrightarrow> length (coeffs p) = degree p + 1"
   357   by (simp add: coeffs_def)
   358 
   359 lemma coeffs_nth: "p \<noteq> 0 \<Longrightarrow> n \<le> degree p \<Longrightarrow> coeffs p ! n = coeff p n"
   360   by (auto simp: coeffs_def simp del: upt_Suc)
   361 
   362 lemma coeff_in_coeffs: "p \<noteq> 0 \<Longrightarrow> n \<le> degree p \<Longrightarrow> coeff p n \<in> set (coeffs p)"
   363   using coeffs_nth [of p n, symmetric] by (simp add: length_coeffs)
   364 
   365 lemma not_0_cCons_eq [simp]: "p \<noteq> 0 \<Longrightarrow> a ## coeffs p = a # coeffs p"
   366   by (simp add: cCons_def)
   367 
   368 lemma Poly_coeffs [simp, code abstype]: "Poly (coeffs p) = p"
   369   by (induct p) auto
   370 
   371 lemma coeffs_Poly [simp]: "coeffs (Poly as) = strip_while (HOL.eq 0) as"
   372 proof (induct as)
   373   case Nil
   374   then show ?case by simp
   375 next
   376   case (Cons a as)
   377   from replicate_length_same [of as 0] have "(\<forall>n. as \<noteq> replicate n 0) \<longleftrightarrow> (\<exists>a\<in>set as. a \<noteq> 0)"
   378     by (auto dest: sym [of _ as])
   379   with Cons show ?case by auto
   380 qed
   381 
   382 lemma no_trailing_coeffs [simp]:
   383   "no_trailing (HOL.eq 0) (coeffs p)"
   384   by (induct p)  auto
   385 
   386 lemma strip_while_coeffs [simp]:
   387   "strip_while (HOL.eq 0) (coeffs p) = coeffs p"
   388   by simp
   389 
   390 lemma coeffs_eq_iff: "p = q \<longleftrightarrow> coeffs p = coeffs q"
   391   (is "?P \<longleftrightarrow> ?Q")
   392 proof
   393   assume ?P
   394   then show ?Q by simp
   395 next
   396   assume ?Q
   397   then have "Poly (coeffs p) = Poly (coeffs q)" by simp
   398   then show ?P by simp
   399 qed
   400 
   401 lemma nth_default_coeffs_eq: "nth_default 0 (coeffs p) = coeff p"
   402   by (simp add: fun_eq_iff coeff_Poly_eq [symmetric])
   403 
   404 lemma [code]: "coeff p = nth_default 0 (coeffs p)"
   405   by (simp add: nth_default_coeffs_eq)
   406 
   407 lemma coeffs_eqI:
   408   assumes coeff: "\<And>n. coeff p n = nth_default 0 xs n"
   409   assumes zero: "no_trailing (HOL.eq 0) xs"
   410   shows "coeffs p = xs"
   411 proof -
   412   from coeff have "p = Poly xs"
   413     by (simp add: poly_eq_iff)
   414   with zero show ?thesis by simp
   415 qed
   416 
   417 lemma degree_eq_length_coeffs [code]: "degree p = length (coeffs p) - 1"
   418   by (simp add: coeffs_def)
   419 
   420 lemma length_coeffs_degree: "p \<noteq> 0 \<Longrightarrow> length (coeffs p) = Suc (degree p)"
   421   by (induct p) (auto simp: cCons_def)
   422 
   423 lemma [code abstract]: "coeffs 0 = []"
   424   by (fact coeffs_0_eq_Nil)
   425 
   426 lemma [code abstract]: "coeffs (pCons a p) = a ## coeffs p"
   427   by (fact coeffs_pCons_eq_cCons)
   428 
   429 lemma set_coeffs_subset_singleton_0_iff [simp]:
   430   "set (coeffs p) \<subseteq> {0} \<longleftrightarrow> p = 0"
   431   by (auto simp add: coeffs_def intro: classical)
   432 
   433 lemma set_coeffs_not_only_0 [simp]:
   434   "set (coeffs p) \<noteq> {0}"
   435   by (auto simp add: set_eq_subset)
   436 
   437 lemma forall_coeffs_conv:
   438   "(\<forall>n. P (coeff p n)) \<longleftrightarrow> (\<forall>c \<in> set (coeffs p). P c)" if "P 0"
   439   using that by (auto simp add: coeffs_def)
   440     (metis atLeastLessThan_iff coeff_eq_0 not_less_iff_gr_or_eq zero_le)
   441 
   442 instantiation poly :: ("{zero, equal}") equal
   443 begin
   444 
   445 definition [code]: "HOL.equal (p::'a poly) q \<longleftrightarrow> HOL.equal (coeffs p) (coeffs q)"
   446 
   447 instance
   448   by standard (simp add: equal equal_poly_def coeffs_eq_iff)
   449 
   450 end
   451 
   452 lemma [code nbe]: "HOL.equal (p :: _ poly) p \<longleftrightarrow> True"
   453   by (fact equal_refl)
   454 
   455 definition is_zero :: "'a::zero poly \<Rightarrow> bool"
   456   where [code]: "is_zero p \<longleftrightarrow> List.null (coeffs p)"
   457 
   458 lemma is_zero_null [code_abbrev]: "is_zero p \<longleftrightarrow> p = 0"
   459   by (simp add: is_zero_def null_def)
   460 
   461 
   462 subsubsection \<open>Reconstructing the polynomial from the list\<close>
   463   \<comment> \<open>contributed by Sebastiaan J.C. Joosten and René Thiemann\<close>
   464 
   465 definition poly_of_list :: "'a::comm_monoid_add list \<Rightarrow> 'a poly"
   466   where [simp]: "poly_of_list = Poly"
   467 
   468 lemma poly_of_list_impl [code abstract]: "coeffs (poly_of_list as) = strip_while (HOL.eq 0) as"
   469   by simp
   470 
   471 
   472 subsection \<open>Fold combinator for polynomials\<close>
   473 
   474 definition fold_coeffs :: "('a::zero \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a poly \<Rightarrow> 'b \<Rightarrow> 'b"
   475   where "fold_coeffs f p = foldr f (coeffs p)"
   476 
   477 lemma fold_coeffs_0_eq [simp]: "fold_coeffs f 0 = id"
   478   by (simp add: fold_coeffs_def)
   479 
   480 lemma fold_coeffs_pCons_eq [simp]: "f 0 = id \<Longrightarrow> fold_coeffs f (pCons a p) = f a \<circ> fold_coeffs f p"
   481   by (simp add: fold_coeffs_def cCons_def fun_eq_iff)
   482 
   483 lemma fold_coeffs_pCons_0_0_eq [simp]: "fold_coeffs f (pCons 0 0) = id"
   484   by (simp add: fold_coeffs_def)
   485 
   486 lemma fold_coeffs_pCons_coeff_not_0_eq [simp]:
   487   "a \<noteq> 0 \<Longrightarrow> fold_coeffs f (pCons a p) = f a \<circ> fold_coeffs f p"
   488   by (simp add: fold_coeffs_def)
   489 
   490 lemma fold_coeffs_pCons_not_0_0_eq [simp]:
   491   "p \<noteq> 0 \<Longrightarrow> fold_coeffs f (pCons a p) = f a \<circ> fold_coeffs f p"
   492   by (simp add: fold_coeffs_def)
   493 
   494 
   495 subsection \<open>Canonical morphism on polynomials -- evaluation\<close>
   496 
   497 definition poly :: "'a::comm_semiring_0 poly \<Rightarrow> 'a \<Rightarrow> 'a"
   498   where "poly p = fold_coeffs (\<lambda>a f x. a + x * f x) p (\<lambda>x. 0)" \<comment> \<open>The Horner Schema\<close>
   499 
   500 lemma poly_0 [simp]: "poly 0 x = 0"
   501   by (simp add: poly_def)
   502 
   503 lemma poly_pCons [simp]: "poly (pCons a p) x = a + x * poly p x"
   504   by (cases "p = 0 \<and> a = 0") (auto simp add: poly_def)
   505 
   506 lemma poly_altdef: "poly p x = (\<Sum>i\<le>degree p. coeff p i * x ^ i)"
   507   for x :: "'a::{comm_semiring_0,semiring_1}"
   508 proof (induction p rule: pCons_induct)
   509   case 0
   510   then show ?case
   511     by simp
   512 next
   513   case (pCons a p)
   514   show ?case
   515   proof (cases "p = 0")
   516     case True
   517     then show ?thesis by simp
   518   next
   519     case False
   520     let ?p' = "pCons a p"
   521     note poly_pCons[of a p x]
   522     also note pCons.IH
   523     also have "a + x * (\<Sum>i\<le>degree p. coeff p i * x ^ i) =
   524         coeff ?p' 0 * x^0 + (\<Sum>i\<le>degree p. coeff ?p' (Suc i) * x^Suc i)"
   525       by (simp add: field_simps sum_distrib_left coeff_pCons)
   526     also note sum_atMost_Suc_shift[symmetric]
   527     also note degree_pCons_eq[OF \<open>p \<noteq> 0\<close>, of a, symmetric]
   528     finally show ?thesis .
   529   qed
   530 qed
   531 
   532 lemma poly_0_coeff_0: "poly p 0 = coeff p 0"
   533   by (cases p) (auto simp: poly_altdef)
   534 
   535 
   536 subsection \<open>Monomials\<close>
   537 
   538 lift_definition monom :: "'a \<Rightarrow> nat \<Rightarrow> 'a::zero poly"
   539   is "\<lambda>a m n. if m = n then a else 0"
   540   by (simp add: MOST_iff_cofinite)
   541 
   542 lemma coeff_monom [simp]: "coeff (monom a m) n = (if m = n then a else 0)"
   543   by transfer rule
   544 
   545 lemma monom_0: "monom a 0 = pCons a 0"
   546   by (rule poly_eqI) (simp add: coeff_pCons split: nat.split)
   547 
   548 lemma monom_Suc: "monom a (Suc n) = pCons 0 (monom a n)"
   549   by (rule poly_eqI) (simp add: coeff_pCons split: nat.split)
   550 
   551 lemma monom_eq_0 [simp]: "monom 0 n = 0"
   552   by (rule poly_eqI) simp
   553 
   554 lemma monom_eq_0_iff [simp]: "monom a n = 0 \<longleftrightarrow> a = 0"
   555   by (simp add: poly_eq_iff)
   556 
   557 lemma monom_eq_iff [simp]: "monom a n = monom b n \<longleftrightarrow> a = b"
   558   by (simp add: poly_eq_iff)
   559 
   560 lemma degree_monom_le: "degree (monom a n) \<le> n"
   561   by (rule degree_le, simp)
   562 
   563 lemma degree_monom_eq: "a \<noteq> 0 \<Longrightarrow> degree (monom a n) = n"
   564   apply (rule order_antisym [OF degree_monom_le])
   565   apply (rule le_degree)
   566   apply simp
   567   done
   568 
   569 lemma coeffs_monom [code abstract]:
   570   "coeffs (monom a n) = (if a = 0 then [] else replicate n 0 @ [a])"
   571   by (induct n) (simp_all add: monom_0 monom_Suc)
   572 
   573 lemma fold_coeffs_monom [simp]: "a \<noteq> 0 \<Longrightarrow> fold_coeffs f (monom a n) = f 0 ^^ n \<circ> f a"
   574   by (simp add: fold_coeffs_def coeffs_monom fun_eq_iff)
   575 
   576 lemma poly_monom: "poly (monom a n) x = a * x ^ n"
   577   for a x :: "'a::comm_semiring_1"
   578   by (cases "a = 0", simp_all) (induct n, simp_all add: mult.left_commute poly_def)
   579 
   580 lemma monom_eq_iff': "monom c n = monom d m \<longleftrightarrow>  c = d \<and> (c = 0 \<or> n = m)"
   581   by (auto simp: poly_eq_iff)
   582 
   583 lemma monom_eq_const_iff: "monom c n = [:d:] \<longleftrightarrow> c = d \<and> (c = 0 \<or> n = 0)"
   584   using monom_eq_iff'[of c n d 0] by (simp add: monom_0)
   585 
   586 
   587 subsection \<open>Leading coefficient\<close>
   588 
   589 abbreviation lead_coeff:: "'a::zero poly \<Rightarrow> 'a"
   590   where "lead_coeff p \<equiv> coeff p (degree p)"
   591 
   592 lemma lead_coeff_pCons[simp]:
   593   "p \<noteq> 0 \<Longrightarrow> lead_coeff (pCons a p) = lead_coeff p"
   594   "p = 0 \<Longrightarrow> lead_coeff (pCons a p) = a"
   595   by auto
   596 
   597 lemma lead_coeff_monom [simp]: "lead_coeff (monom c n) = c"
   598   by (cases "c = 0") (simp_all add: degree_monom_eq)
   599 
   600 lemma last_coeffs_eq_coeff_degree:
   601   "last (coeffs p) = lead_coeff p" if "p \<noteq> 0"
   602   using that by (simp add: coeffs_def)
   603   
   604 
   605 subsection \<open>Addition and subtraction\<close>
   606 
   607 instantiation poly :: (comm_monoid_add) comm_monoid_add
   608 begin
   609 
   610 lift_definition plus_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
   611   is "\<lambda>p q n. coeff p n + coeff q n"
   612 proof -
   613   fix q p :: "'a poly"
   614   show "\<forall>\<^sub>\<infinity>n. coeff p n + coeff q n = 0"
   615     using MOST_coeff_eq_0[of p] MOST_coeff_eq_0[of q] by eventually_elim simp
   616 qed
   617 
   618 lemma coeff_add [simp]: "coeff (p + q) n = coeff p n + coeff q n"
   619   by (simp add: plus_poly.rep_eq)
   620 
   621 instance
   622 proof
   623   fix p q r :: "'a poly"
   624   show "(p + q) + r = p + (q + r)"
   625     by (simp add: poly_eq_iff add.assoc)
   626   show "p + q = q + p"
   627     by (simp add: poly_eq_iff add.commute)
   628   show "0 + p = p"
   629     by (simp add: poly_eq_iff)
   630 qed
   631 
   632 end
   633 
   634 instantiation poly :: (cancel_comm_monoid_add) cancel_comm_monoid_add
   635 begin
   636 
   637 lift_definition minus_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
   638   is "\<lambda>p q n. coeff p n - coeff q n"
   639 proof -
   640   fix q p :: "'a poly"
   641   show "\<forall>\<^sub>\<infinity>n. coeff p n - coeff q n = 0"
   642     using MOST_coeff_eq_0[of p] MOST_coeff_eq_0[of q] by eventually_elim simp
   643 qed
   644 
   645 lemma coeff_diff [simp]: "coeff (p - q) n = coeff p n - coeff q n"
   646   by (simp add: minus_poly.rep_eq)
   647 
   648 instance
   649 proof
   650   fix p q r :: "'a poly"
   651   show "p + q - p = q"
   652     by (simp add: poly_eq_iff)
   653   show "p - q - r = p - (q + r)"
   654     by (simp add: poly_eq_iff diff_diff_eq)
   655 qed
   656 
   657 end
   658 
   659 instantiation poly :: (ab_group_add) ab_group_add
   660 begin
   661 
   662 lift_definition uminus_poly :: "'a poly \<Rightarrow> 'a poly"
   663   is "\<lambda>p n. - coeff p n"
   664 proof -
   665   fix p :: "'a poly"
   666   show "\<forall>\<^sub>\<infinity>n. - coeff p n = 0"
   667     using MOST_coeff_eq_0 by simp
   668 qed
   669 
   670 lemma coeff_minus [simp]: "coeff (- p) n = - coeff p n"
   671   by (simp add: uminus_poly.rep_eq)
   672 
   673 instance
   674 proof
   675   fix p q :: "'a poly"
   676   show "- p + p = 0"
   677     by (simp add: poly_eq_iff)
   678   show "p - q = p + - q"
   679     by (simp add: poly_eq_iff)
   680 qed
   681 
   682 end
   683 
   684 lemma add_pCons [simp]: "pCons a p + pCons b q = pCons (a + b) (p + q)"
   685   by (rule poly_eqI) (simp add: coeff_pCons split: nat.split)
   686 
   687 lemma minus_pCons [simp]: "- pCons a p = pCons (- a) (- p)"
   688   by (rule poly_eqI) (simp add: coeff_pCons split: nat.split)
   689 
   690 lemma diff_pCons [simp]: "pCons a p - pCons b q = pCons (a - b) (p - q)"
   691   by (rule poly_eqI) (simp add: coeff_pCons split: nat.split)
   692 
   693 lemma degree_add_le_max: "degree (p + q) \<le> max (degree p) (degree q)"
   694   by (rule degree_le) (auto simp add: coeff_eq_0)
   695 
   696 lemma degree_add_le: "degree p \<le> n \<Longrightarrow> degree q \<le> n \<Longrightarrow> degree (p + q) \<le> n"
   697   by (auto intro: order_trans degree_add_le_max)
   698 
   699 lemma degree_add_less: "degree p < n \<Longrightarrow> degree q < n \<Longrightarrow> degree (p + q) < n"
   700   by (auto intro: le_less_trans degree_add_le_max)
   701 
   702 lemma degree_add_eq_right: "degree p < degree q \<Longrightarrow> degree (p + q) = degree q"
   703   apply (cases "q = 0")
   704    apply simp
   705   apply (rule order_antisym)
   706    apply (simp add: degree_add_le)
   707   apply (rule le_degree)
   708   apply (simp add: coeff_eq_0)
   709   done
   710 
   711 lemma degree_add_eq_left: "degree q < degree p \<Longrightarrow> degree (p + q) = degree p"
   712   using degree_add_eq_right [of q p] by (simp add: add.commute)
   713 
   714 lemma degree_minus [simp]: "degree (- p) = degree p"
   715   by (simp add: degree_def)
   716 
   717 lemma lead_coeff_add_le: "degree p < degree q \<Longrightarrow> lead_coeff (p + q) = lead_coeff q"
   718   by (metis coeff_add coeff_eq_0 monoid_add_class.add.left_neutral degree_add_eq_right)
   719 
   720 lemma lead_coeff_minus: "lead_coeff (- p) = - lead_coeff p"
   721   by (metis coeff_minus degree_minus)
   722 
   723 lemma degree_diff_le_max: "degree (p - q) \<le> max (degree p) (degree q)"
   724   for p q :: "'a::ab_group_add poly"
   725   using degree_add_le [where p=p and q="-q"] by simp
   726 
   727 lemma degree_diff_le: "degree p \<le> n \<Longrightarrow> degree q \<le> n \<Longrightarrow> degree (p - q) \<le> n"
   728   for p q :: "'a::ab_group_add poly"
   729   using degree_add_le [of p n "- q"] by simp
   730 
   731 lemma degree_diff_less: "degree p < n \<Longrightarrow> degree q < n \<Longrightarrow> degree (p - q) < n"
   732   for p q :: "'a::ab_group_add poly"
   733   using degree_add_less [of p n "- q"] by simp
   734 
   735 lemma add_monom: "monom a n + monom b n = monom (a + b) n"
   736   by (rule poly_eqI) simp
   737 
   738 lemma diff_monom: "monom a n - monom b n = monom (a - b) n"
   739   by (rule poly_eqI) simp
   740 
   741 lemma minus_monom: "- monom a n = monom (- a) n"
   742   by (rule poly_eqI) simp
   743 
   744 lemma coeff_sum: "coeff (\<Sum>x\<in>A. p x) i = (\<Sum>x\<in>A. coeff (p x) i)"
   745   by (induct A rule: infinite_finite_induct) simp_all
   746 
   747 lemma monom_sum: "monom (\<Sum>x\<in>A. a x) n = (\<Sum>x\<in>A. monom (a x) n)"
   748   by (rule poly_eqI) (simp add: coeff_sum)
   749 
   750 fun plus_coeffs :: "'a::comm_monoid_add list \<Rightarrow> 'a list \<Rightarrow> 'a list"
   751   where
   752     "plus_coeffs xs [] = xs"
   753   | "plus_coeffs [] ys = ys"
   754   | "plus_coeffs (x # xs) (y # ys) = (x + y) ## plus_coeffs xs ys"
   755 
   756 lemma coeffs_plus_eq_plus_coeffs [code abstract]:
   757   "coeffs (p + q) = plus_coeffs (coeffs p) (coeffs q)"
   758 proof -
   759   have *: "nth_default 0 (plus_coeffs xs ys) n = nth_default 0 xs n + nth_default 0 ys n"
   760     for xs ys :: "'a list" and n
   761   proof (induct xs ys arbitrary: n rule: plus_coeffs.induct)
   762     case (3 x xs y ys n)
   763     then show ?case
   764       by (cases n) (auto simp add: cCons_def)
   765   qed simp_all
   766   have **: "no_trailing (HOL.eq 0) (plus_coeffs xs ys)"
   767     if "no_trailing (HOL.eq 0) xs" and "no_trailing (HOL.eq 0) ys"
   768     for xs ys :: "'a list"
   769     using that by (induct xs ys rule: plus_coeffs.induct) (simp_all add: cCons_def)
   770   show ?thesis
   771     by (rule coeffs_eqI) (auto simp add: * nth_default_coeffs_eq intro: **)
   772 qed
   773 
   774 lemma coeffs_uminus [code abstract]:
   775   "coeffs (- p) = map uminus (coeffs p)"
   776 proof -
   777   have eq_0: "HOL.eq 0 \<circ> uminus = HOL.eq (0::'a)"
   778     by (simp add: fun_eq_iff)
   779   show ?thesis
   780     by (rule coeffs_eqI) (simp_all add: nth_default_map_eq nth_default_coeffs_eq no_trailing_map eq_0)
   781 qed
   782 
   783 lemma [code]: "p - q = p + - q"
   784   for p q :: "'a::ab_group_add poly"
   785   by (fact diff_conv_add_uminus)
   786 
   787 lemma poly_add [simp]: "poly (p + q) x = poly p x + poly q x"
   788   apply (induct p arbitrary: q)
   789    apply simp
   790   apply (case_tac q, simp, simp add: algebra_simps)
   791   done
   792 
   793 lemma poly_minus [simp]: "poly (- p) x = - poly p x"
   794   for x :: "'a::comm_ring"
   795   by (induct p) simp_all
   796 
   797 lemma poly_diff [simp]: "poly (p - q) x = poly p x - poly q x"
   798   for x :: "'a::comm_ring"
   799   using poly_add [of p "- q" x] by simp
   800 
   801 lemma poly_sum: "poly (\<Sum>k\<in>A. p k) x = (\<Sum>k\<in>A. poly (p k) x)"
   802   by (induct A rule: infinite_finite_induct) simp_all
   803 
   804 lemma degree_sum_le: "finite S \<Longrightarrow> (\<And>p. p \<in> S \<Longrightarrow> degree (f p) \<le> n) \<Longrightarrow> degree (sum f S) \<le> n"
   805 proof (induct S rule: finite_induct)
   806   case empty
   807   then show ?case by simp
   808 next
   809   case (insert p S)
   810   then have "degree (sum f S) \<le> n" "degree (f p) \<le> n"
   811     by auto
   812   then show ?case
   813     unfolding sum.insert[OF insert(1-2)] by (metis degree_add_le)
   814 qed
   815 
   816 lemma poly_as_sum_of_monoms':
   817   assumes "degree p \<le> n"
   818   shows "(\<Sum>i\<le>n. monom (coeff p i) i) = p"
   819 proof -
   820   have eq: "\<And>i. {..n} \<inter> {i} = (if i \<le> n then {i} else {})"
   821     by auto
   822   from assms show ?thesis
   823     by (simp add: poly_eq_iff coeff_sum coeff_eq_0 sum.If_cases eq
   824         if_distrib[where f="\<lambda>x. x * a" for a])
   825 qed
   826 
   827 lemma poly_as_sum_of_monoms: "(\<Sum>i\<le>degree p. monom (coeff p i) i) = p"
   828   by (intro poly_as_sum_of_monoms' order_refl)
   829 
   830 lemma Poly_snoc: "Poly (xs @ [x]) = Poly xs + monom x (length xs)"
   831   by (induct xs) (simp_all add: monom_0 monom_Suc)
   832 
   833 
   834 subsection \<open>Multiplication by a constant, polynomial multiplication and the unit polynomial\<close>
   835 
   836 lift_definition smult :: "'a::comm_semiring_0 \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
   837   is "\<lambda>a p n. a * coeff p n"
   838 proof -
   839   fix a :: 'a and p :: "'a poly"
   840   show "\<forall>\<^sub>\<infinity> i. a * coeff p i = 0"
   841     using MOST_coeff_eq_0[of p] by eventually_elim simp
   842 qed
   843 
   844 lemma coeff_smult [simp]: "coeff (smult a p) n = a * coeff p n"
   845   by (simp add: smult.rep_eq)
   846 
   847 lemma degree_smult_le: "degree (smult a p) \<le> degree p"
   848   by (rule degree_le) (simp add: coeff_eq_0)
   849 
   850 lemma smult_smult [simp]: "smult a (smult b p) = smult (a * b) p"
   851   by (rule poly_eqI) (simp add: mult.assoc)
   852 
   853 lemma smult_0_right [simp]: "smult a 0 = 0"
   854   by (rule poly_eqI) simp
   855 
   856 lemma smult_0_left [simp]: "smult 0 p = 0"
   857   by (rule poly_eqI) simp
   858 
   859 lemma smult_1_left [simp]: "smult (1::'a::comm_semiring_1) p = p"
   860   by (rule poly_eqI) simp
   861 
   862 lemma smult_add_right: "smult a (p + q) = smult a p + smult a q"
   863   by (rule poly_eqI) (simp add: algebra_simps)
   864 
   865 lemma smult_add_left: "smult (a + b) p = smult a p + smult b p"
   866   by (rule poly_eqI) (simp add: algebra_simps)
   867 
   868 lemma smult_minus_right [simp]: "smult a (- p) = - smult a p"
   869   for a :: "'a::comm_ring"
   870   by (rule poly_eqI) simp
   871 
   872 lemma smult_minus_left [simp]: "smult (- a) p = - smult a p"
   873   for a :: "'a::comm_ring"
   874   by (rule poly_eqI) simp
   875 
   876 lemma smult_diff_right: "smult a (p - q) = smult a p - smult a q"
   877   for a :: "'a::comm_ring"
   878   by (rule poly_eqI) (simp add: algebra_simps)
   879 
   880 lemma smult_diff_left: "smult (a - b) p = smult a p - smult b p"
   881   for a b :: "'a::comm_ring"
   882   by (rule poly_eqI) (simp add: algebra_simps)
   883 
   884 lemmas smult_distribs =
   885   smult_add_left smult_add_right
   886   smult_diff_left smult_diff_right
   887 
   888 lemma smult_pCons [simp]: "smult a (pCons b p) = pCons (a * b) (smult a p)"
   889   by (rule poly_eqI) (simp add: coeff_pCons split: nat.split)
   890 
   891 lemma smult_monom: "smult a (monom b n) = monom (a * b) n"
   892   by (induct n) (simp_all add: monom_0 monom_Suc)
   893 
   894 lemma smult_Poly: "smult c (Poly xs) = Poly (map (op * c) xs)"
   895   by (auto simp: poly_eq_iff nth_default_def)
   896 
   897 lemma degree_smult_eq [simp]: "degree (smult a p) = (if a = 0 then 0 else degree p)"
   898   for a :: "'a::{comm_semiring_0,semiring_no_zero_divisors}"
   899   by (cases "a = 0") (simp_all add: degree_def)
   900 
   901 lemma smult_eq_0_iff [simp]: "smult a p = 0 \<longleftrightarrow> a = 0 \<or> p = 0"
   902   for a :: "'a::{comm_semiring_0,semiring_no_zero_divisors}"
   903   by (simp add: poly_eq_iff)
   904 
   905 lemma coeffs_smult [code abstract]:
   906   "coeffs (smult a p) = (if a = 0 then [] else map (Groups.times a) (coeffs p))"
   907   for p :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly"
   908 proof -
   909   have eq_0: "HOL.eq 0 \<circ> times a = HOL.eq (0::'a)" if "a \<noteq> 0"
   910     using that by (simp add: fun_eq_iff)
   911   show ?thesis
   912     by (rule coeffs_eqI) (auto simp add: no_trailing_map nth_default_map_eq nth_default_coeffs_eq eq_0)
   913 qed  
   914 
   915 lemma smult_eq_iff:
   916   fixes b :: "'a :: field"
   917   assumes "b \<noteq> 0"
   918   shows "smult a p = smult b q \<longleftrightarrow> smult (a / b) p = q"
   919     (is "?lhs \<longleftrightarrow> ?rhs")
   920 proof
   921   assume ?lhs
   922   also from assms have "smult (inverse b) \<dots> = q"
   923     by simp
   924   finally show ?rhs
   925     by (simp add: field_simps)
   926 next
   927   assume ?rhs
   928   with assms show ?lhs by auto
   929 qed
   930 
   931 instantiation poly :: (comm_semiring_0) comm_semiring_0
   932 begin
   933 
   934 definition "p * q = fold_coeffs (\<lambda>a p. smult a q + pCons 0 p) p 0"
   935 
   936 lemma mult_poly_0_left: "(0::'a poly) * q = 0"
   937   by (simp add: times_poly_def)
   938 
   939 lemma mult_pCons_left [simp]: "pCons a p * q = smult a q + pCons 0 (p * q)"
   940   by (cases "p = 0 \<and> a = 0") (auto simp add: times_poly_def)
   941 
   942 lemma mult_poly_0_right: "p * (0::'a poly) = 0"
   943   by (induct p) (simp_all add: mult_poly_0_left)
   944 
   945 lemma mult_pCons_right [simp]: "p * pCons a q = smult a p + pCons 0 (p * q)"
   946   by (induct p) (simp_all add: mult_poly_0_left algebra_simps)
   947 
   948 lemmas mult_poly_0 = mult_poly_0_left mult_poly_0_right
   949 
   950 lemma mult_smult_left [simp]: "smult a p * q = smult a (p * q)"
   951   by (induct p) (simp_all add: mult_poly_0 smult_add_right)
   952 
   953 lemma mult_smult_right [simp]: "p * smult a q = smult a (p * q)"
   954   by (induct q) (simp_all add: mult_poly_0 smult_add_right)
   955 
   956 lemma mult_poly_add_left: "(p + q) * r = p * r + q * r"
   957   for p q r :: "'a poly"
   958   by (induct r) (simp_all add: mult_poly_0 smult_distribs algebra_simps)
   959 
   960 instance
   961 proof
   962   fix p q r :: "'a poly"
   963   show 0: "0 * p = 0"
   964     by (rule mult_poly_0_left)
   965   show "p * 0 = 0"
   966     by (rule mult_poly_0_right)
   967   show "(p + q) * r = p * r + q * r"
   968     by (rule mult_poly_add_left)
   969   show "(p * q) * r = p * (q * r)"
   970     by (induct p) (simp_all add: mult_poly_0 mult_poly_add_left)
   971   show "p * q = q * p"
   972     by (induct p) (simp_all add: mult_poly_0)
   973 qed
   974 
   975 end
   976 
   977 lemma coeff_mult_degree_sum:
   978   "coeff (p * q) (degree p + degree q) = coeff p (degree p) * coeff q (degree q)"
   979   by (induct p) (simp_all add: coeff_eq_0)
   980 
   981 instance poly :: ("{comm_semiring_0,semiring_no_zero_divisors}") semiring_no_zero_divisors
   982 proof
   983   fix p q :: "'a poly"
   984   assume "p \<noteq> 0" and "q \<noteq> 0"
   985   have "coeff (p * q) (degree p + degree q) = coeff p (degree p) * coeff q (degree q)"
   986     by (rule coeff_mult_degree_sum)
   987   also from \<open>p \<noteq> 0\<close> \<open>q \<noteq> 0\<close> have "coeff p (degree p) * coeff q (degree q) \<noteq> 0"
   988     by simp
   989   finally have "\<exists>n. coeff (p * q) n \<noteq> 0" ..
   990   then show "p * q \<noteq> 0"
   991     by (simp add: poly_eq_iff)
   992 qed
   993 
   994 instance poly :: (comm_semiring_0_cancel) comm_semiring_0_cancel ..
   995 
   996 lemma coeff_mult: "coeff (p * q) n = (\<Sum>i\<le>n. coeff p i * coeff q (n-i))"
   997 proof (induct p arbitrary: n)
   998   case 0
   999   show ?case by simp
  1000 next
  1001   case (pCons a p n)
  1002   then show ?case
  1003     by (cases n) (simp_all add: sum_atMost_Suc_shift del: sum_atMost_Suc)
  1004 qed
  1005 
  1006 lemma degree_mult_le: "degree (p * q) \<le> degree p + degree q"
  1007   apply (rule degree_le)
  1008   apply (induct p)
  1009    apply simp
  1010   apply (simp add: coeff_eq_0 coeff_pCons split: nat.split)
  1011   done
  1012 
  1013 lemma mult_monom: "monom a m * monom b n = monom (a * b) (m + n)"
  1014   by (induct m) (simp add: monom_0 smult_monom, simp add: monom_Suc)
  1015 
  1016 instantiation poly :: (comm_semiring_1) comm_semiring_1
  1017 begin
  1018 
  1019 lift_definition one_poly :: "'a poly"
  1020   is "\<lambda>n. of_bool (n = 0)"
  1021   by (rule MOST_SucD) simp
  1022 
  1023 lemma coeff_1 [simp]:
  1024   "coeff 1 n = of_bool (n = 0)"
  1025   by (simp add: one_poly.rep_eq)
  1026 
  1027 lemma one_pCons:
  1028   "1 = [:1:]"
  1029   by (simp add: poly_eq_iff coeff_pCons split: nat.splits)
  1030 
  1031 lemma pCons_one:
  1032   "[:1:] = 1"
  1033   by (simp add: one_pCons)
  1034 
  1035 instance
  1036   by standard (simp_all add: one_pCons)
  1037 
  1038 end
  1039 
  1040 lemma poly_1 [simp]:
  1041   "poly 1 x = 1"
  1042   by (simp add: one_pCons)
  1043 
  1044 lemma one_poly_eq_simps [simp]:
  1045   "1 = [:1:] \<longleftrightarrow> True"
  1046   "[:1:] = 1 \<longleftrightarrow> True"
  1047   by (simp_all add: one_pCons)
  1048 
  1049 lemma degree_1 [simp]:
  1050   "degree 1 = 0"
  1051   by (simp add: one_pCons)
  1052 
  1053 lemma coeffs_1_eq [simp, code abstract]:
  1054   "coeffs 1 = [1]"
  1055   by (simp add: one_pCons)
  1056 
  1057 lemma smult_one [simp]:
  1058   "smult c 1 = [:c:]"
  1059   by (simp add: one_pCons)
  1060 
  1061 lemma monom_eq_1 [simp]:
  1062   "monom 1 0 = 1"
  1063   by (simp add: monom_0 one_pCons)
  1064 
  1065 lemma monom_eq_1_iff:
  1066   "monom c n = 1 \<longleftrightarrow> c = 1 \<and> n = 0"
  1067   using monom_eq_const_iff [of c n 1] by auto
  1068 
  1069 lemma monom_altdef:
  1070   "monom c n = smult c ([:0, 1:] ^ n)"
  1071   by (induct n) (simp_all add: monom_0 monom_Suc)  
  1072 
  1073 instance poly :: ("{comm_semiring_1,semiring_1_no_zero_divisors}") semiring_1_no_zero_divisors ..
  1074 instance poly :: (comm_ring) comm_ring ..
  1075 instance poly :: (comm_ring_1) comm_ring_1 ..
  1076 instance poly :: (comm_ring_1) comm_semiring_1_cancel ..
  1077 
  1078 lemma degree_power_le: "degree (p ^ n) \<le> degree p * n"
  1079   by (induct n) (auto intro: order_trans degree_mult_le)
  1080 
  1081 lemma coeff_0_power: "coeff (p ^ n) 0 = coeff p 0 ^ n"
  1082   by (induct n) (simp_all add: coeff_mult)
  1083 
  1084 lemma poly_smult [simp]: "poly (smult a p) x = a * poly p x"
  1085   by (induct p) (simp_all add: algebra_simps)
  1086 
  1087 lemma poly_mult [simp]: "poly (p * q) x = poly p x * poly q x"
  1088   by (induct p) (simp_all add: algebra_simps)
  1089 
  1090 lemma poly_power [simp]: "poly (p ^ n) x = poly p x ^ n"
  1091   for p :: "'a::comm_semiring_1 poly"
  1092   by (induct n) simp_all
  1093 
  1094 lemma poly_prod: "poly (\<Prod>k\<in>A. p k) x = (\<Prod>k\<in>A. poly (p k) x)"
  1095   by (induct A rule: infinite_finite_induct) simp_all
  1096 
  1097 lemma degree_prod_sum_le: "finite S \<Longrightarrow> degree (prod f S) \<le> sum (degree \<circ> f) S"
  1098 proof (induct S rule: finite_induct)
  1099   case empty
  1100   then show ?case by simp
  1101 next
  1102   case (insert a S)
  1103   show ?case
  1104     unfolding prod.insert[OF insert(1-2)] sum.insert[OF insert(1-2)]
  1105     by (rule le_trans[OF degree_mult_le]) (use insert in auto)
  1106 qed
  1107 
  1108 lemma coeff_0_prod_list: "coeff (prod_list xs) 0 = prod_list (map (\<lambda>p. coeff p 0) xs)"
  1109   by (induct xs) (simp_all add: coeff_mult)
  1110 
  1111 lemma coeff_monom_mult: "coeff (monom c n * p) k = (if k < n then 0 else c * coeff p (k - n))"
  1112 proof -
  1113   have "coeff (monom c n * p) k = (\<Sum>i\<le>k. (if n = i then c else 0) * coeff p (k - i))"
  1114     by (simp add: coeff_mult)
  1115   also have "\<dots> = (\<Sum>i\<le>k. (if n = i then c * coeff p (k - i) else 0))"
  1116     by (intro sum.cong) simp_all
  1117   also have "\<dots> = (if k < n then 0 else c * coeff p (k - n))"
  1118     by simp
  1119   finally show ?thesis .
  1120 qed
  1121 
  1122 lemma monom_1_dvd_iff': "monom 1 n dvd p \<longleftrightarrow> (\<forall>k<n. coeff p k = 0)"
  1123 proof
  1124   assume "monom 1 n dvd p"
  1125   then obtain r where "p = monom 1 n * r"
  1126     by (rule dvdE)
  1127   then show "\<forall>k<n. coeff p k = 0"
  1128     by (simp add: coeff_mult)
  1129 next
  1130   assume zero: "(\<forall>k<n. coeff p k = 0)"
  1131   define r where "r = Abs_poly (\<lambda>k. coeff p (k + n))"
  1132   have "\<forall>\<^sub>\<infinity>k. coeff p (k + n) = 0"
  1133     by (subst cofinite_eq_sequentially, subst eventually_sequentially_seg,
  1134         subst cofinite_eq_sequentially [symmetric]) transfer
  1135   then have coeff_r [simp]: "coeff r k = coeff p (k + n)" for k
  1136     unfolding r_def by (subst poly.Abs_poly_inverse) simp_all
  1137   have "p = monom 1 n * r"
  1138     by (rule poly_eqI, subst coeff_monom_mult) (simp_all add: zero)
  1139   then show "monom 1 n dvd p" by simp
  1140 qed
  1141 
  1142 
  1143 subsection \<open>Mapping polynomials\<close>
  1144 
  1145 definition map_poly :: "('a :: zero \<Rightarrow> 'b :: zero) \<Rightarrow> 'a poly \<Rightarrow> 'b poly"
  1146   where "map_poly f p = Poly (map f (coeffs p))"
  1147 
  1148 lemma map_poly_0 [simp]: "map_poly f 0 = 0"
  1149   by (simp add: map_poly_def)
  1150 
  1151 lemma map_poly_1: "map_poly f 1 = [:f 1:]"
  1152   by (simp add: map_poly_def)
  1153 
  1154 lemma map_poly_1' [simp]: "f 1 = 1 \<Longrightarrow> map_poly f 1 = 1"
  1155   by (simp add: map_poly_def one_pCons)
  1156 
  1157 lemma coeff_map_poly:
  1158   assumes "f 0 = 0"
  1159   shows "coeff (map_poly f p) n = f (coeff p n)"
  1160   by (auto simp: assms map_poly_def nth_default_def coeffs_def not_less Suc_le_eq coeff_eq_0
  1161       simp del: upt_Suc)
  1162 
  1163 lemma coeffs_map_poly [code abstract]:
  1164   "coeffs (map_poly f p) = strip_while (op = 0) (map f (coeffs p))"
  1165   by (simp add: map_poly_def)
  1166 
  1167 lemma coeffs_map_poly':
  1168   assumes "\<And>x. x \<noteq> 0 \<Longrightarrow> f x \<noteq> 0"
  1169   shows "coeffs (map_poly f p) = map f (coeffs p)"
  1170   using assms
  1171   by (auto simp add: coeffs_map_poly strip_while_idem_iff
  1172     last_coeffs_eq_coeff_degree no_trailing_unfold last_map)
  1173 
  1174 lemma set_coeffs_map_poly:
  1175   "(\<And>x. f x = 0 \<longleftrightarrow> x = 0) \<Longrightarrow> set (coeffs (map_poly f p)) = f ` set (coeffs p)"
  1176   by (simp add: coeffs_map_poly')
  1177 
  1178 lemma degree_map_poly:
  1179   assumes "\<And>x. x \<noteq> 0 \<Longrightarrow> f x \<noteq> 0"
  1180   shows "degree (map_poly f p) = degree p"
  1181   by (simp add: degree_eq_length_coeffs coeffs_map_poly' assms)
  1182 
  1183 lemma map_poly_eq_0_iff:
  1184   assumes "f 0 = 0" "\<And>x. x \<in> set (coeffs p) \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> f x \<noteq> 0"
  1185   shows "map_poly f p = 0 \<longleftrightarrow> p = 0"
  1186 proof -
  1187   have "(coeff (map_poly f p) n = 0) = (coeff p n = 0)" for n
  1188   proof -
  1189     have "coeff (map_poly f p) n = f (coeff p n)"
  1190       by (simp add: coeff_map_poly assms)
  1191     also have "\<dots> = 0 \<longleftrightarrow> coeff p n = 0"
  1192     proof (cases "n < length (coeffs p)")
  1193       case True
  1194       then have "coeff p n \<in> set (coeffs p)"
  1195         by (auto simp: coeffs_def simp del: upt_Suc)
  1196       with assms show "f (coeff p n) = 0 \<longleftrightarrow> coeff p n = 0"
  1197         by auto
  1198     next
  1199       case False
  1200       then show ?thesis
  1201         by (auto simp: assms length_coeffs nth_default_coeffs_eq [symmetric] nth_default_def)
  1202     qed
  1203     finally show ?thesis .
  1204   qed
  1205   then show ?thesis by (auto simp: poly_eq_iff)
  1206 qed
  1207 
  1208 lemma map_poly_smult:
  1209   assumes "f 0 = 0""\<And>c x. f (c * x) = f c * f x"
  1210   shows "map_poly f (smult c p) = smult (f c) (map_poly f p)"
  1211   by (intro poly_eqI) (simp_all add: assms coeff_map_poly)
  1212 
  1213 lemma map_poly_pCons:
  1214   assumes "f 0 = 0"
  1215   shows "map_poly f (pCons c p) = pCons (f c) (map_poly f p)"
  1216   by (intro poly_eqI) (simp_all add: assms coeff_map_poly coeff_pCons split: nat.splits)
  1217 
  1218 lemma map_poly_map_poly:
  1219   assumes "f 0 = 0" "g 0 = 0"
  1220   shows "map_poly f (map_poly g p) = map_poly (f \<circ> g) p"
  1221   by (intro poly_eqI) (simp add: coeff_map_poly assms)
  1222 
  1223 lemma map_poly_id [simp]: "map_poly id p = p"
  1224   by (simp add: map_poly_def)
  1225 
  1226 lemma map_poly_id' [simp]: "map_poly (\<lambda>x. x) p = p"
  1227   by (simp add: map_poly_def)
  1228 
  1229 lemma map_poly_cong:
  1230   assumes "(\<And>x. x \<in> set (coeffs p) \<Longrightarrow> f x = g x)"
  1231   shows "map_poly f p = map_poly g p"
  1232 proof -
  1233   from assms have "map f (coeffs p) = map g (coeffs p)"
  1234     by (intro map_cong) simp_all
  1235   then show ?thesis
  1236     by (simp only: coeffs_eq_iff coeffs_map_poly)
  1237 qed
  1238 
  1239 lemma map_poly_monom: "f 0 = 0 \<Longrightarrow> map_poly f (monom c n) = monom (f c) n"
  1240   by (intro poly_eqI) (simp_all add: coeff_map_poly)
  1241 
  1242 lemma map_poly_idI:
  1243   assumes "\<And>x. x \<in> set (coeffs p) \<Longrightarrow> f x = x"
  1244   shows "map_poly f p = p"
  1245   using map_poly_cong[OF assms, of _ id] by simp
  1246 
  1247 lemma map_poly_idI':
  1248   assumes "\<And>x. x \<in> set (coeffs p) \<Longrightarrow> f x = x"
  1249   shows "p = map_poly f p"
  1250   using map_poly_cong[OF assms, of _ id] by simp
  1251 
  1252 lemma smult_conv_map_poly: "smult c p = map_poly (\<lambda>x. c * x) p"
  1253   by (intro poly_eqI) (simp_all add: coeff_map_poly)
  1254 
  1255 
  1256 subsection \<open>Conversions\<close>
  1257 
  1258 lemma of_nat_poly:
  1259   "of_nat n = [:of_nat n:]"
  1260   by (induct n) (simp_all add: one_pCons)
  1261 
  1262 lemma of_nat_monom:
  1263   "of_nat n = monom (of_nat n) 0"
  1264   by (simp add: of_nat_poly monom_0)
  1265 
  1266 lemma degree_of_nat [simp]:
  1267   "degree (of_nat n) = 0"
  1268   by (simp add: of_nat_poly)
  1269 
  1270 lemma lead_coeff_of_nat [simp]:
  1271   "lead_coeff (of_nat n) = of_nat n"
  1272   by (simp add: of_nat_poly)
  1273 
  1274 lemma of_int_poly:
  1275   "of_int k = [:of_int k:]"
  1276   by (simp only: of_int_of_nat of_nat_poly) simp
  1277 
  1278 lemma of_int_monom:
  1279   "of_int k = monom (of_int k) 0"
  1280   by (simp add: of_int_poly monom_0)
  1281 
  1282 lemma degree_of_int [simp]:
  1283   "degree (of_int k) = 0"
  1284   by (simp add: of_int_poly)
  1285 
  1286 lemma lead_coeff_of_int [simp]:
  1287   "lead_coeff (of_int k) = of_int k"
  1288   by (simp add: of_int_poly)
  1289 
  1290 lemma numeral_poly: "numeral n = [:numeral n:]"
  1291 proof -
  1292   have "numeral n = of_nat (numeral n)"
  1293     by simp
  1294   also have "\<dots> = [:of_nat (numeral n):]"
  1295     by (simp add: of_nat_poly)
  1296   finally show ?thesis
  1297     by simp
  1298 qed
  1299 
  1300 lemma numeral_monom:
  1301   "numeral n = monom (numeral n) 0"
  1302   by (simp add: numeral_poly monom_0)
  1303 
  1304 lemma degree_numeral [simp]:
  1305   "degree (numeral n) = 0"
  1306   by (simp add: numeral_poly)
  1307 
  1308 lemma lead_coeff_numeral [simp]:
  1309   "lead_coeff (numeral n) = numeral n"
  1310   by (simp add: numeral_poly)
  1311 
  1312 
  1313 subsection \<open>Lemmas about divisibility\<close>
  1314 
  1315 lemma dvd_smult:
  1316   assumes "p dvd q"
  1317   shows "p dvd smult a q"
  1318 proof -
  1319   from assms obtain k where "q = p * k" ..
  1320   then have "smult a q = p * smult a k" by simp
  1321   then show "p dvd smult a q" ..
  1322 qed
  1323 
  1324 lemma dvd_smult_cancel: "p dvd smult a q \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> p dvd q"
  1325   for a :: "'a::field"
  1326   by (drule dvd_smult [where a="inverse a"]) simp
  1327 
  1328 lemma dvd_smult_iff: "a \<noteq> 0 \<Longrightarrow> p dvd smult a q \<longleftrightarrow> p dvd q"
  1329   for a :: "'a::field"
  1330   by (safe elim!: dvd_smult dvd_smult_cancel)
  1331 
  1332 lemma smult_dvd_cancel:
  1333   assumes "smult a p dvd q"
  1334   shows "p dvd q"
  1335 proof -
  1336   from assms obtain k where "q = smult a p * k" ..
  1337   then have "q = p * smult a k" by simp
  1338   then show "p dvd q" ..
  1339 qed
  1340 
  1341 lemma smult_dvd: "p dvd q \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> smult a p dvd q"
  1342   for a :: "'a::field"
  1343   by (rule smult_dvd_cancel [where a="inverse a"]) simp
  1344 
  1345 lemma smult_dvd_iff: "smult a p dvd q \<longleftrightarrow> (if a = 0 then q = 0 else p dvd q)"
  1346   for a :: "'a::field"
  1347   by (auto elim: smult_dvd smult_dvd_cancel)
  1348 
  1349 lemma is_unit_smult_iff: "smult c p dvd 1 \<longleftrightarrow> c dvd 1 \<and> p dvd 1"
  1350 proof -
  1351   have "smult c p = [:c:] * p" by simp
  1352   also have "\<dots> dvd 1 \<longleftrightarrow> c dvd 1 \<and> p dvd 1"
  1353   proof safe
  1354     assume *: "[:c:] * p dvd 1"
  1355     then show "p dvd 1"
  1356       by (rule dvd_mult_right)
  1357     from * obtain q where q: "1 = [:c:] * p * q"
  1358       by (rule dvdE)
  1359     have "c dvd c * (coeff p 0 * coeff q 0)"
  1360       by simp
  1361     also have "\<dots> = coeff ([:c:] * p * q) 0"
  1362       by (simp add: mult.assoc coeff_mult)
  1363     also note q [symmetric]
  1364     finally have "c dvd coeff 1 0" .
  1365     then show "c dvd 1" by simp
  1366   next
  1367     assume "c dvd 1" "p dvd 1"
  1368     from this(1) obtain d where "1 = c * d"
  1369       by (rule dvdE)
  1370     then have "1 = [:c:] * [:d:]"
  1371       by (simp add: one_pCons ac_simps)
  1372     then have "[:c:] dvd 1"
  1373       by (rule dvdI)
  1374     from mult_dvd_mono[OF this \<open>p dvd 1\<close>] show "[:c:] * p dvd 1"
  1375       by simp
  1376   qed
  1377   finally show ?thesis .
  1378 qed
  1379 
  1380 
  1381 subsection \<open>Polynomials form an integral domain\<close>
  1382 
  1383 instance poly :: (idom) idom ..
  1384 
  1385 instance poly :: ("{ring_char_0, comm_ring_1}") ring_char_0
  1386   by standard (auto simp add: of_nat_poly intro: injI)
  1387 
  1388 lemma degree_mult_eq: "p \<noteq> 0 \<Longrightarrow> q \<noteq> 0 \<Longrightarrow> degree (p * q) = degree p + degree q"
  1389   for p q :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly"
  1390   by (rule order_antisym [OF degree_mult_le le_degree]) (simp add: coeff_mult_degree_sum)
  1391 
  1392 lemma degree_mult_eq_0:
  1393   "degree (p * q) = 0 \<longleftrightarrow> p = 0 \<or> q = 0 \<or> (p \<noteq> 0 \<and> q \<noteq> 0 \<and> degree p = 0 \<and> degree q = 0)"
  1394   for p q :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly"
  1395   by (auto simp: degree_mult_eq)
  1396 
  1397 lemma degree_power_eq: "p \<noteq> 0 \<Longrightarrow> degree ((p :: 'a :: idom poly) ^ n) = n * degree p"
  1398   by (induction n) (simp_all add: degree_mult_eq)
  1399 
  1400 lemma degree_mult_right_le:
  1401   fixes p q :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly"
  1402   assumes "q \<noteq> 0"
  1403   shows "degree p \<le> degree (p * q)"
  1404   using assms by (cases "p = 0") (simp_all add: degree_mult_eq)
  1405 
  1406 lemma coeff_degree_mult: "coeff (p * q) (degree (p * q)) = coeff q (degree q) * coeff p (degree p)"
  1407   for p q :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly"
  1408   by (cases "p = 0 \<or> q = 0") (auto simp: degree_mult_eq coeff_mult_degree_sum mult_ac)
  1409 
  1410 lemma dvd_imp_degree_le: "p dvd q \<Longrightarrow> q \<noteq> 0 \<Longrightarrow> degree p \<le> degree q"
  1411   for p q :: "'a::{comm_semiring_1,semiring_no_zero_divisors} poly"
  1412   by (erule dvdE, hypsubst, subst degree_mult_eq) auto
  1413 
  1414 lemma divides_degree:
  1415   fixes p q :: "'a ::{comm_semiring_1,semiring_no_zero_divisors} poly"
  1416   assumes "p dvd q"
  1417   shows "degree p \<le> degree q \<or> q = 0"
  1418   by (metis dvd_imp_degree_le assms)
  1419 
  1420 lemma const_poly_dvd_iff:
  1421   fixes c :: "'a::{comm_semiring_1,semiring_no_zero_divisors}"
  1422   shows "[:c:] dvd p \<longleftrightarrow> (\<forall>n. c dvd coeff p n)"
  1423 proof (cases "c = 0 \<or> p = 0")
  1424   case True
  1425   then show ?thesis
  1426     by (auto intro!: poly_eqI)
  1427 next
  1428   case False
  1429   show ?thesis
  1430   proof
  1431     assume "[:c:] dvd p"
  1432     then show "\<forall>n. c dvd coeff p n"
  1433       by (auto elim!: dvdE simp: coeffs_def)
  1434   next
  1435     assume *: "\<forall>n. c dvd coeff p n"
  1436     define mydiv where "mydiv x y = (SOME z. x = y * z)" for x y :: 'a
  1437     have mydiv: "x = y * mydiv x y" if "y dvd x" for x y
  1438       using that unfolding mydiv_def dvd_def by (rule someI_ex)
  1439     define q where "q = Poly (map (\<lambda>a. mydiv a c) (coeffs p))"
  1440     from False * have "p = q * [:c:]"
  1441       by (intro poly_eqI)
  1442         (auto simp: q_def nth_default_def not_less length_coeffs_degree coeffs_nth
  1443           intro!: coeff_eq_0 mydiv)
  1444     then show "[:c:] dvd p"
  1445       by (simp only: dvd_triv_right)
  1446   qed
  1447 qed
  1448 
  1449 lemma const_poly_dvd_const_poly_iff [simp]: "[:a:] dvd [:b:] \<longleftrightarrow> a dvd b"
  1450   for a b :: "'a::{comm_semiring_1,semiring_no_zero_divisors}"
  1451   by (subst const_poly_dvd_iff) (auto simp: coeff_pCons split: nat.splits)
  1452 
  1453 lemma lead_coeff_mult: "lead_coeff (p * q) = lead_coeff p * lead_coeff q"
  1454   for p q :: "'a::{comm_semiring_0, semiring_no_zero_divisors} poly"
  1455   by (cases "p = 0 \<or> q = 0") (auto simp: coeff_mult_degree_sum degree_mult_eq)
  1456 
  1457 lemma lead_coeff_smult: "lead_coeff (smult c p) = c * lead_coeff p"
  1458   for p :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly"
  1459 proof -
  1460   have "smult c p = [:c:] * p" by simp
  1461   also have "lead_coeff \<dots> = c * lead_coeff p"
  1462     by (subst lead_coeff_mult) simp_all
  1463   finally show ?thesis .
  1464 qed
  1465 
  1466 lemma lead_coeff_1 [simp]: "lead_coeff 1 = 1"
  1467   by simp
  1468 
  1469 lemma lead_coeff_power: "lead_coeff (p ^ n) = lead_coeff p ^ n"
  1470   for p :: "'a::{comm_semiring_1,semiring_no_zero_divisors} poly"
  1471   by (induct n) (simp_all add: lead_coeff_mult)
  1472 
  1473 
  1474 subsection \<open>Polynomials form an ordered integral domain\<close>
  1475 
  1476 definition pos_poly :: "'a::linordered_semidom poly \<Rightarrow> bool"
  1477   where "pos_poly p \<longleftrightarrow> 0 < coeff p (degree p)"
  1478 
  1479 lemma pos_poly_pCons: "pos_poly (pCons a p) \<longleftrightarrow> pos_poly p \<or> (p = 0 \<and> 0 < a)"
  1480   by (simp add: pos_poly_def)
  1481 
  1482 lemma not_pos_poly_0 [simp]: "\<not> pos_poly 0"
  1483   by (simp add: pos_poly_def)
  1484 
  1485 lemma pos_poly_add: "pos_poly p \<Longrightarrow> pos_poly q \<Longrightarrow> pos_poly (p + q)"
  1486   apply (induct p arbitrary: q)
  1487    apply simp
  1488   apply (case_tac q)
  1489   apply (force simp add: pos_poly_pCons add_pos_pos)
  1490   done
  1491 
  1492 lemma pos_poly_mult: "pos_poly p \<Longrightarrow> pos_poly q \<Longrightarrow> pos_poly (p * q)"
  1493   unfolding pos_poly_def
  1494   apply (subgoal_tac "p \<noteq> 0 \<and> q \<noteq> 0")
  1495    apply (simp add: degree_mult_eq coeff_mult_degree_sum)
  1496   apply auto
  1497   done
  1498 
  1499 lemma pos_poly_total: "p = 0 \<or> pos_poly p \<or> pos_poly (- p)"
  1500   for p :: "'a::linordered_idom poly"
  1501   by (induct p) (auto simp: pos_poly_pCons)
  1502 
  1503 lemma pos_poly_coeffs [code]: "pos_poly p \<longleftrightarrow> (let as = coeffs p in as \<noteq> [] \<and> last as > 0)"
  1504   (is "?lhs \<longleftrightarrow> ?rhs")
  1505 proof
  1506   assume ?rhs
  1507   then show ?lhs
  1508     by (auto simp add: pos_poly_def last_coeffs_eq_coeff_degree)
  1509 next
  1510   assume ?lhs
  1511   then have *: "0 < coeff p (degree p)"
  1512     by (simp add: pos_poly_def)
  1513   then have "p \<noteq> 0"
  1514     by auto
  1515   with * show ?rhs
  1516     by (simp add: last_coeffs_eq_coeff_degree)
  1517 qed
  1518 
  1519 instantiation poly :: (linordered_idom) linordered_idom
  1520 begin
  1521 
  1522 definition "x < y \<longleftrightarrow> pos_poly (y - x)"
  1523 
  1524 definition "x \<le> y \<longleftrightarrow> x = y \<or> pos_poly (y - x)"
  1525 
  1526 definition "\<bar>x::'a poly\<bar> = (if x < 0 then - x else x)"
  1527 
  1528 definition "sgn (x::'a poly) = (if x = 0 then 0 else if 0 < x then 1 else - 1)"
  1529 
  1530 instance
  1531 proof
  1532   fix x y z :: "'a poly"
  1533   show "x < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x"
  1534     unfolding less_eq_poly_def less_poly_def
  1535     apply safe
  1536      apply simp
  1537     apply (drule (1) pos_poly_add)
  1538     apply simp
  1539     done
  1540   show "x \<le> x"
  1541     by (simp add: less_eq_poly_def)
  1542   show "x \<le> y \<Longrightarrow> y \<le> z \<Longrightarrow> x \<le> z"
  1543     unfolding less_eq_poly_def
  1544     apply safe
  1545     apply (drule (1) pos_poly_add)
  1546     apply (simp add: algebra_simps)
  1547     done
  1548   show "x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x = y"
  1549     unfolding less_eq_poly_def
  1550     apply safe
  1551     apply (drule (1) pos_poly_add)
  1552     apply simp
  1553     done
  1554   show "x \<le> y \<Longrightarrow> z + x \<le> z + y"
  1555     unfolding less_eq_poly_def
  1556     apply safe
  1557     apply (simp add: algebra_simps)
  1558     done
  1559   show "x \<le> y \<or> y \<le> x"
  1560     unfolding less_eq_poly_def
  1561     using pos_poly_total [of "x - y"]
  1562     by auto
  1563   show "x < y \<Longrightarrow> 0 < z \<Longrightarrow> z * x < z * y"
  1564     by (simp add: less_poly_def right_diff_distrib [symmetric] pos_poly_mult)
  1565   show "\<bar>x\<bar> = (if x < 0 then - x else x)"
  1566     by (rule abs_poly_def)
  1567   show "sgn x = (if x = 0 then 0 else if 0 < x then 1 else - 1)"
  1568     by (rule sgn_poly_def)
  1569 qed
  1570 
  1571 end
  1572 
  1573 text \<open>TODO: Simplification rules for comparisons\<close>
  1574 
  1575 
  1576 subsection \<open>Synthetic division and polynomial roots\<close>
  1577 
  1578 subsubsection \<open>Synthetic division\<close>
  1579 
  1580 text \<open>Synthetic division is simply division by the linear polynomial @{term "x - c"}.\<close>
  1581 
  1582 definition synthetic_divmod :: "'a::comm_semiring_0 poly \<Rightarrow> 'a \<Rightarrow> 'a poly \<times> 'a"
  1583   where "synthetic_divmod p c = fold_coeffs (\<lambda>a (q, r). (pCons r q, a + c * r)) p (0, 0)"
  1584 
  1585 definition synthetic_div :: "'a::comm_semiring_0 poly \<Rightarrow> 'a \<Rightarrow> 'a poly"
  1586   where "synthetic_div p c = fst (synthetic_divmod p c)"
  1587 
  1588 lemma synthetic_divmod_0 [simp]: "synthetic_divmod 0 c = (0, 0)"
  1589   by (simp add: synthetic_divmod_def)
  1590 
  1591 lemma synthetic_divmod_pCons [simp]:
  1592   "synthetic_divmod (pCons a p) c = (\<lambda>(q, r). (pCons r q, a + c * r)) (synthetic_divmod p c)"
  1593   by (cases "p = 0 \<and> a = 0") (auto simp add: synthetic_divmod_def)
  1594 
  1595 lemma synthetic_div_0 [simp]: "synthetic_div 0 c = 0"
  1596   by (simp add: synthetic_div_def)
  1597 
  1598 lemma synthetic_div_unique_lemma: "smult c p = pCons a p \<Longrightarrow> p = 0"
  1599   by (induct p arbitrary: a) simp_all
  1600 
  1601 lemma snd_synthetic_divmod: "snd (synthetic_divmod p c) = poly p c"
  1602   by (induct p) (simp_all add: split_def)
  1603 
  1604 lemma synthetic_div_pCons [simp]:
  1605   "synthetic_div (pCons a p) c = pCons (poly p c) (synthetic_div p c)"
  1606   by (simp add: synthetic_div_def split_def snd_synthetic_divmod)
  1607 
  1608 lemma synthetic_div_eq_0_iff: "synthetic_div p c = 0 \<longleftrightarrow> degree p = 0"
  1609 proof (induct p)
  1610   case 0
  1611   then show ?case by simp
  1612 next
  1613   case (pCons a p)
  1614   then show ?case by (cases p) simp
  1615 qed
  1616 
  1617 lemma degree_synthetic_div: "degree (synthetic_div p c) = degree p - 1"
  1618   by (induct p) (simp_all add: synthetic_div_eq_0_iff)
  1619 
  1620 lemma synthetic_div_correct:
  1621   "p + smult c (synthetic_div p c) = pCons (poly p c) (synthetic_div p c)"
  1622   by (induct p) simp_all
  1623 
  1624 lemma synthetic_div_unique: "p + smult c q = pCons r q \<Longrightarrow> r = poly p c \<and> q = synthetic_div p c"
  1625   apply (induct p arbitrary: q r)
  1626    apply simp
  1627    apply (frule synthetic_div_unique_lemma)
  1628    apply simp
  1629   apply (case_tac q, force)
  1630   done
  1631 
  1632 lemma synthetic_div_correct': "[:-c, 1:] * synthetic_div p c + [:poly p c:] = p"
  1633   for c :: "'a::comm_ring_1"
  1634   using synthetic_div_correct [of p c] by (simp add: algebra_simps)
  1635 
  1636 
  1637 subsubsection \<open>Polynomial roots\<close>
  1638 
  1639 lemma poly_eq_0_iff_dvd: "poly p c = 0 \<longleftrightarrow> [:- c, 1:] dvd p"
  1640   (is "?lhs \<longleftrightarrow> ?rhs")
  1641   for c :: "'a::comm_ring_1"
  1642 proof
  1643   assume ?lhs
  1644   with synthetic_div_correct' [of c p] have "p = [:-c, 1:] * synthetic_div p c" by simp
  1645   then show ?rhs ..
  1646 next
  1647   assume ?rhs
  1648   then obtain k where "p = [:-c, 1:] * k" by (rule dvdE)
  1649   then show ?lhs by simp
  1650 qed
  1651 
  1652 lemma dvd_iff_poly_eq_0: "[:c, 1:] dvd p \<longleftrightarrow> poly p (- c) = 0"
  1653   for c :: "'a::comm_ring_1"
  1654   by (simp add: poly_eq_0_iff_dvd)
  1655 
  1656 lemma poly_roots_finite: "p \<noteq> 0 \<Longrightarrow> finite {x. poly p x = 0}"
  1657   for p :: "'a::{comm_ring_1,ring_no_zero_divisors} poly"
  1658 proof (induct n \<equiv> "degree p" arbitrary: p)
  1659   case 0
  1660   then obtain a where "a \<noteq> 0" and "p = [:a:]"
  1661     by (cases p) (simp split: if_splits)
  1662   then show "finite {x. poly p x = 0}"
  1663     by simp
  1664 next
  1665   case (Suc n)
  1666   show "finite {x. poly p x = 0}"
  1667   proof (cases "\<exists>x. poly p x = 0")
  1668     case False
  1669     then show "finite {x. poly p x = 0}" by simp
  1670   next
  1671     case True
  1672     then obtain a where "poly p a = 0" ..
  1673     then have "[:-a, 1:] dvd p"
  1674       by (simp only: poly_eq_0_iff_dvd)
  1675     then obtain k where k: "p = [:-a, 1:] * k" ..
  1676     with \<open>p \<noteq> 0\<close> have "k \<noteq> 0"
  1677       by auto
  1678     with k have "degree p = Suc (degree k)"
  1679       by (simp add: degree_mult_eq del: mult_pCons_left)
  1680     with \<open>Suc n = degree p\<close> have "n = degree k"
  1681       by simp
  1682     from this \<open>k \<noteq> 0\<close> have "finite {x. poly k x = 0}"
  1683       by (rule Suc.hyps)
  1684     then have "finite (insert a {x. poly k x = 0})"
  1685       by simp
  1686     then show "finite {x. poly p x = 0}"
  1687       by (simp add: k Collect_disj_eq del: mult_pCons_left)
  1688   qed
  1689 qed
  1690 
  1691 lemma poly_eq_poly_eq_iff: "poly p = poly q \<longleftrightarrow> p = q"
  1692   (is "?lhs \<longleftrightarrow> ?rhs")
  1693   for p q :: "'a::{comm_ring_1,ring_no_zero_divisors,ring_char_0} poly"
  1694 proof
  1695   assume ?rhs
  1696   then show ?lhs by simp
  1697 next
  1698   assume ?lhs
  1699   have "poly p = poly 0 \<longleftrightarrow> p = 0" for p :: "'a poly"
  1700     apply (cases "p = 0")
  1701      apply simp_all
  1702     apply (drule poly_roots_finite)
  1703     apply (auto simp add: infinite_UNIV_char_0)
  1704     done
  1705   from \<open>?lhs\<close> and this [of "p - q"] show ?rhs
  1706     by auto
  1707 qed
  1708 
  1709 lemma poly_all_0_iff_0: "(\<forall>x. poly p x = 0) \<longleftrightarrow> p = 0"
  1710   for p :: "'a::{ring_char_0,comm_ring_1,ring_no_zero_divisors} poly"
  1711   by (auto simp add: poly_eq_poly_eq_iff [symmetric])
  1712 
  1713 
  1714 subsubsection \<open>Order of polynomial roots\<close>
  1715 
  1716 definition order :: "'a::idom \<Rightarrow> 'a poly \<Rightarrow> nat"
  1717   where "order a p = (LEAST n. \<not> [:-a, 1:] ^ Suc n dvd p)"
  1718 
  1719 lemma coeff_linear_power: "coeff ([:a, 1:] ^ n) n = 1"
  1720   for a :: "'a::comm_semiring_1"
  1721   apply (induct n)
  1722    apply simp_all
  1723   apply (subst coeff_eq_0)
  1724    apply (auto intro: le_less_trans degree_power_le)
  1725   done
  1726 
  1727 lemma degree_linear_power: "degree ([:a, 1:] ^ n) = n"
  1728   for a :: "'a::comm_semiring_1"
  1729   apply (rule order_antisym)
  1730    apply (rule ord_le_eq_trans [OF degree_power_le])
  1731    apply simp
  1732   apply (rule le_degree)
  1733   apply (simp add: coeff_linear_power)
  1734   done
  1735 
  1736 lemma order_1: "[:-a, 1:] ^ order a p dvd p"
  1737   apply (cases "p = 0")
  1738    apply simp
  1739   apply (cases "order a p")
  1740    apply simp
  1741   apply (subgoal_tac "nat < (LEAST n. \<not> [:-a, 1:] ^ Suc n dvd p)")
  1742    apply (drule not_less_Least)
  1743    apply simp
  1744   apply (fold order_def)
  1745   apply simp
  1746   done
  1747 
  1748 lemma order_2: "p \<noteq> 0 \<Longrightarrow> \<not> [:-a, 1:] ^ Suc (order a p) dvd p"
  1749   unfolding order_def
  1750   apply (rule LeastI_ex)
  1751   apply (rule_tac x="degree p" in exI)
  1752   apply (rule notI)
  1753   apply (drule (1) dvd_imp_degree_le)
  1754   apply (simp only: degree_linear_power)
  1755   done
  1756 
  1757 lemma order: "p \<noteq> 0 \<Longrightarrow> [:-a, 1:] ^ order a p dvd p \<and> \<not> [:-a, 1:] ^ Suc (order a p) dvd p"
  1758   by (rule conjI [OF order_1 order_2])
  1759 
  1760 lemma order_degree:
  1761   assumes p: "p \<noteq> 0"
  1762   shows "order a p \<le> degree p"
  1763 proof -
  1764   have "order a p = degree ([:-a, 1:] ^ order a p)"
  1765     by (simp only: degree_linear_power)
  1766   also from order_1 p have "\<dots> \<le> degree p"
  1767     by (rule dvd_imp_degree_le)
  1768   finally show ?thesis .
  1769 qed
  1770 
  1771 lemma order_root: "poly p a = 0 \<longleftrightarrow> p = 0 \<or> order a p \<noteq> 0"
  1772   apply (cases "p = 0")
  1773    apply simp_all
  1774   apply (rule iffI)
  1775    apply (metis order_2 not_gr0 poly_eq_0_iff_dvd power_0 power_Suc_0 power_one_right)
  1776   unfolding poly_eq_0_iff_dvd
  1777   apply (metis dvd_power dvd_trans order_1)
  1778   done
  1779 
  1780 lemma order_0I: "poly p a \<noteq> 0 \<Longrightarrow> order a p = 0"
  1781   by (subst (asm) order_root) auto
  1782 
  1783 lemma order_unique_lemma:
  1784   fixes p :: "'a::idom poly"
  1785   assumes "[:-a, 1:] ^ n dvd p" "\<not> [:-a, 1:] ^ Suc n dvd p"
  1786   shows "n = order a p"
  1787   unfolding Polynomial.order_def
  1788   apply (rule Least_equality [symmetric])
  1789    apply (fact assms)
  1790   apply (rule classical)
  1791   apply (erule notE)
  1792   unfolding not_less_eq_eq
  1793   using assms(1)
  1794   apply (rule power_le_dvd)
  1795   apply assumption
  1796   done
  1797 
  1798 lemma order_mult: "p * q \<noteq> 0 \<Longrightarrow> order a (p * q) = order a p + order a q"
  1799 proof -
  1800   define i where "i = order a p"
  1801   define j where "j = order a q"
  1802   define t where "t = [:-a, 1:]"
  1803   have t_dvd_iff: "\<And>u. t dvd u \<longleftrightarrow> poly u a = 0"
  1804     by (simp add: t_def dvd_iff_poly_eq_0)
  1805   assume "p * q \<noteq> 0"
  1806   then show "order a (p * q) = i + j"
  1807     apply clarsimp
  1808     apply (drule order [where a=a and p=p, folded i_def t_def])
  1809     apply (drule order [where a=a and p=q, folded j_def t_def])
  1810     apply clarify
  1811     apply (erule dvdE)+
  1812     apply (rule order_unique_lemma [symmetric], fold t_def)
  1813      apply (simp_all add: power_add t_dvd_iff)
  1814     done
  1815 qed
  1816 
  1817 lemma order_smult:
  1818   assumes "c \<noteq> 0"
  1819   shows "order x (smult c p) = order x p"
  1820 proof (cases "p = 0")
  1821   case True
  1822   then show ?thesis
  1823     by simp
  1824 next
  1825   case False
  1826   have "smult c p = [:c:] * p" by simp
  1827   also from assms False have "order x \<dots> = order x [:c:] + order x p"
  1828     by (subst order_mult) simp_all
  1829   also have "order x [:c:] = 0"
  1830     by (rule order_0I) (use assms in auto)
  1831   finally show ?thesis
  1832     by simp
  1833 qed
  1834 
  1835 (* Next two lemmas contributed by Wenda Li *)
  1836 lemma order_1_eq_0 [simp]:"order x 1 = 0"
  1837   by (metis order_root poly_1 zero_neq_one)
  1838 
  1839 lemma order_power_n_n: "order a ([:-a,1:]^n)=n"
  1840 proof (induct n) (*might be proved more concisely using nat_less_induct*)
  1841   case 0
  1842   then show ?case
  1843     by (metis order_root poly_1 power_0 zero_neq_one)
  1844 next
  1845   case (Suc n)
  1846   have "order a ([:- a, 1:] ^ Suc n) = order a ([:- a, 1:] ^ n) + order a [:-a,1:]"
  1847     by (metis (no_types, hide_lams) One_nat_def add_Suc_right monoid_add_class.add.right_neutral
  1848       one_neq_zero order_mult pCons_eq_0_iff power_add power_eq_0_iff power_one_right)
  1849   moreover have "order a [:-a,1:] = 1"
  1850     unfolding order_def
  1851   proof (rule Least_equality, rule notI)
  1852     assume "[:- a, 1:] ^ Suc 1 dvd [:- a, 1:]"
  1853     then have "degree ([:- a, 1:] ^ Suc 1) \<le> degree ([:- a, 1:])"
  1854       by (rule dvd_imp_degree_le) auto
  1855     then show False
  1856       by auto
  1857   next
  1858     fix y
  1859     assume *: "\<not> [:- a, 1:] ^ Suc y dvd [:- a, 1:]"
  1860     show "1 \<le> y"
  1861     proof (rule ccontr)
  1862       assume "\<not> 1 \<le> y"
  1863       then have "y = 0" by auto
  1864       then have "[:- a, 1:] ^ Suc y dvd [:- a, 1:]" by auto
  1865       with * show False by auto
  1866     qed
  1867   qed
  1868   ultimately show ?case
  1869     using Suc by auto
  1870 qed
  1871 
  1872 lemma order_0_monom [simp]: "c \<noteq> 0 \<Longrightarrow> order 0 (monom c n) = n"
  1873   using order_power_n_n[of 0 n] by (simp add: monom_altdef order_smult)
  1874 
  1875 lemma dvd_imp_order_le: "q \<noteq> 0 \<Longrightarrow> p dvd q \<Longrightarrow> Polynomial.order a p \<le> Polynomial.order a q"
  1876   by (auto simp: order_mult elim: dvdE)
  1877 
  1878 text \<open>Now justify the standard squarefree decomposition, i.e. \<open>f / gcd f f'\<close>.\<close>
  1879 
  1880 lemma order_divides: "[:-a, 1:] ^ n dvd p \<longleftrightarrow> p = 0 \<or> n \<le> order a p"
  1881   apply (cases "p = 0")
  1882   apply auto
  1883    apply (drule order_2 [where a=a and p=p])
  1884    apply (metis not_less_eq_eq power_le_dvd)
  1885   apply (erule power_le_dvd [OF order_1])
  1886   done
  1887 
  1888 lemma order_decomp:
  1889   assumes "p \<noteq> 0"
  1890   shows "\<exists>q. p = [:- a, 1:] ^ order a p * q \<and> \<not> [:- a, 1:] dvd q"
  1891 proof -
  1892   from assms have *: "[:- a, 1:] ^ order a p dvd p"
  1893     and **: "\<not> [:- a, 1:] ^ Suc (order a p) dvd p"
  1894     by (auto dest: order)
  1895   from * obtain q where q: "p = [:- a, 1:] ^ order a p * q" ..
  1896   with ** have "\<not> [:- a, 1:] ^ Suc (order a p) dvd [:- a, 1:] ^ order a p * q"
  1897     by simp
  1898   then have "\<not> [:- a, 1:] ^ order a p * [:- a, 1:] dvd [:- a, 1:] ^ order a p * q"
  1899     by simp
  1900   with idom_class.dvd_mult_cancel_left [of "[:- a, 1:] ^ order a p" "[:- a, 1:]" q]
  1901   have "\<not> [:- a, 1:] dvd q" by auto
  1902   with q show ?thesis by blast
  1903 qed
  1904 
  1905 lemma monom_1_dvd_iff: "p \<noteq> 0 \<Longrightarrow> monom 1 n dvd p \<longleftrightarrow> n \<le> order 0 p"
  1906   using order_divides[of 0 n p] by (simp add: monom_altdef)
  1907 
  1908 
  1909 subsection \<open>Additional induction rules on polynomials\<close>
  1910 
  1911 text \<open>
  1912   An induction rule for induction over the roots of a polynomial with a certain property.
  1913   (e.g. all positive roots)
  1914 \<close>
  1915 lemma poly_root_induct [case_names 0 no_roots root]:
  1916   fixes p :: "'a :: idom poly"
  1917   assumes "Q 0"
  1918     and "\<And>p. (\<And>a. P a \<Longrightarrow> poly p a \<noteq> 0) \<Longrightarrow> Q p"
  1919     and "\<And>a p. P a \<Longrightarrow> Q p \<Longrightarrow> Q ([:a, -1:] * p)"
  1920   shows "Q p"
  1921 proof (induction "degree p" arbitrary: p rule: less_induct)
  1922   case (less p)
  1923   show ?case
  1924   proof (cases "p = 0")
  1925     case True
  1926     with assms(1) show ?thesis by simp
  1927   next
  1928     case False
  1929     show ?thesis
  1930     proof (cases "\<exists>a. P a \<and> poly p a = 0")
  1931       case False
  1932       then show ?thesis by (intro assms(2)) blast
  1933     next
  1934       case True
  1935       then obtain a where a: "P a" "poly p a = 0"
  1936         by blast
  1937       then have "-[:-a, 1:] dvd p"
  1938         by (subst minus_dvd_iff) (simp add: poly_eq_0_iff_dvd)
  1939       then obtain q where q: "p = [:a, -1:] * q" by (elim dvdE) simp
  1940       with False have "q \<noteq> 0" by auto
  1941       have "degree p = Suc (degree q)"
  1942         by (subst q, subst degree_mult_eq) (simp_all add: \<open>q \<noteq> 0\<close>)
  1943       then have "Q q" by (intro less) simp
  1944       with a(1) have "Q ([:a, -1:] * q)"
  1945         by (rule assms(3))
  1946       with q show ?thesis by simp
  1947     qed
  1948   qed
  1949 qed
  1950 
  1951 lemma dropWhile_replicate_append:
  1952   "dropWhile (op = a) (replicate n a @ ys) = dropWhile (op = a) ys"
  1953   by (induct n) simp_all
  1954 
  1955 lemma Poly_append_replicate_0: "Poly (xs @ replicate n 0) = Poly xs"
  1956   by (subst coeffs_eq_iff) (simp_all add: strip_while_def dropWhile_replicate_append)
  1957 
  1958 text \<open>
  1959   An induction rule for simultaneous induction over two polynomials,
  1960   prepending one coefficient in each step.
  1961 \<close>
  1962 lemma poly_induct2 [case_names 0 pCons]:
  1963   assumes "P 0 0" "\<And>a p b q. P p q \<Longrightarrow> P (pCons a p) (pCons b q)"
  1964   shows "P p q"
  1965 proof -
  1966   define n where "n = max (length (coeffs p)) (length (coeffs q))"
  1967   define xs where "xs = coeffs p @ (replicate (n - length (coeffs p)) 0)"
  1968   define ys where "ys = coeffs q @ (replicate (n - length (coeffs q)) 0)"
  1969   have "length xs = length ys"
  1970     by (simp add: xs_def ys_def n_def)
  1971   then have "P (Poly xs) (Poly ys)"
  1972     by (induct rule: list_induct2) (simp_all add: assms)
  1973   also have "Poly xs = p"
  1974     by (simp add: xs_def Poly_append_replicate_0)
  1975   also have "Poly ys = q"
  1976     by (simp add: ys_def Poly_append_replicate_0)
  1977   finally show ?thesis .
  1978 qed
  1979 
  1980 
  1981 subsection \<open>Composition of polynomials\<close>
  1982 
  1983 (* Several lemmas contributed by René Thiemann and Akihisa Yamada *)
  1984 
  1985 definition pcompose :: "'a::comm_semiring_0 poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
  1986   where "pcompose p q = fold_coeffs (\<lambda>a c. [:a:] + q * c) p 0"
  1987 
  1988 notation pcompose (infixl "\<circ>\<^sub>p" 71)
  1989 
  1990 lemma pcompose_0 [simp]: "pcompose 0 q = 0"
  1991   by (simp add: pcompose_def)
  1992 
  1993 lemma pcompose_pCons: "pcompose (pCons a p) q = [:a:] + q * pcompose p q"
  1994   by (cases "p = 0 \<and> a = 0") (auto simp add: pcompose_def)
  1995 
  1996 lemma pcompose_1: "pcompose 1 p = 1"
  1997   for p :: "'a::comm_semiring_1 poly"
  1998   by (auto simp: one_pCons pcompose_pCons)
  1999 
  2000 lemma poly_pcompose: "poly (pcompose p q) x = poly p (poly q x)"
  2001   by (induct p) (simp_all add: pcompose_pCons)
  2002 
  2003 lemma degree_pcompose_le: "degree (pcompose p q) \<le> degree p * degree q"
  2004   apply (induct p)
  2005    apply simp
  2006   apply (simp add: pcompose_pCons)
  2007   apply clarify
  2008   apply (rule degree_add_le)
  2009    apply simp
  2010   apply (rule order_trans [OF degree_mult_le])
  2011   apply simp
  2012   done
  2013 
  2014 lemma pcompose_add: "pcompose (p + q) r = pcompose p r + pcompose q r"
  2015   for p q r :: "'a::{comm_semiring_0, ab_semigroup_add} poly"
  2016 proof (induction p q rule: poly_induct2)
  2017   case 0
  2018   then show ?case by simp
  2019 next
  2020   case (pCons a p b q)
  2021   have "pcompose (pCons a p + pCons b q) r = [:a + b:] + r * pcompose p r + r * pcompose q r"
  2022     by (simp_all add: pcompose_pCons pCons.IH algebra_simps)
  2023   also have "[:a + b:] = [:a:] + [:b:]" by simp
  2024   also have "\<dots> + r * pcompose p r + r * pcompose q r =
  2025     pcompose (pCons a p) r + pcompose (pCons b q) r"
  2026     by (simp only: pcompose_pCons add_ac)
  2027   finally show ?case .
  2028 qed
  2029 
  2030 lemma pcompose_uminus: "pcompose (-p) r = -pcompose p r"
  2031   for p r :: "'a::comm_ring poly"
  2032   by (induct p) (simp_all add: pcompose_pCons)
  2033 
  2034 lemma pcompose_diff: "pcompose (p - q) r = pcompose p r - pcompose q r"
  2035   for p q r :: "'a::comm_ring poly"
  2036   using pcompose_add[of p "-q"] by (simp add: pcompose_uminus)
  2037 
  2038 lemma pcompose_smult: "pcompose (smult a p) r = smult a (pcompose p r)"
  2039   for p r :: "'a::comm_semiring_0 poly"
  2040   by (induct p) (simp_all add: pcompose_pCons pcompose_add smult_add_right)
  2041 
  2042 lemma pcompose_mult: "pcompose (p * q) r = pcompose p r * pcompose q r"
  2043   for p q r :: "'a::comm_semiring_0 poly"
  2044   by (induct p arbitrary: q) (simp_all add: pcompose_add pcompose_smult pcompose_pCons algebra_simps)
  2045 
  2046 lemma pcompose_assoc: "pcompose p (pcompose q r) = pcompose (pcompose p q) r"
  2047   for p q r :: "'a::comm_semiring_0 poly"
  2048   by (induct p arbitrary: q) (simp_all add: pcompose_pCons pcompose_add pcompose_mult)
  2049 
  2050 lemma pcompose_idR[simp]: "pcompose p [: 0, 1 :] = p"
  2051   for p :: "'a::comm_semiring_1 poly"
  2052   by (induct p) (simp_all add: pcompose_pCons)
  2053 
  2054 lemma pcompose_sum: "pcompose (sum f A) p = sum (\<lambda>i. pcompose (f i) p) A"
  2055   by (induct A rule: infinite_finite_induct) (simp_all add: pcompose_1 pcompose_add)
  2056 
  2057 lemma pcompose_prod: "pcompose (prod f A) p = prod (\<lambda>i. pcompose (f i) p) A"
  2058   by (induct A rule: infinite_finite_induct) (simp_all add: pcompose_1 pcompose_mult)
  2059 
  2060 lemma pcompose_const [simp]: "pcompose [:a:] q = [:a:]"
  2061   by (subst pcompose_pCons) simp
  2062 
  2063 lemma pcompose_0': "pcompose p 0 = [:coeff p 0:]"
  2064   by (induct p) (auto simp add: pcompose_pCons)
  2065 
  2066 lemma degree_pcompose: "degree (pcompose p q) = degree p * degree q"
  2067   for p q :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly"
  2068 proof (induct p)
  2069   case 0
  2070   then show ?case by auto
  2071 next
  2072   case (pCons a p)
  2073   consider "degree (q * pcompose p q) = 0" | "degree (q * pcompose p q) > 0"
  2074     by blast
  2075   then show ?case
  2076   proof cases
  2077     case prems: 1
  2078     show ?thesis
  2079     proof (cases "p = 0")
  2080       case True
  2081       then show ?thesis by auto
  2082     next
  2083       case False
  2084       from prems have "degree q = 0 \<or> pcompose p q = 0"
  2085         by (auto simp add: degree_mult_eq_0)
  2086       moreover have False if "pcompose p q = 0" "degree q \<noteq> 0"
  2087       proof -
  2088         from pCons.hyps(2) that have "degree p = 0"
  2089           by auto
  2090         then obtain a1 where "p = [:a1:]"
  2091           by (metis degree_pCons_eq_if old.nat.distinct(2) pCons_cases)
  2092         with \<open>pcompose p q = 0\<close> \<open>p \<noteq> 0\<close> show False
  2093           by auto
  2094       qed
  2095       ultimately have "degree (pCons a p) * degree q = 0"
  2096         by auto
  2097       moreover have "degree (pcompose (pCons a p) q) = 0"
  2098       proof -
  2099         from prems have "0 = max (degree [:a:]) (degree (q * pcompose p q))"
  2100           by simp
  2101         also have "\<dots> \<ge> degree ([:a:] + q * pcompose p q)"
  2102           by (rule degree_add_le_max)
  2103         finally show ?thesis
  2104           by (auto simp add: pcompose_pCons)
  2105       qed
  2106       ultimately show ?thesis by simp
  2107     qed
  2108   next
  2109     case prems: 2
  2110     then have "p \<noteq> 0" "q \<noteq> 0" "pcompose p q \<noteq> 0"
  2111       by auto
  2112     from prems degree_add_eq_right [of "[:a:]"]
  2113     have "degree (pcompose (pCons a p) q) = degree (q * pcompose p q)"
  2114       by (auto simp: pcompose_pCons)
  2115     with pCons.hyps(2) degree_mult_eq[OF \<open>q\<noteq>0\<close> \<open>pcompose p q\<noteq>0\<close>] show ?thesis
  2116       by auto
  2117   qed
  2118 qed
  2119 
  2120 lemma pcompose_eq_0:
  2121   fixes p q :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly"
  2122   assumes "pcompose p q = 0" "degree q > 0"
  2123   shows "p = 0"
  2124 proof -
  2125   from assms degree_pcompose [of p q] have "degree p = 0"
  2126     by auto
  2127   then obtain a where "p = [:a:]"
  2128     by (metis degree_pCons_eq_if gr0_conv_Suc neq0_conv pCons_cases)
  2129   with assms(1) have "a = 0"
  2130     by auto
  2131   with \<open>p = [:a:]\<close> show ?thesis
  2132     by simp
  2133 qed
  2134 
  2135 lemma lead_coeff_comp:
  2136   fixes p q :: "'a::{comm_semiring_1,semiring_no_zero_divisors} poly"
  2137   assumes "degree q > 0"
  2138   shows "lead_coeff (pcompose p q) = lead_coeff p * lead_coeff q ^ (degree p)"
  2139 proof (induct p)
  2140   case 0
  2141   then show ?case by auto
  2142 next
  2143   case (pCons a p)
  2144   consider "degree (q * pcompose p q) = 0" | "degree (q * pcompose p q) > 0"
  2145     by blast
  2146   then show ?case
  2147   proof cases
  2148     case prems: 1
  2149     then have "pcompose p q = 0"
  2150       by (metis assms degree_0 degree_mult_eq_0 neq0_conv)
  2151     with pcompose_eq_0[OF _ \<open>degree q > 0\<close>] have "p = 0"
  2152       by simp
  2153     then show ?thesis
  2154       by auto
  2155   next
  2156     case prems: 2
  2157     then have "degree [:a:] < degree (q * pcompose p q)"
  2158       by simp
  2159     then have "lead_coeff ([:a:] + q * p \<circ>\<^sub>p q) = lead_coeff (q * p \<circ>\<^sub>p q)"
  2160       by (rule lead_coeff_add_le)
  2161     then have "lead_coeff (pcompose (pCons a p) q) = lead_coeff (q * pcompose p q)"
  2162       by (simp add: pcompose_pCons)
  2163     also have "\<dots> = lead_coeff q * (lead_coeff p * lead_coeff q ^ degree p)"
  2164       using pCons.hyps(2) lead_coeff_mult[of q "pcompose p q"] by simp
  2165     also have "\<dots> = lead_coeff p * lead_coeff q ^ (degree p + 1)"
  2166       by (auto simp: mult_ac)
  2167     finally show ?thesis by auto
  2168   qed
  2169 qed
  2170 
  2171 
  2172 subsection \<open>Shifting polynomials\<close>
  2173 
  2174 definition poly_shift :: "nat \<Rightarrow> 'a::zero poly \<Rightarrow> 'a poly"
  2175   where "poly_shift n p = Abs_poly (\<lambda>i. coeff p (i + n))"
  2176 
  2177 lemma nth_default_drop: "nth_default x (drop n xs) m = nth_default x xs (m + n)"
  2178   by (auto simp add: nth_default_def add_ac)
  2179 
  2180 lemma nth_default_take: "nth_default x (take n xs) m = (if m < n then nth_default x xs m else x)"
  2181   by (auto simp add: nth_default_def add_ac)
  2182 
  2183 lemma coeff_poly_shift: "coeff (poly_shift n p) i = coeff p (i + n)"
  2184 proof -
  2185   from MOST_coeff_eq_0[of p] obtain m where "\<forall>k>m. coeff p k = 0"
  2186     by (auto simp: MOST_nat)
  2187   then have "\<forall>k>m. coeff p (k + n) = 0"
  2188     by auto
  2189   then have "\<forall>\<^sub>\<infinity>k. coeff p (k + n) = 0"
  2190     by (auto simp: MOST_nat)
  2191   then show ?thesis
  2192     by (simp add: poly_shift_def poly.Abs_poly_inverse)
  2193 qed
  2194 
  2195 lemma poly_shift_id [simp]: "poly_shift 0 = (\<lambda>x. x)"
  2196   by (simp add: poly_eq_iff fun_eq_iff coeff_poly_shift)
  2197 
  2198 lemma poly_shift_0 [simp]: "poly_shift n 0 = 0"
  2199   by (simp add: poly_eq_iff coeff_poly_shift)
  2200 
  2201 lemma poly_shift_1: "poly_shift n 1 = (if n = 0 then 1 else 0)"
  2202   by (simp add: poly_eq_iff coeff_poly_shift)
  2203 
  2204 lemma poly_shift_monom: "poly_shift n (monom c m) = (if m \<ge> n then monom c (m - n) else 0)"
  2205   by (auto simp add: poly_eq_iff coeff_poly_shift)
  2206 
  2207 lemma coeffs_shift_poly [code abstract]:
  2208   "coeffs (poly_shift n p) = drop n (coeffs p)"
  2209 proof (cases "p = 0")
  2210   case True
  2211   then show ?thesis by simp
  2212 next
  2213   case False
  2214   then show ?thesis
  2215     by (intro coeffs_eqI)
  2216       (simp_all add: coeff_poly_shift nth_default_drop nth_default_coeffs_eq)
  2217 qed
  2218 
  2219 
  2220 subsection \<open>Truncating polynomials\<close>
  2221 
  2222 definition poly_cutoff
  2223   where "poly_cutoff n p = Abs_poly (\<lambda>k. if k < n then coeff p k else 0)"
  2224 
  2225 lemma coeff_poly_cutoff: "coeff (poly_cutoff n p) k = (if k < n then coeff p k else 0)"
  2226   unfolding poly_cutoff_def
  2227   by (subst poly.Abs_poly_inverse) (auto simp: MOST_nat intro: exI[of _ n])
  2228 
  2229 lemma poly_cutoff_0 [simp]: "poly_cutoff n 0 = 0"
  2230   by (simp add: poly_eq_iff coeff_poly_cutoff)
  2231 
  2232 lemma poly_cutoff_1 [simp]: "poly_cutoff n 1 = (if n = 0 then 0 else 1)"
  2233   by (simp add: poly_eq_iff coeff_poly_cutoff)
  2234 
  2235 lemma coeffs_poly_cutoff [code abstract]:
  2236   "coeffs (poly_cutoff n p) = strip_while (op = 0) (take n (coeffs p))"
  2237 proof (cases "strip_while (op = 0) (take n (coeffs p)) = []")
  2238   case True
  2239   then have "coeff (poly_cutoff n p) k = 0" for k
  2240     unfolding coeff_poly_cutoff
  2241     by (auto simp: nth_default_coeffs_eq [symmetric] nth_default_def set_conv_nth)
  2242   then have "poly_cutoff n p = 0"
  2243     by (simp add: poly_eq_iff)
  2244   then show ?thesis
  2245     by (subst True) simp_all
  2246 next
  2247   case False
  2248   have "no_trailing (op = 0) (strip_while (op = 0) (take n (coeffs p)))"
  2249     by simp
  2250   with False have "last (strip_while (op = 0) (take n (coeffs p))) \<noteq> 0"
  2251     unfolding no_trailing_unfold by auto
  2252   then show ?thesis
  2253     by (intro coeffs_eqI)
  2254       (simp_all add: coeff_poly_cutoff nth_default_take nth_default_coeffs_eq)
  2255 qed
  2256 
  2257 
  2258 subsection \<open>Reflecting polynomials\<close>
  2259 
  2260 definition reflect_poly :: "'a::zero poly \<Rightarrow> 'a poly"
  2261   where "reflect_poly p = Poly (rev (coeffs p))"
  2262 
  2263 lemma coeffs_reflect_poly [code abstract]:
  2264   "coeffs (reflect_poly p) = rev (dropWhile (op = 0) (coeffs p))"
  2265   by (simp add: reflect_poly_def)
  2266 
  2267 lemma reflect_poly_0 [simp]: "reflect_poly 0 = 0"
  2268   by (simp add: reflect_poly_def)
  2269 
  2270 lemma reflect_poly_1 [simp]: "reflect_poly 1 = 1"
  2271   by (simp add: reflect_poly_def one_pCons)
  2272 
  2273 lemma coeff_reflect_poly:
  2274   "coeff (reflect_poly p) n = (if n > degree p then 0 else coeff p (degree p - n))"
  2275   by (cases "p = 0")
  2276     (auto simp add: reflect_poly_def nth_default_def
  2277       rev_nth degree_eq_length_coeffs coeffs_nth not_less
  2278       dest: le_imp_less_Suc)
  2279 
  2280 lemma coeff_0_reflect_poly_0_iff [simp]: "coeff (reflect_poly p) 0 = 0 \<longleftrightarrow> p = 0"
  2281   by (simp add: coeff_reflect_poly)
  2282 
  2283 lemma reflect_poly_at_0_eq_0_iff [simp]: "poly (reflect_poly p) 0 = 0 \<longleftrightarrow> p = 0"
  2284   by (simp add: coeff_reflect_poly poly_0_coeff_0)
  2285 
  2286 lemma reflect_poly_pCons':
  2287   "p \<noteq> 0 \<Longrightarrow> reflect_poly (pCons c p) = reflect_poly p + monom c (Suc (degree p))"
  2288   by (intro poly_eqI)
  2289     (auto simp: coeff_reflect_poly coeff_pCons not_less Suc_diff_le split: nat.split)
  2290 
  2291 lemma reflect_poly_const [simp]: "reflect_poly [:a:] = [:a:]"
  2292   by (cases "a = 0") (simp_all add: reflect_poly_def)
  2293 
  2294 lemma poly_reflect_poly_nz:
  2295   "x \<noteq> 0 \<Longrightarrow> poly (reflect_poly p) x = x ^ degree p * poly p (inverse x)"
  2296   for x :: "'a::field"
  2297   by (induct rule: pCons_induct) (simp_all add: field_simps reflect_poly_pCons' poly_monom)
  2298 
  2299 lemma coeff_0_reflect_poly [simp]: "coeff (reflect_poly p) 0 = lead_coeff p"
  2300   by (simp add: coeff_reflect_poly)
  2301 
  2302 lemma poly_reflect_poly_0 [simp]: "poly (reflect_poly p) 0 = lead_coeff p"
  2303   by (simp add: poly_0_coeff_0)
  2304 
  2305 lemma reflect_poly_reflect_poly [simp]: "coeff p 0 \<noteq> 0 \<Longrightarrow> reflect_poly (reflect_poly p) = p"
  2306   by (cases p rule: pCons_cases) (simp add: reflect_poly_def )
  2307 
  2308 lemma degree_reflect_poly_le: "degree (reflect_poly p) \<le> degree p"
  2309   by (simp add: degree_eq_length_coeffs coeffs_reflect_poly length_dropWhile_le diff_le_mono)
  2310 
  2311 lemma reflect_poly_pCons: "a \<noteq> 0 \<Longrightarrow> reflect_poly (pCons a p) = Poly (rev (a # coeffs p))"
  2312   by (subst coeffs_eq_iff) (simp add: coeffs_reflect_poly)
  2313 
  2314 lemma degree_reflect_poly_eq [simp]: "coeff p 0 \<noteq> 0 \<Longrightarrow> degree (reflect_poly p) = degree p"
  2315   by (cases p rule: pCons_cases) (simp add: reflect_poly_pCons degree_eq_length_coeffs)
  2316 
  2317 (* TODO: does this work with zero divisors as well? Probably not. *)
  2318 lemma reflect_poly_mult: "reflect_poly (p * q) = reflect_poly p * reflect_poly q"
  2319   for p q :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly"
  2320 proof (cases "p = 0 \<or> q = 0")
  2321   case False
  2322   then have [simp]: "p \<noteq> 0" "q \<noteq> 0" by auto
  2323   show ?thesis
  2324   proof (rule poly_eqI)
  2325     show "coeff (reflect_poly (p * q)) i = coeff (reflect_poly p * reflect_poly q) i" for i
  2326     proof (cases "i \<le> degree (p * q)")
  2327       case True
  2328       define A where "A = {..i} \<inter> {i - degree q..degree p}"
  2329       define B where "B = {..degree p} \<inter> {degree p - i..degree (p*q) - i}"
  2330       let ?f = "\<lambda>j. degree p - j"
  2331 
  2332       from True have "coeff (reflect_poly (p * q)) i = coeff (p * q) (degree (p * q) - i)"
  2333         by (simp add: coeff_reflect_poly)
  2334       also have "\<dots> = (\<Sum>j\<le>degree (p * q) - i. coeff p j * coeff q (degree (p * q) - i - j))"
  2335         by (simp add: coeff_mult)
  2336       also have "\<dots> = (\<Sum>j\<in>B. coeff p j * coeff q (degree (p * q) - i - j))"
  2337         by (intro sum.mono_neutral_right) (auto simp: B_def degree_mult_eq not_le coeff_eq_0)
  2338       also from True have "\<dots> = (\<Sum>j\<in>A. coeff p (degree p - j) * coeff q (degree q - (i - j)))"
  2339         by (intro sum.reindex_bij_witness[of _ ?f ?f])
  2340           (auto simp: A_def B_def degree_mult_eq add_ac)
  2341       also have "\<dots> =
  2342         (\<Sum>j\<le>i.
  2343           if j \<in> {i - degree q..degree p}
  2344           then coeff p (degree p - j) * coeff q (degree q - (i - j))
  2345           else 0)"
  2346         by (subst sum.inter_restrict [symmetric]) (simp_all add: A_def)
  2347       also have "\<dots> = coeff (reflect_poly p * reflect_poly q) i"
  2348         by (fastforce simp: coeff_mult coeff_reflect_poly intro!: sum.cong)
  2349       finally show ?thesis .
  2350     qed (auto simp: coeff_mult coeff_reflect_poly coeff_eq_0 degree_mult_eq intro!: sum.neutral)
  2351   qed
  2352 qed auto
  2353 
  2354 lemma reflect_poly_smult: "reflect_poly (smult c p) = smult c (reflect_poly p)"
  2355   for p :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly"
  2356   using reflect_poly_mult[of "[:c:]" p] by simp
  2357 
  2358 lemma reflect_poly_power: "reflect_poly (p ^ n) = reflect_poly p ^ n"
  2359   for p :: "'a::{comm_semiring_1,semiring_no_zero_divisors} poly"
  2360   by (induct n) (simp_all add: reflect_poly_mult)
  2361 
  2362 lemma reflect_poly_prod: "reflect_poly (prod f A) = prod (\<lambda>x. reflect_poly (f x)) A"
  2363   for f :: "_ \<Rightarrow> _::{comm_semiring_0,semiring_no_zero_divisors} poly"
  2364   by (induct A rule: infinite_finite_induct) (simp_all add: reflect_poly_mult)
  2365 
  2366 lemma reflect_poly_prod_list: "reflect_poly (prod_list xs) = prod_list (map reflect_poly xs)"
  2367   for xs :: "_::{comm_semiring_0,semiring_no_zero_divisors} poly list"
  2368   by (induct xs) (simp_all add: reflect_poly_mult)
  2369 
  2370 lemma reflect_poly_Poly_nz:
  2371   "no_trailing (HOL.eq 0) xs \<Longrightarrow> reflect_poly (Poly xs) = Poly (rev xs)"
  2372   by (simp add: reflect_poly_def)
  2373 
  2374 lemmas reflect_poly_simps =
  2375   reflect_poly_0 reflect_poly_1 reflect_poly_const reflect_poly_smult reflect_poly_mult
  2376   reflect_poly_power reflect_poly_prod reflect_poly_prod_list
  2377 
  2378 
  2379 subsection \<open>Derivatives\<close>
  2380 
  2381 function pderiv :: "('a :: {comm_semiring_1,semiring_no_zero_divisors}) poly \<Rightarrow> 'a poly"
  2382   where "pderiv (pCons a p) = (if p = 0 then 0 else p + pCons 0 (pderiv p))"
  2383   by (auto intro: pCons_cases)
  2384 
  2385 termination pderiv
  2386   by (relation "measure degree") simp_all
  2387 
  2388 declare pderiv.simps[simp del]
  2389 
  2390 lemma pderiv_0 [simp]: "pderiv 0 = 0"
  2391   using pderiv.simps [of 0 0] by simp
  2392 
  2393 lemma pderiv_pCons: "pderiv (pCons a p) = p + pCons 0 (pderiv p)"
  2394   by (simp add: pderiv.simps)
  2395 
  2396 lemma pderiv_1 [simp]: "pderiv 1 = 0"
  2397   by (simp add: one_pCons pderiv_pCons)
  2398 
  2399 lemma pderiv_of_nat [simp]: "pderiv (of_nat n) = 0"
  2400   and pderiv_numeral [simp]: "pderiv (numeral m) = 0"
  2401   by (simp_all add: of_nat_poly numeral_poly pderiv_pCons)
  2402 
  2403 lemma coeff_pderiv: "coeff (pderiv p) n = of_nat (Suc n) * coeff p (Suc n)"
  2404   by (induct p arbitrary: n)
  2405     (auto simp add: pderiv_pCons coeff_pCons algebra_simps split: nat.split)
  2406 
  2407 fun pderiv_coeffs_code :: "'a::{comm_semiring_1,semiring_no_zero_divisors} \<Rightarrow> 'a list \<Rightarrow> 'a list"
  2408   where
  2409     "pderiv_coeffs_code f (x # xs) = cCons (f * x) (pderiv_coeffs_code (f+1) xs)"
  2410   | "pderiv_coeffs_code f [] = []"
  2411 
  2412 definition pderiv_coeffs :: "'a::{comm_semiring_1,semiring_no_zero_divisors} list \<Rightarrow> 'a list"
  2413   where "pderiv_coeffs xs = pderiv_coeffs_code 1 (tl xs)"
  2414 
  2415 (* Efficient code for pderiv contributed by René Thiemann and Akihisa Yamada *)
  2416 lemma pderiv_coeffs_code:
  2417   "nth_default 0 (pderiv_coeffs_code f xs) n = (f + of_nat n) * nth_default 0 xs n"
  2418 proof (induct xs arbitrary: f n)
  2419   case Nil
  2420   then show ?case by simp
  2421 next
  2422   case (Cons x xs)
  2423   show ?case
  2424   proof (cases n)
  2425     case 0
  2426     then show ?thesis
  2427       by (cases "pderiv_coeffs_code (f + 1) xs = [] \<and> f * x = 0") (auto simp: cCons_def)
  2428   next
  2429     case n: (Suc m)
  2430     show ?thesis
  2431     proof (cases "pderiv_coeffs_code (f + 1) xs = [] \<and> f * x = 0")
  2432       case False
  2433       then have "nth_default 0 (pderiv_coeffs_code f (x # xs)) n =
  2434           nth_default 0 (pderiv_coeffs_code (f + 1) xs) m"
  2435         by (auto simp: cCons_def n)
  2436       also have "\<dots> = (f + of_nat n) * nth_default 0 xs m"
  2437         by (simp add: Cons n add_ac)
  2438       finally show ?thesis
  2439         by (simp add: n)
  2440     next
  2441       case True
  2442       have empty: "pderiv_coeffs_code g xs = [] \<Longrightarrow> g + of_nat m = 0 \<or> nth_default 0 xs m = 0" for g
  2443       proof (induct xs arbitrary: g m)
  2444         case Nil
  2445         then show ?case by simp
  2446       next
  2447         case (Cons x xs)
  2448         from Cons(2) have empty: "pderiv_coeffs_code (g + 1) xs = []" and g: "g = 0 \<or> x = 0"
  2449           by (auto simp: cCons_def split: if_splits)
  2450         note IH = Cons(1)[OF empty]
  2451         from IH[of m] IH[of "m - 1"] g show ?case
  2452           by (cases m) (auto simp: field_simps)
  2453       qed
  2454       from True have "nth_default 0 (pderiv_coeffs_code f (x # xs)) n = 0"
  2455         by (auto simp: cCons_def n)
  2456       moreover from True have "(f + of_nat n) * nth_default 0 (x # xs) n = 0"
  2457         by (simp add: n) (use empty[of "f+1"] in \<open>auto simp: field_simps\<close>)
  2458       ultimately show ?thesis by simp
  2459     qed
  2460   qed
  2461 qed
  2462 
  2463 lemma coeffs_pderiv_code [code abstract]: "coeffs (pderiv p) = pderiv_coeffs (coeffs p)"
  2464   unfolding pderiv_coeffs_def
  2465 proof (rule coeffs_eqI, unfold pderiv_coeffs_code coeff_pderiv, goal_cases)
  2466   case (1 n)
  2467   have id: "coeff p (Suc n) = nth_default 0 (map (\<lambda>i. coeff p (Suc i)) [0..<degree p]) n"
  2468     by (cases "n < degree p") (auto simp: nth_default_def coeff_eq_0)
  2469   show ?case
  2470     unfolding coeffs_def map_upt_Suc by (auto simp: id)
  2471 next
  2472   case 2
  2473   obtain n :: 'a and xs where defs: "tl (coeffs p) = xs" "1 = n"
  2474     by simp
  2475   from 2 show ?case
  2476     unfolding defs by (induct xs arbitrary: n) (auto simp: cCons_def)
  2477 qed
  2478 
  2479 lemma pderiv_eq_0_iff: "pderiv p = 0 \<longleftrightarrow> degree p = 0"
  2480   for p :: "'a::{comm_semiring_1,semiring_no_zero_divisors,semiring_char_0} poly"
  2481   apply (rule iffI)
  2482    apply (cases p)
  2483    apply simp
  2484    apply (simp add: poly_eq_iff coeff_pderiv del: of_nat_Suc)
  2485   apply (simp add: poly_eq_iff coeff_pderiv coeff_eq_0)
  2486   done
  2487 
  2488 lemma degree_pderiv: "degree (pderiv p) = degree p - 1"
  2489   for p :: "'a::{comm_semiring_1,semiring_no_zero_divisors,semiring_char_0} poly"
  2490   apply (rule order_antisym [OF degree_le])
  2491    apply (simp add: coeff_pderiv coeff_eq_0)
  2492   apply (cases "degree p")
  2493    apply simp
  2494   apply (rule le_degree)
  2495   apply (simp add: coeff_pderiv del: of_nat_Suc)
  2496   apply (metis degree_0 leading_coeff_0_iff nat.distinct(1))
  2497   done
  2498 
  2499 lemma not_dvd_pderiv:
  2500   fixes p :: "'a::{comm_semiring_1,semiring_no_zero_divisors,semiring_char_0} poly"
  2501   assumes "degree p \<noteq> 0"
  2502   shows "\<not> p dvd pderiv p"
  2503 proof
  2504   assume dvd: "p dvd pderiv p"
  2505   then obtain q where p: "pderiv p = p * q"
  2506     unfolding dvd_def by auto
  2507   from dvd have le: "degree p \<le> degree (pderiv p)"
  2508     by (simp add: assms dvd_imp_degree_le pderiv_eq_0_iff)
  2509   from assms and this [unfolded degree_pderiv]
  2510     show False by auto
  2511 qed
  2512 
  2513 lemma dvd_pderiv_iff [simp]: "p dvd pderiv p \<longleftrightarrow> degree p = 0"
  2514   for p :: "'a::{comm_semiring_1,semiring_no_zero_divisors,semiring_char_0} poly"
  2515   using not_dvd_pderiv[of p] by (auto simp: pderiv_eq_0_iff [symmetric])
  2516 
  2517 lemma pderiv_singleton [simp]: "pderiv [:a:] = 0"
  2518   by (simp add: pderiv_pCons)
  2519 
  2520 lemma pderiv_add: "pderiv (p + q) = pderiv p + pderiv q"
  2521   by (rule poly_eqI) (simp add: coeff_pderiv algebra_simps)
  2522 
  2523 lemma pderiv_minus: "pderiv (- p :: 'a :: idom poly) = - pderiv p"
  2524   by (rule poly_eqI) (simp add: coeff_pderiv algebra_simps)
  2525 
  2526 lemma pderiv_diff: "pderiv ((p :: _ :: idom poly) - q) = pderiv p - pderiv q"
  2527   by (rule poly_eqI) (simp add: coeff_pderiv algebra_simps)
  2528 
  2529 lemma pderiv_smult: "pderiv (smult a p) = smult a (pderiv p)"
  2530   by (rule poly_eqI) (simp add: coeff_pderiv algebra_simps)
  2531 
  2532 lemma pderiv_mult: "pderiv (p * q) = p * pderiv q + q * pderiv p"
  2533   by (induct p) (auto simp: pderiv_add pderiv_smult pderiv_pCons algebra_simps)
  2534 
  2535 lemma pderiv_power_Suc: "pderiv (p ^ Suc n) = smult (of_nat (Suc n)) (p ^ n) * pderiv p"
  2536   apply (induct n)
  2537    apply simp
  2538   apply (subst power_Suc)
  2539   apply (subst pderiv_mult)
  2540   apply (erule ssubst)
  2541   apply (simp only: of_nat_Suc smult_add_left smult_1_left)
  2542   apply (simp add: algebra_simps)
  2543   done
  2544 
  2545 lemma pderiv_pcompose: "pderiv (pcompose p q) = pcompose (pderiv p) q * pderiv q"
  2546   by (induction p rule: pCons_induct)
  2547      (auto simp: pcompose_pCons pderiv_add pderiv_mult pderiv_pCons pcompose_add algebra_simps)
  2548 
  2549 lemma pderiv_prod: "pderiv (prod f (as)) = (\<Sum>a\<in>as. prod f (as - {a}) * pderiv (f a))"
  2550 proof (induct as rule: infinite_finite_induct)
  2551   case (insert a as)
  2552   then have id: "prod f (insert a as) = f a * prod f as"
  2553     "\<And>g. sum g (insert a as) = g a + sum g as"
  2554     "insert a as - {a} = as"
  2555     by auto
  2556   have "prod f (insert a as - {b}) = f a * prod f (as - {b})" if "b \<in> as" for b
  2557   proof -
  2558     from \<open>a \<notin> as\<close> that have *: "insert a as - {b} = insert a (as - {b})"
  2559       by auto
  2560     show ?thesis
  2561       unfolding * by (subst prod.insert) (use insert in auto)
  2562   qed
  2563   then show ?case
  2564     unfolding id pderiv_mult insert(3) sum_distrib_left
  2565     by (auto simp add: ac_simps intro!: sum.cong)
  2566 qed auto
  2567 
  2568 lemma DERIV_pow2: "DERIV (\<lambda>x. x ^ Suc n) x :> real (Suc n) * (x ^ n)"
  2569   by (rule DERIV_cong, rule DERIV_pow) simp
  2570 declare DERIV_pow2 [simp] DERIV_pow [simp]
  2571 
  2572 lemma DERIV_add_const: "DERIV f x :> D \<Longrightarrow> DERIV (\<lambda>x. a + f x :: 'a::real_normed_field) x :> D"
  2573   by (rule DERIV_cong, rule DERIV_add) auto
  2574 
  2575 lemma poly_DERIV [simp]: "DERIV (\<lambda>x. poly p x) x :> poly (pderiv p) x"
  2576   by (induct p) (auto intro!: derivative_eq_intros simp add: pderiv_pCons)
  2577 
  2578 lemma continuous_on_poly [continuous_intros]:
  2579   fixes p :: "'a :: {real_normed_field} poly"
  2580   assumes "continuous_on A f"
  2581   shows "continuous_on A (\<lambda>x. poly p (f x))"
  2582 proof -
  2583   have "continuous_on A (\<lambda>x. (\<Sum>i\<le>degree p. (f x) ^ i * coeff p i))"
  2584     by (intro continuous_intros assms)
  2585   also have "\<dots> = (\<lambda>x. poly p (f x))"
  2586     by (rule ext) (simp add: poly_altdef mult_ac)
  2587   finally show ?thesis .
  2588 qed
  2589 
  2590 text \<open>Consequences of the derivative theorem above.\<close>
  2591 
  2592 lemma poly_differentiable[simp]: "(\<lambda>x. poly p x) differentiable (at x)"
  2593   for x :: real
  2594   by (simp add: real_differentiable_def) (blast intro: poly_DERIV)
  2595 
  2596 lemma poly_isCont[simp]: "isCont (\<lambda>x. poly p x) x"
  2597   for x :: real
  2598   by (rule poly_DERIV [THEN DERIV_isCont])
  2599 
  2600 lemma poly_IVT_pos: "a < b \<Longrightarrow> poly p a < 0 \<Longrightarrow> 0 < poly p b \<Longrightarrow> \<exists>x. a < x \<and> x < b \<and> poly p x = 0"
  2601   for a b :: real
  2602   using IVT_objl [of "poly p" a 0 b] by (auto simp add: order_le_less)
  2603 
  2604 lemma poly_IVT_neg: "a < b \<Longrightarrow> 0 < poly p a \<Longrightarrow> poly p b < 0 \<Longrightarrow> \<exists>x. a < x \<and> x < b \<and> poly p x = 0"
  2605   for a b :: real
  2606   using poly_IVT_pos [where p = "- p"] by simp
  2607 
  2608 lemma poly_IVT: "a < b \<Longrightarrow> poly p a * poly p b < 0 \<Longrightarrow> \<exists>x>a. x < b \<and> poly p x = 0"
  2609   for p :: "real poly"
  2610   by (metis less_not_sym mult_less_0_iff poly_IVT_neg poly_IVT_pos)
  2611 
  2612 lemma poly_MVT: "a < b \<Longrightarrow> \<exists>x. a < x \<and> x < b \<and> poly p b - poly p a = (b - a) * poly (pderiv p) x"
  2613   for a b :: real
  2614   using MVT [of a b "poly p"]
  2615   apply auto
  2616   apply (rule_tac x = z in exI)
  2617   apply (auto simp add: mult_left_cancel poly_DERIV [THEN DERIV_unique])
  2618   done
  2619 
  2620 lemma poly_MVT':
  2621   fixes a b :: real
  2622   assumes "{min a b..max a b} \<subseteq> A"
  2623   shows "\<exists>x\<in>A. poly p b - poly p a = (b - a) * poly (pderiv p) x"
  2624 proof (cases a b rule: linorder_cases)
  2625   case less
  2626   from poly_MVT[OF less, of p] guess x by (elim exE conjE)
  2627   then show ?thesis by (intro bexI[of _ x]) (auto intro!: subsetD[OF assms])
  2628 next
  2629   case greater
  2630   from poly_MVT[OF greater, of p] guess x by (elim exE conjE)
  2631   then show ?thesis by (intro bexI[of _ x]) (auto simp: algebra_simps intro!: subsetD[OF assms])
  2632 qed (use assms in auto)
  2633 
  2634 lemma poly_pinfty_gt_lc:
  2635   fixes p :: "real poly"
  2636   assumes "lead_coeff p > 0"
  2637   shows "\<exists>n. \<forall> x \<ge> n. poly p x \<ge> lead_coeff p"
  2638   using assms
  2639 proof (induct p)
  2640   case 0
  2641   then show ?case by auto
  2642 next
  2643   case (pCons a p)
  2644   from this(1) consider "a \<noteq> 0" "p = 0" | "p \<noteq> 0" by auto
  2645   then show ?case
  2646   proof cases
  2647     case 1
  2648     then show ?thesis by auto
  2649   next
  2650     case 2
  2651     with pCons obtain n1 where gte_lcoeff: "\<forall>x\<ge>n1. lead_coeff p \<le> poly p x"
  2652       by auto
  2653     from pCons(3) \<open>p \<noteq> 0\<close> have gt_0: "lead_coeff p > 0" by auto
  2654     define n where "n = max n1 (1 + \<bar>a\<bar> / lead_coeff p)"
  2655     have "lead_coeff (pCons a p) \<le> poly (pCons a p) x" if "n \<le> x" for x
  2656     proof -
  2657       from gte_lcoeff that have "lead_coeff p \<le> poly p x"
  2658         by (auto simp: n_def)
  2659       with gt_0 have "\<bar>a\<bar> / lead_coeff p \<ge> \<bar>a\<bar> / poly p x" and "poly p x > 0"
  2660         by (auto intro: frac_le)
  2661       with \<open>n \<le> x\<close>[unfolded n_def] have "x \<ge> 1 + \<bar>a\<bar> / poly p x"
  2662         by auto
  2663       with \<open>lead_coeff p \<le> poly p x\<close> \<open>poly p x > 0\<close> \<open>p \<noteq> 0\<close>
  2664       show "lead_coeff (pCons a p) \<le> poly (pCons a p) x"
  2665         by (auto simp: field_simps)
  2666     qed
  2667     then show ?thesis by blast
  2668   qed
  2669 qed
  2670 
  2671 lemma lemma_order_pderiv1:
  2672   "pderiv ([:- a, 1:] ^ Suc n * q) = [:- a, 1:] ^ Suc n * pderiv q +
  2673     smult (of_nat (Suc n)) (q * [:- a, 1:] ^ n)"
  2674   by (simp only: pderiv_mult pderiv_power_Suc) (simp del: power_Suc of_nat_Suc add: pderiv_pCons)
  2675 
  2676 lemma lemma_order_pderiv:
  2677   fixes p :: "'a :: field_char_0 poly"
  2678   assumes n: "0 < n"
  2679     and pd: "pderiv p \<noteq> 0"
  2680     and pe: "p = [:- a, 1:] ^ n * q"
  2681     and nd: "\<not> [:- a, 1:] dvd q"
  2682   shows "n = Suc (order a (pderiv p))"
  2683 proof -
  2684   from assms have "pderiv ([:- a, 1:] ^ n * q) \<noteq> 0"
  2685     by auto
  2686   from assms obtain n' where "n = Suc n'" "0 < Suc n'" "pderiv ([:- a, 1:] ^ Suc n' * q) \<noteq> 0"
  2687     by (cases n) auto
  2688   have *: "k dvd k * pderiv q + smult (of_nat (Suc n')) l \<Longrightarrow> k dvd l" for k l
  2689     by (auto simp del: of_nat_Suc simp: dvd_add_right_iff dvd_smult_iff)
  2690   have "n' = order a (pderiv ([:- a, 1:] ^ Suc n' * q))"
  2691   proof (rule order_unique_lemma)
  2692     show "[:- a, 1:] ^ n' dvd pderiv ([:- a, 1:] ^ Suc n' * q)"
  2693       apply (subst lemma_order_pderiv1)
  2694       apply (rule dvd_add)
  2695        apply (metis dvdI dvd_mult2 power_Suc2)
  2696       apply (metis dvd_smult dvd_triv_right)
  2697       done
  2698     show "\<not> [:- a, 1:] ^ Suc n' dvd pderiv ([:- a, 1:] ^ Suc n' * q)"
  2699       apply (subst lemma_order_pderiv1)
  2700       apply (metis * nd dvd_mult_cancel_right power_not_zero pCons_eq_0_iff power_Suc zero_neq_one)
  2701       done
  2702   qed
  2703   then show ?thesis
  2704     by (metis \<open>n = Suc n'\<close> pe)
  2705 qed
  2706 
  2707 lemma order_pderiv: "pderiv p \<noteq> 0 \<Longrightarrow> order a p \<noteq> 0 \<Longrightarrow> order a p = Suc (order a (pderiv p))"
  2708   for p :: "'a::field_char_0 poly"
  2709   apply (cases "p = 0")
  2710    apply simp
  2711   apply (drule_tac a = a and p = p in order_decomp)
  2712   using neq0_conv
  2713   apply (blast intro: lemma_order_pderiv)
  2714   done
  2715 
  2716 lemma poly_squarefree_decomp_order:
  2717   fixes p :: "'a::field_char_0 poly"
  2718   assumes "pderiv p \<noteq> 0"
  2719     and p: "p = q * d"
  2720     and p': "pderiv p = e * d"
  2721     and d: "d = r * p + s * pderiv p"
  2722   shows "order a q = (if order a p = 0 then 0 else 1)"
  2723 proof (rule classical)
  2724   assume 1: "\<not> ?thesis"
  2725   from \<open>pderiv p \<noteq> 0\<close> have "p \<noteq> 0" by auto
  2726   with p have "order a p = order a q + order a d"
  2727     by (simp add: order_mult)
  2728   with 1 have "order a p \<noteq> 0"
  2729     by (auto split: if_splits)
  2730   from \<open>pderiv p \<noteq> 0\<close> \<open>pderiv p = e * d\<close> have "order a (pderiv p) = order a e + order a d"
  2731     by (simp add: order_mult)
  2732   from \<open>pderiv p \<noteq> 0\<close> \<open>order a p \<noteq> 0\<close> have "order a p = Suc (order a (pderiv p))"
  2733     by (rule order_pderiv)
  2734   from \<open>p \<noteq> 0\<close> \<open>p = q * d\<close> have "d \<noteq> 0"
  2735     by simp
  2736   have "([:-a, 1:] ^ (order a (pderiv p))) dvd d"
  2737     apply (simp add: d)
  2738     apply (rule dvd_add)
  2739      apply (rule dvd_mult)
  2740      apply (simp add: order_divides \<open>p \<noteq> 0\<close> \<open>order a p = Suc (order a (pderiv p))\<close>)
  2741     apply (rule dvd_mult)
  2742     apply (simp add: order_divides)
  2743     done
  2744   with \<open>d \<noteq> 0\<close> have "order a (pderiv p) \<le> order a d"
  2745     by (simp add: order_divides)
  2746   show ?thesis
  2747     using \<open>order a p = order a q + order a d\<close>
  2748       and \<open>order a (pderiv p) = order a e + order a d\<close>
  2749       and \<open>order a p = Suc (order a (pderiv p))\<close>
  2750       and \<open>order a (pderiv p) \<le> order a d\<close>
  2751     by auto
  2752 qed
  2753 
  2754 lemma poly_squarefree_decomp_order2:
  2755   "pderiv p \<noteq> 0 \<Longrightarrow> p = q * d \<Longrightarrow> pderiv p = e * d \<Longrightarrow>
  2756     d = r * p + s * pderiv p \<Longrightarrow> \<forall>a. order a q = (if order a p = 0 then 0 else 1)"
  2757   for p :: "'a::field_char_0 poly"
  2758   by (blast intro: poly_squarefree_decomp_order)
  2759 
  2760 lemma order_pderiv2:
  2761   "pderiv p \<noteq> 0 \<Longrightarrow> order a p \<noteq> 0 \<Longrightarrow> order a (pderiv p) = n \<longleftrightarrow> order a p = Suc n"
  2762   for p :: "'a::field_char_0 poly"
  2763   by (auto dest: order_pderiv)
  2764 
  2765 definition rsquarefree :: "'a::idom poly \<Rightarrow> bool"
  2766   where "rsquarefree p \<longleftrightarrow> p \<noteq> 0 \<and> (\<forall>a. order a p = 0 \<or> order a p = 1)"
  2767 
  2768 lemma pderiv_iszero: "pderiv p = 0 \<Longrightarrow> \<exists>h. p = [:h:]"
  2769   for p :: "'a::{semidom,semiring_char_0} poly"
  2770   by (cases p) (auto simp: pderiv_eq_0_iff split: if_splits)
  2771 
  2772 lemma rsquarefree_roots: "rsquarefree p \<longleftrightarrow> (\<forall>a. \<not> (poly p a = 0 \<and> poly (pderiv p) a = 0))"
  2773   for p :: "'a::field_char_0 poly"
  2774   apply (simp add: rsquarefree_def)
  2775   apply (case_tac "p = 0")
  2776    apply simp
  2777   apply simp
  2778   apply (case_tac "pderiv p = 0")
  2779    apply simp
  2780    apply (drule pderiv_iszero, clarsimp)
  2781    apply (metis coeff_0 coeff_pCons_0 degree_pCons_0 le0 le_antisym order_degree)
  2782   apply (force simp add: order_root order_pderiv2)
  2783   done
  2784 
  2785 lemma poly_squarefree_decomp:
  2786   fixes p :: "'a::field_char_0 poly"
  2787   assumes "pderiv p \<noteq> 0"
  2788     and "p = q * d"
  2789     and "pderiv p = e * d"
  2790     and "d = r * p + s * pderiv p"
  2791   shows "rsquarefree q \<and> (\<forall>a. poly q a = 0 \<longleftrightarrow> poly p a = 0)"
  2792 proof -
  2793   from \<open>pderiv p \<noteq> 0\<close> have "p \<noteq> 0" by auto
  2794   with \<open>p = q * d\<close> have "q \<noteq> 0" by simp
  2795   from assms have "\<forall>a. order a q = (if order a p = 0 then 0 else 1)"
  2796     by (rule poly_squarefree_decomp_order2)
  2797   with \<open>p \<noteq> 0\<close> \<open>q \<noteq> 0\<close> show ?thesis
  2798     by (simp add: rsquarefree_def order_root)
  2799 qed
  2800 
  2801 
  2802 subsection \<open>Algebraic numbers\<close>
  2803 
  2804 text \<open>
  2805   Algebraic numbers can be defined in two equivalent ways: all real numbers that are
  2806   roots of rational polynomials or of integer polynomials. The Algebraic-Numbers AFP entry
  2807   uses the rational definition, but we need the integer definition.
  2808 
  2809   The equivalence is obvious since any rational polynomial can be multiplied with the
  2810   LCM of its coefficients, yielding an integer polynomial with the same roots.
  2811 \<close>
  2812 
  2813 definition algebraic :: "'a :: field_char_0 \<Rightarrow> bool"
  2814   where "algebraic x \<longleftrightarrow> (\<exists>p. (\<forall>i. coeff p i \<in> \<int>) \<and> p \<noteq> 0 \<and> poly p x = 0)"
  2815 
  2816 lemma algebraicI: "(\<And>i. coeff p i \<in> \<int>) \<Longrightarrow> p \<noteq> 0 \<Longrightarrow> poly p x = 0 \<Longrightarrow> algebraic x"
  2817   unfolding algebraic_def by blast
  2818 
  2819 lemma algebraicE:
  2820   assumes "algebraic x"
  2821   obtains p where "\<And>i. coeff p i \<in> \<int>" "p \<noteq> 0" "poly p x = 0"
  2822   using assms unfolding algebraic_def by blast
  2823 
  2824 lemma algebraic_altdef: "algebraic x \<longleftrightarrow> (\<exists>p. (\<forall>i. coeff p i \<in> \<rat>) \<and> p \<noteq> 0 \<and> poly p x = 0)"
  2825   for p :: "'a::field_char_0 poly"
  2826 proof safe
  2827   fix p
  2828   assume rat: "\<forall>i. coeff p i \<in> \<rat>" and root: "poly p x = 0" and nz: "p \<noteq> 0"
  2829   define cs where "cs = coeffs p"
  2830   from rat have "\<forall>c\<in>range (coeff p). \<exists>c'. c = of_rat c'"
  2831     unfolding Rats_def by blast
  2832   then obtain f where f: "coeff p i = of_rat (f (coeff p i))" for i
  2833     by (subst (asm) bchoice_iff) blast
  2834   define cs' where "cs' = map (quotient_of \<circ> f) (coeffs p)"
  2835   define d where "d = Lcm (set (map snd cs'))"
  2836   define p' where "p' = smult (of_int d) p"
  2837 
  2838   have "coeff p' n \<in> \<int>" for n
  2839   proof (cases "n \<le> degree p")
  2840     case True
  2841     define c where "c = coeff p n"
  2842     define a where "a = fst (quotient_of (f (coeff p n)))"
  2843     define b where "b = snd (quotient_of (f (coeff p n)))"
  2844     have b_pos: "b > 0"
  2845       unfolding b_def using quotient_of_denom_pos' by simp
  2846     have "coeff p' n = of_int d * coeff p n"
  2847       by (simp add: p'_def)
  2848     also have "coeff p n = of_rat (of_int a / of_int b)"
  2849       unfolding a_def b_def
  2850       by (subst quotient_of_div [of "f (coeff p n)", symmetric]) (simp_all add: f [symmetric])
  2851     also have "of_int d * \<dots> = of_rat (of_int (a*d) / of_int b)"
  2852       by (simp add: of_rat_mult of_rat_divide)
  2853     also from nz True have "b \<in> snd ` set cs'"
  2854       by (force simp: cs'_def o_def b_def coeffs_def simp del: upt_Suc)
  2855     then have "b dvd (a * d)"
  2856       by (simp add: d_def)
  2857     then have "of_int (a * d) / of_int b \<in> (\<int> :: rat set)"
  2858       by (rule of_int_divide_in_Ints)
  2859     then have "of_rat (of_int (a * d) / of_int b) \<in> \<int>" by (elim Ints_cases) auto
  2860     finally show ?thesis .
  2861   next
  2862     case False
  2863     then show ?thesis
  2864       by (auto simp: p'_def not_le coeff_eq_0)
  2865   qed
  2866   moreover have "set (map snd cs') \<subseteq> {0<..}"
  2867     unfolding cs'_def using quotient_of_denom_pos' by (auto simp: coeffs_def simp del: upt_Suc)
  2868   then have "d \<noteq> 0"
  2869     unfolding d_def by (induct cs') simp_all
  2870   with nz have "p' \<noteq> 0" by (simp add: p'_def)
  2871   moreover from root have "poly p' x = 0"
  2872     by (simp add: p'_def)
  2873   ultimately show "algebraic x"
  2874     unfolding algebraic_def by blast
  2875 next
  2876   assume "algebraic x"
  2877   then obtain p where p: "coeff p i \<in> \<int>" "poly p x = 0" "p \<noteq> 0" for i
  2878     by (force simp: algebraic_def)
  2879   moreover have "coeff p i \<in> \<int> \<Longrightarrow> coeff p i \<in> \<rat>" for i
  2880     by (elim Ints_cases) simp
  2881   ultimately show "\<exists>p. (\<forall>i. coeff p i \<in> \<rat>) \<and> p \<noteq> 0 \<and> poly p x = 0" by auto
  2882 qed
  2883 
  2884 
  2885 subsection \<open>Division of polynomials\<close>
  2886 
  2887 subsubsection \<open>Division in general\<close>
  2888 
  2889 instantiation poly :: (idom_divide) idom_divide
  2890 begin
  2891 
  2892 fun divide_poly_main :: "'a \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a poly"
  2893   where
  2894     "divide_poly_main lc q r d dr (Suc n) =
  2895       (let cr = coeff r dr; a = cr div lc; mon = monom a n in
  2896         if False \<or> a * lc = cr then (* False \<or> is only because of problem in function-package *)
  2897           divide_poly_main
  2898             lc
  2899             (q + mon)
  2900             (r - mon * d)
  2901             d (dr - 1) n else 0)"
  2902   | "divide_poly_main lc q r d dr 0 = q"
  2903 
  2904 definition divide_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
  2905   where "divide_poly f g =
  2906     (if g = 0 then 0
  2907      else
  2908       divide_poly_main (coeff g (degree g)) 0 f g (degree f)
  2909         (1 + length (coeffs f) - length (coeffs g)))"
  2910 
  2911 lemma divide_poly_main:
  2912   assumes d: "d \<noteq> 0" "lc = coeff d (degree d)"
  2913     and "degree (d * r) \<le> dr" "divide_poly_main lc q (d * r) d dr n = q'"
  2914     and "n = 1 + dr - degree d \<or> dr = 0 \<and> n = 0 \<and> d * r = 0"
  2915   shows "q' = q + r"
  2916   using assms(3-)
  2917 proof (induct n arbitrary: q r dr)
  2918   case (Suc n)
  2919   let ?rr = "d * r"
  2920   let ?a = "coeff ?rr dr"
  2921   let ?qq = "?a div lc"
  2922   define b where [simp]: "b = monom ?qq n"
  2923   let ?rrr =  "d * (r - b)"
  2924   let ?qqq = "q + b"
  2925   note res = Suc(3)
  2926   from Suc(4) have dr: "dr = n + degree d" by auto
  2927   from d have lc: "lc \<noteq> 0" by auto
  2928   have "coeff (b * d) dr = coeff b n * coeff d (degree d)"
  2929   proof (cases "?qq = 0")
  2930     case True
  2931     then show ?thesis by simp
  2932   next
  2933     case False
  2934     then have n: "n = degree b"
  2935       by (simp add: degree_monom_eq)
  2936     show ?thesis
  2937       unfolding n dr by (simp add: coeff_mult_degree_sum)
  2938   qed
  2939   also have "\<dots> = lc * coeff b n"
  2940     by (simp add: d)
  2941   finally have c2: "coeff (b * d) dr = lc * coeff b n" .
  2942   have rrr: "?rrr = ?rr - b * d"
  2943     by (simp add: field_simps)
  2944   have c1: "coeff (d * r) dr = lc * coeff r n"
  2945   proof (cases "degree r = n")
  2946     case True
  2947     with Suc(2) show ?thesis
  2948       unfolding dr using coeff_mult_degree_sum[of d r] d by (auto simp: ac_simps)
  2949   next
  2950     case False
  2951     from dr Suc(2) have "degree r \<le> n"
  2952       by auto
  2953         (metis add.commute add_le_cancel_left d(1) degree_0 degree_mult_eq
  2954           diff_is_0_eq diff_zero le_cases)
  2955     with False have r_n: "degree r < n"
  2956       by auto
  2957     then have right: "lc * coeff r n = 0"
  2958       by (simp add: coeff_eq_0)
  2959     have "coeff (d * r) dr = coeff (d * r) (degree d + n)"
  2960       by (simp add: dr ac_simps)
  2961     also from r_n have "\<dots> = 0"
  2962       by (metis False Suc.prems(1) add.commute add_left_imp_eq coeff_degree_mult coeff_eq_0
  2963         coeff_mult_degree_sum degree_mult_le dr le_eq_less_or_eq)
  2964     finally show ?thesis
  2965       by (simp only: right)
  2966   qed
  2967   have c0: "coeff ?rrr dr = 0"
  2968     and id: "lc * (coeff (d * r) dr div lc) = coeff (d * r) dr"
  2969     unfolding rrr coeff_diff c2
  2970     unfolding b_def coeff_monom coeff_smult c1 using lc by auto
  2971   from res[unfolded divide_poly_main.simps[of lc q] Let_def] id
  2972   have res: "divide_poly_main lc ?qqq ?rrr d (dr - 1) n = q'"
  2973     by (simp del: divide_poly_main.simps add: field_simps)
  2974   note IH = Suc(1)[OF _ res]
  2975   from Suc(4) have dr: "dr = n + degree d" by auto
  2976   from Suc(2) have deg_rr: "degree ?rr \<le> dr" by auto
  2977   have deg_bd: "degree (b * d) \<le> dr"
  2978     unfolding dr b_def by (rule order.trans[OF degree_mult_le]) (auto simp: degree_monom_le)
  2979   have "degree ?rrr \<le> dr"
  2980     unfolding rrr by (rule degree_diff_le[OF deg_rr deg_bd])
  2981   with c0 have deg_rrr: "degree ?rrr \<le> (dr - 1)"
  2982     by (rule coeff_0_degree_minus_1)
  2983   have "n = 1 + (dr - 1) - degree d \<or> dr - 1 = 0 \<and> n = 0 \<and> ?rrr = 0"
  2984   proof (cases dr)
  2985     case 0
  2986     with Suc(4) have 0: "dr = 0" "n = 0" "degree d = 0"
  2987       by auto
  2988     with deg_rrr have "degree ?rrr = 0"
  2989       by simp
  2990     from degree_eq_zeroE[OF this] obtain a where rrr: "?rrr = [:a:]"
  2991       by metis
  2992     show ?thesis
  2993       unfolding 0 using c0 unfolding rrr 0 by simp
  2994   next
  2995     case _: Suc
  2996     with Suc(4) show ?thesis by auto
  2997   qed
  2998   from IH[OF deg_rrr this] show ?case
  2999     by simp
  3000 next
  3001   case 0
  3002   show ?case
  3003   proof (cases "r = 0")
  3004     case True
  3005     with 0 show ?thesis by auto
  3006   next
  3007     case False
  3008     from d False have "degree (d * r) = degree d + degree r"
  3009       by (subst degree_mult_eq) auto
  3010     with 0 d show ?thesis by auto
  3011   qed
  3012 qed
  3013 
  3014 lemma divide_poly_main_0: "divide_poly_main 0 0 r d dr n = 0"
  3015 proof (induct n arbitrary: r d dr)
  3016   case 0
  3017   then show ?case by simp
  3018 next
  3019   case Suc
  3020   show ?case
  3021     unfolding divide_poly_main.simps[of _ _ r] Let_def
  3022     by (simp add: Suc del: divide_poly_main.simps)
  3023 qed
  3024 
  3025 lemma divide_poly:
  3026   assumes g: "g \<noteq> 0"
  3027   shows "(f * g) div g = (f :: 'a poly)"
  3028 proof -
  3029   have len: "length (coeffs f) = Suc (degree f)" if "f \<noteq> 0" for f :: "'a poly"
  3030     using that unfolding degree_eq_length_coeffs by auto
  3031   have "divide_poly_main (coeff g (degree g)) 0 (g * f) g (degree (g * f))
  3032     (1 + length (coeffs (g * f)) - length (coeffs  g)) = (f * g) div g"
  3033     by (simp add: divide_poly_def Let_def ac_simps)
  3034   note main = divide_poly_main[OF g refl le_refl this]
  3035   have "(f * g) div g = 0 + f"
  3036   proof (rule main, goal_cases)
  3037     case 1
  3038     show ?case
  3039     proof (cases "f = 0")
  3040       case True
  3041       with g show ?thesis
  3042         by (auto simp: degree_eq_length_coeffs)
  3043     next
  3044       case False
  3045       with g have fg: "g * f \<noteq> 0" by auto
  3046       show ?thesis
  3047         unfolding len[OF fg] len[OF g] by auto
  3048     qed
  3049   qed
  3050   then show ?thesis by simp
  3051 qed
  3052 
  3053 lemma divide_poly_0: "f div 0 = 0"
  3054   for f :: "'a poly"
  3055   by (simp add: divide_poly_def Let_def divide_poly_main_0)
  3056 
  3057 instance
  3058   by standard (auto simp: divide_poly divide_poly_0)
  3059 
  3060 end
  3061 
  3062 instance poly :: (idom_divide) algebraic_semidom ..
  3063 
  3064 lemma div_const_poly_conv_map_poly:
  3065   assumes "[:c:] dvd p"
  3066   shows "p div [:c:] = map_poly (\<lambda>x. x div c) p"
  3067 proof (cases "c = 0")
  3068   case True
  3069   then show ?thesis
  3070     by (auto intro!: poly_eqI simp: coeff_map_poly)
  3071 next
  3072   case False
  3073   from assms obtain q where p: "p = [:c:] * q" by (rule dvdE)
  3074   moreover {
  3075     have "smult c q = [:c:] * q"
  3076       by simp
  3077     also have "\<dots> div [:c:] = q"
  3078       by (rule nonzero_mult_div_cancel_left) (use False in auto)
  3079     finally have "smult c q div [:c:] = q" .
  3080   }
  3081   ultimately show ?thesis by (intro poly_eqI) (auto simp: coeff_map_poly False)
  3082 qed
  3083 
  3084 lemma is_unit_monom_0:
  3085   fixes a :: "'a::field"
  3086   assumes "a \<noteq> 0"
  3087   shows "is_unit (monom a 0)"
  3088 proof
  3089   from assms show "1 = monom a 0 * monom (inverse a) 0"
  3090     by (simp add: mult_monom)
  3091 qed
  3092 
  3093 lemma is_unit_triv: "a \<noteq> 0 \<Longrightarrow> is_unit [:a:]"
  3094   for a :: "'a::field"
  3095   by (simp add: is_unit_monom_0 monom_0 [symmetric])
  3096 
  3097 lemma is_unit_iff_degree:
  3098   fixes p :: "'a::field poly"
  3099   assumes "p \<noteq> 0"
  3100   shows "is_unit p \<longleftrightarrow> degree p = 0"
  3101     (is "?lhs \<longleftrightarrow> ?rhs")
  3102 proof
  3103   assume ?rhs
  3104   then obtain a where "p = [:a:]"
  3105     by (rule degree_eq_zeroE)
  3106   with assms show ?lhs
  3107     by (simp add: is_unit_triv)
  3108 next
  3109   assume ?lhs
  3110   then obtain q where "q \<noteq> 0" "p * q = 1" ..
  3111   then have "degree (p * q) = degree 1"
  3112     by simp
  3113   with \<open>p \<noteq> 0\<close> \<open>q \<noteq> 0\<close> have "degree p + degree q = 0"
  3114     by (simp add: degree_mult_eq)
  3115   then show ?rhs by simp
  3116 qed
  3117 
  3118 lemma is_unit_pCons_iff: "is_unit (pCons a p) \<longleftrightarrow> p = 0 \<and> a \<noteq> 0"
  3119   for p :: "'a::field poly"
  3120   by (cases "p = 0") (auto simp: is_unit_triv is_unit_iff_degree)
  3121 
  3122 lemma is_unit_monom_trival: "is_unit p \<Longrightarrow> monom (coeff p (degree p)) 0 = p"
  3123   for p :: "'a::field poly"
  3124   by (cases p) (simp_all add: monom_0 is_unit_pCons_iff)
  3125 
  3126 lemma is_unit_const_poly_iff: "[:c:] dvd 1 \<longleftrightarrow> c dvd 1"
  3127   for c :: "'a::{comm_semiring_1,semiring_no_zero_divisors}"
  3128   by (auto simp: one_pCons)
  3129 
  3130 lemma is_unit_polyE:
  3131   fixes p :: "'a :: {comm_semiring_1,semiring_no_zero_divisors} poly"
  3132   assumes "p dvd 1"
  3133   obtains c where "p = [:c:]" "c dvd 1"
  3134 proof -
  3135   from assms obtain q where "1 = p * q"
  3136     by (rule dvdE)
  3137   then have "p \<noteq> 0" and "q \<noteq> 0"
  3138     by auto
  3139   from \<open>1 = p * q\<close> have "degree 1 = degree (p * q)"
  3140     by simp
  3141   also from \<open>p \<noteq> 0\<close> and \<open>q \<noteq> 0\<close> have "\<dots> = degree p + degree q"
  3142     by (simp add: degree_mult_eq)
  3143   finally have "degree p = 0" by simp
  3144   with degree_eq_zeroE obtain c where c: "p = [:c:]" .
  3145   with \<open>p dvd 1\<close> have "c dvd 1"
  3146     by (simp add: is_unit_const_poly_iff)
  3147   with c show thesis ..
  3148 qed
  3149 
  3150 lemma is_unit_polyE':
  3151   fixes p :: "'a::field poly"
  3152   assumes "is_unit p"
  3153   obtains a where "p = monom a 0" and "a \<noteq> 0"
  3154 proof -
  3155   obtain a q where "p = pCons a q"
  3156     by (cases p)
  3157   with assms have "p = [:a:]" and "a \<noteq> 0"
  3158     by (simp_all add: is_unit_pCons_iff)
  3159   with that show thesis by (simp add: monom_0)
  3160 qed
  3161 
  3162 lemma is_unit_poly_iff: "p dvd 1 \<longleftrightarrow> (\<exists>c. p = [:c:] \<and> c dvd 1)"
  3163   for p :: "'a::{comm_semiring_1,semiring_no_zero_divisors} poly"
  3164   by (auto elim: is_unit_polyE simp add: is_unit_const_poly_iff)
  3165 
  3166 
  3167 subsubsection \<open>Pseudo-Division\<close>
  3168 
  3169 text \<open>This part is by René Thiemann and Akihisa Yamada.\<close>
  3170 
  3171 fun pseudo_divmod_main ::
  3172   "'a :: comm_ring_1  \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a poly \<times> 'a poly"
  3173   where
  3174     "pseudo_divmod_main lc q r d dr (Suc n) =
  3175       (let
  3176         rr = smult lc r;
  3177         qq = coeff r dr;
  3178         rrr = rr - monom qq n * d;
  3179         qqq = smult lc q + monom qq n
  3180        in pseudo_divmod_main lc qqq rrr d (dr - 1) n)"
  3181   | "pseudo_divmod_main lc q r d dr 0 = (q,r)"
  3182 
  3183 definition pseudo_divmod :: "'a :: comm_ring_1 poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<times> 'a poly"
  3184   where "pseudo_divmod p q \<equiv>
  3185     if q = 0 then (0, p)
  3186     else
  3187       pseudo_divmod_main (coeff q (degree q)) 0 p q (degree p)
  3188         (1 + length (coeffs p) - length (coeffs q))"
  3189 
  3190 lemma pseudo_divmod_main:
  3191   assumes d: "d \<noteq> 0" "lc = coeff d (degree d)"
  3192     and "degree r \<le> dr" "pseudo_divmod_main lc q r d dr n = (q',r')"
  3193     and "n = 1 + dr - degree d \<or> dr = 0 \<and> n = 0 \<and> r = 0"
  3194   shows "(r' = 0 \<or> degree r' < degree d) \<and> smult (lc^n) (d * q + r) = d * q' + r'"
  3195   using assms(3-)
  3196 proof (induct n arbitrary: q r dr)
  3197   case 0
  3198   then show ?case by auto
  3199 next
  3200   case (Suc n)
  3201   let ?rr = "smult lc r"
  3202   let ?qq = "coeff r dr"
  3203   define b where [simp]: "b = monom ?qq n"
  3204   let ?rrr = "?rr - b * d"
  3205   let ?qqq = "smult lc q + b"
  3206   note res = Suc(3)
  3207   from res[unfolded pseudo_divmod_main.simps[of lc q] Let_def]
  3208   have res: "pseudo_divmod_main lc ?qqq ?rrr d (dr - 1) n = (q',r')"
  3209     by (simp del: pseudo_divmod_main.simps)
  3210   from Suc(4) have dr: "dr = n + degree d" by auto
  3211   have "coeff (b * d) dr = coeff b n * coeff d (degree d)"
  3212   proof (cases "?qq = 0")
  3213     case True
  3214     then show ?thesis by auto
  3215   next
  3216     case False
  3217     then have n: "n = degree b"
  3218       by (simp add: degree_monom_eq)
  3219     show ?thesis
  3220       unfolding n dr by (simp add: coeff_mult_degree_sum)
  3221   qed
  3222   also have "\<dots> = lc * coeff b n" by (simp add: d)
  3223   finally have "coeff (b * d) dr = lc * coeff b n" .
  3224   moreover have "coeff ?rr dr = lc * coeff r dr"
  3225     by simp
  3226   ultimately have c0: "coeff ?rrr dr = 0"
  3227     by auto
  3228   from Suc(4) have dr: "dr = n + degree d" by auto
  3229   have deg_rr: "degree ?rr \<le> dr"
  3230     using Suc(2) degree_smult_le dual_order.trans by blast
  3231   have deg_bd: "degree (b * d) \<le> dr"
  3232     unfolding dr by (rule order.trans[OF degree_mult_le]) (auto simp: degree_monom_le)
  3233   have "degree ?rrr \<le> dr"
  3234     using degree_diff_le[OF deg_rr deg_bd] by auto
  3235   with c0 have deg_rrr: "degree ?rrr \<le> (dr - 1)"
  3236     by (rule coeff_0_degree_minus_1)
  3237   have "n = 1 + (dr - 1) - degree d \<or> dr - 1 = 0 \<and> n = 0 \<and> ?rrr = 0"
  3238   proof (cases dr)
  3239     case 0
  3240     with Suc(4) have 0: "dr = 0" "n = 0" "degree d = 0" by auto
  3241     with deg_rrr have "degree ?rrr = 0" by simp
  3242     then have "\<exists>a. ?rrr = [:a:]"
  3243       by (metis degree_pCons_eq_if old.nat.distinct(2) pCons_cases)
  3244     from this obtain a where rrr: "?rrr = [:a:]"
  3245       by auto
  3246     show ?thesis
  3247       unfolding 0 using c0 unfolding rrr 0 by simp
  3248   next
  3249     case _: Suc
  3250     with Suc(4) show ?thesis by auto
  3251   qed
  3252   note IH = Suc(1)[OF deg_rrr res this]
  3253   show ?case
  3254   proof (intro conjI)
  3255     from IH show "r' = 0 \<or> degree r' < degree d"
  3256       by blast
  3257     show "smult (lc ^ Suc n) (d * q + r) = d * q' + r'"
  3258       unfolding IH[THEN conjunct2,symmetric]
  3259       by (simp add: field_simps smult_add_right)
  3260   qed
  3261 qed
  3262 
  3263 lemma pseudo_divmod:
  3264   assumes g: "g \<noteq> 0"
  3265     and *: "pseudo_divmod f g = (q,r)"
  3266   shows "smult (coeff g (degree g) ^ (Suc (degree f) - degree g)) f = g * q + r"  (is ?A)
  3267     and "r = 0 \<or> degree r < degree g"  (is ?B)
  3268 proof -
  3269   from *[unfolded pseudo_divmod_def Let_def]
  3270   have "pseudo_divmod_main (coeff g (degree g)) 0 f g (degree f)
  3271       (1 + length (coeffs f) - length (coeffs g)) = (q, r)"
  3272     by (auto simp: g)
  3273   note main = pseudo_divmod_main[OF _ _ _ this, OF g refl le_refl]
  3274   from g have "1 + length (coeffs f) - length (coeffs g) = 1 + degree f - degree g \<or>
  3275     degree f = 0 \<and> 1 + length (coeffs f) - length (coeffs g) = 0 \<and> f = 0"
  3276     by (cases "f = 0"; cases "coeffs g") (auto simp: degree_eq_length_coeffs)
  3277   note main' = main[OF this]
  3278   then show "r = 0 \<or> degree r < degree g" by auto
  3279   show "smult (coeff g (degree g) ^ (Suc (degree f) - degree g)) f = g * q + r"
  3280     by (subst main'[THEN conjunct2, symmetric], simp add: degree_eq_length_coeffs,
  3281         cases "f = 0"; cases "coeffs g", use g in auto)
  3282 qed
  3283 
  3284 definition "pseudo_mod_main lc r d dr n = snd (pseudo_divmod_main lc 0 r d dr n)"
  3285 
  3286 lemma snd_pseudo_divmod_main:
  3287   "snd (pseudo_divmod_main lc q r d dr n) = snd (pseudo_divmod_main lc q' r d dr n)"
  3288   by (induct n arbitrary: q q' lc r d dr) (simp_all add: Let_def)
  3289 
  3290 definition pseudo_mod :: "'a::{comm_ring_1,semiring_1_no_zero_divisors} poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
  3291   where "pseudo_mod f g = snd (pseudo_divmod f g)"
  3292 
  3293 lemma pseudo_mod:
  3294   fixes f g :: "'a::{comm_ring_1,semiring_1_no_zero_divisors} poly"
  3295   defines "r \<equiv> pseudo_mod f g"
  3296   assumes g: "g \<noteq> 0"
  3297   shows "\<exists>a q. a \<noteq> 0 \<and> smult a f = g * q + r" "r = 0 \<or> degree r < degree g"
  3298 proof -
  3299   let ?cg = "coeff g (degree g)"
  3300   let ?cge = "?cg ^ (Suc (degree f) - degree g)"
  3301   define a where "a = ?cge"
  3302   from r_def[unfolded pseudo_mod_def] obtain q where pdm: "pseudo_divmod f g = (q, r)"
  3303     by (cases "pseudo_divmod f g") auto
  3304   from pseudo_divmod[OF g pdm] have id: "smult a f = g * q + r" and "r = 0 \<or> degree r < degree g"
  3305     by (auto simp: a_def)
  3306   show "r = 0 \<or> degree r < degree g" by fact
  3307   from g have "a \<noteq> 0"
  3308     by (auto simp: a_def)
  3309   with id show "\<exists>a q. a \<noteq> 0 \<and> smult a f = g * q + r"
  3310     by auto
  3311 qed
  3312 
  3313 lemma fst_pseudo_divmod_main_as_divide_poly_main:
  3314   assumes d: "d \<noteq> 0"
  3315   defines lc: "lc \<equiv> coeff d (degree d)"
  3316   shows "fst (pseudo_divmod_main lc q r d dr n) =
  3317     divide_poly_main lc (smult (lc^n) q) (smult (lc^n) r) d dr n"
  3318 proof (induct n arbitrary: q r dr)
  3319   case 0
  3320   then show ?case by simp
  3321 next
  3322   case (Suc n)
  3323   note lc0 = leading_coeff_neq_0[OF d, folded lc]
  3324   then have "pseudo_divmod_main lc q r d dr (Suc n) =
  3325     pseudo_divmod_main lc (smult lc q + monom (coeff r dr) n)
  3326       (smult lc r - monom (coeff r dr) n * d) d (dr - 1) n"
  3327     by (simp add: Let_def ac_simps)
  3328   also have "fst \<dots> = divide_poly_main lc
  3329      (smult (lc^n) (smult lc q + monom (coeff r dr) n))
  3330      (smult (lc^n) (smult lc r - monom (coeff r dr) n * d))
  3331      d (dr - 1) n"
  3332     by (simp only: Suc[unfolded divide_poly_main.simps Let_def])
  3333   also have "\<dots> = divide_poly_main lc (smult (lc ^ Suc n) q) (smult (lc ^ Suc n) r) d dr (Suc n)"
  3334     unfolding smult_monom smult_distribs mult_smult_left[symmetric]
  3335     using lc0 by (simp add: Let_def ac_simps)
  3336   finally show ?case .
  3337 qed
  3338 
  3339 
  3340 subsubsection \<open>Division in polynomials over fields\<close>
  3341 
  3342 lemma pseudo_divmod_field:
  3343   fixes g :: "'a::field poly"
  3344   assumes g: "g \<noteq> 0"
  3345     and *: "pseudo_divmod f g = (q,r)"
  3346   defines "c \<equiv> coeff g (degree g) ^ (Suc (degree f) - degree g)"
  3347   shows "f = g * smult (1/c) q + smult (1/c) r"
  3348 proof -
  3349   from leading_coeff_neq_0[OF g] have c0: "c \<noteq> 0"
  3350     by (auto simp: c_def)
  3351   from pseudo_divmod(1)[OF g *, folded c_def] have "smult c f = g * q + r"
  3352     by auto
  3353   also have "smult (1 / c) \<dots> = g * smult (1 / c) q + smult (1 / c) r"
  3354     by (simp add: smult_add_right)
  3355   finally show ?thesis
  3356     using c0 by auto
  3357 qed
  3358 
  3359 lemma divide_poly_main_field:
  3360   fixes d :: "'a::field poly"
  3361   assumes d: "d \<noteq> 0"
  3362   defines lc: "lc \<equiv> coeff d (degree d)"
  3363   shows "divide_poly_main lc q r d dr n =
  3364     fst (pseudo_divmod_main lc (smult ((1 / lc)^n) q) (smult ((1 / lc)^n) r) d dr n)"
  3365   unfolding lc by (subst fst_pseudo_divmod_main_as_divide_poly_main) (auto simp: d power_one_over)
  3366 
  3367 lemma divide_poly_field:
  3368   fixes f g :: "'a::field poly"
  3369   defines "f' \<equiv> smult ((1 / coeff g (degree g)) ^ (Suc (degree f) - degree g)) f"
  3370   shows "f div g = fst (pseudo_divmod f' g)"
  3371 proof (cases "g = 0")
  3372   case True
  3373   show ?thesis
  3374     unfolding divide_poly_def pseudo_divmod_def Let_def f'_def True
  3375     by (simp add: divide_poly_main_0)
  3376 next
  3377   case False
  3378   from leading_coeff_neq_0[OF False] have "degree f' = degree f"
  3379     by (auto simp: f'_def)
  3380   then show ?thesis
  3381     using length_coeffs_degree[of f'] length_coeffs_degree[of f]
  3382     unfolding divide_poly_def pseudo_divmod_def Let_def
  3383       divide_poly_main_field[OF False]
  3384       length_coeffs_degree[OF False]
  3385       f'_def
  3386     by force
  3387 qed
  3388 
  3389 instantiation poly :: ("{semidom_divide_unit_factor,idom_divide}") normalization_semidom
  3390 begin
  3391 
  3392 definition unit_factor_poly :: "'a poly \<Rightarrow> 'a poly"
  3393   where "unit_factor_poly p = [:unit_factor (lead_coeff p):]"
  3394 
  3395 definition normalize_poly :: "'a poly \<Rightarrow> 'a poly"
  3396   where "normalize p = p div [:unit_factor (lead_coeff p):]"
  3397 
  3398 instance
  3399 proof
  3400   fix p :: "'a poly"
  3401   show "unit_factor p * normalize p = p"
  3402   proof (cases "p = 0")
  3403     case True
  3404     then show ?thesis
  3405       by (simp add: unit_factor_poly_def normalize_poly_def)
  3406   next
  3407     case False
  3408     then have "lead_coeff p \<noteq> 0"
  3409       by simp
  3410     then have *: "unit_factor (lead_coeff p) \<noteq> 0"
  3411       using unit_factor_is_unit [of "lead_coeff p"] by auto
  3412     then have "unit_factor (lead_coeff p) dvd 1"
  3413       by (auto intro: unit_factor_is_unit)
  3414     then have **: "unit_factor (lead_coeff p) dvd c" for c
  3415       by (rule dvd_trans) simp
  3416     have ***: "unit_factor (lead_coeff p) * (c div unit_factor (lead_coeff p)) = c" for c
  3417     proof -
  3418       from ** obtain b where "c = unit_factor (lead_coeff p) * b" ..
  3419       with False * show ?thesis by simp
  3420     qed
  3421     have "p div [:unit_factor (lead_coeff p):] =
  3422       map_poly (\<lambda>c. c div unit_factor (lead_coeff p)) p"
  3423       by (simp add: const_poly_dvd_iff div_const_poly_conv_map_poly **)
  3424     then show ?thesis
  3425       by (simp add: normalize_poly_def unit_factor_poly_def
  3426         smult_conv_map_poly map_poly_map_poly o_def ***)
  3427   qed
  3428 next
  3429   fix p :: "'a poly"
  3430   assume "is_unit p"
  3431   then obtain c where p: "p = [:c:]" "c dvd 1"
  3432     by (auto simp: is_unit_poly_iff)
  3433   then show "unit_factor p = p"
  3434     by (simp add: unit_factor_poly_def monom_0 is_unit_unit_factor)
  3435 next
  3436   fix p :: "'a poly"
  3437   assume "p \<noteq> 0"
  3438   then show "is_unit (unit_factor p)"
  3439     by (simp add: unit_factor_poly_def monom_0 is_unit_poly_iff unit_factor_is_unit)
  3440 qed (simp_all add: normalize_poly_def unit_factor_poly_def monom_0 lead_coeff_mult unit_factor_mult)
  3441 
  3442 end
  3443 
  3444 lemma normalize_poly_eq_map_poly: "normalize p = map_poly (\<lambda>x. x div unit_factor (lead_coeff p)) p"
  3445 proof -
  3446   have "[:unit_factor (lead_coeff p):] dvd p"
  3447     by (metis unit_factor_poly_def unit_factor_self)
  3448   then show ?thesis
  3449     by (simp add: normalize_poly_def div_const_poly_conv_map_poly)
  3450 qed
  3451 
  3452 lemma coeff_normalize [simp]:
  3453   "coeff (normalize p) n = coeff p n div unit_factor (lead_coeff p)"
  3454   by (simp add: normalize_poly_eq_map_poly coeff_map_poly)
  3455 
  3456 class field_unit_factor = field + unit_factor +
  3457   assumes unit_factor_field [simp]: "unit_factor = id"
  3458 begin
  3459 
  3460 subclass semidom_divide_unit_factor
  3461 proof
  3462   fix a
  3463   assume "a \<noteq> 0"
  3464   then have "1 = a * inverse a" by simp
  3465   then have "a dvd 1" ..
  3466   then show "unit_factor a dvd 1" by simp
  3467 qed simp_all
  3468 
  3469 end
  3470 
  3471 lemma unit_factor_pCons:
  3472   "unit_factor (pCons a p) = (if p = 0 then [:unit_factor a:] else unit_factor p)"
  3473   by (simp add: unit_factor_poly_def)
  3474 
  3475 lemma normalize_monom [simp]: "normalize (monom a n) = monom (normalize a) n"
  3476   by (cases "a = 0") (simp_all add: map_poly_monom normalize_poly_eq_map_poly degree_monom_eq)
  3477 
  3478 lemma unit_factor_monom [simp]: "unit_factor (monom a n) = [:unit_factor a:]"
  3479   by (cases "a = 0") (simp_all add: unit_factor_poly_def degree_monom_eq)
  3480 
  3481 lemma normalize_const_poly: "normalize [:c:] = [:normalize c:]"
  3482   by (simp add: normalize_poly_eq_map_poly map_poly_pCons)
  3483 
  3484 lemma normalize_smult: "normalize (smult c p) = smult (normalize c) (normalize p)"
  3485 proof -
  3486   have "smult c p = [:c:] * p" by simp
  3487   also have "normalize \<dots> = smult (normalize c) (normalize p)"
  3488     by (subst normalize_mult) (simp add: normalize_const_poly)
  3489   finally show ?thesis .
  3490 qed
  3491 
  3492 inductive eucl_rel_poly :: "'a::field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<times> 'a poly \<Rightarrow> bool"
  3493   where
  3494     eucl_rel_poly_by0: "eucl_rel_poly x 0 (0, x)"
  3495   | eucl_rel_poly_dividesI: "y \<noteq> 0 \<Longrightarrow> x = q * y \<Longrightarrow> eucl_rel_poly x y (q, 0)"
  3496   | eucl_rel_poly_remainderI:
  3497       "y \<noteq> 0 \<Longrightarrow> degree r < degree y \<Longrightarrow> x = q * y + r \<Longrightarrow> eucl_rel_poly x y (q, r)"
  3498 
  3499 lemma eucl_rel_poly_iff:
  3500   "eucl_rel_poly x y (q, r) \<longleftrightarrow>
  3501     x = q * y + r \<and> (if y = 0 then q = 0 else r = 0 \<or> degree r < degree y)"
  3502   by (auto elim: eucl_rel_poly.cases
  3503       intro: eucl_rel_poly_by0 eucl_rel_poly_dividesI eucl_rel_poly_remainderI)
  3504 
  3505 lemma eucl_rel_poly_0: "eucl_rel_poly 0 y (0, 0)"
  3506   by (simp add: eucl_rel_poly_iff)
  3507 
  3508 lemma eucl_rel_poly_by_0: "eucl_rel_poly x 0 (0, x)"
  3509   by (simp add: eucl_rel_poly_iff)
  3510 
  3511 lemma eucl_rel_poly_pCons:
  3512   assumes rel: "eucl_rel_poly x y (q, r)"
  3513   assumes y: "y \<noteq> 0"
  3514   assumes b: "b = coeff (pCons a r) (degree y) / coeff y (degree y)"
  3515   shows "eucl_rel_poly (pCons a x) y (pCons b q, pCons a r - smult b y)"
  3516     (is "eucl_rel_poly ?x y (?q, ?r)")
  3517 proof -
  3518   from assms have x: "x = q * y + r" and r: "r = 0 \<or> degree r < degree y"
  3519     by (simp_all add: eucl_rel_poly_iff)
  3520   from b x have "?x = ?q * y + ?r" by simp
  3521   moreover
  3522   have "?r = 0 \<or> degree ?r < degree y"
  3523   proof (rule eq_zero_or_degree_less)
  3524     show "degree ?r \<le> degree y"
  3525     proof (rule degree_diff_le)
  3526       from r show "degree (pCons a r) \<le> degree y"
  3527         by auto
  3528       show "degree (smult b y) \<le> degree y"
  3529         by (rule degree_smult_le)
  3530     qed
  3531     from \<open>y \<noteq> 0\<close> show "coeff ?r (degree y) = 0"
  3532       by (simp add: b)
  3533   qed
  3534   ultimately show ?thesis
  3535     unfolding eucl_rel_poly_iff using \<open>y \<noteq> 0\<close> by simp
  3536 qed
  3537 
  3538 lemma eucl_rel_poly_exists: "\<exists>q r. eucl_rel_poly x y (q, r)"
  3539   apply (cases "y = 0")
  3540    apply (fast intro!: eucl_rel_poly_by_0)
  3541   apply (induct x)
  3542    apply (fast intro!: eucl_rel_poly_0)
  3543   apply (fast intro!: eucl_rel_poly_pCons)
  3544   done
  3545 
  3546 lemma eucl_rel_poly_unique:
  3547   assumes 1: "eucl_rel_poly x y (q1, r1)"
  3548   assumes 2: "eucl_rel_poly x y (q2, r2)"
  3549   shows "q1 = q2 \<and> r1 = r2"
  3550 proof (cases "y = 0")
  3551   assume "y = 0"
  3552   with assms show ?thesis
  3553     by (simp add: eucl_rel_poly_iff)
  3554 next
  3555   assume [simp]: "y \<noteq> 0"
  3556   from 1 have q1: "x = q1 * y + r1" and r1: "r1 = 0 \<or> degree r1 < degree y"
  3557     unfolding eucl_rel_poly_iff by simp_all
  3558   from 2 have q2: "x = q2 * y + r2" and r2: "r2 = 0 \<or> degree r2 < degree y"
  3559     unfolding eucl_rel_poly_iff by simp_all
  3560   from q1 q2 have q3: "(q1 - q2) * y = r2 - r1"
  3561     by (simp add: algebra_simps)
  3562   from r1 r2 have r3: "(r2 - r1) = 0 \<or> degree (r2 - r1) < degree y"
  3563     by (auto intro: degree_diff_less)
  3564   show "q1 = q2 \<and> r1 = r2"
  3565   proof (rule classical)
  3566     assume "\<not> ?thesis"
  3567     with q3 have "q1 \<noteq> q2" and "r1 \<noteq> r2" by auto
  3568     with r3 have "degree (r2 - r1) < degree y" by simp
  3569     also have "degree y \<le> degree (q1 - q2) + degree y" by simp
  3570     also from \<open>q1 \<noteq> q2\<close> have "\<dots> = degree ((q1 - q2) * y)"
  3571       by (simp add: degree_mult_eq)
  3572     also from q3 have "\<dots> = degree (r2 - r1)"
  3573       by simp
  3574     finally have "degree (r2 - r1) < degree (r2 - r1)" .
  3575     then show ?thesis by simp
  3576   qed
  3577 qed
  3578 
  3579 lemma eucl_rel_poly_0_iff: "eucl_rel_poly 0 y (q, r) \<longleftrightarrow> q = 0 \<and> r = 0"
  3580   by (auto dest: eucl_rel_poly_unique intro: eucl_rel_poly_0)
  3581 
  3582 lemma eucl_rel_poly_by_0_iff: "eucl_rel_poly x 0 (q, r) \<longleftrightarrow> q = 0 \<and> r = x"
  3583   by (auto dest: eucl_rel_poly_unique intro: eucl_rel_poly_by_0)
  3584 
  3585 lemmas eucl_rel_poly_unique_div = eucl_rel_poly_unique [THEN conjunct1]
  3586 
  3587 lemmas eucl_rel_poly_unique_mod = eucl_rel_poly_unique [THEN conjunct2]
  3588 
  3589 instantiation poly :: (field) semidom_modulo
  3590 begin
  3591 
  3592 definition modulo_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
  3593   where mod_poly_def: "f mod g =
  3594     (if g = 0 then f else pseudo_mod (smult ((1 / lead_coeff g) ^ (Suc (degree f) - degree g)) f) g)"
  3595 
  3596 instance
  3597 proof
  3598   fix x y :: "'a poly"
  3599   show "x div y * y + x mod y = x"
  3600   proof (cases "y = 0")
  3601     case True
  3602     then show ?thesis
  3603       by (simp add: divide_poly_0 mod_poly_def)
  3604   next
  3605     case False
  3606     then have "pseudo_divmod (smult ((1 / lead_coeff y) ^ (Suc (degree x) - degree y)) x) y =
  3607         (x div y, x mod y)"
  3608       by (simp add: divide_poly_field mod_poly_def pseudo_mod_def)
  3609     with False pseudo_divmod [OF False this] show ?thesis
  3610       by (simp add: power_mult_distrib [symmetric] ac_simps)
  3611   qed
  3612 qed
  3613 
  3614 end
  3615 
  3616 lemma eucl_rel_poly: "eucl_rel_poly x y (x div y, x mod y)"
  3617   unfolding eucl_rel_poly_iff
  3618 proof
  3619   show "x = x div y * y + x mod y"
  3620     by (simp add: div_mult_mod_eq)
  3621   show "if y = 0 then x div y = 0 else x mod y = 0 \<or> degree (x mod y) < degree y"
  3622   proof (cases "y = 0")
  3623     case True
  3624     then show ?thesis by auto
  3625   next
  3626     case False
  3627     with pseudo_mod[OF this] show ?thesis
  3628       by (simp add: mod_poly_def)
  3629   qed
  3630 qed
  3631 
  3632 lemma div_poly_eq: "eucl_rel_poly x y (q, r) \<Longrightarrow> x div y = q"
  3633   for x :: "'a::field poly"
  3634   by (rule eucl_rel_poly_unique_div [OF eucl_rel_poly])
  3635 
  3636 lemma mod_poly_eq: "eucl_rel_poly x y (q, r) \<Longrightarrow> x mod y = r"
  3637   for x :: "'a::field poly"
  3638   by (rule eucl_rel_poly_unique_mod [OF eucl_rel_poly])
  3639 
  3640 instance poly :: (field) idom_modulo ..
  3641 
  3642 lemma div_pCons_eq:
  3643   "pCons a p div q =
  3644     (if q = 0 then 0
  3645      else pCons (coeff (pCons a (p mod q)) (degree q) / lead_coeff q) (p div q))"
  3646   using eucl_rel_poly_pCons [OF eucl_rel_poly _ refl, of q a p]
  3647   by (auto intro: div_poly_eq)
  3648 
  3649 lemma mod_pCons_eq:
  3650   "pCons a p mod q =
  3651     (if q = 0 then pCons a p
  3652      else pCons a (p mod q) - smult (coeff (pCons a (p mod q)) (degree q) / lead_coeff q) q)"
  3653   using eucl_rel_poly_pCons [OF eucl_rel_poly _ refl, of q a p]
  3654   by (auto intro: mod_poly_eq)
  3655 
  3656 lemma div_mod_fold_coeffs:
  3657   "(p div q, p mod q) =
  3658     (if q = 0 then (0, p)
  3659      else
  3660       fold_coeffs
  3661         (\<lambda>a (s, r).
  3662           let b = coeff (pCons a r) (degree q) / coeff q (degree q)
  3663           in (pCons b s, pCons a r - smult b q)) p (0, 0))"
  3664   by (rule sym, induct p) (auto simp: div_pCons_eq mod_pCons_eq Let_def)
  3665 
  3666 lemma degree_mod_less: "y \<noteq> 0 \<Longrightarrow> x mod y = 0 \<or> degree (x mod y) < degree y"
  3667   using eucl_rel_poly [of x y] unfolding eucl_rel_poly_iff by simp
  3668 
  3669 lemma degree_mod_less': "b \<noteq> 0 \<Longrightarrow> a mod b \<noteq> 0 \<Longrightarrow> degree (a mod b) < degree b"
  3670   using degree_mod_less[of b a] by auto
  3671 
  3672 lemma div_poly_less:
  3673   fixes x :: "'a::field poly"
  3674   assumes "degree x < degree y"
  3675   shows "x div y = 0"
  3676 proof -
  3677   from assms have "eucl_rel_poly x y (0, x)"
  3678     by (simp add: eucl_rel_poly_iff)
  3679   then show "x div y = 0"
  3680     by (rule div_poly_eq)
  3681 qed
  3682 
  3683 lemma mod_poly_less:
  3684   assumes "degree x < degree y"
  3685   shows "x mod y = x"
  3686 proof -
  3687   from assms have "eucl_rel_poly x y (0, x)"
  3688     by (simp add: eucl_rel_poly_iff)
  3689   then show "x mod y = x"
  3690     by (rule mod_poly_eq)
  3691 qed
  3692 
  3693 lemma eucl_rel_poly_smult_left:
  3694   "eucl_rel_poly x y (q, r) \<Longrightarrow> eucl_rel_poly (smult a x) y (smult a q, smult a r)"
  3695   by (simp add: eucl_rel_poly_iff smult_add_right)
  3696 
  3697 lemma div_smult_left: "(smult a x) div y = smult a (x div y)"
  3698   for x y :: "'a::field poly"
  3699   by (rule div_poly_eq, rule eucl_rel_poly_smult_left, rule eucl_rel_poly)
  3700 
  3701 lemma mod_smult_left: "(smult a x) mod y = smult a (x mod y)"
  3702   by (rule mod_poly_eq, rule eucl_rel_poly_smult_left, rule eucl_rel_poly)
  3703 
  3704 lemma poly_div_minus_left [simp]: "(- x) div y = - (x div y)"
  3705   for x y :: "'a::field poly"
  3706   using div_smult_left [of "- 1::'a"] by simp
  3707 
  3708 lemma poly_mod_minus_left [simp]: "(- x) mod y = - (x mod y)"
  3709   for x y :: "'a::field poly"
  3710   using mod_smult_left [of "- 1::'a"] by simp
  3711 
  3712 lemma eucl_rel_poly_add_left:
  3713   assumes "eucl_rel_poly x y (q, r)"
  3714   assumes "eucl_rel_poly x' y (q', r')"
  3715   shows "eucl_rel_poly (x + x') y (q + q', r + r')"
  3716   using assms unfolding eucl_rel_poly_iff
  3717   by (auto simp: algebra_simps degree_add_less)
  3718 
  3719 lemma poly_div_add_left: "(x + y) div z = x div z + y div z"
  3720   for x y z :: "'a::field poly"
  3721   using eucl_rel_poly_add_left [OF eucl_rel_poly eucl_rel_poly]
  3722   by (rule div_poly_eq)
  3723 
  3724 lemma poly_mod_add_left: "(x + y) mod z = x mod z + y mod z"
  3725   for x y z :: "'a::field poly"
  3726   using eucl_rel_poly_add_left [OF eucl_rel_poly eucl_rel_poly]
  3727   by (rule mod_poly_eq)
  3728 
  3729 lemma poly_div_diff_left: "(x - y) div z = x div z - y div z"
  3730   for x y z :: "'a::field poly"
  3731   by (simp only: diff_conv_add_uminus poly_div_add_left poly_div_minus_left)
  3732 
  3733 lemma poly_mod_diff_left: "(x - y) mod z = x mod z - y mod z"
  3734   for x y z :: "'a::field poly"
  3735   by (simp only: diff_conv_add_uminus poly_mod_add_left poly_mod_minus_left)
  3736 
  3737 lemma eucl_rel_poly_smult_right:
  3738   "a \<noteq> 0 \<Longrightarrow> eucl_rel_poly x y (q, r) \<Longrightarrow> eucl_rel_poly x (smult a y) (smult (inverse a) q, r)"
  3739   by (simp add: eucl_rel_poly_iff)
  3740 
  3741 lemma div_smult_right: "a \<noteq> 0 \<Longrightarrow> x div (smult a y) = smult (inverse a) (x div y)"
  3742   for x y :: "'a::field poly"
  3743   by (rule div_poly_eq, erule eucl_rel_poly_smult_right, rule eucl_rel_poly)
  3744 
  3745 lemma mod_smult_right: "a \<noteq> 0 \<Longrightarrow> x mod (smult a y) = x mod y"
  3746   by (rule mod_poly_eq, erule eucl_rel_poly_smult_right, rule eucl_rel_poly)
  3747 
  3748 lemma poly_div_minus_right [simp]: "x div (- y) = - (x div y)"
  3749   for x y :: "'a::field poly"
  3750   using div_smult_right [of "- 1::'a"] by (simp add: nonzero_inverse_minus_eq)
  3751 
  3752 lemma poly_mod_minus_right [simp]: "x mod (- y) = x mod y"
  3753   for x y :: "'a::field poly"
  3754   using mod_smult_right [of "- 1::'a"] by simp
  3755 
  3756 lemma eucl_rel_poly_mult:
  3757   "eucl_rel_poly x y (q, r) \<Longrightarrow> eucl_rel_poly q z (q', r') \<Longrightarrow>
  3758     eucl_rel_poly x (y * z) (q', y * r' + r)"
  3759   apply (cases "z = 0", simp add: eucl_rel_poly_iff)
  3760   apply (cases "y = 0", simp add: eucl_rel_poly_by_0_iff eucl_rel_poly_0_iff)
  3761   apply (cases "r = 0")
  3762    apply (cases "r' = 0")
  3763     apply (simp add: eucl_rel_poly_iff)
  3764    apply (simp add: eucl_rel_poly_iff field_simps degree_mult_eq)
  3765   apply (cases "r' = 0")
  3766    apply (simp add: eucl_rel_poly_iff degree_mult_eq)
  3767   apply (simp add: eucl_rel_poly_iff field_simps)
  3768   apply (simp add: degree_mult_eq degree_add_less)
  3769   done
  3770 
  3771 lemma poly_div_mult_right: "x div (y * z) = (x div y) div z"
  3772   for x y z :: "'a::field poly"
  3773   by (rule div_poly_eq, rule eucl_rel_poly_mult, (rule eucl_rel_poly)+)
  3774 
  3775 lemma poly_mod_mult_right: "x mod (y * z) = y * (x div y mod z) + x mod y"
  3776   for x y z :: "'a::field poly"
  3777   by (rule mod_poly_eq, rule eucl_rel_poly_mult, (rule eucl_rel_poly)+)
  3778 
  3779 lemma mod_pCons:
  3780   fixes a :: "'a::field"
  3781     and x y :: "'a::field poly"
  3782   assumes y: "y \<noteq> 0"
  3783   defines "b \<equiv> coeff (pCons a (x mod y)) (degree y) / coeff y (degree y)"
  3784   shows "(pCons a x) mod y = pCons a (x mod y) - smult b y"
  3785   unfolding b_def
  3786   by (rule mod_poly_eq, rule eucl_rel_poly_pCons [OF eucl_rel_poly y refl])
  3787 
  3788 
  3789 subsubsection \<open>List-based versions for fast implementation\<close>
  3790 (* Subsection by:
  3791       Sebastiaan Joosten
  3792       René Thiemann
  3793       Akihisa Yamada
  3794     *)
  3795 fun minus_poly_rev_list :: "'a :: group_add list \<Rightarrow> 'a list \<Rightarrow> 'a list"
  3796   where
  3797     "minus_poly_rev_list (x # xs) (y # ys) = (x - y) # (minus_poly_rev_list xs ys)"
  3798   | "minus_poly_rev_list xs [] = xs"
  3799   | "minus_poly_rev_list [] (y # ys) = []"
  3800 
  3801 fun pseudo_divmod_main_list ::
  3802   "'a::comm_ring_1 \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> nat \<Rightarrow> 'a list \<times> 'a list"
  3803   where
  3804     "pseudo_divmod_main_list lc q r d (Suc n) =
  3805       (let
  3806         rr = map (op * lc) r;
  3807         a = hd r;
  3808         qqq = cCons a (map (op * lc) q);
  3809         rrr = tl (if a = 0 then rr else minus_poly_rev_list rr (map (op * a) d))
  3810        in pseudo_divmod_main_list lc qqq rrr d n)"
  3811   | "pseudo_divmod_main_list lc q r d 0 = (q, r)"
  3812 
  3813 fun pseudo_mod_main_list :: "'a::comm_ring_1 \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> nat \<Rightarrow> 'a list"
  3814   where
  3815     "pseudo_mod_main_list lc r d (Suc n) =
  3816       (let
  3817         rr = map (op * lc) r;
  3818         a = hd r;
  3819         rrr = tl (if a = 0 then rr else minus_poly_rev_list rr (map (op * a) d))
  3820        in pseudo_mod_main_list lc rrr d n)"
  3821   | "pseudo_mod_main_list lc r d 0 = r"
  3822 
  3823 
  3824 fun divmod_poly_one_main_list ::
  3825     "'a::comm_ring_1 list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> nat \<Rightarrow> 'a list \<times> 'a list"
  3826   where
  3827     "divmod_poly_one_main_list q r d (Suc n) =
  3828       (let
  3829         a = hd r;
  3830         qqq = cCons a q;
  3831         rr = tl (if a = 0 then r else minus_poly_rev_list r (map (op * a) d))
  3832        in divmod_poly_one_main_list qqq rr d n)"
  3833   | "divmod_poly_one_main_list q r d 0 = (q, r)"
  3834 
  3835 fun mod_poly_one_main_list :: "'a::comm_ring_1 list \<Rightarrow> 'a list \<Rightarrow> nat \<Rightarrow> 'a list"
  3836   where
  3837     "mod_poly_one_main_list r d (Suc n) =
  3838       (let
  3839         a = hd r;
  3840         rr = tl (if a = 0 then r else minus_poly_rev_list r (map (op * a) d))
  3841        in mod_poly_one_main_list rr d n)"
  3842   | "mod_poly_one_main_list r d 0 = r"
  3843 
  3844 definition pseudo_divmod_list :: "'a::comm_ring_1 list \<Rightarrow> 'a list \<Rightarrow> 'a list \<times> 'a list"
  3845   where "pseudo_divmod_list p q =
  3846     (if q = [] then ([], p)
  3847      else
  3848       (let rq = rev q;
  3849         (qu,re) = pseudo_divmod_main_list (hd rq) [] (rev p) rq (1 + length p - length q)
  3850        in (qu, rev re)))"
  3851 
  3852 definition pseudo_mod_list :: "'a::comm_ring_1 list \<Rightarrow> 'a list \<Rightarrow> 'a list"
  3853   where "pseudo_mod_list p q =
  3854     (if q = [] then p
  3855      else
  3856       (let
  3857         rq = rev q;
  3858         re = pseudo_mod_main_list (hd rq) (rev p) rq (1 + length p - length q)
  3859        in rev re))"
  3860 
  3861 lemma minus_zero_does_nothing: "minus_poly_rev_list x (map (op * 0) y) = x"
  3862   for x :: "'a::ring list"
  3863   by (induct x y rule: minus_poly_rev_list.induct) auto
  3864 
  3865 lemma length_minus_poly_rev_list [simp]: "length (minus_poly_rev_list xs ys) = length xs"
  3866   by (induct xs ys rule: minus_poly_rev_list.induct) auto
  3867 
  3868 lemma if_0_minus_poly_rev_list:
  3869   "(if a = 0 then x else minus_poly_rev_list x (map (op * a) y)) =
  3870     minus_poly_rev_list x (map (op * a) y)"
  3871   for a :: "'a::ring"
  3872   by(cases "a = 0") (simp_all add: minus_zero_does_nothing)
  3873 
  3874 lemma Poly_append: "Poly (a @ b) = Poly a + monom 1 (length a) * Poly b"
  3875   for a :: "'a::comm_semiring_1 list"
  3876   by (induct a) (auto simp: monom_0 monom_Suc)
  3877 
  3878 lemma minus_poly_rev_list: "length p \<ge> length q \<Longrightarrow>
  3879   Poly (rev (minus_poly_rev_list (rev p) (rev q))) =
  3880     Poly p - monom 1 (length p - length q) * Poly q"
  3881   for p q :: "'a :: comm_ring_1 list"
  3882 proof (induct "rev p" "rev q" arbitrary: p q rule: minus_poly_rev_list.induct)
  3883   case (1 x xs y ys)
  3884   then have "length (rev q) \<le> length (rev p)"
  3885     by simp
  3886   from this[folded 1(2,3)] have ys_xs: "length ys \<le> length xs"
  3887     by simp
  3888   then have *: "Poly (rev (minus_poly_rev_list xs ys)) =
  3889       Poly (rev xs) - monom 1 (length xs - length ys) * Poly (rev ys)"
  3890     by (subst "1.hyps"(1)[of "rev xs" "rev ys", unfolded rev_rev_ident length_rev]) auto
  3891   have "Poly p - monom 1 (length p - length q) * Poly q =
  3892     Poly (rev (rev p)) - monom 1 (length (rev (rev p)) - length (rev (rev q))) * Poly (rev (rev q))"
  3893     by simp
  3894   also have "\<dots> =
  3895       Poly (rev (x # xs)) - monom 1 (length (x # xs) - length (y # ys)) * Poly (rev (y # ys))"
  3896     unfolding 1(2,3) by simp
  3897   also from ys_xs have "\<dots> =
  3898     Poly (rev xs) + monom x (length xs) -
  3899       (monom 1 (length xs - length ys) * Poly (rev ys) + monom y (length xs))"
  3900     by (simp add: Poly_append distrib_left mult_monom smult_monom)
  3901   also have "\<dots> = Poly (rev (minus_poly_rev_list xs ys)) + monom (x - y) (length xs)"
  3902     unfolding * diff_monom[symmetric] by simp
  3903   finally show ?case
  3904     by (simp add: 1(2,3)[symmetric] smult_monom Poly_append)
  3905 qed auto
  3906 
  3907 lemma smult_monom_mult: "smult a (monom b n * f) = monom (a * b) n * f"
  3908   using smult_monom [of a _ n] by (metis mult_smult_left)
  3909 
  3910 lemma head_minus_poly_rev_list:
  3911   "length d \<le> length r \<Longrightarrow> d \<noteq> [] \<Longrightarrow>
  3912     hd (minus_poly_rev_list (map (op * (last d)) r) (map (op * (hd r)) (rev d))) = 0"
  3913   for d r :: "'a::comm_ring list"
  3914 proof (induct r)
  3915   case Nil
  3916   then show ?case by simp
  3917 next
  3918   case (Cons a rs)
  3919   then show ?case by (cases "rev d") (simp_all add: ac_simps)
  3920 qed
  3921 
  3922 lemma Poly_map: "Poly (map (op * a) p) = smult a (Poly p)"
  3923 proof (induct p)
  3924   case Nil
  3925   then show ?case by simp
  3926 next
  3927   case (Cons x xs)
  3928   then show ?case by (cases "Poly xs = 0") auto
  3929 qed
  3930 
  3931 lemma last_coeff_is_hd: "xs \<noteq> [] \<Longrightarrow> coeff (Poly xs) (length xs - 1) = hd (rev xs)"
  3932   by (simp_all add: hd_conv_nth rev_nth nth_default_nth nth_append)
  3933 
  3934 lemma pseudo_divmod_main_list_invar:
  3935   assumes leading_nonzero: "last d \<noteq> 0"
  3936     and lc: "last d = lc"
  3937     and "d \<noteq> []"
  3938     and "pseudo_divmod_main_list lc q (rev r) (rev d) n = (q', rev r')"
  3939     and "n = 1 + length r - length d"
  3940   shows "pseudo_divmod_main lc (monom 1 n * Poly q) (Poly r) (Poly d) (length r - 1) n =
  3941     (Poly q', Poly r')"
  3942   using assms(4-)
  3943 proof (induct n arbitrary: r q)
  3944   case (Suc n)
  3945   from Suc.prems have *: "\<not> Suc (length r) \<le> length d"
  3946     by simp
  3947   with \<open>d \<noteq> []\<close> have "r \<noteq> []"
  3948     using Suc_leI length_greater_0_conv list.size(3) by fastforce
  3949   let ?a = "(hd (rev r))"
  3950   let ?rr = "map (op * lc) (rev r)"
  3951   let ?rrr = "rev (tl (minus_poly_rev_list ?rr (map (op * ?a) (rev d))))"
  3952   let ?qq = "cCons ?a (map (op * lc) q)"
  3953   from * Suc(3) have n: "n = (1 + length r - length d - 1)"
  3954     by simp
  3955   from * have rr_val:"(length ?rrr) = (length r - 1)"
  3956     by auto
  3957   with \<open>r \<noteq> []\<close> * have rr_smaller: "(1 + length r - length d - 1) = (1 + length ?rrr - length d)"
  3958     by auto
  3959   from * have id: "Suc (length r) - length d = Suc (length r - length d)"
  3960     by auto
  3961   from Suc.prems *
  3962   have "pseudo_divmod_main_list lc ?qq (rev ?rrr) (rev d) (1 + length r - length d - 1) = (q', rev r')"
  3963     by (simp add: Let_def if_0_minus_poly_rev_list id)
  3964   with n have v: "pseudo_divmod_main_list lc ?qq (rev ?rrr) (rev d) n = (q', rev r')"
  3965     by auto
  3966   from * have sucrr:"Suc (length r) - length d = Suc (length r - length d)"
  3967     using Suc_diff_le not_less_eq_eq by blast
  3968   from Suc(3) \<open>r \<noteq> []\<close> have n_ok : "n = 1 + (length ?rrr) - length d"
  3969     by simp
  3970   have cong: "\<And>x1 x2 x3 x4 y1 y2 y3 y4. x1 = y1 \<Longrightarrow> x2 = y2 \<Longrightarrow> x3 = y3 \<Longrightarrow> x4 = y4 \<Longrightarrow>
  3971       pseudo_divmod_main lc x1 x2 x3 x4 n = pseudo_divmod_main lc y1 y2 y3 y4 n"
  3972     by simp
  3973   have hd_rev: "coeff (Poly r) (length r - Suc 0) = hd (rev r)"
  3974     using last_coeff_is_hd[OF \<open>r \<noteq> []\<close>] by simp
  3975   show ?case
  3976     unfolding Suc.hyps(1)[OF v n_ok, symmetric] pseudo_divmod_main.simps Let_def
  3977   proof (rule cong[OF _ _ refl], goal_cases)
  3978     case 1
  3979     show ?case
  3980       by (simp add: monom_Suc hd_rev[symmetric] smult_monom Poly_map)
  3981   next
  3982     case 2
  3983     show ?case
  3984     proof (subst Poly_on_rev_starting_with_0, goal_cases)
  3985       show "hd (minus_poly_rev_list (map (op * lc) (rev r)) (map (op * (hd (rev r))) (rev d))) = 0"
  3986         by (fold lc, subst head_minus_poly_rev_list, insert * \<open>d \<noteq> []\<close>, auto)
  3987       from * have "length d \<le> length r"
  3988         by simp
  3989       then show "smult lc (Poly r) - monom (coeff (Poly r) (length r - 1)) n * Poly d =
  3990           Poly (rev (minus_poly_rev_list (map (op * lc) (rev r)) (map (op * (hd (rev r))) (rev d))))"
  3991         by (fold rev_map) (auto simp add: n smult_monom_mult Poly_map hd_rev [symmetric]
  3992             minus_poly_rev_list)
  3993     qed
  3994   qed simp
  3995 qed simp
  3996 
  3997 lemma pseudo_divmod_impl [code]:
  3998   "pseudo_divmod f g = map_prod poly_of_list poly_of_list (pseudo_divmod_list (coeffs f) (coeffs g))"
  3999     for f g :: "'a::comm_ring_1 poly"
  4000 proof (cases "g = 0")
  4001   case False
  4002   then have "last (coeffs g) \<noteq> 0"
  4003     and "last (coeffs g) = lead_coeff g"
  4004     and "coeffs g \<noteq> []"
  4005     by (simp_all add: last_coeffs_eq_coeff_degree)
  4006   moreover obtain q r where qr: "pseudo_divmod_main_list
  4007     (last (coeffs g)) (rev [])
  4008     (rev (coeffs f)) (rev (coeffs g))
  4009     (1 + length (coeffs f) -
  4010     length (coeffs g)) = (q, rev (rev r))"
  4011     by force
  4012   ultimately have "(Poly q, Poly (rev r)) = pseudo_divmod_main (lead_coeff g) 0 f g
  4013     (length (coeffs f) - Suc 0) (Suc (length (coeffs f)) - length (coeffs g))"
  4014     by (subst pseudo_divmod_main_list_invar [symmetric]) auto
  4015   moreover have "pseudo_divmod_main_list
  4016     (hd (rev (coeffs g))) []
  4017     (rev (coeffs f)) (rev (coeffs g))
  4018     (1 + length (coeffs f) -
  4019     length (coeffs g)) = (q, r)"
  4020     using qr hd_rev [OF \<open>coeffs g \<noteq> []\<close>] by simp
  4021   ultimately show ?thesis
  4022     by (auto simp: degree_eq_length_coeffs pseudo_divmod_def pseudo_divmod_list_def Let_def)
  4023 next
  4024   case True
  4025   then show ?thesis
  4026     by (auto simp add: pseudo_divmod_def pseudo_divmod_list_def)
  4027 qed
  4028 
  4029 lemma pseudo_mod_main_list:
  4030   "snd (pseudo_divmod_main_list l q xs ys n) = pseudo_mod_main_list l xs ys n"
  4031   by (induct n arbitrary: l q xs ys) (auto simp: Let_def)
  4032 
  4033 lemma pseudo_mod_impl[code]: "pseudo_mod f g = poly_of_list (pseudo_mod_list (coeffs f) (coeffs g))"
  4034 proof -
  4035   have snd_case: "\<And>f g p. snd ((\<lambda>(x,y). (f x, g y)) p) = g (snd p)"
  4036     by auto
  4037   show ?thesis
  4038     unfolding pseudo_mod_def pseudo_divmod_impl pseudo_divmod_list_def
  4039       pseudo_mod_list_def Let_def
  4040     by (simp add: snd_case pseudo_mod_main_list)
  4041 qed
  4042 
  4043 
  4044 subsubsection \<open>Improved Code-Equations for Polynomial (Pseudo) Division\<close>
  4045 
  4046 lemma pdivmod_pdivmodrel: "eucl_rel_poly p q (r, s) \<longleftrightarrow> (p div q, p mod q) = (r, s)"
  4047   by (metis eucl_rel_poly eucl_rel_poly_unique)
  4048 
  4049 lemma pdivmod_via_pseudo_divmod:
  4050   "(f div g, f mod g) =
  4051     (if g = 0 then (0, f)
  4052      else
  4053       let
  4054         ilc = inverse (coeff g (degree g));
  4055         h = smult ilc g;
  4056         (q,r) = pseudo_divmod f h
  4057       in (smult ilc q, r))"
  4058   (is "?l = ?r")
  4059 proof (cases "g = 0")
  4060   case True
  4061   then show ?thesis by simp
  4062 next
  4063   case False
  4064   define lc where "lc = inverse (coeff g (degree g))"
  4065   define h where "h = smult lc g"
  4066   from False have h1: "coeff h (degree h) = 1" and lc: "lc \<noteq> 0"
  4067     by (auto simp: h_def lc_def)
  4068   then have h0: "h \<noteq> 0"
  4069     by auto
  4070   obtain q r where p: "pseudo_divmod f h = (q, r)"
  4071     by force
  4072   from False have id: "?r = (smult lc q, r)"
  4073     by (auto simp: Let_def h_def[symmetric] lc_def[symmetric] p)
  4074   from pseudo_divmod[OF h0 p, unfolded h1]
  4075   have f: "f = h * q + r" and r: "r = 0 \<or> degree r < degree h"
  4076     by auto
  4077   from f r h0 have "eucl_rel_poly f h (q, r)"
  4078     by (auto simp: eucl_rel_poly_iff)
  4079   then have "(f div h, f mod h) = (q, r)"
  4080     by (simp add: pdivmod_pdivmodrel)
  4081   with lc have "(f div g, f mod g) = (smult lc q, r)"
  4082     by (auto simp: h_def div_smult_right[OF lc] mod_smult_right[OF lc])
  4083   with id show ?thesis
  4084     by auto
  4085 qed
  4086 
  4087 lemma pdivmod_via_pseudo_divmod_list:
  4088   "(f div g, f mod g) =
  4089     (let cg = coeffs g in
  4090       if cg = [] then (0, f)
  4091       else
  4092         let
  4093           cf = coeffs f;
  4094           ilc = inverse (last cg);
  4095           ch = map (op * ilc) cg;
  4096           (q, r) = pseudo_divmod_main_list 1 [] (rev cf) (rev ch) (1 + length cf - length cg)
  4097         in (poly_of_list (map (op * ilc) q), poly_of_list (rev r)))"
  4098 proof -
  4099   note d = pdivmod_via_pseudo_divmod pseudo_divmod_impl pseudo_divmod_list_def
  4100   show ?thesis
  4101   proof (cases "g = 0")
  4102     case True
  4103     with d show ?thesis by auto
  4104   next
  4105     case False
  4106     define ilc where "ilc = inverse (coeff g (degree g))"
  4107     from False have ilc: "ilc \<noteq> 0"
  4108       by (auto simp: ilc_def)
  4109     with False have id: "g = 0 \<longleftrightarrow> False" "coeffs g = [] \<longleftrightarrow> False"
  4110       "last (coeffs g) = coeff g (degree g)"
  4111       "coeffs (smult ilc g) = [] \<longleftrightarrow> False"
  4112       by (auto simp: last_coeffs_eq_coeff_degree)
  4113     have id2: "hd (rev (coeffs (smult ilc g))) = 1"
  4114       by (subst hd_rev, insert id ilc, auto simp: coeffs_smult, subst last_map, auto simp: id ilc_def)
  4115     have id3: "length (coeffs (smult ilc g)) = length (coeffs g)"
  4116       "rev (coeffs (smult ilc g)) = rev (map (op * ilc) (coeffs g))"
  4117       unfolding coeffs_smult using ilc by auto
  4118     obtain q r where pair:
  4119       "pseudo_divmod_main_list 1 [] (rev (coeffs f)) (rev (map (op * ilc) (coeffs g)))
  4120         (1 + length (coeffs f) - length (coeffs g)) = (q, r)"
  4121       by force
  4122     show ?thesis
  4123       unfolding d Let_def id if_False ilc_def[symmetric] map_prod_def[symmetric] id2
  4124       unfolding id3 pair map_prod_def split
  4125       by (auto simp: Poly_map)
  4126   qed
  4127 qed
  4128 
  4129 lemma pseudo_divmod_main_list_1: "pseudo_divmod_main_list 1 = divmod_poly_one_main_list"
  4130 proof (intro ext, goal_cases)
  4131   case (1 q r d n)
  4132   have *: "map (op * 1) xs = xs" for xs :: "'a list"
  4133     by (induct xs) auto
  4134   show ?case
  4135     by (induct n arbitrary: q r d) (auto simp: * Let_def)
  4136 qed
  4137 
  4138 fun divide_poly_main_list :: "'a::idom_divide \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> nat \<Rightarrow> 'a list"
  4139   where
  4140     "divide_poly_main_list lc q r d (Suc n) =
  4141       (let
  4142         cr = hd r
  4143         in if cr = 0 then divide_poly_main_list lc (cCons cr q) (tl r) d n else let
  4144         a = cr div lc;
  4145         qq = cCons a q;
  4146         rr = minus_poly_rev_list r (map (op * a) d)
  4147        in if hd rr = 0 then divide_poly_main_list lc qq (tl rr) d n else [])"
  4148   | "divide_poly_main_list lc q r d 0 = q"
  4149 
  4150 lemma divide_poly_main_list_simp [simp]:
  4151   "divide_poly_main_list lc q r d (Suc n) =
  4152     (let
  4153       cr = hd r;
  4154       a = cr div lc;
  4155       qq = cCons a q;
  4156       rr = minus_poly_rev_list r (map (op * a) d)
  4157      in if hd rr = 0 then divide_poly_main_list lc qq (tl rr) d n else [])"
  4158   by (simp add: Let_def minus_zero_does_nothing)
  4159 
  4160 declare divide_poly_main_list.simps(1)[simp del]
  4161 
  4162 definition divide_poly_list :: "'a::idom_divide poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
  4163   where "divide_poly_list f g =
  4164     (let cg = coeffs g in
  4165       if cg = [] then g
  4166       else
  4167         let
  4168           cf = coeffs f;
  4169           cgr = rev cg
  4170         in poly_of_list (divide_poly_main_list (hd cgr) [] (rev cf) cgr (1 + length cf - length cg)))"
  4171 
  4172 lemmas pdivmod_via_divmod_list = pdivmod_via_pseudo_divmod_list[unfolded pseudo_divmod_main_list_1]
  4173 
  4174 lemma mod_poly_one_main_list: "snd (divmod_poly_one_main_list q r d n) = mod_poly_one_main_list r d n"
  4175   by (induct n arbitrary: q r d) (auto simp: Let_def)
  4176 
  4177 lemma mod_poly_code [code]:
  4178   "f mod g =
  4179     (let cg = coeffs g in
  4180       if cg = [] then f
  4181       else
  4182         let
  4183           cf = coeffs f;
  4184           ilc = inverse (last cg);
  4185           ch = map (op * ilc) cg;
  4186           r = mod_poly_one_main_list (rev cf) (rev ch) (1 + length cf - length cg)
  4187         in poly_of_list (rev r))"
  4188   (is "_ = ?rhs")
  4189 proof -
  4190   have "snd (f div g, f mod g) = ?rhs"
  4191     unfolding pdivmod_via_divmod_list Let_def mod_poly_one_main_list [symmetric, of _ _ _ Nil]
  4192     by (auto split: prod.splits)
  4193   then show ?thesis by simp
  4194 qed
  4195 
  4196 definition div_field_poly_impl :: "'a :: field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
  4197   where "div_field_poly_impl f g =
  4198     (let cg = coeffs g in
  4199       if cg = [] then 0
  4200       else
  4201         let
  4202           cf = coeffs f;
  4203           ilc = inverse (last cg);
  4204           ch = map (op * ilc) cg;
  4205           q = fst (divmod_poly_one_main_list [] (rev cf) (rev ch) (1 + length cf - length cg))
  4206         in poly_of_list ((map (op * ilc) q)))"
  4207 
  4208 text \<open>We do not declare the following lemma as code equation, since then polynomial division
  4209   on non-fields will no longer be executable. However, a code-unfold is possible, since
  4210   \<open>div_field_poly_impl\<close> is a bit more efficient than the generic polynomial division.\<close>
  4211 lemma div_field_poly_impl[code_unfold]: "op div = div_field_poly_impl"
  4212 proof (intro ext)
  4213   fix f g :: "'a poly"
  4214   have "fst (f div g, f mod g) = div_field_poly_impl f g"
  4215     unfolding div_field_poly_impl_def pdivmod_via_divmod_list Let_def
  4216     by (auto split: prod.splits)
  4217   then show "f div g =  div_field_poly_impl f g"
  4218     by simp
  4219 qed
  4220 
  4221 lemma divide_poly_main_list:
  4222   assumes lc0: "lc \<noteq> 0"
  4223     and lc: "last d = lc"
  4224     and d: "d \<noteq> []"
  4225     and "n = (1 + length r - length d)"
  4226   shows "Poly (divide_poly_main_list lc q (rev r) (rev d) n) =
  4227     divide_poly_main lc (monom 1 n * Poly q) (Poly r) (Poly d) (length r - 1) n"
  4228   using assms(4-)
  4229 proof (induct "n" arbitrary: r q)
  4230   case (Suc n)
  4231   from Suc.prems have ifCond: "\<not> Suc (length r) \<le> length d"
  4232     by simp
  4233   with d have r: "r \<noteq> []"
  4234     using Suc_leI length_greater_0_conv list.size(3) by fastforce
  4235   then obtain rr lcr where r: "r = rr @ [lcr]"
  4236     by (cases r rule: rev_cases) auto
  4237   from d lc obtain dd where d: "d = dd @ [lc]"
  4238     by (cases d rule: rev_cases) auto
  4239   from Suc(2) ifCond have n: "n = 1 + length rr - length d"
  4240     by (auto simp: r)
  4241   from ifCond have len: "length dd \<le> length rr"
  4242     by (simp add: r d)
  4243   show ?case
  4244   proof (cases "lcr div lc * lc = lcr")
  4245     case False
  4246     with r d show ?thesis
  4247       unfolding Suc(2)[symmetric]
  4248       by (auto simp add: Let_def nth_default_append)
  4249   next
  4250     case True
  4251     with r d have id:
  4252       "?thesis \<longleftrightarrow>
  4253         Poly (divide_poly_main_list lc (cCons (lcr div lc) q)
  4254           (rev (rev (minus_poly_rev_list (rev rr) (rev (map (op * (lcr div lc)) dd))))) (rev d) n) =
  4255           divide_poly_main lc
  4256             (monom 1 (Suc n) * Poly q + monom (lcr div lc) n)
  4257             (Poly r - monom (lcr div lc) n * Poly d)
  4258             (Poly d) (length rr - 1) n"
  4259       by (cases r rule: rev_cases; cases "d" rule: rev_cases)
  4260         (auto simp add: Let_def rev_map nth_default_append)
  4261     have cong: "\<And>x1 x2 x3 x4 y1 y2 y3 y4. x1 = y1 \<Longrightarrow> x2 = y2 \<Longrightarrow> x3 = y3 \<Longrightarrow> x4 = y4 \<Longrightarrow>
  4262         divide_poly_main lc x1 x2 x3 x4 n = divide_poly_main lc y1 y2 y3 y4 n"
  4263       by simp
  4264     show ?thesis
  4265       unfolding id
  4266     proof (subst Suc(1), simp add: n,
  4267         subst minus_poly_rev_list, force simp: len, rule cong[OF _ _ refl], goal_cases)
  4268       case 2
  4269       have "monom lcr (length rr) = monom (lcr div lc) (length rr - length dd) * monom lc (length dd)"
  4270         by (simp add: mult_monom len True)
  4271       then show ?case unfolding r d Poly_append n ring_distribs
  4272         by (auto simp: Poly_map smult_monom smult_monom_mult)
  4273     qed (auto simp: len monom_Suc smult_monom)
  4274   qed
  4275 qed simp
  4276 
  4277 lemma divide_poly_list[code]: "f div g = divide_poly_list f g"
  4278 proof -
  4279   note d = divide_poly_def divide_poly_list_def
  4280   show ?thesis
  4281   proof (cases "g = 0")
  4282     case True
  4283     show ?thesis by (auto simp: d True)
  4284   next
  4285     case False
  4286     then obtain cg lcg where cg: "coeffs g = cg @ [lcg]"
  4287       by (cases "coeffs g" rule: rev_cases) auto
  4288     with False have id: "(g = 0) = False" "(cg @ [lcg] = []) = False"
  4289       by auto
  4290     from cg False have lcg: "coeff g (degree g) = lcg"
  4291       using last_coeffs_eq_coeff_degree last_snoc by force
  4292     with False have "lcg \<noteq> 0" by auto
  4293     from cg Poly_coeffs [of g] have ltp: "Poly (cg @ [lcg]) = g"
  4294       by auto
  4295     show ?thesis
  4296       unfolding d cg Let_def id if_False poly_of_list_def
  4297       by (subst divide_poly_main_list, insert False cg \<open>lcg \<noteq> 0\<close>)
  4298         (auto simp: lcg ltp, simp add: degree_eq_length_coeffs)
  4299   qed
  4300 qed
  4301 
  4302 
  4303 subsection \<open>Primality and irreducibility in polynomial rings\<close>
  4304 
  4305 lemma prod_mset_const_poly: "(\<Prod>x\<in>#A. [:f x:]) = [:prod_mset (image_mset f A):]"
  4306   by (induct A) (simp_all add: ac_simps)
  4307 
  4308 lemma irreducible_const_poly_iff:
  4309   fixes c :: "'a :: {comm_semiring_1,semiring_no_zero_divisors}"
  4310   shows "irreducible [:c:] \<longleftrightarrow> irreducible c"
  4311 proof
  4312   assume A: "irreducible c"
  4313   show "irreducible [:c:]"
  4314   proof (rule irreducibleI)
  4315     fix a b assume ab: "[:c:] = a * b"
  4316     hence "degree [:c:] = degree (a * b)" by (simp only: )
  4317     also from A ab have "a \<noteq> 0" "b \<noteq> 0" by auto
  4318     hence "degree (a * b) = degree a + degree b" by (simp add: degree_mult_eq)
  4319     finally have "degree a = 0" "degree b = 0" by auto
  4320     then obtain a' b' where ab': "a = [:a':]" "b = [:b':]" by (auto elim!: degree_eq_zeroE)
  4321     from ab have "coeff [:c:] 0 = coeff (a * b) 0" by (simp only: )
  4322     hence "c = a' * b'" by (simp add: ab' mult_ac)
  4323     from A and this have "a' dvd 1 \<or> b' dvd 1" by (rule irreducibleD)
  4324     with ab' show "a dvd 1 \<or> b dvd 1"
  4325       by (auto simp add: is_unit_const_poly_iff)
  4326   qed (insert A, auto simp: irreducible_def is_unit_poly_iff)
  4327 next
  4328   assume A: "irreducible [:c:]"
  4329   then have "c \<noteq> 0" and "\<not> c dvd 1"
  4330     by (auto simp add: irreducible_def is_unit_const_poly_iff)
  4331   then show "irreducible c"
  4332   proof (rule irreducibleI)
  4333     fix a b assume ab: "c = a * b"
  4334     hence "[:c:] = [:a:] * [:b:]" by (simp add: mult_ac)
  4335     from A and this have "[:a:] dvd 1 \<or> [:b:] dvd 1" by (rule irreducibleD)
  4336     then show "a dvd 1 \<or> b dvd 1"
  4337       by (auto simp add: is_unit_const_poly_iff)
  4338   qed
  4339 qed
  4340 
  4341 lemma lift_prime_elem_poly:
  4342   assumes "prime_elem (c :: 'a :: semidom)"
  4343   shows   "prime_elem [:c:]"
  4344 proof (rule prime_elemI)
  4345   fix a b assume *: "[:c:] dvd a * b"
  4346   from * have dvd: "c dvd coeff (a * b) n" for n
  4347     by (subst (asm) const_poly_dvd_iff) blast
  4348   {
  4349     define m where "m = (GREATEST m. \<not>c dvd coeff b m)"
  4350     assume "\<not>[:c:] dvd b"
  4351     hence A: "\<exists>i. \<not>c dvd coeff b i" by (subst (asm) const_poly_dvd_iff) blast
  4352     have B: "\<forall>i. \<not>c dvd coeff b i \<longrightarrow> i \<le> degree b"
  4353       by (auto intro: le_degree)
  4354     have coeff_m: "\<not>c dvd coeff b m" unfolding m_def by (rule GreatestI_ex_nat[OF A B])
  4355     have "i \<le> m" if "\<not>c dvd coeff b i" for i
  4356       unfolding m_def by (rule Greatest_le_nat[OF that B])
  4357     hence dvd_b: "c dvd coeff b i" if "i > m" for i using that by force
  4358 
  4359     have "c dvd coeff a i" for i
  4360     proof (induction i rule: nat_descend_induct[of "degree a"])
  4361       case (base i)
  4362       thus ?case by (simp add: coeff_eq_0)
  4363     next
  4364       case (descend i)
  4365       let ?A = "{..i+m} - {i}"
  4366       have "c dvd coeff (a * b) (i + m)" by (rule dvd)
  4367       also have "coeff (a * b) (i + m) = (\<Sum>k\<le>i + m. coeff a k * coeff b (i + m - k))"
  4368         by (simp add: coeff_mult)
  4369       also have "{..i+m} = insert i ?A" by auto
  4370       also have "(\<Sum>k\<in>\<dots>. coeff a k * coeff b (i + m - k)) =
  4371                    coeff a i * coeff b m + (\<Sum>k\<in>?A. coeff a k * coeff b (i + m - k))"
  4372         (is "_ = _ + ?S")
  4373         by (subst sum.insert) simp_all
  4374       finally have eq: "c dvd coeff a i * coeff b m + ?S" .
  4375       moreover have "c dvd ?S"
  4376       proof (rule dvd_sum)
  4377         fix k assume k: "k \<in> {..i+m} - {i}"
  4378         show "c dvd coeff a k * coeff b (i + m - k)"
  4379         proof (cases "k < i")
  4380           case False
  4381           with k have "c dvd coeff a k" by (intro descend.IH) simp
  4382           thus ?thesis by simp
  4383         next
  4384           case True
  4385           hence "c dvd coeff b (i + m - k)" by (intro dvd_b) simp
  4386           thus ?thesis by simp
  4387         qed
  4388       qed
  4389       ultimately have "c dvd coeff a i * coeff b m"
  4390         by (simp add: dvd_add_left_iff)
  4391       with assms coeff_m show "c dvd coeff a i"
  4392         by (simp add: prime_elem_dvd_mult_iff)
  4393     qed
  4394     hence "[:c:] dvd a" by (subst const_poly_dvd_iff) blast
  4395   }
  4396   then show "[:c:] dvd a \<or> [:c:] dvd b" by blast
  4397 next
  4398   from assms show "[:c:] \<noteq> 0" and "\<not> [:c:] dvd 1"
  4399     by (simp_all add: prime_elem_def is_unit_const_poly_iff)
  4400 qed
  4401 
  4402 lemma prime_elem_const_poly_iff:
  4403   fixes c :: "'a :: semidom"
  4404   shows   "prime_elem [:c:] \<longleftrightarrow> prime_elem c"
  4405 proof
  4406   assume A: "prime_elem [:c:]"
  4407   show "prime_elem c"
  4408   proof (rule prime_elemI)
  4409     fix a b assume "c dvd a * b"
  4410     hence "[:c:] dvd [:a:] * [:b:]" by (simp add: mult_ac)
  4411     from A and this have "[:c:] dvd [:a:] \<or> [:c:] dvd [:b:]" by (rule prime_elem_dvd_multD)
  4412     thus "c dvd a \<or> c dvd b" by simp
  4413   qed (insert A, auto simp: prime_elem_def is_unit_poly_iff)
  4414 qed (auto intro: lift_prime_elem_poly)
  4415 
  4416 
  4417 subsection \<open>Content and primitive part of a polynomial\<close>
  4418 
  4419 definition content :: "'a::semiring_gcd poly \<Rightarrow> 'a"
  4420   where "content p = gcd_list (coeffs p)"
  4421 
  4422 lemma content_eq_fold_coeffs [code]: "content p = fold_coeffs gcd p 0"
  4423   by (simp add: content_def Gcd_fin.set_eq_fold fold_coeffs_def foldr_fold fun_eq_iff ac_simps)
  4424 
  4425 lemma content_0 [simp]: "content 0 = 0"
  4426   by (simp add: content_def)
  4427 
  4428 lemma content_1 [simp]: "content 1 = 1"
  4429   by (simp add: content_def)
  4430 
  4431 lemma content_const [simp]: "content [:c:] = normalize c"
  4432   by (simp add: content_def cCons_def)
  4433 
  4434 lemma const_poly_dvd_iff_dvd_content: "[:c:] dvd p \<longleftrightarrow> c dvd content p"
  4435   for c :: "'a::semiring_gcd"
  4436 proof (cases "p = 0")
  4437   case True
  4438   then show ?thesis by simp
  4439 next
  4440   case False
  4441   have "[:c:] dvd p \<longleftrightarrow> (\<forall>n. c dvd coeff p n)"
  4442     by (rule const_poly_dvd_iff)
  4443   also have "\<dots> \<longleftrightarrow> (\<forall>a\<in>set (coeffs p). c dvd a)"
  4444   proof safe
  4445     fix n :: nat
  4446     assume "\<forall>a\<in>set (coeffs p). c dvd a"
  4447     then show "c dvd coeff p n"
  4448       by (cases "n \<le> degree p") (auto simp: coeff_eq_0 coeffs_def split: if_splits)
  4449   qed (auto simp: coeffs_def simp del: upt_Suc split: if_splits)
  4450   also have "\<dots> \<longleftrightarrow> c dvd content p"
  4451     by (simp add: content_def dvd_Gcd_fin_iff dvd_mult_unit_iff)
  4452   finally show ?thesis .
  4453 qed
  4454 
  4455 lemma content_dvd [simp]: "[:content p:] dvd p"
  4456   by (subst const_poly_dvd_iff_dvd_content) simp_all
  4457 
  4458 lemma content_dvd_coeff [simp]: "content p dvd coeff p n"
  4459 proof (cases "p = 0")
  4460   case True
  4461   then show ?thesis
  4462     by simp
  4463 next
  4464   case False
  4465   then show ?thesis
  4466     by (cases "n \<le> degree p")
  4467       (auto simp add: content_def not_le coeff_eq_0 coeff_in_coeffs intro: Gcd_fin_dvd)
  4468 qed
  4469 
  4470 lemma content_dvd_coeffs: "c \<in> set (coeffs p) \<Longrightarrow> content p dvd c"
  4471   by (simp add: content_def Gcd_fin_dvd)
  4472 
  4473 lemma normalize_content [simp]: "normalize (content p) = content p"
  4474   by (simp add: content_def)
  4475 
  4476 lemma is_unit_content_iff [simp]: "is_unit (content p) \<longleftrightarrow> content p = 1"
  4477 proof
  4478   assume "is_unit (content p)"
  4479   then have "normalize (content p) = 1" by (simp add: is_unit_normalize del: normalize_content)
  4480   then show "content p = 1" by simp
  4481 qed auto
  4482 
  4483 lemma content_smult [simp]: "content (smult c p) = normalize c * content p"
  4484   by (simp add: content_def coeffs_smult Gcd_fin_mult)
  4485 
  4486 lemma content_eq_zero_iff [simp]: "content p = 0 \<longleftrightarrow> p = 0"
  4487   by (auto simp: content_def simp: poly_eq_iff coeffs_def)
  4488 
  4489 definition primitive_part :: "'a :: semiring_gcd poly \<Rightarrow> 'a poly"
  4490   where "primitive_part p = map_poly (\<lambda>x. x div content p) p"
  4491 
  4492 lemma primitive_part_0 [simp]: "primitive_part 0 = 0"
  4493   by (simp add: primitive_part_def)
  4494 
  4495 lemma content_times_primitive_part [simp]: "smult (content p) (primitive_part p) = p"
  4496   for p :: "'a :: semiring_gcd poly"
  4497 proof (cases "p = 0")
  4498   case True
  4499   then show ?thesis by simp
  4500 next
  4501   case False
  4502   then show ?thesis
  4503   unfolding primitive_part_def
  4504   by (auto simp: smult_conv_map_poly map_poly_map_poly o_def content_dvd_coeffs
  4505       intro: map_poly_idI)
  4506 qed
  4507 
  4508 lemma primitive_part_eq_0_iff [simp]: "primitive_part p = 0 \<longleftrightarrow> p = 0"
  4509 proof (cases "p = 0")
  4510   case True
  4511   then show ?thesis by simp
  4512 next
  4513   case False
  4514   then have "primitive_part p = map_poly (\<lambda>x. x div content p) p"
  4515     by (simp add:  primitive_part_def)
  4516   also from False have "\<dots> = 0 \<longleftrightarrow> p = 0"
  4517     by (intro map_poly_eq_0_iff) (auto simp: dvd_div_eq_0_iff content_dvd_coeffs)
  4518   finally show ?thesis
  4519     using False by simp
  4520 qed
  4521 
  4522 lemma content_primitive_part [simp]:
  4523   assumes "p \<noteq> 0"
  4524   shows "content (primitive_part p) = 1"
  4525 proof -
  4526   have "p = smult (content p) (primitive_part p)"
  4527     by simp
  4528   also have "content \<dots> = content (primitive_part p) * content p"
  4529     by (simp del: content_times_primitive_part add: ac_simps)
  4530   finally have "1 * content p = content (primitive_part p) * content p"
  4531     by simp
  4532   then have "1 * content p div content p = content (primitive_part p) * content p div content p"
  4533     by simp
  4534   with assms show ?thesis
  4535     by simp
  4536 qed
  4537 
  4538 lemma content_decompose:
  4539   obtains p' :: "'a::semiring_gcd poly" where "p = smult (content p) p'" "content p' = 1"
  4540 proof (cases "p = 0")
  4541   case True
  4542   then show ?thesis by (intro that[of 1]) simp_all
  4543 next
  4544   case False
  4545   from content_dvd[of p] obtain r where r: "p = [:content p:] * r"
  4546     by (rule dvdE)
  4547   have "content p * 1 = content p * content r"
  4548     by (subst r) simp
  4549   with False have "content r = 1"
  4550     by (subst (asm) mult_left_cancel) simp_all
  4551   with r show ?thesis
  4552     by (intro that[of r]) simp_all
  4553 qed
  4554 
  4555 lemma content_dvd_contentI [intro]: "p dvd q \<Longrightarrow> content p dvd content q"
  4556   using const_poly_dvd_iff_dvd_content content_dvd dvd_trans by blast
  4557 
  4558 lemma primitive_part_const_poly [simp]: "primitive_part [:x:] = [:unit_factor x:]"
  4559   by (simp add: primitive_part_def map_poly_pCons)
  4560 
  4561 lemma primitive_part_prim: "content p = 1 \<Longrightarrow> primitive_part p = p"
  4562   by (auto simp: primitive_part_def)
  4563 
  4564 lemma degree_primitive_part [simp]: "degree (primitive_part p) = degree p"
  4565 proof (cases "p = 0")
  4566   case True
  4567   then show ?thesis by simp
  4568 next
  4569   case False
  4570   have "p = smult (content p) (primitive_part p)"
  4571     by simp
  4572   also from False have "degree \<dots> = degree (primitive_part p)"
  4573     by (subst degree_smult_eq) simp_all
  4574   finally show ?thesis ..
  4575 qed
  4576 
  4577 lemma smult_content_normalize_primitive_part [simp]:
  4578   "smult (content p) (normalize (primitive_part p)) = normalize p"
  4579 proof -
  4580   have "smult (content p) (normalize (primitive_part p)) =
  4581       normalize ([:content p:] * primitive_part p)"
  4582     by (subst normalize_mult) (simp_all add: normalize_const_poly)
  4583   also have "[:content p:] * primitive_part p = p" by simp
  4584   finally show ?thesis .
  4585 qed
  4586 
  4587 lemma content_mult:
  4588   fixes p q :: "'a :: {factorial_semiring, semiring_Gcd} poly"
  4589   shows "content (p * q) = content p * content q"
  4590 proof -
  4591   from content_decompose[of p] guess p' . note p = this
  4592   from content_decompose[of q] guess q' . note q = this
  4593   have "content (p * q) = content p * content q * content (p' * q')"
  4594     by (subst p, subst q) (simp add: mult_ac normalize_mult)
  4595   also have "content (p' * q') = 1"
  4596   proof (cases "p' * q' = 0")
  4597     case True
  4598     with \<open>content p' = 1\<close> \<open>content q' = 1\<close> show ?thesis
  4599       by auto
  4600   next  
  4601     case False
  4602     from \<open>content p' = 1\<close> \<open>content q' = 1\<close>
  4603     have "p' \<noteq> 0" "q' \<noteq> 0"
  4604       by auto
  4605     then have "p' * q' \<noteq> 0"
  4606       by auto
  4607     have "is_unit (content (p' * q'))"
  4608     proof (rule ccontr)      
  4609       assume "\<not> is_unit (content (p' * q'))"
  4610       with False have "\<exists>p. p dvd content (p' * q') \<and> prime p"
  4611         by (intro prime_divisor_exists) simp_all
  4612       then obtain p where "p dvd content (p' * q')" "prime p"
  4613         by blast
  4614       from \<open>p dvd content (p' * q')\<close> have "[:p:] dvd p' * q'"
  4615         by (simp add: const_poly_dvd_iff_dvd_content)
  4616       moreover from \<open>prime p\<close> have "prime_elem [:p:]"
  4617         by (simp add: lift_prime_elem_poly)
  4618       ultimately have "[:p:] dvd p' \<or> [:p:] dvd q'"
  4619         by (simp add: prime_elem_dvd_mult_iff)
  4620       with \<open>content p' = 1\<close> \<open>content q' = 1\<close> have "is_unit p"
  4621         by (simp add: const_poly_dvd_iff_dvd_content)
  4622       with \<open>prime p\<close> show False
  4623         by simp
  4624     qed    
  4625     then have "normalize (content (p' * q')) = 1"
  4626       by (simp add: is_unit_normalize del: normalize_content)
  4627     then show ?thesis
  4628       by simp
  4629   qed
  4630   finally show ?thesis
  4631     by simp
  4632 qed
  4633 
  4634 lemma primitive_part_mult:
  4635   fixes p q :: "'a :: {factorial_semiring, semiring_Gcd, ring_gcd, idom_divide} poly"
  4636   shows "primitive_part (p * q) = primitive_part p * primitive_part q"
  4637 proof -
  4638   have "primitive_part (p * q) = p * q div [:content (p * q):]"
  4639     by (simp add: primitive_part_def div_const_poly_conv_map_poly)
  4640   also have "\<dots> = (p div [:content p:]) * (q div [:content q:])"
  4641     by (subst div_mult_div_if_dvd) (simp_all add: content_mult mult_ac)
  4642   also have "\<dots> = primitive_part p * primitive_part q"
  4643     by (simp add: primitive_part_def div_const_poly_conv_map_poly)
  4644   finally show ?thesis .
  4645 qed
  4646 
  4647 lemma primitive_part_smult:
  4648   fixes p :: "'a :: {factorial_semiring, semiring_Gcd, ring_gcd, idom_divide} poly"
  4649   shows "primitive_part (smult a p) = smult (unit_factor a) (primitive_part p)"
  4650 proof -
  4651   have "smult a p = [:a:] * p" by simp
  4652   also have "primitive_part \<dots> = smult (unit_factor a) (primitive_part p)"
  4653     by (subst primitive_part_mult) simp_all
  4654   finally show ?thesis .
  4655 qed  
  4656 
  4657 lemma primitive_part_dvd_primitive_partI [intro]:
  4658   fixes p q :: "'a :: {factorial_semiring, semiring_Gcd, ring_gcd, idom_divide} poly"
  4659   shows "p dvd q \<Longrightarrow> primitive_part p dvd primitive_part q"
  4660   by (auto elim!: dvdE simp: primitive_part_mult)
  4661 
  4662 lemma content_prod_mset: 
  4663   fixes A :: "'a :: {factorial_semiring, semiring_Gcd} poly multiset"
  4664   shows "content (prod_mset A) = prod_mset (image_mset content A)"
  4665   by (induction A) (simp_all add: content_mult mult_ac)
  4666 
  4667 lemma content_prod_eq_1_iff: 
  4668   fixes p q :: "'a :: {factorial_semiring, semiring_Gcd} poly"
  4669   shows "content (p * q) = 1 \<longleftrightarrow> content p = 1 \<and> content q = 1"
  4670 proof safe
  4671   assume A: "content (p * q) = 1"
  4672   {
  4673     fix p q :: "'a poly" assume "content p * content q = 1"
  4674     hence "1 = content p * content q" by simp
  4675     hence "content p dvd 1" by (rule dvdI)
  4676     hence "content p = 1" by simp
  4677   } note B = this
  4678   from A B[of p q] B [of q p] show "content p = 1" "content q = 1" 
  4679     by (simp_all add: content_mult mult_ac)
  4680 qed (auto simp: content_mult)
  4681 
  4682 
  4683 no_notation cCons (infixr "##" 65)
  4684 
  4685 end