*To*: filip at matf.bg.ac.rs*Subject*: Re: [isabelle] Efficient Integers?*From*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Date*: Sun, 12 Feb 2012 10:53:54 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <Pine.LNX.4.64.1202111939120.17553@poincare.matf.bg.ac.rs>*Organization*: TU Munich*References*: <4F34D68F.1070409 at irisa.fr> <4F34DB4C.8080206 at in.tum.de> <Pine.LNX.4.64.1202111939120.17553@poincare.matf.bg.ac.rs>*User-agent*: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.9.2.26) Gecko/20120131 Lightning/1.0b2 Thunderbird/3.1.18

Hi Filip, > I have an application that uses only positive integers between 0 and > 2^12 and the only operation performed on these numbers is bitwise > disjunction (which leaves them in this range). In the logic, I used the > nat type and define the bit-or using div/mod, but, of course, this is > very slow when executed (proof checking takes almost half an hour since > there is a lot computation involved). Since the range is bounded, there > is a "meta-theoretic" argument that machine integers would not introduce > unsoundness, so I wonder if it is possible to "cheat" and use them and > instruct the code generator to call the target-language bit-or in place > of my div/mod defined bit-or (I tried something like code_const "bitor" > (SML "IntInf.orb ((_), (_))") (Haskell infixl 6 "(.|.)"), but it did not > give expected efficiency since big integers are used). Evaluations are > used within a "proof-by-evaluation" paradigm and I use the method "by > eval". > > I suppose the other option would be not to use nats but machine words in > the logic level, but then the formalization would be a bit more > complicated, and I not sure what theory I should start from (I assume > there is such a formalization in the Library)? if you really only need disjunction, I would recommend the following: * define your own type for positive integers between 0 and 2^12; HOL/Library/Dlist.thy (among others) is a helpful example to glimpse from * setup code generation for that type as sketched above. There is a formalization of bit-arithmetic in HOL/Word, but it is not very suitable to setup a customary code generation for specific target languages because the bit length is encoded into a type argument, a concept which cannot be mapped straighforwardly to target languages. Hope this helps, Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

**Attachment:
signature.asc**

**References**:**Re: [isabelle] Efficient Integers?***From:*Filip Maric

- Previous by Date: Re: [isabelle] Efficient Integers?
- Next by Date: [isabelle] ICECCS 2012 - Extended deadline March 1st
- Previous by Thread: Re: [isabelle] Efficient Integers?
- Next by Thread: [isabelle] 2 new AFP entries
- Cl-isabelle-users February 2012 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