29451

1 
(* Title: HOL/Polynomial.thy


2 
Author: Brian Huffman


3 
Based on an earlier development by Clemens Ballarin


4 
*)


5 


6 
header {* Univariate Polynomials *}


7 


8 
theory Polynomial


9 
imports Plain SetInterval


10 
begin


11 


12 
subsection {* Definition of type @{text poly} *}


13 


14 
typedef (Poly) 'a poly = "{f::nat \<Rightarrow> 'a::zero. \<exists>n. \<forall>i>n. f i = 0}"


15 
morphisms coeff Abs_poly


16 
by auto


17 


18 
lemma expand_poly_eq: "p = q \<longleftrightarrow> (\<forall>n. coeff p n = coeff q n)"


19 
by (simp add: coeff_inject [symmetric] expand_fun_eq)


20 


21 
lemma poly_ext: "(\<And>n. coeff p n = coeff q n) \<Longrightarrow> p = q"


22 
by (simp add: expand_poly_eq)


23 


24 


25 
subsection {* Degree of a polynomial *}


26 


27 
definition


28 
degree :: "'a::zero poly \<Rightarrow> nat" where


29 
"degree p = (LEAST n. \<forall>i>n. coeff p i = 0)"


30 


31 
lemma coeff_eq_0: "degree p < n \<Longrightarrow> coeff p n = 0"


32 
proof 


33 
have "coeff p \<in> Poly"


34 
by (rule coeff)


35 
hence "\<exists>n. \<forall>i>n. coeff p i = 0"


36 
unfolding Poly_def by simp


37 
hence "\<forall>i>degree p. coeff p i = 0"


38 
unfolding degree_def by (rule LeastI_ex)


39 
moreover assume "degree p < n"


40 
ultimately show ?thesis by simp


41 
qed


42 


43 
lemma le_degree: "coeff p n \<noteq> 0 \<Longrightarrow> n \<le> degree p"


44 
by (erule contrapos_np, rule coeff_eq_0, simp)


45 


46 
lemma degree_le: "\<forall>i>n. coeff p i = 0 \<Longrightarrow> degree p \<le> n"


47 
unfolding degree_def by (erule Least_le)


48 


49 
lemma less_degree_imp: "n < degree p \<Longrightarrow> \<exists>i>n. coeff p i \<noteq> 0"


50 
unfolding degree_def by (drule not_less_Least, simp)


51 


52 


53 
subsection {* The zero polynomial *}


54 


55 
instantiation poly :: (zero) zero


56 
begin


57 


58 
definition


59 
zero_poly_def: "0 = Abs_poly (\<lambda>n. 0)"


60 


61 
instance ..


62 
end


63 


64 
lemma coeff_0 [simp]: "coeff 0 n = 0"


65 
unfolding zero_poly_def


66 
by (simp add: Abs_poly_inverse Poly_def)


67 


68 
lemma degree_0 [simp]: "degree 0 = 0"


69 
by (rule order_antisym [OF degree_le le0]) simp


70 


71 
lemma leading_coeff_neq_0:


72 
assumes "p \<noteq> 0" shows "coeff p (degree p) \<noteq> 0"


73 
proof (cases "degree p")


74 
case 0


75 
from `p \<noteq> 0` have "\<exists>n. coeff p n \<noteq> 0"


76 
by (simp add: expand_poly_eq)


77 
then obtain n where "coeff p n \<noteq> 0" ..


78 
hence "n \<le> degree p" by (rule le_degree)


79 
with `coeff p n \<noteq> 0` and `degree p = 0`


80 
show "coeff p (degree p) \<noteq> 0" by simp


81 
next


82 
case (Suc n)


83 
from `degree p = Suc n` have "n < degree p" by simp


84 
hence "\<exists>i>n. coeff p i \<noteq> 0" by (rule less_degree_imp)


85 
then obtain i where "n < i" and "coeff p i \<noteq> 0" by fast


86 
from `degree p = Suc n` and `n < i` have "degree p \<le> i" by simp


87 
also from `coeff p i \<noteq> 0` have "i \<le> degree p" by (rule le_degree)


88 
finally have "degree p = i" .


89 
with `coeff p i \<noteq> 0` show "coeff p (degree p) \<noteq> 0" by simp


90 
qed


91 


92 
lemma leading_coeff_0_iff [simp]: "coeff p (degree p) = 0 \<longleftrightarrow> p = 0"


93 
by (cases "p = 0", simp, simp add: leading_coeff_neq_0)


94 


95 


96 
subsection {* Liststyle constructor for polynomials *}


97 


98 
definition


99 
pCons :: "'a::zero \<Rightarrow> 'a poly \<Rightarrow> 'a poly"


100 
where


101 
[code del]: "pCons a p = Abs_poly (nat_case a (coeff p))"


102 


103 
lemma Poly_nat_case: "f \<in> Poly \<Longrightarrow> nat_case a f \<in> Poly"


104 
unfolding Poly_def by (auto split: nat.split)


105 


106 
lemma coeff_pCons:


107 
"coeff (pCons a p) = nat_case a (coeff p)"


108 
unfolding pCons_def


109 
by (simp add: Abs_poly_inverse Poly_nat_case coeff)


110 


111 
lemma coeff_pCons_0 [simp]: "coeff (pCons a p) 0 = a"


112 
by (simp add: coeff_pCons)


113 


114 
lemma coeff_pCons_Suc [simp]: "coeff (pCons a p) (Suc n) = coeff p n"


