158 |
158 |
159 lemma fract_poly_is_unit: "p dvd 1 \<Longrightarrow> fract_poly p dvd 1" |
159 lemma fract_poly_is_unit: "p dvd 1 \<Longrightarrow> fract_poly p dvd 1" |
160 using fract_poly_dvd[of p 1] by simp |
160 using fract_poly_dvd[of p 1] by simp |
161 |
161 |
162 lemma fract_poly_smult_eqE: |
162 lemma fract_poly_smult_eqE: |
163 fixes c :: "'a :: {idom_divide,ring_gcd} fract" |
163 fixes c :: "'a :: {idom_divide,ring_gcd,semiring_gcd_mult_normalize} fract" |
164 assumes "fract_poly p = smult c (fract_poly q)" |
164 assumes "fract_poly p = smult c (fract_poly q)" |
165 obtains a b |
165 obtains a b |
166 where "c = to_fract b / to_fract a" "smult a p = smult b q" "coprime a b" "normalize a = a" |
166 where "c = to_fract b / to_fract a" "smult a p = smult b q" "coprime a b" "normalize a = a" |
167 proof - |
167 proof - |
168 define a b where "a = fst (quot_of_fract c)" and "b = snd (quot_of_fract c)" |
168 define a b where "a = fst (quot_of_fract c)" and "b = snd (quot_of_fract c)" |
178 |
178 |
179 |
179 |
180 subsection \<open>Fractional content\<close> |
180 subsection \<open>Fractional content\<close> |
181 |
181 |
182 abbreviation (input) Lcm_coeff_denoms |
182 abbreviation (input) Lcm_coeff_denoms |
183 :: "'a :: {semiring_Gcd,idom_divide,ring_gcd} fract poly \<Rightarrow> 'a" |
183 :: "'a :: {semiring_Gcd,idom_divide,ring_gcd,semiring_gcd_mult_normalize} fract poly \<Rightarrow> 'a" |
184 where "Lcm_coeff_denoms p \<equiv> Lcm (snd ` quot_of_fract ` set (coeffs p))" |
184 where "Lcm_coeff_denoms p \<equiv> Lcm (snd ` quot_of_fract ` set (coeffs p))" |
185 |
185 |
186 definition fract_content :: |
186 definition fract_content :: |
187 "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} fract poly \<Rightarrow> 'a fract" where |
187 "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide,semiring_gcd_mult_normalize} fract poly \<Rightarrow> 'a fract" where |
188 "fract_content p = |
188 "fract_content p = |
189 (let d = Lcm_coeff_denoms p in Fract (content (unfract_poly (smult (to_fract d) p))) d)" |
189 (let d = Lcm_coeff_denoms p in Fract (content (unfract_poly (smult (to_fract d) p))) d)" |
190 |
190 |
191 definition primitive_part_fract :: |
191 definition primitive_part_fract :: |
192 "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} fract poly \<Rightarrow> 'a poly" where |
192 "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide,semiring_gcd_mult_normalize} fract poly \<Rightarrow> 'a poly" where |
193 "primitive_part_fract p = |
193 "primitive_part_fract p = |
194 primitive_part (unfract_poly (smult (to_fract (Lcm_coeff_denoms p)) p))" |
194 primitive_part (unfract_poly (smult (to_fract (Lcm_coeff_denoms p)) p))" |
195 |
195 |
196 lemma primitive_part_fract_0 [simp]: "primitive_part_fract 0 = 0" |
196 lemma primitive_part_fract_0 [simp]: "primitive_part_fract 0 = 0" |
197 by (simp add: primitive_part_fract_def) |
197 by (simp add: primitive_part_fract_def) |
199 lemma fract_content_eq_0_iff [simp]: |
199 lemma fract_content_eq_0_iff [simp]: |
200 "fract_content p = 0 \<longleftrightarrow> p = 0" |
200 "fract_content p = 0 \<longleftrightarrow> p = 0" |
201 unfolding fract_content_def Let_def Zero_fract_def |
201 unfolding fract_content_def Let_def Zero_fract_def |
202 by (subst eq_fract) (auto simp: Lcm_0_iff map_poly_eq_0_iff) |
202 by (subst eq_fract) (auto simp: Lcm_0_iff map_poly_eq_0_iff) |
203 |
203 |
204 lemma content_primitive_part_fract [simp]: "p \<noteq> 0 \<Longrightarrow> content (primitive_part_fract p) = 1" |
204 lemma content_primitive_part_fract [simp]: |
|
205 fixes p :: "'a :: {semiring_gcd_mult_normalize, |
|
206 factorial_semiring, ring_gcd, semiring_Gcd,idom_divide} fract poly" |
|
207 shows "p \<noteq> 0 \<Longrightarrow> content (primitive_part_fract p) = 1" |
205 unfolding primitive_part_fract_def |
208 unfolding primitive_part_fract_def |
206 by (rule content_primitive_part) |
209 by (rule content_primitive_part) |
207 (auto simp: primitive_part_fract_def map_poly_eq_0_iff Lcm_0_iff) |
210 (auto simp: primitive_part_fract_def map_poly_eq_0_iff Lcm_0_iff) |
208 |
211 |
209 lemma content_times_primitive_part_fract: |
212 lemma content_times_primitive_part_fract: |
254 by (intro map_poly_idI) simp_all |
257 by (intro map_poly_idI) simp_all |
255 finally show ?thesis . |
258 finally show ?thesis . |
256 qed |
259 qed |
257 |
260 |
258 lemma content_decompose_fract: |
261 lemma content_decompose_fract: |
259 fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} fract poly" |
262 fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide, |
|
263 semiring_gcd_mult_normalize} fract poly" |
260 obtains c p' where "p = smult c (map_poly to_fract p')" "content p' = 1" |
264 obtains c p' where "p = smult c (map_poly to_fract p')" "content p' = 1" |
261 proof (cases "p = 0") |
265 proof (cases "p = 0") |
262 case True |
266 case True |
263 hence "p = smult 0 (map_poly to_fract 1)" "content 1 = 1" by simp_all |
267 hence "p = smult 0 (map_poly to_fract 1)" "content 1 = 1" by simp_all |
264 thus ?thesis .. |
268 thus ?thesis .. |
345 thus "c dvd a \<or> c dvd b" by simp |
349 thus "c dvd a \<or> c dvd b" by simp |
346 qed (insert A, auto simp: prime_elem_def is_unit_poly_iff) |
350 qed (insert A, auto simp: prime_elem_def is_unit_poly_iff) |
347 qed (auto intro: lift_prime_elem_poly) |
351 qed (auto intro: lift_prime_elem_poly) |
348 |
352 |
349 lemma fract_poly_dvdD: |
353 lemma fract_poly_dvdD: |
350 fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} poly" |
354 fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide, |
|
355 semiring_gcd_mult_normalize} poly" |
351 assumes "fract_poly p dvd fract_poly q" "content p = 1" |
356 assumes "fract_poly p dvd fract_poly q" "content p = 1" |
352 shows "p dvd q" |
357 shows "p dvd q" |
353 proof - |
358 proof - |
354 from assms(1) obtain r where r: "fract_poly q = fract_poly p * r" by (erule dvdE) |
359 from assms(1) obtain r where r: "fract_poly q = fract_poly p * r" by (erule dvdE) |
355 from content_decompose_fract[of r] guess c r' . note r' = this |
360 from content_decompose_fract[of r] guess c r' . note r' = this |
370 |
375 |
371 context |
376 context |
372 begin |
377 begin |
373 |
378 |
374 interpretation field_poly: |
379 interpretation field_poly: |
375 normalization_euclidean_semiring where zero = "0 :: 'a :: field poly" |
380 normalization_euclidean_semiring_multiplicative where zero = "0 :: 'a :: field poly" |
376 and one = 1 and plus = plus and minus = minus |
381 and one = 1 and plus = plus and minus = minus |
377 and times = times |
382 and times = times |
378 and normalize = "\<lambda>p. smult (inverse (lead_coeff p)) p" |
383 and normalize = "\<lambda>p. smult (inverse (lead_coeff p)) p" |
379 and unit_factor = "\<lambda>p. [:lead_coeff p:]" |
384 and unit_factor = "\<lambda>p. [:lead_coeff p:]" |
380 and euclidean_size = "\<lambda>p. if p = 0 then 0 else 2 ^ degree p" |
385 and euclidean_size = "\<lambda>p. if p = 0 then 0 else 2 ^ degree p" |
390 by (simp add: prod_mset_dict) |
395 by (simp add: prod_mset_dict) |
391 show "comm_semiring_1.irreducible times 1 0 = irreducible" |
396 show "comm_semiring_1.irreducible times 1 0 = irreducible" |
392 by (simp add: irreducible_dict) |
397 by (simp add: irreducible_dict) |
393 show "comm_semiring_1.prime_elem times 1 0 = prime_elem" |
398 show "comm_semiring_1.prime_elem times 1 0 = prime_elem" |
394 by (simp add: prime_elem_dict) |
399 by (simp add: prime_elem_dict) |
395 show "class.normalization_euclidean_semiring divide plus minus (0 :: 'a poly) times 1 |
400 show "class.normalization_euclidean_semiring_multiplicative divide plus minus (0 :: 'a poly) times 1 |
396 modulo (\<lambda>p. if p = 0 then 0 else 2 ^ degree p) |
401 modulo (\<lambda>p. if p = 0 then 0 else 2 ^ degree p) |
397 (\<lambda>p. [:lead_coeff p:]) (\<lambda>p. smult (inverse (lead_coeff p)) p)" |
402 (\<lambda>p. [:lead_coeff p:]) (\<lambda>p. smult (inverse (lead_coeff p)) p)" |
398 proof (standard, fold dvd_dict) |
403 proof (standard, fold dvd_dict) |
399 fix p :: "'a poly" |
404 fix p :: "'a poly" |
400 show "[:lead_coeff p:] * smult (inverse (lead_coeff p)) p = p" |
405 show "[:lead_coeff p:] * smult (inverse (lead_coeff p)) p = p" |
405 by (elim is_unit_polyE) (auto simp: monom_0 one_poly_def field_simps) |
410 by (elim is_unit_polyE) (auto simp: monom_0 one_poly_def field_simps) |
406 next |
411 next |
407 fix p :: "'a poly" assume "p \<noteq> 0" |
412 fix p :: "'a poly" assume "p \<noteq> 0" |
408 then show "is_unit [:lead_coeff p:]" |
413 then show "is_unit [:lead_coeff p:]" |
409 by (simp add: is_unit_pCons_iff) |
414 by (simp add: is_unit_pCons_iff) |
|
415 next |
|
416 fix a b :: "'a poly" assume "is_unit a" |
|
417 thus "[:lead_coeff (a * b):] = a * [:lead_coeff b:]" |
|
418 by (auto elim!: is_unit_polyE) |
410 qed (auto simp: lead_coeff_mult Rings.div_mult_mod_eq intro!: degree_mod_less' degree_mult_right_le) |
419 qed (auto simp: lead_coeff_mult Rings.div_mult_mod_eq intro!: degree_mod_less' degree_mult_right_le) |
411 qed |
420 qed |
412 |
421 |
413 lemma field_poly_irreducible_imp_prime: |
422 lemma field_poly_irreducible_imp_prime: |
414 "prime_elem p" if "irreducible p" for p :: "'a :: field poly" |
423 "prime_elem p" if "irreducible p" for p :: "'a :: field poly" |
415 using that by (fact field_poly.irreducible_imp_prime_elem) |
424 using that by (fact field_poly.irreducible_imp_prime_elem) |
416 |
425 find_theorems name:prod_mset_prime_factorization |
417 lemma field_poly_prod_mset_prime_factorization: |
426 lemma field_poly_prod_mset_prime_factorization: |
418 "prod_mset (field_poly.prime_factorization p) = smult (inverse (lead_coeff p)) p" |
427 "prod_mset (field_poly.prime_factorization p) = smult (inverse (lead_coeff p)) p" |
419 if "p \<noteq> 0" for p :: "'a :: field poly" |
428 if "p \<noteq> 0" for p :: "'a :: field poly" |
420 using that by (fact field_poly.prod_mset_prime_factorization) |
429 using that by (fact field_poly.prod_mset_prime_factorization) |
421 |
430 |
427 |
436 |
428 |
437 |
429 subsection \<open>Primality and irreducibility in polynomial rings\<close> |
438 subsection \<open>Primality and irreducibility in polynomial rings\<close> |
430 |
439 |
431 lemma nonconst_poly_irreducible_iff: |
440 lemma nonconst_poly_irreducible_iff: |
432 fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} poly" |
441 fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide,semiring_gcd_mult_normalize} poly" |
433 assumes "degree p \<noteq> 0" |
442 assumes "degree p \<noteq> 0" |
434 shows "irreducible p \<longleftrightarrow> irreducible (fract_poly p) \<and> content p = 1" |
443 shows "irreducible p \<longleftrightarrow> irreducible (fract_poly p) \<and> content p = 1" |
435 proof safe |
444 proof safe |
436 assume p: "irreducible p" |
445 assume p: "irreducible p" |
437 |
446 |
505 by (auto simp: content_prod_eq_1_iff is_unit_fract_poly_iff) |
514 by (auto simp: content_prod_eq_1_iff is_unit_fract_poly_iff) |
506 qed |
515 qed |
507 qed |
516 qed |
508 |
517 |
509 private lemma irreducible_imp_prime_poly: |
518 private lemma irreducible_imp_prime_poly: |
510 fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} poly" |
519 fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide,semiring_gcd_mult_normalize} poly" |
511 assumes "irreducible p" |
520 assumes "irreducible p" |
512 shows "prime_elem p" |
521 shows "prime_elem p" |
513 proof (cases "degree p = 0") |
522 proof (cases "degree p = 0") |
514 case True |
523 case True |
515 with assms show ?thesis |
524 with assms show ?thesis |
540 by (auto simp: degree_map_poly) |
549 by (auto simp: degree_map_poly) |
541 finally show ?thesis .. |
550 finally show ?thesis .. |
542 qed |
551 qed |
543 |
552 |
544 lemma irreducible_primitive_part_fract: |
553 lemma irreducible_primitive_part_fract: |
545 fixes p :: "'a :: {idom_divide, ring_gcd, factorial_semiring, semiring_Gcd} fract poly" |
554 fixes p :: "'a :: {idom_divide, ring_gcd, factorial_semiring, semiring_Gcd,semiring_gcd_mult_normalize} fract poly" |
546 assumes "irreducible p" |
555 assumes "irreducible p" |
547 shows "irreducible (primitive_part_fract p)" |
556 shows "irreducible (primitive_part_fract p)" |
548 proof - |
557 proof - |
549 from assms have deg: "degree (primitive_part_fract p) \<noteq> 0" |
558 from assms have deg: "degree (primitive_part_fract p) \<noteq> 0" |
550 by (intro notI) |
559 by (intro notI) |
559 finally show ?thesis using deg |
568 finally show ?thesis using deg |
560 by (simp add: nonconst_poly_irreducible_iff) |
569 by (simp add: nonconst_poly_irreducible_iff) |
561 qed |
570 qed |
562 |
571 |
563 lemma prime_elem_primitive_part_fract: |
572 lemma prime_elem_primitive_part_fract: |
564 fixes p :: "'a :: {idom_divide, ring_gcd, factorial_semiring, semiring_Gcd} fract poly" |
573 fixes p :: "'a :: {idom_divide, ring_gcd, factorial_semiring, semiring_Gcd,semiring_gcd_mult_normalize} fract poly" |
565 shows "irreducible p \<Longrightarrow> prime_elem (primitive_part_fract p)" |
574 shows "irreducible p \<Longrightarrow> prime_elem (primitive_part_fract p)" |
566 by (intro irreducible_imp_prime_poly irreducible_primitive_part_fract) |
575 by (intro irreducible_imp_prime_poly irreducible_primitive_part_fract) |
567 |
576 |
568 lemma irreducible_linear_field_poly: |
577 lemma irreducible_linear_field_poly: |
569 fixes a b :: "'a::field" |
578 fixes a b :: "'a::field" |
581 lemma prime_elem_linear_field_poly: |
590 lemma prime_elem_linear_field_poly: |
582 "(b :: 'a :: field) \<noteq> 0 \<Longrightarrow> prime_elem [:a,b:]" |
591 "(b :: 'a :: field) \<noteq> 0 \<Longrightarrow> prime_elem [:a,b:]" |
583 by (rule field_poly_irreducible_imp_prime, rule irreducible_linear_field_poly) |
592 by (rule field_poly_irreducible_imp_prime, rule irreducible_linear_field_poly) |
584 |
593 |
585 lemma irreducible_linear_poly: |
594 lemma irreducible_linear_poly: |
586 fixes a b :: "'a::{idom_divide,ring_gcd,factorial_semiring,semiring_Gcd}" |
595 fixes a b :: "'a::{idom_divide,ring_gcd,factorial_semiring,semiring_Gcd,semiring_gcd_mult_normalize}" |
587 shows "b \<noteq> 0 \<Longrightarrow> coprime a b \<Longrightarrow> irreducible [:a,b:]" |
596 shows "b \<noteq> 0 \<Longrightarrow> coprime a b \<Longrightarrow> irreducible [:a,b:]" |
588 by (auto intro!: irreducible_linear_field_poly |
597 by (auto intro!: irreducible_linear_field_poly |
589 simp: nonconst_poly_irreducible_iff content_def map_poly_pCons) |
598 simp: nonconst_poly_irreducible_iff content_def map_poly_pCons) |
590 |
599 |
591 lemma prime_elem_linear_poly: |
600 lemma prime_elem_linear_poly: |
592 fixes a b :: "'a::{idom_divide,ring_gcd,factorial_semiring,semiring_Gcd}" |
601 fixes a b :: "'a::{idom_divide,ring_gcd,factorial_semiring,semiring_Gcd,semiring_gcd_mult_normalize}" |
593 shows "b \<noteq> 0 \<Longrightarrow> coprime a b \<Longrightarrow> prime_elem [:a,b:]" |
602 shows "b \<noteq> 0 \<Longrightarrow> coprime a b \<Longrightarrow> prime_elem [:a,b:]" |
594 by (rule irreducible_imp_prime_poly, rule irreducible_linear_poly) |
603 by (rule irreducible_imp_prime_poly, rule irreducible_linear_poly) |
595 |
604 |
596 |
605 |
597 subsection \<open>Prime factorisation of polynomials\<close> |
606 subsection \<open>Prime factorisation of polynomials\<close> |
598 |
607 |
599 private lemma poly_prime_factorization_exists_content_1: |
608 private lemma poly_prime_factorization_exists_content_1: |
600 fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} poly" |
609 fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide,semiring_gcd_mult_normalize} poly" |
601 assumes "p \<noteq> 0" "content p = 1" |
610 assumes "p \<noteq> 0" "content p = 1" |
602 shows "\<exists>A. (\<forall>p. p \<in># A \<longrightarrow> prime_elem p) \<and> prod_mset A = normalize p" |
611 shows "\<exists>A. (\<forall>p. p \<in># A \<longrightarrow> prime_elem p) \<and> prod_mset A = normalize p" |
603 proof - |
612 proof - |
604 let ?P = "field_poly.prime_factorization (fract_poly p)" |
613 let ?P = "field_poly.prime_factorization (fract_poly p)" |
605 define c where "c = prod_mset (image_mset fract_content ?P)" |
614 define c where "c = prod_mset (image_mset fract_content ?P)" |
655 from this and \<open>prod_mset A = normalize p\<close> show ?thesis |
664 from this and \<open>prod_mset A = normalize p\<close> show ?thesis |
656 by (intro exI[of _ A]) blast |
665 by (intro exI[of _ A]) blast |
657 qed |
666 qed |
658 |
667 |
659 lemma poly_prime_factorization_exists: |
668 lemma poly_prime_factorization_exists: |
660 fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} poly" |
669 fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide,semiring_gcd_mult_normalize} poly" |
661 assumes "p \<noteq> 0" |
670 assumes "p \<noteq> 0" |
662 shows "\<exists>A. (\<forall>p. p \<in># A \<longrightarrow> prime_elem p) \<and> prod_mset A = normalize p" |
671 shows "\<exists>A. (\<forall>p. p \<in># A \<longrightarrow> prime_elem p) \<and> normalize (prod_mset A) = normalize p" |
663 proof - |
672 proof - |
664 define B where "B = image_mset (\<lambda>x. [:x:]) (prime_factorization (content p))" |
673 define B where "B = image_mset (\<lambda>x. [:x:]) (prime_factorization (content p))" |
665 have "\<exists>A. (\<forall>p. p \<in># A \<longrightarrow> prime_elem p) \<and> prod_mset A = normalize (primitive_part p)" |
674 have "\<exists>A. (\<forall>p. p \<in># A \<longrightarrow> prime_elem p) \<and> prod_mset A = normalize (primitive_part p)" |
666 by (rule poly_prime_factorization_exists_content_1) (insert assms, simp_all) |
675 by (rule poly_prime_factorization_exists_content_1) (insert assms, simp_all) |
667 then guess A by (elim exE conjE) note A = this |
676 then guess A by (elim exE conjE) note A = this |
668 moreover from assms have "prod_mset B = [:content p:]" |
677 have "normalize (prod_mset (A + B)) = normalize (prod_mset A * normalize (prod_mset B))" |
669 by (simp add: B_def prod_mset_const_poly prod_mset_prime_factorization) |
678 by simp |
|
679 also from assms have "normalize (prod_mset B) = normalize [:content p:]" |
|
680 by (simp add: prod_mset_const_poly normalize_const_poly prod_mset_prime_factorization_weak B_def) |
|
681 also have "prod_mset A = normalize (primitive_part p)" |
|
682 using A by simp |
|
683 finally have "normalize (prod_mset (A + B)) = normalize (primitive_part p * [:content p:])" |
|
684 by simp |
670 moreover have "\<forall>p. p \<in># B \<longrightarrow> prime_elem p" |
685 moreover have "\<forall>p. p \<in># B \<longrightarrow> prime_elem p" |
671 by (auto simp: B_def intro!: lift_prime_elem_poly dest: in_prime_factors_imp_prime) |
686 by (auto simp: B_def intro!: lift_prime_elem_poly dest: in_prime_factors_imp_prime) |
672 ultimately show ?thesis by (intro exI[of _ "B + A"]) auto |
687 ultimately show ?thesis using A by (intro exI[of _ "A + B"]) (auto) |
673 qed |
688 qed |
674 |
689 |
675 end |
690 end |
676 |
691 |
677 |
692 |
678 subsection \<open>Typeclass instances\<close> |
693 subsection \<open>Typeclass instances\<close> |
679 |
694 |
680 instance poly :: (factorial_ring_gcd) factorial_semiring |
695 instance poly :: ("{factorial_ring_gcd,semiring_gcd_mult_normalize}") factorial_semiring |
681 by standard (rule poly_prime_factorization_exists) |
696 by standard (rule poly_prime_factorization_exists) |
682 |
697 |
683 instantiation poly :: (factorial_ring_gcd) factorial_ring_gcd |
698 instantiation poly :: ("{factorial_ring_gcd, semiring_gcd_mult_normalize}") factorial_ring_gcd |
684 begin |
699 begin |
685 |
700 |
686 definition gcd_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly" where |
701 definition gcd_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly" where |
687 [code del]: "gcd_poly = gcd_factorial" |
702 [code del]: "gcd_poly = gcd_factorial" |
688 |
703 |
697 |
712 |
698 instance by standard (simp_all add: gcd_poly_def lcm_poly_def Gcd_poly_def Lcm_poly_def) |
713 instance by standard (simp_all add: gcd_poly_def lcm_poly_def Gcd_poly_def Lcm_poly_def) |
699 |
714 |
700 end |
715 end |
701 |
716 |
702 instantiation poly :: ("{field,factorial_ring_gcd}") "{unique_euclidean_ring, normalization_euclidean_semiring}" |
717 instance poly :: ("{factorial_ring_gcd, semiring_gcd_mult_normalize}") semiring_gcd_mult_normalize .. |
|
718 |
|
719 instantiation poly :: ("{field,factorial_ring_gcd,semiring_gcd_mult_normalize}") |
|
720 "{unique_euclidean_ring, normalization_euclidean_semiring}" |
703 begin |
721 begin |
704 |
722 |
705 definition euclidean_size_poly :: "'a poly \<Rightarrow> nat" |
723 definition euclidean_size_poly :: "'a poly \<Rightarrow> nat" |
706 where "euclidean_size_poly p = (if p = 0 then 0 else 2 ^ degree p)" |
724 where "euclidean_size_poly p = (if p = 0 then 0 else 2 ^ degree p)" |
707 |
725 |
722 qed (auto simp: euclidean_size_poly_def Rings.div_mult_mod_eq div_poly_less degree_mult_eq power_add |
740 qed (auto simp: euclidean_size_poly_def Rings.div_mult_mod_eq div_poly_less degree_mult_eq power_add |
723 intro!: degree_mod_less' split: if_splits) |
741 intro!: degree_mod_less' split: if_splits) |
724 |
742 |
725 end |
743 end |
726 |
744 |
727 instance poly :: ("{field, normalization_euclidean_semiring, factorial_ring_gcd}") euclidean_ring_gcd |
745 instance poly :: ("{field, normalization_euclidean_semiring, factorial_ring_gcd, |
|
746 semiring_gcd_mult_normalize}") euclidean_ring_gcd |
728 by (rule euclidean_ring_gcd_class.intro, rule factorial_euclidean_semiring_gcdI) standard |
747 by (rule euclidean_ring_gcd_class.intro, rule factorial_euclidean_semiring_gcdI) standard |
729 |
748 |
730 |
749 |
731 subsection \<open>Polynomial GCD\<close> |
750 subsection \<open>Polynomial GCD\<close> |
732 |
751 |
733 lemma gcd_poly_decompose: |
752 lemma gcd_poly_decompose: |
734 fixes p q :: "'a :: factorial_ring_gcd poly" |
753 fixes p q :: "'a :: {factorial_ring_gcd,semiring_gcd_mult_normalize} poly" |
735 shows "gcd p q = |
754 shows "gcd p q = |
736 smult (gcd (content p) (content q)) (gcd (primitive_part p) (primitive_part q))" |
755 smult (gcd (content p) (content q)) (gcd (primitive_part p) (primitive_part q))" |
737 proof (rule sym, rule gcdI) |
756 proof (rule sym, rule gcdI) |
738 have "[:gcd (content p) (content q):] * gcd (primitive_part p) (primitive_part q) dvd |
757 have "[:gcd (content p) (content q):] * gcd (primitive_part p) (primitive_part q) dvd |
739 [:content p:] * primitive_part p" by (intro mult_dvd_mono) simp_all |
758 [:content p:] * primitive_part p" by (intro mult_dvd_mono) simp_all |
753 by simp |
772 by simp |
754 qed (auto simp: normalize_smult) |
773 qed (auto simp: normalize_smult) |
755 |
774 |
756 |
775 |
757 lemma gcd_poly_pseudo_mod: |
776 lemma gcd_poly_pseudo_mod: |
758 fixes p q :: "'a :: factorial_ring_gcd poly" |
777 fixes p q :: "'a :: {factorial_ring_gcd,semiring_gcd_mult_normalize} poly" |
759 assumes nz: "q \<noteq> 0" and prim: "content p = 1" "content q = 1" |
778 assumes nz: "q \<noteq> 0" and prim: "content p = 1" "content q = 1" |
760 shows "gcd p q = gcd q (primitive_part (pseudo_mod p q))" |
779 shows "gcd p q = gcd q (primitive_part (pseudo_mod p q))" |
761 proof - |
780 proof - |
762 define r s where "r = fst (pseudo_divmod p q)" and "s = snd (pseudo_divmod p q)" |
781 define r s where "r = fst (pseudo_divmod p q)" and "s = snd (pseudo_divmod p q)" |
763 define a where "a = [:coeff q (degree q) ^ (Suc (degree p) - degree q):]" |
782 define a where "a = [:coeff q (degree q) ^ (Suc (degree p) - degree q):]" |
832 |
851 |
833 lemma gcd_poly_code [code]: "gcd p q = gcd_poly_code p q" |
852 lemma gcd_poly_code [code]: "gcd p q = gcd_poly_code p q" |
834 by (simp add: gcd_poly_code_def gcd_poly_code_aux_correct gcd_poly_decompose [symmetric]) |
853 by (simp add: gcd_poly_code_def gcd_poly_code_aux_correct gcd_poly_decompose [symmetric]) |
835 |
854 |
836 lemma lcm_poly_code [code]: |
855 lemma lcm_poly_code [code]: |
837 fixes p q :: "'a :: factorial_ring_gcd poly" |
856 fixes p q :: "'a :: {factorial_ring_gcd,semiring_gcd_mult_normalize} poly" |
838 shows "lcm p q = normalize (p * q) div gcd p q" |
857 shows "lcm p q = normalize (p * q div gcd p q)" |
839 by (fact lcm_gcd) |
858 by (fact lcm_gcd) |
840 |
859 |
841 lemmas Gcd_poly_set_eq_fold [code] = Gcd_set_eq_fold [where ?'a = "'a :: factorial_ring_gcd poly"] |
860 lemmas Gcd_poly_set_eq_fold [code] = |
842 lemmas Lcm_poly_set_eq_fold [code] = Lcm_set_eq_fold [where ?'a = "'a :: factorial_ring_gcd poly"] |
861 Gcd_set_eq_fold [where ?'a = "'a :: {factorial_ring_gcd,semiring_gcd_mult_normalize} poly"] |
|
862 lemmas Lcm_poly_set_eq_fold [code] = |
|
863 Lcm_set_eq_fold [where ?'a = "'a :: {factorial_ring_gcd,semiring_gcd_mult_normalize} poly"] |
843 |
864 |
844 text \<open>Example: |
865 text \<open>Example: |
845 @{lemma "Lcm {[:1, 2, 3:], [:2, 3, 4:]} = [:[:2:], [:7:], [:16:], [:17:], [:12 :: int:]:]" by eval} |
866 @{lemma "Lcm {[:1, 2, 3:], [:2, 3, 4:]} = [:[:2:], [:7:], [:16:], [:17:], [:12 :: int:]:]" by eval} |
846 \<close> |
867 \<close> |
847 |
868 |