Sol Swords

Generating Mutually Inductive Theorems from Concise Descriptions

2020 · Electronic Proceedings in Theoretical Computer Science

We describe defret-mutual-generate, a utility for proving ACL2 theorems about large mutually recursive cliques of functions. This builds on previous tools such as defret-mutual and make-flag, which automate parts of the process but still require …