isabelle - 搜索 Isabelle 的一般定义、定理、函数等的最佳方法是什么？

Question

我试图通过 Isabelle(定理证明者)的 Isar 章节，第一个陈述是:

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

我想了解什么是常数 surj曾是。我知道查找定理很容易:

thm notI

显示:

(?P ⟹ False) ⟹ ¬ ?P

我试过谷歌搜索 surj但没有任何有用的东西出现。

我去了文档( https://isabelle.in.tum.de/documentation.html )，但找不到一种简单的方法来搜索它(例如，使用搜索栏)。

人们在做证明时如何搜索定义或一般内容？你如何以有效的方式为伊莎贝尔查找东西，而不必求助于 SO 等琐碎的东西(我应该能够自己查找)？像 man命令或 -help标志等？

我意识到底部有一个查询框，所以我试了一下。但它向我展示了 38 个定理。这是一个很好的进步，但我觉得这是因为当我说我的引理时，伊莎贝尔确切地知道它在使用哪个。有没有办法强制 Isabelle 透露它使用的定义(因为它显然必须知道它使用的是什么)。

我刚刚注意到:

thm surj_def

显示:

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

确实显示了一些东西...这个问题是值得的，因为我发现了查询框，但无论如何人们在 Isabelle 中的发展方式仍然很棒。

编辑:

如果它与解释他们做了什么或类似的事情的战术文档相关联，那也会很好......

Answer 1

如果你已经加载了理论，可以通过ctrl+click跳转到定义.

如果没有，并且您不知道常量在哪里定义，则可以使用 FindFacts网络搜索(完全免责声明:我构建了它)。

Here是对您的 surj 问题的查询。