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