[isabelle-dev] Interpretation in arbitrary targets.

[Clemens Ballarin]

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
   ...
end

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''
end
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).

Clemens


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
>
>