[isabelle-dev] Future of permanent_interpretation

[Clemens Ballarin]

Hi Florian,

thanks for your feedback.  Local theories have done Isabelle and its users a great service in presenting a uniform view of different kinds of declarations in several contexts, and the locales reimplementation would have been much more painful without them.  However, if "local everything" forces us to name commands in the proof language after features that I would consider secondary (permanent vs. ephemeral interpretation) rather than primary (simple interpretation vs. interpretation that changes the locale hierarchy) then we need to check whether we are pushing this idea too far.

Clemens


On 29 October, 2015 11:41 CET, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de> wrote: 
 
> (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
>