src/HOL/Hyperreal/HSeries.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hyperreal/HSeries.thy	Sat Dec 30 22:03:47 2000 +0100
@@ -0,0 +1,30 @@
+(*  Title       : HSeries.thy
+    Author      : Jacques D. Fleuriot
+    Copyright   : 1998  University of Cambridge
+    Description : Finite summation and infinite series
+                  for hyperreals
+*) 
+
+HSeries = Series +
+
+consts 
+   sumhr :: "(hypnat * hypnat * (nat=>real)) => hypreal"
+
+defs
+   sumhr_def
+   "sumhr p
+       == Abs_hypreal(UN X:Rep_hypnat(fst p). 
+              UN Y: Rep_hypnat(fst(snd p)).
+              hyprel ^^{%n::nat. sumr (X n) (Y n) (snd(snd p))})"
+
+constdefs
+   NSsums  :: [nat=>real,real] => bool     (infixr 80)
+   "f NSsums s  == (%n. sumr 0 n f) ----NS> s"
+
+   NSsummable :: (nat=>real) => bool
+   "NSsummable f == (EX s. f NSsums s)"
+
+   NSsuminf   :: (nat=>real) => real
+   "NSsuminf f == (@s. f NSsums s)"
+
+end