在Isabelle中重用AFP条目的正确方法

Question

假设我想在Isabelle中形式化一个关于多元多项式的环的命题。

相关的AFP条目似乎是：

https://www.isa-afp.org/entries/Polynomials.html

但是，在Isabelle分布中，我只发现：

HOL/Algebra/Polynomials.thy

它似乎只处理一元多项式。根据find\_theorems in the AFP，我推断我必须下载法新社条目并从我机器的某个目录中导入它。这又意味着对AFP条目的所有依赖项重复该过程。

这是正确的/最有效的方法吗？

Answer 1

是。要在Isabelle中使用任何理论的结果，您必须处理它及其依赖项。

对于法新社来说，下载整个归档文件并导入您想要的理论通常是最简单的。然后，Isabelle将只处理它所依赖的归档，而不是整个归档，即它将为您执行依赖项解析。

(另请参阅AFP网站上有关使用其他AFP条目的文档，了解如何确保Isabelle在下载AFP后查看AFP中的依赖项)。