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.