author  paulson <lp15@cam.ac.uk> 
Thu, 29 Sep 2016 11:24:36 +0100  
changeset 63954  fb03766658f4 
parent 63950  cdc1e59aa513 
child 64164  38c407446400 
permissions  rwrr 
63764  1 
(* Title: HOL/Library/Polynomial_Factorial.thy 
2 
Author: Brian Huffman 

3 
Author: Clemens Ballarin 

4 
Author: Amine Chaieb 

5 
Author: Florian Haftmann 

6 
Author: Manuel Eberl 

7 
*) 

8 

63498  9 
theory Polynomial_Factorial 
10 
imports 

11 
Complex_Main 

63705
7d371a18b6a2
Polynomial algebra cleanup (tuned)
eberlm <eberlm@in.tum.de>
parents:
63704
diff
changeset

12 
"~~/src/HOL/Number_Theory/Euclidean_Algorithm" 
63498  13 
"~~/src/HOL/Library/Polynomial" 
63500  14 
"~~/src/HOL/Library/Normalized_Fraction" 
63498  15 
begin 
16 

17 
subsection \<open>Prelude\<close> 

18 

63830  19 
lemma prod_mset_mult: 
20 
"prod_mset (image_mset (\<lambda>x. f x * g x) A) = prod_mset (image_mset f A) * prod_mset (image_mset g A)" 

63498  21 
by (induction A) (simp_all add: mult_ac) 
22 

63830  23 
lemma prod_mset_const: "prod_mset (image_mset (\<lambda>_. c) A) = c ^ size A" 
63498  24 
by (induction A) (simp_all add: mult_ac) 
25 

26 
lemma dvd_field_iff: "x dvd y \<longleftrightarrow> (x = 0 \<longrightarrow> y = (0::'a::field))" 

27 
proof safe 

28 
assume "x \<noteq> 0" 

29 
hence "y = x * (y / x)" by (simp add: field_simps) 

30 
thus "x dvd y" by (rule dvdI) 

31 
qed auto 

32 

33 
lemma nat_descend_induct [case_names base descend]: 

34 
assumes "\<And>k::nat. k > n \<Longrightarrow> P k" 

35 
assumes "\<And>k::nat. k \<le> n \<Longrightarrow> (\<And>i. i > k \<Longrightarrow> P i) \<Longrightarrow> P k" 

36 
shows "P m" 

37 
using assms by induction_schema (force intro!: wf_measure[of "\<lambda>k. Suc n  k"])+ 

38 

39 
lemma GreatestI_ex: "\<exists>k::nat. P k \<Longrightarrow> \<forall>y. P y \<longrightarrow> y < b \<Longrightarrow> P (GREATEST x. P x)" 

40 
by (metis GreatestI) 

41 

42 

43 
context field 

44 
begin 

45 

46 
subclass idom_divide .. 

47 

48 
end 

49 

50 
context field 

51 
begin 

52 

53 
definition normalize_field :: "'a \<Rightarrow> 'a" 

54 
where [simp]: "normalize_field x = (if x = 0 then 0 else 1)" 

55 
definition unit_factor_field :: "'a \<Rightarrow> 'a" 

56 
where [simp]: "unit_factor_field x = x" 

57 
definition euclidean_size_field :: "'a \<Rightarrow> nat" 

58 
where [simp]: "euclidean_size_field x = (if x = 0 then 0 else 1)" 

59 
definition mod_field :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" 

60 
where [simp]: "mod_field x y = (if y = 0 then x else 0)" 

61 

62 
end 

63 

64 
instantiation real :: euclidean_ring 

65 
begin 

66 

67 
definition [simp]: "normalize_real = (normalize_field :: real \<Rightarrow> _)" 

68 
definition [simp]: "unit_factor_real = (unit_factor_field :: real \<Rightarrow> _)" 

69 
definition [simp]: "euclidean_size_real = (euclidean_size_field :: real \<Rightarrow> _)" 

63950
cdc1e59aa513
syntactic type class for operation mod named after mod;
haftmann
parents:
63905
diff
changeset

70 
definition [simp]: "modulo_real = (mod_field :: real \<Rightarrow> _)" 
63498  71 

72 
instance by standard (simp_all add: dvd_field_iff divide_simps) 

73 
end 

74 

75 
instantiation real :: euclidean_ring_gcd 

76 
begin 

77 

78 
definition gcd_real :: "real \<Rightarrow> real \<Rightarrow> real" where 

79 
"gcd_real = gcd_eucl" 

80 
definition lcm_real :: "real \<Rightarrow> real \<Rightarrow> real" where 

81 
"lcm_real = lcm_eucl" 

82 
definition Gcd_real :: "real set \<Rightarrow> real" where 

83 
"Gcd_real = Gcd_eucl" 

84 
definition Lcm_real :: "real set \<Rightarrow> real" where 

85 
"Lcm_real = Lcm_eucl" 

86 

87 
instance by standard (simp_all add: gcd_real_def lcm_real_def Gcd_real_def Lcm_real_def) 

88 

89 
end 

90 

91 
instantiation rat :: euclidean_ring 

92 
begin 

93 

94 
definition [simp]: "normalize_rat = (normalize_field :: rat \<Rightarrow> _)" 

95 
definition [simp]: "unit_factor_rat = (unit_factor_field :: rat \<Rightarrow> _)" 

96 
definition [simp]: "euclidean_size_rat = (euclidean_size_field :: rat \<Rightarrow> _)" 

63950
cdc1e59aa513
syntactic type class for operation mod named after mod;
haftmann
parents:
63905
diff
changeset

97 
definition [simp]: "modulo_rat = (mod_field :: rat \<Rightarrow> _)" 
63498  98 

99 
instance by standard (simp_all add: dvd_field_iff divide_simps) 

100 
end 

101 

102 
instantiation rat :: euclidean_ring_gcd 

103 
begin 

104 

105 
definition gcd_rat :: "rat \<Rightarrow> rat \<Rightarrow> rat" where 

106 
"gcd_rat = gcd_eucl" 

107 
definition lcm_rat :: "rat \<Rightarrow> rat \<Rightarrow> rat" where 

108 
"lcm_rat = lcm_eucl" 

109 
definition Gcd_rat :: "rat set \<Rightarrow> rat" where 

110 
"Gcd_rat = Gcd_eucl" 

111 
definition Lcm_rat :: "rat set \<Rightarrow> rat" where 

112 
"Lcm_rat = Lcm_eucl" 

113 

114 
instance by standard (simp_all add: gcd_rat_def lcm_rat_def Gcd_rat_def Lcm_rat_def) 

115 

116 
end 

117 

118 
instantiation complex :: euclidean_ring 

119 
begin 

120 

121 
definition [simp]: "normalize_complex = (normalize_field :: complex \<Rightarrow> _)" 

122 
definition [simp]: "unit_factor_complex = (unit_factor_field :: complex \<Rightarrow> _)" 

123 
definition [simp]: "euclidean_size_complex = (euclidean_size_field :: complex \<Rightarrow> _)" 

63950
cdc1e59aa513
syntactic type class for operation mod named after mod;
haftmann
parents:
63905
diff
changeset

124 
definition [simp]: "modulo_complex = (mod_field :: complex \<Rightarrow> _)" 
63498  125 

126 
instance by standard (simp_all add: dvd_field_iff divide_simps) 

127 
end 

128 

129 
instantiation complex :: euclidean_ring_gcd 

130 
begin 

131 

132 
definition gcd_complex :: "complex \<Rightarrow> complex \<Rightarrow> complex" where 

133 
"gcd_complex = gcd_eucl" 

134 
definition lcm_complex :: "complex \<Rightarrow> complex \<Rightarrow> complex" where 

135 
"lcm_complex = lcm_eucl" 

136 
definition Gcd_complex :: "complex set \<Rightarrow> complex" where 

137 
"Gcd_complex = Gcd_eucl" 

138 
definition Lcm_complex :: "complex set \<Rightarrow> complex" where 

139 
"Lcm_complex = Lcm_eucl" 

140 

141 
instance by standard (simp_all add: gcd_complex_def lcm_complex_def Gcd_complex_def Lcm_complex_def) 

142 

143 
end 

144 

145 

146 

147 
subsection \<open>Lifting elements into the field of fractions\<close> 

148 

149 
definition to_fract :: "'a :: idom \<Rightarrow> 'a fract" where "to_fract x = Fract x 1" 

150 

151 
lemma to_fract_0 [simp]: "to_fract 0 = 0" 

152 
by (simp add: to_fract_def eq_fract Zero_fract_def) 

153 

154 
lemma to_fract_1 [simp]: "to_fract 1 = 1" 

155 
by (simp add: to_fract_def eq_fract One_fract_def) 

156 

157 
lemma to_fract_add [simp]: "to_fract (x + y) = to_fract x + to_fract y" 

158 
by (simp add: to_fract_def) 

159 

160 
lemma to_fract_diff [simp]: "to_fract (x  y) = to_fract x  to_fract y" 

161 
by (simp add: to_fract_def) 

162 

163 
lemma to_fract_uminus [simp]: "to_fract (x) = to_fract x" 

164 
by (simp add: to_fract_def) 

165 

166 
lemma to_fract_mult [simp]: "to_fract (x * y) = to_fract x * to_fract y" 

167 
by (simp add: to_fract_def) 

168 

169 
lemma to_fract_eq_iff [simp]: "to_fract x = to_fract y \<longleftrightarrow> x = y" 

