src/Pure/Tools/named_theorems.ML
author wenzelm
Sun Aug 10 19:53:30 2014 +0200 (2014-08-10)
changeset 57888 9c193dcc8ec8
parent 57886 7cae177c9084
child 57927 f14c1248d064
permissions -rw-r--r--
some localization;
wenzelm@57886
     1
(*  Title:      Pure/Tools/named_theorems.ML
wenzelm@57886
     2
    Author:     Makarius
wenzelm@57886
     3
wenzelm@57886
     4
Named collections of theorems in canonical order.
wenzelm@57886
     5
*)
wenzelm@57886
     6
wenzelm@57886
     7
signature NAMED_THEOREMS =
wenzelm@57886
     8
sig
wenzelm@57886
     9
  val member: Proof.context -> string -> thm -> bool
wenzelm@57886
    10
  val get: Proof.context -> string -> thm list
wenzelm@57886
    11
  val add_thm: string -> thm -> Context.generic -> Context.generic
wenzelm@57886
    12
  val del_thm: string -> thm -> Context.generic -> Context.generic
wenzelm@57886
    13
  val add: string -> attribute
wenzelm@57886
    14
  val del: string -> attribute
wenzelm@57888
    15
  val declare: binding -> string -> local_theory -> string * local_theory
wenzelm@57886
    16
end;
wenzelm@57886
    17
wenzelm@57886
    18
structure Named_Theorems: NAMED_THEOREMS =
wenzelm@57886
    19
struct
wenzelm@57886
    20
wenzelm@57886
    21
(* context data *)
wenzelm@57886
    22
wenzelm@57886
    23
structure Data = Generic_Data
wenzelm@57886
    24
(
wenzelm@57886
    25
  type T = thm Item_Net.T Symtab.table;
wenzelm@57886
    26
  val empty: T = Symtab.empty;
wenzelm@57886
    27
  val extend = I;
wenzelm@57886
    28
  val merge = Symtab.join (K Item_Net.merge);
wenzelm@57886
    29
);
wenzelm@57886
    30
wenzelm@57886
    31
fun new_entry name =
wenzelm@57886
    32
  Data.map (fn data =>
wenzelm@57886
    33
    if Symtab.defined data name
wenzelm@57886
    34
    then error ("Duplicate declaration of named theorems: " ^ quote name)
wenzelm@57886
    35
    else Symtab.update (name, Thm.full_rules) data);
wenzelm@57886
    36
wenzelm@57886
    37
fun the_entry context name =
wenzelm@57886
    38
  (case Symtab.lookup (Data.get context) name of
wenzelm@57886
    39
    NONE => error ("Undeclared named theorems " ^ quote name)
wenzelm@57886
    40
  | SOME entry => entry);
wenzelm@57886
    41
wenzelm@57886
    42
fun map_entry name f context =
wenzelm@57886
    43
  (the_entry context name; Data.map (Symtab.map_entry name f) context);
wenzelm@57886
    44
wenzelm@57886
    45
wenzelm@57886
    46
(* maintain content *)
wenzelm@57886
    47
wenzelm@57886
    48
fun member ctxt = Item_Net.member o the_entry (Context.Proof ctxt);
wenzelm@57886
    49
wenzelm@57886
    50
fun content context = rev o Item_Net.content o the_entry context;
wenzelm@57886
    51
val get = content o Context.Proof;
wenzelm@57886
    52
wenzelm@57886
    53
fun add_thm name = map_entry name o Item_Net.update;
wenzelm@57886
    54
fun del_thm name = map_entry name o Item_Net.remove;
wenzelm@57886
    55
wenzelm@57886
    56
val add = Thm.declaration_attribute o add_thm;
wenzelm@57886
    57
val del = Thm.declaration_attribute o del_thm;
wenzelm@57886
    58
wenzelm@57886
    59
wenzelm@57886
    60
(* declaration *)
wenzelm@57886
    61
wenzelm@57888
    62
fun declare binding descr lthy =
wenzelm@57886
    63
  let
wenzelm@57888
    64
    val name = Name_Space.full_name (Local_Theory.naming_of lthy) binding;
wenzelm@57886
    65
    val description =
wenzelm@57886
    66
      "declaration of " ^ (if descr = "" then Binding.name_of binding ^ " rules" else descr);
wenzelm@57888
    67
    val lthy' = lthy
wenzelm@57888
    68
      |> Local_Theory.background_theory
wenzelm@57888
    69
        (Global_Theory.add_thms_dynamic (binding, fn context => content context name) #>
wenzelm@57888
    70
         Attrib.setup binding (Attrib.add_del (add name) (del name)) description #>
wenzelm@57888
    71
         Context.theory_map (new_entry name))
wenzelm@57888
    72
      |> Local_Theory.map_contexts (K (Context.proof_map (new_entry name)))
wenzelm@57888
    73
      |> Local_Theory.declaration {syntax = false, pervasive = true} (fn phi => fn context =>
wenzelm@57888
    74
          let
wenzelm@57888
    75
            val binding' = Morphism.binding phi binding;
wenzelm@57888
    76
            val context' =
wenzelm@57888
    77
              context |> Context.mapping
wenzelm@57888
    78
                (Global_Theory.alias_fact binding' name)
wenzelm@57888
    79
                (fn ctxt =>
wenzelm@57888
    80
                  if Facts.defined (Proof_Context.facts_of ctxt) name
wenzelm@57888
    81
                  then Proof_Context.fact_alias binding' name ctxt
wenzelm@57888
    82
                  else ctxt);
wenzelm@57888
    83
          in context' end);
wenzelm@57888
    84
  in (name, lthy') end;
wenzelm@57886
    85
wenzelm@57886
    86
val _ =
wenzelm@57888
    87
  Outer_Syntax.local_theory @{command_spec "named_theorems"}
wenzelm@57886
    88
    "declare named collection of theorems"
wenzelm@57888
    89
    (Parse.binding -- Scan.optional Parse.text "" >> (fn (b, descr) => snd o declare b descr));
wenzelm@57886
    90
wenzelm@57886
    91
wenzelm@57886
    92
(* ML antiquotation *)
wenzelm@57886
    93
wenzelm@57886
    94
val _ = Theory.setup
wenzelm@57886
    95
  (ML_Antiquotation.inline @{binding named_theorems}
wenzelm@57886
    96
    (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (xname, pos)) =>
wenzelm@57886
    97
      let
wenzelm@57886
    98
        val thy = Proof_Context.theory_of ctxt;
wenzelm@57886
    99
        val name = Global_Theory.check_fact thy (xname, pos);
wenzelm@57886
   100
        val _ = get ctxt name handle ERROR msg => cat_error msg (Position.here pos);
wenzelm@57886
   101
      in ML_Syntax.print_string name end)));
wenzelm@57886
   102
wenzelm@57886
   103
end;