[isabelle-dev] NEWS: bundled declarations

[Brian Huffman]

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