170 
by (simp add: to_fract_def eq_fract) 

171 

172 
lemma to_fract_eq_0_iff [simp]: "to_fract x = 0 \<longleftrightarrow> x = 0" 

173 
by (simp add: to_fract_def Zero_fract_def eq_fract) 

174 

175 
lemma snd_quot_of_fract_nonzero [simp]: "snd (quot_of_fract x) \<noteq> 0" 

176 
by transfer simp 

177 

178 
lemma Fract_quot_of_fract [simp]: "Fract (fst (quot_of_fract x)) (snd (quot_of_fract x)) = x" 

179 
by transfer (simp del: fractrel_iff, subst fractrel_normalize_quot_left, simp) 

180 

181 
lemma to_fract_quot_of_fract: 

182 
assumes "snd (quot_of_fract x) = 1" 

183 
shows "to_fract (fst (quot_of_fract x)) = x" 

184 
proof  

185 
have "x = Fract (fst (quot_of_fract x)) (snd (quot_of_fract x))" by simp 

186 
also note assms 

187 
finally show ?thesis by (simp add: to_fract_def) 

188 
qed 

189 

190 
lemma snd_quot_of_fract_Fract_whole: 

191 
assumes "y dvd x" 

192 
shows "snd (quot_of_fract (Fract x y)) = 1" 

193 
using assms by transfer (auto simp: normalize_quot_def Let_def gcd_proj2_if_dvd) 

194 

195 
lemma Fract_conv_to_fract: "Fract a b = to_fract a / to_fract b" 

196 
by (simp add: to_fract_def) 

197 

198 
lemma quot_of_fract_to_fract [simp]: "quot_of_fract (to_fract x) = (x, 1)" 

199 
unfolding to_fract_def by transfer (simp add: normalize_quot_def) 

200 

201 
lemma fst_quot_of_fract_eq_0_iff [simp]: "fst (quot_of_fract x) = 0 \<longleftrightarrow> x = 0" 

202 
by transfer simp 

203 

204 
lemma snd_quot_of_fract_to_fract [simp]: "snd (quot_of_fract (to_fract x)) = 1" 

205 
unfolding to_fract_def by (rule snd_quot_of_fract_Fract_whole) simp_all 

206 

207 
lemma coprime_quot_of_fract: 

208 
"coprime (fst (quot_of_fract x)) (snd (quot_of_fract x))" 

209 
by transfer (simp add: coprime_normalize_quot) 

210 

211 
lemma unit_factor_snd_quot_of_fract: "unit_factor (snd (quot_of_fract x)) = 1" 

212 
using quot_of_fract_in_normalized_fracts[of x] 

213 
by (simp add: normalized_fracts_def case_prod_unfold) 

214 

215 
lemma unit_factor_1_imp_normalized: "unit_factor x = 1 \<Longrightarrow> normalize x = x" 

216 
by (subst (2) normalize_mult_unit_factor [symmetric, of x]) 

217 
(simp del: normalize_mult_unit_factor) 

218 

219 
lemma normalize_snd_quot_of_fract: "normalize (snd (quot_of_fract x)) = snd (quot_of_fract x)" 

220 
by (intro unit_factor_1_imp_normalized unit_factor_snd_quot_of_fract) 

221 

222 

223 
subsection \<open>Mapping polynomials\<close> 

224 

225 
definition map_poly 

63954
fb03766658f4
Generalised the type of map_poly
paulson <lp15@cam.ac.uk>
parents:
63950
diff
changeset

226 
:: "('a :: zero \<Rightarrow> 'b :: zero) \<Rightarrow> 'a poly \<Rightarrow> 'b poly" where 
63498  227 
"map_poly f p = Poly (map f (coeffs p))" 
228 

229 
lemma map_poly_0 [simp]: "map_poly f 0 = 0" 

230 
by (simp add: map_poly_def) 

231 

232 
lemma map_poly_1: "map_poly f 1 = [:f 1:]" 

233 
by (simp add: map_poly_def) 

234 

235 
lemma map_poly_1' [simp]: "f 1 = 1 \<Longrightarrow> map_poly f 1 = 1" 

236 
by (simp add: map_poly_def one_poly_def) 

237 

238 
lemma coeff_map_poly: 

239 
assumes "f 0 = 0" 

240 
shows "coeff (map_poly f p) n = f (coeff p n)" 

241 
by (auto simp: map_poly_def nth_default_def coeffs_def assms 

242 
not_less Suc_le_eq coeff_eq_0 simp del: upt_Suc) 

243 

244 
lemma coeffs_map_poly [code abstract]: 

245 
"coeffs (map_poly f p) = strip_while (op = 0) (map f (coeffs p))" 

246 
by (simp add: map_poly_def) 

247 

248 
lemma set_coeffs_map_poly: 

249 
"(\<And>x. f x = 0 \<longleftrightarrow> x = 0) \<Longrightarrow> set (coeffs (map_poly f p)) = f ` set (coeffs p)" 

250 
by (cases "p = 0") (auto simp: coeffs_map_poly last_map last_coeffs_not_0) 

251 

252 
lemma coeffs_map_poly': 

253 
assumes "(\<And>x. x \<noteq> 0 \<Longrightarrow> f x \<noteq> 0)" 

254 
shows "coeffs (map_poly f p) = map f (coeffs p)" 

255 
by (cases "p = 0") (auto simp: coeffs_map_poly last_map last_coeffs_not_0 assms 

256 
intro!: strip_while_not_last split: if_splits) 

257 

258 
lemma degree_map_poly: 

259 
assumes "\<And>x. x \<noteq> 0 \<Longrightarrow> f x \<noteq> 0" 

260 
shows "degree (map_poly f p) = degree p" 

