24592
|
1 |
(* Title: Pure/Isar/instance.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Florian Haftmann, TU Muenchen
|
|
4 |
|
25462
|
5 |
A primitive instance command, based on instantiation target.
|
24592
|
6 |
*)
|
|
7 |
|
|
8 |
signature INSTANCE =
|
|
9 |
sig
|
25536
|
10 |
val instantiation_cmd: xstring list * sort * xstring -> theory -> local_theory
|
|
11 |
val instance_cmd: xstring * sort * xstring -> ((bstring * Attrib.src list) * xstring) list
|
25462
|
12 |
-> theory -> Proof.state
|
24592
|
13 |
end;
|
|
14 |
|
|
15 |
structure Instance : INSTANCE =
|
|
16 |
struct
|
|
17 |
|
25536
|
18 |
fun read_multi_arity thy (raw_tycos, raw_sorts, raw_sort) =
|
|
19 |
let
|
|
20 |
val all_arities = map (fn raw_tyco => Sign.read_arity thy
|
|
21 |
(raw_tyco, raw_sorts, raw_sort)) raw_tycos;
|
|
22 |
val tycos = map #1 all_arities;
|
|
23 |
val (_, sorts, sort) = hd all_arities;
|
|
24 |
in (tycos, sorts, sort) end;
|
|
25 |
|
25462
|
26 |
fun instantiation_cmd raw_arities thy =
|
25536
|
27 |
TheoryTarget.instantiation (read_multi_arity thy raw_arities) thy;
|
25462
|
28 |
|
25502
|
29 |
fun gen_instance prep_arity prep_attr parse_term do_proof do_proof' raw_arities defs thy =
|
24592
|
30 |
let
|
25536
|
31 |
val (tyco, sorts, sort) = prep_arity thy raw_arities;
|
25462
|
32 |
fun export_defs ctxt =
|
|
33 |
let
|
|
34 |
val ctxt_thy = ProofContext.init (ProofContext.theory_of ctxt);
|
|
35 |
in
|
|
36 |
map (snd o snd)
|
|
37 |
#> map (Assumption.export false ctxt ctxt_thy)
|
|
38 |
#> Variable.export ctxt ctxt_thy
|
|
39 |
end;
|
|
40 |
fun mk_def ctxt ((name, raw_attr), raw_t) =
|
24592
|
41 |
let
|
25462
|
42 |
val attr = map (prep_attr thy) raw_attr;
|
25485
|
43 |
val t = parse_term ctxt raw_t;
|
25462
|
44 |
in (NONE, ((name, attr), t)) end;
|
25485
|
45 |
fun define def ctxt =
|
|
46 |
let
|
|
47 |
val def' = (apsnd o apsnd) (Syntax.check_prop ctxt) def;
|
|
48 |
in Specification.definition def' ctxt end;
|
25569
|
49 |
val _ = if not (null defs) then Output.legacy_feature
|
25829
|
50 |
"Instance command with attached definitions; use instantiation instead." else ();
|
25536
|
51 |
in if not (null defs) orelse forall (Class.is_class thy) sort
|
25502
|
52 |
then
|
25462
|
53 |
thy
|
25536
|
54 |
|> TheoryTarget.instantiation ([tyco], sorts, sort)
|
25462
|
55 |
|> `(fn ctxt => map (mk_def ctxt) defs)
|
|
56 |
|-> (fn defs => fold_map Specification.definition defs)
|
|
57 |
|-> (fn defs => `(fn ctxt => export_defs ctxt defs))
|
25514
|
58 |
||> LocalTheory.reinit
|
25502
|
59 |
|-> (fn defs => do_proof defs)
|
|
60 |
else
|
|
61 |
thy
|
25536
|
62 |
|> do_proof' (tyco, sorts, sort)
|
25462
|
63 |
end;
|
24592
|
64 |
|
25485
|
65 |
val instance_cmd = gen_instance Sign.read_arity Attrib.intern_src Syntax.parse_prop
|
25502
|
66 |
(fn _ => Class.instantiation_instance Class.conclude_instantiation) (Class.instance_arity I);
|
24592
|
67 |
|
|
68 |
end;
|