author  wenzelm 
Tue, 21 Dec 2010 21:05:50 +0100  
changeset 41376  08240feb69c7 
parent 37216  3165bc303f66 
child 41486  82c1e348bc18 
permissions  rwrr 
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 

36 
fun thm_antiq kind scan = ML_Context.add_antiq 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); 

41376
08240feb69c7
more robust ML antiquotations  allow original tokens without adjacent whitespace;
wenzelm
parents:
37216
diff
changeset

42 
val ml = (thm_bind kind a i, " Isabelle." ^ a ^ " "); 
27389  43 
in (K ml, background') end)); 
44 

45 
val _ = thm_antiq "thm" (Attrib.thm >> single); 

46 
val _ = thm_antiq "thms" Attrib.thms; 

47 

48 

49 
(* adhoc goals *) 

50 

30266
970bf4f594c9
ML antiquotation @{lemma}: allow 'and' list, proper simultaneous typechecking;
wenzelm
parents:
29606
diff
changeset

51 
val and_ = Args.$$$ "and"; 
27809
a1e409db516b
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27521
diff
changeset

52 
val by = Args.$$$ "by"; 
30266
970bf4f594c9
ML antiquotation @{lemma}: allow 'and' list, proper simultaneous typechecking;
wenzelm
parents:
29606
diff
changeset

53 
val goal = Scan.unless (by  and_) Args.name; 
27389  54 

55 
val _ = ML_Context.add_antiq "lemma" 

33700  56 
(fn _ => Args.context  Args.mode "open"  
36950  57 
Scan.lift (Parse.and_list1 (Scan.repeat1 goal)  
30266
970bf4f594c9
ML antiquotation @{lemma}: allow 'and' list, proper simultaneous typechecking;
wenzelm
parents:
29606
diff
changeset

58 
(by  Method.parse  Scan.option Method.parse)) >> 
35019
1ec0a3ff229e
simplified interface for ML antiquotations, struct_name is always "Isabelle";
wenzelm
parents:
33700
diff
changeset

59 
(fn ((ctxt, is_open), (raw_propss, methods)) => fn background => 
27389  60 
let 
30266
970bf4f594c9
ML antiquotation @{lemma}: allow 'and' list, proper simultaneous typechecking;
wenzelm
parents:
29606
diff
changeset

61 
val propss = burrow (map (rpair []) o Syntax.read_props ctxt) raw_propss; 
27389  62 
val i = serial (); 
33700  63 
val prep_result = Goal.norm_result #> not is_open ? Thm.close_derivation; 
30266
970bf4f594c9
ML antiquotation @{lemma}: allow 'and' list, proper simultaneous typechecking;
wenzelm
parents:
29606
diff
changeset

64 
fun after_qed res goal_ctxt = 
970bf4f594c9
ML antiquotation @{lemma}: allow 'and' list, proper simultaneous typechecking;
wenzelm
parents:
29606
diff
changeset

65 
put_thms (i, map prep_result (ProofContext.export goal_ctxt ctxt (flat res))) goal_ctxt; 
27389  66 
val ctxt' = ctxt 
36323
655e2d74de3a
modernized naming conventions of main Isar proof elements;
wenzelm
parents:
35019
diff
changeset

67 
> Proof.theorem NONE after_qed propss 
27521
44081396d735
@{lemma}: allow terminal method, close derivation unless (open) mode is given;
wenzelm
parents:
27389
diff
changeset

68 
> Proof.global_terminal_proof methods; 
27389  69 
val (a, background') = background 
70 
> ML_Antiquote.variant "lemma" > put_thms (i, the_thms ctxt' i); 

30266
970bf4f594c9
ML antiquotation @{lemma}: allow 'and' list, proper simultaneous typechecking;
wenzelm
parents:
29606
diff
changeset

71 
val ml = 
41376
08240feb69c7
more robust ML antiquotations  allow original tokens without adjacent whitespace;
wenzelm
parents:
37216
diff
changeset

72 
(thm_bind (if length (flat propss) = 1 then "thm" else "thms") a i, 
08240feb69c7
more robust ML antiquotations  allow original tokens without adjacent whitespace;
wenzelm
parents:
37216
diff
changeset

73 
" Isabelle." ^ a ^ " "); 
27389  74 
in (K ml, background') end)); 
75 

76 
end; 

77 