[isabelle-dev] New (Co)datatypes: Status & Plan (FYI)

[Andreas Schropp]

On 08/04/2013 07:09 PM, Florian Haftmann wrote:
> To add a further dimension to the design space, there was once the idea
> of a generalized primrec in the manner:
>
> 1. recursive specification following some pattern considered »primitive«
> 2. foundational definition of this specification using a suitable
> recursion combinator
> 3. maybe some proof by the user that certain conditions a satisfied
> 4. deriving the original specification again
>
> A new command »primitive_recursion« would then expose (3) to the user,
> whereas the existing »primrec« would assume a trivial proof instead
> (similar in appearance like the pair »function« and »fun«)

That sounds like a derivation of a primitive recursion specification over
an ad-hoc nonfree datatype that specifies the "primitive pattern".

Andrei and I submitted a paper on nonfree datatypes to CPP 2013:
     http://home.in.tum.de/~schropp/nonfree-data.pdf
(see appendix for recursors on finite sets)

Integration with the new datatype package is possible
by registering the nonfree datatypes as BNFs.

Cheers,
   Andy