在伊莎贝尔使用"find_theorems"

Question

我想找到定理.我已阅读的部分find_theorems中伊莎贝尔/ ISAR参考手册:

find_theorems 标准

从理论或证据上下文中检索匹配所有给定搜索条件的事实.该标准name: p选择所有完全限定名称与模式p匹配的定理,模式p可能包含" *"通配符.分别与引入,消除或销毁规则匹配当前目标的标准intro, elim和dest选择定理.该标准solves返回所有直接解决当前目标的规则.该标准simp: t 选择左侧与给定术语匹配的所有重写规则.标准项t选择包含模式t的所有定理- 通常,模式可能包含虚拟" _",原理图变量和类型约束的出现.

标准之前可以用" -"来选择不匹配的定理.请注意,给出空标准列表会产生所有当前已知的事实.可以给出打印事实数量的可选限制; 默认值为40.默认情况下,将从搜索结果中删除重复项.使用with_dups显示重复.

据我所知,find_theorems在Isabelle/jEdit的查找窗口中使用.以上并没有帮助我找到以下情况的相关定理(Lambda是一个名义Isabelle扩展的理论.tarball在这里):

theory First
imports Lambda

begin

theorem "Lam [x].(Lam [y].(App (Var x)(Var y))) = Lam [y].(Lam [x].(App (Var y)(Var x)))"

当我尝试搜索表达式时,LamIsabelle/jedit说

Inner syntax error: unexpected end of input
Failed to parse term

我怎样才能找到包含常数的所有定理Lam？

Answer 1

因为Lam像普通的lambda(%)本身不是一个术语,你应该添加剩下的部分来获得一个合适的术语,其中可能包含通配符.在你的例子中,我会表演

find_theorems "Lam [_]. _"

这给了很多答案.