author | paulson |
Fri, 16 Nov 2001 18:24:11 +0100 | |
changeset 12224 | 02df7cbe7d25 |
parent 12018 | ec054019c910 |
child 13810 | c3fbfd472365 |
permissions | -rw-r--r-- |
10751 | 1 |
(* Title : HSeries.ML |
2 |
Author : Jacques D. Fleuriot |
|
3 |
Copyright : 1998 University of Cambridge |
|
4 |
Description : Finite summation and infinite series |
|
5 |
for hyperreals |
|
6 |
*) |
|
7 |
||
8 |
Goalw [sumhr_def] |
|
9 |
"sumhr(M,N,f) = \ |
|
10 |
\ Abs_hypreal(UN X:Rep_hypnat(M). UN Y: Rep_hypnat(N). \ |
|
10834 | 11 |
\ hyprel ``{%n::nat. sumr (X n) (Y n) f})"; |
10751 | 12 |
by (Auto_tac); |
13 |
qed "sumhr_iff"; |
|
14 |
||
15 |
Goalw [sumhr_def] |
|
10834 | 16 |
"sumhr(Abs_hypnat(hypnatrel``{%n. M n}), \ |
17 |
\ Abs_hypnat(hypnatrel``{%n. N n}), f) = \ |
|
18 |
\ Abs_hypreal(hyprel `` {%n. sumr (M n) (N n) f})"; |
|
10751 | 19 |
by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1); |
20 |
by (Auto_tac THEN Ultra_tac 1); |
|
21 |
qed "sumhr"; |
|
22 |
||
23 |
(*------------------------------------------------------- |
|
24 |
lcp's suggestion: exploit pattern matching |
|
25 |
facilities and use as definition instead (to do) |
|
26 |
-------------------------------------------------------*) |
|
27 |
Goalw [sumhr_def] |
|
28 |
"sumhr p = (%(M,N,f). Abs_hypreal(UN X:Rep_hypnat(M). \ |
|
29 |
\ UN Y: Rep_hypnat(N). \ |
|
10834 | 30 |
\ hyprel ``{%n::nat. sumr (X n) (Y n) f})) p"; |
10751 | 31 |
by (res_inst_tac [("p","p")] PairE 1); |
32 |
by (res_inst_tac [("p","y")] PairE 1); |
|
33 |
by (Auto_tac); |
|
34 |
qed "sumhr_iff2"; |
|
35 |
||
36 |
(* Theorem corresponding to base case in def of sumr *) |
|
37 |
Goalw [hypnat_zero_def] |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
38 |
"sumhr (m,0,f) = 0"; |
10751 | 39 |
by (res_inst_tac [("z","m")] eq_Abs_hypnat 1); |
40 |
by (auto_tac (claset(), |
|
41 |
simpset() addsimps [sumhr, symmetric hypreal_zero_def])); |
|
42 |
qed "sumhr_zero"; |
|
43 |
Addsimps [sumhr_zero]; |
|
44 |
||
45 |
(* Theorem corresponding to recursive case in def of sumr *) |
|
46 |
Goalw [hypnat_one_def] |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
47 |
"sumhr(m,n+(1::hypnat),f) = (if n + (1::hypnat) <= m then 0 \ |
10751 | 48 |
\ else sumhr(m,n,f) + (*fNat* f) n)"; |
49 |
by (res_inst_tac [("z","m")] eq_Abs_hypnat 1); |
|
50 |
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); |
|
51 |
by (auto_tac (claset(), |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
52 |
simpset() addsimps [sumhr, hypnat_add,hypnat_le,starfunNat,hypreal_add, |
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
53 |
hypreal_zero_def])); |
10751 | 54 |
by (ALLGOALS(Ultra_tac)); |
55 |
qed "sumhr_if"; |
|
56 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
57 |
Goalw [hypnat_one_def] "sumhr (n + (1::hypnat), n, f) = 0"; |
10751 | 58 |
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); |
59 |
by (auto_tac (claset(), |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
60 |
simpset() addsimps [sumhr, hypnat_add, hypreal_zero_def])); |
10751 | 61 |
qed "sumhr_Suc_zero"; |
62 |
Addsimps [sumhr_Suc_zero]; |
|
63 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
64 |
Goal "sumhr (n,n,f) = 0"; |
10751 | 65 |
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); |
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
66 |
by (auto_tac (claset(), simpset() addsimps [sumhr, hypreal_zero_def])); |
10751 | 67 |
qed "sumhr_eq_bounds"; |
68 |
Addsimps [sumhr_eq_bounds]; |
|
69 |
||
70 |
Goalw [hypnat_one_def] |
|
11713
883d559b0b8c
sane numerals (stage 3): provide generic "1" on all number types;
wenzelm
parents:
11701
diff
changeset
|
71 |
"sumhr (m,m + (1::hypnat),f) = (*fNat* f) m"; |
10751 | 72 |
by (res_inst_tac [("z","m")] eq_Abs_hypnat 1); |
73 |
by (auto_tac (claset(), |
|
74 |
simpset() addsimps [sumhr, hypnat_add,starfunNat])); |
|
75 |
qed "sumhr_Suc"; |
|
76 |
Addsimps [sumhr_Suc]; |
|
77 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
78 |
Goal "sumhr(m+k,k,f) = 0"; |
10751 | 79 |
by (res_inst_tac [("z","m")] eq_Abs_hypnat 1); |
80 |
by (res_inst_tac [("z","k")] eq_Abs_hypnat 1); |
|
81 |
by (auto_tac (claset(), |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
82 |
simpset() addsimps [sumhr, hypnat_add, hypreal_zero_def])); |
10751 | 83 |
qed "sumhr_add_lbound_zero"; |
84 |
Addsimps [sumhr_add_lbound_zero]; |
|
85 |
||
86 |
Goal "sumhr (m,n,f) + sumhr(m,n,g) = sumhr(m,n,%i. f i + g i)"; |
|
87 |
by (res_inst_tac [("z","m")] eq_Abs_hypnat 1); |
|
88 |
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); |
|
89 |
by (auto_tac (claset(), |
|
90 |
simpset() addsimps [sumhr, hypreal_add,sumr_add])); |
|
91 |
qed "sumhr_add"; |
|
92 |
||
93 |
Goalw [hypreal_of_real_def] |
|
94 |
"hypreal_of_real r * sumhr(m,n,f) = sumhr(m,n,%n. r * f n)"; |
|
95 |
by (res_inst_tac [("z","m")] eq_Abs_hypnat 1); |
|
96 |
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); |
|
97 |
by (auto_tac (claset(), |
|
98 |
simpset() addsimps [sumhr, hypreal_mult,sumr_mult])); |
|
99 |
qed "sumhr_mult"; |
|
100 |
||
101 |
Goalw [hypnat_zero_def] |
|
102 |
"n < p ==> sumhr (0,n,f) + sumhr (n,p,f) = sumhr (0,p,f)"; |
|
103 |
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); |
|
104 |
by (res_inst_tac [("z","p")] eq_Abs_hypnat 1); |
|
105 |
by (auto_tac (claset() addSEs [FreeUltrafilterNat_subset], |
|
106 |
simpset() addsimps [sumhr,hypreal_add,hypnat_less, sumr_split_add])); |
|
107 |
qed "sumhr_split_add"; |
|
108 |
||
109 |
(*FIXME delete*) |
|
110 |
Goal "n < p ==> sumhr (0, p, f) + - sumhr (0, n, f) = sumhr (n,p,f)"; |
|
111 |
by (dres_inst_tac [("f1","f")] (sumhr_split_add RS sym) 1); |
|
112 |
by (Asm_simp_tac 1); |
|
113 |
qed "sumhr_split_add_minus"; |
|
114 |
||
115 |
Goal "n < p ==> sumhr (0, p, f) - sumhr (0, n, f) = sumhr (n,p,f)"; |
|
116 |
by (dres_inst_tac [("f1","f")] (sumhr_split_add RS sym) 1); |
|
117 |
by (Asm_simp_tac 1); |
|
118 |
qed "sumhr_split_diff"; |
|
119 |
||
120 |
Goal "abs(sumhr(m,n,f)) <= sumhr(m,n,%i. abs(f i))"; |
|
121 |
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); |
|
122 |
by (res_inst_tac [("z","m")] eq_Abs_hypnat 1); |
|
123 |
by (auto_tac (claset(), |
|
124 |
simpset() addsimps [sumhr, hypreal_le,hypreal_hrabs,sumr_rabs])); |
|
125 |
qed "sumhr_hrabs"; |
|
126 |
||
127 |
(* other general version also needed *) |
|
128 |
Goalw [hypnat_of_nat_def] |
|
129 |
"(ALL r. m <= r & r < n --> f r = g r) --> \ |
|
130 |
\ sumhr(hypnat_of_nat m, hypnat_of_nat n, f) = \ |
|
131 |
\ sumhr(hypnat_of_nat m, hypnat_of_nat n, g)"; |
|
132 |
by (Step_tac 1 THEN dtac sumr_fun_eq 1); |
|
133 |
by (auto_tac (claset(), simpset() addsimps [sumhr])); |
|
134 |
qed "sumhr_fun_hypnat_eq"; |
|
135 |
||
136 |
Goalw [hypnat_zero_def,hypreal_of_real_def] |
|
137 |
"sumhr(0,n,%i. r) = hypreal_of_hypnat n*hypreal_of_real r"; |
|
138 |
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); |
|
139 |
by (asm_simp_tac |
|
140 |
(simpset() addsimps [sumhr, hypreal_of_hypnat,hypreal_mult]) 1); |
|
141 |
qed "sumhr_const"; |
|
142 |
||
143 |
Goalw [hypnat_zero_def,hypreal_of_real_def] |
|
144 |
"sumhr(0,n,f) + -(hypreal_of_hypnat n*hypreal_of_real r) = \ |
|
145 |
\ sumhr(0,n,%i. f i + -r)"; |
|
146 |
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); |
|
147 |
by (asm_simp_tac (simpset() addsimps [sumhr, |
|
148 |
hypreal_of_hypnat,hypreal_mult,hypreal_add, |
|
149 |
hypreal_minus,sumr_add RS sym]) 1); |
|
150 |
qed "sumhr_add_mult_const"; |
|
151 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
152 |
Goal "n < m ==> sumhr (m,n,f) = 0"; |
10751 | 153 |
by (res_inst_tac [("z","m")] eq_Abs_hypnat 1); |
154 |
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); |
|
155 |
by (auto_tac (claset() addEs [FreeUltrafilterNat_subset], |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
156 |
simpset() addsimps [sumhr,hypnat_less, hypreal_zero_def])); |
10751 | 157 |
qed "sumhr_less_bounds_zero"; |
158 |
Addsimps [sumhr_less_bounds_zero]; |
|
159 |
||
160 |
Goal "sumhr(m, n, %i. - f i) = - sumhr(m, n, f)"; |
|
161 |
by (res_inst_tac [("z","m")] eq_Abs_hypnat 1); |
|
162 |
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); |
|
163 |
by (auto_tac (claset(), simpset() addsimps [sumhr, hypreal_minus,sumr_minus])); |
|
164 |
qed "sumhr_minus"; |
|
165 |
||
166 |
Goalw [hypnat_of_nat_def] |
|
167 |
"sumhr(m+hypnat_of_nat k,n+hypnat_of_nat k,f) = sumhr(m,n,%i. f(i + k))"; |
|
168 |
by (res_inst_tac [("z","m")] eq_Abs_hypnat 1); |
|
169 |
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); |
|
170 |
by (auto_tac (claset(), |
|
171 |
simpset() addsimps [sumhr, hypnat_add,sumr_shift_bounds])); |
|
172 |
qed "sumhr_shift_bounds"; |
|
173 |
||
174 |
(*------------------------------------------------------------------ |
|
175 |
Theorems about NS sums - infinite sums are obtained |
|
176 |
by summing to some infinite hypernatural (such as whn) |
|
177 |
-----------------------------------------------------------------*) |
|
178 |
Goalw [hypnat_omega_def,hypnat_zero_def] |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
179 |
"sumhr(0,whn,%i. 1) = hypreal_of_hypnat whn"; |
10751 | 180 |
by (auto_tac (claset(), |
181 |
simpset() addsimps [sumhr, hypreal_of_hypnat])); |
|
182 |
qed "sumhr_hypreal_of_hypnat_omega"; |
|
183 |
||
184 |
Goalw [hypnat_omega_def,hypnat_zero_def,omega_def] |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
185 |
"sumhr(0, whn, %i. 1) = omega - 1"; |
10751 | 186 |
by (simp_tac (HOL_ss addsimps |
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
187 |
[hypreal_numeral_1_eq_1, hypreal_one_def]) 1); |
10751 | 188 |
by (auto_tac (claset(), |
10778
2c6605049646
more tidying, especially to remove real_of_posnat
paulson
parents:
10751
diff
changeset
|
189 |
simpset() addsimps [sumhr, hypreal_diff, real_of_nat_Suc])); |
10751 | 190 |
qed "sumhr_hypreal_omega_minus_one"; |
191 |
||
192 |
Goalw [hypnat_zero_def, hypnat_omega_def] |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
193 |
"sumhr(0, whn + whn, %i. (-1) ^ (i+1)) = 0"; |
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
194 |
by (simp_tac (simpset() delsimps [realpow_Suc] |
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
195 |
addsimps [sumhr,hypnat_add,double_lemma, hypreal_zero_def]) 1); |
10751 | 196 |
qed "sumhr_minus_one_realpow_zero"; |
197 |
Addsimps [sumhr_minus_one_realpow_zero]; |
|
198 |
||
199 |
Goalw [hypnat_of_nat_def,hypreal_of_real_def] |
|
200 |
"(ALL n. m <= Suc n --> f n = r) & m <= na \ |
|
201 |
\ ==> sumhr(hypnat_of_nat m,hypnat_of_nat na,f) = \ |
|
202 |
\ (hypreal_of_nat (na - m) * hypreal_of_real r)"; |
|
203 |
by (auto_tac (claset() addSDs [sumr_interval_const], |
|
10778
2c6605049646
more tidying, especially to remove real_of_posnat
paulson
parents:
10751
diff
changeset
|
204 |
simpset() addsimps [sumhr,hypreal_of_nat_def, |
2c6605049646
more tidying, especially to remove real_of_posnat
paulson
parents:
10751
diff
changeset
|
205 |
hypreal_of_real_def, hypreal_mult])); |
10751 | 206 |
qed "sumhr_interval_const"; |
207 |
||
208 |
Goalw [hypnat_zero_def] |
|
209 |
"(*fNat* (%n. sumr 0 n f)) N = sumhr(0,N,f)"; |
|
210 |
by (res_inst_tac [("z","N")] eq_Abs_hypnat 1); |
|
211 |
by (asm_full_simp_tac (simpset() addsimps [starfunNat,sumhr]) 1); |
|
212 |
qed "starfunNat_sumr"; |
|
213 |
||
214 |
Goal "sumhr (0, M, f) @= sumhr (0, N, f) \ |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
215 |
\ ==> abs (sumhr (M, N, f)) @= 0"; |
10751 | 216 |
by (cut_inst_tac [("x","M"),("y","N")] hypnat_linear 1); |
10919
144ede948e58
renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents:
10834
diff
changeset
|
217 |
by (auto_tac (claset(), simpset() addsimps [approx_refl])); |
144ede948e58
renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents:
10834
diff
changeset
|
218 |
by (dtac (approx_sym RS (approx_minus_iff RS iffD1)) 1); |
144ede948e58
renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents:
10834
diff
changeset
|
219 |
by (auto_tac (claset() addDs [approx_hrabs], |
10751 | 220 |
simpset() addsimps [sumhr_split_add_minus])); |
10919
144ede948e58
renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents:
10834
diff
changeset
|
221 |
qed "sumhr_hrabs_approx"; |
144ede948e58
renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents:
10834
diff
changeset
|
222 |
Addsimps [sumhr_hrabs_approx]; |
10751 | 223 |
|
224 |
(*---------------------------------------------------------------- |
|
225 |
infinite sums: Standard and NS theorems |
|
226 |
----------------------------------------------------------------*) |
|
227 |
Goalw [sums_def,NSsums_def] "(f sums l) = (f NSsums l)"; |
|
228 |
by (simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff]) 1); |
|
229 |
qed "sums_NSsums_iff"; |
|
230 |
||
231 |
Goalw [summable_def,NSsummable_def] |
|
232 |
"(summable f) = (NSsummable f)"; |
|
233 |
by (simp_tac (simpset() addsimps [sums_NSsums_iff]) 1); |
|
234 |
qed "summable_NSsummable_iff"; |
|
235 |
||
236 |
Goalw [suminf_def,NSsuminf_def] |
|
237 |
"(suminf f) = (NSsuminf f)"; |
|
238 |
by (simp_tac (simpset() addsimps [sums_NSsums_iff]) 1); |
|
239 |
qed "suminf_NSsuminf_iff"; |
|
240 |
||
241 |
Goalw [NSsums_def,NSsummable_def] |
|
242 |
"f NSsums l ==> NSsummable f"; |
|
243 |
by (Blast_tac 1); |
|
244 |
qed "NSsums_NSsummable"; |
|
245 |
||
246 |
Goalw [NSsummable_def,NSsuminf_def] |
|
247 |
"NSsummable f ==> f NSsums (NSsuminf f)"; |
|
248 |
by (blast_tac (claset() addIs [someI2]) 1); |
|
249 |
qed "NSsummable_NSsums"; |
|
250 |
||
251 |
Goal "f NSsums s ==> (s = NSsuminf f)"; |
|
252 |
by (asm_full_simp_tac |
|
253 |
(simpset() addsimps [suminf_NSsuminf_iff RS sym,sums_NSsums_iff, |
|
254 |
sums_unique]) 1); |
|
255 |
qed "NSsums_unique"; |
|
256 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
257 |
Goal "ALL m. n <= Suc m --> f(m) = 0 ==> f NSsums (sumr 0 n f)"; |
10751 | 258 |
by (asm_simp_tac (simpset() addsimps [sums_NSsums_iff RS sym, series_zero]) 1); |
259 |
qed "NSseries_zero"; |
|
260 |
||
261 |
Goal "NSsummable f = \ |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
262 |
\ (ALL M: HNatInfinite. ALL N: HNatInfinite. abs (sumhr(M,N,f)) @= 0)"; |
10751 | 263 |
by (auto_tac (claset(), |
264 |
simpset() addsimps [summable_NSsummable_iff RS sym, |
|
265 |
summable_convergent_sumr_iff, convergent_NSconvergent_iff, |
|
266 |
NSCauchy_NSconvergent_iff RS sym, NSCauchy_def, |
|
267 |
starfunNat_sumr])); |
|
268 |
by (cut_inst_tac [("x","M"),("y","N")] hypnat_linear 1); |
|
10919
144ede948e58
renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents:
10834
diff
changeset
|
269 |
by (auto_tac (claset(), simpset() addsimps [approx_refl])); |
144ede948e58
renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents:
10834
diff
changeset
|
270 |
by (rtac ((approx_minus_iff RS iffD2) RS approx_sym) 1); |
144ede948e58
renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents:
10834
diff
changeset
|
271 |
by (rtac (approx_minus_iff RS iffD2) 2); |
144ede948e58
renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents:
10834
diff
changeset
|
272 |
by (auto_tac (claset() addDs [approx_hrabs_zero_cancel], |
10751 | 273 |
simpset() addsimps [sumhr_split_add_minus])); |
274 |
qed "NSsummable_NSCauchy"; |
|
275 |
||
276 |
(*------------------------------------------------------------------- |
|
277 |
Terms of a convergent series tend to zero |
|
278 |
-------------------------------------------------------------------*) |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
279 |
Goalw [NSLIMSEQ_def] "NSsummable f ==> f ----NS> 0"; |
10751 | 280 |
by (auto_tac (claset(), simpset() addsimps [NSsummable_NSCauchy])); |
281 |
by (dtac bspec 1 THEN Auto_tac); |
|
11713
883d559b0b8c
sane numerals (stage 3): provide generic "1" on all number types;
wenzelm
parents:
11701
diff
changeset
|
282 |
by (dres_inst_tac [("x","N + (1::hypnat)")] bspec 1); |
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
283 |
by (auto_tac (claset() addIs [HNatInfinite_add_one, approx_hrabs_zero_cancel], |
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
284 |
simpset())); |
10751 | 285 |
qed "NSsummable_NSLIMSEQ_zero"; |
286 |
||
287 |
(* Easy to prove stsandard case now *) |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
288 |
Goal "summable f ==> f ----> 0"; |
10751 | 289 |
by (auto_tac (claset(), |
290 |
simpset() addsimps [summable_NSsummable_iff, |
|
291 |
LIMSEQ_NSLIMSEQ_iff, NSsummable_NSLIMSEQ_zero])); |
|
292 |
qed "summable_LIMSEQ_zero"; |
|
293 |
||
294 |
(*------------------------------------------------------------------- |
|
295 |
NS Comparison test |
|
296 |
-------------------------------------------------------------------*) |
|
297 |
||
298 |
Goal "[| EX N. ALL n. N <= n --> abs(f n) <= g n; \ |
|
299 |
\ NSsummable g \ |
|
300 |
\ |] ==> NSsummable f"; |
|
301 |
by (auto_tac (claset() addIs [summable_comparison_test], |
|
302 |
simpset() addsimps [summable_NSsummable_iff RS sym])); |
|
303 |
qed "NSsummable_comparison_test"; |
|
304 |
||
305 |
Goal "[| EX N. ALL n. N <= n --> abs(f n) <= g n; \ |
|
306 |
\ NSsummable g \ |
|
307 |
\ |] ==> NSsummable (%k. abs (f k))"; |
|
308 |
by (rtac NSsummable_comparison_test 1); |
|
309 |
by (auto_tac (claset(), simpset() addsimps [abs_idempotent])); |
|
310 |
qed "NSsummable_rabs_comparison_test"; |