Proof Pearl: Defining Functions Over Finite Sets

Tobias Nipkow, Lawrence C. Paulson

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}