# HG changeset patch
# User haftmann
# Date 1240420161 -7200
# Node ID fec1a04b7220c440bf56f6e366d08360a79634ff
# Parent  458e55fd0a338a13b27639f9fcffbee13090d6d2
power operation defined generic

diff -r 458e55fd0a33 -r fec1a04b7220 src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Wed Apr 22 19:09:19 2009 +0200
+++ b/src/HOL/Complex.thy	Wed Apr 22 19:09:21 2009 +0200
@@ -159,19 +159,7 @@
 
 subsection {* Exponentiation *}
 
-instantiation complex :: recpower
-begin
-
-primrec power_complex where
-  "z ^ 0     = (1\<Colon>complex)"
-| "z ^ Suc n = (z\<Colon>complex) * z ^ n"
-
-instance proof
-qed simp_all
-
-declare power_complex.simps [simp del]
-
-end
+instance complex :: recpower ..
 
 
 subsection {* Numerals and Arithmetic *}
diff -r 458e55fd0a33 -r fec1a04b7220 src/HOL/Int.thy
--- 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
diff -r 458e55fd0a33 -r fec1a04b7220 src/HOL/Library/Euclidean_Space.thy
--- a/src/HOL/Library/Euclidean_Space.thy	Wed Apr 22 19:09:19 2009 +0200
+++ b/src/HOL/Library/Euclidean_Space.thy	Wed Apr 22 19:09:21 2009 +0200
@@ -253,12 +253,7 @@
   "vector_power x 0 = 1"
   | "vector_power x (Suc n) = x * vector_power x n"
 
-instantiation "^" :: (recpower,type) recpower
-begin
-  definition vec_power_def: "op ^ \<equiv> vector_power"
-  instance
-  apply (intro_classes) by (simp_all add: vec_power_def)
-end
+instance "^" :: (recpower,type) recpower ..
 
 instance "^" :: (semiring,type) semiring
   apply (intro_classes) by (vector ring_simps)+
diff -r 458e55fd0a33 -r fec1a04b7220 src/HOL/Library/Float.thy
--- a/src/HOL/Library/Float.thy	Wed Apr 22 19:09:19 2009 +0200
+++ b/src/HOL/Library/Float.thy	Wed Apr 22 19:09:21 2009 +0200
@@ -15,8 +15,8 @@
 
 datatype float = Float int int
 
-fun Ifloat :: "float \<Rightarrow> real" where
-"Ifloat (Float a b) = real a * pow2 b"
+primrec Ifloat :: "float \<Rightarrow> real" where
+  "Ifloat (Float a b) = real a * pow2 b"
 
 instantiation float :: zero begin
 definition zero_float where "0 = Float 0 0" 
@@ -33,11 +33,11 @@
 instance ..
 end
 
-fun mantissa :: "float \<Rightarrow> int" where
-"mantissa (Float a b) = a"
+primrec mantissa :: "float \<Rightarrow> int" where
+  "mantissa (Float a b) = a"
 
-fun scale :: "float \<Rightarrow> int" where
-"scale (Float a b) = b"
+primrec scale :: "float \<Rightarrow> int" where
+  "scale (Float a b) = b"
 
 lemma Ifloat_neg_exp: "e < 0 \<Longrightarrow> Ifloat (Float m e) = real m * inverse (2^nat (-e))" by auto
 lemma Ifloat_nge0_exp: "\<not> 0 \<le> e \<Longrightarrow> Ifloat (Float m e) = real m * inverse (2^nat (-e))" by auto
@@ -320,12 +320,12 @@
 end
 
 instantiation float :: uminus begin
-fun uminus_float where [simp del]: "uminus_float (Float m e) = Float (-m) e"
+primrec uminus_float where [simp del]: "uminus_float (Float m e) = Float (-m) e"
 instance ..
 end
 
 instantiation float :: minus begin
