src/HOL/ex/NatSum.thy
author paulson
Wed Nov 05 13:23:46 1997 +0100 (1997-11-05)
changeset 4153 e534c4c32d54
parent 3269 eca2a3634acd
child 5184 9b8547a9496a
permissions -rw-r--r--
Ran expandshort, especially to introduce Safe_tac
     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 primrec "sum" nat 
    12   "sum f 0 = 0"
    13   "sum f (Suc n) = f(n) + sum f n"
    14 
    15 end