(* Title: Pure/ML/ml_thms.ML
ID: $Id$
Author: Makarius
Isar theorem values within ML.
*)
signature ML_THMS =
sig
val the_thms: Proof.context -> int -> thm list
val the_thm: Proof.context -> int -> thm
end;
structure ML_Thms: ML_THMS =
struct
(* auxiliary facts table *)
structure AuxFacts = ProofDataFun
(
type T = thm list Inttab.table;
fun init _ = Inttab.empty;
);
val put_thms = AuxFacts.map o Inttab.update;
fun the_thms ctxt name = the (Inttab.lookup (AuxFacts.get ctxt) name);
fun the_thm ctxt name = the_single (the_thms ctxt name);
fun thm_bind kind a i =
"val " ^ a ^ " = ML_Thms.the_" ^ kind ^
" (ML_Context.the_local_context ()) " ^ string_of_int i ^ ";\n";
(* fact references *)
fun thm_antiq kind scan = ML_Context.add_antiq kind
(scan >> (fn ths => fn {struct_name, background} =>
let
val i = serial ();
val (a, background') = background
|> ML_Antiquote.variant kind ||> put_thms (i, ths);
val ml = (thm_bind kind a i, struct_name ^ "." ^ a);
in (K ml, background') end));
val _ = thm_antiq "thm" (Attrib.thm >> single);
val _ = thm_antiq "thms" Attrib.thms;
(* ad-hoc goals *)
val by = Args.$$$ "by";
val goal = Scan.unless (Scan.lift by) Args.prop;
val _ = ML_Context.add_antiq "lemma"
(Args.context -- Args.mode "open" -- Scan.repeat1 goal --
Scan.lift (by |-- Method.parse -- Scan.option Method.parse) >>
(fn (((ctxt, is_open), props), methods) => fn {struct_name, background} =>
let
val i = serial ();
val prep_result = Goal.norm_result #> not is_open ? Thm.close_derivation;
fun after_qed [res] goal_ctxt =
put_thms (i, map prep_result (ProofContext.export goal_ctxt ctxt res)) goal_ctxt;
val ctxt' = ctxt
|> Proof.theorem_i NONE after_qed [map (rpair []) props]
|> Proof.global_terminal_proof methods;
val (a, background') = background
|> ML_Antiquote.variant "lemma" ||> put_thms (i, the_thms ctxt' i);
val ml = (thm_bind (if length props = 1 then "thm" else "thms") a i, struct_name ^ "." ^ a);
in (K ml, background') end));
end;