[isabelle-dev] Interpretation in arbitrary targets.

Clemens Ballarin ballarin at in.tum.de
Tue Mar 26 20:40:14 CET 2013

Hi Florian,

I'm in favour of generalising interpretation to targets, but in my  
opinion it would not be right to provide the sublocale command as the  
interpretation command in a locale context.  There are two reasons:

1. sublocale modifies the locale graph of the underlying theory.  This  
is a big change and shouldn't happen as a side effect of a command in  
a target context.

2. sublocale and interpretation are more different than it looks:  
interpretation provides inheritance of mixins (or, from the user  
perspective, rewrite morphisms) and it is possible to amend mixins in  
interpretation (currently only through the API).

On the other hand, I see that interpretation in a locale context can  
help working in an incremental fashion in such a context (which I  
assume is the motivation for your patches).

So, what should interpretation in a locale be like?  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

While sublocale is perfect for a), in b) there is a big overhead  
caused by importing all theorems from A into B whenever B is  
activated, while all that's needed is importing theorems from A to B  
once.  The latter is what we should try to address by a variant of the  
interpretation command for locale contexts.  Here's my proposal:

context B begin
   interpretation A

makes the interpretation of A available in the block up to the closing  
'end'.  The interpretation will not be persisted; results are only  
available temporarily to aid establishing some results in B.  Of  
course, this would mean that the literal command

interpretation (in B) A

is useless, but that wouldn't hurt.  On the other hand, if users  
started to use this feature, locale hierarchies could become less  
complex and, as a consequence, theories faster (well, become slower  
more slowly...).  When interpreting a hierarchy A - A' - A''  
incrementally, the pattern would be

context B begin
   interpretation A
   interpretation A'
   interpretation A''
sublocale B < A''

that is, one additional sublocale declaration would be sufficient to  
persist the incremental development.

What do you think of these ideas?  I would appreciate, if you could  
work towards them (I myself never quite mastered the intricacies of  
the ML level target code).


Quoting Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>:

> 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
> 	http://isabelle.in.tum.de/~haftmann/cgi-bin/repos/interpretation
> Explanations follow. It is good tradition not to muddle with the module
> system code arbitrarily, therefore this rather unconventional approach
> to gain feedback.
> 1.
> http://isabelle.in.tum.de/~haftmann/cgi-bin/repos/interpretation/rev/21821401c5a5
> 	Identity juggling to prepare following steps.
> 2.
> http://isabelle.in.tum.de/~haftmann/cgi-bin/repos/interpretation/rev/aee4c6577ff7
> 	Ironing out a FIXME in the code. This already gives a hint how the
> existing code base naturally converges to unify »interpretation« and
> »sublocale«.
> 3.
> http://isabelle.in.tum.de/~haftmann/cgi-bin/repos/interpretation/rev/f6bc704b5cd6
> 	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.
> 4.
> http://isabelle.in.tum.de/~haftmann/cgi-bin/repos/interpretation/rev/9d5c8a5251d5
> 	This establishes sharing of »interpretation« and »sublocale« as far as
> appropriate.
> 5.
> http://isabelle.in.tum.de/~haftmann/cgi-bin/repos/interpretation/rev/1d3a62ef74dd
> 	Identity juggling to prepare following steps.
> 6.
> http://isabelle.in.tum.de/~haftmann/cgi-bin/repos/interpretation/rev/dd6dd81381fb
> 	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.
> 7.
> http://isabelle.in.tum.de/~haftmann/cgi-bin/repos/interpretation/rev/f48553718a7a
> 	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.
> Cheers,
> 	Florian
> --
> PGP available:
> http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

More information about the isabelle-dev mailing list