1.1 --- a/NEWS	Tue Mar 27 15:27:49 2012 +0200
     1.2 +++ b/NEWS	Tue Mar 27 15:34:04 2012 +0200
     1.3 @@ -149,6 +149,8 @@
     1.4    zmod_zminus_zminus ~> mod_minus_minus
     1.5    zdiv_zminus2 ~> div_minus_right
     1.6    zmod_zminus2 ~> mod_minus_right
     1.7 +  zdiv_minus1_right ~> div_minus1_right
     1.8 +  zmod_minus1_right ~> mod_minus1_right
     1.9    mod_mult_distrib ~> mult_mod_left
    1.10    mod_mult_distrib2 ~> mult_mod_right
    1.11  

     2.1 --- a/src/HOL/Divides.thy	Tue Mar 27 15:27:49 2012 +0200
     2.2 +++ b/src/HOL/Divides.thy	Tue Mar 27 15:34:04 2012 +0200
     2.3 @@ -463,6 +463,12 @@
     2.4  lemma mod_minus_right: "a mod (-b) = - ((-a) mod b)"
     2.5    using mod_minus_minus [of "-a" b] by simp
     2.6  
     2.7 +lemma div_minus1_right [simp]: "a div (-1) = -a"
     2.8 +  using div_minus_right [of a 1] by simp
     2.9 +
    2.10 +lemma mod_minus1_right [simp]: "a mod (-1) = 0"
    2.11 +  using mod_minus_right [of a 1] by simp
    2.12 +
    2.13  end
    2.14  
    2.15  
    2.16 @@ -1661,16 +1667,6 @@
    2.17  
    2.18  text{*Special-case simplification *}
    2.19  
    2.20 -lemma zmod_minus1_right [simp]: "a mod (-1::int) = 0"
    2.21 -apply (cut_tac a = a and b = "-1" in neg_mod_sign)
    2.22 -apply (cut_tac [2] a = a and b = "-1" in neg_mod_bound)
    2.23 -apply (auto simp del: neg_mod_sign neg_mod_bound)
    2.24 -done (* FIXME: generalize *)
    2.25 -
    2.26 -lemma zdiv_minus1_right [simp]: "a div (-1::int) = -a"
    2.27 -by (cut_tac a = a and b = "-1" in zmod_zdiv_equality, auto)
    2.28 -(* FIXME: generalize *)
    2.29 -
    2.30  (** The last remaining special cases for constant arithmetic:
    2.31      1 div z and 1 mod z **)
    2.32  

     3.1 --- a/src/HOL/Groebner_Basis.thy	Tue Mar 27 15:27:49 2012 +0200
     3.2 +++ b/src/HOL/Groebner_Basis.thy	Tue Mar 27 15:34:04 2012 +0200
     3.3 @@ -62,8 +62,8 @@
     3.4  declare mod_0[algebra]
     3.5  declare mod_by_1[algebra]
     3.6  declare div_by_1[algebra]
     3.7 -declare zmod_minus1_right[algebra]
     3.8 -declare zdiv_minus1_right[algebra]
     3.9 +declare mod_minus1_right[algebra]
    3.10 +declare div_minus1_right[algebra]
    3.11  declare mod_div_trivial[algebra]
    3.12  declare mod_mod_trivial[algebra]
    3.13  declare mod_mult_self2_is_0[algebra]