# HG changeset patch
# User huffman
# Date 1236215543 28800
# Node ID ecd6f0ca62ea58dfb517e89fa9c8aed6f820f30a
# Parent  5af6ed62385b60dc4eabe73aa405457975d5a33b
declare power_Suc [simp]; remove redundant type-specific versions of power_Suc

diff -r 5af6ed62385b -r ecd6f0ca62ea NEWS
--- a/NEWS	Thu Mar 05 00:16:28 2009 +0100
+++ b/NEWS	Wed Mar 04 17:12:23 2009 -0800
@@ -361,6 +361,19 @@
 further lemmas!). At the moment both still exist but the former will disappear
 at some point.
 
+* HOL/Power: Lemma power_Suc is now declared as a simp rule in class
+recpower.  Type-specific simp rules for various recpower types have
+been removed.  INCOMPATIBILITY.  Rename old lemmas as follows:
+
+rat_power_0    -> power_0
+rat_power_Suc  -> power_Suc
+realpow_0      -> power_0
+realpow_Suc    -> power_Suc
+complexpow_0   -> power_0
+complexpow_Suc -> power_Suc
+power_poly_0   -> power_0
+power_poly_Suc -> power_Suc
+
 * HOL/Ring_and_Field and HOL/Divides: Definition of "op dvd" has been
 moved to separate class dvd in Ring_and_Field; a couple of lemmas on
 dvd has been generalized to class comm_semiring_1.  Likewise a bunch
diff -r 5af6ed62385b -r ecd6f0ca62ea src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Thu Mar 05 00:16:28 2009 +0100
+++ b/src/HOL/Complex.thy	Wed Mar 04 17:12:23 2009 -0800
@@ -163,10 +163,13 @@
 begin
 
 primrec power_complex where
-  complexpow_0:     "z ^ 0     = (1\<Colon>complex)"
-  | complexpow_Suc: "z ^ Suc n = (z\<Colon>complex) * z ^ n"
+  "z ^ 0     = (1\<Colon>complex)"
+| "z ^ Suc n = (z\<Colon>complex) * z ^ n"
 
-instance by intro_classes simp_all
+instance proof
+qed simp_all
+
+declare power_complex.simps [simp del]
 
 end
 
diff -r 5af6ed62385b -r ecd6f0ca62ea src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Thu Mar 05 00:16:28 2009 +0100
+++ b/src/HOL/Decision_Procs/Approximation.thy	Wed Mar 04 17:12:23 2009 -0800
@@ -619,7 +619,7 @@
 	using arctan_0_1_bounds[OF `0 \<le> Ifloat ?DIV` `Ifloat ?DIV \<le> 1`] by auto
       also have "\<dots> \<le> 2 * arctan (Ifloat x / ?R)"
 	using arctan_monotone'[OF monotone] by (auto intro!: mult_left_mono)
-      also have "2 * arctan (Ifloat x / ?R) = arctan (Ifloat x)" using arctan_half[symmetric] unfolding numeral_2_eq_2 power_Suc2 realpow_0 real_mult_1 . 
+      also have "2 * arctan (Ifloat x / ?R) = arctan (Ifloat x)" using arctan_half[symmetric] unfolding numeral_2_eq_2 power_Suc2 power_0 real_mult_1 . 
       finally show ?thesis unfolding lb_arctan.simps Let_def if_not_P[OF `\<not> x < 0`] if_not_P[OF `\<not> x \<le> Float 1 -1`] if_P[OF True] .
     next
       case False
@@ -708,7 +708,7 @@
 	have "0 \<le> Ifloat x / ?R" using `0 \<le> Ifloat x` `0 < ?R` unfolding real_0_le_divide_iff by auto
 	hence "0 \<le> Ifloat ?DIV" using monotone by (rule order_trans)
 
-	have "arctan (Ifloat x) = 2 * arctan (Ifloat x / ?R)" using arctan_half unfolding numeral_2_eq_2 power_Suc2 realpow_0 real_mult_1 .
+	have "arctan (Ifloat x) = 2 * arctan (Ifloat x / ?R)" using arctan_half unfolding numeral_2_eq_2 power_Suc2 power_0 real_mult_1 .
 	also have "\<dots> \<le> 2 * arctan (Ifloat ?DIV)"
 	  using arctan_monotone'[OF monotone] by (auto intro!: mult_left_mono)
 	also have "\<dots> \<le> Ifloat (Float 1 1 * ?ub_horner ?DIV)" unfolding Ifloat_mult[of "Float 1 1"] Float_num
@@ -1285,7 +1285,7 @@
 	have "sin (Ifloat x) = sqrt (1 - cos (Ifloat x) ^ 2)" unfolding sin_squared_eq[symmetric] real_sqrt_abs using `0 \<le> sin (Ifloat x)` by auto
 	also have "\<dots> \<le> sqrt (Ifloat (1 - lb_cos prec x * lb_cos prec x))" 
 	proof (rule real_sqrt_le_mono)
-	  have "Ifloat (lb_cos prec x * lb_cos prec x) \<le> cos (Ifloat x) ^ 2" unfolding numeral_2_eq_2 power_Suc2 realpow_0 Ifloat_mult
+	  have "Ifloat (lb_cos prec x * lb_cos prec x) \<le> cos (Ifloat x) ^ 2" unfolding numeral_2_eq_2 power_Suc2 power_0 Ifloat_mult
 	    using `0 \<le> Ifloat (lb_cos prec x)` lb_cos[OF `0 \<le> Ifloat x` `Ifloat x \<le> pi`] `0 \<le> cos (Ifloat x)` by(auto intro!: mult_mono)
 	  thus "1 - cos (Ifloat x) ^ 2 \<le> Ifloat (1 - lb_cos prec x * lb_cos prec x)" unfolding Ifloat_sub Ifloat_1 by auto
 	qed
@@ -1317,7 +1317,7 @@
 	qed
 	also have "\<dots> \<le> sqrt (1 - cos (Ifloat x) ^ 2)"
 	proof (rule real_sqrt_le_mono)
-	  have "cos (Ifloat x) ^ 2 \<le> Ifloat (ub_cos prec x * ub_cos prec x)" unfolding numeral_2_eq_2 power_Suc2 realpow_0 Ifloat_mult
+	  have "cos (Ifloat x) ^ 2 \<le> Ifloat (ub_cos prec x * ub_cos prec x)" unfolding numeral_2_eq_2 power_Suc2 power_0 Ifloat_mult
 	    using `0 \<le> Ifloat (ub_cos prec x)` lb_cos[OF `0 \<le> Ifloat x` `Ifloat x \<le> pi`] `0 \<le> cos (Ifloat x)` by(auto intro!: mult_mono)
 	  thus "Ifloat (1 - ub_cos prec x * ub_cos prec x) \<le> 1 - cos (Ifloat x) ^ 2" unfolding Ifloat_sub Ifloat_1 by auto
 	qed
