# [isabelle] a proof on primitive recursion

```Hi,

I have proved a simple associativity rule and tried to prove commutativity of an addition function:

imports Main

begin

datatype natural = Zero | Succ natural

primrec add :: "natural â natural â natural"

where

proof -

fix k m n

proof (induct k arbitrary: m n)

fix m n

proof (induct m arbitrary: n)

fix n

next

fix m n

qed

next

fix k m n

qed

qed

text{*

Questions:

* is it usually better in an induction proof to name the other variables as arbitrary? Does this make the proof easier?

* I have created this proof quite mechanically, copying premise as an assumption and the conclusion as the show clause.

Is there a better proof strategy in general, and in particular for this proof?

*}

proof -

fix m n

proof (induct m arbitrary: n)

fix n

proof (induct n)

next

fix n

from this show "add Zero (Succ n) = add (Succ n) Zero" by simp

qed

next

fix m n

from this show "add (Succ m) n = add n (Succ m)"

---

I am stuck here. There is no way of rewriting Succ m in the second parameter of Succ. What is the way out of the bottle?

Should I try another definition?

Should I use the proven theory of builtin natural numbers, prove an adequacy theorem of + and this add function and use the commutativity of + ?, or I can make it without this recourse?

- Gergely

```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.