261 
by (simp add: degree_eq_length_coeffs coeffs_map_poly' assms) 

262 

263 
lemma map_poly_eq_0_iff: 

264 
assumes "f 0 = 0" "\<And>x. x \<in> set (coeffs p) \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> f x \<noteq> 0" 

265 
shows "map_poly f p = 0 \<longleftrightarrow> p = 0" 

266 
proof  

267 
{ 

268 
fix n :: nat 

269 
have "coeff (map_poly f p) n = f (coeff p n)" by (simp add: coeff_map_poly assms) 

270 
also have "\<dots> = 0 \<longleftrightarrow> coeff p n = 0" 

271 
proof (cases "n < length (coeffs p)") 

272 
case True 

273 
hence "coeff p n \<in> set (coeffs p)" by (auto simp: coeffs_def simp del: upt_Suc) 

274 
with assms show "f (coeff p n) = 0 \<longleftrightarrow> coeff p n = 0" by auto 

275 
qed (auto simp: assms length_coeffs nth_default_coeffs_eq [symmetric] nth_default_def) 

276 
finally have "(coeff (map_poly f p) n = 0) = (coeff p n = 0)" . 

277 
} 

278 
thus ?thesis by (auto simp: poly_eq_iff) 

279 
qed 

280 

281 
lemma map_poly_smult: 

282 
assumes "f 0 = 0""\<And>c x. f (c * x) = f c * f x" 

283 
shows "map_poly f (smult c p) = smult (f c) (map_poly f p)" 

284 
by (intro poly_eqI) (simp_all add: assms coeff_map_poly) 

285 

286 
lemma map_poly_pCons: 

287 
assumes "f 0 = 0" 

288 
shows "map_poly f (pCons c p) = pCons (f c) (map_poly f p)" 

289 
by (intro poly_eqI) (simp_all add: assms coeff_map_poly coeff_pCons split: nat.splits) 

290 

291 
lemma map_poly_map_poly: 

292 
assumes "f 0 = 0" "g 0 = 0" 

293 
shows "map_poly f (map_poly g p) = map_poly (f \<circ> g) p" 

294 
by (intro poly_eqI) (simp add: coeff_map_poly assms) 

295 

296 
lemma map_poly_id [simp]: "map_poly id p = p" 

297 
by (simp add: map_poly_def) 

298 

299 
lemma map_poly_id' [simp]: "map_poly (\<lambda>x. x) p = p" 

300 
by (simp add: map_poly_def) 

301 

302 
lemma map_poly_cong: 

303 
assumes "(\<And>x. x \<in> set (coeffs p) \<Longrightarrow> f x = g x)" 

304 
shows "map_poly f p = map_poly g p" 

305 
proof  

306 
from assms have "map f (coeffs p) = map g (coeffs p)" by (intro map_cong) simp_all 

307 
thus ?thesis by (simp only: coeffs_eq_iff coeffs_map_poly) 

308 
qed 

309 

310 
lemma map_poly_monom: "f 0 = 0 \<Longrightarrow> map_poly f (monom c n) = monom (f c) n" 

311 
by (intro poly_eqI) (simp_all add: coeff_map_poly) 

312 

313 
lemma map_poly_idI: 

314 
assumes "\<And>x. x \<in> set (coeffs p) \<Longrightarrow> f x = x" 

315 
shows "map_poly f p = p" 

316 
using map_poly_cong[OF assms, of _ id] by simp 

317 

318 
lemma map_poly_idI': 

319 
assumes "\<And>x. x \<in> set (coeffs p) \<Longrightarrow> f x = x" 

320 
shows "p = map_poly f p" 

321 
using map_poly_cong[OF assms, of _ id] by simp 

322 

323 
lemma smult_conv_map_poly: "smult c p = map_poly (\<lambda>x. c * x) p" 

324 
by (intro poly_eqI) (simp_all add: coeff_map_poly) 

325 

326 
lemma div_const_poly_conv_map_poly: 

327 
assumes "[:c:] dvd p" 

328 
shows "p div [:c:] = map_poly (\<lambda>x. x div c) p" 

329 
proof (cases "c = 0") 

330 
case False 

331 
from assms obtain q where p: "p = [:c:] * q" by (erule dvdE) 

332 
moreover { 

333 
have "smult c q = [:c:] * q" by simp 

334 
also have "\<dots> div [:c:] = q" by (rule nonzero_mult_divide_cancel_left) (insert False, auto) 

335 
finally have "smult c q div [:c:] = q" . 

336 
} 

337 
ultimately show ?thesis by (intro poly_eqI) (auto simp: coeff_map_poly False) 

338 
qed (auto intro!: poly_eqI simp: coeff_map_poly) 

339 

340 

341 

342 
subsection \<open>Various facts about polynomials\<close> 

343 

63830  344 
lemma prod_mset_const_poly: "prod_mset (image_mset (\<lambda>x. [:f x:]) A) = [:prod_mset (image_mset f A):]" 
63498  345 
by (induction A) (simp_all add: one_poly_def mult_ac) 
346 

347 
lemma degree_mod_less': "b \<noteq> 0 \<Longrightarrow> a mod b \<noteq> 0 \<Longrightarrow> degree (a mod b) < degree b" 

348 
using degree_mod_less[of b a] by auto 

349 

350 
lemma is_unit_const_poly_iff: 

351 
"[:c :: 'a :: {comm_semiring_1,semiring_no_zero_divisors}:] dvd 1 \<longleftrightarrow> c dvd 1" 

352 
by (auto simp: one_poly_def) 

353 

354 
lemma is_unit_poly_iff: 

355 
fixes p :: "'a :: {comm_semiring_1,semiring_no_zero_divisors} poly" 

356 
shows "p dvd 1 \<longleftrightarrow> (\<exists>c. p = [:c:] \<and> c dvd 1)" 

357 
proof safe 

358 
assume "p dvd 1" 

359 
then obtain q where pq: "1 = p * q" by (erule dvdE) 

360 
hence "degree 1 = degree (p * q)" by simp 

361 
also from pq have "\<dots> = degree p + degree q" by (intro degree_mult_eq) auto 

362 
finally have "degree p = 0" by simp 

363 
from degree_eq_zeroE[OF this] obtain c where c: "p = [:c:]" . 

364 
with \<open>p dvd 1\<close> show "\<exists>c. p = [:c:] \<and> c dvd 1" 

365 
by (auto simp: is_unit_const_poly_iff) 

366 
qed (auto simp: is_unit_const_poly_iff) 

367 

368 
lemma is_unit_polyE: 

369 
fixes p :: "'a :: {comm_semiring_1,semiring_no_zero_divisors} poly" 

370 
assumes "p dvd 1" obtains c where "p = [:c:]" "c dvd 1" 

371 
using assms by (subst (asm) is_unit_poly_iff) blast 

372 

373 
lemma smult_eq_iff: 

374 
assumes "(b :: 'a :: field) \<noteq> 0" 

375 
shows "smult a p = smult b q \<longleftrightarrow> smult (a / b) p = q" 

376 
proof 

377 
assume "smult a p = smult b q" 

378 
also from assms have "smult (inverse b) \<dots> = q" by simp 

379 
finally show "smult (a / b) p = q" by (simp add: field_simps) 

380 
qed (insert assms, auto) 

381 

382 
lemma irreducible_const_poly_iff: 

383 
fixes c :: "'a :: {comm_semiring_1,semiring_no_zero_divisors}" 

384 
shows "irreducible [:c:] \<longleftrightarrow> irreducible c" 

385 
proof 

386 
assume A: "irreducible c" 

387 
show "irreducible [:c:]" 

388 
proof (rule irreducibleI) 

389 
fix a b assume ab: "[:c:] = a * b" 

390 
hence "degree [:c:] = degree (a * b)" by (simp only: ) 

391 
also from A ab have "a \<noteq> 0" "b \<noteq> 0" by auto 

392 
hence "degree (a * b) = degree a + degree b" by (simp add: degree_mult_eq) 

393 
finally have "degree a = 0" "degree b = 0" by auto 

394 
then obtain a' b' where ab': "a = [:a':]" "b = [:b':]" by (auto elim!: degree_eq_zeroE) 

395 
from ab have "coeff [:c:] 0 = coeff (a * b) 0" by (simp only: ) 

396 
hence "c = a' * b'" by (simp add: ab' mult_ac) 

397 
from A and this have "a' dvd 1 \<or> b' dvd 1" by (rule irreducibleD) 

398 
with ab' show "a dvd 1 \<or> b dvd 1" by (auto simp: one_poly_def) 

399 
qed (insert A, auto simp: irreducible_def is_unit_poly_iff) 

400 
next 

401 
assume A: "irreducible [:c:]" 

402 
show "irreducible c" 

403 
proof (rule irreducibleI) 

404 
fix a b assume ab: "c = a * b" 

405 
hence "[:c:] = [:a:] * [:b:]" by (simp add: mult_ac) 

406 
from A and this have "[:a:] dvd 1 \<or> [:b:] dvd 1" by (rule irreducibleD) 

407 
thus "a dvd 1 \<or> b dvd 1" by (simp add: one_poly_def) 

408 
qed (insert A, auto simp: irreducible_def one_poly_def) 

409 
qed 

410 

411 
lemma lead_coeff_monom [simp]: "lead_coeff (monom c n) = c" 

412 
by (cases "c = 0") (simp_all add: lead_coeff_def degree_monom_eq) 

413 

414 

415 
subsection \<open>Normalisation of polynomials\<close> 

416 

417 
instantiation poly :: ("{normalization_semidom,idom_divide}") normalization_semidom 

418 
begin 

419 

420 
definition unit_factor_poly :: "'a poly \<Rightarrow> 'a poly" 

421 
where "unit_factor_poly p = monom (unit_factor (lead_coeff p)) 0" 

422 

423 
definition normalize_poly :: "'a poly \<Rightarrow> 'a poly" 

424 
where "normalize_poly p = map_poly (\<lambda>x. x div unit_factor (lead_coeff p)) p" 

425 

426 
lemma normalize_poly_altdef: 

427 
"normalize p = p div [:unit_factor (lead_coeff p):]" 

428 
proof (cases "p = 0") 

429 
case False 

430 
thus ?thesis 

431 
by (subst div_const_poly_conv_map_poly) 

432 
(auto simp: normalize_poly_def const_poly_dvd_iff lead_coeff_def ) 

433 
qed (auto simp: normalize_poly_def) 

434 

435 
instance 

436 
proof 

437 
fix p :: "'a poly" 

438 
show "unit_factor p * normalize p = p" 

439 
by (cases "p = 0") 

440 
(simp_all add: unit_factor_poly_def normalize_poly_def monom_0 

441 
smult_conv_map_poly map_poly_map_poly o_def) 

442 
next 

443 
fix p :: "'a poly" 

444 
assume "is_unit p" 

445 
then obtain c where p: "p = [:c:]" "is_unit c" by (auto simp: is_unit_poly_iff) 

446 
thus "normalize p = 1" 

447 
by (simp add: normalize_poly_def map_poly_pCons is_unit_normalize one_poly_def) 

448 
next 

449 
fix p :: "'a poly" assume "p \<noteq> 0" 

450 
thus "is_unit (unit_factor p)" 

451 
by (simp add: unit_factor_poly_def monom_0 is_unit_poly_iff) 

452 
qed (simp_all add: normalize_poly_def unit_factor_poly_def monom_0 lead_coeff_mult unit_factor_mult) 

453 

454 
end 

455 

456 
lemma unit_factor_pCons: 

457 
"unit_factor (pCons a p) = (if p = 0 then monom (unit_factor a) 0 else unit_factor p)" 

458 
by (simp add: unit_factor_poly_def) 

459 

460 
lemma normalize_monom [simp]: 

461 
"normalize (monom a n) = monom (normalize a) n" 

462 
by (simp add: map_poly_monom normalize_poly_def) 

463 

464 
lemma unit_factor_monom [simp]: 

465 
"unit_factor (monom a n) = monom (unit_factor a) 0" 

466 
by (simp add: unit_factor_poly_def ) 

467 

468 
lemma normalize_const_poly: "normalize [:c:] = [:normalize c:]" 

469 
by (simp add: normalize_poly_def map_poly_pCons) 

470 

471 
lemma normalize_smult: "normalize (smult c p) = smult (normalize c) (normalize p)" 

472 
proof  

473 
have "smult c p = [:c:] * p" by simp 

474 
also have "normalize \<dots> = smult (normalize c) (normalize p)" 

475 
by (subst normalize_mult) (simp add: normalize_const_poly) 

476 
finally show ?thesis . 

477 
qed 

478 

479 
lemma is_unit_smult_iff: "smult c p dvd 1 \<longleftrightarrow> c dvd 1 \<and> p dvd 1" 

480 
proof  

481 
have "smult c p = [:c:] * p" by simp 

482 
also have "\<dots> dvd 1 \<longleftrightarrow> c dvd 1 \<and> p dvd 1" 

483 
proof safe 

484 
assume A: "[:c:] * p dvd 1" 

485 
thus "p dvd 1" by (rule dvd_mult_right) 

486 
from A obtain q where B: "1 = [:c:] * p * q" by (erule dvdE) 

487 
have "c dvd c * (coeff p 0 * coeff q 0)" by simp 

488 
also have "\<dots> = coeff ([:c:] * p * q) 0" by (simp add: mult.assoc coeff_mult) 

489 
also note B [symmetric] 

490 
finally show "c dvd 1" by simp 

491 
next 

492 
assume "c dvd 1" "p dvd 1" 

493 
from \<open>c dvd 1\<close> obtain d where "1 = c * d" by (erule dvdE) 

494 
hence "1 = [:c:] * [:d:]" by (simp add: one_poly_def mult_ac) 

495 
hence "[:c:] dvd 1" by (rule dvdI) 

496 
from mult_dvd_mono[OF this \<open>p dvd 1\<close>] show "[:c:] * p dvd 1" by simp 

497 
qed 

498 
finally show ?thesis . 

499 
qed 

500 

501 

502 
subsection \<open>Content and primitive part of a polynomial\<close> 

503 

504 
definition content :: "('a :: semiring_Gcd poly) \<Rightarrow> 'a" where 

505 
"content p = Gcd (set (coeffs p))" 

506 

507 
lemma content_0 [simp]: "content 0 = 0" 

508 
by (simp add: content_def) 

509 

510 
lemma content_1 [simp]: "content 1 = 1" 

511 
by (simp add: content_def) 

512 

513 
lemma content_const [simp]: "content [:c:] = normalize c" 

514 
by (simp add: content_def cCons_def) 

515 

516 
lemma const_poly_dvd_iff_dvd_content: 

517 
fixes c :: "'a :: semiring_Gcd" 

518 
shows "[:c:] dvd p \<longleftrightarrow> c dvd content p" 

519 
proof (cases "p = 0") 

520 
case [simp]: False 

521 
have "[:c:] dvd p \<longleftrightarrow> (\<forall>n. c dvd coeff p n)" by (rule const_poly_dvd_iff) 

522 
also have "\<dots> \<longleftrightarrow> (\<forall>a\<in>set (coeffs p). c dvd a)" 

523 
proof safe 

524 
fix n :: nat assume "\<forall>a\<in>set (coeffs p). c dvd a" 

525 
thus "c dvd coeff p n" 

526 
by (cases "n \<le> degree p") (auto simp: coeff_eq_0 coeffs_def split: if_splits) 

527 
qed (auto simp: coeffs_def simp del: upt_Suc split: if_splits) 

528 
also have "\<dots> \<longleftrightarrow> c dvd content p" 

529 
by (simp add: content_def dvd_Gcd_iff mult.commute [of "unit_factor x" for x] 

530 
dvd_mult_unit_iff lead_coeff_nonzero) 

531 
finally show ?thesis . 

532 
qed simp_all 

533 

534 
lemma content_dvd [simp]: "[:content p:] dvd p" 

535 
by (subst const_poly_dvd_iff_dvd_content) simp_all 

536 

537 
lemma content_dvd_coeff [simp]: "content p dvd coeff p n" 

538 
by (cases "n \<le> degree p") 

539 
(auto simp: content_def coeffs_def not_le coeff_eq_0 simp del: upt_Suc intro: Gcd_dvd) 

540 

541 
lemma content_dvd_coeffs: "c \<in> set (coeffs p) \<Longrightarrow> content p dvd c" 

542 
by (simp add: content_def Gcd_dvd) 

543 

544 
lemma normalize_content [simp]: "normalize (content p) = content p" 

545 
by (simp add: content_def) 

546 

547 
lemma is_unit_content_iff [simp]: "is_unit (content p) \<longleftrightarrow> content p = 1" 

548 
proof 

549 
assume "is_unit (content p)" 

550 
hence "normalize (content p) = 1" by (simp add: is_unit_normalize del: normalize_content) 

551 
thus "content p = 1" by simp 

552 
qed auto 

553 

554 
lemma content_smult [simp]: "content (smult c p) = normalize c * content p" 

555 
by (simp add: content_def coeffs_smult Gcd_mult) 

556 

557 
lemma content_eq_zero_iff [simp]: "content p = 0 \<longleftrightarrow> p = 0" 

558 
by (auto simp: content_def simp: poly_eq_iff coeffs_def) 

559 

560 
definition primitive_part :: "'a :: {semiring_Gcd,idom_divide} poly \<Rightarrow> 'a poly" where 

561 
"primitive_part p = (if p = 0 then 0 else map_poly (\<lambda>x. x div content p) p)" 

562 

563 
lemma primitive_part_0 [simp]: "primitive_part 0 = 0" 

564 
by (simp add: primitive_part_def) 

565 

566 
lemma content_times_primitive_part [simp]: 

567 
fixes p :: "'a :: {idom_divide, semiring_Gcd} poly" 

568 
shows "smult (content p) (primitive_part p) = p" 

569 
proof (cases "p = 0") 

570 
case False 

571 
thus ?thesis 

572 
unfolding primitive_part_def 

573 
by (auto simp: smult_conv_map_poly map_poly_map_poly o_def content_dvd_coeffs 

574 
intro: map_poly_idI) 

575 
qed simp_all 

576 

577 
lemma primitive_part_eq_0_iff [simp]: "primitive_part p = 0 \<longleftrightarrow> p = 0" 

578 
proof (cases "p = 0") 

579 
case False 

580 
hence "primitive_part p = map_poly (\<lambda>x. x div content p) p" 

581 
by (simp add: primitive_part_def) 

582 
also from False have "\<dots> = 0 \<longleftrightarrow> p = 0" 

583 
by (intro map_poly_eq_0_iff) (auto simp: dvd_div_eq_0_iff content_dvd_coeffs) 

584 
finally show ?thesis using False by simp 

585 
qed simp 

586 

587 
lemma content_primitive_part [simp]: 

588 
assumes "p \<noteq> 0" 

589 
shows "content (primitive_part p) = 1" 

590 
proof  

591 
have "p = smult (content p) (primitive_part p)" by simp 

592 
also have "content \<dots> = content p * content (primitive_part p)" 

593 
by (simp del: content_times_primitive_part) 

594 
finally show ?thesis using assms by simp 

595 
qed 

596 

597 
lemma content_decompose: 

598 
fixes p :: "'a :: semiring_Gcd poly" 

599 
obtains p' where "p = smult (content p) p'" "content p' = 1" 

600 
proof (cases "p = 0") 

601 
case True 

602 
thus ?thesis by (intro that[of 1]) simp_all 

603 
next 

604 
case False 

605 
from content_dvd[of p] obtain r where r: "p = [:content p:] * r" by (erule dvdE) 

606 
have "content p * 1 = content p * content r" by (subst r) simp 

607 
with False have "content r = 1" by (subst (asm) mult_left_cancel) simp_all 

608 
with r show ?thesis by (intro that[of r]) simp_all 

609 
qed 

610 

611 
lemma smult_content_normalize_primitive_part [simp]: 

612 
"smult (content p) (normalize (primitive_part p)) = normalize p" 

613 
proof  

614 
have "smult (content p) (normalize (primitive_part p)) = 

615 
normalize ([:content p:] * primitive_part p)" 

616 
by (subst normalize_mult) (simp_all add: normalize_const_poly) 

617 
also have "[:content p:] * primitive_part p = p" by simp 

618 
finally show ?thesis . 

619 
qed 

620 

621 
lemma content_dvd_contentI [intro]: 

622 
"p dvd q \<Longrightarrow> content p dvd content q" 

623 
using const_poly_dvd_iff_dvd_content content_dvd dvd_trans by blast 

624 

625 
lemma primitive_part_const_poly [simp]: "primitive_part [:x:] = [:unit_factor x:]" 

626 
by (simp add: primitive_part_def map_poly_pCons) 

627 

628 
lemma primitive_part_prim: "content p = 1 \<Longrightarrow> primitive_part p = p" 

629 
by (auto simp: primitive_part_def) 

630 

631 
lemma degree_primitive_part [simp]: "degree (primitive_part p) = degree p" 

632 
proof (cases "p = 0") 

633 
case False 

634 
have "p = smult (content p) (primitive_part p)" by simp 

635 
also from False have "degree \<dots> = degree (primitive_part p)" 

636 
by (subst degree_smult_eq) simp_all 

637 
finally show ?thesis .. 

638 
qed simp_all 

639 

640 

641 
subsection \<open>Lifting polynomial coefficients to the field of fractions\<close> 

642 

643 
abbreviation (input) fract_poly 

644 
where "fract_poly \<equiv> map_poly to_fract" 

645 

646 
abbreviation (input) unfract_poly 

647 
where "unfract_poly \<equiv> map_poly (fst \<circ> quot_of_fract)" 

648 

649 
lemma fract_poly_smult [simp]: "fract_poly (smult c p) = smult (to_fract c) (fract_poly p)" 

650 
by (simp add: smult_conv_map_poly map_poly_map_poly o_def) 

651 

652 
lemma fract_poly_0 [simp]: "fract_poly 0 = 0" 

653 
by (simp add: poly_eqI coeff_map_poly) 

654 

655 
lemma fract_poly_1 [simp]: "fract_poly 1 = 1" 

656 
by (simp add: one_poly_def map_poly_pCons) 

657 

658 
lemma fract_poly_add [simp]: 

659 
"fract_poly (p + q) = fract_poly p + fract_poly q" 

660 
by (intro poly_eqI) (simp_all add: coeff_map_poly) 

661 

662 
lemma fract_poly_diff [simp]: 

663 
"fract_poly (p  q) = fract_poly p  fract_poly q" 

664 
by (intro poly_eqI) (simp_all add: coeff_map_poly) 

665 

666 
lemma to_fract_setsum [simp]: "to_fract (setsum f A) = setsum (\<lambda>x. to_fract (f x)) A" 

667 
by (cases "finite A", induction A rule: finite_induct) simp_all 

668 

669 
lemma fract_poly_mult [simp]: 

670 
"fract_poly (p * q) = fract_poly p * fract_poly q" 

671 
by (intro poly_eqI) (simp_all add: coeff_map_poly coeff_mult) 

672 

673 
lemma fract_poly_eq_iff [simp]: "fract_poly p = fract_poly q \<longleftrightarrow> p = q" 

674 
by (auto simp: poly_eq_iff coeff_map_poly) 

675 

676 
lemma fract_poly_eq_0_iff [simp]: "fract_poly p = 0 \<longleftrightarrow> p = 0" 

677 
using fract_poly_eq_iff[of p 0] by (simp del: fract_poly_eq_iff) 

678 

679 
lemma fract_poly_dvd: "p dvd q \<Longrightarrow> fract_poly p dvd fract_poly q" 

680 
by (auto elim!: dvdE) 

681 

63830  682 
lemma prod_mset_fract_poly: 
683 
"prod_mset (image_mset (\<lambda>x. fract_poly (f x)) A) = fract_poly (prod_mset (image_mset f A))" 

63498  684 
by (induction A) (simp_all add: mult_ac) 
685 

686 
lemma is_unit_fract_poly_iff: 

687 
"p dvd 1 \<longleftrightarrow> fract_poly p dvd 1 \<and> content p = 1" 

688 
proof safe 

689 
assume A: "p dvd 1" 

690 
with fract_poly_dvd[of p 1] show "is_unit (fract_poly p)" by simp 

691 
from A show "content p = 1" 

692 
by (auto simp: is_unit_poly_iff normalize_1_iff) 

693 
next 

694 
assume A: "fract_poly p dvd 1" and B: "content p = 1" 

695 
from A obtain c where c: "fract_poly p = [:c:]" by (auto simp: is_unit_poly_iff) 

696 
{ 

697 
fix n :: nat assume "n > 0" 

698 
have "to_fract (coeff p n) = coeff (fract_poly p) n" by (simp add: coeff_map_poly) 

699 
also note c 

700 
also from \<open>n > 0\<close> have "coeff [:c:] n = 0" by (simp add: coeff_pCons split: nat.splits) 

701 
finally have "coeff p n = 0" by simp 

702 
} 

703 
hence "degree p \<le> 0" by (intro degree_le) simp_all 

704 
with B show "p dvd 1" by (auto simp: is_unit_poly_iff normalize_1_iff elim!: degree_eq_zeroE) 

705 
qed 

706 

707 
lemma fract_poly_is_unit: "p dvd 1 \<Longrightarrow> fract_poly p dvd 1" 

708 
using fract_poly_dvd[of p 1] by simp 

709 

710 
lemma fract_poly_smult_eqE: 

711 
fixes c :: "'a :: {idom_divide,ring_gcd} fract" 

712 
assumes "fract_poly p = smult c (fract_poly q)" 

713 
obtains a b 

714 
where "c = to_fract b / to_fract a" "smult a p = smult b q" "coprime a b" "normalize a = a" 

715 
proof  

716 
define a b where "a = fst (quot_of_fract c)" and "b = snd (quot_of_fract c)" 

717 
have "smult (to_fract a) (fract_poly q) = smult (to_fract b) (fract_poly p)" 

718 
by (subst smult_eq_iff) (simp_all add: a_def b_def Fract_conv_to_fract [symmetric] assms) 

719 
hence "fract_poly (smult a q) = fract_poly (smult b p)" by (simp del: fract_poly_eq_iff) 

720 
hence "smult b p = smult a q" by (simp only: fract_poly_eq_iff) 

721 
moreover have "c = to_fract a / to_fract b" "coprime b a" "normalize b = b" 

722 
by (simp_all add: a_def b_def coprime_quot_of_fract gcd.commute 

723 
normalize_snd_quot_of_fract Fract_conv_to_fract [symmetric]) 

724 
ultimately show ?thesis by (intro that[of a b]) 

725 
qed 

726 

727 

728 
subsection \<open>Fractional content\<close> 

729 

730 
abbreviation (input) Lcm_coeff_denoms 

731 
:: "'a :: {semiring_Gcd,idom_divide,ring_gcd} fract poly \<Rightarrow> 'a" 

732 
where "Lcm_coeff_denoms p \<equiv> Lcm (snd ` quot_of_fract ` set (coeffs p))" 

733 

734 
definition fract_content :: 

735 
"'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} fract poly \<Rightarrow> 'a fract" where 

736 
"fract_content p = 

737 
(let d = Lcm_coeff_denoms p in Fract (content (unfract_poly (smult (to_fract d) p))) d)" 

738 

739 
definition primitive_part_fract :: 

740 
"'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} fract poly \<Rightarrow> 'a poly" where 

741 
"primitive_part_fract p = 

742 
primitive_part (unfract_poly (smult (to_fract (Lcm_coeff_denoms p)) p))" 

743 

744 
lemma primitive_part_fract_0 [simp]: "primitive_part_fract 0 = 0" 

745 
by (simp add: primitive_part_fract_def) 

746 

747 
lemma fract_content_eq_0_iff [simp]: 

748 
"fract_content p = 0 \<longleftrightarrow> p = 0" 

749 
unfolding fract_content_def Let_def Zero_fract_def 

750 
by (subst eq_fract) (auto simp: Lcm_0_iff map_poly_eq_0_iff) 

751 

752 
lemma content_primitive_part_fract [simp]: "p \<noteq> 0 \<Longrightarrow> content (primitive_part_fract p) = 1" 

753 
unfolding primitive_part_fract_def 

754 
by (rule content_primitive_part) 

755 
(auto simp: primitive_part_fract_def map_poly_eq_0_iff Lcm_0_iff) 

756 

757 
lemma content_times_primitive_part_fract: 

758 
"smult (fract_content p) (fract_poly (primitive_part_fract p)) = p" 

759 
proof  

760 
define p' where "p' = unfract_poly (smult (to_fract (Lcm_coeff_denoms p)) p)" 

761 
have "fract_poly p' = 

762 
map_poly (to_fract \<circ> fst \<circ> quot_of_fract) (smult (to_fract (Lcm_coeff_denoms p)) p)" 

763 
unfolding primitive_part_fract_def p'_def 

764 
by (subst map_poly_map_poly) (simp_all add: o_assoc) 

765 
also have "\<dots> = smult (to_fract (Lcm_coeff_denoms p)) p" 

766 
proof (intro map_poly_idI, unfold o_apply) 

767 
fix c assume "c \<in> set (coeffs (smult (to_fract (Lcm_coeff_denoms p)) p))" 

768 
then obtain c' where c: "c' \<in> set (coeffs p)" "c = to_fract (Lcm_coeff_denoms p) * c'" 

769 
by (auto simp add: Lcm_0_iff coeffs_smult split: if_splits) 

770 
note c(2) 

771 
also have "c' = Fract (fst (quot_of_fract c')) (snd (quot_of_fract c'))" 

772 
by simp 

773 
also have "to_fract (Lcm_coeff_denoms p) * \<dots> = 

774 
Fract (Lcm_coeff_denoms p * fst (quot_of_fract c')) (snd (quot_of_fract c'))" 

775 
unfolding to_fract_def by (subst mult_fract) simp_all 

776 
also have "snd (quot_of_fract \<dots>) = 1" 

777 
by (intro snd_quot_of_fract_Fract_whole dvd_mult2 dvd_Lcm) (insert c(1), auto) 

778 
finally show "to_fract (fst (quot_of_fract c)) = c" 

779 
by (rule to_fract_quot_of_fract) 

780 
qed 

781 
also have "p' = smult (content p') (primitive_part p')" 

782 
by (rule content_times_primitive_part [symmetric]) 

783 
also have "primitive_part p' = primitive_part_fract p" 

784 
by (simp add: primitive_part_fract_def p'_def) 

785 
also have "fract_poly (smult (content p') (primitive_part_fract p)) = 

786 
smult (to_fract (content p')) (fract_poly (primitive_part_fract p))" by simp 

787 
finally have "smult (to_fract (content p')) (fract_poly (primitive_part_fract p)) = 

788 
smult (to_fract (Lcm_coeff_denoms p)) p" . 

789 
thus ?thesis 

790 
by (subst (asm) smult_eq_iff) 

791 
(auto simp add: Let_def p'_def Fract_conv_to_fract field_simps Lcm_0_iff fract_content_def) 

792 
qed 

793 

794 
lemma fract_content_fract_poly [simp]: "fract_content (fract_poly p) = to_fract (content p)" 

795 
proof  

796 
have "Lcm_coeff_denoms (fract_poly p) = 1" 

63905  797 
by (auto simp: set_coeffs_map_poly) 
63498  798 
hence "fract_content (fract_poly p) = 
799 
to_fract (content (map_poly (fst \<circ> quot_of_fract \<circ> to_fract) p))" 

800 
by (simp add: fract_content_def to_fract_def fract_collapse map_poly_map_poly del: Lcm_1_iff) 

801 
also have "map_poly (fst \<circ> quot_of_fract \<circ> to_fract) p = p" 

802 
by (intro map_poly_idI) simp_all 

803 
finally show ?thesis . 

804 
qed 

805 

806 
lemma content_decompose_fract: 

807 
fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} fract poly" 

808 
obtains c p' where "p = smult c (map_poly to_fract p')" "content p' = 1" 

809 
proof (cases "p = 0") 

810 
case True 

811 
hence "p = smult 0 (map_poly to_fract 1)" "content 1 = 1" by simp_all 

812 
thus ?thesis .. 

813 
next 

814 
case False 

815 
thus ?thesis 

816 
by (rule that[OF content_times_primitive_part_fract [symmetric] content_primitive_part_fract]) 

817 
qed 

818 

819 

820 
subsection \<open>More properties of content and primitive part\<close> 

821 

822 
lemma lift_prime_elem_poly: 

63633  823 
assumes "prime_elem (c :: 'a :: semidom)" 
824 
shows "prime_elem [:c:]" 

825 
proof (rule prime_elemI) 

63498  826 
fix a b assume *: "[:c:] dvd a * b" 
827 
from * have dvd: "c dvd coeff (a * b) n" for n 

828 
by (subst (asm) const_poly_dvd_iff) blast 

829 
{ 

830 
define m where "m = (GREATEST m. \<not>c dvd coeff b m)" 

831 
assume "\<not>[:c:] dvd b" 

832 
hence A: "\<exists>i. \<not>c dvd coeff b i" by (subst (asm) const_poly_dvd_iff) blast 

833 
have B: "\<forall>i. \<not>c dvd coeff b i \<longrightarrow> i < Suc (degree b)" 

834 
by (auto intro: le_degree simp: less_Suc_eq_le) 

835 
have coeff_m: "\<not>c dvd coeff b m" unfolding m_def by (rule GreatestI_ex[OF A B]) 

836 
have "i \<le> m" if "\<not>c dvd coeff b i" for i 

837 
unfolding m_def by (rule Greatest_le[OF that B]) 

838 
hence dvd_b: "c dvd coeff b i" if "i > m" for i using that by force 

839 

840 
have "c dvd coeff a i" for i 

841 
proof (induction i rule: nat_descend_induct[of "degree a"]) 

842 
case (base i) 

843 
thus ?case by (simp add: coeff_eq_0) 

844 
next 

845 
case (descend i) 

846 
let ?A = "{..i+m}  {i}" 

847 
have "c dvd coeff (a * b) (i + m)" by (rule dvd) 

848 
also have "coeff (a * b) (i + m) = (\<Sum>k\<le>i + m. coeff a k * coeff b (i + m  k))" 

849 
by (simp add: coeff_mult) 

850 
also have "{..i+m} = insert i ?A" by auto 

851 
also have "(\<Sum>k\<in>\<dots>. coeff a k * coeff b (i + m  k)) = 

852 
coeff a i * coeff b m + (\<Sum>k\<in>?A. coeff a k * coeff b (i + m  k))" 

853 
(is "_ = _ + ?S") 

854 
by (subst setsum.insert) simp_all 

855 
finally have eq: "c dvd coeff a i * coeff b m + ?S" . 

856 
moreover have "c dvd ?S" 

857 
proof (rule dvd_setsum) 

858 
fix k assume k: "k \<in> {..i+m}  {i}" 

859 
show "c dvd coeff a k * coeff b (i + m  k)" 

860 
proof (cases "k < i") 

861 
case False 

862 
with k have "c dvd coeff a k" by (intro descend.IH) simp 

863 
thus ?thesis by simp 

864 
next 

865 
case True 

866 
hence "c dvd coeff b (i + m  k)" by (intro dvd_b) simp 

867 
thus ?thesis by simp 

868 
qed 

869 
qed 

870 
ultimately have "c dvd coeff a i * coeff b m" 

871 
by (simp add: dvd_add_left_iff) 

872 
with assms coeff_m show "c dvd coeff a i" 

63633  873 
by (simp add: prime_elem_dvd_mult_iff) 
63498  874 
qed 
875 
hence "[:c:] dvd a" by (subst const_poly_dvd_iff) blast 

876 
} 

877 
thus "[:c:] dvd a \<or> [:c:] dvd b" by blast 

63633  878 
qed (insert assms, simp_all add: prime_elem_def one_poly_def) 
63498  879 

880 
lemma prime_elem_const_poly_iff: 

881 
fixes c :: "'a :: semidom" 

63633  882 
shows "prime_elem [:c:] \<longleftrightarrow> prime_elem c" 
63498  883 
proof 
63633  884 
assume A: "prime_elem [:c:]" 
885 
show "prime_elem c" 

886 
proof (rule prime_elemI) 

63498  887 
fix a b assume "c dvd a * b" 
888 
hence "[:c:] dvd [:a:] * [:b:]" by (simp add: mult_ac) 

63633  889 
from A and this have "[:c:] dvd [:a:] \<or> [:c:] dvd [:b:]" by (rule prime_elem_dvd_multD) 
63498  890 
thus "c dvd a \<or> c dvd b" by simp 
63633  891 
qed (insert A, auto simp: prime_elem_def is_unit_poly_iff) 
63498  892 
qed (auto intro: lift_prime_elem_poly) 
893 

894 
context 

895 
begin 

896 

897 
private lemma content_1_mult: 

898 
fixes f g :: "'a :: {semiring_Gcd,factorial_semiring} poly" 

899 
assumes "content f = 1" "content g = 1" 

900 
shows "content (f * g) = 1" 

901 
proof (cases "f * g = 0") 

902 
case False 

903 
from assms have "f \<noteq> 0" "g \<noteq> 0" by auto 

904 

905 
hence "f * g \<noteq> 0" by auto 

906 
{ 

907 
assume "\<not>is_unit (content (f * g))" 

63633  908 
with False have "\<exists>p. p dvd content (f * g) \<and> prime p" 
63498  909 
by (intro prime_divisor_exists) simp_all 
63633  910 
then obtain p where "p dvd content (f * g)" "prime p" by blast 
63498  911 
from \<open>p dvd content (f * g)\<close> have "[:p:] dvd f * g" 
912 
by (simp add: const_poly_dvd_iff_dvd_content) 

63633  913 
moreover from \<open>prime p\<close> have "prime_elem [:p:]" by (simp add: lift_prime_elem_poly) 
63498  914 
ultimately have "[:p:] dvd f \<or> [:p:] dvd g" 
63633  915 
by (simp add: prime_elem_dvd_mult_iff) 
63498  916 
with assms have "is_unit p" by (simp add: const_poly_dvd_iff_dvd_content) 
63633  917 
with \<open>prime p\<close> have False by simp 
63498  918 
} 
919 
hence "is_unit (content (f * g))" by blast 

920 
hence "normalize (content (f * g)) = 1" by (simp add: is_unit_normalize del: normalize_content) 

921 
thus ?thesis by simp 

922 
qed (insert assms, auto) 

923 

924 
lemma content_mult: 

925 
fixes p q :: "'a :: {factorial_semiring, semiring_Gcd} poly" 

926 
shows "content (p * q) = content p * content q" 

927 
proof  

928 
from content_decompose[of p] guess p' . note p = this 

929 
from content_decompose[of q] guess q' . note q = this 

930 
have "content (p * q) = content p * content q * content (p' * q')" 

931 
by (subst p, subst q) (simp add: mult_ac normalize_mult) 

932 
also from p q have "content (p' * q') = 1" by (intro content_1_mult) 

933 
finally show ?thesis by simp 

934 
qed 

935 

936 
lemma primitive_part_mult: 

937 
fixes p q :: "'a :: {factorial_semiring, semiring_Gcd, ring_gcd, idom_divide} poly" 

938 
shows "primitive_part (p * q) = primitive_part p * primitive_part q" 

939 
proof  

940 
have "primitive_part (p * q) = p * q div [:content (p * q):]" 

941 
by (simp add: primitive_part_def div_const_poly_conv_map_poly) 

942 
also have "\<dots> = (p div [:content p:]) * (q div [:content q:])" 

943 
by (subst div_mult_div_if_dvd) (simp_all add: content_mult mult_ac) 

944 
also have "\<dots> = primitive_part p * primitive_part q" 

945 
by (simp add: primitive_part_def div_const_poly_conv_map_poly) 

946 
finally show ?thesis . 

947 
qed 

948 

949 
lemma primitive_part_smult: 

950 
fixes p :: "'a :: {factorial_semiring, semiring_Gcd, ring_gcd, idom_divide} poly" 

951 
shows "primitive_part (smult a p) = smult (unit_factor a) (primitive_part p)" 

952 
proof  

953 
have "smult a p = [:a:] * p" by simp 

954 
also have "primitive_part \<dots> = smult (unit_factor a) (primitive_part p)" 

955 
by (subst primitive_part_mult) simp_all 

956 
finally show ?thesis . 

957 
qed 

958 

959 
lemma primitive_part_dvd_primitive_partI [intro]: 

960 
fixes p q :: "'a :: {factorial_semiring, semiring_Gcd, ring_gcd, idom_divide} poly" 

961 
shows "p dvd q \<Longrightarrow> primitive_part p dvd primitive_part q" 

962 
by (auto elim!: dvdE simp: primitive_part_mult) 

963 

63830  964 
lemma content_prod_mset: 
63498  965 
fixes A :: "'a :: {factorial_semiring, semiring_Gcd} poly multiset" 
63830  966 
shows "content (prod_mset A) = prod_mset (image_mset content A)" 
63498  967 
by (induction A) (simp_all add: content_mult mult_ac) 
968 

969 
lemma fract_poly_dvdD: 

970 
fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} poly" 

971 
assumes "fract_poly p dvd fract_poly q" "content p = 1" 

972 
shows "p dvd q" 

973 
proof  

974 
from assms(1) obtain r where r: "fract_poly q = fract_poly p * r" by (erule dvdE) 

975 
from content_decompose_fract[of r] guess c r' . note r' = this 

976 
from r r' have eq: "fract_poly q = smult c (fract_poly (p * r'))" by simp 

977 
from fract_poly_smult_eqE[OF this] guess a b . note ab = this 

978 
have "content (smult a q) = content (smult b (p * r'))" by (simp only: ab(2)) 

979 
hence eq': "normalize b = a * content q" by (simp add: assms content_mult r' ab(4)) 

