457 fix p q s :: "'a poly" assume "s \<noteq> 0" |
457 fix p q s :: "'a poly" assume "s \<noteq> 0" |
458 moreover assume "(if p = 0 then (0::nat) else 2 ^ degree p) < (if q = 0 then 0 else 2 ^ degree q)" |
458 moreover assume "(if p = 0 then (0::nat) else 2 ^ degree p) < (if q = 0 then 0 else 2 ^ degree q)" |
459 ultimately show "(if p * s = 0 then (0::nat) else 2 ^ degree (p * s)) < (if q * s = 0 then 0 else 2 ^ degree (q * s))" |
459 ultimately show "(if p * s = 0 then (0::nat) else 2 ^ degree (p * s)) < (if q * s = 0 then 0 else 2 ^ degree (q * s))" |
460 by (auto simp add: degree_mult_eq) |
460 by (auto simp add: degree_mult_eq) |
461 next |
461 next |
462 fix p q r :: "'a poly" assume "p \<noteq> 0" |
462 fix p q r :: "'a poly" |
|
463 assume "p \<noteq> 0" |
|
464 with eucl_rel_poly [of r p] have "eucl_rel_poly (r + q * p) p (q + r div p, r mod p)" |
|
465 by (simp add: eucl_rel_poly_iff distrib_right) |
|
466 then have "(r + q * p) div p = q + r div p" |
|
467 by (rule div_poly_eq) |
463 moreover assume "(if r = 0 then (0::nat) else 2 ^ degree r) |
468 moreover assume "(if r = 0 then (0::nat) else 2 ^ degree r) |
464 < (if p = 0 then 0 else 2 ^ degree p)" |
469 < (if p = 0 then 0 else 2 ^ degree p)" |
465 ultimately show "(q * p + r) div p = q" |
470 ultimately show "(q * p + r) div p = q" |
466 by (cases "r = 0") (auto simp add: div_poly_less) |
471 using \<open>p \<noteq> 0\<close> |
|
472 by (cases "r = 0") (simp_all add: div_poly_less ac_simps) |
467 qed (auto simp: lead_coeff_mult Rings.div_mult_mod_eq intro!: degree_mod_less' degree_mult_right_le) |
473 qed (auto simp: lead_coeff_mult Rings.div_mult_mod_eq intro!: degree_mod_less' degree_mult_right_le) |
468 qed |
474 qed |
469 |
475 |
470 lemma field_poly_irreducible_imp_prime: |
476 lemma field_poly_irreducible_imp_prime: |
471 "prime_elem p" if "irreducible p" for p :: "'a :: field poly" |
477 "prime_elem p" if "irreducible p" for p :: "'a :: field poly" |
759 where "euclidean_size_poly p = (if p = 0 then 0 else 2 ^ degree p)" |
765 where "euclidean_size_poly p = (if p = 0 then 0 else 2 ^ degree p)" |
760 |
766 |
761 definition uniqueness_constraint_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> bool" |
767 definition uniqueness_constraint_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> bool" |
762 where [simp]: "uniqueness_constraint_poly = top" |
768 where [simp]: "uniqueness_constraint_poly = top" |
763 |
769 |
764 instance |
770 instance proof |
765 by standard |
771 show "(q * p + r) div p = q" if "p \<noteq> 0" |
766 (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 |
772 and "euclidean_size r < euclidean_size p" for q p r :: "'a poly" |
|
773 proof - |
|
774 from \<open>p \<noteq> 0\<close> eucl_rel_poly [of r p] have "eucl_rel_poly (r + q * p) p (q + r div p, r mod p)" |
|
775 by (simp add: eucl_rel_poly_iff distrib_right) |
|
776 then have "(r + q * p) div p = q + r div p" |
|
777 by (rule div_poly_eq) |
|
778 with that show ?thesis |
|
779 by (cases "r = 0") (simp_all add: euclidean_size_poly_def div_poly_less ac_simps) |
|
780 qed |
|
781 qed (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 |
767 split: if_splits) |
782 split: if_splits) |
768 |
783 |
769 end |
784 end |
770 |
785 |
771 instance poly :: ("{field,factorial_ring_gcd}") euclidean_ring_gcd |
786 instance poly :: ("{field,factorial_ring_gcd}") euclidean_ring_gcd |