187 new_substs ([], substs) |
187 new_substs ([], substs) |
188 in |
188 in |
189 (added_substs, Instances (cfilter, ctab, minsets, substs)) |
189 (added_substs, Instances (cfilter, ctab, minsets, substs)) |
190 end |
190 end |
191 |
191 |
192 |
|
193 fun substs_of (Instances (_,_,_,substs)) = Substtab.keys substs |
192 fun substs_of (Instances (_,_,_,substs)) = Substtab.keys substs |
194 |
193 |
195 local |
194 local |
196 fun get_thm thmname = PureThy.get_thm (theory "Main") (Name thmname) |
195 fun get_thm thmname = PureThy.get_thm (theory "Main") (Name thmname) |
197 val eq_th = get_thm "HOL.eq_reflection" |
196 val eq_th = get_thm "HOL.eq_reflection" |
214 |
213 |
215 end |
214 end |
216 |
215 |
217 signature PCOMPUTE = |
216 signature PCOMPUTE = |
218 sig |
217 sig |
219 |
|
220 type pcomputer |
218 type pcomputer |
221 |
219 |
222 val make : Compute.machine -> theory -> thm list -> Linker.constant list -> pcomputer |
220 val make : Compute.machine -> theory -> thm list -> Linker.constant list -> pcomputer |
223 |
221 |
224 (* val add_thms : pcomputer -> thm list -> bool*) |
222 val add_instances : pcomputer -> Linker.constant list -> bool |
225 |
223 val add_instances' : pcomputer -> term list -> bool |
226 val add_instances : pcomputer -> Linker.constant list -> bool |
|
227 |
224 |
228 val rewrite : pcomputer -> cterm list -> thm list |
225 val rewrite : pcomputer -> cterm list -> thm list |
|
226 val simplify : pcomputer -> Compute.theorem -> thm |
|
227 |
|
228 val make_theorem : pcomputer -> thm -> string list -> Compute.theorem |
|
229 val instantiate : pcomputer -> (string * cterm) list -> Compute.theorem -> Compute.theorem |
|
230 val evaluate_prem : pcomputer -> int -> Compute.theorem -> Compute.theorem |
|
231 val modus_ponens : pcomputer -> int -> thm -> Compute.theorem -> Compute.theorem |
229 |
232 |
230 end |
233 end |
231 |
234 |
232 structure PCompute : PCOMPUTE = struct |
235 structure PCompute : PCOMPUTE = struct |
233 |
236 |
234 exception PCompute of string |
237 exception PCompute of string |
235 |
238 |
236 datatype theorem = MonoThm of thm | PolyThm of thm * Linker.instances * thm list |
239 datatype theorem = MonoThm of thm | PolyThm of thm * Linker.instances * thm list |
237 |
240 |
238 datatype pcomputer = PComputer of Compute.machine * theory_ref * Compute.computer ref * theorem list ref |
241 datatype pcomputer = PComputer of theory_ref * Compute.computer * theorem list ref |
239 |
242 |
240 (*fun collect_consts (Var x) = [] |
243 (*fun collect_consts (Var x) = [] |
241 | collect_consts (Bound _) = [] |
244 | collect_consts (Bound _) = [] |
242 | collect_consts (a $ b) = (collect_consts a)@(collect_consts b) |
245 | collect_consts (a $ b) = (collect_consts a)@(collect_consts b) |
243 | collect_consts (Abs (_, _, body)) = collect_consts body |
246 | collect_consts (Abs (_, _, body)) = collect_consts body |
244 | collect_consts t = [Linker.constant_of t]*) |
247 | collect_consts t = [Linker.constant_of t]*) |
245 |
248 |
246 fun collect_consts_of_thm th = |
249 fun computer_of (PComputer (_,computer,_)) = computer |
|
250 |
|
251 fun collect_consts_of_thm th = |
247 let |
252 let |
248 val th = prop_of th |
253 val th = prop_of th |
249 val (prems, th) = (Logic.strip_imp_prems th, Logic.strip_imp_concl th) |
254 val (prems, th) = (Logic.strip_imp_prems th, Logic.strip_imp_concl th) |
250 val (left, right) = Logic.dest_equals th |
255 val (left, right) = Logic.dest_equals th |
251 in |
256 in |
283 fun add (MonoThm th) ths = th::ths |
288 fun add (MonoThm th) ths = th::ths |
284 | add (PolyThm (_, _, ths')) ths = ths'@ths |
289 | add (PolyThm (_, _, ths')) ths = ths'@ths |
285 val ths = fold_rev add ths [] |
290 val ths = fold_rev add ths [] |
286 in |
291 in |
287 Compute.make machine thy ths |
292 Compute.make machine thy ths |
|
293 end |
|
294 |
|
295 fun update_computer computer ths = |
|
296 let |
|
297 fun add (MonoThm th) ths = th::ths |
|
298 | add (PolyThm (_, _, ths')) ths = ths'@ths |
|
299 val ths = fold_rev add ths [] |
|
300 in |
|
301 Compute.update computer ths |
288 end |
302 end |
289 |
303 |
290 fun conv_subst thy (subst : Type.tyenv) = |
304 fun conv_subst thy (subst : Type.tyenv) = |
291 map (fn (iname, (sort, ty)) => (ctyp_of thy (TVar (iname, sort)), ctyp_of thy ty)) (Vartab.dest subst) |
305 map (fn (iname, (sort, ty)) => (ctyp_of thy (TVar (iname, sort)), ctyp_of thy ty)) (Vartab.dest subst) |
292 |
306 |
354 val _ = map update ths |
368 val _ = map update ths |
355 in |
369 in |
356 map snd (Inttab.dest (!thstab)) |
370 map snd (Inttab.dest (!thstab)) |
357 end |
371 end |
358 |
372 |
359 |
|
360 fun make machine thy ths cs = |
373 fun make machine thy ths cs = |
361 let |
374 let |
362 val ths = remove_duplicates ths |
375 val ths = remove_duplicates ths |
363 val (monocs, ths) = fold_rev (fn th => |
376 val (monocs, ths) = fold_rev (fn th => |
364 fn (monocs, ths) => |
377 fn (monocs, ths) => |
365 let val (m, t) = create_theorem th in |
378 let val (m, t) = create_theorem th in |
366 (m@monocs, t::ths) |
379 (m@monocs, t::ths) |
367 end) |
380 end) |
368 ths (cs, []) |
381 ths (cs, []) |
369 val (_, ths) = add_monos thy monocs ths |
382 val (_, ths) = add_monos thy monocs ths |
370 val computer = create_computer machine thy ths |
383 val computer = create_computer machine thy ths |
371 in |
384 in |
372 PComputer (machine, Theory.check_thy thy, ref computer, ref ths) |
385 PComputer (Theory.check_thy thy, computer, ref ths) |
373 end |
386 end |
374 |
387 |
375 fun add_instances (PComputer (machine, thyref, rcomputer, rths)) cs = |
388 fun add_instances (PComputer (thyref, computer, rths)) cs = |
376 let |
389 let |
377 val thy = Theory.deref thyref |
390 val thy = Theory.deref thyref |
378 val (changed, ths) = add_monos thy cs (!rths) |
391 val (changed, ths) = add_monos thy cs (!rths) |
379 in |
392 in |
380 if changed then |
393 if changed then |
381 (rcomputer := create_computer machine thy ths; |
394 (update_computer computer ths; |
382 rths := ths; |
395 rths := ths; |
383 true) |
396 true) |
384 else |
397 else |
385 false |
398 false |
386 end |
399 |
387 |
400 end |
388 fun rewrite (pc as PComputer (_, _, rcomputer, _)) cts = |
401 |
389 let |
402 fun add_instances' pc ts = add_instances pc (Linker.collect_consts ts) |
390 val _ = map (fn ct => add_instances pc (Linker.collect_consts [term_of ct])) cts |
403 |
391 in |
404 fun rewrite pc cts = |
392 map (fn ct => Compute.rewrite (!rcomputer) ct) cts |
405 let |
393 end |
406 val _ = add_instances' pc (map term_of cts) |
394 |
407 val computer = (computer_of pc) |
395 end |
408 in |
|
409 map (fn ct => Compute.rewrite computer ct) cts |
|
410 end |
|
411 |
|
412 fun simplify pc th = Compute.simplify (computer_of pc) th |
|
413 |
|
414 fun make_theorem pc th vars = |
|
415 let |
|
416 val _ = add_instances' pc [prop_of th] |
|
417 |
|
418 in |
|
419 Compute.make_theorem (computer_of pc) th vars |
|
420 end |
|
421 |
|
422 fun instantiate pc insts th = |
|
423 let |
|
424 val _ = add_instances' pc (map (term_of o snd) insts) |
|
425 in |
|
426 Compute.instantiate (computer_of pc) insts th |
|
427 end |
|
428 |
|
429 fun evaluate_prem pc prem_no th = Compute.evaluate_prem (computer_of pc) prem_no th |
|
430 |
|
431 fun modus_ponens pc prem_no th' th = |
|
432 let |
|
433 val _ = add_instances' pc [prop_of th'] |
|
434 in |
|
435 Compute.modus_ponens (computer_of pc) prem_no th' th |
|
436 end |
|
437 |
|
438 |
|
439 end |