| author | paulson |
| Wed, 26 Jun 2002 10:26:46 +0200 | |
| changeset 13248 | ae66c22ed52e |
| parent 12018 | ec054019c910 |
| child 14416 | 1f256287d4f0 |
| 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 |
|
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11701
diff
changeset
|
12 |
sumr_0 "sumr m 0 f = 0" |
|
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11701
diff
changeset
|
13 |
sumr_Suc "sumr m (Suc n) f = (if n < m then 0 |
| 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 |