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.20      by (simp add: unit_factor_field_poly_def lead_coeff_nonzero is_unit_pCons_iff)
    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