--- 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
--- 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
--- 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
--- 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 *}
--- 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)
--- 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]
--- 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
--- 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
--- 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
--- 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:
--- 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"
--- 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} *}
--- 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
--- 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
--- 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"
--- 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
--- 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"
--- 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)
--- 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:
--- 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:"
--- 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*}
--- 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)
--- 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)"
--- 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 *}
--- 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"
--- 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
--- 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: