Доказательство ассоциативности Nats vs. Lists

Question

Я сравниваю доказательства ассоциативности для Nats и Lists.

Доказательство на списках идет по индукции

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

Но доказательство на Натса

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

что такое Изабель 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,