--- 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 **)