Skip to Content

A macro for reusing abstract functions and theorems

Posted on

Authors:

  • Joosten, Sebastiaan J. C.
  • van Gastel, Bernard
  • Schmaltz, Julien

This paper was presented at the ACL2 Workshop 2013

Published in: arXiv preprint arXiv:1304.7875

Paper

Abstract:

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.

BibTeX entry:

@article{Joosten13a,
 abstract = {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.},
 author = {Joosten, Sebastiaan Jozef Christiaan and van Gastel, Bernard and Schmaltz, Julien},
 day = {30},
 journal = {arXiv preprint arXiv:1304.7875},
 month = {4},
 title = {A macro for reusing abstract functions and theorems},
 year = {2013}
}