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_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
