A Macro for Reusing Abstract Functions and Theorems

Sebastiaan J. C. Joosten
Bernard van Gastel
Julien Schmaltz

Even though the ACL2 logic is first order, the ACL2 system offers several mechanisms providing users with some operations akin to higher order logic ones. In this paper, we propose a macro, named instance-of-defspec, to ease the reuse of abstract functions and facts proven about them. Defspec is an ACL2 book allowing users to define constrained functions and their associated properties. It contains macros facilitating the definition of such abstract specifications and instances thereof. Currently, lemmas and theorems derived from these abstract functions are not automatically instantiated. This is exactly the purpose of our new macro. instance-of-defspec will not only instantiate functions and theorems within a specification but also many more functions and theorems built on top of the specification. As a working example, we describe various fold functions over monoids, which we gradually built from arbitrary functions.

In Ruben Gamboa and Jared Davis: Proceedings International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 2013), Laramie, Wyoming, USA , May 30-31, 2013, Electronic Proceedings in Theoretical Computer Science 114, pp. 29–41.
Published: 26th April 2013.

ArXived at: http://dx.doi.org/10.4204/EPTCS.114.3 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org