@@ -1814,7 +1814,7 @@
 
     {
       have "Ifloat (lb_ln2 prec * ?s) \<le> ln 2 * real (e + (bitlen m - 1))" (is "?lb2 \<le> _")
-	unfolding Ifloat_mult Ifloat_ge0_exp[OF order_refl] nat_0 realpow_0 mult_1_right
+	unfolding Ifloat_mult Ifloat_ge0_exp[OF order_refl] nat_0 power_0 mult_1_right
 	using lb_ln2[of prec]
       proof (rule mult_right_mono)
 	have "1 \<le> Float m e" using `1 \<le> x` Float unfolding le_float_def by auto
@@ -1837,7 +1837,7 @@
       have "ln (Ifloat ?x) \<le> Ifloat ((?x - 1) * ub_ln_horner prec (get_odd prec) 1 (?x - 1))" (is "_ \<le> ?ub_horner") by auto
       moreover
       have "ln 2 * real (e + (bitlen m - 1)) \<le> Ifloat (ub_ln2 prec * ?s)" (is "_ \<le> ?ub2")
-	unfolding Ifloat_mult Ifloat_ge0_exp[OF order_refl] nat_0 realpow_0 mult_1_right
+	unfolding Ifloat_mult Ifloat_ge0_exp[OF order_refl] nat_0 power_0 mult_1_right
 	using ub_ln2[of prec] 
       proof (rule mult_right_mono)
 	have "1 \<le> Float m e" using `1 \<le> x` Float unfolding le_float_def by auto
diff -r 5af6ed62385b -r ecd6f0ca62ea src/HOL/Deriv.thy
--- a/src/HOL/Deriv.thy	Thu Mar 05 00:16:28 2009 +0100
+++ b/src/HOL/Deriv.thy	Wed Mar 04 17:12:23 2009 -0800
@@ -202,7 +202,7 @@
   shows "DERIV (\<lambda>x. f x ^ Suc n) x :> (1 + of_nat n) * (D * f x ^ n)"
 proof (induct n)
 case 0
-  show ?case by (simp add: power_Suc f)
+  show ?case by (simp add: f)
 case (Suc k)
   from DERIV_mult' [OF f Suc] show ?case
     apply (simp only: of_nat_Suc ring_distribs mult_1_left)
@@ -214,7 +214,7 @@
   fixes f :: "'a \<Rightarrow> 'a::{real_normed_field,recpower}"
   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)
+by (cases "n", simp, simp add: DERIV_power_Suc f del: power_Suc)
 
 
 text {* Caratheodory formulation of derivative at a point *}
@@ -289,21 +289,21 @@
 lemma DERIV_inverse:
   fixes x :: "'a::{real_normed_field,recpower}"
   shows "x \<noteq> 0 ==> DERIV (%x. inverse(x)) x :> (-(inverse x ^ Suc (Suc 0)))"
-by (drule DERIV_inverse' [OF DERIV_ident]) (simp add: power_Suc)
+by (drule DERIV_inverse' [OF DERIV_ident]) simp
 
 text{*Derivative of inverse*}
 lemma DERIV_inverse_fun:
   fixes x :: "'a::{real_normed_field,recpower}"
   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 power_Suc nonzero_inverse_mult_distrib)
+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}"
   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 power_Suc)
+by (drule (2) DERIV_divide) (simp add: mult_commute)
 
 lemma lemma_DERIV_subst: "[| DERIV f x :> D; D = E |] ==> DERIV f x :> E"
 by auto
@@ -407,7 +407,7 @@
   fixes f :: "'a::{recpower,real_normed_field} \<Rightarrow> 'a"
   assumes "f differentiable x"
   shows "(\<lambda>x. f x ^ n) differentiable x"
-  by (induct n, simp, simp add: power_Suc prems)
+  by (induct n, simp, simp add: prems)
 
 
 subsection {* Nested Intervals and Bisection *}
diff -r 5af6ed62385b -r ecd6f0ca62ea src/HOL/Int.thy
--- a/src/HOL/Int.thy	Thu Mar 05 00:16:28 2009 +0100
+++ b/src/HOL/Int.thy	Wed Mar 04 17:12:23 2009 -0800
@@ -1870,6 +1870,8 @@
   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)"
@@ -1887,7 +1889,7 @@
 
 lemma of_int_power:
   "of_int (z ^ n) = (of_int z ^ n :: 'a::{recpower, ring_1})"
-  by (induct n) (simp_all add: power_Suc)
+  by (induct n) simp_all
 
 lemma int_power: "int (m^n) = (int m) ^ n"
   by (rule of_nat_power)
diff -r 5af6ed62385b -r ecd6f0ca62ea src/HOL/Library/Binomial.thy
--- a/src/HOL/Library/Binomial.thy	Thu Mar 05 00:16:28 2009 +0100
+++ b/src/HOL/Library/Binomial.thy	Wed Mar 04 17:12:23 2009 -0800
@@ -355,7 +355,6 @@
   using binomial_fact_lemma[OF kn]
   by (simp add: field_simps fact_not_eq_zero of_nat_mult[symmetric])
 
