如何通过明确的恰当的案例来假设Isabelle/Isar证明的第二个案例？

Question

我有一个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"下看到.)

那么是否有一种语法允许假设"假"情况明确,这样读者既不必与IDE交互,也不必向上滚动到proof关键字,但是可以正确看待假设？

Answer 1

在这种情况下,通过明确说明每个案例的假设,证明变得更具可读性:

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

Answer 2

如果False案例较短，只需将其放在第一位。Isar 区块中的证明顺序无关紧要：

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