伊莎贝尔 2017 年——开始

Question

我正在努力学习使用 Isabelle/HOL。我想，“嘿，由一些开发它的人写的教程会很棒”，所以看着 https://isabelle.in.tum.de/doc/tutorial.pdf 其发布日期为 2018 年 8 月 15 日。不过，在尝试通过示例工作时，我在文本中发现了这样的内容：

“经典的 Isabelle 用户界面是 David Aspinall 的 Proof General / Emacs。这本书对 Proof General 的介绍很少，它有自己的文档。” （第三页）

“如果发生任何奇怪的事情，我们建议您通过 Proof General 菜单项 Isabelle > Settings > Show Types 让 Isabelle 显示所有类型信息（有关详细信息，请参阅第 1.5 节）。” （第 5 页）

问题是 Proof General 似乎不再适用于 Isabelle（请参阅 Isabelle2016 and Proof General）。我很困惑为什么教程会基于过时的软件，但我真正的问题是：

“在伊莎贝尔 2017 年，我是否可以学习做最简单的事情？”

Answer 1

截至 2018 年，Isabelle 唯一支持的 IDE 是 Isabelle/jEdit，它包含在您可以从 Isabelle 网站下载的发行版中。有一个实验性的 VSCode 插件正在积极开发中，但我建议暂时使用 Isabelle/jEdit。

您找到的教程在网站上列为“旧手册”之一。它在许多方面都严重过时，不应再使用。发布日期可能毫无意义，因为它是生成 PDF 的日期，而不是编写文本的日期。有些人游说将该教程从网站上完全删除，您的经验似乎证实我们确实应该这样做。

开始学习 Isabelle 的最佳方法之一可能是阅读《‘Concrete Semantics’》这本书（提供免费在线版本）。它的前半部分基本上是对 Isabelle/HOL 的介绍，有很多练习。 Isabelle 网站上还有‘Programming and Proving’ 教程，和《具体语义学》的前半部分几乎一模一样。

但是，它侧重于计算机科学中的应用（编程语言的语义和一些函数式编程）。我不确定是否有关于如何在 Isabelle 中做数学的好教程；无论如何，对于初学者来说，在定理证明器中数学往往更难做，因为与非正式论文推理的差距更大。因此，即使您最终对数学形式化感兴趣，我也推荐“具体语义”。

顺便说一句：您提到了 Isabelle2017，但确实没有理由使用它来代替 Isabelle2018，这是撰写此答案时的最新版本。