# HG changeset patch
# User huffman
# Date 1332855244 -7200
# Node ID 8ada79014cb2911980c360fd80a444809b703ad4
# Parent  978c00c20a59a94514c68bda7eccb5fd0d77652d
generalize more div/mod lemmas

diff -r 978c00c20a59 -r 8ada79014cb2 NEWS
--- a/NEWS	Tue Mar 27 15:27:49 2012 +0200
+++ b/NEWS	Tue Mar 27 15:34:04 2012 +0200
@@ -149,6 +149,8 @@
   zmod_zminus_zminus ~> mod_minus_minus
   zdiv_zminus2 ~> div_minus_right
   zmod_zminus2 ~> mod_minus_right
+  zdiv_minus1_right ~> div_minus1_right
+  zmod_minus1_right ~> mod_minus1_right
   mod_mult_distrib ~> mult_mod_left
   mod_mult_distrib2 ~> mult_mod_right
 
diff -r 978c00c20a59 -r 8ada79014cb2 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Tue Mar 27 15:27:49 2012 +0200
+++ b/src/HOL/Divides.thy	Tue Mar 27 15:34:04 2012 +0200
@@ -463,6 +463,12 @@
 lemma mod_minus_right: "a mod (-b) = - ((-a) mod b)"
   using mod_minus_minus [of "-a" b] by simp
 
+lemma div_minus1_right [simp]: "a div (-1) = -a"
+  using div_minus_right [of a 1] by simp
+
+lemma mod_minus1_right [simp]: "a mod (-1) = 0"
+  using mod_minus_right [of a 1] by simp
+
 end
 
 
@@ -1661,16 +1667,6 @@
 
 text{*Special-case simplification *}
 
-lemma zmod_minus1_right [simp]: "a mod (-1::int) = 0"
-apply (cut_tac a = a and b = "-1" in neg_mod_sign)
-apply (cut_tac [2] a = a and b = "-1" in neg_mod_bound)
-apply (auto simp del: neg_mod_sign neg_mod_bound)
-done (* FIXME: generalize *)
-
-lemma zdiv_minus1_right [simp]: "a div (-1::int) = -a"
-by (cut_tac a = a and b = "-1" in zmod_zdiv_equality, auto)
-(* FIXME: generalize *)
-
 (** The last remaining special cases for constant arithmetic:
     1 div z and 1 mod z **)
 
diff -r 978c00c20a59 -r 8ada79014cb2 src/HOL/Groebner_Basis.thy
--- a/src/HOL/Groebner_Basis.thy	Tue Mar 27 15:27:49 2012 +0200
+++ b/src/HOL/Groebner_Basis.thy	Tue Mar 27 15:34:04 2012 +0200
@@ -62,8 +62,8 @@
 declare mod_0[algebra]
 declare mod_by_1[algebra]
 declare div_by_1[algebra]
-declare zmod_minus1_right[algebra]
-declare zdiv_minus1_right[algebra]
+declare mod_minus1_right[algebra]
+declare div_minus1_right[algebra]
 declare mod_div_trivial[algebra]
 declare mod_mod_trivial[algebra]
 declare mod_mult_self2_is_0[algebra]