115 
by (simp add: coeff_pCons)


116 


117 
lemma degree_pCons_le: "degree (pCons a p) \<le> Suc (degree p)"


118 
by (rule degree_le, simp add: coeff_eq_0 coeff_pCons split: nat.split)


119 


120 
lemma degree_pCons_eq:


121 
"p \<noteq> 0 \<Longrightarrow> degree (pCons a p) = Suc (degree p)"


122 
apply (rule order_antisym [OF degree_pCons_le])


123 
apply (rule le_degree, simp)


124 
done


125 


126 
lemma degree_pCons_0: "degree (pCons a 0) = 0"


127 
apply (rule order_antisym [OF _ le0])


128 
apply (rule degree_le, simp add: coeff_pCons split: nat.split)


129 
done


130 


131 
lemma degree_pCons_eq_if:


132 
"degree (pCons a p) = (if p = 0 then 0 else Suc (degree p))"


133 
apply (cases "p = 0", simp_all)


134 
apply (rule order_antisym [OF _ le0])


135 
apply (rule degree_le, simp add: coeff_pCons split: nat.split)


136 
apply (rule order_antisym [OF degree_pCons_le])


137 
apply (rule le_degree, simp)


138 
done


139 


140 
lemma pCons_0_0 [simp]: "pCons 0 0 = 0"


141 
by (rule poly_ext, simp add: coeff_pCons split: nat.split)


142 


143 
lemma pCons_eq_iff [simp]:


144 
"pCons a p = pCons b q \<longleftrightarrow> a = b \<and> p = q"


145 
proof (safe)


146 
assume "pCons a p = pCons b q"


147 
then have "coeff (pCons a p) 0 = coeff (pCons b q) 0" by simp


148 
then show "a = b" by simp


149 
next


150 
assume "pCons a p = pCons b q"


151 
then have "\<forall>n. coeff (pCons a p) (Suc n) =


152 
coeff (pCons b q) (Suc n)" by simp


153 
then show "p = q" by (simp add: expand_poly_eq)


154 
qed


155 


156 
lemma pCons_eq_0_iff [simp]: "pCons a p = 0 \<longleftrightarrow> a = 0 \<and> p = 0"


157 
using pCons_eq_iff [of a p 0 0] by simp


158 


159 
lemma Poly_Suc: "f \<in> Poly \<Longrightarrow> (\<lambda>n. f (Suc n)) \<in> Poly"


160 
unfolding Poly_def


161 
by (clarify, rule_tac x=n in exI, simp)


162 


163 
lemma pCons_cases [cases type: poly]:


164 
obtains (pCons) a q where "p = pCons a q"


165 
proof


166 
show "p = pCons (coeff p 0) (Abs_poly (\<lambda>n. coeff p (Suc n)))"


167 
by (rule poly_ext)


168 
(simp add: Abs_poly_inverse Poly_Suc coeff coeff_pCons


169 
split: nat.split)


170 
qed


171 


172 
lemma pCons_induct [case_names 0 pCons, induct type: poly]:


173 
assumes zero: "P 0"


174 
assumes pCons: "\<And>a p. P p \<Longrightarrow> P (pCons a p)"


175 
shows "P p"


176 
proof (induct p rule: measure_induct_rule [where f=degree])


177 
case (less p)


178 
obtain a q where "p = pCons a q" by (rule pCons_cases)


179 
have "P q"


180 
proof (cases "q = 0")


181 
case True


182 
then show "P q" by (simp add: zero)


183 
next


184 
case False


185 
then have "degree (pCons a q) = Suc (degree q)"


186 
by (rule degree_pCons_eq)


187 
then have "degree q < degree p"


188 
using `p = pCons a q` by simp


189 
then show "P q"


190 
by (rule less.hyps)


191 
qed


192 
then have "P (pCons a q)"


193 
by (rule pCons)


194 
then show ?case


195 
using `p = pCons a q` by simp


196 
qed


197 


198 


199 
subsection {* Monomials *}


200 


201 
definition


202 
monom :: "'a \<Rightarrow> nat \<Rightarrow> 'a::zero poly" where


203 
"monom a m = Abs_poly (\<lambda>n. if m = n then a else 0)"


204 


205 
lemma coeff_monom [simp]: "coeff (monom a m) n = (if m=n then a else 0)"


206 
unfolding monom_def


207 
by (subst Abs_poly_inverse, auto simp add: Poly_def)


208 


209 
lemma monom_0: "monom a 0 = pCons a 0"


210 
by (rule poly_ext, simp add: coeff_pCons split: nat.split)


211 


212 
lemma monom_Suc: "monom a (Suc n) = pCons 0 (monom a n)"


213 
by (rule poly_ext, simp add: coeff_pCons split: nat.split)


214 


215 
lemma monom_eq_0 [simp]: "monom 0 n = 0"


216 
by (rule poly_ext) simp


217 


218 
lemma monom_eq_0_iff [simp]: "monom a n = 0 \<longleftrightarrow> a = 0"


219 
by (simp add: expand_poly_eq)


220 


221 
lemma monom_eq_iff [simp]: "monom a n = monom b n \<longleftrightarrow> a = b"


222 
by (simp add: expand_poly_eq)


223 


224 
lemma degree_monom_le: "degree (monom a n) \<le> n"


225 
by (rule degree_le, simp)


226 


227 
lemma degree_monom_eq: "a \<noteq> 0 \<Longrightarrow> degree (monom a n) = n"


