| changeset 63 | 94436622324d |
| child 68 | acad709cad5d |
| 62:32a83e3ad5a4 | 63:94436622324d |
|---|---|
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 + |
|
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)" |
|
13 end |