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 it again.


	Makarius





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