2016-11-22 15 views
2

私は"\<forall>x. \<exists>y.\<forall>(z::real). P x y z"のような目標を持っています。すぐに私が"\<forall>x. \<exists>y.\<forall>(z::real). P x y (z-2)"と結論づけることができるルールはありますか?もしそうでなければ、私はこのタイプの目標をどのように証明するかについての一般的な助言に感謝します。普遍的な定量化された変数(Isabelle)の置換を可能にする補題/規則

は私がallIexIallEexEの多くを使用することによってそれを証明することができます知っているが、迅速かつ簡単な方法がなければならないように思えます。

答えて

1

Isabelle2016-1-RC2で、次の作品:

lemma 
    assumes "∀x. ∃y.∀(z::real). P x y z" 
    shows "∀x. ∃y.∀(z::real). P x y (z-2)" 
using assms by force 

あなたはあなたの目標を解決することができます証明メソッドのリストを与えること​​コマンドを使用することができます。

+0

これは役に立ちます。残念ながら、私が実際に証明したいことは、やや複雑で、これを使って動作しません。 –

+1

自動化を支援するために、最小量の作業のみを実行して、もう一方の後に1つの量子をはがしてみることができます。 – larsrh

関連する問題