src/HOL/Library/Polynomial.thy
author haftmann
Wed Feb 17 21:51:58 2016 +0100 (2016-02-17)
changeset 62352 35a9e1cbb5b3
parent 62351 fd049b54ad68
child 62422 4aa35fd6c152
permissions -rw-r--r--
separated potentially conflicting type class instance into separate theory
     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 by (auto intro!: ALL_MOST)
    59 
    60 setup_lifting type_definition_poly
    61 
    62 lemma poly_eq_iff: "p = q \<longleftrightarrow> (\<forall>n. coeff p n = coeff q n)"
    63   by (simp add: coeff_inject [symmetric] fun_eq_iff)
    64 
    65 lemma poly_eqI: "(\<And>n. coeff p n = coeff q n) \<Longrightarrow> p = q"
    66   by (simp add: poly_eq_iff)
    67 
    68 lemma MOST_coeff_eq_0: "\<forall>\<^sub>\<infinity> n. coeff p n = 0"
    69   using coeff [of p] by simp
    70 
    71 
    72 subsection \<open>Degree of a polynomial\<close>
    73 
    74 definition degree :: "'a::zero poly \<Rightarrow> nat"
    75 where
    76   "degree p = (LEAST n. \<forall>i>n. coeff p i = 0)"
    77 
    78 lemma coeff_eq_0:
    79   assumes "degree p < n"
    80   shows "coeff p n = 0"
    81 proof -
    82   have "\<exists>n. \<forall>i>n. coeff p i = 0"
    83     using MOST_coeff_eq_0 by (simp add: MOST_nat)
    84   then have "\<forall>i>degree p. coeff p i = 0"
    85     unfolding degree_def by (rule LeastI_ex)
    86   with assms show ?thesis by simp
    87 qed
    88 
    89 lemma le_degree: "coeff p n \<noteq> 0 \<Longrightarrow> n \<le> degree p"
    90   by (erule contrapos_np, rule coeff_eq_0, simp)
    91 
    92 lemma degree_le: "\<forall>i>n. coeff p i = 0 \<Longrightarrow> degree p \<le> n"
    93   unfolding degree_def by (erule Least_le)
    94 
    95 lemma less_degree_imp: "n < degree p \<Longrightarrow> \<exists>i>n. coeff p i \<noteq> 0"
    96   unfolding degree_def by (drule not_less_Least, simp)
    97 
    98 
    99 subsection \<open>The zero polynomial\<close>
   100 
   101 instantiation poly :: (zero) zero
   102 begin
   103 
   104 lift_definition zero_poly :: "'a poly"
   105   is "\<lambda>_. 0" by (rule MOST_I) simp
   106 
   107 instance ..
   108 
   109 end
   110 
   111 lemma coeff_0 [simp]:
   112   "coeff 0 n = 0"
   113   by transfer rule
   114 
   115 lemma degree_0 [simp]:
   116   "degree 0 = 0"
   117   by (rule order_antisym [OF degree_le le0]) simp
   118 
   119 lemma leading_coeff_neq_0:
   120   assumes "p \<noteq> 0"
   121   shows "coeff p (degree p) \<noteq> 0"
   122 proof (cases "degree p")
   123   case 0
   124   from \<open>p \<noteq> 0\<close> have "\<exists>n. coeff p n \<noteq> 0"
   125     by (simp add: poly_eq_iff)
   126   then obtain n where "coeff p n \<noteq> 0" ..
   127   hence "n \<le> degree p" by (rule le_degree)
   128   with \<open>coeff p n \<noteq> 0\<close> and \<open>degree p = 0\<close>
   129   show "coeff p (degree p) \<noteq> 0" by simp
   130 next
   131   case (Suc n)
   132   from \<open>degree p = Suc n\<close> have "n < degree p" by simp
   133   hence "\<exists>i>n. coeff p i \<noteq> 0" by (rule less_degree_imp)
   134   then obtain i where "n < i" and "coeff p i \<noteq> 0" by fast
   135   from \<open>degree p = Suc n\<close> and \<open>n < i\<close> have "degree p \<le> i" by simp
   136   also from \<open>coeff p i \<noteq> 0\<close> have "i \<le> degree p" by (rule le_degree)
   137   finally have "degree p = i" .
   138   with \<open>coeff p i \<noteq> 0\<close> show "coeff p (degree p) \<noteq> 0" by simp
   139 qed
   140 
   141 lemma leading_coeff_0_iff [simp]:
   142   "coeff p (degree p) = 0 \<longleftrightarrow> p = 0"
   143   by (cases "p = 0", simp, simp add: leading_coeff_neq_0)
   144 
   145 
   146 subsection \<open>List-style constructor for polynomials\<close>
   147 
   148 lift_definition pCons :: "'a::zero \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
   149   is "\<lambda>a p. case_nat a (coeff p)"
   150   by (rule MOST_SucD) (simp add: MOST_coeff_eq_0)
   151 
   152 lemmas coeff_pCons = pCons.rep_eq
   153 
   154 lemma coeff_pCons_0 [simp]:
   155   "coeff (pCons a p) 0 = a"
   156   by transfer simp
   157 
   158 lemma coeff_pCons_Suc [simp]:
   159   "coeff (pCons a p) (Suc n) = coeff p n"
   160   by (simp add: coeff_pCons)
   161 
   162 lemma degree_pCons_le:
   163   "degree (pCons a p) \<le> Suc (degree p)"
   164   by (rule degree_le) (simp add: coeff_eq_0 coeff_pCons split: nat.split)
   165 
   166 lemma degree_pCons_eq:
   167   "p \<noteq> 0 \<Longrightarrow> degree (pCons a p) = Suc (degree p)"
   168   apply (rule order_antisym [OF degree_pCons_le])
   169   apply (rule le_degree, simp)
   170   done
   171 
   172 lemma degree_pCons_0:
   173   "degree (pCons a 0) = 0"
   174   apply (rule order_antisym [OF _ le0])
   175   apply (rule degree_le, simp add: coeff_pCons split: nat.split)
   176   done
   177 
   178 lemma degree_pCons_eq_if [simp]:
   179   "degree (pCons a p) = (if p = 0 then 0 else Suc (degree p))"
   180   apply (cases "p = 0", simp_all)
   181   apply (rule order_antisym [OF _ le0])
   182   apply (rule degree_le, simp add: coeff_pCons split: nat.split)
   183   apply (rule order_antisym [OF degree_pCons_le])
   184   apply (rule le_degree, simp)
   185   done
   186 
   187 lemma pCons_0_0 [simp]:
   188   "pCons 0 0 = 0"
   189   by (rule poly_eqI) (simp add: coeff_pCons split: nat.split)
   190 
   191 lemma pCons_eq_iff [simp]:
   192   "pCons a p = pCons b q \<longleftrightarrow> a = b \<and> p = q"
   193 proof safe
   194   assume "pCons a p = pCons b q"
   195   then have "coeff (pCons a p) 0 = coeff (pCons b q) 0" by simp
   196   then show "a = b" by simp
   197 next
   198   assume "pCons a p = pCons b q"
   199   then have "\<forall>n. coeff (pCons a p) (Suc n) =
   200                  coeff (pCons b q) (Suc n)" by simp
   201   then show "p = q" by (simp add: poly_eq_iff)
   202 qed
   203 
   204 lemma pCons_eq_0_iff [simp]:
   205   "pCons a p = 0 \<longleftrightarrow> a = 0 \<and> p = 0"
   206   using pCons_eq_iff [of a p 0 0] by simp
   207 
   208 lemma pCons_cases [cases type: poly]:
   209   obtains (pCons) a q where "p = pCons a q"
   210 proof
   211   show "p = pCons (coeff p 0) (Abs_poly (\<lambda>n. coeff p (Suc n)))"
   212     by transfer
   213        (simp_all add: MOST_inj[where f=Suc and P="\<lambda>n. p n = 0" for p] fun_eq_iff Abs_poly_inverse
   214                  split: nat.split)
   215 qed
   216 
   217 lemma pCons_induct [case_names 0 pCons, induct type: poly]:
   218   assumes zero: "P 0"
   219   assumes pCons: "\<And>a p. a \<noteq> 0 \<or> p \<noteq> 0 \<Longrightarrow> P p \<Longrightarrow> P (pCons a p)"
   220   shows "P p"
   221 proof (induct p rule: measure_induct_rule [where f=degree])
   222   case (less p)
   223   obtain a q where "p = pCons a q" by (rule pCons_cases)
   224   have "P q"
   225   proof (cases "q = 0")
   226     case True
   227     then show "P q" by (simp add: zero)
   228   next
   229     case False
   230     then have "degree (pCons a q) = Suc (degree q)"
   231       by (rule degree_pCons_eq)
   232     then have "degree q < degree p"
   233       using \<open>p = pCons a q\<close> by simp
   234     then show "P q"
   235       by (rule less.hyps)
   236   qed
   237   have "P (pCons a q)"
   238   proof (cases "a \<noteq> 0 \<or> q \<noteq> 0")
   239     case True
   240     with \<open>P q\<close> show ?thesis by (auto intro: pCons)
   241   next
   242     case False
   243     with zero show ?thesis by simp
   244   qed
   245   then show ?case
   246     using \<open>p = pCons a q\<close> by simp
   247 qed
   248 
   249 lemma degree_eq_zeroE:
   250   fixes p :: "'a::zero poly"
   251   assumes "degree p = 0"
   252   obtains a where "p = pCons a 0"
   253 proof -
   254   obtain a q where p: "p = pCons a q" by (cases p)
   255   with assms have "q = 0" by (cases "q = 0") simp_all
   256   with p have "p = pCons a 0" by simp
   257   with that show thesis .
   258 qed
   259 
   260 
   261 subsection \<open>List-style syntax for polynomials\<close>
   262 
   263 syntax
   264   "_poly" :: "args \<Rightarrow> 'a poly"  ("[:(_):]")
   265 
   266 translations
   267   "[:x, xs:]" == "CONST pCons x [:xs:]"
   268   "[:x:]" == "CONST pCons x 0"
   269   "[:x:]" <= "CONST pCons x (_constrain 0 t)"
   270 
   271 
   272 subsection \<open>Representation of polynomials by lists of coefficients\<close>
   273 
   274 primrec Poly :: "'a::zero list \<Rightarrow> 'a poly"
   275 where
   276   [code_post]: "Poly [] = 0"
   277 | [code_post]: "Poly (a # as) = pCons a (Poly as)"
   278 
   279 lemma Poly_replicate_0 [simp]:
   280   "Poly (replicate n 0) = 0"
   281   by (induct n) simp_all
   282 
   283 lemma Poly_eq_0:
   284   "Poly as = 0 \<longleftrightarrow> (\<exists>n. as = replicate n 0)"
   285   by (induct as) (auto simp add: Cons_replicate_eq)
   286   
   287 lemma degree_Poly: "degree (Poly xs) \<le> length xs"
   288   by (induction xs) simp_all
   289   
   290 definition coeffs :: "'a poly \<Rightarrow> 'a::zero list"
   291 where
   292   "coeffs p = (if p = 0 then [] else map (\<lambda>i. coeff p i) [0 ..< Suc (degree p)])"
   293 
   294 lemma coeffs_eq_Nil [simp]:
   295   "coeffs p = [] \<longleftrightarrow> p = 0"
   296   by (simp add: coeffs_def)
   297 
   298 lemma not_0_coeffs_not_Nil:
   299   "p \<noteq> 0 \<Longrightarrow> coeffs p \<noteq> []"
   300   by simp
   301 
   302 lemma coeffs_0_eq_Nil [simp]:
   303   "coeffs 0 = []"
   304   by simp
   305 
   306 lemma coeffs_pCons_eq_cCons [simp]:
   307   "coeffs (pCons a p) = a ## coeffs p"
   308 proof -
   309   { fix ms :: "nat list" and f :: "nat \<Rightarrow> 'a" and x :: "'a"
   310     assume "\<forall>m\<in>set ms. m > 0"
   311     then have "map (case_nat x f) ms = map f (map (\<lambda>n. n - 1) ms)"
   312       by (induct ms) (auto split: nat.split)
   313   }
   314   note * = this
   315   show ?thesis
   316     by (simp add: coeffs_def * upt_conv_Cons coeff_pCons map_decr_upt del: upt_Suc)
   317 qed
   318 
   319 lemma length_coeffs: "p \<noteq> 0 \<Longrightarrow> length (coeffs p) = degree p + 1"
   320   by (simp add: coeffs_def)
   321   
   322 lemma coeffs_nth:
   323   assumes "p \<noteq> 0" "n \<le> degree p"
   324   shows   "coeffs p ! n = coeff p n"
   325   using assms unfolding coeffs_def by (auto simp del: upt_Suc)
   326 
   327 lemma not_0_cCons_eq [simp]:
   328   "p \<noteq> 0 \<Longrightarrow> a ## coeffs p = a # coeffs p"
   329   by (simp add: cCons_def)
   330 
   331 lemma Poly_coeffs [simp, code abstype]:
   332   "Poly (coeffs p) = p"
   333   by (induct p) auto
   334 
   335 lemma coeffs_Poly [simp]:
   336   "coeffs (Poly as) = strip_while (HOL.eq 0) as"
   337 proof (induct as)
   338   case Nil then show ?case by simp
   339 next
   340   case (Cons a as)
   341   have "(\<forall>n. as \<noteq> replicate n 0) \<longleftrightarrow> (\<exists>a\<in>set as. a \<noteq> 0)"
   342     using replicate_length_same [of as 0] by (auto dest: sym [of _ as])
   343   with Cons show ?case by auto
   344 qed
   345 
   346 lemma last_coeffs_not_0:
   347   "p \<noteq> 0 \<Longrightarrow> last (coeffs p) \<noteq> 0"
   348   by (induct p) (auto simp add: cCons_def)
   349 
   350 lemma strip_while_coeffs [simp]:
   351   "strip_while (HOL.eq 0) (coeffs p) = coeffs p"
   352   by (cases "p = 0") (auto dest: last_coeffs_not_0 intro: strip_while_not_last)
   353 
   354 lemma coeffs_eq_iff:
   355   "p = q \<longleftrightarrow> coeffs p = coeffs q" (is "?P \<longleftrightarrow> ?Q")
   356 proof
   357   assume ?P then show ?Q by simp
   358 next
   359   assume ?Q
   360   then have "Poly (coeffs p) = Poly (coeffs q)" by simp
   361   then show ?P by simp
   362 qed
   363 
   364 lemma coeff_Poly_eq:
   365   "coeff (Poly xs) n = nth_default 0 xs n"
   366   apply (induct xs arbitrary: n) apply simp_all
   367   by (metis nat.case not0_implies_Suc nth_default_Cons_0 nth_default_Cons_Suc pCons.rep_eq)
   368 
   369 lemma nth_default_coeffs_eq:
   370   "nth_default 0 (coeffs p) = coeff p"
   371   by (simp add: fun_eq_iff coeff_Poly_eq [symmetric])
   372 
   373 lemma [code]:
   374   "coeff p = nth_default 0 (coeffs p)"
   375   by (simp add: nth_default_coeffs_eq)
   376 
   377 lemma coeffs_eqI:
   378   assumes coeff: "\<And>n. coeff p n = nth_default 0 xs n"
   379   assumes zero: "xs \<noteq> [] \<Longrightarrow> last xs \<noteq> 0"
   380   shows "coeffs p = xs"
   381 proof -
   382   from coeff have "p = Poly xs" by (simp add: poly_eq_iff coeff_Poly_eq)
   383   with zero show ?thesis by simp (cases xs, simp_all)
   384 qed
   385 
   386 lemma degree_eq_length_coeffs [code]:
   387   "degree p = length (coeffs p) - 1"
   388   by (simp add: coeffs_def)
   389 
   390 lemma length_coeffs_degree:
   391   "p \<noteq> 0 \<Longrightarrow> length (coeffs p) = Suc (degree p)"
   392   by (induct p) (auto simp add: cCons_def)
   393 
   394 lemma [code abstract]:
   395   "coeffs 0 = []"
   396   by (fact coeffs_0_eq_Nil)
   397 
   398 lemma [code abstract]:
   399   "coeffs (pCons a p) = a ## coeffs p"
   400   by (fact coeffs_pCons_eq_cCons)
   401 
   402 instantiation poly :: ("{zero, equal}") equal
   403 begin
   404 
   405 definition
   406   [code]: "HOL.equal (p::'a poly) q \<longleftrightarrow> HOL.equal (coeffs p) (coeffs q)"
   407 
   408 instance
   409   by standard (simp add: equal equal_poly_def coeffs_eq_iff)
   410 
   411 end
   412 
   413 lemma [code nbe]: "HOL.equal (p :: _ poly) p \<longleftrightarrow> True"
   414   by (fact equal_refl)
   415 
   416 definition is_zero :: "'a::zero poly \<Rightarrow> bool"
   417 where
   418   [code]: "is_zero p \<longleftrightarrow> List.null (coeffs p)"
   419 
   420 lemma is_zero_null [code_abbrev]:
   421   "is_zero p \<longleftrightarrow> p = 0"
   422   by (simp add: is_zero_def null_def)
   423 
   424 
   425 subsection \<open>Fold combinator for polynomials\<close>
   426 
   427 definition fold_coeffs :: "('a::zero \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a poly \<Rightarrow> 'b \<Rightarrow> 'b"
   428 where
   429   "fold_coeffs f p = foldr f (coeffs p)"
   430 
   431 lemma fold_coeffs_0_eq [simp]:
   432   "fold_coeffs f 0 = id"
   433   by (simp add: fold_coeffs_def)
   434 
   435 lemma fold_coeffs_pCons_eq [simp]:
   436   "f 0 = id \<Longrightarrow> fold_coeffs f (pCons a p) = f a \<circ> fold_coeffs f p"
   437   by (simp add: fold_coeffs_def cCons_def fun_eq_iff)
   438 
   439 lemma fold_coeffs_pCons_0_0_eq [simp]:
   440   "fold_coeffs f (pCons 0 0) = id"
   441   by (simp add: fold_coeffs_def)
   442 
   443 lemma fold_coeffs_pCons_coeff_not_0_eq [simp]:
   444   "a \<noteq> 0 \<Longrightarrow> fold_coeffs f (pCons a p) = f a \<circ> fold_coeffs f p"
   445   by (simp add: fold_coeffs_def)
   446 
   447 lemma fold_coeffs_pCons_not_0_0_eq [simp]:
   448   "p \<noteq> 0 \<Longrightarrow> fold_coeffs f (pCons a p) = f a \<circ> fold_coeffs f p"
   449   by (simp add: fold_coeffs_def)
   450 
   451 
   452 subsection \<open>Canonical morphism on polynomials -- evaluation\<close>
   453 
   454 definition poly :: "'a::comm_semiring_0 poly \<Rightarrow> 'a \<Rightarrow> 'a"
   455 where
   456   "poly p = fold_coeffs (\<lambda>a f x. a + x * f x) p (\<lambda>x. 0)" \<comment> \<open>The Horner Schema\<close>
   457 
   458 lemma poly_0 [simp]:
   459   "poly 0 x = 0"
   460   by (simp add: poly_def)
   461   
   462 lemma poly_pCons [simp]:
   463   "poly (pCons a p) x = a + x * poly p x"
   464   by (cases "p = 0 \<and> a = 0") (auto simp add: poly_def)
   465 
   466 lemma poly_altdef: 
   467   "poly p (x :: 'a :: {comm_semiring_0, semiring_1}) = (\<Sum>i\<le>degree p. coeff p i * x ^ i)"
   468 proof (induction p rule: pCons_induct)
   469   case (pCons a p)
   470     show ?case
   471     proof (cases "p = 0")
   472       case False
   473       let ?p' = "pCons a p"
   474       note poly_pCons[of a p x]
   475       also note pCons.IH
   476       also have "a + x * (\<Sum>i\<le>degree p. coeff p i * x ^ i) =
   477                  coeff ?p' 0 * x^0 + (\<Sum>i\<le>degree p. coeff ?p' (Suc i) * x^Suc i)"
   478           by (simp add: field_simps setsum_right_distrib coeff_pCons)
   479       also note setsum_atMost_Suc_shift[symmetric]
   480       also note degree_pCons_eq[OF \<open>p \<noteq> 0\<close>, of a, symmetric]
   481       finally show ?thesis .
   482    qed simp
   483 qed simp
   484 
   485 lemma poly_0_coeff_0: "poly p 0 = coeff p 0"
   486   by (cases p) (auto simp: poly_altdef)
   487 
   488 
   489 subsection \<open>Monomials\<close>
   490 
   491 lift_definition monom :: "'a \<Rightarrow> nat \<Rightarrow> 'a::zero poly"
   492   is "\<lambda>a m n. if m = n then a else 0"
   493   by (simp add: MOST_iff_cofinite)
   494 
   495 lemma coeff_monom [simp]:
   496   "coeff (monom a m) n = (if m = n then a else 0)"
   497   by transfer rule
   498 
   499 lemma monom_0:
   500   "monom a 0 = pCons a 0"
   501   by (rule poly_eqI) (simp add: coeff_pCons split: nat.split)
   502 
   503 lemma monom_Suc:
   504   "monom a (Suc n) = pCons 0 (monom a n)"
   505   by (rule poly_eqI) (simp add: coeff_pCons split: nat.split)
   506 
   507 lemma monom_eq_0 [simp]: "monom 0 n = 0"
   508   by (rule poly_eqI) simp
   509 
   510 lemma monom_eq_0_iff [simp]: "monom a n = 0 \<longleftrightarrow> a = 0"
   511   by (simp add: poly_eq_iff)
   512 
   513 lemma monom_eq_iff [simp]: "monom a n = monom b n \<longleftrightarrow> a = b"
   514   by (simp add: poly_eq_iff)
   515 
   516 lemma degree_monom_le: "degree (monom a n) \<le> n"
   517   by (rule degree_le, simp)
   518 
   519 lemma degree_monom_eq: "a \<noteq> 0 \<Longrightarrow> degree (monom a n) = n"
   520   apply (rule order_antisym [OF degree_monom_le])
   521   apply (rule le_degree, simp)
   522   done
   523 
   524 lemma coeffs_monom [code abstract]:
   525   "coeffs (monom a n) = (if a = 0 then [] else replicate n 0 @ [a])"
   526   by (induct n) (simp_all add: monom_0 monom_Suc)
   527 
   528 lemma fold_coeffs_monom [simp]:
   529   "a \<noteq> 0 \<Longrightarrow> fold_coeffs f (monom a n) = f 0 ^^ n \<circ> f a"
   530   by (simp add: fold_coeffs_def coeffs_monom fun_eq_iff)
   531 
   532 lemma poly_monom:
   533   fixes a x :: "'a::{comm_semiring_1}"
   534   shows "poly (monom a n) x = a * x ^ n"
   535   by (cases "a = 0", simp_all)
   536     (induct n, simp_all add: mult.left_commute poly_def)
   537 
   538     
   539 subsection \<open>Addition and subtraction\<close>
   540 
   541 instantiation poly :: (comm_monoid_add) comm_monoid_add
   542 begin
   543 
   544 lift_definition plus_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
   545   is "\<lambda>p q n. coeff p n + coeff q n"
   546 proof -
   547   fix q p :: "'a poly"
   548   show "\<forall>\<^sub>\<infinity>n. coeff p n + coeff q n = 0"
   549     using MOST_coeff_eq_0[of p] MOST_coeff_eq_0[of q] by eventually_elim simp
   550 qed
   551 
   552 lemma coeff_add [simp]: "coeff (p + q) n = coeff p n + coeff q n"
   553   by (simp add: plus_poly.rep_eq)
   554 
   555 instance
   556 proof
   557   fix p q r :: "'a poly"
   558   show "(p + q) + r = p + (q + r)"
   559     by (simp add: poly_eq_iff add.assoc)
   560   show "p + q = q + p"
   561     by (simp add: poly_eq_iff add.commute)
   562   show "0 + p = p"
   563     by (simp add: poly_eq_iff)
   564 qed
   565 
   566 end
   567 
   568 instantiation poly :: (cancel_comm_monoid_add) cancel_comm_monoid_add
   569 begin
   570 
   571 lift_definition minus_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
   572   is "\<lambda>p q n. coeff p n - coeff q n"
   573 proof -
   574   fix q p :: "'a poly"
   575   show "\<forall>\<^sub>\<infinity>n. coeff p n - coeff q n = 0"
   576     using MOST_coeff_eq_0[of p] MOST_coeff_eq_0[of q] by eventually_elim simp
   577 qed
   578 
   579 lemma coeff_diff [simp]: "coeff (p - q) n = coeff p n - coeff q n"
   580   by (simp add: minus_poly.rep_eq)
   581 
   582 instance
   583 proof
   584   fix p q r :: "'a poly"
   585   show "p + q - p = q"
   586     by (simp add: poly_eq_iff)
   587   show "p - q - r = p - (q + r)"
   588     by (simp add: poly_eq_iff diff_diff_eq)
   589 qed
   590 
   591 end
   592 
   593 instantiation poly :: (ab_group_add) ab_group_add
   594 begin
   595 
   596 lift_definition uminus_poly :: "'a poly \<Rightarrow> 'a poly"
   597   is "\<lambda>p n. - coeff p n"
   598 proof -
   599   fix p :: "'a poly"
   600   show "\<forall>\<^sub>\<infinity>n. - coeff p n = 0"
   601     using MOST_coeff_eq_0 by simp
   602 qed
   603 
   604 lemma coeff_minus [simp]: "coeff (- p) n = - coeff p n"
   605   by (simp add: uminus_poly.rep_eq)
   606 
   607 instance
   608 proof
   609   fix p q :: "'a poly"
   610   show "- p + p = 0"
   611     by (simp add: poly_eq_iff)
   612   show "p - q = p + - q"
   613     by (simp add: poly_eq_iff)
   614 qed
   615 
   616 end
   617 
   618 lemma add_pCons [simp]:
   619   "pCons a p + pCons b q = pCons (a + b) (p + q)"
   620   by (rule poly_eqI, simp add: coeff_pCons split: nat.split)
   621 
   622 lemma minus_pCons [simp]:
   623   "- pCons a p = pCons (- a) (- p)"
   624   by (rule poly_eqI, simp add: coeff_pCons split: nat.split)
   625 
   626 lemma diff_pCons [simp]:
   627   "pCons a p - pCons b q = pCons (a - b) (p - q)"
   628   by (rule poly_eqI, simp add: coeff_pCons split: nat.split)
   629 
   630 lemma degree_add_le_max: "degree (p + q) \<le> max (degree p) (degree q)"
   631   by (rule degree_le, auto simp add: coeff_eq_0)
   632 
   633 lemma degree_add_le:
   634   "\<lbrakk>degree p \<le> n; degree q \<le> n\<rbrakk> \<Longrightarrow> degree (p + q) \<le> n"
   635   by (auto intro: order_trans degree_add_le_max)
   636 
   637 lemma degree_add_less:
   638   "\<lbrakk>degree p < n; degree q < n\<rbrakk> \<Longrightarrow> degree (p + q) < n"
   639   by (auto intro: le_less_trans degree_add_le_max)
   640 
   641 lemma degree_add_eq_right:
   642   "degree p < degree q \<Longrightarrow> degree (p + q) = degree q"
   643   apply (cases "q = 0", simp)
   644   apply (rule order_antisym)
   645   apply (simp add: degree_add_le)
   646   apply (rule le_degree)
   647   apply (simp add: coeff_eq_0)
   648   done
   649 
   650 lemma degree_add_eq_left:
   651   "degree q < degree p \<Longrightarrow> degree (p + q) = degree p"
   652   using degree_add_eq_right [of q p]
   653   by (simp add: add.commute)
   654 
   655 lemma degree_minus [simp]:
   656   "degree (- p) = degree p"
   657   unfolding degree_def by simp
   658 
   659 lemma degree_diff_le_max:
   660   fixes p q :: "'a :: ab_group_add poly"
   661   shows "degree (p - q) \<le> max (degree p) (degree q)"
   662   using degree_add_le [where p=p and q="-q"]
   663   by simp
   664 
   665 lemma degree_diff_le:
   666   fixes p q :: "'a :: ab_group_add poly"
   667   assumes "degree p \<le> n" and "degree q \<le> n"
   668   shows "degree (p - q) \<le> n"
   669   using assms degree_add_le [of p n "- q"] by simp
   670 
   671 lemma degree_diff_less:
   672   fixes p q :: "'a :: ab_group_add poly"
   673   assumes "degree p < n" and "degree q < n"
   674   shows "degree (p - q) < n"
   675   using assms degree_add_less [of p n "- q"] by simp
   676 
   677 lemma add_monom: "monom a n + monom b n = monom (a + b) n"
   678   by (rule poly_eqI) simp
   679 
   680 lemma diff_monom: "monom a n - monom b n = monom (a - b) n"
   681   by (rule poly_eqI) simp
   682 
   683 lemma minus_monom: "- monom a n = monom (-a) n"
   684   by (rule poly_eqI) simp
   685 
   686 lemma coeff_setsum: "coeff (\<Sum>x\<in>A. p x) i = (\<Sum>x\<in>A. coeff (p x) i)"
   687   by (cases "finite A", induct set: finite, simp_all)
   688 
   689 lemma monom_setsum: "monom (\<Sum>x\<in>A. a x) n = (\<Sum>x\<in>A. monom (a x) n)"
   690   by (rule poly_eqI) (simp add: coeff_setsum)
   691 
   692 fun plus_coeffs :: "'a::comm_monoid_add list \<Rightarrow> 'a list \<Rightarrow> 'a list"
   693 where
   694   "plus_coeffs xs [] = xs"
   695 | "plus_coeffs [] ys = ys"
   696 | "plus_coeffs (x # xs) (y # ys) = (x + y) ## plus_coeffs xs ys"
   697 
   698 lemma coeffs_plus_eq_plus_coeffs [code abstract]:
   699   "coeffs (p + q) = plus_coeffs (coeffs p) (coeffs q)"
   700 proof -
   701   { fix xs ys :: "'a list" and n
   702     have "nth_default 0 (plus_coeffs xs ys) n = nth_default 0 xs n + nth_default 0 ys n"
   703     proof (induct xs ys arbitrary: n rule: plus_coeffs.induct)
   704       case (3 x xs y ys n)
   705       then show ?case by (cases n) (auto simp add: cCons_def)
   706     qed simp_all }
   707   note * = this
   708   { fix xs ys :: "'a list"
   709     assume "xs \<noteq> [] \<Longrightarrow> last xs \<noteq> 0" and "ys \<noteq> [] \<Longrightarrow> last ys \<noteq> 0"
   710     moreover assume "plus_coeffs xs ys \<noteq> []"
   711     ultimately have "last (plus_coeffs xs ys) \<noteq> 0"
   712     proof (induct xs ys rule: plus_coeffs.induct)
   713       case (3 x xs y ys) then show ?case by (auto simp add: cCons_def) metis
   714     qed simp_all }
   715   note ** = this
   716   show ?thesis
   717     apply (rule coeffs_eqI)
   718     apply (simp add: * nth_default_coeffs_eq)
   719     apply (rule **)
   720     apply (auto dest: last_coeffs_not_0)
   721     done
   722 qed
   723 
   724 lemma coeffs_uminus [code abstract]:
   725   "coeffs (- p) = map (\<lambda>a. - a) (coeffs p)"
   726   by (rule coeffs_eqI)
   727     (simp_all add: not_0_coeffs_not_Nil last_map last_coeffs_not_0 nth_default_map_eq nth_default_coeffs_eq)
   728 
   729 lemma [code]:
   730   fixes p q :: "'a::ab_group_add poly"
   731   shows "p - q = p + - q"
   732   by (fact diff_conv_add_uminus)
   733 
   734 lemma poly_add [simp]: "poly (p + q) x = poly p x + poly q x"
   735   apply (induct p arbitrary: q, simp)
   736   apply (case_tac q, simp, simp add: algebra_simps)
   737   done
   738 
   739 lemma poly_minus [simp]:
   740   fixes x :: "'a::comm_ring"
   741   shows "poly (- p) x = - poly p x"
   742   by (induct p) simp_all
   743 
   744 lemma poly_diff [simp]:
   745   fixes x :: "'a::comm_ring"
   746   shows "poly (p - q) x = poly p x - poly q x"
   747   using poly_add [of p "- q" x] by simp
   748 
   749 lemma poly_setsum: "poly (\<Sum>k\<in>A. p k) x = (\<Sum>k\<in>A. poly (p k) x)"
   750   by (induct A rule: infinite_finite_induct) simp_all
   751 
   752 lemma degree_setsum_le: "finite S \<Longrightarrow> (\<And> p . p \<in> S \<Longrightarrow> degree (f p) \<le> n)
   753   \<Longrightarrow> degree (setsum f S) \<le> n"
   754 proof (induct S rule: finite_induct)
   755   case (insert p S)
   756   hence "degree (setsum f S) \<le> n" "degree (f p) \<le> n" by auto
   757   thus ?case unfolding setsum.insert[OF insert(1-2)] by (metis degree_add_le)
   758 qed simp
   759 
   760 lemma poly_as_sum_of_monoms': 
   761   assumes n: "degree p \<le> n" 
   762   shows "(\<Sum>i\<le>n. monom (coeff p i) i) = p"
   763 proof -
   764   have eq: "\<And>i. {..n} \<inter> {i} = (if i \<le> n then {i} else {})"
   765     by auto
   766   show ?thesis
   767     using n by (simp add: poly_eq_iff coeff_setsum coeff_eq_0 setsum.If_cases eq 
   768                   if_distrib[where f="\<lambda>x. x * a" for a])
   769 qed
   770 
   771 lemma poly_as_sum_of_monoms: "(\<Sum>i\<le>degree p. monom (coeff p i) i) = p"
   772   by (intro poly_as_sum_of_monoms' order_refl)
   773 
   774 lemma Poly_snoc: "Poly (xs @ [x]) = Poly xs + monom x (length xs)"
   775   by (induction xs) (simp_all add: monom_0 monom_Suc)
   776 
   777 
   778 subsection \<open>Multiplication by a constant, polynomial multiplication and the unit polynomial\<close>
   779 
   780 lift_definition smult :: "'a::comm_semiring_0 \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
   781   is "\<lambda>a p n. a * coeff p n"
   782 proof -
   783   fix a :: 'a and p :: "'a poly" show "\<forall>\<^sub>\<infinity> i. a * coeff p i = 0"
   784     using MOST_coeff_eq_0[of p] by eventually_elim simp
   785 qed
   786 
   787 lemma coeff_smult [simp]:
   788   "coeff (smult a p) n = a * coeff p n"
   789   by (simp add: smult.rep_eq)
   790 
   791 lemma degree_smult_le: "degree (smult a p) \<le> degree p"
   792   by (rule degree_le, simp add: coeff_eq_0)
   793 
   794 lemma smult_smult [simp]: "smult a (smult b p) = smult (a * b) p"
   795   by (rule poly_eqI, simp add: mult.assoc)
   796 
   797 lemma smult_0_right [simp]: "smult a 0 = 0"
   798   by (rule poly_eqI, simp)
   799 
   800 lemma smult_0_left [simp]: "smult 0 p = 0"
   801   by (rule poly_eqI, simp)
   802 
   803 lemma smult_1_left [simp]: "smult (1::'a::comm_semiring_1) p = p"
   804   by (rule poly_eqI, simp)
   805 
   806 lemma smult_add_right:
   807   "smult a (p + q) = smult a p + smult a q"
   808   by (rule poly_eqI, simp add: algebra_simps)
   809 
   810 lemma smult_add_left:
   811   "smult (a + b) p = smult a p + smult b p"
   812   by (rule poly_eqI, simp add: algebra_simps)
   813 
   814 lemma smult_minus_right [simp]:
   815   "smult (a::'a::comm_ring) (- p) = - smult a p"
   816   by (rule poly_eqI, simp)
   817 
   818 lemma smult_minus_left [simp]:
   819   "smult (- a::'a::comm_ring) p = - smult a p"
   820   by (rule poly_eqI, simp)
   821 
   822 lemma smult_diff_right:
   823   "smult (a::'a::comm_ring) (p - q) = smult a p - smult a q"
   824   by (rule poly_eqI, simp add: algebra_simps)
   825 
   826 lemma smult_diff_left:
   827   "smult (a - b::'a::comm_ring) p = smult a p - smult b p"
   828   by (rule poly_eqI, simp add: algebra_simps)
   829 
   830 lemmas smult_distribs =
   831   smult_add_left smult_add_right
   832   smult_diff_left smult_diff_right
   833 
   834 lemma smult_pCons [simp]:
   835   "smult a (pCons b p) = pCons (a * b) (smult a p)"
   836   by (rule poly_eqI, simp add: coeff_pCons split: nat.split)
   837 
   838 lemma smult_monom: "smult a (monom b n) = monom (a * b) n"
   839   by (induct n, simp add: monom_0, simp add: monom_Suc)
   840 
   841 lemma degree_smult_eq [simp]:
   842   fixes a :: "'a::idom"
   843   shows "degree (smult a p) = (if a = 0 then 0 else degree p)"
   844   by (cases "a = 0", simp, simp add: degree_def)
   845 
   846 lemma smult_eq_0_iff [simp]:
   847   fixes a :: "'a::idom"
   848   shows "smult a p = 0 \<longleftrightarrow> a = 0 \<or> p = 0"
   849   by (simp add: poly_eq_iff)
   850 
   851 lemma coeffs_smult [code abstract]:
   852   fixes p :: "'a::idom poly"
   853   shows "coeffs (smult a p) = (if a = 0 then [] else map (Groups.times a) (coeffs p))"
   854   by (rule coeffs_eqI)
   855     (auto simp add: not_0_coeffs_not_Nil last_map last_coeffs_not_0 nth_default_map_eq nth_default_coeffs_eq)
   856 
   857 instantiation poly :: (comm_semiring_0) comm_semiring_0
   858 begin
   859 
   860 definition
   861   "p * q = fold_coeffs (\<lambda>a p. smult a q + pCons 0 p) p 0"
   862 
   863 lemma mult_poly_0_left: "(0::'a poly) * q = 0"
   864   by (simp add: times_poly_def)
   865 
   866 lemma mult_pCons_left [simp]:
   867   "pCons a p * q = smult a q + pCons 0 (p * q)"
   868   by (cases "p = 0 \<and> a = 0") (auto simp add: times_poly_def)
   869 
   870 lemma mult_poly_0_right: "p * (0::'a poly) = 0"
   871   by (induct p) (simp add: mult_poly_0_left, simp)
   872 
   873 lemma mult_pCons_right [simp]:
   874   "p * pCons a q = smult a p + pCons 0 (p * q)"
   875   by (induct p) (simp add: mult_poly_0_left, simp add: algebra_simps)
   876 
   877 lemmas mult_poly_0 = mult_poly_0_left mult_poly_0_right
   878 
   879 lemma mult_smult_left [simp]:
   880   "smult a p * q = smult a (p * q)"
   881   by (induct p) (simp add: mult_poly_0, simp add: smult_add_right)
   882 
   883 lemma mult_smult_right [simp]:
   884   "p * smult a q = smult a (p * q)"
   885   by (induct q) (simp add: mult_poly_0, simp add: smult_add_right)
   886 
   887 lemma mult_poly_add_left:
   888   fixes p q r :: "'a poly"
   889   shows "(p + q) * r = p * r + q * r"
   890   by (induct r) (simp add: mult_poly_0, simp add: smult_distribs algebra_simps)
   891 
   892 instance
   893 proof
   894   fix p q r :: "'a poly"
   895   show 0: "0 * p = 0"
   896     by (rule mult_poly_0_left)
   897   show "p * 0 = 0"
   898     by (rule mult_poly_0_right)
   899   show "(p + q) * r = p * r + q * r"
   900     by (rule mult_poly_add_left)
   901   show "(p * q) * r = p * (q * r)"
   902     by (induct p, simp add: mult_poly_0, simp add: mult_poly_add_left)
   903   show "p * q = q * p"
   904     by (induct p, simp add: mult_poly_0, simp)
   905 qed
   906 
   907 end
   908 
   909 instance poly :: (comm_semiring_0_cancel) comm_semiring_0_cancel ..
   910 
   911 lemma coeff_mult:
   912   "coeff (p * q) n = (\<Sum>i\<le>n. coeff p i * coeff q (n-i))"
   913 proof (induct p arbitrary: n)
   914   case 0 show ?case by simp
   915 next
   916   case (pCons a p n) thus ?case
   917     by (cases n, simp, simp add: setsum_atMost_Suc_shift
   918                             del: setsum_atMost_Suc)
   919 qed
   920 
   921 lemma degree_mult_le: "degree (p * q) \<le> degree p + degree q"
   922 apply (rule degree_le)
   923 apply (induct p)
   924 apply simp
   925 apply (simp add: coeff_eq_0 coeff_pCons split: nat.split)
   926 done
   927 
   928 lemma mult_monom: "monom a m * monom b n = monom (a * b) (m + n)"
   929   by (induct m) (simp add: monom_0 smult_monom, simp add: monom_Suc)
   930 
   931 instantiation poly :: (comm_semiring_1) comm_semiring_1
   932 begin
   933 
   934 definition one_poly_def: "1 = pCons 1 0"
   935 
   936 instance
   937 proof
   938   show "1 * p = p" for p :: "'a poly"
   939     unfolding one_poly_def by simp
   940   show "0 \<noteq> (1::'a poly)"
   941     unfolding one_poly_def by simp
   942 qed
   943 
   944 end
   945 
   946 instance poly :: (comm_ring) comm_ring ..
   947 
   948 instance poly :: (comm_ring_1) comm_ring_1 ..
   949 
   950 lemma coeff_1 [simp]: "coeff 1 n = (if n = 0 then 1 else 0)"
   951   unfolding one_poly_def
   952   by (simp add: coeff_pCons split: nat.split)
   953 
   954 lemma monom_eq_1 [simp]:
   955   "monom 1 0 = 1"
   956   by (simp add: monom_0 one_poly_def)
   957   
   958 lemma degree_1 [simp]: "degree 1 = 0"
   959   unfolding one_poly_def
   960   by (rule degree_pCons_0)
   961 
   962 lemma coeffs_1_eq [simp, code abstract]:
   963   "coeffs 1 = [1]"
   964   by (simp add: one_poly_def)
   965 
   966 lemma degree_power_le:
   967   "degree (p ^ n) \<le> degree p * n"
   968   by (induct n) (auto intro: order_trans degree_mult_le)
   969 
   970 lemma poly_smult [simp]:
   971   "poly (smult a p) x = a * poly p x"
   972   by (induct p, simp, simp add: algebra_simps)
   973 
   974 lemma poly_mult [simp]:
   975   "poly (p * q) x = poly p x * poly q x"
   976   by (induct p, simp_all, simp add: algebra_simps)
   977 
   978 lemma poly_1 [simp]:
   979   "poly 1 x = 1"
   980   by (simp add: one_poly_def)
   981 
   982 lemma poly_power [simp]:
   983   fixes p :: "'a::{comm_semiring_1} poly"
   984   shows "poly (p ^ n) x = poly p x ^ n"
   985   by (induct n) simp_all
   986 
   987 lemma poly_setprod: "poly (\<Prod>k\<in>A. p k) x = (\<Prod>k\<in>A. poly (p k) x)"
   988   by (induct A rule: infinite_finite_induct) simp_all
   989 
   990 lemma degree_setprod_setsum_le: "finite S \<Longrightarrow> degree (setprod f S) \<le> setsum (degree o f) S"
   991 proof (induct S rule: finite_induct)
   992   case (insert a S)
   993   show ?case unfolding setprod.insert[OF insert(1-2)] setsum.insert[OF insert(1-2)]
   994     by (rule le_trans[OF degree_mult_le], insert insert, auto)
   995 qed simp
   996 
   997 subsection \<open>Conversions from natural numbers\<close>
   998 
   999 lemma of_nat_poly: "of_nat n = [:of_nat n :: 'a :: comm_semiring_1:]"
  1000 proof (induction n)
  1001   case (Suc n)
  1002   hence "of_nat (Suc n) = 1 + (of_nat n :: 'a poly)" 
  1003     by simp
  1004   also have "(of_nat n :: 'a poly) = [: of_nat n :]" 
  1005     by (subst Suc) (rule refl)
  1006   also have "1 = [:1:]" by (simp add: one_poly_def)
  1007   finally show ?case by (subst (asm) add_pCons) simp
  1008 qed simp
  1009 
  1010 lemma degree_of_nat [simp]: "degree (of_nat n) = 0"
  1011   by (simp add: of_nat_poly)
  1012 
  1013 lemma degree_numeral [simp]: "degree (numeral n) = 0"
  1014   by (subst of_nat_numeral [symmetric], subst of_nat_poly) simp
  1015 
  1016 lemma numeral_poly: "numeral n = [:numeral n:]"
  1017   by (subst of_nat_numeral [symmetric], subst of_nat_poly) simp
  1018 
  1019 subsection \<open>Lemmas about divisibility\<close>
  1020 
  1021 lemma dvd_smult: "p dvd q \<Longrightarrow> p dvd smult a q"
  1022 proof -
  1023   assume "p dvd q"
  1024   then obtain k where "q = p * k" ..
  1025   then have "smult a q = p * smult a k" by simp
  1026   then show "p dvd smult a q" ..
  1027 qed
  1028 
  1029 lemma dvd_smult_cancel:
  1030   fixes a :: "'a :: field"
  1031   shows "p dvd smult a q \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> p dvd q"
  1032   by (drule dvd_smult [where a="inverse a"]) simp
  1033 
  1034 lemma dvd_smult_iff:
  1035   fixes a :: "'a::field"
  1036   shows "a \<noteq> 0 \<Longrightarrow> p dvd smult a q \<longleftrightarrow> p dvd q"
  1037   by (safe elim!: dvd_smult dvd_smult_cancel)
  1038 
  1039 lemma smult_dvd_cancel:
  1040   "smult a p dvd q \<Longrightarrow> p dvd q"
  1041 proof -
  1042   assume "smult a p dvd q"
  1043   then obtain k where "q = smult a p * k" ..
  1044   then have "q = p * smult a k" by simp
  1045   then show "p dvd q" ..
  1046 qed
  1047 
  1048 lemma smult_dvd:
  1049   fixes a :: "'a::field"
  1050   shows "p dvd q \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> smult a p dvd q"
  1051   by (rule smult_dvd_cancel [where a="inverse a"]) simp
  1052 
  1053 lemma smult_dvd_iff:
  1054   fixes a :: "'a::field"
  1055   shows "smult a p dvd q \<longleftrightarrow> (if a = 0 then q = 0 else p dvd q)"
  1056   by (auto elim: smult_dvd smult_dvd_cancel)
  1057 
  1058 
  1059 subsection \<open>Polynomials form an integral domain\<close>
  1060 
  1061 lemma coeff_mult_degree_sum:
  1062   "coeff (p * q) (degree p + degree q) =
  1063    coeff p (degree p) * coeff q (degree q)"
  1064   by (induct p, simp, simp add: coeff_eq_0)
  1065 
  1066 instance poly :: (idom) idom
  1067 proof
  1068   fix p q :: "'a poly"
  1069   assume "p \<noteq> 0" and "q \<noteq> 0"
  1070   have "coeff (p * q) (degree p + degree q) =
  1071         coeff p (degree p) * coeff q (degree q)"
  1072     by (rule coeff_mult_degree_sum)
  1073   also have "coeff p (degree p) * coeff q (degree q) \<noteq> 0"
  1074     using \<open>p \<noteq> 0\<close> and \<open>q \<noteq> 0\<close> by simp
  1075   finally have "\<exists>n. coeff (p * q) n \<noteq> 0" ..
  1076   thus "p * q \<noteq> 0" by (simp add: poly_eq_iff)
  1077 qed
  1078 
  1079 lemma degree_mult_eq:
  1080   fixes p q :: "'a::semidom poly"
  1081   shows "\<lbrakk>p \<noteq> 0; q \<noteq> 0\<rbrakk> \<Longrightarrow> degree (p * q) = degree p + degree q"
  1082 apply (rule order_antisym [OF degree_mult_le le_degree])
  1083 apply (simp add: coeff_mult_degree_sum)
  1084 done
  1085 
  1086 lemma degree_mult_right_le:
  1087   fixes p q :: "'a::semidom poly"
  1088   assumes "q \<noteq> 0"
  1089   shows "degree p \<le> degree (p * q)"
  1090   using assms by (cases "p = 0") (simp_all add: degree_mult_eq)
  1091 
  1092 lemma coeff_degree_mult:
  1093   fixes p q :: "'a::semidom poly"
  1094   shows "coeff (p * q) (degree (p * q)) =
  1095     coeff q (degree q) * coeff p (degree p)"
  1096   by (cases "p = 0 \<or> q = 0") (auto simp add: degree_mult_eq coeff_mult_degree_sum mult_ac)
  1097 
  1098 lemma dvd_imp_degree_le:
  1099   fixes p q :: "'a::semidom poly"
  1100   shows "\<lbrakk>p dvd q; q \<noteq> 0\<rbrakk> \<Longrightarrow> degree p \<le> degree q"
  1101   by (erule dvdE, hypsubst, subst degree_mult_eq) auto
  1102 
  1103 lemma divides_degree:
  1104   assumes pq: "p dvd (q :: 'a :: semidom poly)"
  1105   shows "degree p \<le> degree q \<or> q = 0"
  1106   by (metis dvd_imp_degree_le pq)
  1107 
  1108 subsection \<open>Polynomials form an ordered integral domain\<close>
  1109 
  1110 definition pos_poly :: "'a::linordered_idom poly \<Rightarrow> bool"
  1111 where
  1112   "pos_poly p \<longleftrightarrow> 0 < coeff p (degree p)"
  1113 
  1114 lemma pos_poly_pCons:
  1115   "pos_poly (pCons a p) \<longleftrightarrow> pos_poly p \<or> (p = 0 \<and> 0 < a)"
  1116   unfolding pos_poly_def by simp
  1117 
  1118 lemma not_pos_poly_0 [simp]: "\<not> pos_poly 0"
  1119   unfolding pos_poly_def by simp
  1120 
  1121 lemma pos_poly_add: "\<lbrakk>pos_poly p; pos_poly q\<rbrakk> \<Longrightarrow> pos_poly (p + q)"
  1122   apply (induct p arbitrary: q, simp)
  1123   apply (case_tac q, force simp add: pos_poly_pCons add_pos_pos)
  1124   done
  1125 
  1126 lemma pos_poly_mult: "\<lbrakk>pos_poly p; pos_poly q\<rbrakk> \<Longrightarrow> pos_poly (p * q)"
  1127   unfolding pos_poly_def
  1128   apply (subgoal_tac "p \<noteq> 0 \<and> q \<noteq> 0")
  1129   apply (simp add: degree_mult_eq coeff_mult_degree_sum)
  1130   apply auto
  1131   done
  1132 
  1133 lemma pos_poly_total: "p = 0 \<or> pos_poly p \<or> pos_poly (- p)"
  1134 by (induct p) (auto simp add: pos_poly_pCons)
  1135 
  1136 lemma last_coeffs_eq_coeff_degree:
  1137   "p \<noteq> 0 \<Longrightarrow> last (coeffs p) = coeff p (degree p)"
  1138   by (simp add: coeffs_def)
  1139 
  1140 lemma pos_poly_coeffs [code]:
  1141   "pos_poly p \<longleftrightarrow> (let as = coeffs p in as \<noteq> [] \<and> last as > 0)" (is "?P \<longleftrightarrow> ?Q")
  1142 proof
  1143   assume ?Q then show ?P by (auto simp add: pos_poly_def last_coeffs_eq_coeff_degree)
  1144 next
  1145   assume ?P then have *: "0 < coeff p (degree p)" by (simp add: pos_poly_def)
  1146   then have "p \<noteq> 0" by auto
  1147   with * show ?Q by (simp add: last_coeffs_eq_coeff_degree)
  1148 qed
  1149 
  1150 instantiation poly :: (linordered_idom) linordered_idom
  1151 begin
  1152 
  1153 definition
  1154   "x < y \<longleftrightarrow> pos_poly (y - x)"
  1155 
  1156 definition
  1157   "x \<le> y \<longleftrightarrow> x = y \<or> pos_poly (y - x)"
  1158 
  1159 definition
  1160   "\<bar>x::'a poly\<bar> = (if x < 0 then - x else x)"
  1161 
  1162 definition
  1163   "sgn (x::'a poly) = (if x = 0 then 0 else if 0 < x then 1 else - 1)"
  1164 
  1165 instance
  1166 proof
  1167   fix x y z :: "'a poly"
  1168   show "x < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x"
  1169     unfolding less_eq_poly_def less_poly_def
  1170     apply safe
  1171     apply simp
  1172     apply (drule (1) pos_poly_add)
  1173     apply simp
  1174     done
  1175   show "x \<le> x"
  1176     unfolding less_eq_poly_def by simp
  1177   show "x \<le> y \<Longrightarrow> y \<le> z \<Longrightarrow> x \<le> z"
  1178     unfolding less_eq_poly_def
  1179     apply safe
  1180     apply (drule (1) pos_poly_add)
  1181     apply (simp add: algebra_simps)
  1182     done
  1183   show "x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x = y"
  1184     unfolding less_eq_poly_def
  1185     apply safe
  1186     apply (drule (1) pos_poly_add)
  1187     apply simp
  1188     done
  1189   show "x \<le> y \<Longrightarrow> z + x \<le> z + y"
  1190     unfolding less_eq_poly_def
  1191     apply safe
  1192     apply (simp add: algebra_simps)
  1193     done
  1194   show "x \<le> y \<or> y \<le> x"
  1195     unfolding less_eq_poly_def
  1196     using pos_poly_total [of "x - y"]
  1197     by auto
  1198   show "x < y \<Longrightarrow> 0 < z \<Longrightarrow> z * x < z * y"
  1199     unfolding less_poly_def
  1200     by (simp add: right_diff_distrib [symmetric] pos_poly_mult)
  1201   show "\<bar>x\<bar> = (if x < 0 then - x else x)"
  1202     by (rule abs_poly_def)
  1203   show "sgn x = (if x = 0 then 0 else if 0 < x then 1 else - 1)"
  1204     by (rule sgn_poly_def)
  1205 qed
  1206 
  1207 end
  1208 
  1209 text \<open>TODO: Simplification rules for comparisons\<close>
  1210 
  1211 
  1212 subsection \<open>Synthetic division and polynomial roots\<close>
  1213 
  1214 text \<open>
  1215   Synthetic division is simply division by the linear polynomial @{term "x - c"}.
  1216 \<close>
  1217 
  1218 definition synthetic_divmod :: "'a::comm_semiring_0 poly \<Rightarrow> 'a \<Rightarrow> 'a poly \<times> 'a"
  1219 where
  1220   "synthetic_divmod p c = fold_coeffs (\<lambda>a (q, r). (pCons r q, a + c * r)) p (0, 0)"
  1221 
  1222 definition synthetic_div :: "'a::comm_semiring_0 poly \<Rightarrow> 'a \<Rightarrow> 'a poly"
  1223 where
  1224   "synthetic_div p c = fst (synthetic_divmod p c)"
  1225 
  1226 lemma synthetic_divmod_0 [simp]:
  1227   "synthetic_divmod 0 c = (0, 0)"
  1228   by (simp add: synthetic_divmod_def)
  1229 
  1230 lemma synthetic_divmod_pCons [simp]:
  1231   "synthetic_divmod (pCons a p) c = (\<lambda>(q, r). (pCons r q, a + c * r)) (synthetic_divmod p c)"
  1232   by (cases "p = 0 \<and> a = 0") (auto simp add: synthetic_divmod_def)
  1233 
  1234 lemma synthetic_div_0 [simp]:
  1235   "synthetic_div 0 c = 0"
  1236   unfolding synthetic_div_def by simp
  1237 
  1238 lemma synthetic_div_unique_lemma: "smult c p = pCons a p \<Longrightarrow> p = 0"
  1239 by (induct p arbitrary: a) simp_all
  1240 
  1241 lemma snd_synthetic_divmod:
  1242   "snd (synthetic_divmod p c) = poly p c"
  1243   by (induct p, simp, simp add: split_def)
  1244 
  1245 lemma synthetic_div_pCons [simp]:
  1246   "synthetic_div (pCons a p) c = pCons (poly p c) (synthetic_div p c)"
  1247   unfolding synthetic_div_def
  1248   by (simp add: split_def snd_synthetic_divmod)
  1249 
  1250 lemma synthetic_div_eq_0_iff:
  1251   "synthetic_div p c = 0 \<longleftrightarrow> degree p = 0"
  1252   by (induct p, simp, case_tac p, simp)
  1253 
  1254 lemma degree_synthetic_div:
  1255   "degree (synthetic_div p c) = degree p - 1"
  1256   by (induct p, simp, simp add: synthetic_div_eq_0_iff)
  1257 
  1258 lemma synthetic_div_correct:
  1259   "p + smult c (synthetic_div p c) = pCons (poly p c) (synthetic_div p c)"
  1260   by (induct p) simp_all
  1261 
  1262 lemma synthetic_div_unique:
  1263   "p + smult c q = pCons r q \<Longrightarrow> r = poly p c \<and> q = synthetic_div p c"
  1264 apply (induct p arbitrary: q r)
  1265 apply (simp, frule synthetic_div_unique_lemma, simp)
  1266 apply (case_tac q, force)
  1267 done
  1268 
  1269 lemma synthetic_div_correct':
  1270   fixes c :: "'a::comm_ring_1"
  1271   shows "[:-c, 1:] * synthetic_div p c + [:poly p c:] = p"
  1272   using synthetic_div_correct [of p c]
  1273   by (simp add: algebra_simps)
  1274 
  1275 lemma poly_eq_0_iff_dvd:
  1276   fixes c :: "'a::idom"
  1277   shows "poly p c = 0 \<longleftrightarrow> [:-c, 1:] dvd p"
  1278 proof
  1279   assume "poly p c = 0"
  1280   with synthetic_div_correct' [of c p]
  1281   have "p = [:-c, 1:] * synthetic_div p c" by simp
  1282   then show "[:-c, 1:] dvd p" ..
  1283 next
  1284   assume "[:-c, 1:] dvd p"
  1285   then obtain k where "p = [:-c, 1:] * k" by (rule dvdE)
  1286   then show "poly p c = 0" by simp
  1287 qed
  1288 
  1289 lemma dvd_iff_poly_eq_0:
  1290   fixes c :: "'a::idom"
  1291   shows "[:c, 1:] dvd p \<longleftrightarrow> poly p (-c) = 0"
  1292   by (simp add: poly_eq_0_iff_dvd)
  1293 
  1294 lemma poly_roots_finite:
  1295   fixes p :: "'a::idom poly"
  1296   shows "p \<noteq> 0 \<Longrightarrow> finite {x. poly p x = 0}"
  1297 proof (induct n \<equiv> "degree p" arbitrary: p)
  1298   case (0 p)
  1299   then obtain a where "a \<noteq> 0" and "p = [:a:]"
  1300     by (cases p, simp split: if_splits)
  1301   then show "finite {x. poly p x = 0}" by simp
  1302 next
  1303   case (Suc n p)
  1304   show "finite {x. poly p x = 0}"
  1305   proof (cases "\<exists>x. poly p x = 0")
  1306     case False
  1307     then show "finite {x. poly p x = 0}" by simp
  1308   next
  1309     case True
  1310     then obtain a where "poly p a = 0" ..
  1311     then have "[:-a, 1:] dvd p" by (simp only: poly_eq_0_iff_dvd)
  1312     then obtain k where k: "p = [:-a, 1:] * k" ..
  1313     with \<open>p \<noteq> 0\<close> have "k \<noteq> 0" by auto
  1314     with k have "degree p = Suc (degree k)"
  1315       by (simp add: degree_mult_eq del: mult_pCons_left)
  1316     with \<open>Suc n = degree p\<close> have "n = degree k" by simp
  1317     then have "finite {x. poly k x = 0}" using \<open>k \<noteq> 0\<close> by (rule Suc.hyps)
  1318     then have "finite (insert a {x. poly k x = 0})" by simp
  1319     then show "finite {x. poly p x = 0}"
  1320       by (simp add: k Collect_disj_eq del: mult_pCons_left)
  1321   qed
  1322 qed
  1323 
  1324 lemma poly_eq_poly_eq_iff:
  1325   fixes p q :: "'a::{idom,ring_char_0} poly"
  1326   shows "poly p = poly q \<longleftrightarrow> p = q" (is "?P \<longleftrightarrow> ?Q")
  1327 proof
  1328   assume ?Q then show ?P by simp
  1329 next
  1330   { fix p :: "'a::{idom,ring_char_0} poly"
  1331     have "poly p = poly 0 \<longleftrightarrow> p = 0"
  1332       apply (cases "p = 0", simp_all)
  1333       apply (drule poly_roots_finite)
  1334       apply (auto simp add: infinite_UNIV_char_0)
  1335       done
  1336   } note this [of "p - q"]
  1337   moreover assume ?P
  1338   ultimately show ?Q by auto
  1339 qed
  1340 
  1341 lemma poly_all_0_iff_0:
  1342   fixes p :: "'a::{ring_char_0, idom} poly"
  1343   shows "(\<forall>x. poly p x = 0) \<longleftrightarrow> p = 0"
  1344   by (auto simp add: poly_eq_poly_eq_iff [symmetric])
  1345 
  1346 
  1347 subsection \<open>Long division of polynomials\<close>
  1348 
  1349 definition pdivmod_rel :: "'a::field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<Rightarrow> bool"
  1350 where
  1351   "pdivmod_rel x y q r \<longleftrightarrow>
  1352     x = q * y + r \<and> (if y = 0 then q = 0 else r = 0 \<or> degree r < degree y)"
  1353 
  1354 lemma pdivmod_rel_0:
  1355   "pdivmod_rel 0 y 0 0"
  1356   unfolding pdivmod_rel_def by simp
  1357 
  1358 lemma pdivmod_rel_by_0:
  1359   "pdivmod_rel x 0 0 x"
  1360   unfolding pdivmod_rel_def by simp
  1361 
  1362 lemma eq_zero_or_degree_less:
  1363   assumes "degree p \<le> n" and "coeff p n = 0"
  1364   shows "p = 0 \<or> degree p < n"
  1365 proof (cases n)
  1366   case 0
  1367   with \<open>degree p \<le> n\<close> and \<open>coeff p n = 0\<close>
  1368   have "coeff p (degree p) = 0" by simp
  1369   then have "p = 0" by simp
  1370   then show ?thesis ..
  1371 next
  1372   case (Suc m)
  1373   have "\<forall>i>n. coeff p i = 0"
  1374     using \<open>degree p \<le> n\<close> by (simp add: coeff_eq_0)
  1375   then have "\<forall>i\<ge>n. coeff p i = 0"
  1376     using \<open>coeff p n = 0\<close> by (simp add: le_less)
  1377   then have "\<forall>i>m. coeff p i = 0"
  1378     using \<open>n = Suc m\<close> by (simp add: less_eq_Suc_le)
  1379   then have "degree p \<le> m"
  1380     by (rule degree_le)
  1381   then have "degree p < n"
  1382     using \<open>n = Suc m\<close> by (simp add: less_Suc_eq_le)
  1383   then show ?thesis ..
  1384 qed
  1385 
  1386 lemma pdivmod_rel_pCons:
  1387   assumes rel: "pdivmod_rel x y q r"
  1388   assumes y: "y \<noteq> 0"
  1389   assumes b: "b = coeff (pCons a r) (degree y) / coeff y (degree y)"
  1390   shows "pdivmod_rel (pCons a x) y (pCons b q) (pCons a r - smult b y)"
  1391     (is "pdivmod_rel ?x y ?q ?r")
  1392 proof -
  1393   have x: "x = q * y + r" and r: "r = 0 \<or> degree r < degree y"
  1394     using assms unfolding pdivmod_rel_def by simp_all
  1395 
  1396   have 1: "?x = ?q * y + ?r"
  1397     using b x by simp
  1398 
  1399   have 2: "?r = 0 \<or> degree ?r < degree y"
  1400   proof (rule eq_zero_or_degree_less)
  1401     show "degree ?r \<le> degree y"
  1402     proof (rule degree_diff_le)
  1403       show "degree (pCons a r) \<le> degree y"
  1404         using r by auto
  1405       show "degree (smult b y) \<le> degree y"
  1406         by (rule degree_smult_le)
  1407     qed
  1408   next
  1409     show "coeff ?r (degree y) = 0"
  1410       using \<open>y \<noteq> 0\<close> unfolding b by simp
  1411   qed
  1412 
  1413   from 1 2 show ?thesis
  1414     unfolding pdivmod_rel_def
  1415     using \<open>y \<noteq> 0\<close> by simp
  1416 qed
  1417 
  1418 lemma pdivmod_rel_exists: "\<exists>q r. pdivmod_rel x y q r"
  1419 apply (cases "y = 0")
  1420 apply (fast intro!: pdivmod_rel_by_0)
  1421 apply (induct x)
  1422 apply (fast intro!: pdivmod_rel_0)
  1423 apply (fast intro!: pdivmod_rel_pCons)
  1424 done
  1425 
  1426 lemma pdivmod_rel_unique:
  1427   assumes 1: "pdivmod_rel x y q1 r1"
  1428   assumes 2: "pdivmod_rel x y q2 r2"
  1429   shows "q1 = q2 \<and> r1 = r2"
  1430 proof (cases "y = 0")
  1431   assume "y = 0" with assms show ?thesis
  1432     by (simp add: pdivmod_rel_def)
  1433 next
  1434   assume [simp]: "y \<noteq> 0"
  1435   from 1 have q1: "x = q1 * y + r1" and r1: "r1 = 0 \<or> degree r1 < degree y"
  1436     unfolding pdivmod_rel_def by simp_all
  1437   from 2 have q2: "x = q2 * y + r2" and r2: "r2 = 0 \<or> degree r2 < degree y"
  1438     unfolding pdivmod_rel_def by simp_all
  1439   from q1 q2 have q3: "(q1 - q2) * y = r2 - r1"
  1440     by (simp add: algebra_simps)
  1441   from r1 r2 have r3: "(r2 - r1) = 0 \<or> degree (r2 - r1) < degree y"
  1442     by (auto intro: degree_diff_less)
  1443 
  1444   show "q1 = q2 \<and> r1 = r2"
  1445   proof (rule ccontr)
  1446     assume "\<not> (q1 = q2 \<and> r1 = r2)"
  1447     with q3 have "q1 \<noteq> q2" and "r1 \<noteq> r2" by auto
  1448     with r3 have "degree (r2 - r1) < degree y" by simp
  1449     also have "degree y \<le> degree (q1 - q2) + degree y" by simp
  1450     also have "\<dots> = degree ((q1 - q2) * y)"
  1451       using \<open>q1 \<noteq> q2\<close> by (simp add: degree_mult_eq)
  1452     also have "\<dots> = degree (r2 - r1)"
  1453       using q3 by simp
  1454     finally have "degree (r2 - r1) < degree (r2 - r1)" .
  1455     then show "False" by simp
  1456   qed
  1457 qed
  1458 
  1459 lemma pdivmod_rel_0_iff: "pdivmod_rel 0 y q r \<longleftrightarrow> q = 0 \<and> r = 0"
  1460 by (auto dest: pdivmod_rel_unique intro: pdivmod_rel_0)
  1461 
  1462 lemma pdivmod_rel_by_0_iff: "pdivmod_rel x 0 q r \<longleftrightarrow> q = 0 \<and> r = x"
  1463 by (auto dest: pdivmod_rel_unique intro: pdivmod_rel_by_0)
  1464 
  1465 lemmas pdivmod_rel_unique_div = pdivmod_rel_unique [THEN conjunct1]
  1466 
  1467 lemmas pdivmod_rel_unique_mod = pdivmod_rel_unique [THEN conjunct2]
  1468 
  1469 instantiation poly :: (field) ring_div
  1470 begin
  1471 
  1472 definition divide_poly where
  1473   div_poly_def: "x div y = (THE q. \<exists>r. pdivmod_rel x y q r)"
  1474 
  1475 definition mod_poly where
  1476   "x mod y = (THE r. \<exists>q. pdivmod_rel x y q r)"
  1477 
  1478 lemma div_poly_eq:
  1479   "pdivmod_rel x y q r \<Longrightarrow> x div y = q"
  1480 unfolding div_poly_def
  1481 by (fast elim: pdivmod_rel_unique_div)
  1482 
  1483 lemma mod_poly_eq:
  1484   "pdivmod_rel x y q r \<Longrightarrow> x mod y = r"
  1485 unfolding mod_poly_def
  1486 by (fast elim: pdivmod_rel_unique_mod)
  1487 
  1488 lemma pdivmod_rel:
  1489   "pdivmod_rel x y (x div y) (x mod y)"
  1490 proof -
  1491   from pdivmod_rel_exists
  1492     obtain q r where "pdivmod_rel x y q r" by fast
  1493   thus ?thesis
  1494     by (simp add: div_poly_eq mod_poly_eq)
  1495 qed
  1496 
  1497 instance
  1498 proof
  1499   fix x y :: "'a poly"
  1500   show "x div y * y + x mod y = x"
  1501     using pdivmod_rel [of x y]
  1502     by (simp add: pdivmod_rel_def)
  1503 next
  1504   fix x :: "'a poly"
  1505   have "pdivmod_rel x 0 0 x"
  1506     by (rule pdivmod_rel_by_0)
  1507   thus "x div 0 = 0"
  1508     by (rule div_poly_eq)
  1509 next
  1510   fix y :: "'a poly"
  1511   have "pdivmod_rel 0 y 0 0"
  1512     by (rule pdivmod_rel_0)
  1513   thus "0 div y = 0"
  1514     by (rule div_poly_eq)
  1515 next
  1516   fix x y z :: "'a poly"
  1517   assume "y \<noteq> 0"
  1518   hence "pdivmod_rel (x + z * y) y (z + x div y) (x mod y)"
  1519     using pdivmod_rel [of x y]
  1520     by (simp add: pdivmod_rel_def distrib_right)
  1521   thus "(x + z * y) div y = z + x div y"
  1522     by (rule div_poly_eq)
  1523 next
  1524   fix x y z :: "'a poly"
  1525   assume "x \<noteq> 0"
  1526   show "(x * y) div (x * z) = y div z"
  1527   proof (cases "y \<noteq> 0 \<and> z \<noteq> 0")
  1528     have "\<And>x::'a poly. pdivmod_rel x 0 0 x"
  1529       by (rule pdivmod_rel_by_0)
  1530     then have [simp]: "\<And>x::'a poly. x div 0 = 0"
  1531       by (rule div_poly_eq)
  1532     have "\<And>x::'a poly. pdivmod_rel 0 x 0 0"
  1533       by (rule pdivmod_rel_0)
  1534     then have [simp]: "\<And>x::'a poly. 0 div x = 0"
  1535       by (rule div_poly_eq)
  1536     case False then show ?thesis by auto
  1537   next
  1538     case True then have "y \<noteq> 0" and "z \<noteq> 0" by auto
  1539     with \<open>x \<noteq> 0\<close>
  1540     have "\<And>q r. pdivmod_rel y z q r \<Longrightarrow> pdivmod_rel (x * y) (x * z) q (x * r)"
  1541       by (auto simp add: pdivmod_rel_def algebra_simps)
  1542         (rule classical, simp add: degree_mult_eq)
  1543     moreover from pdivmod_rel have "pdivmod_rel y z (y div z) (y mod z)" .
  1544     ultimately have "pdivmod_rel (x * y) (x * z) (y div z) (x * (y mod z))" .
  1545     then show ?thesis by (simp add: div_poly_eq)
  1546   qed
  1547 qed
  1548 
  1549 end
  1550 
  1551 lemma is_unit_monom_0:
  1552   fixes a :: "'a::field"
  1553   assumes "a \<noteq> 0"
  1554   shows "is_unit (monom a 0)"
  1555 proof
  1556   from assms show "1 = monom a 0 * monom (inverse a) 0"
  1557     by (simp add: mult_monom)
  1558 qed
  1559 
  1560 lemma is_unit_triv:
  1561   fixes a :: "'a::field"
  1562   assumes "a \<noteq> 0"
  1563   shows "is_unit [:a:]"
  1564   using assms by (simp add: is_unit_monom_0 monom_0 [symmetric])
  1565 
  1566 lemma is_unit_iff_degree:
  1567   assumes "p \<noteq> 0"
  1568   shows "is_unit p \<longleftrightarrow> degree p = 0" (is "?P \<longleftrightarrow> ?Q")
  1569 proof
  1570   assume ?Q
  1571   then obtain a where "p = [:a:]" by (rule degree_eq_zeroE)
  1572   with assms show ?P by (simp add: is_unit_triv)
  1573 next
  1574   assume ?P
  1575   then obtain q where "q \<noteq> 0" "p * q = 1" ..
  1576   then have "degree (p * q) = degree 1"
  1577     by simp
  1578   with \<open>p \<noteq> 0\<close> \<open>q \<noteq> 0\<close> have "degree p + degree q = 0"
  1579     by (simp add: degree_mult_eq)
  1580   then show ?Q by simp
  1581 qed
  1582 
  1583 lemma is_unit_pCons_iff:
  1584   "is_unit (pCons a p) \<longleftrightarrow> p = 0 \<and> a \<noteq> 0" (is "?P \<longleftrightarrow> ?Q")
  1585   by (cases "p = 0") (auto simp add: is_unit_triv is_unit_iff_degree)
  1586 
  1587 lemma is_unit_monom_trival:
  1588   fixes p :: "'a::field poly"
  1589   assumes "is_unit p"
  1590   shows "monom (coeff p (degree p)) 0 = p"
  1591   using assms by (cases p) (simp_all add: monom_0 is_unit_pCons_iff)
  1592 
  1593 lemma is_unit_polyE:
  1594   assumes "is_unit p"
  1595   obtains a where "p = monom a 0" and "a \<noteq> 0"
  1596 proof -
  1597   obtain a q where "p = pCons a q" by (cases p)
  1598   with assms have "p = [:a:]" and "a \<noteq> 0"
  1599     by (simp_all add: is_unit_pCons_iff)
  1600   with that show thesis by (simp add: monom_0)
  1601 qed
  1602 
  1603 instantiation poly :: (field) normalization_semidom
  1604 begin
  1605 
  1606 definition normalize_poly :: "'a poly \<Rightarrow> 'a poly"
  1607   where "normalize_poly p = smult (inverse (coeff p (degree p))) p"
  1608 
  1609 definition unit_factor_poly :: "'a poly \<Rightarrow> 'a poly"
  1610   where "unit_factor_poly p = monom (coeff p (degree p)) 0"
  1611 
  1612 instance
  1613 proof
  1614   fix p :: "'a poly"
  1615   show "unit_factor p * normalize p = p"
  1616     by (cases "p = 0")
  1617       (simp_all add: normalize_poly_def unit_factor_poly_def,
  1618       simp only: mult_smult_left [symmetric] smult_monom, simp)
  1619 next
  1620   show "normalize 0 = (0::'a poly)"
  1621     by (simp add: normalize_poly_def)
  1622 next
  1623   show "unit_factor 0 = (0::'a poly)"
  1624     by (simp add: unit_factor_poly_def)
  1625 next
  1626   fix p :: "'a poly"
  1627   assume "is_unit p"
  1628   then obtain a where "p = monom a 0" and "a \<noteq> 0"
  1629     by (rule is_unit_polyE)
  1630   then show "normalize p = 1"
  1631     by (auto simp add: normalize_poly_def smult_monom degree_monom_eq)
  1632 next
  1633   fix p q :: "'a poly"
  1634   assume "q \<noteq> 0"
  1635   from \<open>q \<noteq> 0\<close> have "is_unit (monom (coeff q (degree q)) 0)"
  1636     by (auto intro: is_unit_monom_0)
  1637   then show "is_unit (unit_factor q)"
  1638     by (simp add: unit_factor_poly_def)
  1639 next
  1640   fix p q :: "'a poly"
  1641   have "monom (coeff (p * q) (degree (p * q))) 0 =
  1642     monom (coeff p (degree p)) 0 * monom (coeff q (degree q)) 0"
  1643     by (simp add: monom_0 coeff_degree_mult)
  1644   then show "unit_factor (p * q) =
  1645     unit_factor p * unit_factor q"
  1646     by (simp add: unit_factor_poly_def)
  1647 qed
  1648 
  1649 end
  1650 
  1651 lemma unit_factor_monom [simp]:
  1652   "unit_factor (monom a n) =
  1653      (if a = 0 then 0 else monom a 0)"
  1654   by (simp add: unit_factor_poly_def degree_monom_eq)
  1655 
  1656 lemma unit_factor_pCons [simp]:
  1657   "unit_factor (pCons a p) =
  1658      (if p = 0 then monom a 0 else unit_factor p)"
  1659   by (simp add: unit_factor_poly_def)
  1660 
  1661 lemma normalize_monom [simp]:
  1662   "normalize (monom a n) =
  1663      (if a = 0 then 0 else monom 1 n)"
  1664   by (simp add: normalize_poly_def degree_monom_eq smult_monom)
  1665 
  1666 lemma degree_mod_less:
  1667   "y \<noteq> 0 \<Longrightarrow> x mod y = 0 \<or> degree (x mod y) < degree y"
  1668   using pdivmod_rel [of x y]
  1669   unfolding pdivmod_rel_def by simp
  1670 
  1671 lemma div_poly_less: "degree x < degree y \<Longrightarrow> x div y = 0"
  1672 proof -
  1673   assume "degree x < degree y"
  1674   hence "pdivmod_rel x y 0 x"
  1675     by (simp add: pdivmod_rel_def)
  1676   thus "x div y = 0" by (rule div_poly_eq)
  1677 qed
  1678 
  1679 lemma mod_poly_less: "degree x < degree y \<Longrightarrow> x mod y = x"
  1680 proof -
  1681   assume "degree x < degree y"
  1682   hence "pdivmod_rel x y 0 x"
  1683     by (simp add: pdivmod_rel_def)
  1684   thus "x mod y = x" by (rule mod_poly_eq)
  1685 qed
  1686 
  1687 lemma pdivmod_rel_smult_left:
  1688   "pdivmod_rel x y q r
  1689     \<Longrightarrow> pdivmod_rel (smult a x) y (smult a q) (smult a r)"
  1690   unfolding pdivmod_rel_def by (simp add: smult_add_right)
  1691 
  1692 lemma div_smult_left: "(smult a x) div y = smult a (x div y)"
  1693   by (rule div_poly_eq, rule pdivmod_rel_smult_left, rule pdivmod_rel)
  1694 
  1695 lemma mod_smult_left: "(smult a x) mod y = smult a (x mod y)"
  1696   by (rule mod_poly_eq, rule pdivmod_rel_smult_left, rule pdivmod_rel)
  1697 
  1698 lemma poly_div_minus_left [simp]:
  1699   fixes x y :: "'a::field poly"
  1700   shows "(- x) div y = - (x div y)"
  1701   using div_smult_left [of "- 1::'a"] by simp
  1702 
  1703 lemma poly_mod_minus_left [simp]:
  1704   fixes x y :: "'a::field poly"
  1705   shows "(- x) mod y = - (x mod y)"
  1706   using mod_smult_left [of "- 1::'a"] by simp
  1707 
  1708 lemma pdivmod_rel_add_left:
  1709   assumes "pdivmod_rel x y q r"
  1710   assumes "pdivmod_rel x' y q' r'"
  1711   shows "pdivmod_rel (x + x') y (q + q') (r + r')"
  1712   using assms unfolding pdivmod_rel_def
  1713   by (auto simp add: algebra_simps degree_add_less)
  1714 
  1715 lemma poly_div_add_left:
  1716   fixes x y z :: "'a::field poly"
  1717   shows "(x + y) div z = x div z + y div z"
  1718   using pdivmod_rel_add_left [OF pdivmod_rel pdivmod_rel]
  1719   by (rule div_poly_eq)
  1720 
  1721 lemma poly_mod_add_left:
  1722   fixes x y z :: "'a::field poly"
  1723   shows "(x + y) mod z = x mod z + y mod z"
  1724   using pdivmod_rel_add_left [OF pdivmod_rel pdivmod_rel]
  1725   by (rule mod_poly_eq)
  1726 
  1727 lemma poly_div_diff_left:
  1728   fixes x y z :: "'a::field poly"
  1729   shows "(x - y) div z = x div z - y div z"
  1730   by (simp only: diff_conv_add_uminus poly_div_add_left poly_div_minus_left)
  1731 
  1732 lemma poly_mod_diff_left:
  1733   fixes x y z :: "'a::field poly"
  1734   shows "(x - y) mod z = x mod z - y mod z"
  1735   by (simp only: diff_conv_add_uminus poly_mod_add_left poly_mod_minus_left)
  1736 
  1737 lemma pdivmod_rel_smult_right:
  1738   "\<lbrakk>a \<noteq> 0; pdivmod_rel x y q r\<rbrakk>
  1739     \<Longrightarrow> pdivmod_rel x (smult a y) (smult (inverse a) q) r"
  1740   unfolding pdivmod_rel_def by simp
  1741 
  1742 lemma div_smult_right:
  1743   "a \<noteq> 0 \<Longrightarrow> x div (smult a y) = smult (inverse a) (x div y)"
  1744   by (rule div_poly_eq, erule pdivmod_rel_smult_right, rule pdivmod_rel)
  1745 
  1746 lemma mod_smult_right: "a \<noteq> 0 \<Longrightarrow> x mod (smult a y) = x mod y"
  1747   by (rule mod_poly_eq, erule pdivmod_rel_smult_right, rule pdivmod_rel)
  1748 
  1749 lemma poly_div_minus_right [simp]:
  1750   fixes x y :: "'a::field poly"
  1751   shows "x div (- y) = - (x div y)"
  1752   using div_smult_right [of "- 1::'a"] by (simp add: nonzero_inverse_minus_eq)
  1753 
  1754 lemma poly_mod_minus_right [simp]:
  1755   fixes x y :: "'a::field poly"
  1756   shows "x mod (- y) = x mod y"
  1757   using mod_smult_right [of "- 1::'a"] by simp
  1758 
  1759 lemma pdivmod_rel_mult:
  1760   "\<lbrakk>pdivmod_rel x y q r; pdivmod_rel q z q' r'\<rbrakk>
  1761     \<Longrightarrow> pdivmod_rel x (y * z) q' (y * r' + r)"
  1762 apply (cases "z = 0", simp add: pdivmod_rel_def)
  1763 apply (cases "y = 0", simp add: pdivmod_rel_by_0_iff pdivmod_rel_0_iff)
  1764 apply (cases "r = 0")
  1765 apply (cases "r' = 0")
  1766 apply (simp add: pdivmod_rel_def)
  1767 apply (simp add: pdivmod_rel_def field_simps degree_mult_eq)
  1768 apply (cases "r' = 0")
  1769 apply (simp add: pdivmod_rel_def degree_mult_eq)
  1770 apply (simp add: pdivmod_rel_def field_simps)
  1771 apply (simp add: degree_mult_eq degree_add_less)
  1772 done
  1773 
  1774 lemma poly_div_mult_right:
  1775   fixes x y z :: "'a::field poly"
  1776   shows "x div (y * z) = (x div y) div z"
  1777   by (rule div_poly_eq, rule pdivmod_rel_mult, (rule pdivmod_rel)+)
  1778 
  1779 lemma poly_mod_mult_right:
  1780   fixes x y z :: "'a::field poly"
  1781   shows "x mod (y * z) = y * (x div y mod z) + x mod y"
  1782   by (rule mod_poly_eq, rule pdivmod_rel_mult, (rule pdivmod_rel)+)
  1783 
  1784 lemma mod_pCons:
  1785   fixes a and x
  1786   assumes y: "y \<noteq> 0"
  1787   defines b: "b \<equiv> coeff (pCons a (x mod y)) (degree y) / coeff y (degree y)"
  1788   shows "(pCons a x) mod y = (pCons a (x mod y) - smult b y)"
  1789 unfolding b
  1790 apply (rule mod_poly_eq)
  1791 apply (rule pdivmod_rel_pCons [OF pdivmod_rel y refl])
  1792 done
  1793 
  1794 definition pdivmod :: "'a::field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<times> 'a poly"
  1795 where
  1796   "pdivmod p q = (p div q, p mod q)"
  1797 
  1798 lemma div_poly_code [code]: 
  1799   "p div q = fst (pdivmod p q)"
  1800   by (simp add: pdivmod_def)
  1801 
  1802 lemma mod_poly_code [code]:
  1803   "p mod q = snd (pdivmod p q)"
  1804   by (simp add: pdivmod_def)
  1805 
  1806 lemma pdivmod_0:
  1807   "pdivmod 0 q = (0, 0)"
  1808   by (simp add: pdivmod_def)
  1809 
  1810 lemma pdivmod_pCons:
  1811   "pdivmod (pCons a p) q =
  1812     (if q = 0 then (0, pCons a p) else
  1813       (let (s, r) = pdivmod p q;
  1814            b = coeff (pCons a r) (degree q) / coeff q (degree q)
  1815         in (pCons b s, pCons a r - smult b q)))"
  1816   apply (simp add: pdivmod_def Let_def, safe)
  1817   apply (rule div_poly_eq)
  1818   apply (erule pdivmod_rel_pCons [OF pdivmod_rel _ refl])
  1819   apply (rule mod_poly_eq)
  1820   apply (erule pdivmod_rel_pCons [OF pdivmod_rel _ refl])
  1821   done
  1822 
  1823 lemma pdivmod_fold_coeffs [code]:
  1824   "pdivmod p q = (if q = 0 then (0, p)
  1825     else fold_coeffs (\<lambda>a (s, r).
  1826       let b = coeff (pCons a r) (degree q) / coeff q (degree q)
  1827       in (pCons b s, pCons a r - smult b q)
  1828    ) p (0, 0))"
  1829   apply (cases "q = 0")
  1830   apply (simp add: pdivmod_def)
  1831   apply (rule sym)
  1832   apply (induct p)
  1833   apply (simp_all add: pdivmod_0 pdivmod_pCons)
  1834   apply (case_tac "a = 0 \<and> p = 0")
  1835   apply (auto simp add: pdivmod_def)
  1836   done
  1837 
  1838 
  1839 subsection \<open>Order of polynomial roots\<close>
  1840 
  1841 definition order :: "'a::idom \<Rightarrow> 'a poly \<Rightarrow> nat"
  1842 where
  1843   "order a p = (LEAST n. \<not> [:-a, 1:] ^ Suc n dvd p)"
  1844 
  1845 lemma coeff_linear_power:
  1846   fixes a :: "'a::comm_semiring_1"
  1847   shows "coeff ([:a, 1:] ^ n) n = 1"
  1848 apply (induct n, simp_all)
  1849 apply (subst coeff_eq_0)
  1850 apply (auto intro: le_less_trans degree_power_le)
  1851 done
  1852 
  1853 lemma degree_linear_power:
  1854   fixes a :: "'a::comm_semiring_1"
  1855   shows "degree ([:a, 1:] ^ n) = n"
  1856 apply (rule order_antisym)
  1857 apply (rule ord_le_eq_trans [OF degree_power_le], simp)
  1858 apply (rule le_degree, simp add: coeff_linear_power)
  1859 done
  1860 
  1861 lemma order_1: "[:-a, 1:] ^ order a p dvd p"
  1862 apply (cases "p = 0", simp)
  1863 apply (cases "order a p", simp)
  1864 apply (subgoal_tac "nat < (LEAST n. \<not> [:-a, 1:] ^ Suc n dvd p)")
  1865 apply (drule not_less_Least, simp)
  1866 apply (fold order_def, simp)
  1867 done
  1868 
  1869 lemma order_2: "p \<noteq> 0 \<Longrightarrow> \<not> [:-a, 1:] ^ Suc (order a p) dvd p"
  1870 unfolding order_def
  1871 apply (rule LeastI_ex)
  1872 apply (rule_tac x="degree p" in exI)
  1873 apply (rule notI)
  1874 apply (drule (1) dvd_imp_degree_le)
  1875 apply (simp only: degree_linear_power)
  1876 done
  1877 
  1878 lemma order:
  1879   "p \<noteq> 0 \<Longrightarrow> [:-a, 1:] ^ order a p dvd p \<and> \<not> [:-a, 1:] ^ Suc (order a p) dvd p"
  1880 by (rule conjI [OF order_1 order_2])
  1881 
  1882 lemma order_degree:
  1883   assumes p: "p \<noteq> 0"
  1884   shows "order a p \<le> degree p"
  1885 proof -
  1886   have "order a p = degree ([:-a, 1:] ^ order a p)"
  1887     by (simp only: degree_linear_power)
  1888   also have "\<dots> \<le> degree p"
  1889     using order_1 p by (rule dvd_imp_degree_le)
  1890   finally show ?thesis .
  1891 qed
  1892 
  1893 lemma order_root: "poly p a = 0 \<longleftrightarrow> p = 0 \<or> order a p \<noteq> 0"
  1894 apply (cases "p = 0", simp_all)
  1895 apply (rule iffI)
  1896 apply (metis order_2 not_gr0 poly_eq_0_iff_dvd power_0 power_Suc_0 power_one_right)
  1897 unfolding poly_eq_0_iff_dvd
  1898 apply (metis dvd_power dvd_trans order_1)
  1899 done
  1900 
  1901 lemma order_0I: "poly p a \<noteq> 0 \<Longrightarrow> order a p = 0"
  1902   by (subst (asm) order_root) auto
  1903 
  1904 
  1905 subsection \<open>Additional induction rules on polynomials\<close>
  1906 
  1907 text \<open>
  1908   An induction rule for induction over the roots of a polynomial with a certain property. 
  1909   (e.g. all positive roots)
  1910 \<close>
  1911 lemma poly_root_induct [case_names 0 no_roots root]:
  1912   fixes p :: "'a :: idom poly"
  1913   assumes "Q 0"
  1914   assumes "\<And>p. (\<And>a. P a \<Longrightarrow> poly p a \<noteq> 0) \<Longrightarrow> Q p"
  1915   assumes "\<And>a p. P a \<Longrightarrow> Q p \<Longrightarrow> Q ([:a, -1:] * p)"
  1916   shows   "Q p"
  1917 proof (induction "degree p" arbitrary: p rule: less_induct)
  1918   case (less p)
  1919   show ?case
  1920   proof (cases "p = 0")
  1921     assume nz: "p \<noteq> 0"
  1922     show ?case
  1923     proof (cases "\<exists>a. P a \<and> poly p a = 0")
  1924       case False
  1925       thus ?thesis by (intro assms(2)) blast
  1926     next
  1927       case True
  1928       then obtain a where a: "P a" "poly p a = 0" 
  1929         by blast
  1930       hence "-[:-a, 1:] dvd p" 
  1931         by (subst minus_dvd_iff) (simp add: poly_eq_0_iff_dvd)
  1932       then obtain q where q: "p = [:a, -1:] * q" by (elim dvdE) simp
  1933       with nz have q_nz: "q \<noteq> 0" by auto
  1934       have "degree p = Suc (degree q)"
  1935         by (subst q, subst degree_mult_eq) (simp_all add: q_nz)
  1936       hence "Q q" by (intro less) simp
  1937       from a(1) and this have "Q ([:a, -1:] * q)" 
  1938         by (rule assms(3))
  1939       with q show ?thesis by simp
  1940     qed
  1941   qed (simp add: assms(1))
  1942 qed
  1943 
  1944 lemma dropWhile_replicate_append: 
  1945   "dropWhile (op= a) (replicate n a @ ys) = dropWhile (op= a) ys"
  1946   by (induction n) simp_all
  1947 
  1948 lemma Poly_append_replicate_0: "Poly (xs @ replicate n 0) = Poly xs"
  1949   by (subst coeffs_eq_iff) (simp_all add: strip_while_def dropWhile_replicate_append)
  1950 
  1951 text \<open>
  1952   An induction rule for simultaneous induction over two polynomials, 
  1953   prepending one coefficient in each step.
  1954 \<close>
  1955 lemma poly_induct2 [case_names 0 pCons]:
  1956   assumes "P 0 0" "\<And>a p b q. P p q \<Longrightarrow> P (pCons a p) (pCons b q)"
  1957   shows   "P p q"
  1958 proof -
  1959   def n \<equiv> "max (length (coeffs p)) (length (coeffs q))"
  1960   def xs \<equiv> "coeffs p @ (replicate (n - length (coeffs p)) 0)"
  1961   def ys \<equiv> "coeffs q @ (replicate (n - length (coeffs q)) 0)"
  1962   have "length xs = length ys" 
  1963     by (simp add: xs_def ys_def n_def)
  1964   hence "P (Poly xs) (Poly ys)" 
  1965     by (induction rule: list_induct2) (simp_all add: assms)
  1966   also have "Poly xs = p" 
  1967     by (simp add: xs_def Poly_append_replicate_0)
  1968   also have "Poly ys = q" 
  1969     by (simp add: ys_def Poly_append_replicate_0)
  1970   finally show ?thesis .
  1971 qed
  1972 
  1973 
  1974 subsection \<open>Composition of polynomials\<close>
  1975 
  1976 (* Several lemmas contributed by René Thiemann and Akihisa Yamada *)
  1977 
  1978 definition pcompose :: "'a::comm_semiring_0 poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
  1979 where
  1980   "pcompose p q = fold_coeffs (\<lambda>a c. [:a:] + q * c) p 0"
  1981 
  1982 notation pcompose (infixl "\<circ>\<^sub>p" 71)
  1983 
  1984 lemma pcompose_0 [simp]:
  1985   "pcompose 0 q = 0"
  1986   by (simp add: pcompose_def)
  1987   
  1988 lemma pcompose_pCons:
  1989   "pcompose (pCons a p) q = [:a:] + q * pcompose p q"
  1990   by (cases "p = 0 \<and> a = 0") (auto simp add: pcompose_def)
  1991 
  1992 lemma pcompose_1:
  1993   fixes p :: "'a :: comm_semiring_1 poly"
  1994   shows "pcompose 1 p = 1"
  1995   unfolding one_poly_def by (auto simp: pcompose_pCons)
  1996 
  1997 lemma poly_pcompose:
  1998   "poly (pcompose p q) x = poly p (poly q x)"
  1999   by (induct p) (simp_all add: pcompose_pCons)
  2000 
  2001 lemma degree_pcompose_le:
  2002   "degree (pcompose p q) \<le> degree p * degree q"
  2003 apply (induct p, simp)
  2004 apply (simp add: pcompose_pCons, clarify)
  2005 apply (rule degree_add_le, simp)
  2006 apply (rule order_trans [OF degree_mult_le], simp)
  2007 done
  2008 
  2009 lemma pcompose_add:
  2010   fixes p q r :: "'a :: {comm_semiring_0, ab_semigroup_add} poly"
  2011   shows "pcompose (p + q) r = pcompose p r + pcompose q r"
  2012 proof (induction p q rule: poly_induct2)
  2013   case (pCons a p b q)
  2014   have "pcompose (pCons a p + pCons b q) r = 
  2015           [:a + b:] + r * pcompose p r + r * pcompose q r"
  2016     by (simp_all add: pcompose_pCons pCons.IH algebra_simps)
  2017   also have "[:a + b:] = [:a:] + [:b:]" by simp
  2018   also have "\<dots> + r * pcompose p r + r * pcompose q r = 
  2019                  pcompose (pCons a p) r + pcompose (pCons b q) r"
  2020     by (simp only: pcompose_pCons add_ac)
  2021   finally show ?case .
  2022 qed simp
  2023 
  2024 lemma pcompose_uminus:
  2025   fixes p r :: "'a :: comm_ring poly"
  2026   shows "pcompose (-p) r = -pcompose p r"
  2027   by (induction p) (simp_all add: pcompose_pCons)
  2028 
  2029 lemma pcompose_diff:
  2030   fixes p q r :: "'a :: comm_ring poly"
  2031   shows "pcompose (p - q) r = pcompose p r - pcompose q r"
  2032   using pcompose_add[of p "-q"] by (simp add: pcompose_uminus)
  2033 
  2034 lemma pcompose_smult:
  2035   fixes p r :: "'a :: comm_semiring_0 poly"
  2036   shows "pcompose (smult a p) r = smult a (pcompose p r)"
  2037   by (induction p) 
  2038      (simp_all add: pcompose_pCons pcompose_add smult_add_right)
  2039 
  2040 lemma pcompose_mult:
  2041   fixes p q r :: "'a :: comm_semiring_0 poly"
  2042   shows "pcompose (p * q) r = pcompose p r * pcompose q r"
  2043   by (induction p arbitrary: q)
  2044      (simp_all add: pcompose_add pcompose_smult pcompose_pCons algebra_simps)
  2045 
  2046 lemma pcompose_assoc: 
  2047   "pcompose p (pcompose q r :: 'a :: comm_semiring_0 poly ) =
  2048      pcompose (pcompose p q) r"
  2049   by (induction p arbitrary: q) 
  2050      (simp_all add: pcompose_pCons pcompose_add pcompose_mult)
  2051 
  2052 lemma pcompose_idR[simp]:
  2053   fixes p :: "'a :: comm_semiring_1 poly"
  2054   shows "pcompose p [: 0, 1 :] = p"
  2055   by (induct p; simp add: pcompose_pCons)
  2056 
  2057 
  2058 (* The remainder of this section and the next were contributed by Wenda Li *)
  2059 
  2060 lemma degree_mult_eq_0:
  2061   fixes p q:: "'a :: semidom poly"
  2062   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)"
  2063 by (auto simp add:degree_mult_eq)
  2064 
  2065 lemma pcompose_const[simp]:"pcompose [:a:] q = [:a:]" by (subst pcompose_pCons,simp) 
  2066 
  2067 lemma pcompose_0': "pcompose p 0 = [:coeff p 0:]"
  2068   by (induct p) (auto simp add:pcompose_pCons)
  2069 
  2070 lemma degree_pcompose:
  2071   fixes p q:: "'a::semidom poly"
  2072   shows "degree (pcompose p q) = degree p * degree q"
  2073 proof (induct p)
  2074   case 0
  2075   thus ?case by auto
  2076 next
  2077   case (pCons a p)
  2078   have "degree (q * pcompose p q) = 0 \<Longrightarrow> ?case" 
  2079     proof (cases "p=0")
  2080       case True
  2081       thus ?thesis by auto
  2082     next
  2083       case False assume "degree (q * pcompose p q) = 0"
  2084       hence "degree q=0 \<or> pcompose p q=0" by (auto simp add: degree_mult_eq_0)
  2085       moreover have "\<lbrakk>pcompose p q=0;degree q\<noteq>0\<rbrakk> \<Longrightarrow> False" using pCons.hyps(2) \<open>p\<noteq>0\<close> 
  2086         proof -
  2087           assume "pcompose p q=0" "degree q\<noteq>0"
  2088           hence "degree p=0" using pCons.hyps(2) by auto
  2089           then obtain a1 where "p=[:a1:]"
  2090             by (metis degree_pCons_eq_if old.nat.distinct(2) pCons_cases)
  2091           thus False using \<open>pcompose p q=0\<close> \<open>p\<noteq>0\<close> by auto
  2092         qed
  2093       ultimately have "degree (pCons a p) * degree q=0" by auto
  2094       moreover have "degree (pcompose (pCons a p) q) = 0" 
  2095         proof -
  2096           have" 0 = max (degree [:a:]) (degree (q*pcompose p q))"
  2097             using \<open>degree (q * pcompose p q) = 0\<close> by simp
  2098           also have "... \<ge> degree ([:a:] + q * pcompose p q)"
  2099             by (rule degree_add_le_max)
  2100           finally show ?thesis by (auto simp add:pcompose_pCons)
  2101         qed
  2102       ultimately show ?thesis by simp
  2103     qed
  2104   moreover have "degree (q * pcompose p q)>0 \<Longrightarrow> ?case" 
  2105     proof -
  2106       assume asm:"0 < degree (q * pcompose p q)"
  2107       hence "p\<noteq>0" "q\<noteq>0" "pcompose p q\<noteq>0" by auto
  2108       have "degree (pcompose (pCons a p) q) = degree ( q * pcompose p q)"
  2109         unfolding pcompose_pCons
  2110         using degree_add_eq_right[of "[:a:]" ] asm by auto       
  2111       thus ?thesis 
  2112         using pCons.hyps(2) degree_mult_eq[OF \<open>q\<noteq>0\<close> \<open>pcompose p q\<noteq>0\<close>] by auto
  2113     qed
  2114   ultimately show ?case by blast
  2115 qed
  2116 
  2117 lemma pcompose_eq_0:
  2118   fixes p q:: "'a :: semidom poly"
  2119   assumes "pcompose p q = 0" "degree q > 0" 
  2120   shows "p = 0"
  2121 proof -
  2122   have "degree p=0" using assms degree_pcompose[of p q] by auto
  2123   then obtain a where "p=[:a:]" 
  2124     by (metis degree_pCons_eq_if gr0_conv_Suc neq0_conv pCons_cases)
  2125   hence "a=0" using assms(1) by auto
  2126   thus ?thesis using \<open>p=[:a:]\<close> by simp
  2127 qed
  2128 
  2129 
  2130 subsection \<open>Leading coefficient\<close>
  2131 
  2132 definition lead_coeff:: "'a::zero poly \<Rightarrow> 'a" where
  2133   "lead_coeff p= coeff p (degree p)"
  2134 
  2135 lemma lead_coeff_pCons[simp]:
  2136     "p\<noteq>0 \<Longrightarrow>lead_coeff (pCons a p) = lead_coeff p"
  2137     "p=0 \<Longrightarrow> lead_coeff (pCons a p) = a"
  2138 unfolding lead_coeff_def by auto
  2139 
  2140 lemma lead_coeff_0[simp]:"lead_coeff 0 =0" 
  2141   unfolding lead_coeff_def by auto
  2142 
  2143 lemma lead_coeff_mult:
  2144    fixes p q::"'a ::idom poly"
  2145    shows "lead_coeff (p * q) = lead_coeff p * lead_coeff q"
  2146 by (unfold lead_coeff_def,cases "p=0 \<or> q=0",auto simp add:coeff_mult_degree_sum degree_mult_eq)
  2147 
  2148 lemma lead_coeff_add_le:
  2149   assumes "degree p < degree q"
  2150   shows "lead_coeff (p+q) = lead_coeff q" 
  2151 using assms unfolding lead_coeff_def
  2152 by (metis coeff_add coeff_eq_0 monoid_add_class.add.left_neutral degree_add_eq_right)
  2153 
  2154 lemma lead_coeff_minus:
  2155   "lead_coeff (-p) = - lead_coeff p"
  2156 by (metis coeff_minus degree_minus lead_coeff_def)
  2157 
  2158 
  2159 lemma lead_coeff_comp:
  2160   fixes p q:: "'a::idom poly"
  2161   assumes "degree q > 0" 
  2162   shows "lead_coeff (pcompose p q) = lead_coeff p * lead_coeff q ^ (degree p)"
  2163 proof (induct p)
  2164   case 0
  2165   thus ?case unfolding lead_coeff_def by auto
  2166 next
  2167   case (pCons a p)
  2168   have "degree ( q * pcompose p q) = 0 \<Longrightarrow> ?case"
  2169     proof -
  2170       assume "degree ( q * pcompose p q) = 0"
  2171       hence "pcompose p q = 0" by (metis assms degree_0 degree_mult_eq_0 neq0_conv)
  2172       hence "p=0" using pcompose_eq_0[OF _ \<open>degree q > 0\<close>] by simp
  2173       thus ?thesis by auto
  2174     qed
  2175   moreover have "degree ( q * pcompose p q) > 0 \<Longrightarrow> ?case" 
  2176     proof -
  2177       assume "degree ( q * pcompose p q) > 0"
  2178       hence "lead_coeff (pcompose (pCons a p) q) =lead_coeff ( q * pcompose p q)"
  2179         by (auto simp add:pcompose_pCons lead_coeff_add_le)
  2180       also have "... = lead_coeff q * (lead_coeff p * lead_coeff q ^ degree p)"
  2181         using pCons.hyps(2) lead_coeff_mult[of q "pcompose p q"] by simp
  2182       also have "... = lead_coeff p * lead_coeff q ^ (degree p + 1)"
  2183         by auto
  2184       finally show ?thesis by auto
  2185     qed
  2186   ultimately show ?case by blast
  2187 qed
  2188 
  2189 lemma lead_coeff_smult: 
  2190   "lead_coeff (smult c p :: 'a :: idom poly) = c * lead_coeff p"
  2191 proof -
  2192   have "smult c p = [:c:] * p" by simp
  2193   also have "lead_coeff \<dots> = c * lead_coeff p" 
  2194     by (subst lead_coeff_mult) simp_all
  2195   finally show ?thesis .
  2196 qed
  2197 
  2198 lemma lead_coeff_1 [simp]: "lead_coeff 1 = 1"
  2199   by (simp add: lead_coeff_def)
  2200 
  2201 lemma lead_coeff_of_nat [simp]:
  2202   "lead_coeff (of_nat n) = (of_nat n :: 'a :: {comm_semiring_1,semiring_char_0})"
  2203   by (induction n) (simp_all add: lead_coeff_def of_nat_poly)
  2204 
  2205 lemma lead_coeff_numeral [simp]: 
  2206   "lead_coeff (numeral n) = numeral n"
  2207   unfolding lead_coeff_def
  2208   by (subst of_nat_numeral [symmetric], subst of_nat_poly) simp
  2209 
  2210 lemma lead_coeff_power: 
  2211   "lead_coeff (p ^ n :: 'a :: idom poly) = lead_coeff p ^ n"
  2212   by (induction n) (simp_all add: lead_coeff_mult)
  2213 
  2214 lemma lead_coeff_nonzero: "p \<noteq> 0 \<Longrightarrow> lead_coeff p \<noteq> 0"
  2215   by (simp add: lead_coeff_def)
  2216 
  2217 
  2218 subsection \<open>Derivatives of univariate polynomials\<close>
  2219 
  2220 function pderiv :: "('a :: semidom) poly \<Rightarrow> 'a poly"
  2221 where
  2222   [simp del]: "pderiv (pCons a p) = (if p = 0 then 0 else p + pCons 0 (pderiv p))"
  2223   by (auto intro: pCons_cases)
  2224 
  2225 termination pderiv
  2226   by (relation "measure degree") simp_all
  2227 
  2228 lemma pderiv_0 [simp]:
  2229   "pderiv 0 = 0"
  2230   using pderiv.simps [of 0 0] by simp
  2231 
  2232 lemma pderiv_pCons:
  2233   "pderiv (pCons a p) = p + pCons 0 (pderiv p)"
  2234   by (simp add: pderiv.simps)
  2235 
  2236 lemma pderiv_1 [simp]: "pderiv 1 = 0" 
  2237   unfolding one_poly_def by (simp add: pderiv_pCons)
  2238 
  2239 lemma pderiv_of_nat  [simp]: "pderiv (of_nat n) = 0"
  2240   and pderiv_numeral [simp]: "pderiv (numeral m) = 0"
  2241   by (simp_all add: of_nat_poly numeral_poly pderiv_pCons)
  2242 
  2243 lemma coeff_pderiv: "coeff (pderiv p) n = of_nat (Suc n) * coeff p (Suc n)"
  2244   by (induct p arbitrary: n) 
  2245      (auto simp add: pderiv_pCons coeff_pCons algebra_simps split: nat.split)
  2246 
  2247 fun pderiv_coeffs_code :: "('a :: semidom) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
  2248   "pderiv_coeffs_code f (x # xs) = cCons (f * x) (pderiv_coeffs_code (f+1) xs)"
  2249 | "pderiv_coeffs_code f [] = []"
  2250 
  2251 definition pderiv_coeffs :: "('a :: semidom) list \<Rightarrow> 'a list" where
  2252   "pderiv_coeffs xs = pderiv_coeffs_code 1 (tl xs)"
  2253 
  2254 (* Efficient code for pderiv contributed by René Thiemann and Akihisa Yamada *)
  2255 lemma pderiv_coeffs_code: 
  2256   "nth_default 0 (pderiv_coeffs_code f xs) n = (f + of_nat n) * (nth_default 0 xs n)"
  2257 proof (induct xs arbitrary: f n)
  2258   case (Cons x xs f n)
  2259   show ?case 
  2260   proof (cases n)
  2261     case 0
  2262     thus ?thesis by (cases "pderiv_coeffs_code (f + 1) xs = [] \<and> f * x = 0", auto simp: cCons_def)
  2263   next
  2264     case (Suc m) note n = this
  2265     show ?thesis 
  2266     proof (cases "pderiv_coeffs_code (f + 1) xs = [] \<and> f * x = 0")
  2267       case False
  2268       hence "nth_default 0 (pderiv_coeffs_code f (x # xs)) n = 
  2269                nth_default 0 (pderiv_coeffs_code (f + 1) xs) m" 
  2270         by (auto simp: cCons_def n)
  2271       also have "\<dots> = (f + of_nat n) * (nth_default 0 xs m)" 
  2272         unfolding Cons by (simp add: n add_ac)
  2273       finally show ?thesis by (simp add: n)
  2274     next
  2275       case True
  2276       {
  2277         fix g 
  2278         have "pderiv_coeffs_code g xs = [] \<Longrightarrow> g + of_nat m = 0 \<or> nth_default 0 xs m = 0"
  2279         proof (induct xs arbitrary: g m)
  2280           case (Cons x xs g)
  2281           from Cons(2) have empty: "pderiv_coeffs_code (g + 1) xs = []"
  2282                             and g: "(g = 0 \<or> x = 0)"
  2283             by (auto simp: cCons_def split: if_splits)
  2284           note IH = Cons(1)[OF empty]
  2285           from IH[of m] IH[of "m - 1"] g
  2286           show ?case by (cases m, auto simp: field_simps)
  2287         qed simp
  2288       } note empty = this
  2289       from True have "nth_default 0 (pderiv_coeffs_code f (x # xs)) n = 0"
  2290         by (auto simp: cCons_def n)
  2291       moreover have "(f + of_nat n) * nth_default 0 (x # xs) n = 0" using True
  2292         by (simp add: n, insert empty[of "f+1"], auto simp: field_simps)
  2293       ultimately show ?thesis by simp
  2294     qed
  2295   qed
  2296 qed simp
  2297 
  2298 lemma map_upt_Suc: "map f [0 ..< Suc n] = f 0 # map (\<lambda> i. f (Suc i)) [0 ..< n]"
  2299   by (induct n arbitrary: f, auto)
  2300 
  2301 lemma coeffs_pderiv_code [code abstract]:
  2302   "coeffs (pderiv p) = pderiv_coeffs (coeffs p)" unfolding pderiv_coeffs_def
  2303 proof (rule coeffs_eqI, unfold pderiv_coeffs_code coeff_pderiv, goal_cases)
  2304   case (1 n)
  2305   have id: "coeff p (Suc n) = nth_default 0 (map (\<lambda>i. coeff p (Suc i)) [0..<degree p]) n"
  2306     by (cases "n < degree p", auto simp: nth_default_def coeff_eq_0)
  2307   show ?case unfolding coeffs_def map_upt_Suc by (auto simp: id)
  2308 next
  2309   case 2
  2310   obtain n xs where id: "tl (coeffs p) = xs" "(1 :: 'a) = n" by auto
  2311   from 2 show ?case
  2312     unfolding id by (induct xs arbitrary: n, auto simp: cCons_def)
  2313 qed
  2314 
  2315 context
  2316   assumes "SORT_CONSTRAINT('a::{semidom, semiring_char_0})"
  2317 begin
  2318 
  2319 lemma pderiv_eq_0_iff: 
  2320   "pderiv (p :: 'a poly) = 0 \<longleftrightarrow> degree p = 0"
  2321   apply (rule iffI)
  2322   apply (cases p, simp)
  2323   apply (simp add: poly_eq_iff coeff_pderiv del: of_nat_Suc)
  2324   apply (simp add: poly_eq_iff coeff_pderiv coeff_eq_0)
  2325   done
  2326 
  2327 lemma degree_pderiv: "degree (pderiv (p :: 'a poly)) = degree p - 1"
  2328   apply (rule order_antisym [OF degree_le])
  2329   apply (simp add: coeff_pderiv coeff_eq_0)
  2330   apply (cases "degree p", simp)
  2331   apply (rule le_degree)
  2332   apply (simp add: coeff_pderiv del: of_nat_Suc)
  2333   apply (metis degree_0 leading_coeff_0_iff nat.distinct(1))
  2334   done
  2335 
  2336 lemma not_dvd_pderiv: 
  2337   assumes "degree (p :: 'a poly) \<noteq> 0"
  2338   shows "\<not> p dvd pderiv p"
  2339 proof
  2340   assume dvd: "p dvd pderiv p"
  2341   then obtain q where p: "pderiv p = p * q" unfolding dvd_def by auto
  2342   from dvd have le: "degree p \<le> degree (pderiv p)"
  2343     by (simp add: assms dvd_imp_degree_le pderiv_eq_0_iff)
  2344   from this[unfolded degree_pderiv] assms show False by auto
  2345 qed
  2346 
  2347 lemma dvd_pderiv_iff [simp]: "(p :: 'a poly) dvd pderiv p \<longleftrightarrow> degree p = 0"
  2348   using not_dvd_pderiv[of p] by (auto simp: pderiv_eq_0_iff [symmetric])
  2349 
  2350 end
  2351 
  2352 lemma pderiv_singleton [simp]: "pderiv [:a:] = 0"
  2353 by (simp add: pderiv_pCons)
  2354 
  2355 lemma pderiv_add: "pderiv (p + q) = pderiv p + pderiv q"
  2356 by (rule poly_eqI, simp add: coeff_pderiv algebra_simps)
  2357 
  2358 lemma pderiv_minus: "pderiv (- p :: 'a :: idom poly) = - pderiv p"
  2359 by (rule poly_eqI, simp add: coeff_pderiv algebra_simps)
  2360 
  2361 lemma pderiv_diff: "pderiv (p - q) = pderiv p - pderiv q"
  2362 by (rule poly_eqI, simp add: coeff_pderiv algebra_simps)
  2363 
  2364 lemma pderiv_smult: "pderiv (smult a p) = smult a (pderiv p)"
  2365 by (rule poly_eqI, simp add: coeff_pderiv algebra_simps)
  2366 
  2367 lemma pderiv_mult: "pderiv (p * q) = p * pderiv q + q * pderiv p"
  2368 by (induct p) (auto simp: pderiv_add pderiv_smult pderiv_pCons algebra_simps)
  2369 
  2370 lemma pderiv_power_Suc:
  2371   "pderiv (p ^ Suc n) = smult (of_nat (Suc n)) (p ^ n) * pderiv p"
  2372 apply (induct n)
  2373 apply simp
  2374 apply (subst power_Suc)
  2375 apply (subst pderiv_mult)
  2376 apply (erule ssubst)
  2377 apply (simp only: of_nat_Suc smult_add_left smult_1_left)
  2378 apply (simp add: algebra_simps)
  2379 done
  2380 
  2381 lemma pderiv_setprod: "pderiv (setprod f (as)) = 
  2382   (\<Sum>a \<in> as. setprod f (as - {a}) * pderiv (f a))"
  2383 proof (induct as rule: infinite_finite_induct)
  2384   case (insert a as)
  2385   hence id: "setprod f (insert a as) = f a * setprod f as" 
  2386     "\<And> g. setsum g (insert a as) = g a + setsum g as"
  2387     "insert a as - {a} = as"
  2388     by auto
  2389   {
  2390     fix b
  2391     assume "b \<in> as"
  2392     hence id2: "insert a as - {b} = insert a (as - {b})" using \<open>a \<notin> as\<close> by auto
  2393     have "setprod f (insert a as - {b}) = f a * setprod f (as - {b})"
  2394       unfolding id2
  2395       by (subst setprod.insert, insert insert, auto)
  2396   } note id2 = this
  2397   show ?case
  2398     unfolding id pderiv_mult insert(3) setsum_right_distrib
  2399     by (auto simp add: ac_simps id2 intro!: setsum.cong)
  2400 qed auto
  2401 
  2402 lemma DERIV_pow2: "DERIV (%x. x ^ Suc n) x :> real (Suc n) * (x ^ n)"
  2403 by (rule DERIV_cong, rule DERIV_pow, simp)
  2404 declare DERIV_pow2 [simp] DERIV_pow [simp]
  2405 
  2406 lemma DERIV_add_const: "DERIV f x :> D ==>  DERIV (%x. a + f x :: 'a::real_normed_field) x :> D"
  2407 by (rule DERIV_cong, rule DERIV_add, auto)
  2408 
  2409 lemma poly_DERIV [simp]: "DERIV (%x. poly p x) x :> poly (pderiv p) x"
  2410   by (induct p, auto intro!: derivative_eq_intros simp add: pderiv_pCons)
  2411 
  2412 lemma continuous_on_poly [continuous_intros]: 
  2413   fixes p :: "'a :: {real_normed_field} poly"
  2414   assumes "continuous_on A f"
  2415   shows   "continuous_on A (\<lambda>x. poly p (f x))"
  2416 proof -
  2417   have "continuous_on A (\<lambda>x. (\<Sum>i\<le>degree p. (f x) ^ i * coeff p i))" 
  2418     by (intro continuous_intros assms)
  2419   also have "\<dots> = (\<lambda>x. poly p (f x))" by (intro ext) (simp add: poly_altdef mult_ac)
  2420   finally show ?thesis .
  2421 qed
  2422 
  2423 text\<open>Consequences of the derivative theorem above\<close>
  2424 
  2425 lemma poly_differentiable[simp]: "(%x. poly p x) differentiable (at x::real filter)"
  2426 apply (simp add: real_differentiable_def)
  2427 apply (blast intro: poly_DERIV)
  2428 done
  2429 
  2430 lemma poly_isCont[simp]: "isCont (%x. poly p x) (x::real)"
  2431 by (rule poly_DERIV [THEN DERIV_isCont])
  2432 
  2433 lemma poly_IVT_pos: "[| a < b; poly p (a::real) < 0; 0 < poly p b |]
  2434       ==> \<exists>x. a < x & x < b & (poly p x = 0)"
  2435 using IVT_objl [of "poly p" a 0 b]
  2436 by (auto simp add: order_le_less)
  2437 
  2438 lemma poly_IVT_neg: "[| (a::real) < b; 0 < poly p a; poly p b < 0 |]
  2439       ==> \<exists>x. a < x & x < b & (poly p x = 0)"
  2440 by (insert poly_IVT_pos [where p = "- p" ]) simp
  2441 
  2442 lemma poly_IVT:
  2443   fixes p::"real poly"
  2444   assumes "a<b" and "poly p a * poly p b < 0"
  2445   shows "\<exists>x>a. x < b \<and> poly p x = 0"
  2446 by (metis assms(1) assms(2) less_not_sym mult_less_0_iff poly_IVT_neg poly_IVT_pos)
  2447 
  2448 lemma poly_MVT: "(a::real) < b ==>
  2449      \<exists>x. a < x & x < b & (poly p b - poly p a = (b - a) * poly (pderiv p) x)"
  2450 using MVT [of a b "poly p"]
  2451 apply auto
  2452 apply (rule_tac x = z in exI)
  2453 apply (auto simp add: mult_left_cancel poly_DERIV [THEN DERIV_unique])
  2454 done
  2455 
  2456 lemma poly_MVT':
  2457   assumes "{min a b..max a b} \<subseteq> A"
  2458   shows   "\<exists>x\<in>A. poly p b - poly p a = (b - a) * poly (pderiv p) (x::real)"
  2459 proof (cases a b rule: linorder_cases)
  2460   case less
  2461   from poly_MVT[OF less, of p] guess x by (elim exE conjE)
  2462   thus ?thesis by (intro bexI[of _ x]) (auto intro!: subsetD[OF assms])
  2463 
  2464 next
  2465   case greater
  2466   from poly_MVT[OF greater, of p] guess x by (elim exE conjE)
  2467   thus ?thesis by (intro bexI[of _ x]) (auto simp: algebra_simps intro!: subsetD[OF assms])
  2468 qed (insert assms, auto)
  2469 
  2470 lemma poly_pinfty_gt_lc:
  2471   fixes p:: "real poly"
  2472   assumes  "lead_coeff p > 0" 
  2473   shows "\<exists> n. \<forall> x \<ge> n. poly p x \<ge> lead_coeff p" using assms
  2474 proof (induct p)
  2475   case 0
  2476   thus ?case by auto
  2477 next
  2478   case (pCons a p)
  2479   have "\<lbrakk>a\<noteq>0;p=0\<rbrakk> \<Longrightarrow> ?case" by auto
  2480   moreover have "p\<noteq>0 \<Longrightarrow> ?case"
  2481     proof -
  2482       assume "p\<noteq>0"
  2483       then obtain n1 where gte_lcoeff:"\<forall>x\<ge>n1. lead_coeff p \<le> poly p x" using that pCons by auto
  2484       have gt_0:"lead_coeff p >0" using pCons(3) \<open>p\<noteq>0\<close> by auto
  2485       def n\<equiv>"max n1 (1+ \<bar>a\<bar>/(lead_coeff p))"
  2486       show ?thesis 
  2487         proof (rule_tac x=n in exI,rule,rule) 
  2488           fix x assume "n \<le> x"
  2489           hence "lead_coeff p \<le> poly p x" 
  2490             using gte_lcoeff unfolding n_def by auto
  2491           hence " \<bar>a\<bar>/(lead_coeff p) \<ge> \<bar>a\<bar>/(poly p x)" and "poly p x>0" using gt_0
  2492             by (intro frac_le,auto)
  2493           hence "x\<ge>1+ \<bar>a\<bar>/(poly p x)" using \<open>n\<le>x\<close>[unfolded n_def] by auto
  2494           thus "lead_coeff (pCons a p) \<le> poly (pCons a p) x"
  2495             using \<open>lead_coeff p \<le> poly p x\<close> \<open>poly p x>0\<close> \<open>p\<noteq>0\<close>
  2496             by (auto simp add:field_simps)
  2497         qed
  2498     qed
  2499   ultimately show ?case by fastforce
  2500 qed
  2501 
  2502 
  2503 subsection \<open>Algebraic numbers\<close>
  2504 
  2505 text \<open>
  2506   Algebraic numbers can be defined in two equivalent ways: all real numbers that are 
  2507   roots of rational polynomials or of integer polynomials. The Algebraic-Numbers AFP entry 
  2508   uses the rational definition, but we need the integer definition.
  2509 
  2510   The equivalence is obvious since any rational polynomial can be multiplied with the 
  2511   LCM of its coefficients, yielding an integer polynomial with the same roots.
  2512 \<close>
  2513 subsection \<open>Algebraic numbers\<close>
  2514 
  2515 definition algebraic :: "'a :: field_char_0 \<Rightarrow> bool" where
  2516   "algebraic x \<longleftrightarrow> (\<exists>p. (\<forall>i. coeff p i \<in> \<int>) \<and> p \<noteq> 0 \<and> poly p x = 0)"
  2517 
  2518 lemma algebraicI:
  2519   assumes "\<And>i. coeff p i \<in> \<int>" "p \<noteq> 0" "poly p x = 0"
  2520   shows   "algebraic x"
  2521   using assms unfolding algebraic_def by blast
  2522   
  2523 lemma algebraicE:
  2524   assumes "algebraic x"
  2525   obtains p where "\<And>i. coeff p i \<in> \<int>" "p \<noteq> 0" "poly p x = 0"
  2526   using assms unfolding algebraic_def by blast
  2527 
  2528 lemma quotient_of_denom_pos': "snd (quotient_of x) > 0"
  2529   using quotient_of_denom_pos[OF surjective_pairing] .
  2530   
  2531 lemma of_int_div_in_Ints: 
  2532   "b dvd a \<Longrightarrow> of_int a div of_int b \<in> (\<int> :: 'a :: ring_div set)"
  2533 proof (cases "of_int b = (0 :: 'a)")
  2534   assume "b dvd a" "of_int b \<noteq> (0::'a)"
  2535   then obtain c where "a = b * c" by (elim dvdE)
  2536   with \<open>of_int b \<noteq> (0::'a)\<close> show ?thesis by simp
  2537 qed auto
  2538 
  2539 lemma of_int_divide_in_Ints: 
  2540   "b dvd a \<Longrightarrow> of_int a / of_int b \<in> (\<int> :: 'a :: field set)"
  2541 proof (cases "of_int b = (0 :: 'a)")
  2542   assume "b dvd a" "of_int b \<noteq> (0::'a)"
  2543   then obtain c where "a = b * c" by (elim dvdE)
  2544   with \<open>of_int b \<noteq> (0::'a)\<close> show ?thesis by simp
  2545 qed auto
  2546 
  2547 lemma algebraic_altdef:
  2548   fixes p :: "'a :: field_char_0 poly"
  2549   shows "algebraic x \<longleftrightarrow> (\<exists>p. (\<forall>i. coeff p i \<in> \<rat>) \<and> p \<noteq> 0 \<and> poly p x = 0)"
  2550 proof safe
  2551   fix p assume rat: "\<forall>i. coeff p i \<in> \<rat>" and root: "poly p x = 0" and nz: "p \<noteq> 0"
  2552   def cs \<equiv> "coeffs p"
  2553   from rat have "\<forall>c\<in>range (coeff p). \<exists>c'. c = of_rat c'" unfolding Rats_def by blast
  2554   then obtain f where f: "\<And>i. coeff p i = of_rat (f (coeff p i))" 
  2555     by (subst (asm) bchoice_iff) blast
  2556   def cs' \<equiv> "map (quotient_of \<circ> f) (coeffs p)"
  2557   def d \<equiv> "Lcm (set (map snd cs'))"
  2558   def p' \<equiv> "smult (of_int d) p"
  2559   
  2560   have "\<forall>n. coeff p' n \<in> \<int>"
  2561   proof
  2562     fix n :: nat
  2563     show "coeff p' n \<in> \<int>"
  2564     proof (cases "n \<le> degree p")
  2565       case True
  2566       def c \<equiv> "coeff p n"
  2567       def a \<equiv> "fst (quotient_of (f (coeff p n)))" and b \<equiv> "snd (quotient_of (f (coeff p n)))"
  2568       have b_pos: "b > 0" unfolding b_def using quotient_of_denom_pos' by simp
  2569       have "coeff p' n = of_int d * coeff p n" by (simp add: p'_def)
  2570       also have "coeff p n = of_rat (of_int a / of_int b)" unfolding a_def b_def
  2571         by (subst quotient_of_div [of "f (coeff p n)", symmetric])
  2572            (simp_all add: f [symmetric])
  2573       also have "of_int d * \<dots> = of_rat (of_int (a*d) / of_int b)"
  2574         by (simp add: of_rat_mult of_rat_divide)
  2575       also from nz True have "b \<in> snd ` set cs'" unfolding cs'_def
  2576         by (force simp: o_def b_def coeffs_def simp del: upt_Suc)
  2577       hence "b dvd (a * d)" unfolding d_def by simp
  2578       hence "of_int (a * d) / of_int b \<in> (\<int> :: rat set)"
  2579         by (rule of_int_divide_in_Ints)
  2580       hence "of_rat (of_int (a * d) / of_int b) \<in> \<int>" by (elim Ints_cases) auto
  2581       finally show ?thesis .
  2582     qed (auto simp: p'_def not_le coeff_eq_0)
  2583   qed
  2584   
  2585   moreover have "set (map snd cs') \<subseteq> {0<..}"
  2586     unfolding cs'_def using quotient_of_denom_pos' by (auto simp: coeffs_def simp del: upt_Suc) 
  2587   hence "d \<noteq> 0" unfolding d_def by (induction cs') simp_all
  2588   with nz have "p' \<noteq> 0" by (simp add: p'_def)
  2589   moreover from root have "poly p' x = 0" by (simp add: p'_def)
  2590   ultimately show "algebraic x" unfolding algebraic_def by blast
  2591 next
  2592 
  2593   assume "algebraic x"
  2594   then obtain p where p: "\<And>i. coeff p i \<in> \<int>" "poly p x = 0" "p \<noteq> 0" 
  2595     by (force simp: algebraic_def)
  2596   moreover have "coeff p i \<in> \<int> \<Longrightarrow> coeff p i \<in> \<rat>" for i by (elim Ints_cases) simp
  2597   ultimately show  "(\<exists>p. (\<forall>i. coeff p i \<in> \<rat>) \<and> p \<noteq> 0 \<and> poly p x = 0)" by auto
  2598 qed
  2599 
  2600 
  2601 text\<open>Lemmas for Derivatives\<close>
  2602 
  2603 lemma order_unique_lemma:
  2604   fixes p :: "'a::idom poly"
  2605   assumes "[:-a, 1:] ^ n dvd p" "\<not> [:-a, 1:] ^ Suc n dvd p"
  2606   shows "n = order a p"
  2607 unfolding Polynomial.order_def
  2608 apply (rule Least_equality [symmetric])
  2609 apply (fact assms)
  2610 apply (rule classical)
  2611 apply (erule notE)
  2612 unfolding not_less_eq_eq
  2613 using assms(1) apply (rule power_le_dvd)
  2614 apply assumption
  2615 done
  2616 
  2617 lemma lemma_order_pderiv1:
  2618   "pderiv ([:- a, 1:] ^ Suc n * q) = [:- a, 1:] ^ Suc n * pderiv q +
  2619     smult (of_nat (Suc n)) (q * [:- a, 1:] ^ n)"
  2620 apply (simp only: pderiv_mult pderiv_power_Suc)
  2621 apply (simp del: power_Suc of_nat_Suc add: pderiv_pCons)
  2622 done
  2623 
  2624 lemma lemma_order_pderiv:
  2625   fixes p :: "'a :: field_char_0 poly"
  2626   assumes n: "0 < n" 
  2627       and pd: "pderiv p \<noteq> 0" 
  2628       and pe: "p = [:- a, 1:] ^ n * q" 
  2629       and nd: "~ [:- a, 1:] dvd q"
  2630     shows "n = Suc (order a (pderiv p))"
  2631 using n 
  2632 proof -
  2633   have "pderiv ([:- a, 1:] ^ n * q) \<noteq> 0"
  2634     using assms by auto
  2635   obtain n' where "n = Suc n'" "0 < Suc n'" "pderiv ([:- a, 1:] ^ Suc n' * q) \<noteq> 0"
  2636     using assms by (cases n) auto
  2637   have *: "!!k l. k dvd k * pderiv q + smult (of_nat (Suc n')) l \<Longrightarrow> k dvd l"
  2638     by (auto simp del: of_nat_Suc simp: dvd_add_right_iff dvd_smult_iff)
  2639   have "n' = order a (pderiv ([:- a, 1:] ^ Suc n' * q))" 
  2640   proof (rule order_unique_lemma)
  2641     show "[:- a, 1:] ^ n' dvd pderiv ([:- a, 1:] ^ Suc n' * q)"
  2642       apply (subst lemma_order_pderiv1)
  2643       apply (rule dvd_add)
  2644       apply (metis dvdI dvd_mult2 power_Suc2)
  2645       apply (metis dvd_smult dvd_triv_right)
  2646       done
  2647   next
  2648     show "\<not> [:- a, 1:] ^ Suc n' dvd pderiv ([:- a, 1:] ^ Suc n' * q)"
  2649      apply (subst lemma_order_pderiv1)
  2650      by (metis * nd dvd_mult_cancel_right power_not_zero pCons_eq_0_iff power_Suc zero_neq_one)
  2651   qed
  2652   then show ?thesis
  2653     by (metis \<open>n = Suc n'\<close> pe)
  2654 qed
  2655 
  2656 lemma order_decomp:
  2657   assumes "p \<noteq> 0"
  2658   shows "\<exists>q. p = [:- a, 1:] ^ order a p * q \<and> \<not> [:- a, 1:] dvd q"
  2659 proof -
  2660   from assms have A: "[:- a, 1:] ^ order a p dvd p"
  2661     and B: "\<not> [:- a, 1:] ^ Suc (order a p) dvd p" by (auto dest: order)
  2662   from A obtain q where C: "p = [:- a, 1:] ^ order a p * q" ..
  2663   with B have "\<not> [:- a, 1:] ^ Suc (order a p) dvd [:- a, 1:] ^ order a p * q"
  2664     by simp
  2665   then have "\<not> [:- a, 1:] ^ order a p * [:- a, 1:] dvd [:- a, 1:] ^ order a p * q"
  2666     by simp
  2667   then have D: "\<not> [:- a, 1:] dvd q"
  2668     using idom_class.dvd_mult_cancel_left [of "[:- a, 1:] ^ order a p" "[:- a, 1:]" q]
  2669     by auto
  2670   from C D show ?thesis by blast
  2671 qed
  2672 
  2673 lemma order_pderiv:
  2674   "\<lbrakk>pderiv p \<noteq> 0; order a (p :: 'a :: field_char_0 poly) \<noteq> 0\<rbrakk> \<Longrightarrow>
  2675      (order a p = Suc (order a (pderiv p)))"
  2676 apply (case_tac "p = 0", simp)
  2677 apply (drule_tac a = a and p = p in order_decomp)
  2678 using neq0_conv
  2679 apply (blast intro: lemma_order_pderiv)
  2680 done
  2681 
  2682 lemma order_mult: "p * q \<noteq> 0 \<Longrightarrow> order a (p * q) = order a p + order a q"
  2683 proof -
  2684   def i \<equiv> "order a p"
  2685   def j \<equiv> "order a q"
  2686   def t \<equiv> "[:-a, 1:]"
  2687   have t_dvd_iff: "\<And>u. t dvd u \<longleftrightarrow> poly u a = 0"
  2688     unfolding t_def by (simp add: dvd_iff_poly_eq_0)
  2689   assume "p * q \<noteq> 0"
  2690   then show "order a (p * q) = i + j"
  2691     apply clarsimp
  2692     apply (drule order [where a=a and p=p, folded i_def t_def])
  2693     apply (drule order [where a=a and p=q, folded j_def t_def])
  2694     apply clarify
  2695     apply (erule dvdE)+
  2696     apply (rule order_unique_lemma [symmetric], fold t_def)
  2697     apply (simp_all add: power_add t_dvd_iff)
  2698     done
  2699 qed
  2700 
  2701 lemma order_smult:
  2702   assumes "c \<noteq> 0" 
  2703   shows "order x (smult c p) = order x p"
  2704 proof (cases "p = 0")
  2705   case False
  2706   have "smult c p = [:c:] * p" by simp
  2707   also from assms False have "order x \<dots> = order x [:c:] + order x p" 
  2708     by (subst order_mult) simp_all
  2709   also from assms have "order x [:c:] = 0" by (intro order_0I) auto
  2710   finally show ?thesis by simp
  2711 qed simp
  2712 
  2713 (* Next two lemmas contributed by Wenda Li *)
  2714 lemma order_1_eq_0 [simp]:"order x 1 = 0" 
  2715   by (metis order_root poly_1 zero_neq_one)
  2716 
  2717 lemma order_power_n_n: "order a ([:-a,1:]^n)=n" 
  2718 proof (induct n) (*might be proved more concisely using nat_less_induct*)
  2719   case 0
  2720   thus ?case by (metis order_root poly_1 power_0 zero_neq_one)
  2721 next 
  2722   case (Suc n)
  2723   have "order a ([:- a, 1:] ^ Suc n)=order a ([:- a, 1:] ^ n) + order a [:-a,1:]" 
  2724     by (metis (no_types, hide_lams) One_nat_def add_Suc_right monoid_add_class.add.right_neutral 
  2725       one_neq_zero order_mult pCons_eq_0_iff power_add power_eq_0_iff power_one_right)
  2726   moreover have "order a [:-a,1:]=1" unfolding order_def
  2727     proof (rule Least_equality,rule ccontr)
  2728       assume  "\<not> \<not> [:- a, 1:] ^ Suc 1 dvd [:- a, 1:]"
  2729       hence "[:- a, 1:] ^ Suc 1 dvd [:- a, 1:]" by simp
  2730       hence "degree ([:- a, 1:] ^ Suc 1) \<le> degree ([:- a, 1:] )" 
  2731         by (rule dvd_imp_degree_le,auto) 
  2732       thus False by auto
  2733     next
  2734       fix y assume asm:"\<not> [:- a, 1:] ^ Suc y dvd [:- a, 1:]"
  2735       show "1 \<le> y" 
  2736         proof (rule ccontr)
  2737           assume "\<not> 1 \<le> y"
  2738           hence "y=0" by auto
  2739           hence "[:- a, 1:] ^ Suc y dvd [:- a, 1:]" by auto
  2740           thus False using asm by auto
  2741         qed
  2742     qed
  2743   ultimately show ?case using Suc by auto
  2744 qed
  2745 
  2746 text\<open>Now justify the standard squarefree decomposition, i.e. f / gcd(f,f').\<close>
  2747 
  2748 lemma order_divides: "[:-a, 1:] ^ n dvd p \<longleftrightarrow> p = 0 \<or> n \<le> order a p"
  2749 apply (cases "p = 0", auto)
  2750 apply (drule order_2 [where a=a and p=p])
  2751 apply (metis not_less_eq_eq power_le_dvd)
  2752 apply (erule power_le_dvd [OF order_1])
  2753 done
  2754 
  2755 lemma poly_squarefree_decomp_order:
  2756   assumes "pderiv (p :: 'a :: field_char_0 poly) \<noteq> 0"
  2757   and p: "p = q * d"
  2758   and p': "pderiv p = e * d"
  2759   and d: "d = r * p + s * pderiv p"
  2760   shows "order a q = (if order a p = 0 then 0 else 1)"
  2761 proof (rule classical)
  2762   assume 1: "order a q \<noteq> (if order a p = 0 then 0 else 1)"
  2763   from \<open>pderiv p \<noteq> 0\<close> have "p \<noteq> 0" by auto
  2764   with p have "order a p = order a q + order a d"
  2765     by (simp add: order_mult)
  2766   with 1 have "order a p \<noteq> 0" by (auto split: if_splits)
  2767   have "order a (pderiv p) = order a e + order a d"
  2768     using \<open>pderiv p \<noteq> 0\<close> \<open>pderiv p = e * d\<close> by (simp add: order_mult)
  2769   have "order a p = Suc (order a (pderiv p))"
  2770     using \<open>pderiv p \<noteq> 0\<close> \<open>order a p \<noteq> 0\<close> by (rule order_pderiv)
  2771   have "d \<noteq> 0" using \<open>p \<noteq> 0\<close> \<open>p = q * d\<close> by simp
  2772   have "([:-a, 1:] ^ (order a (pderiv p))) dvd d"
  2773     apply (simp add: d)
  2774     apply (rule dvd_add)
  2775     apply (rule dvd_mult)
  2776     apply (simp add: order_divides \<open>p \<noteq> 0\<close>
  2777            \<open>order a p = Suc (order a (pderiv p))\<close>)
  2778     apply (rule dvd_mult)
  2779     apply (simp add: order_divides)
  2780     done
  2781   then have "order a (pderiv p) \<le> order a d"
  2782     using \<open>d \<noteq> 0\<close> by (simp add: order_divides)
  2783   show ?thesis
  2784     using \<open>order a p = order a q + order a d\<close>
  2785     using \<open>order a (pderiv p) = order a e + order a d\<close>
  2786     using \<open>order a p = Suc (order a (pderiv p))\<close>
  2787     using \<open>order a (pderiv p) \<le> order a d\<close>
  2788     by auto
  2789 qed
  2790 
  2791 lemma poly_squarefree_decomp_order2: 
  2792      "\<lbrakk>pderiv p \<noteq> (0 :: 'a :: field_char_0 poly);
  2793        p = q * d;
  2794        pderiv p = e * d;
  2795        d = r * p + s * pderiv p
  2796       \<rbrakk> \<Longrightarrow> \<forall>a. order a q = (if order a p = 0 then 0 else 1)"
  2797 by (blast intro: poly_squarefree_decomp_order)
  2798 
  2799 lemma order_pderiv2: 
  2800   "\<lbrakk>pderiv p \<noteq> 0; order a (p :: 'a :: field_char_0 poly) \<noteq> 0\<rbrakk>
  2801       \<Longrightarrow> (order a (pderiv p) = n) = (order a p = Suc n)"
  2802 by (auto dest: order_pderiv)
  2803 
  2804 definition
  2805   rsquarefree :: "'a::idom poly => bool" where
  2806   "rsquarefree p = (p \<noteq> 0 & (\<forall>a. (order a p = 0) | (order a p = 1)))"
  2807 
  2808 lemma pderiv_iszero: "pderiv p = 0 \<Longrightarrow> \<exists>h. p = [:h :: 'a :: {semidom,semiring_char_0}:]"
  2809 apply (simp add: pderiv_eq_0_iff)
  2810 apply (case_tac p, auto split: if_splits)
  2811 done
  2812 
  2813 lemma rsquarefree_roots:
  2814   fixes p :: "'a :: field_char_0 poly"
  2815   shows "rsquarefree p = (\<forall>a. \<not>(poly p a = 0 \<and> poly (pderiv p) a = 0))"
  2816 apply (simp add: rsquarefree_def)
  2817 apply (case_tac "p = 0", simp, simp)
  2818 apply (case_tac "pderiv p = 0")
  2819 apply simp
  2820 apply (drule pderiv_iszero, clarsimp)
  2821 apply (metis coeff_0 coeff_pCons_0 degree_pCons_0 le0 le_antisym order_degree)
  2822 apply (force simp add: order_root order_pderiv2)
  2823 done
  2824 
  2825 lemma poly_squarefree_decomp:
  2826   assumes "pderiv (p :: 'a :: field_char_0 poly) \<noteq> 0"
  2827     and "p = q * d"
  2828     and "pderiv p = e * d"
  2829     and "d = r * p + s * pderiv p"
  2830   shows "rsquarefree q & (\<forall>a. (poly q a = 0) = (poly p a = 0))"
  2831 proof -
  2832   from \<open>pderiv p \<noteq> 0\<close> have "p \<noteq> 0" by auto
  2833   with \<open>p = q * d\<close> have "q \<noteq> 0" by simp
  2834   have "\<forall>a. order a q = (if order a p = 0 then 0 else 1)"
  2835     using assms by (rule poly_squarefree_decomp_order2)
  2836   with \<open>p \<noteq> 0\<close> \<open>q \<noteq> 0\<close> show ?thesis
  2837     by (simp add: rsquarefree_def order_root)
  2838 qed
  2839 
  2840 
  2841 no_notation cCons (infixr "##" 65)
  2842 
  2843 end