论文标题
从简明的描述中产生相互归纳定理
Generating Mutually Inductive Theorems from Concise Descriptions
论文作者
论文摘要
我们描述了Defret-Mutual-Genatore，这是一种证明有关大型互惠式函数集团的ACL2定理的实用性。这建立在以前的工具上，例如Defret-Mutual和Make-Flag，它们可以自动化该过程的一部分，但仍需要为集团中的每个功能写出定理主体。 对于大型集团，这往往意味着某些常见的假设和结论是多次重复的，从而使证据难以阅读，写作和维护。 该实用程序可自动化这些形式中发生的几种最常见的模式，例如基于正式名称或类型的假设。 它的输入语言足够丰富，可以支持具有某些常见部分和每个功能的独特部分的形式。 Defret-Mutual-Genate的一种应用是支持有关FGL重写器的证据，该证明由49个函数的相互递归集团组成。 该实用程序的使用减少了表达对该集团的定理的形式的大小，通过一个数量级。即使在添加或删除功能时，它也大大减少了在更改集团中更改定义时编辑定理表单的需求。
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 a theorem body to be written out for each function in the clique. For large cliques, this tends to mean that certain common hypotheses and conclusions are repeated many times, making proofs difficult to read, write, and maintain. This utility automates several of the most common patterns that occur in these forms, such as including hypotheses based on formal names or types. Its input language is rich enough to support forms that have some common parts and some unique parts per function. One application of defret-mutual-generate has been to support proofs about the FGL rewriter, which consists of a mutually recursive clique of 49 functions. The use of this utility reduced the size of the forms that express theorems about this clique by an order of magnitude. It also greatly has reduced the need to edit theorem forms when changing definitions in the clique, even when adding or removing functions.
