旧的Isabelle项目使用“uses”导入ml文件，我应该如何替换它？

Question

我继承了一个古老的伊莎贝尔项目，希望能与2016年的伊莎贝尔合作。当项目启动文件时，它通常会启动：

theory my_theory
imports Main uses "my_theory.ML"
begin
lemma my_lemma: ...
by ...
end

uses关键字似乎不再存在，因此我尝试将其更改为：

theory my_theory
imports Main
begin
ML_file "my_theory.ML"

lemma my_lemma: ...
by ...

end

这确实包括了该文件，但我最终在ML文件中出现了错误，这些错误可能是相关的，也可能不是相关的，例如：@{thm my_lemma}代码行上的:my_lemma。

使用ML_file命令包含ML文件的更改正确吗？这对我收到的ML错误有影响吗？

Answer 1

我不熟悉uses关键字；在我开始使用伊莎贝尔之前，它一定已经被删除了。

ML_file应该是前进的道路；但是，您必须在启动/结束理论的begin命令和end命令之间编写ML_file。此外，ML_file调用必须在定义您在ML文件中使用的任何内容之后(常量、事实、定理集合、simprocs、…)。

在您的示例中，它应该如下所示：

theory my_theory
imports Main
begin

lemma my_lemma: ...
  by ...

ML_file "my_theory.ML"

end

请注意，伊莎贝尔变化很大。您所拥有的任何ML代码--特别是如果它是那么旧的--在使用现代的Isabelle版本之前可能需要进行大量的更改。从头开始重写它可能会更容易。这就是伊莎贝尔项目应该放到正式证明档案中的原因，在那里，开发人员会对伊莎贝尔系统中的任何更改进行更新。在法新社之外的任何伊莎贝尔项目都有可能在几年内屈服于腐烂。