# HG changeset patch
# User haftmann
# Date 1201269232 -3600
# Node ID ec39d7e40554a06126949adccd3f06e3c6483abb
# Parent  1f9956e0bd892e3d51489fd3855da5efadab373f
moved definition of power on ints to theory Int

diff -r 1f9956e0bd89 -r ec39d7e40554 NEWS
--- a/NEWS	Thu Jan 24 23:51:22 2008 +0100
+++ b/NEWS	Fri Jan 25 14:53:52 2008 +0100
@@ -25,6 +25,8 @@
 
 *** HOL ***
 
+* Theorems "power.simps" renamed to "power_int.simps".
+
 * New class semiring_div provides basic abstract properties of semirings
 with division and modulo operations.  Subsumes former class dvd_mod.
 
diff -r 1f9956e0bd89 -r ec39d7e40554 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Thu Jan 24 23:51:22 2008 +0100
+++ b/src/HOL/Int.thy	Fri Jan 25 14:53:52 2008 +0100
@@ -221,6 +221,7 @@
     by (cases i, cases j, cases k) (simp add: le add)
 qed
 
+
 text{*Strict Monotonicity of Multiplication*}
 
 text{*strict, in 1st argument; proof is by induction on k>0*}
@@ -261,6 +262,13 @@
     by (simp only: zsgn_def)
 qed
 
+instance int :: lordered_ring
+proof  
+  fix k :: int
+  show "abs k = sup k (- k)"
+    by (auto simp add: sup_int_def zabs_def max_def less_minus_self_iff [symmetric])
+qed
+
 lemma zless_imp_add1_zle: "w < z \<Longrightarrow> w + (1\<Colon>int) \<le> z"
 apply (cases w, cases z) 
 apply (simp add: less le add One_int_def)
@@ -1729,6 +1737,46 @@
 qed
 
 
+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
+
+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)
+
+lemma of_int_power:
+  "of_int (z ^ n) = (of_int z ^ n :: 'a::{recpower, ring_1})"
+  by (induct n) (simp_all add: power_Suc)
+
+lemma int_power: "int (m^n) = (int m) ^ n"
+  by (rule of_nat_power)
+
+lemmas zpower_int = int_power [symmetric]
+
 subsection {* Configuration of the code generator *}
 
 instance int :: eq ..
@@ -1765,7 +1813,7 @@
 
 lemma one_is_num_one [code func, code inline, symmetric, code post]:
   "(1\<Colon>int) = Numeral1" 
-  by simp 
+  by simp
 
 code_modulename SML
   Int Integer
diff -r 1f9956e0bd89 -r ec39d7e40554 src/HOL/IntDiv.thy
--- a/src/HOL/IntDiv.thy	Thu Jan 24 23:51:22 2008 +0100
+++ b/src/HOL/IntDiv.thy	Fri Jan 25 14:53:52 2008 +0100
@@ -1418,28 +1418,6 @@
   apply (auto simp add: dvd_imp_le)
   done
 
-
-subsection{*Integer Powers*} 
-
-instance int :: power ..
-
-primrec
-  "p ^ 0 = 1"
-  "p ^ (Suc n) = (p::int) * (p ^ n)"
-
-
-instance int :: recpower
-proof
-  fix z :: int
-  fix n :: nat
-  show "z^0 = 1" by simp
-  show "z^(Suc n) = z * (z^n)" by simp
-qed
-
-lemma of_int_power:
-  "of_int (z ^ n) = (of_int z ^ n :: 'a::{recpower, ring_1})"
-  by (induct n) (simp_all add: power_Suc)
-
 lemma zpower_zmod: "((x::int) mod m)^y mod m = x^y mod m"
 apply (induct "y", auto)
 apply (rule zmod_zmult1_eq [THEN trans])
@@ -1447,29 +1425,6 @@
 apply (rule zmod_zmult_distrib [symmetric])
 done
 
-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) = (x \<noteq> (0::int) | n=0)"
-apply (induct "n")
-apply (auto simp add: zero_less_mult_iff)
-done
-
-lemma zero_le_zpower_abs [simp]: "(0::int) <= (abs x)^n"
-apply (induct "n")
-apply (auto simp add: zero_le_mult_iff)
-done
-
-lemma int_power: "int (m^n) = (int m) ^ n"
-  by (rule of_nat_power)
-
-text{*Compatibility binding*}
-lemmas zpower_int = int_power [symmetric]
-
 lemma zdiv_int: "int (a div b) = (int a) div (int b)"
 apply (subst split_div, auto)
 apply (subst split_zdiv, auto)
diff -r 1f9956e0bd89 -r ec39d7e40554 src/HOL/Library/Word.thy
--- a/src/HOL/Library/Word.thy	Thu Jan 24 23:51:22 2008 +0100
+++ b/src/HOL/Library/Word.thy	Fri Jan 25 14:53:52 2008 +0100
@@ -40,11 +40,11 @@
     Zero ("\<zero>")
   | One ("\<one>")
 
-consts
+primrec
   bitval :: "bit => nat"
-primrec
+where
   "bitval \<zero> = 0"
-  "bitval \<one> = 1"
+  | "bitval \<one> = 1"
 
 consts
   bitnot :: "bit => bit"
@@ -1531,7 +1531,7 @@
     show ?thesis
       apply simp
       apply (subst power_Suc [symmetric])
-      apply (simp del: power.simps)
+      apply (simp del: power_int.simps)
       done
   qed
   finally show ?thesis .