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