src/Pure/Tools/named_theorems.ML
author wenzelm
Tue, 27 Nov 2018 21:07:39 +0100
changeset 69349 7cef9e386ffe
parent 69289 bf6937af7fe8
child 69592 a80d8ec6c998
permissions -rw-r--r--
more accurate positions for "name" (quoted string) and "embedded" (cartouche): refer to content without delimiters, which is e.g. relevant for systematic selection/renaming of scope groups; tuned signature;
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
61900
wenzelm
parents: 61049
diff changeset
    11
  val clear: string -> Context.generic -> Context.generic
57886
7cae177c9084 support for named collections of theorems in canonical order;
wenzelm
parents:
diff changeset
    12
  val add_thm: string -> thm -> Context.generic -> Context.generic
7cae177c9084 support for named collections of theorems in canonical order;
wenzelm
parents:
diff changeset
    13
  val del_thm: string -> thm -> Context.generic -> Context.generic
7cae177c9084 support for named collections of theorems in canonical order;
wenzelm
parents:
diff changeset
    14
  val add: string -> attribute
7cae177c9084 support for named collections of theorems in canonical order;
wenzelm
parents:
diff changeset
    15
  val del: string -> attribute
59920
86d302846b16 check wrt. proper context, e.g. relevant for 'experiment' target;
wenzelm
parents: 59879
diff changeset
    16
  val check: Proof.context -> string * Position.T -> string
57888
9c193dcc8ec8 some localization;
wenzelm
parents: 57886
diff changeset
    17
  val declare: binding -> string -> local_theory -> string * local_theory
57886
7cae177c9084 support for named collections of theorems in canonical order;
wenzelm
parents:
diff changeset
    18
end;
7cae177c9084 support for named collections of theorems in canonical order;
wenzelm
parents:
diff changeset
    19
7cae177c9084 support for named collections of theorems in canonical order;
wenzelm
parents:
diff changeset
    20
structure Named_Theorems: NAMED_THEOREMS =
7cae177c9084 support for named collections of theorems in canonical order;
wenzelm
parents:
diff changeset
    21
