isabelle proving commutativity for add

Question

Im trying to prove commutativity in Isabelle/HOL for a self-defined add function. I managed to prove associativity but I'm stuck on this.

The definition of add:

fun add :: "nat ⇒ nat ⇒ nat" where
"add 0 n = n" |
"add (Suc m) n = Suc(add m n)"

The proof of associativity:

lemma add_Associative: "add(add k m) z = add k (add m z)"
apply(induction k)
apply(auto)
done

The proof of commutativity:

theorem add_commutativity: "add k m = add m k"
apply(induction k)
apply(induction m)
apply(auto)

I get the following goals:

goal (3 subgoals):
1. add 0 0 = add 0 0
2. ⋀m. add 0 m = add m 0 ⟹
     add 0 (Suc m) = add (Suc m) 0
3. ⋀k. add k m = add m k ⟹
     add (Suc k) m = add m (Suc k)

After applying auto I'm left with just subgoal 3:

3. ⋀k. add k m = add m k ⟹
     add (Suc k) m = add m (Suc k)

EDIT: Im not so much looking for an answer, as a push in the right direction. These are exercises from a book called Concrete Sementics.

Answer 1

I would suggest to make the proof as modular as possible (i.e., prove intermediate lemmas that will later help to solve the commutativity proof). To this end it is often more informative to meditate on the subgoals introduced by induct, before applyng full automation (like your apply (auto)).

lemma add_comm:
  "add k m = add m k"
  apply (induct k)

At this point the subgoals are:

 goal (2 subgoals):
  1. add 0 m = add m 0
  2. ⋀k. add k m = add m k ⟹ add (Suc k) m = add m (Suc k)

Lets look at them separately.

1. Using the definition of add we will only be able to simplify the left-hand side, i.e., add 0 m = m. Then the question remains how to prove add m 0 = m. You did this as part of your main proof. I would argue that it increases readability to proof the following separate lemma

   lemma add_0 [simp]:
     "add m 0 = m"
     by (induct m) simp_all
   

   and add it to the automated tools (like simp and auto) using [simp]. At this point the first subgoal can be solved by simp and only the second subgoal remains.

2. After applying the definition of add as well as the induction hypothesis (add k m = add m k) we will have to prove Suc (add m k) = add m (Suc k). This looks very similar to the second equation of the original definition of add, only with swapped arguments. (From that perspective, what we had to prove for the first subgoal corresponded to the first equation in the definition of add with swapped arguments.) Now, I would suggest to try to prove the general lemma add m (Suc n) = Suc (add m n) in order to proceed.