# HG changeset patch
# User huffman
# Date 1332856428 -7200
# Node ID 248376f8881d9032f782934c4715cd558f695a5b
# Parent  9d7d919b9fd8c711519a8806030d4baa8bb9c228
remove redundant lemma

diff -r 9d7d919b9fd8 -r 248376f8881d NEWS
--- a/NEWS	Tue Mar 27 15:40:11 2012 +0200
+++ b/NEWS	Tue Mar 27 15:53:48 2012 +0200
@@ -152,6 +152,7 @@
   zdiv_minus1_right ~> div_minus1_right
   zmod_minus1_right ~> mod_minus1_right
   zdvd_mult_div_cancel ~> dvd_mult_div_cancel
+  zmod_zmult1_eq ~> mod_mult_right_eq
   mod_mult_distrib ~> mult_mod_left
   mod_mult_distrib2 ~> mult_mod_right
 
diff -r 9d7d919b9fd8 -r 248376f8881d src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Tue Mar 27 15:40:11 2012 +0200
+++ b/src/HOL/Divides.thy	Tue Mar 27 15:53:48 2012 +0200
@@ -1786,9 +1786,6 @@
 apply (blast intro: divmod_int_rel_div_mod [THEN zmult1_lemma, THEN div_int_unique])
 done
 
-lemma zmod_zmult1_eq: "(a*b) mod c = a*(b mod c) mod (c::int)"
-  by (fact mod_mult_right_eq) (* FIXME: delete *)
-
 text{*proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) *}
 
 lemma zadd1_lemma:
diff -r 9d7d919b9fd8 -r 248376f8881d src/HOL/Number_Theory/Cong.thy
--- a/src/HOL/Number_Theory/Cong.thy	Tue Mar 27 15:40:11 2012 +0200
+++ b/src/HOL/Number_Theory/Cong.thy	Tue Mar 27 15:53:48 2012 +0200
@@ -214,9 +214,9 @@
 lemma cong_mult_int:
     "[(a::int) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a * c = b * d] (mod m)"
   apply (unfold cong_int_def)
-  apply (subst (1 2) zmod_zmult1_eq)
+  apply (subst (1 2) mod_mult_right_eq)
   apply (subst (1 2) mult_commute)
-  apply (subst (1 2) zmod_zmult1_eq)
+  apply (subst (1 2) mod_mult_right_eq)
   apply simp
   done
 
diff -r 9d7d919b9fd8 -r 248376f8881d src/HOL/Number_Theory/Residues.thy
--- a/src/HOL/Number_Theory/Residues.thy	Tue Mar 27 15:40:11 2012 +0200
+++ b/src/HOL/Number_Theory/Residues.thy	Tue Mar 27 15:53:48 2012 +0200
@@ -56,7 +56,7 @@
   apply auto
   apply (subgoal_tac "x * y mod m * z mod m = z * (x * y mod m) mod m")
   apply (erule ssubst)
-  apply (subst zmod_zmult1_eq [symmetric])+
+  apply (subst mod_mult_right_eq [symmetric])+
   apply (simp_all only: mult_ac)
   done
 
@@ -67,7 +67,7 @@
   apply (unfold R_def residue_ring_def, auto)
   apply (subst mod_add_eq [symmetric])
   apply (subst mult_commute)
-  apply (subst zmod_zmult1_eq [symmetric])
+  apply (subst mod_mult_right_eq [symmetric])
   apply (simp add: field_simps)
   done
 
@@ -151,9 +151,9 @@
 
 lemma mult_cong: "(x mod m) \<otimes> (y mod m) = (x * y) mod m"
   apply (unfold R_def residue_ring_def, auto)
-  apply (subst zmod_zmult1_eq [symmetric])
+  apply (subst mod_mult_right_eq [symmetric])
   apply (subst mult_commute)
-  apply (subst zmod_zmult1_eq [symmetric])
+  apply (subst mod_mult_right_eq [symmetric])
   apply (subst mult_commute)
   apply auto
   done
diff -r 9d7d919b9fd8 -r 248376f8881d src/HOL/Old_Number_Theory/IntPrimes.thy
--- a/src/HOL/Old_Number_Theory/IntPrimes.thy	Tue Mar 27 15:40:11 2012 +0200
+++ b/src/HOL/Old_Number_Theory/IntPrimes.thy	Tue Mar 27 15:53:48 2012 +0200
@@ -407,7 +407,7 @@
   apply (cut_tac a = a and n = n in zcong_lineq_ex, auto)
   apply (rule_tac x = "x * b mod n" in exI, safe)
     apply (simp_all (no_asm_simp))
