src/HOL/Computational_Algebra/Polynomial_Factorial.thy
changeset 66817 0b12755ccbb2
parent 66808 1907167b6038
child 66838 17989f6bc7b2
     1.1 --- a/src/HOL/Computational_Algebra/Polynomial_Factorial.thy	Sun Oct 08 22:28:22 2017 +0200
     1.2 +++ b/src/HOL/Computational_Algebra/Polynomial_Factorial.thy	Sun Oct 08 22:28:22 2017 +0200
     1.3 @@ -416,14 +416,12 @@
     1.4  begin
     1.5  
     1.6  interpretation field_poly: 
     1.7 -  unique_euclidean_ring where zero = "0 :: 'a :: field poly"
     1.8 -    and one = 1 and plus = plus
     1.9 -    and uminus = uminus and minus = minus
    1.10 +  normalization_euclidean_semiring where zero = "0 :: 'a :: field poly"
    1.11 +    and one = 1 and plus = plus and minus = minus
    1.12      and times = times
    1.13      and normalize = "\<lambda>p. smult (inverse (lead_coeff p)) p"
    1.14      and unit_factor = "\<lambda>p. [:lead_coeff p:]"
    1.15      and euclidean_size = "\<lambda>p. if p = 0 then 0 else 2 ^ degree p"
    1.16 -    and uniqueness_constraint = top
    1.17      and divide = divide and modulo = modulo
    1.18    rewrites "dvd.dvd (times :: 'a poly \<Rightarrow> _) = Rings.dvd"
    1.19      and "comm_monoid_mult.prod_mset times 1 = prod_mset"
    1.20 @@ -438,9 +436,9 @@
    1.21      by (simp add: irreducible_dict)
    1.22    show "comm_semiring_1.prime_elem times 1 0 = prime_elem"
    1.23      by (simp add: prime_elem_dict)
    1.24 -  show "class.unique_euclidean_ring divide plus minus (0 :: 'a poly) times 1
    1.25 -    (\<lambda>p. [:lead_coeff p:]) (\<lambda>p. smult (inverse (lead_coeff p)) p) modulo
    1.26 -    (\<lambda>p. if p = 0 then 0 else 2 ^ degree p) uminus top"
    1.27 +  show "class.normalization_euclidean_semiring divide plus minus (0 :: 'a poly) times 1
    1.28 +    modulo (\<lambda>p. if p = 0 then 0 else 2 ^ degree p)
    1.29 +    (\<lambda>p. [:lead_coeff p:]) (\<lambda>p. smult (inverse (lead_coeff p)) p)"
    1.30    proof (standard, fold dvd_dict)
    1.31      fix p :: "'a poly"
    1.32      show "[:lead_coeff p:] * smult (inverse (lead_coeff p)) p = p"
    1.33 @@ -453,23 +451,6 @@
    1.34      fix p :: "'a poly" assume "p \<noteq> 0"
    1.35      then show "is_unit [:lead_coeff p:]"
    1.36        by (simp add: is_unit_pCons_iff)
    1.37 -  next
    1.38 -    fix p q s :: "'a poly" assume "s \<noteq> 0"
    1.39 -    moreover assume "(if p = 0 then (0::nat) else 2 ^ degree p) < (if q = 0 then 0 else 2 ^ degree q)"
    1.40 -    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))"
    1.41 -      by (auto simp add: degree_mult_eq)
    1.42 -  next
    1.43 -    fix p q r :: "'a poly"
    1.44 -    assume "p \<noteq> 0"
    1.45 -    with eucl_rel_poly [of r p] have "eucl_rel_poly (r + q * p) p (q + r div p, r mod p)"
    1.46 -      by (simp add: eucl_rel_poly_iff distrib_right)
    1.47 -    then have "(r + q * p) div p = q + r div p"
    1.48 -      by (rule div_poly_eq)
    1.49 -    moreover assume "(if r = 0 then (0::nat) else 2 ^ degree r)
    1.50 -      < (if p = 0 then 0 else 2 ^ degree p)"
    1.51 -    ultimately show "(q * p + r) div p = q"
    1.52 -      using \<open>p \<noteq> 0\<close>
    1.53 -      by (cases "r = 0") (simp_all add: div_poly_less ac_simps)
    1.54    qed (auto simp: lead_coeff_mult Rings.div_mult_mod_eq intro!: degree_mod_less' degree_mult_right_le)
    1.55  qed
    1.56  
    1.57 @@ -758,7 +739,7 @@
    1.58  
    1.59  end
    1.60  
    1.61 -instantiation poly :: ("{field,factorial_ring_gcd}") unique_euclidean_ring
    1.62 +instantiation poly :: ("{field,factorial_ring_gcd}") "{unique_euclidean_ring, normalization_euclidean_semiring}"
    1.63  begin
    1.64  
    1.65  definition euclidean_size_poly :: "'a poly \<Rightarrow> nat"
    1.66 @@ -783,9 +764,8 @@
    1.67  
    1.68  end
    1.69  
    1.70 -instance poly :: ("{field,factorial_ring_gcd}") euclidean_ring_gcd
    1.71 -  by (rule euclidean_ring_gcd_class.intro, rule factorial_euclidean_semiring_gcdI)
    1.72 -    standard
    1.73 +instance poly :: ("{field, normalization_euclidean_semiring, factorial_ring_gcd}") euclidean_ring_gcd
    1.74 +  by (rule euclidean_ring_gcd_class.intro, rule factorial_euclidean_semiring_gcdI) standard
    1.75  
    1.76    
    1.77  subsection \<open>Polynomial GCD\<close>