author  berghofe 
Sun, 10 Jan 2010 18:43:45 +0100  
changeset 34915  7894c7dab132 
parent 31998  2c7a24f74db9 
child 34973  ae634fad947e 
permissions  rwrr 
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 

30738  9 
imports Main 
29451  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 

29455  103 
syntax 
104 
"_poly" :: "args \<Rightarrow> 'a poly" ("[:(_):]") 

105 

106 
translations 

107 
"[:x, xs:]" == "CONST pCons x [:xs:]" 

108 
"[:x:]" == "CONST pCons x 0" 

30155
f65dc19cd5f0
make liststyle polynomial syntax work when show_sorts is on
huffman
parents:
30072
diff
changeset

109 
"[:x:]" <= "CONST pCons x (_constrain 0 t)" 
29455  110 

29451  111 
lemma Poly_nat_case: "f \<in> Poly \<Longrightarrow> nat_case a f \<in> Poly" 
112 
unfolding Poly_def by (auto split: nat.split) 

113 

114 
lemma coeff_pCons: 

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

116 
unfolding pCons_def 

117 
by (simp add: Abs_poly_inverse Poly_nat_case coeff) 

118 

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

120 
by (simp add: coeff_pCons) 

121 

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

123 
by (simp add: coeff_pCons) 

124 

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

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

127 

128 
lemma degree_pCons_eq: 

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

130 
apply (rule order_antisym [OF degree_pCons_le]) 

131 
apply (rule le_degree, simp) 

132 
done 

133 

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

135 
apply (rule order_antisym [OF _ le0]) 

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

137 
done 

138 

29460
ad87e5d1488b
new lemmas about synthetic_div; declare degree_pCons_eq_if [simp]
huffman
parents:
29457
diff
changeset

139 
lemma degree_pCons_eq_if [simp]: 
29451  140 
"degree (pCons a p) = (if p = 0 then 0 else Suc (degree p))" 
141 
apply (cases "p = 0", simp_all) 

142 
apply (rule order_antisym [OF _ le0]) 

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

144 
apply (rule order_antisym [OF degree_pCons_le]) 

145 
apply (rule le_degree, simp) 

146 
done 

147 

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

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

150 

151 
lemma pCons_eq_iff [simp]: 

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

153 
proof (safe) 

154 
assume "pCons a p = pCons b q" 

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

156 
then show "a = b" by simp 

157 
next 

158 
assume "pCons a p = pCons b q" 

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

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

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

162 
qed 

163 

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

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

166 

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

168 
unfolding Poly_def 

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

170 

171 
lemma pCons_cases [cases type: poly]: 

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

173 
proof 

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

175 
by (rule poly_ext) 

176 
(simp add: Abs_poly_inverse Poly_Suc coeff coeff_pCons 

177 
split: nat.split) 

178 
qed 

179 

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

181 
assumes zero: "P 0" 

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

183 
shows "P p" 

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

185 
case (less p) 

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

187 
have "P q" 

188 
proof (cases "q = 0") 

189 
case True 

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

191 
next 

192 
case False 

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

194 
by (rule degree_pCons_eq) 

195 
then have "degree q < degree p" 

196 
using `p = pCons a q` by simp 

197 
then show "P q" 

198 
by (rule less.hyps) 

199 
qed 

200 
then have "P (pCons a q)" 

201 
by (rule pCons) 

202 
then show ?case 

203 
using `p = pCons a q` by simp 

204 
qed 

205 

206 

29454
b0f586f38dd7
add recursion combinator poly_rec; define poly function using poly_rec
huffman
parents:
29453
diff
changeset

207 
subsection {* Recursion combinator for polynomials *} 
b0f586f38dd7
add recursion combinator poly_rec; define poly function using poly_rec
huffman
parents:
29453
diff
changeset

208 

b0f586f38dd7
add recursion combinator poly_rec; define poly function using poly_rec
huffman
parents:
29453
diff
changeset

209 
function 
b0f586f38dd7
add recursion combinator poly_rec; define poly function using poly_rec
huffman
parents:
29453
diff
changeset

210 
poly_rec :: "'b \<Rightarrow> ('a::zero \<Rightarrow> 'a poly \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a poly \<Rightarrow> 'b" 
b0f586f38dd7
add recursion combinator poly_rec; define poly function using poly_rec
huffman
parents:
29453
diff
changeset

211 
where 
29475  212 
poly_rec_pCons_eq_if [simp del, code del]: 
29454
b0f586f38dd7
add recursion combinator poly_rec; define poly function using poly_rec
huffman
parents:
29453
diff
changeset

213 
"poly_rec z f (pCons a p) = f a p (if p = 0 then z else poly_rec z f p)" 
b0f586f38dd7
add recursion combinator poly_rec; define poly function using poly_rec
huffman
parents:
29453
diff
changeset

214 
by (case_tac x, rename_tac q, case_tac q, auto) 
b0f586f38dd7
add recursion combinator poly_rec; define poly function using poly_rec
huffman
parents:
29453
diff
changeset

215 

b0f586f38dd7
add recursion combinator poly_rec; define poly function using poly_rec
huffman
parents:
29453
diff
changeset

216 
termination poly_rec 
b0f586f38dd7
add recursion combinator poly_rec; define poly function using poly_rec
huffman
parents:
29453
diff
changeset

217 
by (relation "measure (degree \<circ> snd \<circ> snd)", simp) 
b0f586f38dd7
add recursion combinator poly_rec; define poly function using poly_rec
huffman
parents:
29453
diff
changeset

218 
(simp add: degree_pCons_eq) 
b0f586f38dd7
add recursion combinator poly_rec; define poly function using poly_rec
huffman
parents:
29453
diff
changeset

219 

b0f586f38dd7
add recursion combinator poly_rec; define poly function using poly_rec
huffman
parents:
29453
diff
changeset

220 
lemma poly_rec_0: 
b0f586f38dd7
add recursion combinator poly_rec; define poly function using poly_rec
huffman
parents:
29453
diff
changeset

221 
"f 0 0 z = z \<Longrightarrow> poly_rec z f 0 = z" 
b0f586f38dd7
add recursion combinator poly_rec; define poly function using poly_rec
huffman
parents:
29453
diff
changeset

222 
using poly_rec_pCons_eq_if [of z f 0 0] by simp 
b0f586f38dd7
add recursion combinator poly_rec; define poly function using poly_rec
huffman
parents:
29453
diff
changeset

223 

b0f586f38dd7
add recursion combinator poly_rec; define poly function using poly_rec
huffman
parents:
29453
diff
changeset

224 
lemma poly_rec_pCons: 
b0f586f38dd7
add recursion combinator poly_rec; define poly function using poly_rec
huffman
parents:
29453
diff
changeset

225 
"f 0 0 z = z \<Longrightarrow> poly_rec z f (pCons a p) = f a p (poly_rec z f p)" 
b0f586f38dd7
add recursion combinator poly_rec; define poly function using poly_rec
huffman
parents:
29453
diff
changeset

226 
by (simp add: poly_rec_pCons_eq_if poly_rec_0) 
b0f586f38dd7
add recursion combinator poly_rec; define poly function using poly_rec
huffman
parents:
29453
diff
changeset

227 

b0f586f38dd7
add recursion combinator poly_rec; define poly function using poly_rec
huffman
parents:
29453
diff
changeset

228 

29451  229 
subsection {* Monomials *} 
230 

231 
definition 

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

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

234 

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

236 
unfolding monom_def 

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

238 

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

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

241 

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

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

244 

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

246 
by (rule poly_ext) simp 

247 

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

249 
by (simp add: expand_poly_eq) 

250 

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

252 
by (simp add: expand_poly_eq) 

253 

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

255 
by (rule degree_le, simp) 

256 

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

258 
apply (rule order_antisym [OF degree_monom_le]) 

259 
apply (rule le_degree, simp) 

260 
done 

261 

262 

263 
subsection {* Addition and subtraction *} 

