我有 Isabelle/HOL 理论，我该如何继续它的应用？

Question

我正在尝试了解 Isabelle/HOL 理论的用途。我已经编写并保存了一个理论文件：

theory MonoidalLogic
  imports sequents
begin
consts
  Test :: "test"
axiomatization where
  identity "φ⊢φ" and
  cut "φ⊢ψ;ψ⊢ρ⟹φ⊢ρ"
  l "φ⊢⊤⨂ψ⟺φ⊢ψ"
  r "φ⊢ψ⨂⊤⟺φ⊢ψ"
end

现在我想得到一些关于这个理论的反馈 - Isabelle 是否接受它，以某种方式编译它 - 我该怎么做？在此之后 - 我想使用这个理论 - 例如为此编写一些引理并调用交互式证明会话。我怎样才能做到这一点？我可以在 jEdit 对话框中输入理论，但我没有收到任何反馈。我不明白我应该如何关闭这个理论文件并开始我可以使用这个理论文件的交互式会话？

据我所知，我应该：

1. 写入初始理论文件；

2. 调用交互式会话，我可以在其中找到该理论的一些引理的证明

3. 如果我设法找到了引理的证明，那么我可以将这些引理添加到我的理论文件中，以便进一步立即用于其他证明（无需重复证明）。

我正在阅读Concrete Semantics、LNCS 教程和其他教程，但我没有看到此基本工作流程的示例 - 如何执行此工作流程以及我是否理解正确。

我的意图是采用这个逻辑 http://www.sciencedirect.com/science/article/pii/S1570868314000573 并在 Isabelle/HOL 中为这个逻辑创建定理证明器，即将这个逻辑作为 Isabelle 中的对象逻辑自动化。

据我了解 - jEdit 主窗口用于编辑理论文件。所以 - 我应该寻找一些控制台（附加窗口），我可以在其中运行引理，针对这个理论的引理证明命令？

Answer 1

我可以在 jEdit 对话框中输入理论，但我没有收到任何反馈。

听起来您可能没有安装有效的 Isabelle。在工作安装中，任何扩展名为 .thy 的文件都会在 Isabelle/jEdit 中检查。例如，错误以红色突出显示，您将在“输出”和“状态”面板中看到证明者输出，您可以按住 Ctrl 键单击实体以跳转到其定义。

所以 - 我应该寻找一些控制台（附加窗口），我可以在其中运行引理，针对这个理论的引理证明命令？

您不必这样做，但可以。在system manual 中，描述了如何运行一组理论的“批量构建”（在伊莎贝尔行话中：“一个会话”）。在最简单的情况下，归结为运行isabelle mkroot，然后运行带有适当标志的isabelle build。有关独立示例，请参阅该手册中的 §3.2。

在此之后 - 我想使用这个理论 - 例如为此编写一些引理并调用交互式证明会话。

在同一个 Isabelle/jEdit 窗口中，您可以创建一个新的理论文件，为其命名，然后按如下方式导入您的理论：

theory Test
imports MonoidalLogic
begin

Answer 2

确保将您的理论 (.thy) 文件保存在 jEdit 在其路径中的文件夹之一中。我相信使用 $ISABELLE_HOME_USER 作为文件的根是最好的；您可以在“文件保存”弹出窗口的“收藏夹”下找到它。这解决了我的类似问题。