author  wenzelm 
Wed, 08 Mar 2017 10:50:59 +0100  
changeset 65151  a7394aa4d21c 
parent 64911  f0e07600de47 
child 65366  10ca63a18e56 
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 

12 
"~~/src/HOL/Library/Polynomial" 

63500  13 
"~~/src/HOL/Library/Normalized_Fraction" 
64591
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64267
diff
changeset

14 
"~~/src/HOL/Library/Field_as_Ring" 
63498  15 
begin 
16 

64591
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64267
diff
changeset

17 
subsection \<open>Various facts about polynomials\<close> 
63498  18 

64591
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64267
diff
changeset

19 
lemma prod_mset_const_poly: "prod_mset (image_mset (\<lambda>x. [:f x:]) A) = [:prod_mset (image_mset f A):]" 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64267
diff
changeset

20 
by (induction A) (simp_all add: one_poly_def mult_ac) 
63498  21 

64591
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64267
diff
changeset

22 
lemma irreducible_const_poly_iff: 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64267
diff
changeset

23 
fixes c :: "'a :: {comm_semiring_1,semiring_no_zero_divisors}" 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64267
diff
changeset

24 
shows "irreducible [:c:] \<longleftrightarrow> irreducible c" 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64267
diff
changeset

25 
proof 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64267
diff
changeset

26 
assume A: "irreducible c" 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64267
diff
changeset

27 
show "irreducible [:c:]" 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64267
diff
changeset

28 
proof (rule irreducibleI) 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64267
diff
changeset

29 
fix a b assume ab: "[:c:] = a * b" 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64267
diff
changeset

30 
hence "degree [:c:] = degree (a * b)" by (simp only: ) 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64267
diff
changeset

31 
also from A ab have "a \<noteq> 0" "b \<noteq> 0" by auto 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64267
diff
changeset

32 
hence "degree (a * b) = degree a + degree b" by (simp add: degree_mult_eq) 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64267
diff
changeset

33 
finally have "degree a = 0" "degree b = 0" by auto 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64267
diff
changeset

