# HG changeset patch
# User wenzelm
# Date 1332270013 -3600
# Node ID 12423b36fcc4d1912df41c916a97f49632ebd61c
# Parent  b32e6de4a39b1cddb1f6de774a9cecbd0a587da4
basic support for bundled declarations;

diff -r b32e6de4a39b -r 12423b36fcc4 etc/isar-keywords-ZF.el
--- a/etc/isar-keywords-ZF.el	Tue Mar 20 18:01:34 2012 +0100
+++ b/etc/isar-keywords-ZF.el	Tue Mar 20 20:00:13 2012 +0100
@@ -29,6 +29,7 @@
     "axiomatization"
     "axioms"
     "back"
+    "bundle"
     "by"
     "cannot_undo"
     "case"
@@ -76,6 +77,8 @@
     "hide_const"
     "hide_fact"
     "hide_type"
+    "include"
+    "including"
     "inductive"
     "inductive_cases"
     "init_toplevel"
@@ -120,6 +123,7 @@
     "print_ast_translation"
     "print_attributes"
     "print_binds"
+    "print_bundles"
     "print_cases"
     "print_claset"
     "print_classes"
@@ -287,6 +291,7 @@
     "print_antiquotations"
     "print_attributes"
     "print_binds"
+    "print_bundles"
     "print_cases"
     "print_claset"
     "print_classes"
@@ -342,6 +347,7 @@
     "attribute_setup"
     "axiomatization"
     "axioms"
+    "bundle"
     "class"
     "classes"
     "classrel"
