# HG changeset patch
# User haftmann
# Date 1240926630 -7200
# Node ID 2c227493ea566caaa81a371fbd94ead78014c08e
# Parent  e1309df633c648eeefe804ff70df8cdb109d14e4
stripped class recpower further

diff -r e1309df633c6 -r 2c227493ea56 src/HOL/Deriv.thy
--- a/src/HOL/Deriv.thy	Tue Apr 28 15:50:30 2009 +0200
+++ b/src/HOL/Deriv.thy	Tue Apr 28 15:50:30 2009 +0200
@@ -1,5 +1,4 @@
 (*  Title       : Deriv.thy
-    ID          : $Id$
     Author      : Jacques D. Fleuriot
     Copyright   : 1998  University of Cambridge
     Conversion to Isar and new proofs by Lawrence C Paulson, 2004
@@ -197,7 +196,7 @@
 done
 
 lemma DERIV_power_Suc:
-  fixes f :: "'a \<Rightarrow> 'a::{real_normed_field,recpower}"
+  fixes f :: "'a \<Rightarrow> 'a::{real_normed_field}"
   assumes f: "DERIV f x :> D"
   shows "DERIV (\<lambda>x. f x ^ Suc n) x :> (1 + of_nat n) * (D * f x ^ n)"
 proof (induct n)
@@ -211,7 +210,7 @@
 qed
 
 lemma DERIV_power:
-  fixes f :: "'a \<Rightarrow> 'a::{real_normed_field,recpower}"
+  fixes f :: "'a \<Rightarrow> 'a::{real_normed_field}"
   assumes f: "DERIV f x :> D"
   shows "DERIV (\<lambda>x. f x ^ n) x :> of_nat n * (D * f x ^ (n - Suc 0))"
 by (cases "n", simp, simp add: DERIV_power_Suc f del: power_Suc)
@@ -287,20 +286,20 @@
 text{*Power of -1*}
 
 lemma DERIV_inverse:
-  fixes x :: "'a::{real_normed_field,recpower}"
+  fixes x :: "'a::{real_normed_field}"
   shows "x \<noteq> 0 ==> DERIV (%x. inverse(x)) x :> (-(inverse x ^ Suc (Suc 0)))"
 by (drule DERIV_inverse' [OF DERIV_ident]) simp
 
 text{*Derivative of inverse*}
 lemma DERIV_inverse_fun:
-  fixes x :: "'a::{real_normed_field,recpower}"
+  fixes x :: "'a::{real_normed_field}"
   shows "[| DERIV f x :> d; f(x) \<noteq> 0 |]
       ==> DERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ Suc (Suc 0))))"
 by (drule (1) DERIV_inverse') (simp add: mult_ac nonzero_inverse_mult_distrib)
 
 text{*Derivative of quotient*}
 lemma DERIV_quotient:
-  fixes x :: "'a::{real_normed_field,recpower}"
+  fixes x :: "'a::{real_normed_field}"
   shows "[| DERIV f x :> d; DERIV g x :> e; g(x) \<noteq> 0 |]
        ==> DERIV (%y. f(y) / (g y)) x :> (d*g(x) - (e*f(x))) / (g(x) ^ Suc (Suc 0))"
 by (drule (2) DERIV_divide) (simp add: mult_commute)
@@ -404,7 +403,7 @@
   unfolding divide_inverse using prems by simp
 
 lemma differentiable_power [simp]:
-  fixes f :: "'a::{recpower,real_normed_field} \<Rightarrow> 'a"
+  fixes f :: "'a::{real_normed_field} \<Rightarrow> 'a"
   assumes "f differentiable x"
   shows "(\<lambda>x. f x ^ n) differentiable x"
   by (induct n, simp, simp add: prems)
diff -r e1309df633c6 -r 2c227493ea56 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Tue Apr 28 15:50:30 2009 +0200
+++ b/src/HOL/Finite_Set.thy	Tue Apr 28 15:50:30 2009 +0200
@@ -2047,14 +2047,14 @@
 apply (auto simp add: algebra_simps)
 done
 
-lemma setprod_constant: "finite A ==> (\<Prod>x\<in> A. (y::'a::{recpower, comm_monoid_mult})) = y^(card A)"
+lemma setprod_constant: "finite A ==> (\<Prod>x\<in> A. (y::'a::{comm_monoid_mult})) = y^(card A)"
 apply (erule finite_induct)
 apply (auto simp add: power_Suc)
 done
 
 lemma setprod_gen_delta:
   assumes fS: "finite S"
-  shows "setprod (\<lambda>k. if k=a then b k else c) S = (if a \<in> S then (b a ::'a::{comm_monoid_mult, recpower}) * c^ (card S - 1) else c^ card S)"
+  shows "setprod (\<lambda>k. if k=a then b k else c) S = (if a \<in> S then (b a ::'a::{comm_monoid_mult}) * c^ (card S - 1) else c^ card S)"
 proof-
   let ?f = "(\<lambda>k. if k=a then b k else c)"
   {assume a: "a \<notin> S"
diff -r e1309df633c6 -r 2c227493ea56 src/HOL/Groebner_Basis.thy
--- a/src/HOL/Groebner_Basis.thy	Tue Apr 28 15:50:30 2009 +0200
+++ b/src/HOL/Groebner_Basis.thy	Tue Apr 28 15:50:30 2009 +0200
@@ -164,7 +164,7 @@
 end
 
 interpretation class_semiring: gb_semiring
-    "op +" "op *" "op ^" "0::'a::{comm_semiring_1, recpower}" "1"
+    "op +" "op *" "op ^" "0::'a::{comm_semiring_1}" "1"
   proof qed (auto simp add: algebra_simps power_Suc)
 
 lemmas nat_arith =
@@ -242,7 +242,7 @@
 
 
 interpretation class_ring: gb_ring "op +" "op *" "op ^"
-    "0::'a::{comm_semiring_1,recpower,number_ring}" 1 "op -" "uminus"
+    "0::'a::{comm_semiring_1,number_ring}" 1 "op -" "uminus"
   proof qed simp_all
 
 
@@ -349,9 +349,9 @@
 qed
 
 interpretation class_ringb: ringb
-  "op +" "op *" "op ^" "0::'a::{idom,recpower,number_ring}" "1" "op -" "uminus"
+  "op +" "op *" "op ^" "0::'a::{idom,number_ring}" "1" "op -" "uminus"
 proof(unfold_locales, simp add: algebra_simps power_Suc, auto)
-  fix w x y z ::"'a::{idom,recpower,number_ring}"
+  fix w x y z ::"'a::{idom,number_ring}"
   assume p: "w * y + x * z = w * z + x * y" and ynz: "y \<noteq> z"
   hence ynz': "y - z \<noteq> 0" by simp
   from p have "w * y + x* z - w*z - x*y = 0" by simp
@@ -471,7 +471,7 @@
 subsection{* Groebner Bases for fields *}
 
 interpretation class_fieldgb:
-  fieldgb "op +" "op *" "op ^" "0::'a::{field,recpower,number_ring}" "1" "op -" "uminus" "op /" "inverse" apply (unfold_locales) by (simp_all add: divide_inverse)
+  fieldgb "op +" "op *" "op ^" "0::'a::{field,number_ring}" "1" "op -" "uminus" "op /" "inverse" apply (unfold_locales) by (simp_all add: divide_inverse)
 
 lemma divide_Numeral1: "(x::'a::{field,number_ring}) / Numeral1 = x" by simp
 lemma divide_Numeral0: "(x::'a::{field,number_ring, division_by_zero}) / Numeral0 = 0"
diff -r e1309df633c6 -r 2c227493ea56 src/HOL/Lim.thy
--- a/src/HOL/Lim.thy	Tue Apr 28 15:50:30 2009 +0200
+++ b/src/HOL/Lim.thy	Tue Apr 28 15:50:30 2009 +0200
@@ -383,7 +383,7 @@
 lemmas LIM_of_real = of_real.LIM
 
 lemma LIM_power:
-  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::{recpower,real_normed_algebra}"
+  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::{power,real_normed_algebra}"
   assumes f: "f -- a --> l"
   shows "(\<lambda>x. f x ^ n) -- a --> l ^ n"
 by (induct n, simp, simp add: LIM_mult f)
@@ -530,7 +530,7 @@
   unfolding isCont_def by (rule LIM_of_real)
 
 lemma isCont_power:
-  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::{recpower,real_normed_algebra}"
+  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::{power,real_normed_algebra}"
   shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. f x ^ n) a"
   unfolding isCont_def by (rule LIM_power)
 
diff -r e1309df633c6 -r 2c227493ea56 src/HOL/NSA/HDeriv.thy
--- a/src/HOL/NSA/HDeriv.thy	Tue Apr 28 15:50:30 2009 +0200
+++ b/src/HOL/NSA/HDeriv.thy	Tue Apr 28 15:50:30 2009 +0200
@@ -1,5 +1,4 @@
 (*  Title       : Deriv.thy
-    ID          : $Id$
     Author      : Jacques D. Fleuriot
     Copyright   : 1998  University of Cambridge
     Conversion to Isar and new proofs by Lawrence C Paulson, 2004
@@ -345,7 +344,7 @@
 
 (*Can't get rid of x \<noteq> 0 because it isn't continuous at zero*)
 lemma NSDERIV_inverse:
-  fixes x :: "'a::{real_normed_field,recpower}"
+  fixes x :: "'a::{real_normed_field}"
   shows "x \<noteq> 0 ==> NSDERIV (%x. inverse(x)) x :> (- (inverse x ^ Suc (Suc 0)))"
 apply (simp add: nsderiv_def)
 apply (rule ballI, simp, clarify)
@@ -383,7 +382,7 @@
 text{*Derivative of inverse*}
 
 lemma NSDERIV_inverse_fun:
-  fixes x :: "'a::{real_normed_field,recpower}"
+  fixes x :: "'a::{real_normed_field}"
   shows "[| NSDERIV f x :> d; f(x) \<noteq> 0 |]
       ==> NSDERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ Suc (Suc 0))))"
 by (simp add: NSDERIV_DERIV_iff DERIV_inverse_fun del: power_Suc)
