Proof pearl: Defining functions over finite sets

Tobias Nipkow; Lawrence C. Paulson

doi:10.1007/11541868_25

Proof pearl: Defining functions over finite sets

Tobias Nipkow, Lawrence C. Paulson

Default

University of Cambridge

Research output: Contribution to journal › Conference article › peer-review

10 Scopus citations

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.

Original language	English
Pages (from-to)	385-396
Number of pages	12
Journal	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	3603
DOIs	https://doi.org/10.1007/11541868_25
State	Published - 2005
Event	18th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2005 - Oxford, United Kingdom Duration: 22 Aug 2005 → 25 Aug 2005

Access to Document

10.1007/11541868_25

Cite this

@article{eb4cd952f5604f6ba803aee1866e3eb7,

title = "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.",

author = "Tobias Nipkow and Paulson, {Lawrence C.}",

year = "2005",

doi = "10.1007/11541868_25",

language = "English",

volume = "3603",

pages = "385--396",

journal = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

issn = "0302-9743",

publisher = "Springer Science and Business Media Deutschland GmbH",

note = "18th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2005 ; Conference date: 22-08-2005 Through 25-08-2005",

}

TY - JOUR

T1 - Proof pearl

T2 - 18th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2005

AU - Nipkow, Tobias

AU - Paulson, Lawrence C.

PY - 2005

Y1 - 2005

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=26844549136&partnerID=8YFLogxK

U2 - 10.1007/11541868_25

DO - 10.1007/11541868_25

M3 - Conference article

AN - SCOPUS:26844549136

SN - 0302-9743

VL - 3603

SP - 385

EP - 396

JO - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

JF - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

Y2 - 22 August 2005 through 25 August 2005

ER -

Proof pearl: Defining functions over finite sets

Abstract

Access to Document

Other files and links

Fingerprint

Cite this