10

我有一个结构如下的伊莎贝尔证明：

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关键字，但可以看到正确的假设？

4

3 回答 3

6

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

proof cases
  assume "n = 0"
  show ?thesis sorry
next
  assume "n ≠ 0"
  show ?thesis sorry
qed
于 2013-05-18T23:16:36.183 回答
5

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

proof (cases "n = 0")
  case False
  show ?thesis sorry
next
  case True
  show ?thesis sorry
qed
于 2013-05-19T09:41:53.657 回答
2

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
于 2013-10-09T19:39:32.310 回答