diff -r 3736cdf9398b -r 2c69bb1374b8 src/HOL/IntDiv.thy
--- a/src/HOL/IntDiv.thy	Thu Jul 19 21:47:37 2007 +0200
+++ b/src/HOL/IntDiv.thy	Thu Jul 19 21:47:38 2007 +0200
@@ -1398,7 +1398,32 @@
  apply simp_all
 done
 
-text {* code serializer setup *}
+text {* by Brian Huffman *}
+lemma zminus_zmod: "- ((x::int) mod m) mod m = - x mod m"
+by (simp only: zmod_zminus1_eq_if mod_mod_trivial)
+
+lemma zdiff_zmod_left: "(x mod m - y) mod m = (x - y) mod (m::int)"
+by (simp only: diff_def zmod_zadd_left_eq [symmetric])
+
+lemma zdiff_zmod_right: "(x - y mod m) mod m = (x - y) mod (m::int)"
+proof -
+  have "(x + - (y mod m) mod m) mod m = (x + - y mod m) mod m"
+    by (simp only: zminus_zmod)
+  hence "(x + - (y mod m)) mod m = (x + - y) mod m"
+    by (simp only: zmod_zadd_right_eq [symmetric])
+  thus "(x - y mod m) mod m = (x - y) mod m"
+    by (simp only: diff_def)
+qed
+
+lemmas zmod_simps =
+  IntDiv.zmod_zadd_left_eq  [symmetric]
+  IntDiv.zmod_zadd_right_eq [symmetric]
+  IntDiv.zmod_zmult1_eq     [symmetric]
+  IntDiv.zmod_zmult1_eq'    [symmetric]
+  IntDiv.zpower_zmod
+  zminus_zmod zdiff_zmod_left zdiff_zmod_right
+
+text {* code generator setup *}
 
 code_modulename SML
   IntDiv Integer