stripped class recpower further
authorhaftmann
Tue Apr 28 15:50:30 2009 +0200 (2009-04-28)
changeset 310172c227493ea56
parent 31016 e1309df633c6
child 31018 b8a8cf6e16f2
stripped class recpower further
src/HOL/Deriv.thy
src/HOL/Finite_Set.thy
src/HOL/Groebner_Basis.thy
src/HOL/Lim.thy
src/HOL/NSA/HDeriv.thy
src/HOL/NSA/HSEQ.thy
src/HOL/NSA/HyperDef.thy
src/HOL/NSA/NSA.thy
src/HOL/NSA/NSComplex.thy
src/HOL/Parity.thy
src/HOL/Rational.thy
src/HOL/RealVector.thy
src/HOL/SEQ.thy
src/HOL/Series.thy
src/HOL/SetInterval.thy
src/HOL/Transcendental.thy
src/HOL/Word/WordArith.thy
     1.1 --- a/src/HOL/Deriv.thy	Tue Apr 28 15:50:30 2009 +0200
     1.2 +++ b/src/HOL/Deriv.thy	Tue Apr 28 15:50:30 2009 +0200
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title       : Deriv.thy
     1.5 -    ID          : $Id$
     1.6      Author      : Jacques D. Fleuriot
     1.7      Copyright   : 1998  University of Cambridge
     1.8      Conversion to Isar and new proofs by Lawrence C Paulson, 2004
     1.9 @@ -197,7 +196,7 @@
    1.10  done
    1.11  
    1.12  lemma DERIV_power_Suc:
    1.13 -  fixes f :: "'a \<Rightarrow> 'a::{real_normed_field,recpower}"
    1.14 +  fixes f :: "'a \<Rightarrow> 'a::{real_normed_field}"
    1.15    assumes f: "DERIV f x :> D"
    1.16    shows "DERIV (\<lambda>x. f x ^ Suc n) x :> (1 + of_nat n) * (D * f x ^ n)"
    1.17  proof (induct n)
    1.18 @@ -211,7 +210,7 @@
    1.19  qed
    1.20  
    1.21  lemma DERIV_power:
    1.22 -  fixes f :: "'a \<Rightarrow> 'a::{real_normed_field,recpower}"
    1.23 +  fixes f :: "'a \<Rightarrow> 'a::{real_normed_field}"
    1.24    assumes f: "DERIV f x :> D"
    1.25    shows "DERIV (\<lambda>x. f x ^ n) x :> of_nat n * (D * f x ^ (n - Suc 0))"
    1.26  by (cases "n", simp, simp add: DERIV_power_Suc f del: power_Suc)
    1.27 @@ -287,20 +286,20 @@
    1.28  text{*Power of -1*}
    1.29  
    1.30  lemma DERIV_inverse:
    1.31 -  fixes x :: "'a::{real_normed_field,recpower}"
    1.32 +  fixes x :: "'a::{real_normed_field}"
    1.33    shows "x \<noteq> 0 ==> DERIV (%x. inverse(x)) x :> (-(inverse x ^ Suc (Suc 0)))"
    1.34  by (drule DERIV_inverse' [OF DERIV_ident]) simp
    1.35  
    1.36  text{*Derivative of inverse*}
    1.37  lemma DERIV_inverse_fun:
    1.38 -  fixes x :: "'a::{real_normed_field,recpower}"
    1.39 +  fixes x :: "'a::{real_normed_field}"
    1.40    shows "[| DERIV f x :> d; f(x) \<noteq> 0 |]
    1.41        ==> DERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ Suc (Suc 0))))"
    1.42  by (drule (1) DERIV_inverse') (simp add: mult_ac nonzero_inverse_mult_distrib)
    1.43  
    1.44  text{*Derivative of quotient*}
    1.45  lemma DERIV_quotient:
    1.46 -  fixes x :: "'a::{real_normed_field,recpower}"
    1.47 +  fixes x :: "'a::{real_normed_field}"
    1.48    shows "[| DERIV f x :> d; DERIV g x :> e; g(x) \<noteq> 0 |]
    1.49         ==> DERIV (%y. f(y) / (g y)) x :> (d*g(x) - (e*f(x))) / (g(x) ^ Suc (Suc 0))"
    1.50  by (drule (2) DERIV_divide) (simp add: mult_commute)
    1.51 @@ -404,7 +403,7 @@
    1.52    unfolding divide_inverse using prems by simp
    1.53  
    1.54  lemma differentiable_power [simp]:
    1.55 -  fixes f :: "'a::{recpower,real_normed_field} \<Rightarrow> 'a"
    1.56 +  fixes f :: "'a::{real_normed_field} \<Rightarrow> 'a"
    1.57    assumes "f differentiable x"
    1.58    shows "(\<lambda>x. f x ^ n) differentiable x"
    1.59    by (induct n, simp, simp add: prems)
     2.1 --- a/src/HOL/Finite_Set.thy	Tue Apr 28 15:50:30 2009 +0200
     2.2 +++ b/src/HOL/Finite_Set.thy	Tue Apr 28 15:50:30 2009 +0200
     2.3 @@ -2047,14 +2047,14 @@
     2.4  apply (auto simp add: algebra_simps)
     2.5  done
     2.6  
     2.7 -lemma setprod_constant: "finite A ==> (\<Prod>x\<in> A. (y::'a::{recpower, comm_monoid_mult})) = y^(card A)"
     2.8 +lemma setprod_constant: "finite A ==> (\<Prod>x\<in> A. (y::'a::{comm_monoid_mult})) = y^(card A)"
     2.9  apply (erule finite_induct)
    2.10  apply (auto simp add: power_Suc)
    2.11  done
    2.12  
    2.13  lemma setprod_gen_delta:
    2.14    assumes fS: "finite S"
    2.15 -  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)"
    2.16 +  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)"
    2.17  proof-
    2.18    let ?f = "(\<lambda>k. if k=a then b k else c)"
    2.19    {assume a: "a \<notin> S"
     3.1 --- a/src/HOL/Groebner_Basis.thy	Tue Apr 28 15:50:30 2009 +0200
     3.2 +++ b/src/HOL/Groebner_Basis.thy	Tue Apr 28 15:50:30 2009 +0200
     3.3 @@ -164,7 +164,7 @@
     3.4  end
     3.5  
     3.6  interpretation class_semiring: gb_semiring
     3.7 -    "op +" "op *" "op ^" "0::'a::{comm_semiring_1, recpower}" "1"
     3.8 +    "op +" "op *" "op ^" "0::'a::{comm_semiring_1}" "1"
     3.9    proof qed (auto simp add: algebra_simps power_Suc)
    3.10  
    3.11  lemmas nat_arith =
    3.12 @@ -242,7 +242,7 @@
    3.13  
    3.14  
    3.15  interpretation class_ring: gb_ring "op +" "op *" "op ^"
    3.16 -    "0::'a::{comm_semiring_1,recpower,number_ring}" 1 "op -" "uminus"
    3.17 +    "0::'a::{comm_semiring_1,number_ring}" 1 "op -" "uminus"
    3.18    proof qed simp_all
    3.19  
    3.20  
    3.21 @@ -349,9 +349,9 @@
    3.22  qed
    3.23  
    3.24  interpretation class_ringb: ringb
    3.25 -  "op +" "op *" "op ^" "0::'a::{idom,recpower,number_ring}" "1" "op -" "uminus"
    3.26 +  "op +" "op *" "op ^" "0::'a::{idom,number_ring}" "1" "op -" "uminus"
    3.27  proof(unfold_locales, simp add: algebra_simps power_Suc, auto)
    3.28 -  fix w x y z ::"'a::{idom,recpower,number_ring}"
    3.29 +  fix w x y z ::"'a::{idom,number_ring}"
    3.30    assume p: "w * y + x * z = w * z + x * y" and ynz: "y \<noteq> z"
    3.31    hence ynz': "y - z \<noteq> 0" by simp
    3.32    from p have "w * y + x* z - w*z - x*y = 0" by simp
    3.33 @@ -471,7 +471,7 @@
    3.34  subsection{* Groebner Bases for fields *}
    3.35  
    3.36  interpretation class_fieldgb:
    3.37 -  fieldgb "op +" "op *" "op ^" "0::'a::{field,recpower,number_ring}" "1" "op -" "uminus" "op /" "inverse" apply (unfold_locales) by (simp_all add: divide_inverse)
    3.38 +  fieldgb "op +" "op *" "op ^" "0::'a::{field,number_ring}" "1" "op -" "uminus" "op /" "inverse" apply (unfold_locales) by (simp_all add: divide_inverse)
    3.39  
    3.40  lemma divide_Numeral1: "(x::'a::{field,number_ring}) / Numeral1 = x" by simp
    3.41  lemma divide_Numeral0: "(x::'a::{field,number_ring, division_by_zero}) / Numeral0 = 0"
     4.1 --- a/src/HOL/Lim.thy	Tue Apr 28 15:50:30 2009 +0200
     4.2 +++ b/src/HOL/Lim.thy	Tue Apr 28 15:50:30 2009 +0200
     4.3 @@ -383,7 +383,7 @@
     4.4  lemmas LIM_of_real = of_real.LIM
     4.5  
     4.6  lemma LIM_power:
     4.7 -  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::{recpower,real_normed_algebra}"
     4.8 +  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::{power,real_normed_algebra}"
     4.9    assumes f: "f -- a --> l"
    4.10    shows "(\<lambda>x. f x ^ n) -- a --> l ^ n"
    4.11  by (induct n, simp, simp add: LIM_mult f)
    4.12 @@ -530,7 +530,7 @@
    4.13    unfolding isCont_def by (rule LIM_of_real)
    4.14  
    4.15  lemma isCont_power:
    4.16 -  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::{recpower,real_normed_algebra}"
    4.17 +  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::{power,real_normed_algebra}"
    4.18    shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. f x ^ n) a"
    4.19    unfolding isCont_def by (rule LIM_power)
    4.20  
     5.1 --- a/src/HOL/NSA/HDeriv.thy	Tue Apr 28 15:50:30 2009 +0200
     5.2 +++ b/src/HOL/NSA/HDeriv.thy	Tue Apr 28 15:50:30 2009 +0200
     5.3 @@ -1,5 +1,4 @@
     5.4  (*  Title       : Deriv.thy
     5.5 -    ID          : $Id$
     5.6      Author      : Jacques D. Fleuriot
     5.7      Copyright   : 1998  University of Cambridge
     5.8      Conversion to Isar and new proofs by Lawrence C Paulson, 2004
     5.9 @@ -345,7 +344,7 @@
    5.10  
    5.11  (*Can't get rid of x \<noteq> 0 because it isn't continuous at zero*)
    5.12  lemma NSDERIV_inverse:
    5.13 -  fixes x :: "'a::{real_normed_field,recpower}"
    5.14 +  fixes x :: "'a::{real_normed_field}"
    5.15    shows "x \<noteq> 0 ==> NSDERIV (%x. inverse(x)) x :> (- (inverse x ^ Suc (Suc 0)))"
    5.16  apply (simp add: nsderiv_def)
    5.17  apply (rule ballI, simp, clarify)
    5.18 @@ -383,7 +382,7 @@
    5.19  text{*Derivative of inverse*}
    5.20  
    5.21  lemma NSDERIV_inverse_fun:
    5.22 -  fixes x :: "'a::{real_normed_field,recpower}"
    5.23 +  fixes x :: "'a::{real_normed_field}"
    5.24    shows "[| NSDERIV f x :> d; f(x) \<noteq> 0 |]
    5.25        ==> NSDERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ Suc (Suc 0))))"
    5.26  by (simp add: NSDERIV_DERIV_iff DERIV_inverse_fun del: power_Suc)
    5.27 @@ -391,7 +390,7 @@
    5.28  text{*Derivative of quotient*}
    5.29  
    5.30  lemma NSDERIV_quotient:
    5.31 -  fixes x :: "'a::{real_normed_field,recpower}"
    5.32 +  fixes x :: "'a::{real_normed_field}"
    5.33    shows "[| NSDERIV f x :> d; NSDERIV g x :> e; g(x) \<noteq> 0 |]
    5.34         ==> NSDERIV (%y. f(y) / (g y)) x :> (d*g(x)
    5.35                              - (e*f(x))) / (g(x) ^ Suc (Suc 0))"
     6.1 --- a/src/HOL/NSA/HSEQ.thy	Tue Apr 28 15:50:30 2009 +0200
     6.2 +++ b/src/HOL/NSA/HSEQ.thy	Tue Apr 28 15:50:30 2009 +0200
     6.3 @@ -110,7 +110,7 @@
     6.4  done
     6.5  
     6.6  lemma NSLIMSEQ_pow [rule_format]:
     6.7 -  fixes a :: "'a::{real_normed_algebra,recpower}"
     6.8 +  fixes a :: "'a::{real_normed_algebra,power}"
     6.9    shows "(X ----NS> a) --> ((%n. (X n) ^ m) ----NS> a ^ m)"
    6.10  apply (induct "m")
    6.11  apply (auto simp add: power_Suc intro: NSLIMSEQ_mult NSLIMSEQ_const)
     7.1 --- a/src/HOL/NSA/HyperDef.thy	Tue Apr 28 15:50:30 2009 +0200
     7.2 +++ b/src/HOL/NSA/HyperDef.thy	Tue Apr 28 15:50:30 2009 +0200
     7.3 @@ -417,7 +417,7 @@
     7.4  declare power_hypreal_of_real_number_of [of _ "number_of w", standard, simp]
     7.5  (*
     7.6  lemma hrealpow_HFinite:
     7.7 -  fixes x :: "'a::{real_normed_algebra,recpower} star"
     7.8 +  fixes x :: "'a::{real_normed_algebra,power} star"
     7.9    shows "x \<in> HFinite ==> x ^ n \<in> HFinite"
    7.10  apply (induct_tac "n")
    7.11  apply (auto simp add: power_Suc intro: HFinite_mult)
    7.12 @@ -438,24 +438,24 @@
    7.13  by (simp add: hyperpow_def starfun2_star_n)
    7.14  
    7.15  lemma hyperpow_zero [simp]:
    7.16 -  "\<And>n. (0::'a::{recpower,semiring_0} star) pow (n + (1::hypnat)) = 0"
    7.17 +  "\<And>n. (0::'a::{power,semiring_0} star) pow (n + (1::hypnat)) = 0"
    7.18  by transfer simp
    7.19  
    7.20  lemma hyperpow_not_zero:
    7.21 -  "\<And>r n. r \<noteq> (0::'a::{recpower,field} star) ==> r pow n \<noteq> 0"
    7.22 +  "\<And>r n. r \<noteq> (0::'a::{field} star) ==> r pow n \<noteq> 0"
    7.23  by transfer (rule field_power_not_zero)
    7.24  
    7.25  lemma hyperpow_inverse:
    7.26 -  "\<And>r n. r \<noteq> (0::'a::{recpower,division_by_zero,field} star)
    7.27 +  "\<And>r n. r \<noteq> (0::'a::{division_by_zero,field} star)
    7.28     \<Longrightarrow> inverse (r pow n) = (inverse r) pow n"
    7.29  by transfer (rule power_inverse)
    7.30 -
    7.31 +  
    7.32  lemma hyperpow_hrabs:
    7.33 -  "\<And>r n. abs (r::'a::{recpower,ordered_idom} star) pow n = abs (r pow n)"
    7.34 +  "\<And>r n. abs (r::'a::{ordered_idom} star) pow n = abs (r pow n)"
    7.35  by transfer (rule power_abs [symmetric])
    7.36  
    7.37  lemma hyperpow_add:
    7.38 -  "\<And>r n m. (r::'a::recpower star) pow (n + m) = (r pow n) * (r pow m)"
    7.39 +  "\<And>r n m. (r::'a::monoid_mult star) pow (n + m) = (r pow n) * (r pow m)"
    7.40  by transfer (rule power_add)
    7.41  
    7.42  lemma hyperpow_one [simp]:
    7.43 @@ -463,46 +463,46 @@
    7.44  by transfer (rule power_one_right)
    7.45  
    7.46  lemma hyperpow_two:
    7.47 -  "\<And>r. (r::'a::recpower star) pow ((1::hypnat) + (1::hypnat)) = r * r"
    7.48 -by transfer (simp add: power_Suc)
    7.49 +  "\<And>r. (r::'a::monoid_mult star) pow ((1::hypnat) + (1::hypnat)) = r * r"
    7.50 +by transfer simp
    7.51  
    7.52  lemma hyperpow_gt_zero:
    7.53 -  "\<And>r n. (0::'a::{recpower,ordered_semidom} star) < r \<Longrightarrow> 0 < r pow n"
    7.54 +  "\<And>r n. (0::'a::{ordered_semidom} star) < r \<Longrightarrow> 0 < r pow n"
    7.55  by transfer (rule zero_less_power)
    7.56  
    7.57  lemma hyperpow_ge_zero:
    7.58 -  "\<And>r n. (0::'a::{recpower,ordered_semidom} star) \<le> r \<Longrightarrow> 0 \<le> r pow n"
    7.59 +  "\<And>r n. (0::'a::{ordered_semidom} star) \<le> r \<Longrightarrow> 0 \<le> r pow n"
    7.60  by transfer (rule zero_le_power)
    7.61  
    7.62  lemma hyperpow_le:
    7.63 -  "\<And>x y n. \<lbrakk>(0::'a::{recpower,ordered_semidom} star) < x; x \<le> y\<rbrakk>
    7.64 +  "\<And>x y n. \<lbrakk>(0::'a::{ordered_semidom} star) < x; x \<le> y\<rbrakk>
    7.65     \<Longrightarrow> x pow n \<le> y pow n"
    7.66  by transfer (rule power_mono [OF _ order_less_imp_le])
    7.67  
    7.68  lemma hyperpow_eq_one [simp]:
    7.69 -  "\<And>n. 1 pow n = (1::'a::recpower star)"
    7.70 +  "\<And>n. 1 pow n = (1::'a::monoid_mult star)"
    7.71  by transfer (rule power_one)
    7.72  
    7.73  lemma hrabs_hyperpow_minus_one [simp]:
    7.74 -  "\<And>n. abs(-1 pow n) = (1::'a::{number_ring,recpower,ordered_idom} star)"
    7.75 +  "\<And>n. abs(-1 pow n) = (1::'a::{number_ring,ordered_idom} star)"
    7.76  by transfer (rule abs_power_minus_one)
    7.77  
    7.78  lemma hyperpow_mult:
    7.79 -  "\<And>r s n. (r * s::'a::{comm_monoid_mult,recpower} star) pow n
    7.80 +  "\<And>r s n. (r * s::'a::{comm_monoid_mult} star) pow n
    7.81     = (r pow n) * (s pow n)"
    7.82  by transfer (rule power_mult_distrib)
    7.83  
    7.84  lemma hyperpow_two_le [simp]:
    7.85 -  "(0::'a::{recpower,ordered_ring_strict} star) \<le> r pow (1 + 1)"
    7.86 +  "(0::'a::{monoid_mult,ordered_ring_strict} star) \<le> r pow (1 + 1)"
    7.87  by (auto simp add: hyperpow_two zero_le_mult_iff)
    7.88  
    7.89  lemma hrabs_hyperpow_two [simp]:
    7.90    "abs(x pow (1 + 1)) =
    7.91 -   (x::'a::{recpower,ordered_ring_strict} star) pow (1 + 1)"
    7.92 +   (x::'a::{monoid_mult,ordered_ring_strict} star) pow (1 + 1)"
    7.93  by (simp only: abs_of_nonneg hyperpow_two_le)
    7.94  
    7.95  lemma hyperpow_two_hrabs [simp]:
    7.96 -  "abs(x::'a::{recpower,ordered_idom} star) pow (1 + 1)  = x pow (1 + 1)"
    7.97 +  "abs(x::'a::{ordered_idom} star) pow (1 + 1)  = x pow (1 + 1)"
    7.98  by (simp add: hyperpow_hrabs)
    7.99  
   7.100  text{*The precondition could be weakened to @{term "0\<le>x"}*}
   7.101 @@ -511,11 +511,11 @@
   7.102   by (simp add: Ring_and_Field.mult_strict_mono order_less_imp_le)
   7.103  
   7.104  lemma hyperpow_two_gt_one:
   7.105 -  "\<And>r::'a::{recpower,ordered_semidom} star. 1 < r \<Longrightarrow> 1 < r pow (1 + 1)"
   7.106 +  "\<And>r::'a::{ordered_semidom} star. 1 < r \<Longrightarrow> 1 < r pow (1 + 1)"
   7.107  by transfer (simp add: power_gt1 del: power_Suc)
   7.108  
   7.109  lemma hyperpow_two_ge_one:
   7.110 -  "\<And>r::'a::{recpower,ordered_semidom} star. 1 \<le> r \<Longrightarrow> 1 \<le> r pow (1 + 1)"
   7.111 +  "\<And>r::'a::{ordered_semidom} star. 1 \<le> r \<Longrightarrow> 1 \<le> r pow (1 + 1)"
   7.112  by transfer (simp add: one_le_power del: power_Suc)
   7.113  
   7.114  lemma two_hyperpow_ge_one [simp]: "(1::hypreal) \<le> 2 pow n"
   7.115 @@ -565,7 +565,7 @@
   7.116  
   7.117  lemma of_hypreal_hyperpow:
   7.118    "\<And>x n. of_hypreal (x pow n) =
   7.119 -   (of_hypreal x::'a::{real_algebra_1,recpower} star) pow n"
   7.120 +   (of_hypreal x::'a::{real_algebra_1} star) pow n"
   7.121  by transfer (rule of_real_power)
   7.122  
   7.123  end
     8.1 --- a/src/HOL/NSA/NSA.thy	Tue Apr 28 15:50:30 2009 +0200
     8.2 +++ b/src/HOL/NSA/NSA.thy	Tue Apr 28 15:50:30 2009 +0200
     8.3 @@ -101,7 +101,7 @@
     8.4  by transfer (rule norm_mult)
     8.5  
     8.6  lemma hnorm_hyperpow:
     8.7 -  "\<And>(x::'a::{real_normed_div_algebra,recpower} star) n.
     8.8 +  "\<And>(x::'a::{real_normed_div_algebra} star) n.
     8.9     hnorm (x pow n) = hnorm x pow n"
    8.10  by transfer (rule norm_power)
    8.11  
    8.12 @@ -304,15 +304,15 @@
    8.13  unfolding star_one_def by (rule HFinite_star_of)
    8.14  
    8.15  lemma hrealpow_HFinite:
    8.16 -  fixes x :: "'a::{real_normed_algebra,recpower} star"
    8.17 +  fixes x :: "'a::{real_normed_algebra,monoid_mult} star"
    8.18    shows "x \<in> HFinite ==> x ^ n \<in> HFinite"
    8.19 -apply (induct_tac "n")
    8.20 +apply (induct n)
    8.21  apply (auto simp add: power_Suc intro: HFinite_mult)
    8.22  done
    8.23  
    8.24  lemma HFinite_bounded:
    8.25    "[|(x::hypreal) \<in> HFinite; y \<le> x; 0 \<le> y |] ==> y \<in> HFinite"
    8.26 -apply (case_tac "x \<le> 0")
    8.27 +apply (cases "x \<le> 0")
    8.28  apply (drule_tac y = x in order_trans)
    8.29  apply (drule_tac [2] order_antisym)
    8.30  apply (auto simp add: linorder_not_le)
     9.1 --- a/src/HOL/NSA/NSComplex.thy	Tue Apr 28 15:50:30 2009 +0200
     9.2 +++ b/src/HOL/NSA/NSComplex.thy	Tue Apr 28 15:50:30 2009 +0200
     9.3 @@ -383,7 +383,7 @@
     9.4  by transfer (rule power_mult_distrib)
     9.5  
     9.6  lemma hcpow_zero2 [simp]:
     9.7 -  "\<And>n. 0 pow (hSuc n) = (0::'a::{recpower,semiring_0} star)"
     9.8 +  "\<And>n. 0 pow (hSuc n) = (0::'a::{semiring_0} star)"
     9.9  by transfer (rule power_0_Suc)
    9.10  
    9.11  lemma hcpow_not_zero [simp,intro]:
    10.1 --- a/src/HOL/Parity.thy	Tue Apr 28 15:50:30 2009 +0200
    10.2 +++ b/src/HOL/Parity.thy	Tue Apr 28 15:50:30 2009 +0200
    10.3 @@ -178,7 +178,7 @@
    10.4  subsection {* Parity and powers *}
    10.5  
    10.6  lemma  minus_one_even_odd_power:
    10.7 -     "(even x --> (- 1::'a::{comm_ring_1,recpower})^x = 1) &
    10.8 +     "(even x --> (- 1::'a::{comm_ring_1})^x = 1) &
    10.9        (odd x --> (- 1::'a)^x = - 1)"
   10.10    apply (induct x)
   10.11    apply (rule conjI)
   10.12 @@ -188,37 +188,37 @@
   10.13    done
   10.14  
   10.15  lemma minus_one_even_power [simp]:
   10.16 -    "even x ==> (- 1::'a::{comm_ring_1,recpower})^x = 1"
   10.17 +    "even x ==> (- 1::'a::{comm_ring_1})^x = 1"
   10.18    using minus_one_even_odd_power by blast
   10.19  
   10.20  lemma minus_one_odd_power [simp]:
   10.21 -    "odd x ==> (- 1::'a::{comm_ring_1,recpower})^x = - 1"
   10.22 +    "odd x ==> (- 1::'a::{comm_ring_1})^x = - 1"
   10.23    using minus_one_even_odd_power by blast
   10.24  
   10.25  lemma neg_one_even_odd_power:
   10.26 -     "(even x --> (-1::'a::{number_ring,recpower})^x = 1) &
   10.27 +     "(even x --> (-1::'a::{number_ring})^x = 1) &
   10.28        (odd x --> (-1::'a)^x = -1)"
   10.29    apply (induct x)
   10.30    apply (simp, simp add: power_Suc)
   10.31    done
   10.32  
   10.33  lemma neg_one_even_power [simp]:
   10.34 -    "even x ==> (-1::'a::{number_ring,recpower})^x = 1"
   10.35 +    "even x ==> (-1::'a::{number_ring})^x = 1"
   10.36    using neg_one_even_odd_power by blast
   10.37  
   10.38  lemma neg_one_odd_power [simp]:
   10.39 -    "odd x ==> (-1::'a::{number_ring,recpower})^x = -1"
   10.40 +    "odd x ==> (-1::'a::{number_ring})^x = -1"
   10.41    using neg_one_even_odd_power by blast
   10.42  
   10.43  lemma neg_power_if:
   10.44 -     "(-x::'a::{comm_ring_1,recpower}) ^ n =
   10.45 +     "(-x::'a::{comm_ring_1}) ^ n =
   10.46        (if even n then (x ^ n) else -(x ^ n))"
   10.47    apply (induct n)
   10.48    apply (simp_all split: split_if_asm add: power_Suc)
   10.49    done
   10.50  
   10.51  lemma zero_le_even_power: "even n ==>
   10.52 -    0 <= (x::'a::{recpower,ordered_ring_strict}) ^ n"
   10.53 +    0 <= (x::'a::{ordered_ring_strict,monoid_mult}) ^ n"
   10.54    apply (simp add: even_nat_equiv_def2)
   10.55    apply (erule exE)
   10.56    apply (erule ssubst)
   10.57 @@ -227,12 +227,12 @@
   10.58    done
   10.59  
   10.60  lemma zero_le_odd_power: "odd n ==>
   10.61 -    (0 <= (x::'a::{recpower,ordered_idom}) ^ n) = (0 <= x)"
   10.62 +    (0 <= (x::'a::{ordered_idom}) ^ n) = (0 <= x)"
   10.63  apply (auto simp: odd_nat_equiv_def2 power_Suc power_add zero_le_mult_iff)
   10.64  apply (metis field_power_not_zero no_zero_divirors_neq0 order_antisym_conv zero_le_square)
   10.65  done
   10.66  
   10.67 -lemma zero_le_power_eq[presburger]: "(0 <= (x::'a::{recpower,ordered_idom}) ^ n) =
   10.68 +lemma zero_le_power_eq[presburger]: "(0 <= (x::'a::{ordered_idom}) ^ n) =
   10.69      (even n | (odd n & 0 <= x))"
   10.70    apply auto
   10.71    apply (subst zero_le_odd_power [symmetric])
   10.72 @@ -240,19 +240,19 @@
   10.73    apply (erule zero_le_even_power)
   10.74    done
   10.75  
   10.76 -lemma zero_less_power_eq[presburger]: "(0 < (x::'a::{recpower,ordered_idom}) ^ n) =
   10.77 +lemma zero_less_power_eq[presburger]: "(0 < (x::'a::{ordered_idom}) ^ n) =
   10.78      (n = 0 | (even n & x ~= 0) | (odd n & 0 < x))"
   10.79  
   10.80    unfolding order_less_le zero_le_power_eq by auto
   10.81  
   10.82 -lemma power_less_zero_eq[presburger]: "((x::'a::{recpower,ordered_idom}) ^ n < 0) =
   10.83 +lemma power_less_zero_eq[presburger]: "((x::'a::{ordered_idom}) ^ n < 0) =
   10.84      (odd n & x < 0)"
   10.85    apply (subst linorder_not_le [symmetric])+
   10.86    apply (subst zero_le_power_eq)
   10.87    apply auto
   10.88    done
   10.89  
   10.90 -lemma power_le_zero_eq[presburger]: "((x::'a::{recpower,ordered_idom}) ^ n <= 0) =
   10.91 +lemma power_le_zero_eq[presburger]: "((x::'a::{ordered_idom}) ^ n <= 0) =
   10.92      (n ~= 0 & ((odd n & x <= 0) | (even n & x = 0)))"
   10.93    apply (subst linorder_not_less [symmetric])+
   10.94    apply (subst zero_less_power_eq)
   10.95 @@ -260,7 +260,7 @@
   10.96    done
   10.97  
   10.98  lemma power_even_abs: "even n ==>
   10.99 -    (abs (x::'a::{recpower,ordered_idom}))^n = x^n"
  10.100 +    (abs (x::'a::{ordered_idom}))^n = x^n"
  10.101    apply (subst power_abs [symmetric])
  10.102    apply (simp add: zero_le_even_power)
  10.103    done
  10.104 @@ -269,18 +269,18 @@
  10.105    by (induct n) auto
  10.106  
  10.107  lemma power_minus_even [simp]: "even n ==>
  10.108 -    (- x)^n = (x^n::'a::{recpower,comm_ring_1})"
  10.109 +    (- x)^n = (x^n::'a::{comm_ring_1})"
  10.110    apply (subst power_minus)
  10.111    apply simp
  10.112    done
  10.113  
  10.114  lemma power_minus_odd [simp]: "odd n ==>
  10.115 -    (- x)^n = - (x^n::'a::{recpower,comm_ring_1})"
  10.116 +    (- x)^n = - (x^n::'a::{comm_ring_1})"
  10.117    apply (subst power_minus)
  10.118    apply simp
  10.119    done
  10.120  
  10.121 -lemma power_mono_even: fixes x y :: "'a :: {recpower, ordered_idom}"
  10.122 +lemma power_mono_even: fixes x y :: "'a :: {ordered_idom}"
  10.123    assumes "even n" and "\<bar>x\<bar> \<le> \<bar>y\<bar>"
  10.124    shows "x^n \<le> y^n"
  10.125  proof -
  10.126 @@ -292,7 +292,7 @@
  10.127  
  10.128  lemma odd_pos: "odd (n::nat) \<Longrightarrow> 0 < n" by presburger
  10.129  
  10.130 -lemma power_mono_odd: fixes x y :: "'a :: {recpower, ordered_idom}"
  10.131 +lemma power_mono_odd: fixes x y :: "'a :: {ordered_idom}"
  10.132    assumes "odd n" and "x \<le> y"
  10.133    shows "x^n \<le> y^n"
  10.134  proof (cases "y < 0")
  10.135 @@ -406,11 +406,11 @@
  10.136  subsection {* An Equivalence for @{term [source] "0 \<le> a^n"} *}
  10.137  
  10.138  lemma even_power_le_0_imp_0:
  10.139 -    "a ^ (2*k) \<le> (0::'a::{ordered_idom,recpower}) ==> a=0"
  10.140 +    "a ^ (2*k) \<le> (0::'a::{ordered_idom}) ==> a=0"
  10.141    by (induct k) (auto simp add: zero_le_mult_iff mult_le_0_iff power_Suc)
  10.142  
  10.143  lemma zero_le_power_iff[presburger]:
  10.144 -  "(0 \<le> a^n) = (0 \<le> (a::'a::{ordered_idom,recpower}) | even n)"
  10.145 +  "(0 \<le> a^n) = (0 \<le> (a::'a::{ordered_idom}) | even n)"
  10.146  proof cases
  10.147    assume even: "even n"
  10.148    then obtain k where "n = 2*k"
    11.1 --- a/src/HOL/Rational.thy	Tue Apr 28 15:50:30 2009 +0200
    11.2 +++ b/src/HOL/Rational.thy	Tue Apr 28 15:50:30 2009 +0200
    11.3 @@ -90,7 +90,7 @@
    11.4    and "\<And>a c. Fract 0 a = Fract 0 c"
    11.5    by (simp_all add: Fract_def)
    11.6  
    11.7 -instantiation rat :: "{comm_ring_1, recpower}"
    11.8 +instantiation rat :: comm_ring_1
    11.9  begin
   11.10  
   11.11  definition
   11.12 @@ -185,9 +185,6 @@
   11.13      by (cases q, cases r, cases s) (simp add: eq_rat algebra_simps)
   11.14  next
   11.15    show "(0::rat) \<noteq> 1" by (simp add: Zero_rat_def One_rat_def eq_rat)
   11.16 -next
   11.17 -  fix q :: rat show "q * 1 = q"
   11.18 -    by (cases q) (simp add: One_rat_def eq_rat)
   11.19  qed
   11.20  
   11.21  end
   11.22 @@ -656,7 +653,7 @@
   11.23  by (cases "b = 0") (simp_all add: nonzero_of_rat_divide)
   11.24  
   11.25  lemma of_rat_power:
   11.26 -  "(of_rat (a ^ n)::'a::{field_char_0,recpower}) = of_rat a ^ n"
   11.27 +  "(of_rat (a ^ n)::'a::field_char_0) = of_rat a ^ n"
   11.28  by (induct n) (simp_all add: of_rat_mult)
   11.29  
   11.30  lemma of_rat_eq_iff [simp]: "(of_rat a = of_rat b) = (a = b)"
   11.31 @@ -816,7 +813,7 @@
   11.32  done
   11.33  
   11.34  lemma Rats_power [simp]:
   11.35 -  fixes a :: "'a::{field_char_0,recpower}"
   11.36 +  fixes a :: "'a::field_char_0"
   11.37    shows "a \<in> Rats \<Longrightarrow> a ^ n \<in> Rats"
   11.38  apply (auto simp add: Rats_def)
   11.39  apply (rule range_eqI)
   11.40 @@ -837,6 +834,8 @@
   11.41    "q \<in> \<rat> \<Longrightarrow> (\<And>r. P (of_rat r)) \<Longrightarrow> P q"
   11.42    by (rule Rats_cases) auto
   11.43  
   11.44 +instance rat :: recpower ..
   11.45 +
   11.46  
   11.47  subsection {* Implementation of rational numbers as pairs of integers *}
   11.48  
    12.1 --- a/src/HOL/RealVector.thy	Tue Apr 28 15:50:30 2009 +0200
    12.2 +++ b/src/HOL/RealVector.thy	Tue Apr 28 15:50:30 2009 +0200
    12.3 @@ -259,7 +259,7 @@
    12.4  by (simp add: divide_inverse)
    12.5  
    12.6  lemma of_real_power [simp]:
    12.7 -  "of_real (x ^ n) = (of_real x :: 'a::{real_algebra_1,recpower}) ^ n"
    12.8 +  "of_real (x ^ n) = (of_real x :: 'a::{real_algebra_1}) ^ n"
    12.9  by (induct n) simp_all
   12.10  
   12.11  lemma of_real_eq_iff [simp]: "(of_real x = of_real y) = (x = y)"
   12.12 @@ -389,7 +389,7 @@
   12.13  done
   12.14  
   12.15  lemma Reals_power [simp]:
   12.16 -  fixes a :: "'a::{real_algebra_1,recpower}"
   12.17 +  fixes a :: "'a::{real_algebra_1}"
   12.18    shows "a \<in> Reals \<Longrightarrow> a ^ n \<in> Reals"
   12.19  apply (auto simp add: Reals_def)
   12.20  apply (rule range_eqI)
   12.21 @@ -613,7 +613,7 @@
   12.22  by (simp add: divide_inverse norm_mult norm_inverse)
   12.23  
   12.24  lemma norm_power_ineq:
   12.25 -  fixes x :: "'a::{real_normed_algebra_1,recpower}"
   12.26 +  fixes x :: "'a::{real_normed_algebra_1}"
   12.27    shows "norm (x ^ n) \<le> norm x ^ n"
   12.28  proof (induct n)
   12.29    case 0 show "norm (x ^ 0) \<le> norm x ^ 0" by simp
   12.30 @@ -628,7 +628,7 @@
   12.31  qed
   12.32  
   12.33  lemma norm_power:
   12.34 -  fixes x :: "'a::{real_normed_div_algebra,recpower}"
   12.35 +  fixes x :: "'a::{real_normed_div_algebra}"
   12.36    shows "norm (x ^ n) = norm x ^ n"
   12.37  by (induct n) (simp_all add: norm_mult)
   12.38  
    13.1 --- a/src/HOL/SEQ.thy	Tue Apr 28 15:50:30 2009 +0200
    13.2 +++ b/src/HOL/SEQ.thy	Tue Apr 28 15:50:30 2009 +0200
    13.3 @@ -487,7 +487,7 @@
    13.4  by (simp add: LIMSEQ_mult LIMSEQ_inverse divide_inverse)
    13.5  
    13.6  lemma LIMSEQ_pow:
    13.7 -  fixes a :: "'a::{real_normed_algebra,recpower}"
    13.8 +  fixes a :: "'a::{power, real_normed_algebra}"
    13.9    shows "X ----> a \<Longrightarrow> (\<lambda>n. (X n) ^ m) ----> a ^ m"
   13.10  by (induct m) (simp_all add: LIMSEQ_const LIMSEQ_mult)
   13.11  
   13.12 @@ -1394,7 +1394,7 @@
   13.13  qed
   13.14  
   13.15  lemma LIMSEQ_power_zero:
   13.16 -  fixes x :: "'a::{real_normed_algebra_1,recpower}"
   13.17 +  fixes x :: "'a::{real_normed_algebra_1}"
   13.18    shows "norm x < 1 \<Longrightarrow> (\<lambda>n. x ^ n) ----> 0"
   13.19  apply (drule LIMSEQ_realpow_zero [OF norm_ge_zero])
   13.20  apply (simp only: LIMSEQ_Zseq_iff, erule Zseq_le)
    14.1 --- a/src/HOL/Series.thy	Tue Apr 28 15:50:30 2009 +0200
    14.2 +++ b/src/HOL/Series.thy	Tue Apr 28 15:50:30 2009 +0200
    14.3 @@ -331,7 +331,7 @@
    14.4  lemmas sumr_geometric = geometric_sum [where 'a = real]
    14.5  
    14.6  lemma geometric_sums:
    14.7 -  fixes x :: "'a::{real_normed_field,recpower}"
    14.8 +  fixes x :: "'a::{real_normed_field}"
    14.9    shows "norm x < 1 \<Longrightarrow> (\<lambda>n. x ^ n) sums (1 / (1 - x))"
   14.10  proof -
   14.11    assume less_1: "norm x < 1"
   14.12 @@ -348,7 +348,7 @@
   14.13  qed
   14.14  
   14.15  lemma summable_geometric:
   14.16 -  fixes x :: "'a::{real_normed_field,recpower}"
   14.17 +  fixes x :: "'a::{real_normed_field}"
   14.18    shows "norm x < 1 \<Longrightarrow> summable (\<lambda>n. x ^ n)"
   14.19  by (rule geometric_sums [THEN sums_summable])
   14.20  
   14.21 @@ -434,7 +434,7 @@
   14.22  text{*Summability of geometric series for real algebras*}
   14.23  
   14.24  lemma complete_algebra_summable_geometric:
   14.25 -  fixes x :: "'a::{real_normed_algebra_1,banach,recpower}"
   14.26 +  fixes x :: "'a::{real_normed_algebra_1,banach}"
   14.27    shows "norm x < 1 \<Longrightarrow> summable (\<lambda>n. x ^ n)"
   14.28  proof (rule summable_comparison_test)
   14.29    show "\<exists>N. \<forall>n\<ge>N. norm (x ^ n) \<le> norm x ^ n"
    15.1 --- a/src/HOL/SetInterval.thy	Tue Apr 28 15:50:30 2009 +0200
    15.2 +++ b/src/HOL/SetInterval.thy	Tue Apr 28 15:50:30 2009 +0200
    15.3 @@ -855,7 +855,7 @@
    15.4  
    15.5  lemma geometric_sum:
    15.6    "x ~= 1 ==> (\<Sum>i=0..<n. x ^ i) =
    15.7 -  (x ^ n - 1) / (x - 1::'a::{field, recpower})"
    15.8 +  (x ^ n - 1) / (x - 1::'a::{field})"
    15.9  by (induct "n") (simp_all add:field_simps power_Suc)
   15.10  
   15.11  subsection {* The formula for arithmetic sums *}
    16.1 --- a/src/HOL/Transcendental.thy	Tue Apr 28 15:50:30 2009 +0200
    16.2 +++ b/src/HOL/Transcendental.thy	Tue Apr 28 15:50:30 2009 +0200
    16.3 @@ -14,7 +14,7 @@
    16.4  subsection {* Properties of Power Series *}
    16.5  
    16.6  lemma lemma_realpow_diff:
    16.7 -  fixes y :: "'a::recpower"
    16.8 +  fixes y :: "'a::monoid_mult"
    16.9    shows "p \<le> n \<Longrightarrow> y ^ (Suc n - p) = (y ^ (n - p)) * y"
   16.10  proof -
   16.11    assume "p \<le> n"
   16.12 @@ -23,14 +23,14 @@
   16.13  qed
   16.14  
   16.15  lemma lemma_realpow_diff_sumr:
   16.16 -  fixes y :: "'a::{recpower,comm_semiring_0}" shows
   16.17 +  fixes y :: "'a::{comm_semiring_0,monoid_mult}" shows
   16.18       "(\<Sum>p=0..<Suc n. (x ^ p) * y ^ (Suc n - p)) =  
   16.19        y * (\<Sum>p=0..<Suc n. (x ^ p) * y ^ (n - p))"
   16.20  by (simp add: setsum_right_distrib lemma_realpow_diff mult_ac
   16.21           del: setsum_op_ivl_Suc cong: strong_setsum_cong)
   16.22  
   16.23  lemma lemma_realpow_diff_sumr2:
   16.24 -  fixes y :: "'a::{recpower,comm_ring}" shows
   16.25 +  fixes y :: "'a::{comm_ring,monoid_mult}" shows
   16.26       "x ^ (Suc n) - y ^ (Suc n) =  
   16.27        (x - y) * (\<Sum>p=0..<Suc n. (x ^ p) * y ^ (n - p))"
   16.28  apply (induct n, simp)
   16.29 @@ -56,7 +56,7 @@
   16.30  x}, then it sums absolutely for @{term z} with @{term "\<bar>z\<bar> < \<bar>x\<bar>"}.*}
   16.31  
   16.32  lemma powser_insidea:
   16.33 -  fixes x z :: "'a::{real_normed_field,banach,recpower}"
   16.34 +  fixes x z :: "'a::{real_normed_field,banach}"
   16.35    assumes 1: "summable (\<lambda>n. f n * x ^ n)"
   16.36    assumes 2: "norm z < norm x"
   16.37    shows "summable (\<lambda>n. norm (f n * z ^ n))"
   16.38 @@ -108,7 +108,7 @@
   16.39  qed
   16.40  
   16.41  lemma powser_inside:
   16.42 -  fixes f :: "nat \<Rightarrow> 'a::{real_normed_field,banach,recpower}" shows
   16.43 +  fixes f :: "nat \<Rightarrow> 'a::{real_normed_field,banach}" shows
   16.44       "[| summable (%n. f(n) * (x ^ n)); norm z < norm x |]  
   16.45        ==> summable (%n. f(n) * (z ^ n))"
   16.46  by (rule powser_insidea [THEN summable_norm_cancel])
   16.47 @@ -347,7 +347,7 @@
   16.48  done
   16.49  
   16.50  lemma lemma_termdiff1:
   16.51 -  fixes z :: "'a :: {recpower,comm_ring}" shows
   16.52 +  fixes z :: "'a :: {monoid_mult,comm_ring}" shows
   16.53    "(\<Sum>p=0..<m. (((z + h) ^ (m - p)) * (z ^ p)) - (z ^ m)) =  
   16.54     (\<Sum>p=0..<m. (z ^ p) * (((z + h) ^ (m - p)) - (z ^ (m - p))))"
   16.55  by(auto simp add: algebra_simps power_add [symmetric] cong: strong_setsum_cong)
   16.56 @@ -357,7 +357,7 @@
   16.57  by (simp add: setsum_subtractf)
   16.58  
   16.59  lemma lemma_termdiff2:
   16.60 -  fixes h :: "'a :: {recpower,field}"
   16.61 +  fixes h :: "'a :: {field}"
   16.62    assumes h: "h \<noteq> 0" shows
   16.63    "((z + h) ^ n - z ^ n) / h - of_nat n * z ^ (n - Suc 0) =
   16.64     h * (\<Sum>p=0..< n - Suc 0. \<Sum>q=0..< n - Suc 0 - p.
   16.65 @@ -393,7 +393,7 @@
   16.66  done
   16.67  
   16.68  lemma lemma_termdiff3:
   16.69 -  fixes h z :: "'a::{real_normed_field,recpower}"
   16.70 +  fixes h z :: "'a::{real_normed_field}"
   16.71    assumes 1: "h \<noteq> 0"
   16.72    assumes 2: "norm z \<le> K"
   16.73    assumes 3: "norm (z + h) \<le> K"
   16.74 @@ -433,7 +433,7 @@
   16.75  qed
   16.76  
   16.77  lemma lemma_termdiff4:
   16.78 -  fixes f :: "'a::{real_normed_field,recpower} \<Rightarrow>
   16.79 +  fixes f :: "'a::{real_normed_field} \<Rightarrow>
   16.80                'b::real_normed_vector"
   16.81    assumes k: "0 < (k::real)"
   16.82    assumes le: "\<And>h. \<lbrakk>h \<noteq> 0; norm h < k\<rbrakk> \<Longrightarrow> norm (f h) \<le> K * norm h"
   16.83 @@ -478,7 +478,7 @@
   16.84  qed
   16.85  
   16.86  lemma lemma_termdiff5:
   16.87 -  fixes g :: "'a::{recpower,real_normed_field} \<Rightarrow>
   16.88 +  fixes g :: "'a::{real_normed_field} \<Rightarrow>
   16.89                nat \<Rightarrow> 'b::banach"
   16.90    assumes k: "0 < (k::real)"
   16.91    assumes f: "summable f"
   16.92 @@ -507,7 +507,7 @@
   16.93  text{* FIXME: Long proofs*}
   16.94  
   16.95  lemma termdiffs_aux:
   16.96 -  fixes x :: "'a::{recpower,real_normed_field,banach}"
   16.97 +  fixes x :: "'a::{real_normed_field,banach}"
   16.98    assumes 1: "summable (\<lambda>n. diffs (diffs c) n * K ^ n)"
   16.99    assumes 2: "norm x < norm K"
  16.100    shows "(\<lambda>h. \<Sum>n. c n * (((x + h) ^ n - x ^ n) / h
  16.101 @@ -572,7 +572,7 @@
  16.102  qed
  16.103  
  16.104  lemma termdiffs:
  16.105 -  fixes K x :: "'a::{recpower,real_normed_field,banach}"
  16.106 +  fixes K x :: "'a::{real_normed_field,banach}"
  16.107    assumes 1: "summable (\<lambda>n. c n * K ^ n)"
  16.108    assumes 2: "summable (\<lambda>n. (diffs c) n * K ^ n)"
  16.109    assumes 3: "summable (\<lambda>n. (diffs (diffs c)) n * K ^ n)"
  16.110 @@ -822,11 +822,11 @@
  16.111  subsection {* Exponential Function *}
  16.112  
  16.113  definition
  16.114 -  exp :: "'a \<Rightarrow> 'a::{recpower,real_normed_field,banach}" where
  16.115 +  exp :: "'a \<Rightarrow> 'a::{real_normed_field,banach}" where
  16.116    "exp x = (\<Sum>n. x ^ n /\<^sub>R real (fact n))"
  16.117  
  16.118  lemma summable_exp_generic:
  16.119 -  fixes x :: "'a::{real_normed_algebra_1,recpower,banach}"
  16.120 +  fixes x :: "'a::{real_normed_algebra_1,banach}"
  16.121    defines S_def: "S \<equiv> \<lambda>n. x ^ n /\<^sub>R real (fact n)"
  16.122    shows "summable S"
  16.123  proof -
  16.124 @@ -856,7 +856,7 @@
  16.125  qed
  16.126  
  16.127  lemma summable_norm_exp:
  16.128 -  fixes x :: "'a::{real_normed_algebra_1,recpower,banach}"
  16.129 +  fixes x :: "'a::{real_normed_algebra_1,banach}"
  16.130    shows "summable (\<lambda>n. norm (x ^ n /\<^sub>R real (fact n)))"
  16.131  proof (rule summable_norm_comparison_test [OF exI, rule_format])
  16.132    show "summable (\<lambda>n. norm x ^ n /\<^sub>R real (fact n))"
  16.133 @@ -901,7 +901,7 @@
  16.134  subsubsection {* Properties of the Exponential Function *}
  16.135  
  16.136  lemma powser_zero:
  16.137 -  fixes f :: "nat \<Rightarrow> 'a::{real_normed_algebra_1,recpower}"
  16.138 +  fixes f :: "nat \<Rightarrow> 'a::{real_normed_algebra_1}"
  16.139    shows "(\<Sum>n. f n * 0 ^ n) = f 0"
  16.140  proof -
  16.141    have "(\<Sum>n = 0..<1. f n * 0 ^ n) = (\<Sum>n. f n * 0 ^ n)"
  16.142 @@ -918,7 +918,7 @@
  16.143           del: setsum_cl_ivl_Suc)
  16.144  
  16.145  lemma exp_series_add:
  16.146 -  fixes x y :: "'a::{real_field,recpower}"
  16.147 +  fixes x y :: "'a::{real_field}"
  16.148    defines S_def: "S \<equiv> \<lambda>x n. x ^ n /\<^sub>R real (fact n)"
  16.149    shows "S (x + y) n = (\<Sum>i=0..n. S x i * S y (n - i))"
  16.150  proof (induct n)
    17.1 --- a/src/HOL/Word/WordArith.thy	Tue Apr 28 15:50:30 2009 +0200
    17.2 +++ b/src/HOL/Word/WordArith.thy	Tue Apr 28 15:50:30 2009 +0200
    17.3 @@ -790,15 +790,14 @@
    17.4  instance word :: (len) comm_semiring_1 
    17.5    by (intro_classes) (simp add: lenw1_zero_neq_one)
    17.6  
    17.7 +instance word :: (len) recpower ..
    17.8 +
    17.9  instance word :: (len) comm_ring_1 ..
   17.10  
   17.11  instance word :: (len0) comm_semiring_0 ..
   17.12  
   17.13  instance word :: (len0) order ..
   17.14  
   17.15 -instance word :: (len) recpower
   17.16 -  by (intro_classes) simp_all
   17.17 -
   17.18  (* note that iszero_def is only for class comm_semiring_1_cancel,
   17.19     which requires word length >= 1, ie 'a :: len word *) 
   17.20  lemma zero_bintrunc: