时间戳

首页 > 解决方案 > 如何在 Isabelle/HOL 中使用 lambda 表达式？

isabelle - 如何在 Isabelle/HOL 中使用 lambda 表达式？

问题描述

在我学习 Isabelle/HOL 语法的练习中，我试图证明下面的一个玩具引理。它是关于 lambda 表达式（以及将谓词作为输入的“最伟大”表示法之类的东西）。引理的预期内容是“le 1 的最大自然数是 1”。

lemma "1 = Greatest (λ x::nat. x ≤ 1)"
proof - 
  show ?thesis 
    by auto
qed

auto但是，上述证明对or都不起作用simp，并生成一条消息。

Failed to finish proof⌂:
goal (1 subgoal):
 1. Suc 0 = (GREATEST x. x ≤ Suc 0)

有人可以帮助解释该陈述出了什么问题或如何正确证明这一点（如果该陈述正确）？

标签： isabelle

解决方案

引理没有任何问题，只是没有以了解它们Greatest的方式声明任何规则。auto这可能很好，因为这些类型的规则往往会干扰自动化。

您可以使用例如规则来证明您的陈述Greatest_equality：

lemma "1 = Greatest (λ x::nat. x ≤ 1)"
proof - 
  have "(GREATEST (x::nat). x ≤ 1) = 1"
    by (rule Greatest_equality) auto
  thus ?thesis by simp
qed

您可以使用 Isabelle/jEdit 中的 Query 面板或find_theorems通过搜索常量 的命令找到类似的规则Greatest。

如果这GREATEST件事让您感到困惑，那么语法GREATEST x. P x只是Greatest (λx. P x). 这种符号在 Isabelle 中是相当标准的，我们也有∃x. P xforEx (λx. P x)等。

推荐阅读