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.