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
     1 (*  Title:      HOL/Library/reify_data.ML
     2     Author:     Amine Chaieb, TU Muenchen
     3 
     4 Data for the reification and reflection methods.
     5 *)
     6 
     7 signature REIFY_DATA =
     8 sig
     9   val get: Proof.context -> thm list * thm list
    10   val add: attribute
    11   val del: attribute
    12   val radd: attribute
    13   val rdel: attribute
    14   val setup: theory -> theory
    15 end;
    16 
    17 structure Reify_Data : REIFY_DATA =
    18 struct
    19 
    20 structure Data = Generic_Data
    21 (
    22   type T = thm list * thm list;
    23   val empty = ([], []);
    24   val extend = I;
    25   fun merge ((ths1, rths1), (ths2, rths2)) =
    26     (Thm.merge_thms (ths1, ths2), Thm.merge_thms (rths1, rths2));
    27 );
    28 
    29 val get = Data.get o Context.Proof;
    30 
    31 val add = Thm.declaration_attribute (Data.map o apfst o Thm.add_thm);
    32 val del = Thm.declaration_attribute (Data.map o apfst o Thm.del_thm);
    33 val radd = Thm.declaration_attribute (Data.map o apsnd o Thm.add_thm);
    34 val rdel = Thm.declaration_attribute (Data.map o apsnd o Thm.del_thm);
    35 
    36 val setup =
    37   Attrib.setup @{binding reify} (Attrib.add_del add del) "reify data" #>
    38   Attrib.setup @{binding reflection} (Attrib.add_del radd rdel) "reflection data";
    39 
    40 end;