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