[isabelle-dev] Locale morphisms

[Tobias Nipkow]

On 07/01/2022 15:12, Clemens Ballarin wrote:
> 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

I wonder if "with" could be reused instead?

Tobias

> 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.
> 
> Clemens
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5535 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20220107/cd367fa8/attachment.bin>