[isabelle-dev] Interpretation in arbitrary targets.

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Sun Mar 24 20:51:45 CET 2013

There is a series of minimal invasive patches to generalize
»interpretation« / »sublocale« to »interpretation« in arbitrary targets,
not just theories and locales. The patches are inspectible at


Explanations follow. It is good tradition not to muddle with the module
system code arbitrarily, therefore this rather unconventional approach
to gain feedback.

	Identity juggling to prepare following steps.


	Ironing out a FIXME in the code. This already gives a hint how the
existing code base naturally converges to unify »interpretation« and


	In order to let »interpretation« and »sublocale« converge, the close
marriage of »interpretation« and »interpret« must be given up. This is a
step back only in the first instance – it would still be possible to
factor out common code of the resulting unified »interpretation« and
»interpret« in a separate step afterwards. In the same breath the
(operationally void!) switch from »ctxt« to »lthy« yields the key clue
of the whole story.


	This establishes sharing of »interpretation« and »sublocale« as far as


	Identity juggling to prepare following steps.


	This is the key step: »subscription« as target operation to make
»interpretation« work regardless of the underlying target.
	The »potential_reinit« is a wart: when interpreting locales into
locales, the new facts must be provided in the local theory context of
this locale also, and I have up after a few experiments with
Locale.activate_facts etc. Note the same situation has been occuring in
»subclass« for years now. Here it is more critical since interpretation
should be fully target-ignorant (unlike subclass which always knows that
it operates on classes). However I have let it stand for the moment as a
conceptual preview. I'm thankful for any hints how to resolve this.
	In this change the clone in src/Tools/ has been changed accordingly –
its future is still not so clear yet.


	Some examples. Note that I have experienced that »interpretation« does
sometimes not work inside »instantiation« (something in connection with
abbreviations), but this indicates a weakness of the instantiation
target rather than a conceptual mistake in interpretation. This needs to
be amended separately.

The next steps after those would be something like
* Amend the wart mentioned in (6).
* Add documentation.
* One round trip over the whole sources to avoid references to (then
legacy) »sublocale«.
* Amend the instantiation target not to choke on abbreviations stemming
from interpretations.
* Examine whether this code basis already allows to have confined
interpretations inside context … begin … end blocks.

I'm looking forward to responses.



PGP available:

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 261 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20130324/e07b1393/attachment.asc>

More information about the isabelle-dev mailing list