-
 lemma binomial_gbinomial: "of_nat (n choose k) = of_nat n gchoose k"
 proof-
   {assume kn: "k > n" 
@@ -384,7 +383,7 @@
     have ?thesis using kn
       apply (simp add: binomial_fact[OF kn, where ?'a = 'a] 
 	gbinomial_pochhammer field_simps pochhammer_Suc_setprod)
-      apply (simp add: pochhammer_Suc_setprod fact_setprod h of_nat_setprod setprod_timesf[symmetric] eq' del: One_nat_def)
+      apply (simp add: pochhammer_Suc_setprod fact_setprod h of_nat_setprod setprod_timesf[symmetric] eq' del: One_nat_def power_Suc)
       unfolding setprod_Un_disjoint[OF th0, unfolded eq3, of "of_nat:: nat \<Rightarrow> 'a"] eq[unfolded h]
       unfolding mult_assoc[symmetric] 
       unfolding setprod_timesf[symmetric]
diff -r 5af6ed62385b -r ecd6f0ca62ea src/HOL/Library/Commutative_Ring.thy
--- a/src/HOL/Library/Commutative_Ring.thy	Thu Mar 05 00:16:28 2009 +0100
+++ b/src/HOL/Library/Commutative_Ring.thy	Wed Mar 04 17:12:23 2009 -0800
@@ -291,7 +291,8 @@
 	  then have "Ipol ls P * Ipol ls P = Ipol ls P ^ 2"
 	    by (simp add: numerals)
           with Suc show ?thesis
-            by (auto simp add: power_mult [symmetric, of _ 2 _] two_times mul_ci sqr_ci)
+            by (auto simp add: power_mult [symmetric, of _ 2 _] two_times mul_ci sqr_ci
+                     simp del: power_Suc)
         qed
       } with 1 Suc `odd l` show ?thesis by simp
     qed
diff -r 5af6ed62385b -r ecd6f0ca62ea src/HOL/Library/Formal_Power_Series.thy
--- a/src/HOL/Library/Formal_Power_Series.thy	Thu Mar 05 00:16:28 2009 +0100
+++ b/src/HOL/Library/Formal_Power_Series.thy	Wed Mar 04 17:12:23 2009 -0800
@@ -1303,7 +1303,7 @@
 lemma fps_power_nth:
   fixes m :: nat and a :: "('a::comm_ring_1) fps"
   shows "(a ^m)$n = (if m=0 then 1$n else setsum (\<lambda>v. setprod (\<lambda>j. a $ (v!j)) {0..m - 1}) (natpermute n m))"
-  by (cases m, simp_all add: fps_power_nth_Suc)
+  by (cases m, simp_all add: fps_power_nth_Suc del: power_Suc)
 
 lemma fps_nth_power_0: 
   fixes m :: nat and a :: "('a::{comm_ring_1, recpower}) fps"
@@ -1314,7 +1314,7 @@
   {fix n assume m: "m = Suc n"
     have c: "m = card {0..n}" using m by simp
    have "(a ^m)$0 = setprod (\<lambda>i. a$0) {0..n}"
-     apply (simp add: m fps_power_nth del: replicate.simps)
+     apply (simp add: m fps_power_nth del: replicate.simps power_Suc)
      apply (rule setprod_cong)
      by (simp_all del: replicate.simps)
    also have "\<dots> = (a$0) ^ m"
@@ -1613,7 +1613,7 @@
   shows "(fps_radical r (Suc k) (a ^ Suc k)) = a"
 proof-
   let ?ak = "a^ Suc k"
-  have ak0: "?ak $ 0 = (a$0) ^ Suc k" by (simp add: fps_nth_power_0)
+  have ak0: "?ak $ 0 = (a$0) ^ Suc k" by (simp add: fps_nth_power_0 del: power_Suc)
   from r0 have th0: "r (Suc k) (a ^ Suc k $ 0) ^ Suc k = a ^ Suc k $ 0" using ak0 by auto
   from r0 ak0 have th1: "r (Suc k) (a ^ Suc k $ 0) = a $ 0" by auto
   from ak0 a0 have ak00: "?ak $ 0 \<noteq>0 " by auto
@@ -1634,7 +1634,7 @@
   from power_radical[of r, OF r0 a0]
   have "fps_deriv (?r ^ Suc k) = fps_deriv a" by simp
   hence "fps_deriv ?r * ?w = fps_deriv a"
-    by (simp add: fps_deriv_power mult_ac)
+    by (simp add: fps_deriv_power mult_ac del: power_Suc)
   hence "?iw * fps_deriv ?r * ?w = ?iw * fps_deriv a" by simp
   hence "fps_deriv ?r * (?iw * ?w) = fps_deriv a / ?w"
     by (simp add: fps_divide_def)
@@ -1663,7 +1663,7 @@
   have ab0: "(a*b) $ 0 \<noteq> 0" using a0 b0 by (simp add: fps_mult_nth)
   from radical_unique[of r h "a*b" "fps_radical r (Suc h) a * fps_radical r (Suc h) b", OF r0[unfolded k] th0 ab0, symmetric] 
     power_radical[of r, OF ra0[unfolded k] a0] power_radical[of r, OF rb0[unfolded k] b0] k
-  have ?thesis by (auto simp add: power_mult_distrib)}
+  have ?thesis by (auto simp add: power_mult_distrib simp del: power_Suc)}
 ultimately show ?thesis by (cases k, auto)
 qed
 
@@ -1684,7 +1684,8 @@
     from ra0 a0 have th00: "r (Suc h) (a$0) \<noteq> 0" by auto
     have ria0': "r (Suc h) (inverse a $ 0) ^ Suc h = inverse a$0"
     using ria0 ra0 a0
-    by (simp add: fps_inverse_def  nonzero_power_inverse[OF th00, symmetric])
+    by (simp add: fps_inverse_def  nonzero_power_inverse[OF th00, symmetric]
+             del: power_Suc)
   from inverse_mult_eq_1[OF a0] have th0: "a * inverse a = 1" 
     by (simp add: mult_commute)
   from radical_unique[where a=1 and b=1 and r=r and k=h, simplified, OF r1[unfolded k]]
@@ -1848,7 +1849,8 @@
       moreover
       {fix n1 assume n1: "n = Suc n1"
 	have "?i $ n = setsum (\<lambda>i. (fps_inv a $ i) * (a^i)$n) {0 .. n1} + fps_inv a $ Suc n1 * (a $ 1)^ Suc n1"
-	  by (simp add: fps_compose_nth n1 startsby_zero_power_nth_same[OF a0])
+	  by (simp add: fps_compose_nth n1 startsby_zero_power_nth_same[OF a0]
+                   del: power_Suc)
 	also have "\<dots> = setsum (\<lambda>i. (fps_inv a $ i) * (a^i)$n) {0 .. n1} + (X$ Suc n1 - setsum (\<lambda>i. (fps_inv a $ i) * (a^i)$n) {0 .. n1})"
 	  using a0 a1 n1 by (simp add: fps_inv_def)
 	also have "\<dots> = X$n" using n1 by simp 
@@ -1878,7 +1880,8 @@
       moreover
       {fix n1 assume n1: "n = Suc n1"
 	have "?i $ n = setsum (\<lambda>i. (fps_ginv b a $ i) * (a^i)$n) {0 .. n1} + fps_ginv b a $ Suc n1 * (a $ 1)^ Suc n1"
-	  by (simp add: fps_compose_nth n1 startsby_zero_power_nth_same[OF a0])
+	  by (simp add: fps_compose_nth n1 startsby_zero_power_nth_same[OF a0]
+                   del: power_Suc)
 	also have "\<dots> = setsum (\<lambda>i. (fps_ginv b a $ i) * (a^i)$n) {0 .. n1} + (b$ Suc n1 - setsum (\<lambda>i. (fps_ginv b a $ i) * (a^i)$n) {0 .. n1})"
 	  using a0 a1 n1 by (simp add: fps_ginv_def)
 	also have "\<dots> = b$n" using n1 by simp 
@@ -2086,7 +2089,7 @@
   {fix h assume h: "k = Suc h"
     {fix n
       {assume kn: "k>n" hence "?l $ n = ?r $n" using a0 startsby_zero_power_prefix[OF a0] h 
-	  by (simp add: fps_compose_nth)}
+	  by (simp add: fps_compose_nth del: power_Suc)}
       moreover
       {assume kn: "k \<le> n"
 	hence "?l$n = ?r$n"
@@ -2138,7 +2141,7 @@
 proof-
   {fix n
     have "?l$n = ?r $ n"
-  apply (auto simp add: E_def field_simps power_Suc[symmetric]simp del: fact_Suc of_nat_Suc)
+  apply (auto simp add: E_def field_simps power_Suc[symmetric]simp del: fact_Suc of_nat_Suc power_Suc)
   by (simp add: of_nat_mult ring_simps)}
 then show ?thesis by (simp add: fps_eq_iff)
 qed
diff -r 5af6ed62385b -r ecd6f0ca62ea src/HOL/Library/FrechetDeriv.thy
--- a/src/HOL/Library/FrechetDeriv.thy	Thu Mar 05 00:16:28 2009 +0100
+++ b/src/HOL/Library/FrechetDeriv.thy	Wed Mar 04 17:12:23 2009 -0800
@@ -397,7 +397,7 @@
   shows "FDERIV (\<lambda>x. x ^ n) x :> (\<lambda>h. of_nat n * x ^ (n - 1) * h)"
   apply (cases n)
    apply (simp add: FDERIV_const)
-  apply (simp add: FDERIV_power_Suc)
+  apply (simp add: FDERIV_power_Suc del: power_Suc)
   done
 
 
diff -r 5af6ed62385b -r ecd6f0ca62ea src/HOL/Library/Poly_Deriv.thy
--- a/src/HOL/Library/Poly_Deriv.thy	Thu Mar 05 00:16:28 2009 +0100
+++ b/src/HOL/Library/Poly_Deriv.thy	Wed Mar 04 17:12:23 2009 -0800
@@ -139,7 +139,7 @@
   "pderiv ([:- a, 1:] ^ Suc n * q) = [:- a, 1:] ^ Suc n * pderiv q +
     smult (of_nat (Suc n)) (q * [:- a, 1:] ^ n)"
 apply (simp only: pderiv_mult pderiv_power_Suc)
-apply (simp del: power_poly_Suc of_nat_Suc add: pderiv_pCons)
+apply (simp del: power_Suc of_nat_Suc add: pderiv_pCons)
 done
 
 lemma dvd_add_cancel1:
diff -r 5af6ed62385b -r ecd6f0ca62ea src/HOL/Library/Polynomial.thy
--- a/src/HOL/Library/Polynomial.thy	Thu Mar 05 00:16:28 2009 +0100
+++ b/src/HOL/Library/Polynomial.thy	Wed Mar 04 17:12:23 2009 -0800
@@ -636,12 +636,14 @@
 begin
 
 primrec power_poly where
-  power_poly_0: "(p::'a poly) ^ 0 = 1"
-| power_poly_Suc: "(p::'a poly) ^ (Suc n) = p * p ^ n"
+  "(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
 
 lemma degree_power_le: "degree (p ^ n) \<le> degree p * n"
diff -r 5af6ed62385b -r ecd6f0ca62ea src/HOL/Lim.thy
--- a/src/HOL/Lim.thy	Thu Mar 05 00:16:28 2009 +0100
+++ b/src/HOL/Lim.thy	Wed Mar 04 17:12:23 2009 -0800
@@ -386,7 +386,7 @@
   fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::{recpower,real_normed_algebra}"
   assumes f: "f -- a --> l"
   shows "(\<lambda>x. f x ^ n) -- a --> l ^ n"
-by (induct n, simp, simp add: power_Suc LIM_mult f)
+by (induct n, simp, simp add: LIM_mult f)
 
 subsubsection {* Derived theorems about @{term LIM} *}
 
diff -r 5af6ed62385b -r ecd6f0ca62ea src/HOL/Ln.thy
--- a/src/HOL/Ln.thy	Thu Mar 05 00:16:28 2009 +0100
+++ b/src/HOL/Ln.thy	Wed Mar 04 17:12:23 2009 -0800
@@ -98,7 +98,7 @@
     also have "... = x ^ 2 / 2 * (1 / 2 * (1 / 2) ^ n)"
       by auto
     also have "(1::real) / 2 * (1 / 2) ^ n = (1 / 2) ^ (Suc n)"
-      by (rule realpow_Suc [THEN sym])
+      by (rule power_Suc [THEN sym])
     finally show ?thesis .
   qed
 qed
diff -r 5af6ed62385b -r ecd6f0ca62ea src/HOL/MacLaurin.thy
--- a/src/HOL/MacLaurin.thy	Thu Mar 05 00:16:28 2009 +0100
+++ b/src/HOL/MacLaurin.thy	Wed Mar 04 17:12:23 2009 -0800
@@ -82,13 +82,13 @@
  apply (frule less_iff_Suc_add [THEN iffD1], clarify)
  apply (simp del: setsum_op_ivl_Suc)
  apply (insert sumr_offset4 [of "Suc 0"])
- apply (simp del: setsum_op_ivl_Suc fact_Suc realpow_Suc)
+ apply (simp del: setsum_op_ivl_Suc fact_Suc power_Suc)
  apply (rule lemma_DERIV_subst)
   apply (rule DERIV_add)
    apply (rule_tac [2] DERIV_const)
   apply (rule DERIV_sumr, clarify)
   prefer 2 apply simp
- apply (simp (no_asm) add: divide_inverse mult_assoc del: fact_Suc realpow_Suc)
+ apply (simp (no_asm) add: divide_inverse mult_assoc del: fact_Suc power_Suc)
  apply (rule DERIV_cmult)
  apply (rule lemma_DERIV_subst)
   apply (best intro: DERIV_chain2 intro!: DERIV_intros)
@@ -145,7 +145,7 @@
     apply (frule less_iff_Suc_add [THEN iffD1], clarify)
     apply (simp del: setsum_op_ivl_Suc)
     apply (insert sumr_offset4 [of "Suc 0"])
-    apply (simp del: setsum_op_ivl_Suc fact_Suc realpow_Suc)
+    apply (simp del: setsum_op_ivl_Suc fact_Suc)
     done
 
   have isCont_difg: "\<And>m x. \<lbrakk>m < n; 0 \<le> x; x \<le> h\<rbrakk> \<Longrightarrow> isCont (difg m) x"
@@ -205,7 +205,7 @@
       (\<Sum>m = 0..<n. diff m 0 / real (fact m) * h ^ m) +
       diff n t / real (fact n) * h ^ n"
       using `difg (Suc m) t = 0`
-      by (simp add: m f_h difg_def del: realpow_Suc fact_Suc)
+      by (simp add: m f_h difg_def del: fact_Suc)
   qed
 
 qed
diff -r 5af6ed62385b -r ecd6f0ca62ea src/HOL/NSA/HDeriv.thy
--- a/src/HOL/NSA/HDeriv.thy	Thu Mar 05 00:16:28 2009 +0100
+++ b/src/HOL/NSA/HDeriv.thy	Wed Mar 04 17:12:23 2009 -0800
@@ -386,7 +386,7 @@
   fixes x :: "'a::{real_normed_field,recpower}"
   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: realpow_Suc)
+by (simp add: NSDERIV_DERIV_iff DERIV_inverse_fun del: power_Suc)
 
 text{*Derivative of quotient*}
 
@@ -395,7 +395,7 @@
   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))"
-by (simp add: NSDERIV_DERIV_iff DERIV_quotient del: realpow_Suc)
+by (simp add: NSDERIV_DERIV_iff DERIV_quotient del: power_Suc)
 
 lemma CARAT_NSDERIV: "NSDERIV f x :> l ==>
       \<exists>g. (\<forall>z. f z - f x = g z * (z-x)) & isNSCont g x & g x = l"
diff -r 5af6ed62385b -r ecd6f0ca62ea src/HOL/NSA/HSeries.thy
--- a/src/HOL/NSA/HSeries.thy	Thu Mar 05 00:16:28 2009 +0100
+++ b/src/HOL/NSA/HSeries.thy	Wed Mar 04 17:12:23 2009 -0800
@@ -114,7 +114,7 @@
 lemma sumhr_minus_one_realpow_zero [simp]: 
      "!!N. sumhr(0, N + N, %i. (-1) ^ (i+1)) = 0"
 unfolding sumhr_app
-by transfer (simp del: realpow_Suc add: nat_mult_2 [symmetric])
+by transfer (simp del: power_Suc add: nat_mult_2 [symmetric])
 
 lemma sumhr_interval_const:
      "(\<forall>n. m \<le> Suc n --> f n = r) & m \<le> na  
diff -r 5af6ed62385b -r ecd6f0ca62ea src/HOL/NSA/HTranscendental.thy
--- a/src/HOL/NSA/HTranscendental.thy	Thu Mar 05 00:16:28 2009 +0100
+++ b/src/HOL/NSA/HTranscendental.thy	Wed Mar 04 17:12:23 2009 -0800
@@ -38,7 +38,7 @@
 lemma hypreal_sqrt_pow2_iff: "(( *f* sqrt)(x) ^ 2 = x) = (0 \<le> x)"
 apply (cases x)
 apply (auto simp add: star_n_le star_n_zero_num starfun hrealpow star_n_eq_iff
-            simp del: hpowr_Suc realpow_Suc)
+            simp del: hpowr_Suc power_Suc)
 done
 
 lemma hypreal_sqrt_gt_zero_pow2: "!!x. 0 < x ==> ( *f* sqrt) (x) ^ 2 = x"
diff -r 5af6ed62385b -r ecd6f0ca62ea src/HOL/NSA/HyperDef.thy
--- a/src/HOL/NSA/HyperDef.thy	Thu Mar 05 00:16:28 2009 +0100
+++ b/src/HOL/NSA/HyperDef.thy	Wed Mar 04 17:12:23 2009 -0800
@@ -512,11 +512,11 @@
 
 lemma hyperpow_two_gt_one:
   "\<And>r::'a::{recpower,ordered_semidom} star. 1 < r \<Longrightarrow> 1 < r pow (1 + 1)"
-by transfer (simp add: power_gt1)
+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)"
-by transfer (simp add: one_le_power)
+by transfer (simp add: one_le_power del: power_Suc)
 
 lemma two_hyperpow_ge_one [simp]: "(1::hypreal) \<le> 2 pow n"
 apply (rule_tac y = "1 pow n" in order_trans)
