author | wenzelm |
Sat, 23 Apr 2005 19:51:54 +0200 | |
changeset 15836 | b805d85909c7 |
parent 15801 | d2f5ca3c048d |
child 17170 | cbe14eb12729 |
permissions | -rw-r--r-- |
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
1 |
(* Title: Pure/Thy/thm_database.ML |
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
2 |
ID: $Id$ |
11895 | 3 |
Author: Markus Wenzel, TU Muenchen |
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
4 |
|
15836 | 5 |
Theorem database ML interface. |
4023 | 6 |
*) |
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset
|
7 |
|
6204 | 8 |
signature BASIC_THM_DATABASE = |
4023 | 9 |
sig |
10 |
val store_thm: string * thm -> thm |
|
7410 | 11 |
val store_thms: string * thm list -> thm list |
4023 | 12 |
end; |
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
13 |
|
6204 | 14 |
signature THM_DATABASE = |
15 |
sig |
|
16 |
include BASIC_THM_DATABASE |
|
7410 | 17 |
val qed_thms: thm list ref |
6204 | 18 |
val ml_store_thm: string * thm -> unit |
7410 | 19 |
val ml_store_thms: string * thm list -> unit |
14680 | 20 |
val ml_reserved: string list |
6204 | 21 |
val is_ml_identifier: string -> bool |
22 |
end; |
|
23 |
||
3627 | 24 |
structure ThmDatabase: THM_DATABASE = |
1221 | 25 |
struct |
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
26 |
|
4023 | 27 |
(** store theorems **) |
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
28 |
|
13279
8a722689a1c9
removed thms_containing (see pure_thy.ML and proof_context.ML);
wenzelm
parents:
11895
diff
changeset
|
29 |
(* store in theory and perform presentation *) |
1136
3910c96551d1
fixed bug in thms_containing; changed error/warning messages;
clasohm
parents:
1134
diff
changeset
|
30 |
|
4023 | 31 |
fun store_thm (name, thm) = |
7410 | 32 |
let val thm' = hd (PureThy.smart_store_thms (name, [thm])) |
6327 | 33 |
in Present.theorem name thm'; thm' end; |
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
34 |
|
7410 | 35 |
fun store_thms (name, thms) = |
36 |
let val thms' = PureThy.smart_store_thms (name, thms) |
|
37 |
in Present.theorems name thms'; thms' end; |
|
38 |
||
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset
|
39 |
|
4023 | 40 |
(* store on ML toplevel *) |
41 |
||
7410 | 42 |
val qed_thms: thm list ref = ref []; |
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset
|
43 |
|
4023 | 44 |
val ml_reserved = |
45 |
["abstype", "and", "andalso", "as", "case", "do", "datatype", "else", |
|
46 |
"end", "exception", "fn", "fun", "handle", "if", "in", "infix", |
|
47 |
"infixr", "let", "local", "nonfix", "of", "op", "open", "orelse", |
|
48 |
"raise", "rec", "then", "type", "val", "with", "withtype", "while", |
|
49 |
"eqtype", "functor", "include", "sharing", "sig", "signature", |
|
50 |
"struct", "structure", "where"]; |
|
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset
|
51 |
|
4023 | 52 |
fun is_ml_identifier name = |
14680 | 53 |
not (name mem_string ml_reserved) andalso Syntax.is_ascii_identifier name; |
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset
|
54 |
|
7410 | 55 |
fun warn_ml name = |
56 |
if is_ml_identifier name then false |
|
7573 | 57 |
else if name = "" then true |
7410 | 58 |
else (warning ("Cannot bind theorem(s) " ^ quote name ^ " as ML value"); true); |
59 |
||
10914 | 60 |
val use_text_verbose = use_text Context.ml_output true; |
7854 | 61 |
|
4023 | 62 |
fun ml_store_thm (name, thm) = |
63 |
let val thm' = store_thm (name, thm) in |
|
7410 | 64 |
if warn_ml name then () |
13279
8a722689a1c9
removed thms_containing (see pure_thy.ML and proof_context.ML);
wenzelm
parents:
11895
diff
changeset
|
65 |
else (qed_thms := [thm']; |
8a722689a1c9
removed thms_containing (see pure_thy.ML and proof_context.ML);
wenzelm
parents:
11895
diff
changeset
|
66 |
use_text_verbose ("val " ^ name ^ " = hd (! ThmDatabase.qed_thms);")) |
7410 | 67 |
end; |
68 |
||
69 |
fun ml_store_thms (name, thms) = |
|
70 |
let val thms' = store_thms (name, thms) in |
|
71 |
if warn_ml name then () |
|
7854 | 72 |
else (qed_thms := thms'; use_text_verbose ("val " ^ name ^ " = ! ThmDatabase.qed_thms;")) |
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset
|
73 |
end; |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1245
diff
changeset
|
74 |
|
4023 | 75 |
|
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
diff
changeset
|
76 |
end; |
6204 | 77 |
|
78 |
structure BasicThmDatabase: BASIC_THM_DATABASE = ThmDatabase; |
|
79 |
open BasicThmDatabase; |