980 
have "1 = gcd a (normalize b)" by (simp add: ab) 

981 
also note eq' 

982 
also have "gcd a (a * content q) = a" by (simp add: gcd_proj1_if_dvd ab(4)) 

983 
finally have [simp]: "a = 1" by simp 

984 
from eq ab have "q = p * ([:b:] * r')" by simp 

985 
thus ?thesis by (rule dvdI) 

986 
qed 

987 

988 
lemma content_prod_eq_1_iff: 

989 
fixes p q :: "'a :: {factorial_semiring, semiring_Gcd} poly" 

990 
shows "content (p * q) = 1 \<longleftrightarrow> content p = 1 \<and> content q = 1" 

991 
proof safe 

992 
assume A: "content (p * q) = 1" 

993 
{ 

994 
fix p q :: "'a poly" assume "content p * content q = 1" 

995 
hence "1 = content p * content q" by simp 

996 
hence "content p dvd 1" by (rule dvdI) 

997 
hence "content p = 1" by simp 

998 
} note B = this 

999 
from A B[of p q] B [of q p] show "content p = 1" "content q = 1" 

1000 
by (simp_all add: content_mult mult_ac) 

1001 
qed (auto simp: content_mult) 

1002 

1003 
end 

1004 

1005 

1006 
subsection \<open>Polynomials over a field are a Euclidean ring\<close> 

