[isabelle-dev] NEWS: avoid the Complex constructor, use the more natural

[Jasmin Christian Blanchette]

Am 13.05.2014 um 14:11 schrieb Manuel Eberl <eberlm at in.tum.de>:

> In particular, any algebraic datatype with only one constructor can be rewritten into a corresponding codatatype, allowing you to use primcorec for it.

In fact, even (nonrecursive) datatypes with several constructors can be rewritten into a codatatype -- it's just that the syntax gets a bit heavier, with the discriminator formulas in addition to the selector equations.

In fact, it should not be difficult to extend "primcorec" so that it can define nonrecursive functions on nonrecursive datatypes, and probably nonrecursive functions on recursive datatypes as well. This might in many cases be preferable to redefining the type as a codatatype, breaking any applications that rely on the (degenerate) induction rule or recursor.

Ideally, one could imagine that destructor-style specifications could be handled with "fun" -- but I doubt this is likely to happen anytime soon. In contrast, the above modification to "primcorec" would be relatively easy -- all we need to do is to derive a noncorecursive corecursor from a freely generated type (e.g., a datatype), a fairly simple undertaking.

Jasmin