3

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

具体来说：我有一个受 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. 如果我尝试，它会给我错误消息“未绑定的示意图变量：？case”。 print_cases在证明里面输出以下内容：

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

这表明它不起作用，因为?P不受trivial.

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

4

1 回答 1

3

正如 Joachim 已经提到的，与 不同induct的是，该cases方法不绑定示意图变量?case。我会说进行案例分析（作为证明方法）的“规范”方式符合这种设置，因为通常只考虑不同的假设——它们加在一起是详尽无遗的——而结论保持不变（缩写为?thesisin伊莎贝尔）在不同的情况下。我会设置你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}。

旁注：您可以trivial_cases通过添加属性进一步调整cases pred: trivial。然后，无论何时trivial ?X将主要假设提供给cases，都会隐式使用该规则trivial_cases，即，您可以执行以下操作

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

在上述证明中。

于 2013-09-09T01:43:30.957 回答