1007 

63722
b9c8da46443b
Deprivatisation of lemmas in Polynomial_Factorial
Manuel Eberl <eberlm@in.tum.de>
parents:
63705
diff
changeset

1008 
definition unit_factor_field_poly :: "'a :: field poly \<Rightarrow> 'a poly" where 
63498  1009 
"unit_factor_field_poly p = [:lead_coeff p:]" 
1010 

63722
b9c8da46443b
Deprivatisation of lemmas in Polynomial_Factorial
Manuel Eberl <eberlm@in.tum.de>
parents:
63705
diff
changeset

1011 
definition normalize_field_poly :: "'a :: field poly \<Rightarrow> 'a poly" where 
63498  1012 
"normalize_field_poly p = smult (inverse (lead_coeff p)) p" 
1013 

63722
b9c8da46443b
Deprivatisation of lemmas in Polynomial_Factorial
Manuel Eberl <eberlm@in.tum.de>
parents:
63705
diff
changeset

1014 
definition euclidean_size_field_poly :: "'a :: field poly \<Rightarrow> nat" where 
63498  1015 
"euclidean_size_field_poly p = (if p = 0 then 0 else 2 ^ degree p)" 
1016 

63722
b9c8da46443b
Deprivatisation of lemmas in Polynomial_Factorial
Manuel Eberl <eberlm@in.tum.de>
parents:
63705
diff
changeset