diff -r 5af6ed62385b -r ecd6f0ca62ea src/HOL/NatBin.thy
--- a/src/HOL/NatBin.thy	Thu Mar 05 00:16:28 2009 +0100
+++ b/src/HOL/NatBin.thy	Wed Mar 04 17:12:23 2009 -0800
@@ -419,13 +419,13 @@
      "(a::'a::{ordered_idom,recpower}) < 0 ==> a ^ Suc(2*n) < 0"
 proof (induct "n")
   case 0
-  then show ?case by (simp add: Power.power_Suc)
+  then show ?case by simp
 next
   case (Suc n)
-  have "a ^ Suc (2 * Suc n) = (a*a) * a ^ Suc(2*n)" 
-    by (simp add: mult_ac power_add power2_eq_square Power.power_Suc)
+  have "a ^ Suc (2 * Suc n) = (a*a) * a ^ Suc(2*n)"
+    by (simp add: mult_ac power_add power2_eq_square)
   thus ?case
-    by (simp add: prems mult_less_0_iff mult_neg_neg)
+    by (simp del: power_Suc add: prems mult_less_0_iff mult_neg_neg)
 qed
 
 lemma odd_0_le_power_imp_0_le:
diff -r 5af6ed62385b -r ecd6f0ca62ea src/HOL/NthRoot.thy
--- a/src/HOL/NthRoot.thy	Thu Mar 05 00:16:28 2009 +0100
+++ b/src/HOL/NthRoot.thy	Wed Mar 04 17:12:23 2009 -0800
@@ -613,7 +613,7 @@
 apply (auto simp add: real_0_le_divide_iff power_divide)
 apply (rule_tac t = "u\<twosuperior>" in real_sum_of_halves [THEN subst])
 apply (rule add_mono)
