author | paulson |
Mon, 15 Mar 2004 10:46:19 +0100 | |
changeset 14468 | 6be497cacab5 |
parent 14435 | 9e22eeccf129 |
child 15047 | fa62de5862b9 |
permissions | -rw-r--r-- |
10751 | 1 |
(* Title : HSeries.thy |
2 |
Author : Jacques D. Fleuriot |
|
3 |
Copyright : 1998 University of Cambridge |
|
14413 | 4 |
|
5 |
Converted to Isar and polished by lcp |
|
10751 | 6 |
*) |
7 |
||
14413 | 8 |
header{*Finite Summation and Infinite Series for Hyperreals*} |
10751 | 9 |
|
14413 | 10 |
theory HSeries = Series: |
10751 | 11 |
|
14413 | 12 |
constdefs |
13 |
sumhr :: "(hypnat * hypnat * (nat=>real)) => hypreal" |
|
14 |
"sumhr p == |
|
15 |
(%(M,N,f). Abs_hypreal(\<Union>X \<in> Rep_hypnat(M). \<Union>Y \<in> Rep_hypnat(N). |
|
16 |
hyprel ``{%n::nat. sumr (X n) (Y n) f})) p" |
|
10751 | 17 |
|
14413 | 18 |
NSsums :: "[nat=>real,real] => bool" (infixr "NSsums" 80) |
10751 | 19 |
"f NSsums s == (%n. sumr 0 n f) ----NS> s" |
20 |
||
14413 | 21 |
NSsummable :: "(nat=>real) => bool" |
22 |
"NSsummable f == (\<exists>s. f NSsums s)" |
|
10751 | 23 |
|
14413 | 24 |
NSsuminf :: "(nat=>real) => real" |
10751 | 25 |
"NSsuminf f == (@s. f NSsums s)" |
26 |
||
14413 | 27 |
|
28 |
lemma sumhr: |
|
29 |
"sumhr(Abs_hypnat(hypnatrel``{%n. M n}), |
|
30 |
Abs_hypnat(hypnatrel``{%n. N n}), f) = |
|
31 |
Abs_hypreal(hyprel `` {%n. sumr (M n) (N n) f})" |
|
32 |
apply (simp add: sumhr_def) |
|
33 |
apply (rule arg_cong [where f = Abs_hypreal]) |
|
34 |
apply (auto, ultra) |
|
35 |
done |
|
36 |
||
37 |
text{*Base case in definition of @{term sumr}*} |
|
38 |
lemma sumhr_zero [simp]: "sumhr (m,0,f) = 0" |
|
14468 | 39 |
apply (cases m) |
14413 | 40 |
apply (simp add: hypnat_zero_def sumhr symmetric hypreal_zero_def) |
41 |
done |
|
42 |
||
43 |
text{*Recursive case in definition of @{term sumr}*} |
|
44 |
lemma sumhr_if: |
|
45 |
"sumhr(m,n+1,f) = |
|
46 |
(if n + 1 \<le> m then 0 else sumhr(m,n,f) + ( *fNat* f) n)" |
|
14468 | 47 |
apply (cases m, cases n) |
14413 | 48 |
apply (auto simp add: hypnat_one_def sumhr hypnat_add hypnat_le starfunNat |
49 |
hypreal_add hypreal_zero_def, ultra+) |
|
50 |
done |
|
51 |
||
52 |
lemma sumhr_Suc_zero [simp]: "sumhr (n + 1, n, f) = 0" |
|
14468 | 53 |
apply (cases n) |
14413 | 54 |
apply (simp add: hypnat_one_def sumhr hypnat_add hypreal_zero_def) |
55 |
done |
|
56 |
||
57 |
lemma sumhr_eq_bounds [simp]: "sumhr (n,n,f) = 0" |
|
14468 | 58 |
apply (cases n) |
14413 | 59 |
apply (simp add: sumhr hypreal_zero_def) |
60 |
done |
|
61 |
||
62 |
lemma sumhr_Suc [simp]: "sumhr (m,m + 1,f) = ( *fNat* f) m" |
|
14468 | 63 |
apply (cases m) |
14413 | 64 |
apply (simp add: sumhr hypnat_one_def hypnat_add starfunNat) |
65 |
done |
|
66 |
||
67 |
lemma sumhr_add_lbound_zero [simp]: "sumhr(m+k,k,f) = 0" |
|
14468 | 68 |
apply (cases m, cases k) |
14413 | 69 |
apply (simp add: sumhr hypnat_add hypreal_zero_def) |
70 |
done |
|
71 |
||
72 |
lemma sumhr_add: "sumhr (m,n,f) + sumhr(m,n,g) = sumhr(m,n,%i. f i + g i)" |
|
14468 | 73 |
apply (cases m, cases n) |
14413 | 74 |
apply (simp add: sumhr hypreal_add sumr_add) |
75 |
done |
|
76 |
||
77 |
lemma sumhr_mult: "hypreal_of_real r * sumhr(m,n,f) = sumhr(m,n,%n. r * f n)" |
|
14468 | 78 |
apply (cases m, cases n) |
14413 | 79 |
apply (simp add: sumhr hypreal_of_real_def hypreal_mult sumr_mult) |
80 |
done |
|
81 |
||
82 |
lemma sumhr_split_add: "n < p ==> sumhr(0,n,f) + sumhr(n,p,f) = sumhr(0,p,f)" |
|
14468 | 83 |
apply (cases n, cases p) |
14413 | 84 |
apply (auto elim!: FreeUltrafilterNat_subset simp |
85 |
add: hypnat_zero_def sumhr hypreal_add hypnat_less sumr_split_add) |
|
86 |
done |
|
87 |
||
88 |
lemma sumhr_split_diff: "n<p ==> sumhr(0,p,f) - sumhr(0,n,f) = sumhr(n,p,f)" |
|
89 |
by (drule_tac f1 = f in sumhr_split_add [symmetric], simp) |
|
90 |
||
91 |
lemma sumhr_hrabs: "abs(sumhr(m,n,f)) \<le> sumhr(m,n,%i. abs(f i))" |
|
14468 | 92 |
apply (cases n, cases m) |
14413 | 93 |
apply (simp add: sumhr hypreal_le hypreal_hrabs sumr_rabs) |
94 |
done |
|
95 |
||
96 |
text{* other general version also needed *} |
|
97 |
lemma sumhr_fun_hypnat_eq: |
|
98 |
"(\<forall>r. m \<le> r & r < n --> f r = g r) --> |
|
99 |
sumhr(hypnat_of_nat m, hypnat_of_nat n, f) = |
|
100 |
sumhr(hypnat_of_nat m, hypnat_of_nat n, g)" |
|
101 |
apply (safe, drule sumr_fun_eq) |
|
102 |
apply (simp add: sumhr hypnat_of_nat_eq) |
|
103 |
done |
|
104 |
||
105 |
lemma sumhr_const: "sumhr(0,n,%i. r) = hypreal_of_hypnat n*hypreal_of_real r" |
|
14468 | 106 |
apply (cases n) |
14413 | 107 |
apply (simp add: sumhr hypnat_zero_def hypreal_of_real_def hypreal_of_hypnat hypreal_mult) |
108 |
done |
|
109 |
||
110 |
lemma sumhr_add_mult_const: |
|
111 |
"sumhr(0,n,f) + -(hypreal_of_hypnat n*hypreal_of_real r) = |
|
112 |
sumhr(0,n,%i. f i + -r)" |
|
14468 | 113 |
apply (cases n) |
14413 | 114 |
apply (simp add: sumhr hypnat_zero_def hypreal_of_real_def hypreal_of_hypnat |
115 |
hypreal_mult hypreal_add hypreal_minus sumr_add [symmetric]) |
|
116 |
done |
|
117 |
||
118 |
lemma sumhr_less_bounds_zero [simp]: "n < m ==> sumhr(m,n,f) = 0" |
|
14468 | 119 |
apply (cases m, cases n) |
14413 | 120 |
apply (auto elim: FreeUltrafilterNat_subset |
121 |
simp add: sumhr hypnat_less hypreal_zero_def) |
|
122 |
done |
|
123 |
||
124 |
lemma sumhr_minus: "sumhr(m, n, %i. - f i) = - sumhr(m, n, f)" |
|
14468 | 125 |
apply (cases m, cases n) |
14413 | 126 |
apply (simp add: sumhr hypreal_minus sumr_minus) |
127 |
done |
|
128 |
||
129 |
lemma sumhr_shift_bounds: |
|
130 |
"sumhr(m+hypnat_of_nat k,n+hypnat_of_nat k,f) = sumhr(m,n,%i. f(i + k))" |
|
14468 | 131 |
apply (cases m, cases n) |
14413 | 132 |
apply (simp add: sumhr hypnat_add sumr_shift_bounds hypnat_of_nat_eq) |
133 |
done |
|
134 |
||
135 |
||
136 |
subsection{*Nonstandard Sums*} |
|
137 |
||
138 |
text{*Infinite sums are obtained by summing to some infinite hypernatural |
|
139 |
(such as @{term whn})*} |
|
140 |
lemma sumhr_hypreal_of_hypnat_omega: |
|
141 |
"sumhr(0,whn,%i. 1) = hypreal_of_hypnat whn" |
|
142 |
by (simp add: hypnat_omega_def hypnat_zero_def sumhr hypreal_of_hypnat) |
|
143 |
||
144 |
lemma sumhr_hypreal_omega_minus_one: "sumhr(0, whn, %i. 1) = omega - 1" |
|
145 |
by (simp add: hypnat_omega_def hypnat_zero_def omega_def hypreal_one_def |
|
146 |
sumhr hypreal_diff real_of_nat_Suc) |
|
147 |
||
148 |
lemma sumhr_minus_one_realpow_zero [simp]: |
|
149 |
"sumhr(0, whn + whn, %i. (-1) ^ (i+1)) = 0" |
|
150 |
by (simp del: realpow_Suc |
|
14435
9e22eeccf129
Conversion of Poly to Isar script, and other tidying of HOL/Hyperreal
paulson
parents:
14413
diff
changeset
|
151 |
add: sumhr hypnat_add nat_mult_2 [symmetric] hypreal_zero_def |
14413 | 152 |
hypnat_zero_def hypnat_omega_def) |
153 |
||
154 |
lemma sumhr_interval_const: |
|
155 |
"(\<forall>n. m \<le> Suc n --> f n = r) & m \<le> na |
|
156 |
==> sumhr(hypnat_of_nat m,hypnat_of_nat na,f) = |
|
157 |
(hypreal_of_nat (na - m) * hypreal_of_real r)" |
|
158 |
by (auto dest!: sumr_interval_const |
|
159 |
simp add: hypreal_of_real_def sumhr hypreal_of_nat_eq |
|
160 |
hypnat_of_nat_eq hypreal_of_real_def hypreal_mult) |
|
161 |
||
162 |
lemma starfunNat_sumr: "( *fNat* (%n. sumr 0 n f)) N = sumhr(0,N,f)" |
|
14468 | 163 |
apply (cases N) |
14413 | 164 |
apply (simp add: hypnat_zero_def starfunNat sumhr) |
165 |
done |
|
166 |
||
167 |
lemma sumhr_hrabs_approx [simp]: "sumhr(0, M, f) @= sumhr(0, N, f) |
|
168 |
==> abs (sumhr(M, N, f)) @= 0" |
|
169 |
apply (cut_tac x = M and y = N in linorder_less_linear) |
|
170 |
apply (auto simp add: approx_refl) |
|
171 |
apply (drule approx_sym [THEN approx_minus_iff [THEN iffD1]]) |
|
172 |
apply (auto dest: approx_hrabs |
|
173 |
simp add: sumhr_split_diff diff_minus [symmetric]) |
|
174 |
done |
|
175 |
||
176 |
(*---------------------------------------------------------------- |
|
177 |
infinite sums: Standard and NS theorems |
|
178 |
----------------------------------------------------------------*) |
|
179 |
lemma sums_NSsums_iff: "(f sums l) = (f NSsums l)" |
|
180 |
by (simp add: sums_def NSsums_def LIMSEQ_NSLIMSEQ_iff) |
|
181 |
||
182 |
lemma summable_NSsummable_iff: "(summable f) = (NSsummable f)" |
|
183 |
by (simp add: summable_def NSsummable_def sums_NSsums_iff) |
|
184 |
||
185 |
lemma suminf_NSsuminf_iff: "(suminf f) = (NSsuminf f)" |
|
186 |
by (simp add: suminf_def NSsuminf_def sums_NSsums_iff) |
|
187 |
||
188 |
lemma NSsums_NSsummable: "f NSsums l ==> NSsummable f" |
|
189 |
by (simp add: NSsums_def NSsummable_def, blast) |
|
190 |
||
191 |
lemma NSsummable_NSsums: "NSsummable f ==> f NSsums (NSsuminf f)" |
|
192 |
apply (simp add: NSsummable_def NSsuminf_def) |
|
193 |
apply (blast intro: someI2) |
|
194 |
done |
|
195 |
||
196 |
lemma NSsums_unique: "f NSsums s ==> (s = NSsuminf f)" |
|
197 |
by (simp add: suminf_NSsuminf_iff [symmetric] sums_NSsums_iff sums_unique) |
|
198 |
||
199 |
lemma NSseries_zero: "\<forall>m. n \<le> Suc m --> f(m) = 0 ==> f NSsums (sumr 0 n f)" |
|
200 |
by (simp add: sums_NSsums_iff [symmetric] series_zero) |
|
201 |
||
202 |
lemma NSsummable_NSCauchy: |
|
203 |
"NSsummable f = |
|
204 |
(\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite. abs (sumhr(M,N,f)) @= 0)" |
|
205 |
apply (auto simp add: summable_NSsummable_iff [symmetric] |
|
206 |
summable_convergent_sumr_iff convergent_NSconvergent_iff |
|
207 |
NSCauchy_NSconvergent_iff [symmetric] NSCauchy_def starfunNat_sumr) |
|
208 |
apply (cut_tac x = M and y = N in linorder_less_linear) |
|
209 |
apply (auto simp add: approx_refl) |
|
210 |
apply (rule approx_minus_iff [THEN iffD2, THEN approx_sym]) |
|
211 |
apply (rule_tac [2] approx_minus_iff [THEN iffD2]) |
|
212 |
apply (auto dest: approx_hrabs_zero_cancel |
|
213 |
simp add: sumhr_split_diff diff_minus [symmetric]) |
|
214 |
done |
|
215 |
||
216 |
||
217 |
text{*Terms of a convergent series tend to zero*} |
|
218 |
lemma NSsummable_NSLIMSEQ_zero: "NSsummable f ==> f ----NS> 0" |
|
219 |
apply (auto simp add: NSLIMSEQ_def NSsummable_NSCauchy) |
|
220 |
apply (drule bspec, auto) |
|
221 |
apply (drule_tac x = "N + 1 " in bspec) |
|
222 |
apply (auto intro: HNatInfinite_add_one approx_hrabs_zero_cancel) |
|
223 |
done |
|
224 |
||
225 |
text{* Easy to prove stsandard case now *} |
|
226 |
lemma summable_LIMSEQ_zero: "summable f ==> f ----> 0" |
|
227 |
by (simp add: summable_NSsummable_iff LIMSEQ_NSLIMSEQ_iff NSsummable_NSLIMSEQ_zero) |
|
228 |
||
229 |
text{*Nonstandard comparison test*} |
|
230 |
lemma NSsummable_comparison_test: |
|
231 |
"[| \<exists>N. \<forall>n. N \<le> n --> abs(f n) \<le> g n; NSsummable g |] ==> NSsummable f" |
|
232 |
by (auto intro: summable_comparison_test |
|
233 |
simp add: summable_NSsummable_iff [symmetric]) |
|
234 |
||
235 |
lemma NSsummable_rabs_comparison_test: |
|
236 |
"[| \<exists>N. \<forall>n. N \<le> n --> abs(f n) \<le> g n; NSsummable g |] |
|
237 |
==> NSsummable (%k. abs (f k))" |
|
238 |
apply (rule NSsummable_comparison_test) |
|
239 |
apply (auto simp add: abs_idempotent) |
|
240 |
done |
|
241 |
||
242 |
ML |
|
243 |
{* |
|
244 |
val sumhr = thm "sumhr"; |
|
245 |
val sumhr_zero = thm "sumhr_zero"; |
|
246 |
val sumhr_if = thm "sumhr_if"; |
|
247 |
val sumhr_Suc_zero = thm "sumhr_Suc_zero"; |
|
248 |
val sumhr_eq_bounds = thm "sumhr_eq_bounds"; |
|
249 |
val sumhr_Suc = thm "sumhr_Suc"; |
|
250 |
val sumhr_add_lbound_zero = thm "sumhr_add_lbound_zero"; |
|
251 |
val sumhr_add = thm "sumhr_add"; |
|
252 |
val sumhr_mult = thm "sumhr_mult"; |
|
253 |
val sumhr_split_add = thm "sumhr_split_add"; |
|
254 |
val sumhr_split_diff = thm "sumhr_split_diff"; |
|
255 |
val sumhr_hrabs = thm "sumhr_hrabs"; |
|
256 |
val sumhr_fun_hypnat_eq = thm "sumhr_fun_hypnat_eq"; |
|
257 |
val sumhr_const = thm "sumhr_const"; |
|
258 |
val sumhr_add_mult_const = thm "sumhr_add_mult_const"; |
|
259 |
val sumhr_less_bounds_zero = thm "sumhr_less_bounds_zero"; |
|
260 |
val sumhr_minus = thm "sumhr_minus"; |
|
261 |
val sumhr_shift_bounds = thm "sumhr_shift_bounds"; |
|
262 |
val sumhr_hypreal_of_hypnat_omega = thm "sumhr_hypreal_of_hypnat_omega"; |
|
263 |
val sumhr_hypreal_omega_minus_one = thm "sumhr_hypreal_omega_minus_one"; |
|
264 |
val sumhr_minus_one_realpow_zero = thm "sumhr_minus_one_realpow_zero"; |
|
265 |
val sumhr_interval_const = thm "sumhr_interval_const"; |
|
266 |
val starfunNat_sumr = thm "starfunNat_sumr"; |
|
267 |
val sumhr_hrabs_approx = thm "sumhr_hrabs_approx"; |
|
268 |
val sums_NSsums_iff = thm "sums_NSsums_iff"; |
|
269 |
val summable_NSsummable_iff = thm "summable_NSsummable_iff"; |
|
270 |
val suminf_NSsuminf_iff = thm "suminf_NSsuminf_iff"; |
|
271 |
val NSsums_NSsummable = thm "NSsums_NSsummable"; |
|
272 |
val NSsummable_NSsums = thm "NSsummable_NSsums"; |
|
273 |
val NSsums_unique = thm "NSsums_unique"; |
|
274 |
val NSseries_zero = thm "NSseries_zero"; |
|
275 |
val NSsummable_NSCauchy = thm "NSsummable_NSCauchy"; |
|
276 |
val NSsummable_NSLIMSEQ_zero = thm "NSsummable_NSLIMSEQ_zero"; |
|
277 |
val summable_LIMSEQ_zero = thm "summable_LIMSEQ_zero"; |
|
278 |
val NSsummable_comparison_test = thm "NSsummable_comparison_test"; |
|
279 |
val NSsummable_rabs_comparison_test = thm "NSsummable_rabs_comparison_test"; |
|
280 |
*} |
|
281 |
||
10751 | 282 |
end |