[isabelle-dev] Future of permanent_interpretation

[Florian Haftmann]

(this continues the previous mail)

>>>> Certainly, your work has partly been inspired by the feeling that
>>>> the current locale commands only provide the bare basics for
>>>> manipulating locales.  For example, basing an interpretation or
>>>> sublocale declaration on definitions is certainly something that
>>>> could be done in a fancier manner.

According to my feelings, the whole locale machinery is an excellent and
powerful part of the systems.  The addition of mixin definitions as
special case of mixin rewrites do not touch the foundations (locale.ML /
expression.ML) at all – there is no restriction to achieve the same
result without them.  This implementation simplicity is the main reason
I dared to undertake this adventure.

> This is certainly useful, but it is not general enough for making it the preferred command.  For example, it doesn't permit function declarations.  

I don't think this generality is needed.  The idea behind mixin
definitions could be fomulated as »reinterpret this term as a new
definition«; the properties are already there afterwards, there is no
need for definitional extensions or construct them.

> The required definitions and proofs for an interpretation could for example be collected in a dedicated context in a step-by-step manner similar to that of class instantiation.

This could be thought of, but is another story.

> Your work also seems to be inspired by the desire to gradually rename 'sublocale' to 'interpretation', which I find surprising, because, compared to classes, 'sublocale' is the direct analogue of 'subclass' and 'interpretation' is the direct analogue of 'instantiation
> '.

You are right with the type class / locale analogy.  But type classes
only permit the algebraic view, they are too restricted for the »local
everything« approach.  As mentioned in my previous mail, I am happy to
leave both views stand in the long run, if we find a way to sort out the
(now still hypothetic) corner cases of epheremal interpretation on the
theory level and permanent interpretation in a nested context.

-- 

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