我有 Isabelle/HOL 个理论，如何进行应用？

Question

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

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

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

据我了解，那么我应该：

编写初始理论文件；
调用交互式会话，我可以在其中找到该理论的某些引理的证明
如果我设法找到了引理的证明，那么我可以将这些引理添加到我的理论文件中，以进一步立即用于其他证明（无需重复证明）。

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

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

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

Answer 1

I can enter theory in jEdit dialog but I am not receiving any feedback.

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

So - I should seek some console (additional window) in which I can run lemmas, lemma proof commands against this theory?

你不必，但你可以。在system manual中，描述了如何运行一个"batch build"的一组理论（用伊莎贝尔的行话："a session"）。在最简单的情况下，可以归结为运行ning isabelle mkroot 后跟带有适当标志的 isabelle build。有关独立示例，请参阅该手册中的 §3.2。

And after this - I would like to use this theory - e.g. write some lemma and invoke interactive proof session for this.

在同一个Isabelle/jEdit window，你可以新建一个理论文件，给它起个名字，导入你的理论如下：

theory Test
imports MonoidalLogic
begin

Answer 2

确保将理论 (.thy) 文件保存在 jEdit 路径中的其中一个文件夹中。我认为最好使用 $ISABELLE_HOME_USER 作为文件的根目录；您可以在文件保存 pop-up window 的收藏夹下找到它。那解决了我的类似问题。

我有 Isabelle/HOL 个理论，如何进行应用？

I have Isabelle/HOL theory, how can I proceed with its application?

isabelle