author | berghofe |
Fri, 24 Jul 1998 13:19:38 +0200 | |
changeset 5184 | 9b8547a9496a |
parent 3269 | eca2a3634acd |
child 8356 | 14d89313c66c |
permissions | -rw-r--r-- |
1476 | 1 |
(* Title: HOL/ex/natsum.thy |
969 | 2 |
ID: $Id$ |
1476 | 3 |
Author: Tobias Nipkow |
969 | 4 |
Copyright 1994 TU Muenchen |
5 |
||
6 |
A summation operator. sum(f,n+1) is the sum of all f(i), i=0...n. |
|
7 |
*) |
|
8 |
||
9 |
NatSum = Arith + |
|
1376 | 10 |
consts sum :: [nat=>nat, nat] => nat |
5184 | 11 |
primrec |
3269 | 12 |
"sum f 0 = 0" |
13 |
"sum f (Suc n) = f(n) + sum f n" |
|
14 |
||
969 | 15 |
end |