-  apply (metis zcong_scalar zcong_zmod zmod_zmult1_eq mult_1 mult_assoc)
+  apply (metis zcong_scalar zcong_zmod mod_mult_right_eq mult_1 mult_assoc)
   done
 
 end
diff -r 9d7d919b9fd8 -r 248376f8881d src/HOL/Old_Number_Theory/WilsonRuss.thy
--- a/src/HOL/Old_Number_Theory/WilsonRuss.thy	Tue Mar 27 15:40:11 2012 +0200
+++ b/src/HOL/Old_Number_Theory/WilsonRuss.thy	Tue Mar 27 15:53:48 2012 +0200
@@ -35,7 +35,7 @@
     "zprime p \<Longrightarrow> 0 < a \<Longrightarrow> a < p ==> [a * inv p a = 1] (mod p)"
   apply (unfold inv_def)
   apply (subst zcong_zmod)
-  apply (subst zmod_zmult1_eq [symmetric])
+  apply (subst mod_mult_right_eq [symmetric])
   apply (subst zcong_zmod [symmetric])
   apply (subst power_Suc [symmetric])
   apply (subst inv_is_inv_aux)
diff -r 9d7d919b9fd8 -r 248376f8881d src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Tue Mar 27 15:40:11 2012 +0200
+++ b/src/HOL/Parity.thy	Tue Mar 27 15:53:48 2012 +0200
@@ -74,7 +74,7 @@
 lemma anything_times_even: "even (y::int) ==> even (x * y)" by algebra
 
 lemma odd_times_odd: "odd (x::int) ==> odd y ==> odd (x * y)" 
-  by (simp add: even_def zmod_zmult1_eq)
+  by (simp add: even_def mod_mult_right_eq)
 
 lemma even_product[simp,presburger]: "even((x::int) * y) = (even x | even y)"
   apply (auto simp add: even_times_anything anything_times_even)
diff -r 9d7d919b9fd8 -r 248376f8881d src/HOL/Word/Bit_Representation.thy
--- a/src/HOL/Word/Bit_Representation.thy	Tue Mar 27 15:40:11 2012 +0200
+++ b/src/HOL/Word/Bit_Representation.thy	Tue Mar 27 15:53:48 2012 +0200
@@ -630,13 +630,13 @@
 lemmas brdmod1s' [symmetric] = 
   mod_add_left_eq mod_add_right_eq 
   zmod_zsub_left_eq zmod_zsub_right_eq 
-  zmod_zmult1_eq zmod_zmult1_eq_rev 
+  mod_mult_right_eq zmod_zmult1_eq_rev 
 
 lemmas brdmods' [symmetric] = 
   zpower_zmod' [symmetric]
   trans [OF mod_add_left_eq mod_add_right_eq] 
   trans [OF zmod_zsub_left_eq zmod_zsub_right_eq] 
-  trans [OF zmod_zmult1_eq zmod_zmult1_eq_rev] 
+  trans [OF mod_mult_right_eq zmod_zmult1_eq_rev] 
   zmod_uminus' [symmetric]
   mod_add_left_eq [where b = "1::int"]
   zmod_zsub_left_eq [where b = "1"]
diff -r 9d7d919b9fd8 -r 248376f8881d src/HOL/Word/Misc_Numeric.thy
--- a/src/HOL/Word/Misc_Numeric.thy	Tue Mar 27 15:40:11 2012 +0200
+++ b/src/HOL/Word/Misc_Numeric.thy	Tue Mar 27 15:53:48 2012 +0200
@@ -121,13 +121,13 @@
 lemma zmod_zmult1_eq_rev:
   "b * a mod c = b mod c * a mod (c::int)"
   apply (simp add: mult_commute)
-  apply (subst zmod_zmult1_eq)
+  apply (subst mod_mult_right_eq)
   apply simp
   done
 
 lemmas rdmods [symmetric] = zmod_uminus [symmetric]
   zmod_zsub_left_eq zmod_zsub_right_eq mod_add_left_eq
-  mod_add_right_eq zmod_zmult1_eq zmod_zmult1_eq_rev
+  mod_add_right_eq mod_mult_right_eq zmod_zmult1_eq_rev
 
 lemma mod_plus_right:
   "((a + x) mod m = (b + x) mod m) = (a mod m = b mod (m :: nat))"