isabelle: src/HOL/Library/reify_data.ML@37d52be4d8db (annotated)

37744 3daaf23b9ab4 tuned titles haftmann parents: 33518 diff changeset	1	(* Title: HOL/Library/reify_data.ML
23545 2fddae6056ab Context Data for the reflection and reification methods chaieb parents: diff changeset	2	Author: Amine Chaieb, TU Muenchen
2fddae6056ab Context Data for the reflection and reification methods chaieb parents: diff changeset	3
24045 bead02a55952 renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms; wenzelm parents: 23647 diff changeset	4	Data for the reification and reflection methods.
23545 2fddae6056ab Context Data for the reflection and reification methods chaieb parents: diff changeset	5	*)
2fddae6056ab Context Data for the reflection and reification methods chaieb parents: diff changeset	6
2fddae6056ab Context Data for the reflection and reification methods chaieb parents: diff changeset	7	signature REIFY_DATA =
2fddae6056ab Context Data for the reflection and reification methods chaieb parents: diff changeset	8	sig
29650 cc3958d31b1d Reflection.thy now in HOL/Library haftmann parents: 25979 diff changeset	9	val get: Proof.context -> thm list * thm list
cc3958d31b1d Reflection.thy now in HOL/Library haftmann parents: 25979 diff changeset	10	val add: attribute
23606 60950b22dcbf Cleaned add and del attributes chaieb parents: 23545 diff changeset	11	val del: attribute
29650 cc3958d31b1d Reflection.thy now in HOL/Library haftmann parents: 25979 diff changeset	12	val radd: attribute
cc3958d31b1d Reflection.thy now in HOL/Library haftmann parents: 25979 diff changeset	13	val rdel: attribute
23545 2fddae6056ab Context Data for the reflection and reification methods chaieb parents: diff changeset	14	val setup: theory -> theory
2fddae6056ab Context Data for the reflection and reification methods chaieb parents: diff changeset	15	end;
2fddae6056ab Context Data for the reflection and reification methods chaieb parents: diff changeset	16
2fddae6056ab Context Data for the reflection and reification methods chaieb parents: diff changeset	17	structure Reify_Data : REIFY_DATA =
2fddae6056ab Context Data for the reflection and reification methods chaieb parents: diff changeset	18	struct
2fddae6056ab Context Data for the reflection and reification methods chaieb parents: diff changeset	19
33518 24563731b9b2 adapted Generic_Data; wenzelm parents: 30528 diff changeset	20	structure Data = Generic_Data
24045 bead02a55952 renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms; wenzelm parents: 23647 diff changeset	21	(
29650 cc3958d31b1d Reflection.thy now in HOL/Library haftmann parents: 25979 diff changeset	22	type T = thm list * thm list;
cc3958d31b1d Reflection.thy now in HOL/Library haftmann parents: 25979 diff changeset	23	val empty = ([], []);
cc3958d31b1d Reflection.thy now in HOL/Library haftmann parents: 25979 diff changeset	24	val extend = I;
33518 24563731b9b2 adapted Generic_Data; wenzelm parents: 30528 diff changeset	25	fun merge ((ths1, rths1), (ths2, rths2)) =
24563731b9b2 adapted Generic_Data; wenzelm parents: 30528 diff changeset	26	(Thm.merge_thms (ths1, ths2), Thm.merge_thms (rths1, rths2));
24045 bead02a55952 renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms; wenzelm parents: 23647 diff changeset	27	);
23545 2fddae6056ab Context Data for the reflection and reification methods chaieb parents: diff changeset	28
2fddae6056ab Context Data for the reflection and reification methods chaieb parents: diff changeset	29	val get = Data.get o Context.Proof;
2fddae6056ab Context Data for the reflection and reification methods chaieb parents: diff changeset	30
29650 cc3958d31b1d Reflection.thy now in HOL/Library haftmann parents: 25979 diff changeset	31	val add = Thm.declaration_attribute (Data.map o apfst o Thm.add_thm);
cc3958d31b1d Reflection.thy now in HOL/Library haftmann parents: 25979 diff changeset	32	val del = Thm.declaration_attribute (Data.map o apfst o Thm.del_thm);
cc3958d31b1d Reflection.thy now in HOL/Library haftmann parents: 25979 diff changeset	33	val radd = Thm.declaration_attribute (Data.map o apsnd o Thm.add_thm);
cc3958d31b1d Reflection.thy now in HOL/Library haftmann parents: 25979 diff changeset	34	val rdel = Thm.declaration_attribute (Data.map o apsnd o Thm.del_thm);
23545 2fddae6056ab Context Data for the reflection and reification methods chaieb parents: diff changeset	35
30528 7173bf123335 simplified attribute setup; wenzelm parents: 29650 diff changeset	36	val setup =
7173bf123335 simplified attribute setup; wenzelm parents: 29650 diff changeset	37	Attrib.setup @{binding reify} (Attrib.add_del add del) "reify data" #>
7173bf123335 simplified attribute setup; wenzelm parents: 29650 diff changeset	38	Attrib.setup @{binding reflection} (Attrib.add_del radd rdel) "reflection data";
23545 2fddae6056ab Context Data for the reflection and reification methods chaieb parents: diff changeset	39
2fddae6056ab Context Data for the reflection and reification methods chaieb parents: diff changeset	40	end;

author	wenzelm
	Fri, 01 Jul 2011 18:11:17 +0200
changeset 43632	37d52be4d8db
parent 37744	3daaf23b9ab4
permissions	-rw-r--r--