--- a/src/HOL/Int.thy Mon Apr 27 08:22:37 2009 +0200
+++ b/src/HOL/Int.thy Mon Apr 27 10:11:44 2009 +0200
@@ -1536,7 +1536,7 @@
by (simp add: abs_if)
lemma abs_power_minus_one [simp]:
- "abs(-1 ^ n) = (1::'a::{ordered_idom,number_ring,recpower})"
+ "abs(-1 ^ n) = (1::'a::{ordered_idom,number_ring})"
by (simp add: power_abs)
lemma of_int_number_of_eq [simp]:
@@ -1848,18 +1848,21 @@
subsection {* Integer Powers *}
-instance int :: recpower ..
+context ring_1
+begin
lemma of_int_power:
- "of_int (z ^ n) = (of_int z ^ n :: 'a::{recpower, ring_1})"
+ "of_int (z ^ n) = of_int z ^ n"
by (induct n) simp_all
+end
+
lemma zpower_zpower:
"(x ^ y) ^ z = (x ^ (y * z)::int)"
by (rule power_mult [symmetric])
lemma int_power:
- "int (m^n) = (int m) ^ n"
+ "int (m ^ n) = int m ^ n"
by (rule of_nat_power)
lemmas zpower_int = int_power [symmetric]
@@ -2200,6 +2203,8 @@
subsection {* Legacy theorems *}
+instance int :: recpower ..
+
lemmas zminus_zminus = minus_minus [of "z::int", standard]
lemmas zminus_0 = minus_zero [where 'a=int]
lemmas zminus_zadd_distrib = minus_add_distrib [of "z::int" "w", standard]