isabelle - Nats vs. Lists 的关联性证明

Question

我正在比较Nats和Lists的关联性证明。

Lists 上的证明是通过归纳法进行的

lemma append_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)"
by (induct xs) auto

但是，关于 Nats 的证明是

lemma nat_add_assoc: "(m + n) + k = m + ((n + k)::nat)"
by (rule add_assoc)

为什么我不需要对nat_add_assoc证明进行归纳？是因为自然数上发生了一些自动化吗？

Answer 1

上的关联性证明nat也是通过归纳来完成的。

在Nat.thy你可以找到

instantiation nat :: comm_monoid_diff

这是 Isabelle 的说法nathas type class comm_monoid_diff。下面的定义和引理表明，自然数是加法下的可交换幺半群，并且还有减法。

在此块中，您可以找到证明：

instance proof
  fix n m q :: nat
  show "(n + m) + q = n + (m + q)" by (induct n) simp_all

然后实例化给了我们引理add_assocon nat。