src/HOL/Library/reify_data.ML
author hoelzl
Tue Jul 19 14:37:49 2011 +0200 (2011-07-19)
changeset 43922 c6f35921056e
parent 37744 3daaf23b9ab4
permissions -rw-r--r--
add nat => enat coercion
haftmann@37744
     1
(*  Title:      HOL/Library/reify_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;