Isabelle: [simp] leading to an infinite loop

Question

I am trying to solve the simple lemma "add m (Suc n) = add n (Suc m)" by induction over m. I tried solving the last remaining subgoal after applying auto by another lemma, howerver if i use the simplification rule on that auxiliary lemma it leads to an infinite loop at apply(auto) in the original lemma.

Do you know why that happens? And if my way doesn't work, how would i solve the original lemma?

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

lemma aux:"Suc n = add n (Suc 0)"
  apply(induction n)
   apply(auto)
  done

lemma original:"add m (Suc n) = add n (Suc m)"
  apply(induction m arbitrary: n)
   apply(auto)
  oops

These are the lemmas in question, i also proved commutatvity of add in a seperate lemma. The subgoal of "original" after apply(auto) is

1. ⋀n. Suc n = add n (Suc 0) When adding [simp] to the lemma aux, the apply(auto) in the lemma original gets into an infinite loop.

Sorry if this is trivial, i am just getting into Isabelle.

Answer 1

Designing good simp rules is an art in and of itself. In your case, aux is exactly oriented the wrong way round. You have Suc n on the left-hand side and you have something that Suc n matches on on the right-hand side, namely Suc 0. So that alone gives you an infinite loop.

If you flip the two sides of aux it works fine.

A general rule is that in a simp rule, the right-hand side should be ‘simpler’ than the left-hand one. In this case it's very clear what that means, but there are other cases where it is trickier, e.g. if you have something like f (x + y) = f x + f y.

In those cases the typical approach is to either globally decide that your goal is to push f as far inside the term as possible or to pull it out as far as possible, and then design all simp rules involving f accordingly.