-fun minus_float where [simp del]: "(z::float) - w = z + (- w)"
+definition minus_float where [simp del]: "(z::float) - w = z + (- w)"
 instance ..
 end
 
@@ -334,11 +334,11 @@
 instance ..
 end
 
-fun float_pprt :: "float \<Rightarrow> float" where
-"float_pprt (Float a e) = (if 0 <= a then (Float a e) else 0)"
+primrec float_pprt :: "float \<Rightarrow> float" where
+  "float_pprt (Float a e) = (if 0 <= a then (Float a e) else 0)"
 
-fun float_nprt :: "float \<Rightarrow> float" where
-"float_nprt (Float a e) = (if 0 <= a then 0 else (Float a e))" 
+primrec float_nprt :: "float \<Rightarrow> float" where
+  "float_nprt (Float a e) = (if 0 <= a then 0 else (Float a e))" 
 
 instantiation float :: ord begin
 definition le_float_def: "z \<le> w \<equiv> Ifloat z \<le> Ifloat w"
@@ -354,7 +354,7 @@
   by (cases a, simp add: uminus_float.simps)
 
 lemma Ifloat_sub[simp]: "Ifloat (a - b) = Ifloat a - Ifloat b" 
-  by (cases a, cases b, simp add: minus_float.simps)
+  by (cases a, cases b, simp add: minus_float_def)
 
 lemma Ifloat_mult[simp]: "Ifloat (a*b) = Ifloat a * Ifloat b"
   by (cases a, cases b, simp add: times_float.simps pow2_add)
@@ -443,37 +443,10 @@
 lemma Ifloat_min: "Ifloat (min x y) = min (Ifloat x) (Ifloat y)" unfolding min_def le_float_def by auto
 lemma Ifloat_max: "Ifloat (max a b) = max (Ifloat a) (Ifloat b)" unfolding max_def le_float_def by auto
 
-instantiation float :: power begin 
-fun power_float where [simp del]: "(Float m e) ^ n = Float (m ^ n) (e * int n)"
-instance ..
-end
-
-instance float :: recpower
-proof (intro_classes)
-  fix a :: float show "a ^ 0 = 1" by (cases a, auto simp add: power_float.simps one_float_def)
-next
-  fix a :: float and n :: nat show "a ^ (Suc n) = a * a ^ n" 
-  by (cases a, auto simp add: power_float.simps times_float.simps algebra_simps)
-qed
+instance float :: recpower ..
 
-lemma float_power: "Ifloat (x ^ n) = (Ifloat x) ^ n"
-proof (cases x)
-  case (Float m e)
-  
-  have "pow2 e ^ n = pow2 (e * int n)"
-  proof (cases "e >= 0")
-    case True hence e_nat: "e = int (nat e)" by auto
-    hence "pow2 e ^ n = (2 ^ nat e) ^ n" using pow2_int[of "nat e"] by auto
-    thus ?thesis unfolding power_mult[symmetric] unfolding pow2_int[symmetric] int_mult e_nat[symmetric] .
-  next
-    case False hence e_minus: "-e = int (nat (-e))" by auto
-    hence "pow2 (-e) ^ n = (2 ^ nat (-e)) ^ n" using pow2_int[of "nat (-e)"] by auto
-    hence "pow2 (-e) ^ n = pow2 ((-e) * int n)" unfolding power_mult[symmetric] unfolding pow2_int[symmetric] int_mult e_minus[symmetric] zmult_zminus .
-    thus ?thesis unfolding pow2_neg[of "-e"] pow2_neg[of "-e * int n"] unfolding zmult_zminus zminus_zminus nonzero_power_inverse[OF pow2_neq_zero, symmetric]
-      using nonzero_inverse_eq_imp_eq[OF _ pow2_neq_zero pow2_neq_zero] by auto
-  qed
-  thus ?thesis by (auto simp add: Float power_mult_distrib Ifloat.simps power_float.simps)
-qed
+lemma float_power: "Ifloat (x ^ n) = Ifloat x ^ n"
+  by (induct n) simp_all
 
 lemma zero_le_pow2[simp]: "0 \<le> pow2 s"
   apply (subgoal_tac "0 < pow2 s")
