[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.