Re: [isabelle] Automatic derivation of a total order on datatypes
as Andreas already stated, there is such an order generator in the AFP.
However, the tactics in the AFP-Entry for the Isabelle2012 release version
contain some known gaps, so that the generator may fail on some datatypes.
All known gaps have been fixed in the development version of the AFP.
So, if you are working with the development version of Isabelle, just use the development version of the AFP.
If however, you are working with Isabelle2012, then please download a fixed version of the AFP-entry at
which contains all the fixes of the order generator and works with Isabelle2012.
Am 14.11.2012 um 08:10 schrieb Andreas Lochbihler <andreas.lochbihler at kit.edu>:
> 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
> 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.edu
> KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum in der Helmholtz-Gemeinschaft
René Thiemann mailto:rene.thiemann at uibk.ac.at
Computational Logic Group http://cl-informatik.uibk.ac.at/~thiemann/
Institute of Computer Science phone: +43 512 507-6434
University of Innsbruck
This archive was generated by a fusion of
Pipermail (Mailman edition) and