Re: [isabelle] Efficient Integers?

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,


PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.