1.1 --- a/NEWS	Tue Mar 27 15:53:48 2012 +0200
     1.2 +++ b/NEWS	Tue Mar 27 16:04:51 2012 +0200
     1.3 @@ -153,6 +153,7 @@
     1.4    zmod_minus1_right ~> mod_minus1_right
     1.5    zdvd_mult_div_cancel ~> dvd_mult_div_cancel
     1.6    zmod_zmult1_eq ~> mod_mult_right_eq
     1.7 +  zpower_zmod ~> power_mod
     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:53:48 2012 +0200
     2.2 +++ b/src/HOL/Divides.thy	Tue Mar 27 16:04:51 2012 +0200
     2.3 @@ -283,6 +283,15 @@
     2.4      by (simp only: mod_mult_eq [symmetric])
     2.5  qed
     2.6  
     2.7 +text {* Exponentiation respects modular equivalence. *}
     2.8 +
     2.9 +lemma power_mod: "(a mod b)^n mod b = a^n mod b"
    2.10 +apply (induct n, simp_all)
    2.11 +apply (rule mod_mult_right_eq [THEN trans])
    2.12 +apply (simp (no_asm_simp))
    2.13 +apply (rule mod_mult_eq [symmetric])
    2.14 +done
    2.15 +
    2.16  lemma mod_mod_cancel:
    2.17    assumes "c dvd b"
    2.18    shows "a mod b mod c = a mod c"
    2.19 @@ -2179,13 +2188,6 @@
    2.20    using zmod_zdiv_equality[where a="m" and b="n"]
    2.21    by (simp add: algebra_simps) (* FIXME: generalize *)
    2.22  
    2.23 -lemma zpower_zmod: "((x::int) mod m)^y mod m = x^y mod m"
    2.24 -apply (induct "y", auto)
    2.25 -apply (rule mod_mult_right_eq [THEN trans])
    2.26 -apply (simp (no_asm_simp))
    2.27 -apply (rule mod_mult_eq [symmetric])
    2.28 -done (* FIXME: generalize *)
    2.29 -
    2.30  lemma zdiv_int: "int (a div b) = (int a) div (int b)"
    2.31  apply (subst split_div, auto)
    2.32  apply (subst split_zdiv, auto)
    2.33 @@ -2228,7 +2230,7 @@
    2.34    mod_add_right_eq [symmetric]
    2.35    mod_mult_right_eq[symmetric]
    2.36    mod_mult_left_eq [symmetric]
    2.37 -  zpower_zmod
    2.38 +  power_mod
    2.39    zminus_zmod zdiff_zmod_left zdiff_zmod_right
    2.40  
    2.41  text {* Distributive laws for function @{text nat}. *}

     3.1 --- a/src/HOL/Old_Number_Theory/WilsonRuss.thy	Tue Mar 27 15:53:48 2012 +0200
     3.2 +++ b/src/HOL/Old_Number_Theory/WilsonRuss.thy	Tue Mar 27 16:04:51 2012 +0200
     3.3 @@ -137,7 +137,7 @@
     3.4  lemma inv_inv: "zprime p \<Longrightarrow>
     3.5      5 \<le> p \<Longrightarrow> 0 < a \<Longrightarrow> a < p ==> inv p (inv p a) = a"
     3.6    apply (unfold inv_def)
     3.7 -  apply (subst zpower_zmod)
     3.8 +  apply (subst power_mod)
     3.9    apply (subst zpower_zpower)
    3.10    apply (rule zcong_zless_imp_eq)
    3.11        prefer 5

     4.1 --- a/src/HOL/Word/Bit_Representation.thy	Tue Mar 27 15:53:48 2012 +0200
     4.2 +++ b/src/HOL/Word/Bit_Representation.thy	Tue Mar 27 16:04:51 2012 +0200
     4.3 @@ -625,7 +625,7 @@
     4.4    unfolding no_sbintr_alt2 by (drule sb_dec_lem') simp
     4.5  
     4.6  lemmas zmod_uminus' = zmod_uminus [where b=c] for c
     4.7 -lemmas zpower_zmod' = zpower_zmod [where m=c and y=k] for c k
     4.8 +lemmas zpower_zmod' = power_mod [where b=c and n=k] for c k
     4.9  
    4.10  lemmas brdmod1s' [symmetric] = 
    4.11    mod_add_left_eq mod_add_right_eq