如何证明“Isabelle/HOL 中的编程和证明”中练习 4.6 中的引理？答案

【问题标题】：How can I prove the lemma in Exercise 4.6 in “Programming and Proving in Isabelle/HOL”?如何证明“Isabelle/HOL 中的编程和证明”中练习 4.6 中的引理？
【发布时间】：2018-05-08 00:15:45
【问题描述】：

我正在尝试解决“Isabelle/HOL 中的编程和证明”中的练习 4.6。它要求定义一个函数elems :: "'a list ⇒ 'a set"，将列表转换为集合，并证明引理"x ∈ elems xs ⟹ ∃ ys zs . xs = ys @ x # zs ∧ x ∉ elems ys"。到目前为止，我已经走了这么远：

fun elems :: "'a list ⇒ 'a set" where
  "elems [] = {}" |
  "elems (x # xs) = {x} ∪ elems xs"

lemma first_occ: "x ∈ elems xs ⟹ ∃ ys zs . xs = ys @ x # zs ∧ x ∉ elems ys"
proof (induction xs)
  case Nil
  thus ?case by simp
next
  case (Cons u us)
  show ?case
  proof cases
    assume "x = u"
    thus ?case
    proof
    ⟨…⟩

此时，我收到错误消息“无法应用初始证明方法”。这很奇怪，因为目标?case 是命题∃ ys zs . u # us = ys @ x # zs ∧ x ∉ elems ys，并且应该可以通过在∃ 下为特定证人显示命题来证明存在命题。

【问题讨论】：

标签： isabelle quantifiers isar

【解决方案1】：

您的proof 行的问题在于它proof 旨在应用一些默认规则。在上面的证明中，Isabelle 无法弄清楚你想要进行存在性介绍。因此，您可能希望明确告诉系统这样做，例如，继续使用 proof (intro exI) 之类的内容。

我希望这会有所帮助，勒内

【讨论】：

伊莎贝尔为什么想不通？如果目标是∃ x . P 形式的命题；所以伊莎贝尔应该自动选择存在介绍。它在其他情况下也有效（例如，在我的问题“How can I efficiently prove existential propositions with multiple variables in Isabelle/Isar?” 中的示例代码中；为什么不在这里？
因为您还与thus 绑定了一个事实。像rule 这样的证明方法只有在所有链接的事实都可以与规则的假设统一并以正确的顺序应用时才有效。如果您没有明确提供方法，Isabelle 将使用standard，这与rule 类似，带有一些默认规则集。 TL;DR 你很少想将事实链接到proof。在这里使用show 而不是thus。