[isabelle-dev] Alternative approach to »efficient« natural numbers

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Sun Apr 29 15:51:26 CEST 2012

Hi all,

I did an experiment with Flyspeck-Tame (on macbroyXY):

Using the Efficient_Nat theory where Isabelle nat is directly
represented as PolyML int:

> Finished HOL-Flyspeck-Tame (11:50:46 elapsed time, 13:54:35 cpu time, factor 1.17)

Using the Target_Numeral theory where Isabelle nat is an abstract
datatype over PolyML int:

> Finished HOL-Flyspeck-Tame (10:55:49 elapsed time, 13:57:31 cpu time, factor 1.27)

The reason why this has the same magnitude of runtime is that in PolyML
trivial datatypes like

> datatype nat = Nat of int
> fun int_of (Nat k) = k

are optimized away.

This is a proof of concept that it is possible in the future to have
just *one* type which is mapped onto target language numerals by
default, and to refine nat and/or int to use this is implementation if
desired, rather than adhoc code_const setups etc. for nat and int.  Cf.
also https://isabelle.in.tum.de/community/Numerals


P.S. This his no consequences for the upcoming release.


PGP available:

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 262 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20120429/b9c957c6/attachment.asc>

More information about the isabelle-dev mailing list