--- 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
--- 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:
--- 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
--- 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
--- 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
--- 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)
--- 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)
--- 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"]
--- 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))"