remove redundant lemma
authorhuffman
Tue Mar 27 15:53:48 2012 +0200 (2012-03-27)
changeset 47163248376f8881d
parent 47162 9d7d919b9fd8
child 47164 6a4c479ba94f
remove redundant lemma
NEWS
src/HOL/Divides.thy
src/HOL/Number_Theory/Cong.thy
src/HOL/Number_Theory/Residues.thy
src/HOL/Old_Number_Theory/IntPrimes.thy
src/HOL/Old_Number_Theory/WilsonRuss.thy
src/HOL/Parity.thy
src/HOL/Word/Bit_Representation.thy
src/HOL/Word/Misc_Numeric.thy
     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))"