264 

265 
instantiation poly :: (comm_monoid_add) comm_monoid_add 

266 
begin 

267 

268 
definition 

269 
plus_poly_def [code del]: 

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

271 

272 
lemma Poly_add: 

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

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

275 
unfolding Poly_def 

276 
apply (clarify, rename_tac m n) 

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

278 
done 

279 

280 
lemma coeff_add [simp]: 

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

282 
unfolding plus_poly_def 

283 
by (simp add: Abs_poly_inverse coeff Poly_add) 

284 

285 
instance proof 

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

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

288 
by (simp add: expand_poly_eq add_assoc) 

289 
show "p + q = q + p" 

290 
by (simp add: expand_poly_eq add_commute) 

291 
show "0 + p = p" 

292 
by (simp add: expand_poly_eq) 

293 
qed 

294 

295 
end 

296 

29904  297 
instance poly :: (cancel_comm_monoid_add) cancel_comm_monoid_add 
29540  298 
proof 
299 
fix p q r :: "'a poly" 

300 
assume "p + q = p + r" thus "q = r" 

301 
by (simp add: expand_poly_eq) 

302 
qed 

303 

29451  304 
instantiation poly :: (ab_group_add) ab_group_add 
305 
begin 

306 

307 
definition 

308 
uminus_poly_def [code del]: 

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

310 

311 
definition 

312 
minus_poly_def [code del]: 

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

314 

315 
lemma Poly_minus: 

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

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

318 
unfolding Poly_def by simp 

319 

320 
lemma Poly_diff: 

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

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

323 
unfolding diff_minus by (simp add: Poly_add Poly_minus) 

324 

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

326 
unfolding uminus_poly_def 

327 
by (simp add: Abs_poly_inverse coeff Poly_minus) 

328 

329 
lemma coeff_diff [simp]: 

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

331 
unfolding minus_poly_def 

332 
by (simp add: Abs_poly_inverse coeff Poly_diff) 

333 

334 
instance proof 

335 
fix p q :: "'a poly" 

336 
show " p + p = 0" 

337 
by (simp add: expand_poly_eq) 

338 
show "p  q = p +  q" 

339 
by (simp add: expand_poly_eq diff_minus) 

340 
qed 

341 

342 
end 

343 

344 
lemma add_pCons [simp]: 

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

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

347 

348 
lemma minus_pCons [simp]: 

349 
" pCons a p = pCons ( a) ( p)" 

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

351 

352 
lemma diff_pCons [simp]: 

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

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

355 

29539  356 
lemma degree_add_le_max: "degree (p + q) \<le> max (degree p) (degree q)" 
29451  357 
by (rule degree_le, auto simp add: coeff_eq_0) 
358 

29539  359 
lemma degree_add_le: 
360 
"\<lbrakk>degree p \<le> n; degree q \<le> n\<rbrakk> \<Longrightarrow> degree (p + q) \<le> n" 

361 
by (auto intro: order_trans degree_add_le_max) 

362 

29453  363 
lemma degree_add_less: 
364 
"\<lbrakk>degree p < n; degree q < n\<rbrakk> \<Longrightarrow> degree (p + q) < n" 

29539  365 
by (auto intro: le_less_trans degree_add_le_max) 
29453  366 

29451  367 
lemma degree_add_eq_right: 
368 
"degree p < degree q \<Longrightarrow> degree (p + q) = degree q" 

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

370 
apply (rule order_antisym) 

29539  371 
apply (simp add: degree_add_le) 
29451  372 
apply (rule le_degree) 
373 
apply (simp add: coeff_eq_0) 

374 
done 

375 

376 
lemma degree_add_eq_left: 

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

378 
using degree_add_eq_right [of q p] 

379 
by (simp add: add_commute) 

380 

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

382 
unfolding degree_def by simp 

383 

29539  384 
lemma degree_diff_le_max: "degree (p  q) \<le> max (degree p) (degree q)" 
29451  385 
using degree_add_le [where p=p and q="q"] 
386 
by (simp add: diff_minus) 

387 

29539  388 
lemma degree_diff_le: 
389 
"\<lbrakk>degree p \<le> n; degree q \<le> n\<rbrakk> \<Longrightarrow> degree (p  q) \<le> n" 

390 
by (simp add: diff_minus degree_add_le) 

391 

29453  392 
lemma degree_diff_less: 
393 
"\<lbrakk>degree p < n; degree q < n\<rbrakk> \<Longrightarrow> degree (p  q) < n" 

29539  394 
by (simp add: diff_minus degree_add_less) 
29453  395 

29451  396 
lemma add_monom: "monom a n + monom b n = monom (a + b) n" 
397 
by (rule poly_ext) simp 

398 

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

400 
by (rule poly_ext) simp 

401 

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

403 
by (rule poly_ext) simp 

404 

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

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

407 

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

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

410 

411 

412 
subsection {* Multiplication by a constant *} 

413 

414 
definition 

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

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

417 

418 
lemma Poly_smult: 

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

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

421 
unfolding Poly_def 

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

423 

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

425 
unfolding smult_def 

426 
by (simp add: Abs_poly_inverse Poly_smult coeff) 

427 

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

429 
by (rule degree_le, simp add: coeff_eq_0) 

430 

29472  431 
lemma smult_smult [simp]: "smult a (smult b p) = smult (a * b) p" 
29451  432 
by (rule poly_ext, simp add: mult_assoc) 
433 

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

435 
by (rule poly_ext, simp) 

436 

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

438 
by (rule poly_ext, simp) 

439 

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

441 
by (rule poly_ext, simp) 

442 

443 
lemma smult_add_right: 

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

29667  445 
by (rule poly_ext, simp add: algebra_simps) 
29451  446 

447 
lemma smult_add_left: 

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

29667  449 
by (rule poly_ext, simp add: algebra_simps) 
29451  450 

29457  451 
lemma smult_minus_right [simp]: 
29451  452 
"smult (a::'a::comm_ring) ( p) =  smult a p" 
453 
by (rule poly_ext, simp) 

454 

29457  455 
lemma smult_minus_left [simp]: 
29451  456 
"smult ( a::'a::comm_ring) p =  smult a p" 
457 
by (rule poly_ext, simp) 

458 

459 
lemma smult_diff_right: 

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

29667  461 
by (rule poly_ext, simp add: algebra_simps) 
29451  462 

463 
lemma smult_diff_left: 

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

29667  465 
by (rule poly_ext, simp add: algebra_simps) 
29451  466 

29472  467 
lemmas smult_distribs = 
468 
smult_add_left smult_add_right 

469 
smult_diff_left smult_diff_right 

470 

29451  471 
lemma smult_pCons [simp]: 
472 
"smult a (pCons b p) = pCons (a * b) (smult a p)" 

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

474 

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

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

477 

29659  478 
lemma degree_smult_eq [simp]: 
479 
fixes a :: "'a::idom" 

480 
shows "degree (smult a p) = (if a = 0 then 0 else degree p)" 

481 
by (cases "a = 0", simp, simp add: degree_def) 

482 

483 
lemma smult_eq_0_iff [simp]: 

484 
fixes a :: "'a::idom" 

485 
shows "smult a p = 0 \<longleftrightarrow> a = 0 \<or> p = 0" 

486 
by (simp add: expand_poly_eq) 

487 

29451  488 

489 
subsection {* Multiplication of polynomials *} 

490 

29474  491 
text {* TODO: move to SetInterval.thy *} 
29451  492 
lemma setsum_atMost_Suc_shift: 
493 
fixes f :: "nat \<Rightarrow> 'a::comm_monoid_add" 

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

495 
proof (induct n) 

496 
case 0 show ?case by simp 

497 
next 

498 
case (Suc n) note IH = this 

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

500 
by (rule setsum_atMost_Suc) 

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

502 
by (rule IH) 

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

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

505 
by (rule add_assoc) 

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

507 
by (rule setsum_atMost_Suc [symmetric]) 

