有没有办法自动拆分连接？

我想在伊莎贝尔证明A /\ B /\ C /\ D /\ E /\ F。我如何在proof(rule ...)中自动将子目标分成6个子目标，然后我可以单独证明它们？有没有办法自动拆分连接？

当然，我可以写proof(rule conjI) 5次，但也许有一个更优雅的方式来分裂一步？

来源

2013-11-28 Nadezhda Baklanova

使用intro方法：proof (intro conjI)

来源

2013-11-28 14:49:37

谢谢！伟大的作品 –

我的理解是'intro foo'与'（rule foo）+'相同，即它尽可能多地应用规则'foo'。 –

情况并非如此。 '（rule foo）+'只会试图将规则应用到第一个新的子目标，而'intro foo'也会将其应用于所有其他出现的新子目标。例如，用'引理'（a∧b）∧c∧d“'并比较'apply（rule conjI）+'和'apply（intro conjI）'。在第一种情况下，你可以得到子目标'a'，'b'和'c∧D'，在第二种情况下，你得到'a'，'b'，'c'和'd'。 –

另一种方式来证明这些目标是通过使用原始证据块。例如，如下

lemma "A & B & C & D & E & F" 
proof - 
    { have "A" ... } 
    moreover 
    { have "B" ... } 
    moreover 
    { have "C" ... } 
    moreover 
    { have "D" ... } 
    moreover 
    { have "E" ... } 
    moreover 
    { have "F" ... } 
    ultimately 
    show ?thesis by blast 
qed

不同的是，在这里你做了更多的前瞻性证明（我发现有时更具可读性）。你只是从你知道的事情开始，无论如何你都必须证明，最终让一些自动化的方法（这里是blast）找出“微不足道”的步骤。

来源

2013-12-03 09:17:14 chris

有没有办法自动拆分连接？

回答

相关问题