嵌套析取的证明(规则disjE) [英] proof (rule disjE) for nested disjunction

问题描述

在Isar风格的Isabelle证明中，这很好用:

In Isar-style Isabelle proofs, this works nicely:

from `a ∨ b` have foo
proof
  assume a
  show foo sorry
next
  assume b
  show foo sorry
qed

此处由proof调用的隐式规则为rule conjE.但是，我应该在其中放置哪些内容，以使其不止一种分离:

The implicit rule called by proof here is rule conjE. But what should I put there to make it work for more than just one disjunction:

from `a ∨ b ∨ c` have foo
proof(?)
  assume a
  show foo sorry
next
  assume b
  show foo sorry
next
  assume c
  show foo sorry
qed

推荐答案

在编写问题时，我有一个主意，事实证明这是我想要的:

While writing the question, I had an idea, and it turns out to be what I want:

from `a ∨ b ∨ c` have foo
proof(elim disjE)
  assume a
  show foo sorry
next
  assume b
  show foo sorry
next
  assume c
  show foo sorry
qed

这篇关于嵌套析取的证明(规则disjE)的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！