# HG changeset patch
# User huffman
# Date 1332857091 -7200
# Node ID 6a4c479ba94f03195678df906a3dbb4ffc1894e1
# Parent  248376f8881d9032f782934c4715cd558f695a5b
generalized lemma zpower_zmod

diff -r 248376f8881d -r 6a4c479ba94f NEWS
--- a/NEWS	Tue Mar 27 15:53:48 2012 +0200
+++ b/NEWS	Tue Mar 27 16:04:51 2012 +0200
@@ -153,6 +153,7 @@
   zmod_minus1_right ~> mod_minus1_right
   zdvd_mult_div_cancel ~> dvd_mult_div_cancel
   zmod_zmult1_eq ~> mod_mult_right_eq
+  zpower_zmod ~> power_mod
   mod_mult_distrib ~> mult_mod_left
   mod_mult_distrib2 ~> mult_mod_right
 
diff -r 248376f8881d -r 6a4c479ba94f src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Tue Mar 27 15:53:48 2012 +0200
+++ b/src/HOL/Divides.thy	Tue Mar 27 16:04:51 2012 +0200
@@ -283,6 +283,15 @@
     by (simp only: mod_mult_eq [symmetric])
 qed
 
+text {* Exponentiation respects modular equivalence. *}
+
+lemma power_mod: "(a mod b)^n mod b = a^n mod b"
+apply (induct n, simp_all)
+apply (rule mod_mult_right_eq [THEN trans])
+apply (simp (no_asm_simp))
+apply (rule mod_mult_eq [symmetric])
+done
+
 lemma mod_mod_cancel:
   assumes "c dvd b"
   shows "a mod b mod c = a mod c"
@@ -2179,13 +2188,6 @@
   using zmod_zdiv_equality[where a="m" and b="n"]
   by (simp add: algebra_simps) (* FIXME: generalize *)
 
-lemma zpower_zmod: "((x::int) mod m)^y mod m = x^y mod m"
-apply (induct "y", auto)
-apply (rule mod_mult_right_eq [THEN trans])
-apply (simp (no_asm_simp))
-apply (rule mod_mult_eq [symmetric])
-done (* FIXME: generalize *)
-
 lemma zdiv_int: "int (a div b) = (int a) div (int b)"
 apply (subst split_div, auto)
 apply (subst split_zdiv, auto)
@@ -2228,7 +2230,7 @@
   mod_add_right_eq [symmetric]
   mod_mult_right_eq[symmetric]
   mod_mult_left_eq [symmetric]
-  zpower_zmod
+  power_mod
   zminus_zmod zdiff_zmod_left zdiff_zmod_right
 
 text {* Distributive laws for function @{text nat}. *}
diff -r 248376f8881d -r 6a4c479ba94f src/HOL/Old_Number_Theory/WilsonRuss.thy
--- a/src/HOL/Old_Number_Theory/WilsonRuss.thy	Tue Mar 27 15:53:48 2012 +0200
+++ b/src/HOL/Old_Number_Theory/WilsonRuss.thy	Tue Mar 27 16:04:51 2012 +0200
@@ -137,7 +137,7 @@
 lemma inv_inv: "zprime p \<Longrightarrow>
     5 \<le> p \<Longrightarrow> 0 < a \<Longrightarrow> a < p ==> inv p (inv p a) = a"
   apply (unfold inv_def)
-  apply (subst zpower_zmod)
+  apply (subst power_mod)
   apply (subst zpower_zpower)
   apply (rule zcong_zless_imp_eq)
       prefer 5
diff -r 248376f8881d -r 6a4c479ba94f src/HOL/Word/Bit_Representation.thy
--- a/src/HOL/Word/Bit_Representation.thy	Tue Mar 27 15:53:48 2012 +0200
+++ b/src/HOL/Word/Bit_Representation.thy	Tue Mar 27 16:04:51 2012 +0200
@@ -625,7 +625,7 @@
   unfolding no_sbintr_alt2 by (drule sb_dec_lem') simp
 
 lemmas zmod_uminus' = zmod_uminus [where b=c] for c
-lemmas zpower_zmod' = zpower_zmod [where m=c and y=k] for c k
+lemmas zpower_zmod' = power_mod [where b=c and n=k] for c k
 
 lemmas brdmod1s' [symmetric] = 
   mod_add_left_eq mod_add_right_eq