63498
|
1 |
theory Polynomial_Factorial
|
|
2 |
imports
|
|
3 |
Complex_Main
|
|
4 |
Euclidean_Algorithm
|
|
5 |
"~~/src/HOL/Library/Fraction_Field"
|
|
6 |
"~~/src/HOL/Library/Polynomial"
|
|
7 |
"/home/manuel/hg/Linear_Recurrences/Normalized_Fraction"
|
|
8 |
begin
|
|
9 |
|
|
10 |
subsection \<open>Prelude\<close>
|
|
11 |
|
|
12 |
lemma msetprod_mult:
|
|
13 |
"msetprod (image_mset (\<lambda>x. f x * g x) A) = msetprod (image_mset f A) * msetprod (image_mset g A)"
|
|
14 |
by (induction A) (simp_all add: mult_ac)
|
|
15 |
|
|
16 |
lemma msetprod_const: "msetprod (image_mset (\<lambda>_. c) A) = c ^ size A"
|
|
17 |
by (induction A) (simp_all add: mult_ac)
|
|
18 |
|
|
19 |
lemma dvd_field_iff: "x dvd y \<longleftrightarrow> (x = 0 \<longrightarrow> y = (0::'a::field))"
|
|
20 |
proof safe
|
|
21 |
assume "x \<noteq> 0"
|
|
22 |
hence "y = x * (y / x)" by (simp add: field_simps)
|
|
23 |
thus "x dvd y" by (rule dvdI)
|
|
24 |
qed auto
|
|
25 |
|
|
26 |
lemma nat_descend_induct [case_names base descend]:
|
|
27 |
assumes "\<And>k::nat. k > n \<Longrightarrow> P k"
|
|
28 |
assumes "\<And>k::nat. k \<le> n \<Longrightarrow> (\<And>i. i > k \<Longrightarrow> P i) \<Longrightarrow> P k"
|
|
29 |
shows "P m"
|
|
30 |
using assms by induction_schema (force intro!: wf_measure[of "\<lambda>k. Suc n - k"])+
|
|
31 |
|
|
32 |
lemma GreatestI_ex: "\<exists>k::nat. P k \<Longrightarrow> \<forall>y. P y \<longrightarrow> y < b \<Longrightarrow> P (GREATEST x. P x)"
|
|
33 |
by (metis GreatestI)
|
|
34 |
|
|
35 |
|
|
36 |
context field
|
|
37 |
begin
|
|
38 |
|
|
39 |
subclass idom_divide ..
|
|
40 |
|
|
41 |
end
|
|
42 |
|
|
43 |
context field
|
|
44 |
begin
|
|
45 |
|
|
46 |
definition normalize_field :: "'a \<Rightarrow> 'a"
|
|
47 |
where [simp]: "normalize_field x = (if x = 0 then 0 else 1)"
|
|
48 |
definition unit_factor_field :: "'a \<Rightarrow> 'a"
|
|
49 |
where [simp]: "unit_factor_field x = x"
|
|
50 |
definition euclidean_size_field :: "'a \<Rightarrow> nat"
|
|
51 |
where [simp]: "euclidean_size_field x = (if x = 0 then 0 else 1)"
|
|
52 |
definition mod_field :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
|
|
53 |
where [simp]: "mod_field x y = (if y = 0 then x else 0)"
|
|
54 |
|
|
55 |
end
|
|
56 |
|
|
57 |
instantiation real :: euclidean_ring
|
|
58 |
begin
|
|
59 |
|
|
60 |
definition [simp]: "normalize_real = (normalize_field :: real \<Rightarrow> _)"
|
|
61 |
definition [simp]: "unit_factor_real = (unit_factor_field :: real \<Rightarrow> _)"
|
|
62 |
definition [simp]: "euclidean_size_real = (euclidean_size_field :: real \<Rightarrow> _)"
|
|
63 |
definition [simp]: "mod_real = (mod_field :: real \<Rightarrow> _)"
|
|
64 |
|
|
65 |
instance by standard (simp_all add: dvd_field_iff divide_simps)
|
|
66 |
end
|
|
67 |
|
|
68 |
instantiation real :: euclidean_ring_gcd
|
|
69 |
begin
|
|
70 |
|
|
71 |
definition gcd_real :: "real \<Rightarrow> real \<Rightarrow> real" where
|
|
72 |
"gcd_real = gcd_eucl"
|
|
73 |
definition lcm_real :: "real \<Rightarrow> real \<Rightarrow> real" where
|
|
74 |
"lcm_real = lcm_eucl"
|
|
75 |
definition Gcd_real :: "real set \<Rightarrow> real" where
|
|
76 |
"Gcd_real = Gcd_eucl"
|
|
77 |
definition Lcm_real :: "real set \<Rightarrow> real" where
|
|
78 |
"Lcm_real = Lcm_eucl"
|
|
79 |
|
|
80 |
instance by standard (simp_all add: gcd_real_def lcm_real_def Gcd_real_def Lcm_real_def)
|
|
81 |
|
|
82 |
end
|
|
83 |
|
|
84 |
instantiation rat :: euclidean_ring
|
|
85 |
begin
|
|
86 |
|
|
87 |
definition [simp]: "normalize_rat = (normalize_field :: rat \<Rightarrow> _)"
|
|
88 |
definition [simp]: "unit_factor_rat = (unit_factor_field :: rat \<Rightarrow> _)"
|
|
89 |
definition [simp]: "euclidean_size_rat = (euclidean_size_field :: rat \<Rightarrow> _)"
|
|
90 |
definition [simp]: "mod_rat = (mod_field :: rat \<Rightarrow> _)"
|
|
91 |
|
|
92 |
instance by standard (simp_all add: dvd_field_iff divide_simps)
|
|
93 |
end
|
|
94 |
|
|
95 |
instantiation rat :: euclidean_ring_gcd
|
|
96 |
begin
|
|
97 |
|
|
98 |
definition gcd_rat :: "rat \<Rightarrow> rat \<Rightarrow> rat" where
|
|
99 |
"gcd_rat = gcd_eucl"
|
|
100 |
definition lcm_rat :: "rat \<Rightarrow> rat \<Rightarrow> rat" where
|
|
101 |
"lcm_rat = lcm_eucl"
|
|
102 |
definition Gcd_rat :: "rat set \<Rightarrow> rat" where
|
|
103 |
"Gcd_rat = Gcd_eucl"
|
|
104 |
definition Lcm_rat :: "rat set \<Rightarrow> rat" where
|
|
105 |
"Lcm_rat = Lcm_eucl"
|
|
106 |
|
|
107 |
instance by standard (simp_all add: gcd_rat_def lcm_rat_def Gcd_rat_def Lcm_rat_def)
|
|
108 |
|
|
109 |
end
|
|
110 |
|
|
111 |
instantiation complex :: euclidean_ring
|
|
112 |
begin
|
|
113 |
|
|
114 |
definition [simp]: "normalize_complex = (normalize_field :: complex \<Rightarrow> _)"
|
|
115 |
definition [simp]: "unit_factor_complex = (unit_factor_field :: complex \<Rightarrow> _)"
|
|
116 |
definition [simp]: "euclidean_size_complex = (euclidean_size_field :: complex \<Rightarrow> _)"
|
|
117 |
definition [simp]: "mod_complex = (mod_field :: complex \<Rightarrow> _)"
|
|
118 |
|
|
119 |
instance by standard (simp_all add: dvd_field_iff divide_simps)
|
|
120 |
end
|
|
121 |
|
|
122 |
instantiation complex :: euclidean_ring_gcd
|
|
123 |
begin
|
|
124 |
|
|
125 |
definition gcd_complex :: "complex \<Rightarrow> complex \<Rightarrow> complex" where
|
|
126 |
"gcd_complex = gcd_eucl"
|
|
127 |
definition lcm_complex :: "complex \<Rightarrow> complex \<Rightarrow> complex" where
|
|
128 |
"lcm_complex = lcm_eucl"
|
|
129 |
definition Gcd_complex :: "complex set \<Rightarrow> complex" where
|
|
130 |
"Gcd_complex = Gcd_eucl"
|
|
131 |
definition Lcm_complex :: "complex set \<Rightarrow> complex" where
|
|
132 |
"Lcm_complex = Lcm_eucl"
|
|
133 |
|
|
134 |
instance by standard (simp_all add: gcd_complex_def lcm_complex_def Gcd_complex_def Lcm_complex_def)
|
|
135 |
|
|
136 |
end
|
|
137 |
|
|
138 |
|
|
139 |
|
|
140 |
subsection \<open>Lifting elements into the field of fractions\<close>
|
|
141 |
|
|
142 |
definition to_fract :: "'a :: idom \<Rightarrow> 'a fract" where "to_fract x = Fract x 1"
|
|
143 |
|
|
144 |
lemma to_fract_0 [simp]: "to_fract 0 = 0"
|
|
145 |
by (simp add: to_fract_def eq_fract Zero_fract_def)
|
|
146 |
|
|
147 |
lemma to_fract_1 [simp]: "to_fract 1 = 1"
|
|
148 |
by (simp add: to_fract_def eq_fract One_fract_def)
|
|
149 |
|
|
150 |
lemma to_fract_add [simp]: "to_fract (x + y) = to_fract x + to_fract y"
|
|
151 |
by (simp add: to_fract_def)
|
|
152 |
|
|
153 |
lemma to_fract_diff [simp]: "to_fract (x - y) = to_fract x - to_fract y"
|
|
154 |
by (simp add: to_fract_def)
|
|
155 |
|
|
156 |
lemma to_fract_uminus [simp]: "to_fract (-x) = -to_fract x"
|
|
157 |
by (simp add: to_fract_def)
|
|
158 |
|
|
159 |
lemma to_fract_mult [simp]: "to_fract (x * y) = to_fract x * to_fract y"
|
|
160 |
by (simp add: to_fract_def)
|
|
161 |
|
|
162 |
lemma to_fract_eq_iff [simp]: "to_fract x = to_fract y \<longleftrightarrow> x = y"
|
|
163 |
by (simp add: to_fract_def eq_fract)
|
|
164 |
|
|
165 |
lemma to_fract_eq_0_iff [simp]: "to_fract x = 0 \<longleftrightarrow> x = 0"
|
|
166 |
by (simp add: to_fract_def Zero_fract_def eq_fract)
|
|
167 |
|
|
168 |
lemma snd_quot_of_fract_nonzero [simp]: "snd (quot_of_fract x) \<noteq> 0"
|
|
169 |
by transfer simp
|
|
170 |
|
|
171 |
lemma Fract_quot_of_fract [simp]: "Fract (fst (quot_of_fract x)) (snd (quot_of_fract x)) = x"
|
|
172 |
by transfer (simp del: fractrel_iff, subst fractrel_normalize_quot_left, simp)
|
|
173 |
|
|
174 |
lemma to_fract_quot_of_fract:
|
|
175 |
assumes "snd (quot_of_fract x) = 1"
|
|
176 |
shows "to_fract (fst (quot_of_fract x)) = x"
|
|
177 |
proof -
|
|
178 |
have "x = Fract (fst (quot_of_fract x)) (snd (quot_of_fract x))" by simp
|
|
179 |
also note assms
|
|
180 |
finally show ?thesis by (simp add: to_fract_def)
|
|
181 |
qed
|
|
182 |
|
|
183 |
lemma snd_quot_of_fract_Fract_whole:
|
|
184 |
assumes "y dvd x"
|
|
185 |
shows "snd (quot_of_fract (Fract x y)) = 1"
|
|
186 |
using assms by transfer (auto simp: normalize_quot_def Let_def gcd_proj2_if_dvd)
|
|
187 |
|
|
188 |
lemma Fract_conv_to_fract: "Fract a b = to_fract a / to_fract b"
|
|
189 |
by (simp add: to_fract_def)
|
|
190 |
|
|
191 |
lemma quot_of_fract_to_fract [simp]: "quot_of_fract (to_fract x) = (x, 1)"
|
|
192 |
unfolding to_fract_def by transfer (simp add: normalize_quot_def)
|
|
193 |
|
|
194 |
lemma fst_quot_of_fract_eq_0_iff [simp]: "fst (quot_of_fract x) = 0 \<longleftrightarrow> x = 0"
|
|
195 |
by transfer simp
|
|
196 |
|
|
197 |
lemma snd_quot_of_fract_to_fract [simp]: "snd (quot_of_fract (to_fract x)) = 1"
|
|
198 |
unfolding to_fract_def by (rule snd_quot_of_fract_Fract_whole) simp_all
|
|
199 |
|
|
200 |
lemma coprime_quot_of_fract:
|
|
201 |
"coprime (fst (quot_of_fract x)) (snd (quot_of_fract x))"
|
|
202 |
by transfer (simp add: coprime_normalize_quot)
|
|
203 |
|
|
204 |
lemma unit_factor_snd_quot_of_fract: "unit_factor (snd (quot_of_fract x)) = 1"
|
|
205 |
using quot_of_fract_in_normalized_fracts[of x]
|
|
206 |
by (simp add: normalized_fracts_def case_prod_unfold)
|
|
207 |
|
|
208 |
lemma unit_factor_1_imp_normalized: "unit_factor x = 1 \<Longrightarrow> normalize x = x"
|
|
209 |
by (subst (2) normalize_mult_unit_factor [symmetric, of x])
|
|
210 |
(simp del: normalize_mult_unit_factor)
|
|
211 |
|
|
212 |
lemma normalize_snd_quot_of_fract: "normalize (snd (quot_of_fract x)) = snd (quot_of_fract x)"
|
|
213 |
by (intro unit_factor_1_imp_normalized unit_factor_snd_quot_of_fract)
|
|
214 |
|
|
215 |
|
|
216 |
subsection \<open>Mapping polynomials\<close>
|
|
217 |
|
|
218 |
definition map_poly
|
|
219 |
:: "('a :: comm_semiring_0 \<Rightarrow> 'b :: comm_semiring_0) \<Rightarrow> 'a poly \<Rightarrow> 'b poly" where
|
|
220 |
"map_poly f p = Poly (map f (coeffs p))"
|
|
221 |
|
|
222 |
lemma map_poly_0 [simp]: "map_poly f 0 = 0"
|
|
223 |
by (simp add: map_poly_def)
|
|
224 |
|
|
225 |
lemma map_poly_1: "map_poly f 1 = [:f 1:]"
|
|
226 |
by (simp add: map_poly_def)
|
|
227 |
|
|
228 |
lemma map_poly_1' [simp]: "f 1 = 1 \<Longrightarrow> map_poly f 1 = 1"
|
|
229 |
by (simp add: map_poly_def one_poly_def)
|
|
230 |
|
|
231 |
lemma coeff_map_poly:
|
|
232 |
assumes "f 0 = 0"
|
|
233 |
shows "coeff (map_poly f p) n = f (coeff p n)"
|
|
234 |
by (auto simp: map_poly_def nth_default_def coeffs_def assms
|
|
235 |
not_less Suc_le_eq coeff_eq_0 simp del: upt_Suc)
|
|
236 |
|
|
237 |
lemma coeffs_map_poly [code abstract]:
|
|
238 |
"coeffs (map_poly f p) = strip_while (op = 0) (map f (coeffs p))"
|
|
239 |
by (simp add: map_poly_def)
|
|
240 |
|
|
241 |
lemma set_coeffs_map_poly:
|
|
242 |
"(\<And>x. f x = 0 \<longleftrightarrow> x = 0) \<Longrightarrow> set (coeffs (map_poly f p)) = f ` set (coeffs p)"
|
|
243 |
by (cases "p = 0") (auto simp: coeffs_map_poly last_map last_coeffs_not_0)
|
|
244 |
|
|
245 |
lemma coeffs_map_poly':
|
|
246 |
assumes "(\<And>x. x \<noteq> 0 \<Longrightarrow> f x \<noteq> 0)"
|
|
247 |
shows "coeffs (map_poly f p) = map f (coeffs p)"
|
|
248 |
by (cases "p = 0") (auto simp: coeffs_map_poly last_map last_coeffs_not_0 assms
|
|
249 |
intro!: strip_while_not_last split: if_splits)
|
|
250 |
|
|
251 |
lemma degree_map_poly:
|
|
252 |
assumes "\<And>x. x \<noteq> 0 \<Longrightarrow> f x \<noteq> 0"
|
|
253 |
shows "degree (map_poly f p) = degree p"
|
|
254 |
by (simp add: degree_eq_length_coeffs coeffs_map_poly' assms)
|
|
255 |
|
|
256 |
lemma map_poly_eq_0_iff:
|
|
257 |
assumes "f 0 = 0" "\<And>x. x \<in> set (coeffs p) \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> f x \<noteq> 0"
|
|
258 |
shows "map_poly f p = 0 \<longleftrightarrow> p = 0"
|
|
259 |
proof -
|
|
260 |
{
|
|
261 |
fix n :: nat
|
|
262 |
have "coeff (map_poly f p) n = f (coeff p n)" by (simp add: coeff_map_poly assms)
|
|
263 |
also have "\<dots> = 0 \<longleftrightarrow> coeff p n = 0"
|
|
264 |
proof (cases "n < length (coeffs p)")
|
|
265 |
case True
|
|
266 |
hence "coeff p n \<in> set (coeffs p)" by (auto simp: coeffs_def simp del: upt_Suc)
|
|
267 |
with assms show "f (coeff p n) = 0 \<longleftrightarrow> coeff p n = 0" by auto
|
|
268 |
qed (auto simp: assms length_coeffs nth_default_coeffs_eq [symmetric] nth_default_def)
|
|
269 |
finally have "(coeff (map_poly f p) n = 0) = (coeff p n = 0)" .
|
|
270 |
}
|
|
271 |
thus ?thesis by (auto simp: poly_eq_iff)
|
|
272 |
qed
|
|
273 |
|
|
274 |
lemma map_poly_smult:
|
|
275 |
assumes "f 0 = 0""\<And>c x. f (c * x) = f c * f x"
|
|
276 |
shows "map_poly f (smult c p) = smult (f c) (map_poly f p)"
|
|
277 |
by (intro poly_eqI) (simp_all add: assms coeff_map_poly)
|
|
278 |
|
|
279 |
lemma map_poly_pCons:
|
|
280 |
assumes "f 0 = 0"
|
|
281 |
shows "map_poly f (pCons c p) = pCons (f c) (map_poly f p)"
|
|
282 |
by (intro poly_eqI) (simp_all add: assms coeff_map_poly coeff_pCons split: nat.splits)
|
|
283 |
|
|
284 |
lemma map_poly_map_poly:
|
|
285 |
assumes "f 0 = 0" "g 0 = 0"
|
|
286 |
shows "map_poly f (map_poly g p) = map_poly (f \<circ> g) p"
|
|
287 |
by (intro poly_eqI) (simp add: coeff_map_poly assms)
|
|
288 |
|
|
289 |
lemma map_poly_id [simp]: "map_poly id p = p"
|
|
290 |
by (simp add: map_poly_def)
|
|
291 |
|
|
292 |
lemma map_poly_id' [simp]: "map_poly (\<lambda>x. x) p = p"
|
|
293 |
by (simp add: map_poly_def)
|
|
294 |
|
|
295 |
lemma map_poly_cong:
|
|
296 |
assumes "(\<And>x. x \<in> set (coeffs p) \<Longrightarrow> f x = g x)"
|
|
297 |
shows "map_poly f p = map_poly g p"
|
|
298 |
proof -
|
|
299 |
from assms have "map f (coeffs p) = map g (coeffs p)" by (intro map_cong) simp_all
|
|
300 |
thus ?thesis by (simp only: coeffs_eq_iff coeffs_map_poly)
|
|
301 |
qed
|
|
302 |
|
|
303 |
lemma map_poly_monom: "f 0 = 0 \<Longrightarrow> map_poly f (monom c n) = monom (f c) n"
|
|
304 |
by (intro poly_eqI) (simp_all add: coeff_map_poly)
|
|
305 |
|
|
306 |
lemma map_poly_idI:
|
|
307 |
assumes "\<And>x. x \<in> set (coeffs p) \<Longrightarrow> f x = x"
|
|
308 |
shows "map_poly f p = p"
|
|
309 |
using map_poly_cong[OF assms, of _ id] by simp
|
|
310 |
|
|
311 |
lemma map_poly_idI':
|
|
312 |
assumes "\<And>x. x \<in> set (coeffs p) \<Longrightarrow> f x = x"
|
|
313 |
shows "p = map_poly f p"
|
|
314 |
using map_poly_cong[OF assms, of _ id] by simp
|
|
315 |
|
|
316 |
lemma smult_conv_map_poly: "smult c p = map_poly (\<lambda>x. c * x) p"
|
|
317 |
by (intro poly_eqI) (simp_all add: coeff_map_poly)
|
|
318 |
|
|
319 |
lemma div_const_poly_conv_map_poly:
|
|
320 |
assumes "[:c:] dvd p"
|
|
321 |
shows "p div [:c:] = map_poly (\<lambda>x. x div c) p"
|
|
322 |
proof (cases "c = 0")
|
|
323 |
case False
|
|
324 |
from assms obtain q where p: "p = [:c:] * q" by (erule dvdE)
|
|
325 |
moreover {
|
|
326 |
have "smult c q = [:c:] * q" by simp
|
|
327 |
also have "\<dots> div [:c:] = q" by (rule nonzero_mult_divide_cancel_left) (insert False, auto)
|
|
328 |
finally have "smult c q div [:c:] = q" .
|
|
329 |
}
|
|
330 |
ultimately show ?thesis by (intro poly_eqI) (auto simp: coeff_map_poly False)
|
|
331 |
qed (auto intro!: poly_eqI simp: coeff_map_poly)
|
|
332 |
|
|
333 |
|
|
334 |
|
|
335 |
subsection \<open>Various facts about polynomials\<close>
|
|
336 |
|
|
337 |
lemma msetprod_const_poly: "msetprod (image_mset (\<lambda>x. [:f x:]) A) = [:msetprod (image_mset f A):]"
|
|
338 |
by (induction A) (simp_all add: one_poly_def mult_ac)
|
|
339 |
|
|
340 |
lemma degree_mod_less': "b \<noteq> 0 \<Longrightarrow> a mod b \<noteq> 0 \<Longrightarrow> degree (a mod b) < degree b"
|
|
341 |
using degree_mod_less[of b a] by auto
|
|
342 |
|
|
343 |
lemma is_unit_const_poly_iff:
|
|
344 |
"[:c :: 'a :: {comm_semiring_1,semiring_no_zero_divisors}:] dvd 1 \<longleftrightarrow> c dvd 1"
|
|
345 |
by (auto simp: one_poly_def)
|
|
346 |
|
|
347 |
lemma is_unit_poly_iff:
|
|
348 |
fixes p :: "'a :: {comm_semiring_1,semiring_no_zero_divisors} poly"
|
|
349 |
shows "p dvd 1 \<longleftrightarrow> (\<exists>c. p = [:c:] \<and> c dvd 1)"
|
|
350 |
proof safe
|
|
351 |
assume "p dvd 1"
|
|
352 |
then obtain q where pq: "1 = p * q" by (erule dvdE)
|
|
353 |
hence "degree 1 = degree (p * q)" by simp
|
|
354 |
also from pq have "\<dots> = degree p + degree q" by (intro degree_mult_eq) auto
|
|
355 |
finally have "degree p = 0" by simp
|
|
356 |
from degree_eq_zeroE[OF this] obtain c where c: "p = [:c:]" .
|
|
357 |
with \<open>p dvd 1\<close> show "\<exists>c. p = [:c:] \<and> c dvd 1"
|
|
358 |
by (auto simp: is_unit_const_poly_iff)
|
|
359 |
qed (auto simp: is_unit_const_poly_iff)
|
|
360 |
|
|
361 |
lemma is_unit_polyE:
|
|
362 |
fixes p :: "'a :: {comm_semiring_1,semiring_no_zero_divisors} poly"
|
|
363 |
assumes "p dvd 1" obtains c where "p = [:c:]" "c dvd 1"
|
|
364 |
using assms by (subst (asm) is_unit_poly_iff) blast
|
|
365 |
|
|
366 |
lemma smult_eq_iff:
|
|
367 |
assumes "(b :: 'a :: field) \<noteq> 0"
|
|
368 |
shows "smult a p = smult b q \<longleftrightarrow> smult (a / b) p = q"
|
|
369 |
proof
|
|
370 |
assume "smult a p = smult b q"
|
|
371 |
also from assms have "smult (inverse b) \<dots> = q" by simp
|
|
372 |
finally show "smult (a / b) p = q" by (simp add: field_simps)
|
|
373 |
qed (insert assms, auto)
|
|
374 |
|
|
375 |
lemma irreducible_const_poly_iff:
|
|
376 |
fixes c :: "'a :: {comm_semiring_1,semiring_no_zero_divisors}"
|
|
377 |
shows "irreducible [:c:] \<longleftrightarrow> irreducible c"
|
|
378 |
proof
|
|
379 |
assume A: "irreducible c"
|
|
380 |
show "irreducible [:c:]"
|
|
381 |
proof (rule irreducibleI)
|
|
382 |
fix a b assume ab: "[:c:] = a * b"
|
|
383 |
hence "degree [:c:] = degree (a * b)" by (simp only: )
|
|
384 |
also from A ab have "a \<noteq> 0" "b \<noteq> 0" by auto
|
|
385 |
hence "degree (a * b) = degree a + degree b" by (simp add: degree_mult_eq)
|
|
386 |
finally have "degree a = 0" "degree b = 0" by auto
|
|
387 |
then obtain a' b' where ab': "a = [:a':]" "b = [:b':]" by (auto elim!: degree_eq_zeroE)
|
|
388 |
from ab have "coeff [:c:] 0 = coeff (a * b) 0" by (simp only: )
|
|
389 |
hence "c = a' * b'" by (simp add: ab' mult_ac)
|
|
390 |
from A and this have "a' dvd 1 \<or> b' dvd 1" by (rule irreducibleD)
|
|
391 |
with ab' show "a dvd 1 \<or> b dvd 1" by (auto simp: one_poly_def)
|
|
392 |
qed (insert A, auto simp: irreducible_def is_unit_poly_iff)
|
|
393 |
next
|
|
394 |
assume A: "irreducible [:c:]"
|
|
395 |
show "irreducible c"
|
|
396 |
proof (rule irreducibleI)
|
|
397 |
fix a b assume ab: "c = a * b"
|
|
398 |
hence "[:c:] = [:a:] * [:b:]" by (simp add: mult_ac)
|
|
399 |
from A and this have "[:a:] dvd 1 \<or> [:b:] dvd 1" by (rule irreducibleD)
|
|
400 |
thus "a dvd 1 \<or> b dvd 1" by (simp add: one_poly_def)
|
|
401 |
qed (insert A, auto simp: irreducible_def one_poly_def)
|
|
402 |
qed
|
|
403 |
|
|
404 |
lemma lead_coeff_monom [simp]: "lead_coeff (monom c n) = c"
|
|
405 |
by (cases "c = 0") (simp_all add: lead_coeff_def degree_monom_eq)
|
|
406 |
|
|
407 |
|
|
408 |
subsection \<open>Normalisation of polynomials\<close>
|
|
409 |
|
|
410 |
instantiation poly :: ("{normalization_semidom,idom_divide}") normalization_semidom
|
|
411 |
begin
|
|
412 |
|
|
413 |
definition unit_factor_poly :: "'a poly \<Rightarrow> 'a poly"
|
|
414 |
where "unit_factor_poly p = monom (unit_factor (lead_coeff p)) 0"
|
|
415 |
|
|
416 |
definition normalize_poly :: "'a poly \<Rightarrow> 'a poly"
|
|
417 |
where "normalize_poly p = map_poly (\<lambda>x. x div unit_factor (lead_coeff p)) p"
|
|
418 |
|
|
419 |
lemma normalize_poly_altdef:
|
|
420 |
"normalize p = p div [:unit_factor (lead_coeff p):]"
|
|
421 |
proof (cases "p = 0")
|
|
422 |
case False
|
|
423 |
thus ?thesis
|
|
424 |
by (subst div_const_poly_conv_map_poly)
|
|
425 |
(auto simp: normalize_poly_def const_poly_dvd_iff lead_coeff_def )
|
|
426 |
qed (auto simp: normalize_poly_def)
|
|
427 |
|
|
428 |
instance
|
|
429 |
proof
|
|
430 |
fix p :: "'a poly"
|
|
431 |
show "unit_factor p * normalize p = p"
|
|
432 |
by (cases "p = 0")
|
|
433 |
(simp_all add: unit_factor_poly_def normalize_poly_def monom_0
|
|
434 |
smult_conv_map_poly map_poly_map_poly o_def)
|
|
435 |
next
|
|
436 |
fix p :: "'a poly"
|
|
437 |
assume "is_unit p"
|
|
438 |
then obtain c where p: "p = [:c:]" "is_unit c" by (auto simp: is_unit_poly_iff)
|
|
439 |
thus "normalize p = 1"
|
|
440 |
by (simp add: normalize_poly_def map_poly_pCons is_unit_normalize one_poly_def)
|
|
441 |
next
|
|
442 |
fix p :: "'a poly" assume "p \<noteq> 0"
|
|
443 |
thus "is_unit (unit_factor p)"
|
|
444 |
by (simp add: unit_factor_poly_def monom_0 is_unit_poly_iff)
|
|
445 |
qed (simp_all add: normalize_poly_def unit_factor_poly_def monom_0 lead_coeff_mult unit_factor_mult)
|
|
446 |
|
|
447 |
end
|
|
448 |
|
|
449 |
lemma unit_factor_pCons:
|
|
450 |
"unit_factor (pCons a p) = (if p = 0 then monom (unit_factor a) 0 else unit_factor p)"
|
|
451 |
by (simp add: unit_factor_poly_def)
|
|
452 |
|
|
453 |
lemma normalize_monom [simp]:
|
|
454 |
"normalize (monom a n) = monom (normalize a) n"
|
|
455 |
by (simp add: map_poly_monom normalize_poly_def)
|
|
456 |
|
|
457 |
lemma unit_factor_monom [simp]:
|
|
458 |
"unit_factor (monom a n) = monom (unit_factor a) 0"
|
|
459 |
by (simp add: unit_factor_poly_def )
|
|
460 |
|
|
461 |
lemma normalize_const_poly: "normalize [:c:] = [:normalize c:]"
|
|
462 |
by (simp add: normalize_poly_def map_poly_pCons)
|
|
463 |
|
|
464 |
lemma normalize_smult: "normalize (smult c p) = smult (normalize c) (normalize p)"
|
|
465 |
proof -
|
|
466 |
have "smult c p = [:c:] * p" by simp
|
|
467 |
also have "normalize \<dots> = smult (normalize c) (normalize p)"
|
|
468 |
by (subst normalize_mult) (simp add: normalize_const_poly)
|
|
469 |
finally show ?thesis .
|
|
470 |
qed
|
|
471 |
|
|
472 |
lemma is_unit_smult_iff: "smult c p dvd 1 \<longleftrightarrow> c dvd 1 \<and> p dvd 1"
|
|
473 |
proof -
|
|
474 |
have "smult c p = [:c:] * p" by simp
|
|
475 |
also have "\<dots> dvd 1 \<longleftrightarrow> c dvd 1 \<and> p dvd 1"
|
|
476 |
proof safe
|
|
477 |
assume A: "[:c:] * p dvd 1"
|
|
478 |
thus "p dvd 1" by (rule dvd_mult_right)
|
|
479 |
from A obtain q where B: "1 = [:c:] * p * q" by (erule dvdE)
|
|
480 |
have "c dvd c * (coeff p 0 * coeff q 0)" by simp
|
|
481 |
also have "\<dots> = coeff ([:c:] * p * q) 0" by (simp add: mult.assoc coeff_mult)
|
|
482 |
also note B [symmetric]
|
|
483 |
finally show "c dvd 1" by simp
|
|
484 |
next
|
|
485 |
assume "c dvd 1" "p dvd 1"
|
|
486 |
from \<open>c dvd 1\<close> obtain d where "1 = c * d" by (erule dvdE)
|
|
487 |
hence "1 = [:c:] * [:d:]" by (simp add: one_poly_def mult_ac)
|
|
488 |
hence "[:c:] dvd 1" by (rule dvdI)
|
|
489 |
from mult_dvd_mono[OF this \<open>p dvd 1\<close>] show "[:c:] * p dvd 1" by simp
|
|
490 |
qed
|
|
491 |
finally show ?thesis .
|
|
492 |
qed
|
|
493 |
|
|
494 |
|
|
495 |
subsection \<open>Content and primitive part of a polynomial\<close>
|
|
496 |
|
|
497 |
definition content :: "('a :: semiring_Gcd poly) \<Rightarrow> 'a" where
|
|
498 |
"content p = Gcd (set (coeffs p))"
|
|
499 |
|
|
500 |
lemma content_0 [simp]: "content 0 = 0"
|
|
501 |
by (simp add: content_def)
|
|
502 |
|
|
503 |
lemma content_1 [simp]: "content 1 = 1"
|
|
504 |
by (simp add: content_def)
|
|
505 |
|
|
506 |
lemma content_const [simp]: "content [:c:] = normalize c"
|
|
507 |
by (simp add: content_def cCons_def)
|
|
508 |
|
|
509 |
lemma const_poly_dvd_iff_dvd_content:
|
|
510 |
fixes c :: "'a :: semiring_Gcd"
|
|
511 |
shows "[:c:] dvd p \<longleftrightarrow> c dvd content p"
|
|
512 |
proof (cases "p = 0")
|
|
513 |
case [simp]: False
|
|
514 |
have "[:c:] dvd p \<longleftrightarrow> (\<forall>n. c dvd coeff p n)" by (rule const_poly_dvd_iff)
|
|
515 |
also have "\<dots> \<longleftrightarrow> (\<forall>a\<in>set (coeffs p). c dvd a)"
|
|
516 |
proof safe
|
|
517 |
fix n :: nat assume "\<forall>a\<in>set (coeffs p). c dvd a"
|
|
518 |
thus "c dvd coeff p n"
|
|
519 |
by (cases "n \<le> degree p") (auto simp: coeff_eq_0 coeffs_def split: if_splits)
|
|
520 |
qed (auto simp: coeffs_def simp del: upt_Suc split: if_splits)
|
|
521 |
also have "\<dots> \<longleftrightarrow> c dvd content p"
|
|
522 |
by (simp add: content_def dvd_Gcd_iff mult.commute [of "unit_factor x" for x]
|
|
523 |
dvd_mult_unit_iff lead_coeff_nonzero)
|
|
524 |
finally show ?thesis .
|
|
525 |
qed simp_all
|
|
526 |
|
|
527 |
lemma content_dvd [simp]: "[:content p:] dvd p"
|
|
528 |
by (subst const_poly_dvd_iff_dvd_content) simp_all
|
|
529 |
|
|
530 |
lemma content_dvd_coeff [simp]: "content p dvd coeff p n"
|
|
531 |
by (cases "n \<le> degree p")
|
|
532 |
(auto simp: content_def coeffs_def not_le coeff_eq_0 simp del: upt_Suc intro: Gcd_dvd)
|
|
533 |
|
|
534 |
lemma content_dvd_coeffs: "c \<in> set (coeffs p) \<Longrightarrow> content p dvd c"
|
|
535 |
by (simp add: content_def Gcd_dvd)
|
|
536 |
|
|
537 |
lemma normalize_content [simp]: "normalize (content p) = content p"
|
|
538 |
by (simp add: content_def)
|
|
539 |
|
|
540 |
lemma is_unit_content_iff [simp]: "is_unit (content p) \<longleftrightarrow> content p = 1"
|
|
541 |
proof
|
|
542 |
assume "is_unit (content p)"
|
|
543 |
hence "normalize (content p) = 1" by (simp add: is_unit_normalize del: normalize_content)
|
|
544 |
thus "content p = 1" by simp
|
|
545 |
qed auto
|
|
546 |
|
|
547 |
lemma content_smult [simp]: "content (smult c p) = normalize c * content p"
|
|
548 |
by (simp add: content_def coeffs_smult Gcd_mult)
|
|
549 |
|
|
550 |
lemma content_eq_zero_iff [simp]: "content p = 0 \<longleftrightarrow> p = 0"
|
|
551 |
by (auto simp: content_def simp: poly_eq_iff coeffs_def)
|
|
552 |
|
|
553 |
definition primitive_part :: "'a :: {semiring_Gcd,idom_divide} poly \<Rightarrow> 'a poly" where
|
|
554 |
"primitive_part p = (if p = 0 then 0 else map_poly (\<lambda>x. x div content p) p)"
|
|
555 |
|
|
556 |
lemma primitive_part_0 [simp]: "primitive_part 0 = 0"
|
|
557 |
by (simp add: primitive_part_def)
|
|
558 |
|
|
559 |
lemma content_times_primitive_part [simp]:
|
|
560 |
fixes p :: "'a :: {idom_divide, semiring_Gcd} poly"
|
|
561 |
shows "smult (content p) (primitive_part p) = p"
|
|
562 |
proof (cases "p = 0")
|
|
563 |
case False
|
|
564 |
thus ?thesis
|
|
565 |
unfolding primitive_part_def
|
|
566 |
by (auto simp: smult_conv_map_poly map_poly_map_poly o_def content_dvd_coeffs
|
|
567 |
intro: map_poly_idI)
|
|
568 |
qed simp_all
|
|
569 |
|
|
570 |
lemma primitive_part_eq_0_iff [simp]: "primitive_part p = 0 \<longleftrightarrow> p = 0"
|
|
571 |
proof (cases "p = 0")
|
|
572 |
case False
|
|
573 |
hence "primitive_part p = map_poly (\<lambda>x. x div content p) p"
|
|
574 |
by (simp add: primitive_part_def)
|
|
575 |
also from False have "\<dots> = 0 \<longleftrightarrow> p = 0"
|
|
576 |
by (intro map_poly_eq_0_iff) (auto simp: dvd_div_eq_0_iff content_dvd_coeffs)
|
|
577 |
finally show ?thesis using False by simp
|
|
578 |
qed simp
|
|
579 |
|
|
580 |
lemma content_primitive_part [simp]:
|
|
581 |
assumes "p \<noteq> 0"
|
|
582 |
shows "content (primitive_part p) = 1"
|
|
583 |
proof -
|
|
584 |
have "p = smult (content p) (primitive_part p)" by simp
|
|
585 |
also have "content \<dots> = content p * content (primitive_part p)"
|
|
586 |
by (simp del: content_times_primitive_part)
|
|
587 |
finally show ?thesis using assms by simp
|
|
588 |
qed
|
|
589 |
|
|
590 |
lemma content_decompose:
|
|
591 |
fixes p :: "'a :: semiring_Gcd poly"
|
|
592 |
obtains p' where "p = smult (content p) p'" "content p' = 1"
|
|
593 |
proof (cases "p = 0")
|
|
594 |
case True
|
|
595 |
thus ?thesis by (intro that[of 1]) simp_all
|
|
596 |
next
|
|
597 |
case False
|
|
598 |
from content_dvd[of p] obtain r where r: "p = [:content p:] * r" by (erule dvdE)
|
|
599 |
have "content p * 1 = content p * content r" by (subst r) simp
|
|
600 |
with False have "content r = 1" by (subst (asm) mult_left_cancel) simp_all
|
|
601 |
with r show ?thesis by (intro that[of r]) simp_all
|
|
602 |
qed
|
|
603 |
|
|
604 |
lemma smult_content_normalize_primitive_part [simp]:
|
|
605 |
"smult (content p) (normalize (primitive_part p)) = normalize p"
|
|
606 |
proof -
|
|
607 |
have "smult (content p) (normalize (primitive_part p)) =
|
|
608 |
normalize ([:content p:] * primitive_part p)"
|
|
609 |
by (subst normalize_mult) (simp_all add: normalize_const_poly)
|
|
610 |
also have "[:content p:] * primitive_part p = p" by simp
|
|
611 |
finally show ?thesis .
|
|
612 |
qed
|
|
613 |
|
|
614 |
lemma content_dvd_contentI [intro]:
|
|
615 |
"p dvd q \<Longrightarrow> content p dvd content q"
|
|
616 |
using const_poly_dvd_iff_dvd_content content_dvd dvd_trans by blast
|
|
617 |
|
|
618 |
lemma primitive_part_const_poly [simp]: "primitive_part [:x:] = [:unit_factor x:]"
|
|
619 |
by (simp add: primitive_part_def map_poly_pCons)
|
|
620 |
|
|
621 |
lemma primitive_part_prim: "content p = 1 \<Longrightarrow> primitive_part p = p"
|
|
622 |
by (auto simp: primitive_part_def)
|
|
623 |
|
|
624 |
lemma degree_primitive_part [simp]: "degree (primitive_part p) = degree p"
|
|
625 |
proof (cases "p = 0")
|
|
626 |
case False
|
|
627 |
have "p = smult (content p) (primitive_part p)" by simp
|
|
628 |
also from False have "degree \<dots> = degree (primitive_part p)"
|
|
629 |
by (subst degree_smult_eq) simp_all
|
|
630 |
finally show ?thesis ..
|
|
631 |
qed simp_all
|
|
632 |
|
|
633 |
|
|
634 |
subsection \<open>Lifting polynomial coefficients to the field of fractions\<close>
|
|
635 |
|
|
636 |
abbreviation (input) fract_poly
|
|
637 |
where "fract_poly \<equiv> map_poly to_fract"
|
|
638 |
|
|
639 |
abbreviation (input) unfract_poly
|
|
640 |
where "unfract_poly \<equiv> map_poly (fst \<circ> quot_of_fract)"
|
|
641 |
|
|
642 |
lemma fract_poly_smult [simp]: "fract_poly (smult c p) = smult (to_fract c) (fract_poly p)"
|
|
643 |
by (simp add: smult_conv_map_poly map_poly_map_poly o_def)
|
|
644 |
|
|
645 |
lemma fract_poly_0 [simp]: "fract_poly 0 = 0"
|
|
646 |
by (simp add: poly_eqI coeff_map_poly)
|
|
647 |
|
|
648 |
lemma fract_poly_1 [simp]: "fract_poly 1 = 1"
|
|
649 |
by (simp add: one_poly_def map_poly_pCons)
|
|
650 |
|
|
651 |
lemma fract_poly_add [simp]:
|
|
652 |
"fract_poly (p + q) = fract_poly p + fract_poly q"
|
|
653 |
by (intro poly_eqI) (simp_all add: coeff_map_poly)
|
|
654 |
|
|
655 |
lemma fract_poly_diff [simp]:
|
|
656 |
"fract_poly (p - q) = fract_poly p - fract_poly q"
|
|
657 |
by (intro poly_eqI) (simp_all add: coeff_map_poly)
|
|
658 |
|
|
659 |
lemma to_fract_setsum [simp]: "to_fract (setsum f A) = setsum (\<lambda>x. to_fract (f x)) A"
|
|
660 |
by (cases "finite A", induction A rule: finite_induct) simp_all
|
|
661 |
|
|
662 |
lemma fract_poly_mult [simp]:
|
|
663 |
"fract_poly (p * q) = fract_poly p * fract_poly q"
|
|
664 |
by (intro poly_eqI) (simp_all add: coeff_map_poly coeff_mult)
|
|
665 |
|
|
666 |
lemma fract_poly_eq_iff [simp]: "fract_poly p = fract_poly q \<longleftrightarrow> p = q"
|
|
667 |
by (auto simp: poly_eq_iff coeff_map_poly)
|
|
668 |
|
|
669 |
lemma fract_poly_eq_0_iff [simp]: "fract_poly p = 0 \<longleftrightarrow> p = 0"
|
|
670 |
using fract_poly_eq_iff[of p 0] by (simp del: fract_poly_eq_iff)
|
|
671 |
|
|
672 |
lemma fract_poly_dvd: "p dvd q \<Longrightarrow> fract_poly p dvd fract_poly q"
|
|
673 |
by (auto elim!: dvdE)
|
|
674 |
|
|
675 |
lemma msetprod_fract_poly:
|
|
676 |
"msetprod (image_mset (\<lambda>x. fract_poly (f x)) A) = fract_poly (msetprod (image_mset f A))"
|
|
677 |
by (induction A) (simp_all add: mult_ac)
|
|
678 |
|
|
679 |
lemma is_unit_fract_poly_iff:
|
|
680 |
"p dvd 1 \<longleftrightarrow> fract_poly p dvd 1 \<and> content p = 1"
|
|
681 |
proof safe
|
|
682 |
assume A: "p dvd 1"
|
|
683 |
with fract_poly_dvd[of p 1] show "is_unit (fract_poly p)" by simp
|
|
684 |
from A show "content p = 1"
|
|
685 |
by (auto simp: is_unit_poly_iff normalize_1_iff)
|
|
686 |
next
|
|
687 |
assume A: "fract_poly p dvd 1" and B: "content p = 1"
|
|
688 |
from A obtain c where c: "fract_poly p = [:c:]" by (auto simp: is_unit_poly_iff)
|
|
689 |
{
|
|
690 |
fix n :: nat assume "n > 0"
|
|
691 |
have "to_fract (coeff p n) = coeff (fract_poly p) n" by (simp add: coeff_map_poly)
|
|
692 |
also note c
|
|
693 |
also from \<open>n > 0\<close> have "coeff [:c:] n = 0" by (simp add: coeff_pCons split: nat.splits)
|
|
694 |
finally have "coeff p n = 0" by simp
|
|
695 |
}
|
|
696 |
hence "degree p \<le> 0" by (intro degree_le) simp_all
|
|
697 |
with B show "p dvd 1" by (auto simp: is_unit_poly_iff normalize_1_iff elim!: degree_eq_zeroE)
|
|
698 |
qed
|
|
699 |
|
|
700 |
lemma fract_poly_is_unit: "p dvd 1 \<Longrightarrow> fract_poly p dvd 1"
|
|
701 |
using fract_poly_dvd[of p 1] by simp
|
|
702 |
|
|
703 |
lemma fract_poly_smult_eqE:
|
|
704 |
fixes c :: "'a :: {idom_divide,ring_gcd} fract"
|
|
705 |
assumes "fract_poly p = smult c (fract_poly q)"
|
|
706 |
obtains a b
|
|
707 |
where "c = to_fract b / to_fract a" "smult a p = smult b q" "coprime a b" "normalize a = a"
|
|
708 |
proof -
|
|
709 |
define a b where "a = fst (quot_of_fract c)" and "b = snd (quot_of_fract c)"
|
|
710 |
have "smult (to_fract a) (fract_poly q) = smult (to_fract b) (fract_poly p)"
|
|
711 |
by (subst smult_eq_iff) (simp_all add: a_def b_def Fract_conv_to_fract [symmetric] assms)
|
|
712 |
hence "fract_poly (smult a q) = fract_poly (smult b p)" by (simp del: fract_poly_eq_iff)
|
|
713 |
hence "smult b p = smult a q" by (simp only: fract_poly_eq_iff)
|
|
714 |
moreover have "c = to_fract a / to_fract b" "coprime b a" "normalize b = b"
|
|
715 |
by (simp_all add: a_def b_def coprime_quot_of_fract gcd.commute
|
|
716 |
normalize_snd_quot_of_fract Fract_conv_to_fract [symmetric])
|
|
717 |
ultimately show ?thesis by (intro that[of a b])
|
|
718 |
qed
|
|
719 |
|
|
720 |
|
|
721 |
subsection \<open>Fractional content\<close>
|
|
722 |
|
|
723 |
abbreviation (input) Lcm_coeff_denoms
|
|
724 |
:: "'a :: {semiring_Gcd,idom_divide,ring_gcd} fract poly \<Rightarrow> 'a"
|
|
725 |
where "Lcm_coeff_denoms p \<equiv> Lcm (snd ` quot_of_fract ` set (coeffs p))"
|
|
726 |
|
|
727 |
definition fract_content ::
|
|
728 |
"'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} fract poly \<Rightarrow> 'a fract" where
|
|
729 |
"fract_content p =
|
|
730 |
(let d = Lcm_coeff_denoms p in Fract (content (unfract_poly (smult (to_fract d) p))) d)"
|
|
731 |
|
|
732 |
definition primitive_part_fract ::
|
|
733 |
"'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} fract poly \<Rightarrow> 'a poly" where
|
|
734 |
"primitive_part_fract p =
|
|
735 |
primitive_part (unfract_poly (smult (to_fract (Lcm_coeff_denoms p)) p))"
|
|
736 |
|
|
737 |
lemma primitive_part_fract_0 [simp]: "primitive_part_fract 0 = 0"
|
|
738 |
by (simp add: primitive_part_fract_def)
|
|
739 |
|
|
740 |
lemma fract_content_eq_0_iff [simp]:
|
|
741 |
"fract_content p = 0 \<longleftrightarrow> p = 0"
|
|
742 |
unfolding fract_content_def Let_def Zero_fract_def
|
|
743 |
by (subst eq_fract) (auto simp: Lcm_0_iff map_poly_eq_0_iff)
|
|
744 |
|
|
745 |
lemma content_primitive_part_fract [simp]: "p \<noteq> 0 \<Longrightarrow> content (primitive_part_fract p) = 1"
|
|
746 |
unfolding primitive_part_fract_def
|
|
747 |
by (rule content_primitive_part)
|
|
748 |
(auto simp: primitive_part_fract_def map_poly_eq_0_iff Lcm_0_iff)
|
|
749 |
|
|
750 |
lemma content_times_primitive_part_fract:
|
|
751 |
"smult (fract_content p) (fract_poly (primitive_part_fract p)) = p"
|
|
752 |
proof -
|
|
753 |
define p' where "p' = unfract_poly (smult (to_fract (Lcm_coeff_denoms p)) p)"
|
|
754 |
have "fract_poly p' =
|
|
755 |
map_poly (to_fract \<circ> fst \<circ> quot_of_fract) (smult (to_fract (Lcm_coeff_denoms p)) p)"
|
|
756 |
unfolding primitive_part_fract_def p'_def
|
|
757 |
by (subst map_poly_map_poly) (simp_all add: o_assoc)
|
|
758 |
also have "\<dots> = smult (to_fract (Lcm_coeff_denoms p)) p"
|
|
759 |
proof (intro map_poly_idI, unfold o_apply)
|
|
760 |
fix c assume "c \<in> set (coeffs (smult (to_fract (Lcm_coeff_denoms p)) p))"
|
|
761 |
then obtain c' where c: "c' \<in> set (coeffs p)" "c = to_fract (Lcm_coeff_denoms p) * c'"
|
|
762 |
by (auto simp add: Lcm_0_iff coeffs_smult split: if_splits)
|
|
763 |
note c(2)
|
|
764 |
also have "c' = Fract (fst (quot_of_fract c')) (snd (quot_of_fract c'))"
|
|
765 |
by simp
|
|
766 |
also have "to_fract (Lcm_coeff_denoms p) * \<dots> =
|
|
767 |
Fract (Lcm_coeff_denoms p * fst (quot_of_fract c')) (snd (quot_of_fract c'))"
|
|
768 |
unfolding to_fract_def by (subst mult_fract) simp_all
|
|
769 |
also have "snd (quot_of_fract \<dots>) = 1"
|
|
770 |
by (intro snd_quot_of_fract_Fract_whole dvd_mult2 dvd_Lcm) (insert c(1), auto)
|
|
771 |
finally show "to_fract (fst (quot_of_fract c)) = c"
|
|
772 |
by (rule to_fract_quot_of_fract)
|
|
773 |
qed
|
|
774 |
also have "p' = smult (content p') (primitive_part p')"
|
|
775 |
by (rule content_times_primitive_part [symmetric])
|
|
776 |
also have "primitive_part p' = primitive_part_fract p"
|
|
777 |
by (simp add: primitive_part_fract_def p'_def)
|
|
778 |
also have "fract_poly (smult (content p') (primitive_part_fract p)) =
|
|
779 |
smult (to_fract (content p')) (fract_poly (primitive_part_fract p))" by simp
|
|
780 |
finally have "smult (to_fract (content p')) (fract_poly (primitive_part_fract p)) =
|
|
781 |
smult (to_fract (Lcm_coeff_denoms p)) p" .
|
|
782 |
thus ?thesis
|
|
783 |
by (subst (asm) smult_eq_iff)
|
|
784 |
(auto simp add: Let_def p'_def Fract_conv_to_fract field_simps Lcm_0_iff fract_content_def)
|
|
785 |
qed
|
|
786 |
|
|
787 |
lemma fract_content_fract_poly [simp]: "fract_content (fract_poly p) = to_fract (content p)"
|
|
788 |
proof -
|
|
789 |
have "Lcm_coeff_denoms (fract_poly p) = 1"
|
|
790 |
by (auto simp: Lcm_1_iff set_coeffs_map_poly)
|
|
791 |
hence "fract_content (fract_poly p) =
|
|
792 |
to_fract (content (map_poly (fst \<circ> quot_of_fract \<circ> to_fract) p))"
|
|
793 |
by (simp add: fract_content_def to_fract_def fract_collapse map_poly_map_poly del: Lcm_1_iff)
|
|
794 |
also have "map_poly (fst \<circ> quot_of_fract \<circ> to_fract) p = p"
|
|
795 |
by (intro map_poly_idI) simp_all
|
|
796 |
finally show ?thesis .
|
|
797 |
qed
|
|
798 |
|
|
799 |
lemma content_decompose_fract:
|
|
800 |
fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} fract poly"
|
|
801 |
obtains c p' where "p = smult c (map_poly to_fract p')" "content p' = 1"
|
|
802 |
proof (cases "p = 0")
|
|
803 |
case True
|
|
804 |
hence "p = smult 0 (map_poly to_fract 1)" "content 1 = 1" by simp_all
|
|
805 |
thus ?thesis ..
|
|
806 |
next
|
|
807 |
case False
|
|
808 |
thus ?thesis
|
|
809 |
by (rule that[OF content_times_primitive_part_fract [symmetric] content_primitive_part_fract])
|
|
810 |
qed
|
|
811 |
|
|
812 |
|
|
813 |
subsection \<open>More properties of content and primitive part\<close>
|
|
814 |
|
|
815 |
lemma lift_prime_elem_poly:
|
|
816 |
assumes "is_prime_elem (c :: 'a :: semidom)"
|
|
817 |
shows "is_prime_elem [:c:]"
|
|
818 |
proof (rule is_prime_elemI)
|
|
819 |
fix a b assume *: "[:c:] dvd a * b"
|
|
820 |
from * have dvd: "c dvd coeff (a * b) n" for n
|
|
821 |
by (subst (asm) const_poly_dvd_iff) blast
|
|
822 |
{
|
|
823 |
define m where "m = (GREATEST m. \<not>c dvd coeff b m)"
|
|
824 |
assume "\<not>[:c:] dvd b"
|
|
825 |
hence A: "\<exists>i. \<not>c dvd coeff b i" by (subst (asm) const_poly_dvd_iff) blast
|
|
826 |
have B: "\<forall>i. \<not>c dvd coeff b i \<longrightarrow> i < Suc (degree b)"
|
|
827 |
by (auto intro: le_degree simp: less_Suc_eq_le)
|
|
828 |
have coeff_m: "\<not>c dvd coeff b m" unfolding m_def by (rule GreatestI_ex[OF A B])
|
|
829 |
have "i \<le> m" if "\<not>c dvd coeff b i" for i
|
|
830 |
unfolding m_def by (rule Greatest_le[OF that B])
|
|
831 |
hence dvd_b: "c dvd coeff b i" if "i > m" for i using that by force
|
|
832 |
|
|
833 |
have "c dvd coeff a i" for i
|
|
834 |
proof (induction i rule: nat_descend_induct[of "degree a"])
|
|
835 |
case (base i)
|
|
836 |
thus ?case by (simp add: coeff_eq_0)
|
|
837 |
next
|
|
838 |
case (descend i)
|
|
839 |
let ?A = "{..i+m} - {i}"
|
|
840 |
have "c dvd coeff (a * b) (i + m)" by (rule dvd)
|
|
841 |
also have "coeff (a * b) (i + m) = (\<Sum>k\<le>i + m. coeff a k * coeff b (i + m - k))"
|
|
842 |
by (simp add: coeff_mult)
|
|
843 |
also have "{..i+m} = insert i ?A" by auto
|
|
844 |
also have "(\<Sum>k\<in>\<dots>. coeff a k * coeff b (i + m - k)) =
|
|
845 |
coeff a i * coeff b m + (\<Sum>k\<in>?A. coeff a k * coeff b (i + m - k))"
|
|
846 |
(is "_ = _ + ?S")
|
|
847 |
by (subst setsum.insert) simp_all
|
|
848 |
finally have eq: "c dvd coeff a i * coeff b m + ?S" .
|
|
849 |
moreover have "c dvd ?S"
|
|
850 |
proof (rule dvd_setsum)
|
|
851 |
fix k assume k: "k \<in> {..i+m} - {i}"
|
|
852 |
show "c dvd coeff a k * coeff b (i + m - k)"
|
|
853 |
proof (cases "k < i")
|
|
854 |
case False
|
|
855 |
with k have "c dvd coeff a k" by (intro descend.IH) simp
|
|
856 |
thus ?thesis by simp
|
|
857 |
next
|
|
858 |
case True
|
|
859 |
hence "c dvd coeff b (i + m - k)" by (intro dvd_b) simp
|
|
860 |
thus ?thesis by simp
|
|
861 |
qed
|
|
862 |
qed
|
|
863 |
ultimately have "c dvd coeff a i * coeff b m"
|
|
864 |
by (simp add: dvd_add_left_iff)
|
|
865 |
with assms coeff_m show "c dvd coeff a i"
|
|
866 |
by (simp add: prime_dvd_mult_iff)
|
|
867 |
qed
|
|
868 |
hence "[:c:] dvd a" by (subst const_poly_dvd_iff) blast
|
|
869 |
}
|
|
870 |
thus "[:c:] dvd a \<or> [:c:] dvd b" by blast
|
|
871 |
qed (insert assms, simp_all add: is_prime_elem_def one_poly_def)
|
|
872 |
|
|
873 |
lemma prime_elem_const_poly_iff:
|
|
874 |
fixes c :: "'a :: semidom"
|
|
875 |
shows "is_prime_elem [:c:] \<longleftrightarrow> is_prime_elem c"
|
|
876 |
proof
|
|
877 |
assume A: "is_prime_elem [:c:]"
|
|
878 |
show "is_prime_elem c"
|
|
879 |
proof (rule is_prime_elemI)
|
|
880 |
fix a b assume "c dvd a * b"
|
|
881 |
hence "[:c:] dvd [:a:] * [:b:]" by (simp add: mult_ac)
|
|
882 |
from A and this have "[:c:] dvd [:a:] \<or> [:c:] dvd [:b:]" by (rule prime_divides_productD)
|
|
883 |
thus "c dvd a \<or> c dvd b" by simp
|
|
884 |
qed (insert A, auto simp: is_prime_elem_def is_unit_poly_iff)
|
|
885 |
qed (auto intro: lift_prime_elem_poly)
|
|
886 |
|
|
887 |
context
|
|
888 |
begin
|
|
889 |
|
|
890 |
private lemma content_1_mult:
|
|
891 |
fixes f g :: "'a :: {semiring_Gcd,factorial_semiring} poly"
|
|
892 |
assumes "content f = 1" "content g = 1"
|
|
893 |
shows "content (f * g) = 1"
|
|
894 |
proof (cases "f * g = 0")
|
|
895 |
case False
|
|
896 |
from assms have "f \<noteq> 0" "g \<noteq> 0" by auto
|
|
897 |
|
|
898 |
hence "f * g \<noteq> 0" by auto
|
|
899 |
{
|
|
900 |
assume "\<not>is_unit (content (f * g))"
|
|
901 |
with False have "\<exists>p. p dvd content (f * g) \<and> is_prime p"
|
|
902 |
by (intro prime_divisor_exists) simp_all
|
|
903 |
then obtain p where "p dvd content (f * g)" "is_prime p" by blast
|
|
904 |
from \<open>p dvd content (f * g)\<close> have "[:p:] dvd f * g"
|
|
905 |
by (simp add: const_poly_dvd_iff_dvd_content)
|
|
906 |
moreover from \<open>is_prime p\<close> have "is_prime_elem [:p:]" by (simp add: lift_prime_elem_poly)
|
|
907 |
ultimately have "[:p:] dvd f \<or> [:p:] dvd g"
|
|
908 |
by (simp add: prime_dvd_mult_iff)
|
|
909 |
with assms have "is_unit p" by (simp add: const_poly_dvd_iff_dvd_content)
|
|
910 |
with \<open>is_prime p\<close> have False by simp
|
|
911 |
}
|
|
912 |
hence "is_unit (content (f * g))" by blast
|
|
913 |
hence "normalize (content (f * g)) = 1" by (simp add: is_unit_normalize del: normalize_content)
|
|
914 |
thus ?thesis by simp
|
|
915 |
qed (insert assms, auto)
|
|
916 |
|
|
917 |
lemma content_mult:
|
|
918 |
fixes p q :: "'a :: {factorial_semiring, semiring_Gcd} poly"
|
|
919 |
shows "content (p * q) = content p * content q"
|
|
920 |
proof -
|
|
921 |
from content_decompose[of p] guess p' . note p = this
|
|
922 |
from content_decompose[of q] guess q' . note q = this
|
|
923 |
have "content (p * q) = content p * content q * content (p' * q')"
|
|
924 |
by (subst p, subst q) (simp add: mult_ac normalize_mult)
|
|
925 |
also from p q have "content (p' * q') = 1" by (intro content_1_mult)
|
|
926 |
finally show ?thesis by simp
|
|
927 |
qed
|
|
928 |
|
|
929 |
lemma primitive_part_mult:
|
|
930 |
fixes p q :: "'a :: {factorial_semiring, semiring_Gcd, ring_gcd, idom_divide} poly"
|
|
931 |
shows "primitive_part (p * q) = primitive_part p * primitive_part q"
|
|
932 |
proof -
|
|
933 |
have "primitive_part (p * q) = p * q div [:content (p * q):]"
|
|
934 |
by (simp add: primitive_part_def div_const_poly_conv_map_poly)
|
|
935 |
also have "\<dots> = (p div [:content p:]) * (q div [:content q:])"
|
|
936 |
by (subst div_mult_div_if_dvd) (simp_all add: content_mult mult_ac)
|
|
937 |
also have "\<dots> = primitive_part p * primitive_part q"
|
|
938 |
by (simp add: primitive_part_def div_const_poly_conv_map_poly)
|
|
939 |
finally show ?thesis .
|
|
940 |
qed
|
|
941 |
|
|
942 |
lemma primitive_part_smult:
|
|
943 |
fixes p :: "'a :: {factorial_semiring, semiring_Gcd, ring_gcd, idom_divide} poly"
|
|
944 |
shows "primitive_part (smult a p) = smult (unit_factor a) (primitive_part p)"
|
|
945 |
proof -
|
|
946 |
have "smult a p = [:a:] * p" by simp
|
|
947 |
also have "primitive_part \<dots> = smult (unit_factor a) (primitive_part p)"
|
|
948 |
by (subst primitive_part_mult) simp_all
|
|
949 |
finally show ?thesis .
|
|
950 |
qed
|
|
951 |
|
|
952 |
lemma primitive_part_dvd_primitive_partI [intro]:
|
|
953 |
fixes p q :: "'a :: {factorial_semiring, semiring_Gcd, ring_gcd, idom_divide} poly"
|
|
954 |
shows "p dvd q \<Longrightarrow> primitive_part p dvd primitive_part q"
|
|
955 |
by (auto elim!: dvdE simp: primitive_part_mult)
|
|
956 |
|
|
957 |
lemma content_msetprod:
|
|
958 |
fixes A :: "'a :: {factorial_semiring, semiring_Gcd} poly multiset"
|
|
959 |
shows "content (msetprod A) = msetprod (image_mset content A)"
|
|
960 |
by (induction A) (simp_all add: content_mult mult_ac)
|
|
961 |
|
|
962 |
lemma fract_poly_dvdD:
|
|
963 |
fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} poly"
|
|
964 |
assumes "fract_poly p dvd fract_poly q" "content p = 1"
|
|
965 |
shows "p dvd q"
|
|
966 |
proof -
|
|
967 |
from assms(1) obtain r where r: "fract_poly q = fract_poly p * r" by (erule dvdE)
|
|
968 |
from content_decompose_fract[of r] guess c r' . note r' = this
|
|
969 |
from r r' have eq: "fract_poly q = smult c (fract_poly (p * r'))" by simp
|
|
970 |
from fract_poly_smult_eqE[OF this] guess a b . note ab = this
|
|
971 |
have "content (smult a q) = content (smult b (p * r'))" by (simp only: ab(2))
|
|
972 |
hence eq': "normalize b = a * content q" by (simp add: assms content_mult r' ab(4))
|
|
973 |
have "1 = gcd a (normalize b)" by (simp add: ab)
|
|
974 |
also note eq'
|
|
975 |
also have "gcd a (a * content q) = a" by (simp add: gcd_proj1_if_dvd ab(4))
|
|
976 |
finally have [simp]: "a = 1" by simp
|
|
977 |
from eq ab have "q = p * ([:b:] * r')" by simp
|
|
978 |
thus ?thesis by (rule dvdI)
|
|
979 |
qed
|
|
980 |
|
|
981 |
lemma content_prod_eq_1_iff:
|
|
982 |
fixes p q :: "'a :: {factorial_semiring, semiring_Gcd} poly"
|
|
983 |
shows "content (p * q) = 1 \<longleftrightarrow> content p = 1 \<and> content q = 1"
|
|
984 |
proof safe
|
|
985 |
assume A: "content (p * q) = 1"
|
|
986 |
{
|
|
987 |
fix p q :: "'a poly" assume "content p * content q = 1"
|
|
988 |
hence "1 = content p * content q" by simp
|
|
989 |
hence "content p dvd 1" by (rule dvdI)
|
|
990 |
hence "content p = 1" by simp
|
|
991 |
} note B = this
|
|
992 |
from A B[of p q] B [of q p] show "content p = 1" "content q = 1"
|
|
993 |
by (simp_all add: content_mult mult_ac)
|
|
994 |
qed (auto simp: content_mult)
|
|
995 |
|
|
996 |
end
|
|
997 |
|
|
998 |
|
|
999 |
subsection \<open>Polynomials over a field are a Euclidean ring\<close>
|
|
1000 |
|
|
1001 |
context
|
|
1002 |
begin
|
|
1003 |
|
|
1004 |
private definition unit_factor_field_poly :: "'a :: field poly \<Rightarrow> 'a poly" where
|
|
1005 |
"unit_factor_field_poly p = [:lead_coeff p:]"
|
|
1006 |
|
|
1007 |
private definition normalize_field_poly :: "'a :: field poly \<Rightarrow> 'a poly" where
|
|
1008 |
"normalize_field_poly p = smult (inverse (lead_coeff p)) p"
|
|
1009 |
|
|
1010 |
private definition euclidean_size_field_poly :: "'a :: field poly \<Rightarrow> nat" where
|
|
1011 |
"euclidean_size_field_poly p = (if p = 0 then 0 else 2 ^ degree p)"
|
|
1012 |
|
|
1013 |
private lemma dvd_field_poly: "dvd.dvd (op * :: 'a :: field poly \<Rightarrow> _) = op dvd"
|
|
1014 |
by (intro ext) (simp_all add: dvd.dvd_def dvd_def)
|
|
1015 |
|
|
1016 |
interpretation field_poly:
|
|
1017 |
euclidean_ring "op div" "op *" "op mod" "op +" "op -" 0 "1 :: 'a :: field poly"
|
|
1018 |
normalize_field_poly unit_factor_field_poly euclidean_size_field_poly uminus
|
|
1019 |
proof (standard, unfold dvd_field_poly)
|
|
1020 |
fix p :: "'a poly"
|
|
1021 |
show "unit_factor_field_poly p * normalize_field_poly p = p"
|
|
1022 |
by (cases "p = 0")
|
|
1023 |
(simp_all add: unit_factor_field_poly_def normalize_field_poly_def lead_coeff_nonzero)
|
|
1024 |
next
|
|
1025 |
fix p :: "'a poly" assume "is_unit p"
|
|
1026 |
thus "normalize_field_poly p = 1"
|
|
1027 |
by (elim is_unit_polyE) (auto simp: normalize_field_poly_def monom_0 one_poly_def field_simps)
|
|
1028 |
next
|
|
1029 |
fix p :: "'a poly" assume "p \<noteq> 0"
|
|
1030 |
thus "is_unit (unit_factor_field_poly p)"
|
|
1031 |
by (simp add: unit_factor_field_poly_def lead_coeff_nonzero is_unit_pCons_iff)
|
|
1032 |
qed (auto simp: unit_factor_field_poly_def normalize_field_poly_def lead_coeff_mult
|
|
1033 |
euclidean_size_field_poly_def intro!: degree_mod_less' degree_mult_right_le)
|
|
1034 |
|
|
1035 |
private lemma field_poly_irreducible_imp_prime:
|
|
1036 |
assumes "irreducible (p :: 'a :: field poly)"
|
|
1037 |
shows "is_prime_elem p"
|
|
1038 |
proof -
|
|
1039 |
have A: "class.comm_semiring_1 op * 1 op + (0 :: 'a poly)" ..
|
|
1040 |
from field_poly.irreducible_imp_prime[of p] assms
|
|
1041 |
show ?thesis unfolding irreducible_def is_prime_elem_def dvd_field_poly
|
|
1042 |
comm_semiring_1.irreducible_def[OF A] comm_semiring_1.is_prime_elem_def[OF A] by blast
|
|
1043 |
qed
|
|
1044 |
|
|
1045 |
private lemma field_poly_msetprod_prime_factorization:
|
|
1046 |
assumes "(x :: 'a :: field poly) \<noteq> 0"
|
|
1047 |
shows "msetprod (field_poly.prime_factorization x) = normalize_field_poly x"
|
|
1048 |
proof -
|
|
1049 |
have A: "class.comm_monoid_mult op * (1 :: 'a poly)" ..
|
|
1050 |
have "comm_monoid_mult.msetprod op * (1 :: 'a poly) = msetprod"
|
|
1051 |
by (intro ext) (simp add: comm_monoid_mult.msetprod_def[OF A] msetprod_def)
|
|
1052 |
with field_poly.msetprod_prime_factorization[OF assms] show ?thesis by simp
|
|
1053 |
qed
|
|
1054 |
|
|
1055 |
private lemma field_poly_in_prime_factorization_imp_prime:
|
|
1056 |
assumes "(p :: 'a :: field poly) \<in># field_poly.prime_factorization x"
|
|
1057 |
shows "is_prime_elem p"
|
|
1058 |
proof -
|
|
1059 |
have A: "class.comm_semiring_1 op * 1 op + (0 :: 'a poly)" ..
|
|
1060 |
have B: "class.normalization_semidom op div op + op - (0 :: 'a poly) op * 1
|
|
1061 |
normalize_field_poly unit_factor_field_poly" ..
|
|
1062 |
from field_poly.in_prime_factorization_imp_prime[of p x] assms
|
|
1063 |
show ?thesis unfolding is_prime_elem_def dvd_field_poly
|
|
1064 |
comm_semiring_1.is_prime_elem_def[OF A] normalization_semidom.is_prime_def[OF B] by blast
|
|
1065 |
qed
|
|
1066 |
|
|
1067 |
|
|
1068 |
subsection \<open>Primality and irreducibility in polynomial rings\<close>
|
|
1069 |
|
|
1070 |
lemma nonconst_poly_irreducible_iff:
|
|
1071 |
fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} poly"
|
|
1072 |
assumes "degree p \<noteq> 0"
|
|
1073 |
shows "irreducible p \<longleftrightarrow> irreducible (fract_poly p) \<and> content p = 1"
|
|
1074 |
proof safe
|
|
1075 |
assume p: "irreducible p"
|
|
1076 |
|
|
1077 |
from content_decompose[of p] guess p' . note p' = this
|
|
1078 |
hence "p = [:content p:] * p'" by simp
|
|
1079 |
from p this have "[:content p:] dvd 1 \<or> p' dvd 1" by (rule irreducibleD)
|
|
1080 |
moreover have "\<not>p' dvd 1"
|
|
1081 |
proof
|
|
1082 |
assume "p' dvd 1"
|
|
1083 |
hence "degree p = 0" by (subst p') (auto simp: is_unit_poly_iff)
|
|
1084 |
with assms show False by contradiction
|
|
1085 |
qed
|
|
1086 |
ultimately show [simp]: "content p = 1" by (simp add: is_unit_const_poly_iff)
|
|
1087 |
|
|
1088 |
show "irreducible (map_poly to_fract p)"
|
|
1089 |
proof (rule irreducibleI)
|
|
1090 |
have "fract_poly p = 0 \<longleftrightarrow> p = 0" by (intro map_poly_eq_0_iff) auto
|
|
1091 |
with assms show "map_poly to_fract p \<noteq> 0" by auto
|
|
1092 |
next
|
|
1093 |
show "\<not>is_unit (fract_poly p)"
|
|
1094 |
proof
|
|
1095 |
assume "is_unit (map_poly to_fract p)"
|
|
1096 |
hence "degree (map_poly to_fract p) = 0"
|
|
1097 |
by (auto simp: is_unit_poly_iff)
|
|
1098 |
hence "degree p = 0" by (simp add: degree_map_poly)
|
|
1099 |
with assms show False by contradiction
|
|
1100 |
qed
|
|
1101 |
next
|
|
1102 |
fix q r assume qr: "fract_poly p = q * r"
|
|
1103 |
from content_decompose_fract[of q] guess cg q' . note q = this
|
|
1104 |
from content_decompose_fract[of r] guess cr r' . note r = this
|
|
1105 |
from qr q r p have nz: "cg \<noteq> 0" "cr \<noteq> 0" by auto
|
|
1106 |
from qr have eq: "fract_poly p = smult (cr * cg) (fract_poly (q' * r'))"
|
|
1107 |
by (simp add: q r)
|
|
1108 |
from fract_poly_smult_eqE[OF this] guess a b . note ab = this
|
|
1109 |
hence "content (smult a p) = content (smult b (q' * r'))" by (simp only:)
|
|
1110 |
with ab(4) have a: "a = normalize b" by (simp add: content_mult q r)
|
|
1111 |
hence "normalize b = gcd a b" by simp
|
|
1112 |
also from ab(3) have "\<dots> = 1" .
|
|
1113 |
finally have "a = 1" "is_unit b" by (simp_all add: a normalize_1_iff)
|
|
1114 |
|
|
1115 |
note eq
|
|
1116 |
also from ab(1) \<open>a = 1\<close> have "cr * cg = to_fract b" by simp
|
|
1117 |
also have "smult \<dots> (fract_poly (q' * r')) = fract_poly (smult b (q' * r'))" by simp
|
|
1118 |
finally have "p = ([:b:] * q') * r'" by (simp del: fract_poly_smult)
|
|
1119 |
from p and this have "([:b:] * q') dvd 1 \<or> r' dvd 1" by (rule irreducibleD)
|
|
1120 |
hence "q' dvd 1 \<or> r' dvd 1" by (auto dest: dvd_mult_right simp del: mult_pCons_left)
|
|
1121 |
hence "fract_poly q' dvd 1 \<or> fract_poly r' dvd 1" by (auto simp: fract_poly_is_unit)
|
|
1122 |
with q r show "is_unit q \<or> is_unit r"
|
|
1123 |
by (auto simp add: is_unit_smult_iff dvd_field_iff nz)
|
|
1124 |
qed
|
|
1125 |
|
|
1126 |
next
|
|
1127 |
|
|
1128 |
assume irred: "irreducible (fract_poly p)" and primitive: "content p = 1"
|
|
1129 |
show "irreducible p"
|
|
1130 |
proof (rule irreducibleI)
|
|
1131 |
from irred show "p \<noteq> 0" by auto
|
|
1132 |
next
|
|
1133 |
from irred show "\<not>p dvd 1"
|
|
1134 |
by (auto simp: irreducible_def dest: fract_poly_is_unit)
|
|
1135 |
next
|
|
1136 |
fix q r assume qr: "p = q * r"
|
|
1137 |
hence "fract_poly p = fract_poly q * fract_poly r" by simp
|
|
1138 |
from irred and this have "fract_poly q dvd 1 \<or> fract_poly r dvd 1"
|
|
1139 |
by (rule irreducibleD)
|
|
1140 |
with primitive qr show "q dvd 1 \<or> r dvd 1"
|
|
1141 |
by (auto simp: content_prod_eq_1_iff is_unit_fract_poly_iff)
|
|
1142 |
qed
|
|
1143 |
qed
|
|
1144 |
|
|
1145 |
private lemma irreducible_imp_prime_poly:
|
|
1146 |
fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} poly"
|
|
1147 |
assumes "irreducible p"
|
|
1148 |
shows "is_prime_elem p"
|
|
1149 |
proof (cases "degree p = 0")
|
|
1150 |
case True
|
|
1151 |
with assms show ?thesis
|
|
1152 |
by (auto simp: prime_elem_const_poly_iff irreducible_const_poly_iff
|
|
1153 |
intro!: irreducible_imp_prime elim!: degree_eq_zeroE)
|
|
1154 |
next
|
|
1155 |
case False
|
|
1156 |
from assms False have irred: "irreducible (fract_poly p)" and primitive: "content p = 1"
|
|
1157 |
by (simp_all add: nonconst_poly_irreducible_iff)
|
|
1158 |
from irred have prime: "is_prime_elem (fract_poly p)" by (rule field_poly_irreducible_imp_prime)
|
|
1159 |
show ?thesis
|
|
1160 |
proof (rule is_prime_elemI)
|
|
1161 |
fix q r assume "p dvd q * r"
|
|
1162 |
hence "fract_poly p dvd fract_poly (q * r)" by (rule fract_poly_dvd)
|
|
1163 |
hence "fract_poly p dvd fract_poly q * fract_poly r" by simp
|
|
1164 |
from prime and this have "fract_poly p dvd fract_poly q \<or> fract_poly p dvd fract_poly r"
|
|
1165 |
by (rule prime_divides_productD)
|
|
1166 |
with primitive show "p dvd q \<or> p dvd r" by (auto dest: fract_poly_dvdD)
|
|
1167 |
qed (insert assms, auto simp: irreducible_def)
|
|
1168 |
qed
|
|
1169 |
|
|
1170 |
|
|
1171 |
lemma degree_primitive_part_fract [simp]:
|
|
1172 |
"degree (primitive_part_fract p) = degree p"
|
|
1173 |
proof -
|
|
1174 |
have "p = smult (fract_content p) (fract_poly (primitive_part_fract p))"
|
|
1175 |
by (simp add: content_times_primitive_part_fract)
|
|
1176 |
also have "degree \<dots> = degree (primitive_part_fract p)"
|
|
1177 |
by (auto simp: degree_map_poly)
|
|
1178 |
finally show ?thesis ..
|
|
1179 |
qed
|
|
1180 |
|
|
1181 |
lemma irreducible_primitive_part_fract:
|
|
1182 |
fixes p :: "'a :: {idom_divide, ring_gcd, factorial_semiring, semiring_Gcd} fract poly"
|
|
1183 |
assumes "irreducible p"
|
|
1184 |
shows "irreducible (primitive_part_fract p)"
|
|
1185 |
proof -
|
|
1186 |
from assms have deg: "degree (primitive_part_fract p) \<noteq> 0"
|
|
1187 |
by (intro notI)
|
|
1188 |
(auto elim!: degree_eq_zeroE simp: irreducible_def is_unit_poly_iff dvd_field_iff)
|
|
1189 |
hence [simp]: "p \<noteq> 0" by auto
|
|
1190 |
|
|
1191 |
note \<open>irreducible p\<close>
|
|
1192 |
also have "p = [:fract_content p:] * fract_poly (primitive_part_fract p)"
|
|
1193 |
by (simp add: content_times_primitive_part_fract)
|
|
1194 |
also have "irreducible \<dots> \<longleftrightarrow> irreducible (fract_poly (primitive_part_fract p))"
|
|
1195 |
by (intro irreducible_mult_unit_left) (simp_all add: is_unit_poly_iff dvd_field_iff)
|
|
1196 |
finally show ?thesis using deg
|
|
1197 |
by (simp add: nonconst_poly_irreducible_iff)
|
|
1198 |
qed
|
|
1199 |
|
|
1200 |
lemma is_prime_elem_primitive_part_fract:
|
|
1201 |
fixes p :: "'a :: {idom_divide, ring_gcd, factorial_semiring, semiring_Gcd} fract poly"
|
|
1202 |
shows "irreducible p \<Longrightarrow> is_prime_elem (primitive_part_fract p)"
|
|
1203 |
by (intro irreducible_imp_prime_poly irreducible_primitive_part_fract)
|
|
1204 |
|
|
1205 |
lemma irreducible_linear_field_poly:
|
|
1206 |
fixes a b :: "'a::field"
|
|
1207 |
assumes "b \<noteq> 0"
|
|
1208 |
shows "irreducible [:a,b:]"
|
|
1209 |
proof (rule irreducibleI)
|
|
1210 |
fix p q assume pq: "[:a,b:] = p * q"
|
|
1211 |
also from this assms have "degree \<dots> = degree p + degree q"
|
|
1212 |
by (intro degree_mult_eq) auto
|
|
1213 |
finally have "degree p = 0 \<or> degree q = 0" using assms by auto
|
|
1214 |
with assms pq show "is_unit p \<or> is_unit q"
|
|
1215 |
by (auto simp: is_unit_const_poly_iff dvd_field_iff elim!: degree_eq_zeroE)
|
|
1216 |
qed (insert assms, auto simp: is_unit_poly_iff)
|
|
1217 |
|
|
1218 |
lemma is_prime_elem_linear_field_poly:
|
|
1219 |
"(b :: 'a :: field) \<noteq> 0 \<Longrightarrow> is_prime_elem [:a,b:]"
|
|
1220 |
by (rule field_poly_irreducible_imp_prime, rule irreducible_linear_field_poly)
|
|
1221 |
|
|
1222 |
lemma irreducible_linear_poly:
|
|
1223 |
fixes a b :: "'a::{idom_divide,ring_gcd,factorial_semiring,semiring_Gcd}"
|
|
1224 |
shows "b \<noteq> 0 \<Longrightarrow> coprime a b \<Longrightarrow> irreducible [:a,b:]"
|
|
1225 |
by (auto intro!: irreducible_linear_field_poly
|
|
1226 |
simp: nonconst_poly_irreducible_iff content_def map_poly_pCons)
|
|
1227 |
|
|
1228 |
lemma is_prime_elem_linear_poly:
|
|
1229 |
fixes a b :: "'a::{idom_divide,ring_gcd,factorial_semiring,semiring_Gcd}"
|
|
1230 |
shows "b \<noteq> 0 \<Longrightarrow> coprime a b \<Longrightarrow> is_prime_elem [:a,b:]"
|
|
1231 |
by (rule irreducible_imp_prime_poly, rule irreducible_linear_poly)
|
|
1232 |
|
|
1233 |
|
|
1234 |
subsection \<open>Prime factorisation of polynomials\<close>
|
|
1235 |
|
|
1236 |
private lemma poly_prime_factorization_exists_content_1:
|
|
1237 |
fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} poly"
|
|
1238 |
assumes "p \<noteq> 0" "content p = 1"
|
|
1239 |
shows "\<exists>A. (\<forall>p. p \<in># A \<longrightarrow> is_prime_elem p) \<and> msetprod A = normalize p"
|
|
1240 |
proof -
|
|
1241 |
let ?P = "field_poly.prime_factorization (fract_poly p)"
|
|
1242 |
define c where "c = msetprod (image_mset fract_content ?P)"
|
|
1243 |
define c' where "c' = c * to_fract (lead_coeff p)"
|
|
1244 |
define e where "e = msetprod (image_mset primitive_part_fract ?P)"
|
|
1245 |
define A where "A = image_mset (normalize \<circ> primitive_part_fract) ?P"
|
|
1246 |
have "content e = (\<Prod>x\<in>#field_poly.prime_factorization (map_poly to_fract p).
|
|
1247 |
content (primitive_part_fract x))"
|
|
1248 |
by (simp add: e_def content_msetprod multiset.map_comp o_def)
|
|
1249 |
also have "image_mset (\<lambda>x. content (primitive_part_fract x)) ?P = image_mset (\<lambda>_. 1) ?P"
|
|
1250 |
by (intro image_mset_cong content_primitive_part_fract) auto
|
|
1251 |
finally have content_e: "content e = 1" by (simp add: msetprod_const)
|
|
1252 |
|
|
1253 |
have "fract_poly p = unit_factor_field_poly (fract_poly p) *
|
|
1254 |
normalize_field_poly (fract_poly p)" by simp
|
|
1255 |
also have "unit_factor_field_poly (fract_poly p) = [:to_fract (lead_coeff p):]"
|
|
1256 |
by (simp add: unit_factor_field_poly_def lead_coeff_def monom_0 degree_map_poly coeff_map_poly)
|
|
1257 |
also from assms have "normalize_field_poly (fract_poly p) = msetprod ?P"
|
|
1258 |
by (subst field_poly_msetprod_prime_factorization) simp_all
|
|
1259 |
also have "\<dots> = msetprod (image_mset id ?P)" by simp
|
|
1260 |
also have "image_mset id ?P =
|
|
1261 |
image_mset (\<lambda>x. [:fract_content x:] * fract_poly (primitive_part_fract x)) ?P"
|
|
1262 |
by (intro image_mset_cong) (auto simp: content_times_primitive_part_fract)
|
|
1263 |
also have "msetprod \<dots> = smult c (fract_poly e)"
|
|
1264 |
by (subst msetprod_mult) (simp_all add: msetprod_fract_poly msetprod_const_poly c_def e_def)
|
|
1265 |
also have "[:to_fract (lead_coeff p):] * \<dots> = smult c' (fract_poly e)"
|
|
1266 |
by (simp add: c'_def)
|
|
1267 |
finally have eq: "fract_poly p = smult c' (fract_poly e)" .
|
|
1268 |
also obtain b where b: "c' = to_fract b" "is_unit b"
|
|
1269 |
proof -
|
|
1270 |
from fract_poly_smult_eqE[OF eq] guess a b . note ab = this
|
|
1271 |
from ab(2) have "content (smult a p) = content (smult b e)" by (simp only: )
|
|
1272 |
with assms content_e have "a = normalize b" by (simp add: ab(4))
|
|
1273 |
with ab have ab': "a = 1" "is_unit b" by (simp_all add: normalize_1_iff)
|
|
1274 |
with ab ab' have "c' = to_fract b" by auto
|
|
1275 |
from this and \<open>is_unit b\<close> show ?thesis by (rule that)
|
|
1276 |
qed
|
|
1277 |
hence "smult c' (fract_poly e) = fract_poly (smult b e)" by simp
|
|
1278 |
finally have "p = smult b e" by (simp only: fract_poly_eq_iff)
|
|
1279 |
hence "p = [:b:] * e" by simp
|
|
1280 |
with b have "normalize p = normalize e"
|
|
1281 |
by (simp only: normalize_mult) (simp add: is_unit_normalize is_unit_poly_iff)
|
|
1282 |
also have "normalize e = msetprod A"
|
|
1283 |
by (simp add: multiset.map_comp e_def A_def normalize_msetprod)
|
|
1284 |
finally have "msetprod A = normalize p" ..
|
|
1285 |
|
|
1286 |
have "is_prime_elem p" if "p \<in># A" for p
|
|
1287 |
using that by (auto simp: A_def is_prime_elem_primitive_part_fract prime_imp_irreducible
|
|
1288 |
dest!: field_poly_in_prime_factorization_imp_prime )
|
|
1289 |
from this and \<open>msetprod A = normalize p\<close> show ?thesis
|
|
1290 |
by (intro exI[of _ A]) blast
|
|
1291 |
qed
|
|
1292 |
|
|
1293 |
lemma poly_prime_factorization_exists:
|
|
1294 |
fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} poly"
|
|
1295 |
assumes "p \<noteq> 0"
|
|
1296 |
shows "\<exists>A. (\<forall>p. p \<in># A \<longrightarrow> is_prime_elem p) \<and> msetprod A = normalize p"
|
|
1297 |
proof -
|
|
1298 |
define B where "B = image_mset (\<lambda>x. [:x:]) (prime_factorization (content p))"
|
|
1299 |
have "\<exists>A. (\<forall>p. p \<in># A \<longrightarrow> is_prime_elem p) \<and> msetprod A = normalize (primitive_part p)"
|
|
1300 |
by (rule poly_prime_factorization_exists_content_1) (insert assms, simp_all)
|
|
1301 |
then guess A by (elim exE conjE) note A = this
|
|
1302 |
moreover from assms have "msetprod B = [:content p:]"
|
|
1303 |
by (simp add: B_def msetprod_const_poly msetprod_prime_factorization)
|
|
1304 |
moreover have "\<forall>p. p \<in># B \<longrightarrow> is_prime_elem p"
|
|
1305 |
by (auto simp: B_def intro: lift_prime_elem_poly dest: in_prime_factorization_imp_prime)
|
|
1306 |
ultimately show ?thesis by (intro exI[of _ "B + A"]) auto
|
|
1307 |
qed
|
|
1308 |
|
|
1309 |
end
|
|
1310 |
|
|
1311 |
|
|
1312 |
subsection \<open>Typeclass instances\<close>
|
|
1313 |
|
|
1314 |
instance poly :: (factorial_ring_gcd) factorial_semiring
|
|
1315 |
by standard (rule poly_prime_factorization_exists)
|
|
1316 |
|
|
1317 |
instantiation poly :: (factorial_ring_gcd) factorial_ring_gcd
|
|
1318 |
begin
|
|
1319 |
|
|
1320 |
definition gcd_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly" where
|
|
1321 |
[code del]: "gcd_poly = gcd_factorial"
|
|
1322 |
|
|
1323 |
definition lcm_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly" where
|
|
1324 |
[code del]: "lcm_poly = lcm_factorial"
|
|
1325 |
|
|
1326 |
definition Gcd_poly :: "'a poly set \<Rightarrow> 'a poly" where
|
|
1327 |
[code del]: "Gcd_poly = Gcd_factorial"
|
|
1328 |
|
|
1329 |
definition Lcm_poly :: "'a poly set \<Rightarrow> 'a poly" where
|
|
1330 |
[code del]: "Lcm_poly = Lcm_factorial"
|
|
1331 |
|
|
1332 |
instance by standard (simp_all add: gcd_poly_def lcm_poly_def Gcd_poly_def Lcm_poly_def)
|
|
1333 |
|
|
1334 |
end
|
|
1335 |
|
|
1336 |
instantiation poly :: ("{field,factorial_ring_gcd}") euclidean_ring
|
|
1337 |
begin
|
|
1338 |
|
|
1339 |
definition euclidean_size_poly :: "'a poly \<Rightarrow> nat" where
|
|
1340 |
"euclidean_size_poly p = (if p = 0 then 0 else 2 ^ degree p)"
|
|
1341 |
|
|
1342 |
instance
|
|
1343 |
by standard (auto simp: euclidean_size_poly_def intro!: degree_mod_less' degree_mult_right_le)
|
|
1344 |
end
|
|
1345 |
|
|
1346 |
instance poly :: ("{field,factorial_ring_gcd}") euclidean_ring_gcd
|
|
1347 |
by standard (simp_all add: gcd_poly_def lcm_poly_def Gcd_poly_def Lcm_poly_def eucl_eq_factorial)
|
|
1348 |
|
|
1349 |
|
|
1350 |
subsection \<open>Polynomial GCD\<close>
|
|
1351 |
|
|
1352 |
lemma gcd_poly_decompose:
|
|
1353 |
fixes p q :: "'a :: factorial_ring_gcd poly"
|
|
1354 |
shows "gcd p q =
|
|
1355 |
smult (gcd (content p) (content q)) (gcd (primitive_part p) (primitive_part q))"
|
|
1356 |
proof (rule sym, rule gcdI)
|
|
1357 |
have "[:gcd (content p) (content q):] * gcd (primitive_part p) (primitive_part q) dvd
|
|
1358 |
[:content p:] * primitive_part p" by (intro mult_dvd_mono) simp_all
|
|
1359 |
thus "smult (gcd (content p) (content q)) (gcd (primitive_part p) (primitive_part q)) dvd p"
|
|
1360 |
by simp
|
|
1361 |
next
|
|
1362 |
have "[:gcd (content p) (content q):] * gcd (primitive_part p) (primitive_part q) dvd
|
|
1363 |
[:content q:] * primitive_part q" by (intro mult_dvd_mono) simp_all
|
|
1364 |
thus "smult (gcd (content p) (content q)) (gcd (primitive_part p) (primitive_part q)) dvd q"
|
|
1365 |
by simp
|
|
1366 |
next
|
|
1367 |
fix d assume "d dvd p" "d dvd q"
|
|
1368 |
hence "[:content d:] * primitive_part d dvd
|
|
1369 |
[:gcd (content p) (content q):] * gcd (primitive_part p) (primitive_part q)"
|
|
1370 |
by (intro mult_dvd_mono) auto
|
|
1371 |
thus "d dvd smult (gcd (content p) (content q)) (gcd (primitive_part p) (primitive_part q))"
|
|
1372 |
by simp
|
|
1373 |
qed (auto simp: normalize_smult)
|
|
1374 |
|
|
1375 |
|
|
1376 |
lemma gcd_poly_pseudo_mod:
|
|
1377 |
fixes p q :: "'a :: factorial_ring_gcd poly"
|
|
1378 |
assumes nz: "q \<noteq> 0" and prim: "content p = 1" "content q = 1"
|
|
1379 |
shows "gcd p q = gcd q (primitive_part (pseudo_mod p q))"
|
|
1380 |
proof -
|
|
1381 |
define r s where "r = fst (pseudo_divmod p q)" and "s = snd (pseudo_divmod p q)"
|
|
1382 |
define a where "a = [:coeff q (degree q) ^ (Suc (degree p) - degree q):]"
|
|
1383 |
have [simp]: "primitive_part a = unit_factor a"
|
|
1384 |
by (simp add: a_def unit_factor_poly_def unit_factor_power monom_0)
|
|
1385 |
from nz have [simp]: "a \<noteq> 0" by (auto simp: a_def)
|
|
1386 |
|
|
1387 |
have rs: "pseudo_divmod p q = (r, s)" by (simp add: r_def s_def)
|
|
1388 |
have "gcd (q * r + s) q = gcd q s"
|
|
1389 |
using gcd_add_mult[of q r s] by (simp add: gcd.commute add_ac mult_ac)
|
|
1390 |
with pseudo_divmod(1)[OF nz rs]
|
|
1391 |
have "gcd (p * a) q = gcd q s" by (simp add: a_def)
|
|
1392 |
also from prim have "gcd (p * a) q = gcd p q"
|
|
1393 |
by (subst gcd_poly_decompose)
|
|
1394 |
(auto simp: primitive_part_mult gcd_mult_unit1 primitive_part_prim
|
|
1395 |
simp del: mult_pCons_right )
|
|
1396 |
also from prim have "gcd q s = gcd q (primitive_part s)"
|
|
1397 |
by (subst gcd_poly_decompose) (simp_all add: primitive_part_prim)
|
|
1398 |
also have "s = pseudo_mod p q" by (simp add: s_def pseudo_mod_def)
|
|
1399 |
finally show ?thesis .
|
|
1400 |
qed
|
|
1401 |
|
|
1402 |
lemma degree_pseudo_mod_less:
|
|
1403 |
assumes "q \<noteq> 0" "pseudo_mod p q \<noteq> 0"
|
|
1404 |
shows "degree (pseudo_mod p q) < degree q"
|
|
1405 |
using pseudo_mod(2)[of q p] assms by auto
|
|
1406 |
|
|
1407 |
function gcd_poly_code_aux :: "'a :: factorial_ring_gcd poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly" where
|
|
1408 |
"gcd_poly_code_aux p q =
|
|
1409 |
(if q = 0 then normalize p else gcd_poly_code_aux q (primitive_part (pseudo_mod p q)))"
|
|
1410 |
by auto
|
|
1411 |
termination
|
|
1412 |
by (relation "measure ((\<lambda>p. if p = 0 then 0 else Suc (degree p)) \<circ> snd)")
|
|
1413 |
(auto simp: degree_primitive_part degree_pseudo_mod_less)
|
|
1414 |
|
|
1415 |
declare gcd_poly_code_aux.simps [simp del]
|
|
1416 |
|
|
1417 |
lemma gcd_poly_code_aux_correct:
|
|
1418 |
assumes "content p = 1" "q = 0 \<or> content q = 1"
|
|
1419 |
shows "gcd_poly_code_aux p q = gcd p q"
|
|
1420 |
using assms
|
|
1421 |
proof (induction p q rule: gcd_poly_code_aux.induct)
|
|
1422 |
case (1 p q)
|
|
1423 |
show ?case
|
|
1424 |
proof (cases "q = 0")
|
|
1425 |
case True
|
|
1426 |
thus ?thesis by (subst gcd_poly_code_aux.simps) auto
|
|
1427 |
next
|
|
1428 |
case False
|
|
1429 |
hence "gcd_poly_code_aux p q = gcd_poly_code_aux q (primitive_part (pseudo_mod p q))"
|
|
1430 |
by (subst gcd_poly_code_aux.simps) simp_all
|
|
1431 |
also from "1.prems" False
|
|
1432 |
have "primitive_part (pseudo_mod p q) = 0 \<or>
|
|
1433 |
content (primitive_part (pseudo_mod p q)) = 1"
|
|
1434 |
by (cases "pseudo_mod p q = 0") auto
|
|
1435 |
with "1.prems" False
|
|
1436 |
have "gcd_poly_code_aux q (primitive_part (pseudo_mod p q)) =
|
|
1437 |
gcd q (primitive_part (pseudo_mod p q))"
|
|
1438 |
by (intro 1) simp_all
|
|
1439 |
also from "1.prems" False
|
|
1440 |
have "\<dots> = gcd p q" by (intro gcd_poly_pseudo_mod [symmetric]) auto
|
|
1441 |
finally show ?thesis .
|
|
1442 |
qed
|
|
1443 |
qed
|
|
1444 |
|
|
1445 |
definition gcd_poly_code
|
|
1446 |
:: "'a :: factorial_ring_gcd poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
|
|
1447 |
where "gcd_poly_code p q =
|
|
1448 |
(if p = 0 then normalize q else if q = 0 then normalize p else
|
|
1449 |
smult (gcd (content p) (content q))
|
|
1450 |
(gcd_poly_code_aux (primitive_part p) (primitive_part q)))"
|
|
1451 |
|
|
1452 |
lemma lcm_poly_code [code]:
|
|
1453 |
fixes p q :: "'a :: factorial_ring_gcd poly"
|
|
1454 |
shows "lcm p q = normalize (p * q) div gcd p q"
|
|
1455 |
by (rule lcm_gcd)
|
|
1456 |
|
|
1457 |
lemma gcd_poly_code [code]: "gcd p q = gcd_poly_code p q"
|
|
1458 |
by (simp add: gcd_poly_code_def gcd_poly_code_aux_correct gcd_poly_decompose [symmetric])
|
|
1459 |
|
|
1460 |
declare Gcd_set
|
|
1461 |
[where ?'a = "'a :: factorial_ring_gcd poly", code]
|
|
1462 |
|
|
1463 |
declare Lcm_set
|
|
1464 |
[where ?'a = "'a :: factorial_ring_gcd poly", code]
|
|
1465 |
|
|
1466 |
value [code] "Lcm {[:1,2,3:], [:2,3,4::int poly:]}"
|
|
1467 |
|
|
1468 |
end
|