proof - 如何在规则中绑定(bind)原理图变量 ?case 以通过案例进行证明？

Question

我想定义一个案例证明规则，与proof (cases rule: <rule-name>)一起使用.我设法使用了 case_names和 consumes参数，但我没有设法绑定(bind)原理图变量 ?case ，因此，在使用我的规则进行证明的情况下，可以编写 show ?case ... .如何绑定(bind)？

具体来说:我有一个受 Mizar 启发的平凡集概念，即空集或单例集。我想通过空 与单例 案例分析来证明平凡集的属性。到目前为止，我有:

definition trivial where "trivial x = (x ⊆ {the_elem x})"

lemma trivial_cases [case_names empty singleton, consumes 1]:
  assumes "trivial X"
  assumes empty: "P {}"
      and singleton: "⋀ x . X = {x} ⟹ P {x}"
  shows "P X"
using assms unfolding trivial_def by (metis subset_singletonD)

我可以按如下方式使用它:

notepad
begin
  fix Q
  fix X::"'a set"
  have "trivial X" sorry
  then have "Q X"
  proof (cases rule: trivial_cases)
    case empty
    show "Q {}" sorry
  next
    case (singleton x)
    show "Q {x}" sorry
  qed
end

但我不能使用 show ?case .如果我尝试，它会给我错误消息“Unbound schematic variable: ?case”。 print_cases在证明中输出以下内容:

cases:
  empty:
    let "?case" = "?P {}"
  singleton:
    fix x_
    let "?case" = "?P {x_}"
    assume "X = {x_}"

这表明它不起作用，因为 ?P未绑定(bind) trivial .

顺便说一句:我使用它的完整上下文可以在 https://github.com/formare/auctions/blob/master/isabelle/Auction/SetUtils.thy 中看到。 .

Answer 1

正如 Joachim 已经提到的，与 induct 不同，cases 方法不绑定(bind)原理图变量 ?case。我会说进行案例分析的“规范”方式(作为证明方法)符合这种设置，因为通常只考虑不同的假设——这些假设加在一起是详尽无遗的——而结论在不同的情况下保持不变(在 Isabelle 中缩写为 ?thesis)。我会按如下方式设置您的 trivial_cases:

lemma trivial_cases [consumes 1, case_names empty singleton]:
  assumes "trivial X" and "X = {} ⟹ P" and "⋀x . X = {x} ⟹ P"
  shows "P"
  using assms by (auto simp: trivial_def)

然后你就可以像这样使用了

notepad
begin
  fix P and X :: "'a set"
  have "trivial X" sorry
  then have "P X"
  proof (cases rule: trivial_cases)
    case empty
    then show ?thesis sorry
  next
    case (singleton x)
    then show ?thesis sorry
  qed
end

简化器或显式展开负责将 X 分别专门化为 {} 和 {x}。

旁注:您可以通过添加属性 cases pred: trivial 进一步调整 trivial_cases。然后，每当 trivial ?X 是提供给 cases 的主要假设时，规则 trivial_cases 就会被隐式使用，即，您可以执行以下操作

have "trivial X" sorry
then have "P X"
proof (cases)

在上面的证明中。