Nats vs. Lists的相关性证明

Question

我正在比较Nats和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说的nat有类型的方式comm_monoid_diff.下面的定义和引理表明,自然数是加法下的可交换幺半群,并且还有减法.

在这个区块中,您可以找到证据:

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

实例化则给了我们引理add_assoc上nat.