author  haftmann 
Wed, 05 Apr 2017 13:47:40 +0200  
changeset 65389  6f9c6ae27984 
parent 65366  10ca63a18e56 
child 65390  83586780598b 
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 

65366  12 
Polynomial 
13 
Normalized_Fraction 

14 
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 

65389  19 
lemma prod_mset_const_poly: " (\<Prod>x\<in>#A. [:f x:]) = [:prod_mset (image_mset f A):]" 
20 
by (induct A) (simp_all add: one_poly_def ac_simps) 

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))" 

65389  172 
by (induct A) (simp_all add: one_poly_def ac_simps) 
63498  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" 

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

63498  180 
from A show "content p = 1" 
181 
by (auto simp: is_unit_poly_iff normalize_1_iff) 

182 
next 

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

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

185 
{ 

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

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

188 
also note c 

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

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

191 
} 

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

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

194 
qed 

195 

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

197 
using fract_poly_dvd[of p 1] by simp 

198 

199 
lemma fract_poly_smult_eqE: 

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

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

202 
obtains a b 

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

204 
proof  

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

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

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

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

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

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

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

212 
normalize_snd_quot_of_fract Fract_conv_to_fract [symmetric]) 

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

214 
qed 

215 

216 

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

218 

219 
abbreviation (input) Lcm_coeff_denoms 

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

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

222 

223 
definition fract_content :: 

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

225 
"fract_content p = 

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

227 

228 
definition primitive_part_fract :: 

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

230 
"primitive_part_fract p = 

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

232 

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

234 
by (simp add: primitive_part_fract_def) 

235 

236 
lemma fract_content_eq_0_iff [simp]: 

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

238 
unfolding fract_content_def Let_def Zero_fract_def 

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

240 

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

242 
unfolding primitive_part_fract_def 

243 
by (rule content_primitive_part) 

244 
(auto simp: primitive_part_fract_def map_poly_eq_0_iff Lcm_0_iff) 

245 

246 
lemma content_times_primitive_part_fract: 

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

248 
proof  

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

250 
have "fract_poly p' = 

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

252 
unfolding primitive_part_fract_def p'_def 

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

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

255 
proof (intro map_poly_idI, unfold o_apply) 

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

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

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

259 
note c(2) 

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

261 
by simp 

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

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

264 
unfolding to_fract_def by (subst mult_fract) simp_all 

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

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

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

268 
by (rule to_fract_quot_of_fract) 

269 
qed 

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

271 
by (rule content_times_primitive_part [symmetric]) 

272 
also have "primitive_part p' = primitive_part_fract p" 

