[isabelle-dev] Interpretation in arbitrary targets.

[Makarius]

On Tue, 26 Mar 2013, Florian Haftmann wrote:

> Clemens Ballarin wrote:
>> Currently, sublocale is used for two purposes:
>>
>> a) relating two locales to each other (such as "a total order is a
>> lattice")
>>
>> b) import (a typically small number of) lemmas, which are needed for
>> establishing some result, from one locale A into another locale B

> Currently, there is check that »interpretation« may only be issued at 
> the bottom level of the local theory stack, outside any free-floating 
> context.  Although I have no constructive proof at hand yet, I believe 
> that by lifting the check appropriately we get b) for free: similar to 
> »interpret«, this would only yield facts inside the context (whose 
> bindings disappear after »end«) without any additional dependencies or 
> registrations.  This is also why I adhered to »interpretation« in the 
> end.

> So, your example could somehow look like
>
> context B begin
>  context
>  begin
>    interpretation A
>  end
>  context
>  begin
>    interpretation A'
>  end
>  context
>  begin
>    interpretation A''
>  end
>  interpretation A'' -- {* permanent subscription *}
> end

Note that we have one more aspect in the back-end that could help here: 
the 'private' modifier.  Its meaning was not fully defined so far, but it 
could do the job:

   context B
   begin

   private interpretation A ...
   private interpretation A' ...
   private interpretation A'' ...

   interpretation A'' ...

   end

Until I manage to get 'private' as command modifier into the toplevel 
interpreter, we can tentatively use 'private_interpretation'.

Note that there might be still certain "foundations" that have to be 
pushed through to the background theory, despite the privateness.  For 
example "private definition ..." has to introduce a global const, but the 
name space entries can differ. (We can think about this side-branch harder 
about this when we are standing there.)

For interpretation, the foundation aspect are the details about 
subscription and the registration that is left behind in the context(s).


> You might still argue about syntax, e.g. having separate commands
>  subscription – what is currently interpretation and subscription, not
> in free-floating contexts (as implemented in the patches).
>  interpretation – only in confined contexts (locales, context begin …
> end, but not global theories any longer) without any subscription.

That paragraph is very difficult to understand.


> Overall I am amazed how well this all would fit to the existing local 
> theories.

I agree with that formal observation.  The changeset line is carefully 
constructed as a "proof" on the history, where each step can be followed 
in isolation.  The main thing is 
http://isabelle.in.tum.de/~haftmann/cgi-bin/repos/interpretation/rev/dd6dd81381fb 
"subscription as dedicated target concept", when the result suddenly pops 
out almost for free.  (Apart from small snags concerning context reinit.)


 	Makarius