|
63
|
1 |
(* Title: HOL/ex/sum.thy
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Tobias Nipkow
|
|
|
4 |
Copyright 1994 TU Muenchen
|
|
|
5 |
|
|
|
6 |
A summation operator
|
|
|
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
|