Proof pearl: Defining functions over finite sets

Tobias Nipkow, Lawrence C. Paulson

Research output: Contribution to journalConference articlepeer-review

10 Scopus citations


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.

Original languageEnglish
Pages (from-to)385-396
Number of pages12
JournalLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
StatePublished - 2005
Event18th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2005 - Oxford, United Kingdom
Duration: 22 Aug 200525 Aug 2005


Dive into the research topics of 'Proof pearl: Defining functions over finite sets'. Together they form a unique fingerprint.

Cite this