[isabelle-dev] Interpretation in arbitrary targets.
ballarin at in.tum.de
Fri Apr 12 21:03:58 CEST 2013
> 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 ...
> sublocale ...
> instance ...
> 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
> 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
> foo ...
> 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.
More information about the isabelle-dev