用algebra_simps实现算术表达式的等价性

Question

在在Isabelle/HOL中的编程和证明中有练习2.4，它建议在简单算术表达式上使用'algebra_simps‘，表示为'datatype exp’。有人能给出一个例子，如何使用algebra_simps来证明这些表达式的一些简单属性？例如'Mult a b= 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规则，则伊莎贝尔的简化器将自动应用它，方法如下：

apply (simp add: algebra_simps)

而不是

apply simp