我正在尝试阅读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中开发仍然很重要。
编辑:
如果链接到解释他们所做内容的策略文档之类的东西,那也很不错...
blast
(https://search.isabelle.in.tum.de/#search/default_Isabelle2020-RC4_afp-2020-234a91c26d02?q=%7B%7D),但没有任何结果。这是一个错误吗?你的工具有哪些限制? - Charlie Parker