抽象函数和定理的重用宏
A Macro for Reusing Abstract Functions and Theorems
摘要：
尽管ACL 2逻辑是一阶的，但ACL 2系统提供了几种机制，为用户提供类似于高阶逻辑的操作。在本文中，我们提出了一个宏，命名为instance-of-defspec，以方便重用的抽象函数和事实证明他们。Defspec是一本ACL 2书籍，允许用户定义约束函数及其相关属性。它包含了便于定义这种抽象规范及其实例的宏。目前，从这些抽象函数导出的引理和定理不会自动实例化。这正是我们新宏的目的。instance-of-defspec将不仅实例化规范内的函数和定理，而且实例化在规范之上构建的更多函数和定理。作为一个工作示例，我们描述了monoid上的各种折叠函数，这些函数是我们从任意函数逐渐构建的。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