273 
by (simp add: primitive_part_fract_def p'_def) 

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

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

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

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

278 
thus ?thesis 

279 
by (subst (asm) smult_eq_iff) 

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

281 
qed 

282 

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

284 
proof  

285 
have "Lcm_coeff_denoms (fract_poly p) = 1" 

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

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

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

291 
by (intro map_poly_idI) simp_all 

292 
finally show ?thesis . 

293 
qed 

294 

295 
lemma content_decompose_fract: 

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

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

298 
proof (cases "p = 0") 

299 
case True 

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

301 
thus ?thesis .. 

302 
next 

303 
case False 

304 
thus ?thesis 

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

306 
qed 

307 

308 

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

310 

311 
lemma lift_prime_elem_poly: 

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

314 
proof (rule prime_elemI) 

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

317 
by (subst (asm) const_poly_dvd_iff) blast 

318 
{ 

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

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

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

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

323 
by (auto intro: le_degree simp: less_Suc_eq_le) 

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

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

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

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

328 

329 
have "c dvd coeff a i" for i 

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

331 
case (base i) 

332 
thus ?case by (simp add: coeff_eq_0) 

333 
next 

334 
case (descend i) 

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

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

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

338 
by (simp add: coeff_mult) 

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

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

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

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

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

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

349 
proof (cases "k < i") 

350 
case False 

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

352 
thus ?thesis by simp 

353 
next 

354 
case True 

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

356 
thus ?thesis by simp 

357 
qed 

358 
qed 

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

360 
by (simp add: dvd_add_left_iff) 

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

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

365 
} 

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

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

369 
lemma prime_elem_const_poly_iff: 

370 
fixes c :: "'a :: semidom" 

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

375 
proof (rule prime_elemI) 

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

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

383 
context 

384 
begin 

385 

386 
private lemma content_1_mult: 

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

388 
assumes "content f = 1" "content g = 1" 

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

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

391 
case False 

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

393 

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

395 
{ 

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

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

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

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

410 
thus ?thesis by simp 

411 
qed (insert assms, auto) 

412 

413 
lemma content_mult: 

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

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

416 
proof  

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

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

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

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

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

422 
finally show ?thesis by simp 

423 
qed 

424 

425 
lemma primitive_part_mult: 

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

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

428 
proof  

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

430 
by (simp add: primitive_part_def div_const_poly_conv_map_poly) 

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

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

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

434 
by (simp add: primitive_part_def div_const_poly_conv_map_poly) 

435 
finally show ?thesis . 

436 
qed 

437 

438 
lemma primitive_part_smult: 

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

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

441 
proof  

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

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

444 
by (subst primitive_part_mult) simp_all 

445 
finally show ?thesis . 

446 
qed 

447 

448 
lemma primitive_part_dvd_primitive_partI [intro]: 

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

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

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

452 

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

458 
lemma fract_poly_dvdD: 

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

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

461 
shows "p dvd q" 

462 
proof  

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

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

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

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

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

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

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

470 
also note eq' 

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

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

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

474 
thus ?thesis by (rule dvdI) 

475 
qed 

476 

477 
lemma content_prod_eq_1_iff: 

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

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

480 
proof safe 

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

482 
{ 

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

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

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

486 
hence "content p = 1" by simp 

487 
} note B = this 

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

489 
by (simp_all add: content_mult mult_ac) 

490 
qed (auto simp: content_mult) 

491 

492 
end 

493 

494 

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

496 

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

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

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

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

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

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

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

506 
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

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

509 
interpretation field_poly: 

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

510 
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

511 
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

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

513 
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

514 
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

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

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

519 
show "unit_factor_field_poly p * normalize_field_poly p = p" 

520 
by (cases "p = 0") 

64794  521 
(simp_all add: unit_factor_field_poly_def normalize_field_poly_def) 
63498  522 
next 
523 
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

524 
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

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

528 
thus "is_unit (unit_factor_field_poly p)" 

64794  529 
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

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

531 
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

532 
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

533 
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

534 
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

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

536 
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

537 
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

538 
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

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

540 
(auto simp add: unit_factor_field_poly_def euclidean_size_field_poly_def div_poly_less) 
63498  541 
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

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

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

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

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

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

63498  552 
qed 
553 

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

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

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

63498  562 
qed 
563 

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

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

569 
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

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

63498  574 
qed 
575 

576 

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

578 

579 
lemma nonconst_poly_irreducible_iff: 

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

581 
assumes "degree p \<noteq> 0" 

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

583 
proof safe 

584 
assume p: "irreducible p" 

585 

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

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

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

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

590 
proof 

591 
assume "p' dvd 1" 

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

593 
with assms show False by contradiction 

594 
qed 

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

596 

597 
show "irreducible (map_poly to_fract p)" 

598 
proof (rule irreducibleI) 

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

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

601 
next 

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

603 
proof 

604 
assume "is_unit (map_poly to_fract p)" 

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

606 
by (auto simp: is_unit_poly_iff) 

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

608 
with assms show False by contradiction 

609 
qed 

610 
next 

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

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

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

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

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

616 
by (simp add: q r) 

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

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

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

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

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

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

623 

624 
note eq 

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

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

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

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

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

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

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

632 
by (auto simp add: is_unit_smult_iff dvd_field_iff nz) 

633 
qed 

634 

635 
next 

636 

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

638 
show "irreducible p" 

639 
proof (rule irreducibleI) 

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

641 
next 

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

643 
by (auto simp: irreducible_def dest: fract_poly_is_unit) 

644 
next 

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

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

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

648 
by (rule irreducibleD) 

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

650 
by (auto simp: content_prod_eq_1_iff is_unit_fract_poly_iff) 

651 
qed 

652 
qed 

653 

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

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

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

656 

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

659 
assumes "irreducible p" 

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

663 
with assms show ?thesis 

664 
by (auto simp: prime_elem_const_poly_iff irreducible_const_poly_iff 

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

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

669 
by (simp_all add: nonconst_poly_irreducible_iff) 

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

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

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

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

680 
qed 

681 

682 

683 
lemma degree_primitive_part_fract [simp]: 

684 
"degree (primitive_part_fract p) = degree p" 

685 
proof  

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

687 
by (simp add: content_times_primitive_part_fract) 

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

689 
by (auto simp: degree_map_poly) 

690 
finally show ?thesis .. 

691 
qed 

692 

693 
lemma irreducible_primitive_part_fract: 

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

695 
assumes "irreducible p" 

696 
shows "irreducible (primitive_part_fract p)" 

697 
proof  

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

699 
by (intro notI) 

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

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

702 

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

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

705 
by (simp add: content_times_primitive_part_fract) 

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

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

708 
finally show ?thesis using deg 

709 
by (simp add: nonconst_poly_irreducible_iff) 

710 
qed 

711 

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

717 
lemma irreducible_linear_field_poly: 

718 
fixes a b :: "'a::field" 

719 
assumes "b \<noteq> 0" 

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

721 
proof (rule irreducibleI) 

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

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

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

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

728 
qed (insert assms, auto simp: is_unit_poly_iff) 

729 

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

63498  732 
by (rule field_poly_irreducible_imp_prime, rule irreducible_linear_field_poly) 
733 

734 
lemma irreducible_linear_poly: 

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

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

737 
by (auto intro!: irreducible_linear_field_poly 

738 
simp: nonconst_poly_irreducible_iff content_def map_poly_pCons) 

739 

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

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

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

746 

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

747 

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

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

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

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

752 

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

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

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

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

764 
content (primitive_part_fract x))" 

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

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

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

769 
by simp 
63498  770 

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

772 
normalize_field_poly (fract_poly p)" by simp 

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

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

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

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

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

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

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

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

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

787 
proof  

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

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

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

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

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

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

794 
qed 

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

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

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

798 
with b have "normalize p = normalize e" 

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

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

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

63498  803 

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

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

810 

811 
lemma poly_prime_factorization_exists: 

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

813 
assumes "p \<noteq> 0" 

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

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

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

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

826 

827 
end 

828 

829 

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

831 

832 
instance poly :: (factorial_ring_gcd) factorial_semiring 

833 
by standard (rule poly_prime_factorization_exists) 

834 

835 
instantiation poly :: (factorial_ring_gcd) factorial_ring_gcd 

836 
begin 

837 

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

839 
[code del]: "gcd_poly = gcd_factorial" 

840 

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

842 
[code del]: "lcm_poly = lcm_factorial" 

843 

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

845 
[code del]: "Gcd_poly = Gcd_factorial" 

846 

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

848 
[code del]: "Lcm_poly = Lcm_factorial" 

849 

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

851 

852 
end 

853 

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

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

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

857 
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

858 
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

859 

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

860 
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

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

863 
instance 

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

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

865 
(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

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

867 

63498  868 
end 
869 

870 
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

871 
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

872 
standard 
63498  873 

874 

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

876 

877 
lemma gcd_poly_decompose: 

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

879 
shows "gcd p q = 

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

881 
proof (rule sym, rule gcdI) 

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

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

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

885 
by simp 

886 
next 

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

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

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

890 
by simp 

891 
next 

892 
fix d assume "d dvd p" "d dvd q" 

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

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

895 
by (intro mult_dvd_mono) auto 

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

897 
by simp 

898 
qed (auto simp: normalize_smult) 

899 

900 

901 
lemma gcd_poly_pseudo_mod: 

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

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

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

905 
proof  

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

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

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

909 
by (simp add: a_def unit_factor_poly_def unit_factor_power monom_0) 

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

911 

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

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

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

915 
with pseudo_divmod(1)[OF nz rs] 

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

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

918 
by (subst gcd_poly_decompose) 

919 
(auto simp: primitive_part_mult gcd_mult_unit1 primitive_part_prim 

920 
simp del: mult_pCons_right ) 

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

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

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

924 
finally show ?thesis . 

925 
qed 

926 

927 
lemma degree_pseudo_mod_less: 

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

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

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

931 

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

933 
"gcd_poly_code_aux p q = 

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

935 
by auto 

936 
termination 

937 
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

938 
(auto simp: degree_pseudo_mod_less) 
63498  939 

940 
declare gcd_poly_code_aux.simps [simp del] 

941 

942 
lemma gcd_poly_code_aux_correct: 

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

944 
shows "gcd_poly_code_aux p q = gcd p q" 

945 
using assms 

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

947 
case (1 p q) 

948 
show ?case 

949 
proof (cases "q = 0") 

950 
case True 

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

952 
next 

953 
case False 

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

955 
by (subst gcd_poly_code_aux.simps) simp_all 

956 
also from "1.prems" False 

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

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

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

960 
with "1.prems" False 

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

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

963 
by (intro 1) simp_all 

964 
also from "1.prems" False 

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

966 
finally show ?thesis . 

967 
qed 

968 
qed 

969 

970 
definition gcd_poly_code 

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

972 
where "gcd_poly_code p q = 

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

974 
smult (gcd (content p) (content q)) 

975 
(gcd_poly_code_aux (primitive_part p) (primitive_part q)))" 

976 

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

977 
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

978 
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

979 

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

982 
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

983 
by (fact lcm_gcd) 
63498  984 

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

64860  987 

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

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

989 
@{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

990 
\<close> 
63498  991 

63764  992 
end 