Welcome to OGeek Q&A Community for programmer and developer-Open, Learning and Share
Welcome To Ask or Share your Answers For Others

Categories

0 votes
344 views
in Technique[技术] by (71.8m points)

isabelle - proof (rule disjE) for nested disjunction

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

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
See Question&Answers more detail:os

与恶龙缠斗过久,自身亦成为恶龙;凝视深渊过久,深渊将回以凝视…
Welcome To Ask or Share your Answers For Others

1 Reply

0 votes
by (71.8m points)

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

与恶龙缠斗过久,自身亦成为恶龙;凝视深渊过久,深渊将回以凝视…
OGeek|极客中国-欢迎来到极客的世界,一个免费开放的程序员编程交流平台!开放,进步,分享!让技术改变生活,让极客改变未来! Welcome to OGeek Q&A Community for programmer and developer-Open, Learning and Share
Click Here to Ask a Question

1.4m articles

1.4m replys

5 comments

57.0k users

...