equal
deleted
inserted
replaced
1 (* Title: HOL/ex/natsum.thy |
1 (* Title: HOL/ex/NatSum.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Tobias Nipkow |
3 Author: Tobias Nipkow |
4 Copyright 1994 TU Muenchen |
4 Copyright 1994 TU Muenchen |
5 |
5 |
6 A summation operator. sum(f,n+1) is the sum of all f(i), i=0...n. |
6 A summation operator. sum(f,n+1) is the sum of all f(i), i=0...n. |
7 *) |
7 *) |
8 |
8 |
9 NatSum = Main + |
9 NatSum = Main + |
10 consts sum :: [nat=>nat, nat] => nat |
10 consts sum :: [nat=>nat, nat] => nat |
11 primrec |
11 primrec |
12 "sum f 0 = 0" |
12 sum_0 "sum f 0 = 0" |
13 "sum f (Suc n) = f(n) + sum f n" |
13 sum_Suc "sum f (Suc n) = f(n) + sum f n" |
14 |
14 |
15 end |
15 end |