diff -r ee15ccdeaa72 -r 98ab21b14f09 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Thu Jan 08 08:36:16 2009 -0800
+++ b/src/HOL/Divides.thy	Thu Jan 08 09:12:29 2009 -0800
@@ -267,6 +267,55 @@
 
 end
 
+class ring_div = semiring_div + comm_ring_1
+begin
+
+text {* Negation respects modular equivalence. *}
+
+lemma mod_minus_eq: "(- a) mod b = (- (a mod b)) mod b"
+proof -
+  have "(- a) mod b = (- (a div b * b + a mod b)) mod b"
+    by (simp only: mod_div_equality)
+  also have "\<dots> = (- (a mod b) + - (a div b) * b) mod b"
+    by (simp only: minus_add_distrib minus_mult_left add_ac)
+  also have "\<dots> = (- (a mod b)) mod b"
+    by (rule mod_mult_self1)
+  finally show ?thesis .
+qed
+
+lemma mod_minus_cong:
+  assumes "a mod b = a' mod b"
+  shows "(- a) mod b = (- a') mod b"
+proof -
+  have "(- (a mod b)) mod b = (- (a' mod b)) mod b"
+    unfolding assms ..
+  thus ?thesis
+    by (simp only: mod_minus_eq [symmetric])
+qed
+
+text {* Subtraction respects modular equivalence. *}
+
+lemma mod_diff_left_eq: "(a - b) mod c = (a mod c - b) mod c"
+  unfolding diff_minus
+  by (intro mod_add_cong mod_minus_cong) simp_all
+
+lemma mod_diff_right_eq: "(a - b) mod c = (a - b mod c) mod c"
+  unfolding diff_minus
+  by (intro mod_add_cong mod_minus_cong) simp_all
+
+lemma mod_diff_eq: "(a - b) mod c = (a mod c - b mod c) mod c"
+  unfolding diff_minus
+  by (intro mod_add_cong mod_minus_cong) simp_all
+
+lemma mod_diff_cong:
+  assumes "a mod c = a' mod c"
+  assumes "b mod c = b' mod c"
+  shows "(a - b) mod c = (a' - b') mod c"
+  unfolding diff_minus using assms
+  by (intro mod_add_cong mod_minus_cong)
+
+end
+
 
 subsection {* Division on @{typ nat} *}