我需要保存Isabelle文件来导入它们吗?

Question

我想导入ListSum理论，而ListSum理论又依赖于ListAux, EfficientNat和Main理论文件。

然而，我无法导入这些，所以我尝试复制和保存ListSum，但它取决于ListAux，似乎使用过时的风格/语法(至少是我在谷歌上找到的版本)。

最后，我只想做一些像

n = sum_{i =1…m}(列表!我)*我

首先，我需要对列表求和哪些文件，我需要将它们保存在本地吗?我成功导入了HOL。Groups_List和HOL。阶乘(理论?)而不需要在本地下载这些…为什么?但是当我尝试将ListSum添加到imports"第一行抛出错误。

其次，我如何用Isabelle写上面的求和?

Answer 1

ListSum理论是Isabelle AFP(见isa-afp.org/entries/Flyspeck-Tame.html)中Flyspeck I: Tame Graphs条目的一部分，似乎是一个内部理论，它基本上包含用于列表和相关属性求和的特殊构造∑⇘x ∈ xs⇙ f。

关于你问题的第二部分:在Isabelle中，你的总和写为∑i ∈ {1..m}. List ! i * i。您不需要为此导入任何特殊内容。