230 mult_unit_dvd_iff dvd_mult_unit_iff) |
230 mult_unit_dvd_iff dvd_mult_unit_iff) |
231 |
231 |
232 lemma is_prime_elem_mult_unit_left: |
232 lemma is_prime_elem_mult_unit_left: |
233 "is_unit a \<Longrightarrow> is_prime_elem (a * p) \<longleftrightarrow> is_prime_elem p" |
233 "is_unit a \<Longrightarrow> is_prime_elem (a * p) \<longleftrightarrow> is_prime_elem p" |
234 by (auto simp: is_prime_elem_def mult.commute[of a] is_unit_mult_iff mult_unit_dvd_iff) |
234 by (auto simp: is_prime_elem_def mult.commute[of a] is_unit_mult_iff mult_unit_dvd_iff) |
|
235 |
|
236 lemma prime_dvd_cases: |
|
237 assumes pk: "p*k dvd m*n" and p: "is_prime_elem p" |
|
238 shows "(\<exists>x. k dvd x*n \<and> m = p*x) \<or> (\<exists>y. k dvd m*y \<and> n = p*y)" |
|
239 proof - |
|
240 have "p dvd m*n" using dvd_mult_left pk by blast |
|
241 then consider "p dvd m" | "p dvd n" |
|
242 using p prime_dvd_mult_iff by blast |
|
243 then show ?thesis |
|
244 proof cases |
|
245 case 1 then obtain a where "m = p * a" by (metis dvd_mult_div_cancel) |
|
246 then have "\<exists>x. k dvd x * n \<and> m = p * x" |
|
247 using p pk by (auto simp: mult.assoc) |
|
248 then show ?thesis .. |
|
249 next |
|
250 case 2 then obtain b where "n = p * b" by (metis dvd_mult_div_cancel) |
|
251 with p pk have "\<exists>y. k dvd m*y \<and> n = p*y" |
|
252 by (metis dvd_mult_right dvd_times_left_cancel_iff mult.left_commute mult_zero_left) |
|
253 then show ?thesis .. |
|
254 qed |
|
255 qed |
|
256 |
|
257 lemma prime_power_dvd_prod: |
|
258 assumes pc: "p^c dvd m*n" and p: "is_prime_elem p" |
|
259 shows "\<exists>a b. a+b = c \<and> p^a dvd m \<and> p^b dvd n" |
|
260 using pc |
|
261 proof (induct c arbitrary: m n) |
|
262 case 0 show ?case by simp |
|
263 next |
|
264 case (Suc c) |
|
265 consider x where "p^c dvd x*n" "m = p*x" | y where "p^c dvd m*y" "n = p*y" |
|
266 using prime_dvd_cases [of _ "p^c", OF _ p] Suc.prems by force |
|
267 then show ?case |
|
268 proof cases |
|
269 case (1 x) |
|
270 with Suc.hyps[of x n] obtain a b where "a + b = c \<and> p ^ a dvd x \<and> p ^ b dvd n" by blast |
|
271 with 1 have "Suc a + b = Suc c \<and> p ^ Suc a dvd m \<and> p ^ b dvd n" |
|
272 by (auto intro: mult_dvd_mono) |
|
273 thus ?thesis by blast |
|
274 next |
|
275 case (2 y) |
|
276 with Suc.hyps[of m y] obtain a b where "a + b = c \<and> p ^ a dvd m \<and> p ^ b dvd y" by blast |
|
277 with 2 have "a + Suc b = Suc c \<and> p ^ a dvd m \<and> p ^ Suc b dvd n" |
|
278 by (auto intro: mult_dvd_mono) |
|
279 with Suc.hyps [of m y] show "\<exists>a b. a + b = Suc c \<and> p ^ a dvd m \<and> p ^ b dvd n" |
|
280 by force |
|
281 qed |
|
282 qed |
|
283 |
|
284 lemma add_eq_Suc_lem: "a+b = Suc (x+y) \<Longrightarrow> a \<le> x \<or> b \<le> y" |
|
285 by arith |
|
286 |
|
287 lemma prime_power_dvd_cases: |
|
288 "\<lbrakk>p^c dvd m * n; a + b = Suc c; is_prime_elem p\<rbrakk> \<Longrightarrow> p ^ a dvd m \<or> p ^ b dvd n" |
|
289 using power_le_dvd prime_power_dvd_prod by (blast dest: prime_power_dvd_prod add_eq_Suc_lem) |
235 |
290 |
236 end |
291 end |
237 |
292 |
238 context normalization_semidom |
293 context normalization_semidom |
239 begin |
294 begin |
1382 also from assms have "prime_factorization (\<Prod>i \<in># N. i) = N" |
1437 also from assms have "prime_factorization (\<Prod>i \<in># N. i) = N" |
1383 by (subst prime_factorization_msetprod_primes) simp_all |
1438 by (subst prime_factorization_msetprod_primes) simp_all |
1384 finally show ?thesis . |
1439 finally show ?thesis . |
1385 qed |
1440 qed |
1386 |
1441 |
|
1442 lemma multiplicity_cong: |
|
1443 "(\<And>r. p ^ r dvd a \<longleftrightarrow> p ^ r dvd b) \<Longrightarrow> multiplicity p a = multiplicity p b" |
|
1444 by (simp add: multiplicity_def) |
|
1445 |
|
1446 lemma not_dvd_imp_multiplicity_0: |
|
1447 assumes "\<not>p dvd x" |
|
1448 shows "multiplicity p x = 0" |
|
1449 proof - |
|
1450 from assms have "multiplicity p x < 1" |
|
1451 by (intro multiplicity_lessI) auto |
|
1452 thus ?thesis by simp |
|
1453 qed |
|
1454 |
1387 |
1455 |
1388 definition "gcd_factorial a b = (if a = 0 then normalize b |
1456 definition "gcd_factorial a b = (if a = 0 then normalize b |
1389 else if b = 0 then normalize a |
1457 else if b = 0 then normalize a |
1390 else msetprod (prime_factorization a #\<inter> prime_factorization b))" |
1458 else msetprod (prime_factorization a #\<inter> prime_factorization b))" |
1391 |
1459 |