struct
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
(* context 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
structure Data = Generic_Data
7cae177c9084 support for named collections of theorems in canonical order;
wenzelm
parents:
diff changeset
    26
(
7cae177c9084 support for named collections of theorems in canonical order;
wenzelm
parents:
diff changeset
    27
  type T = thm Item_Net.T Symtab.table;
7cae177c9084 support for named collections of theorems in canonical order;
wenzelm
parents:
diff changeset
    28
  val empty: T = Symtab.empty;
7cae177c9084 support for named collections of theorems in canonical order;
wenzelm
parents:
diff changeset
    29
  val extend = I;
57965
a18a351132b7 made SML/NJ happy;
wenzelm
parents: 57929
diff changeset
    30
  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
    31
);
7cae177c9084 support for named collections of theorems in canonical order;
wenzelm
parents:
diff changeset
    32
7cae177c9084 support for named collections of theorems in canonical order;
wenzelm
parents:
diff changeset
    33
fun new_entry name =
7cae177c9084 support for named collections of theorems in canonical order;
wenzelm
parents:
diff changeset
    34
  Data.map (fn data =>
7cae177c9084 support for named collections of theorems in canonical order;
wenzelm
parents:
diff changeset
    35
    if Symtab.defined data name
7cae177c9084 support for named collections of theorems in canonical order;
wenzelm
parents:
diff changeset
    36
    then error ("Duplicate declaration of named theorems: " ^ quote name)
7cae177c9084 support for named collections of theorems in canonical order;
wenzelm
parents:
diff changeset
    37
    else Symtab.update (name, Thm.full_rules) data);
7cae177c9084 support for named collections of theorems in canonical order;
wenzelm
parents:
diff changeset
    38
59920
86d302846b16 check wrt. proper context, e.g. relevant for 'experiment' target;
wenzelm
parents: 59879
diff changeset
    39
fun undeclared name = "Undeclared named theorems " ^ quote name;
86d302846b16 check wrt. proper context, e.g. relevant for 'experiment' target;
wenzelm
parents: 59879
diff changeset
    40
69185
6f79d6a5acad proper completion for @{named_theorems};
wenzelm
parents: 67649
diff changeset
    41
val defined_entry = Symtab.defined o Data.get;
6f79d6a5acad proper completion for @{named_theorems};
wenzelm
parents: 67649
diff changeset
    42
57886
7cae177c9084 support for named collections of theorems in canonical order;
wenzelm
parents:
diff changeset
    43
fun the_entry context name =
7cae177c9084 support for named collections of theorems in canonical order;
wenzelm
parents:
diff changeset
    44
  (case Symtab.lookup (Data.get context) name of
59920
86d302846b16 check wrt. proper context, e.g. relevant for 'experiment' target;
wenzelm
parents: 59879
diff changeset
    45
    NONE => error (undeclared name)
57886
7cae177c9084 support for named collections of theorems in canonical order;
wenzelm
parents:
diff changeset
    46
  | SOME entry => entry);
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 map_entry name f context =
7cae177c9084 support for named collections of theorems in canonical order;
wenzelm
parents:
diff changeset
    49
  (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
    50
7cae177c9084 support for named collections of theorems in canonical order;
wenzelm
parents:
diff changeset
    51
7cae177c9084 support for named collections of theorems in canonical order;
wenzelm
parents:
diff changeset
    52
(* maintain content *)
7cae177c9084 support for named collections of theorems in canonical order;
wenzelm
parents:
diff changeset
    53
7cae177c9084 support for named collections of theorems in canonical order;
wenzelm
parents:
diff changeset
    54
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
    55
61049
0d401f874942 trim context for persistent storage;
wenzelm
parents: 59936
diff changeset
    56
fun content context =
67649
1e1782c1aedf tuned signature;
wenzelm
parents: 67147
diff changeset
    57
  rev o map (Thm.transfer'' context) o Item_Net.content o the_entry context;
61049
0d401f874942 trim context for persistent storage;
wenzelm
parents: 59936
diff changeset
    58
57886
7cae177c9084 support for named collections of theorems in canonical order;
wenzelm
parents:
diff changeset
    59
val get = content o Context.Proof;
7cae177c9084 support for named collections of theorems in canonical order;
wenzelm
parents:
diff changeset
    60
61900
wenzelm
parents: 61049
diff changeset
    61
fun clear name = map_entry name (K Thm.full_rules);
wenzelm
parents: 61049
diff changeset
    62
61049
0d401f874942 trim context for persistent storage;
wenzelm
parents: 59936
diff changeset
    63
fun add_thm name th = map_entry name (Item_Net.update (Thm.trim_context th));
57886
7cae177c9084 support for named collections of theorems in canonical order;
wenzelm
parents:
diff changeset
    64
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
    65
7cae177c9084 support for named collections of theorems in canonical order;
wenzelm
parents:
diff changeset
    66
val add = Thm.declaration_attribute o add_thm;
7cae177c9084 support for named collections of theorems in canonical order;
wenzelm
parents:
diff changeset
    67
val del = Thm.declaration_attribute o del_thm;
7cae177c9084 support for named collections of theorems in canonical order;
wenzelm
parents:
diff changeset
    68
7cae177c9084 support for named collections of theorems in canonical order;
wenzelm
parents:
diff changeset
    69
59920
86d302846b16 check wrt. proper context, e.g. relevant for 'experiment' target;
wenzelm
parents: 59879
diff changeset
    70
(* check *)
86d302846b16 check wrt. proper context, e.g. relevant for 'experiment' target;
wenzelm
parents: 59879
diff changeset
    71
86d302846b16 check wrt. proper context, e.g. relevant for 'experiment' target;
wenzelm
parents: 59879
diff changeset
    72
fun check ctxt (xname, pos) =
86d302846b16 check wrt. proper context, e.g. relevant for 'experiment' target;
wenzelm
parents: 59879
diff changeset
    73
  let
86d302846b16 check wrt. proper context, e.g. relevant for 'experiment' target;
wenzelm
parents: 59879
diff changeset
    74
    val context = Context.Proof ctxt;
86d302846b16 check wrt. proper context, e.g. relevant for 'experiment' target;
wenzelm
parents: 59879
diff changeset
    75
    val fact_ref = Facts.Named ((xname, Position.none), NONE);
69185
6f79d6a5acad proper completion for @{named_theorems};
wenzelm
parents: 67649
diff changeset
    76
    fun err () =
6f79d6a5acad proper completion for @{named_theorems};
wenzelm
parents: 67649
diff changeset
    77
      let
6f79d6a5acad proper completion for @{named_theorems};
wenzelm
parents: 67649
diff changeset
    78
        val space = Facts.space_of (Proof_Context.facts_of ctxt);
6f79d6a5acad proper completion for @{named_theorems};
wenzelm
parents: 67649
diff changeset
    79
        val completion = Name_Space.completion context space (defined_entry context) (xname, pos);
69289
bf6937af7fe8 clarified signature;
wenzelm
parents: 69185
diff changeset
    80
      in error (undeclared xname ^ Position.here pos ^ Completion.markup_report [completion]) end;
59920
86d302846b16 check wrt. proper context, e.g. relevant for 'experiment' target;
wenzelm
parents: 59879
diff changeset
    81
  in
86d302846b16 check wrt. proper context, e.g. relevant for 'experiment' target;
wenzelm
parents: 59879
diff changeset
    82
    (case try (Proof_Context.get_fact_generic context) fact_ref of
69185
6f79d6a5acad proper completion for @{named_theorems};
wenzelm
parents: 67649
diff changeset
    83
      SOME (SOME name, _) => if defined_entry context name then name else err ()
59920
86d302846b16 check wrt. proper context, e.g. relevant for 'experiment' target;
wenzelm
parents: 59879
diff changeset
    84
    | _ => err ())
86d302846b16 check wrt. proper context, e.g. relevant for 'experiment' target;
wenzelm
parents: 59879
diff changeset
    85
  end;
86d302846b16 check wrt. proper context, e.g. relevant for 'experiment' target;
wenzelm
parents: 59879
diff changeset
    86
86d302846b16 check wrt. proper context, e.g. relevant for 'experiment' target;
wenzelm
parents: 59879
diff changeset
    87
57886
7cae177c9084 support for named collections of theorems in canonical order;
wenzelm
parents:
diff changeset
    88
(* declaration *)
7cae177c9084 support for named collections of theorems in canonical order;
wenzelm
parents:
diff changeset
    89
57888
9c193dcc8ec8 some localization;
wenzelm
parents: 57886
diff changeset
    90
fun declare binding descr lthy =
57886
7cae177c9084 support for named collections of theorems in canonical order;
wenzelm
parents:
diff changeset
    91
  let
59879
wenzelm
parents: 59878
diff changeset
    92
    val name = Local_Theory.full_name lthy binding;
57886
7cae177c9084 support for named collections of theorems in canonical order;
wenzelm
parents:
diff changeset
    93
    val description =
7cae177c9084 support for named collections of theorems in canonical order;
wenzelm
parents:
diff changeset
    94
      "declaration of " ^ (if descr = "" then Binding.name_of binding ^ " rules" else descr);
57888
9c193dcc8ec8 some localization;
wenzelm
parents: 57886
diff changeset
    95
    val lthy' = lthy
57929
c5063c033a5a tuned signature -- proper Local_Theory.add_thms_dynamic;
wenzelm
parents: 57928
diff changeset
    96
      |> Local_Theory.background_theory (Context.theory_map (new_entry name))
c5063c033a5a tuned signature -- proper Local_Theory.add_thms_dynamic;
wenzelm
parents: 57928
diff changeset
    97
      |> 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
    98
      |> Local_Theory.add_thms_dynamic (binding, fn context => content context name)
57927
f14c1248d064 localized attribute definitions;
wenzelm
parents: 57888
diff changeset
    99
      |> Attrib.local_setup binding (Attrib.add_del (add name) (del name)) description
57888
9c193dcc8ec8 some localization;
wenzelm
parents: 57886
diff changeset
   100
  in (name, lthy') end;
57886
7cae177c9084 support for named collections of theorems in canonical order;
wenzelm
parents:
diff changeset
   101
7cae177c9084 support for named collections of theorems in canonical order;
wenzelm
parents:
diff changeset
   102
7cae177c9084 support for named collections of theorems in canonical order;
wenzelm
parents:
diff changeset
   103
(* ML antiquotation *)
7cae177c9084 support for named collections of theorems in canonical order;
wenzelm
parents:
diff changeset
   104
7cae177c9084 support for named collections of theorems in canonical order;
wenzelm
parents:
diff changeset
   105
val _ = Theory.setup
67147
dea94b1aabc3 prefer control symbol antiquotations;
wenzelm
parents: 67146
diff changeset
   106
  (ML_Antiquotation.inline \<^binding>\<open>named_theorems\<close>
69349
7cef9e386ffe more accurate positions for "name" (quoted string) and "embedded" (cartouche): refer to content without delimiters, which is e.g. relevant for systematic selection/renaming of scope groups;
wenzelm
parents: 69289
diff changeset
   107
    (Args.context -- Scan.lift Args.embedded_position >>
59920
86d302846b16 check wrt. proper context, e.g. relevant for 'experiment' target;
wenzelm
parents: 59879
diff changeset
   108
      (fn (ctxt, name) => ML_Syntax.print_string (check ctxt name))));
57886
7cae177c9084 support for named collections of theorems in canonical order;
wenzelm
parents:
diff changeset
   109
7cae177c9084 support for named collections of theorems in canonical order;
wenzelm
parents:
diff changeset
   110
end;