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