src/HOL/Divides.thy
 changeset 47164 6a4c479ba94f parent 47163 248376f8881d child 47165 9344891b504b
```     1.1 --- a/src/HOL/Divides.thy	Tue Mar 27 15:53:48 2012 +0200
1.2 +++ b/src/HOL/Divides.thy	Tue Mar 27 16:04:51 2012 +0200
1.3 @@ -283,6 +283,15 @@
1.4      by (simp only: mod_mult_eq [symmetric])
1.5  qed
1.6
1.7 +text {* Exponentiation respects modular equivalence. *}
1.8 +
1.9 +lemma power_mod: "(a mod b)^n mod b = a^n mod b"
1.10 +apply (induct n, simp_all)
1.11 +apply (rule mod_mult_right_eq [THEN trans])
1.12 +apply (simp (no_asm_simp))
1.13 +apply (rule mod_mult_eq [symmetric])
1.14 +done
1.15 +
1.16  lemma mod_mod_cancel:
1.17    assumes "c dvd b"
1.18    shows "a mod b mod c = a mod c"
1.19 @@ -2179,13 +2188,6 @@
1.20    using zmod_zdiv_equality[where a="m" and b="n"]
1.21    by (simp add: algebra_simps) (* FIXME: generalize *)
1.22
1.23 -lemma zpower_zmod: "((x::int) mod m)^y mod m = x^y mod m"
1.24 -apply (induct "y", auto)
1.25 -apply (rule mod_mult_right_eq [THEN trans])
1.26 -apply (simp (no_asm_simp))
1.27 -apply (rule mod_mult_eq [symmetric])
1.28 -done (* FIXME: generalize *)
1.29 -
1.30  lemma zdiv_int: "int (a div b) = (int a) div (int b)"
1.31  apply (subst split_div, auto)
1.32  apply (subst split_zdiv, auto)
1.33 @@ -2228,7 +2230,7 @@
1.34    mod_add_right_eq [symmetric]
1.35    mod_mult_right_eq[symmetric]
1.36    mod_mult_left_eq [symmetric]
1.37 -  zpower_zmod
1.38 +  power_mod
1.39    zminus_zmod zdiff_zmod_left zdiff_zmod_right
1.40
1.41  text {* Distributive laws for function @{text nat}. *}
```