8 signature RES_AXIOMS = |
8 signature RES_AXIOMS = |
9 sig |
9 sig |
10 val cnf_axiom: thm -> thm list |
10 val cnf_axiom: thm -> thm list |
11 val meta_cnf_axiom: thm -> thm list |
11 val meta_cnf_axiom: thm -> thm list |
12 val pairname: thm -> string * thm |
12 val pairname: thm -> string * thm |
|
13 val multi_base_blacklist: string list |
13 val skolem_thm: thm -> thm list |
14 val skolem_thm: thm -> thm list |
14 val cnf_rules_pairs: (string * thm) list -> (thm * (string * int)) list |
15 val cnf_rules_pairs: (string * thm) list -> (thm * (string * int)) list |
15 val cnf_rules_of_ths: thm list -> thm list |
16 val cnf_rules_of_ths: thm list -> thm list |
16 val neg_clausify: thm list -> thm list |
17 val neg_clausify: thm list -> thm list |
17 val expand_defs_tac: thm -> tactic |
18 val expand_defs_tac: thm -> tactic |
447 else excessive_lambdas (t, max_lambda_nesting); |
448 else excessive_lambdas (t, max_lambda_nesting); |
448 |
449 |
449 fun too_complex t = |
450 fun too_complex t = |
450 Meson.too_many_clauses t orelse excessive_lambdas_fm [] t; |
451 Meson.too_many_clauses t orelse excessive_lambdas_fm [] t; |
451 |
452 |
|
453 val multi_base_blacklist = |
|
454 ["defs","select_defs","update_defs","induct","inducts","split","splits","split_asm"]; |
|
455 |
452 fun skolem_cache th thy = |
456 fun skolem_cache th thy = |
453 if PureThy.is_internal th orelse too_complex (prop_of th) then thy |
457 if PureThy.is_internal th orelse too_complex (prop_of th) then thy |
454 else #2 (skolem_cache_thm th thy); |
458 else #2 (skolem_cache_thm th thy); |
455 |
459 |
456 val skolem_cache_theorems_of = Symtab.fold (fold skolem_cache o snd) o #2 o PureThy.theorems_of; |
460 fun skolem_cache_list (a,ths) thy = |
|
461 if (Sign.base_name a) mem_string multi_base_blacklist then thy |
|
462 else fold skolem_cache ths thy; |
|
463 |
|
464 val skolem_cache_theorems_of = Symtab.fold skolem_cache_list o #2 o PureThy.theorems_of; |
457 fun skolem_cache_node thy = skolem_cache_theorems_of thy thy; |
465 fun skolem_cache_node thy = skolem_cache_theorems_of thy thy; |
458 fun skolem_cache_all thy = fold skolem_cache_theorems_of (thy :: Theory.ancestors_of thy) thy; |
466 fun skolem_cache_all thy = fold skolem_cache_theorems_of (thy :: Theory.ancestors_of thy) thy; |
459 |
467 |
460 (*The cache can be kept smaller by inspecting the prop of each thm. Can ignore all that are |
468 (*The cache can be kept smaller by inspecting the prop of each thm. Can ignore all that are |
461 lambda_free, but then the individual theory caches become much bigger.*) |
469 lambda_free, but then the individual theory caches become much bigger.*) |