1 (* Title: Pure/Thy/thm_database.ML |
1 (* Title: Pure/Thy/thm_database.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Carsten Clasohm and Tobias Nipkow |
3 Author: Carsten Clasohm and Tobias Nipkow and Markus Wenzel, TU Muenchen |
4 Copyright 1995 TU Muenchen |
4 |
|
5 User level interface to thm database (see also Pure/pure_thy.ML). |
5 *) |
6 *) |
6 |
7 |
7 datatype thm_db = |
|
8 ThmDB of {count: int, |
|
9 thy_idx: (Sign.sg * (string list * int list)) list, |
|
10 const_idx: ((int * (string * thm)) list) Symtab.table}; |
|
11 (*count: number of theorems in database (used as unique ID for next thm) |
|
12 thy_idx: constants and IDs of theorems |
|
13 indexed by the theory's signature they belong to |
|
14 const_idx: named theorems tagged by numbers and |
|
15 indexed by the constants they contain*) |
|
16 |
|
17 signature THM_DATABASE = |
8 signature THM_DATABASE = |
18 sig |
9 sig |
19 val thm_db: thm_db ref |
10 val store_thm: string * thm -> thm |
20 val store_thm_db: string * thm -> thm |
11 val qed_thm: thm option ref |
21 val delete_thm_db: theory -> unit |
12 val bind_thm: string * thm -> unit |
|
13 val qed: string -> unit |
|
14 val qed_goal: string -> theory -> string -> (thm list -> tactic list) -> unit |
|
15 val qed_goalw: string -> theory -> thm list -> string -> (thm list -> tactic list) -> unit |
|
16 (*these peek at the proof state!*) |
22 val thms_containing: string list -> (string * thm) list |
17 val thms_containing: string list -> (string * thm) list |
23 val findI: int -> (string * thm)list |
18 val findI: int -> (string * thm) list |
24 val findEs: int -> (string * thm)list |
19 val findEs: int -> (string * thm) list |
25 val findE: int -> int -> (string * thm)list |
20 val findE: int -> int -> (string * thm) list |
26 |
21 end; |
27 val store_thm : string * thm -> thm |
|
28 val bind_thm : string * thm -> unit |
|
29 val qed : string -> unit |
|
30 val qed_thm : thm ref |
|
31 val qed_goal : string -> theory -> string |
|
32 -> (thm list -> tactic list) -> unit |
|
33 val qed_goalw : string -> theory -> thm list -> string |
|
34 -> (thm list -> tactic list) -> unit |
|
35 val get_thm : theory -> string -> thm |
|
36 val thms_of : theory -> (string * thm) list |
|
37 val delete_thms : string -> unit |
|
38 |
|
39 val print_theory : theory -> unit |
|
40 end; |
|
41 |
22 |
42 structure ThmDatabase: THM_DATABASE = |
23 structure ThmDatabase: THM_DATABASE = |
43 struct |
24 struct |
44 |
25 |
45 open ThyInfo BrowserInfo; |
26 (** store theorems **) |
46 |
27 |
47 (*** ignore and top_const could be turned into functor-parameters, but are |
28 (* store in theory and generate HTML *) |
48 currently identical for all object logics ***) |
|
49 |
29 |
50 (* Constants not to be used for theorem indexing *) |
30 fun store_thm (name, thm) = |
51 val ignore = ["Trueprop", "all", "==>", "=="]; |
31 let val thm' = PureThy.smart_store_thm (name, thm) in |
52 |
32 BrowserInfo.thm_to_html thm' name; thm' |
53 (* top_const: main constant, ignoring Trueprop *) |
|
54 fun top_const (_ $ t) = (case head_of t of Const(c,_) => Some c |
|
55 | _ => None) |
|
56 | top_const _ = None; |
|
57 |
|
58 (*Symtab which associates a constant with a list of theorems that contain the |
|
59 constant (theorems are tagged with numbers)*) |
|
60 val thm_db = ref (ThmDB |
|
61 {count = 0, thy_idx = []:(Sign.sg * (string list * int list)) list, |
|
62 const_idx = Symtab.make ([]:(string * ((int * (string * thm)) list)) list)}); |
|
63 |
|
64 (*List all relevant constants a term contains*) |
|
65 fun list_consts t = |
|
66 let fun consts (Const (c, _)) = if c mem ignore then [] else [c] |
|
67 | consts (Free _) = [] |
|
68 | consts (Var _) = [] |
|
69 | consts (Bound _) = [] |
|
70 | consts (Abs (_, _, t)) = consts t |
|
71 | consts (t1$t2) = (consts t1) union (consts t2); |
|
72 in distinct (consts t) end; |
|
73 |
|
74 (*Store a theorem in database*) |
|
75 fun store_thm_db (named_thm as (name, thm)) = |
|
76 let val {prop, hyps, sign, ...} = rep_thm thm; |
|
77 |
|
78 val consts = distinct (flat (map list_consts (prop :: hyps))); |
|
79 |
|
80 val ThmDB {count, thy_idx, const_idx} = !thm_db; |
|
81 |
|
82 fun update_thys [] = [(sign, (consts, [count]))] |
|
83 | update_thys ((thy as (thy_sign, (thy_consts, thy_nums))) :: ts) = |
|
84 if Sign.eq_sg (sign, thy_sign) then |
|
85 (thy_sign, (thy_consts union consts, count :: thy_nums)) :: ts |
|
86 else thy :: update_thys ts; |
|
87 |
|
88 val tagged_thm = (count, named_thm); |
|
89 |
|
90 fun update_db _ [] result = Some result |
|
91 | update_db checked (c :: cs) result = |
|
92 let |
|
93 val old_thms = Symtab.lookup_multi (result, c); |
|
94 |
|
95 val duplicate = |
|
96 if checked then false |
|
97 else case find_first (fn (_, (n, _)) => n = name) old_thms of |
|
98 Some (_, (_, t)) => eq_thm (t, thm) |
|
99 | None => false |
|
100 in if duplicate then None |
|
101 else update_db true |
|
102 cs (Symtab.update ((c, tagged_thm :: old_thms), result)) |
|
103 end; |
|
104 |
|
105 val const_idx' = update_db false consts const_idx; |
|
106 in if consts = [] then warning ("Theorem " ^ name ^ |
|
107 " cannot be stored in ThmDB\n\t because it \ |
|
108 \contains no or only ignored constants.") |
|
109 else if is_some const_idx' then |
|
110 thm_db := ThmDB {count = count+1, thy_idx = update_thys thy_idx, |
|
111 const_idx = the const_idx'} |
|
112 else (); |
|
113 thm |
|
114 end; |
33 end; |
115 |
34 |
116 (*Remove all theorems with given signature from database*) |
|
117 fun delete_thm_db thy = |
|
118 let |
|
119 val sign = sign_of thy; |
|
120 |
35 |
121 val ThmDB {count, thy_idx, const_idx} = !thm_db; |
36 (* store on ML toplevel *) |
122 |
37 |
123 (*Remove theory from thy_idx and get the data associated with it*) |
38 val qed_thm: thm option ref = ref None; |
124 fun update_thys [] result = (result, [], []) |
|
125 | update_thys ((thy as (thy_sign, (thy_consts, thy_nums))) :: ts) |
|
126 result = |
|
127 if Sign.eq_sg (sign, thy_sign) then |
|
128 (result @ ts, thy_consts, thy_nums) |
|
129 else update_thys ts (thy :: result); |
|
130 |
39 |
131 val (thy_idx', thy_consts, thy_nums) = update_thys thy_idx []; |
40 val ml_reserved = |
|
41 ["abstype", "and", "andalso", "as", "case", "do", "datatype", "else", |
|
42 "end", "exception", "fn", "fun", "handle", "if", "in", "infix", |
|
43 "infixr", "let", "local", "nonfix", "of", "op", "open", "orelse", |
|
44 "raise", "rec", "then", "type", "val", "with", "withtype", "while", |
|
45 "eqtype", "functor", "include", "sharing", "sig", "signature", |
|
46 "struct", "structure", "where"]; |
132 |
47 |
133 (*Remove all theorems belonging to a theory*) |
48 fun is_ml_identifier name = |
134 fun update_db [] result = result |
49 Syntax.is_identifier name andalso not (name mem ml_reserved); |
135 | update_db (c :: cs) result = |
50 |
136 let val thms' = filter_out (fn (num, _) => num mem thy_nums) |
51 fun ml_store_thm (name, thm) = |
137 (Symtab.lookup_multi (result, c)); |
52 let val thm' = store_thm (name, thm) in |
138 in update_db cs (Symtab.update ((c, thms'), result)) end; |
53 if is_ml_identifier name then |
139 in thm_db := ThmDB {count = count, thy_idx = thy_idx', |
54 (qed_thm := Some thm'; |
140 const_idx = update_db thy_consts const_idx} |
55 use_strings ["val " ^ name ^ " = the (! ThmDatabase.qed_thm);"]) |
|
56 else warning ("Cannot bind thm " ^ quote name ^ " as ML value") |
141 end; |
57 end; |
142 |
58 |
143 (*Intersection of two theorem lists with descending tags*) |
59 fun bind_thm (name, thm) = ml_store_thm (name, standard thm); |
144 infix desc_inter; |
60 fun qed name = ml_store_thm (name, result ()); |
145 fun ([] : (int*'a) list) desc_inter (ys : (int*'a) list) = [] |
61 fun qed_goal name thy goal tacsf = ml_store_thm (name, prove_goal thy goal tacsf); |
146 | xs desc_inter [] = [] |
62 fun qed_goalw name thy rews goal tacsf = ml_store_thm (name, prove_goalw thy rews goal tacsf); |
147 | (xss as ((x as (xi,_)) :: xs)) desc_inter (yss as ((yi,_) :: ys)) = |
|
148 if xi = yi then x :: (xs desc_inter ys) |
|
149 else if xi > yi then xs desc_inter yss |
|
150 else xss desc_inter ys; |
|
151 |
63 |
152 (*Get all theorems from database that contain a list of constants*) |
|
153 fun thms_containing constants = |
|
154 let fun collect [] _ result = map snd result |
|
155 | collect (c :: cs) first result = |
|
156 let val ThmDB {const_idx, ...} = !thm_db; |
|
157 |
64 |
158 val new_thms = Symtab.lookup_multi (const_idx, c); |
|
159 in collect cs false (if first then new_thms |
|
160 else (result desc_inter new_thms)) |
|
161 end; |
|
162 |
65 |
163 val look_for = constants \\ ignore; |
66 (** retrieve theorems **) (*peek at current proof state*) |
164 in if null look_for then |
67 |
165 error ("No or only ignored constants were specified for theorem \ |
68 (*get theorems that contain *all* of given constants*) |
166 \database search:\n " ^ commas (map quote ignore)) |
69 fun thms_containing raw_consts = |
167 else (); |
70 let |
168 collect look_for true [] end; |
71 val sign = sign_of_thm (topthm ()); |
|
72 val consts = map (Sign.intern_const sign) raw_consts; |
|
73 val thy = ThyInfo.theory_of_sign sign; |
|
74 in |
|
75 PureThy.thms_containing thy (consts \\ PureThy.ignored_consts) |
|
76 end; |
|
77 |
|
78 |
|
79 (*top_const: main constant, ignoring Trueprop*) |
|
80 fun top_const (_ $ t) = (case head_of t of Const (c, _) => Some c | _ => None) |
|
81 | top_const _ = None; |
169 |
82 |
170 val intro_const = top_const o concl_of; |
83 val intro_const = top_const o concl_of; |
171 |
84 |
172 fun elim_const thm = case prems_of thm of [] => None | p::_ => top_const(p); |
85 fun elim_const thm = case prems_of thm of [] => None | p::_ => top_const p; |
173 |
86 |
174 (* In case faster access is necessary, the thm db should provide special |
87 (* In case faster access is necessary, the thm db should provide special |
175 functions |
88 functions |
176 |
89 |
177 index_intros, index_elims: string -> (string * thm) list |
90 index_intros, index_elims: string -> (string * thm) list |
263 fun findE i j = |
176 fun findE i j = |
264 let val sign = #sign(rep_thm(topthm())) |
177 let val sign = #sign(rep_thm(topthm())) |
265 in find_elims sign (nth_elem(j-1, prems_of_goal i)) end; |
178 in find_elims sign (nth_elem(j-1, prems_of_goal i)) end; |
266 |
179 |
267 |
180 |
268 (*** Store and retrieve theorems ***) |
|
269 |
|
270 (** Store theorems **) |
|
271 |
|
272 (*Store a theorem in the thy_info of its theory, |
|
273 and in the theory's HTML file*) |
|
274 fun store_thm (name, thm) = |
|
275 let |
|
276 val (thy_name, {path, children, parents, thy_time, ml_time, |
|
277 theory, thms, methods, data}) = |
|
278 thyinfo_of_sign (#sign (rep_thm thm)) |
|
279 |
|
280 val (thms', duplicate) = (Symtab.update_new ((name, thm), thms), false) |
|
281 handle Symtab.DUPLICATE s => |
|
282 (if eq_thm (the (Symtab.lookup (thms, name)), thm) then |
|
283 (warning ("Theory database already contains copy of\ |
|
284 \ theorem " ^ quote name); |
|
285 (thms, true)) |
|
286 else error ("Duplicate theorem name " ^ quote s |
|
287 ^ " used in theory database")); |
|
288 |
|
289 (*Label this theorem*) |
|
290 val thm' = Thm.name_thm (name, thm) |
|
291 in |
|
292 loaded_thys := Symtab.update |
|
293 ((thy_name, {path = path, children = children, parents = parents, |
|
294 thy_time = thy_time, ml_time = ml_time, |
|
295 theory = theory, thms = thms', |
|
296 methods = methods, data = data}), |
|
297 !loaded_thys); |
|
298 thm_to_html thm name; |
|
299 if duplicate then thm' else store_thm_db (name, thm') |
|
300 end; |
|
301 |
|
302 |
|
303 (*Store result of proof in loaded_thys and as ML value*) |
|
304 |
|
305 val qed_thm = ref ProtoPure.flexpair_def(*dummy*); |
|
306 |
|
307 |
|
308 fun bind_thm (name, thm) = |
|
309 (qed_thm := store_thm (name, (standard thm)); |
|
310 use_strings ["val " ^ name ^ " = !qed_thm;"]); |
|
311 |
|
312 |
|
313 fun qed name = |
|
314 (qed_thm := store_thm (name, result ()); |
|
315 use_strings ["val " ^ name ^ " = !qed_thm;"]); |
|
316 |
|
317 |
|
318 fun qed_goal name thy agoal tacsf = |
|
319 (qed_thm := store_thm (name, prove_goal thy agoal tacsf); |
|
320 use_strings ["val " ^ name ^ " = !qed_thm;"]); |
|
321 |
|
322 |
|
323 fun qed_goalw name thy rths agoal tacsf = |
|
324 (qed_thm := store_thm (name, prove_goalw thy rths agoal tacsf); |
|
325 use_strings ["val " ^ name ^ " = !qed_thm;"]); |
|
326 |
|
327 |
|
328 (** Retrieve theorems **) |
|
329 |
|
330 (*Get all theorems belonging to a given theory*) |
|
331 fun thmtab_of_thy thy = |
|
332 let val (_, {thms, ...}) = thyinfo_of_sign (sign_of thy); |
|
333 in thms end; |
|
334 |
|
335 |
|
336 fun thmtab_of_name name = |
|
337 let val {thms, ...} = the (get_thyinfo name); |
|
338 in thms end; |
|
339 |
|
340 |
|
341 (*Get a stored theorem specified by theory and name. *) |
|
342 fun get_thm thy name = |
|
343 let fun get [] [] searched = |
|
344 raise THEORY ("get_thm: no theorem " ^ quote name, [thy]) |
|
345 | get [] ng searched = |
|
346 get (ng \\ searched) [] searched |
|
347 | get (t::ts) ng searched = |
|
348 (case Symtab.lookup (thmtab_of_name t, name) of |
|
349 Some thm => thm |
|
350 | None => get ts (ng union (parents_of_name t)) (t::searched)); |
|
351 |
|
352 val (tname, _) = thyinfo_of_sign (sign_of thy); |
|
353 in get [tname] [] [] end; |
|
354 |
|
355 |
|
356 (*Get stored theorems of a theory (original derivations) *) |
|
357 val thms_of = Symtab.dest o thmtab_of_thy; |
|
358 |
|
359 |
|
360 (*Remove theorems associated with a theory from theory and theorem database*) |
|
361 fun delete_thms tname = |
|
362 let |
|
363 val tinfo = case get_thyinfo tname of |
|
364 Some ({path, children, parents, thy_time, ml_time, theory, |
|
365 methods, data, ...}) => |
|
366 {path = path, children = children, parents = parents, |
|
367 thy_time = thy_time, ml_time = ml_time, |
|
368 theory = theory, thms = Symtab.null, |
|
369 methods = methods, data = data} |
|
370 | None => error ("Theory " ^ tname ^ " not stored by loader"); |
|
371 |
|
372 val {theory, ...} = tinfo; |
|
373 in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys); |
|
374 case theory of |
|
375 Some t => delete_thm_db t |
|
376 | None => () |
|
377 end; |
|
378 |
|
379 |
|
380 (*** Print theory ***) |
|
381 |
|
382 fun print_thms thy = |
|
383 let |
|
384 val thms = thms_of thy; |
|
385 fun prt_thm (s, th) = Pretty.block [Pretty.str (s ^ ":"), Pretty.brk 1, |
|
386 Pretty.quote (pretty_thm th)]; |
|
387 in |
|
388 Pretty.writeln (Pretty.big_list "stored theorems:" (map prt_thm thms)) |
|
389 end; |
|
390 |
|
391 |
|
392 fun print_theory thy = (Display.print_theory thy; print_thms thy); |
|
393 |
|
394 end; |
181 end; |