isabelle: src/ZF/ex/NatSum.thy@50be659d4222 (annotated)

9647 e9623f47275b new example ZF/ex/NatSum paulson parents: diff changeset	1	(* Title: HOL/ex/Natsum.thy
e9623f47275b new example ZF/ex/NatSum paulson parents: diff changeset	2	ID: $Id$
e9623f47275b new example ZF/ex/NatSum paulson parents: diff changeset	3	Author: Tobias Nipkow & Lawrence C Paulson
e9623f47275b new example ZF/ex/NatSum paulson parents: diff changeset	4
e9623f47275b new example ZF/ex/NatSum paulson parents: diff changeset	5	A summation operator. sum(f,n+1) is the sum of all f(i), i=0...n.
e9623f47275b new example ZF/ex/NatSum paulson parents: diff changeset	6
e9623f47275b new example ZF/ex/NatSum paulson parents: diff changeset	7	Note: n is a natural number but the sum is an integer,
e9623f47275b new example ZF/ex/NatSum paulson parents: diff changeset	8	and f maps integers to integers
e9623f47275b new example ZF/ex/NatSum paulson parents: diff changeset	9	*)
e9623f47275b new example ZF/ex/NatSum paulson parents: diff changeset	10
e9623f47275b new example ZF/ex/NatSum paulson parents: diff changeset	11	NatSum = Main +
e9623f47275b new example ZF/ex/NatSum paulson parents: diff changeset	12
e9623f47275b new example ZF/ex/NatSum paulson parents: diff changeset	13	consts sum :: [i=>i, i] => i
e9623f47275b new example ZF/ex/NatSum paulson parents: diff changeset	14	primrec
e9623f47275b new example ZF/ex/NatSum paulson parents: diff changeset	15	"sum (f,0) = #0"
e9623f47275b new example ZF/ex/NatSum paulson parents: diff changeset	16	"sum (f, succ(n)) = f($#n) $+ sum(f,n)"
e9623f47275b new example ZF/ex/NatSum paulson parents: diff changeset	17
e9623f47275b new example ZF/ex/NatSum paulson parents: diff changeset	18	end

author	wenzelm
	Fri, 06 Oct 2000 17:35:58 +0200
changeset 10168	50be659d4222
parent 9647	e9623f47275b
child 12867	5c900a821a7c
permissions	-rw-r--r--