*To*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Subject*: Re: [isabelle] bijections to/from the natural numbers*From*: Alexander Krauss <krauss at in.tum.de>*Date*: Tue, 09 Mar 2010 22:17:11 +0100*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>, Brian Huffman <brianh at cs.pdx.edu>*In-reply-to*: <4B96A8AA.5050201@informatik.tu-muenchen.de>*References*: <cc2478ab1003091151w5ca1e422q7115256177b91109@mail.gmail.com> <4B96A8AA.5050201@informatik.tu-muenchen.de>*User-agent*: Mozilla-Thunderbird 2.0.0.22 (X11/20091109)

Florian Haftmann wrote:

I have only one comment: the standard naming scheme should be (as in Isabelle/ML)

foo_of_bar :: bar => foo

nat_to_int_bij n = (if 2 dvd n then int(n div 2) else -int(Suc n div 2)) Naming it "int_of_nat" would be confusing IMO.

Other naming suggestions: cantor_pair :: "nat * nat => nat" cantor_unpair :: "nat => nat * nat" (or cantor_split) Alex

**Follow-Ups**:**Re: [isabelle] bijections to/from the natural numbers***From:*Florian Haftmann

**References**:**[isabelle] bijections to/from the natural numbers***From:*Brian Huffman

**Re: [isabelle] bijections to/from the natural numbers***From:*Florian Haftmann

- Previous by Date: [isabelle] Workshop PAR'10 at FLOC'10: 2nd CFP
- Next by Date: Re: [isabelle] Generalized elimination rule?
- Previous by Thread: Re: [isabelle] bijections to/from the natural numbers
- Next by Thread: Re: [isabelle] bijections to/from the natural numbers
- Cl-isabelle-users March 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