1017 
lemma dvd_field_poly: "dvd.dvd (op * :: 'a :: field poly \<Rightarrow> _) = op dvd" 
63498  1018 
by (intro ext) (simp_all add: dvd.dvd_def dvd_def) 
1019 

1020 
interpretation field_poly: 

1021 
euclidean_ring "op div" "op *" "op mod" "op +" "op " 0 "1 :: 'a :: field poly" 

1022 
normalize_field_poly unit_factor_field_poly euclidean_size_field_poly uminus 

1023 
proof (standard, unfold dvd_field_poly) 

1024 
fix p :: "'a poly" 

1025 
show "unit_factor_field_poly p * normalize_field_poly p = p" 

1026 
by (cases "p = 0") 

1027 
(simp_all add: unit_factor_field_poly_def normalize_field_poly_def lead_coeff_nonzero) 

1028 
next 

1029 
fix p :: "'a poly" assume "is_unit p" 

1030 
thus "normalize_field_poly p = 1" 

1031 
by (elim is_unit_polyE) (auto simp: normalize_field_poly_def monom_0 one_poly_def field_simps) 

1032 
next 

1033 
fix p :: "'a poly" assume "p \<noteq> 0" 

1034 
thus "is_unit (unit_factor_field_poly p)" 

1035 
by (simp add: unit_factor_field_poly_def lead_coeff_nonzero is_unit_pCons_iff) 

