4 Copyright 2000 University of Cambridge |
4 Copyright 2000 University of Cambridge |
5 |
5 |
6 Integer powers |
6 Integer powers |
7 *) |
7 *) |
8 |
8 |
9 IntPower = IntDiv + |
9 theory IntPower = IntDiv: |
10 |
10 |
11 instance |
11 instance int :: power .. |
12 int :: {power} |
|
13 |
12 |
14 primrec |
13 primrec |
15 power_0 "p ^ 0 = 1" |
14 power_0: "p ^ 0 = 1" |
16 power_Suc "p ^ (Suc n) = (p::int) * (p ^ n)" |
15 power_Suc: "p ^ (Suc n) = (p::int) * (p ^ n)" |
|
16 |
|
17 |
|
18 lemma zpower_zmod: "((x::int) mod m)^y mod m = x^y mod m" |
|
19 apply (induct_tac "y", auto) |
|
20 apply (rule zmod_zmult1_eq [THEN trans]) |
|
21 apply (simp (no_asm_simp)) |
|
22 apply (rule zmod_zmult_distrib [symmetric]) |
|
23 done |
|
24 |
|
25 lemma zpower_1 [simp]: "1^y = (1::int)" |
|
26 by (induct_tac "y", auto) |
|
27 |
|
28 lemma zpower_zmult_distrib: "(x*z)^y = ((x^y)*(z^y)::int)" |
|
29 by (induct_tac "y", auto) |
|
30 |
|
31 lemma zpower_zadd_distrib: "x^(y+z) = ((x^y)*(x^z)::int)" |
|
32 by (induct_tac "y", auto) |
|
33 |
|
34 lemma zpower_zpower: "(x^y)^z = (x^(y*z)::int)" |
|
35 apply (induct_tac "y", auto) |
|
36 apply (subst zpower_zmult_distrib) |
|
37 apply (subst zpower_zadd_distrib) |
|
38 apply (simp (no_asm_simp)) |
|
39 done |
|
40 |
|
41 |
|
42 (*** Logical equivalences for inequalities ***) |
|
43 |
|
44 lemma zpower_eq_0_iff [simp]: "(x^n = 0) = (x = (0::int) & 0<n)" |
|
45 by (induct_tac "n", auto) |
|
46 |
|
47 lemma zero_less_zpower_abs_iff [simp]: |
|
48 "(0 < (abs x)^n) = (x \<noteq> (0::int) | n=0)" |
|
49 apply (induct_tac "n") |
|
50 apply (auto simp add: int_0_less_mult_iff) |
|
51 done |
|
52 |
|
53 lemma zero_le_zpower_abs [simp]: "(0::int) <= (abs x)^n" |
|
54 apply (induct_tac "n") |
|
55 apply (auto simp add: int_0_le_mult_iff) |
|
56 done |
|
57 |
|
58 ML |
|
59 {* |
|
60 val zpower_zmod = thm "zpower_zmod"; |
|
61 val zpower_1 = thm "zpower_1"; |
|
62 val zpower_zmult_distrib = thm "zpower_zmult_distrib"; |
|
63 val zpower_zadd_distrib = thm "zpower_zadd_distrib"; |
|
64 val zpower_zpower = thm "zpower_zpower"; |
|
65 val zpower_eq_0_iff = thm "zpower_eq_0_iff"; |
|
66 val zero_less_zpower_abs_iff = thm "zero_less_zpower_abs_iff"; |
|
67 val zero_le_zpower_abs = thm "zero_le_zpower_abs"; |
|
68 *} |
17 |
69 |
18 end |
70 end |
|
71 |