[isabelle-dev] Specification packages in Isabelle/HOL, particularly primrec

[Florian Haftmann]

Hi all,

after 3bfa28b3a5b2  (followed-up by AFP  d058960a13d6) the matter of
affairs with specification packages is as as follows:

The prototypical specification interface is of shape

  val add_specification: spec -> local_theory -> result * local_theory

where »spec« is the input specification and »result« a characterization
of the definitional extension with enough information to build on it in
derived tools.

The corresponding package is supposed to provide a morphism lifter for
results

  val transform: morphism -> result -> result

The local theory stemming from add_specification may still contain
hypothetical results of the specification construction (I left this
untouched contrary to an idea I have expressed earlier on this
mailinglist); to get a proper close-up, there is a set of combinators:

* Local_Theory.subtarget_result for regular nested local theory;
* Named_Target.theory_map_result for global specifications;
* Overloading.theory_map_result for global overloaded specifications;
* Class.theory_map_result for global overloaded specifications relating
to type class instantiation.

Hence various *_global variants for specification packages have been
removed.

What I have left untouched are the various variants of primrec. Is there
still an ongoing work or plan to get rid of the old datatype / primrec
layer, or at least to have that retreat further? Otherwise I would have
a closer look a it to get an idea what can be done there.

Cheers,
	Florian

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 228 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20190221/80ed7532/attachment.asc>