Stream: Mirror: Isabelle Development Mailing List

Topic: [isabelle-dev] Locale morphisms


view this post on Zulip Email Gateway (Jan 07 2022 at 14:37):

From: Tobias Nipkow <nipkow@in.tum.de>
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@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
smime.p7s


Last updated: Mar 04 2024 at 12:30 UTC