将任意方法应用于所有子目标的一般方法？

Question

假设我有一个应用样式证明中的子目标列表。我知道类似于

apply blast 

将为此列表中的许多子目标提供证据。有没有办法避免重复这一行？

例如，假设我有三个子目标，其中第一和第三是可证明使用上述方法，而第二种是可证明的东西，如

apply (metis lemma1 lemma2 ...) 

用于这种子目标幼稚证明将看起来像

apply blast 
    apply (metis lemma1 lemma2 ...) 
    apply blast 

我在寻找的是一种证明而不复制apply blast部分证明的方法。注意使用组合子+的方法不会达到此目的;它只是反复应用该方法直到第一次失败。

Answer 1

其实apply blast只会尝试解决第一个子目标。如果你想解决尽可能多的子目标尽可能你可以尝试

apply blast+ 

我不知道你想实现什么，而是你的using some_lemma另一种可能是

apply (insert some_lemma) 

这将插入some_lemma作为你所有子目标的额外假设。

更新： Isabelle中提供了一些基本的证明方法组合器（另请参见第6.4.1节：证明方法表达式，isar-ref）。所以，你可以例如

apply (blast | metis ...)+ 

将首先尝试blast且仅当此失败时metis ...解决一个子目标做。然而，它的用处取决于特定的子目标情况，例如，如果blast在失败之前需要很长时间，它可能不合适。通过最近的Isabelle/Eisbach证明方法语言可以获得更细致的证明方法控制（参见isabelle doc eisbach）。