@@ -1182,12 +1155,12 @@
     unfolding x_eq y_eq float_divr.simps Let_def le_float_def Ifloat_0 Ifloat_mult by (auto intro!: mult_nonneg_nonpos)
 qed
 
-fun round_down :: "nat \<Rightarrow> float \<Rightarrow> float" where
+primrec round_down :: "nat \<Rightarrow> float \<Rightarrow> float" where
 "round_down prec (Float m e) = (let d = bitlen m - int prec in
      if 0 < d then let P = 2^nat d ; n = m div P in Float n (e + d)
               else Float m e)"
 
-fun round_up :: "nat \<Rightarrow> float \<Rightarrow> float" where
+primrec round_up :: "nat \<Rightarrow> float \<Rightarrow> float" where
 "round_up prec (Float m e) = (let d = bitlen m - int prec in
   if 0 < d then let P = 2^nat d ; n = m div P ; r = m mod P in Float (n + (if r = 0 then 0 else 1)) (e + d) 
            else Float m e)"
@@ -1314,8 +1287,8 @@
   finally show ?thesis .
 qed
 
-fun float_abs :: "float \<Rightarrow> float" where
-"float_abs (Float m e) = Float \<bar>m\<bar> e"
+primrec float_abs :: "float \<Rightarrow> float" where
+  "float_abs (Float m e) = Float \<bar>m\<bar> e"
 
 instantiation float :: abs begin
 definition abs_float_def: "\<bar>x\<bar> = float_abs x"
@@ -1329,8 +1302,8 @@
   thus ?thesis unfolding Float abs_float_def float_abs.simps Ifloat.simps by auto
 qed
 
-fun floor_fl :: "float \<Rightarrow> float" where
-"floor_fl (Float m e) = (if 0 \<le> e then Float m e
+primrec floor_fl :: "float \<Rightarrow> float" where
+  "floor_fl (Float m e) = (if 0 \<le> e then Float m e
                                   else Float (m div (2 ^ (nat (-e)))) 0)"
 
 lemma floor_fl: "Ifloat (floor_fl x) \<le> Ifloat x"
@@ -1358,8 +1331,8 @@
 
 declare floor_fl.simps[simp del]
 
-fun ceiling_fl :: "float \<Rightarrow> float" where
-"ceiling_fl (Float m e) = (if 0 \<le> e then Float m e
+primrec ceiling_fl :: "float \<Rightarrow> float" where
+  "ceiling_fl (Float m e) = (if 0 \<le> e then Float m e
                                     else Float (m div (2 ^ (nat (-e))) + 1) 0)"
 
 lemma ceiling_fl: "Ifloat x \<le> Ifloat (ceiling_fl x)"
diff -r 458e55fd0a33 -r fec1a04b7220 src/HOL/Library/Formal_Power_Series.thy
--- a/src/HOL/Library/Formal_Power_Series.thy	Wed Apr 22 19:09:19 2009 +0200
+++ b/src/HOL/Library/Formal_Power_Series.thy	Wed Apr 22 19:09:21 2009 +0200
@@ -680,30 +680,14 @@
 
 subsection {* Powers*}
 
-instantiation fps :: (semiring_1) power
-begin
-
-fun fps_pow :: "nat \<Rightarrow> 'a fps \<Rightarrow> 'a fps" where
-  "fps_pow 0 f = 1"
-| "fps_pow (Suc n) f = f * fps_pow n f"
-
-definition fps_power_def: "power (f::'a fps) n = fps_pow n f"
-instance ..
-end
-
-instantiation fps :: (comm_ring_1) recpower
-begin
-instance
-  apply (intro_classes)
-  by (simp_all add: fps_power_def)
-end
+instance fps :: (semiring_1) recpower ..
 
 lemma fps_power_zeroth_eq_one: "a$0 =1 \<Longrightarrow> a^n $ 0 = (1::'a::semiring_1)"
