src/HOL/Library/reify_data.ML
author wenzelm
Sun Nov 08 16:28:18 2009 +0100 (2009-11-08)
changeset 33518 24563731b9b2
parent 30528 7173bf123335
child 37744 3daaf23b9ab4
permissions -rw-r--r--
adapted Generic_Data;
proper merge of fst/fst and snd/snd;
haftmann@29650
     1
(*  Title:      HOL/Library/reflection_data.ML
chaieb@23545
     2
    Author:     Amine Chaieb, TU Muenchen
chaieb@23545
     3
wenzelm@24045
     4
Data for the reification and reflection methods.
chaieb@23545
     5
*)
chaieb@23545
     6
chaieb@23545
     7
signature REIFY_DATA =
chaieb@23545
     8
sig
haftmann@29650
     9
  val get: Proof.context -> thm list * thm list
haftmann@29650
    10
  val add: attribute
chaieb@23606
    11
  val del: attribute
haftmann@29650
    12
  val radd: attribute
haftmann@29650
    13
  val rdel: attribute
chaieb@23545
    14
  val setup: theory -> theory
chaieb@23545
    15
end;
chaieb@23545
    16
chaieb@23545
    17
structure Reify_Data : REIFY_DATA =
chaieb@23545
    18
struct
chaieb@23545
    19
wenzelm@33518
    20
structure Data = Generic_Data
wenzelm@24045
    21
(
haftmann@29650
    22
  type T = thm list * thm list;
haftmann@29650
    23
  val empty = ([], []);
haftmann@29650
    24
  val extend = I;
wenzelm@33518
    25
  fun merge ((ths1, rths1), (ths2, rths2)) =
wenzelm@33518
    26
    (Thm.merge_thms (ths1, ths2), Thm.merge_thms (rths1, rths2));
wenzelm@24045
    27
);
chaieb@23545
    28
chaieb@23545
    29
val get = Data.get o Context.Proof;
chaieb@23545
    30
haftmann@29650
    31
val add = Thm.declaration_attribute (Data.map o apfst o Thm.add_thm);
haftmann@29650
    32
val del = Thm.declaration_attribute (Data.map o apfst o Thm.del_thm);
haftmann@29650
    33
val radd = Thm.declaration_attribute (Data.map o apsnd o Thm.add_thm);
haftmann@29650
    34
val rdel = Thm.declaration_attribute (Data.map o apsnd o Thm.del_thm);
chaieb@23545
    35
wenzelm@30528
    36
val setup =
wenzelm@30528
    37
  Attrib.setup @{binding reify} (Attrib.add_del add del) "reify data" #>
wenzelm@30528
    38
  Attrib.setup @{binding reflection} (Attrib.add_del radd rdel) "reflection data";
chaieb@23545
    39
chaieb@23545
    40
end;