gpt4 book ai didi

isabelle - 嵌套析取的证明(规则 disjE)

转载 作者:行者123 更新时间:2023-12-04 11:08:49 25 4
gpt4 key购买 nike

在 Isar 风格的 Isabelle 证明中,这很有效:

from `a ∨ b` have foo
proof
assume a
show foo sorry
next
assume b
show foo sorry
qed
proof调用的隐式规则这是 rule conjE .但是我应该在那里放什么才能使它不仅适用于一种分离:
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

最佳答案

在写这个问题的时候,我有了一个想法,结果是我想要的:

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

关于isabelle - 嵌套析取的证明(规则 disjE),我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/15901570/

25 4 0
Copyright 2021 - 2024 cfsdn All Rights Reserved 蜀ICP备2022000587号
广告合作:1813099741@qq.com 6ren.com