@@ -391,7 +390,7 @@
 text{*Derivative of quotient*}
 
 lemma NSDERIV_quotient:
-  fixes x :: "'a::{real_normed_field,recpower}"
+  fixes x :: "'a::{real_normed_field}"
   shows "[| NSDERIV f x :> d; NSDERIV g x :> e; g(x) \<noteq> 0 |]
        ==> NSDERIV (%y. f(y) / (g y)) x :> (d*g(x)
                             - (e*f(x))) / (g(x) ^ Suc (Suc 0))"
diff -r e1309df633c6 -r 2c227493ea56 src/HOL/NSA/HSEQ.thy
--- a/src/HOL/NSA/HSEQ.thy	Tue Apr 28 15:50:30 2009 +0200
+++ b/src/HOL/NSA/HSEQ.thy	Tue Apr 28 15:50:30 2009 +0200
@@ -110,7 +110,7 @@
 done
 
 lemma NSLIMSEQ_pow [rule_format]:
-  fixes a :: "'a::{real_normed_algebra,recpower}"
+  fixes a :: "'a::{real_normed_algebra,power}"
   shows "(X ----NS> a) --> ((%n. (X n) ^ m) ----NS> a ^ m)"
 apply (induct "m")
 apply (auto simp add: power_Suc intro: NSLIMSEQ_mult NSLIMSEQ_const)
