[isabelle-dev] Locale morphisms

Clemens Ballarin ballarin at in.tum.de
Fri Jan 7 15:12:46 CET 2022

Dear Isabelle Developers,

I'm working on an extension of the locale machinery by a means of 
declaring morphisms for use in locale expressions. Currently morphisms 
only appear within locale expressions. For example, in

   interpretation my_locale where A = t and B = s

the parameters A and B of 'my_locale' are mapped to t and s from the 
current context. The extension would introduce a new command 'morphism' 
for declaring morphisms and a new keyword 'under' for referring to these 
morphisms in expressions:

   morphism my_morphism where A = t and B = s

   interpretation my_locale under my_morphism

This will be helpful especially in applications where locales have more 
than just a handful of parameters.

I'm mainly writing to find out whether the new keywords 'morphism' and 
'under' would be considered appropriate in the current framework of 
Isabelle's outer syntax.


More information about the isabelle-dev mailing list