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

Hi René

The derive linorder works really well, but I've come across an odd example
which doesn't work, namely:

datatype vbasic = BoolI bool | ListI "vbasic list"
derive linorder vbasic

Fails to prove. If I replace the bool with an int or remove the list
constructor, it works fine. There seems to be an odd interaction between
bool and list. The following works fine:

datatype vbasic = TrueI | FalseI | IntI "int" | ListI "vbasic list"

Do you know what's causing this?



On 14 November 2012 09:42, René Thiemann <rene.thiemann at> wrote:

> 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
> which contains all the fixes of the order generator and works with
> Isabelle2012.
> Best regards,
> René

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