如何在Isabelle中搜索常规定义、定理、函数等内容的最佳方法？

Question

我正在尝试阅读Isabelle（定理证明器）的Isar章节，第一个语句如下：

lemma "¬ surj(f :: 'a ⇒ 'a set)"

我想了解常数surj是什么。我知道可以使用以下方法查找相关定理：

thm notI

显示的内容为：

(?P ⟹ False) ⟹ ¬ ?P

我尝试使用谷歌搜索 surj ，但没有找到有用的结果。

我查看了文档 (https://isabelle.in.tum.de/documentation.html)，但我没有找到一个简单的方法来搜索它 (比如说搜索栏)。

人们在进行证明时如何搜索定义或一般信息？如何有效地查找Isabelle中的东西，而不必求助于SO等为微不足道的东西(可能我应该自己能够查找)？像man命令或-help标志等方式？

---

我意识到底部有一个查询框，所以我试了一下。但它显示了38个定理。这是进展，但我觉得因为当我陈述我的引理时，Isabelle知道它正在使用哪一个。有没有一种方法可以强制Isabelle透露它使用的是什么定义(因为它显然知道它正在使用什么)？

---

我刚刚注意到:

thm surj_def

显示：

surj ?f = (∀y. ∃x. y = ?f x)

确实显示了一些内容...这个问题是有价值的，因为我发现了查询框，但人们如何在Isabelle中开发仍然很重要。

---

编辑：

如果链接到解释他们所做内容的策略文档之类的东西，那也很不错...

- Charlie Parker

Answer 1

如果您已经加载了该理论，您可以使用 ctrl+click 跳转到定义。

如果没有加载并且您不知道常量定义在哪里，您可以使用FindFacts 网站搜索（完全声明：我构建了它）。

这里是一个查询您的 surj 问题的链接。

- Dacit

---

我尝试搜索 blast (https://search.isabelle.in.tum.de/#search/default_Isabelle2020-RC4_afp-2020-234a91c26d02?q=%7B%7D)，但没有任何结果。这是一个错误吗？你的工具有哪些限制？ - Charlie Parker

你确定那是正确的链接吗？因为该查询为空。 当我搜索blast时，我得到了定义。 - Dacit

似乎你的工具在Chrome上无法使用，可能是问题所在。我尝试了一个新的自动搜索，但结果太多了。也许一个小的Markdown教程（+5分钟视频）可以使你的工具更易用。看起来有很大的潜力。 - Charlie Parker

谢谢。有一份详细的帮助页面来解释使用方法，还有一个示例页面，可以进行交互式演示常见搜索场景。 关于您的浏览器问题，您能告诉我确切的版本和遇到的问题吗？该工具已经进行了跨测，并且应该可以在大多数流行浏览器中正常使用。 - Dacit