0

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?

Niki
  • 11
  • 1
  • Why are you looking at source code from the Isabelle2013 distribution and not at the up to date files from Isabelle2017? – ammbauer Feb 27 '18 at 22:37
  • Good point! Just because the Isabelle2013 came up when I searched for the proofs. Let me update my search. – Niki Feb 28 '18 at 15:01

1 Answers1

5

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.

ammbauer
  • 426
  • 2
  • 7
  • Well, this still does not explain how the same proof can be done without explicit use of the induct strategy. – Niki Feb 28 '18 at 15:02
  • When you write `rule add_assoc`, that means you just apply the theorem `add_assoc`. Basically, you're using a theorem that has been proven elsewhere. As ammbauer pointed out, *that* proof *was* done by induction, so of course you don't have to do the induction again. In fact, I'm not sure why `nat_add_assoc` even exists since it's literally the same thing as `add_assoc` specialised to `nat`. Probably historic reasons. – Manuel Eberl Feb 28 '18 at 21:49
  • oh, thanks! It makes sense! It is shadowing the names! I though it was doing a recursive call on the theorem to be proved! – Niki Mar 01 '18 at 18:18
  • There is no shadowing going on, as `nat_add_assoc` and `add_assoc` are not the same. – chris Mar 14 '18 at 11:36