author | wenzelm |
Thu, 10 Jul 2008 13:37:34 +0200 | |
changeset 27521 | 44081396d735 |
parent 27389 | 823c7ec3ea4f |
child 27809 | a1e409db516b |
permissions | -rw-r--r-- |
27389 | 1 |
(* Title: Pure/ML/ml_thms.ML |
2 |
ID: $Id$ |
|
3 |
Author: Makarius |
|
4 |
||
5 |
Isar theorem values within ML. |
|
6 |
*) |
|
7 |
||
8 |
signature ML_THMS = |
|
9 |
sig |
|
10 |
val the_thms: Proof.context -> int -> thm list |
|
11 |
val the_thm: Proof.context -> int -> thm |
|
12 |
end; |
|
13 |
||
14 |
structure ML_Thms: ML_THMS = |
|
15 |
struct |
|
16 |
||
17 |
(* auxiliary facts table *) |
|
18 |
||
19 |
structure AuxFacts = ProofDataFun |
|
20 |
( |
|
21 |
type T = thm list Inttab.table; |
|
22 |
fun init _ = Inttab.empty; |
|
23 |
); |
|
24 |
||
25 |
val put_thms = AuxFacts.map o Inttab.update; |
|
26 |
||
27 |
fun the_thms ctxt name = the (Inttab.lookup (AuxFacts.get ctxt) name); |
|
28 |
fun the_thm ctxt name = the_single (the_thms ctxt name); |
|
29 |
||
30 |
fun thm_bind kind a i = |
|
31 |
"val " ^ a ^ " = ML_Thms.the_" ^ kind ^ |
|
32 |
" (ML_Context.the_local_context ()) " ^ string_of_int i ^ ";\n"; |
|
33 |
||
34 |
||
35 |
(* fact references *) |
|
36 |
||
37 |
fun thm_antiq kind scan = ML_Context.add_antiq kind |
|
38 |
(scan >> (fn ths => fn {struct_name, background} => |
|
39 |
let |
|
40 |
val i = serial (); |
|
41 |
val (a, background') = background |
|
42 |
|> ML_Antiquote.variant kind ||> put_thms (i, ths); |
|
43 |
val ml = (thm_bind kind a i, struct_name ^ "." ^ a); |
|
44 |
in (K ml, background') end)); |
|
45 |
||
46 |
val _ = thm_antiq "thm" (Attrib.thm >> single); |
|
47 |
val _ = thm_antiq "thms" Attrib.thms; |
|
48 |
||
49 |
||
50 |
(* ad-hoc goals *) |
|
51 |
||
52 |
fun by x = Scan.lift (Args.$$$ "by") x; |
|
53 |
val goal = Scan.unless by Args.prop; |
|
54 |
||
55 |
val _ = ML_Context.add_antiq "lemma" |
|
27521
44081396d735
@{lemma}: allow terminal method, close derivation unless (open) mode is given;
wenzelm
parents:
27389
diff
changeset
|
56 |
((Args.context -- Args.mode "open" -- Scan.repeat1 goal -- |
44081396d735
@{lemma}: allow terminal method, close derivation unless (open) mode is given;
wenzelm
parents:
27389
diff
changeset
|
57 |
(by |-- Scan.lift Method.parse_args -- Scan.option (Scan.lift Method.parse_args))) >> |
44081396d735
@{lemma}: allow terminal method, close derivation unless (open) mode is given;
wenzelm
parents:
27389
diff
changeset
|
58 |
(fn (((ctxt, is_open), props), methods) => fn {struct_name, background} => |
27389 | 59 |
let |
60 |
val i = serial (); |
|
27521
44081396d735
@{lemma}: allow terminal method, close derivation unless (open) mode is given;
wenzelm
parents:
27389
diff
changeset
|
61 |
val prep_result = Goal.norm_result #> not is_open ? Thm.close_derivation; |
27389 | 62 |
fun after_qed [res] goal_ctxt = |
27521
44081396d735
@{lemma}: allow terminal method, close derivation unless (open) mode is given;
wenzelm
parents:
27389
diff
changeset
|
63 |
put_thms (i, map prep_result (ProofContext.export goal_ctxt ctxt res)) goal_ctxt; |
27389 | 64 |
val ctxt' = ctxt |
65 |
|> Proof.theorem_i NONE after_qed [map (rpair []) props] |
|
27521
44081396d735
@{lemma}: allow terminal method, close derivation unless (open) mode is given;
wenzelm
parents:
27389
diff
changeset
|
66 |
|> Proof.global_terminal_proof methods; |
27389 | 67 |
val (a, background') = background |
68 |
|> ML_Antiquote.variant "lemma" ||> put_thms (i, the_thms ctxt' i); |
|
69 |
val ml = (thm_bind (if length props = 1 then "thm" else "thms") a i, struct_name ^ "." ^ a); |
|
70 |
in (K ml, background') end)); |
|
71 |
||
72 |
end; |
|
73 |