228 
apply (rule order_antisym [OF degree_monom_le])


229 
apply (rule le_degree, simp)


230 
done


231 


232 


233 
subsection {* Addition and subtraction *}


234 


235 
instantiation poly :: (comm_monoid_add) comm_monoid_add


236 
begin


237 


238 
definition


239 
plus_poly_def [code del]:


240 
"p + q = Abs_poly (\<lambda>n. coeff p n + coeff q n)"


241 


242 
lemma Poly_add:


243 
fixes f g :: "nat \<Rightarrow> 'a"


244 
shows "\<lbrakk>f \<in> Poly; g \<in> Poly\<rbrakk> \<Longrightarrow> (\<lambda>n. f n + g n) \<in> Poly"


245 
unfolding Poly_def


246 
apply (clarify, rename_tac m n)


247 
apply (rule_tac x="max m n" in exI, simp)


248 
done


249 


250 
lemma coeff_add [simp]:


251 
"coeff (p + q) n = coeff p n + coeff q n"


252 
unfolding plus_poly_def


253 
by (simp add: Abs_poly_inverse coeff Poly_add)


254 


255 
instance proof


256 
fix p q r :: "'a poly"


257 
show "(p + q) + r = p + (q + r)"


258 
by (simp add: expand_poly_eq add_assoc)


259 
show "p + q = q + p"


260 
by (simp add: expand_poly_eq add_commute)


261 
show "0 + p = p"


262 
by (simp add: expand_poly_eq)


263 
qed


264 


265 
end


266 


267 
instantiation poly :: (ab_group_add) ab_group_add


268 
begin


269 


270 
definition


271 
uminus_poly_def [code del]:


272 
" p = Abs_poly (\<lambda>n.  coeff p n)"


273 


274 
definition


275 
minus_poly_def [code del]:


276 
"p  q = Abs_poly (\<lambda>n. coeff p n  coeff q n)"


277 


278 
lemma Poly_minus:


279 
fixes f :: "nat \<Rightarrow> 'a"


280 
shows "f \<in> Poly \<Longrightarrow> (\<lambda>n.  f n) \<in> Poly"


281 
unfolding Poly_def by simp


282 


283 
lemma Poly_diff:


284 
fixes f g :: "nat \<Rightarrow> 'a"


285 
shows "\<lbrakk>f \<in> Poly; g \<in> Poly\<rbrakk> \<Longrightarrow> (\<lambda>n. f n  g n) \<in> Poly"


286 
unfolding diff_minus by (simp add: Poly_add Poly_minus)


287 


288 
lemma coeff_minus [simp]: "coeff ( p) n =  coeff p n"


289 
unfolding uminus_poly_def


290 
by (simp add: Abs_poly_inverse coeff Poly_minus)


291 


292 
lemma coeff_diff [simp]:


293 
"coeff (p  q) n = coeff p n  coeff q n"


294 
unfolding minus_poly_def


295 
by (simp add: Abs_poly_inverse coeff Poly_diff)


296 


297 
instance proof


298 
fix p q :: "'a poly"


299 
show " p + p = 0"


300 
by (simp add: expand_poly_eq)


301 
show "p  q = p +  q"


302 
by (simp add: expand_poly_eq diff_minus)


303 
qed


304 


305 
end


306 


307 
lemma add_pCons [simp]:


308 
"pCons a p + pCons b q = pCons (a + b) (p + q)"


309 
by (rule poly_ext, simp add: coeff_pCons split: nat.split)


310 


311 
lemma minus_pCons [simp]:


312 
" pCons a p = pCons ( a) ( p)"


313 
by (rule poly_ext, simp add: coeff_pCons split: nat.split)


314 


315 
lemma diff_pCons [simp]:


316 
"pCons a p  pCons b q = pCons (a  b) (p  q)"


317 
by (rule poly_ext, simp add: coeff_pCons split: nat.split)


318 


319 
lemma degree_add_le: "degree (p + q) \<le> max (degree p) (degree q)"


320 
by (rule degree_le, auto simp add: coeff_eq_0)


321 


322 
lemma degree_add_eq_right:


323 
"degree p < degree q \<Longrightarrow> degree (p + q) = degree q"


324 
apply (cases "q = 0", simp)


325 
apply (rule order_antisym)


326 
apply (rule ord_le_eq_trans [OF degree_add_le])


327 
apply simp


328 
apply (rule le_degree)


329 
apply (simp add: coeff_eq_0)


330 
done


331 


332 
lemma degree_add_eq_left:


333 
"degree q < degree p \<Longrightarrow> degree (p + q) = degree p"


334 
using degree_add_eq_right [of q p]


335 
by (simp add: add_commute)


336 


337 
lemma degree_minus [simp]: "degree ( p) = degree p"


338 
unfolding degree_def by simp


339 


340 
lemma degree_diff_le: "degree (p  q) \<le> max (degree p) (degree q)"


341 
using degree_add_le [where p=p and q="q"]


342 
by (simp add: diff_minus)


343 


344 
lemma add_monom: "monom a n + monom b n = monom (a + b) n"


345 
by (rule poly_ext) simp


346 


347 
lemma diff_monom: "monom a n  monom b n = monom (a  b) n"


348 
by (rule poly_ext) simp


349 


350 
lemma minus_monom: " monom a n = monom (a) n"


351 
by (rule poly_ext) simp


352 


