# HG changeset patch
# User wenzelm
# Date 1407679992 -7200
# Node ID 7cae177c9084afcbaf2cd1e7c6e61ca2c1c077f1
# Parent  0835aa55ba21291a86936f4f502c232862b9ce28
support for named collections of theorems in canonical order;

diff -r 0835aa55ba21 -r 7cae177c9084 etc/isar-keywords-ZF.el
--- a/etc/isar-keywords-ZF.el	Sun Aug 10 15:59:12 2014 +0200
+++ b/etc/isar-keywords-ZF.el	Sun Aug 10 16:13:12 2014 +0200
@@ -97,6 +97,7 @@
     "locale_deps"
     "method_setup"
     "moreover"
+    "named_theorems"
     "next"
     "no_notation"
     "no_syntax"
@@ -378,6 +379,7 @@
     "local_setup"
     "locale"
     "method_setup"
+    "named_theorems"
     "no_notation"
     "no_syntax"
     "no_translations"
diff -r 0835aa55ba21 -r 7cae177c9084 etc/isar-keywords.el
--- a/etc/isar-keywords.el	Sun Aug 10 15:59:12 2014 +0200
+++ b/etc/isar-keywords.el	Sun Aug 10 16:13:12 2014 +0200
@@ -139,6 +139,7 @@
     "locale_deps"
     "method_setup"
     "moreover"
+    "named_theorems"
     "next"
     "nitpick"
     "nitpick_params"
@@ -550,6 +551,7 @@
     "local_setup"
     "locale"
     "method_setup"
+    "named_theorems"
     "nitpick_params"
     "no_adhoc_overloading"
     "no_notation"
diff -r 0835aa55ba21 -r 7cae177c9084 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Sun Aug 10 15:59:12 2014 +0200
+++ b/src/Pure/Pure.thy	Sun Aug 10 16:13:12 2014 +0200
@@ -99,6 +99,7 @@
   and "realizability" :: thy_decl == ""
   and "extract_type" "extract" :: thy_decl
   and "find_theorems" "find_consts" :: diag
+  and "named_theorems" :: thy_decl
   and "ProofGeneral.process_pgip" "ProofGeneral.pr" "ProofGeneral.undo"
     "ProofGeneral.restart" "ProofGeneral.kill_proof" "ProofGeneral.inform_file_processed"
     "ProofGeneral.inform_file_retracted" :: control
@@ -115,6 +116,7 @@
 ML_file "Tools/find_consts.ML"
 ML_file "Tools/proof_general_pure.ML"
 ML_file "Tools/simplifier_trace.ML"
+ML_file "Tools/named_theorems.ML"
 
 
 section {* Basic attributes *}
diff -r 0835aa55ba21 -r 7cae177c9084 src/Pure/Tools/named_theorems.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/named_theorems.ML	Sun Aug 10 16:13:12 2014 +0200
@@ -0,0 +1,96 @@
+(*  Title:      Pure/Tools/named_theorems.ML
+    Author:     Makarius
+
+Named collections of theorems in canonical order.
+*)
+
+signature NAMED_THEOREMS =
+sig
+  val member: Proof.context -> string -> thm -> bool
+  val get: Proof.context -> string -> thm list
+  val add_thm: string -> thm -> Context.generic -> Context.generic
+  val del_thm: string -> thm -> Context.generic -> Context.generic
+  val add: string -> attribute
+  val del: string -> attribute
+  val declare: binding -> string -> theory -> string * theory
+end;
+
+structure Named_Theorems: NAMED_THEOREMS =
+struct
+
+(* context data *)
+
+structure Data = Generic_Data
+(
+  type T = thm Item_Net.T Symtab.table;
+  val empty: T = Symtab.empty;
+  val extend = I;
+  val merge = Symtab.join (K Item_Net.merge);
+);
+
+fun new_entry name =
+  Data.map (fn data =>
+    if Symtab.defined data name
+    then error ("Duplicate declaration of named theorems: " ^ quote name)
+    else Symtab.update (name, Thm.full_rules) data);
+
+fun the_entry context name =
+  (case Symtab.lookup (Data.get context) name of
+    NONE => error ("Undeclared named theorems " ^ quote name)
+  | SOME entry => entry);
+
+fun map_entry name f context =
+  (the_entry context name; Data.map (Symtab.map_entry name f) context);
+
+
+(* maintain content *)
+
+fun member ctxt = Item_Net.member o the_entry (Context.Proof ctxt);
+
+fun content context = rev o Item_Net.content o the_entry context;
+val get = content o Context.Proof;
+
+fun add_thm name = map_entry name o Item_Net.update;
+fun del_thm name = map_entry name o Item_Net.remove;
+
+val add = Thm.declaration_attribute o add_thm;
+val del = Thm.declaration_attribute o del_thm;
+
+
+(* declaration *)
+
+fun declare binding descr thy =
+  let
+    (* FIXME proper result from Global_Theory.add_thms_dynamic *)
+    val naming = Name_Space.naming_of (Context.Theory thy);
+    val name = Name_Space.full_name naming binding;
+
+    val thy' = thy
+      |> Global_Theory.add_thms_dynamic (binding, fn context => content context name);
+
+    val description =
+      "declaration of " ^ (if descr = "" then Binding.name_of binding ^ " rules" else descr);
+    val thy'' = thy'
+      |> Context.theory_map (new_entry name)
+      |> Attrib.setup binding (Attrib.add_del (add name) (del name)) description;
+  in (name, thy'') end;
+
+val _ =
+  Outer_Syntax.command @{command_spec "named_theorems"}
+    "declare named collection of theorems"
+    (Parse.binding -- Scan.optional Parse.text ""
+      >> (fn (binding, descr) => Toplevel.theory (snd o declare binding descr)));
+
+
+(* ML antiquotation *)
+
+val _ = Theory.setup
+  (ML_Antiquotation.inline @{binding named_theorems}
+    (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (xname, pos)) =>
+      let
+        val thy = Proof_Context.theory_of ctxt;
+        val name = Global_Theory.check_fact thy (xname, pos);
+        val _ = get ctxt name handle ERROR msg => cat_error msg (Position.here pos);
+      in ML_Syntax.print_string name end)));
+
+end;