Re: [isabelle] rep_datatype and Datatype exception

Hi all,

the issue with rep_datatype is that it started as a semi-official
bootstrap device for HOL and, over the last years, turned more and more
in a user-space command which still carries around restrictions from
that time.  For this sake I recommend to prefer datatype, and use
rep_datatype only under special conditions.

Traditionally, Isabelle/HOL is built in a way that there is practically
only one way to introduce a certain type, although there might be a
couple of legitimate views on that type (e.g. multisets either as
typedef with a restriction predicate over 'a => nat or a quotient of 'a
list).  This is indeed a constructivism which has no justification
except pragmatism, and maybe future developments should lift that
restriction.  For the moment, the only known exception to this is indeed
rep_datatype, which in its current implementation is an
underapproximation of what it should be properly.

> To the Isabelle developers: I was able to get a little further on this
> example by modifying HOL/Tools/Datatype/datatype_data.ML like this:

> Now the rep_datatype command produces the right goals for me to prove,
> but it raises another Datatype exception after I finish the proof.
> Maybe whoever is currently maintaining the datatype package (Stefan or
> Florian?) can follow up on this.

Maybe I find some time to have a look at it.




PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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