[isabelle-dev] NEWS: Locale rewrite morphism moved into expressions

Clemens Ballarin ballarin at in.tum.de
Mon Mar 5 21:16:24 CET 2018

In addition to Makarius' recent performance improvements, there is a 
modest reform to the way rewrite morphism are integrated with locales.  
Previously they were added as an after-thought to the interpretation 
commands.  Now they are integrated with locale expressions.

The main advantage is that situations where locale expressions lead to 
duplicate constant declaration errors can now better be avoided.  In 
principle, rewrite morphisms could also be allowed in locale 
declarations.  This would imply a proof block after every locale 
declaration, so I haven't done so.

These are the relevant NEWS entries:

* Rewrites clauses (keyword 'rewrites') were moved into the locale
expression syntax, where they are part of locale instances.  In
interpretation commands rewrites clauses now need to occur before
'for' and 'defines'.  Minor INCOMPATIBILITY.

* For rewrites clauses, if activating a locale instance fails, fall
back to reading the clause first.  This helps avoid qualification of
locale instances where the qualifier's sole purpose is avoiding
duplicate constant declarations.

These are the relevant changesets in Isabelle and the AFP:

   Proper rewrite morphisms in locale instances.
   Fall back to reading rewrite morphism first if activation fails 
without it.
   Drop rewrites after defines in interpretations.

   Rewrites clauses are now part of locale expressions.
   Pull rewrites clause in front of defines.

Some internal cleanup is still to come.


More information about the isabelle-dev mailing list