[isabelle-dev] Locale interpretation with mixins

[Florian Haftmann]

Hi Clemens, hi Makarius,

let me resume this running thread (not necessarily gag).

Let me quote two emails by Clemens on this issue:

> What is called mixin in the implementation is a transfer principle that is applied in addition to the interpretation morphism.  Currently users can only give equations, which yield rewrite morphisms, and consequently, the term 'mixin' appears nowhere in the documentation.  On the other hand, the locale core 'knows' nothing about the equations.  For it, their are just general transfer principles.

> This decision shouldn't prevent providing commands that solve important special cases, like exporting all constants and then interpreting onto them.  This seems to be an important use case for code generation.  In fact, in my terminology, this operation would compute a locale instance, not an interpretation (in analogy to type classes).

In the light of these statements, my current view on this issue is as
follows:

a) There is the mechanism for locale interpretation, which permits
arbitrary mixin morphisms
b) There is the interpretation command, which exposes the mixin
interface by taking equations as arguments.

My argument is (and that's what's prototyped in
Tools/interpretation_with_defs.ML) that there are alternatives for the
user interface b).
The current interface allows

c) to map derived defs in a locale under interpretation to »existing terms«

The proposal is to extend this to allow also

d) mixins to map derived defs in a locale under interpretation to newly
introduced defs

This is the base line we would have to agree upon if
Tools/interpretation_with_defs.ML should be (re-)integrated into the
regular locale/interpretation corpus.  An alternative would be a
distinct command, but I am not that happy with this:
* It would revive the ancient interpret / invoke duality on a different
level.
* Could duplication would remain, or a couple of not-so-abstract
interfaces would need to be exported from expression.ML

A less crucial manner is syntax (for convenience, I will continue on
this in a separate email)

Cheers,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

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