10751

1 
(* Title : Series.thy


2 
Author : Jacques D. Fleuriot


3 
Copyright : 1998 University of Cambridge


4 
Description : Finite summation and infinite series


5 
*)


6 


7 


8 
Series = SEQ + Lim +


9 


10 
consts sumr :: "[nat,nat,(nat=>real)] => real"


11 
primrec


12 
sumr_0 "sumr m 0 f = #0"


13 
sumr_Suc "sumr m (Suc n) f = (if n < m then #0


14 
else sumr m n f + f(n))"


15 


16 
constdefs


17 
sums :: [nat=>real,real] => bool (infixr 80)


18 
"f sums s == (%n. sumr 0 n f) > s"


19 


20 
summable :: (nat=>real) => bool


21 
"summable f == (EX s. f sums s)"


22 


23 
suminf :: (nat=>real) => real


24 
"suminf f == (@s. f sums s)"


25 
end


26 


27 
