95 val cert = Thm.cterm_of thy; |
98 val cert = Thm.cterm_of thy; |
96 val certT = Thm.ctyp_of thy; |
99 val certT = Thm.ctyp_of thy; |
97 |
100 |
98 val (type_insts, term_insts) = List.partition (is_tvar o fst) mixed_insts; |
101 val (type_insts, term_insts) = List.partition (is_tvar o fst) mixed_insts; |
99 val internal_insts = term_insts |> map_filter |
102 val internal_insts = term_insts |> map_filter |
100 (fn (xi, Args.Term t) => SOME (xi, t) |
103 (fn (xi, T.Term t) => SOME (xi, t) |
101 | (_, Args.Text _) => NONE |
104 | (_, T.Text _) => NONE |
102 | (xi, _) => error_var "Term argument expected for " xi); |
105 | (xi, _) => error_var "Term argument expected for " xi); |
103 val external_insts = term_insts |> map_filter |
106 val external_insts = term_insts |> map_filter |
104 (fn (xi, Args.Text s) => SOME (xi, s) | _ => NONE); |
107 (fn (xi, T.Text s) => SOME (xi, s) | _ => NONE); |
105 |
108 |
106 |
109 |
107 (* mixed type instantiations *) |
110 (* mixed type instantiations *) |
108 |
111 |
109 fun readT (xi, arg) = |
112 fun readT (xi, arg) = |
110 let |
113 let |
111 val S = the_sort tvars xi; |
114 val S = the_sort tvars xi; |
112 val T = |
115 val T = |
113 (case arg of |
116 (case arg of |
114 Args.Text s => Syntax.read_typ ctxt s |
117 T.Text s => Syntax.read_typ ctxt s |
115 | Args.Typ T => T |
118 | T.Typ T => T |
116 | _ => error_var "Type argument expected for " xi); |
119 | _ => error_var "Type argument expected for " xi); |
117 in |
120 in |
118 if Sign.of_sort thy (T, S) then ((xi, S), T) |
121 if Sign.of_sort thy (T, S) then ((xi, S), T) |
119 else error_var "Incompatible sort for typ instantiation of " xi |
122 else error_var "Incompatible sort for typ instantiation of " xi |
120 end; |
123 end; |
167 val ((type_insts, term_insts), insts) = read_insts ctxt' (map snd mixed_insts) (tvars, vars); |
170 val ((type_insts, term_insts), insts) = read_insts ctxt' (map snd mixed_insts) (tvars, vars); |
168 |
171 |
169 val _ = (*assign internalized values*) |
172 val _ = (*assign internalized values*) |
170 mixed_insts |> List.app (fn (arg, (xi, _)) => |
173 mixed_insts |> List.app (fn (arg, (xi, _)) => |
171 if is_tvar xi then |
174 if is_tvar xi then |
172 Args.assign (SOME (Args.Typ (the (AList.lookup (op =) type_insts xi)))) arg |
175 T.assign (SOME (T.Typ (the (AList.lookup (op =) type_insts xi)))) arg |
173 else |
176 else |
174 Args.assign (SOME (Args.Term (the (AList.lookup (op =) term_insts xi)))) arg); |
177 T.assign (SOME (T.Term (the (AList.lookup (op =) term_insts xi)))) arg); |
175 in |
178 in |
176 Drule.instantiate insts thm |> RuleCases.save thm |
179 Drule.instantiate insts thm |> RuleCases.save thm |
177 end; |
180 end; |
178 |
181 |
179 fun read_instantiate_mixed' ctxt (args, concl_args) thm = |
182 fun read_instantiate_mixed' ctxt (args, concl_args) thm = |
192 |
195 |
193 (* instantiation of rule or goal state *) |
196 (* instantiation of rule or goal state *) |
194 |
197 |
195 fun read_instantiate ctxt args thm = |
198 fun read_instantiate ctxt args thm = |
196 read_instantiate_mixed (ctxt |> ProofContext.set_mode ProofContext.mode_schematic) (* FIXME !? *) |
199 read_instantiate_mixed (ctxt |> ProofContext.set_mode ProofContext.mode_schematic) (* FIXME !? *) |
197 (map (fn (x, y) => (Args.eof, (x, Args.Text y))) args) thm; |
200 (map (fn (x, y) => (T.eof, (x, T.Text y))) args) thm; |
198 |
201 |
199 fun instantiate_tac ctxt args = PRIMITIVE (read_instantiate ctxt args); |
202 fun instantiate_tac ctxt args = PRIMITIVE (read_instantiate ctxt args); |
200 |
203 |
201 |
204 |
202 |
205 |
205 (* where: named instantiation *) |
208 (* where: named instantiation *) |
206 |
209 |
207 local |
210 local |
208 |
211 |
209 val value = |
212 val value = |
210 Args.internal_typ >> Args.Typ || |
213 Args.internal_typ >> T.Typ || |
211 Args.internal_term >> Args.Term || |
214 Args.internal_term >> T.Term || |
212 Args.name >> Args.Text; |
215 Args.name >> T.Text; |
213 |
216 |
214 val inst = Args.var -- (Args.$$$ "=" |-- Args.ahead -- value) |
217 val inst = Args.var -- (Args.$$$ "=" |-- Scan.ahead P.not_eof -- value) |
215 >> (fn (xi, (a, v)) => (a, (xi, v))); |
218 >> (fn (xi, (a, v)) => (a, (xi, v))); |
216 |
219 |
217 in |
220 in |
218 |
221 |
219 val where_att = Attrib.syntax (Args.and_list (Scan.lift inst) >> (fn args => |
222 val where_att = Attrib.syntax (Scan.lift (P.and_list inst) >> (fn args => |
220 Thm.rule_attribute (fn context => read_instantiate_mixed (Context.proof_of context) args))); |
223 Thm.rule_attribute (fn context => read_instantiate_mixed (Context.proof_of context) args))); |
221 |
224 |
222 end; |
225 end; |
223 |
226 |
224 |
227 |
225 (* of: positional instantiation (terms only) *) |
228 (* of: positional instantiation (terms only) *) |
226 |
229 |
227 local |
230 local |
228 |
231 |
229 val value = |
232 val value = |
230 Args.internal_term >> Args.Term || |
233 Args.internal_term >> T.Term || |
231 Args.name >> Args.Text; |
234 Args.name >> T.Text; |
232 |
235 |
233 val inst = Args.ahead -- Args.maybe value; |
236 val inst = Scan.ahead P.not_eof -- Args.maybe value; |
234 val concl = Args.$$$ "concl" -- Args.colon; |
237 val concl = Args.$$$ "concl" -- Args.colon; |
235 |
238 |
236 val insts = |
239 val insts = |
237 Scan.repeat (Scan.unless concl inst) -- |
240 Scan.repeat (Scan.unless concl inst) -- |
238 Scan.optional (concl |-- Scan.repeat inst) []; |
241 Scan.optional (concl |-- Scan.repeat inst) []; |
404 |
407 |
405 (* method syntax *) |
408 (* method syntax *) |
406 |
409 |
407 val insts = |
410 val insts = |
408 Scan.optional |
411 Scan.optional |
409 (Args.and_list1 (Scan.lift (Args.name -- (Args.$$$ "=" |-- Args.!!! Args.name))) --| |
412 (Scan.lift (P.and_list1 (Args.name -- (Args.$$$ "=" |-- P.!!! Args.name)) --| Args.$$$ "in")) [] |
410 Scan.lift (Args.$$$ "in")) [] -- Attrib.thms; |
413 -- Attrib.thms; |
411 |
414 |
412 fun inst_args f src ctxt = |
415 fun inst_args f src ctxt = |
413 f ctxt (fst (Method.syntax (Args.goal_spec HEADGOAL -- insts) src ctxt)); |
416 f ctxt (fst (Method.syntax (Args.goal_spec HEADGOAL -- insts) src ctxt)); |
414 |
417 |
415 val insts_var = |
418 val insts_var = |
416 Scan.optional |
419 Scan.optional |
417 (Args.and_list1 (Scan.lift (Args.var -- (Args.$$$ "=" |-- Args.!!! Args.name))) --| |
420 (Scan.lift (P.and_list1 (Args.var -- (Args.$$$ "=" |-- P.!!! Args.name)) --| Args.$$$ "in")) [] |
418 Scan.lift (Args.$$$ "in")) [] -- Attrib.thms; |
421 -- Attrib.thms; |
419 |
422 |
420 fun inst_args_var f src ctxt = |
423 fun inst_args_var f src ctxt = |
421 f ctxt (fst (Method.syntax (Args.goal_spec HEADGOAL -- insts_var) src ctxt)); |
424 f ctxt (fst (Method.syntax (Args.goal_spec HEADGOAL -- insts_var) src ctxt)); |
422 |
425 |
423 |
426 |