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