*To*: Christoph Feller <c_feller at informatik.uni-kl.de>*Subject*: Re: [isabelle] even/odd with primrec*From*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Date*: Tue, 20 Apr 2010 17:32:01 +0200*Cc*: isabelle-users <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <i2ma1e5e35a1004190716jec2d7a0cyb375e8adc2e1b2f3@mail.gmail.com>*Organization*: TU München, Lehrstuhl Software and Systems Engineering*References*: <i2ma1e5e35a1004190716jec2d7a0cyb375e8adc2e1b2f3@mail.gmail.com>*User-agent*: Thunderbird 2.0.0.24 (X11/20100317)

> primrec even :: "nat => bool" > and odd :: "nat => bool" where > "even 0 = True" | > "even (Suc n) = odd n" | > "odd 0 = False" | > "odd (Suc n) = even n" Also note that the original specification of things does not matter as long as you can derive the desired properties. In that case you could e.g. define definition even :: "nat => bool" where "even n <-> n mod 2 = 0" definition odd :: "nat => bool" where odd n <-> n mod 2 = 1" and derive the recursive rules: lemma [simp]: "even 0 = True" "even (Suc n) = odd n" "odd 0 = False" "odd (Suc n) = even n" <proof> Also note that even/odd is already present in the HOL theory Parity; just import theory Complex_Main to use it. Hope this helps, Florian -- Home: http://www.in.tum.de/~haftmann PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

**Attachment:
signature.asc**

**References**:**[isabelle] even/odd with primrec***From:*Christoph Feller

- Previous by Date: [isabelle] limiting unfolding using definitions
- Next by Date: Re: [isabelle] Questions about . method
- Previous by Thread: Re: [isabelle] even/odd with primrec
- Next by Thread: [isabelle] finding a rule
- Cl-isabelle-users April 2010 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