Isabelleでルール誘導と変数一般化を組み合わせるにはどうすればよいですか？

Question

イザベルでは、arbitraryキーワードを使用して、誘導プルーフの変数を一般化できます。これは間違いなく普通の誘導のために働きます。apply (induction n arbitrary: m)のように。私はapply (induction rule: R.induct)のようにルールの誘導をすることもできます。しかし、ルール誘導を使用するときに、どのように変数を一般化できますか？

私の特定の使用例では、形式​​の定理を証明する必要があります。述語Rが誘導的に定義されており、ルール誘導を使用したいと思います。変数yは、証明では修正できませんが、任意である必要があります。回避策として、私は代わりにR x ⟹ (∀ y . S y ⟶ ⟨…⟩)の定理を証明しましたが、スレッジハンマーに頼らなくてもそれを証明することはできませんでした。また、∀と⟶を使用するのは正式ではないと思います。

Answer 1

arbitraryとruleを問題なく組み合わせることができます。ただし、arbitraryはruleより前に表示されなければなりません。