-apply (auto simp add: four_x_squared simp del: realpow_Suc intro: power_mono)
+apply (auto simp add: four_x_squared intro: power_mono)
 done
 
 text "Legacy theorem names:"
diff -r 5af6ed62385b -r ecd6f0ca62ea src/HOL/Power.thy
--- a/src/HOL/Power.thy	Thu Mar 05 00:16:28 2009 +0100
+++ b/src/HOL/Power.thy	Wed Mar 04 17:12:23 2009 -0800
@@ -18,55 +18,50 @@
 
 class recpower = monoid_mult + power +
   assumes power_0 [simp]: "a ^ 0       = 1"
-  assumes power_Suc:      "a ^ Suc n = a * (a ^ n)"
+  assumes power_Suc [simp]: "a ^ Suc n = a * (a ^ n)"
 
 lemma power_0_Suc [simp]: "(0::'a::{recpower,semiring_0}) ^ (Suc n) = 0"
-  by (simp add: power_Suc)
+  by simp
 
 text{*It looks plausible as a simprule, but its effect can be strange.*}
 lemma power_0_left: "0^n = (if n=0 then 1 else (0::'a::{recpower,semiring_0}))"
   by (induct n) simp_all
 
 lemma power_one [simp]: "1^n = (1::'a::recpower)"
-  by (induct n) (simp_all add: power_Suc)
+  by (induct n) simp_all
 
 lemma power_one_right [simp]: "(a::'a::recpower) ^ 1 = a"
-  unfolding One_nat_def by (simp add: power_Suc)
+  unfolding One_nat_def by simp
 
 lemma power_commutes: "(a::'a::recpower) ^ n * a = a * a ^ n"
-  by (induct n) (simp_all add: power_Suc mult_assoc)
+  by (induct n) (simp_all add: mult_assoc)
 
 lemma power_Suc2: "(a::'a::recpower) ^ Suc n = a ^ n * a"
-  by (simp add: power_Suc power_commutes)
+  by (simp add: power_commutes)
 
 lemma power_add: "(a::'a::recpower) ^ (m+n) = (a^m) * (a^n)"
-  by (induct m) (simp_all add: power_Suc mult_ac)
+  by (induct m) (simp_all add: mult_ac)
 
 lemma power_mult: "(a::'a::recpower) ^ (m*n) = (a^m) ^ n"
-  by (induct n) (simp_all add: power_Suc power_add)
+  by (induct n) (simp_all add: power_add)
 
 lemma power_mult_distrib: "((a::'a::{recpower,comm_monoid_mult}) * b) ^ n = (a^n) * (b^n)"
-  by (induct n) (simp_all add: power_Suc mult_ac)
+  by (induct n) (simp_all add: mult_ac)
 
 lemma zero_less_power[simp]:
      "0 < (a::'a::{ordered_semidom,recpower}) ==> 0 < a^n"
-apply (induct "n")
-apply (simp_all add: power_Suc zero_less_one mult_pos_pos)
-done
+by (induct n) (simp_all add: mult_pos_pos)
 
 lemma zero_le_power[simp]:
      "0 \<le> (a::'a::{ordered_semidom,recpower}) ==> 0 \<le> a^n"
-apply (simp add: order_le_less)
-apply (erule disjE)
-apply (simp_all add: zero_less_one power_0_left)
-done
+by (induct n) (simp_all add: mult_nonneg_nonneg)
 
 lemma one_le_power[simp]:
      "1 \<le> (a::'a::{ordered_semidom,recpower}) ==> 1 \<le> a^n"
 apply (induct "n")
-apply (simp_all add: power_Suc)
+apply simp_all
 apply (rule order_trans [OF _ mult_mono [of 1 _ 1]])
-apply (simp_all add: zero_le_one order_trans [OF zero_le_one])
+apply (simp_all add: order_trans [OF zero_le_one])
 done
 
 lemma gt1_imp_ge0: "1 < a ==> 0 \<le> (a::'a::ordered_semidom)"
@@ -85,11 +80,11 @@
 
 lemma one_less_power[simp]:
   "\<lbrakk>1 < (a::'a::{ordered_semidom,recpower}); 0 < n\<rbrakk> \<Longrightarrow> 1 < a ^ n"
-by (cases n, simp_all add: power_gt1_lemma power_Suc)
+by (cases n, simp_all add: power_gt1_lemma)
 
 lemma power_gt1:
      "1 < (a::'a::{ordered_semidom,recpower}) ==> 1 < a ^ (Suc n)"
