*To*: Isabelle Users <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] reasoning with even and odd numbers*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Wed, 15 Oct 2014 08:00:33 +0200*In-reply-to*: <543DEC15.1020302@illinois.edu>*References*: <543DEC15.1020302@illinois.edu>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.9; rv:24.0) Gecko/20100101 Thunderbird/24.6.0

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)"

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]] by(simp add: numeral_eq_Suc)

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

**Follow-Ups**:**Re: [isabelle] reasoning with even and odd numbers***From:*Amarin Phaosawasdi

**References**:**[isabelle] reasoning with even and odd numbers***From:*Amarin Phaosawasdi

- Previous by Date: [isabelle] reasoning with even and odd numbers
- Next by Date: Re: [isabelle] reasoning with even and odd numbers
- Previous by Thread: [isabelle] reasoning with even and odd numbers
- Next by Thread: Re: [isabelle] reasoning with even and odd numbers
- Cl-isabelle-users October 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list