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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
