author | haftmann |
Thu, 06 Apr 2017 21:37:13 +0200 | |
changeset 65417 | fc41a5650fb1 |
parent 65390 | src/HOL/Library/Polynomial_Factorial.thy@83586780598b |
child 65435 | 378175f44328 |
permissions | -rw-r--r-- |
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: |
65390 | 171 |
"(\<Prod>x\<in>#A. map_poly to_fract (f x)) = fract_poly (prod_mset (image_mset f A))" |
172 |
by (induct A) (simp_all add: 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 |