1.1 --- a/src/HOL/Transcendental.thy Tue Apr 28 15:50:30 2009 +0200
1.2 +++ b/src/HOL/Transcendental.thy Tue Apr 28 15:50:30 2009 +0200
1.3 @@ -14,7 +14,7 @@
1.4 subsection {* Properties of Power Series *}
1.5
1.6 lemma lemma_realpow_diff:
1.7 - fixes y :: "'a::recpower"
1.8 + fixes y :: "'a::monoid_mult"
1.9 shows "p \<le> n \<Longrightarrow> y ^ (Suc n - p) = (y ^ (n - p)) * y"
1.10 proof -
1.11 assume "p \<le> n"
1.12 @@ -23,14 +23,14 @@
1.13 qed
1.14
1.15 lemma lemma_realpow_diff_sumr:
1.16 - fixes y :: "'a::{recpower,comm_semiring_0}" shows
1.17 + fixes y :: "'a::{comm_semiring_0,monoid_mult}" shows
1.18 "(\<Sum>p=0..<Suc n. (x ^ p) * y ^ (Suc n - p)) =
1.19 y * (\<Sum>p=0..<Suc n. (x ^ p) * y ^ (n - p))"
1.20 by (simp add: setsum_right_distrib lemma_realpow_diff mult_ac
1.21 del: setsum_op_ivl_Suc cong: strong_setsum_cong)
1.22
1.23 lemma lemma_realpow_diff_sumr2:
1.24 - fixes y :: "'a::{recpower,comm_ring}" shows
1.25 + fixes y :: "'a::{comm_ring,monoid_mult}" shows
1.26 "x ^ (Suc n) - y ^ (Suc n) =
1.27 (x - y) * (\<Sum>p=0..<Suc n. (x ^ p) * y ^ (n - p))"
1.28 apply (induct n, simp)
1.29 @@ -56,7 +56,7 @@
1.30 x}, then it sums absolutely for @{term z} with @{term "\<bar>z\<bar> < \<bar>x\<bar>"}.*}
1.31
1.32 lemma powser_insidea:
1.33 - fixes x z :: "'a::{real_normed_field,banach,recpower}"
1.34 + fixes x z :: "'a::{real_normed_field,banach}"
1.35 assumes 1: "summable (\<lambda>n. f n * x ^ n)"
1.36 assumes 2: "norm z < norm x"
1.37 shows "summable (\<lambda>n. norm (f n * z ^ n))"
1.38 @@ -108,7 +108,7 @@
1.39 qed
1.40
1.41 lemma powser_inside:
1.42 - fixes f :: "nat \<Rightarrow> 'a::{real_normed_field,banach,recpower}" shows
1.43 + fixes f :: "nat \<Rightarrow> 'a::{real_normed_field,banach}" shows
1.44 "[| summable (%n. f(n) * (x ^ n)); norm z < norm x |]
1.45 ==> summable (%n. f(n) * (z ^ n))"
1.46 by (rule powser_insidea [THEN summable_norm_cancel])
1.47 @@ -347,7 +347,7 @@
1.48 done
1.49
1.50 lemma lemma_termdiff1:
1.51 - fixes z :: "'a :: {recpower,comm_ring}" shows
1.52 + fixes z :: "'a :: {monoid_mult,comm_ring}" shows
1.53 "(\<Sum>p=0..<m. (((z + h) ^ (m - p)) * (z ^ p)) - (z ^ m)) =
1.54 (\<Sum>p=0..<m. (z ^ p) * (((z + h) ^ (m - p)) - (z ^ (m - p))))"
1.55 by(auto simp add: algebra_simps power_add [symmetric] cong: strong_setsum_cong)
1.56 @@ -357,7 +357,7 @@
1.57 by (simp add: setsum_subtractf)
1.58
1.59 lemma lemma_termdiff2:
1.60 - fixes h :: "'a :: {recpower,field}"
1.61 + fixes h :: "'a :: {field}"
1.62 assumes h: "h \<noteq> 0" shows
1.63 "((z + h) ^ n - z ^ n) / h - of_nat n * z ^ (n - Suc 0) =
1.64 h * (\<Sum>p=0..< n - Suc 0. \<Sum>q=0..< n - Suc 0 - p.
1.65 @@ -393,7 +393,7 @@
1.66 done
1.67
1.68 lemma lemma_termdiff3:
1.69 - fixes h z :: "'a::{real_normed_field,recpower}"
1.70 + fixes h z :: "'a::{real_normed_field}"
1.71 assumes 1: "h \<noteq> 0"
1.72 assumes 2: "norm z \<le> K"
1.73 assumes 3: "norm (z + h) \<le> K"
1.74 @@ -433,7 +433,7 @@
1.75 qed
1.76
1.77 lemma lemma_termdiff4:
1.78 - fixes f :: "'a::{real_normed_field,recpower} \<Rightarrow>
1.79 + fixes f :: "'a::{real_normed_field} \<Rightarrow>
1.80 'b::real_normed_vector"
1.81 assumes k: "0 < (k::real)"
1.82 assumes le: "\<And>h. \<lbrakk>h \<noteq> 0; norm h < k\<rbrakk> \<Longrightarrow> norm (f h) \<le> K * norm h"
1.83 @@ -478,7 +478,7 @@
1.84 qed
1.85
1.86 lemma lemma_termdiff5:
1.87 - fixes g :: "'a::{recpower,real_normed_field} \<Rightarrow>
1.88 + fixes g :: "'a::{real_normed_field} \<Rightarrow>
1.89 nat \<Rightarrow> 'b::banach"
1.90 assumes k: "0 < (k::real)"
1.91 assumes f: "summable f"
1.92 @@ -507,7 +507,7 @@
1.93 text{* FIXME: Long proofs*}
1.94
1.95 lemma termdiffs_aux:
1.96 - fixes x :: "'a::{recpower,real_normed_field,banach}"
1.97 + fixes x :: "'a::{real_normed_field,banach}"
1.98 assumes 1: "summable (\<lambda>n. diffs (diffs c) n * K ^ n)"
1.99 assumes 2: "norm x < norm K"
1.100 shows "(\<lambda>h. \<Sum>n. c n * (((x + h) ^ n - x ^ n) / h
1.101 @@ -572,7 +572,7 @@
1.102 qed
1.103
1.104 lemma termdiffs:
1.105 - fixes K x :: "'a::{recpower,real_normed_field,banach}"
1.106 + fixes K x :: "'a::{real_normed_field,banach}"
1.107 assumes 1: "summable (\<lambda>n. c n * K ^ n)"
1.108 assumes 2: "summable (\<lambda>n. (diffs c) n * K ^ n)"
1.109 assumes 3: "summable (\<lambda>n. (diffs (diffs c)) n * K ^ n)"
1.110 @@ -822,11 +822,11 @@
1.111 subsection {* Exponential Function *}
1.112
1.113 definition
1.114 - exp :: "'a \<Rightarrow> 'a::{recpower,real_normed_field,banach}" where
1.115 + exp :: "'a \<Rightarrow> 'a::{real_normed_field,banach}" where
1.116 "exp x = (\<Sum>n. x ^ n /\<^sub>R real (fact n))"
1.117
1.118 lemma summable_exp_generic:
1.119 - fixes x :: "'a::{real_normed_algebra_1,recpower,banach}"
1.120 + fixes x :: "'a::{real_normed_algebra_1,banach}"
1.121 defines S_def: "S \<equiv> \<lambda>n. x ^ n /\<^sub>R real (fact n)"
1.122 shows "summable S"
1.123 proof -
1.124 @@ -856,7 +856,7 @@
1.125 qed
1.126
1.127 lemma summable_norm_exp:
1.128 - fixes x :: "'a::{real_normed_algebra_1,recpower,banach}"
1.129 + fixes x :: "'a::{real_normed_algebra_1,banach}"
1.130 shows "summable (\<lambda>n. norm (x ^ n /\<^sub>R real (fact n)))"
1.131 proof (rule summable_norm_comparison_test [OF exI, rule_format])
1.132 show "summable (\<lambda>n. norm x ^ n /\<^sub>R real (fact n))"
1.133 @@ -901,7 +901,7 @@
1.134 subsubsection {* Properties of the Exponential Function *}
1.135
1.136 lemma powser_zero:
1.137 - fixes f :: "nat \<Rightarrow> 'a::{real_normed_algebra_1,recpower}"
1.138 + fixes f :: "nat \<Rightarrow> 'a::{real_normed_algebra_1}"
1.139 shows "(\<Sum>n. f n * 0 ^ n) = f 0"
1.140 proof -
1.141 have "(\<Sum>n = 0..<1. f n * 0 ^ n) = (\<Sum>n. f n * 0 ^ n)"
1.142 @@ -918,7 +918,7 @@
1.143 del: setsum_cl_ivl_Suc)
1.144
1.145 lemma exp_series_add:
1.146 - fixes x y :: "'a::{real_field,recpower}"
1.147 + fixes x y :: "'a::{real_field}"
1.148 defines S_def: "S \<equiv> \<lambda>x n. x ^ n /\<^sub>R real (fact n)"
1.149 shows "S (x + y) n = (\<Sum>i=0..n. S x i * S y (n - i))"
1.150 proof (induct n)