如何通过案例明确正确地假设 Isabelle/Isar 证明的第二种情况？答案

【问题标题】：How to make the assumption of the second case of an Isabelle/Isar proof by cases explicit right in place?如何通过案例明确正确地假设 Isabelle/Isar 证明的第二种情况？
【发布时间】：2013-05-18 22:02:53
【问题描述】：

我有一个结构如下的 Isabelle 证明：

proof (cases "n = 0")
  case True
  (* lots of stuff here *)
  show ?thesis sorry
next
  case False
  (* lots of stuff here too *)
  show ?thesis sorry
qed

第一个案例实际上有好几页长，所以在阅读第二个案例时，普通读者甚至我自己都不清楚False 指的是什么。（嗯，它实际上是，但不是来自阅读，只是在交互式环境中：如果，例如，在 Isabelle/jEdit 中，将光标放在 case False 之后，你会看到 n ≠ 0在“输出”面板中的“this”下。）

那么是否有一种语法允许明确假设“False”情况，这样读者既不必与 IDE 交互，也不必向上滚动到 proof 关键字，但可以看到假设到位了吗？

【问题讨论】：

重新开放！让我们从 cmets 重新开始，好吗？

标签： proof isabelle isar

【解决方案1】：

在这种情况下，通过明确说明每种情况的假设，证明变得更具可读性：

proof cases
  assume "n = 0"
  show ?thesis sorry
next
  assume "n ≠ 0"
  show ?thesis sorry
qed

【讨论】：

注意：如果您重新订购箱子，这将失败（正如@LarsNoschinsiki 在对我的回答的评论中指出的那样）。

【解决方案2】：

如果False 的大小写较短，只需将其放在首位。 Isar 区块中的证明顺序无关紧要：

proof (cases "n = 0")
  case False
  show ?thesis sorry
next
  case True
  show ?thesis sorry
qed

【讨论】：

一般来说，如果我们进行案例分析的属性很短（如n = 0），为了可读性，我总是更喜欢显式版本而不是case False、case True . （有趣的是，从组合性的角度来看，情况正好相反。）
请注意，如果您使用参数调用 cases 方法，则只能重新排序案例。如果您使用proof cases assume P ... next assume "~P" ... 形式，则否定的情况必须是第二个（因为目标中有原理图，由第一个show 命令实例化）。
我什至不知道你可以在没有参数的情况下使用cases :-)

【解决方案3】：

Isar 允许同一主题有多种变化。保留原始大纲，您可以像这样明确中间事实：

proof (cases "n = 0")
  case True
  (* lots of stuff here *)
  from `n = 0` show ?thesis sorry
next
  case False
  (* lots of stuff here too *)
  from `n ≠ 0` show ?thesis sorry
qed

这是对原始证明大纲的保守扩展，即它不会对检查、统一、搜索等策略进行任何更改。

一般情况下

note `prop`

等价于

have "prop" by fact

【讨论】：