Isabelle Proves Commutativity to Add

Question

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

Definition add:

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

Associative Proof:

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

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 only have subtitle 3 left:

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

EDIT: I'm not really looking for an answer, like a push in the right direction. These are exercises from a book called Concrete Sementics.

Answer 1

(.. , ). , induct, (, apply (auto)).

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

:

 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)

.

• add, , .. add 0 m = m. , add m 0 = m. . ,

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

  (, simp auto) [simp]. simp, .

• add, (add k m = add m k) Suc (add m k) = add m (Suc k). add, . ( , , add .) add m (Suc n) = Suc (add m n), .

Answer 2

RainyCats : " ". add , Isar.

, k:

• k= 0 add (add 0 m) z = add 0 (add m z).

  add:

  • add (add 0 m) z ⇢ add m z
  • add 0 (add m z) ⇢ add m z

  =.

• k= Suc k'

  • add (add k' m) z = add k' (add m z).
  • add (add (Suc k') m) z = add (Suc k') (add m z).

  add:

  • add (add (Suc k') m) z ⇢ add (Suc (add k' m)) z ⇢ Suc (add (add k' m) z)
  • add (Suc k') (add m z) ⇢ Suc (add k' (add m z))

  : Suc (add (add k' m) z) ⇢ Suc (add k' (add m z))

  =.

Isar :

lemma add_Associative: "add(add k m) z = add k (add m z)"
proof (induction k)
  case 0
    have "add (add 0 m) z = add m z" by (subst add.simps, intro refl)
    moreover have "add 0 (add m z) = add m z" by (subst add.simps, intro refl)
    ultimately show ?case by (elim ssubst, intro refl)
next
  case (Suc k')
    have "add (add (Suc k') m) z = add (Suc (add k' m)) z" by (subst add.simps, intro refl)
    also have "… = Suc (add (add k' m) z)" by (subst add.simps, intro refl)
    also have "… = Suc (add k' (add m z))" by (subst Suc, intro refl)
    moreover have "add (Suc k') (add m z) = Suc (add k' (add m z))" by (subst add.simps, intro refl)
    ultimately show ?case by (elim ssubst, intro refl)
qed

by ... by simp.