508 
finally show ?case . 

509 
qed 

510 

511 
instantiation poly :: (comm_semiring_0) comm_semiring_0 

512 
begin 

513 

514 
definition 

29475  515 
times_poly_def [code del]: 
29474  516 
"p * q = poly_rec 0 (\<lambda>a p pq. smult a q + pCons 0 pq) p" 
517 

518 
lemma mult_poly_0_left: "(0::'a poly) * q = 0" 

519 
unfolding times_poly_def by (simp add: poly_rec_0) 

520 

521 
lemma mult_pCons_left [simp]: 

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

523 
unfolding times_poly_def by (simp add: poly_rec_pCons) 

524 

525 
lemma mult_poly_0_right: "p * (0::'a poly) = 0" 

526 
by (induct p, simp add: mult_poly_0_left, simp) 

29451  527 

29474  528 
lemma mult_pCons_right [simp]: 
529 
"p * pCons a q = smult a p + pCons 0 (p * q)" 

29667  530 
by (induct p, simp add: mult_poly_0_left, simp add: algebra_simps) 
29474  531 

532 
lemmas mult_poly_0 = mult_poly_0_left mult_poly_0_right 

533 

534 
lemma mult_smult_left [simp]: "smult a p * q = smult a (p * q)" 

535 
by (induct p, simp add: mult_poly_0, simp add: smult_add_right) 

536 

537 
lemma mult_smult_right [simp]: "p * smult a q = smult a (p * q)" 

538 
by (induct q, simp add: mult_poly_0, simp add: smult_add_right) 

539 

540 
lemma mult_poly_add_left: 

541 
fixes p q r :: "'a poly" 

542 
shows "(p + q) * r = p * r + q * r" 

543 
by (induct r, simp add: mult_poly_0, 

29667  544 
simp add: smult_distribs algebra_simps) 
29451  545 

546 
instance proof 

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

548 
show 0: "0 * p = 0" 

29474  549 
by (rule mult_poly_0_left) 
29451  550 
show "p * 0 = 0" 
29474  551 
by (rule mult_poly_0_right) 
29451  552 
show "(p + q) * r = p * r + q * r" 
29474  553 
by (rule mult_poly_add_left) 
29451  554 
show "(p * q) * r = p * (q * r)" 
29474  555 
by (induct p, simp add: mult_poly_0, simp add: mult_poly_add_left) 
29451  556 
show "p * q = q * p" 
29474  557 
by (induct p, simp add: mult_poly_0, simp) 
29451  558 
qed 
559 

560 
end 

561 

29540  562 
instance poly :: (comm_semiring_0_cancel) comm_semiring_0_cancel .. 
563 

29474  564 
lemma coeff_mult: 
565 
"coeff (p * q) n = (\<Sum>i\<le>n. coeff p i * coeff q (ni))" 

566 
proof (induct p arbitrary: n) 

567 
case 0 show ?case by simp 

568 
next 

569 
case (pCons a p n) thus ?case 

570 
by (cases n, simp, simp add: setsum_atMost_Suc_shift 

571 
del: setsum_atMost_Suc) 

572 
qed 

29451  573 

29474  574 
lemma degree_mult_le: "degree (p * q) \<le> degree p + degree q" 
575 
apply (rule degree_le) 

576 
apply (induct p) 

577 
apply simp 

578 
apply (simp add: coeff_eq_0 coeff_pCons split: nat.split) 

29451  579 
done 
580 

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

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

583 

584 

585 
subsection {* The unit polynomial and exponentiation *} 

586 

587 
instantiation poly :: (comm_semiring_1) comm_semiring_1 

588 
begin 

589 

590 
definition 

591 
one_poly_def: 

592 
"1 = pCons 1 0" 

593 

594 
instance proof 

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

596 
unfolding one_poly_def 

597 
by simp 

598 
next 

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

600 
unfolding one_poly_def by simp 

601 
qed 

602 

603 
end 

604 

29540  605 
instance poly :: (comm_semiring_1_cancel) comm_semiring_1_cancel .. 
606 

29451  607 
lemma coeff_1 [simp]: "coeff 1 n = (if n = 0 then 1 else 0)" 
608 
unfolding one_poly_def 

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

610 

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

612 
unfolding one_poly_def 

613 
by (rule degree_pCons_0) 

614 

29979  615 
text {* Lemmas about divisibility *} 
616 

617 
lemma dvd_smult: "p dvd q \<Longrightarrow> p dvd smult a q" 

618 
proof  

619 
assume "p dvd q" 

620 
then obtain k where "q = p * k" .. 

621 
then have "smult a q = p * smult a k" by simp 

622 
then show "p dvd smult a q" .. 

623 
qed 

624 

625 
lemma dvd_smult_cancel: 

626 
fixes a :: "'a::field" 

627 
shows "p dvd smult a q \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> p dvd q" 

628 
by (drule dvd_smult [where a="inverse a"]) simp 

629 

630 
lemma dvd_smult_iff: 

631 
fixes a :: "'a::field" 

632 
shows "a \<noteq> 0 \<Longrightarrow> p dvd smult a q \<longleftrightarrow> p dvd q" 

633 
by (safe elim!: dvd_smult dvd_smult_cancel) 

634 

31663  635 
lemma smult_dvd_cancel: 
636 
"smult a p dvd q \<Longrightarrow> p dvd q" 

637 
proof  

638 
assume "smult a p dvd q" 

639 
then obtain k where "q = smult a p * k" .. 

640 
then have "q = p * smult a k" by simp 

641 
then show "p dvd q" .. 

642 
qed 

643 

644 
lemma smult_dvd: 

645 
fixes a :: "'a::field" 

646 
shows "p dvd q \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> smult a p dvd q" 

647 
by (rule smult_dvd_cancel [where a="inverse a"]) simp 

648 

649 
lemma smult_dvd_iff: 

650 
fixes a :: "'a::field" 

651 
shows "smult a p dvd q \<longleftrightarrow> (if a = 0 then q = 0 else p dvd q)" 

652 
by (auto elim: smult_dvd smult_dvd_cancel) 

653 

29979  654 
lemma degree_power_le: "degree (p ^ n) \<le> degree p * n" 
655 
by (induct n, simp, auto intro: order_trans degree_mult_le) 

656 

29451  657 
instance poly :: (comm_ring) comm_ring .. 
658 

659 
instance poly :: (comm_ring_1) comm_ring_1 .. 

660 

661 
instantiation poly :: (comm_ring_1) number_ring 

662 
begin 

663 

664 
definition 

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

666 

667 
instance 

668 
by default (rule number_of_poly_def) 

669 

670 
end 

671 

672 

673 
subsection {* Polynomials form an integral domain *} 

674 

675 
lemma coeff_mult_degree_sum: 

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

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

29471  678 
by (induct p, simp, simp add: coeff_eq_0) 
29451  679 

680 
instance poly :: (idom) idom 

681 
proof 

682 
fix p q :: "'a poly" 

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

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

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

686 
by (rule coeff_mult_degree_sum) 

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

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

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

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

691 
qed 

692 

693 
lemma degree_mult_eq: 

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

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

696 
apply (rule order_antisym [OF degree_mult_le le_degree]) 

697 
apply (simp add: coeff_mult_degree_sum) 

698 
done 

699 

700 
lemma dvd_imp_degree_le: 

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

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

703 
by (erule dvdE, simp add: degree_mult_eq) 

704 

705 

29878  706 
subsection {* Polynomials form an ordered integral domain *} 
707 

708 
definition 

709 
pos_poly :: "'a::ordered_idom poly \<Rightarrow> bool" 

710 
where 

711 
"pos_poly p \<longleftrightarrow> 0 < coeff p (degree p)" 

712 

713 
lemma pos_poly_pCons: 

714 
"pos_poly (pCons a p) \<longleftrightarrow> pos_poly p \<or> (p = 0 \<and> 0 < a)" 

715 
unfolding pos_poly_def by simp 