34 
then obtain a' b' where ab': "a = [:a':]" "b = [:b':]" by (auto elim!: degree_eq_zeroE) 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64267
diff
changeset

35 
from ab have "coeff [:c:] 0 = coeff (a * b) 0" by (simp only: ) 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64267
diff
changeset

36 
hence "c = a' * b'" by (simp add: ab' mult_ac) 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64267
diff
changeset

37 
from A and this have "a' dvd 1 \<or> b' dvd 1" by (rule irreducibleD) 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64267
diff
changeset

38 
with ab' show "a dvd 1 \<or> b dvd 1" by (auto simp: one_poly_def) 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64267
diff
changeset

39 
qed (insert A, auto simp: irreducible_def is_unit_poly_iff) 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64267
diff
changeset

40 
next 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64267
diff
changeset

41 
assume A: "irreducible [:c:]" 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64267
diff
changeset

42 
show "irreducible c" 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64267
diff
changeset

43 
proof (rule irreducibleI) 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64267
diff
changeset

44 
fix a b assume ab: "c = a * b" 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64267
diff
changeset

45 
hence "[:c:] = [:a:] * [:b:]" by (simp add: mult_ac) 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64267
diff
changeset

46 
from A and this have "[:a:] dvd 1 \<or> [:b:] dvd 1" by (rule irreducibleD) 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64267
diff
changeset

47 
thus "a dvd 1 \<or> b dvd 1" by (simp add: one_poly_def) 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64267
diff
changeset

48 
qed (insert A, auto simp: irreducible_def one_poly_def) 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64267
diff
changeset

49 
qed 
63498  50 

51 

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

53 

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

64911  55 
\<comment> \<open>FIXME: name \<open>of_idom\<close>, abbreviation\<close> 
63498  56 

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

58 
by (simp add: to_fract_def eq_fract Zero_fract_def) 

59 

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

61 
by (simp add: to_fract_def eq_fract One_fract_def) 

62 

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

64 
by (simp add: to_fract_def) 

65 

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

67 
by (simp add: to_fract_def) 

68 

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

70 
by (simp add: to_fract_def) 

71 

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

73 
by (simp add: to_fract_def) 

74 

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

76 
by (simp add: to_fract_def eq_fract) 

77 

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

79 
by (simp add: to_fract_def Zero_fract_def eq_fract) 

80 

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

82 
by transfer simp 

83 

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

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

86 

87 
lemma to_fract_quot_of_fract: 

88 
assumes "snd (quot_of_fract x) = 1" 

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

90 
proof  

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

92 
also note assms 

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

94 
qed 

95 

96 
lemma snd_quot_of_fract_Fract_whole: 

97 
assumes "y dvd x" 

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

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

100 

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

102 
by (simp add: to_fract_def) 

103 

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

105 
unfolding to_fract_def by transfer (simp add: normalize_quot_def) 

106 

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

108 
by transfer simp 

109 

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

111 
unfolding to_fract_def by (rule snd_quot_of_fract_Fract_whole) simp_all 

112 

113 
lemma coprime_quot_of_fract: 

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

115 
by transfer (simp add: coprime_normalize_quot) 

116 

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

118 
using quot_of_fract_in_normalized_fracts[of x] 

119 
by (simp add: normalized_fracts_def case_prod_unfold) 

120 

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

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

123 
(simp del: normalize_mult_unit_factor) 

124 

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

126 
by (intro unit_factor_1_imp_normalized unit_factor_snd_quot_of_fract) 

127 

128 

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

130 

131 
abbreviation (input) fract_poly 

132 
where "fract_poly \<equiv> map_poly to_fract" 

133 

134 
abbreviation (input) unfract_poly 

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

136 

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

138 
by (simp add: smult_conv_map_poly map_poly_map_poly o_def) 

139 

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

141 
by (simp add: poly_eqI coeff_map_poly) 

142 

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

144 
by (simp add: one_poly_def map_poly_pCons) 

145 

146 
lemma fract_poly_add [simp]: 

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

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

149 

150 
lemma fract_poly_diff [simp]: 

151 
"fract_poly (p  q) = fract_poly p  fract_poly q" 

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

153 

64267  154 
lemma to_fract_sum [simp]: "to_fract (sum f A) = sum (\<lambda>x. to_fract (f x)) A" 
63498  155 
by (cases "finite A", induction A rule: finite_induct) simp_all 
156 

157 
lemma fract_poly_mult [simp]: 

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

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

160 

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

162 
by (auto simp: poly_eq_iff coeff_map_poly) 

163 

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

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

166 

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

168 
by (auto elim!: dvdE) 

169 

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

63498  172 
by (induction A) (simp_all add: mult_ac) 
173 

174 
lemma is_unit_fract_poly_iff: 

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

176 
proof safe 

177 
assume A: "p dvd 1" 

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

179 
from A show "content p = 1" 

180 
by (auto simp: is_unit_poly_iff normalize_1_iff) 

181 
next 

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

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

184 
{ 

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

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

187 
also note c 

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

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

190 
} 

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

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

193 
qed 

194 

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

196 
using fract_poly_dvd[of p 1] by simp 

197 

198 
lemma fract_poly_smult_eqE: 

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

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

201 
obtains a b 

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

203 
proof  

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

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

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

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

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

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

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

211 
normalize_snd_quot_of_fract Fract_conv_to_fract [symmetric]) 

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

213 
qed 

214 

215 

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

217 

218 
abbreviation (input) Lcm_coeff_denoms 

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

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

221 

222 
definition fract_content :: 

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

224 
"fract_content p = 

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

226 

227 
definition primitive_part_fract :: 

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

229 
"primitive_part_fract p = 

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

231 

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

233 
by (simp add: primitive_part_fract_def) 

234 

235 
lemma fract_content_eq_0_iff [simp]: 

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

237 
unfolding fract_content_def Let_def Zero_fract_def 

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

239 

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

241 
unfolding primitive_part_fract_def 

242 
by (rule content_primitive_part) 

243 
(auto simp: primitive_part_fract_def map_poly_eq_0_iff Lcm_0_iff) 

244 

245 
lemma content_times_primitive_part_fract: 

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

247 
proof  

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

249 
have "fract_poly p' = 

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

251 
unfolding primitive_part_fract_def p'_def 

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

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

254 
proof (intro map_poly_idI, unfold o_apply) 

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

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

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

258 
note c(2) 

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

260 
by simp 

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

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

263 
unfolding to_fract_def by (subst mult_fract) simp_all 

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

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

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

267 
by (rule to_fract_quot_of_fract) 

268 
qed 

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

270 
by (rule content_times_primitive_part [symmetric]) 

271 
also have "primitive_part p' = primitive_part_fract p" 

272 
by (simp add: primitive_part_fract_def p'_def) 

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

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

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

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

277 
thus ?thesis 

278 
by (subst (asm) smult_eq_iff) 

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

280 
qed 

281 

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

283 
proof  

284 
have "Lcm_coeff_denoms (fract_poly p) = 1" 

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

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

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

290 
by (intro map_poly_idI) simp_all 

291 
finally show ?thesis . 

292 
qed 

293 

294 
lemma content_decompose_fract: 

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

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

297 
proof (cases "p = 0") 

298 
case True 

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

300 
thus ?thesis .. 

301 
next 

302 
case False 

303 
thus ?thesis 

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

305 
qed 

306 

307 

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

309 

310 
lemma lift_prime_elem_poly: 

63633  311 
assumes "prime_elem (c :: 'a :: semidom)" 
312 
shows "prime_elem [:c:]" 

313 
proof (rule prime_elemI) 

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

316 
by (subst (asm) const_poly_dvd_iff) blast 

317 
{ 

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

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

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

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

322 
by (auto intro: le_degree simp: less_Suc_eq_le) 

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

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

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

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

327 

328 
have "c dvd coeff a i" for i 

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

330 
case (base i) 

331 
thus ?case by (simp add: coeff_eq_0) 

332 
next 

333 
case (descend i) 

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

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

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

337 
by (simp add: coeff_mult) 

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

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

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

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

64267  342 
by (subst sum.insert) simp_all 
63498  343 
finally have eq: "c dvd coeff a i * coeff b m + ?S" . 
344 
moreover have "c dvd ?S" 

64267  345 
proof (rule dvd_sum) 
63498  346 
fix k assume k: "k \<in> {..i+m}  {i}" 
347 
show "c dvd coeff a k * coeff b (i + m  k)" 

348 
proof (cases "k < i") 

349 
case False 

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

351 
thus ?thesis by simp 

352 
next 

353 
case True 

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

355 
thus ?thesis by simp 

356 
qed 

357 
qed 

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

359 
by (simp add: dvd_add_left_iff) 

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

63633  361 
by (simp add: prime_elem_dvd_mult_iff) 
63498  362 
qed 
363 
hence "[:c:] dvd a" by (subst const_poly_dvd_iff) blast 

364 
} 

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

63633  366 
qed (insert assms, simp_all add: prime_elem_def one_poly_def) 
63498  367 

368 
lemma prime_elem_const_poly_iff: 

369 
fixes c :: "'a :: semidom" 

63633  370 
shows "prime_elem [:c:] \<longleftrightarrow> prime_elem c" 
63498  371 
proof 
63633  372 
assume A: "prime_elem [:c:]" 
373 
show "prime_elem c" 

374 
proof (rule prime_elemI) 

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

63633  377 
from A and this have "[:c:] dvd [:a:] \<or> [:c:] dvd [:b:]" by (rule prime_elem_dvd_multD) 
63498  378 
thus "c dvd a \<or> c dvd b" by simp 
63633  379 
qed (insert A, auto simp: prime_elem_def is_unit_poly_iff) 
63498  380 
qed (auto intro: lift_prime_elem_poly) 
381 

382 
context 

383 
begin 

384 

385 
private lemma content_1_mult: 

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

387 
assumes "content f = 1" "content g = 1" 

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

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

390 
case False 

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

392 

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

394 
{ 

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

63633  396 
with False have "\<exists>p. p dvd content (f * g) \<and> prime p" 
63498  397 
by (intro prime_divisor_exists) simp_all 
63633  398 
then obtain p where "p dvd content (f * g)" "prime p" by blast 
63498  399 
from \<open>p dvd content (f * g)\<close> have "[:p:] dvd f * g" 
400 
by (simp add: const_poly_dvd_iff_dvd_content) 

63633  401 
moreover from \<open>prime p\<close> have "prime_elem [:p:]" by (simp add: lift_prime_elem_poly) 
63498  402 
ultimately have "[:p:] dvd f \<or> [:p:] dvd g" 
63633  403 
by (simp add: prime_elem_dvd_mult_iff) 
63498  404 
with assms have "is_unit p" by (simp add: const_poly_dvd_iff_dvd_content) 
63633  405 
with \<open>prime p\<close> have False by simp 
63498  406 
} 
407 
hence "is_unit (content (f * g))" by blast 

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

409 
thus ?thesis by simp 

410 
qed (insert assms, auto) 

411 

412 
lemma content_mult: 

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

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

415 
proof  

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

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

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

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

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

421 
finally show ?thesis by simp 

422 
qed 

423 

424 
lemma primitive_part_mult: 

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

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

427 
proof  

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

429 
by (simp add: primitive_part_def div_const_poly_conv_map_poly) 

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

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

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

433 
by (simp add: primitive_part_def div_const_poly_conv_map_poly) 

434 
finally show ?thesis . 

435 
qed 

436 

437 
lemma primitive_part_smult: 

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

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

440 
proof  

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

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

443 
by (subst primitive_part_mult) simp_all 

444 
finally show ?thesis . 

445 
qed 

446 

447 
lemma primitive_part_dvd_primitive_partI [intro]: 

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

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

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

451 

63830  452 
lemma content_prod_mset: 
63498  453 
fixes A :: "'a :: {factorial_semiring, semiring_Gcd} poly multiset" 
63830  454 
shows "content (prod_mset A) = prod_mset (image_mset content A)" 
63498  455 
by (induction A) (simp_all add: content_mult mult_ac) 
456 

457 
lemma fract_poly_dvdD: 

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

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

460 
shows "p dvd q" 

461 
proof  

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

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

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

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

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

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

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

469 
also note eq' 

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

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

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

473 
thus ?thesis by (rule dvdI) 

474 
qed 

475 

476 
lemma content_prod_eq_1_iff: 

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

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

479 
proof safe 

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

481 
{ 

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

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

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

485 
hence "content p = 1" by simp 

486 
} note B = this 

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

488 
by (simp_all add: content_mult mult_ac) 

489 
qed (auto simp: content_mult) 

490 

491 
end 

492 

493 

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

495 

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

496 
definition unit_factor_field_poly :: "'a :: field poly \<Rightarrow> 'a poly" where 
63498  497 
"unit_factor_field_poly p = [:lead_coeff p:]" 
498 

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

499 
definition normalize_field_poly :: "'a :: field poly \<Rightarrow> 'a poly" where 
63498  500 
"normalize_field_poly p = smult (inverse (lead_coeff p)) p" 
501 

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

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

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

505 
lemma dvd_field_poly: "dvd.dvd (op * :: 'a :: field poly \<Rightarrow> _) = op dvd" 
64784
5cb5e7ecb284
reshaped euclidean semiring into hierarchy of euclidean semirings culminating in uniquely determined euclidean divion
haftmann
parents:
64591
diff
changeset

506 
by (intro ext) (simp_all add: dvd.dvd_def dvd_def) 
63498  507 

508 
interpretation field_poly: 

64784
5cb5e7ecb284
reshaped euclidean semiring into hierarchy of euclidean semirings culminating in uniquely determined euclidean divion
haftmann
parents:
64591
diff
changeset

509 
unique_euclidean_ring where zero = "0 :: 'a :: field poly" 
64164
38c407446400
separate type class for arbitrary quotient and remainder partitions
haftmann
parents:
63954
diff
changeset

510 
and one = 1 and plus = plus and uminus = uminus and minus = minus 
38c407446400
separate type class for arbitrary quotient and remainder partitions
haftmann
parents:
63954
diff
changeset

511 
and times = times 
38c407446400
separate type class for arbitrary quotient and remainder partitions
haftmann
parents:
63954
diff
changeset

512 
and normalize = normalize_field_poly and unit_factor = unit_factor_field_poly 
38c407446400
separate type class for arbitrary quotient and remainder partitions
haftmann
parents:
63954
diff
changeset

513 
and euclidean_size = euclidean_size_field_poly 
64784
5cb5e7ecb284
reshaped euclidean semiring into hierarchy of euclidean semirings culminating in uniquely determined euclidean divion
haftmann
parents:
64591
diff
changeset

514 
and uniqueness_constraint = top 
64164
38c407446400
separate type class for arbitrary quotient and remainder partitions
haftmann
parents:
63954
diff
changeset

515 
and divide = divide and modulo = modulo 
63498  516 
proof (standard, unfold dvd_field_poly) 
517 
fix p :: "'a poly" 

518 
show "unit_factor_field_poly p * normalize_field_poly p = p" 

519 
by (cases "p = 0") 

64794  520 
(simp_all add: unit_factor_field_poly_def normalize_field_poly_def) 
63498  521 
next 
522 
fix p :: "'a poly" assume "is_unit p" 

64848
c50db2128048
slightly generalized type class hierarchy concerning unit factors, to allow for lean polynomial normalization
haftmann
parents:
64795
diff
changeset

523 
then show "unit_factor_field_poly p = p" 
c50db2128048
slightly generalized type class hierarchy concerning unit factors, to allow for lean polynomial normalization
haftmann
parents:
64795
diff
changeset

524 
by (elim is_unit_polyE) (auto simp: unit_factor_field_poly_def monom_0 one_poly_def field_simps) 
63498  525 
next 
526 
fix p :: "'a poly" assume "p \<noteq> 0" 

527 
thus "is_unit (unit_factor_field_poly p)" 

64794  528 
by (simp add: unit_factor_field_poly_def is_unit_pCons_iff) 
64784
5cb5e7ecb284
reshaped euclidean semiring into hierarchy of euclidean semirings culminating in uniquely determined euclidean divion
haftmann
parents:
64591
diff
changeset

529 
next 
5cb5e7ecb284
reshaped euclidean semiring into hierarchy of euclidean semirings culminating in uniquely determined euclidean divion
haftmann
parents:
64591
diff
changeset

530 
fix p q s :: "'a poly" assume "s \<noteq> 0" 
5cb5e7ecb284
reshaped euclidean semiring into hierarchy of euclidean semirings culminating in uniquely determined euclidean divion
haftmann
parents:
64591
diff
changeset

531 
moreover assume "euclidean_size_field_poly p < euclidean_size_field_poly q" 
5cb5e7ecb284
reshaped euclidean semiring into hierarchy of euclidean semirings culminating in uniquely determined euclidean divion
haftmann
parents:
64591
diff
changeset

532 
ultimately show "euclidean_size_field_poly (p * s) < euclidean_size_field_poly (q * s)" 
5cb5e7ecb284
reshaped euclidean semiring into hierarchy of euclidean semirings culminating in uniquely determined euclidean divion
haftmann
parents:
64591
diff
changeset

533 
by (auto simp add: euclidean_size_field_poly_def degree_mult_eq) 
5cb5e7ecb284
reshaped euclidean semiring into hierarchy of euclidean semirings culminating in uniquely determined euclidean divion
haftmann
parents:
64591
diff
changeset

534 
next 
5cb5e7ecb284
reshaped euclidean semiring into hierarchy of euclidean semirings culminating in uniquely determined euclidean divion
haftmann
parents:
64591
diff
changeset

535 
fix p q r :: "'a poly" assume "p \<noteq> 0" 
5cb5e7ecb284
reshaped euclidean semiring into hierarchy of euclidean semirings culminating in uniquely determined euclidean divion
haftmann
parents:
64591
diff
changeset

536 
moreover assume "euclidean_size_field_poly r < euclidean_size_field_poly p" 
5cb5e7ecb284
reshaped euclidean semiring into hierarchy of euclidean semirings culminating in uniquely determined euclidean divion
haftmann
parents:
64591
diff
changeset

537 
ultimately show "(q * p + r) div p = q" 
5cb5e7ecb284
reshaped euclidean semiring into hierarchy of euclidean semirings culminating in uniquely determined euclidean divion
haftmann
parents:
64591
diff
changeset

538 
by (cases "r = 0") 
5cb5e7ecb284
reshaped euclidean semiring into hierarchy of euclidean semirings culminating in uniquely determined euclidean divion
haftmann
parents:
64591
diff
changeset

539 
(auto simp add: unit_factor_field_poly_def euclidean_size_field_poly_def div_poly_less) 
63498  540 
qed (auto simp: unit_factor_field_poly_def normalize_field_poly_def lead_coeff_mult 
64242
93c6f0da5c70
more standardized theorem names for facts involving the div and mod identity
haftmann
parents:
64240
diff
changeset

541 
euclidean_size_field_poly_def Rings.div_mult_mod_eq intro!: degree_mod_less' degree_mult_right_le) 
63498  542 

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

543 
lemma field_poly_irreducible_imp_prime: 
63498  544 
assumes "irreducible (p :: 'a :: field poly)" 
63633  545 
shows "prime_elem p" 
63498  546 
proof  
547 
have A: "class.comm_semiring_1 op * 1 op + (0 :: 'a poly)" .. 

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

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

63498  551 
qed 
552 

63830  553 
lemma field_poly_prod_mset_prime_factorization: 
63498  554 
assumes "(x :: 'a :: field poly) \<noteq> 0" 
63830  555 
shows "prod_mset (field_poly.prime_factorization x) = normalize_field_poly x" 
63498  556 
proof  
557 
have A: "class.comm_monoid_mult op * (1 :: 'a poly)" .. 

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

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

63498  561 
qed 
562 

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

563 
lemma field_poly_in_prime_factorization_imp_prime: 
63498  564 
assumes "(p :: 'a :: field poly) \<in># field_poly.prime_factorization x" 
63633  565 
shows "prime_elem p" 
63498  566 
proof  
567 
have A: "class.comm_semiring_1 op * 1 op + (0 :: 'a poly)" .. 

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

64848
c50db2128048
slightly generalized type class hierarchy concerning unit factors, to allow for lean polynomial normalization
haftmann
parents:
64795
diff
changeset

569 
unit_factor_field_poly normalize_field_poly" .. 
63905  570 
from field_poly.in_prime_factors_imp_prime [of p x] assms 
63633  571 
show ?thesis unfolding prime_elem_def dvd_field_poly 
572 
comm_semiring_1.prime_elem_def[OF A] normalization_semidom.prime_def[OF B] by blast 

63498  573 
qed 
574 

575 

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

577 

578 
lemma nonconst_poly_irreducible_iff: 

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

580 
assumes "degree p \<noteq> 0" 

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

582 
proof safe 

583 
assume p: "irreducible p" 

584 

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

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

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

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

589 
proof 

590 
assume "p' dvd 1" 

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

592 
with assms show False by contradiction 

593 
qed 

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

595 

596 
show "irreducible (map_poly to_fract p)" 

597 
proof (rule irreducibleI) 

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

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

600 
next 

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

602 
proof 

603 
assume "is_unit (map_poly to_fract p)" 

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

605 
by (auto simp: is_unit_poly_iff) 

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

607 
with assms show False by contradiction 

608 
qed 

609 
next 

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

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

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

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

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

615 
by (simp add: q r) 

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

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

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

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

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

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

622 

623 
note eq 

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

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

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

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

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

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

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

631 
by (auto simp add: is_unit_smult_iff dvd_field_iff nz) 

632 
qed 

633 

634 
next 

635 

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

637 
show "irreducible p" 

638 
proof (rule irreducibleI) 

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

640 
next 

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

642 
by (auto simp: irreducible_def dest: fract_poly_is_unit) 

643 
next 

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

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

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

647 
by (rule irreducibleD) 

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

649 
by (auto simp: content_prod_eq_1_iff is_unit_fract_poly_iff) 

650 
qed 

651 
qed 

652 

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

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

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

655 

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

658 
assumes "irreducible p" 

63633  659 
shows "prime_elem p" 
63498  660 
proof (cases "degree p = 0") 
661 
case True 

662 
with assms show ?thesis 

663 
by (auto simp: prime_elem_const_poly_iff irreducible_const_poly_iff 

63633  664 
intro!: irreducible_imp_prime_elem elim!: degree_eq_zeroE) 
63498  665 
next 
666 
case False 

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

668 
by (simp_all add: nonconst_poly_irreducible_iff) 

63633  669 
from irred have prime: "prime_elem (fract_poly p)" by (rule field_poly_irreducible_imp_prime) 
63498  670 
show ?thesis 
63633  671 
proof (rule prime_elemI) 
63498  672 
fix q r assume "p dvd q * r" 
673 
hence "fract_poly p dvd fract_poly (q * r)" by (rule fract_poly_dvd) 

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

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

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

679 
qed 

680 

681 

682 
lemma degree_primitive_part_fract [simp]: 

683 
"degree (primitive_part_fract p) = degree p" 

684 
proof  

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

686 
by (simp add: content_times_primitive_part_fract) 

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

688 
by (auto simp: degree_map_poly) 

689 
finally show ?thesis .. 

690 
qed 

691 

692 
lemma irreducible_primitive_part_fract: 

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

694 
assumes "irreducible p" 

695 
shows "irreducible (primitive_part_fract p)" 

696 
proof  

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

698 
by (intro notI) 

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

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

701 

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

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

704 
by (simp add: content_times_primitive_part_fract) 

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

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

707 
finally show ?thesis using deg 

708 
by (simp add: nonconst_poly_irreducible_iff) 

709 
qed 

710 

63633  711 
lemma prime_elem_primitive_part_fract: 
63498  712 
fixes p :: "'a :: {idom_divide, ring_gcd, factorial_semiring, semiring_Gcd} fract poly" 
63633  713 
shows "irreducible p \<Longrightarrow> prime_elem (primitive_part_fract p)" 
63498  714 
by (intro irreducible_imp_prime_poly irreducible_primitive_part_fract) 
715 

716 
lemma irreducible_linear_field_poly: 

717 
fixes a b :: "'a::field" 

718 
assumes "b \<noteq> 0" 

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

720 
proof (rule irreducibleI) 

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

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

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

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

727 
qed (insert assms, auto simp: is_unit_poly_iff) 

728 

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

63498  731 
by (rule field_poly_irreducible_imp_prime, rule irreducible_linear_field_poly) 
732 

733 
lemma irreducible_linear_poly: 

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

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

736 
by (auto intro!: irreducible_linear_field_poly 

737 
simp: nonconst_poly_irreducible_iff content_def map_poly_pCons) 

738 

63633  739 
lemma prime_elem_linear_poly: 
63498  740 
fixes a b :: "'a::{idom_divide,ring_gcd,factorial_semiring,semiring_Gcd}" 
63633  741 
shows "b \<noteq> 0 \<Longrightarrow> coprime a b \<Longrightarrow> prime_elem [:a,b:]" 
63498  742 
by (rule irreducible_imp_prime_poly, rule irreducible_linear_poly) 
743 

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

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

745 

64591
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64267
diff
changeset

746 

63498  747 
subsection \<open>Prime factorisation of polynomials\<close> 
748 

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

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

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

751 

63498  752 
private lemma poly_prime_factorization_exists_content_1: 
753 
fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} poly" 

754 
assumes "p \<noteq> 0" "content p = 1" 

63830  755 
shows "\<exists>A. (\<forall>p. p \<in># A \<longrightarrow> prime_elem p) \<and> prod_mset A = normalize p" 
63498  756 
proof  
757 
let ?P = "field_poly.prime_factorization (fract_poly p)" 

63830  758 
define c where "c = prod_mset (image_mset fract_content ?P)" 
63498  759 
define c' where "c' = c * to_fract (lead_coeff p)" 
63830  760 
define e where "e = prod_mset (image_mset primitive_part_fract ?P)" 
63498  761 
define A where "A = image_mset (normalize \<circ> primitive_part_fract) ?P" 
762 
have "content e = (\<Prod>x\<in>#field_poly.prime_factorization (map_poly to_fract p). 

763 
content (primitive_part_fract x))" 

63830  764 
by (simp add: e_def content_prod_mset multiset.map_comp o_def) 
63498  765 
also have "image_mset (\<lambda>x. content (primitive_part_fract x)) ?P = image_mset (\<lambda>_. 1) ?P" 
766 
by (intro image_mset_cong content_primitive_part_fract) auto 

64591
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64267
diff
changeset

767 
finally have content_e: "content e = 1" 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64267
diff
changeset

768 
by simp 
63498  769 

770 
have "fract_poly p = unit_factor_field_poly (fract_poly p) * 

771 
normalize_field_poly (fract_poly p)" by simp 

772 
also have "unit_factor_field_poly (fract_poly p) = [:to_fract (lead_coeff p):]" 

64794  773 
by (simp add: unit_factor_field_poly_def monom_0 degree_map_poly coeff_map_poly) 
63830  774 
also from assms have "normalize_field_poly (fract_poly p) = prod_mset ?P" 
775 
by (subst field_poly_prod_mset_prime_factorization) simp_all 

776 
also have "\<dots> = prod_mset (image_mset id ?P)" by simp 

63498  777 
also have "image_mset id ?P = 
778 
image_mset (\<lambda>x. [:fract_content x:] * fract_poly (primitive_part_fract x)) ?P" 

779 
by (intro image_mset_cong) (auto simp: content_times_primitive_part_fract) 

63830  780 
also have "prod_mset \<dots> = smult c (fract_poly e)" 
64591
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64267
diff
changeset

781 
by (subst prod_mset.distrib) (simp_all add: prod_mset_fract_poly prod_mset_const_poly c_def e_def) 
63498  782 
also have "[:to_fract (lead_coeff p):] * \<dots> = smult c' (fract_poly e)" 
783 
by (simp add: c'_def) 

784 
finally have eq: "fract_poly p = smult c' (fract_poly e)" . 

785 
also obtain b where b: "c' = to_fract b" "is_unit b" 

786 
proof  

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

788 
from ab(2) have "content (smult a p) = content (smult b e)" by (simp only: ) 

789 
with assms content_e have "a = normalize b" by (simp add: ab(4)) 

790 
with ab have ab': "a = 1" "is_unit b" by (simp_all add: normalize_1_iff) 

791 
with ab ab' have "c' = to_fract b" by auto 

792 
from this and \<open>is_unit b\<close> show ?thesis by (rule that) 

793 
qed 

794 
hence "smult c' (fract_poly e) = fract_poly (smult b e)" by simp 

795 
finally have "p = smult b e" by (simp only: fract_poly_eq_iff) 

796 
hence "p = [:b:] * e" by simp 

797 
with b have "normalize p = normalize e" 

798 
by (simp only: normalize_mult) (simp add: is_unit_normalize is_unit_poly_iff) 

63830  799 
also have "normalize e = prod_mset A" 
800 
by (simp add: multiset.map_comp e_def A_def normalize_prod_mset) 

801 
finally have "prod_mset A = normalize p" .. 

63498  802 

63633  803 
have "prime_elem p" if "p \<in># A" for p 
804 
using that by (auto simp: A_def prime_elem_primitive_part_fract prime_elem_imp_irreducible 

63498  805 
dest!: field_poly_in_prime_factorization_imp_prime ) 
63830  806 
from this and \<open>prod_mset A = normalize p\<close> show ?thesis 
63498  807 
by (intro exI[of _ A]) blast 
808 
qed 

809 

810 
lemma poly_prime_factorization_exists: 

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

812 
assumes "p \<noteq> 0" 

63830  813 
shows "\<exists>A. (\<forall>p. p \<in># A \<longrightarrow> prime_elem p) \<and> prod_mset A = normalize p" 
63498  814 
proof  
815 
define B where "B = image_mset (\<lambda>x. [:x:]) (prime_factorization (content p))" 

63830  816 
have "\<exists>A. (\<forall>p. p \<in># A \<longrightarrow> prime_elem p) \<and> prod_mset A = normalize (primitive_part p)" 
63498  817 
by (rule poly_prime_factorization_exists_content_1) (insert assms, simp_all) 
818 
then guess A by (elim exE conjE) note A = this 

63830  819 
moreover from assms have "prod_mset B = [:content p:]" 
820 
by (simp add: B_def prod_mset_const_poly prod_mset_prime_factorization) 

63633  821 
moreover have "\<forall>p. p \<in># B \<longrightarrow> prime_elem p" 
63905  822 
by (auto simp: B_def intro!: lift_prime_elem_poly dest: in_prime_factors_imp_prime) 
63498  823 
ultimately show ?thesis by (intro exI[of _ "B + A"]) auto 
824 
qed 

825 

826 
end 

827 

828 

829 
subsection \<open>Typeclass instances\<close> 

830 

831 
instance poly :: (factorial_ring_gcd) factorial_semiring 

832 
by standard (rule poly_prime_factorization_exists) 

833 

834 
instantiation poly :: (factorial_ring_gcd) factorial_ring_gcd 

835 
begin 

836 

837 
definition gcd_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly" where 

838 
[code del]: "gcd_poly = gcd_factorial" 

839 

840 
definition lcm_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly" where 

841 
[code del]: "lcm_poly = lcm_factorial" 

842 

843 
definition Gcd_poly :: "'a poly set \<Rightarrow> 'a poly" where 

844 
[code del]: "Gcd_poly = Gcd_factorial" 

845 

846 
definition Lcm_poly :: "'a poly set \<Rightarrow> 'a poly" where 

847 
[code del]: "Lcm_poly = Lcm_factorial" 

848 

849 
instance by standard (simp_all add: gcd_poly_def lcm_poly_def Gcd_poly_def Lcm_poly_def) 

850 

851 
end 

852 

64784
5cb5e7ecb284
reshaped euclidean semiring into hierarchy of euclidean semirings culminating in uniquely determined euclidean divion
haftmann
parents:
64591
diff
changeset

853 
instantiation poly :: ("{field,factorial_ring_gcd}") unique_euclidean_ring 
63498  854 
begin 
855 

64784
5cb5e7ecb284
reshaped euclidean semiring into hierarchy of euclidean semirings culminating in uniquely determined euclidean divion
haftmann
parents:
64591
diff
changeset

856 
definition euclidean_size_poly :: "'a poly \<Rightarrow> nat" 
5cb5e7ecb284
reshaped euclidean semiring into hierarchy of euclidean semirings culminating in uniquely determined euclidean divion
haftmann
parents:
64591
diff
changeset

857 
where "euclidean_size_poly p = (if p = 0 then 0 else 2 ^ degree p)" 
5cb5e7ecb284
reshaped euclidean semiring into hierarchy of euclidean semirings culminating in uniquely determined euclidean divion
haftmann
parents:
64591
diff
changeset

858 

5cb5e7ecb284
reshaped euclidean semiring into hierarchy of euclidean semirings culminating in uniquely determined euclidean divion
haftmann
parents:
64591
diff
changeset

859 
definition uniqueness_constraint_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> bool" 
5cb5e7ecb284
reshaped euclidean semiring into hierarchy of euclidean semirings culminating in uniquely determined euclidean divion
haftmann
parents:
64591
diff
changeset

860 
where [simp]: "uniqueness_constraint_poly = top" 
63498  861 

862 
instance 

64784
5cb5e7ecb284
reshaped euclidean semiring into hierarchy of euclidean semirings culminating in uniquely determined euclidean divion
haftmann
parents:
64591
diff
changeset

863 
by standard 
5cb5e7ecb284
reshaped euclidean semiring into hierarchy of euclidean semirings culminating in uniquely determined euclidean divion
haftmann
parents:
64591
diff
changeset

864 
(auto simp: euclidean_size_poly_def Rings.div_mult_mod_eq div_poly_less degree_mult_eq intro!: degree_mod_less' degree_mult_right_le 
5cb5e7ecb284
reshaped euclidean semiring into hierarchy of euclidean semirings culminating in uniquely determined euclidean divion
haftmann
parents:
64591
diff
changeset

865 
split: if_splits) 
5cb5e7ecb284
reshaped euclidean semiring into hierarchy of euclidean semirings culminating in uniquely determined euclidean divion
haftmann
parents:
64591
diff
changeset

866 

63498  867 
end 
868 

869 
instance poly :: ("{field,factorial_ring_gcd}") euclidean_ring_gcd 

64786
340db65fd2c1
reworked to provide auxiliary operations Euclidean_Algorithm.* to instantiate gcd etc. for euclidean rings
haftmann
parents:
64784
diff
changeset

870 
by (rule euclidean_ring_gcd_class.intro, rule factorial_euclidean_semiring_gcdI) 
340db65fd2c1
reworked to provide auxiliary operations Euclidean_Algorithm.* to instantiate gcd etc. for euclidean rings
haftmann
parents:
64784
diff
changeset

871 
standard 
63498  872 

873 

874 
subsection \<open>Polynomial GCD\<close> 

875 

876 
lemma gcd_poly_decompose: 

877 
fixes p q :: "'a :: factorial_ring_gcd poly" 

878 
shows "gcd p q = 

879 
smult (gcd (content p) (content q)) (gcd (primitive_part p) (primitive_part q))" 

880 
proof (rule sym, rule gcdI) 

881 
have "[:gcd (content p) (content q):] * gcd (primitive_part p) (primitive_part q) dvd 

882 
[:content p:] * primitive_part p" by (intro mult_dvd_mono) simp_all 

883 
thus "smult (gcd (content p) (content q)) (gcd (primitive_part p) (primitive_part q)) dvd p" 

884 
by simp 

885 
next 

886 
have "[:gcd (content p) (content q):] * gcd (primitive_part p) (primitive_part q) dvd 

887 
[:content q:] * primitive_part q" by (intro mult_dvd_mono) simp_all 

888 
thus "smult (gcd (content p) (content q)) (gcd (primitive_part p) (primitive_part q)) dvd q" 

889 
by simp 

890 
next 

891 
fix d assume "d dvd p" "d dvd q" 

892 
hence "[:content d:] * primitive_part d dvd 

893 
[:gcd (content p) (content q):] * gcd (primitive_part p) (primitive_part q)" 

894 
by (intro mult_dvd_mono) auto 

895 
thus "d dvd smult (gcd (content p) (content q)) (gcd (primitive_part p) (primitive_part q))" 

896 
by simp 

897 
qed (auto simp: normalize_smult) 

898 

899 

900 
lemma gcd_poly_pseudo_mod: 

901 
fixes p q :: "'a :: factorial_ring_gcd poly" 

902 
assumes nz: "q \<noteq> 0" and prim: "content p = 1" "content q = 1" 

903 
shows "gcd p q = gcd q (primitive_part (pseudo_mod p q))" 

904 
proof  

905 
define r s where "r = fst (pseudo_divmod p q)" and "s = snd (pseudo_divmod p q)" 

906 
define a where "a = [:coeff q (degree q) ^ (Suc (degree p)  degree q):]" 

907 
have [simp]: "primitive_part a = unit_factor a" 

908 
by (simp add: a_def unit_factor_poly_def unit_factor_power monom_0) 

909 
from nz have [simp]: "a \<noteq> 0" by (auto simp: a_def) 

910 

911 
have rs: "pseudo_divmod p q = (r, s)" by (simp add: r_def s_def) 

912 
have "gcd (q * r + s) q = gcd q s" 

913 
using gcd_add_mult[of q r s] by (simp add: gcd.commute add_ac mult_ac) 

914 
with pseudo_divmod(1)[OF nz rs] 

915 
have "gcd (p * a) q = gcd q s" by (simp add: a_def) 

916 
also from prim have "gcd (p * a) q = gcd p q" 

917 
by (subst gcd_poly_decompose) 

918 
(auto simp: primitive_part_mult gcd_mult_unit1 primitive_part_prim 

919 
simp del: mult_pCons_right ) 

920 
also from prim have "gcd q s = gcd q (primitive_part s)" 

921 
by (subst gcd_poly_decompose) (simp_all add: primitive_part_prim) 

922 
also have "s = pseudo_mod p q" by (simp add: s_def pseudo_mod_def) 

923 
finally show ?thesis . 

924 
qed 

925 

926 
lemma degree_pseudo_mod_less: 

927 
assumes "q \<noteq> 0" "pseudo_mod p q \<noteq> 0" 

928 
shows "degree (pseudo_mod p q) < degree q" 

929 
using pseudo_mod(2)[of q p] assms by auto 

930 

931 
function gcd_poly_code_aux :: "'a :: factorial_ring_gcd poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly" where 

932 
"gcd_poly_code_aux p q = 

933 
(if q = 0 then normalize p else gcd_poly_code_aux q (primitive_part (pseudo_mod p q)))" 

934 
by auto 

935 
termination 

936 
by (relation "measure ((\<lambda>p. if p = 0 then 0 else Suc (degree p)) \<circ> snd)") 

64164
38c407446400
separate type class for arbitrary quotient and remainder partitions
haftmann
parents:
63954
diff
changeset

937 
(auto simp: degree_pseudo_mod_less) 
63498  938 

939 
declare gcd_poly_code_aux.simps [simp del] 

940 

941 
lemma gcd_poly_code_aux_correct: 

942 
assumes "content p = 1" "q = 0 \<or> content q = 1" 

943 
shows "gcd_poly_code_aux p q = gcd p q" 

944 
using assms 

945 
proof (induction p q rule: gcd_poly_code_aux.induct) 

946 
case (1 p q) 

947 
show ?case 

948 
proof (cases "q = 0") 

949 
case True 

950 
thus ?thesis by (subst gcd_poly_code_aux.simps) auto 

951 
next 

952 
case False 

953 
hence "gcd_poly_code_aux p q = gcd_poly_code_aux q (primitive_part (pseudo_mod p q))" 

954 
by (subst gcd_poly_code_aux.simps) simp_all 

955 
also from "1.prems" False 

956 
have "primitive_part (pseudo_mod p q) = 0 \<or> 

957 
content (primitive_part (pseudo_mod p q)) = 1" 

958 
by (cases "pseudo_mod p q = 0") auto 

959 
with "1.prems" False 

960 
have "gcd_poly_code_aux q (primitive_part (pseudo_mod p q)) = 

961 
gcd q (primitive_part (pseudo_mod p q))" 

962 
by (intro 1) simp_all 

963 
also from "1.prems" False 

964 
have "\<dots> = gcd p q" by (intro gcd_poly_pseudo_mod [symmetric]) auto 

965 
finally show ?thesis . 

966 
qed 

967 
qed 

968 

969 
definition gcd_poly_code 

970 
:: "'a :: factorial_ring_gcd poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly" 

971 
where "gcd_poly_code p q = 

972 
(if p = 0 then normalize q else if q = 0 then normalize p else 

973 
smult (gcd (content p) (content q)) 

974 
(gcd_poly_code_aux (primitive_part p) (primitive_part q)))" 

975 

64591
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64267
diff
changeset

976 
lemma gcd_poly_code [code]: "gcd p q = gcd_poly_code p q" 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64267
diff
changeset

977 
by (simp add: gcd_poly_code_def gcd_poly_code_aux_correct gcd_poly_decompose [symmetric]) 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64267
diff
changeset

978 

63498  979 
lemma lcm_poly_code [code]: 
980 
fixes p q :: "'a :: factorial_ring_gcd poly" 

981 
shows "lcm p q = normalize (p * q) div gcd p q" 

64591
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64267
diff
changeset

982 
by (fact lcm_gcd) 
63498  983 

64850  984 
lemmas Gcd_poly_set_eq_fold [code] = Gcd_set_eq_fold [where ?'a = "'a :: factorial_ring_gcd poly"] 
985 
lemmas Lcm_poly_set_eq_fold [code] = Lcm_set_eq_fold [where ?'a = "'a :: factorial_ring_gcd poly"] 

64860  986 

64591
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64267
diff
changeset

987 
text \<open>Example: 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64267
diff
changeset

988 
@{lemma "Lcm {[:1, 2, 3:], [:2, 3, 4:]} = [:[:2:], [:7:], [:16:], [:17:], [:12 :: int:]:]" by eval} 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64267
diff
changeset

989 
\<close> 
63498  990 

63764  991 
end 