#### Proof Pearl: Defining Functions Over Finite Sets

Structural recursion over sets is meaningful only if the result is
independent of the order in which the set's elements are enumerated. This
paper outlines a theory of function definition for finite sets, based on the
fold functionals often used with lists. The fold functional is introduced as
a relation, which is then shown to denote a function under certain
conditions. Applications include summation and maximum. The theory has been
formalized using Isabelle/HOL.
pdf (c) Springer Verlag

BibTeX:

@inproceedings{NipkowP-TPHOLs05,
author={Tobias Nipkow and Lawrence C. Paulson},
title={Proof Pearl: Defining Functions Over Finite Sets},
booktitle={Theorem Proving in Higher Order Logics (TPHOLs 2005)},
editor={J. Hurd},
publisher=Springer,series=LNCS,volume=3603,pages={385-396},year=2005}