[isabelle] bundle commands inside a locale



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

 


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