@@ -458,6 +464,8 @@
 (defconst isar-keywords-proof-decl
   '("ML_prf"
     "also"
+    "include"
+    "including"
     "let"
     "moreover"
     "note"
diff -r b32e6de4a39b -r 12423b36fcc4 etc/isar-keywords.el
--- a/etc/isar-keywords.el	Tue Mar 20 18:01:34 2012 +0100
+++ b/etc/isar-keywords.el	Tue Mar 20 20:00:13 2012 +0100
@@ -35,6 +35,7 @@
     "boogie_open"
     "boogie_status"
     "boogie_vc"
+    "bundle"
     "by"
     "cannot_undo"
     "case"
@@ -108,6 +109,8 @@
     "hide_fact"
     "hide_type"
     "import_tptp"
+    "include"
+    "including"
     "inductive"
     "inductive_cases"
     "inductive_set"
@@ -162,6 +165,7 @@
     "print_ast_translation"
     "print_attributes"
     "print_binds"
+    "print_bundles"
     "print_cases"
     "print_claset"
     "print_classes"
@@ -372,6 +376,7 @@
     "print_antiquotations"
     "print_attributes"
     "print_binds"
+    "print_bundles"
     "print_cases"
     "print_claset"
     "print_classes"
@@ -446,6 +451,7 @@
     "axioms"
     "boogie_end"
     "boogie_open"
+    "bundle"
     "class"
     "classes"
     "classrel"
@@ -613,6 +619,8 @@
 (defconst isar-keywords-proof-decl
   '("ML_prf"
     "also"
+    "include"
+    "including"
     "let"
     "moreover"
     "note"
diff -r b32e6de4a39b -r 12423b36fcc4 src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Tue Mar 20 18:01:34 2012 +0100
+++ b/src/Pure/IsaMakefile	Tue Mar 20 20:00:13 2012 +0100
@@ -108,6 +108,7 @@
   Isar/args.ML						\
   Isar/attrib.ML					\
   Isar/auto_bind.ML					\
+  Isar/bundle.ML					\
   Isar/calculation.ML					\
   Isar/class.ML						\
   Isar/class_declaration.ML				\
diff -r b32e6de4a39b -r 12423b36fcc4 src/Pure/Isar/bundle.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Isar/bundle.ML	Tue Mar 20 20:00:13 2012 +0100
@@ -0,0 +1,115 @@
+(*  Title:      Pure/Isar/bundle.ML
+    Author:     Makarius
+
+Bundled declarations (notes etc.).
+*)
+
+signature BUNDLE =
+sig
+  type bundle = (thm list * Args.src list) list
+  val the_bundle: Proof.context -> string -> bundle
+  val check: Proof.context -> xstring * Position.T -> string
+  val bundle: binding * (thm list * Args.src list) list ->
+    (binding * typ option * mixfix) list -> local_theory -> local_theory
+  val bundle_cmd: binding * (Facts.ref * Args.src list) list ->
+    (binding * string option * mixfix) list -> local_theory -> local_theory
+  val include_: string -> Proof.state -> Proof.state
+  val include_cmd: xstring * Position.T -> Proof.state -> Proof.state
+  val including: string -> Proof.state -> Proof.state
+  val including_cmd: xstring * Position.T -> Proof.state -> Proof.state
+  val print_bundles: Proof.context -> unit
+end;
+
+structure Bundle: BUNDLE =
+struct
+
+(* maintain bundles *)
+
+type bundle = (thm list * Args.src list) list;
+
+fun transform_bundle phi : bundle -> bundle =
+  map (fn (fact, atts) => (Morphism.fact phi fact, map (Args.transform_values phi) atts));
+
+structure Data = Generic_Data
+(
+  type T = bundle Name_Space.table;
+  val empty : T = Name_Space.empty_table "bundle";
+  val extend = I;
+  val merge = Name_Space.merge_tables;
+);
+
+val get_bundles = Data.get o Context.Proof;
+
+fun the_bundle ctxt name =
+  (case Symtab.lookup (#2 (get_bundles ctxt)) name of
+    SOME bundle => bundle
+  | NONE => error ("Unknown bundle " ^ quote name));
+
+fun check ctxt = #1 o Name_Space.check (Context.Proof ctxt) (get_bundles ctxt);
+
+
+(* define bundle *)
+
+local
+
+fun gen_bundle prep_fact prep_att prep_vars (binding, raw_bundle) fixes lthy =
+  let
+    val (_, ctxt') = lthy |> prep_vars fixes |-> Proof_Context.add_fixes;
+    val bundle0 = raw_bundle
+      |> map (fn (fact, atts) => (prep_fact lthy fact, map (prep_att lthy) atts));
+    val bundle =
+      Attrib.partial_evaluation ctxt' [(Attrib.empty_binding, bundle0)] |> map snd |> flat
+      |> transform_bundle (Proof_Context.export_morphism ctxt' lthy);
+  in
+    lthy |> Local_Theory.declaration {syntax = false, pervasive = true}
+      (fn phi => fn context =>
+        context |> Data.map
+          (#2 o Name_Space.define context true
+            (Morphism.binding phi binding, transform_bundle phi bundle)))
+  end;
+
+in
+
+val bundle = gen_bundle (K I) (K I) Proof_Context.cert_vars;
+val bundle_cmd =
+  gen_bundle Proof_Context.get_fact (Attrib.intern_src o Proof_Context.theory_of)
+    Proof_Context.read_vars;
+
+end;
+
+
+(* include bundle *)
+
+fun gen_include prep raw_name =
+  Proof.map_context (fn ctxt =>
+    let
+      val bundle = the_bundle ctxt (prep ctxt raw_name);
+      val attrib = Attrib.attribute_i (Proof_Context.theory_of ctxt);
+      val note = ((Binding.empty, []), map (apsnd (map attrib)) bundle);
+    in #2 (Proof_Context.note_thmss "" [note] ctxt) end);
+
+fun include_ name = Proof.assert_forward #> gen_include (K I) name #> Proof.put_facts NONE;
+fun include_cmd name = Proof.assert_forward #> gen_include check name #> Proof.put_facts NONE;
+fun including name = Proof.assert_backward #> gen_include (K I) name;
+fun including_cmd name = Proof.assert_backward #> gen_include check name;
+
+
+(* print_bundles *)
+
+fun print_bundles ctxt =
+  let
+    val prt_thm = Pretty.backquote o Display.pretty_thm ctxt;
+
+    fun prt_fact (ths, []) = map prt_thm ths
+      | prt_fact (ths, atts) = Pretty.enclose "(" ")"
+          (Pretty.breaks (map prt_thm ths)) :: Attrib.pretty_attribs ctxt atts;
+
+    fun prt_bundle (name, bundle) =
+      Pretty.block (Pretty.command "bundle" :: Pretty.str " " :: Pretty.str name ::
+        Pretty.breaks (Pretty.str " =" :: maps prt_fact bundle));
+  in
+    map prt_bundle (Name_Space.extern_table ctxt (get_bundles ctxt))
+  end |> Pretty.chunks |> Pretty.writeln;
+
+end;
+
diff -r b32e6de4a39b -r 12423b36fcc4 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Tue Mar 20 18:01:34 2012 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Tue Mar 20 20:00:13 2012 +0100
@@ -414,6 +414,29 @@
       Toplevel.print o Toplevel.begin_local_theory true (Named_Target.context_cmd name)));
 
 
+(* bundled declarations *)
+
+val _ =
+  Outer_Syntax.local_theory ("bundle", Keyword.thy_decl) "define bundle of declarations"
+    ((Parse.binding --| Parse.$$$ "=") -- Parse_Spec.xthms1 -- Parse.for_fixes
+      >> (uncurry Bundle.bundle_cmd));
+
+val _ =
+  Outer_Syntax.command ("include", Keyword.prf_decl)
+    "include declarations from bundle in proof body"
+    (Parse.position Parse.xname >> (Toplevel.print oo (Toplevel.proof o Bundle.include_cmd)));
+
+val _ =
+  Outer_Syntax.command ("including", Keyword.prf_decl)
+    "include declarations from bundle in goal refinement"
+    (Parse.position Parse.xname >> (Toplevel.print oo (Toplevel.proof o Bundle.including_cmd)));
+
+val _ =
+  Outer_Syntax.improper_command ("print_bundles", Keyword.diag) "print bundles of declarations"
+    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
+      Toplevel.keep (Bundle.print_bundles o Toplevel.context_of)));
+
+
 (* locales *)
 
 val locale_val =
diff -r b32e6de4a39b -r 12423b36fcc4 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Tue Mar 20 18:01:34 2012 +0100
+++ b/src/Pure/ROOT.ML	Tue Mar 20 20:00:13 2012 +0100
@@ -224,6 +224,7 @@
 use "Isar/named_target.ML";
 use "Isar/expression.ML";
 use "Isar/class_declaration.ML";
+use "Isar/bundle.ML";
 
 use "simplifier.ML";