src/HOL/Library/reify_data.ML
author wenzelm
Sun, 08 Nov 2009 16:28:18 +0100
changeset 33518 24563731b9b2
parent 30528 7173bf123335
child 37744 3daaf23b9ab4
permissions -rw-r--r--
adapted Generic_Data; proper merge of fst/fst and snd/snd;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
29650
cc3958d31b1d Reflection.thy now in HOL/Library
haftmann
parents: 25979
diff changeset
     1
(*  Title:      HOL/Library/reflection_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;