move Polynomial.thy to Library
authorhuffman
Wed Feb 18 20:14:45 2009 -0800 (2009-02-18)
changeset 29987391dcbd7e4dd
parent 29986 6b1ccda8bf19
child 29988 747f0c519090
move Polynomial.thy to Library
src/HOL/Deriv.thy
src/HOL/IsaMakefile
src/HOL/Library/Library.thy
src/HOL/Library/Polynomial.thy
src/HOL/Polynomial.thy
     1.1 --- a/src/HOL/Deriv.thy	Wed Feb 18 19:51:39 2009 -0800
     1.2 +++ b/src/HOL/Deriv.thy	Wed Feb 18 20:14:45 2009 -0800
     1.3 @@ -9,7 +9,7 @@
     1.4  header{* Differentiation *}
     1.5  
     1.6  theory Deriv
     1.7 -imports Lim Polynomial
     1.8 +imports Lim
     1.9  begin
    1.10  
    1.11  text{*Standard Definitions*}
     2.1 --- a/src/HOL/IsaMakefile	Wed Feb 18 19:51:39 2009 -0800
     2.2 +++ b/src/HOL/IsaMakefile	Wed Feb 18 20:14:45 2009 -0800
     2.3 @@ -284,7 +284,6 @@
     2.4    GCD.thy \
     2.5    Parity.thy \
     2.6    Lubs.thy \
     2.7 -  Polynomial.thy \
     2.8    PReal.thy \
     2.9    Rational.thy \
    2.10    RComplete.thy \
    2.11 @@ -337,6 +336,7 @@
    2.12    Library/RBT.thy	Library/Univ_Poly.thy	\
    2.13    Library/Random.thy	Library/Quickcheck.thy	\
    2.14    Library/Poly_Deriv.thy \
    2.15 +  Library/Polynomial.thy \
    2.16    Library/Enum.thy Library/Float.thy $(SRC)/Tools/float.ML $(SRC)/HOL/Tools/float_arith.ML \
    2.17    Library/reify_data.ML Library/reflection.ML
    2.18  	@cd Library; $(ISABELLE_TOOL) usedir $(OUT)/HOL Library
     3.1 --- a/src/HOL/Library/Library.thy	Wed Feb 18 19:51:39 2009 -0800
     3.2 +++ b/src/HOL/Library/Library.thy	Wed Feb 18 20:14:45 2009 -0800
     3.3 @@ -37,6 +37,7 @@
     3.4    Permutation
     3.5    Pocklington
     3.6    Poly_Deriv
     3.7 +  Polynomial
     3.8    Primes
     3.9    Quickcheck
    3.10    Quicksort
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Library/Polynomial.thy	Wed Feb 18 20:14:45 2009 -0800
     4.3 @@ -0,0 +1,1441 @@
     4.4 +(*  Title:      HOL/Polynomial.thy
     4.5 +    Author:     Brian Huffman
     4.6 +                Based on an earlier development by Clemens Ballarin
     4.7 +*)
     4.8 +
     4.9 +header {* Univariate Polynomials *}
    4.10 +
    4.11 +theory Polynomial
    4.12 +imports Plain SetInterval Main
    4.13 +begin
    4.14 +
    4.15 +subsection {* Definition of type @{text poly} *}
    4.16 +
    4.17 +typedef (Poly) 'a poly = "{f::nat \<Rightarrow> 'a::zero. \<exists>n. \<forall>i>n. f i = 0}"
    4.18 +  morphisms coeff Abs_poly
    4.19 +  by auto
    4.20 +
    4.21 +lemma expand_poly_eq: "p = q \<longleftrightarrow> (\<forall>n. coeff p n = coeff q n)"
    4.22 +by (simp add: coeff_inject [symmetric] expand_fun_eq)
    4.23 +
    4.24 +lemma poly_ext: "(\<And>n. coeff p n = coeff q n) \<Longrightarrow> p = q"
    4.25 +by (simp add: expand_poly_eq)
    4.26 +
    4.27 +
    4.28 +subsection {* Degree of a polynomial *}
    4.29 +
    4.30 +definition
    4.31 +  degree :: "'a::zero poly \<Rightarrow> nat" where
    4.32 +  "degree p = (LEAST n. \<forall>i>n. coeff p i = 0)"
    4.33 +
    4.34 +lemma coeff_eq_0: "degree p < n \<Longrightarrow> coeff p n = 0"
    4.35 +proof -
    4.36 +  have "coeff p \<in> Poly"
    4.37 +    by (rule coeff)
    4.38 +  hence "\<exists>n. \<forall>i>n. coeff p i = 0"
    4.39 +    unfolding Poly_def by simp
    4.40 +  hence "\<forall>i>degree p. coeff p i = 0"
    4.41 +    unfolding degree_def by (rule LeastI_ex)
    4.42 +  moreover assume "degree p < n"
    4.43 +  ultimately show ?thesis by simp
    4.44 +qed
    4.45 +
    4.46 +lemma le_degree: "coeff p n \<noteq> 0 \<Longrightarrow> n \<le> degree p"
    4.47 +  by (erule contrapos_np, rule coeff_eq_0, simp)
    4.48 +
    4.49 +lemma degree_le: "\<forall>i>n. coeff p i = 0 \<Longrightarrow> degree p \<le> n"
    4.50 +  unfolding degree_def by (erule Least_le)
    4.51 +
    4.52 +lemma less_degree_imp: "n < degree p \<Longrightarrow> \<exists>i>n. coeff p i \<noteq> 0"
    4.53 +  unfolding degree_def by (drule not_less_Least, simp)
    4.54 +
    4.55 +
    4.56 +subsection {* The zero polynomial *}
    4.57 +
    4.58 +instantiation poly :: (zero) zero
    4.59 +begin
    4.60 +
    4.61 +definition
    4.62 +  zero_poly_def: "0 = Abs_poly (\<lambda>n. 0)"
    4.63 +
    4.64 +instance ..
    4.65 +end
    4.66 +
    4.67 +lemma coeff_0 [simp]: "coeff 0 n = 0"
    4.68 +  unfolding zero_poly_def
    4.69 +  by (simp add: Abs_poly_inverse Poly_def)
    4.70 +
    4.71 +lemma degree_0 [simp]: "degree 0 = 0"
    4.72 +  by (rule order_antisym [OF degree_le le0]) simp
    4.73 +
    4.74 +lemma leading_coeff_neq_0:
    4.75 +  assumes "p \<noteq> 0" shows "coeff p (degree p) \<noteq> 0"
    4.76 +proof (cases "degree p")
    4.77 +  case 0
    4.78 +  from `p \<noteq> 0` have "\<exists>n. coeff p n \<noteq> 0"
    4.79 +    by (simp add: expand_poly_eq)
    4.80 +  then obtain n where "coeff p n \<noteq> 0" ..
    4.81 +  hence "n \<le> degree p" by (rule le_degree)
    4.82 +  with `coeff p n \<noteq> 0` and `degree p = 0`
    4.83 +  show "coeff p (degree p) \<noteq> 0" by simp
    4.84 +next
    4.85 +  case (Suc n)
    4.86 +  from `degree p = Suc n` have "n < degree p" by simp
    4.87 +  hence "\<exists>i>n. coeff p i \<noteq> 0" by (rule less_degree_imp)
    4.88 +  then obtain i where "n < i" and "coeff p i \<noteq> 0" by fast
    4.89 +  from `degree p = Suc n` and `n < i` have "degree p \<le> i" by simp
    4.90 +  also from `coeff p i \<noteq> 0` have "i \<le> degree p" by (rule le_degree)
    4.91 +  finally have "degree p = i" .
    4.92 +  with `coeff p i \<noteq> 0` show "coeff p (degree p) \<noteq> 0" by simp
    4.93 +qed
    4.94 +
    4.95 +lemma leading_coeff_0_iff [simp]: "coeff p (degree p) = 0 \<longleftrightarrow> p = 0"
    4.96 +  by (cases "p = 0", simp, simp add: leading_coeff_neq_0)
    4.97 +
    4.98 +
    4.99 +subsection {* List-style constructor for polynomials *}
   4.100 +
   4.101 +definition
   4.102 +  pCons :: "'a::zero \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
   4.103 +where
   4.104 +  [code del]: "pCons a p = Abs_poly (nat_case a (coeff p))"
   4.105 +
   4.106 +syntax
   4.107 +  "_poly" :: "args \<Rightarrow> 'a poly"  ("[:(_):]")
   4.108 +
   4.109 +translations
   4.110 +  "[:x, xs:]" == "CONST pCons x [:xs:]"
   4.111 +  "[:x:]" == "CONST pCons x 0"
   4.112 +
   4.113 +lemma Poly_nat_case: "f \<in> Poly \<Longrightarrow> nat_case a f \<in> Poly"
   4.114 +  unfolding Poly_def by (auto split: nat.split)
   4.115 +
   4.116 +lemma coeff_pCons:
   4.117 +  "coeff (pCons a p) = nat_case a (coeff p)"
   4.118 +  unfolding pCons_def
   4.119 +  by (simp add: Abs_poly_inverse Poly_nat_case coeff)
   4.120 +
   4.121 +lemma coeff_pCons_0 [simp]: "coeff (pCons a p) 0 = a"
   4.122 +  by (simp add: coeff_pCons)
   4.123 +
   4.124 +lemma coeff_pCons_Suc [simp]: "coeff (pCons a p) (Suc n) = coeff p n"
   4.125 +  by (simp add: coeff_pCons)
   4.126 +
   4.127 +lemma degree_pCons_le: "degree (pCons a p) \<le> Suc (degree p)"
   4.128 +by (rule degree_le, simp add: coeff_eq_0 coeff_pCons split: nat.split)
   4.129 +
   4.130 +lemma degree_pCons_eq:
   4.131 +  "p \<noteq> 0 \<Longrightarrow> degree (pCons a p) = Suc (degree p)"
   4.132 +apply (rule order_antisym [OF degree_pCons_le])
   4.133 +apply (rule le_degree, simp)
   4.134 +done
   4.135 +
   4.136 +lemma degree_pCons_0: "degree (pCons a 0) = 0"
   4.137 +apply (rule order_antisym [OF _ le0])
   4.138 +apply (rule degree_le, simp add: coeff_pCons split: nat.split)
   4.139 +done
   4.140 +
   4.141 +lemma degree_pCons_eq_if [simp]:
   4.142 +  "degree (pCons a p) = (if p = 0 then 0 else Suc (degree p))"
   4.143 +apply (cases "p = 0", simp_all)
   4.144 +apply (rule order_antisym [OF _ le0])
   4.145 +apply (rule degree_le, simp add: coeff_pCons split: nat.split)
   4.146 +apply (rule order_antisym [OF degree_pCons_le])
   4.147 +apply (rule le_degree, simp)
   4.148 +done
   4.149 +
   4.150 +lemma pCons_0_0 [simp]: "pCons 0 0 = 0"
   4.151 +by (rule poly_ext, simp add: coeff_pCons split: nat.split)
   4.152 +
   4.153 +lemma pCons_eq_iff [simp]:
   4.154 +  "pCons a p = pCons b q \<longleftrightarrow> a = b \<and> p = q"
   4.155 +proof (safe)
   4.156 +  assume "pCons a p = pCons b q"
   4.157 +  then have "coeff (pCons a p) 0 = coeff (pCons b q) 0" by simp
   4.158 +  then show "a = b" by simp
   4.159 +next
   4.160 +  assume "pCons a p = pCons b q"
   4.161 +  then have "\<forall>n. coeff (pCons a p) (Suc n) =
   4.162 +                 coeff (pCons b q) (Suc n)" by simp
   4.163 +  then show "p = q" by (simp add: expand_poly_eq)
   4.164 +qed
   4.165 +
   4.166 +lemma pCons_eq_0_iff [simp]: "pCons a p = 0 \<longleftrightarrow> a = 0 \<and> p = 0"
   4.167 +  using pCons_eq_iff [of a p 0 0] by simp
   4.168 +
   4.169 +lemma Poly_Suc: "f \<in> Poly \<Longrightarrow> (\<lambda>n. f (Suc n)) \<in> Poly"
   4.170 +  unfolding Poly_def
   4.171 +  by (clarify, rule_tac x=n in exI, simp)
   4.172 +
   4.173 +lemma pCons_cases [cases type: poly]:
   4.174 +  obtains (pCons) a q where "p = pCons a q"
   4.175 +proof
   4.176 +  show "p = pCons (coeff p 0) (Abs_poly (\<lambda>n. coeff p (Suc n)))"
   4.177 +    by (rule poly_ext)
   4.178 +       (simp add: Abs_poly_inverse Poly_Suc coeff coeff_pCons
   4.179 +             split: nat.split)
   4.180 +qed
   4.181 +
   4.182 +lemma pCons_induct [case_names 0 pCons, induct type: poly]:
   4.183 +  assumes zero: "P 0"
   4.184 +  assumes pCons: "\<And>a p. P p \<Longrightarrow> P (pCons a p)"
   4.185 +  shows "P p"
   4.186 +proof (induct p rule: measure_induct_rule [where f=degree])
   4.187 +  case (less p)
   4.188 +  obtain a q where "p = pCons a q" by (rule pCons_cases)
   4.189 +  have "P q"
   4.190 +  proof (cases "q = 0")
   4.191 +    case True
   4.192 +    then show "P q" by (simp add: zero)
   4.193 +  next
   4.194 +    case False
   4.195 +    then have "degree (pCons a q) = Suc (degree q)"
   4.196 +      by (rule degree_pCons_eq)
   4.197 +    then have "degree q < degree p"
   4.198 +      using `p = pCons a q` by simp
   4.199 +    then show "P q"
   4.200 +      by (rule less.hyps)
   4.201 +  qed
   4.202 +  then have "P (pCons a q)"
   4.203 +    by (rule pCons)
   4.204 +  then show ?case
   4.205 +    using `p = pCons a q` by simp
   4.206 +qed
   4.207 +
   4.208 +
   4.209 +subsection {* Recursion combinator for polynomials *}
   4.210 +
   4.211 +function
   4.212 +  poly_rec :: "'b \<Rightarrow> ('a::zero \<Rightarrow> 'a poly \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a poly \<Rightarrow> 'b"
   4.213 +where
   4.214 +  poly_rec_pCons_eq_if [simp del, code del]:
   4.215 +    "poly_rec z f (pCons a p) = f a p (if p = 0 then z else poly_rec z f p)"
   4.216 +by (case_tac x, rename_tac q, case_tac q, auto)
   4.217 +
   4.218 +termination poly_rec
   4.219 +by (relation "measure (degree \<circ> snd \<circ> snd)", simp)
   4.220 +   (simp add: degree_pCons_eq)
   4.221 +
   4.222 +lemma poly_rec_0:
   4.223 +  "f 0 0 z = z \<Longrightarrow> poly_rec z f 0 = z"
   4.224 +  using poly_rec_pCons_eq_if [of z f 0 0] by simp
   4.225 +
   4.226 +lemma poly_rec_pCons:
   4.227 +  "f 0 0 z = z \<Longrightarrow> poly_rec z f (pCons a p) = f a p (poly_rec z f p)"
   4.228 +  by (simp add: poly_rec_pCons_eq_if poly_rec_0)
   4.229 +
   4.230 +
   4.231 +subsection {* Monomials *}
   4.232 +
   4.233 +definition
   4.234 +  monom :: "'a \<Rightarrow> nat \<Rightarrow> 'a::zero poly" where
   4.235 +  "monom a m = Abs_poly (\<lambda>n. if m = n then a else 0)"
   4.236 +
   4.237 +lemma coeff_monom [simp]: "coeff (monom a m) n = (if m=n then a else 0)"
   4.238 +  unfolding monom_def
   4.239 +  by (subst Abs_poly_inverse, auto simp add: Poly_def)
   4.240 +
   4.241 +lemma monom_0: "monom a 0 = pCons a 0"
   4.242 +  by (rule poly_ext, simp add: coeff_pCons split: nat.split)
   4.243 +
   4.244 +lemma monom_Suc: "monom a (Suc n) = pCons 0 (monom a n)"
   4.245 +  by (rule poly_ext, simp add: coeff_pCons split: nat.split)
   4.246 +
   4.247 +lemma monom_eq_0 [simp]: "monom 0 n = 0"
   4.248 +  by (rule poly_ext) simp
   4.249 +
   4.250 +lemma monom_eq_0_iff [simp]: "monom a n = 0 \<longleftrightarrow> a = 0"
   4.251 +  by (simp add: expand_poly_eq)
   4.252 +
   4.253 +lemma monom_eq_iff [simp]: "monom a n = monom b n \<longleftrightarrow> a = b"
   4.254 +  by (simp add: expand_poly_eq)
   4.255 +
   4.256 +lemma degree_monom_le: "degree (monom a n) \<le> n"
   4.257 +  by (rule degree_le, simp)
   4.258 +
   4.259 +lemma degree_monom_eq: "a \<noteq> 0 \<Longrightarrow> degree (monom a n) = n"
   4.260 +  apply (rule order_antisym [OF degree_monom_le])
   4.261 +  apply (rule le_degree, simp)
   4.262 +  done
   4.263 +
   4.264 +
   4.265 +subsection {* Addition and subtraction *}
   4.266 +
   4.267 +instantiation poly :: (comm_monoid_add) comm_monoid_add
   4.268 +begin
   4.269 +
   4.270 +definition
   4.271 +  plus_poly_def [code del]:
   4.272 +    "p + q = Abs_poly (\<lambda>n. coeff p n + coeff q n)"
   4.273 +
   4.274 +lemma Poly_add:
   4.275 +  fixes f g :: "nat \<Rightarrow> 'a"
   4.276 +  shows "\<lbrakk>f \<in> Poly; g \<in> Poly\<rbrakk> \<Longrightarrow> (\<lambda>n. f n + g n) \<in> Poly"
   4.277 +  unfolding Poly_def
   4.278 +  apply (clarify, rename_tac m n)
   4.279 +  apply (rule_tac x="max m n" in exI, simp)
   4.280 +  done
   4.281 +
   4.282 +lemma coeff_add [simp]:
   4.283 +  "coeff (p + q) n = coeff p n + coeff q n"
   4.284 +  unfolding plus_poly_def
   4.285 +  by (simp add: Abs_poly_inverse coeff Poly_add)
   4.286 +
   4.287 +instance proof
   4.288 +  fix p q r :: "'a poly"
   4.289 +  show "(p + q) + r = p + (q + r)"
   4.290 +    by (simp add: expand_poly_eq add_assoc)
   4.291 +  show "p + q = q + p"
   4.292 +    by (simp add: expand_poly_eq add_commute)
   4.293 +  show "0 + p = p"
   4.294 +    by (simp add: expand_poly_eq)
   4.295 +qed
   4.296 +
   4.297 +end
   4.298 +
   4.299 +instance poly :: (cancel_comm_monoid_add) cancel_comm_monoid_add
   4.300 +proof
   4.301 +  fix p q r :: "'a poly"
   4.302 +  assume "p + q = p + r" thus "q = r"
   4.303 +    by (simp add: expand_poly_eq)
   4.304 +qed
   4.305 +
   4.306 +instantiation poly :: (ab_group_add) ab_group_add
   4.307 +begin
   4.308 +
   4.309 +definition
   4.310 +  uminus_poly_def [code del]:
   4.311 +    "- p = Abs_poly (\<lambda>n. - coeff p n)"
   4.312 +
   4.313 +definition
   4.314 +  minus_poly_def [code del]:
   4.315 +    "p - q = Abs_poly (\<lambda>n. coeff p n - coeff q n)"
   4.316 +
   4.317 +lemma Poly_minus:
   4.318 +  fixes f :: "nat \<Rightarrow> 'a"
   4.319 +  shows "f \<in> Poly \<Longrightarrow> (\<lambda>n. - f n) \<in> Poly"
   4.320 +  unfolding Poly_def by simp
   4.321 +
   4.322 +lemma Poly_diff:
   4.323 +  fixes f g :: "nat \<Rightarrow> 'a"
   4.324 +  shows "\<lbrakk>f \<in> Poly; g \<in> Poly\<rbrakk> \<Longrightarrow> (\<lambda>n. f n - g n) \<in> Poly"
   4.325 +  unfolding diff_minus by (simp add: Poly_add Poly_minus)
   4.326 +
   4.327 +lemma coeff_minus [simp]: "coeff (- p) n = - coeff p n"
   4.328 +  unfolding uminus_poly_def
   4.329 +  by (simp add: Abs_poly_inverse coeff Poly_minus)
   4.330 +
   4.331 +lemma coeff_diff [simp]:
   4.332 +  "coeff (p - q) n = coeff p n - coeff q n"
   4.333 +  unfolding minus_poly_def
   4.334 +  by (simp add: Abs_poly_inverse coeff Poly_diff)
   4.335 +
   4.336 +instance proof
   4.337 +  fix p q :: "'a poly"
   4.338 +  show "- p + p = 0"
   4.339 +    by (simp add: expand_poly_eq)
   4.340 +  show "p - q = p + - q"
   4.341 +    by (simp add: expand_poly_eq diff_minus)
   4.342 +qed
   4.343 +
   4.344 +end
   4.345 +
   4.346 +lemma add_pCons [simp]:
   4.347 +  "pCons a p + pCons b q = pCons (a + b) (p + q)"
   4.348 +  by (rule poly_ext, simp add: coeff_pCons split: nat.split)
   4.349 +
   4.350 +lemma minus_pCons [simp]:
   4.351 +  "- pCons a p = pCons (- a) (- p)"
   4.352 +  by (rule poly_ext, simp add: coeff_pCons split: nat.split)
   4.353 +
   4.354 +lemma diff_pCons [simp]:
   4.355 +  "pCons a p - pCons b q = pCons (a - b) (p - q)"
   4.356 +  by (rule poly_ext, simp add: coeff_pCons split: nat.split)
   4.357 +
   4.358 +lemma degree_add_le_max: "degree (p + q) \<le> max (degree p) (degree q)"
   4.359 +  by (rule degree_le, auto simp add: coeff_eq_0)
   4.360 +
   4.361 +lemma degree_add_le:
   4.362 +  "\<lbrakk>degree p \<le> n; degree q \<le> n\<rbrakk> \<Longrightarrow> degree (p + q) \<le> n"
   4.363 +  by (auto intro: order_trans degree_add_le_max)
   4.364 +
   4.365 +lemma degree_add_less:
   4.366 +  "\<lbrakk>degree p < n; degree q < n\<rbrakk> \<Longrightarrow> degree (p + q) < n"
   4.367 +  by (auto intro: le_less_trans degree_add_le_max)
   4.368 +
   4.369 +lemma degree_add_eq_right:
   4.370 +  "degree p < degree q \<Longrightarrow> degree (p + q) = degree q"
   4.371 +  apply (cases "q = 0", simp)
   4.372 +  apply (rule order_antisym)
   4.373 +  apply (simp add: degree_add_le)
   4.374 +  apply (rule le_degree)
   4.375 +  apply (simp add: coeff_eq_0)
   4.376 +  done
   4.377 +
   4.378 +lemma degree_add_eq_left:
   4.379 +  "degree q < degree p \<Longrightarrow> degree (p + q) = degree p"
   4.380 +  using degree_add_eq_right [of q p]
   4.381 +  by (simp add: add_commute)
   4.382 +
   4.383 +lemma degree_minus [simp]: "degree (- p) = degree p"
   4.384 +  unfolding degree_def by simp
   4.385 +
   4.386 +lemma degree_diff_le_max: "degree (p - q) \<le> max (degree p) (degree q)"
   4.387 +  using degree_add_le [where p=p and q="-q"]
   4.388 +  by (simp add: diff_minus)
   4.389 +
   4.390 +lemma degree_diff_le:
   4.391 +  "\<lbrakk>degree p \<le> n; degree q \<le> n\<rbrakk> \<Longrightarrow> degree (p - q) \<le> n"
   4.392 +  by (simp add: diff_minus degree_add_le)
   4.393 +
   4.394 +lemma degree_diff_less:
   4.395 +  "\<lbrakk>degree p < n; degree q < n\<rbrakk> \<Longrightarrow> degree (p - q) < n"
   4.396 +  by (simp add: diff_minus degree_add_less)
   4.397 +
   4.398 +lemma add_monom: "monom a n + monom b n = monom (a + b) n"
   4.399 +  by (rule poly_ext) simp
   4.400 +
   4.401 +lemma diff_monom: "monom a n - monom b n = monom (a - b) n"
   4.402 +  by (rule poly_ext) simp
   4.403 +
   4.404 +lemma minus_monom: "- monom a n = monom (-a) n"
   4.405 +  by (rule poly_ext) simp
   4.406 +
   4.407 +lemma coeff_setsum: "coeff (\<Sum>x\<in>A. p x) i = (\<Sum>x\<in>A. coeff (p x) i)"
   4.408 +  by (cases "finite A", induct set: finite, simp_all)
   4.409 +
   4.410 +lemma monom_setsum: "monom (\<Sum>x\<in>A. a x) n = (\<Sum>x\<in>A. monom (a x) n)"
   4.411 +  by (rule poly_ext) (simp add: coeff_setsum)
   4.412 +
   4.413 +
   4.414 +subsection {* Multiplication by a constant *}
   4.415 +
   4.416 +definition
   4.417 +  smult :: "'a::comm_semiring_0 \<Rightarrow> 'a poly \<Rightarrow> 'a poly" where
   4.418 +  "smult a p = Abs_poly (\<lambda>n. a * coeff p n)"
   4.419 +
   4.420 +lemma Poly_smult:
   4.421 +  fixes f :: "nat \<Rightarrow> 'a::comm_semiring_0"
   4.422 +  shows "f \<in> Poly \<Longrightarrow> (\<lambda>n. a * f n) \<in> Poly"
   4.423 +  unfolding Poly_def
   4.424 +  by (clarify, rule_tac x=n in exI, simp)
   4.425 +
   4.426 +lemma coeff_smult [simp]: "coeff (smult a p) n = a * coeff p n"
   4.427 +  unfolding smult_def
   4.428 +  by (simp add: Abs_poly_inverse Poly_smult coeff)
   4.429 +
   4.430 +lemma degree_smult_le: "degree (smult a p) \<le> degree p"
   4.431 +  by (rule degree_le, simp add: coeff_eq_0)
   4.432 +
   4.433 +lemma smult_smult [simp]: "smult a (smult b p) = smult (a * b) p"
   4.434 +  by (rule poly_ext, simp add: mult_assoc)
   4.435 +
   4.436 +lemma smult_0_right [simp]: "smult a 0 = 0"
   4.437 +  by (rule poly_ext, simp)
   4.438 +
   4.439 +lemma smult_0_left [simp]: "smult 0 p = 0"
   4.440 +  by (rule poly_ext, simp)
   4.441 +
   4.442 +lemma smult_1_left [simp]: "smult (1::'a::comm_semiring_1) p = p"
   4.443 +  by (rule poly_ext, simp)
   4.444 +
   4.445 +lemma smult_add_right:
   4.446 +  "smult a (p + q) = smult a p + smult a q"
   4.447 +  by (rule poly_ext, simp add: algebra_simps)
   4.448 +
   4.449 +lemma smult_add_left:
   4.450 +  "smult (a + b) p = smult a p + smult b p"
   4.451 +  by (rule poly_ext, simp add: algebra_simps)
   4.452 +
   4.453 +lemma smult_minus_right [simp]:
   4.454 +  "smult (a::'a::comm_ring) (- p) = - smult a p"
   4.455 +  by (rule poly_ext, simp)
   4.456 +
   4.457 +lemma smult_minus_left [simp]:
   4.458 +  "smult (- a::'a::comm_ring) p = - smult a p"
   4.459 +  by (rule poly_ext, simp)
   4.460 +
   4.461 +lemma smult_diff_right:
   4.462 +  "smult (a::'a::comm_ring) (p - q) = smult a p - smult a q"
   4.463 +  by (rule poly_ext, simp add: algebra_simps)
   4.464 +
   4.465 +lemma smult_diff_left:
   4.466 +  "smult (a - b::'a::comm_ring) p = smult a p - smult b p"
   4.467 +  by (rule poly_ext, simp add: algebra_simps)
   4.468 +
   4.469 +lemmas smult_distribs =
   4.470 +  smult_add_left smult_add_right
   4.471 +  smult_diff_left smult_diff_right
   4.472 +
   4.473 +lemma smult_pCons [simp]:
   4.474 +  "smult a (pCons b p) = pCons (a * b) (smult a p)"
   4.475 +  by (rule poly_ext, simp add: coeff_pCons split: nat.split)
   4.476 +
   4.477 +lemma smult_monom: "smult a (monom b n) = monom (a * b) n"
   4.478 +  by (induct n, simp add: monom_0, simp add: monom_Suc)
   4.479 +
   4.480 +lemma degree_smult_eq [simp]:
   4.481 +  fixes a :: "'a::idom"
   4.482 +  shows "degree (smult a p) = (if a = 0 then 0 else degree p)"
   4.483 +  by (cases "a = 0", simp, simp add: degree_def)
   4.484 +
   4.485 +lemma smult_eq_0_iff [simp]:
   4.486 +  fixes a :: "'a::idom"
   4.487 +  shows "smult a p = 0 \<longleftrightarrow> a = 0 \<or> p = 0"
   4.488 +  by (simp add: expand_poly_eq)
   4.489 +
   4.490 +
   4.491 +subsection {* Multiplication of polynomials *}
   4.492 +
   4.493 +text {* TODO: move to SetInterval.thy *}
   4.494 +lemma setsum_atMost_Suc_shift:
   4.495 +  fixes f :: "nat \<Rightarrow> 'a::comm_monoid_add"
   4.496 +  shows "(\<Sum>i\<le>Suc n. f i) = f 0 + (\<Sum>i\<le>n. f (Suc i))"
   4.497 +proof (induct n)
   4.498 +  case 0 show ?case by simp
   4.499 +next
   4.500 +  case (Suc n) note IH = this
   4.501 +  have "(\<Sum>i\<le>Suc (Suc n). f i) = (\<Sum>i\<le>Suc n. f i) + f (Suc (Suc n))"
   4.502 +    by (rule setsum_atMost_Suc)
   4.503 +  also have "(\<Sum>i\<le>Suc n. f i) = f 0 + (\<Sum>i\<le>n. f (Suc i))"
   4.504 +    by (rule IH)
   4.505 +  also have "f 0 + (\<Sum>i\<le>n. f (Suc i)) + f (Suc (Suc n)) =
   4.506 +             f 0 + ((\<Sum>i\<le>n. f (Suc i)) + f (Suc (Suc n)))"
   4.507 +    by (rule add_assoc)
   4.508 +  also have "(\<Sum>i\<le>n. f (Suc i)) + f (Suc (Suc n)) = (\<Sum>i\<le>Suc n. f (Suc i))"
   4.509 +    by (rule setsum_atMost_Suc [symmetric])
   4.510 +  finally show ?case .
   4.511 +qed
   4.512 +
   4.513 +instantiation poly :: (comm_semiring_0) comm_semiring_0
   4.514 +begin
   4.515 +
   4.516 +definition
   4.517 +  times_poly_def [code del]:
   4.518 +    "p * q = poly_rec 0 (\<lambda>a p pq. smult a q + pCons 0 pq) p"
   4.519 +
   4.520 +lemma mult_poly_0_left: "(0::'a poly) * q = 0"
   4.521 +  unfolding times_poly_def by (simp add: poly_rec_0)
   4.522 +
   4.523 +lemma mult_pCons_left [simp]:
   4.524 +  "pCons a p * q = smult a q + pCons 0 (p * q)"
   4.525 +  unfolding times_poly_def by (simp add: poly_rec_pCons)
   4.526 +
   4.527 +lemma mult_poly_0_right: "p * (0::'a poly) = 0"
   4.528 +  by (induct p, simp add: mult_poly_0_left, simp)
   4.529 +
   4.530 +lemma mult_pCons_right [simp]:
   4.531 +  "p * pCons a q = smult a p + pCons 0 (p * q)"
   4.532 +  by (induct p, simp add: mult_poly_0_left, simp add: algebra_simps)
   4.533 +
   4.534 +lemmas mult_poly_0 = mult_poly_0_left mult_poly_0_right
   4.535 +
   4.536 +lemma mult_smult_left [simp]: "smult a p * q = smult a (p * q)"
   4.537 +  by (induct p, simp add: mult_poly_0, simp add: smult_add_right)
   4.538 +
   4.539 +lemma mult_smult_right [simp]: "p * smult a q = smult a (p * q)"
   4.540 +  by (induct q, simp add: mult_poly_0, simp add: smult_add_right)
   4.541 +
   4.542 +lemma mult_poly_add_left:
   4.543 +  fixes p q r :: "'a poly"
   4.544 +  shows "(p + q) * r = p * r + q * r"
   4.545 +  by (induct r, simp add: mult_poly_0,
   4.546 +                simp add: smult_distribs algebra_simps)
   4.547 +
   4.548 +instance proof
   4.549 +  fix p q r :: "'a poly"
   4.550 +  show 0: "0 * p = 0"
   4.551 +    by (rule mult_poly_0_left)
   4.552 +  show "p * 0 = 0"
   4.553 +    by (rule mult_poly_0_right)
   4.554 +  show "(p + q) * r = p * r + q * r"
   4.555 +    by (rule mult_poly_add_left)
   4.556 +  show "(p * q) * r = p * (q * r)"
   4.557 +    by (induct p, simp add: mult_poly_0, simp add: mult_poly_add_left)
   4.558 +  show "p * q = q * p"
   4.559 +    by (induct p, simp add: mult_poly_0, simp)
   4.560 +qed
   4.561 +
   4.562 +end
   4.563 +
   4.564 +instance poly :: (comm_semiring_0_cancel) comm_semiring_0_cancel ..
   4.565 +
   4.566 +lemma coeff_mult:
   4.567 +  "coeff (p * q) n = (\<Sum>i\<le>n. coeff p i * coeff q (n-i))"
   4.568 +proof (induct p arbitrary: n)
   4.569 +  case 0 show ?case by simp
   4.570 +next
   4.571 +  case (pCons a p n) thus ?case
   4.572 +    by (cases n, simp, simp add: setsum_atMost_Suc_shift
   4.573 +                            del: setsum_atMost_Suc)
   4.574 +qed
   4.575 +
   4.576 +lemma degree_mult_le: "degree (p * q) \<le> degree p + degree q"
   4.577 +apply (rule degree_le)
   4.578 +apply (induct p)
   4.579 +apply simp
   4.580 +apply (simp add: coeff_eq_0 coeff_pCons split: nat.split)
   4.581 +done
   4.582 +
   4.583 +lemma mult_monom: "monom a m * monom b n = monom (a * b) (m + n)"
   4.584 +  by (induct m, simp add: monom_0 smult_monom, simp add: monom_Suc)
   4.585 +
   4.586 +
   4.587 +subsection {* The unit polynomial and exponentiation *}
   4.588 +
   4.589 +instantiation poly :: (comm_semiring_1) comm_semiring_1
   4.590 +begin
   4.591 +
   4.592 +definition
   4.593 +  one_poly_def:
   4.594 +    "1 = pCons 1 0"
   4.595 +
   4.596 +instance proof
   4.597 +  fix p :: "'a poly" show "1 * p = p"
   4.598 +    unfolding one_poly_def
   4.599 +    by simp
   4.600 +next
   4.601 +  show "0 \<noteq> (1::'a poly)"
   4.602 +    unfolding one_poly_def by simp
   4.603 +qed
   4.604 +
   4.605 +end
   4.606 +
   4.607 +instance poly :: (comm_semiring_1_cancel) comm_semiring_1_cancel ..
   4.608 +
   4.609 +lemma coeff_1 [simp]: "coeff 1 n = (if n = 0 then 1 else 0)"
   4.610 +  unfolding one_poly_def
   4.611 +  by (simp add: coeff_pCons split: nat.split)
   4.612 +
   4.613 +lemma degree_1 [simp]: "degree 1 = 0"
   4.614 +  unfolding one_poly_def
   4.615 +  by (rule degree_pCons_0)
   4.616 +
   4.617 +text {* Lemmas about divisibility *}
   4.618 +
   4.619 +lemma dvd_smult: "p dvd q \<Longrightarrow> p dvd smult a q"
   4.620 +proof -
   4.621 +  assume "p dvd q"
   4.622 +  then obtain k where "q = p * k" ..
   4.623 +  then have "smult a q = p * smult a k" by simp
   4.624 +  then show "p dvd smult a q" ..
   4.625 +qed
   4.626 +
   4.627 +lemma dvd_smult_cancel:
   4.628 +  fixes a :: "'a::field"
   4.629 +  shows "p dvd smult a q \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> p dvd q"
   4.630 +  by (drule dvd_smult [where a="inverse a"]) simp
   4.631 +
   4.632 +lemma dvd_smult_iff:
   4.633 +  fixes a :: "'a::field"
   4.634 +  shows "a \<noteq> 0 \<Longrightarrow> p dvd smult a q \<longleftrightarrow> p dvd q"
   4.635 +  by (safe elim!: dvd_smult dvd_smult_cancel)
   4.636 +
   4.637 +instantiation poly :: (comm_semiring_1) recpower
   4.638 +begin
   4.639 +
   4.640 +primrec power_poly where
   4.641 +  power_poly_0: "(p::'a poly) ^ 0 = 1"
   4.642 +| power_poly_Suc: "(p::'a poly) ^ (Suc n) = p * p ^ n"
   4.643 +
   4.644 +instance
   4.645 +  by default simp_all
   4.646 +
   4.647 +end
   4.648 +
   4.649 +lemma degree_power_le: "degree (p ^ n) \<le> degree p * n"
   4.650 +by (induct n, simp, auto intro: order_trans degree_mult_le)
   4.651 +
   4.652 +instance poly :: (comm_ring) comm_ring ..
   4.653 +
   4.654 +instance poly :: (comm_ring_1) comm_ring_1 ..
   4.655 +
   4.656 +instantiation poly :: (comm_ring_1) number_ring
   4.657 +begin
   4.658 +
   4.659 +definition
   4.660 +  "number_of k = (of_int k :: 'a poly)"
   4.661 +
   4.662 +instance
   4.663 +  by default (rule number_of_poly_def)
   4.664 +
   4.665 +end
   4.666 +
   4.667 +
   4.668 +subsection {* Polynomials form an integral domain *}
   4.669 +
   4.670 +lemma coeff_mult_degree_sum:
   4.671 +  "coeff (p * q) (degree p + degree q) =
   4.672 +   coeff p (degree p) * coeff q (degree q)"
   4.673 +  by (induct p, simp, simp add: coeff_eq_0)
   4.674 +
   4.675 +instance poly :: (idom) idom
   4.676 +proof
   4.677 +  fix p q :: "'a poly"
   4.678 +  assume "p \<noteq> 0" and "q \<noteq> 0"
   4.679 +  have "coeff (p * q) (degree p + degree q) =
   4.680 +        coeff p (degree p) * coeff q (degree q)"
   4.681 +    by (rule coeff_mult_degree_sum)
   4.682 +  also have "coeff p (degree p) * coeff q (degree q) \<noteq> 0"
   4.683 +    using `p \<noteq> 0` and `q \<noteq> 0` by simp
   4.684 +  finally have "\<exists>n. coeff (p * q) n \<noteq> 0" ..
   4.685 +  thus "p * q \<noteq> 0" by (simp add: expand_poly_eq)
   4.686 +qed
   4.687 +
   4.688 +lemma degree_mult_eq:
   4.689 +  fixes p q :: "'a::idom poly"
   4.690 +  shows "\<lbrakk>p \<noteq> 0; q \<noteq> 0\<rbrakk> \<Longrightarrow> degree (p * q) = degree p + degree q"
   4.691 +apply (rule order_antisym [OF degree_mult_le le_degree])
   4.692 +apply (simp add: coeff_mult_degree_sum)
   4.693 +done
   4.694 +
   4.695 +lemma dvd_imp_degree_le:
   4.696 +  fixes p q :: "'a::idom poly"
   4.697 +  shows "\<lbrakk>p dvd q; q \<noteq> 0\<rbrakk> \<Longrightarrow> degree p \<le> degree q"
   4.698 +  by (erule dvdE, simp add: degree_mult_eq)
   4.699 +
   4.700 +
   4.701 +subsection {* Polynomials form an ordered integral domain *}
   4.702 +
   4.703 +definition
   4.704 +  pos_poly :: "'a::ordered_idom poly \<Rightarrow> bool"
   4.705 +where
   4.706 +  "pos_poly p \<longleftrightarrow> 0 < coeff p (degree p)"
   4.707 +
   4.708 +lemma pos_poly_pCons:
   4.709 +  "pos_poly (pCons a p) \<longleftrightarrow> pos_poly p \<or> (p = 0 \<and> 0 < a)"
   4.710 +  unfolding pos_poly_def by simp
   4.711 +
   4.712 +lemma not_pos_poly_0 [simp]: "\<not> pos_poly 0"
   4.713 +  unfolding pos_poly_def by simp
   4.714 +
   4.715 +lemma pos_poly_add: "\<lbrakk>pos_poly p; pos_poly q\<rbrakk> \<Longrightarrow> pos_poly (p + q)"
   4.716 +  apply (induct p arbitrary: q, simp)
   4.717 +  apply (case_tac q, force simp add: pos_poly_pCons add_pos_pos)
   4.718 +  done
   4.719 +
   4.720 +lemma pos_poly_mult: "\<lbrakk>pos_poly p; pos_poly q\<rbrakk> \<Longrightarrow> pos_poly (p * q)"
   4.721 +  unfolding pos_poly_def
   4.722 +  apply (subgoal_tac "p \<noteq> 0 \<and> q \<noteq> 0")
   4.723 +  apply (simp add: degree_mult_eq coeff_mult_degree_sum mult_pos_pos)
   4.724 +  apply auto
   4.725 +  done
   4.726 +
   4.727 +lemma pos_poly_total: "p = 0 \<or> pos_poly p \<or> pos_poly (- p)"
   4.728 +by (induct p) (auto simp add: pos_poly_pCons)
   4.729 +
   4.730 +instantiation poly :: (ordered_idom) ordered_idom
   4.731 +begin
   4.732 +
   4.733 +definition
   4.734 +  [code del]:
   4.735 +    "x < y \<longleftrightarrow> pos_poly (y - x)"
   4.736 +
   4.737 +definition
   4.738 +  [code del]:
   4.739 +    "x \<le> y \<longleftrightarrow> x = y \<or> pos_poly (y - x)"
   4.740 +
   4.741 +definition
   4.742 +  [code del]:
   4.743 +    "abs (x::'a poly) = (if x < 0 then - x else x)"
   4.744 +
   4.745 +definition
   4.746 +  [code del]:
   4.747 +    "sgn (x::'a poly) = (if x = 0 then 0 else if 0 < x then 1 else - 1)"
   4.748 +
   4.749 +instance proof
   4.750 +  fix x y :: "'a poly"
   4.751 +  show "x < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x"
   4.752 +    unfolding less_eq_poly_def less_poly_def
   4.753 +    apply safe
   4.754 +    apply simp
   4.755 +    apply (drule (1) pos_poly_add)
   4.756 +    apply simp
   4.757 +    done
   4.758 +next
   4.759 +  fix x :: "'a poly" show "x \<le> x"
   4.760 +    unfolding less_eq_poly_def by simp
   4.761 +next
   4.762 +  fix x y z :: "'a poly"
   4.763 +  assume "x \<le> y" and "y \<le> z" thus "x \<le> z"
   4.764 +    unfolding less_eq_poly_def
   4.765 +    apply safe
   4.766 +    apply (drule (1) pos_poly_add)
   4.767 +    apply (simp add: algebra_simps)
   4.768 +    done
   4.769 +next
   4.770 +  fix x y :: "'a poly"
   4.771 +  assume "x \<le> y" and "y \<le> x" thus "x = y"
   4.772 +    unfolding less_eq_poly_def
   4.773 +    apply safe
   4.774 +    apply (drule (1) pos_poly_add)
   4.775 +    apply simp
   4.776 +    done
   4.777 +next
   4.778 +  fix x y z :: "'a poly"
   4.779 +  assume "x \<le> y" thus "z + x \<le> z + y"
   4.780 +    unfolding less_eq_poly_def
   4.781 +    apply safe
   4.782 +    apply (simp add: algebra_simps)
   4.783 +    done
   4.784 +next
   4.785 +  fix x y :: "'a poly"
   4.786 +  show "x \<le> y \<or> y \<le> x"
   4.787 +    unfolding less_eq_poly_def
   4.788 +    using pos_poly_total [of "x - y"]
   4.789 +    by auto
   4.790 +next
   4.791 +  fix x y z :: "'a poly"
   4.792 +  assume "x < y" and "0 < z"
   4.793 +  thus "z * x < z * y"
   4.794 +    unfolding less_poly_def
   4.795 +    by (simp add: right_diff_distrib [symmetric] pos_poly_mult)
   4.796 +next
   4.797 +  fix x :: "'a poly"
   4.798 +  show "\<bar>x\<bar> = (if x < 0 then - x else x)"
   4.799 +    by (rule abs_poly_def)
   4.800 +next
   4.801 +  fix x :: "'a poly"
   4.802 +  show "sgn x = (if x = 0 then 0 else if 0 < x then 1 else - 1)"
   4.803 +    by (rule sgn_poly_def)
   4.804 +qed
   4.805 +
   4.806 +end
   4.807 +
   4.808 +text {* TODO: Simplification rules for comparisons *}
   4.809 +
   4.810 +
   4.811 +subsection {* Long division of polynomials *}
   4.812 +
   4.813 +definition
   4.814 +  pdivmod_rel :: "'a::field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<Rightarrow> bool"
   4.815 +where
   4.816 +  [code del]:
   4.817 +  "pdivmod_rel x y q r \<longleftrightarrow>
   4.818 +    x = q * y + r \<and> (if y = 0 then q = 0 else r = 0 \<or> degree r < degree y)"
   4.819 +
   4.820 +lemma pdivmod_rel_0:
   4.821 +  "pdivmod_rel 0 y 0 0"
   4.822 +  unfolding pdivmod_rel_def by simp
   4.823 +
   4.824 +lemma pdivmod_rel_by_0:
   4.825 +  "pdivmod_rel x 0 0 x"
   4.826 +  unfolding pdivmod_rel_def by simp
   4.827 +
   4.828 +lemma eq_zero_or_degree_less:
   4.829 +  assumes "degree p \<le> n" and "coeff p n = 0"
   4.830 +  shows "p = 0 \<or> degree p < n"
   4.831 +proof (cases n)
   4.832 +  case 0
   4.833 +  with `degree p \<le> n` and `coeff p n = 0`
   4.834 +  have "coeff p (degree p) = 0" by simp
   4.835 +  then have "p = 0" by simp
   4.836 +  then show ?thesis ..
   4.837 +next
   4.838 +  case (Suc m)
   4.839 +  have "\<forall>i>n. coeff p i = 0"
   4.840 +    using `degree p \<le> n` by (simp add: coeff_eq_0)
   4.841 +  then have "\<forall>i\<ge>n. coeff p i = 0"
   4.842 +    using `coeff p n = 0` by (simp add: le_less)
   4.843 +  then have "\<forall>i>m. coeff p i = 0"
   4.844 +    using `n = Suc m` by (simp add: less_eq_Suc_le)
   4.845 +  then have "degree p \<le> m"
   4.846 +    by (rule degree_le)
   4.847 +  then have "degree p < n"
   4.848 +    using `n = Suc m` by (simp add: less_Suc_eq_le)
   4.849 +  then show ?thesis ..
   4.850 +qed
   4.851 +
   4.852 +lemma pdivmod_rel_pCons:
   4.853 +  assumes rel: "pdivmod_rel x y q r"
   4.854 +  assumes y: "y \<noteq> 0"
   4.855 +  assumes b: "b = coeff (pCons a r) (degree y) / coeff y (degree y)"
   4.856 +  shows "pdivmod_rel (pCons a x) y (pCons b q) (pCons a r - smult b y)"
   4.857 +    (is "pdivmod_rel ?x y ?q ?r")
   4.858 +proof -
   4.859 +  have x: "x = q * y + r" and r: "r = 0 \<or> degree r < degree y"
   4.860 +    using assms unfolding pdivmod_rel_def by simp_all
   4.861 +
   4.862 +  have 1: "?x = ?q * y + ?r"
   4.863 +    using b x by simp
   4.864 +
   4.865 +  have 2: "?r = 0 \<or> degree ?r < degree y"
   4.866 +  proof (rule eq_zero_or_degree_less)
   4.867 +    show "degree ?r \<le> degree y"
   4.868 +    proof (rule degree_diff_le)
   4.869 +      show "degree (pCons a r) \<le> degree y"
   4.870 +        using r by auto
   4.871 +      show "degree (smult b y) \<le> degree y"
   4.872 +        by (rule degree_smult_le)
   4.873 +    qed
   4.874 +  next
   4.875 +    show "coeff ?r (degree y) = 0"
   4.876 +      using `y \<noteq> 0` unfolding b by simp
   4.877 +  qed
   4.878 +
   4.879 +  from 1 2 show ?thesis
   4.880 +    unfolding pdivmod_rel_def
   4.881 +    using `y \<noteq> 0` by simp
   4.882 +qed
   4.883 +
   4.884 +lemma pdivmod_rel_exists: "\<exists>q r. pdivmod_rel x y q r"
   4.885 +apply (cases "y = 0")
   4.886 +apply (fast intro!: pdivmod_rel_by_0)
   4.887 +apply (induct x)
   4.888 +apply (fast intro!: pdivmod_rel_0)
   4.889 +apply (fast intro!: pdivmod_rel_pCons)
   4.890 +done
   4.891 +
   4.892 +lemma pdivmod_rel_unique:
   4.893 +  assumes 1: "pdivmod_rel x y q1 r1"
   4.894 +  assumes 2: "pdivmod_rel x y q2 r2"
   4.895 +  shows "q1 = q2 \<and> r1 = r2"
   4.896 +proof (cases "y = 0")
   4.897 +  assume "y = 0" with assms show ?thesis
   4.898 +    by (simp add: pdivmod_rel_def)
   4.899 +next
   4.900 +  assume [simp]: "y \<noteq> 0"
   4.901 +  from 1 have q1: "x = q1 * y + r1" and r1: "r1 = 0 \<or> degree r1 < degree y"
   4.902 +    unfolding pdivmod_rel_def by simp_all
   4.903 +  from 2 have q2: "x = q2 * y + r2" and r2: "r2 = 0 \<or> degree r2 < degree y"
   4.904 +    unfolding pdivmod_rel_def by simp_all
   4.905 +  from q1 q2 have q3: "(q1 - q2) * y = r2 - r1"
   4.906 +    by (simp add: algebra_simps)
   4.907 +  from r1 r2 have r3: "(r2 - r1) = 0 \<or> degree (r2 - r1) < degree y"
   4.908 +    by (auto intro: degree_diff_less)
   4.909 +
   4.910 +  show "q1 = q2 \<and> r1 = r2"
   4.911 +  proof (rule ccontr)
   4.912 +    assume "\<not> (q1 = q2 \<and> r1 = r2)"
   4.913 +    with q3 have "q1 \<noteq> q2" and "r1 \<noteq> r2" by auto
   4.914 +    with r3 have "degree (r2 - r1) < degree y" by simp
   4.915 +    also have "degree y \<le> degree (q1 - q2) + degree y" by simp
   4.916 +    also have "\<dots> = degree ((q1 - q2) * y)"
   4.917 +      using `q1 \<noteq> q2` by (simp add: degree_mult_eq)
   4.918 +    also have "\<dots> = degree (r2 - r1)"
   4.919 +      using q3 by simp
   4.920 +    finally have "degree (r2 - r1) < degree (r2 - r1)" .
   4.921 +    then show "False" by simp
   4.922 +  qed
   4.923 +qed
   4.924 +
   4.925 +lemma pdivmod_rel_0_iff: "pdivmod_rel 0 y q r \<longleftrightarrow> q = 0 \<and> r = 0"
   4.926 +by (auto dest: pdivmod_rel_unique intro: pdivmod_rel_0)
   4.927 +
   4.928 +lemma pdivmod_rel_by_0_iff: "pdivmod_rel x 0 q r \<longleftrightarrow> q = 0 \<and> r = x"
   4.929 +by (auto dest: pdivmod_rel_unique intro: pdivmod_rel_by_0)
   4.930 +
   4.931 +lemmas pdivmod_rel_unique_div =
   4.932 +  pdivmod_rel_unique [THEN conjunct1, standard]
   4.933 +
   4.934 +lemmas pdivmod_rel_unique_mod =
   4.935 +  pdivmod_rel_unique [THEN conjunct2, standard]
   4.936 +
   4.937 +instantiation poly :: (field) ring_div
   4.938 +begin
   4.939 +
   4.940 +definition div_poly where
   4.941 +  [code del]: "x div y = (THE q. \<exists>r. pdivmod_rel x y q r)"
   4.942 +
   4.943 +definition mod_poly where
   4.944 +  [code del]: "x mod y = (THE r. \<exists>q. pdivmod_rel x y q r)"
   4.945 +
   4.946 +lemma div_poly_eq:
   4.947 +  "pdivmod_rel x y q r \<Longrightarrow> x div y = q"
   4.948 +unfolding div_poly_def
   4.949 +by (fast elim: pdivmod_rel_unique_div)
   4.950 +
   4.951 +lemma mod_poly_eq:
   4.952 +  "pdivmod_rel x y q r \<Longrightarrow> x mod y = r"
   4.953 +unfolding mod_poly_def
   4.954 +by (fast elim: pdivmod_rel_unique_mod)
   4.955 +
   4.956 +lemma pdivmod_rel:
   4.957 +  "pdivmod_rel x y (x div y) (x mod y)"
   4.958 +proof -
   4.959 +  from pdivmod_rel_exists
   4.960 +    obtain q r where "pdivmod_rel x y q r" by fast
   4.961 +  thus ?thesis
   4.962 +    by (simp add: div_poly_eq mod_poly_eq)
   4.963 +qed
   4.964 +
   4.965 +instance proof
   4.966 +  fix x y :: "'a poly"
   4.967 +  show "x div y * y + x mod y = x"
   4.968 +    using pdivmod_rel [of x y]
   4.969 +    by (simp add: pdivmod_rel_def)
   4.970 +next
   4.971 +  fix x :: "'a poly"
   4.972 +  have "pdivmod_rel x 0 0 x"
   4.973 +    by (rule pdivmod_rel_by_0)
   4.974 +  thus "x div 0 = 0"
   4.975 +    by (rule div_poly_eq)
   4.976 +next
   4.977 +  fix y :: "'a poly"
   4.978 +  have "pdivmod_rel 0 y 0 0"
   4.979 +    by (rule pdivmod_rel_0)
   4.980 +  thus "0 div y = 0"
   4.981 +    by (rule div_poly_eq)
   4.982 +next
   4.983 +  fix x y z :: "'a poly"
   4.984 +  assume "y \<noteq> 0"
   4.985 +  hence "pdivmod_rel (x + z * y) y (z + x div y) (x mod y)"
   4.986 +    using pdivmod_rel [of x y]
   4.987 +    by (simp add: pdivmod_rel_def left_distrib)
   4.988 +  thus "(x + z * y) div y = z + x div y"
   4.989 +    by (rule div_poly_eq)
   4.990 +qed
   4.991 +
   4.992 +end
   4.993 +
   4.994 +lemma degree_mod_less:
   4.995 +  "y \<noteq> 0 \<Longrightarrow> x mod y = 0 \<or> degree (x mod y) < degree y"
   4.996 +  using pdivmod_rel [of x y]
   4.997 +  unfolding pdivmod_rel_def by simp
   4.998 +
   4.999 +lemma div_poly_less: "degree x < degree y \<Longrightarrow> x div y = 0"
  4.1000 +proof -
  4.1001 +  assume "degree x < degree y"
  4.1002 +  hence "pdivmod_rel x y 0 x"
  4.1003 +    by (simp add: pdivmod_rel_def)
  4.1004 +  thus "x div y = 0" by (rule div_poly_eq)
  4.1005 +qed
  4.1006 +
  4.1007 +lemma mod_poly_less: "degree x < degree y \<Longrightarrow> x mod y = x"
  4.1008 +proof -
  4.1009 +  assume "degree x < degree y"
  4.1010 +  hence "pdivmod_rel x y 0 x"
  4.1011 +    by (simp add: pdivmod_rel_def)
  4.1012 +  thus "x mod y = x" by (rule mod_poly_eq)
  4.1013 +qed
  4.1014 +
  4.1015 +lemma pdivmod_rel_smult_left:
  4.1016 +  "pdivmod_rel x y q r
  4.1017 +    \<Longrightarrow> pdivmod_rel (smult a x) y (smult a q) (smult a r)"
  4.1018 +  unfolding pdivmod_rel_def by (simp add: smult_add_right)
  4.1019 +
  4.1020 +lemma div_smult_left: "(smult a x) div y = smult a (x div y)"
  4.1021 +  by (rule div_poly_eq, rule pdivmod_rel_smult_left, rule pdivmod_rel)
  4.1022 +
  4.1023 +lemma mod_smult_left: "(smult a x) mod y = smult a (x mod y)"
  4.1024 +  by (rule mod_poly_eq, rule pdivmod_rel_smult_left, rule pdivmod_rel)
  4.1025 +
  4.1026 +lemma pdivmod_rel_smult_right:
  4.1027 +  "\<lbrakk>a \<noteq> 0; pdivmod_rel x y q r\<rbrakk>
  4.1028 +    \<Longrightarrow> pdivmod_rel x (smult a y) (smult (inverse a) q) r"
  4.1029 +  unfolding pdivmod_rel_def by simp
  4.1030 +
  4.1031 +lemma div_smult_right:
  4.1032 +  "a \<noteq> 0 \<Longrightarrow> x div (smult a y) = smult (inverse a) (x div y)"
  4.1033 +  by (rule div_poly_eq, erule pdivmod_rel_smult_right, rule pdivmod_rel)
  4.1034 +
  4.1035 +lemma mod_smult_right: "a \<noteq> 0 \<Longrightarrow> x mod (smult a y) = x mod y"
  4.1036 +  by (rule mod_poly_eq, erule pdivmod_rel_smult_right, rule pdivmod_rel)
  4.1037 +
  4.1038 +lemma pdivmod_rel_mult:
  4.1039 +  "\<lbrakk>pdivmod_rel x y q r; pdivmod_rel q z q' r'\<rbrakk>
  4.1040 +    \<Longrightarrow> pdivmod_rel x (y * z) q' (y * r' + r)"
  4.1041 +apply (cases "z = 0", simp add: pdivmod_rel_def)
  4.1042 +apply (cases "y = 0", simp add: pdivmod_rel_by_0_iff pdivmod_rel_0_iff)
  4.1043 +apply (cases "r = 0")
  4.1044 +apply (cases "r' = 0")
  4.1045 +apply (simp add: pdivmod_rel_def)
  4.1046 +apply (simp add: pdivmod_rel_def ring_simps degree_mult_eq)
  4.1047 +apply (cases "r' = 0")
  4.1048 +apply (simp add: pdivmod_rel_def degree_mult_eq)
  4.1049 +apply (simp add: pdivmod_rel_def ring_simps)
  4.1050 +apply (simp add: degree_mult_eq degree_add_less)
  4.1051 +done
  4.1052 +
  4.1053 +lemma poly_div_mult_right:
  4.1054 +  fixes x y z :: "'a::field poly"
  4.1055 +  shows "x div (y * z) = (x div y) div z"
  4.1056 +  by (rule div_poly_eq, rule pdivmod_rel_mult, (rule pdivmod_rel)+)
  4.1057 +
  4.1058 +lemma poly_mod_mult_right:
  4.1059 +  fixes x y z :: "'a::field poly"
  4.1060 +  shows "x mod (y * z) = y * (x div y mod z) + x mod y"
  4.1061 +  by (rule mod_poly_eq, rule pdivmod_rel_mult, (rule pdivmod_rel)+)
  4.1062 +
  4.1063 +lemma mod_pCons:
  4.1064 +  fixes a and x
  4.1065 +  assumes y: "y \<noteq> 0"
  4.1066 +  defines b: "b \<equiv> coeff (pCons a (x mod y)) (degree y) / coeff y (degree y)"
  4.1067 +  shows "(pCons a x) mod y = (pCons a (x mod y) - smult b y)"
  4.1068 +unfolding b
  4.1069 +apply (rule mod_poly_eq)
  4.1070 +apply (rule pdivmod_rel_pCons [OF pdivmod_rel y refl])
  4.1071 +done
  4.1072 +
  4.1073 +
  4.1074 +subsection {* Evaluation of polynomials *}
  4.1075 +
  4.1076 +definition
  4.1077 +  poly :: "'a::comm_semiring_0 poly \<Rightarrow> 'a \<Rightarrow> 'a" where
  4.1078 +  "poly = poly_rec (\<lambda>x. 0) (\<lambda>a p f x. a + x * f x)"
  4.1079 +
  4.1080 +lemma poly_0 [simp]: "poly 0 x = 0"
  4.1081 +  unfolding poly_def by (simp add: poly_rec_0)
  4.1082 +
  4.1083 +lemma poly_pCons [simp]: "poly (pCons a p) x = a + x * poly p x"
  4.1084 +  unfolding poly_def by (simp add: poly_rec_pCons)
  4.1085 +
  4.1086 +lemma poly_1 [simp]: "poly 1 x = 1"
  4.1087 +  unfolding one_poly_def by simp
  4.1088 +
  4.1089 +lemma poly_monom:
  4.1090 +  fixes a x :: "'a::{comm_semiring_1,recpower}"
  4.1091 +  shows "poly (monom a n) x = a * x ^ n"
  4.1092 +  by (induct n, simp add: monom_0, simp add: monom_Suc power_Suc mult_ac)
  4.1093 +
  4.1094 +lemma poly_add [simp]: "poly (p + q) x = poly p x + poly q x"
  4.1095 +  apply (induct p arbitrary: q, simp)
  4.1096 +  apply (case_tac q, simp, simp add: algebra_simps)
  4.1097 +  done
  4.1098 +
  4.1099 +lemma poly_minus [simp]:
  4.1100 +  fixes x :: "'a::comm_ring"
  4.1101 +  shows "poly (- p) x = - poly p x"
  4.1102 +  by (induct p, simp_all)
  4.1103 +
  4.1104 +lemma poly_diff [simp]:
  4.1105 +  fixes x :: "'a::comm_ring"
  4.1106 +  shows "poly (p - q) x = poly p x - poly q x"
  4.1107 +  by (simp add: diff_minus)
  4.1108 +
  4.1109 +lemma poly_setsum: "poly (\<Sum>k\<in>A. p k) x = (\<Sum>k\<in>A. poly (p k) x)"
  4.1110 +  by (cases "finite A", induct set: finite, simp_all)
  4.1111 +
  4.1112 +lemma poly_smult [simp]: "poly (smult a p) x = a * poly p x"
  4.1113 +  by (induct p, simp, simp add: algebra_simps)
  4.1114 +
  4.1115 +lemma poly_mult [simp]: "poly (p * q) x = poly p x * poly q x"
  4.1116 +  by (induct p, simp_all, simp add: algebra_simps)
  4.1117 +
  4.1118 +lemma poly_power [simp]:
  4.1119 +  fixes p :: "'a::{comm_semiring_1,recpower} poly"
  4.1120 +  shows "poly (p ^ n) x = poly p x ^ n"
  4.1121 +  by (induct n, simp, simp add: power_Suc)
  4.1122 +
  4.1123 +
  4.1124 +subsection {* Synthetic division *}
  4.1125 +
  4.1126 +text {*
  4.1127 +  Synthetic division is simply division by the
  4.1128 +  linear polynomial @{term "x - c"}.
  4.1129 +*}
  4.1130 +
  4.1131 +definition
  4.1132 +  synthetic_divmod :: "'a::comm_semiring_0 poly \<Rightarrow> 'a \<Rightarrow> 'a poly \<times> 'a"
  4.1133 +where [code del]:
  4.1134 +  "synthetic_divmod p c =
  4.1135 +    poly_rec (0, 0) (\<lambda>a p (q, r). (pCons r q, a + c * r)) p"
  4.1136 +
  4.1137 +definition
  4.1138 +  synthetic_div :: "'a::comm_semiring_0 poly \<Rightarrow> 'a \<Rightarrow> 'a poly"
  4.1139 +where
  4.1140 +  "synthetic_div p c = fst (synthetic_divmod p c)"
  4.1141 +
  4.1142 +lemma synthetic_divmod_0 [simp]:
  4.1143 +  "synthetic_divmod 0 c = (0, 0)"
  4.1144 +  unfolding synthetic_divmod_def
  4.1145 +  by (simp add: poly_rec_0)
  4.1146 +
  4.1147 +lemma synthetic_divmod_pCons [simp]:
  4.1148 +  "synthetic_divmod (pCons a p) c =
  4.1149 +    (\<lambda>(q, r). (pCons r q, a + c * r)) (synthetic_divmod p c)"
  4.1150 +  unfolding synthetic_divmod_def
  4.1151 +  by (simp add: poly_rec_pCons)
  4.1152 +
  4.1153 +lemma snd_synthetic_divmod: "snd (synthetic_divmod p c) = poly p c"
  4.1154 +  by (induct p, simp, simp add: split_def)
  4.1155 +
  4.1156 +lemma synthetic_div_0 [simp]: "synthetic_div 0 c = 0"
  4.1157 +  unfolding synthetic_div_def by simp
  4.1158 +
  4.1159 +lemma synthetic_div_pCons [simp]:
  4.1160 +  "synthetic_div (pCons a p) c = pCons (poly p c) (synthetic_div p c)"
  4.1161 +  unfolding synthetic_div_def
  4.1162 +  by (simp add: split_def snd_synthetic_divmod)
  4.1163 +
  4.1164 +lemma synthetic_div_eq_0_iff:
  4.1165 +  "synthetic_div p c = 0 \<longleftrightarrow> degree p = 0"
  4.1166 +  by (induct p, simp, case_tac p, simp)
  4.1167 +
  4.1168 +lemma degree_synthetic_div:
  4.1169 +  "degree (synthetic_div p c) = degree p - 1"
  4.1170 +  by (induct p, simp, simp add: synthetic_div_eq_0_iff)
  4.1171 +
  4.1172 +lemma synthetic_div_correct:
  4.1173 +  "p + smult c (synthetic_div p c) = pCons (poly p c) (synthetic_div p c)"
  4.1174 +  by (induct p) simp_all
  4.1175 +
  4.1176 +lemma synthetic_div_unique_lemma: "smult c p = pCons a p \<Longrightarrow> p = 0"
  4.1177 +by (induct p arbitrary: a) simp_all
  4.1178 +
  4.1179 +lemma synthetic_div_unique:
  4.1180 +  "p + smult c q = pCons r q \<Longrightarrow> r = poly p c \<and> q = synthetic_div p c"
  4.1181 +apply (induct p arbitrary: q r)
  4.1182 +apply (simp, frule synthetic_div_unique_lemma, simp)
  4.1183 +apply (case_tac q, force)
  4.1184 +done
  4.1185 +
  4.1186 +lemma synthetic_div_correct':
  4.1187 +  fixes c :: "'a::comm_ring_1"
  4.1188 +  shows "[:-c, 1:] * synthetic_div p c + [:poly p c:] = p"
  4.1189 +  using synthetic_div_correct [of p c]
  4.1190 +  by (simp add: algebra_simps)
  4.1191 +
  4.1192 +lemma poly_eq_0_iff_dvd:
  4.1193 +  fixes c :: "'a::idom"
  4.1194 +  shows "poly p c = 0 \<longleftrightarrow> [:-c, 1:] dvd p"
  4.1195 +proof
  4.1196 +  assume "poly p c = 0"
  4.1197 +  with synthetic_div_correct' [of c p]
  4.1198 +  have "p = [:-c, 1:] * synthetic_div p c" by simp
  4.1199 +  then show "[:-c, 1:] dvd p" ..
  4.1200 +next
  4.1201 +  assume "[:-c, 1:] dvd p"
  4.1202 +  then obtain k where "p = [:-c, 1:] * k" by (rule dvdE)
  4.1203 +  then show "poly p c = 0" by simp
  4.1204 +qed
  4.1205 +
  4.1206 +lemma dvd_iff_poly_eq_0:
  4.1207 +  fixes c :: "'a::idom"
  4.1208 +  shows "[:c, 1:] dvd p \<longleftrightarrow> poly p (-c) = 0"
  4.1209 +  by (simp add: poly_eq_0_iff_dvd)
  4.1210 +
  4.1211 +lemma poly_roots_finite:
  4.1212 +  fixes p :: "'a::idom poly"
  4.1213 +  shows "p \<noteq> 0 \<Longrightarrow> finite {x. poly p x = 0}"
  4.1214 +proof (induct n \<equiv> "degree p" arbitrary: p)
  4.1215 +  case (0 p)
  4.1216 +  then obtain a where "a \<noteq> 0" and "p = [:a:]"
  4.1217 +    by (cases p, simp split: if_splits)
  4.1218 +  then show "finite {x. poly p x = 0}" by simp
  4.1219 +next
  4.1220 +  case (Suc n p)
  4.1221 +  show "finite {x. poly p x = 0}"
  4.1222 +  proof (cases "\<exists>x. poly p x = 0")
  4.1223 +    case False
  4.1224 +    then show "finite {x. poly p x = 0}" by simp
  4.1225 +  next
  4.1226 +    case True
  4.1227 +    then obtain a where "poly p a = 0" ..
  4.1228 +    then have "[:-a, 1:] dvd p" by (simp only: poly_eq_0_iff_dvd)
  4.1229 +    then obtain k where k: "p = [:-a, 1:] * k" ..
  4.1230 +    with `p \<noteq> 0` have "k \<noteq> 0" by auto
  4.1231 +    with k have "degree p = Suc (degree k)"
  4.1232 +      by (simp add: degree_mult_eq del: mult_pCons_left)
  4.1233 +    with `Suc n = degree p` have "n = degree k" by simp
  4.1234 +    with `k \<noteq> 0` have "finite {x. poly k x = 0}" by (rule Suc.hyps)
  4.1235 +    then have "finite (insert a {x. poly k x = 0})" by simp
  4.1236 +    then show "finite {x. poly p x = 0}"
  4.1237 +      by (simp add: k uminus_add_conv_diff Collect_disj_eq
  4.1238 +               del: mult_pCons_left)
  4.1239 +  qed
  4.1240 +qed
  4.1241 +
  4.1242 +lemma poly_zero:
  4.1243 +  fixes p :: "'a::{idom,ring_char_0} poly"
  4.1244 +  shows "poly p = poly 0 \<longleftrightarrow> p = 0"
  4.1245 +apply (cases "p = 0", simp_all)
  4.1246 +apply (drule poly_roots_finite)
  4.1247 +apply (auto simp add: infinite_UNIV_char_0)
  4.1248 +done
  4.1249 +
  4.1250 +lemma poly_eq_iff:
  4.1251 +  fixes p q :: "'a::{idom,ring_char_0} poly"
  4.1252 +  shows "poly p = poly q \<longleftrightarrow> p = q"
  4.1253 +  using poly_zero [of "p - q"]
  4.1254 +  by (simp add: expand_fun_eq)
  4.1255 +
  4.1256 +
  4.1257 +subsection {* Composition of polynomials *}
  4.1258 +
  4.1259 +definition
  4.1260 +  pcompose :: "'a::comm_semiring_0 poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
  4.1261 +where
  4.1262 +  "pcompose p q = poly_rec 0 (\<lambda>a _ c. [:a:] + q * c) p"
  4.1263 +
  4.1264 +lemma pcompose_0 [simp]: "pcompose 0 q = 0"
  4.1265 +  unfolding pcompose_def by (simp add: poly_rec_0)
  4.1266 +
  4.1267 +lemma pcompose_pCons:
  4.1268 +  "pcompose (pCons a p) q = [:a:] + q * pcompose p q"
  4.1269 +  unfolding pcompose_def by (simp add: poly_rec_pCons)
  4.1270 +
  4.1271 +lemma poly_pcompose: "poly (pcompose p q) x = poly p (poly q x)"
  4.1272 +  by (induct p) (simp_all add: pcompose_pCons)
  4.1273 +
  4.1274 +lemma degree_pcompose_le:
  4.1275 +  "degree (pcompose p q) \<le> degree p * degree q"
  4.1276 +apply (induct p, simp)
  4.1277 +apply (simp add: pcompose_pCons, clarify)
  4.1278 +apply (rule degree_add_le, simp)
  4.1279 +apply (rule order_trans [OF degree_mult_le], simp)
  4.1280 +done
  4.1281 +
  4.1282 +
  4.1283 +subsection {* Order of polynomial roots *}
  4.1284 +
  4.1285 +definition
  4.1286 +  order :: "'a::idom \<Rightarrow> 'a poly \<Rightarrow> nat"
  4.1287 +where
  4.1288 +  [code del]:
  4.1289 +  "order a p = (LEAST n. \<not> [:-a, 1:] ^ Suc n dvd p)"
  4.1290 +
  4.1291 +lemma coeff_linear_power:
  4.1292 +  fixes a :: "'a::comm_semiring_1"
  4.1293 +  shows "coeff ([:a, 1:] ^ n) n = 1"
  4.1294 +apply (induct n, simp_all)
  4.1295 +apply (subst coeff_eq_0)
  4.1296 +apply (auto intro: le_less_trans degree_power_le)
  4.1297 +done
  4.1298 +
  4.1299 +lemma degree_linear_power:
  4.1300 +  fixes a :: "'a::comm_semiring_1"
  4.1301 +  shows "degree ([:a, 1:] ^ n) = n"
  4.1302 +apply (rule order_antisym)
  4.1303 +apply (rule ord_le_eq_trans [OF degree_power_le], simp)
  4.1304 +apply (rule le_degree, simp add: coeff_linear_power)
  4.1305 +done
  4.1306 +
  4.1307 +lemma order_1: "[:-a, 1:] ^ order a p dvd p"
  4.1308 +apply (cases "p = 0", simp)
  4.1309 +apply (cases "order a p", simp)
  4.1310 +apply (subgoal_tac "nat < (LEAST n. \<not> [:-a, 1:] ^ Suc n dvd p)")
  4.1311 +apply (drule not_less_Least, simp)
  4.1312 +apply (fold order_def, simp)
  4.1313 +done
  4.1314 +
  4.1315 +lemma order_2: "p \<noteq> 0 \<Longrightarrow> \<not> [:-a, 1:] ^ Suc (order a p) dvd p"
  4.1316 +unfolding order_def
  4.1317 +apply (rule LeastI_ex)
  4.1318 +apply (rule_tac x="degree p" in exI)
  4.1319 +apply (rule notI)
  4.1320 +apply (drule (1) dvd_imp_degree_le)
  4.1321 +apply (simp only: degree_linear_power)
  4.1322 +done
  4.1323 +
  4.1324 +lemma order:
  4.1325 +  "p \<noteq> 0 \<Longrightarrow> [:-a, 1:] ^ order a p dvd p \<and> \<not> [:-a, 1:] ^ Suc (order a p) dvd p"
  4.1326 +by (rule conjI [OF order_1 order_2])
  4.1327 +
  4.1328 +lemma order_degree:
  4.1329 +  assumes p: "p \<noteq> 0"
  4.1330 +  shows "order a p \<le> degree p"
  4.1331 +proof -
  4.1332 +  have "order a p = degree ([:-a, 1:] ^ order a p)"
  4.1333 +    by (simp only: degree_linear_power)
  4.1334 +  also have "\<dots> \<le> degree p"
  4.1335 +    using order_1 p by (rule dvd_imp_degree_le)
  4.1336 +  finally show ?thesis .
  4.1337 +qed
  4.1338 +
  4.1339 +lemma order_root: "poly p a = 0 \<longleftrightarrow> p = 0 \<or> order a p \<noteq> 0"
  4.1340 +apply (cases "p = 0", simp_all)
  4.1341 +apply (rule iffI)
  4.1342 +apply (rule ccontr, simp)
  4.1343 +apply (frule order_2 [where a=a], simp)
  4.1344 +apply (simp add: poly_eq_0_iff_dvd)
  4.1345 +apply (simp add: poly_eq_0_iff_dvd)
  4.1346 +apply (simp only: order_def)
  4.1347 +apply (drule not_less_Least, simp)
  4.1348 +done
  4.1349 +
  4.1350 +
  4.1351 +subsection {* Configuration of the code generator *}
  4.1352 +
  4.1353 +code_datatype "0::'a::zero poly" pCons
  4.1354 +
  4.1355 +declare pCons_0_0 [code post]
  4.1356 +
  4.1357 +instantiation poly :: ("{zero,eq}") eq
  4.1358 +begin
  4.1359 +
  4.1360 +definition [code del]:
  4.1361 +  "eq_class.eq (p::'a poly) q \<longleftrightarrow> p = q"
  4.1362 +
  4.1363 +instance
  4.1364 +  by default (rule eq_poly_def)
  4.1365 +
  4.1366 +end
  4.1367 +
  4.1368 +lemma eq_poly_code [code]:
  4.1369 +  "eq_class.eq (0::_ poly) (0::_ poly) \<longleftrightarrow> True"
  4.1370 +  "eq_class.eq (0::_ poly) (pCons b q) \<longleftrightarrow> eq_class.eq 0 b \<and> eq_class.eq 0 q"
  4.1371 +  "eq_class.eq (pCons a p) (0::_ poly) \<longleftrightarrow> eq_class.eq a 0 \<and> eq_class.eq p 0"
  4.1372 +  "eq_class.eq (pCons a p) (pCons b q) \<longleftrightarrow> eq_class.eq a b \<and> eq_class.eq p q"
  4.1373 +unfolding eq by simp_all
  4.1374 +
  4.1375 +lemmas coeff_code [code] =
  4.1376 +  coeff_0 coeff_pCons_0 coeff_pCons_Suc
  4.1377 +
  4.1378 +lemmas degree_code [code] =
  4.1379 +  degree_0 degree_pCons_eq_if
  4.1380 +
  4.1381 +lemmas monom_poly_code [code] =
  4.1382 +  monom_0 monom_Suc
  4.1383 +
  4.1384 +lemma add_poly_code [code]:
  4.1385 +  "0 + q = (q :: _ poly)"
  4.1386 +  "p + 0 = (p :: _ poly)"
  4.1387 +  "pCons a p + pCons b q = pCons (a + b) (p + q)"
  4.1388 +by simp_all
  4.1389 +
  4.1390 +lemma minus_poly_code [code]:
  4.1391 +  "- 0 = (0 :: _ poly)"
  4.1392 +  "- pCons a p = pCons (- a) (- p)"
  4.1393 +by simp_all
  4.1394 +
  4.1395 +lemma diff_poly_code [code]:
  4.1396 +  "0 - q = (- q :: _ poly)"
  4.1397 +  "p - 0 = (p :: _ poly)"
  4.1398 +  "pCons a p - pCons b q = pCons (a - b) (p - q)"
  4.1399 +by simp_all
  4.1400 +
  4.1401 +lemmas smult_poly_code [code] =
  4.1402 +  smult_0_right smult_pCons
  4.1403 +
  4.1404 +lemma mult_poly_code [code]:
  4.1405 +  "0 * q = (0 :: _ poly)"
  4.1406 +  "pCons a p * q = smult a q + pCons 0 (p * q)"
  4.1407 +by simp_all
  4.1408 +
  4.1409 +lemmas poly_code [code] =
  4.1410 +  poly_0 poly_pCons
  4.1411 +
  4.1412 +lemmas synthetic_divmod_code [code] =
  4.1413 +  synthetic_divmod_0 synthetic_divmod_pCons
  4.1414 +
  4.1415 +text {* code generator setup for div and mod *}
  4.1416 +
  4.1417 +definition
  4.1418 +  pdivmod :: "'a::field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<times> 'a poly"
  4.1419 +where
  4.1420 +  [code del]: "pdivmod x y = (x div y, x mod y)"
  4.1421 +
  4.1422 +lemma div_poly_code [code]: "x div y = fst (pdivmod x y)"
  4.1423 +  unfolding pdivmod_def by simp
  4.1424 +
  4.1425 +lemma mod_poly_code [code]: "x mod y = snd (pdivmod x y)"
  4.1426 +  unfolding pdivmod_def by simp
  4.1427 +
  4.1428 +lemma pdivmod_0 [code]: "pdivmod 0 y = (0, 0)"
  4.1429 +  unfolding pdivmod_def by simp
  4.1430 +
  4.1431 +lemma pdivmod_pCons [code]:
  4.1432 +  "pdivmod (pCons a x) y =
  4.1433 +    (if y = 0 then (0, pCons a x) else
  4.1434 +      (let (q, r) = pdivmod x y;
  4.1435 +           b = coeff (pCons a r) (degree y) / coeff y (degree y)
  4.1436 +        in (pCons b q, pCons a r - smult b y)))"
  4.1437 +apply (simp add: pdivmod_def Let_def, safe)
  4.1438 +apply (rule div_poly_eq)
  4.1439 +apply (erule pdivmod_rel_pCons [OF pdivmod_rel _ refl])
  4.1440 +apply (rule mod_poly_eq)
  4.1441 +apply (erule pdivmod_rel_pCons [OF pdivmod_rel _ refl])
  4.1442 +done
  4.1443 +
  4.1444 +end
     5.1 --- a/src/HOL/Polynomial.thy	Wed Feb 18 19:51:39 2009 -0800
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,1441 +0,0 @@
     5.4 -(*  Title:      HOL/Polynomial.thy
     5.5 -    Author:     Brian Huffman
     5.6 -                Based on an earlier development by Clemens Ballarin
     5.7 -*)
     5.8 -
     5.9 -header {* Univariate Polynomials *}
    5.10 -
    5.11 -theory Polynomial
    5.12 -imports Plain SetInterval Main
    5.13 -begin
    5.14 -
    5.15 -subsection {* Definition of type @{text poly} *}
    5.16 -
    5.17 -typedef (Poly) 'a poly = "{f::nat \<Rightarrow> 'a::zero. \<exists>n. \<forall>i>n. f i = 0}"
    5.18 -  morphisms coeff Abs_poly
    5.19 -  by auto
    5.20 -
    5.21 -lemma expand_poly_eq: "p = q \<longleftrightarrow> (\<forall>n. coeff p n = coeff q n)"
    5.22 -by (simp add: coeff_inject [symmetric] expand_fun_eq)
    5.23 -
    5.24 -lemma poly_ext: "(\<And>n. coeff p n = coeff q n) \<Longrightarrow> p = q"
    5.25 -by (simp add: expand_poly_eq)
    5.26 -
    5.27 -
    5.28 -subsection {* Degree of a polynomial *}
    5.29 -
    5.30 -definition
    5.31 -  degree :: "'a::zero poly \<Rightarrow> nat" where
    5.32 -  "degree p = (LEAST n. \<forall>i>n. coeff p i = 0)"
    5.33 -
    5.34 -lemma coeff_eq_0: "degree p < n \<Longrightarrow> coeff p n = 0"
    5.35 -proof -
    5.36 -  have "coeff p \<in> Poly"
    5.37 -    by (rule coeff)
    5.38 -  hence "\<exists>n. \<forall>i>n. coeff p i = 0"
    5.39 -    unfolding Poly_def by simp
    5.40 -  hence "\<forall>i>degree p. coeff p i = 0"
    5.41 -    unfolding degree_def by (rule LeastI_ex)
    5.42 -  moreover assume "degree p < n"
    5.43 -  ultimately show ?thesis by simp
    5.44 -qed
    5.45 -
    5.46 -lemma le_degree: "coeff p n \<noteq> 0 \<Longrightarrow> n \<le> degree p"
    5.47 -  by (erule contrapos_np, rule coeff_eq_0, simp)
    5.48 -
    5.49 -lemma degree_le: "\<forall>i>n. coeff p i = 0 \<Longrightarrow> degree p \<le> n"
    5.50 -  unfolding degree_def by (erule Least_le)
    5.51 -
    5.52 -lemma less_degree_imp: "n < degree p \<Longrightarrow> \<exists>i>n. coeff p i \<noteq> 0"
    5.53 -  unfolding degree_def by (drule not_less_Least, simp)
    5.54 -
    5.55 -
    5.56 -subsection {* The zero polynomial *}
    5.57 -
    5.58 -instantiation poly :: (zero) zero
    5.59 -begin
    5.60 -
    5.61 -definition
    5.62 -  zero_poly_def: "0 = Abs_poly (\<lambda>n. 0)"
    5.63 -
    5.64 -instance ..
    5.65 -end
    5.66 -
    5.67 -lemma coeff_0 [simp]: "coeff 0 n = 0"
    5.68 -  unfolding zero_poly_def
    5.69 -  by (simp add: Abs_poly_inverse Poly_def)
    5.70 -
    5.71 -lemma degree_0 [simp]: "degree 0 = 0"
    5.72 -  by (rule order_antisym [OF degree_le le0]) simp
    5.73 -
    5.74 -lemma leading_coeff_neq_0:
    5.75 -  assumes "p \<noteq> 0" shows "coeff p (degree p) \<noteq> 0"
    5.76 -proof (cases "degree p")
    5.77 -  case 0
    5.78 -  from `p \<noteq> 0` have "\<exists>n. coeff p n \<noteq> 0"
    5.79 -    by (simp add: expand_poly_eq)
    5.80 -  then obtain n where "coeff p n \<noteq> 0" ..
    5.81 -  hence "n \<le> degree p" by (rule le_degree)
    5.82 -  with `coeff p n \<noteq> 0` and `degree p = 0`
    5.83 -  show "coeff p (degree p) \<noteq> 0" by simp
    5.84 -next
    5.85 -  case (Suc n)
    5.86 -  from `degree p = Suc n` have "n < degree p" by simp
    5.87 -  hence "\<exists>i>n. coeff p i \<noteq> 0" by (rule less_degree_imp)
    5.88 -  then obtain i where "n < i" and "coeff p i \<noteq> 0" by fast
    5.89 -  from `degree p = Suc n` and `n < i` have "degree p \<le> i" by simp
    5.90 -  also from `coeff p i \<noteq> 0` have "i \<le> degree p" by (rule le_degree)
    5.91 -  finally have "degree p = i" .
    5.92 -  with `coeff p i \<noteq> 0` show "coeff p (degree p) \<noteq> 0" by simp
    5.93 -qed
    5.94 -
    5.95 -lemma leading_coeff_0_iff [simp]: "coeff p (degree p) = 0 \<longleftrightarrow> p = 0"
    5.96 -  by (cases "p = 0", simp, simp add: leading_coeff_neq_0)
    5.97 -
    5.98 -
    5.99 -subsection {* List-style constructor for polynomials *}
   5.100 -
   5.101 -definition
   5.102 -  pCons :: "'a::zero \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
   5.103 -where
   5.104 -  [code del]: "pCons a p = Abs_poly (nat_case a (coeff p))"
   5.105 -
   5.106 -syntax
   5.107 -  "_poly" :: "args \<Rightarrow> 'a poly"  ("[:(_):]")
   5.108 -
   5.109 -translations
   5.110 -  "[:x, xs:]" == "CONST pCons x [:xs:]"
   5.111 -  "[:x:]" == "CONST pCons x 0"
   5.112 -
   5.113 -lemma Poly_nat_case: "f \<in> Poly \<Longrightarrow> nat_case a f \<in> Poly"
   5.114 -  unfolding Poly_def by (auto split: nat.split)
   5.115 -
   5.116 -lemma coeff_pCons:
   5.117 -  "coeff (pCons a p) = nat_case a (coeff p)"
   5.118 -  unfolding pCons_def
   5.119 -  by (simp add: Abs_poly_inverse Poly_nat_case coeff)
   5.120 -
   5.121 -lemma coeff_pCons_0 [simp]: "coeff (pCons a p) 0 = a"
   5.122 -  by (simp add: coeff_pCons)
   5.123 -
   5.124 -lemma coeff_pCons_Suc [simp]: "coeff (pCons a p) (Suc n) = coeff p n"
   5.125 -  by (simp add: coeff_pCons)
   5.126 -
   5.127 -lemma degree_pCons_le: "degree (pCons a p) \<le> Suc (degree p)"
   5.128 -by (rule degree_le, simp add: coeff_eq_0 coeff_pCons split: nat.split)
   5.129 -
   5.130 -lemma degree_pCons_eq:
   5.131 -  "p \<noteq> 0 \<Longrightarrow> degree (pCons a p) = Suc (degree p)"
   5.132 -apply (rule order_antisym [OF degree_pCons_le])
   5.133 -apply (rule le_degree, simp)
   5.134 -done
   5.135 -
   5.136 -lemma degree_pCons_0: "degree (pCons a 0) = 0"
   5.137 -apply (rule order_antisym [OF _ le0])
   5.138 -apply (rule degree_le, simp add: coeff_pCons split: nat.split)
   5.139 -done
   5.140 -
   5.141 -lemma degree_pCons_eq_if [simp]:
   5.142 -  "degree (pCons a p) = (if p = 0 then 0 else Suc (degree p))"
   5.143 -apply (cases "p = 0", simp_all)
   5.144 -apply (rule order_antisym [OF _ le0])
   5.145 -apply (rule degree_le, simp add: coeff_pCons split: nat.split)
   5.146 -apply (rule order_antisym [OF degree_pCons_le])
   5.147 -apply (rule le_degree, simp)
   5.148 -done
   5.149 -
   5.150 -lemma pCons_0_0 [simp]: "pCons 0 0 = 0"
   5.151 -by (rule poly_ext, simp add: coeff_pCons split: nat.split)
   5.152 -
   5.153 -lemma pCons_eq_iff [simp]:
   5.154 -  "pCons a p = pCons b q \<longleftrightarrow> a = b \<and> p = q"
   5.155 -proof (safe)
   5.156 -  assume "pCons a p = pCons b q"
   5.157 -  then have "coeff (pCons a p) 0 = coeff (pCons b q) 0" by simp
   5.158 -  then show "a = b" by simp
   5.159 -next
   5.160 -  assume "pCons a p = pCons b q"
   5.161 -  then have "\<forall>n. coeff (pCons a p) (Suc n) =
   5.162 -                 coeff (pCons b q) (Suc n)" by simp
   5.163 -  then show "p = q" by (simp add: expand_poly_eq)
   5.164 -qed
   5.165 -
   5.166 -lemma pCons_eq_0_iff [simp]: "pCons a p = 0 \<longleftrightarrow> a = 0 \<and> p = 0"
   5.167 -  using pCons_eq_iff [of a p 0 0] by simp
   5.168 -
   5.169 -lemma Poly_Suc: "f \<in> Poly \<Longrightarrow> (\<lambda>n. f (Suc n)) \<in> Poly"
   5.170 -  unfolding Poly_def
   5.171 -  by (clarify, rule_tac x=n in exI, simp)
   5.172 -
   5.173 -lemma pCons_cases [cases type: poly]:
   5.174 -  obtains (pCons) a q where "p = pCons a q"
   5.175 -proof
   5.176 -  show "p = pCons (coeff p 0) (Abs_poly (\<lambda>n. coeff p (Suc n)))"
   5.177 -    by (rule poly_ext)
   5.178 -       (simp add: Abs_poly_inverse Poly_Suc coeff coeff_pCons
   5.179 -             split: nat.split)
   5.180 -qed
   5.181 -
   5.182 -lemma pCons_induct [case_names 0 pCons, induct type: poly]:
   5.183 -  assumes zero: "P 0"
   5.184 -  assumes pCons: "\<And>a p. P p \<Longrightarrow> P (pCons a p)"
   5.185 -  shows "P p"
   5.186 -proof (induct p rule: measure_induct_rule [where f=degree])
   5.187 -  case (less p)
   5.188 -  obtain a q where "p = pCons a q" by (rule pCons_cases)
   5.189 -  have "P q"
   5.190 -  proof (cases "q = 0")
   5.191 -    case True
   5.192 -    then show "P q" by (simp add: zero)
   5.193 -  next
   5.194 -    case False
   5.195 -    then have "degree (pCons a q) = Suc (degree q)"
   5.196 -      by (rule degree_pCons_eq)
   5.197 -    then have "degree q < degree p"
   5.198 -      using `p = pCons a q` by simp
   5.199 -    then show "P q"
   5.200 -      by (rule less.hyps)
   5.201 -  qed
   5.202 -  then have "P (pCons a q)"
   5.203 -    by (rule pCons)
   5.204 -  then show ?case
   5.205 -    using `p = pCons a q` by simp
   5.206 -qed
   5.207 -
   5.208 -
   5.209 -subsection {* Recursion combinator for polynomials *}
   5.210 -
   5.211 -function
   5.212 -  poly_rec :: "'b \<Rightarrow> ('a::zero \<Rightarrow> 'a poly \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a poly \<Rightarrow> 'b"
   5.213 -where
   5.214 -  poly_rec_pCons_eq_if [simp del, code del]:
   5.215 -    "poly_rec z f (pCons a p) = f a p (if p = 0 then z else poly_rec z f p)"
   5.216 -by (case_tac x, rename_tac q, case_tac q, auto)
   5.217 -
   5.218 -termination poly_rec
   5.219 -by (relation "measure (degree \<circ> snd \<circ> snd)", simp)
   5.220 -   (simp add: degree_pCons_eq)
   5.221 -
   5.222 -lemma poly_rec_0:
   5.223 -  "f 0 0 z = z \<Longrightarrow> poly_rec z f 0 = z"
   5.224 -  using poly_rec_pCons_eq_if [of z f 0 0] by simp
   5.225 -
   5.226 -lemma poly_rec_pCons:
   5.227 -  "f 0 0 z = z \<Longrightarrow> poly_rec z f (pCons a p) = f a p (poly_rec z f p)"
   5.228 -  by (simp add: poly_rec_pCons_eq_if poly_rec_0)
   5.229 -
   5.230 -
   5.231 -subsection {* Monomials *}
   5.232 -
   5.233 -definition
   5.234 -  monom :: "'a \<Rightarrow> nat \<Rightarrow> 'a::zero poly" where
   5.235 -  "monom a m = Abs_poly (\<lambda>n. if m = n then a else 0)"
   5.236 -
   5.237 -lemma coeff_monom [simp]: "coeff (monom a m) n = (if m=n then a else 0)"
   5.238 -  unfolding monom_def
   5.239 -  by (subst Abs_poly_inverse, auto simp add: Poly_def)
   5.240 -
   5.241 -lemma monom_0: "monom a 0 = pCons a 0"
   5.242 -  by (rule poly_ext, simp add: coeff_pCons split: nat.split)
   5.243 -
   5.244 -lemma monom_Suc: "monom a (Suc n) = pCons 0 (monom a n)"
   5.245 -  by (rule poly_ext, simp add: coeff_pCons split: nat.split)
   5.246 -
   5.247 -lemma monom_eq_0 [simp]: "monom 0 n = 0"
   5.248 -  by (rule poly_ext) simp
   5.249 -
   5.250 -lemma monom_eq_0_iff [simp]: "monom a n = 0 \<longleftrightarrow> a = 0"
   5.251 -  by (simp add: expand_poly_eq)
   5.252 -
   5.253 -lemma monom_eq_iff [simp]: "monom a n = monom b n \<longleftrightarrow> a = b"
   5.254 -  by (simp add: expand_poly_eq)
   5.255 -
   5.256 -lemma degree_monom_le: "degree (monom a n) \<le> n"
   5.257 -  by (rule degree_le, simp)
   5.258 -
   5.259 -lemma degree_monom_eq: "a \<noteq> 0 \<Longrightarrow> degree (monom a n) = n"
   5.260 -  apply (rule order_antisym [OF degree_monom_le])
   5.261 -  apply (rule le_degree, simp)
   5.262 -  done
   5.263 -
   5.264 -
   5.265 -subsection {* Addition and subtraction *}
   5.266 -
   5.267 -instantiation poly :: (comm_monoid_add) comm_monoid_add
   5.268 -begin
   5.269 -
   5.270 -definition
   5.271 -  plus_poly_def [code del]:
   5.272 -    "p + q = Abs_poly (\<lambda>n. coeff p n + coeff q n)"
   5.273 -
   5.274 -lemma Poly_add:
   5.275 -  fixes f g :: "nat \<Rightarrow> 'a"
   5.276 -  shows "\<lbrakk>f \<in> Poly; g \<in> Poly\<rbrakk> \<Longrightarrow> (\<lambda>n. f n + g n) \<in> Poly"
   5.277 -  unfolding Poly_def
   5.278 -  apply (clarify, rename_tac m n)
   5.279 -  apply (rule_tac x="max m n" in exI, simp)
   5.280 -  done
   5.281 -
   5.282 -lemma coeff_add [simp]:
   5.283 -  "coeff (p + q) n = coeff p n + coeff q n"
   5.284 -  unfolding plus_poly_def
   5.285 -  by (simp add: Abs_poly_inverse coeff Poly_add)
   5.286 -
   5.287 -instance proof
   5.288 -  fix p q r :: "'a poly"
   5.289 -  show "(p + q) + r = p + (q + r)"
   5.290 -    by (simp add: expand_poly_eq add_assoc)
   5.291 -  show "p + q = q + p"
   5.292 -    by (simp add: expand_poly_eq add_commute)
   5.293 -  show "0 + p = p"
   5.294 -    by (simp add: expand_poly_eq)
   5.295 -qed
   5.296 -
   5.297 -end
   5.298 -
   5.299 -instance poly :: (cancel_comm_monoid_add) cancel_comm_monoid_add
   5.300 -proof
   5.301 -  fix p q r :: "'a poly"
   5.302 -  assume "p + q = p + r" thus "q = r"
   5.303 -    by (simp add: expand_poly_eq)
   5.304 -qed
   5.305 -
   5.306 -instantiation poly :: (ab_group_add) ab_group_add
   5.307 -begin
   5.308 -
   5.309 -definition
   5.310 -  uminus_poly_def [code del]:
   5.311 -    "- p = Abs_poly (\<lambda>n. - coeff p n)"
   5.312 -
   5.313 -definition
   5.314 -  minus_poly_def [code del]:
   5.315 -    "p - q = Abs_poly (\<lambda>n. coeff p n - coeff q n)"
   5.316 -
   5.317 -lemma Poly_minus:
   5.318 -  fixes f :: "nat \<Rightarrow> 'a"
   5.319 -  shows "f \<in> Poly \<Longrightarrow> (\<lambda>n. - f n) \<in> Poly"
   5.320 -  unfolding Poly_def by simp
   5.321 -
   5.322 -lemma Poly_diff:
   5.323 -  fixes f g :: "nat \<Rightarrow> 'a"
   5.324 -  shows "\<lbrakk>f \<in> Poly; g \<in> Poly\<rbrakk> \<Longrightarrow> (\<lambda>n. f n - g n) \<in> Poly"
   5.325 -  unfolding diff_minus by (simp add: Poly_add Poly_minus)
   5.326 -
   5.327 -lemma coeff_minus [simp]: "coeff (- p) n = - coeff p n"
   5.328 -  unfolding uminus_poly_def
   5.329 -  by (simp add: Abs_poly_inverse coeff Poly_minus)
   5.330 -
   5.331 -lemma coeff_diff [simp]:
   5.332 -  "coeff (p - q) n = coeff p n - coeff q n"
   5.333 -  unfolding minus_poly_def
   5.334 -  by (simp add: Abs_poly_inverse coeff Poly_diff)
   5.335 -
   5.336 -instance proof
   5.337 -  fix p q :: "'a poly"
   5.338 -  show "- p + p = 0"
   5.339 -    by (simp add: expand_poly_eq)
   5.340 -  show "p - q = p + - q"
   5.341 -    by (simp add: expand_poly_eq diff_minus)
   5.342 -qed
   5.343 -
   5.344 -end
   5.345 -
   5.346 -lemma add_pCons [simp]:
   5.347 -  "pCons a p + pCons b q = pCons (a + b) (p + q)"
   5.348 -  by (rule poly_ext, simp add: coeff_pCons split: nat.split)
   5.349 -
   5.350 -lemma minus_pCons [simp]:
   5.351 -  "- pCons a p = pCons (- a) (- p)"
   5.352 -  by (rule poly_ext, simp add: coeff_pCons split: nat.split)
   5.353 -
   5.354 -lemma diff_pCons [simp]:
   5.355 -  "pCons a p - pCons b q = pCons (a - b) (p - q)"
   5.356 -  by (rule poly_ext, simp add: coeff_pCons split: nat.split)
   5.357 -
   5.358 -lemma degree_add_le_max: "degree (p + q) \<le> max (degree p) (degree q)"
   5.359 -  by (rule degree_le, auto simp add: coeff_eq_0)
   5.360 -
   5.361 -lemma degree_add_le:
   5.362 -  "\<lbrakk>degree p \<le> n; degree q \<le> n\<rbrakk> \<Longrightarrow> degree (p + q) \<le> n"
   5.363 -  by (auto intro: order_trans degree_add_le_max)
   5.364 -
   5.365 -lemma degree_add_less:
   5.366 -  "\<lbrakk>degree p < n; degree q < n\<rbrakk> \<Longrightarrow> degree (p + q) < n"
   5.367 -  by (auto intro: le_less_trans degree_add_le_max)
   5.368 -
   5.369 -lemma degree_add_eq_right:
   5.370 -  "degree p < degree q \<Longrightarrow> degree (p + q) = degree q"
   5.371 -  apply (cases "q = 0", simp)
   5.372 -  apply (rule order_antisym)
   5.373 -  apply (simp add: degree_add_le)
   5.374 -  apply (rule le_degree)
   5.375 -  apply (simp add: coeff_eq_0)
   5.376 -  done
   5.377 -
   5.378 -lemma degree_add_eq_left:
   5.379 -  "degree q < degree p \<Longrightarrow> degree (p + q) = degree p"
   5.380 -  using degree_add_eq_right [of q p]
   5.381 -  by (simp add: add_commute)
   5.382 -
   5.383 -lemma degree_minus [simp]: "degree (- p) = degree p"
   5.384 -  unfolding degree_def by simp
   5.385 -
   5.386 -lemma degree_diff_le_max: "degree (p - q) \<le> max (degree p) (degree q)"
   5.387 -  using degree_add_le [where p=p and q="-q"]
   5.388 -  by (simp add: diff_minus)
   5.389 -
   5.390 -lemma degree_diff_le:
   5.391 -  "\<lbrakk>degree p \<le> n; degree q \<le> n\<rbrakk> \<Longrightarrow> degree (p - q) \<le> n"
   5.392 -  by (simp add: diff_minus degree_add_le)
   5.393 -
   5.394 -lemma degree_diff_less:
   5.395 -  "\<lbrakk>degree p < n; degree q < n\<rbrakk> \<Longrightarrow> degree (p - q) < n"
   5.396 -  by (simp add: diff_minus degree_add_less)
   5.397 -
   5.398 -lemma add_monom: "monom a n + monom b n = monom (a + b) n"
   5.399 -  by (rule poly_ext) simp
   5.400 -
   5.401 -lemma diff_monom: "monom a n - monom b n = monom (a - b) n"
   5.402 -  by (rule poly_ext) simp
   5.403 -
   5.404 -lemma minus_monom: "- monom a n = monom (-a) n"
   5.405 -  by (rule poly_ext) simp
   5.406 -
   5.407 -lemma coeff_setsum: "coeff (\<Sum>x\<in>A. p x) i = (\<Sum>x\<in>A. coeff (p x) i)"
   5.408 -  by (cases "finite A", induct set: finite, simp_all)
   5.409 -
   5.410 -lemma monom_setsum: "monom (\<Sum>x\<in>A. a x) n = (\<Sum>x\<in>A. monom (a x) n)"
   5.411 -  by (rule poly_ext) (simp add: coeff_setsum)
   5.412 -
   5.413 -
   5.414 -subsection {* Multiplication by a constant *}
   5.415 -
   5.416 -definition
   5.417 -  smult :: "'a::comm_semiring_0 \<Rightarrow> 'a poly \<Rightarrow> 'a poly" where
   5.418 -  "smult a p = Abs_poly (\<lambda>n. a * coeff p n)"
   5.419 -
   5.420 -lemma Poly_smult:
   5.421 -  fixes f :: "nat \<Rightarrow> 'a::comm_semiring_0"
   5.422 -  shows "f \<in> Poly \<Longrightarrow> (\<lambda>n. a * f n) \<in> Poly"
   5.423 -  unfolding Poly_def
   5.424 -  by (clarify, rule_tac x=n in exI, simp)
   5.425 -
   5.426 -lemma coeff_smult [simp]: "coeff (smult a p) n = a * coeff p n"
   5.427 -  unfolding smult_def
   5.428 -  by (simp add: Abs_poly_inverse Poly_smult coeff)
   5.429 -
   5.430 -lemma degree_smult_le: "degree (smult a p) \<le> degree p"
   5.431 -  by (rule degree_le, simp add: coeff_eq_0)
   5.432 -
   5.433 -lemma smult_smult [simp]: "smult a (smult b p) = smult (a * b) p"
   5.434 -  by (rule poly_ext, simp add: mult_assoc)
   5.435 -
   5.436 -lemma smult_0_right [simp]: "smult a 0 = 0"
   5.437 -  by (rule poly_ext, simp)
   5.438 -
   5.439 -lemma smult_0_left [simp]: "smult 0 p = 0"
   5.440 -  by (rule poly_ext, simp)
   5.441 -
   5.442 -lemma smult_1_left [simp]: "smult (1::'a::comm_semiring_1) p = p"
   5.443 -  by (rule poly_ext, simp)
   5.444 -
   5.445 -lemma smult_add_right:
   5.446 -  "smult a (p + q) = smult a p + smult a q"
   5.447 -  by (rule poly_ext, simp add: algebra_simps)
   5.448 -
   5.449 -lemma smult_add_left:
   5.450 -  "smult (a + b) p = smult a p + smult b p"
   5.451 -  by (rule poly_ext, simp add: algebra_simps)
   5.452 -
   5.453 -lemma smult_minus_right [simp]:
   5.454 -  "smult (a::'a::comm_ring) (- p) = - smult a p"
   5.455 -  by (rule poly_ext, simp)
   5.456 -
   5.457 -lemma smult_minus_left [simp]:
   5.458 -  "smult (- a::'a::comm_ring) p = - smult a p"
   5.459 -  by (rule poly_ext, simp)
   5.460 -
   5.461 -lemma smult_diff_right:
   5.462 -  "smult (a::'a::comm_ring) (p - q) = smult a p - smult a q"
   5.463 -  by (rule poly_ext, simp add: algebra_simps)
   5.464 -
   5.465 -lemma smult_diff_left:
   5.466 -  "smult (a - b::'a::comm_ring) p = smult a p - smult b p"
   5.467 -  by (rule poly_ext, simp add: algebra_simps)
   5.468 -
   5.469 -lemmas smult_distribs =
   5.470 -  smult_add_left smult_add_right
   5.471 -  smult_diff_left smult_diff_right
   5.472 -
   5.473 -lemma smult_pCons [simp]:
   5.474 -  "smult a (pCons b p) = pCons (a * b) (smult a p)"
   5.475 -  by (rule poly_ext, simp add: coeff_pCons split: nat.split)
   5.476 -
   5.477 -lemma smult_monom: "smult a (monom b n) = monom (a * b) n"
   5.478 -  by (induct n, simp add: monom_0, simp add: monom_Suc)
   5.479 -
   5.480 -lemma degree_smult_eq [simp]:
   5.481 -  fixes a :: "'a::idom"
   5.482 -  shows "degree (smult a p) = (if a = 0 then 0 else degree p)"
   5.483 -  by (cases "a = 0", simp, simp add: degree_def)
   5.484 -
   5.485 -lemma smult_eq_0_iff [simp]:
   5.486 -  fixes a :: "'a::idom"
   5.487 -  shows "smult a p = 0 \<longleftrightarrow> a = 0 \<or> p = 0"
   5.488 -  by (simp add: expand_poly_eq)
   5.489 -
   5.490 -
   5.491 -subsection {* Multiplication of polynomials *}
   5.492 -
   5.493 -text {* TODO: move to SetInterval.thy *}
   5.494 -lemma setsum_atMost_Suc_shift:
   5.495 -  fixes f :: "nat \<Rightarrow> 'a::comm_monoid_add"
   5.496 -  shows "(\<Sum>i\<le>Suc n. f i) = f 0 + (\<Sum>i\<le>n. f (Suc i))"
   5.497 -proof (induct n)
   5.498 -  case 0 show ?case by simp
   5.499 -next
   5.500 -  case (Suc n) note IH = this
   5.501 -  have "(\<Sum>i\<le>Suc (Suc n). f i) = (\<Sum>i\<le>Suc n. f i) + f (Suc (Suc n))"
   5.502 -    by (rule setsum_atMost_Suc)
   5.503 -  also have "(\<Sum>i\<le>Suc n. f i) = f 0 + (\<Sum>i\<le>n. f (Suc i))"
   5.504 -    by (rule IH)
   5.505 -  also have "f 0 + (\<Sum>i\<le>n. f (Suc i)) + f (Suc (Suc n)) =
   5.506 -             f 0 + ((\<Sum>i\<le>n. f (Suc i)) + f (Suc (Suc n)))"
   5.507 -    by (rule add_assoc)
   5.508 -  also have "(\<Sum>i\<le>n. f (Suc i)) + f (Suc (Suc n)) = (\<Sum>i\<le>Suc n. f (Suc i))"
   5.509 -    by (rule setsum_atMost_Suc [symmetric])
   5.510 -  finally show ?case .
   5.511 -qed
   5.512 -
   5.513 -instantiation poly :: (comm_semiring_0) comm_semiring_0
   5.514 -begin
   5.515 -
   5.516 -definition
   5.517 -  times_poly_def [code del]:
   5.518 -    "p * q = poly_rec 0 (\<lambda>a p pq. smult a q + pCons 0 pq) p"
   5.519 -
   5.520 -lemma mult_poly_0_left: "(0::'a poly) * q = 0"
   5.521 -  unfolding times_poly_def by (simp add: poly_rec_0)
   5.522 -
   5.523 -lemma mult_pCons_left [simp]:
   5.524 -  "pCons a p * q = smult a q + pCons 0 (p * q)"
   5.525 -  unfolding times_poly_def by (simp add: poly_rec_pCons)
   5.526 -
   5.527 -lemma mult_poly_0_right: "p * (0::'a poly) = 0"
   5.528 -  by (induct p, simp add: mult_poly_0_left, simp)
   5.529 -
   5.530 -lemma mult_pCons_right [simp]:
   5.531 -  "p * pCons a q = smult a p + pCons 0 (p * q)"
   5.532 -  by (induct p, simp add: mult_poly_0_left, simp add: algebra_simps)
   5.533 -
   5.534 -lemmas mult_poly_0 = mult_poly_0_left mult_poly_0_right
   5.535 -
   5.536 -lemma mult_smult_left [simp]: "smult a p * q = smult a (p * q)"
   5.537 -  by (induct p, simp add: mult_poly_0, simp add: smult_add_right)
   5.538 -
   5.539 -lemma mult_smult_right [simp]: "p * smult a q = smult a (p * q)"
   5.540 -  by (induct q, simp add: mult_poly_0, simp add: smult_add_right)
   5.541 -
   5.542 -lemma mult_poly_add_left:
   5.543 -  fixes p q r :: "'a poly"
   5.544 -  shows "(p + q) * r = p * r + q * r"
   5.545 -  by (induct r, simp add: mult_poly_0,
   5.546 -                simp add: smult_distribs algebra_simps)
   5.547 -
   5.548 -instance proof
   5.549 -  fix p q r :: "'a poly"
   5.550 -  show 0: "0 * p = 0"
   5.551 -    by (rule mult_poly_0_left)
   5.552 -  show "p * 0 = 0"
   5.553 -    by (rule mult_poly_0_right)
   5.554 -  show "(p + q) * r = p * r + q * r"
   5.555 -    by (rule mult_poly_add_left)
   5.556 -  show "(p * q) * r = p * (q * r)"
   5.557 -    by (induct p, simp add: mult_poly_0, simp add: mult_poly_add_left)
   5.558 -  show "p * q = q * p"
   5.559 -    by (induct p, simp add: mult_poly_0, simp)
   5.560 -qed
   5.561 -
   5.562 -end
   5.563 -
   5.564 -instance poly :: (comm_semiring_0_cancel) comm_semiring_0_cancel ..
   5.565 -
   5.566 -lemma coeff_mult:
   5.567 -  "coeff (p * q) n = (\<Sum>i\<le>n. coeff p i * coeff q (n-i))"
   5.568 -proof (induct p arbitrary: n)
   5.569 -  case 0 show ?case by simp
   5.570 -next
   5.571 -  case (pCons a p n) thus ?case
   5.572 -    by (cases n, simp, simp add: setsum_atMost_Suc_shift
   5.573 -                            del: setsum_atMost_Suc)
   5.574 -qed
   5.575 -
   5.576 -lemma degree_mult_le: "degree (p * q) \<le> degree p + degree q"
   5.577 -apply (rule degree_le)
   5.578 -apply (induct p)
   5.579 -apply simp
   5.580 -apply (simp add: coeff_eq_0 coeff_pCons split: nat.split)
   5.581 -done
   5.582 -
   5.583 -lemma mult_monom: "monom a m * monom b n = monom (a * b) (m + n)"
   5.584 -  by (induct m, simp add: monom_0 smult_monom, simp add: monom_Suc)
   5.585 -
   5.586 -
   5.587 -subsection {* The unit polynomial and exponentiation *}
   5.588 -
   5.589 -instantiation poly :: (comm_semiring_1) comm_semiring_1
   5.590 -begin
   5.591 -
   5.592 -definition
   5.593 -  one_poly_def:
   5.594 -    "1 = pCons 1 0"
   5.595 -
   5.596 -instance proof
   5.597 -  fix p :: "'a poly" show "1 * p = p"
   5.598 -    unfolding one_poly_def
   5.599 -    by simp
   5.600 -next
   5.601 -  show "0 \<noteq> (1::'a poly)"
   5.602 -    unfolding one_poly_def by simp
   5.603 -qed
   5.604 -
   5.605 -end
   5.606 -
   5.607 -instance poly :: (comm_semiring_1_cancel) comm_semiring_1_cancel ..
   5.608 -
   5.609 -lemma coeff_1 [simp]: "coeff 1 n = (if n = 0 then 1 else 0)"
   5.610 -  unfolding one_poly_def
   5.611 -  by (simp add: coeff_pCons split: nat.split)
   5.612 -
   5.613 -lemma degree_1 [simp]: "degree 1 = 0"
   5.614 -  unfolding one_poly_def
   5.615 -  by (rule degree_pCons_0)
   5.616 -
   5.617 -text {* Lemmas about divisibility *}
   5.618 -
   5.619 -lemma dvd_smult: "p dvd q \<Longrightarrow> p dvd smult a q"
   5.620 -proof -
   5.621 -  assume "p dvd q"
   5.622 -  then obtain k where "q = p * k" ..
   5.623 -  then have "smult a q = p * smult a k" by simp
   5.624 -  then show "p dvd smult a q" ..
   5.625 -qed
   5.626 -
   5.627 -lemma dvd_smult_cancel:
   5.628 -  fixes a :: "'a::field"
   5.629 -  shows "p dvd smult a q \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> p dvd q"
   5.630 -  by (drule dvd_smult [where a="inverse a"]) simp
   5.631 -
   5.632 -lemma dvd_smult_iff:
   5.633 -  fixes a :: "'a::field"
   5.634 -  shows "a \<noteq> 0 \<Longrightarrow> p dvd smult a q \<longleftrightarrow> p dvd q"
   5.635 -  by (safe elim!: dvd_smult dvd_smult_cancel)
   5.636 -
   5.637 -instantiation poly :: (comm_semiring_1) recpower
   5.638 -begin
   5.639 -
   5.640 -primrec power_poly where
   5.641 -  power_poly_0: "(p::'a poly) ^ 0 = 1"
   5.642 -| power_poly_Suc: "(p::'a poly) ^ (Suc n) = p * p ^ n"
   5.643 -
   5.644 -instance
   5.645 -  by default simp_all
   5.646 -
   5.647 -end
   5.648 -
   5.649 -lemma degree_power_le: "degree (p ^ n) \<le> degree p * n"
   5.650 -by (induct n, simp, auto intro: order_trans degree_mult_le)
   5.651 -
   5.652 -instance poly :: (comm_ring) comm_ring ..
   5.653 -
   5.654 -instance poly :: (comm_ring_1) comm_ring_1 ..
   5.655 -
   5.656 -instantiation poly :: (comm_ring_1) number_ring
   5.657 -begin
   5.658 -
   5.659 -definition
   5.660 -  "number_of k = (of_int k :: 'a poly)"
   5.661 -
   5.662 -instance
   5.663 -  by default (rule number_of_poly_def)
   5.664 -
   5.665 -end
   5.666 -
   5.667 -
   5.668 -subsection {* Polynomials form an integral domain *}
   5.669 -
   5.670 -lemma coeff_mult_degree_sum:
   5.671 -  "coeff (p * q) (degree p + degree q) =
   5.672 -   coeff p (degree p) * coeff q (degree q)"
   5.673 -  by (induct p, simp, simp add: coeff_eq_0)
   5.674 -
   5.675 -instance poly :: (idom) idom
   5.676 -proof
   5.677 -  fix p q :: "'a poly"
   5.678 -  assume "p \<noteq> 0" and "q \<noteq> 0"
   5.679 -  have "coeff (p * q) (degree p + degree q) =
   5.680 -        coeff p (degree p) * coeff q (degree q)"
   5.681 -    by (rule coeff_mult_degree_sum)
   5.682 -  also have "coeff p (degree p) * coeff q (degree q) \<noteq> 0"
   5.683 -    using `p \<noteq> 0` and `q \<noteq> 0` by simp
   5.684 -  finally have "\<exists>n. coeff (p * q) n \<noteq> 0" ..
   5.685 -  thus "p * q \<noteq> 0" by (simp add: expand_poly_eq)
   5.686 -qed
   5.687 -
   5.688 -lemma degree_mult_eq:
   5.689 -  fixes p q :: "'a::idom poly"
   5.690 -  shows "\<lbrakk>p \<noteq> 0; q \<noteq> 0\<rbrakk> \<Longrightarrow> degree (p * q) = degree p + degree q"
   5.691 -apply (rule order_antisym [OF degree_mult_le le_degree])
   5.692 -apply (simp add: coeff_mult_degree_sum)
   5.693 -done
   5.694 -
   5.695 -lemma dvd_imp_degree_le:
   5.696 -  fixes p q :: "'a::idom poly"
   5.697 -  shows "\<lbrakk>p dvd q; q \<noteq> 0\<rbrakk> \<Longrightarrow> degree p \<le> degree q"
   5.698 -  by (erule dvdE, simp add: degree_mult_eq)
   5.699 -
   5.700 -
   5.701 -subsection {* Polynomials form an ordered integral domain *}
   5.702 -
   5.703 -definition
   5.704 -  pos_poly :: "'a::ordered_idom poly \<Rightarrow> bool"
   5.705 -where
   5.706 -  "pos_poly p \<longleftrightarrow> 0 < coeff p (degree p)"
   5.707 -
   5.708 -lemma pos_poly_pCons:
   5.709 -  "pos_poly (pCons a p) \<longleftrightarrow> pos_poly p \<or> (p = 0 \<and> 0 < a)"
   5.710 -  unfolding pos_poly_def by simp
   5.711 -
   5.712 -lemma not_pos_poly_0 [simp]: "\<not> pos_poly 0"
   5.713 -  unfolding pos_poly_def by simp
   5.714 -
   5.715 -lemma pos_poly_add: "\<lbrakk>pos_poly p; pos_poly q\<rbrakk> \<Longrightarrow> pos_poly (p + q)"
   5.716 -  apply (induct p arbitrary: q, simp)
   5.717 -  apply (case_tac q, force simp add: pos_poly_pCons add_pos_pos)
   5.718 -  done
   5.719 -
   5.720 -lemma pos_poly_mult: "\<lbrakk>pos_poly p; pos_poly q\<rbrakk> \<Longrightarrow> pos_poly (p * q)"
   5.721 -  unfolding pos_poly_def
   5.722 -  apply (subgoal_tac "p \<noteq> 0 \<and> q \<noteq> 0")
   5.723 -  apply (simp add: degree_mult_eq coeff_mult_degree_sum mult_pos_pos)
   5.724 -  apply auto
   5.725 -  done
   5.726 -
   5.727 -lemma pos_poly_total: "p = 0 \<or> pos_poly p \<or> pos_poly (- p)"
   5.728 -by (induct p) (auto simp add: pos_poly_pCons)
   5.729 -
   5.730 -instantiation poly :: (ordered_idom) ordered_idom
   5.731 -begin
   5.732 -
   5.733 -definition
   5.734 -  [code del]:
   5.735 -    "x < y \<longleftrightarrow> pos_poly (y - x)"
   5.736 -
   5.737 -definition
   5.738 -  [code del]:
   5.739 -    "x \<le> y \<longleftrightarrow> x = y \<or> pos_poly (y - x)"
   5.740 -
   5.741 -definition
   5.742 -  [code del]:
   5.743 -    "abs (x::'a poly) = (if x < 0 then - x else x)"
   5.744 -
   5.745 -definition
   5.746 -  [code del]:
   5.747 -    "sgn (x::'a poly) = (if x = 0 then 0 else if 0 < x then 1 else - 1)"
   5.748 -
   5.749 -instance proof
   5.750 -  fix x y :: "'a poly"
   5.751 -  show "x < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x"
   5.752 -    unfolding less_eq_poly_def less_poly_def
   5.753 -    apply safe
   5.754 -    apply simp
   5.755 -    apply (drule (1) pos_poly_add)
   5.756 -    apply simp
   5.757 -    done
   5.758 -next
   5.759 -  fix x :: "'a poly" show "x \<le> x"
   5.760 -    unfolding less_eq_poly_def by simp
   5.761 -next
   5.762 -  fix x y z :: "'a poly"
   5.763 -  assume "x \<le> y" and "y \<le> z" thus "x \<le> z"
   5.764 -    unfolding less_eq_poly_def
   5.765 -    apply safe
   5.766 -    apply (drule (1) pos_poly_add)
   5.767 -    apply (simp add: algebra_simps)
   5.768 -    done
   5.769 -next
   5.770 -  fix x y :: "'a poly"
   5.771 -  assume "x \<le> y" and "y \<le> x" thus "x = y"
   5.772 -    unfolding less_eq_poly_def
   5.773 -    apply safe
   5.774 -    apply (drule (1) pos_poly_add)
   5.775 -    apply simp
   5.776 -    done
   5.777 -next
   5.778 -  fix x y z :: "'a poly"
   5.779 -  assume "x \<le> y" thus "z + x \<le> z + y"
   5.780 -    unfolding less_eq_poly_def
   5.781 -    apply safe
   5.782 -    apply (simp add: algebra_simps)
   5.783 -    done
   5.784 -next
   5.785 -  fix x y :: "'a poly"
   5.786 -  show "x \<le> y \<or> y \<le> x"
   5.787 -    unfolding less_eq_poly_def
   5.788 -    using pos_poly_total [of "x - y"]
   5.789 -    by auto
   5.790 -next
   5.791 -  fix x y z :: "'a poly"
   5.792 -  assume "x < y" and "0 < z"
   5.793 -  thus "z * x < z * y"
   5.794 -    unfolding less_poly_def
   5.795 -    by (simp add: right_diff_distrib [symmetric] pos_poly_mult)
   5.796 -next
   5.797 -  fix x :: "'a poly"
   5.798 -  show "\<bar>x\<bar> = (if x < 0 then - x else x)"
   5.799 -    by (rule abs_poly_def)
   5.800 -next
   5.801 -  fix x :: "'a poly"
   5.802 -  show "sgn x = (if x = 0 then 0 else if 0 < x then 1 else - 1)"
   5.803 -    by (rule sgn_poly_def)
   5.804 -qed
   5.805 -
   5.806 -end
   5.807 -
   5.808 -text {* TODO: Simplification rules for comparisons *}
   5.809 -
   5.810 -
   5.811 -subsection {* Long division of polynomials *}
   5.812 -
   5.813 -definition
   5.814 -  pdivmod_rel :: "'a::field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<Rightarrow> bool"
   5.815 -where
   5.816 -  [code del]:
   5.817 -  "pdivmod_rel x y q r \<longleftrightarrow>
   5.818 -    x = q * y + r \<and> (if y = 0 then q = 0 else r = 0 \<or> degree r < degree y)"
   5.819 -
   5.820 -lemma pdivmod_rel_0:
   5.821 -  "pdivmod_rel 0 y 0 0"
   5.822 -  unfolding pdivmod_rel_def by simp
   5.823 -
   5.824 -lemma pdivmod_rel_by_0:
   5.825 -  "pdivmod_rel x 0 0 x"
   5.826 -  unfolding pdivmod_rel_def by simp
   5.827 -
   5.828 -lemma eq_zero_or_degree_less:
   5.829 -  assumes "degree p \<le> n" and "coeff p n = 0"
   5.830 -  shows "p = 0 \<or> degree p < n"
   5.831 -proof (cases n)
   5.832 -  case 0
   5.833 -  with `degree p \<le> n` and `coeff p n = 0`
   5.834 -  have "coeff p (degree p) = 0" by simp
   5.835 -  then have "p = 0" by simp
   5.836 -  then show ?thesis ..
   5.837 -next
   5.838 -  case (Suc m)
   5.839 -  have "\<forall>i>n. coeff p i = 0"
   5.840 -    using `degree p \<le> n` by (simp add: coeff_eq_0)
   5.841 -  then have "\<forall>i\<ge>n. coeff p i = 0"
   5.842 -    using `coeff p n = 0` by (simp add: le_less)
   5.843 -  then have "\<forall>i>m. coeff p i = 0"
   5.844 -    using `n = Suc m` by (simp add: less_eq_Suc_le)
   5.845 -  then have "degree p \<le> m"
   5.846 -    by (rule degree_le)
   5.847 -  then have "degree p < n"
   5.848 -    using `n = Suc m` by (simp add: less_Suc_eq_le)
   5.849 -  then show ?thesis ..
   5.850 -qed
   5.851 -
   5.852 -lemma pdivmod_rel_pCons:
   5.853 -  assumes rel: "pdivmod_rel x y q r"
   5.854 -  assumes y: "y \<noteq> 0"
   5.855 -  assumes b: "b = coeff (pCons a r) (degree y) / coeff y (degree y)"
   5.856 -  shows "pdivmod_rel (pCons a x) y (pCons b q) (pCons a r - smult b y)"
   5.857 -    (is "pdivmod_rel ?x y ?q ?r")
   5.858 -proof -
   5.859 -  have x: "x = q * y + r" and r: "r = 0 \<or> degree r < degree y"
   5.860 -    using assms unfolding pdivmod_rel_def by simp_all
   5.861 -
   5.862 -  have 1: "?x = ?q * y + ?r"
   5.863 -    using b x by simp
   5.864 -
   5.865 -  have 2: "?r = 0 \<or> degree ?r < degree y"
   5.866 -  proof (rule eq_zero_or_degree_less)
   5.867 -    show "degree ?r \<le> degree y"
   5.868 -    proof (rule degree_diff_le)
   5.869 -      show "degree (pCons a r) \<le> degree y"
   5.870 -        using r by auto
   5.871 -      show "degree (smult b y) \<le> degree y"
   5.872 -        by (rule degree_smult_le)
   5.873 -    qed
   5.874 -  next
   5.875 -    show "coeff ?r (degree y) = 0"
   5.876 -      using `y \<noteq> 0` unfolding b by simp
   5.877 -  qed
   5.878 -
   5.879 -  from 1 2 show ?thesis
   5.880 -    unfolding pdivmod_rel_def
   5.881 -    using `y \<noteq> 0` by simp
   5.882 -qed
   5.883 -
   5.884 -lemma pdivmod_rel_exists: "\<exists>q r. pdivmod_rel x y q r"
   5.885 -apply (cases "y = 0")
   5.886 -apply (fast intro!: pdivmod_rel_by_0)
   5.887 -apply (induct x)
   5.888 -apply (fast intro!: pdivmod_rel_0)
   5.889 -apply (fast intro!: pdivmod_rel_pCons)
   5.890 -done
   5.891 -
   5.892 -lemma pdivmod_rel_unique:
   5.893 -  assumes 1: "pdivmod_rel x y q1 r1"
   5.894 -  assumes 2: "pdivmod_rel x y q2 r2"
   5.895 -  shows "q1 = q2 \<and> r1 = r2"
   5.896 -proof (cases "y = 0")
   5.897 -  assume "y = 0" with assms show ?thesis
   5.898 -    by (simp add: pdivmod_rel_def)
   5.899 -next
   5.900 -  assume [simp]: "y \<noteq> 0"
   5.901 -  from 1 have q1: "x = q1 * y + r1" and r1: "r1 = 0 \<or> degree r1 < degree y"
   5.902 -    unfolding pdivmod_rel_def by simp_all
   5.903 -  from 2 have q2: "x = q2 * y + r2" and r2: "r2 = 0 \<or> degree r2 < degree y"
   5.904 -    unfolding pdivmod_rel_def by simp_all
   5.905 -  from q1 q2 have q3: "(q1 - q2) * y = r2 - r1"
   5.906 -    by (simp add: algebra_simps)
   5.907 -  from r1 r2 have r3: "(r2 - r1) = 0 \<or> degree (r2 - r1) < degree y"
   5.908 -    by (auto intro: degree_diff_less)
   5.909 -
   5.910 -  show "q1 = q2 \<and> r1 = r2"
   5.911 -  proof (rule ccontr)
   5.912 -    assume "\<not> (q1 = q2 \<and> r1 = r2)"
   5.913 -    with q3 have "q1 \<noteq> q2" and "r1 \<noteq> r2" by auto
   5.914 -    with r3 have "degree (r2 - r1) < degree y" by simp
   5.915 -    also have "degree y \<le> degree (q1 - q2) + degree y" by simp
   5.916 -    also have "\<dots> = degree ((q1 - q2) * y)"
   5.917 -      using `q1 \<noteq> q2` by (simp add: degree_mult_eq)
   5.918 -    also have "\<dots> = degree (r2 - r1)"
   5.919 -      using q3 by simp
   5.920 -    finally have "degree (r2 - r1) < degree (r2 - r1)" .
   5.921 -    then show "False" by simp
   5.922 -  qed
   5.923 -qed
   5.924 -
   5.925 -lemma pdivmod_rel_0_iff: "pdivmod_rel 0 y q r \<longleftrightarrow> q = 0 \<and> r = 0"
   5.926 -by (auto dest: pdivmod_rel_unique intro: pdivmod_rel_0)
   5.927 -
   5.928 -lemma pdivmod_rel_by_0_iff: "pdivmod_rel x 0 q r \<longleftrightarrow> q = 0 \<and> r = x"
   5.929 -by (auto dest: pdivmod_rel_unique intro: pdivmod_rel_by_0)
   5.930 -
   5.931 -lemmas pdivmod_rel_unique_div =
   5.932 -  pdivmod_rel_unique [THEN conjunct1, standard]
   5.933 -
   5.934 -lemmas pdivmod_rel_unique_mod =
   5.935 -  pdivmod_rel_unique [THEN conjunct2, standard]
   5.936 -
   5.937 -instantiation poly :: (field) ring_div
   5.938 -begin
   5.939 -
   5.940 -definition div_poly where
   5.941 -  [code del]: "x div y = (THE q. \<exists>r. pdivmod_rel x y q r)"
   5.942 -
   5.943 -definition mod_poly where
   5.944 -  [code del]: "x mod y = (THE r. \<exists>q. pdivmod_rel x y q r)"
   5.945 -
   5.946 -lemma div_poly_eq:
   5.947 -  "pdivmod_rel x y q r \<Longrightarrow> x div y = q"
   5.948 -unfolding div_poly_def
   5.949 -by (fast elim: pdivmod_rel_unique_div)
   5.950 -
   5.951 -lemma mod_poly_eq:
   5.952 -  "pdivmod_rel x y q r \<Longrightarrow> x mod y = r"
   5.953 -unfolding mod_poly_def
   5.954 -by (fast elim: pdivmod_rel_unique_mod)
   5.955 -
   5.956 -lemma pdivmod_rel:
   5.957 -  "pdivmod_rel x y (x div y) (x mod y)"
   5.958 -proof -
   5.959 -  from pdivmod_rel_exists
   5.960 -    obtain q r where "pdivmod_rel x y q r" by fast
   5.961 -  thus ?thesis
   5.962 -    by (simp add: div_poly_eq mod_poly_eq)
   5.963 -qed
   5.964 -
   5.965 -instance proof
   5.966 -  fix x y :: "'a poly"
   5.967 -  show "x div y * y + x mod y = x"
   5.968 -    using pdivmod_rel [of x y]
   5.969 -    by (simp add: pdivmod_rel_def)
   5.970 -next
   5.971 -  fix x :: "'a poly"
   5.972 -  have "pdivmod_rel x 0 0 x"
   5.973 -    by (rule pdivmod_rel_by_0)
   5.974 -  thus "x div 0 = 0"
   5.975 -    by (rule div_poly_eq)
   5.976 -next
   5.977 -  fix y :: "'a poly"
   5.978 -  have "pdivmod_rel 0 y 0 0"
   5.979 -    by (rule pdivmod_rel_0)
   5.980 -  thus "0 div y = 0"
   5.981 -    by (rule div_poly_eq)
   5.982 -next
   5.983 -  fix x y z :: "'a poly"
   5.984 -  assume "y \<noteq> 0"
   5.985 -  hence "pdivmod_rel (x + z * y) y (z + x div y) (x mod y)"
   5.986 -    using pdivmod_rel [of x y]
   5.987 -    by (simp add: pdivmod_rel_def left_distrib)
   5.988 -  thus "(x + z * y) div y = z + x div y"
   5.989 -    by (rule div_poly_eq)
   5.990 -qed
   5.991 -
   5.992 -end
   5.993 -
   5.994 -lemma degree_mod_less:
   5.995 -  "y \<noteq> 0 \<Longrightarrow> x mod y = 0 \<or> degree (x mod y) < degree y"
   5.996 -  using pdivmod_rel [of x y]
   5.997 -  unfolding pdivmod_rel_def by simp
   5.998 -
   5.999 -lemma div_poly_less: "degree x < degree y \<Longrightarrow> x div y = 0"
  5.1000 -proof -
  5.1001 -  assume "degree x < degree y"
  5.1002 -  hence "pdivmod_rel x y 0 x"
  5.1003 -    by (simp add: pdivmod_rel_def)
  5.1004 -  thus "x div y = 0" by (rule div_poly_eq)
  5.1005 -qed
  5.1006 -
  5.1007 -lemma mod_poly_less: "degree x < degree y \<Longrightarrow> x mod y = x"
  5.1008 -proof -
  5.1009 -  assume "degree x < degree y"
  5.1010 -  hence "pdivmod_rel x y 0 x"
  5.1011 -    by (simp add: pdivmod_rel_def)
  5.1012 -  thus "x mod y = x" by (rule mod_poly_eq)
  5.1013 -qed
  5.1014 -
  5.1015 -lemma pdivmod_rel_smult_left:
  5.1016 -  "pdivmod_rel x y q r
  5.1017 -    \<Longrightarrow> pdivmod_rel (smult a x) y (smult a q) (smult a r)"
  5.1018 -  unfolding pdivmod_rel_def by (simp add: smult_add_right)
  5.1019 -
  5.1020 -lemma div_smult_left: "(smult a x) div y = smult a (x div y)"
  5.1021 -  by (rule div_poly_eq, rule pdivmod_rel_smult_left, rule pdivmod_rel)
  5.1022 -
  5.1023 -lemma mod_smult_left: "(smult a x) mod y = smult a (x mod y)"
  5.1024 -  by (rule mod_poly_eq, rule pdivmod_rel_smult_left, rule pdivmod_rel)
  5.1025 -
  5.1026 -lemma pdivmod_rel_smult_right:
  5.1027 -  "\<lbrakk>a \<noteq> 0; pdivmod_rel x y q r\<rbrakk>
  5.1028 -    \<Longrightarrow> pdivmod_rel x (smult a y) (smult (inverse a) q) r"
  5.1029 -  unfolding pdivmod_rel_def by simp
  5.1030 -
  5.1031 -lemma div_smult_right:
  5.1032 -  "a \<noteq> 0 \<Longrightarrow> x div (smult a y) = smult (inverse a) (x div y)"
  5.1033 -  by (rule div_poly_eq, erule pdivmod_rel_smult_right, rule pdivmod_rel)
  5.1034 -
  5.1035 -lemma mod_smult_right: "a \<noteq> 0 \<Longrightarrow> x mod (smult a y) = x mod y"
  5.1036 -  by (rule mod_poly_eq, erule pdivmod_rel_smult_right, rule pdivmod_rel)
  5.1037 -
  5.1038 -lemma pdivmod_rel_mult:
  5.1039 -  "\<lbrakk>pdivmod_rel x y q r; pdivmod_rel q z q' r'\<rbrakk>
  5.1040 -    \<Longrightarrow> pdivmod_rel x (y * z) q' (y * r' + r)"
  5.1041 -apply (cases "z = 0", simp add: pdivmod_rel_def)
  5.1042 -apply (cases "y = 0", simp add: pdivmod_rel_by_0_iff pdivmod_rel_0_iff)
  5.1043 -apply (cases "r = 0")
  5.1044 -apply (cases "r' = 0")
  5.1045 -apply (simp add: pdivmod_rel_def)
  5.1046 -apply (simp add: pdivmod_rel_def ring_simps degree_mult_eq)
  5.1047 -apply (cases "r' = 0")
  5.1048 -apply (simp add: pdivmod_rel_def degree_mult_eq)
  5.1049 -apply (simp add: pdivmod_rel_def ring_simps)
  5.1050 -apply (simp add: degree_mult_eq degree_add_less)
  5.1051 -done
  5.1052 -
  5.1053 -lemma poly_div_mult_right:
  5.1054 -  fixes x y z :: "'a::field poly"
  5.1055 -  shows "x div (y * z) = (x div y) div z"
  5.1056 -  by (rule div_poly_eq, rule pdivmod_rel_mult, (rule pdivmod_rel)+)
  5.1057 -
  5.1058 -lemma poly_mod_mult_right:
  5.1059 -  fixes x y z :: "'a::field poly"
  5.1060 -  shows "x mod (y * z) = y * (x div y mod z) + x mod y"
  5.1061 -  by (rule mod_poly_eq, rule pdivmod_rel_mult, (rule pdivmod_rel)+)
  5.1062 -
  5.1063 -lemma mod_pCons:
  5.1064 -  fixes a and x
  5.1065 -  assumes y: "y \<noteq> 0"
  5.1066 -  defines b: "b \<equiv> coeff (pCons a (x mod y)) (degree y) / coeff y (degree y)"
  5.1067 -  shows "(pCons a x) mod y = (pCons a (x mod y) - smult b y)"
  5.1068 -unfolding b
  5.1069 -apply (rule mod_poly_eq)
  5.1070 -apply (rule pdivmod_rel_pCons [OF pdivmod_rel y refl])
  5.1071 -done
  5.1072 -
  5.1073 -
  5.1074 -subsection {* Evaluation of polynomials *}
  5.1075 -
  5.1076 -definition
  5.1077 -  poly :: "'a::comm_semiring_0 poly \<Rightarrow> 'a \<Rightarrow> 'a" where
  5.1078 -  "poly = poly_rec (\<lambda>x. 0) (\<lambda>a p f x. a + x * f x)"
  5.1079 -
  5.1080 -lemma poly_0 [simp]: "poly 0 x = 0"
  5.1081 -  unfolding poly_def by (simp add: poly_rec_0)
  5.1082 -
  5.1083 -lemma poly_pCons [simp]: "poly (pCons a p) x = a + x * poly p x"
  5.1084 -  unfolding poly_def by (simp add: poly_rec_pCons)
  5.1085 -
  5.1086 -lemma poly_1 [simp]: "poly 1 x = 1"
  5.1087 -  unfolding one_poly_def by simp
  5.1088 -
  5.1089 -lemma poly_monom:
  5.1090 -  fixes a x :: "'a::{comm_semiring_1,recpower}"
  5.1091 -  shows "poly (monom a n) x = a * x ^ n"
  5.1092 -  by (induct n, simp add: monom_0, simp add: monom_Suc power_Suc mult_ac)
  5.1093 -
  5.1094 -lemma poly_add [simp]: "poly (p + q) x = poly p x + poly q x"
  5.1095 -  apply (induct p arbitrary: q, simp)
  5.1096 -  apply (case_tac q, simp, simp add: algebra_simps)
  5.1097 -  done
  5.1098 -
  5.1099 -lemma poly_minus [simp]:
  5.1100 -  fixes x :: "'a::comm_ring"
  5.1101 -  shows "poly (- p) x = - poly p x"
  5.1102 -  by (induct p, simp_all)
  5.1103 -
  5.1104 -lemma poly_diff [simp]:
  5.1105 -  fixes x :: "'a::comm_ring"
  5.1106 -  shows "poly (p - q) x = poly p x - poly q x"
  5.1107 -  by (simp add: diff_minus)
  5.1108 -
  5.1109 -lemma poly_setsum: "poly (\<Sum>k\<in>A. p k) x = (\<Sum>k\<in>A. poly (p k) x)"
  5.1110 -  by (cases "finite A", induct set: finite, simp_all)
  5.1111 -
  5.1112 -lemma poly_smult [simp]: "poly (smult a p) x = a * poly p x"
  5.1113 -  by (induct p, simp, simp add: algebra_simps)
  5.1114 -
  5.1115 -lemma poly_mult [simp]: "poly (p * q) x = poly p x * poly q x"
  5.1116 -  by (induct p, simp_all, simp add: algebra_simps)
  5.1117 -
  5.1118 -lemma poly_power [simp]:
  5.1119 -  fixes p :: "'a::{comm_semiring_1,recpower} poly"
  5.1120 -  shows "poly (p ^ n) x = poly p x ^ n"
  5.1121 -  by (induct n, simp, simp add: power_Suc)
  5.1122 -
  5.1123 -
  5.1124 -subsection {* Synthetic division *}
  5.1125 -
  5.1126 -text {*
  5.1127 -  Synthetic division is simply division by the
  5.1128 -  linear polynomial @{term "x - c"}.
  5.1129 -*}
  5.1130 -
  5.1131 -definition
  5.1132 -  synthetic_divmod :: "'a::comm_semiring_0 poly \<Rightarrow> 'a \<Rightarrow> 'a poly \<times> 'a"
  5.1133 -where [code del]:
  5.1134 -  "synthetic_divmod p c =
  5.1135 -    poly_rec (0, 0) (\<lambda>a p (q, r). (pCons r q, a + c * r)) p"
  5.1136 -
  5.1137 -definition
  5.1138 -  synthetic_div :: "'a::comm_semiring_0 poly \<Rightarrow> 'a \<Rightarrow> 'a poly"
  5.1139 -where
  5.1140 -  "synthetic_div p c = fst (synthetic_divmod p c)"
  5.1141 -
  5.1142 -lemma synthetic_divmod_0 [simp]:
  5.1143 -  "synthetic_divmod 0 c = (0, 0)"
  5.1144 -  unfolding synthetic_divmod_def
  5.1145 -  by (simp add: poly_rec_0)
  5.1146 -
  5.1147 -lemma synthetic_divmod_pCons [simp]:
  5.1148 -  "synthetic_divmod (pCons a p) c =
  5.1149 -    (\<lambda>(q, r). (pCons r q, a + c * r)) (synthetic_divmod p c)"
  5.1150 -  unfolding synthetic_divmod_def
  5.1151 -  by (simp add: poly_rec_pCons)
  5.1152 -
  5.1153 -lemma snd_synthetic_divmod: "snd (synthetic_divmod p c) = poly p c"
  5.1154 -  by (induct p, simp, simp add: split_def)
  5.1155 -
  5.1156 -lemma synthetic_div_0 [simp]: "synthetic_div 0 c = 0"
  5.1157 -  unfolding synthetic_div_def by simp
  5.1158 -
  5.1159 -lemma synthetic_div_pCons [simp]:
  5.1160 -  "synthetic_div (pCons a p) c = pCons (poly p c) (synthetic_div p c)"
  5.1161 -  unfolding synthetic_div_def
  5.1162 -  by (simp add: split_def snd_synthetic_divmod)
  5.1163 -
  5.1164 -lemma synthetic_div_eq_0_iff:
  5.1165 -  "synthetic_div p c = 0 \<longleftrightarrow> degree p = 0"
  5.1166 -  by (induct p, simp, case_tac p, simp)
  5.1167 -
  5.1168 -lemma degree_synthetic_div:
  5.1169 -  "degree (synthetic_div p c) = degree p - 1"
  5.1170 -  by (induct p, simp, simp add: synthetic_div_eq_0_iff)
  5.1171 -
  5.1172 -lemma synthetic_div_correct:
  5.1173 -  "p + smult c (synthetic_div p c) = pCons (poly p c) (synthetic_div p c)"
  5.1174 -  by (induct p) simp_all
  5.1175 -
  5.1176 -lemma synthetic_div_unique_lemma: "smult c p = pCons a p \<Longrightarrow> p = 0"
  5.1177 -by (induct p arbitrary: a) simp_all
  5.1178 -
  5.1179 -lemma synthetic_div_unique:
  5.1180 -  "p + smult c q = pCons r q \<Longrightarrow> r = poly p c \<and> q = synthetic_div p c"
  5.1181 -apply (induct p arbitrary: q r)
  5.1182 -apply (simp, frule synthetic_div_unique_lemma, simp)
  5.1183 -apply (case_tac q, force)
  5.1184 -done
  5.1185 -
  5.1186 -lemma synthetic_div_correct':
  5.1187 -  fixes c :: "'a::comm_ring_1"
  5.1188 -  shows "[:-c, 1:] * synthetic_div p c + [:poly p c:] = p"
  5.1189 -  using synthetic_div_correct [of p c]
  5.1190 -  by (simp add: algebra_simps)
  5.1191 -
  5.1192 -lemma poly_eq_0_iff_dvd:
  5.1193 -  fixes c :: "'a::idom"
  5.1194 -  shows "poly p c = 0 \<longleftrightarrow> [:-c, 1:] dvd p"
  5.1195 -proof
  5.1196 -  assume "poly p c = 0"
  5.1197 -  with synthetic_div_correct' [of c p]
  5.1198 -  have "p = [:-c, 1:] * synthetic_div p c" by simp
  5.1199 -  then show "[:-c, 1:] dvd p" ..
  5.1200 -next
  5.1201 -  assume "[:-c, 1:] dvd p"
  5.1202 -  then obtain k where "p = [:-c, 1:] * k" by (rule dvdE)
  5.1203 -  then show "poly p c = 0" by simp
  5.1204 -qed
  5.1205 -
  5.1206 -lemma dvd_iff_poly_eq_0:
  5.1207 -  fixes c :: "'a::idom"
  5.1208 -  shows "[:c, 1:] dvd p \<longleftrightarrow> poly p (-c) = 0"
  5.1209 -  by (simp add: poly_eq_0_iff_dvd)
  5.1210 -
  5.1211 -lemma poly_roots_finite:
  5.1212 -  fixes p :: "'a::idom poly"
  5.1213 -  shows "p \<noteq> 0 \<Longrightarrow> finite {x. poly p x = 0}"
  5.1214 -proof (induct n \<equiv> "degree p" arbitrary: p)
  5.1215 -  case (0 p)
  5.1216 -  then obtain a where "a \<noteq> 0" and "p = [:a:]"
  5.1217 -    by (cases p, simp split: if_splits)
  5.1218 -  then show "finite {x. poly p x = 0}" by simp
  5.1219 -next
  5.1220 -  case (Suc n p)
  5.1221 -  show "finite {x. poly p x = 0}"
  5.1222 -  proof (cases "\<exists>x. poly p x = 0")
  5.1223 -    case False
  5.1224 -    then show "finite {x. poly p x = 0}" by simp
  5.1225 -  next
  5.1226 -    case True
  5.1227 -    then obtain a where "poly p a = 0" ..
  5.1228 -    then have "[:-a, 1:] dvd p" by (simp only: poly_eq_0_iff_dvd)
  5.1229 -    then obtain k where k: "p = [:-a, 1:] * k" ..
  5.1230 -    with `p \<noteq> 0` have "k \<noteq> 0" by auto
  5.1231 -    with k have "degree p = Suc (degree k)"
  5.1232 -      by (simp add: degree_mult_eq del: mult_pCons_left)
  5.1233 -    with `Suc n = degree p` have "n = degree k" by simp
  5.1234 -    with `k \<noteq> 0` have "finite {x. poly k x = 0}" by (rule Suc.hyps)
  5.1235 -    then have "finite (insert a {x. poly k x = 0})" by simp
  5.1236 -    then show "finite {x. poly p x = 0}"
  5.1237 -      by (simp add: k uminus_add_conv_diff Collect_disj_eq
  5.1238 -               del: mult_pCons_left)
  5.1239 -  qed
  5.1240 -qed
  5.1241 -
  5.1242 -lemma poly_zero:
  5.1243 -  fixes p :: "'a::{idom,ring_char_0} poly"
  5.1244 -  shows "poly p = poly 0 \<longleftrightarrow> p = 0"
  5.1245 -apply (cases "p = 0", simp_all)
  5.1246 -apply (drule poly_roots_finite)
  5.1247 -apply (auto simp add: infinite_UNIV_char_0)
  5.1248 -done
  5.1249 -
  5.1250 -lemma poly_eq_iff:
  5.1251 -  fixes p q :: "'a::{idom,ring_char_0} poly"
  5.1252 -  shows "poly p = poly q \<longleftrightarrow> p = q"
  5.1253 -  using poly_zero [of "p - q"]
  5.1254 -  by (simp add: expand_fun_eq)
  5.1255 -
  5.1256 -
  5.1257 -subsection {* Composition of polynomials *}
  5.1258 -
  5.1259 -definition
  5.1260 -  pcompose :: "'a::comm_semiring_0 poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
  5.1261 -where
  5.1262 -  "pcompose p q = poly_rec 0 (\<lambda>a _ c. [:a:] + q * c) p"
  5.1263 -
  5.1264 -lemma pcompose_0 [simp]: "pcompose 0 q = 0"
  5.1265 -  unfolding pcompose_def by (simp add: poly_rec_0)
  5.1266 -
  5.1267 -lemma pcompose_pCons:
  5.1268 -  "pcompose (pCons a p) q = [:a:] + q * pcompose p q"
  5.1269 -  unfolding pcompose_def by (simp add: poly_rec_pCons)
  5.1270 -
  5.1271 -lemma poly_pcompose: "poly (pcompose p q) x = poly p (poly q x)"
  5.1272 -  by (induct p) (simp_all add: pcompose_pCons)
  5.1273 -
  5.1274 -lemma degree_pcompose_le:
  5.1275 -  "degree (pcompose p q) \<le> degree p * degree q"
  5.1276 -apply (induct p, simp)
  5.1277 -apply (simp add: pcompose_pCons, clarify)
  5.1278 -apply (rule degree_add_le, simp)
  5.1279 -apply (rule order_trans [OF degree_mult_le], simp)
  5.1280 -done
  5.1281 -
  5.1282 -
  5.1283 -subsection {* Order of polynomial roots *}
  5.1284 -
  5.1285 -definition
  5.1286 -  order :: "'a::idom \<Rightarrow> 'a poly \<Rightarrow> nat"
  5.1287 -where
  5.1288 -  [code del]:
  5.1289 -  "order a p = (LEAST n. \<not> [:-a, 1:] ^ Suc n dvd p)"
  5.1290 -
  5.1291 -lemma coeff_linear_power:
  5.1292 -  fixes a :: "'a::comm_semiring_1"
  5.1293 -  shows "coeff ([:a, 1:] ^ n) n = 1"
  5.1294 -apply (induct n, simp_all)
  5.1295 -apply (subst coeff_eq_0)
  5.1296 -apply (auto intro: le_less_trans degree_power_le)
  5.1297 -done
  5.1298 -
  5.1299 -lemma degree_linear_power:
  5.1300 -  fixes a :: "'a::comm_semiring_1"
  5.1301 -  shows "degree ([:a, 1:] ^ n) = n"
  5.1302 -apply (rule order_antisym)
  5.1303 -apply (rule ord_le_eq_trans [OF degree_power_le], simp)
  5.1304 -apply (rule le_degree, simp add: coeff_linear_power)
  5.1305 -done
  5.1306 -
  5.1307 -lemma order_1: "[:-a, 1:] ^ order a p dvd p"
  5.1308 -apply (cases "p = 0", simp)
  5.1309 -apply (cases "order a p", simp)
  5.1310 -apply (subgoal_tac "nat < (LEAST n. \<not> [:-a, 1:] ^ Suc n dvd p)")
  5.1311 -apply (drule not_less_Least, simp)
  5.1312 -apply (fold order_def, simp)
  5.1313 -done
  5.1314 -
  5.1315 -lemma order_2: "p \<noteq> 0 \<Longrightarrow> \<not> [:-a, 1:] ^ Suc (order a p) dvd p"
  5.1316 -unfolding order_def
  5.1317 -apply (rule LeastI_ex)
  5.1318 -apply (rule_tac x="degree p" in exI)
  5.1319 -apply (rule notI)
  5.1320 -apply (drule (1) dvd_imp_degree_le)
  5.1321 -apply (simp only: degree_linear_power)
  5.1322 -done
  5.1323 -
  5.1324 -lemma order:
  5.1325 -  "p \<noteq> 0 \<Longrightarrow> [:-a, 1:] ^ order a p dvd p \<and> \<not> [:-a, 1:] ^ Suc (order a p) dvd p"
  5.1326 -by (rule conjI [OF order_1 order_2])
  5.1327 -
  5.1328 -lemma order_degree:
  5.1329 -  assumes p: "p \<noteq> 0"
  5.1330 -  shows "order a p \<le> degree p"
  5.1331 -proof -
  5.1332 -  have "order a p = degree ([:-a, 1:] ^ order a p)"
  5.1333 -    by (simp only: degree_linear_power)
  5.1334 -  also have "\<dots> \<le> degree p"
  5.1335 -    using order_1 p by (rule dvd_imp_degree_le)
  5.1336 -  finally show ?thesis .
  5.1337 -qed
  5.1338 -
  5.1339 -lemma order_root: "poly p a = 0 \<longleftrightarrow> p = 0 \<or> order a p \<noteq> 0"
  5.1340 -apply (cases "p = 0", simp_all)
  5.1341 -apply (rule iffI)
  5.1342 -apply (rule ccontr, simp)
  5.1343 -apply (frule order_2 [where a=a], simp)
  5.1344 -apply (simp add: poly_eq_0_iff_dvd)
  5.1345 -apply (simp add: poly_eq_0_iff_dvd)
  5.1346 -apply (simp only: order_def)
  5.1347 -apply (drule not_less_Least, simp)
  5.1348 -done
  5.1349 -
  5.1350 -
  5.1351 -subsection {* Configuration of the code generator *}
  5.1352 -
  5.1353 -code_datatype "0::'a::zero poly" pCons
  5.1354 -
  5.1355 -declare pCons_0_0 [code post]
  5.1356 -
  5.1357 -instantiation poly :: ("{zero,eq}") eq
  5.1358 -begin
  5.1359 -
  5.1360 -definition [code del]:
  5.1361 -  "eq_class.eq (p::'a poly) q \<longleftrightarrow> p = q"
  5.1362 -
  5.1363 -instance
  5.1364 -  by default (rule eq_poly_def)
  5.1365 -
  5.1366 -end
  5.1367 -
  5.1368 -lemma eq_poly_code [code]:
  5.1369 -  "eq_class.eq (0::_ poly) (0::_ poly) \<longleftrightarrow> True"
  5.1370 -  "eq_class.eq (0::_ poly) (pCons b q) \<longleftrightarrow> eq_class.eq 0 b \<and> eq_class.eq 0 q"
  5.1371 -  "eq_class.eq (pCons a p) (0::_ poly) \<longleftrightarrow> eq_class.eq a 0 \<and> eq_class.eq p 0"
  5.1372 -  "eq_class.eq (pCons a p) (pCons b q) \<longleftrightarrow> eq_class.eq a b \<and> eq_class.eq p q"
  5.1373 -unfolding eq by simp_all
  5.1374 -
  5.1375 -lemmas coeff_code [code] =
  5.1376 -  coeff_0 coeff_pCons_0 coeff_pCons_Suc
  5.1377 -
  5.1378 -lemmas degree_code [code] =
  5.1379 -  degree_0 degree_pCons_eq_if
  5.1380 -
  5.1381 -lemmas monom_poly_code [code] =
  5.1382 -  monom_0 monom_Suc
  5.1383 -
  5.1384 -lemma add_poly_code [code]:
  5.1385 -  "0 + q = (q :: _ poly)"
  5.1386 -  "p + 0 = (p :: _ poly)"
  5.1387 -  "pCons a p + pCons b q = pCons (a + b) (p + q)"
  5.1388 -by simp_all
  5.1389 -
  5.1390 -lemma minus_poly_code [code]:
  5.1391 -  "- 0 = (0 :: _ poly)"
  5.1392 -  "- pCons a p = pCons (- a) (- p)"
  5.1393 -by simp_all
  5.1394 -
  5.1395 -lemma diff_poly_code [code]:
  5.1396 -  "0 - q = (- q :: _ poly)"
  5.1397 -  "p - 0 = (p :: _ poly)"
  5.1398 -  "pCons a p - pCons b q = pCons (a - b) (p - q)"
  5.1399 -by simp_all
  5.1400 -
  5.1401 -lemmas smult_poly_code [code] =
  5.1402 -  smult_0_right smult_pCons
  5.1403 -
  5.1404 -lemma mult_poly_code [code]:
  5.1405 -  "0 * q = (0 :: _ poly)"
  5.1406 -  "pCons a p * q = smult a q + pCons 0 (p * q)"
  5.1407 -by simp_all
  5.1408 -
  5.1409 -lemmas poly_code [code] =
  5.1410 -  poly_0 poly_pCons
  5.1411 -
  5.1412 -lemmas synthetic_divmod_code [code] =
  5.1413 -  synthetic_divmod_0 synthetic_divmod_pCons
  5.1414 -
  5.1415 -text {* code generator setup for div and mod *}
  5.1416 -
  5.1417 -definition
  5.1418 -  pdivmod :: "'a::field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<times> 'a poly"
  5.1419 -where
  5.1420 -  [code del]: "pdivmod x y = (x div y, x mod y)"
  5.1421 -
  5.1422 -lemma div_poly_code [code]: "x div y = fst (pdivmod x y)"
  5.1423 -  unfolding pdivmod_def by simp
  5.1424 -
  5.1425 -lemma mod_poly_code [code]: "x mod y = snd (pdivmod x y)"
  5.1426 -  unfolding pdivmod_def by simp
  5.1427 -
  5.1428 -lemma pdivmod_0 [code]: "pdivmod 0 y = (0, 0)"
  5.1429 -  unfolding pdivmod_def by simp
  5.1430 -
  5.1431 -lemma pdivmod_pCons [code]:
  5.1432 -  "pdivmod (pCons a x) y =
  5.1433 -    (if y = 0 then (0, pCons a x) else
  5.1434 -      (let (q, r) = pdivmod x y;
  5.1435 -           b = coeff (pCons a r) (degree y) / coeff y (degree y)
  5.1436 -        in (pCons b q, pCons a r - smult b y)))"
  5.1437 -apply (simp add: pdivmod_def Let_def, safe)
  5.1438 -apply (rule div_poly_eq)
  5.1439 -apply (erule pdivmod_rel_pCons [OF pdivmod_rel _ refl])
  5.1440 -apply (rule mod_poly_eq)
  5.1441 -apply (erule pdivmod_rel_pCons [OF pdivmod_rel _ refl])
  5.1442 -done
  5.1443 -
  5.1444 -end