Re: [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.  


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.