|
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 |
|
|
|
18 |
Goal "#1^y = (#1::int)";
|
|
|
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 |
|