Cha*_*ker 8 theorem-proving isabelle
我试图通过 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 中的发展方式仍然很棒。
编辑：
如果它与解释他们做了什么或类似的事情的战术文档相关联，那也会很好......