Old_HOL: ex/natsum.thy@c0ff8f1ebc16 (annotated)

63 94436622324d Added some sums. nipkow parents: diff changeset	1	(* Title: HOL/ex/natsum.thy
94436622324d Added some sums. nipkow parents: diff changeset	2	ID: $Id$
94436622324d Added some sums. nipkow parents: diff changeset	3	Author: Tobias Nipkow
94436622324d Added some sums. nipkow parents: diff changeset	4	Copyright 1994 TU Muenchen
94436622324d Added some sums. nipkow parents: diff changeset	5
94436622324d Added some sums. nipkow parents: diff changeset	6	A summation operator. sum(f,n+1) is the sum of all f(i), i=0...n.
94436622324d Added some sums. nipkow parents: diff changeset	7	*)
94436622324d Added some sums. nipkow parents: diff changeset	8
94436622324d Added some sums. nipkow parents: diff changeset	9	NatSum = Arith +
68 acad709cad5d tidied definitions and proofs lcp parents: 63 diff changeset	10	consts sum :: "[nat=>nat, nat] => nat"
acad709cad5d tidied definitions and proofs lcp parents: 63 diff changeset	11	rules sum_0 "sum(f,0) = 0"
acad709cad5d tidied definitions and proofs lcp parents: 63 diff changeset	12	sum_Suc "sum(f,Suc(n)) = f(n) + sum(f,n)"
63 94436622324d Added some sums. nipkow parents: diff changeset	13	end