*To*: Filip Maric <filip at matf.bg.ac.rs>*Subject*: Re: [isabelle] Efficient Integers?*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Sat, 11 Feb 2012 22:01:20 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <Pine.LNX.4.64.1202111939120.17553@poincare.matf.bg.ac.rs>*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 (Macintosh; Intel Mac OS X 10.6; rv:9.0) Gecko/20111222 Thunderbird/9.0.1

You can do anything you want, at your own risk, if you modify what the code generator turns a certain type into. See the code generation documentation and see what Code_Integer does. Tobias Am 11/02/2012 20:06, schrieb Filip Maric: > Hello, > > although it is generally unsound, is there still a simple way to get > machine integers? > > 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)? > > Thank you very much, > Filip > > On Fri, 10 Feb 2012, Tobias Nipkow wrote: > >> PS No, you don't get machine integers, that would be unsound. You get >> big integers, which are language specific. I assume that in most of the >> languages we support big integers are like machine integers plus some >> fixed overhead, as long as you stay in the machine integer range. >>

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

- Previous by Date: Re: [isabelle] Efficient Integers?
- Next by Date: Re: [isabelle] Efficient Integers?
- Previous by Thread: Re: [isabelle] Efficient Integers?
- Next by Thread: Re: [isabelle] Efficient Integers?
- 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