wenzelm@27389
|
1 |
(* Title: Pure/ML/ml_thms.ML
|
wenzelm@27389
|
2 |
Author: Makarius
|
wenzelm@27389
|
3 |
|
wenzelm@27389
|
4 |
Isar theorem values within ML.
|
wenzelm@27389
|
5 |
*)
|
wenzelm@27389
|
6 |
|
wenzelm@27389
|
7 |
signature ML_THMS =
|
wenzelm@27389
|
8 |
sig
|
wenzelm@27389
|
9 |
val the_thms: Proof.context -> int -> thm list
|
wenzelm@27389
|
10 |
val the_thm: Proof.context -> int -> thm
|
wenzelm@27389
|
11 |
end;
|
wenzelm@27389
|
12 |
|
wenzelm@27389
|
13 |
structure ML_Thms: ML_THMS =
|
wenzelm@27389
|
14 |
struct
|
wenzelm@27389
|
15 |
|
wenzelm@27389
|
16 |
(* auxiliary facts table *)
|
wenzelm@27389
|
17 |
|
wenzelm@37216
|
18 |
structure Aux_Facts = Proof_Data
|
wenzelm@27389
|
19 |
(
|
wenzelm@27389
|
20 |
type T = thm list Inttab.table;
|
wenzelm@27389
|
21 |
fun init _ = Inttab.empty;
|
wenzelm@27389
|
22 |
);
|
wenzelm@27389
|
23 |
|
wenzelm@37216
|
24 |
val put_thms = Aux_Facts.map o Inttab.update;
|
wenzelm@27389
|
25 |
|
wenzelm@37216
|
26 |
fun the_thms ctxt name = the (Inttab.lookup (Aux_Facts.get ctxt) name);
|
wenzelm@27389
|
27 |
fun the_thm ctxt name = the_single (the_thms ctxt name);
|
wenzelm@27389
|
28 |
|
wenzelm@27389
|
29 |
fun thm_bind kind a i =
|
wenzelm@27389
|
30 |
"val " ^ a ^ " = ML_Thms.the_" ^ kind ^
|
wenzelm@27389
|
31 |
" (ML_Context.the_local_context ()) " ^ string_of_int i ^ ";\n";
|
wenzelm@27389
|
32 |
|
wenzelm@27389
|
33 |
|
wenzelm@27389
|
34 |
(* fact references *)
|
wenzelm@27389
|
35 |
|
wenzelm@27389
|
36 |
fun thm_antiq kind scan = ML_Context.add_antiq kind
|
wenzelm@35019
|
37 |
(fn _ => scan >> (fn ths => fn background =>
|
wenzelm@27389
|
38 |
let
|
wenzelm@27389
|
39 |
val i = serial ();
|
wenzelm@27389
|
40 |
val (a, background') = background
|
wenzelm@27389
|
41 |
|> ML_Antiquote.variant kind ||> put_thms (i, ths);
|
wenzelm@35019
|
42 |
val ml = (thm_bind kind a i, "Isabelle." ^ a);
|
wenzelm@27389
|
43 |
in (K ml, background') end));
|
wenzelm@27389
|
44 |
|
wenzelm@27389
|
45 |
val _ = thm_antiq "thm" (Attrib.thm >> single);
|
wenzelm@27389
|
46 |
val _ = thm_antiq "thms" Attrib.thms;
|
wenzelm@27389
|
47 |
|
wenzelm@27389
|
48 |
|
wenzelm@27389
|
49 |
(* ad-hoc goals *)
|
wenzelm@27389
|
50 |
|
wenzelm@30266
|
51 |
val and_ = Args.$$$ "and";
|
wenzelm@27809
|
52 |
val by = Args.$$$ "by";
|
wenzelm@30266
|
53 |
val goal = Scan.unless (by || and_) Args.name;
|
wenzelm@27389
|
54 |
|
wenzelm@27389
|
55 |
val _ = ML_Context.add_antiq "lemma"
|
wenzelm@33700
|
56 |
(fn _ => Args.context -- Args.mode "open" --
|
wenzelm@36950
|
57 |
Scan.lift (Parse.and_list1 (Scan.repeat1 goal) --
|
wenzelm@30266
|
58 |
(by |-- Method.parse -- Scan.option Method.parse)) >>
|
wenzelm@35019
|
59 |
(fn ((ctxt, is_open), (raw_propss, methods)) => fn background =>
|
wenzelm@27389
|
60 |
let
|
wenzelm@30266
|
61 |
val propss = burrow (map (rpair []) o Syntax.read_props ctxt) raw_propss;
|
wenzelm@27389
|
62 |
val i = serial ();
|
wenzelm@33700
|
63 |
val prep_result = Goal.norm_result #> not is_open ? Thm.close_derivation;
|
wenzelm@30266
|
64 |
fun after_qed res goal_ctxt =
|
wenzelm@30266
|
65 |
put_thms (i, map prep_result (ProofContext.export goal_ctxt ctxt (flat res))) goal_ctxt;
|
wenzelm@27389
|
66 |
val ctxt' = ctxt
|
wenzelm@36334
|
67 |
|> Proof.theorem NONE after_qed propss
|
wenzelm@27521
|
68 |
|> Proof.global_terminal_proof methods;
|
wenzelm@27389
|
69 |
val (a, background') = background
|
wenzelm@27389
|
70 |
|> ML_Antiquote.variant "lemma" ||> put_thms (i, the_thms ctxt' i);
|
wenzelm@30266
|
71 |
val ml =
|
wenzelm@35019
|
72 |
(thm_bind (if length (flat propss) = 1 then "thm" else "thms") a i, "Isabelle." ^ a);
|
wenzelm@27389
|
73 |
in (K ml, background') end));
|
wenzelm@27389
|
74 |
|
wenzelm@27389
|
75 |
end;
|
wenzelm@27389
|
76 |
|