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
clasohm@1476
     1
(*  Title:      HOL/ex/natsum.thy
clasohm@969
     2
    ID:         $Id$
clasohm@1476
     3
    Author:     Tobias Nipkow
clasohm@969
     4
    Copyright   1994 TU Muenchen
clasohm@969
     5
clasohm@969
     6
A summation operator. sum(f,n+1) is the sum of all f(i), i=0...n.
clasohm@969
     7
*)
clasohm@969
     8
clasohm@969
     9
NatSum = Arith +
clasohm@1376
    10
consts sum     :: [nat=>nat, nat] => nat
paulson@3269
    11
primrec "sum" nat 
paulson@3269
    12
  "sum f 0 = 0"
paulson@3269
    13
  "sum f (Suc n) = f(n) + sum f n"
paulson@3269
    14
clasohm@969
    15
end