[isabelle-dev] Afterthoughts on Local_Theory.subtarget_result

[Florian Haftmann]

Hi all,

as of 82f57315cade (followed-up by AFP bf62184), the still occasionally
seen Local_Theory.reset invocations are gone, conveniently replaced by
Local_Theory.subtarget_result.

I'm considering pushing that even further: specification tools should by
contract provide a »clean« definitional extension without any artefacts
of the internal construction leaking out, i. e.

  val 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 resulting local_theory can be continued on directly
-- all internal construction steps are hid in a local subtarget.

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

  val transform: morphism -> result -> result

hence exporting up through nested context is trivial.

This would also open up the possibility to get rid of the still seen
*_global variants for specification tools: using a combinator

  Named_Target.theory_map_result: (morphism -> 'a -> 'a) ->
(local_theory -> 'a * local_theory) -> theory -> 'a * theory

any Package.spec_global can be trivially inlined as

  Named_Target.theory_map_result Package.transform (Package.spec …)

So much my current understanding of affairs.

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/20190122/a86ae71d/attachment.asc>