Associativity proof on Nats vs. Lists

Question

I am comparing the associativity proofs for Nats and Lists.

The proof on Lists goes by induction

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

But, the proof on Nats is

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

Why do I not need induction on the nat_add_assoc proof? Is it because of some automation happening on natural numbers?

Answer 1

The associativity proof on nat is also done by induction.

In Nat.thy you can find

instantiation nat :: comm_monoid_diff

which is the Isabelle way of saying nat has type class comm_monoid_diff. The following definitions and lemmas then show that the natural numbers are a commutative monoid under addition and that there's also subtraction.

In this block you find the proof:

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

The instantiation then gives us the lemma add_assoc on nat.