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?

Thanks,

-Simon.

On 14 November 2012 09:42, René Thiemann <rene.thiemann at uibk.ac.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
>
> 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é
>




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