[isabelle-dev] Future of permanent_interpretation

[Florian Haftmann]

For further discussion, see now fd4ac1530d63, particulary
src/Pure/Isar/interpretation.ML and 5.7.3 »Locale interpretation« in
*isar-ref*.

This goes along the following lines:

* »Interpretation« in general is used as generic heading for every kind
of intepretation into different destination contexts.
* *interpretation* in particular denotes interpretation into a confined
context. (The wording in the implementation is not yet consistent,
ranging from »epheremal« to »confined«; I have a slight inclination to
stick to the latter). *interpret* is the variant for proof blocks. This
use of terminology IMHO is consistent with typical uses in mathematics
and there had been little debate about that so far.

So far for the seemingly non-controversial matter.

Concerning the »persistent« / »permanent« / »subscribing« kinds of
interpretation, there are two conflicting views so far:

* Each local theory can »subscribe« to locales, given that it underlying
target implements it. Hence all targets (particularly, global theories
and locales) are treated uniformly, using one keyword
*permanent_interpretation.*
* The user interfaces emphasizes the non-trivial differences between
»subscription« into global theories and into locales, particularly the
side effects of the latter on the existing locale hierarchy.

Personally I have no strong inclination to follow the one or the other
and I am happy to abandon the first in favour for the second. However
then I also suggest a dedicated keyword for interpretation into global
theories:
a) *interpretation* would otherwise be strangely overloaded, allowing
mixin definitions on the level of global theories but not in other local
theories.
b) Conceptually it would also be possible to allow »subscribing«
interpretation into global theories inside a nested local theory
(although it is not clear whether our current implementation is actually
suitable for that). Then *theory* … *context* … *begin … interpretation*
would be ambiguous.
c) Similarly, also a theory itself can be seen as a confined context
block, making *theory* … *interpretation* itself ambiguous.
Suitable candidates could be *theory_interpretation *or
*global_interpreation*. Better suggestions welcome. Of course, the
actual replacement would not occur in the upcoming but a later release.

On that single matter I want to excite some feedback before continuing.
Also suggestions on 5.7.3 »Locale interpretation« in *isar-ref* are welcome.

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: 198 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20151115/827816c3/attachment.sig>