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



Dear René

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

http://cl-informatik.uibk.ac.at/software/ceta/Datatype_Order_Generator.tgz

which contains all the fixes of the order generator and works with Isabelle2012.

Best regards,
René


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

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