如何在 Isabelle 中将规则归纳与变量泛化结合起来？

Question

在 Isabelle 中，我可以使用 arbitrary 关键字概括归纳证明中的变量。这绝对适用于普通归纳，例如apply (induction n arbitrary: m)。我也可以进行规则归纳，例如apply (induction rule: R.induct)。但是在使用规则归纳的时候如何泛化变量呢？

在我的特定用例中，我需要证明R x ⟹ S y ⟹ ⟨…⟩ 形式的定理。谓词R 是归纳定义的，我想对其使用规则归纳。变量y 在证明中不能固定，但必须是任意的。作为一种解决方法，我已经证明了定理 R x ⟹ (∀ y . S y ⟶ ⟨…⟩)，但如果不使用大锤我无法证明它，而且我还猜想这里使用 ∀ 和 ⟶ 是不规范的。

Answer 1

您可以毫无问题地组合arbitrary 和rule。但是，arbitrary 必须出现在 rule 之前。