716 

717 
lemma not_pos_poly_0 [simp]: "\<not> pos_poly 0" 

718 
unfolding pos_poly_def by simp 

719 

720 
lemma pos_poly_add: "\<lbrakk>pos_poly p; pos_poly q\<rbrakk> \<Longrightarrow> pos_poly (p + q)" 

721 
apply (induct p arbitrary: q, simp) 

722 
apply (case_tac q, force simp add: pos_poly_pCons add_pos_pos) 

723 
done 

724 

725 
lemma pos_poly_mult: "\<lbrakk>pos_poly p; pos_poly q\<rbrakk> \<Longrightarrow> pos_poly (p * q)" 

726 
unfolding pos_poly_def 

727 
apply (subgoal_tac "p \<noteq> 0 \<and> q \<noteq> 0") 

728 
apply (simp add: degree_mult_eq coeff_mult_degree_sum mult_pos_pos) 

729 
apply auto 

730 
done 

731 

732 
lemma pos_poly_total: "p = 0 \<or> pos_poly p \<or> pos_poly ( p)" 

733 
by (induct p) (auto simp add: pos_poly_pCons) 

734 

735 
instantiation poly :: (ordered_idom) ordered_idom 

736 
begin 

737 

738 
definition 

739 
[code del]: 

740 
"x < y \<longleftrightarrow> pos_poly (y  x)" 

741 

742 
definition 

743 
[code del]: 

744 
"x \<le> y \<longleftrightarrow> x = y \<or> pos_poly (y  x)" 

745 

746 
definition 

747 
[code del]: 

748 
"abs (x::'a poly) = (if x < 0 then  x else x)" 

749 

750 
definition 

751 
[code del]: 

752 
"sgn (x::'a poly) = (if x = 0 then 0 else if 0 < x then 1 else  1)" 

753 

754 
instance proof 

755 
fix x y :: "'a poly" 

756 
show "x < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x" 

757 
unfolding less_eq_poly_def less_poly_def 

758 
apply safe 

759 
apply simp 

760 
apply (drule (1) pos_poly_add) 

761 
apply simp 

762 
done 

763 
next 

764 
fix x :: "'a poly" show "x \<le> x" 

765 
unfolding less_eq_poly_def by simp 

766 
next 

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

768 
assume "x \<le> y" and "y \<le> z" thus "x \<le> z" 

769 
unfolding less_eq_poly_def 

770 
apply safe 

771 
apply (drule (1) pos_poly_add) 

772 
apply (simp add: algebra_simps) 

773 
done 

774 
next 

775 
fix x y :: "'a poly" 

776 
assume "x \<le> y" and "y \<le> x" thus "x = y" 

777 
unfolding less_eq_poly_def 

778 
apply safe 

779 
apply (drule (1) pos_poly_add) 

780 
apply simp 

781 
done 

782 
next 

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

784 
assume "x \<le> y" thus "z + x \<le> z + y" 

785 
unfolding less_eq_poly_def 

786 
apply safe 

787 
apply (simp add: algebra_simps) 

788 
done 

789 
next 

790 
fix x y :: "'a poly" 

791 
show "x \<le> y \<or> y \<le> x" 

792 
unfolding less_eq_poly_def 

793 
using pos_poly_total [of "x  y"] 

794 
by auto 

795 
next 

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

797 
assume "x < y" and "0 < z" 

798 
thus "z * x < z * y" 

799 
unfolding less_poly_def 

800 
by (simp add: right_diff_distrib [symmetric] pos_poly_mult) 

801 
next 

802 
fix x :: "'a poly" 

803 
show "\<bar>x\<bar> = (if x < 0 then  x else x)" 

804 
by (rule abs_poly_def) 

805 
next 

806 
fix x :: "'a poly" 

807 
show "sgn x = (if x = 0 then 0 else if 0 < x then 1 else  1)" 

808 
by (rule sgn_poly_def) 

809 
qed 

810 

811 
end 

812 

813 
text {* TODO: Simplification rules for comparisons *} 

814 

815 

29451  816 
subsection {* Long division of polynomials *} 
817 

818 
definition 

29537  819 
pdivmod_rel :: "'a::field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<Rightarrow> bool" 
29451  820 
where 
29475  821 
[code del]: 
29537  822 
"pdivmod_rel x y q r \<longleftrightarrow> 
29451  823 
x = q * y + r \<and> (if y = 0 then q = 0 else r = 0 \<or> degree r < degree y)" 
824 

29537  825 
lemma pdivmod_rel_0: 
826 
"pdivmod_rel 0 y 0 0" 

827 
unfolding pdivmod_rel_def by simp 

29451  828 

29537  829 
lemma pdivmod_rel_by_0: 
830 
"pdivmod_rel x 0 0 x" 

831 
unfolding pdivmod_rel_def by simp 

29451  832 

833 
lemma eq_zero_or_degree_less: 

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

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

836 
proof (cases n) 

837 
case 0 

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

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

840 
then have "p = 0" by simp 

841 
then show ?thesis .. 

842 
next 

843 
case (Suc m) 

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

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

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

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

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

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

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

851 
by (rule degree_le) 

852 
then have "degree p < n" 

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

854 
then show ?thesis .. 

855 
qed 

856 

29537  857 
lemma pdivmod_rel_pCons: 
858 
assumes rel: "pdivmod_rel x y q r" 

29451  859 
assumes y: "y \<noteq> 0" 
860 
assumes b: "b = coeff (pCons a r) (degree y) / coeff y (degree y)" 

29537  861 
shows "pdivmod_rel (pCons a x) y (pCons b q) (pCons a r  smult b y)" 
862 
(is "pdivmod_rel ?x y ?q ?r") 

29451  863 
proof  
864 
have x: "x = q * y + r" and r: "r = 0 \<or> degree r < degree y" 

29537  865 
using assms unfolding pdivmod_rel_def by simp_all 
29451  866 

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

868 
using b x by simp 

869 

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

871 
proof (rule eq_zero_or_degree_less) 

29539  872 
show "degree ?r \<le> degree y" 
873 
proof (rule degree_diff_le) 

29451  874 
show "degree (pCons a r) \<le> degree y" 
29460
ad87e5d1488b
new lemmas about synthetic_div; declare degree_pCons_eq_if [simp]
huffman
parents:
29457
diff
changeset

875 
using r by auto 
29451  876 
show "degree (smult b y) \<le> degree y" 
877 
by (rule degree_smult_le) 

878 
qed 

879 
next 

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

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

882 
qed 

883 

884 
from 1 2 show ?thesis 

29537  885 
unfolding pdivmod_rel_def 
29451  886 
using `y \<noteq> 0` by simp 
887 
qed 

888 

29537  889 
lemma pdivmod_rel_exists: "\<exists>q r. pdivmod_rel x y q r" 
29451  890 
apply (cases "y = 0") 
29537  891 
apply (fast intro!: pdivmod_rel_by_0) 
29451  892 
apply (induct x) 
29537  893 
apply (fast intro!: pdivmod_rel_0) 
894 
apply (fast intro!: pdivmod_rel_pCons) 

29451  895 
done 
896 

29537  897 
lemma pdivmod_rel_unique: 
898 
assumes 1: "pdivmod_rel x y q1 r1" 

899 
assumes 2: "pdivmod_rel x y q2 r2" 

29451  900 
shows "q1 = q2 \<and> r1 = r2" 
901 
proof (cases "y = 0") 

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

29537  903 
by (simp add: pdivmod_rel_def) 
29451  904 
next 
905 
assume [simp]: "y \<noteq> 0" 

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

29537  907 
unfolding pdivmod_rel_def by simp_all 
29451  908 
from 2 have q2: "x = q2 * y + r2" and r2: "r2 = 0 \<or> degree r2 < degree y" 
29537  909 
unfolding pdivmod_rel_def by simp_all 
29451  910 
from q1 q2 have q3: "(q1  q2) * y = r2  r1" 
29667  911 
by (simp add: algebra_simps) 
29451  912 
from r1 r2 have r3: "(r2  r1) = 0 \<or> degree (r2  r1) < degree y" 
29453  913 
by (auto intro: degree_diff_less) 
29451  914 

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

