189 by (auto_tac (claset(), |
189 by (auto_tac (claset(), |
190 simpset() addsimps [sumhr, hypreal_of_hypnat])); |
190 simpset() addsimps [sumhr, hypreal_of_hypnat])); |
191 qed "sumhr_hypreal_of_hypnat_omega"; |
191 qed "sumhr_hypreal_of_hypnat_omega"; |
192 |
192 |
193 Goalw [hypnat_omega_def,hypnat_zero_def,omega_def] |
193 Goalw [hypnat_omega_def,hypnat_zero_def,omega_def] |
194 "sumhr(0, whn, %i. #1) = whr - #1"; |
194 "sumhr(0, whn, %i. #1) = omega - #1"; |
195 by (simp_tac (HOL_ss addsimps |
195 by (simp_tac (HOL_ss addsimps |
196 [one_eq_numeral_1 RS sym, hypreal_one_def]) 1); |
196 [one_eq_numeral_1 RS sym, hypreal_one_def]) 1); |
197 by (auto_tac (claset(), |
197 by (auto_tac (claset(), |
198 simpset() addsimps [sumhr, hypreal_diff, real_of_nat_Suc])); |
198 simpset() addsimps [sumhr, hypreal_diff, real_of_nat_Suc])); |
199 qed "sumhr_hypreal_omega_minus_one"; |
199 qed "sumhr_hypreal_omega_minus_one"; |
222 qed "starfunNat_sumr"; |
222 qed "starfunNat_sumr"; |
223 |
223 |
224 Goal "sumhr (0, M, f) @= sumhr (0, N, f) \ |
224 Goal "sumhr (0, M, f) @= sumhr (0, N, f) \ |
225 \ ==> abs (sumhr (M, N, f)) @= #0"; |
225 \ ==> abs (sumhr (M, N, f)) @= #0"; |
226 by (cut_inst_tac [("x","M"),("y","N")] hypnat_linear 1); |
226 by (cut_inst_tac [("x","M"),("y","N")] hypnat_linear 1); |
227 by (auto_tac (claset(), simpset() addsimps [inf_close_refl])); |
227 by (auto_tac (claset(), simpset() addsimps [approx_refl])); |
228 by (dtac (inf_close_sym RS (inf_close_minus_iff RS iffD1)) 1); |
228 by (dtac (approx_sym RS (approx_minus_iff RS iffD1)) 1); |
229 by (auto_tac (claset() addDs [inf_close_hrabs], |
229 by (auto_tac (claset() addDs [approx_hrabs], |
230 simpset() addsimps [sumhr_split_add_minus])); |
230 simpset() addsimps [sumhr_split_add_minus])); |
231 qed "sumhr_hrabs_inf_close"; |
231 qed "sumhr_hrabs_approx"; |
232 Addsimps [sumhr_hrabs_inf_close]; |
232 Addsimps [sumhr_hrabs_approx]; |
233 |
233 |
234 (*---------------------------------------------------------------- |
234 (*---------------------------------------------------------------- |
235 infinite sums: Standard and NS theorems |
235 infinite sums: Standard and NS theorems |
236 ----------------------------------------------------------------*) |
236 ----------------------------------------------------------------*) |
237 Goalw [sums_def,NSsums_def] "(f sums l) = (f NSsums l)"; |
237 Goalw [sums_def,NSsums_def] "(f sums l) = (f NSsums l)"; |
274 simpset() addsimps [summable_NSsummable_iff RS sym, |
274 simpset() addsimps [summable_NSsummable_iff RS sym, |
275 summable_convergent_sumr_iff, convergent_NSconvergent_iff, |
275 summable_convergent_sumr_iff, convergent_NSconvergent_iff, |
276 NSCauchy_NSconvergent_iff RS sym, NSCauchy_def, |
276 NSCauchy_NSconvergent_iff RS sym, NSCauchy_def, |
277 starfunNat_sumr])); |
277 starfunNat_sumr])); |
278 by (cut_inst_tac [("x","M"),("y","N")] hypnat_linear 1); |
278 by (cut_inst_tac [("x","M"),("y","N")] hypnat_linear 1); |
279 by (auto_tac (claset(), simpset() addsimps [inf_close_refl])); |
279 by (auto_tac (claset(), simpset() addsimps [approx_refl])); |
280 by (rtac ((inf_close_minus_iff RS iffD2) RS inf_close_sym) 1); |
280 by (rtac ((approx_minus_iff RS iffD2) RS approx_sym) 1); |
281 by (rtac (inf_close_minus_iff RS iffD2) 2); |
281 by (rtac (approx_minus_iff RS iffD2) 2); |
282 by (auto_tac (claset() addDs [inf_close_hrabs_zero_cancel], |
282 by (auto_tac (claset() addDs [approx_hrabs_zero_cancel], |
283 simpset() addsimps [sumhr_split_add_minus])); |
283 simpset() addsimps [sumhr_split_add_minus])); |
284 qed "NSsummable_NSCauchy"; |
284 qed "NSsummable_NSCauchy"; |
285 |
285 |
286 (*------------------------------------------------------------------- |
286 (*------------------------------------------------------------------- |
287 Terms of a convergent series tend to zero |
287 Terms of a convergent series tend to zero |
289 Goalw [NSLIMSEQ_def] "NSsummable f ==> f ----NS> #0"; |
289 Goalw [NSLIMSEQ_def] "NSsummable f ==> f ----NS> #0"; |
290 by (auto_tac (claset(), simpset() addsimps [NSsummable_NSCauchy])); |
290 by (auto_tac (claset(), simpset() addsimps [NSsummable_NSCauchy])); |
291 by (dtac bspec 1 THEN Auto_tac); |
291 by (dtac bspec 1 THEN Auto_tac); |
292 by (dres_inst_tac [("x","N + 1hn")] bspec 1); |
292 by (dres_inst_tac [("x","N + 1hn")] bspec 1); |
293 by (auto_tac (claset() addIs [HNatInfinite_add_one, |
293 by (auto_tac (claset() addIs [HNatInfinite_add_one, |
294 inf_close_hrabs_zero_cancel], |
294 approx_hrabs_zero_cancel], |
295 simpset() addsimps [rename_numerals hypreal_of_real_zero])); |
295 simpset() addsimps [rename_numerals hypreal_of_real_zero])); |
296 qed "NSsummable_NSLIMSEQ_zero"; |
296 qed "NSsummable_NSLIMSEQ_zero"; |
297 |
297 |
298 (* Easy to prove stsandard case now *) |
298 (* Easy to prove stsandard case now *) |
299 Goal "summable f ==> f ----> #0"; |
299 Goal "summable f ==> f ----> #0"; |