# A Versatile, Sound Tool for Simplifying Definitions

## TL;DR

The paper introduces simplify-defun, a tool that simplifies function definitions while ensuring their correctness through proof, aiding program transformation in synthesis and verification.

## Contribution

It presents a novel tool that automates function simplification with proof support, enhancing program transformation processes.

## Key findings

- Successfully simplifies functions with proof guarantees
- Generates termination and guard proofs automatically
- Facilitates program synthesis and verification

## Abstract

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 and new functions are equivalent. When appropriate it also generates termination and guard proofs for the new function. We explain how the tool is engineered so that these proofs will succeed. Examples illustrate its utility, in particular for program transformation in synthesis and verification.