Re: [isabelle] rep_datatype and Datatype exception
On Fri, 17 Dec 2010, Florian Haftmann wrote:
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.
Right. And of course there is no "bug" in the package, it merely tells
you via a low-level exception that it cannot handle certain cases.
I have recently had other surprises with 'rep_datatype', which are in fact
to be expected, since the main characterizing theorems that your have
already usually differ from what 'datatype' would produce (induct rule
etc.). This means one should not lean out of the window too much, and use
plain datatype from the very start whenever this is possible.
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.
The situation of the datatype package is twofold:
(1) It is very complex already.
(2) It still needs to be localized.
Practically this means that I will have to spend quite some time with it
myself, to upgrade it to the current system infrastructure. I hope that
this is still feasible, so that this key component of Isabelle/HOL is not
stuck in the past -- due to a load of features that is too heavy to lift
This archive was generated by a fusion of
Pipermail (Mailman edition) and