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

```
On 15/10/2014 05:37, Amarin Phaosawasdi wrote:
```
```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)"
```
```
```
For a start, note that a bit further down, in the section "In Isabelle", the "+2" is replaced by "Suc(Suc". The "+2" version was just an intuitive starter.
```
```
```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"?
```
```
Yes, you can combine attributes with ",":
evSS[OF evSS[OF ev0], simplified]

```
```Q2: I am not able to prove "ev 4". The closest that I got is this.
```
```
Numerals are distinct from Suc terms.

```
```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"?
```
```
One possibility:

lemma "ev 4"
using evSS[OF evSS[OF ev0]]

```
where numeral_eq_Suc expands numerals to Sc terms. There may also exist a set of rules that performs the opposite conversion.
```
```
```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)"
```
```
Rule evS violates the format for inductive definitions (see 4.5.3).

```
```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"
```
```
You have to rephrase it such that you can apply induction, eg

ev n ==> n ~= 1

Tobias

```
```Maybe the questions weren't that short, sorry about that.

Any help on any of the questions are much appreciated.

Thank you,
Amarin

```
```

```

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

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