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: http://afp.sourceforge.net/entries/Datatype_Order_Generator.shtml

Best,
Andreas

Am 14.11.2012 00:38, schrieb René Neumann:
Hi,

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
constructors)...

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.edu
http://pp.info.uni-karlsruhe.de
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.