# 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.*