--- a/src/HOL/Int.thy Tue Apr 28 15:50:29 2009 +0200
+++ b/src/HOL/Int.thy Tue Apr 28 15:50:29 2009 +0200
@@ -292,9 +292,7 @@
context ring_1
begin
-definition
- of_int :: "int \<Rightarrow> 'a"
-where
+definition of_int :: "int \<Rightarrow> 'a" where
[code del]: "of_int z = contents (\<Union>(i, j) \<in> Rep_Integ z. { of_nat i - of_nat j })"
lemma of_int: "of_int (Abs_Integ (intrel `` {(i,j)})) = of_nat i - of_nat j"
@@ -330,6 +328,10 @@
lemma of_int_of_nat_eq [simp]: "of_int (of_nat n) = of_nat n"
by (induct n) auto
+lemma of_int_power:
+ "of_int (z ^ n) = of_int z ^ n"
+ by (induct n) simp_all
+
end
context ordered_idom
@@ -1841,23 +1843,6 @@
qed
-subsection {* Integer Powers *}
-
-lemma of_int_power:
- "of_int (z ^ n) = of_int z ^ n"
- by (induct n) simp_all
-
-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]
-
-
subsection {* Further theorems on numerals *}
subsubsection{*Special Simplification for Constants*}
@@ -2260,4 +2245,14 @@
lemma zero_le_zpower_abs: "(0::int) \<le> abs x ^ n"
by (rule zero_le_power_abs)
+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]
+
end