916 
proof (rule ccontr) 

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

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

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

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

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

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

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

924 
using q3 by simp 

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

926 
then show "False" by simp 

927 
qed 

928 
qed 

929 

29660  930 
lemma pdivmod_rel_0_iff: "pdivmod_rel 0 y q r \<longleftrightarrow> q = 0 \<and> r = 0" 
931 
by (auto dest: pdivmod_rel_unique intro: pdivmod_rel_0) 

932 

933 
lemma pdivmod_rel_by_0_iff: "pdivmod_rel x 0 q r \<longleftrightarrow> q = 0 \<and> r = x" 

934 
by (auto dest: pdivmod_rel_unique intro: pdivmod_rel_by_0) 

935 

29537  936 
lemmas pdivmod_rel_unique_div = 
937 
pdivmod_rel_unique [THEN conjunct1, standard] 

29451  938 

29537  939 
lemmas pdivmod_rel_unique_mod = 
940 
pdivmod_rel_unique [THEN conjunct2, standard] 

29451  941 

942 
instantiation poly :: (field) ring_div 

943 
begin 

944 

945 
definition div_poly where 

29537  946 
[code del]: "x div y = (THE q. \<exists>r. pdivmod_rel x y q r)" 
29451  947 

948 
definition mod_poly where 

29537  949 
[code del]: "x mod y = (THE r. \<exists>q. pdivmod_rel x y q r)" 
29451  950 

951 
lemma div_poly_eq: 

29537  952 
"pdivmod_rel x y q r \<Longrightarrow> x div y = q" 
29451  953 
unfolding div_poly_def 
29537  954 
by (fast elim: pdivmod_rel_unique_div) 
29451  955 

956 
lemma mod_poly_eq: 

29537  957 
"pdivmod_rel x y q r \<Longrightarrow> x mod y = r" 
29451  958 
unfolding mod_poly_def 
29537  959 
by (fast elim: pdivmod_rel_unique_mod) 
29451  960 

29537  961 
lemma pdivmod_rel: 
962 
"pdivmod_rel x y (x div y) (x mod y)" 

29451  963 
proof  
29537  964 
from pdivmod_rel_exists 
965 
obtain q r where "pdivmod_rel x y q r" by fast 

29451  966 
thus ?thesis 
967 
by (simp add: div_poly_eq mod_poly_eq) 

968 
qed 

969 

970 
instance proof 

971 
fix x y :: "'a poly" 

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

29537  973 
using pdivmod_rel [of x y] 
974 
by (simp add: pdivmod_rel_def) 

29451  975 
next 
976 
fix x :: "'a poly" 

29537  977 
have "pdivmod_rel x 0 0 x" 
978 
by (rule pdivmod_rel_by_0) 

29451  979 
thus "x div 0 = 0" 
980 
by (rule div_poly_eq) 

981 
next 

982 
fix y :: "'a poly" 

29537  983 
have "pdivmod_rel 0 y 0 0" 
984 
by (rule pdivmod_rel_0) 

29451  985 
thus "0 div y = 0" 
986 
by (rule div_poly_eq) 

987 
next 

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

989 
assume "y \<noteq> 0" 

29537  990 
hence "pdivmod_rel (x + z * y) y (z + x div y) (x mod y)" 
991 
using pdivmod_rel [of x y] 

992 
by (simp add: pdivmod_rel_def left_distrib) 

29451  993 
thus "(x + z * y) div y = z + x div y" 
994 
by (rule div_poly_eq) 

30930  995 
next 
996 
fix x y z :: "'a poly" 

997 
assume "x \<noteq> 0" 

998 
show "(x * y) div (x * z) = y div z" 

999 
proof (cases "y \<noteq> 0 \<and> z \<noteq> 0") 

1000 
have "\<And>x::'a poly. pdivmod_rel x 0 0 x" 

1001 
by (rule pdivmod_rel_by_0) 

1002 
then have [simp]: "\<And>x::'a poly. x div 0 = 0" 

1003 
by (rule div_poly_eq) 

1004 
have "\<And>x::'a poly. pdivmod_rel 0 x 0 0" 

1005 
by (rule pdivmod_rel_0) 

1006 
then have [simp]: "\<And>x::'a poly. 0 div x = 0" 

1007 
by (rule div_poly_eq) 

1008 
case False then show ?thesis by auto 

1009 
next 

1010 
case True then have "y \<noteq> 0" and "z \<noteq> 0" by auto 

1011 
with `x \<noteq> 0` 

1012 
have "\<And>q r. pdivmod_rel y z q r \<Longrightarrow> pdivmod_rel (x * y) (x * z) q (x * r)" 

1013 
by (auto simp add: pdivmod_rel_def algebra_simps) 

1014 
(rule classical, simp add: degree_mult_eq) 

1015 
moreover from pdivmod_rel have "pdivmod_rel y z (y div z) (y mod z)" . 

1016 
ultimately have "pdivmod_rel (x * y) (x * z) (y div z) (x * (y mod z))" . 

1017 
then show ?thesis by (simp add: div_poly_eq) 

1018 
qed 

29451  1019 
qed 
1020 

1021 
end 

1022 

1023 
lemma degree_mod_less: 

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

29537  1025 
using pdivmod_rel [of x y] 
1026 
unfolding pdivmod_rel_def by simp 

29451  1027 

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

1029 
proof  

1030 
assume "degree x < degree y" 

29537  1031 
hence "pdivmod_rel x y 0 x" 
1032 
by (simp add: pdivmod_rel_def) 

29451  1033 
thus "x div y = 0" by (rule div_poly_eq) 
1034 
qed 

1035 

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

1037 
proof  

1038 
assume "degree x < degree y" 

29537  1039 
hence "pdivmod_rel x y 0 x" 
1040 
by (simp add: pdivmod_rel_def) 

29451  1041 
thus "x mod y = x" by (rule mod_poly_eq) 
1042 
qed 

1043 

29659  1044 
lemma pdivmod_rel_smult_left: 
1045 
"pdivmod_rel x y q r 

1046 
\<Longrightarrow> pdivmod_rel (smult a x) y (smult a q) (smult a r)" 

1047 
unfolding pdivmod_rel_def by (simp add: smult_add_right) 

1048 

1049 
lemma div_smult_left: "(smult a x) div y = smult a (x div y)" 

1050 
by (rule div_poly_eq, rule pdivmod_rel_smult_left, rule pdivmod_rel) 

1051 

1052 
lemma mod_smult_left: "(smult a x) mod y = smult a (x mod y)" 

1053 
by (rule mod_poly_eq, rule pdivmod_rel_smult_left, rule pdivmod_rel) 

1054 

30072  1055 
lemma poly_div_minus_left [simp]: 
1056 
fixes x y :: "'a::field poly" 

1057 
shows "( x) div y =  (x div y)" 

1058 
using div_smult_left [of " 1::'a"] by simp 

1059 

1060 
lemma poly_mod_minus_left [simp]: 

1061 
fixes x y :: "'a::field poly" 

1062 
shows "( x) mod y =  (x mod y)" 

1063 
using mod_smult_left [of " 1::'a"] by simp 

1064 

29659  1065 
lemma pdivmod_rel_smult_right: 
1066 
"\<lbrakk>a \<noteq> 0; pdivmod_rel x y q r\<rbrakk> 

1067 
\<Longrightarrow> pdivmod_rel x (smult a y) (smult (inverse a) q) r" 

1068 
unfolding pdivmod_rel_def by simp 

1069 

1070 
lemma div_smult_right: 

1071 
"a \<noteq> 0 \<Longrightarrow> x div (smult a y) = smult (inverse a) (x div y)" 

