[isabelle] Question about simp

[Ching-Tsun Chou]

Consider the following inductive definition and a simple lemma about it:

inductive ev' :: "nat ⇒ bool" where
ev'_0: "ev' 0" |
ev'_2: "ev' 2" |
ev'_sum: "ev' n ⟹ ev' m ⟹ ev' (n+m)"

lemma test1: "ev' n ⟹ ev' (n + 2)"
apply (rule ev'_sum)
by (simp_all add: ev'_2)

But when I tried to prove the lemma using simp:

by (simp add: ev'_sum ev'_2)

Isabelle seems to try to turn the (n+2) into (Suc (Suc n)) and then get
stuck:

Failed to finish proof⌂:
goal (1 subgoal):
1. ev' n ⟹ ev' (Suc (Suc n))

Is there a way to tell Isabelle not to do that?

Thanks!
- Ching Tsun