8

我想在名为 的理论中定义我自己的列表类型List，但已经有一个具有该名称的理论。有比 更轻量级的理论Main吗？

4

3 回答 3

6

请注意，这$ISABELLE_HOME/src/HOL/ex/Seq.thy给出了一个定义您自己的列表数据类型以进行实验的最小示例，而不涉及如何在其Main入口点下方使用系统的微妙问题。（初学者会感到困惑，专家不会这样做。）

从理论上讲，您可以导入的最原始的理论是Pure，但这只是最基本的逻辑框架，还没有任何像 HOL 这样的对象逻辑。只是出于好奇，您可能会查看从$ISABELLE_HOME/src/HOL/ex/Higher_Order_Logic.thy哪个开始Pure并在其之上定义了 HOL 的最小版本，但没有任何您期望从完整的 Isabelle/HOL 获得的高级理论和工具。

于 2013-02-28T21:21:37.107 回答
4

您不能在 Isabelle 中导入任何内容（因为即使对于基本逻辑也需要导入）。Isabelle 中 HOL 的实现具有三个受支持的入口点：Main、Complex_Main（Main加上一些分析）和Plain，但只有前两个是用于常规使用的。

Plain 已经包含基本逻辑，但在标准库方面几乎没有（例如没有列表）。但也缺少 QuickCheck、Sledgehammer 和代码生成器等重要工具。此外，如果您从 Plain 开始能够命名您自己的理论列表，请注意您的理论将与 Main 上的任何工作（几乎所有内容）都不兼容。

因此，除非您有充分的理由这样做，否则我建议您遵循 Raphael 的评论并为您的列表理论重新命名。

于 2012-12-06T23:44:04.740 回答
0

您只能导入HOL，如

theory Test_Theory
imports HOL
begin
  …
end

我经常这样做是为了测试和调查伊莎贝尔。

但是，您将缺少数据类型定义，并且可能需要导入Datatype（甚至可能是Record），以便能够编写您的List理论。

theory Test_Theory
imports HOL Datatype Record
begin
  …
end

作为两者Datatype和Recordimports HOL，您可能只需要：

theory Test_Theory
imports Datatype Record
begin
  …
end

没有理论Main，这并不容易，但并非不可能。请注意，您将不得不放弃许多广泛使用的定理，并且可能必须编写并证明您自己的定理。

于 2013-02-23T06:12:35.527 回答