1.1 --- a/src/HOL/Deriv.thy Tue Apr 28 18:42:26 2009 +0200
1.2 +++ b/src/HOL/Deriv.thy Tue Apr 28 19:15:50 2009 +0200
1.3 @@ -1,5 +1,4 @@
1.4 (* Title : Deriv.thy
1.5 - ID : $Id$
1.6 Author : Jacques D. Fleuriot
1.7 Copyright : 1998 University of Cambridge
1.8 Conversion to Isar and new proofs by Lawrence C Paulson, 2004
1.9 @@ -197,7 +196,7 @@
1.10 done
1.11
1.12 lemma DERIV_power_Suc:
1.13 - fixes f :: "'a \<Rightarrow> 'a::{real_normed_field,recpower}"
1.14 + fixes f :: "'a \<Rightarrow> 'a::{real_normed_field}"
1.15 assumes f: "DERIV f x :> D"
1.16 shows "DERIV (\<lambda>x. f x ^ Suc n) x :> (1 + of_nat n) * (D * f x ^ n)"
1.17 proof (induct n)
1.18 @@ -211,7 +210,7 @@
1.19 qed
1.20
1.21 lemma DERIV_power:
1.22 - fixes f :: "'a \<Rightarrow> 'a::{real_normed_field,recpower}"
1.23 + fixes f :: "'a \<Rightarrow> 'a::{real_normed_field}"
1.24 assumes f: "DERIV f x :> D"
1.25 shows "DERIV (\<lambda>x. f x ^ n) x :> of_nat n * (D * f x ^ (n - Suc 0))"
1.26 by (cases "n", simp, simp add: DERIV_power_Suc f del: power_Suc)
1.27 @@ -287,20 +286,20 @@
1.28 text{*Power of -1*}
1.29
1.30 lemma DERIV_inverse:
1.31 - fixes x :: "'a::{real_normed_field,recpower}"
1.32 + fixes x :: "'a::{real_normed_field}"
1.33 shows "x \<noteq> 0 ==> DERIV (%x. inverse(x)) x :> (-(inverse x ^ Suc (Suc 0)))"
1.34 by (drule DERIV_inverse' [OF DERIV_ident]) simp
1.35
1.36 text{*Derivative of inverse*}
1.37 lemma DERIV_inverse_fun:
1.38 - fixes x :: "'a::{real_normed_field,recpower}"
1.39 + fixes x :: "'a::{real_normed_field}"
1.40 shows "[| DERIV f x :> d; f(x) \<noteq> 0 |]
1.41 ==> DERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ Suc (Suc 0))))"
1.42 by (drule (1) DERIV_inverse') (simp add: mult_ac nonzero_inverse_mult_distrib)
1.43
1.44 text{*Derivative of quotient*}
1.45 lemma DERIV_quotient:
1.46 - fixes x :: "'a::{real_normed_field,recpower}"
1.47 + fixes x :: "'a::{real_normed_field}"
1.48 shows "[| DERIV f x :> d; DERIV g x :> e; g(x) \<noteq> 0 |]
1.49 ==> DERIV (%y. f(y) / (g y)) x :> (d*g(x) - (e*f(x))) / (g(x) ^ Suc (Suc 0))"
1.50 by (drule (2) DERIV_divide) (simp add: mult_commute)
1.51 @@ -404,7 +403,7 @@
1.52 unfolding divide_inverse using prems by simp
1.53
1.54 lemma differentiable_power [simp]:
1.55 - fixes f :: "'a::{recpower,real_normed_field} \<Rightarrow> 'a"
1.56 + fixes f :: "'a::{real_normed_field} \<Rightarrow> 'a"
1.57 assumes "f differentiable x"
1.58 shows "(\<lambda>x. f x ^ n) differentiable x"
1.59 by (induct n, simp, simp add: prems)
2.1 --- a/src/HOL/Finite_Set.thy Tue Apr 28 18:42:26 2009 +0200
2.2 +++ b/src/HOL/Finite_Set.thy Tue Apr 28 19:15:50 2009 +0200
2.3 @@ -2047,14 +2047,14 @@
2.4 apply (auto simp add: algebra_simps)
2.5 done
2.6
2.7 -lemma setprod_constant: "finite A ==> (\<Prod>x\<in> A. (y::'a::{recpower, comm_monoid_mult})) = y^(card A)"
2.8 +lemma setprod_constant: "finite A ==> (\<Prod>x\<in> A. (y::'a::{comm_monoid_mult})) = y^(card A)"
2.9 apply (erule finite_induct)
2.10 apply (auto simp add: power_Suc)
2.11 done
2.12
2.13 lemma setprod_gen_delta:
2.14 assumes fS: "finite S"
2.15 - shows "setprod (\<lambda>k. if k=a then b k else c) S = (if a \<in> S then (b a ::'a::{comm_monoid_mult, recpower}) * c^ (card S - 1) else c^ card S)"
2.16 + shows "setprod (\<lambda>k. if k=a then b k else c) S = (if a \<in> S then (b a ::'a::{comm_monoid_mult}) * c^ (card S - 1) else c^ card S)"
2.17 proof-
2.18 let ?f = "(\<lambda>k. if k=a then b k else c)"
2.19 {assume a: "a \<notin> S"
3.1 --- a/src/HOL/Groebner_Basis.thy Tue Apr 28 18:42:26 2009 +0200
3.2 +++ b/src/HOL/Groebner_Basis.thy Tue Apr 28 19:15:50 2009 +0200
3.3 @@ -164,7 +164,7 @@
3.4 end
3.5
3.6 interpretation class_semiring: gb_semiring
3.7 - "op +" "op *" "op ^" "0::'a::{comm_semiring_1, recpower}" "1"
3.8 + "op +" "op *" "op ^" "0::'a::{comm_semiring_1}" "1"
3.9 proof qed (auto simp add: algebra_simps power_Suc)
3.10
3.11 lemmas nat_arith =
3.12 @@ -242,7 +242,7 @@
3.13
3.14
3.15 interpretation class_ring: gb_ring "op +" "op *" "op ^"
3.16 - "0::'a::{comm_semiring_1,recpower,number_ring}" 1 "op -" "uminus"
3.17 + "0::'a::{comm_semiring_1,number_ring}" 1 "op -" "uminus"
3.18 proof qed simp_all
3.19
3.20
3.21 @@ -349,9 +349,9 @@
3.22 qed
3.23
3.24 interpretation class_ringb: ringb
3.25 - "op +" "op *" "op ^" "0::'a::{idom,recpower,number_ring}" "1" "op -" "uminus"
3.26 + "op +" "op *" "op ^" "0::'a::{idom,number_ring}" "1" "op -" "uminus"
3.27 proof(unfold_locales, simp add: algebra_simps power_Suc, auto)
3.28 - fix w x y z ::"'a::{idom,recpower,number_ring}"
3.29 + fix w x y z ::"'a::{idom,number_ring}"
3.30 assume p: "w * y + x * z = w * z + x * y" and ynz: "y \<noteq> z"
3.31 hence ynz': "y - z \<noteq> 0" by simp
3.32 from p have "w * y + x* z - w*z - x*y = 0" by simp
3.33 @@ -471,7 +471,7 @@
3.34 subsection{* Groebner Bases for fields *}
3.35
3.36 interpretation class_fieldgb:
3.37 - fieldgb "op +" "op *" "op ^" "0::'a::{field,recpower,number_ring}" "1" "op -" "uminus" "op /" "inverse" apply (unfold_locales) by (simp_all add: divide_inverse)
3.38 + fieldgb "op +" "op *" "op ^" "0::'a::{field,number_ring}" "1" "op -" "uminus" "op /" "inverse" apply (unfold_locales) by (simp_all add: divide_inverse)
3.39
3.40 lemma divide_Numeral1: "(x::'a::{field,number_ring}) / Numeral1 = x" by simp
3.41 lemma divide_Numeral0: "(x::'a::{field,number_ring, division_by_zero}) / Numeral0 = 0"
4.1 --- a/src/HOL/Int.thy Tue Apr 28 18:42:26 2009 +0200
4.2 +++ b/src/HOL/Int.thy Tue Apr 28 19:15:50 2009 +0200
4.3 @@ -292,9 +292,7 @@
4.4 context ring_1
4.5 begin
4.6
4.7 -definition
4.8 - of_int :: "int \<Rightarrow> 'a"
4.9 -where
4.10 +definition of_int :: "int \<Rightarrow> 'a" where
4.11 [code del]: "of_int z = contents (\<Union>(i, j) \<in> Rep_Integ z. { of_nat i - of_nat j })"
4.12
4.13 lemma of_int: "of_int (Abs_Integ (intrel `` {(i,j)})) = of_nat i - of_nat j"
4.14 @@ -330,6 +328,10 @@
4.15 lemma of_int_of_nat_eq [simp]: "of_int (of_nat n) = of_nat n"
4.16 by (induct n) auto
4.17
4.18 +lemma of_int_power:
4.19 + "of_int (z ^ n) = of_int z ^ n"
4.20 + by (induct n) simp_all
4.21 +
4.22 end
4.23
4.24 context ordered_idom
4.25 @@ -1841,23 +1843,6 @@
4.26 qed
4.27
4.28
4.29 -subsection {* Integer Powers *}
4.30 -
4.31 -lemma of_int_power:
4.32 - "of_int (z ^ n) = of_int z ^ n"
4.33 - by (induct n) simp_all
4.34 -
4.35 -lemma zpower_zpower:
4.36 - "(x ^ y) ^ z = (x ^ (y * z)::int)"
4.37 - by (rule power_mult [symmetric])
4.38 -
4.39 -lemma int_power:
4.40 - "int (m ^ n) = int m ^ n"
4.41 - by (rule of_nat_power)
4.42 -
4.43 -lemmas zpower_int = int_power [symmetric]
4.44 -
4.45 -
4.46 subsection {* Further theorems on numerals *}
4.47
4.48 subsubsection{*Special Simplification for Constants*}
4.49 @@ -2260,4 +2245,14 @@
4.50 lemma zero_le_zpower_abs: "(0::int) \<le> abs x ^ n"
4.51 by (rule zero_le_power_abs)
4.52
4.53 +lemma zpower_zpower:
4.54 + "(x ^ y) ^ z = (x ^ (y * z)::int)"
4.55 + by (rule power_mult [symmetric])
4.56 +
4.57 +lemma int_power:
4.58 + "int (m ^ n) = int m ^ n"
4.59 + by (rule of_nat_power)
4.60 +
4.61 +lemmas zpower_int = int_power [symmetric]
4.62 +
4.63 end
5.1 --- a/src/HOL/Lim.thy Tue Apr 28 18:42:26 2009 +0200
5.2 +++ b/src/HOL/Lim.thy Tue Apr 28 19:15:50 2009 +0200
5.3 @@ -383,7 +383,7 @@
5.4 lemmas LIM_of_real = of_real.LIM
5.5
5.6 lemma LIM_power:
5.7 - fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::{recpower,real_normed_algebra}"
5.8 + fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::{power,real_normed_algebra}"
5.9 assumes f: "f -- a --> l"
5.10 shows "(\<lambda>x. f x ^ n) -- a --> l ^ n"
5.11 by (induct n, simp, simp add: LIM_mult f)
5.12 @@ -530,7 +530,7 @@
5.13 unfolding isCont_def by (rule LIM_of_real)
5.14
5.15 lemma isCont_power:
5.16 - fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::{recpower,real_normed_algebra}"
5.17 + fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::{power,real_normed_algebra}"
5.18 shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. f x ^ n) a"
5.19 unfolding isCont_def by (rule LIM_power)
5.20
6.1 --- a/src/HOL/NSA/HDeriv.thy Tue Apr 28 18:42:26 2009 +0200
6.2 +++ b/src/HOL/NSA/HDeriv.thy Tue Apr 28 19:15:50 2009 +0200
6.3 @@ -1,5 +1,4 @@
6.4 (* Title : Deriv.thy
6.5 - ID : $Id$
6.6 Author : Jacques D. Fleuriot
6.7 Copyright : 1998 University of Cambridge
6.8 Conversion to Isar and new proofs by Lawrence C Paulson, 2004
6.9 @@ -345,7 +344,7 @@
6.10
6.11 (*Can't get rid of x \<noteq> 0 because it isn't continuous at zero*)
6.12 lemma NSDERIV_inverse:
6.13 - fixes x :: "'a::{real_normed_field,recpower}"
6.14 + fixes x :: "'a::{real_normed_field}"
6.15 shows "x \<noteq> 0 ==> NSDERIV (%x. inverse(x)) x :> (- (inverse x ^ Suc (Suc 0)))"
6.16 apply (simp add: nsderiv_def)
6.17 apply (rule ballI, simp, clarify)
6.18 @@ -383,7 +382,7 @@
6.19 text{*Derivative of inverse*}
6.20
6.21 lemma NSDERIV_inverse_fun:
6.22 - fixes x :: "'a::{real_normed_field,recpower}"
6.23 + fixes x :: "'a::{real_normed_field}"
6.24 shows "[| NSDERIV f x :> d; f(x) \<noteq> 0 |]
6.25 ==> NSDERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ Suc (Suc 0))))"
6.26 by (simp add: NSDERIV_DERIV_iff DERIV_inverse_fun del: power_Suc)
6.27 @@ -391,7 +390,7 @@
6.28 text{*Derivative of quotient*}
6.29
6.30 lemma NSDERIV_quotient:
6.31 - fixes x :: "'a::{real_normed_field,recpower}"
6.32 + fixes x :: "'a::{real_normed_field}"
6.33 shows "[| NSDERIV f x :> d; NSDERIV g x :> e; g(x) \<noteq> 0 |]
6.34 ==> NSDERIV (%y. f(y) / (g y)) x :> (d*g(x)
6.35 - (e*f(x))) / (g(x) ^ Suc (Suc 0))"
7.1 --- a/src/HOL/NSA/HSEQ.thy Tue Apr 28 18:42:26 2009 +0200
7.2 +++ b/src/HOL/NSA/HSEQ.thy Tue Apr 28 19:15:50 2009 +0200
7.3 @@ -110,7 +110,7 @@
7.4 done
7.5
7.6 lemma NSLIMSEQ_pow [rule_format]:
7.7 - fixes a :: "'a::{real_normed_algebra,recpower}"
7.8 + fixes a :: "'a::{real_normed_algebra,power}"
7.9 shows "(X ----NS> a) --> ((%n. (X n) ^ m) ----NS> a ^ m)"
7.10 apply (induct "m")
7.11 apply (auto simp add: power_Suc intro: NSLIMSEQ_mult NSLIMSEQ_const)
8.1 --- a/src/HOL/NSA/HyperDef.thy Tue Apr 28 18:42:26 2009 +0200
8.2 +++ b/src/HOL/NSA/HyperDef.thy Tue Apr 28 19:15:50 2009 +0200
8.3 @@ -417,7 +417,7 @@
8.4 declare power_hypreal_of_real_number_of [of _ "number_of w", standard, simp]
8.5 (*
8.6 lemma hrealpow_HFinite:
8.7 - fixes x :: "'a::{real_normed_algebra,recpower} star"
8.8 + fixes x :: "'a::{real_normed_algebra,power} star"
8.9 shows "x \<in> HFinite ==> x ^ n \<in> HFinite"
8.10 apply (induct_tac "n")
8.11 apply (auto simp add: power_Suc intro: HFinite_mult)
8.12 @@ -438,24 +438,24 @@
8.13 by (simp add: hyperpow_def starfun2_star_n)
8.14
8.15 lemma hyperpow_zero [simp]:
8.16 - "\<And>n. (0::'a::{recpower,semiring_0} star) pow (n + (1::hypnat)) = 0"
8.17 + "\<And>n. (0::'a::{power,semiring_0} star) pow (n + (1::hypnat)) = 0"
8.18 by transfer simp
8.19
8.20 lemma hyperpow_not_zero:
8.21 - "\<And>r n. r \<noteq> (0::'a::{recpower,field} star) ==> r pow n \<noteq> 0"
8.22 + "\<And>r n. r \<noteq> (0::'a::{field} star) ==> r pow n \<noteq> 0"
8.23 by transfer (rule field_power_not_zero)
8.24
8.25 lemma hyperpow_inverse:
8.26 - "\<And>r n. r \<noteq> (0::'a::{recpower,division_by_zero,field} star)
8.27 + "\<And>r n. r \<noteq> (0::'a::{division_by_zero,field} star)
8.28 \<Longrightarrow> inverse (r pow n) = (inverse r) pow n"
8.29 by transfer (rule power_inverse)
8.30 -
8.31 +
8.32 lemma hyperpow_hrabs:
8.33 - "\<And>r n. abs (r::'a::{recpower,ordered_idom} star) pow n = abs (r pow n)"
8.34 + "\<And>r n. abs (r::'a::{ordered_idom} star) pow n = abs (r pow n)"
8.35 by transfer (rule power_abs [symmetric])
8.36
8.37 lemma hyperpow_add:
8.38 - "\<And>r n m. (r::'a::recpower star) pow (n + m) = (r pow n) * (r pow m)"
8.39 + "\<And>r n m. (r::'a::monoid_mult star) pow (n + m) = (r pow n) * (r pow m)"
8.40 by transfer (rule power_add)
8.41
8.42 lemma hyperpow_one [simp]:
8.43 @@ -463,46 +463,46 @@
8.44 by transfer (rule power_one_right)
8.45
8.46 lemma hyperpow_two:
8.47 - "\<And>r. (r::'a::recpower star) pow ((1::hypnat) + (1::hypnat)) = r * r"
8.48 -by transfer (simp add: power_Suc)
8.49 + "\<And>r. (r::'a::monoid_mult star) pow ((1::hypnat) + (1::hypnat)) = r * r"
8.50 +by transfer simp
8.51
8.52 lemma hyperpow_gt_zero:
8.53 - "\<And>r n. (0::'a::{recpower,ordered_semidom} star) < r \<Longrightarrow> 0 < r pow n"
8.54 + "\<And>r n. (0::'a::{ordered_semidom} star) < r \<Longrightarrow> 0 < r pow n"
8.55 by transfer (rule zero_less_power)
8.56
8.57 lemma hyperpow_ge_zero:
8.58 - "\<And>r n. (0::'a::{recpower,ordered_semidom} star) \<le> r \<Longrightarrow> 0 \<le> r pow n"
8.59 + "\<And>r n. (0::'a::{ordered_semidom} star) \<le> r \<Longrightarrow> 0 \<le> r pow n"
8.60 by transfer (rule zero_le_power)
8.61
8.62 lemma hyperpow_le:
8.63 - "\<And>x y n. \<lbrakk>(0::'a::{recpower,ordered_semidom} star) < x; x \<le> y\<rbrakk>
8.64 + "\<And>x y n. \<lbrakk>(0::'a::{ordered_semidom} star) < x; x \<le> y\<rbrakk>
8.65 \<Longrightarrow> x pow n \<le> y pow n"
8.66 by transfer (rule power_mono [OF _ order_less_imp_le])
8.67
8.68 lemma hyperpow_eq_one [simp]:
8.69 - "\<And>n. 1 pow n = (1::'a::recpower star)"
8.70 + "\<And>n. 1 pow n = (1::'a::monoid_mult star)"
8.71 by transfer (rule power_one)
8.72
8.73 lemma hrabs_hyperpow_minus_one [simp]:
8.74 - "\<And>n. abs(-1 pow n) = (1::'a::{number_ring,recpower,ordered_idom} star)"
8.75 + "\<And>n. abs(-1 pow n) = (1::'a::{number_ring,ordered_idom} star)"
8.76 by transfer (rule abs_power_minus_one)
8.77
8.78 lemma hyperpow_mult:
8.79 - "\<And>r s n. (r * s::'a::{comm_monoid_mult,recpower} star) pow n
8.80 + "\<And>r s n. (r * s::'a::{comm_monoid_mult} star) pow n
8.81 = (r pow n) * (s pow n)"
8.82 by transfer (rule power_mult_distrib)
8.83
8.84 lemma hyperpow_two_le [simp]:
8.85 - "(0::'a::{recpower,ordered_ring_strict} star) \<le> r pow (1 + 1)"
8.86 + "(0::'a::{monoid_mult,ordered_ring_strict} star) \<le> r pow (1 + 1)"
8.87 by (auto simp add: hyperpow_two zero_le_mult_iff)
8.88
8.89 lemma hrabs_hyperpow_two [simp]:
8.90 "abs(x pow (1 + 1)) =
8.91 - (x::'a::{recpower,ordered_ring_strict} star) pow (1 + 1)"
8.92 + (x::'a::{monoid_mult,ordered_ring_strict} star) pow (1 + 1)"
8.93 by (simp only: abs_of_nonneg hyperpow_two_le)
8.94
8.95 lemma hyperpow_two_hrabs [simp]:
8.96 - "abs(x::'a::{recpower,ordered_idom} star) pow (1 + 1) = x pow (1 + 1)"
8.97 + "abs(x::'a::{ordered_idom} star) pow (1 + 1) = x pow (1 + 1)"
8.98 by (simp add: hyperpow_hrabs)
8.99
8.100 text{*The precondition could be weakened to @{term "0\<le>x"}*}
8.101 @@ -511,11 +511,11 @@
8.102 by (simp add: Ring_and_Field.mult_strict_mono order_less_imp_le)
8.103
8.104 lemma hyperpow_two_gt_one:
8.105 - "\<And>r::'a::{recpower,ordered_semidom} star. 1 < r \<Longrightarrow> 1 < r pow (1 + 1)"
8.106 + "\<And>r::'a::{ordered_semidom} star. 1 < r \<Longrightarrow> 1 < r pow (1 + 1)"
8.107 by transfer (simp add: power_gt1 del: power_Suc)
8.108
8.109 lemma hyperpow_two_ge_one:
8.110 - "\<And>r::'a::{recpower,ordered_semidom} star. 1 \<le> r \<Longrightarrow> 1 \<le> r pow (1 + 1)"
8.111 + "\<And>r::'a::{ordered_semidom} star. 1 \<le> r \<Longrightarrow> 1 \<le> r pow (1 + 1)"
8.112 by transfer (simp add: one_le_power del: power_Suc)
8.113
8.114 lemma two_hyperpow_ge_one [simp]: "(1::hypreal) \<le> 2 pow n"
8.115 @@ -565,7 +565,7 @@
8.116
8.117 lemma of_hypreal_hyperpow:
8.118 "\<And>x n. of_hypreal (x pow n) =
8.119 - (of_hypreal x::'a::{real_algebra_1,recpower} star) pow n"
8.120 + (of_hypreal x::'a::{real_algebra_1} star) pow n"
8.121 by transfer (rule of_real_power)
8.122
8.123 end
9.1 --- a/src/HOL/NSA/NSA.thy Tue Apr 28 18:42:26 2009 +0200
9.2 +++ b/src/HOL/NSA/NSA.thy Tue Apr 28 19:15:50 2009 +0200
9.3 @@ -101,7 +101,7 @@
9.4 by transfer (rule norm_mult)
9.5
9.6 lemma hnorm_hyperpow:
9.7 - "\<And>(x::'a::{real_normed_div_algebra,recpower} star) n.
9.8 + "\<And>(x::'a::{real_normed_div_algebra} star) n.
9.9 hnorm (x pow n) = hnorm x pow n"
9.10 by transfer (rule norm_power)
9.11
9.12 @@ -304,15 +304,15 @@
9.13 unfolding star_one_def by (rule HFinite_star_of)
9.14
9.15 lemma hrealpow_HFinite:
9.16 - fixes x :: "'a::{real_normed_algebra,recpower} star"
9.17 + fixes x :: "'a::{real_normed_algebra,monoid_mult} star"
9.18 shows "x \<in> HFinite ==> x ^ n \<in> HFinite"
9.19 -apply (induct_tac "n")
9.20 +apply (induct n)
9.21 apply (auto simp add: power_Suc intro: HFinite_mult)
9.22 done
9.23
9.24 lemma HFinite_bounded:
9.25 "[|(x::hypreal) \<in> HFinite; y \<le> x; 0 \<le> y |] ==> y \<in> HFinite"
9.26 -apply (case_tac "x \<le> 0")
9.27 +apply (cases "x \<le> 0")
9.28 apply (drule_tac y = x in order_trans)
9.29 apply (drule_tac [2] order_antisym)
9.30 apply (auto simp add: linorder_not_le)
10.1 --- a/src/HOL/NSA/NSComplex.thy Tue Apr 28 18:42:26 2009 +0200
10.2 +++ b/src/HOL/NSA/NSComplex.thy Tue Apr 28 19:15:50 2009 +0200
10.3 @@ -383,7 +383,7 @@
10.4 by transfer (rule power_mult_distrib)
10.5
10.6 lemma hcpow_zero2 [simp]:
10.7 - "\<And>n. 0 pow (hSuc n) = (0::'a::{recpower,semiring_0} star)"
10.8 + "\<And>n. 0 pow (hSuc n) = (0::'a::{power,semiring_0} star)"
10.9 by transfer (rule power_0_Suc)
10.10
10.11 lemma hcpow_not_zero [simp,intro]:
11.1 --- a/src/HOL/Nat_Numeral.thy Tue Apr 28 18:42:26 2009 +0200
11.2 +++ b/src/HOL/Nat_Numeral.thy Tue Apr 28 19:15:50 2009 +0200
11.3 @@ -10,6 +10,8 @@
11.4 uses ("Tools/nat_simprocs.ML")
11.5 begin
11.6
11.7 +subsection {* Numerals for natural numbers *}
11.8 +
11.9 text {*
11.10 Arithmetic for naturals is reduced to that for the non-negative integers.
11.11 *}
11.12 @@ -28,7 +30,16 @@
11.13 "nat (number_of v) = number_of v"
11.14 unfolding nat_number_of_def ..
11.15
11.16 -context recpower
11.17 +
11.18 +subsection {* Special case: squares and cubes *}
11.19 +
11.20 +lemma numeral_2_eq_2: "2 = Suc (Suc 0)"
11.21 + by (simp add: nat_number_of_def)
11.22 +
11.23 +lemma numeral_3_eq_3: "3 = Suc (Suc (Suc 0))"
11.24 + by (simp add: nat_number_of_def)
11.25 +
11.26 +context power
11.27 begin
11.28
11.29 abbreviation (xsymbols)
11.30 @@ -43,6 +54,205 @@
11.31
11.32 end
11.33
11.34 +context monoid_mult
11.35 +begin
11.36 +
11.37 +lemma power2_eq_square: "a\<twosuperior> = a * a"
11.38 + by (simp add: numeral_2_eq_2)
11.39 +
11.40 +lemma power3_eq_cube: "a ^ 3 = a * a * a"
11.41 + by (simp add: numeral_3_eq_3 mult_assoc)
11.42 +
11.43 +lemma power_even_eq:
11.44 + "a ^ (2*n) = (a ^ n) ^ 2"
11.45 + by (subst OrderedGroup.mult_commute) (simp add: power_mult)
11.46 +
11.47 +lemma power_odd_eq:
11.48 + "a ^ Suc (2*n) = a * (a ^ n) ^ 2"
11.49 + by (simp add: power_even_eq)
11.50 +
11.51 +end
11.52 +
11.53 +context semiring_1
11.54 +begin
11.55 +
11.56 +lemma zero_power2 [simp]: "0\<twosuperior> = 0"
11.57 + by (simp add: power2_eq_square)
11.58 +
11.59 +lemma one_power2 [simp]: "1\<twosuperior> = 1"
11.60 + by (simp add: power2_eq_square)
11.61 +
11.62 +end
11.63 +
11.64 +context comm_ring_1
11.65 +begin
11.66 +
11.67 +lemma power2_minus [simp]:
11.68 + "(- a)\<twosuperior> = a\<twosuperior>"
11.69 + by (simp add: power2_eq_square)
11.70 +
11.71 +text{*
11.72 + We cannot prove general results about the numeral @{term "-1"},
11.73 + so we have to use @{term "- 1"} instead.
11.74 +*}
11.75 +
11.76 +lemma power_minus1_even [simp]:
11.77 + "(- 1) ^ (2*n) = 1"
11.78 +proof (induct n)
11.79 + case 0 show ?case by simp
11.80 +next
11.81 + case (Suc n) then show ?case by (simp add: power_add)
11.82 +qed
11.83 +
11.84 +lemma power_minus1_odd:
11.85 + "(- 1) ^ Suc (2*n) = - 1"
11.86 + by simp
11.87 +
11.88 +lemma power_minus_even [simp]:
11.89 + "(-a) ^ (2*n) = a ^ (2*n)"
11.90 + by (simp add: power_minus [of a])
11.91 +
11.92 +end
11.93 +
11.94 +context ordered_ring_strict
11.95 +begin
11.96 +
11.97 +lemma sum_squares_ge_zero:
11.98 + "0 \<le> x * x + y * y"
11.99 + by (intro add_nonneg_nonneg zero_le_square)
11.100 +
11.101 +lemma not_sum_squares_lt_zero:
11.102 + "\<not> x * x + y * y < 0"
11.103 + by (simp add: not_less sum_squares_ge_zero)
11.104 +
11.105 +lemma sum_squares_eq_zero_iff:
11.106 + "x * x + y * y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
11.107 + by (simp add: sum_nonneg_eq_zero_iff)
11.108 +
11.109 +lemma sum_squares_le_zero_iff:
11.110 + "x * x + y * y \<le> 0 \<longleftrightarrow> x = 0 \<and> y = 0"
11.111 + by (simp add: le_less not_sum_squares_lt_zero sum_squares_eq_zero_iff)
11.112 +
11.113 +lemma sum_squares_gt_zero_iff:
11.114 + "0 < x * x + y * y \<longleftrightarrow> x \<noteq> 0 \<or> y \<noteq> 0"
11.115 +proof -
11.116 + have "x * x + y * y \<noteq> 0 \<longleftrightarrow> x \<noteq> 0 \<or> y \<noteq> 0"
11.117 + by (simp add: sum_squares_eq_zero_iff)
11.118 + then have "0 \<noteq> x * x + y * y \<longleftrightarrow> x \<noteq> 0 \<or> y \<noteq> 0"
11.119 + by auto
11.120 + then show ?thesis
11.121 + by (simp add: less_le sum_squares_ge_zero)
11.122 +qed
11.123 +
11.124 +end
11.125 +
11.126 +context ordered_semidom
11.127 +begin
11.128 +
11.129 +lemma power2_le_imp_le:
11.130 + "x\<twosuperior> \<le> y\<twosuperior> \<Longrightarrow> 0 \<le> y \<Longrightarrow> x \<le> y"
11.131 + unfolding numeral_2_eq_2 by (rule power_le_imp_le_base)
11.132 +
11.133 +lemma power2_less_imp_less:
11.134 + "x\<twosuperior> < y\<twosuperior> \<Longrightarrow> 0 \<le> y \<Longrightarrow> x < y"
11.135 + by (rule power_less_imp_less_base)
11.136 +
11.137 +lemma power2_eq_imp_eq:
11.138 + "x\<twosuperior> = y\<twosuperior> \<Longrightarrow> 0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> x = y"
11.139 + unfolding numeral_2_eq_2 by (erule (2) power_eq_imp_eq_base) simp
11.140 +
11.141 +end
11.142 +
11.143 +context ordered_idom
11.144 +begin
11.145 +
11.146 +lemma zero_eq_power2 [simp]:
11.147 + "a\<twosuperior> = 0 \<longleftrightarrow> a = 0"
11.148 + by (force simp add: power2_eq_square)
11.149 +
11.150 +lemma zero_le_power2 [simp]:
11.151 + "0 \<le> a\<twosuperior>"
11.152 + by (simp add: power2_eq_square)
11.153 +
11.154 +lemma zero_less_power2 [simp]:
11.155 + "0 < a\<twosuperior> \<longleftrightarrow> a \<noteq> 0"
11.156 + by (force simp add: power2_eq_square zero_less_mult_iff linorder_neq_iff)
11.157 +
11.158 +lemma power2_less_0 [simp]:
11.159 + "\<not> a\<twosuperior> < 0"
11.160 + by (force simp add: power2_eq_square mult_less_0_iff)
11.161 +
11.162 +lemma abs_power2 [simp]:
11.163 + "abs (a\<twosuperior>) = a\<twosuperior>"
11.164 + by (simp add: power2_eq_square abs_mult abs_mult_self)
11.165 +
11.166 +lemma power2_abs [simp]:
11.167 + "(abs a)\<twosuperior> = a\<twosuperior>"
11.168 + by (simp add: power2_eq_square abs_mult_self)
11.169 +
11.170 +lemma odd_power_less_zero:
11.171 + "a < 0 \<Longrightarrow> a ^ Suc (2*n) < 0"
11.172 +proof (induct n)
11.173 + case 0
11.174 + then show ?case by simp
11.175 +next
11.176 + case (Suc n)
11.177 + have "a ^ Suc (2 * Suc n) = (a*a) * a ^ Suc(2*n)"
11.178 + by (simp add: mult_ac power_add power2_eq_square)
11.179 + thus ?case
11.180 + by (simp del: power_Suc add: Suc mult_less_0_iff mult_neg_neg)
11.181 +qed
11.182 +
11.183 +lemma odd_0_le_power_imp_0_le:
11.184 + "0 \<le> a ^ Suc (2*n) \<Longrightarrow> 0 \<le> a"
11.185 + using odd_power_less_zero [of a n]
11.186 + by (force simp add: linorder_not_less [symmetric])
11.187 +
11.188 +lemma zero_le_even_power'[simp]:
11.189 + "0 \<le> a ^ (2*n)"
11.190 +proof (induct n)
11.191 + case 0
11.192 + show ?case by (simp add: zero_le_one)
11.193 +next
11.194 + case (Suc n)
11.195 + have "a ^ (2 * Suc n) = (a*a) * a ^ (2*n)"
11.196 + by (simp add: mult_ac power_add power2_eq_square)
11.197 + thus ?case
11.198 + by (simp add: Suc zero_le_mult_iff)
11.199 +qed
11.200 +
11.201 +lemma sum_power2_ge_zero:
11.202 + "0 \<le> x\<twosuperior> + y\<twosuperior>"
11.203 + unfolding power2_eq_square by (rule sum_squares_ge_zero)
11.204 +
11.205 +lemma not_sum_power2_lt_zero:
11.206 + "\<not> x\<twosuperior> + y\<twosuperior> < 0"
11.207 + unfolding power2_eq_square by (rule not_sum_squares_lt_zero)
11.208 +
11.209 +lemma sum_power2_eq_zero_iff:
11.210 + "x\<twosuperior> + y\<twosuperior> = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
11.211 + unfolding power2_eq_square by (rule sum_squares_eq_zero_iff)
11.212 +
11.213 +lemma sum_power2_le_zero_iff:
11.214 + "x\<twosuperior> + y\<twosuperior> \<le> 0 \<longleftrightarrow> x = 0 \<and> y = 0"
11.215 + unfolding power2_eq_square by (rule sum_squares_le_zero_iff)
11.216 +
11.217 +lemma sum_power2_gt_zero_iff:
11.218 + "0 < x\<twosuperior> + y\<twosuperior> \<longleftrightarrow> x \<noteq> 0 \<or> y \<noteq> 0"
11.219 + unfolding power2_eq_square by (rule sum_squares_gt_zero_iff)
11.220 +
11.221 +end
11.222 +
11.223 +lemma power2_sum:
11.224 + fixes x y :: "'a::number_ring"
11.225 + shows "(x + y)\<twosuperior> = x\<twosuperior> + y\<twosuperior> + 2 * x * y"
11.226 + by (simp add: ring_distribs power2_eq_square)
11.227 +
11.228 +lemma power2_diff:
11.229 + fixes x y :: "'a::number_ring"
11.230 + shows "(x - y)\<twosuperior> = x\<twosuperior> + y\<twosuperior> - 2 * x * y"
11.231 + by (simp add: ring_distribs power2_eq_square)
11.232 +
11.233
11.234 subsection {* Predicate for negative binary numbers *}
11.235
11.236 @@ -115,11 +325,6 @@
11.237 lemma numeral_1_eq_Suc_0: "Numeral1 = Suc 0"
11.238 by (simp add: nat_numeral_1_eq_1)
11.239
11.240 -lemma numeral_2_eq_2: "2 = Suc (Suc 0)"
11.241 -apply (unfold nat_number_of_def)
11.242 -apply (rule nat_2)
11.243 -done
11.244 -
11.245
11.246 subsection{*Function @{term int}: Coercion from Type @{typ nat} to @{typ int}*}
11.247
11.248 @@ -314,128 +519,10 @@
11.249
11.250 subsection{*Powers with Numeric Exponents*}
11.251
11.252 -text{*We cannot refer to the number @{term 2} in @{text Ring_and_Field.thy}.
11.253 -We cannot prove general results about the numeral @{term "-1"}, so we have to
11.254 -use @{term "- 1"} instead.*}
11.255 +text{*Squares of literal numerals will be evaluated.*}
11.256 +lemmas power2_eq_square_number_of [simp] =
11.257 + power2_eq_square [of "number_of w", standard]
11.258
11.259 -lemma power2_eq_square: "(a::'a::recpower)\<twosuperior> = a * a"
11.260 - by (simp add: numeral_2_eq_2 Power.power_Suc)
11.261 -
11.262 -lemma zero_power2 [simp]: "(0::'a::{semiring_1,recpower})\<twosuperior> = 0"
11.263 - by (simp add: power2_eq_square)
11.264 -
11.265 -lemma one_power2 [simp]: "(1::'a::{semiring_1,recpower})\<twosuperior> = 1"
11.266 - by (simp add: power2_eq_square)
11.267 -
11.268 -lemma power3_eq_cube: "(x::'a::recpower) ^ 3 = x * x * x"
11.269 - apply (subgoal_tac "3 = Suc (Suc (Suc 0))")
11.270 - apply (erule ssubst)
11.271 - apply (simp add: power_Suc mult_ac)
11.272 - apply (unfold nat_number_of_def)
11.273 - apply (subst nat_eq_iff)
11.274 - apply simp
11.275 -done
11.276 -
11.277 -text{*Squares of literal numerals will be evaluated.*}
11.278 -lemmas power2_eq_square_number_of =
11.279 - power2_eq_square [of "number_of w", standard]
11.280 -declare power2_eq_square_number_of [simp]
11.281 -
11.282 -
11.283 -lemma zero_le_power2[simp]: "0 \<le> (a\<twosuperior>::'a::{ordered_idom,recpower})"
11.284 - by (simp add: power2_eq_square)
11.285 -
11.286 -lemma zero_less_power2[simp]:
11.287 - "(0 < a\<twosuperior>) = (a \<noteq> (0::'a::{ordered_idom,recpower}))"
11.288 - by (force simp add: power2_eq_square zero_less_mult_iff linorder_neq_iff)
11.289 -
11.290 -lemma power2_less_0[simp]:
11.291 - fixes a :: "'a::{ordered_idom,recpower}"
11.292 - shows "~ (a\<twosuperior> < 0)"
11.293 -by (force simp add: power2_eq_square mult_less_0_iff)
11.294 -
11.295 -lemma zero_eq_power2[simp]:
11.296 - "(a\<twosuperior> = 0) = (a = (0::'a::{ordered_idom,recpower}))"
11.297 - by (force simp add: power2_eq_square mult_eq_0_iff)
11.298 -
11.299 -lemma abs_power2[simp]:
11.300 - "abs(a\<twosuperior>) = (a\<twosuperior>::'a::{ordered_idom,recpower})"
11.301 - by (simp add: power2_eq_square abs_mult abs_mult_self)
11.302 -
11.303 -lemma power2_abs[simp]:
11.304 - "(abs a)\<twosuperior> = (a\<twosuperior>::'a::{ordered_idom,recpower})"
11.305 - by (simp add: power2_eq_square abs_mult_self)
11.306 -
11.307 -lemma power2_minus[simp]:
11.308 - "(- a)\<twosuperior> = (a\<twosuperior>::'a::{comm_ring_1,recpower})"
11.309 - by (simp add: power2_eq_square)
11.310 -
11.311 -lemma power2_le_imp_le:
11.312 - fixes x y :: "'a::{ordered_semidom,recpower}"
11.313 - shows "\<lbrakk>x\<twosuperior> \<le> y\<twosuperior>; 0 \<le> y\<rbrakk> \<Longrightarrow> x \<le> y"
11.314 -unfolding numeral_2_eq_2 by (rule power_le_imp_le_base)
11.315 -
11.316 -lemma power2_less_imp_less:
11.317 - fixes x y :: "'a::{ordered_semidom,recpower}"
11.318 - shows "\<lbrakk>x\<twosuperior> < y\<twosuperior>; 0 \<le> y\<rbrakk> \<Longrightarrow> x < y"
11.319 -by (rule power_less_imp_less_base)
11.320 -
11.321 -lemma power2_eq_imp_eq:
11.322 - fixes x y :: "'a::{ordered_semidom,recpower}"
11.323 - shows "\<lbrakk>x\<twosuperior> = y\<twosuperior>; 0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> x = y"
11.324 -unfolding numeral_2_eq_2 by (erule (2) power_eq_imp_eq_base, simp)
11.325 -
11.326 -lemma power_minus1_even[simp]: "(- 1) ^ (2*n) = (1::'a::{comm_ring_1,recpower})"
11.327 -proof (induct n)
11.328 - case 0 show ?case by simp
11.329 -next
11.330 - case (Suc n) then show ?case by (simp add: power_Suc power_add)
11.331 -qed
11.332 -
11.333 -lemma power_minus1_odd: "(- 1) ^ Suc(2*n) = -(1::'a::{comm_ring_1,recpower})"
11.334 - by (simp add: power_Suc)
11.335 -
11.336 -lemma power_even_eq: "(a::'a::recpower) ^ (2*n) = (a^n)^2"
11.337 - by (subst mult_commute) (simp add: power_mult)
11.338 -
11.339 -lemma power_odd_eq: "(a::int) ^ Suc(2*n) = a * (a^n)^2"
11.340 - by (simp add: power_even_eq)
11.341 -
11.342 -lemma power_minus_even [simp]:
11.343 - "(-a) ^ (2*n) = (a::'a::{comm_ring_1,recpower}) ^ (2*n)"
11.344 - by (simp add: power_minus [of a])
11.345 -
11.346 -lemma zero_le_even_power'[simp]:
11.347 - "0 \<le> (a::'a::{ordered_idom,recpower}) ^ (2*n)"
11.348 -proof (induct "n")
11.349 - case 0
11.350 - show ?case by (simp add: zero_le_one)
11.351 -next
11.352 - case (Suc n)
11.353 - have "a ^ (2 * Suc n) = (a*a) * a ^ (2*n)"
11.354 - by (simp add: mult_ac power_add power2_eq_square)
11.355 - thus ?case
11.356 - by (simp add: prems zero_le_mult_iff)
11.357 -qed
11.358 -
11.359 -lemma odd_power_less_zero:
11.360 - "(a::'a::{ordered_idom,recpower}) < 0 ==> a ^ Suc(2*n) < 0"
11.361 -proof (induct "n")
11.362 - case 0
11.363 - then show ?case by simp
11.364 -next
11.365 - case (Suc n)
11.366 - have "a ^ Suc (2 * Suc n) = (a*a) * a ^ Suc(2*n)"
11.367 - by (simp add: mult_ac power_add power2_eq_square)
11.368 - thus ?case
11.369 - by (simp del: power_Suc add: prems mult_less_0_iff mult_neg_neg)
11.370 -qed
11.371 -
11.372 -lemma odd_0_le_power_imp_0_le:
11.373 - "0 \<le> a ^ Suc(2*n) ==> 0 \<le> (a::'a::{ordered_idom,recpower})"
11.374 -apply (insert odd_power_less_zero [of a n])
11.375 -apply (force simp add: linorder_not_less [symmetric])
11.376 -done
11.377
11.378 text{*Simprules for comparisons where common factors can be cancelled.*}
11.379 lemmas zero_compare_simps =
11.380 @@ -621,7 +708,7 @@
11.381 text{*For arbitrary rings*}
11.382
11.383 lemma power_number_of_even:
11.384 - fixes z :: "'a::{number_ring,recpower}"
11.385 + fixes z :: "'a::number_ring"
11.386 shows "z ^ number_of (Int.Bit0 w) = (let w = z ^ (number_of w) in w * w)"
11.387 unfolding Let_def nat_number_of_def number_of_Bit0
11.388 apply (rule_tac x = "number_of w" in spec, clarify)
11.389 @@ -630,7 +717,7 @@
11.390 done
11.391
11.392 lemma power_number_of_odd:
11.393 - fixes z :: "'a::{number_ring,recpower}"
11.394 + fixes z :: "'a::number_ring"
11.395 shows "z ^ number_of (Int.Bit1 w) = (if (0::int) <= number_of w
11.396 then (let w = z ^ (number_of w) in z * w * w) else 1)"
11.397 unfolding Let_def nat_number_of_def number_of_Bit1
11.398 @@ -697,11 +784,11 @@
11.399 lemma Let_Suc [simp]: "Let (Suc n) f == f (Suc n)"
11.400 by (simp add: Let_def)
11.401
11.402 -lemma power_m1_even: "(-1) ^ (2*n) = (1::'a::{number_ring,recpower})"
11.403 -by (simp add: power_mult power_Suc);
11.404 +lemma power_m1_even: "(-1) ^ (2*n) = (1::'a::{number_ring})"
11.405 + by (simp only: number_of_Min power_minus1_even)
11.406
11.407 -lemma power_m1_odd: "(-1) ^ Suc(2*n) = (-1::'a::{number_ring,recpower})"
11.408 -by (simp add: power_mult power_Suc);
11.409 +lemma power_m1_odd: "(-1) ^ Suc(2*n) = (-1::'a::{number_ring})"
11.410 + by (simp only: number_of_Min power_minus1_odd)
11.411
11.412
11.413 subsection{*Literal arithmetic and @{term of_nat}*}
12.1 --- a/src/HOL/NthRoot.thy Tue Apr 28 18:42:26 2009 +0200
12.2 +++ b/src/HOL/NthRoot.thy Tue Apr 28 19:15:50 2009 +0200
12.3 @@ -565,16 +565,6 @@
12.4 lemma le_real_sqrt_sumsq [simp]: "x \<le> sqrt (x * x + y * y)"
12.5 by (simp add: power2_eq_square [symmetric])
12.6
12.7 -lemma power2_sum:
12.8 - fixes x y :: "'a::{number_ring,recpower}"
12.9 - shows "(x + y)\<twosuperior> = x\<twosuperior> + y\<twosuperior> + 2 * x * y"
12.10 -by (simp add: ring_distribs power2_eq_square)
12.11 -
12.12 -lemma power2_diff:
12.13 - fixes x y :: "'a::{number_ring,recpower}"
12.14 - shows "(x - y)\<twosuperior> = x\<twosuperior> + y\<twosuperior> - 2 * x * y"
12.15 -by (simp add: ring_distribs power2_eq_square)
12.16 -
12.17 lemma real_sqrt_sum_squares_triangle_ineq:
12.18 "sqrt ((a + c)\<twosuperior> + (b + d)\<twosuperior>) \<le> sqrt (a\<twosuperior> + b\<twosuperior>) + sqrt (c\<twosuperior> + d\<twosuperior>)"
12.19 apply (rule power2_le_imp_le, simp)
13.1 --- a/src/HOL/OrderedGroup.thy Tue Apr 28 18:42:26 2009 +0200
13.2 +++ b/src/HOL/OrderedGroup.thy Tue Apr 28 19:15:50 2009 +0200
13.3 @@ -637,6 +637,27 @@
13.4 lemma le_iff_diff_le_0: "a \<le> b \<longleftrightarrow> a - b \<le> 0"
13.5 by (simp add: algebra_simps)
13.6
13.7 +lemma sum_nonneg_eq_zero_iff:
13.8 + assumes x: "0 \<le> x" and y: "0 \<le> y"
13.9 + shows "(x + y = 0) = (x = 0 \<and> y = 0)"
13.10 +proof -
13.11 + have "x + y = 0 \<Longrightarrow> x = 0"
13.12 + proof -
13.13 + from y have "x + 0 \<le> x + y" by (rule add_left_mono)
13.14 + also assume "x + y = 0"
13.15 + finally have "x \<le> 0" by simp
13.16 + then show "x = 0" using x by (rule antisym)
13.17 + qed
13.18 + moreover have "x + y = 0 \<Longrightarrow> y = 0"
13.19 + proof -
13.20 + from x have "0 + y \<le> x + y" by (rule add_right_mono)
13.21 + also assume "x + y = 0"
13.22 + finally have "y \<le> 0" by simp
13.23 + then show "y = 0" using y by (rule antisym)
13.24 + qed
13.25 + ultimately show ?thesis by auto
13.26 +qed
13.27 +
13.28 text{*Legacy - use @{text algebra_simps} *}
13.29 lemmas group_simps[noatp] = algebra_simps
13.30
14.1 --- a/src/HOL/Parity.thy Tue Apr 28 18:42:26 2009 +0200
14.2 +++ b/src/HOL/Parity.thy Tue Apr 28 19:15:50 2009 +0200
14.3 @@ -178,7 +178,7 @@
14.4 subsection {* Parity and powers *}
14.5
14.6 lemma minus_one_even_odd_power:
14.7 - "(even x --> (- 1::'a::{comm_ring_1,recpower})^x = 1) &
14.8 + "(even x --> (- 1::'a::{comm_ring_1})^x = 1) &
14.9 (odd x --> (- 1::'a)^x = - 1)"
14.10 apply (induct x)
14.11 apply (rule conjI)
14.12 @@ -188,37 +188,37 @@
14.13 done
14.14
14.15 lemma minus_one_even_power [simp]:
14.16 - "even x ==> (- 1::'a::{comm_ring_1,recpower})^x = 1"
14.17 + "even x ==> (- 1::'a::{comm_ring_1})^x = 1"
14.18 using minus_one_even_odd_power by blast
14.19
14.20 lemma minus_one_odd_power [simp]:
14.21 - "odd x ==> (- 1::'a::{comm_ring_1,recpower})^x = - 1"
14.22 + "odd x ==> (- 1::'a::{comm_ring_1})^x = - 1"
14.23 using minus_one_even_odd_power by blast
14.24
14.25 lemma neg_one_even_odd_power:
14.26 - "(even x --> (-1::'a::{number_ring,recpower})^x = 1) &
14.27 + "(even x --> (-1::'a::{number_ring})^x = 1) &
14.28 (odd x --> (-1::'a)^x = -1)"
14.29 apply (induct x)
14.30 apply (simp, simp add: power_Suc)
14.31 done
14.32
14.33 lemma neg_one_even_power [simp]:
14.34 - "even x ==> (-1::'a::{number_ring,recpower})^x = 1"
14.35 + "even x ==> (-1::'a::{number_ring})^x = 1"
14.36 using neg_one_even_odd_power by blast
14.37
14.38 lemma neg_one_odd_power [simp]:
14.39 - "odd x ==> (-1::'a::{number_ring,recpower})^x = -1"
14.40 + "odd x ==> (-1::'a::{number_ring})^x = -1"
14.41 using neg_one_even_odd_power by blast
14.42
14.43 lemma neg_power_if:
14.44 - "(-x::'a::{comm_ring_1,recpower}) ^ n =
14.45 + "(-x::'a::{comm_ring_1}) ^ n =
14.46 (if even n then (x ^ n) else -(x ^ n))"
14.47 apply (induct n)
14.48 apply (simp_all split: split_if_asm add: power_Suc)
14.49 done
14.50
14.51 lemma zero_le_even_power: "even n ==>
14.52 - 0 <= (x::'a::{recpower,ordered_ring_strict}) ^ n"
14.53 + 0 <= (x::'a::{ordered_ring_strict,monoid_mult}) ^ n"
14.54 apply (simp add: even_nat_equiv_def2)
14.55 apply (erule exE)
14.56 apply (erule ssubst)
14.57 @@ -227,12 +227,12 @@
14.58 done
14.59
14.60 lemma zero_le_odd_power: "odd n ==>
14.61 - (0 <= (x::'a::{recpower,ordered_idom}) ^ n) = (0 <= x)"
14.62 + (0 <= (x::'a::{ordered_idom}) ^ n) = (0 <= x)"
14.63 apply (auto simp: odd_nat_equiv_def2 power_Suc power_add zero_le_mult_iff)
14.64 apply (metis field_power_not_zero no_zero_divirors_neq0 order_antisym_conv zero_le_square)
14.65 done
14.66
14.67 -lemma zero_le_power_eq[presburger]: "(0 <= (x::'a::{recpower,ordered_idom}) ^ n) =
14.68 +lemma zero_le_power_eq[presburger]: "(0 <= (x::'a::{ordered_idom}) ^ n) =
14.69 (even n | (odd n & 0 <= x))"
14.70 apply auto
14.71 apply (subst zero_le_odd_power [symmetric])
14.72 @@ -240,19 +240,19 @@
14.73 apply (erule zero_le_even_power)
14.74 done
14.75
14.76 -lemma zero_less_power_eq[presburger]: "(0 < (x::'a::{recpower,ordered_idom}) ^ n) =
14.77 +lemma zero_less_power_eq[presburger]: "(0 < (x::'a::{ordered_idom}) ^ n) =
14.78 (n = 0 | (even n & x ~= 0) | (odd n & 0 < x))"
14.79
14.80 unfolding order_less_le zero_le_power_eq by auto
14.81
14.82 -lemma power_less_zero_eq[presburger]: "((x::'a::{recpower,ordered_idom}) ^ n < 0) =
14.83 +lemma power_less_zero_eq[presburger]: "((x::'a::{ordered_idom}) ^ n < 0) =
14.84 (odd n & x < 0)"
14.85 apply (subst linorder_not_le [symmetric])+
14.86 apply (subst zero_le_power_eq)
14.87 apply auto
14.88 done
14.89
14.90 -lemma power_le_zero_eq[presburger]: "((x::'a::{recpower,ordered_idom}) ^ n <= 0) =
14.91 +lemma power_le_zero_eq[presburger]: "((x::'a::{ordered_idom}) ^ n <= 0) =
14.92 (n ~= 0 & ((odd n & x <= 0) | (even n & x = 0)))"
14.93 apply (subst linorder_not_less [symmetric])+
14.94 apply (subst zero_less_power_eq)
14.95 @@ -260,7 +260,7 @@
14.96 done
14.97
14.98 lemma power_even_abs: "even n ==>
14.99 - (abs (x::'a::{recpower,ordered_idom}))^n = x^n"
14.100 + (abs (x::'a::{ordered_idom}))^n = x^n"
14.101 apply (subst power_abs [symmetric])
14.102 apply (simp add: zero_le_even_power)
14.103 done
14.104 @@ -269,18 +269,18 @@
14.105 by (induct n) auto
14.106
14.107 lemma power_minus_even [simp]: "even n ==>
14.108 - (- x)^n = (x^n::'a::{recpower,comm_ring_1})"
14.109 + (- x)^n = (x^n::'a::{comm_ring_1})"
14.110 apply (subst power_minus)
14.111 apply simp
14.112 done
14.113
14.114 lemma power_minus_odd [simp]: "odd n ==>
14.115 - (- x)^n = - (x^n::'a::{recpower,comm_ring_1})"
14.116 + (- x)^n = - (x^n::'a::{comm_ring_1})"
14.117 apply (subst power_minus)
14.118 apply simp
14.119 done
14.120
14.121 -lemma power_mono_even: fixes x y :: "'a :: {recpower, ordered_idom}"
14.122 +lemma power_mono_even: fixes x y :: "'a :: {ordered_idom}"
14.123 assumes "even n" and "\<bar>x\<bar> \<le> \<bar>y\<bar>"
14.124 shows "x^n \<le> y^n"
14.125 proof -
14.126 @@ -292,7 +292,7 @@
14.127
14.128 lemma odd_pos: "odd (n::nat) \<Longrightarrow> 0 < n" by presburger
14.129
14.130 -lemma power_mono_odd: fixes x y :: "'a :: {recpower, ordered_idom}"
14.131 +lemma power_mono_odd: fixes x y :: "'a :: {ordered_idom}"
14.132 assumes "odd n" and "x \<le> y"
14.133 shows "x^n \<le> y^n"
14.134 proof (cases "y < 0")
14.135 @@ -406,11 +406,11 @@
14.136 subsection {* An Equivalence for @{term [source] "0 \<le> a^n"} *}
14.137
14.138 lemma even_power_le_0_imp_0:
14.139 - "a ^ (2*k) \<le> (0::'a::{ordered_idom,recpower}) ==> a=0"
14.140 + "a ^ (2*k) \<le> (0::'a::{ordered_idom}) ==> a=0"
14.141 by (induct k) (auto simp add: zero_le_mult_iff mult_le_0_iff power_Suc)
14.142
14.143 lemma zero_le_power_iff[presburger]:
14.144 - "(0 \<le> a^n) = (0 \<le> (a::'a::{ordered_idom,recpower}) | even n)"
14.145 + "(0 \<le> a^n) = (0 \<le> (a::'a::{ordered_idom}) | even n)"
14.146 proof cases
14.147 assume even: "even n"
14.148 then obtain k where "n = 2*k"
15.1 --- a/src/HOL/Rational.thy Tue Apr 28 18:42:26 2009 +0200
15.2 +++ b/src/HOL/Rational.thy Tue Apr 28 19:15:50 2009 +0200
15.3 @@ -90,7 +90,7 @@
15.4 and "\<And>a c. Fract 0 a = Fract 0 c"
15.5 by (simp_all add: Fract_def)
15.6
15.7 -instantiation rat :: "{comm_ring_1, recpower}"
15.8 +instantiation rat :: comm_ring_1
15.9 begin
15.10
15.11 definition
15.12 @@ -185,9 +185,6 @@
15.13 by (cases q, cases r, cases s) (simp add: eq_rat algebra_simps)
15.14 next
15.15 show "(0::rat) \<noteq> 1" by (simp add: Zero_rat_def One_rat_def eq_rat)
15.16 -next
15.17 - fix q :: rat show "q * 1 = q"
15.18 - by (cases q) (simp add: One_rat_def eq_rat)
15.19 qed
15.20
15.21 end
15.22 @@ -656,7 +653,7 @@
15.23 by (cases "b = 0") (simp_all add: nonzero_of_rat_divide)
15.24
15.25 lemma of_rat_power:
15.26 - "(of_rat (a ^ n)::'a::{field_char_0,recpower}) = of_rat a ^ n"
15.27 + "(of_rat (a ^ n)::'a::field_char_0) = of_rat a ^ n"
15.28 by (induct n) (simp_all add: of_rat_mult)
15.29
15.30 lemma of_rat_eq_iff [simp]: "(of_rat a = of_rat b) = (a = b)"
15.31 @@ -816,7 +813,7 @@
15.32 done
15.33
15.34 lemma Rats_power [simp]:
15.35 - fixes a :: "'a::{field_char_0,recpower}"
15.36 + fixes a :: "'a::field_char_0"
15.37 shows "a \<in> Rats \<Longrightarrow> a ^ n \<in> Rats"
15.38 apply (auto simp add: Rats_def)
15.39 apply (rule range_eqI)
15.40 @@ -837,6 +834,8 @@
15.41 "q \<in> \<rat> \<Longrightarrow> (\<And>r. P (of_rat r)) \<Longrightarrow> P q"
15.42 by (rule Rats_cases) auto
15.43
15.44 +instance rat :: recpower ..
15.45 +
15.46
15.47 subsection {* Implementation of rational numbers as pairs of integers *}
15.48
16.1 --- a/src/HOL/RealPow.thy Tue Apr 28 18:42:26 2009 +0200
16.2 +++ b/src/HOL/RealPow.thy Tue Apr 28 19:15:50 2009 +0200
16.3 @@ -83,75 +83,6 @@
16.4 declare power_real_number_of [of _ "number_of w", standard, simp]
16.5
16.6
16.7 -subsection {* Properties of Squares *}
16.8 -
16.9 -lemma sum_squares_ge_zero:
16.10 - fixes x y :: "'a::ordered_ring_strict"
16.11 - shows "0 \<le> x * x + y * y"
16.12 -by (intro add_nonneg_nonneg zero_le_square)
16.13 -
16.14 -lemma not_sum_squares_lt_zero:
16.15 - fixes x y :: "'a::ordered_ring_strict"
16.16 - shows "\<not> x * x + y * y < 0"
16.17 -by (simp add: linorder_not_less sum_squares_ge_zero)
16.18 -
16.19 -lemma sum_nonneg_eq_zero_iff:
16.20 - fixes x y :: "'a::pordered_ab_group_add"
16.21 - assumes x: "0 \<le> x" and y: "0 \<le> y"
16.22 - shows "(x + y = 0) = (x = 0 \<and> y = 0)"
16.23 -proof (auto)
16.24 - from y have "x + 0 \<le> x + y" by (rule add_left_mono)
16.25 - also assume "x + y = 0"
16.26 - finally have "x \<le> 0" by simp
16.27 - thus "x = 0" using x by (rule order_antisym)
16.28 -next
16.29 - from x have "0 + y \<le> x + y" by (rule add_right_mono)
16.30 - also assume "x + y = 0"
16.31 - finally have "y \<le> 0" by simp
16.32 - thus "y = 0" using y by (rule order_antisym)
16.33 -qed
16.34 -
16.35 -lemma sum_squares_eq_zero_iff:
16.36 - fixes x y :: "'a::ordered_ring_strict"
16.37 - shows "(x * x + y * y = 0) = (x = 0 \<and> y = 0)"
16.38 -by (simp add: sum_nonneg_eq_zero_iff)
16.39 -
16.40 -lemma sum_squares_le_zero_iff:
16.41 - fixes x y :: "'a::ordered_ring_strict"
16.42 - shows "(x * x + y * y \<le> 0) = (x = 0 \<and> y = 0)"
16.43 -by (simp add: order_le_less not_sum_squares_lt_zero sum_squares_eq_zero_iff)
16.44 -
16.45 -lemma sum_squares_gt_zero_iff:
16.46 - fixes x y :: "'a::ordered_ring_strict"
16.47 - shows "(0 < x * x + y * y) = (x \<noteq> 0 \<or> y \<noteq> 0)"
16.48 -by (simp add: order_less_le sum_squares_ge_zero sum_squares_eq_zero_iff)
16.49 -
16.50 -lemma sum_power2_ge_zero:
16.51 - fixes x y :: "'a::{ordered_idom,recpower}"
16.52 - shows "0 \<le> x\<twosuperior> + y\<twosuperior>"
16.53 -unfolding power2_eq_square by (rule sum_squares_ge_zero)
16.54 -
16.55 -lemma not_sum_power2_lt_zero:
16.56 - fixes x y :: "'a::{ordered_idom,recpower}"
16.57 - shows "\<not> x\<twosuperior> + y\<twosuperior> < 0"
16.58 -unfolding power2_eq_square by (rule not_sum_squares_lt_zero)
16.59 -
16.60 -lemma sum_power2_eq_zero_iff:
16.61 - fixes x y :: "'a::{ordered_idom,recpower}"
16.62 - shows "(x\<twosuperior> + y\<twosuperior> = 0) = (x = 0 \<and> y = 0)"
16.63 -unfolding power2_eq_square by (rule sum_squares_eq_zero_iff)
16.64 -
16.65 -lemma sum_power2_le_zero_iff:
16.66 - fixes x y :: "'a::{ordered_idom,recpower}"
16.67 - shows "(x\<twosuperior> + y\<twosuperior> \<le> 0) = (x = 0 \<and> y = 0)"
16.68 -unfolding power2_eq_square by (rule sum_squares_le_zero_iff)
16.69 -
16.70 -lemma sum_power2_gt_zero_iff:
16.71 - fixes x y :: "'a::{ordered_idom,recpower}"
16.72 - shows "(0 < x\<twosuperior> + y\<twosuperior>) = (x \<noteq> 0 \<or> y \<noteq> 0)"
16.73 -unfolding power2_eq_square by (rule sum_squares_gt_zero_iff)
16.74 -
16.75 -
16.76 subsection{* Squares of Reals *}
16.77
16.78 lemma real_two_squares_add_zero_iff [simp]:
17.1 --- a/src/HOL/RealVector.thy Tue Apr 28 18:42:26 2009 +0200
17.2 +++ b/src/HOL/RealVector.thy Tue Apr 28 19:15:50 2009 +0200
17.3 @@ -259,7 +259,7 @@
17.4 by (simp add: divide_inverse)
17.5
17.6 lemma of_real_power [simp]:
17.7 - "of_real (x ^ n) = (of_real x :: 'a::{real_algebra_1,recpower}) ^ n"
17.8 + "of_real (x ^ n) = (of_real x :: 'a::{real_algebra_1}) ^ n"
17.9 by (induct n) simp_all
17.10
17.11 lemma of_real_eq_iff [simp]: "(of_real x = of_real y) = (x = y)"
17.12 @@ -389,7 +389,7 @@
17.13 done
17.14
17.15 lemma Reals_power [simp]:
17.16 - fixes a :: "'a::{real_algebra_1,recpower}"
17.17 + fixes a :: "'a::{real_algebra_1}"
17.18 shows "a \<in> Reals \<Longrightarrow> a ^ n \<in> Reals"
17.19 apply (auto simp add: Reals_def)
17.20 apply (rule range_eqI)
17.21 @@ -613,7 +613,7 @@
17.22 by (simp add: divide_inverse norm_mult norm_inverse)
17.23
17.24 lemma norm_power_ineq:
17.25 - fixes x :: "'a::{real_normed_algebra_1,recpower}"
17.26 + fixes x :: "'a::{real_normed_algebra_1}"
17.27 shows "norm (x ^ n) \<le> norm x ^ n"
17.28 proof (induct n)
17.29 case 0 show "norm (x ^ 0) \<le> norm x ^ 0" by simp
17.30 @@ -628,7 +628,7 @@
17.31 qed
17.32
17.33 lemma norm_power:
17.34 - fixes x :: "'a::{real_normed_div_algebra,recpower}"
17.35 + fixes x :: "'a::{real_normed_div_algebra}"
17.36 shows "norm (x ^ n) = norm x ^ n"
17.37 by (induct n) (simp_all add: norm_mult)
17.38
18.1 --- a/src/HOL/SEQ.thy Tue Apr 28 18:42:26 2009 +0200
18.2 +++ b/src/HOL/SEQ.thy Tue Apr 28 19:15:50 2009 +0200
18.3 @@ -487,7 +487,7 @@
18.4 by (simp add: LIMSEQ_mult LIMSEQ_inverse divide_inverse)
18.5
18.6 lemma LIMSEQ_pow:
18.7 - fixes a :: "'a::{real_normed_algebra,recpower}"
18.8 + fixes a :: "'a::{power, real_normed_algebra}"
18.9 shows "X ----> a \<Longrightarrow> (\<lambda>n. (X n) ^ m) ----> a ^ m"
18.10 by (induct m) (simp_all add: LIMSEQ_const LIMSEQ_mult)
18.11
18.12 @@ -1394,7 +1394,7 @@
18.13 qed
18.14
18.15 lemma LIMSEQ_power_zero:
18.16 - fixes x :: "'a::{real_normed_algebra_1,recpower}"
18.17 + fixes x :: "'a::{real_normed_algebra_1}"
18.18 shows "norm x < 1 \<Longrightarrow> (\<lambda>n. x ^ n) ----> 0"
18.19 apply (drule LIMSEQ_realpow_zero [OF norm_ge_zero])
18.20 apply (simp only: LIMSEQ_Zseq_iff, erule Zseq_le)
19.1 --- a/src/HOL/Series.thy Tue Apr 28 18:42:26 2009 +0200
19.2 +++ b/src/HOL/Series.thy Tue Apr 28 19:15:50 2009 +0200
19.3 @@ -331,7 +331,7 @@
19.4 lemmas sumr_geometric = geometric_sum [where 'a = real]
19.5
19.6 lemma geometric_sums:
19.7 - fixes x :: "'a::{real_normed_field,recpower}"
19.8 + fixes x :: "'a::{real_normed_field}"
19.9 shows "norm x < 1 \<Longrightarrow> (\<lambda>n. x ^ n) sums (1 / (1 - x))"
19.10 proof -
19.11 assume less_1: "norm x < 1"
19.12 @@ -348,7 +348,7 @@
19.13 qed
19.14
19.15 lemma summable_geometric:
19.16 - fixes x :: "'a::{real_normed_field,recpower}"
19.17 + fixes x :: "'a::{real_normed_field}"
19.18 shows "norm x < 1 \<Longrightarrow> summable (\<lambda>n. x ^ n)"
19.19 by (rule geometric_sums [THEN sums_summable])
19.20
19.21 @@ -434,7 +434,7 @@
19.22 text{*Summability of geometric series for real algebras*}
19.23
19.24 lemma complete_algebra_summable_geometric:
19.25 - fixes x :: "'a::{real_normed_algebra_1,banach,recpower}"
19.26 + fixes x :: "'a::{real_normed_algebra_1,banach}"
19.27 shows "norm x < 1 \<Longrightarrow> summable (\<lambda>n. x ^ n)"
19.28 proof (rule summable_comparison_test)
19.29 show "\<exists>N. \<forall>n\<ge>N. norm (x ^ n) \<le> norm x ^ n"
20.1 --- a/src/HOL/SetInterval.thy Tue Apr 28 18:42:26 2009 +0200
20.2 +++ b/src/HOL/SetInterval.thy Tue Apr 28 19:15:50 2009 +0200
20.3 @@ -855,7 +855,7 @@
20.4
20.5 lemma geometric_sum:
20.6 "x ~= 1 ==> (\<Sum>i=0..<n. x ^ i) =
20.7 - (x ^ n - 1) / (x - 1::'a::{field, recpower})"
20.8 + (x ^ n - 1) / (x - 1::'a::{field})"
20.9 by (induct "n") (simp_all add:field_simps power_Suc)
20.10
20.11 subsection {* The formula for arithmetic sums *}
21.1 --- a/src/HOL/Transcendental.thy Tue Apr 28 18:42:26 2009 +0200
21.2 +++ b/src/HOL/Transcendental.thy Tue Apr 28 19:15:50 2009 +0200
21.3 @@ -14,7 +14,7 @@
21.4 subsection {* Properties of Power Series *}
21.5
21.6 lemma lemma_realpow_diff:
21.7 - fixes y :: "'a::recpower"
21.8 + fixes y :: "'a::monoid_mult"
21.9 shows "p \<le> n \<Longrightarrow> y ^ (Suc n - p) = (y ^ (n - p)) * y"
21.10 proof -
21.11 assume "p \<le> n"
21.12 @@ -23,14 +23,14 @@
21.13 qed
21.14
21.15 lemma lemma_realpow_diff_sumr:
21.16 - fixes y :: "'a::{recpower,comm_semiring_0}" shows
21.17 + fixes y :: "'a::{comm_semiring_0,monoid_mult}" shows
21.18 "(\<Sum>p=0..<Suc n. (x ^ p) * y ^ (Suc n - p)) =
21.19 y * (\<Sum>p=0..<Suc n. (x ^ p) * y ^ (n - p))"
21.20 by (simp add: setsum_right_distrib lemma_realpow_diff mult_ac
21.21 del: setsum_op_ivl_Suc cong: strong_setsum_cong)
21.22
21.23 lemma lemma_realpow_diff_sumr2:
21.24 - fixes y :: "'a::{recpower,comm_ring}" shows
21.25 + fixes y :: "'a::{comm_ring,monoid_mult}" shows
21.26 "x ^ (Suc n) - y ^ (Suc n) =
21.27 (x - y) * (\<Sum>p=0..<Suc n. (x ^ p) * y ^ (n - p))"
21.28 apply (induct n, simp)
21.29 @@ -56,7 +56,7 @@
21.30 x}, then it sums absolutely for @{term z} with @{term "\<bar>z\<bar> < \<bar>x\<bar>"}.*}
21.31
21.32 lemma powser_insidea:
21.33 - fixes x z :: "'a::{real_normed_field,banach,recpower}"
21.34 + fixes x z :: "'a::{real_normed_field,banach}"
21.35 assumes 1: "summable (\<lambda>n. f n * x ^ n)"
21.36 assumes 2: "norm z < norm x"
21.37 shows "summable (\<lambda>n. norm (f n * z ^ n))"
21.38 @@ -108,7 +108,7 @@
21.39 qed
21.40
21.41 lemma powser_inside:
21.42 - fixes f :: "nat \<Rightarrow> 'a::{real_normed_field,banach,recpower}" shows
21.43 + fixes f :: "nat \<Rightarrow> 'a::{real_normed_field,banach}" shows
21.44 "[| summable (%n. f(n) * (x ^ n)); norm z < norm x |]
21.45 ==> summable (%n. f(n) * (z ^ n))"
21.46 by (rule powser_insidea [THEN summable_norm_cancel])
21.47 @@ -347,7 +347,7 @@
21.48 done
21.49
21.50 lemma lemma_termdiff1:
21.51 - fixes z :: "'a :: {recpower,comm_ring}" shows
21.52 + fixes z :: "'a :: {monoid_mult,comm_ring}" shows
21.53 "(\<Sum>p=0..<m. (((z + h) ^ (m - p)) * (z ^ p)) - (z ^ m)) =
21.54 (\<Sum>p=0..<m. (z ^ p) * (((z + h) ^ (m - p)) - (z ^ (m - p))))"
21.55 by(auto simp add: algebra_simps power_add [symmetric] cong: strong_setsum_cong)
21.56 @@ -357,7 +357,7 @@
21.57 by (simp add: setsum_subtractf)
21.58
21.59 lemma lemma_termdiff2:
21.60 - fixes h :: "'a :: {recpower,field}"
21.61 + fixes h :: "'a :: {field}"
21.62 assumes h: "h \<noteq> 0" shows
21.63 "((z + h) ^ n - z ^ n) / h - of_nat n * z ^ (n - Suc 0) =
21.64 h * (\<Sum>p=0..< n - Suc 0. \<Sum>q=0..< n - Suc 0 - p.
21.65 @@ -393,7 +393,7 @@
21.66 done
21.67
21.68 lemma lemma_termdiff3:
21.69 - fixes h z :: "'a::{real_normed_field,recpower}"
21.70 + fixes h z :: "'a::{real_normed_field}"
21.71 assumes 1: "h \<noteq> 0"
21.72 assumes 2: "norm z \<le> K"
21.73 assumes 3: "norm (z + h) \<le> K"
21.74 @@ -433,7 +433,7 @@
21.75 qed
21.76
21.77 lemma lemma_termdiff4:
21.78 - fixes f :: "'a::{real_normed_field,recpower} \<Rightarrow>
21.79 + fixes f :: "'a::{real_normed_field} \<Rightarrow>
21.80 'b::real_normed_vector"
21.81 assumes k: "0 < (k::real)"
21.82 assumes le: "\<And>h. \<lbrakk>h \<noteq> 0; norm h < k\<rbrakk> \<Longrightarrow> norm (f h) \<le> K * norm h"
21.83 @@ -478,7 +478,7 @@
21.84 qed
21.85
21.86 lemma lemma_termdiff5:
21.87 - fixes g :: "'a::{recpower,real_normed_field} \<Rightarrow>
21.88 + fixes g :: "'a::{real_normed_field} \<Rightarrow>
21.89 nat \<Rightarrow> 'b::banach"
21.90 assumes k: "0 < (k::real)"
21.91 assumes f: "summable f"
21.92 @@ -507,7 +507,7 @@
21.93 text{* FIXME: Long proofs*}
21.94
21.95 lemma termdiffs_aux:
21.96 - fixes x :: "'a::{recpower,real_normed_field,banach}"
21.97 + fixes x :: "'a::{real_normed_field,banach}"
21.98 assumes 1: "summable (\<lambda>n. diffs (diffs c) n * K ^ n)"
21.99 assumes 2: "norm x < norm K"
21.100 shows "(\<lambda>h. \<Sum>n. c n * (((x + h) ^ n - x ^ n) / h
21.101 @@ -572,7 +572,7 @@
21.102 qed
21.103
21.104 lemma termdiffs:
21.105 - fixes K x :: "'a::{recpower,real_normed_field,banach}"
21.106 + fixes K x :: "'a::{real_normed_field,banach}"
21.107 assumes 1: "summable (\<lambda>n. c n * K ^ n)"
21.108 assumes 2: "summable (\<lambda>n. (diffs c) n * K ^ n)"
21.109 assumes 3: "summable (\<lambda>n. (diffs (diffs c)) n * K ^ n)"
21.110 @@ -822,11 +822,11 @@
21.111 subsection {* Exponential Function *}
21.112
21.113 definition
21.114 - exp :: "'a \<Rightarrow> 'a::{recpower,real_normed_field,banach}" where
21.115 + exp :: "'a \<Rightarrow> 'a::{real_normed_field,banach}" where
21.116 "exp x = (\<Sum>n. x ^ n /\<^sub>R real (fact n))"
21.117
21.118 lemma summable_exp_generic:
21.119 - fixes x :: "'a::{real_normed_algebra_1,recpower,banach}"
21.120 + fixes x :: "'a::{real_normed_algebra_1,banach}"
21.121 defines S_def: "S \<equiv> \<lambda>n. x ^ n /\<^sub>R real (fact n)"
21.122 shows "summable S"
21.123 proof -
21.124 @@ -856,7 +856,7 @@
21.125 qed
21.126
21.127 lemma summable_norm_exp:
21.128 - fixes x :: "'a::{real_normed_algebra_1,recpower,banach}"
21.129 + fixes x :: "'a::{real_normed_algebra_1,banach}"
21.130 shows "summable (\<lambda>n. norm (x ^ n /\<^sub>R real (fact n)))"
21.131 proof (rule summable_norm_comparison_test [OF exI, rule_format])
21.132 show "summable (\<lambda>n. norm x ^ n /\<^sub>R real (fact n))"
21.133 @@ -901,7 +901,7 @@
21.134 subsubsection {* Properties of the Exponential Function *}
21.135
21.136 lemma powser_zero:
21.137 - fixes f :: "nat \<Rightarrow> 'a::{real_normed_algebra_1,recpower}"
21.138 + fixes f :: "nat \<Rightarrow> 'a::{real_normed_algebra_1}"
21.139 shows "(\<Sum>n. f n * 0 ^ n) = f 0"
21.140 proof -
21.141 have "(\<Sum>n = 0..<1. f n * 0 ^ n) = (\<Sum>n. f n * 0 ^ n)"
21.142 @@ -918,7 +918,7 @@
21.143 del: setsum_cl_ivl_Suc)
21.144
21.145 lemma exp_series_add:
21.146 - fixes x y :: "'a::{real_field,recpower}"
21.147 + fixes x y :: "'a::{real_field}"
21.148 defines S_def: "S \<equiv> \<lambda>x n. x ^ n /\<^sub>R real (fact n)"
21.149 shows "S (x + y) n = (\<Sum>i=0..n. S x i * S y (n - i))"
21.150 proof (induct n)
22.1 --- a/src/HOL/Word/Num_Lemmas.thy Tue Apr 28 18:42:26 2009 +0200
22.2 +++ b/src/HOL/Word/Num_Lemmas.thy Tue Apr 28 19:15:50 2009 +0200
22.3 @@ -45,10 +45,6 @@
22.4 apply (simp add: number_of_eq nat_diff_distrib [symmetric])
22.5 done
22.6
22.7 -lemma of_int_power:
22.8 - "of_int (a ^ n) = (of_int a ^ n :: 'a :: {recpower, comm_ring_1})"
22.9 - by (induct n) (auto simp add: power_Suc)
22.10 -
22.11 lemma zless2: "0 < (2 :: int)" by arith
22.12
22.13 lemmas zless2p [simp] = zless2 [THEN zero_less_power]
23.1 --- a/src/HOL/Word/WordArith.thy Tue Apr 28 18:42:26 2009 +0200
23.2 +++ b/src/HOL/Word/WordArith.thy Tue Apr 28 19:15:50 2009 +0200
23.3 @@ -790,15 +790,14 @@
23.4 instance word :: (len) comm_semiring_1
23.5 by (intro_classes) (simp add: lenw1_zero_neq_one)
23.6
23.7 +instance word :: (len) recpower ..
23.8 +
23.9 instance word :: (len) comm_ring_1 ..
23.10
23.11 instance word :: (len0) comm_semiring_0 ..
23.12
23.13 instance word :: (len0) order ..
23.14
23.15 -instance word :: (len) recpower
23.16 - by (intro_classes) simp_all
23.17 -
23.18 (* note that iszero_def is only for class comm_semiring_1_cancel,
23.19 which requires word length >= 1, ie 'a :: len word *)
23.20 lemma zero_bintrunc: