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.22    show "comm_semiring_1.prime_elem times 1 0 = prime_elem"
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.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.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>
```