| author | lcp |
| Thu, 21 Apr 1994 11:28:32 +0200 | |
| changeset 68 | acad709cad5d |
| parent 63 | 94436622324d |
| permissions | -rw-r--r-- |
| 63 | 1 |
(* Title: HOL/ex/natsum.thy |
2 |
ID: $Id$ |
|
3 |
Author: Tobias Nipkow |
|
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 + |
|
| 68 | 10 |
consts sum :: "[nat=>nat, nat] => nat" |
11 |
rules sum_0 "sum(f,0) = 0" |
|
12 |
sum_Suc "sum(f,Suc(n)) = f(n) + sum(f,n)" |
|
| 63 | 13 |
end |