1.1 --- a/NEWS Tue Mar 27 15:40:11 2012 +0200
1.2 +++ b/NEWS Tue Mar 27 15:53:48 2012 +0200
1.3 @@ -152,6 +152,7 @@
1.4 zdiv_minus1_right ~> div_minus1_right
1.5 zmod_minus1_right ~> mod_minus1_right
1.6 zdvd_mult_div_cancel ~> dvd_mult_div_cancel
1.7 + zmod_zmult1_eq ~> mod_mult_right_eq
1.8 mod_mult_distrib ~> mult_mod_left
1.9 mod_mult_distrib2 ~> mult_mod_right
1.10
2.1 --- a/src/HOL/Divides.thy Tue Mar 27 15:40:11 2012 +0200
2.2 +++ b/src/HOL/Divides.thy Tue Mar 27 15:53:48 2012 +0200
2.3 @@ -1786,9 +1786,6 @@
2.4 apply (blast intro: divmod_int_rel_div_mod [THEN zmult1_lemma, THEN div_int_unique])
2.5 done
2.6
2.7 -lemma zmod_zmult1_eq: "(a*b) mod c = a*(b mod c) mod (c::int)"
2.8 - by (fact mod_mult_right_eq) (* FIXME: delete *)
2.9 -
2.10 text{*proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) *}
2.11
2.12 lemma zadd1_lemma:
3.1 --- a/src/HOL/Number_Theory/Cong.thy Tue Mar 27 15:40:11 2012 +0200
3.2 +++ b/src/HOL/Number_Theory/Cong.thy Tue Mar 27 15:53:48 2012 +0200
3.3 @@ -214,9 +214,9 @@
3.4 lemma cong_mult_int:
3.5 "[(a::int) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a * c = b * d] (mod m)"
3.6 apply (unfold cong_int_def)
3.7 - apply (subst (1 2) zmod_zmult1_eq)
3.8 + apply (subst (1 2) mod_mult_right_eq)
3.9 apply (subst (1 2) mult_commute)
3.10 - apply (subst (1 2) zmod_zmult1_eq)
3.11 + apply (subst (1 2) mod_mult_right_eq)
3.12 apply simp
3.13 done
3.14
4.1 --- a/src/HOL/Number_Theory/Residues.thy Tue Mar 27 15:40:11 2012 +0200
4.2 +++ b/src/HOL/Number_Theory/Residues.thy Tue Mar 27 15:53:48 2012 +0200
4.3 @@ -56,7 +56,7 @@
4.4 apply auto
4.5 apply (subgoal_tac "x * y mod m * z mod m = z * (x * y mod m) mod m")
4.6 apply (erule ssubst)
4.7 - apply (subst zmod_zmult1_eq [symmetric])+
4.8 + apply (subst mod_mult_right_eq [symmetric])+
4.9 apply (simp_all only: mult_ac)
4.10 done
4.11
4.12 @@ -67,7 +67,7 @@
4.13 apply (unfold R_def residue_ring_def, auto)
4.14 apply (subst mod_add_eq [symmetric])
4.15 apply (subst mult_commute)
4.16 - apply (subst zmod_zmult1_eq [symmetric])
4.17 + apply (subst mod_mult_right_eq [symmetric])
4.18 apply (simp add: field_simps)
4.19 done
4.20
4.21 @@ -151,9 +151,9 @@
4.22
4.23 lemma mult_cong: "(x mod m) \<otimes> (y mod m) = (x * y) mod m"
4.24 apply (unfold R_def residue_ring_def, auto)
4.25 - apply (subst zmod_zmult1_eq [symmetric])
4.26 + apply (subst mod_mult_right_eq [symmetric])
4.27 apply (subst mult_commute)
4.28 - apply (subst zmod_zmult1_eq [symmetric])
4.29 + apply (subst mod_mult_right_eq [symmetric])
4.30 apply (subst mult_commute)
4.31 apply auto
4.32 done
5.1 --- a/src/HOL/Old_Number_Theory/IntPrimes.thy Tue Mar 27 15:40:11 2012 +0200
5.2 +++ b/src/HOL/Old_Number_Theory/IntPrimes.thy Tue Mar 27 15:53:48 2012 +0200
5.3 @@ -407,7 +407,7 @@
5.4 apply (cut_tac a = a and n = n in zcong_lineq_ex, auto)
5.5 apply (rule_tac x = "x * b mod n" in exI, safe)
5.6 apply (simp_all (no_asm_simp))
5.7 - apply (metis zcong_scalar zcong_zmod zmod_zmult1_eq mult_1 mult_assoc)
5.8 + apply (metis zcong_scalar zcong_zmod mod_mult_right_eq mult_1 mult_assoc)
5.9 done
5.10
5.11 end
6.1 --- a/src/HOL/Old_Number_Theory/WilsonRuss.thy Tue Mar 27 15:40:11 2012 +0200
6.2 +++ b/src/HOL/Old_Number_Theory/WilsonRuss.thy Tue Mar 27 15:53:48 2012 +0200
6.3 @@ -35,7 +35,7 @@
6.4 "zprime p \<Longrightarrow> 0 < a \<Longrightarrow> a < p ==> [a * inv p a = 1] (mod p)"
6.5 apply (unfold inv_def)
6.6 apply (subst zcong_zmod)
6.7 - apply (subst zmod_zmult1_eq [symmetric])
6.8 + apply (subst mod_mult_right_eq [symmetric])
6.9 apply (subst zcong_zmod [symmetric])
6.10 apply (subst power_Suc [symmetric])
6.11 apply (subst inv_is_inv_aux)
7.1 --- a/src/HOL/Parity.thy Tue Mar 27 15:40:11 2012 +0200
7.2 +++ b/src/HOL/Parity.thy Tue Mar 27 15:53:48 2012 +0200
7.3 @@ -74,7 +74,7 @@
7.4 lemma anything_times_even: "even (y::int) ==> even (x * y)" by algebra
7.5
7.6 lemma odd_times_odd: "odd (x::int) ==> odd y ==> odd (x * y)"
7.7 - by (simp add: even_def zmod_zmult1_eq)
7.8 + by (simp add: even_def mod_mult_right_eq)
7.9
7.10 lemma even_product[simp,presburger]: "even((x::int) * y) = (even x | even y)"
7.11 apply (auto simp add: even_times_anything anything_times_even)
8.1 --- a/src/HOL/Word/Bit_Representation.thy Tue Mar 27 15:40:11 2012 +0200
8.2 +++ b/src/HOL/Word/Bit_Representation.thy Tue Mar 27 15:53:48 2012 +0200
8.3 @@ -630,13 +630,13 @@
8.4 lemmas brdmod1s' [symmetric] =
8.5 mod_add_left_eq mod_add_right_eq
8.6 zmod_zsub_left_eq zmod_zsub_right_eq
8.7 - zmod_zmult1_eq zmod_zmult1_eq_rev
8.8 + mod_mult_right_eq zmod_zmult1_eq_rev
8.9
8.10 lemmas brdmods' [symmetric] =
8.11 zpower_zmod' [symmetric]
8.12 trans [OF mod_add_left_eq mod_add_right_eq]
8.13 trans [OF zmod_zsub_left_eq zmod_zsub_right_eq]
8.14 - trans [OF zmod_zmult1_eq zmod_zmult1_eq_rev]
8.15 + trans [OF mod_mult_right_eq zmod_zmult1_eq_rev]
8.16 zmod_uminus' [symmetric]
8.17 mod_add_left_eq [where b = "1::int"]
8.18 zmod_zsub_left_eq [where b = "1"]
9.1 --- a/src/HOL/Word/Misc_Numeric.thy Tue Mar 27 15:40:11 2012 +0200
9.2 +++ b/src/HOL/Word/Misc_Numeric.thy Tue Mar 27 15:53:48 2012 +0200
9.3 @@ -121,13 +121,13 @@
9.4 lemma zmod_zmult1_eq_rev:
9.5 "b * a mod c = b mod c * a mod (c::int)"
9.6 apply (simp add: mult_commute)
9.7 - apply (subst zmod_zmult1_eq)
9.8 + apply (subst mod_mult_right_eq)
9.9 apply simp
9.10 done
9.11
9.12 lemmas rdmods [symmetric] = zmod_uminus [symmetric]
9.13 zmod_zsub_left_eq zmod_zsub_right_eq mod_add_left_eq
9.14 - mod_add_right_eq zmod_zmult1_eq zmod_zmult1_eq_rev
9.15 + mod_add_right_eq mod_mult_right_eq zmod_zmult1_eq_rev
9.16
9.17 lemma mod_plus_right:
9.18 "((a + x) mod m = (b + x) mod m) = (a mod m = b mod (m :: nat))"