在 Isabelle 中使用“find_theorems”答案

【问题标题】：Using "find_theorems" in Isabelle在 Isabelle 中使用“find_theorems”
【发布时间】：2014-01-21 20:46:06
【问题描述】：

我想找到定理。我已经阅读了Isabelle/Isar reference manual 中关于find_theorems 的部分：

find_theorems 标准

从与所有给定搜索匹配的理论或证明上下文中检索事实标准。标准 name: p 选择所有符合条件的定理 name 匹配模式 p，其中可能包含“*”通配符。标准intro， elim 和 dest 选择与当前目标匹配的定理作为介绍，分别消除或销毁规则。标准 solves 返回所有可以直接解决当前目标的规则。标准 simp: t 选择左侧与给定术语匹配的所有重写规则。这标准术语 t 选择所有包含模式 t 的定理——像往常一样，模式可能包含出现的虚拟“_”、示意图变量和类型约束。

标准前面可以加上“-”来选择不匹配的定理。笔记给出空的标准列表会产生所有当前已知的事实。一个可以对打印事实的数量进行可选限制；默认值为 40。默认情况下，从搜索结果中删除重复项。使用 with_dups 来显示重复项。

据我了解，find_theorems 用于 Isabelle/jEdit 的查找窗口。以上内容并不能帮助我找到以下情况的相关定理（Lambda 是 Nominal Isabelle 扩展的理论。压缩包是 here）：

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 的所有定理？

【问题讨论】：

标签： isabelle

【解决方案1】：

由于Lam 像普通的 lambda (%) 本身不是一个术语，因此您应该添加其余部分以获得适当的术语，其中可能包含通配符。在你的例子中，我会执行

find_theorems "Lam [_]. _"

它给出了很多答案。

【讨论】：

【解决方案2】：

通常，只要为某个常量定义了特殊语法，就会发生这种情况。但是（几乎）总是有一个潜在的（“原始”）常量。找出哪个常量提供Lam [_]. _ 语法。您可以在 Isabelle/jEdit 中 Ctrl-单击 Lam（在专有术语内）。这将跳转到底层常量的定义。

对于Lam，还有一个额外的复杂性，即绑定语法使用与底层常量完全相同的字符串，即Lam，如在定义处可见：

nominal_datatype lam =
  Var "name"
| App "lam" "lam"
| Lam x::"name" l::"lam"  binds x in l ("Lam [_]. _" [100, 100] 100)

在这种情况下，您可以使用常量的长名称，方法是在其前面加上理论名称，即Lambda.Lam。

注意：同样适用于像 ALL x. P x 这样的活页夹（带有底层常量 All），但不适用于内置的 %x. x。

【讨论】：