author  wenzelm 
Wed, 19 Oct 2011 17:03:07 +0200  
changeset 45198  f579dab96734 
parent 43560  d1650e3720fd 
child 45592  8baa0b7f3f66 
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 

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 
(* adhoc goals *) 

52 

30266
970bf4f594c9
ML antiquotation @{lemma}: allow 'and' list, proper simultaneous typechecking;
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 