| author | wenzelm |
| Fri, 05 Oct 2001 21:52:39 +0200 | |
| changeset 11701 | 3d51fbf81c17 |
| parent 9509 | 0f3ee1f89ca8 |
| child 11868 | 56db9f3a6b3e |
| permissions | -rw-r--r-- |
| 9509 | 1 |
(* Title: IntPower.thy |
2 |
ID: $Id$ |
|
3 |
Author: Thomas M. Rasmussen |
|
4 |
Copyright 2000 University of Cambridge |
|
5 |
||
6 |
Integer powers |
|
7 |
*) |
|
8 |
||
9 |
||
10 |
Goal "((x::int) mod m)^y mod m = x^y mod m"; |
|
11 |
by (induct_tac "y" 1); |
|
12 |
by Auto_tac; |
|
13 |
by (rtac (zmod_zmult1_eq RS trans) 1); |
|
14 |
by (Asm_simp_tac 1); |
|
15 |
by (rtac (zmod_zmult_distrib RS sym) 1); |
|
16 |
qed "zpower_zmod"; |
|
17 |
||
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
9509
diff
changeset
|
18 |
Goal "Numeral1^y = (Numeral1::int)"; |
| 9509 | 19 |
by (induct_tac "y" 1); |
20 |
by Auto_tac; |
|
21 |
qed "zpower_1"; |
|
22 |
Addsimps [zpower_1]; |
|
23 |
||
24 |
Goal "(x*z)^y = ((x^y)*(z^y)::int)"; |
|
25 |
by (induct_tac "y" 1); |
|
26 |
by Auto_tac; |
|
27 |
qed "zpower_zmult_distrib"; |
|
28 |
||
29 |
Goal "x^(y+z) = ((x^y)*(x^z)::int)"; |
|
30 |
by (induct_tac "y" 1); |
|
31 |
by Auto_tac; |
|
32 |
qed "zpower_zadd_distrib"; |
|
33 |
||
34 |
Goal "(x^y)^z = (x^(y*z)::int)"; |
|
35 |
by (induct_tac "y" 1); |
|
36 |
by Auto_tac; |
|
37 |
by (stac zpower_zmult_distrib 1); |
|
38 |
by (stac zpower_zadd_distrib 1); |
|
39 |
by (Asm_simp_tac 1); |
|
40 |
qed "zpower_zpower"; |
|
41 |