isabelle - 適用スタイルの目標に変数をドロップする

Question

最近、適用スタイルの証明で不要な前提を削除する方法を学んだので、不要な変数を削除する方法を知りたいと思っています。つまり、私が目標を持っているとします

1. !!x y z. A ⟹ B ⟹ C

whereは、またはyには現れません。次のように変換するにはどうすればよいですか？ABC

1. !!x z. A ⟹ B ⟹ C

Answer 1

triv_forall_equality冗長なパラメーターを削除するための純粋なルールです。prune_params_tacML 戦術としてそれを行うこともあり、すべてのサブゴールで動作します。後者は、実際にはほとんど必要とされないため、Isar 証明方法として公開されていないことに注意してsimpくださいauto。

via のアプローチ(simp only: triv_forall_equality)は多くの状況で機能しますが、問題もあります。Isabelle only/HOL の修飾子は、指定された simp ルールを「のみ」使用するだけではありません。これには算術ソルバーなどが含まれており、状況によっては驚きや混乱を引き起こす可能性があります。

prune_params_tacIsar メソッド言語内で正確に模倣するために、使用できます(unfold triv_forall_equality)が、小さな概念上の障害があります。方程式を単にインフォールディングするのではなく、任意の書き換えを使用することは、c = t単なる歴史的な事故です。

Answer 2

シンプルな：

apply simp

トリックを行います。目標状態で他の変換を実行したくない場合は、次を試すことができます。

apply (simp only: triv_forall_equality)

これにより、不要なメタ量指定子が削除されますが、それ以外の場合は目標状態は変更されません。