Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] bundle commands inside a locale

Email Gateway (Aug 22 2022 at 19:28):

From: anonymous user <anonymous-for-isabelle-ml@outlook.com>
Hi,

I am trying to find a way to encapsulate all the notations that are defined inside a locale into a separate bundle. For a locale called "Foo", this would allow me to toggle the notation whenever I unfold "Foo" using the "interpretaion" or "sublocale" command inside another locale called "Bar".

locale Foo =

fixes A :: "'a => bool"

assumes "P A"

begin

## (let's say I define some notation here)

definition

t :: "'a => bool" ("TTT _" [50])

where

"t == A"

lemma "TTT x ⟹ A x" unfolding t_def .

## end

## locale Bar =

fixes B :: "'a => bool"

assumes a1:"P B" and "Q B"

begin

## interpretation Foo B using a1 .

## (*the syntax is lost here. TTT not recognized anymore...

lemma "TTT x ⟹ B x"*)

## (* assuming that I could create a bundle inside Foo locale,

how can I include the Foo_syntax bundle here? ...*)

## end

Note that I am aware of the possibility to define bundle blocks that include some notation commands like bellow. However, this is only applicable for those terms which are not defined inside a locale.

definition "t == True"

## bundle Foo_syntax

begin

notation t ("TTT" [50])

end

What I am looking for is a way to wrap "notation" command inside an inline "bundle" inside a locale as follows:

context Foo

begin

## bundle Foo_syntax = {

notation t ("TTT" [50]),

(or any other command here...)

}

## end

Thanks in advance for your help. :)
-- an Isabelle user

Email Gateway (Aug 22 2022 at 19:29):

From: mailing-list anonymous <mailing.list.anonymous@gmail.com>
Dear Anonymous,

I am far from being an expert on notation/bundles. Therefore, hopefully,
someone else will provide a better reply. However, given your examples, I
do not understand why would it not be suitable to merely provide the
notation explicitly inside the locale Foo using the command notation?
For example,

locale Foo =
fixes A :: "'a => bool"
assumes "P A"
begin
definition t :: "'a ⇒ bool" ("TTT _" [50]) where "t == A"
notation t ("TTT _" [50])
lemma "TTT x ⟹ A x" unfolding t_def .
end

locale Bar =
fixes B :: "'a ⇒ bool"
assumes a1:"P B" and "Q B"
begin
interpretation Foo B using a1 .
lemma "TTT x ⟹ B x" by (simp add: t_def) (the notation is now available)
end

Alternatively, in my own work, usually, for each locale, I provide another
locale with the notation specified explicitly (I adopted this method from
an answer to one of my own old and rather naive questions that was provided
by Akihisa Yamada:
https://stackoverflow.com/questions/50085849/importing-classes-into-a-locale-in-isabelle-and-other-related-questions).
This allows me to switch between different notations if necessary. However,
this method does incur a certain amount of boilerplate code. Quite frankly,
I would also be interested to know if there is a more standard approach
that would allow for switching between different sets of notation with
ease.

Thank you

Email Gateway (Aug 22 2022 at 19:29):

From: anonymous user <anonymous-for-isabelle-ml@outlook.com>
Dear Anonymous@gmail,

Using the notation command explicitly inside a locale is quite convenient, however, it is cumbersome to use when notations are reused. For an example, consider the following graph locales:

locale graph

begin

definition "path u es v ≡ True"

notation path ("_ --_--> _" [50, 50, 50] 90)

end

locale graph_special =

fixes P :: "'a => 'b => bool"

begin

interpretation graph .

definition "spath u es v ≡ path u es v & P u v"

notation spath ("_ --_--> _" [50, 50, 50] 90)

(* Now, both "spath" and "path" have the same notation.

Preferably, the "path" notation should have been

shadowed by the new "spath" notation.... *)

end

The second option that you have mentioned is very close to the solution that I am looking for. Thanks for referring me to it.

Kind regards,
-- anonymous Isabelle user with an @outlook address

Last updated: Apr 30 2024 at 12:28 UTC