-by (simp add: power_gt1_lemma power_Suc)
+by (simp add: power_gt1_lemma)
 
 lemma power_le_imp_le_exp:
   assumes gt1: "(1::'a::{recpower,ordered_semidom}) < a"
@@ -102,7 +97,7 @@
   show ?case
   proof (cases n)
     case 0
-    from prems have "a * a^m \<le> 1" by (simp add: power_Suc)
+    from prems have "a * a^m \<le> 1" by simp
     with gt1 show ?thesis
       by (force simp only: power_gt1_lemma
           linorder_not_less [symmetric])
@@ -110,7 +105,7 @@
     case (Suc n)
     from prems show ?thesis
       by (force dest: mult_left_le_imp_le
-          simp add: power_Suc order_less_trans [OF zero_less_one gt1])
+          simp add: order_less_trans [OF zero_less_one gt1])
   qed
 qed
 
@@ -130,7 +125,7 @@
 lemma power_mono:
      "[|a \<le> b; (0::'a::{recpower,ordered_semidom}) \<le> a|] ==> a^n \<le> b^n"
 apply (induct "n")
-apply (simp_all add: power_Suc)
+apply simp_all
 apply (auto intro: mult_mono order_trans [of 0 a b])
 done
 
@@ -138,15 +133,14 @@
      "[|a < b; (0::'a::{recpower,ordered_semidom}) \<le> a|]
       ==> 0 < n --> a^n < b^n"
 apply (induct "n")
