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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
