| author | kleing |
| Tue, 13 May 2003 08:59:21 +0200 | |
| changeset 14024 | 213dcc39358f |
| parent 12196 | a3be6b3a9c0b |
| 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 |
||
|
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset
|
18 |
Goal "1^y = (1::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 |
||
| 12196 | 42 |
|
43 |
(*** Logical equivalences for inequalities ***) |
|
44 |
||
45 |
Goal "(x^n = 0) = (x = (0::int) & 0<n)"; |
|
46 |
by (induct_tac "n" 1); |
|
47 |
by Auto_tac; |
|
48 |
qed "zpower_eq_0_iff"; |
|
49 |
Addsimps [zpower_eq_0_iff]; |
|
50 |
||
51 |
Goal "(0 < (abs x)^n) = (x ~= (0::int) | n=0)"; |
|
52 |
by (induct_tac "n" 1); |
|
53 |
by (auto_tac (claset(), simpset() addsimps [int_0_less_mult_iff])); |
|
54 |
qed "zero_less_zpower_abs_iff"; |
|
55 |
Addsimps [zero_less_zpower_abs_iff]; |
|
56 |
||
57 |
Goal "(0::int) <= (abs x)^n"; |
|
58 |
by (induct_tac "n" 1); |
|
59 |
by (auto_tac (claset(), simpset() addsimps [int_0_le_mult_iff])); |
|
60 |
qed "zero_le_zpower_abs"; |
|
61 |
Addsimps [zero_le_zpower_abs]; |