1072 
by (rule div_poly_eq, erule pdivmod_rel_smult_right, rule pdivmod_rel) 

1073 

1074 
lemma mod_smult_right: "a \<noteq> 0 \<Longrightarrow> x mod (smult a y) = x mod y" 

1075 
by (rule mod_poly_eq, erule pdivmod_rel_smult_right, rule pdivmod_rel) 

1076 

30072  1077 
lemma poly_div_minus_right [simp]: 
1078 
fixes x y :: "'a::field poly" 

1079 
shows "x div ( y) =  (x div y)" 

1080 
using div_smult_right [of " 1::'a"] 

1081 
by (simp add: nonzero_inverse_minus_eq) 

1082 

1083 
lemma poly_mod_minus_right [simp]: 

1084 
fixes x y :: "'a::field poly" 

1085 
shows "x mod ( y) = x mod y" 

1086 
using mod_smult_right [of " 1::'a"] by simp 

1087 

29660  1088 
lemma pdivmod_rel_mult: 
1089 
"\<lbrakk>pdivmod_rel x y q r; pdivmod_rel q z q' r'\<rbrakk> 

1090 
\<Longrightarrow> pdivmod_rel x (y * z) q' (y * r' + r)" 

1091 
apply (cases "z = 0", simp add: pdivmod_rel_def) 

1092 
apply (cases "y = 0", simp add: pdivmod_rel_by_0_iff pdivmod_rel_0_iff) 

1093 
apply (cases "r = 0") 

1094 
apply (cases "r' = 0") 

1095 
apply (simp add: pdivmod_rel_def) 

1096 
apply (simp add: pdivmod_rel_def ring_simps degree_mult_eq) 

1097 
apply (cases "r' = 0") 

1098 
apply (simp add: pdivmod_rel_def degree_mult_eq) 

1099 
apply (simp add: pdivmod_rel_def ring_simps) 

1100 
apply (simp add: degree_mult_eq degree_add_less) 

1101 
done 

1102 

1103 
lemma poly_div_mult_right: 

1104 
fixes x y z :: "'a::field poly" 

1105 
shows "x div (y * z) = (x div y) div z" 

1106 
by (rule div_poly_eq, rule pdivmod_rel_mult, (rule pdivmod_rel)+) 

1107 

1108 
lemma poly_mod_mult_right: 

1109 
fixes x y z :: "'a::field poly" 

1110 
shows "x mod (y * z) = y * (x div y mod z) + x mod y" 

1111 
by (rule mod_poly_eq, rule pdivmod_rel_mult, (rule pdivmod_rel)+) 

1112 

29451  1113 
lemma mod_pCons: 
1114 
fixes a and x 

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

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

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

1118 
unfolding b 

1119 
apply (rule mod_poly_eq) 

29537  1120 
apply (rule pdivmod_rel_pCons [OF pdivmod_rel y refl]) 
29451  1121 
done 
1122 

1123 

31663  1124 
subsection {* GCD of polynomials *} 
1125 

1126 
function 

1127 
poly_gcd :: "'a::field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly" where 

1128 
"poly_gcd x 0 = smult (inverse (coeff x (degree x))) x" 

1129 
 "y \<noteq> 0 \<Longrightarrow> poly_gcd x y = poly_gcd y (x mod y)" 

1130 
by auto 

1131 

1132 
termination poly_gcd 

1133 
by (relation "measure (\<lambda>(x, y). if y = 0 then 0 else Suc (degree y))") 

1134 
(auto dest: degree_mod_less) 

1135 

1136 
declare poly_gcd.simps [simp del, code del] 

1137 

1138 
lemma poly_gcd_dvd1 [iff]: "poly_gcd x y dvd x" 

1139 
and poly_gcd_dvd2 [iff]: "poly_gcd x y dvd y" 

1140 
apply (induct x y rule: poly_gcd.induct) 

1141 
apply (simp_all add: poly_gcd.simps) 

1142 
apply (fastsimp simp add: smult_dvd_iff dest: inverse_zero_imp_zero) 

1143 
apply (blast dest: dvd_mod_imp_dvd) 

1144 
done 

1145 

1146 
lemma poly_gcd_greatest: "k dvd x \<Longrightarrow> k dvd y \<Longrightarrow> k dvd poly_gcd x y" 

1147 
by (induct x y rule: poly_gcd.induct) 

1148 
(simp_all add: poly_gcd.simps dvd_mod dvd_smult) 

1149 

1150 
lemma dvd_poly_gcd_iff [iff]: 

1151 
"k dvd poly_gcd x y \<longleftrightarrow> k dvd x \<and> k dvd y" 

1152 
by (blast intro!: poly_gcd_greatest intro: dvd_trans) 

1153 

1154 
lemma poly_gcd_monic: 

1155 
"coeff (poly_gcd x y) (degree (poly_gcd x y)) = 

1156 
(if x = 0 \<and> y = 0 then 0 else 1)" 

1157 
by (induct x y rule: poly_gcd.induct) 

1158 
(simp_all add: poly_gcd.simps nonzero_imp_inverse_nonzero) 

1159 

1160 
lemma poly_gcd_zero_iff [simp]: 

1161 
"poly_gcd x y = 0 \<longleftrightarrow> x = 0 \<and> y = 0" 

1162 
by (simp only: dvd_0_left_iff [symmetric] dvd_poly_gcd_iff) 

1163 

1164 
lemma poly_gcd_0_0 [simp]: "poly_gcd 0 0 = 0" 

1165 
by simp 

1166 

1167 
lemma poly_dvd_antisym: 

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

1169 
assumes coeff: "coeff p (degree p) = coeff q (degree q)" 

1170 
assumes dvd1: "p dvd q" and dvd2: "q dvd p" shows "p = q" 

1171 
proof (cases "p = 0") 

1172 
case True with coeff show "p = q" by simp 

1173 
next 

1174 
case False with coeff have "q \<noteq> 0" by auto 

1175 
have degree: "degree p = degree q" 

1176 
using `p dvd q` `q dvd p` `p \<noteq> 0` `q \<noteq> 0` 

1177 
by (intro order_antisym dvd_imp_degree_le) 

1178 

1179 
from `p dvd q` obtain a where a: "q = p * a" .. 

1180 
with `q \<noteq> 0` have "a \<noteq> 0" by auto 

1181 
with degree a `p \<noteq> 0` have "degree a = 0" 

1182 
by (simp add: degree_mult_eq) 

1183 
with coeff a show "p = q" 

1184 
by (cases a, auto split: if_splits) 

1185 
qed 

1186 

1187 
lemma poly_gcd_unique: 

1188 
assumes dvd1: "d dvd x" and dvd2: "d dvd y" 

1189 
and greatest: "\<And>k. k dvd x \<Longrightarrow> k dvd y \<Longrightarrow> k dvd d" 

1190 
and monic: "coeff d (degree d) = (if x = 0 \<and> y = 0 then 0 else 1)" 

1191 
shows "poly_gcd x y = d" 

1192 
proof  

1193 
have "coeff (poly_gcd x y) (degree (poly_gcd x y)) = coeff d (degree d)" 

1194 
by (simp_all add: poly_gcd_monic monic) 

1195 
moreover have "poly_gcd x y dvd d" 

1196 
using poly_gcd_dvd1 poly_gcd_dvd2 by (rule greatest) 

1197 
moreover have "d dvd poly_gcd x y" 

1198 
using dvd1 dvd2 by (rule poly_gcd_greatest) 

1199 
ultimately show ?thesis 

1200 
by (rule poly_dvd_antisym) 

1201 
qed 

1202 

1203 
lemma poly_gcd_commute: "poly_gcd x y = poly_gcd y x" 

1204 
by (rule poly_gcd_unique) (simp_all add: poly_gcd_monic) 

1205 

1206 
lemma poly_gcd_assoc: "poly_gcd (poly_gcd x y) z = poly_gcd x (poly_gcd y z)" 

