13 end; |
13 end; |
14 |
14 |
15 signature ATTRIB = |
15 signature ATTRIB = |
16 sig |
16 sig |
17 include BASIC_ATTRIB |
17 include BASIC_ATTRIB |
|
18 exception ATTRIB_FAIL of (string * Position.T) * exn |
18 val global_attribute: theory -> Args.src -> theory attribute |
19 val global_attribute: theory -> Args.src -> theory attribute |
19 val local_attribute: theory -> Args.src -> Proof.context attribute |
20 val local_attribute: theory -> Args.src -> Proof.context attribute |
|
21 val local_attribute': Proof.context -> Args.src -> Proof.context attribute |
20 val add_attributes: (bstring * ((Args.src -> theory attribute) * |
22 val add_attributes: (bstring * ((Args.src -> theory attribute) * |
21 (Args.src -> Proof.context attribute)) * string) list -> theory -> theory |
23 (Args.src -> Proof.context attribute)) * string) list -> theory -> theory |
22 val global_thm: theory * Args.T list -> tthm * (theory * Args.T list) |
24 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) |
25 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) |
26 val global_thmss: theory * Args.T list -> tthm list * (theory * Args.T list) |
80 val ((raw_name, _), pos) = Args.dest_src src; |
84 val ((raw_name, _), pos) = Args.dest_src src; |
81 val name = NameSpace.intern space raw_name; |
85 val name = NameSpace.intern space raw_name; |
82 in |
86 in |
83 (case Symtab.lookup (attrs, name) of |
87 (case Symtab.lookup (attrs, name) of |
84 None => error ("Unknown attribute: " ^ quote name ^ Position.str_of pos) |
88 None => error ("Unknown attribute: " ^ quote name ^ Position.str_of pos) |
85 | Some ((p, _), _) => which p src) |
89 | Some ((p, _), _) => transform_failure (curry ATTRIB_FAIL (name, pos)) (which p src)) |
86 end; |
90 end; |
87 in attr end; |
91 in attr end; |
88 |
92 |
89 val global_attribute = gen_attribute fst; |
93 val global_attribute = gen_attribute fst; |
90 val local_attribute = gen_attribute snd; |
94 val local_attribute = gen_attribute snd; |
178 |
180 |
179 val global_APP = syntax (global_thmss >> apply); |
181 val global_APP = syntax (global_thmss >> apply); |
180 val local_APP = syntax (local_thmss >> apply); |
182 val local_APP = syntax (local_thmss >> apply); |
181 |
183 |
182 |
184 |
183 (* instantiations *) |
185 (* where: named instantiations *) |
184 |
186 |
185 (* FIXME assumes non var hyps *) (* FIXME move (see also drule.ML) *) |
187 fun read_instantiate context_of insts x thm = |
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))); |
|
188 |
|
189 fun read_instantiate context_of raw_insts x thm = |
|
190 let |
188 let |
191 val ctxt = context_of x; |
189 val ctxt = context_of x; |
192 val sign = ProofContext.sign_of ctxt; |
190 val sign = ProofContext.sign_of ctxt; |
193 |
191 |
194 val vars = vars_of thm; |
192 val vars = Drule.vars_of thm; |
195 fun get_typ xi = |
193 fun get_typ xi = |
196 (case assoc (vars, xi) of |
194 (case assoc (vars, xi) of |
197 Some T => T |
195 Some T => T |
198 | None => error ("No such variable in theorem: " ^ Syntax.string_of_vname xi)); |
196 | None => error ("No such variable in theorem: " ^ Syntax.string_of_vname xi)); |
199 |
197 |
200 val (xs, ss) = Library.split_list raw_insts; |
198 val (xs, ss) = Library.split_list insts; |
201 val Ts = map get_typ xs; |
199 val Ts = map get_typ xs; |
202 |
200 |
203 (* FIXME really declare_thm (!!!!??????) *) |
|
204 val (ts, envT) = ProofContext.read_termTs (ctxt |> ProofContext.declare_thm thm) (ss ~~ Ts); |
201 val (ts, envT) = ProofContext.read_termTs (ctxt |> ProofContext.declare_thm thm) (ss ~~ Ts); |
205 |
|
206 val cenvT = map (apsnd (Thm.ctyp_of sign)) envT; |
202 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); |
203 val cenv = |
|
204 map (fn (xi, t) => pairself (Thm.cterm_of sign) (Var (xi, fastype_of t), t)) |
|
205 (gen_distinct (fn ((x1, t1), (x2, t2)) => x1 = x2 andalso t1 aconv t2) (xs ~~ ts)); |
208 in Thm.instantiate (cenvT, cenv) thm end; |
206 in Thm.instantiate (cenvT, cenv) thm end; |
209 |
207 |
210 |
208 fun insts x = Scan.lift (Args.enum "and" (Args.var --| Args.$$$ "=" -- Args.name)) x; |
211 fun insts x = Scan.lift (Args.enum1 "and" (Args.var --| Args.$$$ "=" -- Args.name)) x; |
209 |
212 fun gen_where context_of = syntax (insts >> (Attribute.rule o read_instantiate context_of)); |
210 fun gen_where context_of = syntax (insts >> (Attribute.rule o read_instantiate context_of)); |
213 |
211 |
214 val global_where = gen_where ProofContext.init; |
212 val global_where = gen_where ProofContext.init; |
215 val local_where = gen_where I; |
213 val local_where = gen_where I; |
|
214 |
|
215 |
|
216 (* with: positional instantiations *) |
|
217 |
|
218 fun read_instantiate' context_of (args, concl_args) x thm = |
|
219 let |
|
220 fun zip_vars _ [] = [] |
|
221 | zip_vars (_ :: xs) (None :: opt_ts) = zip_vars xs opt_ts |
|
222 | zip_vars ((x, _) :: xs) (Some t :: opt_ts) = (x, t) :: zip_vars xs opt_ts |
|
223 | zip_vars [] _ = error "More instantiations than variables in theorem"; |
|
224 val insts = |
|
225 zip_vars (Drule.vars_of_terms [#prop (Thm.rep_thm thm)]) args @ |
|
226 zip_vars (Drule.vars_of_terms [Thm.concl_of thm]) concl_args; |
|
227 in read_instantiate context_of insts x thm end; |
|
228 |
|
229 val concl = Args.$$$ "concl" -- Args.$$$ ":"; |
|
230 val inst_arg = Scan.unless concl (Args.$$$ "_" >> K None || Args.name >> Some); |
|
231 val inst_args = Scan.repeat inst_arg; |
|
232 fun insts' x = Scan.lift (inst_args -- Scan.optional (concl |-- Args.!!! inst_args) []) x; |
|
233 |
|
234 fun gen_with context_of = syntax (insts' >> (Attribute.rule o read_instantiate' context_of)); |
|
235 |
|
236 val global_with = gen_with ProofContext.init; |
|
237 val local_with = gen_with I; |
216 |
238 |
217 |
239 |
218 (* misc rules *) |
240 (* misc rules *) |
219 |
241 |
220 fun standard x = no_args (Attribute.rule (K Drule.standard)) x; |
242 fun standard x = no_args (Attribute.rule (K Drule.standard)) x; |
227 (* pure_attributes *) |
249 (* pure_attributes *) |
228 |
250 |
229 val pure_attributes = |
251 val pure_attributes = |
230 [("tag", (gen_tag, gen_tag), "tag theorem"), |
252 [("tag", (gen_tag, gen_tag), "tag theorem"), |
231 ("untag", (gen_untag, gen_untag), "untag theorem"), |
253 ("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"), |
|
234 ("RS", (global_RS, local_RS), "resolve with rule"), |
254 ("RS", (global_RS, local_RS), "resolve with rule"), |
235 ("APP", (global_APP, local_APP), "resolve rule with"), |
255 ("APP", (global_APP, local_APP), "resolve rule with"), |
236 ("where", (global_where, local_where), "instantiate theorem (named vars)"), |
256 ("where", (global_where, local_where), "named instantiation of theorem"), |
|
257 ("with", (global_with, local_with), "positional instantiation of theorem"), |
237 ("standard", (standard, standard), "put theorem into standard form"), |
258 ("standard", (standard, standard), "put theorem into standard form"), |
238 ("elimify", (elimify, elimify), "turn destruct rule into elimination rule"), |
259 ("elimify", (elimify, elimify), "turn destruct rule into elimination rule"), |
239 ("transfer", (global_transfer, local_transfer), "transfer theorem to this theory")]; |
260 ("transfer", (global_transfer, local_transfer), "transfer theorem to this theory")]; |
240 |
261 |
241 |
262 |