[isabelle-dev] Locale morphisms
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