isabelle - 使用 algebra_simps 的算术表达式等价

Question

在Isabelle/HOL 的编程和证明中，练习 2.4 建议在简单的算术表达式上使用“algebra_simps”，表示为“数据类型 exp”。有人可以举一个例子，如何使用 algebra_simps 证明这些表达式的一些简单属性？例如'Mult ab = Mult b a'？

一般来说，我试图证明以类似形式表示的简单算术表达式的等价性（使用有限的运算符集）。

Answer 1

如果您已经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