  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.