1207 
by (rule poly_gcd_unique) (auto intro: dvd_trans simp add: poly_gcd_monic) 

1208 

1209 
lemmas poly_gcd_left_commute = 

1210 
mk_left_commute [where f=poly_gcd, OF poly_gcd_assoc poly_gcd_commute] 

1211 

1212 
lemmas poly_gcd_ac = poly_gcd_assoc poly_gcd_commute poly_gcd_left_commute 

1213 

1214 
lemma poly_gcd_1_left [simp]: "poly_gcd 1 y = 1" 

1215 
by (rule poly_gcd_unique) simp_all 

1216 

1217 
lemma poly_gcd_1_right [simp]: "poly_gcd x 1 = 1" 

1218 
by (rule poly_gcd_unique) simp_all 

1219 

1220 
lemma poly_gcd_minus_left [simp]: "poly_gcd ( x) y = poly_gcd x y" 

1221 
by (rule poly_gcd_unique) (simp_all add: poly_gcd_monic) 

1222 

1223 
lemma poly_gcd_minus_right [simp]: "poly_gcd x ( y) = poly_gcd x y" 

1224 
by (rule poly_gcd_unique) (simp_all add: poly_gcd_monic) 

1225 

1226 

29451  1227 
subsection {* Evaluation of polynomials *} 
1228 

1229 
definition 

29454
b0f586f38dd7
add recursion combinator poly_rec; define poly function using poly_rec
huffman
parents:
29453
diff
changeset

1230 
poly :: "'a::comm_semiring_0 poly \<Rightarrow> 'a \<Rightarrow> 'a" where 
b0f586f38dd7
add recursion combinator poly_rec; define poly function using poly_rec
huffman
parents:
29453
diff
changeset

1231 
"poly = poly_rec (\<lambda>x. 0) (\<lambda>a p f x. a + x * f x)" 
29451  1232 

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

29454
b0f586f38dd7
add recursion combinator poly_rec; define poly function using poly_rec
huffman
parents:
29453
diff
changeset

1234 
unfolding poly_def by (simp add: poly_rec_0) 
29451  1235 

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

29454
b0f586f38dd7
add recursion combinator poly_rec; define poly function using poly_rec
huffman
parents:
29453
diff
changeset

1237 
unfolding poly_def by (simp add: poly_rec_pCons) 
29451  1238 

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

1240 
unfolding one_poly_def by simp 

1241 

29454
b0f586f38dd7
add recursion combinator poly_rec; define poly function using poly_rec
huffman
parents:
29453
diff
changeset

1242 
lemma poly_monom: 
31021  1243 
fixes a x :: "'a::{comm_semiring_1}" 
29454
b0f586f38dd7
add recursion combinator poly_rec; define poly function using poly_rec
huffman
parents:
29453
diff
changeset

1244 
shows "poly (monom a n) x = a * x ^ n" 
29451  1245 
by (induct n, simp add: monom_0, simp add: monom_Suc power_Suc mult_ac) 
1246 

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

1248 
apply (induct p arbitrary: q, simp) 

29667  1249 
apply (case_tac q, simp, simp add: algebra_simps) 
29451  1250 
done 
1251 

1252 
lemma poly_minus [simp]: 

29454
b0f586f38dd7
add recursion combinator poly_rec; define poly function using poly_rec
huffman
parents:
29453
diff
changeset

1253 
fixes x :: "'a::comm_ring" 
29451  1254 
shows "poly ( p) x =  poly p x" 
1255 
by (induct p, simp_all) 

1256 

1257 
lemma poly_diff [simp]: 

29454
b0f586f38dd7
add recursion combinator poly_rec; define poly function using poly_rec
huffman
parents:
29453
diff
changeset

1258 
fixes x :: "'a::comm_ring" 
29451  1259 
shows "poly (p  q) x = poly p x  poly q x" 
1260 
by (simp add: diff_minus) 

1261 

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

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

1264 

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

29667  1266 
by (induct p, simp, simp add: algebra_simps) 
29451  1267 

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

29667  1269 
by (induct p, simp_all, simp add: algebra_simps) 
29451  1270 

29462  1271 
lemma poly_power [simp]: 
31021  1272 
fixes p :: "'a::{comm_semiring_1} poly" 
29462  1273 
shows "poly (p ^ n) x = poly p x ^ n" 
1274 
by (induct n, simp, simp add: power_Suc) 

1275 

29456  1276 

1277 
subsection {* Synthetic division *} 

1278 

29980  1279 
text {* 
1280 
Synthetic division is simply division by the 

1281 
linear polynomial @{term "x  c"}. 

1282 
*} 

1283 

29456  1284 
definition 
1285 
synthetic_divmod :: "'a::comm_semiring_0 poly \<Rightarrow> 'a \<Rightarrow> 'a poly \<times> 'a" 

29478  1286 
where [code del]: 
29456  1287 
"synthetic_divmod p c = 
1288 
poly_rec (0, 0) (\<lambda>a p (q, r). (pCons r q, a + c * r)) p" 

1289 

1290 
definition 

1291 
synthetic_div :: "'a::comm_semiring_0 poly \<Rightarrow> 'a \<Rightarrow> 'a poly" 

1292 
where 

1293 
"synthetic_div p c = fst (synthetic_divmod p c)" 

1294 

1295 
lemma synthetic_divmod_0 [simp]: 

1296 
"synthetic_divmod 0 c = (0, 0)" 

1297 
unfolding synthetic_divmod_def 

1298 
by (simp add: poly_rec_0) 

1299 

1300 
lemma synthetic_divmod_pCons [simp]: 

1301 
"synthetic_divmod (pCons a p) c = 

1302 
(\<lambda>(q, r). (pCons r q, a + c * r)) (synthetic_divmod p c)" 

1303 
unfolding synthetic_divmod_def 

1304 
by (simp add: poly_rec_pCons) 

1305 

1306 
lemma snd_synthetic_divmod: "snd (synthetic_divmod p c) = poly p c" 

1307 
by (induct p, simp, simp add: split_def) 

1308 

1309 
lemma synthetic_div_0 [simp]: "synthetic_div 0 c = 0" 

1310 
unfolding synthetic_div_def by simp 

1311 

1312 
lemma synthetic_div_pCons [simp]: 

1313 
"synthetic_div (pCons a p) c = pCons (poly p c) (synthetic_div p c)" 

1314 
unfolding synthetic_div_def 

1315 
by (simp add: split_def snd_synthetic_divmod) 

1316 

29460
ad87e5d1488b
new lemmas about synthetic_div; declare degree_pCons_eq_if [simp]
huffman
parents:
29457
diff
changeset

1317 
lemma synthetic_div_eq_0_iff: 
ad87e5d1488b
new lemmas about synthetic_div; declare degree_pCons_eq_if [simp]
huffman
parents:
29457
diff
changeset

1318 
"synthetic_div p c = 0 \<longleftrightarrow> degree p = 0" 
ad87e5d1488b
new lemmas about synthetic_div; declare degree_pCons_eq_if [simp]
huffman
parents:
29457
diff
changeset

1319 
by (induct p, simp, case_tac p, simp) 
ad87e5d1488b
new lemmas about synthetic_div; declare degree_pCons_eq_if [simp]
huffman
parents:
29457
diff
changeset

1320 

ad87e5d1488b
new lemmas about synthetic_div; declare degree_pCons_eq_if [simp]
huffman
parents:
29457
diff
changeset

1321 
lemma degree_synthetic_div: 
ad87e5d1488b
new lemmas about synthetic_div; declare degree_pCons_eq_if [simp]
huffman
parents:
29457
diff
changeset

1322 
"degree (synthetic_div p c) = degree p  1" 
ad87e5d1488b
new lemmas about synthetic_div; declare degree_pCons_eq_if [simp]
huffman
parents:
29457
diff
changeset

1323 
by (induct p, simp, simp add: synthetic_div_eq_0_iff) 
ad87e5d1488b
new lemmas about synthetic_div; declare degree_pCons_eq_if [simp]
huffman
parents:
29457
diff
changeset

