# HG changeset patch
# User haftmann
# Date 1240926629 -7200
# Node ID 555f4033cd971bd4f0ba0de9194d8e3d56844ff7
# Parent  79f0858d9d4946a8d1669c663a432ff5256c1f75
reorganization of power lemmas

diff -r 79f0858d9d49 -r 555f4033cd97 src/HOL/Int.thy
--- 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