[isabelle-dev] Interpretation in arbitrary targets.

[Florian Haftmann]

Hi Clemens,

>>>> Let those thoughts sink further few days.  If there is no veto until
>>>> Apr
>>>> 7th, I would go ahead to turn the patches upstream.
> 
> You have proposed a change about which doubts were raised.  I don't
> consider it acceptable to then announce a deadline after which you will
> go ahead and push.  People simply may not be able to respond in time,
> especially in a vacation period.

This was by no means meant to put pressure on anybody or you in
particular.  For this sake I have asked for a »veto« which does not need
a justification at the same time.

> Let me note that, of
> course, the user interface design should not make the implementation
> unnecessarily complicated (but I believe we are far away from that).

Agree.

> In this light, if a version of the sublocale command seems necessary in
> context blocks, why no call it 'sublocale'?  Of course, the global
> version should remain
> 
>   sublocale l < e.
> 
> It should not be turned into
> 
>   sublocale (in l) e
> 
> because the former much more clearly indicates the change to the locale
> hierarchy.  This design has the additional benefits that users don't
> need to change existing proof documents, terminology in the literature
> remains up to date, and, most importantly, the sublocale command is
> clearly recognisable in context blocks.

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.

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.

Just to be clear again, I do not disregard your proposal in itself, but
it is not as general as the general subscription, with more or less the
same code basis behind.

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.

> This change was motivated by the realisation that interpretation between locales essentially means changing the module hierarchy.  This is a remarkable feature for a module system, which deserves emphasis and isn't really appropriately described by 'interpretation'

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.« ).

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