src/HOL/Library/Polynomial.thy
changeset 47108 2a1953f0d20d
parent 47002 9435d419109a
child 47317 432b29a96f61
     1.1 --- a/src/HOL/Library/Polynomial.thy	Sat Mar 24 16:27:04 2012 +0100
     1.2 +++ b/src/HOL/Library/Polynomial.thy	Sun Mar 25 20:15:39 2012 +0200
     1.3 @@ -662,17 +662,6 @@
     1.4  
     1.5  instance poly :: (comm_ring_1) comm_ring_1 ..
     1.6  
     1.7 -instantiation poly :: (comm_ring_1) number_ring
     1.8 -begin
     1.9 -
    1.10 -definition
    1.11 -  "number_of k = (of_int k :: 'a poly)"
    1.12 -
    1.13 -instance
    1.14 -  by default (rule number_of_poly_def)
    1.15 -
    1.16 -end
    1.17 -
    1.18  
    1.19  subsection {* Polynomials form an integral domain *}
    1.20  
    1.21 @@ -1052,12 +1041,12 @@
    1.22  lemma poly_div_minus_left [simp]:
    1.23    fixes x y :: "'a::field poly"
    1.24    shows "(- x) div y = - (x div y)"
    1.25 -  using div_smult_left [of "- 1::'a"] by simp
    1.26 +  using div_smult_left [of "- 1::'a"] by (simp del: minus_one) (* FIXME *)
    1.27  
    1.28  lemma poly_mod_minus_left [simp]:
    1.29    fixes x y :: "'a::field poly"
    1.30    shows "(- x) mod y = - (x mod y)"
    1.31 -  using mod_smult_left [of "- 1::'a"] by simp
    1.32 +  using mod_smult_left [of "- 1::'a"] by (simp del: minus_one) (* FIXME *)
    1.33  
    1.34  lemma pdivmod_rel_smult_right:
    1.35    "\<lbrakk>a \<noteq> 0; pdivmod_rel x y q r\<rbrakk>
    1.36 @@ -1075,12 +1064,12 @@
    1.37    fixes x y :: "'a::field poly"
    1.38    shows "x div (- y) = - (x div y)"
    1.39    using div_smult_right [of "- 1::'a"]
    1.40 -  by (simp add: nonzero_inverse_minus_eq)
    1.41 +  by (simp add: nonzero_inverse_minus_eq del: minus_one) (* FIXME *)
    1.42  
    1.43  lemma poly_mod_minus_right [simp]:
    1.44    fixes x y :: "'a::field poly"
    1.45    shows "x mod (- y) = x mod y"
    1.46 -  using mod_smult_right [of "- 1::'a"] by simp
    1.47 +  using mod_smult_right [of "- 1::'a"] by (simp del: minus_one) (* FIXME *)
    1.48  
    1.49  lemma pdivmod_rel_mult:
    1.50    "\<lbrakk>pdivmod_rel x y q r; pdivmod_rel q z q' r'\<rbrakk>