1324 

29457  1325 
lemma synthetic_div_correct: 
29456  1326 
"p + smult c (synthetic_div p c) = pCons (poly p c) (synthetic_div p c)" 
1327 
by (induct p) simp_all 

1328 

29457  1329 
lemma synthetic_div_unique_lemma: "smult c p = pCons a p \<Longrightarrow> p = 0" 
1330 
by (induct p arbitrary: a) simp_all 

1331 

1332 
lemma synthetic_div_unique: 

1333 
"p + smult c q = pCons r q \<Longrightarrow> r = poly p c \<and> q = synthetic_div p c" 

1334 
apply (induct p arbitrary: q r) 

1335 
apply (simp, frule synthetic_div_unique_lemma, simp) 

1336 
apply (case_tac q, force) 

1337 
done 

1338 

1339 
lemma synthetic_div_correct': 

1340 
fixes c :: "'a::comm_ring_1" 

1341 
shows "[:c, 1:] * synthetic_div p c + [:poly p c:] = p" 

1342 
using synthetic_div_correct [of p c] 

29667  1343 
by (simp add: algebra_simps) 
29457  1344 

29460
ad87e5d1488b
new lemmas about synthetic_div; declare degree_pCons_eq_if [simp]
huffman
parents:
29457
diff
changeset

1345 
lemma poly_eq_0_iff_dvd: 
ad87e5d1488b
new lemmas about synthetic_div; declare degree_pCons_eq_if [simp]
huffman
parents:
29457
diff
changeset

1346 
fixes c :: "'a::idom" 
ad87e5d1488b
new lemmas about synthetic_div; declare degree_pCons_eq_if [simp]
huffman
parents:
29457
diff
changeset

1347 
shows "poly p c = 0 \<longleftrightarrow> [:c, 1:] dvd p" 
ad87e5d1488b
new lemmas about synthetic_div; declare degree_pCons_eq_if [simp]
huffman
parents:
29457
diff
changeset

1348 
proof 
ad87e5d1488b
new lemmas about synthetic_div; declare degree_pCons_eq_if [simp]
huffman
parents:
29457
diff
changeset

1349 
assume "poly p c = 0" 
ad87e5d1488b
new lemmas about synthetic_div; declare degree_pCons_eq_if [simp]
huffman
parents:
29457
diff
changeset

1350 
with synthetic_div_correct' [of c p] 
ad87e5d1488b
new lemmas about synthetic_div; declare degree_pCons_eq_if [simp]
huffman
parents:
29457
diff
changeset

1351 
have "p = [:c, 1:] * synthetic_div p c" by simp 
ad87e5d1488b
new lemmas about synthetic_div; declare degree_pCons_eq_if [simp]
huffman
parents:
29457
diff
changeset

1352 
then show "[:c, 1:] dvd p" .. 
ad87e5d1488b
new lemmas about synthetic_div; declare degree_pCons_eq_if [simp]
huffman
parents:
29457
diff
changeset

1353 
next 
ad87e5d1488b
new lemmas about synthetic_div; declare degree_pCons_eq_if [simp]
huffman
parents:
29457
diff
changeset

1354 
assume "[:c, 1:] dvd p" 
ad87e5d1488b
new lemmas about synthetic_div; declare degree_pCons_eq_if [simp]
huffman
parents:
29457
diff
changeset

1355 
then obtain k where "p = [:c, 1:] * k" by (rule dvdE) 
ad87e5d1488b
new lemmas about synthetic_div; declare degree_pCons_eq_if [simp]
huffman
parents:
29457
diff
changeset

1356 
then show "poly p c = 0" by simp 
ad87e5d1488b
new lemmas about synthetic_div; declare degree_pCons_eq_if [simp]
huffman
parents:
29457
diff
changeset

1357 
qed 
ad87e5d1488b
new lemmas about synthetic_div; declare degree_pCons_eq_if [simp]
huffman
parents:
29457
diff
changeset

1358 

ad87e5d1488b
new lemmas about synthetic_div; declare degree_pCons_eq_if [simp]
huffman
parents:
29457
diff
changeset

1359 
lemma dvd_iff_poly_eq_0: 
ad87e5d1488b
new lemmas about synthetic_div; declare degree_pCons_eq_if [simp]
huffman
parents:
29457
diff
changeset

1360 
fixes c :: "'a::idom" 
ad87e5d1488b
new lemmas about synthetic_div; declare degree_pCons_eq_if [simp]
huffman
parents:
29457
diff
changeset

1361 
shows "[:c, 1:] dvd p \<longleftrightarrow> poly p (c) = 0" 
ad87e5d1488b
new lemmas about synthetic_div; declare degree_pCons_eq_if [simp]
huffman
parents:
29457
diff
changeset

1362 
by (simp add: poly_eq_0_iff_dvd) 
ad87e5d1488b
new lemmas about synthetic_div; declare degree_pCons_eq_if [simp]
huffman
parents:
29457
diff
changeset

1363 

29462  1364 
lemma poly_roots_finite: 
1365 
fixes p :: "'a::idom poly" 

1366 
shows "p \<noteq> 0 \<Longrightarrow> finite {x. poly p x = 0}" 

1367 
proof (induct n \<equiv> "degree p" arbitrary: p) 

1368 
case (0 p) 

1369 
then obtain a where "a \<noteq> 0" and "p = [:a:]" 

1370 
by (cases p, simp split: if_splits) 

1371 
then show "finite {x. poly p x = 0}" by simp 

1372 
next 

1373 
case (Suc n p) 

1374 
show "finite {x. poly p x = 0}" 

1375 
proof (cases "\<exists>x. poly p x = 0") 

1376 
case False 

1377 
then show "finite {x. poly p x = 0}" by simp 

1378 
next 

1379 
case True 

1380 
then obtain a where "poly p a = 0" .. 

1381 
then have "[:a, 1:] dvd p" by (simp only: poly_eq_0_iff_dvd) 

1382 
then obtain k where k: "p = [:a, 1:] * k" .. 

1383 
with `p \<noteq> 0` have "k \<noteq> 0" by auto 

1384 
with k have "degree p = Suc (degree k)" 

1385 
by (simp add: degree_mult_eq del: mult_pCons_left) 

1386 
with `Suc n = degree p` have "n = degree k" by simp 

34915  1387 
then have "finite {x. poly k x = 0}" using `k \<noteq> 0` by (rule Suc.hyps) 
29462  1388 
then have "finite (insert a {x. poly k x = 0})" by simp 
1389 
then show "finite {x. poly p x = 0}" 

1390 
by (simp add: k uminus_add_conv_diff Collect_disj_eq 

1391 
del: mult_pCons_left) 

1392 
qed 

1393 
qed 

1394 

29979  1395 
lemma poly_zero: 
1396 
fixes p :: "'a::{idom,ring_char_0} poly" 

1397 
shows "poly p = poly 0 \<longleftrightarrow> p = 0" 

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

1399 
apply (drule poly_roots_finite) 

1400 
apply (auto simp add: infinite_UNIV_char_0) 

1401 
done 

1402 

1403 
lemma poly_eq_iff: 

1404 
fixes p q :: "'a::{idom,ring_char_0} poly" 

1405 
shows "poly p = poly q \<longleftrightarrow> p = q" 

1406 
using poly_zero [of "p  q"] 

1407 
by (simp add: expand_fun_eq) 

1408 

29478  1409 

29980  1410 
subsection {* Composition of polynomials *} 
1411 

1412 
definition 

1413 
pcompose :: "'a::comm_semiring_0 poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly" 

1414 
where 

1415 
"pcompose p q = poly_rec 0 (\<lambda>a _ c. [:a:] + q * c) p" 

1416 

1417 
lemma pcompose_0 [simp]: "pcompose 0 q = 0" 

1418 
unfolding pcompose_def by (simp add: poly_rec_0) 
