# HG changeset patch
# User huffman
# Date 1231432576 28800
# Node ID ee15ccdeaa727f731e60236360e903d7788c710e
# Parent  fe17df4e4ab3e95ef1dab960443244c1f5610d63
generalize zmod_zmod_cancel -> mod_mod_cancel

diff -r fe17df4e4ab3 -r ee15ccdeaa72 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Thu Jan 08 08:24:08 2009 -0800
+++ b/src/HOL/Divides.thy	Thu Jan 08 08:36:16 2009 -0800
@@ -248,6 +248,23 @@
     by (simp only: mod_mult_eq [symmetric])
 qed
 
+lemma mod_mod_cancel:
+  assumes "c dvd b"
+  shows "a mod b mod c = a mod c"
+proof -
+  from `c dvd b` obtain k where "b = c * k"
+    by (rule dvdE)
+  have "a mod b mod c = a mod (c * k) mod c"
+    by (simp only: `b = c * k`)
+  also have "\<dots> = (a mod (c * k) + a div (c * k) * k * c) mod c"
+    by (simp only: mod_mult_self1)
+  also have "\<dots> = (a div (c * k) * (c * k) + a mod (c * k)) mod c"
+    by (simp only: add_ac mult_ac)
+  also have "\<dots> = a mod c"
+    by (simp only: mod_div_equality)
+  finally show ?thesis .
+qed
+
 end
 
 
diff -r fe17df4e4ab3 -r ee15ccdeaa72 src/HOL/IntDiv.thy
--- a/src/HOL/IntDiv.thy	Thu Jan 08 08:24:08 2009 -0800
+++ b/src/HOL/IntDiv.thy	Thu Jan 08 08:36:16 2009 -0800
@@ -938,18 +938,8 @@
 apply (auto simp add: mult_commute)
 done
 
-lemma zmod_zmod_cancel:
-assumes "n dvd m" shows "(k::int) mod m mod n = k mod n"
-proof -
-  from `n dvd m` obtain r where "m = n*r" by(auto simp:dvd_def)
-  have "k mod n = (m * (k div m) + k mod m) mod n"
-    using zmod_zdiv_equality[of k m] by simp
-  also have "\<dots> = (m * (k div m) mod n + k mod m mod n) mod n"
-    by(subst zmod_zadd1_eq, rule refl)
-  also have "m * (k div m) mod n = 0" using `m = n*r`
-    by(simp add:mult_ac)
-  finally show ?thesis by simp
-qed
+lemma zmod_zmod_cancel: "n dvd m \<Longrightarrow> (k::int) mod m mod n = k mod n"
+by (rule mod_mod_cancel)
 
 
 subsection {*Splitting Rules for div and mod*}