author | haftmann |
Mon, 21 Jan 2008 08:43:29 +0100 | |
changeset 25929 | 6bfef23e26be |
parent 24045 | bead02a55952 |
child 25979 | 3297781f8141 |
permissions | -rw-r--r-- |
23545 | 1 |
(* Title: HOL/ex/reflection_data.ML |
2 |
ID: $Id$ |
|
3 |
Author: Amine Chaieb, TU Muenchen |
|
4 |
||
24045
bead02a55952
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
23647
diff
changeset
|
5 |
Data for the reification and reflection methods. |
23545 | 6 |
*) |
7 |
||
8 |
signature REIFY_DATA = |
|
9 |
sig |
|
24045
bead02a55952
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
23647
diff
changeset
|
10 |
type entry = thm list * thm list |
23545 | 11 |
val get: Proof.context -> entry |
23606 | 12 |
val del: attribute |
24045
bead02a55952
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
23647
diff
changeset
|
13 |
val add: attribute |
23545 | 14 |
val setup: theory -> theory |
15 |
end; |
|
16 |
||
17 |
structure Reify_Data : REIFY_DATA = |
|
18 |
struct |
|
19 |
||
24045
bead02a55952
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
23647
diff
changeset
|
20 |
type entry = thm list * thm list; |
23545 | 21 |
|
22 |
structure Data = GenericDataFun |
|
24045
bead02a55952
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
23647
diff
changeset
|
23 |
( |
23647
89286c4e7928
Context data now consist of eqations for reification and equations for correctness theorems for reflection; Added attribute reflection to store correctness theorems to be trued by default
chaieb
parents:
23606
diff
changeset
|
24 |
type T = entry |
24045
bead02a55952
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
23647
diff
changeset
|
25 |
val empty = ([], []) |
23545 | 26 |
val extend = I |
24045
bead02a55952
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
23647
diff
changeset
|
27 |
fun merge _ = pairself Thm.merge_thms |
bead02a55952
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
23647
diff
changeset
|
28 |
); |
23545 | 29 |
|
30 |
val get = Data.get o Context.Proof; |
|
31 |
||
24045
bead02a55952
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
23647
diff
changeset
|
32 |
val add = Thm.declaration_attribute (fn th => fn context => |
bead02a55952
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
23647
diff
changeset
|
33 |
context |> Data.map (apfst (Thm.add_thm th))) |
23545 | 34 |
|
24045
bead02a55952
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
23647
diff
changeset
|
35 |
val del = Thm.declaration_attribute (fn th => fn context => |
bead02a55952
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
23647
diff
changeset
|
36 |
context |> Data.map (apfst (Thm.del_thm th))) |
23647
89286c4e7928
Context data now consist of eqations for reification and equations for correctness theorems for reflection; Added attribute reflection to store correctness theorems to be trued by default
chaieb
parents:
23606
diff
changeset
|
37 |
|
24045
bead02a55952
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
23647
diff
changeset
|
38 |
val radd = Thm.declaration_attribute (fn th => fn context => |
bead02a55952
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
23647
diff
changeset
|
39 |
context |> Data.map (apsnd (Thm.add_thm th))) |
23647
89286c4e7928
Context data now consist of eqations for reification and equations for correctness theorems for reflection; Added attribute reflection to store correctness theorems to be trued by default
chaieb
parents:
23606
diff
changeset
|
40 |
|
24045
bead02a55952
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
23647
diff
changeset
|
41 |
val rdel = Thm.declaration_attribute (fn th => fn context => |
bead02a55952
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
23647
diff
changeset
|
42 |
context |> Data.map (apsnd (Thm.del_thm th))) |
23545 | 43 |
|
44 |
(* concrete syntax *) |
|
23606 | 45 |
(* |
23545 | 46 |
local |
47 |
fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K (); |
|
48 |
||
49 |
val constsN = "consts"; |
|
50 |
val addN = "add"; |
|
51 |
val delN = "del"; |
|
52 |
val any_keyword = keyword constsN || keyword addN || keyword delN; |
|
53 |
val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat; |
|
54 |
val terms = thms >> map (term_of o Drule.dest_term); |
|
55 |
||
56 |
fun optional scan = Scan.optional scan []; |
|
57 |
||
58 |
in |
|
59 |
fun att_syntax src = src |> Attrib.syntax |
|
60 |
((Scan.lift (Args.$$$ "del") |-- thms) >> del || |
|
61 |
optional (keyword addN |-- thms) >> add) |
|
62 |
end; |
|
23606 | 63 |
*) |
23545 | 64 |
|
65 |
(* theory setup *) |
|
66 |
val setup = |
|
23647
89286c4e7928
Context data now consist of eqations for reification and equations for correctness theorems for reflection; Added attribute reflection to store correctness theorems to be trued by default
chaieb
parents:
23606
diff
changeset
|
67 |
Attrib.add_attributes [("reify", Attrib.add_del_args add del, "Reify data"), |
89286c4e7928
Context data now consist of eqations for reification and equations for correctness theorems for reflection; Added attribute reflection to store correctness theorems to be trued by default
chaieb
parents:
23606
diff
changeset
|
68 |
("reflection", Attrib.add_del_args radd rdel, "Reflection data")]; |
23545 | 69 |
end; |