5823
|
1 |
(* Title: Pure/Isar/attrib.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Markus Wenzel, TU Muenchen
|
|
4 |
|
|
5 |
Symbolic theorem attributes.
|
|
6 |
*)
|
|
7 |
|
|
8 |
signature BASIC_ATTRIB =
|
|
9 |
sig
|
|
10 |
val print_attributes: theory -> unit
|
5879
|
11 |
val Attribute: bstring -> (Args.src -> theory attribute) * (Args.src -> Proof.context attribute)
|
|
12 |
-> string -> unit
|
5823
|
13 |
end;
|
|
14 |
|
|
15 |
signature ATTRIB =
|
|
16 |
sig
|
|
17 |
include BASIC_ATTRIB
|
|
18 |
val global_attribute: theory -> Args.src -> theory attribute
|
|
19 |
val local_attribute: theory -> Args.src -> Proof.context attribute
|
|
20 |
val add_attributes: (bstring * ((Args.src -> theory attribute) *
|
|
21 |
(Args.src -> Proof.context attribute)) * string) list -> theory -> theory
|
5879
|
22 |
val global_thm: theory * Args.T list -> tthm * (theory * Args.T list)
|
|
23 |
val global_thms: theory * Args.T list -> tthm list * (theory * Args.T list)
|
|
24 |
val global_thmss: theory * Args.T list -> tthm list * (theory * Args.T list)
|
|
25 |
val local_thm: Proof.context * Args.T list -> tthm * (Proof.context * Args.T list)
|
|
26 |
val local_thms: Proof.context * Args.T list -> tthm list * (Proof.context * Args.T list)
|
|
27 |
val local_thmss: Proof.context * Args.T list -> tthm list * (Proof.context * Args.T list)
|
|
28 |
val syntax: ('a * Args.T list -> 'a attribute * ('a * Args.T list)) -> Args.src -> 'a attribute
|
5823
|
29 |
val no_args: 'a attribute -> Args.src -> 'a attribute
|
|
30 |
val setup: (theory -> theory) list
|
|
31 |
end;
|
|
32 |
|
|
33 |
structure Attrib: ATTRIB =
|
|
34 |
struct
|
|
35 |
|
|
36 |
|
|
37 |
(** attributes theory data **)
|
|
38 |
|
|
39 |
(* data kind 'Isar/attributes' *)
|
|
40 |
|
|
41 |
structure AttributesDataArgs =
|
|
42 |
struct
|
|
43 |
val name = "Isar/attributes";
|
|
44 |
type T =
|
|
45 |
{space: NameSpace.T,
|
|
46 |
attrs:
|
|
47 |
((((Args.src -> theory attribute) * (Args.src -> Proof.context attribute))
|
|
48 |
* string) * stamp) Symtab.table};
|
|
49 |
|
|
50 |
val empty = {space = NameSpace.empty, attrs = Symtab.empty};
|
|
51 |
val prep_ext = I;
|
|
52 |
|
|
53 |
fun merge ({space = space1, attrs = attrs1}, {space = space2, attrs = attrs2}) =
|
|
54 |
{space = NameSpace.merge (space1, space2),
|
|
55 |
attrs = Symtab.merge eq_snd (attrs1, attrs2) handle Symtab.DUPS dups =>
|
|
56 |
error ("Attempt to merge different versions of attributes " ^ commas_quote dups)};
|
|
57 |
|
|
58 |
fun print _ ({space, attrs}) =
|
|
59 |
let
|
|
60 |
fun prt_attr (name, ((_, comment), _)) = Pretty.block
|
|
61 |
[Pretty.str (NameSpace.cond_extern space name ^ ":"), Pretty.brk 2, Pretty.str comment];
|
|
62 |
in
|
|
63 |
Pretty.writeln (Display.pretty_name_space ("attribute name space", space));
|
|
64 |
Pretty.writeln (Pretty.big_list "attributes:" (map prt_attr (Symtab.dest attrs)))
|
|
65 |
end;
|
|
66 |
end;
|
|
67 |
|
|
68 |
structure AttributesData = TheoryDataFun(AttributesDataArgs);
|
|
69 |
val print_attributes = AttributesData.print;
|
|
70 |
|
|
71 |
|
|
72 |
(* get global / local attributes *)
|
|
73 |
|
|
74 |
fun gen_attribute which thy =
|
|
75 |
let
|
|
76 |
val {space, attrs} = AttributesData.get thy;
|
|
77 |
|
5879
|
78 |
fun attr src =
|
|
79 |
let
|
|
80 |
val ((raw_name, _), pos) = Args.dest_src src;
|
|
81 |
val name = NameSpace.intern space raw_name;
|
|
82 |
in
|
5823
|
83 |
(case Symtab.lookup (attrs, name) of
|
|
84 |
None => error ("Unknown attribute: " ^ quote name ^ Position.str_of pos)
|
5879
|
85 |
| Some ((p, _), _) => which p src)
|
5823
|
86 |
end;
|
|
87 |
in attr end;
|
|
88 |
|
|
89 |
val global_attribute = gen_attribute fst;
|
|
90 |
val local_attribute = gen_attribute snd;
|
5879
|
91 |
val local_attribute' = local_attribute o ProofContext.theory_of;
|
5823
|
92 |
|
|
93 |
|
|
94 |
(* add_attributes *)
|
|
95 |
|
|
96 |
fun add_attributes raw_attrs thy =
|
|
97 |
let
|
|
98 |
val full = Sign.full_name (Theory.sign_of thy);
|
|
99 |
val new_attrs =
|
|
100 |
map (fn (name, (f, g), comment) => (full name, (((f, g), comment), stamp ()))) raw_attrs;
|
|
101 |
|
|
102 |
val {space, attrs} = AttributesData.get thy;
|
|
103 |
val space' = NameSpace.extend (space, map fst new_attrs);
|
|
104 |
val attrs' = Symtab.extend (attrs, new_attrs) handle Symtab.DUPS dups =>
|
|
105 |
error ("Duplicate declaration of attributes(s) " ^ commas_quote dups);
|
|
106 |
in thy |> AttributesData.put {space = space', attrs = attrs'} end;
|
|
107 |
|
5879
|
108 |
(*implicit version*)
|
|
109 |
fun Attribute name att cmt = Context.>> (add_attributes [(name, att, cmt)]);
|
5823
|
110 |
|
5879
|
111 |
|
|
112 |
|
|
113 |
(** attribute parsers **)
|
|
114 |
|
|
115 |
(* tags *)
|
5823
|
116 |
|
5879
|
117 |
fun tag x = Scan.lift (Args.name -- Scan.repeat Args.name) x;
|
|
118 |
|
|
119 |
|
|
120 |
(* theorems *)
|
|
121 |
|
|
122 |
fun gen_thm get attrib app =
|
|
123 |
Scan.depend (fn st => Args.name -- Args.opt_attribs >>
|
|
124 |
(fn (name, srcs) => app ((st, get st name), map (attrib st) srcs)));
|
5823
|
125 |
|
5879
|
126 |
val global_thm = gen_thm PureThy.get_tthm global_attribute Attribute.apply;
|
|
127 |
val global_thms = gen_thm PureThy.get_tthms global_attribute Attribute.applys;
|
|
128 |
val global_thmss = Scan.repeat global_thms >> flat;
|
|
129 |
|
|
130 |
val local_thm = gen_thm ProofContext.get_tthm local_attribute' Attribute.apply;
|
|
131 |
val local_thms = gen_thm ProofContext.get_tthms local_attribute' Attribute.applys;
|
|
132 |
val local_thmss = Scan.repeat local_thms >> flat;
|
|
133 |
|
5823
|
134 |
|
5879
|
135 |
|
|
136 |
(** attribute syntax **)
|
5823
|
137 |
|
5879
|
138 |
fun syntax scan src (st, th) =
|
|
139 |
let val (st', f) = Args.syntax "attribute" scan st src
|
|
140 |
in f (st', th) end;
|
|
141 |
|
|
142 |
fun no_args x = syntax (Scan.succeed x);
|
5823
|
143 |
|
|
144 |
|
|
145 |
|
|
146 |
(** Pure attributes **)
|
|
147 |
|
|
148 |
(* tags *)
|
|
149 |
|
5879
|
150 |
fun gen_tag x = syntax (tag >> Attribute.tag) x;
|
|
151 |
fun gen_untag x = syntax (tag >> Attribute.untag) x;
|
5823
|
152 |
fun gen_lemma x = no_args Attribute.tag_lemma x;
|
|
153 |
fun gen_assumption x = no_args Attribute.tag_assumption x;
|
|
154 |
|
|
155 |
|
5879
|
156 |
(* transfer *)
|
|
157 |
|
|
158 |
fun gen_transfer theory_of = no_args (Attribute.rule (fn st => Thm.transfer (theory_of st)));
|
|
159 |
|
|
160 |
val global_transfer = gen_transfer I;
|
|
161 |
val local_transfer = gen_transfer ProofContext.theory_of;
|
|
162 |
|
|
163 |
|
|
164 |
(* RS *)
|
|
165 |
|
|
166 |
fun resolve (i, B) (x, A) =
|
|
167 |
(x, Attribute.tthm_of (Attribute.thm_of A RSN (i, Attribute.thm_of B)));
|
|
168 |
|
|
169 |
fun gen_RS thm = syntax (Scan.lift (Scan.optional Args.nat 1) -- thm >> resolve);
|
|
170 |
val global_RS = gen_RS global_thm;
|
|
171 |
val local_RS = gen_RS local_thm;
|
|
172 |
|
|
173 |
|
|
174 |
(* APP *)
|
|
175 |
|
|
176 |
fun apply Bs (x, A) =
|
|
177 |
(x, Attribute.tthm_of (Attribute.thms_of Bs MRS Attribute.thm_of A));
|
|
178 |
|
|
179 |
val global_APP = syntax (global_thmss >> apply);
|
|
180 |
val local_APP = syntax (local_thmss >> apply);
|
|
181 |
|
|
182 |
|
|
183 |
(* instantiations *)
|
|
184 |
|
|
185 |
(* FIXME assumes non var hyps *) (* FIXME move (see also drule.ML) *)
|
|
186 |
val add_vars = foldl_aterms (fn (vs, Var v) => v ins vs | (vs, _) => vs);
|
|
187 |
fun vars_of thm = (add_vars ([], #prop (Thm.rep_thm thm)));
|
5823
|
188 |
|
5879
|
189 |
fun read_instantiate context_of raw_insts x thm =
|
|
190 |
let
|
|
191 |
val ctxt = context_of x;
|
|
192 |
val sign = ProofContext.sign_of ctxt;
|
|
193 |
|
|
194 |
val vars = vars_of thm;
|
|
195 |
fun get_typ xi =
|
|
196 |
(case assoc (vars, xi) of
|
|
197 |
Some T => T
|
|
198 |
| None => error ("No such variable in theorem: " ^ Syntax.string_of_vname xi));
|
|
199 |
|
|
200 |
val (xs, ss) = Library.split_list raw_insts;
|
|
201 |
val Ts = map get_typ xs;
|
|
202 |
|
|
203 |
(* FIXME really declare_thm (!!!!??????) *)
|
|
204 |
val (ts, envT) = ProofContext.read_termTs (ctxt |> ProofContext.declare_thm thm) (ss ~~ Ts);
|
5823
|
205 |
|
5879
|
206 |
val cenvT = map (apsnd (Thm.ctyp_of sign)) envT;
|
|
207 |
val cenv = map2 (fn (xi, t) => pairself (Thm.cterm_of sign) (Var (xi, fastype_of t), t)) (xs, ts);
|
|
208 |
in Thm.instantiate (cenvT, cenv) thm end;
|
|
209 |
|
|
210 |
|
5894
|
211 |
fun insts x = Scan.lift (Args.enum1 "and" (Args.var --| Args.$$$ "=" -- Args.name)) x;
|
5879
|
212 |
fun gen_where context_of = syntax (insts >> (Attribute.rule o read_instantiate context_of));
|
5823
|
213 |
|
5879
|
214 |
val global_where = gen_where ProofContext.init;
|
|
215 |
val local_where = gen_where I;
|
|
216 |
|
|
217 |
|
|
218 |
(* misc rules *)
|
|
219 |
|
|
220 |
fun standard x = no_args (Attribute.rule (K Drule.standard)) x;
|
|
221 |
fun elimify x = no_args (Attribute.rule (K Tactic.make_elim)) x;
|
|
222 |
|
|
223 |
|
|
224 |
|
|
225 |
(** theory setup **)
|
5823
|
226 |
|
|
227 |
(* pure_attributes *)
|
|
228 |
|
|
229 |
val pure_attributes =
|
|
230 |
[("tag", (gen_tag, gen_tag), "tag theorem"),
|
|
231 |
("untag", (gen_untag, gen_untag), "untag theorem"),
|
|
232 |
("lemma", (gen_lemma, gen_lemma), "tag as lemma"),
|
|
233 |
("assumption", (gen_assumption, gen_assumption), "tag as assumption"),
|
5879
|
234 |
("RS", (global_RS, local_RS), "resolve with rule"),
|
|
235 |
("APP", (global_APP, local_APP), "resolve rule with"),
|
|
236 |
("where", (global_where, local_where), "instantiate theorem (named vars)"),
|
|
237 |
("standard", (standard, standard), "put theorem into standard form"),
|
|
238 |
("elimify", (elimify, elimify), "turn destruct rule into elimination rule"),
|
|
239 |
("transfer", (global_transfer, local_transfer), "transfer theorem to this theory")];
|
5823
|
240 |
|
|
241 |
|
5879
|
242 |
(* setup *)
|
5823
|
243 |
|
|
244 |
val setup = [AttributesData.init, add_attributes pure_attributes];
|
|
245 |
|
|
246 |
|
|
247 |
end;
|
|
248 |
|
|
249 |
|
|
250 |
structure BasicAttrib: BASIC_ATTRIB = Attrib;
|
|
251 |
open BasicAttrib;
|