[isabelle-dev] Interpretation in arbitrary targets.

Makarius makarius at sketis.net
Wed Mar 27 11:01:09 CET 2013

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

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

   interpretation A'' ...


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 
"subscription as dedicated target concept", when the result suddenly pops 
out almost for free.  (Apart from small snags concerning context reinit.)


More information about the isabelle-dev mailing list