*To*: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>, mailing-list anonymous <mailing.list.anonymous at gmail.com>*Subject*: Re: [isabelle] bundle commands inside a locale*From*: anonymous user <anonymous-for-isabelle-ml at outlook.com>*Date*: Wed, 24 Apr 2019 08:22:05 +0000*Accept-language*: en-US*In-reply-to*: <CALaF1UKM7vy9puVLwqHL3rHqZ-eq5CKnV+=2U+iKNjtBoWKHog@mail.gmail.com>*References*: <CALaF1UKM7vy9puVLwqHL3rHqZ-eq5CKnV+=2U+iKNjtBoWKHog@mail.gmail.com>*Thread-index*: AQHU+eVI8FZtvw/xgkqlIyJFeWse/qZK7r1P*Thread-topic*: [isabelle] bundle commands inside a locale

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 -------------------------------------------------------------------------------- -------------------------------------------------------------------------------- -------------------------------------------------------------------------------- From: mailing-list anonymous <mailing.list.anonymous at gmail.com> Sent: Tuesday, April 23, 2019 5:00 PM To: cl-isabelle-users at lists.cam.ac.uk Cc: anonymous-for-isabelle-ml at outlook.com Subject: Re: [isabelle] bundle commands inside a locale 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 -- Please accept my apologies for posting anonymously. This is done to protect my privacy. I can make my identity and my real contact details available upon request in private communication under the condition that they are not to be mentioned on the mailing list.

**References**:**Re: [isabelle] bundle commands inside a locale***From:*mailing-list anonymous

- Previous by Date: [isabelle] PxTP 2019 - Second Call for Papers
- Next by Date: [isabelle] CakeML Developers Meeting 13-14 May 2019
- Previous by Thread: Re: [isabelle] bundle commands inside a locale
- Next by Thread: [isabelle] FroCoS 2019 (London): DEADLINE EXTENSION and final call for papers
- Cl-isabelle-users April 2019 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list