| author | wenzelm |
| Fri, 06 Oct 2000 17:35:58 +0200 | |
| changeset 10168 | 50be659d4222 |
| parent 10045 | c76b73e16711 |
| permissions | -rw-r--r-- |
|
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
1 |
(* Title : Series.thy |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
2 |
Author : Jacques D. Fleuriot |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
3 |
Copyright : 1998 University of Cambridge |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
4 |
Description : Finite summation and infinite series |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
5 |
*) |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
6 |
|
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
7 |
|
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
8 |
Series = SEQ + Lim + |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
9 |
|
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
10 |
consts sumr :: "[nat,nat,(nat=>real)] => real" |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
11 |
primrec |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
12 |
sumr_0 "sumr m 0 f = #0" |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
13 |
sumr_Suc "sumr m (Suc n) f = (if n < m then #0 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
14 |
else sumr m n f + f(n))" |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
15 |
|
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
16 |
constdefs |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
17 |
sums :: [nat=>real,real] => bool (infixr 80) |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
18 |
"f sums s == (%n. sumr 0 n f) ----> s" |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
19 |
|
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
20 |
summable :: (nat=>real) => bool |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
21 |
"summable f == (EX s. f sums s)" |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
22 |
|
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
23 |
suminf :: (nat=>real) => real |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
24 |
"suminf f == (@s. f sums s)" |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
25 |
end |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
26 |
|
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
27 |