1036 
qed (auto simp: unit_factor_field_poly_def normalize_field_poly_def lead_coeff_mult 

1037 
euclidean_size_field_poly_def intro!: degree_mod_less' degree_mult_right_le) 

1038 

63722
b9c8da46443b
Deprivatisation of lemmas in Polynomial_Factorial
Manuel Eberl <eberlm@in.tum.de>
parents:
63705
diff
changeset

1039 
lemma field_poly_irreducible_imp_prime: 
63498  1040 
assumes "irreducible (p :: 'a :: field poly)" 
63633  1041 
shows "prime_elem p" 
63498  1042 
proof  
1043 
have A: "class.comm_semiring_1 op * 1 op + (0 :: 'a poly)" .. 

63633  1044 
from field_poly.irreducible_imp_prime_elem[of p] assms 
1045 
show ?thesis unfolding irreducible_def prime_elem_def dvd_field_poly 

1046 
comm_semiring_1.irreducible_def[OF A] comm_semiring_1.prime_elem_def[OF A] by blast 

63498  1047 
qed 
1048 

63830  1049 
lemma field_poly_prod_mset_prime_factorization: 
63498  1050 
assumes "(x :: 'a :: field poly) \<noteq> 0" 
63830  1051 
shows "prod_mset (field_poly.prime_factorization x) = normalize_field_poly x" 
63498  1052 
proof  
1053 
have A: "class.comm_monoid_mult op * (1 :: 'a poly)" .. 

63830  1054 
have "comm_monoid_mult.prod_mset op * (1 :: 'a poly) = prod_mset" 
1055 
by (intro ext) (simp add: comm_monoid_mult.prod_mset_def[OF A] prod_mset_def) 

1056 
with field_poly.prod_mset_prime_factorization[OF assms] show ?thesis by simp 

63498  1057 
qed 
1058 

63722
b9c8da46443b
Deprivatisation of lemmas in Polynomial_Factorial
Manuel Eberl <eberlm@in.tum.de>
parents:
63705
diff
changeset

1059 
lemma field_poly_in_prime_factorization_imp_prime: 
63498  1060 
assumes "(p :: 'a :: field poly) \<in># field_poly.prime_factorization x" 
63633  1061 
shows "prime_elem p" 
63498  1062 
proof  
1063 
have A: "class.comm_semiring_1 op * 1 op + (0 :: 'a poly)" .. 

1064 
have B: "class.normalization_semidom op div op + op  (0 :: 'a poly) op * 1 

1065 
normalize_field_poly unit_factor_field_poly" .. 

63905  1066 
from field_poly.in_prime_factors_imp_prime [of p x] assms 
63633  1067 
show ?thesis unfolding prime_elem_def dvd_field_poly 
1068 
comm_semiring_1.prime_elem_def[OF A] normalization_semidom.prime_def[OF B] by blast 

63498  1069 
qed 
1070 

1071 

1072 
subsection \<open>Primality and irreducibility in polynomial rings\<close> 

1073 

1074 
lemma nonconst_poly_irreducible_iff: 

1075 
fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} poly" 

1076 
assumes "degree p \<noteq> 0" 

1077 
shows "irreducible p \<longleftrightarrow> irreducible (fract_poly p) \<and> content p = 1" 

1078 
proof safe 

1079 
assume p: "irreducible p" 

1080 

1081 
from content_decompose[of p] guess p' . note p' = this 

1082 
hence "p = [:content p:] * p'" by simp 

1083 
from p this have "[:content p:] dvd 1 \<or> p' dvd 1" by (rule irreducibleD) 

1084 
moreover have "\<not>p' dvd 1" 

1085 
proof 

1086 
assume "p' dvd 1" 

