A Versatile, Sound Tool for Simplifying Definitions

Alessandro Coglio, Matt Kaufmann, Eric W. Smith

We present a tool, simplify-defun, that transforms the definition of a given function into a simplified definition of a new function, providing a proof checked by ACL2 that the old…