diff -r e1309df633c6 -r 2c227493ea56 src/HOL/NSA/HyperDef.thy
--- a/src/HOL/NSA/HyperDef.thy	Tue Apr 28 15:50:30 2009 +0200
+++ b/src/HOL/NSA/HyperDef.thy	Tue Apr 28 15:50:30 2009 +0200
@@ -417,7 +417,7 @@
 declare power_hypreal_of_real_number_of [of _ "number_of w", standard, simp]
 (*
 lemma hrealpow_HFinite:
-  fixes x :: "'a::{real_normed_algebra,recpower} star"
+  fixes x :: "'a::{real_normed_algebra,power} star"
   shows "x \<in> HFinite ==> x ^ n \<in> HFinite"
 apply (induct_tac "n")
 apply (auto simp add: power_Suc intro: HFinite_mult)
@@ -438,24 +438,24 @@
 by (simp add: hyperpow_def starfun2_star_n)
 
 lemma hyperpow_zero [simp]:
-  "\<And>n. (0::'a::{recpower,semiring_0} star) pow (n + (1::hypnat)) = 0"
+  "\<And>n. (0::'a::{power,semiring_0} star) pow (n + (1::hypnat)) = 0"
 by transfer simp
 
 lemma hyperpow_not_zero:
-  "\<And>r n. r \<noteq> (0::'a::{recpower,field} star) ==> r pow n \<noteq> 0"
+  "\<And>r n. r \<noteq> (0::'a::{field} star) ==> r pow n \<noteq> 0"
 by transfer (rule field_power_not_zero)
 
 lemma hyperpow_inverse:
-  "\<And>r n. r \<noteq> (0::'a::{recpower,division_by_zero,field} star)
+  "\<And>r n. r \<noteq> (0::'a::{division_by_zero,field} star)
    \<Longrightarrow> inverse (r pow n) = (inverse r) pow n"
 by transfer (rule power_inverse)
-
+  
 lemma hyperpow_hrabs:
-  "\<And>r n. abs (r::'a::{recpower,ordered_idom} star) pow n = abs (r pow n)"
+  "\<And>r n. abs (r::'a::{ordered_idom} star) pow n = abs (r pow n)"
 by transfer (rule power_abs [symmetric])
 
 lemma hyperpow_add:
-  "\<And>r n m. (r::'a::recpower star) pow (n + m) = (r pow n) * (r pow m)"
+  "\<And>r n m. (r::'a::monoid_mult star) pow (n + m) = (r pow n) * (r pow m)"
 by transfer (rule power_add)
 
 lemma hyperpow_one [simp]:
@@ -463,46 +463,46 @@
 by transfer (rule power_one_right)
 
 lemma hyperpow_two:
-  "\<And>r. (r::'a::recpower star) pow ((1::hypnat) + (1::hypnat)) = r * r"
-by transfer (simp add: power_Suc)
+  "\<And>r. (r::'a::monoid_mult star) pow ((1::hypnat) + (1::hypnat)) = r * r"
+by transfer simp
 
 lemma hyperpow_gt_zero:
-  "\<And>r n. (0::'a::{recpower,ordered_semidom} star) < r \<Longrightarrow> 0 < r pow n"
+  "\<And>r n. (0::'a::{ordered_semidom} star) < r \<Longrightarrow> 0 < r pow n"
 by transfer (rule zero_less_power)
 
 lemma hyperpow_ge_zero:
-  "\<And>r n. (0::'a::{recpower,ordered_semidom} star) \<le> r \<Longrightarrow> 0 \<le> r pow n"
+  "\<And>r n. (0::'a::{ordered_semidom} star) \<le> r \<Longrightarrow> 0 \<le> r pow n"
 by transfer (rule zero_le_power)
 
 lemma hyperpow_le:
-  "\<And>x y n. \<lbrakk>(0::'a::{recpower,ordered_semidom} star) < x; x \<le> y\<rbrakk>
+  "\<And>x y n. \<lbrakk>(0::'a::{ordered_semidom} star) < x; x \<le> y\<rbrakk>
    \<Longrightarrow> x pow n \<le> y pow n"
 by transfer (rule power_mono [OF _ order_less_imp_le])
 
 lemma hyperpow_eq_one [simp]:
-  "\<And>n. 1 pow n = (1::'a::recpower star)"
+  "\<And>n. 1 pow n = (1::'a::monoid_mult star)"
 by transfer (rule power_one)
 
 lemma hrabs_hyperpow_minus_one [simp]:
-  "\<And>n. abs(-1 pow n) = (1::'a::{number_ring,recpower,ordered_idom} star)"
+  "\<And>n. abs(-1 pow n) = (1::'a::{number_ring,ordered_idom} star)"
 by transfer (rule abs_power_minus_one)
 
 lemma hyperpow_mult:
-  "\<And>r s n. (r * s::'a::{comm_monoid_mult,recpower} star) pow n
+  "\<And>r s n. (r * s::'a::{comm_monoid_mult} star) pow n
    = (r pow n) * (s pow n)"
 by transfer (rule power_mult_distrib)
 
 lemma hyperpow_two_le [simp]:
-  "(0::'a::{recpower,ordered_ring_strict} star) \<le> r pow (1 + 1)"
+  "(0::'a::{monoid_mult,ordered_ring_strict} star) \<le> r pow (1 + 1)"
 by (auto simp add: hyperpow_two zero_le_mult_iff)
 
 lemma hrabs_hyperpow_two [simp]:
   "abs(x pow (1 + 1)) =
-   (x::'a::{recpower,ordered_ring_strict} star) pow (1 + 1)"
+   (x::'a::{monoid_mult,ordered_ring_strict} star) pow (1 + 1)"
 by (simp only: abs_of_nonneg hyperpow_two_le)
 
 lemma hyperpow_two_hrabs [simp]:
-  "abs(x::'a::{recpower,ordered_idom} star) pow (1 + 1)  = x pow (1 + 1)"
+  "abs(x::'a::{ordered_idom} star) pow (1 + 1)  = x pow (1 + 1)"
 by (simp add: hyperpow_hrabs)
 
 text{*The precondition could be weakened to @{term "0\<le>x"}*}
@@ -511,11 +511,11 @@
  by (simp add: Ring_and_Field.mult_strict_mono order_less_imp_le)
 
 lemma hyperpow_two_gt_one:
-  "\<And>r::'a::{recpower,ordered_semidom} star. 1 < r \<Longrightarrow> 1 < r pow (1 + 1)"
+  "\<And>r::'a::{ordered_semidom} star. 1 < r \<Longrightarrow> 1 < r pow (1 + 1)"
 by transfer (simp add: power_gt1 del: power_Suc)
 
 lemma hyperpow_two_ge_one:
-  "\<And>r::'a::{recpower,ordered_semidom} star. 1 \<le> r \<Longrightarrow> 1 \<le> r pow (1 + 1)"
+  "\<And>r::'a::{ordered_semidom} star. 1 \<le> r \<Longrightarrow> 1 \<le> r pow (1 + 1)"
 by transfer (simp add: one_le_power del: power_Suc)
 
 lemma two_hyperpow_ge_one [simp]: "(1::hypreal) \<le> 2 pow n"
@@ -565,7 +565,7 @@
 
 lemma of_hypreal_hyperpow:
   "\<And>x n. of_hypreal (x pow n) =
-   (of_hypreal x::'a::{real_algebra_1,recpower} star) pow n"
+   (of_hypreal x::'a::{real_algebra_1} star) pow n"
 by transfer (rule of_real_power)
 
 end
diff -r e1309df633c6 -r 2c227493ea56 src/HOL/NSA/NSA.thy
--- a/src/HOL/NSA/NSA.thy	Tue Apr 28 15:50:30 2009 +0200
+++ b/src/HOL/NSA/NSA.thy	Tue Apr 28 15:50:30 2009 +0200
@@ -101,7 +101,7 @@
 by transfer (rule norm_mult)
 
 lemma hnorm_hyperpow:
-  "\<And>(x::'a::{real_normed_div_algebra,recpower} star) n.
+  "\<And>(x::'a::{real_normed_div_algebra} star) n.
    hnorm (x pow n) = hnorm x pow n"
 by transfer (rule norm_power)
 
@@ -304,15 +304,15 @@
 unfolding star_one_def by (rule HFinite_star_of)
 
 lemma hrealpow_HFinite:
-  fixes x :: "'a::{real_normed_algebra,recpower} star"
+  fixes x :: "'a::{real_normed_algebra,monoid_mult} star"
   shows "x \<in> HFinite ==> x ^ n \<in> HFinite"
-apply (induct_tac "n")
+apply (induct n)
 apply (auto simp add: power_Suc intro: HFinite_mult)
 done
 
 lemma HFinite_bounded:
   "[|(x::hypreal) \<in> HFinite; y \<le> x; 0 \<le> y |] ==> y \<in> HFinite"
-apply (case_tac "x \<le> 0")
+apply (cases "x \<le> 0")
 apply (drule_tac y = x in order_trans)
 apply (drule_tac [2] order_antisym)
 apply (auto simp add: linorder_not_le)
diff -r e1309df633c6 -r 2c227493ea56 src/HOL/NSA/NSComplex.thy
--- a/src/HOL/NSA/NSComplex.thy	Tue Apr 28 15:50:30 2009 +0200
+++ b/src/HOL/NSA/NSComplex.thy	Tue Apr 28 15:50:30 2009 +0200
@@ -383,7 +383,7 @@
 by transfer (rule power_mult_distrib)
 
 lemma hcpow_zero2 [simp]:
-  "\<And>n. 0 pow (hSuc n) = (0::'a::{recpower,semiring_0} star)"
+  "\<And>n. 0 pow (hSuc n) = (0::'a::{semiring_0} star)"
 by transfer (rule power_0_Suc)
 
 lemma hcpow_not_zero [simp,intro]:
diff -r e1309df633c6 -r 2c227493ea56 src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Tue Apr 28 15:50:30 2009 +0200
+++ b/src/HOL/Parity.thy	Tue Apr 28 15:50:30 2009 +0200
@@ -178,7 +178,7 @@
 subsection {* Parity and powers *}
 
 lemma  minus_one_even_odd_power:
-     "(even x --> (- 1::'a::{comm_ring_1,recpower})^x = 1) &
+     "(even x --> (- 1::'a::{comm_ring_1})^x = 1) &
       (odd x --> (- 1::'a)^x = - 1)"
   apply (induct x)
   apply (rule conjI)
@@ -188,37 +188,37 @@
   done
 
 lemma minus_one_even_power [simp]:
-    "even x ==> (- 1::'a::{comm_ring_1,recpower})^x = 1"
+    "even x ==> (- 1::'a::{comm_ring_1})^x = 1"
   using minus_one_even_odd_power by blast
 
 lemma minus_one_odd_power [simp]:
-    "odd x ==> (- 1::'a::{comm_ring_1,recpower})^x = - 1"
+    "odd x ==> (- 1::'a::{comm_ring_1})^x = - 1"
   using minus_one_even_odd_power by blast
 
 lemma neg_one_even_odd_power:
-     "(even x --> (-1::'a::{number_ring,recpower})^x = 1) &
+     "(even x --> (-1::'a::{number_ring})^x = 1) &
       (odd x --> (-1::'a)^x = -1)"
   apply (induct x)
   apply (simp, simp add: power_Suc)
   done
 
 lemma neg_one_even_power [simp]:
-    "even x ==> (-1::'a::{number_ring,recpower})^x = 1"
+    "even x ==> (-1::'a::{number_ring})^x = 1"
   using neg_one_even_odd_power by blast
 
 lemma neg_one_odd_power [simp]:
-    "odd x ==> (-1::'a::{number_ring,recpower})^x = -1"
+    "odd x ==> (-1::'a::{number_ring})^x = -1"
   using neg_one_even_odd_power by blast
 
 lemma neg_power_if:
-     "(-x::'a::{comm_ring_1,recpower}) ^ n =
+     "(-x::'a::{comm_ring_1}) ^ n =
       (if even n then (x ^ n) else -(x ^ n))"
   apply (induct n)
   apply (simp_all split: split_if_asm add: power_Suc)
   done
 
 lemma zero_le_even_power: "even n ==>
-    0 <= (x::'a::{recpower,ordered_ring_strict}) ^ n"
+    0 <= (x::'a::{ordered_ring_strict,monoid_mult}) ^ n"
   apply (simp add: even_nat_equiv_def2)
   apply (erule exE)
   apply (erule ssubst)
@@ -227,12 +227,12 @@
   done
 
 lemma zero_le_odd_power: "odd n ==>
-    (0 <= (x::'a::{recpower,ordered_idom}) ^ n) = (0 <= x)"
+    (0 <= (x::'a::{ordered_idom}) ^ n) = (0 <= x)"
 apply (auto simp: odd_nat_equiv_def2 power_Suc power_add zero_le_mult_iff)
 apply (metis field_power_not_zero no_zero_divirors_neq0 order_antisym_conv zero_le_square)
 done
 
-lemma zero_le_power_eq[presburger]: "(0 <= (x::'a::{recpower,ordered_idom}) ^ n) =
+lemma zero_le_power_eq[presburger]: "(0 <= (x::'a::{ordered_idom}) ^ n) =
     (even n | (odd n & 0 <= x))"
   apply auto
   apply (subst zero_le_odd_power [symmetric])
@@ -240,19 +240,19 @@
   apply (erule zero_le_even_power)
   done
 
-lemma zero_less_power_eq[presburger]: "(0 < (x::'a::{recpower,ordered_idom}) ^ n) =
+lemma zero_less_power_eq[presburger]: "(0 < (x::'a::{ordered_idom}) ^ n) =
     (n = 0 | (even n & x ~= 0) | (odd n & 0 < x))"
 
   unfolding order_less_le zero_le_power_eq by auto
 
-lemma power_less_zero_eq[presburger]: "((x::'a::{recpower,ordered_idom}) ^ n < 0) =
+lemma power_less_zero_eq[presburger]: "((x::'a::{ordered_idom}) ^ n < 0) =
     (odd n & x < 0)"
   apply (subst linorder_not_le [symmetric])+
   apply (subst zero_le_power_eq)
   apply auto
   done
 
-lemma power_le_zero_eq[presburger]: "((x::'a::{recpower,ordered_idom}) ^ n <= 0) =
+lemma power_le_zero_eq[presburger]: "((x::'a::{ordered_idom}) ^ n <= 0) =
     (n ~= 0 & ((odd n & x <= 0) | (even n & x = 0)))"
   apply (subst linorder_not_less [symmetric])+
   apply (subst zero_less_power_eq)
@@ -260,7 +260,7 @@
   done
 
 lemma power_even_abs: "even n ==>
-    (abs (x::'a::{recpower,ordered_idom}))^n = x^n"
+    (abs (x::'a::{ordered_idom}))^n = x^n"
   apply (subst power_abs [symmetric])
   apply (simp add: zero_le_even_power)
   done
@@ -269,18 +269,18 @@
   by (induct n) auto
 
 lemma power_minus_even [simp]: "even n ==>
-    (- x)^n = (x^n::'a::{recpower,comm_ring_1})"
+    (- x)^n = (x^n::'a::{comm_ring_1})"
   apply (subst power_minus)
   apply simp
   done
 
 lemma power_minus_odd [simp]: "odd n ==>
-    (- x)^n = - (x^n::'a::{recpower,comm_ring_1})"
+    (- x)^n = - (x^n::'a::{comm_ring_1})"
   apply (subst power_minus)
   apply simp
   done
 
-lemma power_mono_even: fixes x y :: "'a :: {recpower, ordered_idom}"
+lemma power_mono_even: fixes x y :: "'a :: {ordered_idom}"
   assumes "even n" and "\<bar>x\<bar> \<le> \<bar>y\<bar>"
   shows "x^n \<le> y^n"
 proof -
@@ -292,7 +292,7 @@
 
 lemma odd_pos: "odd (n::nat) \<Longrightarrow> 0 < n" by presburger
 
-lemma power_mono_odd: fixes x y :: "'a :: {recpower, ordered_idom}"
+lemma power_mono_odd: fixes x y :: "'a :: {ordered_idom}"
   assumes "odd n" and "x \<le> y"
   shows "x^n \<le> y^n"
 proof (cases "y < 0")
@@ -406,11 +406,11 @@
 subsection {* An Equivalence for @{term [source] "0 \<le> a^n"} *}
 
 lemma even_power_le_0_imp_0:
-    "a ^ (2*k) \<le> (0::'a::{ordered_idom,recpower}) ==> a=0"
+    "a ^ (2*k) \<le> (0::'a::{ordered_idom}) ==> a=0"
   by (induct k) (auto simp add: zero_le_mult_iff mult_le_0_iff power_Suc)
 
 lemma zero_le_power_iff[presburger]:
-  "(0 \<le> a^n) = (0 \<le> (a::'a::{ordered_idom,recpower}) | even n)"
+  "(0 \<le> a^n) = (0 \<le> (a::'a::{ordered_idom}) | even n)"
 proof cases
   assume even: "even n"
   then obtain k where "n = 2*k"
diff -r e1309df633c6 -r 2c227493ea56 src/HOL/Rational.thy
--- a/src/HOL/Rational.thy	Tue Apr 28 15:50:30 2009 +0200
+++ b/src/HOL/Rational.thy	Tue Apr 28 15:50:30 2009 +0200
@@ -90,7 +90,7 @@
   and "\<And>a c. Fract 0 a = Fract 0 c"
   by (simp_all add: Fract_def)
 
-instantiation rat :: "{comm_ring_1, recpower}"
+instantiation rat :: comm_ring_1
 begin
 
 definition
@@ -185,9 +185,6 @@
     by (cases q, cases r, cases s) (simp add: eq_rat algebra_simps)
 next
   show "(0::rat) \<noteq> 1" by (simp add: Zero_rat_def One_rat_def eq_rat)
-next
-  fix q :: rat show "q * 1 = q"
-    by (cases q) (simp add: One_rat_def eq_rat)
 qed
 
 end
@@ -656,7 +653,7 @@
 by (cases "b = 0") (simp_all add: nonzero_of_rat_divide)
 
 lemma of_rat_power:
-  "(of_rat (a ^ n)::'a::{field_char_0,recpower}) = of_rat a ^ n"
+  "(of_rat (a ^ n)::'a::field_char_0) = of_rat a ^ n"
 by (induct n) (simp_all add: of_rat_mult)
 
 lemma of_rat_eq_iff [simp]: "(of_rat a = of_rat b) = (a = b)"
@@ -816,7 +813,7 @@
 done
 
 lemma Rats_power [simp]:
-  fixes a :: "'a::{field_char_0,recpower}"
+  fixes a :: "'a::field_char_0"
   shows "a \<in> Rats \<Longrightarrow> a ^ n \<in> Rats"
 apply (auto simp add: Rats_def)
 apply (rule range_eqI)
@@ -837,6 +834,8 @@
   "q \<in> \<rat> \<Longrightarrow> (\<And>r. P (of_rat r)) \<Longrightarrow> P q"
   by (rule Rats_cases) auto
 
+instance rat :: recpower ..
+
 
 subsection {* Implementation of rational numbers as pairs of integers *}
 
diff -r e1309df633c6 -r 2c227493ea56 src/HOL/RealVector.thy
--- a/src/HOL/RealVector.thy	Tue Apr 28 15:50:30 2009 +0200
+++ b/src/HOL/RealVector.thy	Tue Apr 28 15:50:30 2009 +0200
@@ -259,7 +259,7 @@
 by (simp add: divide_inverse)
 
 lemma of_real_power [simp]:
-  "of_real (x ^ n) = (of_real x :: 'a::{real_algebra_1,recpower}) ^ n"
+  "of_real (x ^ n) = (of_real x :: 'a::{real_algebra_1}) ^ n"
 by (induct n) simp_all
 
 lemma of_real_eq_iff [simp]: "(of_real x = of_real y) = (x = y)"
@@ -389,7 +389,7 @@
 done
 
 lemma Reals_power [simp]:
-  fixes a :: "'a::{real_algebra_1,recpower}"
+  fixes a :: "'a::{real_algebra_1}"
   shows "a \<in> Reals \<Longrightarrow> a ^ n \<in> Reals"
 apply (auto simp add: Reals_def)
 apply (rule range_eqI)
@@ -613,7 +613,7 @@
 by (simp add: divide_inverse norm_mult norm_inverse)
 
 lemma norm_power_ineq:
-  fixes x :: "'a::{real_normed_algebra_1,recpower}"
+  fixes x :: "'a::{real_normed_algebra_1}"
   shows "norm (x ^ n) \<le> norm x ^ n"
 proof (induct n)
   case 0 show "norm (x ^ 0) \<le> norm x ^ 0" by simp
@@ -628,7 +628,7 @@
 qed
 
 lemma norm_power:
-  fixes x :: "'a::{real_normed_div_algebra,recpower}"
+  fixes x :: "'a::{real_normed_div_algebra}"
   shows "norm (x ^ n) = norm x ^ n"
 by (induct n) (simp_all add: norm_mult)
 
diff -r e1309df633c6 -r 2c227493ea56 src/HOL/SEQ.thy
--- a/src/HOL/SEQ.thy	Tue Apr 28 15:50:30 2009 +0200
+++ b/src/HOL/SEQ.thy	Tue Apr 28 15:50:30 2009 +0200
@@ -487,7 +487,7 @@
 by (simp add: LIMSEQ_mult LIMSEQ_inverse divide_inverse)
 
 lemma LIMSEQ_pow:
-  fixes a :: "'a::{real_normed_algebra,recpower}"
+  fixes a :: "'a::{power, real_normed_algebra}"
   shows "X ----> a \<Longrightarrow> (\<lambda>n. (X n) ^ m) ----> a ^ m"
 by (induct m) (simp_all add: LIMSEQ_const LIMSEQ_mult)
 
@@ -1394,7 +1394,7 @@
 qed
 
 lemma LIMSEQ_power_zero:
-  fixes x :: "'a::{real_normed_algebra_1,recpower}"
+  fixes x :: "'a::{real_normed_algebra_1}"
   shows "norm x < 1 \<Longrightarrow> (\<lambda>n. x ^ n) ----> 0"
 apply (drule LIMSEQ_realpow_zero [OF norm_ge_zero])
 apply (simp only: LIMSEQ_Zseq_iff, erule Zseq_le)
diff -r e1309df633c6 -r 2c227493ea56 src/HOL/Series.thy
--- a/src/HOL/Series.thy	Tue Apr 28 15:50:30 2009 +0200
+++ b/src/HOL/Series.thy	Tue Apr 28 15:50:30 2009 +0200
@@ -331,7 +331,7 @@
 lemmas sumr_geometric = geometric_sum [where 'a = real]
 
 lemma geometric_sums:
-  fixes x :: "'a::{real_normed_field,recpower}"
+  fixes x :: "'a::{real_normed_field}"
   shows "norm x < 1 \<Longrightarrow> (\<lambda>n. x ^ n) sums (1 / (1 - x))"
 proof -
   assume less_1: "norm x < 1"
@@ -348,7 +348,7 @@
 qed
 
 lemma summable_geometric:
-  fixes x :: "'a::{real_normed_field,recpower}"
+  fixes x :: "'a::{real_normed_field}"
   shows "norm x < 1 \<Longrightarrow> summable (\<lambda>n. x ^ n)"
 by (rule geometric_sums [THEN sums_summable])
 
@@ -434,7 +434,7 @@
 text{*Summability of geometric series for real algebras*}
 
 lemma complete_algebra_summable_geometric:
-  fixes x :: "'a::{real_normed_algebra_1,banach,recpower}"
+  fixes x :: "'a::{real_normed_algebra_1,banach}"
   shows "norm x < 1 \<Longrightarrow> summable (\<lambda>n. x ^ n)"
 proof (rule summable_comparison_test)
   show "\<exists>N. \<forall>n\<ge>N. norm (x ^ n) \<le> norm x ^ n"
diff -r e1309df633c6 -r 2c227493ea56 src/HOL/SetInterval.thy
--- a/src/HOL/SetInterval.thy	Tue Apr 28 15:50:30 2009 +0200
+++ b/src/HOL/SetInterval.thy	Tue Apr 28 15:50:30 2009 +0200
@@ -855,7 +855,7 @@
 
 lemma geometric_sum:
   "x ~= 1 ==> (\<Sum>i=0..<n. x ^ i) =
-  (x ^ n - 1) / (x - 1::'a::{field, recpower})"
+  (x ^ n - 1) / (x - 1::'a::{field})"
 by (induct "n") (simp_all add:field_simps power_Suc)
 
 subsection {* The formula for arithmetic sums *}
diff -r e1309df633c6 -r 2c227493ea56 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Tue Apr 28 15:50:30 2009 +0200
+++ b/src/HOL/Transcendental.thy	Tue Apr 28 15:50:30 2009 +0200
@@ -14,7 +14,7 @@
 subsection {* Properties of Power Series *}
 
 lemma lemma_realpow_diff:
-  fixes y :: "'a::recpower"
+  fixes y :: "'a::monoid_mult"
   shows "p \<le> n \<Longrightarrow> y ^ (Suc n - p) = (y ^ (n - p)) * y"
 proof -
   assume "p \<le> n"
@@ -23,14 +23,14 @@
 qed
 
 lemma lemma_realpow_diff_sumr:
-  fixes y :: "'a::{recpower,comm_semiring_0}" shows
+  fixes y :: "'a::{comm_semiring_0,monoid_mult}" shows
      "(\<Sum>p=0..<Suc n. (x ^ p) * y ^ (Suc n - p)) =  
       y * (\<Sum>p=0..<Suc n. (x ^ p) * y ^ (n - p))"
 by (simp add: setsum_right_distrib lemma_realpow_diff mult_ac
          del: setsum_op_ivl_Suc cong: strong_setsum_cong)
 
 lemma lemma_realpow_diff_sumr2:
-  fixes y :: "'a::{recpower,comm_ring}" shows
+  fixes y :: "'a::{comm_ring,monoid_mult}" shows
      "x ^ (Suc n) - y ^ (Suc n) =  
       (x - y) * (\<Sum>p=0..<Suc n. (x ^ p) * y ^ (n - p))"
 apply (induct n, simp)
@@ -56,7 +56,7 @@
 x}, then it sums absolutely for @{term z} with @{term "\<bar>z\<bar> < \<bar>x\<bar>"}.*}
 
 lemma powser_insidea:
-  fixes x z :: "'a::{real_normed_field,banach,recpower}"
+  fixes x z :: "'a::{real_normed_field,banach}"
   assumes 1: "summable (\<lambda>n. f n * x ^ n)"
   assumes 2: "norm z < norm x"
   shows "summable (\<lambda>n. norm (f n * z ^ n))"
@@ -108,7 +108,7 @@
 qed
 
 lemma powser_inside:
-  fixes f :: "nat \<Rightarrow> 'a::{real_normed_field,banach,recpower}" shows
+  fixes f :: "nat \<Rightarrow> 'a::{real_normed_field,banach}" shows
      "[| summable (%n. f(n) * (x ^ n)); norm z < norm x |]  
       ==> summable (%n. f(n) * (z ^ n))"
 by (rule powser_insidea [THEN summable_norm_cancel])
@@ -347,7 +347,7 @@
 done
 
 lemma lemma_termdiff1:
-  fixes z :: "'a :: {recpower,comm_ring}" shows
+  fixes z :: "'a :: {monoid_mult,comm_ring}" shows
   "(\<Sum>p=0..<m. (((z + h) ^ (m - p)) * (z ^ p)) - (z ^ m)) =  
    (\<Sum>p=0..<m. (z ^ p) * (((z + h) ^ (m - p)) - (z ^ (m - p))))"
 by(auto simp add: algebra_simps power_add [symmetric] cong: strong_setsum_cong)
@@ -357,7 +357,7 @@
 by (simp add: setsum_subtractf)
 
 lemma lemma_termdiff2:
-  fixes h :: "'a :: {recpower,field}"
+  fixes h :: "'a :: {field}"
   assumes h: "h \<noteq> 0" shows
   "((z + h) ^ n - z ^ n) / h - of_nat n * z ^ (n - Suc 0) =
    h * (\<Sum>p=0..< n - Suc 0. \<Sum>q=0..< n - Suc 0 - p.
@@ -393,7 +393,7 @@
 done
 
 lemma lemma_termdiff3:
-  fixes h z :: "'a::{real_normed_field,recpower}"
+  fixes h z :: "'a::{real_normed_field}"
   assumes 1: "h \<noteq> 0"
   assumes 2: "norm z \<le> K"
   assumes 3: "norm (z + h) \<le> K"
@@ -433,7 +433,7 @@
 qed
 
 lemma lemma_termdiff4:
-  fixes f :: "'a::{real_normed_field,recpower} \<Rightarrow>
+  fixes f :: "'a::{real_normed_field} \<Rightarrow>
               'b::real_normed_vector"
   assumes k: "0 < (k::real)"
   assumes le: "\<And>h. \<lbrakk>h \<noteq> 0; norm h < k\<rbrakk> \<Longrightarrow> norm (f h) \<le> K * norm h"
@@ -478,7 +478,7 @@
 qed
 
 lemma lemma_termdiff5:
-  fixes g :: "'a::{recpower,real_normed_field} \<Rightarrow>
+  fixes g :: "'a::{real_normed_field} \<Rightarrow>
               nat \<Rightarrow> 'b::banach"
   assumes k: "0 < (k::real)"
   assumes f: "summable f"
@@ -507,7 +507,7 @@
 text{* FIXME: Long proofs*}
 
 lemma termdiffs_aux:
-  fixes x :: "'a::{recpower,real_normed_field,banach}"
+  fixes x :: "'a::{real_normed_field,banach}"
   assumes 1: "summable (\<lambda>n. diffs (diffs c) n * K ^ n)"
   assumes 2: "norm x < norm K"
   shows "(\<lambda>h. \<Sum>n. c n * (((x + h) ^ n - x ^ n) / h
@@ -572,7 +572,7 @@
 qed
 
 lemma termdiffs:
-  fixes K x :: "'a::{recpower,real_normed_field,banach}"
+  fixes K x :: "'a::{real_normed_field,banach}"
   assumes 1: "summable (\<lambda>n. c n * K ^ n)"
   assumes 2: "summable (\<lambda>n. (diffs c) n * K ^ n)"
   assumes 3: "summable (\<lambda>n. (diffs (diffs c)) n * K ^ n)"
@@ -822,11 +822,11 @@
 subsection {* Exponential Function *}
 
 definition
-  exp :: "'a \<Rightarrow> 'a::{recpower,real_normed_field,banach}" where
+  exp :: "'a \<Rightarrow> 'a::{real_normed_field,banach}" where
   "exp x = (\<Sum>n. x ^ n /\<^sub>R real (fact n))"
 
 lemma summable_exp_generic:
-  fixes x :: "'a::{real_normed_algebra_1,recpower,banach}"
+  fixes x :: "'a::{real_normed_algebra_1,banach}"
   defines S_def: "S \<equiv> \<lambda>n. x ^ n /\<^sub>R real (fact n)"
   shows "summable S"
 proof -
@@ -856,7 +856,7 @@
 qed
 
 lemma summable_norm_exp:
-  fixes x :: "'a::{real_normed_algebra_1,recpower,banach}"
+  fixes x :: "'a::{real_normed_algebra_1,banach}"
   shows "summable (\<lambda>n. norm (x ^ n /\<^sub>R real (fact n)))"
 proof (rule summable_norm_comparison_test [OF exI, rule_format])
   show "summable (\<lambda>n. norm x ^ n /\<^sub>R real (fact n))"
@@ -901,7 +901,7 @@
 subsubsection {* Properties of the Exponential Function *}
 
 lemma powser_zero:
-  fixes f :: "nat \<Rightarrow> 'a::{real_normed_algebra_1,recpower}"
+  fixes f :: "nat \<Rightarrow> 'a::{real_normed_algebra_1}"
   shows "(\<Sum>n. f n * 0 ^ n) = f 0"
 proof -
   have "(\<Sum>n = 0..<1. f n * 0 ^ n) = (\<Sum>n. f n * 0 ^ n)"
@@ -918,7 +918,7 @@
          del: setsum_cl_ivl_Suc)
 
 lemma exp_series_add:
-  fixes x y :: "'a::{real_field,recpower}"
+  fixes x y :: "'a::{real_field}"
   defines S_def: "S \<equiv> \<lambda>x n. x ^ n /\<^sub>R real (fact n)"
   shows "S (x + y) n = (\<Sum>i=0..n. S x i * S y (n - i))"
 proof (induct n)
diff -r e1309df633c6 -r 2c227493ea56 src/HOL/Word/WordArith.thy
--- a/src/HOL/Word/WordArith.thy	Tue Apr 28 15:50:30 2009 +0200
+++ b/src/HOL/Word/WordArith.thy	Tue Apr 28 15:50:30 2009 +0200
@@ -790,15 +790,14 @@
 instance word :: (len) comm_semiring_1 
   by (intro_classes) (simp add: lenw1_zero_neq_one)
 
+instance word :: (len) recpower ..
+
 instance word :: (len) comm_ring_1 ..
 
 instance word :: (len0) comm_semiring_0 ..
 
 instance word :: (len0) order ..
 
-instance word :: (len) recpower
-  by (intro_classes) simp_all
-
 (* note that iszero_def is only for class comm_semiring_1_cancel,
    which requires word length >= 1, ie 'a :: len word *) 
 lemma zero_bintrunc: