src/HOL/Library/Polynomial_Factorial.thy
 changeset 64164 38c407446400 parent 63954 fb03766658f4 child 64240 eabf80376aab
```     1.1 --- a/src/HOL/Library/Polynomial_Factorial.thy	Tue Oct 11 16:44:13 2016 +0200
1.2 +++ b/src/HOL/Library/Polynomial_Factorial.thy	Wed Oct 12 20:38:47 2016 +0200
1.3 @@ -1018,8 +1018,12 @@
1.4      by (intro ext) (simp_all add: dvd.dvd_def dvd_def)
1.5
1.6  interpretation field_poly:
1.7 -  euclidean_ring "op div" "op *" "op mod" "op +" "op -" 0 "1 :: 'a :: field poly"
1.8 -    normalize_field_poly unit_factor_field_poly euclidean_size_field_poly uminus
1.9 +  euclidean_ring where zero = "0 :: 'a :: field poly"
1.10 +    and one = 1 and plus = plus and uminus = uminus and minus = minus
1.11 +    and times = times
1.12 +    and normalize = normalize_field_poly and unit_factor = unit_factor_field_poly
1.13 +    and euclidean_size = euclidean_size_field_poly
1.14 +    and divide = divide and modulo = modulo
1.15  proof (standard, unfold dvd_field_poly)
1.16    fix p :: "'a poly"
1.17    show "unit_factor_field_poly p * normalize_field_poly p = p"
1.18 @@ -1034,7 +1038,7 @@
1.19    thus "is_unit (unit_factor_field_poly p)"
1.21  qed (auto simp: unit_factor_field_poly_def normalize_field_poly_def lead_coeff_mult
1.22 -       euclidean_size_field_poly_def intro!: degree_mod_less' degree_mult_right_le)
1.23 +       euclidean_size_field_poly_def Rings.mod_div_equality intro!: degree_mod_less' degree_mult_right_le)
1.24
1.25  lemma field_poly_irreducible_imp_prime:
1.26    assumes "irreducible (p :: 'a :: field poly)"
1.27 @@ -1352,7 +1356,7 @@
1.28    "euclidean_size_poly p = (if p = 0 then 0 else 2 ^ degree p)"
1.29
1.30  instance
1.31 -  by standard (auto simp: euclidean_size_poly_def intro!: degree_mod_less' degree_mult_right_le)
1.32 +  by standard (auto simp: euclidean_size_poly_def Rings.mod_div_equality intro!: degree_mod_less' degree_mult_right_le)
1.33  end
1.34
1.35
1.36 @@ -1423,7 +1427,7 @@
1.37  by auto
1.38  termination
1.39    by (relation "measure ((\<lambda>p. if p = 0 then 0 else Suc (degree p)) \<circ> snd)")
1.40 -     (auto simp: degree_primitive_part degree_pseudo_mod_less)
1.41 +     (auto simp: degree_pseudo_mod_less)
1.42
1.43  declare gcd_poly_code_aux.simps [simp del]
1.44
```