353 
lemma coeff_setsum: "coeff (\<Sum>x\<in>A. p x) i = (\<Sum>x\<in>A. coeff (p x) i)"


354 
by (cases "finite A", induct set: finite, simp_all)


355 


356 
lemma monom_setsum: "monom (\<Sum>x\<in>A. a x) n = (\<Sum>x\<in>A. monom (a x) n)"


357 
by (rule poly_ext) (simp add: coeff_setsum)


358 


359 


360 
subsection {* Multiplication by a constant *}


361 


362 
definition


363 
smult :: "'a::comm_semiring_0 \<Rightarrow> 'a poly \<Rightarrow> 'a poly" where


364 
"smult a p = Abs_poly (\<lambda>n. a * coeff p n)"


365 


366 
lemma Poly_smult:


367 
fixes f :: "nat \<Rightarrow> 'a::comm_semiring_0"


368 
shows "f \<in> Poly \<Longrightarrow> (\<lambda>n. a * f n) \<in> Poly"


369 
unfolding Poly_def


370 
by (clarify, rule_tac x=n in exI, simp)


371 


372 
lemma coeff_smult [simp]: "coeff (smult a p) n = a * coeff p n"


373 
unfolding smult_def


374 
by (simp add: Abs_poly_inverse Poly_smult coeff)


375 


376 
lemma degree_smult_le: "degree (smult a p) \<le> degree p"


377 
by (rule degree_le, simp add: coeff_eq_0)


378 


379 
lemma smult_smult: "smult a (smult b p) = smult (a * b) p"


380 
by (rule poly_ext, simp add: mult_assoc)


381 


382 
lemma smult_0_right [simp]: "smult a 0 = 0"


383 
by (rule poly_ext, simp)


384 


385 
lemma smult_0_left [simp]: "smult 0 p = 0"


386 
by (rule poly_ext, simp)


387 


388 
lemma smult_1_left [simp]: "smult (1::'a::comm_semiring_1) p = p"


389 
by (rule poly_ext, simp)


390 


391 
lemma smult_add_right:


392 
"smult a (p + q) = smult a p + smult a q"


393 
by (rule poly_ext, simp add: ring_simps)


394 


395 
lemma smult_add_left:


396 
"smult (a + b) p = smult a p + smult b p"


397 
by (rule poly_ext, simp add: ring_simps)


398 


399 
lemma smult_minus_right:


400 
"smult (a::'a::comm_ring) ( p) =  smult a p"


401 
by (rule poly_ext, simp)


402 


403 
lemma smult_minus_left:


404 
"smult ( a::'a::comm_ring) p =  smult a p"


405 
by (rule poly_ext, simp)


406 


407 
lemma smult_diff_right:


408 
"smult (a::'a::comm_ring) (p  q) = smult a p  smult a q"


409 
by (rule poly_ext, simp add: ring_simps)


410 


411 
lemma smult_diff_left:


412 
"smult (a  b::'a::comm_ring) p = smult a p  smult b p"


413 
by (rule poly_ext, simp add: ring_simps)


414 


415 
lemma smult_pCons [simp]:


416 
"smult a (pCons b p) = pCons (a * b) (smult a p)"


417 
by (rule poly_ext, simp add: coeff_pCons split: nat.split)


418 


419 
lemma smult_monom: "smult a (monom b n) = monom (a * b) n"


420 
by (induct n, simp add: monom_0, simp add: monom_Suc)


421 


422 


423 
subsection {* Multiplication of polynomials *}


424 


425 
lemma Poly_mult_lemma:


426 
fixes f g :: "nat \<Rightarrow> 'a::comm_semiring_0" and m n :: nat


427 
assumes "\<forall>i>m. f i = 0"


428 
assumes "\<forall>j>n. g j = 0"


429 
shows "\<forall>k>m+n. (\<Sum>i\<le>k. f i * g (ki)) = 0"


430 
proof (clarify)


431 
fix k :: nat


432 
assume "m + n < k"


433 
show "(\<Sum>i\<le>k. f i * g (k  i)) = 0"