-apply (auto simp add: mult_strict_mono power_Suc
-                      order_le_less_trans [of 0 a b])
+apply (auto simp add: mult_strict_mono order_le_less_trans [of 0 a b])
 done
 
 lemma power_eq_0_iff [simp]:
   "(a^n = 0) \<longleftrightarrow>
    (a = (0::'a::{mult_zero,zero_neq_one,no_zero_divisors,recpower}) & n\<noteq>0)"
 apply (induct "n")
-apply (auto simp add: power_Suc zero_neq_one [THEN not_sym] no_zero_divisors)
+apply (auto simp add: no_zero_divisors)
 done
 
 
@@ -158,7 +152,7 @@
   fixes a :: "'a::{division_ring,recpower}"
   shows "a \<noteq> 0 ==> inverse (a ^ n) = (inverse a) ^ n"
 apply (induct "n")
-apply (auto simp add: power_Suc nonzero_inverse_mult_distrib power_commutes)
+apply (auto simp add: nonzero_inverse_mult_distrib power_commutes)
 done (* TODO: reorient or rename to nonzero_inverse_power *)
 
 text{*Perhaps these should be simprules.*}
@@ -189,18 +183,17 @@
 
 lemma power_abs: "abs(a ^ n) = abs(a::'a::{ordered_idom,recpower}) ^ n"
 apply (induct "n")
-apply (auto simp add: power_Suc abs_mult)
+apply (auto simp add: abs_mult)
 done
 
 lemma zero_less_power_abs_iff [simp,noatp]:
      "(0 < (abs a)^n) = (a \<noteq> (0::'a::{ordered_idom,recpower}) | n=0)"
 proof (induct "n")
   case 0
-    show ?case by (simp add: zero_less_one)
+    show ?case by simp
 next
   case (Suc n)
-    show ?case by (auto simp add: prems power_Suc zero_less_mult_iff
-      abs_zero)
+    show ?case by (auto simp add: prems zero_less_mult_iff)
 qed
 
 lemma zero_le_power_abs [simp]:
@@ -212,7 +205,7 @@
   case 0 show ?case by simp
 next
   case (Suc n) then show ?case
-    by (simp add: power_Suc2 mult_assoc)
+    by (simp del: power_Suc add: power_Suc2 mult_assoc)
 qed
 
 text{*Lemma for @{text power_strict_decreasing}*}
@@ -220,7 +213,7 @@
      "[|(0::'a::{ordered_semidom,recpower}) < a; a < 1|]
       ==> a * a^n < a^n"
 apply (induct n)
-apply (auto simp add: power_Suc mult_strict_left_mono)
+apply (auto simp add: mult_strict_left_mono)
 done
 
 lemma power_strict_decreasing:
@@ -228,11 +221,11 @@
       ==> a^N < a^n"
 apply (erule rev_mp)
 apply (induct "N")
-apply (auto simp add: power_Suc power_Suc_less less_Suc_eq)
+apply (auto simp add: power_Suc_less less_Suc_eq)
 apply (rename_tac m)
 apply (subgoal_tac "a * a^m < 1 * a^n", simp)
 apply (rule mult_strict_mono)
-apply (auto simp add: zero_less_one order_less_imp_le)
+apply (auto simp add: order_less_imp_le)
 done
 
 text{*Proof resembles that of @{text power_strict_decreasing}*}
@@ -241,11 +234,11 @@
       ==> a^N \<le> a^n"
 apply (erule rev_mp)
 apply (induct "N")
-apply (auto simp add: power_Suc  le_Suc_eq)
+apply (auto simp add: le_Suc_eq)
 apply (rename_tac m)
 apply (subgoal_tac "a * a^m \<le> 1 * a^n", simp)
 apply (rule mult_mono)
-apply (auto simp add: zero_le_one)
+apply auto
 done
 
 lemma power_Suc_less_one:
@@ -258,7 +251,7 @@
      "[|n \<le> N; (1::'a::{ordered_semidom,recpower}) \<le> a|] ==> a^n \<le> a^N"
 apply (erule rev_mp)
 apply (induct "N")
-apply (auto simp add: power_Suc le_Suc_eq)
+apply (auto simp add: le_Suc_eq)
 apply (rename_tac m)
 apply (subgoal_tac "1 * a^n \<le> a * a^m", simp)
 apply (rule mult_mono)
@@ -269,14 +262,14 @@
 lemma power_less_power_Suc:
      "(1::'a::{ordered_semidom,recpower}) < a ==> a^n < a * a^n"
 apply (induct n)
-apply (auto simp add: power_Suc mult_strict_left_mono order_less_trans [OF zero_less_one])
+apply (auto simp add: mult_strict_left_mono order_less_trans [OF zero_less_one])
 done
 
 lemma power_strict_increasing:
      "[|n < N; (1::'a::{ordered_semidom,recpower}) < a|] ==> a^n < a^N"
 apply (erule rev_mp)
 apply (induct "N")
-apply (auto simp add: power_less_power_Suc power_Suc less_Suc_eq)
+apply (auto simp add: power_less_power_Suc less_Suc_eq)
 apply (rename_tac m)
 apply (subgoal_tac "1 * a^n < a * a^m", simp)
 apply (rule mult_strict_mono)
@@ -324,7 +317,7 @@
 lemma power_eq_imp_eq_base:
   fixes a b :: "'a::{ordered_semidom,recpower}"
   shows "\<lbrakk>a ^ n = b ^ n; 0 \<le> a; 0 \<le> b; 0 < n\<rbrakk> \<Longrightarrow> a = b"
-by (cases n, simp_all, rule power_inject_base)
+by (cases n, simp_all del: power_Suc, rule power_inject_base)
 
 text {* The divides relation *}
 
@@ -360,11 +353,13 @@
   show "z^(Suc n) = z * (z^n)" by simp
 qed
 
+declare power_nat.simps [simp del]
+
 end
 
 lemma of_nat_power:
   "of_nat (m ^ n) = (of_nat m::'a::{semiring_1,recpower}) ^ n"
-by (induct n, simp_all add: power_Suc of_nat_mult)
+by (induct n, simp_all add: of_nat_mult)
 
 lemma nat_one_le_power [simp]: "Suc 0 \<le> i ==> Suc 0 \<le> i^n"
 by (rule one_le_power [of i n, unfolded One_nat_def])
@@ -397,7 +392,7 @@
   assumes nz: "a ~= 0"
   shows "n <= m ==> (a::'a::{recpower, field}) ^ (m-n) = (a^m) / (a^n)"
   by (induct m n rule: diff_induct)
-    (simp_all add: power_Suc nonzero_mult_divide_cancel_left nz)
+    (simp_all add: nonzero_mult_divide_cancel_left nz)
 
 
 text{*ML bindings for the general exponentiation theorems*}
diff -r 5af6ed62385b -r ecd6f0ca62ea src/HOL/Rational.thy
--- a/src/HOL/Rational.thy	Thu Mar 05 00:16:28 2009 +0100
+++ b/src/HOL/Rational.thy	Wed Mar 04 17:12:23 2009 -0800
@@ -158,8 +158,8 @@
 
 primrec power_rat
 where
-  rat_power_0:     "q ^ 0 = (1\<Colon>rat)"
-  | rat_power_Suc: "q ^ Suc n = (q\<Colon>rat) * (q ^ n)"
+  "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)" 
@@ -200,6 +200,8 @@
   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"
@@ -666,7 +668,7 @@
 
 lemma of_rat_power:
   "(of_rat (a ^ n)::'a::{field_char_0,recpower}) = of_rat a ^ n"
-by (induct n) (simp_all add: of_rat_mult power_Suc)
+by (induct n) (simp_all add: of_rat_mult)
 
 lemma of_rat_eq_iff [simp]: "(of_rat a = of_rat b) = (a = b)"
 apply (induct a, induct b)
diff -r 5af6ed62385b -r ecd6f0ca62ea src/HOL/RealPow.thy
--- a/src/HOL/RealPow.thy	Thu Mar 05 00:16:28 2009 +0100
+++ b/src/HOL/RealPow.thy	Wed Mar 04 17:12:23 2009 -0800
@@ -16,8 +16,8 @@
 begin
 
 primrec power_real where
-  realpow_0:     "r ^ 0     = (1\<Colon>real)"
-  | realpow_Suc: "r ^ Suc n = (r\<Colon>real) * r ^ n"
+  "r ^ 0     = (1\<Colon>real)"
+| "r ^ Suc n = (r\<Colon>real) * r ^ n"
 
 instance proof
   fix z :: real
@@ -26,6 +26,8 @@
   show "z^(Suc n) = z * (z^n)" by simp
 qed
 
+declare power_real.simps [simp del]
+
 end
 
 
@@ -65,7 +67,7 @@
 lemma realpow_two_disj:
      "((x::real)^Suc (Suc 0) = y^Suc (Suc 0)) = (x = y | x = -y)"
 apply (cut_tac x = x and y = y in realpow_two_diff)
-apply (auto simp del: realpow_Suc)
+apply auto
 done
 
 lemma realpow_real_of_nat: "real (m::nat) ^ n = real (m ^ n)"
diff -r 5af6ed62385b -r ecd6f0ca62ea src/HOL/RealVector.thy
--- a/src/HOL/RealVector.thy	Thu Mar 05 00:16:28 2009 +0100
+++ b/src/HOL/RealVector.thy	Wed Mar 04 17:12:23 2009 -0800
@@ -260,7 +260,7 @@
 
 lemma of_real_power [simp]:
   "of_real (x ^ n) = (of_real x :: 'a::{real_algebra_1,recpower}) ^ n"
-by (induct n) (simp_all add: power_Suc)
+by (induct n) simp_all
 
 lemma of_real_eq_iff [simp]: "(of_real x = of_real y) = (x = y)"
 by (simp add: of_real_def scaleR_cancel_right)
@@ -624,13 +624,13 @@
   also from Suc have "\<dots> \<le> norm x * norm x ^ n"
     using norm_ge_zero by (rule mult_left_mono)
   finally show "norm (x ^ Suc n) \<le> norm x ^ Suc n"
-    by (simp add: power_Suc)
+    by simp
 qed
 
 lemma norm_power:
   fixes x :: "'a::{real_normed_div_algebra,recpower}"
   shows "norm (x ^ n) = norm x ^ n"
-by (induct n) (simp_all add: power_Suc norm_mult)
+by (induct n) (simp_all add: norm_mult)
 
 
 subsection {* Sign function *}
diff -r 5af6ed62385b -r ecd6f0ca62ea src/HOL/SEQ.thy
--- a/src/HOL/SEQ.thy	Thu Mar 05 00:16:28 2009 +0100
+++ b/src/HOL/SEQ.thy	Wed Mar 04 17:12:23 2009 -0800
@@ -476,7 +476,7 @@
 lemma LIMSEQ_pow:
   fixes a :: "'a::{real_normed_algebra,recpower}"
   shows "X ----> a \<Longrightarrow> (\<lambda>n. (X n) ^ m) ----> a ^ m"
-by (induct m) (simp_all add: power_Suc LIMSEQ_const LIMSEQ_mult)
+by (induct m) (simp_all add: LIMSEQ_const LIMSEQ_mult)
 
 lemma LIMSEQ_setsum:
   assumes n: "\<And>n. n \<in> S \<Longrightarrow> X n ----> L n"
diff -r 5af6ed62385b -r ecd6f0ca62ea src/HOL/SizeChange/Kleene_Algebras.thy
--- a/src/HOL/SizeChange/Kleene_Algebras.thy	Thu Mar 05 00:16:28 2009 +0100
+++ b/src/HOL/SizeChange/Kleene_Algebras.thy	Wed Mar 04 17:12:23 2009 -0800
@@ -128,7 +128,7 @@
     apply (rule plus_leI, simp)
     apply (simp add:star_cont[of 1 a a, simplified])
     apply (simp add:star_cont[of 1 a 1, simplified])
-    by (auto intro: SUP_leI le_SUPI UNIV_I simp add: power_Suc[symmetric] power_commutes)
+    by (auto intro: SUP_leI le_SUPI simp add: power_Suc[symmetric] power_commutes simp del: power_Suc)
 
   show "a * x \<le> x \<Longrightarrow> star a * x \<le> x"
   proof -
@@ -138,13 +138,13 @@
       fix n
       have "a ^ (Suc n) * x \<le> a ^ n * x"
       proof (induct n)
-        case 0 thus ?case by (simp add:a power_Suc)
+        case 0 thus ?case by (simp add: a)
       next
         case (Suc n)
         hence "a * (a ^ Suc n * x) \<le> a * (a ^ n * x)"
           by (auto intro: mult_mono)
         thus ?case
-          by (simp add:power_Suc mult_assoc)
+          by (simp add: mult_assoc)
       qed
     }
     note a = this
@@ -173,13 +173,13 @@
       fix n
       have "x * a ^ (Suc n) \<le> x * a ^ n"
       proof (induct n)
-        case 0 thus ?case by (simp add:a power_Suc)
+        case 0 thus ?case by (simp add: a)
       next
         case (Suc n)
         hence "(x * a ^ Suc n) * a  \<le> (x * a ^ n) * a"
           by (auto intro: mult_mono)
         thus ?case
-          by (simp add:power_Suc power_commutes mult_assoc)
+          by (simp add: power_commutes mult_assoc)
       qed
     }
     note a = this
