[isabelle-dev] NEWS: bundled declarations
Brian Huffman
huffman at in.tum.de
Tue Apr 24 09:03:11 CEST 2012
On Sun, Apr 15, 2012 at 3:00 PM, Makarius <makarius at sketis.net> wrote:
> * Bundled declarations associate attributed fact expressions with a
> given name in the context. These may be later included in other
> contexts. This allows to manage context extensions casually, without
> the logical dependencies of locales and locale interpretation.
This seems like a really nice feature! I think it will be especially
useful in combination with local context blocks.
> The present implementation is rather modest, only for closed expressions of
> theorems with attributes. It can conceptually be extended to a full target
> on its own, e.g. to allow bundling of notation,
About the bundling of notation: It seems to me that the implementation
of bundling doesn't need to change at all; we just need a way to
register notation using attributes. I just had a go at a notation
attribute this morning, and here is what I came up with:
setup {*
let
val mode_spec : (string * bool) parser =
(Parse.$$$ "output" >> K ("", false)) ||
Parse.name -- Scan.optional (Parse.$$$ "output" >> K false) true;
val opt_mode =
Scan.optional (Parse.$$$ "(" |-- Parse.!!! (mode_spec --| Parse.$$$
")")) Syntax.mode_default
fun notation add ctxt : (Context.generic -> Context.generic) parser =
(opt_mode -- Parse.and_list1 ((Parse.const >>
Proof_Context.read_const ctxt false dummyT) -- Parse.mixfix)
>> (fn (mode, args) => Proof_Context.generic_notation add mode
args Morphism.identity))
fun attrib add : attribute context_parser =
Scan.depend (fn context => notation add (Context.proof_of context) >>
(pair context o Thm.declaration_attribute o K))
in
Attrib.setup @{binding notation_add} (attrib true) "notation as attribute"
#>
Attrib.setup @{binding notation_del} (attrib false) "notation as attribute"
end
*}
bundle quot_syntax =
[[notation_add fun_rel (infix "===>" 55)]]
[[notation_add map_fun (infix "--->" 55)]]
lemma
includes quot_syntax
shows "(op = ===> op =) id id"
unfolding fun_rel_def by simp
This seems to me like a much nicer way to use optional syntax than the
other workarounds we have now (e.g. importing
Library/{Quotient,Lattice}_Syntax.thy, which doesn't give you a way to
disable the syntax again, or cut-and-pasting a whole block of
notation/no_notation commands).
By the way, is there a way to add bundles to the context at top-level,
like a "declare" command that takes a bundle as an argument? It seems
that "include" doesn't work at top-level.
- Brian
More information about the isabelle-dev
mailing list