# HG changeset patch
# User huffman
# Date 1231434749 28800
# Node ID 98ab21b14f09eb612415f4813cc46ecab15d1ccb
# Parent  ee15ccdeaa727f731e60236360e903d7788c710e
add class ring_div; generalize mod/diff/minus proofs for class ring_div

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} *}
 
diff -r ee15ccdeaa72 -r 98ab21b14f09 src/HOL/IntDiv.thy
--- a/src/HOL/IntDiv.thy	Thu Jan 08 08:36:16 2009 -0800
+++ b/src/HOL/IntDiv.thy	Thu Jan 08 09:12:29 2009 -0800
@@ -776,7 +776,7 @@
 apply (blast intro: zadd1_lemma [OF quorem_div_mod quorem_div_mod] quorem_mod)
 done
 
-instance int :: semiring_div
+instance int :: ring_div
 proof
   fix a b c :: int
   assume not0: "b \<noteq> 0"
@@ -818,14 +818,8 @@
 lemma zmod_zadd_self2: "(b+a) mod a = b mod (a::int)"
 by (rule mod_add_self2) (* already declared [simp] *)
 
-lemma zmod_zdiff1_eq: fixes a::int
-  shows "(a - b) mod c = (a mod c - b mod c) mod c" (is "?l = ?r")
-proof -
-  have "?l = (c + (a mod c - b mod c)) mod c"
-    using zmod_zadd1_eq[of a "-b" c] by(simp add:ring_simps zmod_zminus1_eq_if)
-  also have "\<dots> = ?r" by simp
-  finally show ?thesis .
-qed
+lemma zmod_zdiff1_eq: "(a - b) mod c = (a mod c - b mod c) mod (c::int)"
+by (rule mod_diff_eq)
 
 subsection{*Proving  @{term "a div (b*c) = (a div b) div c"} *}
 
@@ -1423,20 +1417,13 @@
 
 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)
+by (rule mod_minus_eq [symmetric])
 
 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])
+by (rule mod_diff_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
+by (rule mod_diff_right_eq [symmetric])
 
 lemmas zmod_simps =
   IntDiv.zmod_zadd_left_eq  [symmetric]