# HG changeset patch
# User huffman
# Date 1231431848 28800
# Node ID fe17df4e4ab3e95ef1dab960443244c1f5610d63
# Parent  9610f3870d64ef33b393e4471544e2aea082835a
generalize some div/mod lemmas; remove type-specific proofs

diff -r 9610f3870d64 -r fe17df4e4ab3 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Wed Jan 07 08:13:56 2009 -0800
+++ b/src/HOL/Divides.thy	Thu Jan 08 08:24:08 2009 -0800
@@ -33,6 +33,10 @@
   unfolding mult_commute [of b]
   by (rule mod_div_equality)
 
+lemma mod_div_equality': "a mod b + a div b * b = a"
+  using mod_div_equality [of a b]
+  by (simp only: add_ac)
+
 lemma div_mod_equality: "((a div b) * b + a mod b) + c = a + c"
   by (simp add: mod_div_equality)
 
@@ -143,6 +147,107 @@
   then show "b mod a = 0" by simp
 qed
 
+lemma mod_div_trivial [simp]: "a mod b div b = 0"
+proof (cases "b = 0")
+  assume "b = 0"
+  thus ?thesis by simp
+next
+  assume "b \<noteq> 0"
+  hence "a div b + a mod b div b = (a mod b + a div b * b) div b"
+    by (rule div_mult_self1 [symmetric])
+  also have "\<dots> = a div b"
+    by (simp only: mod_div_equality')
+  also have "\<dots> = a div b + 0"
+    by simp
+  finally show ?thesis
+    by (rule add_left_imp_eq)
+qed
+
+lemma mod_mod_trivial [simp]: "a mod b mod b = a mod b"
+proof -
+  have "a mod b mod b = (a mod b + a div b * b) mod b"
+    by (simp only: mod_mult_self1)
+  also have "\<dots> = a mod b"
+    by (simp only: mod_div_equality')
+  finally show ?thesis .
+qed
+
+text {* Addition respects modular equivalence. *}
+
+lemma mod_add_left_eq: "(a + b) mod c = (a mod c + b) mod c"
+proof -
+  have "(a + b) mod c = (a div c * c + a mod c + b) mod c"
+    by (simp only: mod_div_equality)
+  also have "\<dots> = (a mod c + b + a div c * c) mod c"
+    by (simp only: add_ac)
+  also have "\<dots> = (a mod c + b) mod c"
+    by (rule mod_mult_self1)
+  finally show ?thesis .
+qed
+
+lemma mod_add_right_eq: "(a + b) mod c = (a + b mod c) mod c"
+proof -
+  have "(a + b) mod c = (a + (b div c * c + b mod c)) mod c"
+    by (simp only: mod_div_equality)
+  also have "\<dots> = (a + b mod c + b div c * c) mod c"
+    by (simp only: add_ac)
+  also have "\<dots> = (a + b mod c) mod c"
+    by (rule mod_mult_self1)
+  finally show ?thesis .
+qed
+
+lemma mod_add_eq: "(a + b) mod c = (a mod c + b mod c) mod c"
+by (rule trans [OF mod_add_left_eq mod_add_right_eq])
+
+lemma mod_add_cong:
+  assumes "a mod c = a' mod c"
+  assumes "b mod c = b' mod c"
+  shows "(a + b) mod c = (a' + b') mod c"
+proof -
+  have "(a mod c + b mod c) mod c = (a' mod c + b' mod c) mod c"
+    unfolding assms ..
+  thus ?thesis
+    by (simp only: mod_add_eq [symmetric])
+qed
+
+text {* Multiplication respects modular equivalence. *}
+
+lemma mod_mult_left_eq: "(a * b) mod c = ((a mod c) * b) mod c"
+proof -
+  have "(a * b) mod c = ((a div c * c + a mod c) * b) mod c"
+    by (simp only: mod_div_equality)
+  also have "\<dots> = (a mod c * b + a div c * b * c) mod c"
+    by (simp only: left_distrib right_distrib add_ac mult_ac)
+  also have "\<dots> = (a mod c * b) mod c"
+    by (rule mod_mult_self1)
+  finally show ?thesis .
+qed
+
+lemma mod_mult_right_eq: "(a * b) mod c = (a * (b mod c)) mod c"
+proof -
+  have "(a * b) mod c = (a * (b div c * c + b mod c)) mod c"
+    by (simp only: mod_div_equality)
+  also have "\<dots> = (a * (b mod c) + a * (b div c) * c) mod c"
+    by (simp only: left_distrib right_distrib add_ac mult_ac)
+  also have "\<dots> = (a * (b mod c)) mod c"
+    by (rule mod_mult_self1)
+  finally show ?thesis .
+qed
+
+lemma mod_mult_eq: "(a * b) mod c = ((a mod c) * (b mod c)) mod c"
+by (rule trans [OF mod_mult_left_eq mod_mult_right_eq])
+
+lemma mod_mult_cong:
+  assumes "a mod c = a' mod c"
+  assumes "b mod c = b' mod c"
+  shows "(a * b) mod c = (a' * b') mod c"
+proof -
+  have "(a mod c * (b mod c)) mod c = (a' mod c * (b' mod c)) mod c"
+    unfolding assms ..
+  thus ?thesis
+    by (simp only: mod_mult_eq [symmetric])
+qed
+
 end
 
 
@@ -467,22 +572,14 @@
 done
 
 lemma mod_mult1_eq: "(a*b) mod c = a*(b mod c) mod (c::nat)"
-apply (cases "c = 0", simp)
-apply (blast intro: divmod_rel [THEN divmod_rel_mult1_eq, THEN mod_eq])
-done
+  by (rule mod_mult_right_eq)
 
 lemma mod_mult1_eq': "(a*b) mod (c::nat) = ((a mod c) * b) mod c"
-  apply (rule trans)
-   apply (rule_tac s = "b*a mod c" in trans)
-    apply (rule_tac [2] mod_mult1_eq)
-   apply (simp_all add: mult_commute)
-  done
+  by (rule mod_mult_left_eq)
 
 lemma mod_mult_distrib_mod:
   "(a*b) mod (c::nat) = ((a mod c) * (b mod c)) mod c"
-apply (rule mod_mult1_eq' [THEN trans])
-apply (rule mod_mult1_eq)
-done
+  by (rule mod_mult_eq)
 
 lemma divmod_rel_add1_eq:
   "[| divmod_rel a c aq ar; divmod_rel b c bq br;  c > 0 |]
@@ -497,9 +594,7 @@
 done
 
 lemma mod_add1_eq: "(a+b) mod (c::nat) = (a mod c + b mod c) mod c"
-apply (cases "c = 0", simp)
-apply (blast intro: divmod_rel_add1_eq [THEN mod_eq] divmod_rel)
-done
+  by (rule mod_add_eq)
 
 lemma mod_lemma: "[| (0::nat) < c; r < b |] ==> b * (q mod c) + r < b * c"
   apply (cut_tac m = q and n = c in mod_less_divisor)
@@ -618,11 +713,11 @@
 apply (auto simp add: Suc_diff_le le_mod_geq)
 done
 
-lemma nat_mod_div_trivial [simp]: "m mod n div n = (0 :: nat)"
-  by (cases "n = 0") auto
+lemma nat_mod_div_trivial: "m mod n div n = (0 :: nat)"
+  by simp
 
-lemma nat_mod_mod_trivial [simp]: "m mod n mod n = (m mod n :: nat)"
-  by (cases "n = 0") auto
+lemma nat_mod_mod_trivial: "m mod n mod n = (m mod n :: nat)"
+  by simp
 
 
 subsubsection {* The Divides Relation *}
@@ -718,18 +813,6 @@
   apply (simp add: power_add)
   done
 
-lemma mod_add_left_eq: "((a::nat) + b) mod c = (a mod c + b) mod c"
-  apply (rule trans [symmetric])
-   apply (rule mod_add1_eq, simp)
-  apply (rule mod_add1_eq [symmetric])
-  done
-
-lemma mod_add_right_eq: "(a+b) mod (c::nat) = (a + (b mod c)) mod c"
-  apply (rule trans [symmetric])
-   apply (rule mod_add1_eq, simp)
-  apply (rule mod_add1_eq [symmetric])
-  done
-
 lemma nat_zero_less_power_iff [simp]: "(x^n > 0) = (x > (0::nat) | n=0)"
   by (induct n) auto
 
diff -r 9610f3870d64 -r fe17df4e4ab3 src/HOL/IntDiv.thy
--- a/src/HOL/IntDiv.thy	Wed Jan 07 08:13:56 2009 -0800
+++ b/src/HOL/IntDiv.thy	Thu Jan 08 08:24:08 2009 -0800
@@ -747,12 +747,12 @@
 lemma zdiv_zmult_self1 [simp]: "b \<noteq> (0::int) ==> (a*b) div b = a"
 by (simp add: zdiv_zmult1_eq)
 
-lemma mod_div_trivial [simp]: "(a mod b) div b = (0::int)"
+lemma zmod_zdiv_trivial: "(a mod b) div b = (0::int)"
 apply (case_tac "b = 0", simp)
 apply (auto simp add: linorder_neq_iff div_pos_pos_trivial div_neg_neg_trivial)
 done
 
-lemma mod_mod_trivial [simp]: "(a mod b) mod b = a mod (b::int)"
+lemma zmod_zmod_trivial: "(a mod b) mod b = a mod (b::int)"
 apply (case_tac "b = 0", simp)
 apply (force simp add: linorder_neq_iff mod_pos_pos_trivial mod_neg_neg_trivial)
 done
@@ -776,63 +776,47 @@
 apply (blast intro: zadd1_lemma [OF quorem_div_mod quorem_div_mod] quorem_mod)
 done
 
-lemma zdiv_zadd_self1[simp]: "a \<noteq> (0::int) ==> (a+b) div a = b div a + 1"
-by (simp add: zdiv_zadd1_eq)
-
-lemma zdiv_zadd_self2[simp]: "a \<noteq> (0::int) ==> (b+a) div a = b div a + 1"
-by (simp add: zdiv_zadd1_eq)
-
 instance int :: semiring_div
 proof
   fix a b c :: int
   assume not0: "b \<noteq> 0"
   show "(a + c * b) div b = c + a div b"
     unfolding zdiv_zadd1_eq [of a "c * b"] using not0 
-      by (simp add: zmod_zmult1_eq)
+      by (simp add: zmod_zmult1_eq zmod_zdiv_trivial)
 qed auto
 
-lemma zdiv_zmult_self2 [simp]: "b \<noteq> (0::int) ==> (b*a) div b = a"
-by (subst mult_commute, erule zdiv_zmult_self1)
+lemma zdiv_zadd_self1: "a \<noteq> (0::int) ==> (a+b) div a = b div a + 1"
+by (rule div_add_self1) (* already declared [simp] *)
+
+lemma zdiv_zadd_self2: "a \<noteq> (0::int) ==> (b+a) div a = b div a + 1"
+by (rule div_add_self2) (* already declared [simp] *)
 
-lemma zmod_zmult_self1 [simp]: "(a*b) mod b = (0::int)"
-by (simp add: zmod_zmult1_eq)
+lemma zdiv_zmult_self2: "b \<noteq> (0::int) ==> (b*a) div b = a"
+by (rule div_mult_self1_is_id) (* already declared [simp] *)
 
-lemma zmod_zmult_self2 [simp]: "(b*a) mod b = (0::int)"
-by (simp add: mult_commute zmod_zmult1_eq)
+lemma zmod_zmult_self1: "(a*b) mod b = (0::int)"
+by (rule mod_mult_self2_is_0) (* already declared [simp] *)
+
+lemma zmod_zmult_self2: "(b*a) mod b = (0::int)"
+by (rule mod_mult_self1_is_0) (* already declared [simp] *)
 
 lemma zmod_eq_0_iff: "(m mod d = 0) = (EX q::int. m = d*q)"
-proof
-  assume "m mod d = 0"
-  with zmod_zdiv_equality[of m d] show "EX q::int. m = d*q" by auto
-next
-  assume "EX q::int. m = d*q"
-  thus "m mod d = 0" by auto
-qed
+by (simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def)
 
+(* REVISIT: should this be generalized to all semiring_div types? *)
 lemmas zmod_eq_0D [dest!] = zmod_eq_0_iff [THEN iffD1]
 
 lemma zmod_zadd_left_eq: "(a+b) mod (c::int) = ((a mod c) + b) mod c"
-apply (rule trans [symmetric])
-apply (rule zmod_zadd1_eq, simp)
-apply (rule zmod_zadd1_eq [symmetric])
-done
+by (rule mod_add_left_eq)
 
 lemma zmod_zadd_right_eq: "(a+b) mod (c::int) = (a + (b mod c)) mod c"
-apply (rule trans [symmetric])
-apply (rule zmod_zadd1_eq, simp)
-apply (rule zmod_zadd1_eq [symmetric])
-done
+by (rule mod_add_right_eq)
 
-lemma zmod_zadd_self1[simp]: "(a+b) mod a = b mod (a::int)"
-apply (case_tac "a = 0", simp)
-apply (simp add: zmod_zadd1_eq)
-done
+lemma zmod_zadd_self1: "(a+b) mod a = b mod (a::int)"
+by (rule mod_add_self1) (* already declared [simp] *)
 
-lemma zmod_zadd_self2[simp]: "(b+a) mod a = b mod (a::int)"
-apply (case_tac "a = 0", simp)
-apply (simp add: zmod_zadd1_eq)
-done
-
+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")