嵌套析取的证明(规则disjE)
嵌套析取的证明(规则disjE)
提问于 2013-04-09 20:12:27
在Isar风格的Isabelle证明中，这很好地工作：
from `a ∨ b` have foo
proof
assume a
show foo sorry
next
assume b
show foo sorry
qedproof在这里调用的隐式规则是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回答 3
Stack Overflow用户
回答已采纳
发布于 2013-04-09 20:12:27
在写这个问题的时候，我有了一个想法，事实证明它就是我想要的：
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
qedStack Overflow用户
发布于 2013-04-10 17:26:31
进行这种案例分析的另一种规范方法如下：
{ assume a
have foo sorry }
moreover
{ assume b
have foo sorry }
moreover
{ assume c
have foo sorry }
ultimately
have foo using `a ∨ b ∨ c` by blast也就是说，让一个自动工具在最后“弄清楚”细节。这在考虑算术情况时尤其有效(使用by arith作为最后一步)。
更新：使用新的consider语句可以执行以下操作：
notepad
begin
fix A B C assume "A ∨ B ∨ C"
then consider A | B | C by blast
then have "something"
proof (cases)
case 1
show ?thesis sorry
next
case 2
show ?thesis sorry
next
case 3
show ?thesis sorry
qed
endStack Overflow用户
发布于 2016-05-04 16:14:52
或者，为了区分不同的情况，似乎可以使用更通用的induct方法来执行您的命令。对于三种情况，这将像这样工作:证明一个引理disjCases3
lemma disjCases3[consumes 1, case_names 1 2 3]:
assumes ABC: "A ∨ B ∨ C"
and AP: "A ⟹ P"
and BP: "B ⟹ P"
and CP: "C ⟹ P"
shows "P"
proof -
from ABC AP BP CP show ?thesis by blast
qed您可以使用此引理，如下所示：
from `a ∨ b ∨ c` have foo
proof(induct rule: disjCases3)
case 1 thus ?case
sorry
next
case 2 thus ?case
sorry
next
case 3 thus ?case
sorry
qed缺点是你需要一堆引理来涵盖任何数量的情况，disjCases2，disjCases3，disjCases4，disjCases5等，但除此之外，它似乎工作得很好。
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/15901570
复制相关文章
相似问题
腾讯云开发者
