Proof pearl: Defining functions over finite sets

Abstract

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 functional 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. © Springer-Verlag Berlin Heidelberg 2005.