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

[Florian Haftmann]

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

Cheers,
	Florian

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

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- 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>