-  by (induct n, auto simp add: fps_power_def expand_fps_eq fps_mult_nth)
+  by (induct n, auto simp add: expand_fps_eq fps_mult_nth)
 
 lemma fps_power_first_eq: "(a:: 'a::comm_ring_1 fps)$0 =1 \<Longrightarrow> a^n $ 1 = of_nat n * a$1"
 proof(induct n)
-  case 0 thus ?case by (simp add: fps_power_def)
+  case 0 thus ?case by simp
 next
   case (Suc n)
   note h = Suc.hyps[OF `a$0 = 1`]
@@ -712,13 +696,13 @@
 qed
 
 lemma startsby_one_power:"a $ 0 = (1::'a::comm_ring_1) \<Longrightarrow> a^n $ 0 = 1"
-  by (induct n, auto simp add: fps_power_def fps_mult_nth)
+  by (induct n, auto simp add: fps_mult_nth)
 
 lemma startsby_zero_power:"a $0 = (0::'a::comm_ring_1) \<Longrightarrow> n > 0 \<Longrightarrow> a^n $0 = 0"
-  by (induct n, auto simp add: fps_power_def fps_mult_nth)
+  by (induct n, auto simp add: fps_mult_nth)
 
 lemma startsby_power:"a $0 = (v::'a::{comm_ring_1, recpower}) \<Longrightarrow> a^n $0 = v^n"
-  by (induct n, auto simp add: fps_power_def fps_mult_nth power_Suc)
+  by (induct n, auto simp add: fps_mult_nth power_Suc)
 
 lemma startsby_zero_power_iff[simp]:
   "a^n $0 = (0::'a::{idom, recpower}) \<longleftrightarrow> (n \<noteq> 0 \<and> a$0 = 0)"
@@ -901,7 +885,7 @@
 
 lemma X_power_iff: "X^k = Abs_fps (\<lambda>n. if n = k then (1::'a::comm_ring_1) else 0)"
 proof(induct k)
