author | clasohm |
Fri, 01 Dec 1995 12:03:13 +0100 | |
changeset 1376 | 92f83b9d17e1 |
parent 969 | b051e2fc2e34 |
child 1476 | 608483c2122a |
permissions | -rw-r--r-- |
969 | 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 + |
|
1376 | 10 |
consts sum :: [nat=>nat, nat] => nat |
969 | 11 |
rules sum_0 "sum f 0 = 0" |
12 |
sum_Suc "sum f (Suc n) = f(n) + sum f n" |
|
13 |
end |