[isabelle-dev] Interpretation in arbitrary targets.

[Clemens Ballarin]

Hi Florian,

> I do not object to your suggestion, and it is clearly in reach within
> the current code base.  But... it is a different thing.  Your suggestion
> is to make sublocale work in locale targets seamlessly.  But something like
>
> instantiation ...
> begin
>
> sublocale ...
>
> instance ...
>
> end
>
> then just does not make sense: either it is not covered (or blocked) by
> the implementation, or »sublocale« is just the wrong wording since it
> assumes locales on both producer and consumer side so to speak.

I don't know what interpretation (or sublocale) would mean in an  
instantiation context, so I cannot tell what would be more  
appropriate.  It seems natural though, that, if additional commands  
are to be 'targetized', some commands will not be meaningful in some  
kinds of targets.  So, if sublocale were only available in locale  
targets, I wouldn't consider that a problem.  (If sublocale
were not available in locale targets, I wouldn't consider that a  
problem either, but that's not the the point of this discussion.)

In any case, it would make sense to discuss what a command would mean  
in all of the targets (and where it is not meaningful) before making  
it available in some targets.

> You might ask at first what interpretation in instantiation blocks is
> supposed to be.  I think it can be a neat pattern to approach
> instantiation by default definitions; here the interpretation would
> provide that OFCLASS theorem to prove the claimed instance relationship
> finally or something alike.

I'm unsure whether I understand this fully.  But to me it looks like  
the purpose of the instantiation target is to declare instance  
relations between classes.  If that is the case, then there is no  
further need to stress the 'subscriptive' nature and it might be  
legitimate to just call the command 'interpretation'.  But, of course,  
it depends on what the command would actually do.  I guess this would  
replace some existing command that already exists.

This is different if the target is a locale.  The purpose of a locale  
target is to work in a locale, not add relations between locales.  We  
don't have a sublocale target, whose purpose could be to establish  
interpretation relations between locales.  Instead there is just the  
sublocale command, which is fairly primitive.  The mechanisms offered  
by the instantiation target, which lets one make the necessary  
constructions needed for the instantiation in a clean way, are much  
more elaborate.

> Two asides:
>
>> Of course, the global
>>> version should remain
>>>
>>>   sublocale l < e.
>>>
>>> It should not be turned into
>>>
>>>   sublocale (in l) e
>
> foo (in l) ...
>
> is equivalent to
>
> context l
> begin
>
> foo ...
>
> end
>
> by construction.  We cannot have just one of them.

That sounds a bit dogmatic.  If additional commands are made available  
for targets, then the syntax should clearly be more flexible if better  
intuition can be achieved.

> It is also notable that we have definitions in locales (although this is
> far beneath your great achievements with sublocale etc.).  With them it
> is the case that we provide them *uniformly* for theories, locales and
> other targets (something which has been commented as seemingly trivial,
> »but maybe this is the achievement.« ).

I strongly believe that definitions in locales are a great  
achievement.  Without them all the other work would not have been  
worth it.  I hope, though, it has become clear that I'm not opposed to  
having interpretation in locale contexts by principle, I'm merely  
opposed to explaining them in the way you propose.

Clemens