Hi Alex, (Briefly reviving an old thread...)
Am 06.08.2013 um 00:36 schrieb Alexander Krauss <[email protected]>: > In summary, except for the size functions which are somewhat special > (and only used for termination proofs), the function package never uses > any inductiveness and would happily swallow codatatypes as well. > > Thus, I would propose to model the concept of a "type made of > constructors" explicitly as a declaration which other tools can look up > and add further interpretations to (in the sense of datatype > interpretations). The function package would only depend on that. If I > understand correctly, that declaration would essentially be rep_datatype > without the induction rule. The function package (and I assume other > tools, such as case syntax generation) can only rely on that and thus > treat datatypes and codadatypes uniformly. > > But, according to your schedule, these considerations become important > only after the coming release, so I'll shut up for the moment. The repository version of Isabelle (e95831757903) now has such a concept as part of the "HOL" image. It is called "Ctr_Sugar" [*]. Datatypes defined using "datatype" or "datatype_new", and codatatypes defined using "codatatype", are registered there; and using the ML interface, users can extend the database. Users can also use the command "wrap_free_constructors" to derive case constants (+ syntax), discriminators, selectors, and a wealth of properties about them. I have also ported some of the existing code, including the function package (except "size" and "fundef_cong"), to use the new interface. Jasmin [*] Name suggestions welcome. _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
