author | wenzelm |
Mon, 07 Nov 2011 21:34:11 +0100 | |
changeset 45395 | 830c9b9b0d66 |
parent 45198 | f579dab96734 |
child 45592 | 8baa0b7f3f66 |
permissions | -rw-r--r-- |
27389 | 1 |
(* Title: Pure/ML/ml_thms.ML |
2 |
Author: Makarius |
|
3 |
||
4 |
Isar theorem values within ML. |
|
5 |
*) |
|
6 |
||
7 |
signature ML_THMS = |
|
8 |
sig |
|
9 |
val the_thms: Proof.context -> int -> thm list |
|
10 |
val the_thm: Proof.context -> int -> thm |
|
11 |
end; |
|
12 |
||
13 |
structure ML_Thms: ML_THMS = |
|
14 |
struct |
|
15 |
||
16 |
(* auxiliary facts table *) |
|
17 |
||
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
36950
diff
changeset
|
18 |
structure Aux_Facts = Proof_Data |
27389 | 19 |
( |
20 |
type T = thm list Inttab.table; |
|
21 |
fun init _ = Inttab.empty; |
|
22 |
); |
|
23 |
||
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
36950
diff
changeset
|
24 |
val put_thms = Aux_Facts.map o Inttab.update; |
27389 | 25 |
|
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
36950
diff
changeset
|
26 |
fun the_thms ctxt name = the (Inttab.lookup (Aux_Facts.get ctxt) name); |
27389 | 27 |
fun the_thm ctxt name = the_single (the_thms ctxt name); |
28 |
||
29 |
fun thm_bind kind a i = |
|
30 |
"val " ^ a ^ " = ML_Thms.the_" ^ kind ^ |
|
31 |
" (ML_Context.the_local_context ()) " ^ string_of_int i ^ ";\n"; |
|
32 |
||
33 |
||
34 |
(* fact references *) |
|
35 |
||
43560
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42360
diff
changeset
|
36 |
fun thm_antiq kind scan = ML_Context.add_antiq (Binding.name kind) |
35019
1ec0a3ff229e
simplified interface for ML antiquotations, struct_name is always "Isabelle";
wenzelm
parents:
33700
diff
changeset
|
37 |
(fn _ => scan >> (fn ths => fn background => |
27389 | 38 |
let |
39 |
val i = serial (); |
|
40 |
val (a, background') = background |
|
41 |
|> ML_Antiquote.variant kind ||> put_thms (i, ths); |
|
41486
82c1e348bc18
reverted 08240feb69c7 -- breaks positions of reports;
wenzelm
parents:
41376
diff
changeset
|
42 |
val ml = (thm_bind kind a i, "Isabelle." ^ a); |
27389 | 43 |
in (K ml, background') end)); |
44 |
||
43560
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42360
diff
changeset
|
45 |
val _ = |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42360
diff
changeset
|
46 |
Context.>> (Context.map_theory |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42360
diff
changeset
|
47 |
(thm_antiq "thm" (Attrib.thm >> single) #> |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42360
diff
changeset
|
48 |
thm_antiq "thms" Attrib.thms)); |
27389 | 49 |
|
50 |
||
51 |
(* ad-hoc goals *) |
|
52 |
||
30266
970bf4f594c9
ML antiquotation @{lemma}: allow 'and' list, proper simultaneous type-checking;
wenzelm
parents:
29606
diff
changeset
|
53 |
val and_ = Args.$$$ "and"; |
27809
a1e409db516b
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27521
diff
changeset
|
54 |
val by = Args.$$$ "by"; |
45198 | 55 |
val goal = Scan.unless (by || and_) Args.name_source; |
27389 | 56 |
|
43560
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42360
diff
changeset
|
57 |
val _ = |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42360
diff
changeset
|
58 |
Context.>> (Context.map_theory |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42360
diff
changeset
|
59 |
(ML_Context.add_antiq (Binding.name "lemma") |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42360
diff
changeset
|
60 |
(fn _ => Args.context -- Args.mode "open" -- |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42360
diff
changeset
|
61 |
Scan.lift (Parse.and_list1 (Scan.repeat1 goal) -- |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42360
diff
changeset
|
62 |
(by |-- Method.parse -- Scan.option Method.parse)) >> |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42360
diff
changeset
|
63 |
(fn ((ctxt, is_open), (raw_propss, methods)) => fn background => |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42360
diff
changeset
|
64 |
let |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42360
diff
changeset
|
65 |
val propss = burrow (map (rpair []) o Syntax.read_props ctxt) raw_propss; |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42360
diff
changeset
|
66 |
val i = serial (); |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42360
diff
changeset
|
67 |
val prep_result = Goal.norm_result #> not is_open ? Thm.close_derivation; |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42360
diff
changeset
|
68 |
fun after_qed res goal_ctxt = |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42360
diff
changeset
|
69 |
put_thms (i, map prep_result (Proof_Context.export goal_ctxt ctxt (flat res))) goal_ctxt; |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42360
diff
changeset
|
70 |
val ctxt' = ctxt |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42360
diff
changeset
|
71 |
|> Proof.theorem NONE after_qed propss |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42360
diff
changeset
|
72 |
|> Proof.global_terminal_proof methods; |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42360
diff
changeset
|
73 |
val (a, background') = background |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42360
diff
changeset
|
74 |
|> ML_Antiquote.variant "lemma" ||> put_thms (i, the_thms ctxt' i); |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42360
diff
changeset
|
75 |
val ml = |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42360
diff
changeset
|
76 |
(thm_bind (if length (flat propss) = 1 then "thm" else "thms") a i, "Isabelle." ^ a); |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42360
diff
changeset
|
77 |
in (K ml, background') end)))); |
27389 | 78 |
|
79 |
end; |
|
80 |