-  case 0 thus ?case by (simp add: X_def fps_power_def fps_eq_iff)
+  case 0 thus ?case by (simp add: X_def fps_eq_iff)
 next
   case (Suc k)
   {fix m
@@ -1903,19 +1887,16 @@
   done
 
 lemma fps_compose_1[simp]: "1 oo a = 1"
-  by (simp add: fps_eq_iff fps_compose_nth fps_power_def mult_delta_left setsum_delta)
+  by (simp add: fps_eq_iff fps_compose_nth mult_delta_left setsum_delta)
 
 lemma fps_compose_0[simp]: "0 oo a = 0"
   by (simp add: fps_eq_iff fps_compose_nth)
 
-lemma fps_pow_0: "fps_pow n 0 = (if n = 0 then 1 else 0)"
-  by (induct n, simp_all)
-
 lemma fps_compose_0_right[simp]: "a oo 0 = fps_const (a$0)"
-  by (auto simp add: fps_eq_iff fps_compose_nth fps_power_def fps_pow_0 setsum_0')
+  by (auto simp add: fps_eq_iff fps_compose_nth power_0_left setsum_0')
 
 lemma fps_compose_add_distrib: "(a + b) oo c = (a oo c) + (b oo c)"
-  by (simp add: fps_eq_iff fps_compose_nth  ring_simps setsum_addf)
+  by (simp add: fps_eq_iff fps_compose_nth ring_simps setsum_addf)
 
 lemma fps_compose_setsum_distrib: "(setsum f S) oo a = setsum (\<lambda>i. f i oo a) S"
 proof-
@@ -2343,11 +2324,11 @@
 proof-
   have "fps_deriv ?lhs = 0"
     apply (simp add:  fps_deriv_power fps_sin_deriv fps_cos_deriv power_Suc)
-    by (simp add: fps_power_def ring_simps fps_const_neg[symmetric] del: fps_const_neg)
+    by (simp add: ring_simps fps_const_neg[symmetric] del: fps_const_neg)
   then have "?lhs = fps_const (?lhs $ 0)"
     unfolding fps_deriv_eq_0_iff .
   also have "\<dots> = 1"
-    by (auto simp add: fps_eq_iff fps_power_def numeral_2_eq_2 fps_mult_nth fps_cos_def fps_sin_def)
+    by (auto simp add: fps_eq_iff numeral_2_eq_2 fps_mult_nth fps_cos_def fps_sin_def)
   finally show ?thesis .
 qed
 
diff -r 458e55fd0a33 -r fec1a04b7220 src/HOL/Library/Numeral_Type.thy
--- a/src/HOL/Library/Numeral_Type.thy	Wed Apr 22 19:09:19 2009 +0200
+++ b/src/HOL/Library/Numeral_Type.thy	Wed Apr 22 19:09:21 2009 +0200
@@ -154,8 +154,8 @@
 
 locale mod_type =
   fixes n :: int
-  and Rep :: "'a::{zero,one,plus,times,uminus,minus,power} \<Rightarrow> int"
-  and Abs :: "int \<Rightarrow> 'a::{zero,one,plus,times,uminus,minus,power}"
+  and Rep :: "'a::{zero,one,plus,times,uminus,minus} \<Rightarrow> int"
+  and Abs :: "int \<Rightarrow> 'a::{zero,one,plus,times,uminus,minus}"
   assumes type: "type_definition Rep Abs {0..<n}"
   and size1: "1 < n"
   and zero_def: "0 = Abs 0"
@@ -164,14 +164,13 @@
   and mult_def: "x * y = Abs ((Rep x * Rep y) mod n)"
   and diff_def: "x - y = Abs ((Rep x - Rep y) mod n)"
   and minus_def: "- x = Abs ((- Rep x) mod n)"
-  and power_def: "x ^ k = Abs (Rep x ^ k mod n)"
 begin
 
 lemma size0: "0 < n"
 by (cut_tac size1, simp)
 
 lemmas definitions =
-  zero_def one_def add_def mult_def minus_def diff_def power_def
+  zero_def one_def add_def mult_def minus_def diff_def
 
 lemma Rep_less_n: "Rep x < n"
 by (rule type_definition.Rep [OF type, simplified, THEN conjunct2])
@@ -227,8 +226,8 @@
 
 locale mod_ring = mod_type +
   constrains n :: int
-  and Rep :: "'a::{number_ring,power} \<Rightarrow> int"
-  and Abs :: "int \<Rightarrow> 'a::{number_ring,power}"
+  and Rep :: "'a::{number_ring} \<Rightarrow> int"
+  and Abs :: "int \<Rightarrow> 'a::{number_ring}"
 begin
 
 lemma of_nat_eq: "of_nat k = Abs (int k mod n)"
@@ -272,7 +271,7 @@
   @{typ num1}, since 0 and 1 are not distinct.
 *}
 
-instantiation num1 :: "{comm_ring,comm_monoid_mult,number,recpower}"
+instantiation num1 :: "{comm_ring,comm_monoid_mult,number}"
 begin
 
 lemma num1_eq_iff: "(x::num1) = (y::num1) \<longleftrightarrow> True"
@@ -284,7 +283,7 @@
 end
 
 instantiation
-  bit0 and bit1 :: (finite) "{zero,one,plus,times,uminus,minus,power}"
+  bit0 and bit1 :: (finite) "{zero,one,plus,times,uminus,minus}"
 begin
 
 definition Abs_bit0' :: "int \<Rightarrow> 'a bit0" where
@@ -299,7 +298,6 @@
 definition "x * y = Abs_bit0' (Rep_bit0 x * Rep_bit0 y)"
 definition "x - y = Abs_bit0' (Rep_bit0 x - Rep_bit0 y)"
 definition "- x = Abs_bit0' (- Rep_bit0 x)"
-definition "x ^ k = Abs_bit0' (Rep_bit0 x ^ k)"
 
 definition "0 = Abs_bit1 0"
 definition "1 = Abs_bit1 1"
@@ -307,7 +305,6 @@
 definition "x * y = Abs_bit1' (Rep_bit1 x * Rep_bit1 y)"
 definition "x - y = Abs_bit1' (Rep_bit1 x - Rep_bit1 y)"
 definition "- x = Abs_bit1' (- Rep_bit1 x)"
-definition "x ^ k = Abs_bit1' (Rep_bit1 x ^ k)"
 
 instance ..
 
@@ -326,7 +323,6 @@
 apply (rule times_bit0_def [unfolded Abs_bit0'_def])
 apply (rule minus_bit0_def [unfolded Abs_bit0'_def])
 apply (rule uminus_bit0_def [unfolded Abs_bit0'_def])
-apply (rule power_bit0_def [unfolded Abs_bit0'_def])
 done
 
 interpretation bit1:
@@ -342,7 +338,6 @@
 apply (rule times_bit1_def [unfolded Abs_bit1'_def])
 apply (rule minus_bit1_def [unfolded Abs_bit1'_def])
 apply (rule uminus_bit1_def [unfolded Abs_bit1'_def])
-apply (rule power_bit1_def [unfolded Abs_bit1'_def])
 done
 
 instance bit0 :: (finite) "{comm_ring_1,recpower}"
@@ -386,9 +381,6 @@
 lemmas bit0_iszero_number_of [simp] = bit0.iszero_number_of
 lemmas bit1_iszero_number_of [simp] = bit1.iszero_number_of
 
-declare power_Suc [where ?'a="'a::finite bit0", standard, simp]
-declare power_Suc [where ?'a="'a::finite bit1", standard, simp]
-
 
 subsection {* Syntax *}
 
diff -r 458e55fd0a33 -r fec1a04b7220 src/HOL/Library/Polynomial.thy
--- a/src/HOL/Library/Polynomial.thy	Wed Apr 22 19:09:19 2009 +0200
+++ b/src/HOL/Library/Polynomial.thy	Wed Apr 22 19:09:21 2009 +0200
@@ -632,19 +632,7 @@
   shows "a \<noteq> 0 \<Longrightarrow> p dvd smult a q \<longleftrightarrow> p dvd q"
   by (safe elim!: dvd_smult dvd_smult_cancel)
 
-instantiation poly :: (comm_semiring_1) recpower
-begin
-
-primrec power_poly where
-  "(p::'a poly) ^ 0 = 1"
-| "(p::'a poly) ^ (Suc n) = p * p ^ n"
-
-instance
-  by default simp_all
-
-declare power_poly.simps [simp del]
-
-end
+instance poly :: (comm_semiring_1) recpower ..
 
 lemma degree_power_le: "degree (p ^ n) \<le> degree p * n"
 by (induct n, simp, auto intro: order_trans degree_mult_le)
diff -r 458e55fd0a33 -r fec1a04b7220 src/HOL/Library/Word.thy
--- a/src/HOL/Library/Word.thy	Wed Apr 22 19:09:19 2009 +0200
+++ b/src/HOL/Library/Word.thy	Wed Apr 22 19:09:21 2009 +0200
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Library/Word.thy
-    ID:         $Id$
     Author:     Sebastian Skalberg (TU Muenchen)
 *)
 
@@ -40,10 +39,8 @@
     Zero ("\<zero>")
   | One ("\<one>")
 
-primrec
-  bitval :: "bit => nat"
-where
-  "bitval \<zero> = 0"
+primrec bitval :: "bit => nat" where
+    "bitval \<zero> = 0"
   | "bitval \<one> = 1"
 
 consts
@@ -1531,7 +1528,7 @@
     show ?thesis
       apply simp
       apply (subst power_Suc [symmetric])
-      apply (simp del: power_int.simps)
+      apply simp
       done
   qed
   finally show ?thesis .
diff -r 458e55fd0a33 -r fec1a04b7220 src/HOL/Nat_Numeral.thy
--- a/src/HOL/Nat_Numeral.thy	Wed Apr 22 19:09:19 2009 +0200
+++ b/src/HOL/Nat_Numeral.thy	Wed Apr 22 19:09:21 2009 +0200
@@ -28,9 +28,12 @@
   "nat (number_of v) = number_of v"
   unfolding nat_number_of_def ..
 
+context recpower
+begin
+
 abbreviation (xsymbols)
-  power2 :: "'a::power => 'a"  ("(_\<twosuperior>)" [1000] 999) where
-  "x\<twosuperior> == x^2"
+  power2 :: "'a \<Rightarrow> 'a"  ("(_\<twosuperior>)" [1000] 999) where
+  "x\<twosuperior> \<equiv> x ^ 2"
 
 notation (latex output)
   power2  ("(_\<twosuperior>)" [1000] 999)
@@ -38,6 +41,8 @@
 notation (HTML output)
   power2  ("(_\<twosuperior>)" [1000] 999)
 
+end
+
 
 subsection {* Predicate for negative binary numbers *}
 
@@ -397,8 +402,8 @@
 by (simp add: power_even_eq) 
 
 lemma power_minus_even [simp]:
-     "(-a) ^ (2*n) = (a::'a::{comm_ring_1,recpower}) ^ (2*n)"
-by (simp add: power_minus1_even power_minus [of a]) 
+  "(-a) ^ (2*n) = (a::'a::{comm_ring_1,recpower}) ^ (2*n)"
+  by (simp add: power_minus [of a]) 
 
 lemma zero_le_even_power'[simp]:
      "0 \<le> (a::'a::{ordered_idom,recpower}) ^ (2*n)"
@@ -972,4 +977,4 @@
     Suc_mod_eq_add3_mod [of _ "number_of v", standard]
 declare Suc_mod_eq_add3_mod_number_of [simp]
 
-end
+end
\ No newline at end of file
diff -r 458e55fd0a33 -r fec1a04b7220 src/HOL/Power.thy
--- a/src/HOL/Power.thy	Wed Apr 22 19:09:19 2009 +0200
+++ b/src/HOL/Power.thy	Wed Apr 22 19:09:21 2009 +0200
@@ -1,24 +1,24 @@
 (*  Title:      HOL/Power.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1997  University of Cambridge
-
 *)
 
-header{*Exponentiation*}
+header {* Exponentiation *}
 
 theory Power
 imports Nat
 begin
 
-class power =
-  fixes power :: "'a \<Rightarrow> nat \<Rightarrow> 'a"            (infixr "^" 80)
+subsection {* Powers for Arbitrary Monoids *}
+
+class recpower = monoid_mult
+begin
 
-subsection{*Powers for Arbitrary Monoids*}
+primrec power :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infixr "^" 80) where
+    power_0: "a ^ 0 = 1"
+  | power_Suc: "a ^ Suc n = a * a ^ n"
 
-class recpower = monoid_mult + power +
-  assumes power_0 [simp]: "a ^ 0       = 1"
-  assumes power_Suc [simp]: "a ^ Suc n = a * (a ^ n)"
+end
 
 lemma power_0_Suc [simp]: "(0::'a::{recpower,semiring_0}) ^ (Suc n) = 0"
   by simp
@@ -360,24 +360,9 @@
 done
 
 
-subsection{*Exponentiation for the Natural Numbers*}
-
-instantiation nat :: recpower
-begin
-
-primrec power_nat where
-  "p ^ 0 = (1\<Colon>nat)"
-  | "p ^ (Suc n) = (p\<Colon>nat) * (p ^ n)"
+subsection {* Exponentiation for the Natural Numbers *}
 
-instance proof
-  fix z n :: nat
-  show "z^0 = 1" by simp
-  show "z^(Suc n) = z * (z^n)" by simp
-qed
-
-declare power_nat.simps [simp del]
-
-end
+instance nat :: recpower ..
 
 lemma of_nat_power:
   "of_nat (m ^ n) = (of_nat m::'a::{semiring_1,recpower}) ^ n"
@@ -391,7 +376,7 @@
 
 lemma nat_power_eq_Suc_0_iff [simp]: 
   "((x::nat)^m = Suc 0) = (m = 0 | x = Suc 0)"
-by (induct_tac m, auto)
+by (induct m, auto)
 
 lemma power_Suc_0[simp]: "(Suc 0)^n = Suc 0"
 by simp
diff -r 458e55fd0a33 -r fec1a04b7220 src/HOL/Rational.thy
--- a/src/HOL/Rational.thy	Wed Apr 22 19:09:19 2009 +0200
+++ b/src/HOL/Rational.thy	Wed Apr 22 19:09:21 2009 +0200
@@ -156,11 +156,6 @@
   then show ?thesis by (simp add: mult_rat [symmetric])
 qed
 
-primrec power_rat
-where
-  "q ^ 0 = (1\<Colon>rat)"
-| "q ^ Suc n = (q\<Colon>rat) * (q ^ n)"
-
 instance proof
   fix q r s :: rat show "(q * r) * s = q * (r * s)" 
     by (cases q, cases r, cases s) (simp add: eq_rat)
@@ -193,15 +188,8 @@
 next
   fix q :: rat show "q * 1 = q"
     by (cases q) (simp add: One_rat_def eq_rat)
-next
-  fix q :: rat
-  fix n :: nat
-  show "q ^ 0 = 1" by simp
-  show "q ^ (Suc n) = q * (q ^ n)" by simp
 qed
 
-declare power_rat.simps [simp del]
-
 end
 
 lemma of_nat_rat: "of_nat k = Fract (of_nat k) 1"
@@ -222,7 +210,8 @@
 definition
   rat_number_of_def [code del]: "number_of w = Fract w 1"
 
-instance by intro_classes (simp add: rat_number_of_def of_int_rat)
+instance proof
+qed (simp add: rat_number_of_def of_int_rat)
 
 end
 
diff -r 458e55fd0a33 -r fec1a04b7220 src/HOL/RealPow.thy
--- a/src/HOL/RealPow.thy	Wed Apr 22 19:09:19 2009 +0200
+++ b/src/HOL/RealPow.thy	Wed Apr 22 19:09:21 2009 +0200
@@ -12,24 +12,7 @@
 
 declare abs_mult_self [simp]
 
-instantiation real :: recpower
-begin
-
-primrec power_real where
-  "r ^ 0     = (1\<Colon>real)"
-| "r ^ Suc n = (r\<Colon>real) * r ^ n"
-
-instance proof
-  fix z :: real
-  fix n :: nat
-  show "z^0 = 1" by simp
-  show "z^(Suc n) = z * (z^n)" by simp
-qed
-
-declare power_real.simps [simp del]
-
-end
-
+instance real :: recpower ..
 
 lemma two_realpow_ge_one [simp]: "(1::real) \<le> 2 ^ n"
 by simp
@@ -47,7 +30,6 @@
 
 lemma realpow_minus_mult [rule_format]:
      "0 < n --> (x::real) ^ (n - 1) * x = x ^ n"
-unfolding One_nat_def
 apply (simp split add: nat_diff_split)
 done