author  wenzelm 
Fri, 05 Oct 2001 21:52:39 +0200  
changeset 11701  3d51fbf81c17 
parent 10751  a81ea5d3dd41 
child 12018  ec054019c910 
permissions  rwrr 
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 

11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10751
diff
changeset

12 
sumr_0 "sumr m 0 f = Numeral0" 
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10751
diff
changeset

13 
sumr_Suc "sumr m (Suc n) f = (if n < m then Numeral0 
10751  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 