diff -r 5af6ed62385b -r ecd6f0ca62ea src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Thu Mar 05 00:16:28 2009 +0100
+++ b/src/HOL/Transcendental.thy	Wed Mar 04 17:12:23 2009 -0800
@@ -19,7 +19,7 @@
 proof -
   assume "p \<le> n"
   hence "Suc n - p = Suc (n - p)" by (rule Suc_diff_le)
-  thus ?thesis by (simp add: power_Suc power_commutes)
+  thus ?thesis by (simp add: power_commutes)
 qed
 
 lemma lemma_realpow_diff_sumr:
@@ -33,14 +33,14 @@
   fixes y :: "'a::{recpower,comm_ring}" shows
      "x ^ (Suc n) - y ^ (Suc n) =  
       (x - y) * (\<Sum>p=0..<Suc n. (x ^ p) * y ^ (n - p))"
-apply (induct n, simp add: power_Suc)
-apply (simp add: power_Suc del: setsum_op_ivl_Suc)
+apply (induct n, simp)
+apply (simp del: setsum_op_ivl_Suc)
 apply (subst setsum_op_ivl_Suc)
 apply (subst lemma_realpow_diff_sumr)
 apply (simp add: right_distrib del: setsum_op_ivl_Suc)
 apply (subst mult_left_commute [where a="x - y"])
 apply (erule subst)
-apply (simp add: power_Suc algebra_simps)
+apply (simp add: algebra_simps)
 done
 
 lemma lemma_realpow_rev_sumr:
@@ -368,7 +368,7 @@
 apply (cases "n", simp)
 apply (simp add: lemma_realpow_diff_sumr2 h
                  right_diff_distrib [symmetric] mult_assoc
-            del: realpow_Suc setsum_op_ivl_Suc of_nat_Suc)
+            del: power_Suc setsum_op_ivl_Suc of_nat_Suc)
 apply (subst lemma_realpow_rev_sumr)
 apply (subst sumr_diff_mult_const2)
 apply simp
@@ -377,7 +377,7 @@
 apply (simp add: diff_minus [symmetric] less_iff_Suc_add)
 apply (clarify)
 apply (simp add: setsum_right_distrib lemma_realpow_diff_sumr2 mult_ac
-            del: setsum_op_ivl_Suc realpow_Suc)
+            del: setsum_op_ivl_Suc power_Suc)
 apply (subst mult_assoc [symmetric], subst power_add [symmetric])
 apply (simp add: mult_ac)
 done
@@ -831,7 +831,7 @@
   shows "summable S"
 proof -
   have S_Suc: "\<And>n. S (Suc n) = (x * S n) /\<^sub>R real (Suc n)"
-    unfolding S_def by (simp add: power_Suc del: mult_Suc)
+    unfolding S_def by (simp del: mult_Suc)
   obtain r :: real where r0: "0 < r" and r1: "r < 1"
     using dense [OF zero_less_one] by fast
   obtain N :: nat where N: "norm x < real N * r"
@@ -928,7 +928,7 @@
 next
   case (Suc n)
   have S_Suc: "\<And>x n. S x (Suc n) = (x * S x n) /\<^sub>R real (Suc n)"
-    unfolding S_def by (simp add: power_Suc del: mult_Suc)
+    unfolding S_def by (simp del: mult_Suc)
   hence times_S: "\<And>x n. x * S x n = real (Suc n) *\<^sub>R S x (Suc n)"
     by simp
 
@@ -1471,22 +1471,22 @@
 
 lemma sin_cos_squared_add2 [simp]: "((cos x)\<twosuperior>) + ((sin x)\<twosuperior>) = 1"
 apply (subst add_commute)
-apply (simp (no_asm) del: realpow_Suc)
+apply (rule sin_cos_squared_add)
 done
 
 lemma sin_cos_squared_add3 [simp]: "cos x * cos x + sin x * sin x = 1"
 apply (cut_tac x = x in sin_cos_squared_add2)
-apply (auto simp add: numeral_2_eq_2)
+apply (simp add: power2_eq_square)
 done
 
 lemma sin_squared_eq: "(sin x)\<twosuperior> = 1 - (cos x)\<twosuperior>"
 apply (rule_tac a1 = "(cos x)\<twosuperior>" in add_right_cancel [THEN iffD1])
-apply (simp del: realpow_Suc)
+apply simp
 done
 
 lemma cos_squared_eq: "(cos x)\<twosuperior> = 1 - (sin x)\<twosuperior>"
 apply (rule_tac a1 = "(sin x)\<twosuperior>" in add_right_cancel [THEN iffD1])
-apply (simp del: realpow_Suc)
+apply simp
 done
 
 lemma abs_sin_le_one [simp]: "\<bar>sin x\<bar> \<le> 1"
@@ -1642,6 +1642,7 @@
   thus ?thesis unfolding One_nat_def by (simp add: mult_ac)
 qed
 
+text {* FIXME: This is a long, ugly proof! *}
 lemma sin_gt_zero: "[|0 < x; x < 2 |] ==> 0 < sin x"
 apply (subgoal_tac 
        "(\<lambda>n. \<Sum>k = n * 2..<n * 2 + 2.
@@ -1652,11 +1653,11 @@
 apply (rotate_tac 2)
 apply (drule sin_paired [THEN sums_unique, THEN ssubst])
 unfolding One_nat_def
-apply (auto simp del: fact_Suc realpow_Suc)
+apply (auto simp del: fact_Suc)
 apply (frule sums_unique)
-apply (auto simp del: fact_Suc realpow_Suc)
+apply (auto simp del: fact_Suc)
 apply (rule_tac n1 = 0 in series_pos_less [THEN [2] order_le_less_trans])
-apply (auto simp del: fact_Suc realpow_Suc)
+apply (auto simp del: fact_Suc)
 apply (erule sums_summable)
 apply (case_tac "m=0")
 apply (simp (no_asm_simp))
@@ -1721,7 +1722,7 @@
 apply (rule_tac y =
  "\<Sum>n=0..< Suc(Suc(Suc 0)). - (-1 ^ n / (real(fact (2*n))) * 2 ^ (2*n))"
        in order_less_trans)
-apply (simp (no_asm) add: fact_num_eq_if realpow_num_eq_if del: fact_Suc realpow_Suc)
+apply (simp (no_asm) add: fact_num_eq_if realpow_num_eq_if del: fact_Suc)
 apply (simp (no_asm) add: mult_assoc del: setsum_op_ivl_Suc)
 apply (rule sumr_pos_lt_pair)
 apply (erule sums_summable, safe)
@@ -2456,8 +2457,7 @@
 apply (rule_tac c1 = "(cos x)\<twosuperior>" in real_mult_right_cancel [THEN iffD1])
 apply (auto dest: field_power_not_zero
         simp add: power_mult_distrib left_distrib power_divide tan_def 
-                  mult_assoc power_inverse [symmetric] 
-        simp del: realpow_Suc)
+                  mult_assoc power_inverse [symmetric])
 done
 
 lemma isCont_inverse_function2: