Re: [isabelle] Automatic derivation of a total order on datatypes

Hi René,

René Thiemann has implemented such support, it is available in the Archive of Formal Proofs:


Am 14.11.2012 00:38, schrieb René Neumann:

is it possible to automa(t/g)ically instantiate a datatype as linorder,
if it is enough that there exists any order (e.g. the order of the
constructors in the definition with the restriction that all arguments
are of class linorder too)?

Use-case: Insert the datatype into a structure that needs an order on
its members. And if one does not care about the specific order, manually
defining it is quite cumbersome (especially for a large number of

Any hints on (semi-)automatic tools/tricks are highly appreciated :)

- René

Karlsruher Institut für Technologie
IPD Snelting

Dr. Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Am Fasanengarten 5, Geb. 50.34, Raum 025
76131 Karlsruhe

Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum in der Helmholtz-Gemeinschaft

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