1087 
hence "degree p = 0" by (subst p') (auto simp: is_unit_poly_iff) 

1088 
with assms show False by contradiction 

1089 
qed 

1090 
ultimately show [simp]: "content p = 1" by (simp add: is_unit_const_poly_iff) 

1091 

1092 
show "irreducible (map_poly to_fract p)" 

1093 
proof (rule irreducibleI) 

1094 
have "fract_poly p = 0 \<longleftrightarrow> p = 0" by (intro map_poly_eq_0_iff) auto 

1095 
with assms show "map_poly to_fract p \<noteq> 0" by auto 

1096 
next 

1097 
show "\<not>is_unit (fract_poly p)" 

1098 
proof 

1099 
assume "is_unit (map_poly to_fract p)" 

1100 
hence "degree (map_poly to_fract p) = 0" 

1101 
by (auto simp: is_unit_poly_iff) 

1102 
hence "degree p = 0" by (simp add: degree_map_poly) 

1103 
with assms show False by contradiction 

1104 
qed 

1105 
next 

1106 
fix q r assume qr: "fract_poly p = q * r" 

1107 
from content_decompose_fract[of q] guess cg q' . note q = this 

1108 
from content_decompose_fract[of r] guess cr r' . note r = this 

1109 
from qr q r p have nz: "cg \<noteq> 0" "cr \<noteq> 0" by auto 

1110 
from qr have eq: "fract_poly p = smult (cr * cg) (fract_poly (q' * r'))" 

1111 
by (simp add: q r) 

1112 
from fract_poly_smult_eqE[OF this] guess a b . note ab = this 

1113 
hence "content (smult a p) = content (smult b (q' * r'))" by (simp only:) 

1114 
with ab(4) have a: "a = normalize b" by (simp add: content_mult q r) 

1115 
hence "normalize b = gcd a b" by simp 

1116 
also from ab(3) have "\<dots> = 1" . 

1117 
finally have "a = 1" "is_unit b" by (simp_all add: a normalize_1_iff) 

1118 

1119 
note eq 

1120 
also from ab(1) \<open>a = 1\<close> have "cr * cg = to_fract b" by simp 

1121 
also have "smult \<dots> (fract_poly (q' * r')) = fract_poly (smult b (q' * r'))" by simp 

1122 
finally have "p = ([:b:] * q') * r'" by (simp del: fract_poly_smult) 

1123 
from p and this have "([:b:] * q') dvd 1 \<or> r' dvd 1" by (rule irreducibleD) 

1124 
hence "q' dvd 1 \<or> r' dvd 1" by (auto dest: dvd_mult_right simp del: mult_pCons_left) 

1125 
hence "fract_poly q' dvd 1 \<or> fract_poly r' dvd 1" by (auto simp: fract_poly_is_unit) 

1126 
with q r show "is_unit q \<or> is_unit r" 

1127 
by (auto simp add: is_unit_smult_iff dvd_field_iff nz) 

1128 
qed 

1129 

1130 
next 

1131 

1132 
assume irred: "irreducible (fract_poly p)" and primitive: "content p = 1" 

1133 
show "irreducible p" 

1134 
proof (rule irreducibleI) 

1135 
from irred show "p \<noteq> 0" by auto 

1136 
next 

1137 
from irred show "\<not>p dvd 1" 

1138 
by (auto simp: irreducible_def dest: fract_poly_is_unit) 

1139 
next 

1140 
fix q r assume qr: "p = q * r" 

1141 
hence "fract_poly p = fract_poly q * fract_poly r" by simp 

1142 
from irred and this have "fract_poly q dvd 1 \<or> fract_poly r dvd 1" 

1143 
by (rule irreducibleD) 

1144 
with primitive qr show "q dvd 1 \<or> r dvd 1" 

1145 
by (auto simp: content_prod_eq_1_iff is_unit_fract_poly_iff) 

1146 
qed 

1147 
qed 

1148 

63722
b9c8da46443b
Deprivatisation of lemmas in Polynomial_Factorial
Manuel Eberl <eberlm@in.tum.de>
parents:
63705
diff
changeset

1149 
context 
b9c8da46443b
Deprivatisation of lemmas in Polynomial_Factorial
Manuel Eberl <eberlm@in.tum.de>
parents:
63705
diff
changeset

1150 
begin 
b9c8da46443b
Deprivatisation of lemmas in Polynomial_Factorial
Manuel Eberl <eberlm@in.tum.de>
parents:
63705
diff
changeset

1151 

63498  1152 
private lemma irreducible_imp_prime_poly: 
1153 
fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} poly" 

1154 
assumes "irreducible p" 

63633  1155 
shows "prime_elem p" 
63498  1156 
proof (cases "degree p = 0") 
1157 
case True 

1158 
with assms show ?thesis 

1159 
by (auto simp: prime_elem_const_poly_iff irreducible_const_poly_iff 

63633  1160 
intro!: irreducible_imp_prime_elem elim!: degree_eq_zeroE) 
63498  1161 
next 
1162 
case False 

1163 
from assms False have irred: "irreducible (fract_poly p)" and primitive: "content p = 1" 

1164 
by (simp_all add: nonconst_poly_irreducible_iff) 

63633  1165 
from irred have prime: "prime_elem (fract_poly p)" by (rule field_poly_irreducible_imp_prime) 
63498  1166 
show ?thesis 
63633  1167 
proof (rule prime_elemI) 
63498  1168 
fix q r assume "p dvd q * r" 
1169 
hence "fract_poly p dvd fract_poly (q * r)" by (rule fract_poly_dvd) 

1170 
hence "fract_poly p dvd fract_poly q * fract_poly r" by simp 

1171 
from prime and this have "fract_poly p dvd fract_poly q \<or> fract_poly p dvd fract_poly r" 

63633  1172 
by (rule prime_elem_dvd_multD) 
63498  1173 
with primitive show "p dvd q \<or> p dvd r" by (auto dest: fract_poly_dvdD) 
1174 
qed (insert assms, auto simp: irreducible_def) 

1175 
qed 

1176 

1177 

1178 
lemma degree_primitive_part_fract [simp]: 

1179 
"degree (primitive_part_fract p) = degree p" 

1180 
proof  

1181 
have "p = smult (fract_content p) (fract_poly (primitive_part_fract p))" 

1182 
by (simp add: content_times_primitive_part_fract) 

1183 
also have "degree \<dots> = degree (primitive_part_fract p)" 

1184 
by (auto simp: degree_map_poly) 

1185 
finally show ?thesis .. 

1186 
qed 

1187 

1188 
lemma irreducible_primitive_part_fract: 

1189 
fixes p :: "'a :: {idom_divide, ring_gcd, factorial_semiring, semiring_Gcd} fract poly" 

1190 
assumes "irreducible p" 

1191 
shows "irreducible (primitive_part_fract p)" 

1192 
proof  

1193 
from assms have deg: "degree (primitive_part_fract p) \<noteq> 0" 

1194 
by (intro notI) 

1195 
(auto elim!: degree_eq_zeroE simp: irreducible_def is_unit_poly_iff dvd_field_iff) 

1196 
hence [simp]: "p \<noteq> 0" by auto 

1197 

1198 
note \<open>irreducible p\<close> 

1199 
also have "p = [:fract_content p:] * fract_poly (primitive_part_fract p)" 

1200 
by (simp add: content_times_primitive_part_fract) 

1201 
also have "irreducible \<dots> \<longleftrightarrow> irreducible (fract_poly (primitive_part_fract p))" 

1202 
by (intro irreducible_mult_unit_left) (simp_all add: is_unit_poly_iff dvd_field_iff) 

1203 
finally show ?thesis using deg 

1204 
by (simp add: nonconst_poly_irreducible_iff) 

1205 
qed 

1206 

63633  1207 
lemma prime_elem_primitive_part_fract: 
63498  1208 
fixes p :: "'a :: {idom_divide, ring_gcd, factorial_semiring, semiring_Gcd} fract poly" 
63633  1209 
shows "irreducible p \<Longrightarrow> prime_elem (primitive_part_fract p)" 
63498  1210 
by (intro irreducible_imp_prime_poly irreducible_primitive_part_fract) 
1211 

1212 
lemma irreducible_linear_field_poly: 

1213 
fixes a b :: "'a::field" 

1214 
assumes "b \<noteq> 0" 

1215 
shows "irreducible [:a,b:]" 

1216 
proof (rule irreducibleI) 

1217 
fix p q assume pq: "[:a,b:] = p * q" 

63539  1218 
also from pq assms have "degree \<dots> = degree p + degree q" 
63498  1219 
by (intro degree_mult_eq) auto 
1220 
finally have "degree p = 0 \<or> degree q = 0" using assms by auto 

1221 
with assms pq show "is_unit p \<or> is_unit q" 

1222 
by (auto simp: is_unit_const_poly_iff dvd_field_iff elim!: degree_eq_zeroE) 

1223 
qed (insert assms, auto simp: is_unit_poly_iff) 

1224 

63633  1225 
lemma prime_elem_linear_field_poly: 
1226 
"(b :: 'a :: field) \<noteq> 0 \<Longrightarrow> prime_elem [:a,b:]" 

63498  1227 
by (rule field_poly_irreducible_imp_prime, rule irreducible_linear_field_poly) 
1228 

1229 
lemma irreducible_linear_poly: 

1230 
fixes a b :: "'a::{idom_divide,ring_gcd,factorial_semiring,semiring_Gcd}" 

1231 
shows "b \<noteq> 0 \<Longrightarrow> coprime a b \<Longrightarrow> irreducible [:a,b:]" 

1232 
by (auto intro!: irreducible_linear_field_poly 

1233 
simp: nonconst_poly_irreducible_iff content_def map_poly_pCons) 

1234 

63633  1235 
lemma prime_elem_linear_poly: 
63498  1236 
fixes a b :: "'a::{idom_divide,ring_gcd,factorial_semiring,semiring_Gcd}" 
63633  1237 
shows "b \<noteq> 0 \<Longrightarrow> coprime a b \<Longrightarrow> prime_elem [:a,b:]" 