haftmann@37744: (*  Title:      HOL/Library/reify_data.ML
chaieb@23545:     Author:     Amine Chaieb, TU Muenchen
chaieb@23545: 
wenzelm@24045: Data for the reification and reflection methods.
chaieb@23545: *)
chaieb@23545: 
chaieb@23545: signature REIFY_DATA =
chaieb@23545: sig
haftmann@29650:   val get: Proof.context -> thm list * thm list
haftmann@29650:   val add: attribute
chaieb@23606:   val del: attribute
haftmann@29650:   val radd: attribute
haftmann@29650:   val rdel: attribute
chaieb@23545:   val setup: theory -> theory
chaieb@23545: end;
chaieb@23545: 
chaieb@23545: structure Reify_Data : REIFY_DATA =
chaieb@23545: struct
chaieb@23545: 
wenzelm@33518: structure Data = Generic_Data
wenzelm@24045: (
haftmann@29650:   type T = thm list * thm list;
haftmann@29650:   val empty = ([], []);
haftmann@29650:   val extend = I;
wenzelm@33518:   fun merge ((ths1, rths1), (ths2, rths2)) =
wenzelm@33518:     (Thm.merge_thms (ths1, ths2), Thm.merge_thms (rths1, rths2));
wenzelm@24045: );
chaieb@23545: 
chaieb@23545: val get = Data.get o Context.Proof;
chaieb@23545: 
haftmann@29650: val add = Thm.declaration_attribute (Data.map o apfst o Thm.add_thm);
haftmann@29650: val del = Thm.declaration_attribute (Data.map o apfst o Thm.del_thm);
haftmann@29650: val radd = Thm.declaration_attribute (Data.map o apsnd o Thm.add_thm);
haftmann@29650: val rdel = Thm.declaration_attribute (Data.map o apsnd o Thm.del_thm);
chaieb@23545: 
wenzelm@30528: val setup =
wenzelm@30528:   Attrib.setup @{binding reify} (Attrib.add_del add del) "reify data" #>
wenzelm@30528:   Attrib.setup @{binding reflection} (Attrib.add_del radd rdel) "reflection data";
chaieb@23545: 
chaieb@23545: end;