434 
proof (rule setsum_0' [rule_format])


435 
fix i :: nat


436 
assume "i \<in> {..k}" hence "i \<le> k" by simp


437 
with `m + n < k` have "m < i \<or> n < k  i" by arith


438 
thus "f i * g (k  i) = 0"


439 
using prems by auto


440 
qed


441 
qed


442 


443 
lemma Poly_mult:


444 
fixes f g :: "nat \<Rightarrow> 'a::comm_semiring_0"


445 
shows "\<lbrakk>f \<in> Poly; g \<in> Poly\<rbrakk> \<Longrightarrow> (\<lambda>n. \<Sum>i\<le>n. f i * g (ni)) \<in> Poly"


446 
unfolding Poly_def


447 
by (safe, rule exI, rule Poly_mult_lemma)


448 


449 
lemma poly_mult_assoc_lemma:


450 
fixes k :: nat and f :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a::comm_monoid_add"


451 
shows "(\<Sum>j\<le>k. \<Sum>i\<le>j. f i (j  i) (n  j)) =


452 
(\<Sum>j\<le>k. \<Sum>i\<le>k  j. f j i (n  j  i))"


453 
proof (induct k)


454 
case 0 show ?case by simp


455 
next


456 
case (Suc k) thus ?case


457 
by (simp add: Suc_diff_le setsum_addf add_assoc


458 
cong: strong_setsum_cong)


459 
qed


460 


461 
lemma poly_mult_commute_lemma:


462 
fixes n :: nat and f :: "nat \<Rightarrow> nat \<Rightarrow> 'a::comm_monoid_add"


463 
shows "(\<Sum>i\<le>n. f i (n  i)) = (\<Sum>i\<le>n. f (n  i) i)"


464 
proof (rule setsum_reindex_cong)


465 
show "inj_on (\<lambda>i. n  i) {..n}"


466 
by (rule inj_onI) simp


467 
show "{..n} = (\<lambda>i. n  i) ` {..n}"


468 
by (auto, rule_tac x="n  x" in image_eqI, simp_all)


469 
next


470 
fix i assume "i \<in> {..n}"


471 
hence "n  (n  i) = i" by simp


472 
thus "f (n  i) i = f (n  i) (n  (n  i))" by simp


473 
qed


474 


475 
text {* TODO: move to appropriate theory *}


476 
lemma setsum_atMost_Suc_shift:


477 
fixes f :: "nat \<Rightarrow> 'a::comm_monoid_add"


478 
shows "(\<Sum>i\<le>Suc n. f i) = f 0 + (\<Sum>i\<le>n. f (Suc i))"


479 
proof (induct n)


480 
case 0 show ?case by simp


481 
next


482 
case (Suc n) note IH = this


483 
have "(\<Sum>i\<le>Suc (Suc n). f i) = (\<Sum>i\<le>Suc n. f i) + f (Suc (Suc n))"


484 
by (rule setsum_atMost_Suc)


485 
also have "(\<Sum>i\<le>Suc n. f i) = f 0 + (\<Sum>i\<le>n. f (Suc i))"


486 
by (rule IH)


487 
also have "f 0 + (\<Sum>i\<le>n. f (Suc i)) + f (Suc (Suc n)) =


488 
f 0 + ((\<Sum>i\<le>n. f (Suc i)) + f (Suc (Suc n)))"


489 
by (rule add_assoc)


490 
also have "(\<Sum>i\<le>n. f (Suc i)) + f (Suc (Suc n)) = (\<Sum>i\<le>Suc n. f (Suc i))"


491 
by (rule setsum_atMost_Suc [symmetric])


492 
finally show ?case .


493 
qed


494 


495 
instantiation poly :: (comm_semiring_0) comm_semiring_0


496 
begin


497 


498 
definition


499 
times_poly_def:


500 
"p * q = Abs_poly (\<lambda>n. \<Sum>i\<le>n. coeff p i * coeff q (ni))"


501 


502 
lemma coeff_mult:


503 
"coeff (p * q) n = (\<Sum>i\<le>n. coeff p i * coeff q (ni))"


504 
unfolding times_poly_def


505 
by (simp add: Abs_poly_inverse coeff Poly_mult)


506 


507 
instance proof


508 
fix p q r :: "'a poly"


509 
show 0: "0 * p = 0"


510 
by (simp add: expand_poly_eq coeff_mult)


511 
show "p * 0 = 0"


512 
by (simp add: expand_poly_eq coeff_mult)


513 
show "(p + q) * r = p * r + q * r"


514 
by (simp add: expand_poly_eq coeff_mult left_distrib setsum_addf)


515 
show "(p * q) * r = p * (q * r)"


516 
proof (rule poly_ext)


517 
fix n :: nat


518 
have "(\<Sum>j\<le>n. \<Sum>i\<le>j. coeff p i * coeff q (j  i) * coeff r (n  j)) =


519 
(\<Sum>j\<le>n. \<Sum>i\<le>n  j. coeff p j * coeff q i * coeff r (n  j  i))"


520 
by (rule poly_mult_assoc_lemma)


521 
thus "coeff ((p * q) * r) n = coeff (p * (q * r)) n"


522 
by (simp add: coeff_mult setsum_right_distrib


523 
setsum_left_distrib mult_assoc)


524 
qed


525 
show "p * q = q * p"


526 
proof (rule poly_ext)


527 
fix n :: nat


528 
have "(\<Sum>i\<le>n. coeff p i * coeff q (n  i)) =


529 
(\<Sum>i\<le>n. coeff p (n  i) * coeff q i)"


530 
by (rule poly_mult_commute_lemma)


531 
thus "coeff (p * q) n = coeff (q * p) n"


532 
by (simp add: coeff_mult mult_commute)


533 
qed


534 
qed


535 


536 
end


537 


538 
lemma degree_mult_le: "degree (p * q) \<le> degree p + degree q"


539 
apply (rule degree_le, simp add: coeff_mult)


540 
apply (rule Poly_mult_lemma)


541 
apply (simp_all add: coeff_eq_0)


542 
done


543 


544 
lemma mult_pCons_left [simp]:


545 
"pCons a p * q = smult a q + pCons 0 (p * q)"


546 
apply (rule poly_ext)


547 
apply (case_tac n)


548 
apply (simp add: coeff_mult)


549 
apply (simp add: coeff_mult setsum_atMost_Suc_shift


550 
del: setsum_atMost_Suc)


551 
done


552 


553 
lemma mult_pCons_right [simp]:


554 
"p * pCons a q = smult a p + pCons 0 (p * q)"


555 
using mult_pCons_left [of a q p] by (simp add: mult_commute)


556 


557 
lemma mult_smult_left: "smult a p * q = smult a (p * q)"


558 
by (induct p, simp, simp add: smult_add_right smult_smult)


559 


560 
lemma mult_smult_right: "p * smult a q = smult a (p * q)"


561 
using mult_smult_left [of a q p] by (simp add: mult_commute)


562 


563 
lemma mult_monom: "monom a m * monom b n = monom (a * b) (m + n)"


564 
by (induct m, simp add: monom_0 smult_monom, simp add: monom_Suc)


565 


566 


567 
subsection {* The unit polynomial and exponentiation *}


568 


569 
instantiation poly :: (comm_semiring_1) comm_semiring_1


570 
begin


571 


572 
definition


573 
one_poly_def:


574 
"1 = pCons 1 0"


575 


576 
instance proof


577 
fix p :: "'a poly" show "1 * p = p"


578 
unfolding one_poly_def


579 
by simp


580 
next


581 
show "0 \<noteq> (1::'a poly)"


582 
unfolding one_poly_def by simp


583 
qed


584 


585 
end


586 


587 
lemma coeff_1 [simp]: "coeff 1 n = (if n = 0 then 1 else 0)"


588 
unfolding one_poly_def


589 
by (simp add: coeff_pCons split: nat.split)


590 


591 
lemma degree_1 [simp]: "degree 1 = 0"


592 
unfolding one_poly_def


593 
by (rule degree_pCons_0)


594 


595 
instantiation poly :: (comm_semiring_1) recpower


596 
begin


597 


598 
primrec power_poly where


599 
power_poly_0: "(p::'a poly) ^ 0 = 1"


600 
 power_poly_Suc: "(p::'a poly) ^ (Suc n) = p * p ^ n"


601 


602 
instance


603 
by default simp_all


604 


605 
end


606 


607 
instance poly :: (comm_ring) comm_ring ..


608 


609 
instance poly :: (comm_ring_1) comm_ring_1 ..


610 


611 
instantiation poly :: (comm_ring_1) number_ring


612 
begin


613 


614 
definition


615 
"number_of k = (of_int k :: 'a poly)"


616 


617 
instance


618 
by default (rule number_of_poly_def)


619 


620 
end


621 


622 


623 
subsection {* Polynomials form an integral domain *}


624 


625 
lemma coeff_mult_degree_sum:


626 
"coeff (p * q) (degree p + degree q) =


627 
coeff p (degree p) * coeff q (degree q)"


628 
apply (simp add: coeff_mult)


629 
apply (subst setsum_diff1' [where a="degree p"])


630 
apply simp


631 
apply simp


632 
apply (subst setsum_0' [rule_format])


633 
apply clarsimp


634 
apply (subgoal_tac "degree p < a \<or> degree q < degree p + degree q  a")


635 
apply (force simp add: coeff_eq_0)


636 
apply arith


637 
apply simp


638 
done


639 


640 
instance poly :: (idom) idom


641 
proof


642 
fix p q :: "'a poly"


643 
assume "p \<noteq> 0" and "q \<noteq> 0"


644 
have "coeff (p * q) (degree p + degree q) =


645 
coeff p (degree p) * coeff q (degree q)"


646 
by (rule coeff_mult_degree_sum)


647 
also have "coeff p (degree p) * coeff q (degree q) \<noteq> 0"


648 
using `p \<noteq> 0` and `q \<noteq> 0` by simp


649 
finally have "\<exists>n. coeff (p * q) n \<noteq> 0" ..


650 
thus "p * q \<noteq> 0" by (simp add: expand_poly_eq)


651 
qed


652 


653 
lemma degree_mult_eq:


654 
fixes p q :: "'a::idom poly"


655 
shows "\<lbrakk>p \<noteq> 0; q \<noteq> 0\<rbrakk> \<Longrightarrow> degree (p * q) = degree p + degree q"


656 
apply (rule order_antisym [OF degree_mult_le le_degree])


657 
apply (simp add: coeff_mult_degree_sum)


658 
done


659 


660 
lemma dvd_imp_degree_le:


661 
fixes p q :: "'a::idom poly"


662 
shows "\<lbrakk>p dvd q; q \<noteq> 0\<rbrakk> \<Longrightarrow> degree p \<le> degree q"


663 
by (erule dvdE, simp add: degree_mult_eq)


664 


665 


666 
subsection {* Long division of polynomials *}


667 


668 
definition


669 
divmod_poly_rel :: "'a::field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<Rightarrow> bool"


670 
where


671 
"divmod_poly_rel x y q r \<longleftrightarrow>


672 
x = q * y + r \<and> (if y = 0 then q = 0 else r = 0 \<or> degree r < degree y)"


673 


674 
lemma divmod_poly_rel_0:


675 
"divmod_poly_rel 0 y 0 0"


676 
unfolding divmod_poly_rel_def by simp


677 


678 
lemma divmod_poly_rel_by_0:


679 
"divmod_poly_rel x 0 0 x"


680 
unfolding divmod_poly_rel_def by simp


681 


682 
lemma eq_zero_or_degree_less:


683 
assumes "degree p \<le> n" and "coeff p n = 0"


684 
shows "p = 0 \<or> degree p < n"


685 
proof (cases n)


686 
case 0


687 
with `degree p \<le> n` and `coeff p n = 0`


688 
have "coeff p (degree p) = 0" by simp


689 
then have "p = 0" by simp


690 
then show ?thesis ..


691 
next


692 
case (Suc m)


693 
have "\<forall>i>n. coeff p i = 0"


694 
using `degree p \<le> n` by (simp add: coeff_eq_0)


695 
then have "\<forall>i\<ge>n. coeff p i = 0"


696 
using `coeff p n = 0` by (simp add: le_less)


697 
then have "\<forall>i>m. coeff p i = 0"


698 
using `n = Suc m` by (simp add: less_eq_Suc_le)


699 
then have "degree p \<le> m"


700 
by (rule degree_le)


701 
then have "degree p < n"


702 
using `n = Suc m` by (simp add: less_Suc_eq_le)


703 
then show ?thesis ..


704 
qed


705 


706 
lemma divmod_poly_rel_pCons:


707 
assumes rel: "divmod_poly_rel x y q r"


708 
assumes y: "y \<noteq> 0"


709 
assumes b: "b = coeff (pCons a r) (degree y) / coeff y (degree y)"


710 
shows "divmod_poly_rel (pCons a x) y (pCons b q) (pCons a r  smult b y)"


711 
(is "divmod_poly_rel ?x y ?q ?r")


712 
proof 


713 
have x: "x = q * y + r" and r: "r = 0 \<or> degree r < degree y"


714 
using assms unfolding divmod_poly_rel_def by simp_all


715 


716 
have 1: "?x = ?q * y + ?r"


717 
using b x by simp


718 


719 
have 2: "?r = 0 \<or> degree ?r < degree y"


720 
proof (rule eq_zero_or_degree_less)


721 
have "degree ?r \<le> max (degree (pCons a r)) (degree (smult b y))"


722 
by (rule degree_diff_le)


723 
also have "\<dots> \<le> degree y"


724 
proof (rule min_max.le_supI)


725 
show "degree (pCons a r) \<le> degree y"


726 
using r by (auto simp add: degree_pCons_eq_if)


727 
show "degree (smult b y) \<le> degree y"


728 
by (rule degree_smult_le)


729 
qed


730 
finally show "degree ?r \<le> degree y" .


731 
next


732 
show "coeff ?r (degree y) = 0"


733 
using `y \<noteq> 0` unfolding b by simp


734 
qed


735 


736 
from 1 2 show ?thesis


737 
unfolding divmod_poly_rel_def


738 
using `y \<noteq> 0` by simp


739 
qed


740 


741 
lemma divmod_poly_rel_exists: "\<exists>q r. divmod_poly_rel x y q r"


742 
apply (cases "y = 0")


743 
apply (fast intro!: divmod_poly_rel_by_0)


744 
apply (induct x)


745 
apply (fast intro!: divmod_poly_rel_0)


746 
apply (fast intro!: divmod_poly_rel_pCons)


747 
done


748 


749 
lemma divmod_poly_rel_unique:


750 
assumes 1: "divmod_poly_rel x y q1 r1"


751 
assumes 2: "divmod_poly_rel x y q2 r2"


752 
shows "q1 = q2 \<and> r1 = r2"


753 
proof (cases "y = 0")


754 
assume "y = 0" with assms show ?thesis


755 
by (simp add: divmod_poly_rel_def)


756 
next


757 
assume [simp]: "y \<noteq> 0"


758 
from 1 have q1: "x = q1 * y + r1" and r1: "r1 = 0 \<or> degree r1 < degree y"


759 
unfolding divmod_poly_rel_def by simp_all


760 
from 2 have q2: "x = q2 * y + r2" and r2: "r2 = 0 \<or> degree r2 < degree y"


761 
unfolding divmod_poly_rel_def by simp_all


762 
from q1 q2 have q3: "(q1  q2) * y = r2  r1"


763 
by (simp add: ring_simps)


764 
from r1 r2 have r3: "(r2  r1) = 0 \<or> degree (r2  r1) < degree y"


765 
by (auto intro: le_less_trans [OF degree_diff_le])


766 


767 
show "q1 = q2 \<and> r1 = r2"


768 
proof (rule ccontr)


769 
assume "\<not> (q1 = q2 \<and> r1 = r2)"


770 
with q3 have "q1 \<noteq> q2" and "r1 \<noteq> r2" by auto


771 
with r3 have "degree (r2  r1) < degree y" by simp


772 
also have "degree y \<le> degree (q1  q2) + degree y" by simp


773 
also have "\<dots> = degree ((q1  q2) * y)"


774 
using `q1 \<noteq> q2` by (simp add: degree_mult_eq)


775 
also have "\<dots> = degree (r2  r1)"


776 
using q3 by simp


777 
finally have "degree (r2  r1) < degree (r2  r1)" .


778 
then show "False" by simp


779 
qed


780 
qed


781 


782 
lemmas divmod_poly_rel_unique_div =


783 
divmod_poly_rel_unique [THEN conjunct1, standard]


784 


785 
lemmas divmod_poly_rel_unique_mod =


786 
divmod_poly_rel_unique [THEN conjunct2, standard]


787 


788 
instantiation poly :: (field) ring_div


789 
begin


790 


791 
definition div_poly where


792 
[code del]: "x div y = (THE q. \<exists>r. divmod_poly_rel x y q r)"


793 


794 
definition mod_poly where


795 
[code del]: "x mod y = (THE r. \<exists>q. divmod_poly_rel x y q r)"


796 


797 
lemma div_poly_eq:


798 
"divmod_poly_rel x y q r \<Longrightarrow> x div y = q"


799 
unfolding div_poly_def


800 
by (fast elim: divmod_poly_rel_unique_div)


801 


802 
lemma mod_poly_eq:


803 
"divmod_poly_rel x y q r \<Longrightarrow> x mod y = r"


804 
unfolding mod_poly_def


805 
by (fast elim: divmod_poly_rel_unique_mod)


806 


807 
lemma divmod_poly_rel:


808 
"divmod_poly_rel x y (x div y) (x mod y)"


809 
proof 


810 
from divmod_poly_rel_exists


811 
obtain q r where "divmod_poly_rel x y q r" by fast


812 
thus ?thesis


813 
by (simp add: div_poly_eq mod_poly_eq)


814 
qed


815 


816 
instance proof


817 
fix x y :: "'a poly"


818 
show "x div y * y + x mod y = x"


819 
using divmod_poly_rel [of x y]


820 
by (simp add: divmod_poly_rel_def)


821 
next


822 
fix x :: "'a poly"


823 
have "divmod_poly_rel x 0 0 x"


824 
by (rule divmod_poly_rel_by_0)


825 
thus "x div 0 = 0"


826 
by (rule div_poly_eq)


827 
next


828 
fix y :: "'a poly"


829 
have "divmod_poly_rel 0 y 0 0"


830 
by (rule divmod_poly_rel_0)


831 
thus "0 div y = 0"


832 
by (rule div_poly_eq)


833 
next


834 
fix x y z :: "'a poly"


835 
assume "y \<noteq> 0"


836 
hence "divmod_poly_rel (x + z * y) y (z + x div y) (x mod y)"


837 
using divmod_poly_rel [of x y]


838 
by (simp add: divmod_poly_rel_def left_distrib)


839 
thus "(x + z * y) div y = z + x div y"


840 
by (rule div_poly_eq)


841 
qed


842 


843 
end


844 


845 
lemma degree_mod_less:


846 
"y \<noteq> 0 \<Longrightarrow> x mod y = 0 \<or> degree (x mod y) < degree y"


847 
using divmod_poly_rel [of x y]


848 
unfolding divmod_poly_rel_def by simp


849 


850 
lemma div_poly_less: "degree x < degree y \<Longrightarrow> x div y = 0"


851 
proof 


852 
assume "degree x < degree y"


853 
hence "divmod_poly_rel x y 0 x"


854 
by (simp add: divmod_poly_rel_def)


855 
thus "x div y = 0" by (rule div_poly_eq)


856 
qed


857 


858 
lemma mod_poly_less: "degree x < degree y \<Longrightarrow> x mod y = x"


859 
proof 


860 
assume "degree x < degree y"


861 
hence "divmod_poly_rel x y 0 x"


862 
by (simp add: divmod_poly_rel_def)


863 
thus "x mod y = x" by (rule mod_poly_eq)


864 
qed


865 


866 
lemma mod_pCons:


867 
fixes a and x


868 
assumes y: "y \<noteq> 0"


869 
defines b: "b \<equiv> coeff (pCons a (x mod y)) (degree y) / coeff y (degree y)"


870 
shows "(pCons a x) mod y = (pCons a (x mod y)  smult b y)"


871 
unfolding b


872 
apply (rule mod_poly_eq)


873 
apply (rule divmod_poly_rel_pCons [OF divmod_poly_rel y refl])


874 
done


875 


876 


877 
subsection {* Evaluation of polynomials *}


878 


879 
definition


880 
poly :: "'a::{comm_semiring_1,recpower} poly \<Rightarrow> 'a \<Rightarrow> 'a" where


881 
"poly p = (\<lambda>x. \<Sum>n\<le>degree p. coeff p n * x ^ n)"


882 


883 
lemma poly_0 [simp]: "poly 0 x = 0"


884 
unfolding poly_def by simp


885 


886 
lemma poly_pCons [simp]: "poly (pCons a p) x = a + x * poly p x"


887 
unfolding poly_def


888 
by (simp add: degree_pCons_eq_if setsum_atMost_Suc_shift power_Suc


889 
setsum_left_distrib setsum_right_distrib mult_ac


890 
del: setsum_atMost_Suc)


891 


892 
lemma poly_1 [simp]: "poly 1 x = 1"


893 
unfolding one_poly_def by simp


894 


895 
lemma poly_monom: "poly (monom a n) x = a * x ^ n"


896 
by (induct n, simp add: monom_0, simp add: monom_Suc power_Suc mult_ac)


897 


898 
lemma poly_add [simp]: "poly (p + q) x = poly p x + poly q x"


899 
apply (induct p arbitrary: q, simp)


900 
apply (case_tac q, simp, simp add: ring_simps)


901 
done


902 


903 
lemma poly_minus [simp]:


904 
fixes x :: "'a::{comm_ring_1,recpower}"


905 
shows "poly ( p) x =  poly p x"


906 
by (induct p, simp_all)


907 


908 
lemma poly_diff [simp]:


909 
fixes x :: "'a::{comm_ring_1,recpower}"


910 
shows "poly (p  q) x = poly p x  poly q x"


911 
by (simp add: diff_minus)


912 


913 
lemma poly_setsum: "poly (\<Sum>k\<in>A. p k) x = (\<Sum>k\<in>A. poly (p k) x)"


914 
by (cases "finite A", induct set: finite, simp_all)


915 


916 
lemma poly_smult [simp]: "poly (smult a p) x = a * poly p x"


917 
by (induct p, simp, simp add: ring_simps)


918 


919 
lemma poly_mult [simp]: "poly (p * q) x = poly p x * poly q x"


920 
by (induct p, simp_all, simp add: ring_simps)


921 


922 
end
