# [isabelle] reasoning with even and odd numbers

Hello,

`I have a series of short, related questions regarding reasoning with
``even and odd numbers.
`

`There are a lot of examples on the inductive definitions of even
``numbers, such as the following from the book Concrete Semantics.
`
inductive ev :: "nat ⇒ bool" where
ev0: "ev 0" |
evSS: "ev n ⟹ ev (n + 2)"
Proving that 4 is even can be done like this.
lemmas four_is_even = evSS[OF evSS[OF ev0]]
lemma "ev (Suc(Suc(Suc(Suc 0))))"
by (rule four_is_even[simplified])

`Q1: Is there anyway to simplify "evSS[OF evSS[OF ev0]]" on the fly such
``that I don't need the lemma "four_is_even"?
`
Q2: I am not able to prove "ev 4". The closest that I got is this.
lemma "ev 4"
apply (subgoal_tac "ev (0 + 2 + 2)")
sorry
Simplification just yields "ev (Suc(Suc(Suc(Suc 0))))", not "ev 4".
How can I prove "ev 4"?

`Q3: I also wanted to prove that "¬ev 1", so I tried modifying the
``inductive definition as follows.
`
inductive ev :: "nat ⇒ bool" where
ev0: "ev 0" |
evS: "¬ev n ⟹ ev (n + 1)" |
evSS: "ev n ⟹ ev (n + 2)"
Isabelle told me that proof failed for the goal.
mono (λp x. x = 0 ∨ (∃n. x = n + 1 ∧ ¬ p n) ∨ (∃n. x = n + 2 ∧ p n))

`What's going on? If I can't define ev this way, what's the best way to
``prove "¬ev 1"
`
Maybe the questions weren't that short, sorry about that.
Any help on any of the questions are much appreciated.
Thank you,
Amarin

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