[isabelle-dev] Changes to the locale syntax

[Clemens Ballarin]

I'm planning two moderate changes to the locale syntax:

* The default of qualifiers in locale expressions will change from optional 
("?") to mandatory ("!") in the context of "locale" and "sublocale".  This 
brings these commands in line with "interpretation" and "interpret".  In larger 
developments it is apparent that this is the better default.

* As already mentioned in my previous message, I plan to change the keyword for 
rewrite morphisms from "where" to "rewrites".  This is to better distinguish 
these from named instantiations in locale expressions.  The syntax will then be

  sublocale A < B where y = x for x rewrites "z = w"

rather than

  sublocale A < B where y = x for x where "z = w"

Clemens

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Future of permanent_interpretation

[Clemens Ballarin]

On 26 October, 2015 10:38 CET, Tobias Nipkow  wrote: 
 
> My desire to generate code from locale interpretations w/o having to make a 
> number of trivial function definitions was what started this whole business a 
> number of years back. Florian's very useful implementation of that really 
> needs 
> to make it into Main.

It could simply be integrated with the current interpretation and sublocale 
commands, where the definitions could be supplied in a separate clause, as 
suggested by Florian, perhaps using "defines" as keyword.  Would this suit your 
needs?

(Independently I intend to change the keyword for the rewrite morphisms clause 
of these commands from "where" to "rewrites", to better distinguish it from 
named instantiations in locale expressions.)

> My understanding of "sublocale" is that it is an interpretation within a 
> locale 
> and I have used that explanation in papers because I find it very succinct. 
> Thus 
> I would welcome if the same keyword is used.

This view is of course valid, but it isn't the whole story.  With "sublocale" 
these interpretations are orchestrated in a manner such that the locale 
hierarchy is effectively changed.  Now I can see that there might be domains 
where this more abstract view is not relevant, but when working with a 
hierarchy of locales representing algebraic structures it is certainly 
appropriate.  It should also be kept in mind that "sublocale" is established in 
the locale documentation including my JAR paper [1].  If the desire for a 
different keyword is so strong, perhaps an alias might be a solution.

Clemens

[1] Clemens Ballarin. Locales: a module system for mathematical theories. 
Journal of Automated Reasoning, 52(2):123–153, 2014.


> On 25/10/2015 11:16, Clemens Ballarin wrote:
> > Hi Florian,
> >
> > this proposal goes too far, of perhaps, not far enough.  Let me explain.
> >
> > There is of course nothing wrong with providing new commands and 
> > enhancements for frequent use cases.  However, I don't see a good reason 
> > why users should be forced to write 'permanent_interpretation' where they 
> > could write 'interpretation' or 'sublocale'.
> >
> > I don't object to a careful evolution of the user interface to locales, but 
> > I don't think you're heading in the right direction.  Your 
> > 'permanent_interpretation' lets users make some definitions followed by, 
> > depending on the context, an interpretation or a sublocale declaration.  
> > This is certainly useful, but it is not general enough for making it the 
> > preferred command.  For example, it doesn't permit function declarations.  
> > It also blurs the distinction between 'interpretation' and 'sublocale' by 
> > calling the latter 'permanent_interpretation' when in a locale context, but 
> > not at the level of theories, but instead calling the former 
> > 'permanent_interpretation' at the level of theories.
> >
> > It should be kept in mind that in the current design the 'interpretation' 
> > commands are effective for the lifetime of their context: in theories they 
> > are therefore permanent, in context blocks they persist for that block and 
> > within a proof 'interpret' provides services for that proof.  This is 
> > pretty straightforward.  On the other hand, 'locale' and 'sublocale' are 
> > theory-level commands that relate a locale to a locale expression (which in 
> > both cases becomes a sublocale of the locale).  Their only difference is 
> > that 'locale' declares a new locale while 'sublocale' refers to an existing 
> > one.  We have allowed the use of 'sublocale' in locale contexts as a 
> > notational convenience, but I don't consider it a good idea to further blur 
> > the distinction between 'interpretation' and 'sublocale'.  Calling 
> > 'sublocale' 'permanent_interpretation' in some contexts and 'sublocale' in 
> > others is certainly bad.  The current design is, of course, not cast in 
> > stone, but for changing it, there has to be a 
> consistent vision first, so we know where we are heading.
> >
> > 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.  
> > The situation is perhaps a bit similar to that of 'axclass' several years 
> > ago, where your work on type classes has improved the user experience 
> > dramatically.  If you would like to bring locales forward, you might 
> > consider developing ideas along those lines.  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.  
> > Your work also seems to be inspired by the desire to gradually rename 
> > 'sublocale' to 'interpretation', which I find surprising, because, compared 
> > to