[isabelle-dev] Locale interpretation with mixins

[Makarius]

On Sun, 22 Jul 2012, Florian Haftmann wrote:

> Hi Clemens, hi Makarius,
>
> let me resume this running thread (not necessarily gag).
>
> Let me quote two emails by Clemens on this issue:
>
> 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.

After studying the sources a few times this year and reading again various 
documents by Clemens, I think I understand at last a bit how it works, 
which does not mean it would be easy nor easy to change.


> 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

In December 2011 we were both staring at interpretation_with_defs.ML and 
could not fully see the principle how it would work for complex hiearchies 
of locales and interpretations.  I.e. it is EXPERIMENTAL with the 
capitalization that you've put there in Jan 2011 (c34415351b6d).

Are there any new insights about it in the meantime?


Just a general question: Why does the code generator require a closed 
constant as a starting point?  Couldn't it just take an arbitrary term, 
with some decoration how it should be abstracted into a closed thing?


 	Makarius