Re: [isabelle] datatype definition performance

Last time Michael and I looked at this, some of the theorems produced by
the datatype package, e.g., the prim. rec. theorem, had unavoidable quadratic
behaviour in their proofs. And it seemed to me that nested datatypes
were even worse, but my memory could be faulty.


On Feb 8, 2006, at 4:33 AM, Stefan Berghofer wrote:

Peter Sewell wrote:
(still, 9 minutes to really prove those theorems seems quite a while -
for curiosity, is it known how this should scale with the numbers of
mutually-recursive types and of constructors?)

Appendix B (page 88) of my diploma thesis, which is available at

contains a table with runtimes for various datatype definitions
and a comparison with John Harrison's datatype package for HOL Light
(unfortunately, the thesis is in German). For example, processing
a datatype with 62 constructors (representing the SML grammar) took
2759.88 seconds, whereas a datatype with 124 constructors (representing
the Verilog grammar) took 17516.06 seconds (measured on a Sun Ultra-2
workstation a long time ago).


Dr. Stefan Berghofer               E-Mail: berghofe at
Institut fuer Informatik           Phone: +49 89 289 17328
Technische Universitaet Muenchen   Fax:   +49 89 289 17307
Boltzmannstr. 3                    Room: 01.11.059
85748 Garching, GERMANY  

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