--- a/src/HOL/Int.thy Wed Apr 22 19:09:19 2009 +0200
+++ b/src/HOL/Int.thy Wed Apr 22 19:09:21 2009 +0200
@@ -1848,42 +1848,18 @@
subsection {* Integer Powers *}
-instantiation int :: recpower
-begin
-
-primrec power_int where
- "p ^ 0 = (1\<Colon>int)"
- | "p ^ (Suc n) = (p\<Colon>int) * (p ^ n)"
-
-instance proof
- fix z :: int
- fix n :: nat
- show "z ^ 0 = 1" by simp
- show "z ^ Suc n = z * (z ^ n)" by simp
-qed
-
-declare power_int.simps [simp del]
-
-end
-
-lemma zpower_zadd_distrib: "x ^ (y + z) = ((x ^ y) * (x ^ z)::int)"
- by (rule Power.power_add)
-
-lemma zpower_zpower: "(x ^ y) ^ z = (x ^ (y * z)::int)"
- by (rule Power.power_mult [symmetric])
-
-lemma zero_less_zpower_abs_iff [simp]:
- "(0 < abs x ^ n) \<longleftrightarrow> (x \<noteq> (0::int) | n = 0)"
- by (induct n) (auto simp add: zero_less_mult_iff)
-
-lemma zero_le_zpower_abs [simp]: "(0::int) \<le> abs x ^ n"
- by (induct n) (auto simp add: zero_le_mult_iff)
+instance int :: recpower ..
lemma of_int_power:
"of_int (z ^ n) = (of_int z ^ n :: 'a::{recpower, ring_1})"
by (induct n) simp_all
-lemma int_power: "int (m^n) = (int m) ^ n"
+lemma zpower_zpower:
+ "(x ^ y) ^ z = (x ^ (y * z)::int)"
+ by (rule power_mult [symmetric])
+
+lemma int_power:
+ "int (m^n) = (int m) ^ n"
by (rule of_nat_power)
lemmas zpower_int = int_power [symmetric]
@@ -2278,4 +2254,15 @@
lemmas zless_le = less_int_def
lemmas int_eq_of_nat = TrueI
+lemma zpower_zadd_distrib:
+ "x ^ (y + z) = ((x ^ y) * (x ^ z)::int)"
+ by (rule power_add)
+
+lemma zero_less_zpower_abs_iff:
+ "(0 < abs x ^ n) \<longleftrightarrow> (x \<noteq> (0::int) | n = 0)"
+ by (rule zero_less_power_abs_iff)
+
+lemma zero_le_zpower_abs: "(0::int) \<le> abs x ^ n"
+ by (rule zero_le_power_abs)
+
end