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.5  instance poly :: (comm_ring_1) comm_ring_1 ..
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.19  subsection {* Polynomials form an integral domain *}
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.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.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.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.49  lemma pdivmod_rel_mult:
1.50    "\<lbrakk>pdivmod_rel x y q r; pdivmod_rel q z q' r'\<rbrakk>