# Re: [isabelle] reasoning with even and odd numbers

```I definitely learned a lot here. Thanks.
```
```For more complicated examples, you can prove the following (intuitively
obvious) lemma:
```
```lemma ev_imp_not_ev_Suc: "ev n ⟹ ¬ev (Suc n)"
```
```I will not give you the proof – it can be proven by induction over the
inductive definition of ‘ev’ and I think it makes a nice exercise. You
may also want to look up the ev.cases rule and the ‘inductive_cases’
command.
```
```
Here's one way I did it.

lemma suc0:"¬ev (Suc 0)"
by (subst ev.simps, simp)

lemma sucSS:"⋀n. ev n ⟹ ¬ ev (Suc n) ⟹ ¬ ev (Suc (Suc (Suc n)))"
by (erule ev.cases) (subst ev.simps, simp)+

lemma "ev n ⟹ ¬ev (Suc n)"
by (induction rule: ev.induct) (simp add: suc0 sucSS)+

```
The other way, as you hinted, was adding the elimination rules so that auto can use them.
```
inductive_cases evE[elim!]: "ev n"
lemma "ev n ⟹ ¬ev (Suc n)"
by (induction rule: ev.induct) auto

I'm a little curious though.

How did evE[elim!] help me with, for example, "¬ev (Suc 0)"?

As you can see above, without evE, I would prove it as follows.

lemma "¬ev (Suc 0)"
by (subst ev.simps, simp)

But with it, I can simply do.

lemma "¬ev (Suc 0)"
by auto

```
How would I prove "¬ev (Suc 0)" using evE (or ev.cases) explicitly the way that auto is presumably using behind the scenes?
```
Amarin

```

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