Isabelle/HOL でのプログラミングと証明には、「データ型 exp」として表される単純な算術式で「algebra_simps」を使用することを提案する演習 2.4 があります。algebra_simps を使用して、そのような式のいくつかの単純なプロパティを証明する方法を誰かが例を挙げてもらえますか? たとえば、「Mult ab = Mult b a」?
一般に、同様の形式で表された単純な算術式の同等性を証明しようとしています (演算子のセットは限られています)。
1 に答える
2
関数を適切に定義しevalた場合は、例で指定したプロパティを次のように証明できます。
lemma Mult_comm: "eval (Mult a b) x = eval (Mult b a) x"
by simp
algebra_simps群と環 (この場合は整数など) の基本的な単純化規則の集まりです。これらは、この特定の例とは何の関係もありません。と入力すると、含まれている補題を見ることができますthm algebra_simps。
この特定の証明では、実際には は必要ありませんalgebra_simps。整数乗算の可換性は、とにかくデフォルトの単純化規則であるためです。
したがって、 の使用方法を示すためalgebra_simpsに、実際にそれらが必要な例を考えてみましょう: 乗算の右分配:
lemma Mult_distrib_right: "eval (Mult (Add a b) c) x = eval (Add (Mult a c) (Mult b c)) x"
これだけ試着apply simpしたらゴールにはまりそう
(eval a x + eval b x) * eval c x =
eval a x * eval c x + eval b x * eval c x
幸いなことに、ルールalgebra_simps(4)はまさにそれを言うルールです: thm algebra_simps(4)は、このルールが であることを示します(?a + ?b) * ?c = ?a * ?c + ?b * ?c。algebra_simpsルールを使用するように指示すると、Isabelle の単純化機能が自動的に適用されます。次のようにします。
apply (simp add: algebra_simps)
それ以外の
apply simp
于 2014-06-13T23:45:35.997 に答える