equal
deleted
inserted
replaced
4 *) |
4 *) |
5 |
5 |
6 signature RES_CLASIMP = |
6 signature RES_CLASIMP = |
7 sig |
7 sig |
8 val blacklist : string list ref (*Theorems forbidden in the output*) |
8 val blacklist : string list ref (*Theorems forbidden in the output*) |
|
9 val whitelist : thm list ref (*Theorems required in the output*) |
9 val use_simpset: bool ref |
10 val use_simpset: bool ref |
10 val get_clasimp_atp_lemmas : |
11 val get_clasimp_atp_lemmas : |
11 Proof.context -> |
12 Proof.context -> |
12 Term.term list -> |
13 Term.term list -> |
13 (string * Thm.thm) list -> |
14 (string * Thm.thm) list -> |
16 |
17 |
17 structure ResClasimp : RES_CLASIMP = |
18 structure ResClasimp : RES_CLASIMP = |
18 struct |
19 struct |
19 val use_simpset = ref false; (*Performance is much better without simprules*) |
20 val use_simpset = ref false; (*Performance is much better without simprules*) |
20 |
21 |
|
22 (*The rule subsetI is frequently omitted by the relevance filter.*) |
|
23 val whitelist = ref [subsetI]; |
21 |
24 |
22 (*In general, these produce clauses that are prolific (match too many equality or |
25 (*In general, these produce clauses that are prolific (match too many equality or |
23 membership literals) and relate to seldom-used facts. Some duplicate other rules. |
26 membership literals) and relate to seldom-used facts. Some duplicate other rules. |
24 FIXME: this blacklist needs to be maintained using theory data and added to using |
27 FIXME: this blacklist needs to be maintained using theory data and added to using |
25 an attribute.*) |
28 an attribute.*) |
283 val atpset_thms = |
286 val atpset_thms = |
284 if use_atpset then |
287 if use_atpset then |
285 map put_name_pair (ResAxioms.atpset_rules_of_ctxt ctxt) |
288 map put_name_pair (ResAxioms.atpset_rules_of_ctxt ctxt) |
286 else [] |
289 else [] |
287 val _ = warning_thms atpset_thms |
290 val _ = warning_thms atpset_thms |
288 val user_rules = map put_name_pair user_thms |
291 val user_rules = |
|
292 case user_thms of (*use whitelist if there are no user-supplied rules*) |
|
293 [] => map (put_name_pair o ResAxioms.pairname) (!whitelist) |
|
294 | _ => map put_name_pair user_thms |
289 val banned = make_banned_test (map #1 (user_rules@atpset_thms@claset_thms@simpset_thms)) |
295 val banned = make_banned_test (map #1 (user_rules@atpset_thms@claset_thms@simpset_thms)) |
290 fun ok (a,_) = not (banned a) |
296 fun ok (a,_) = not (banned a) |
291 val claset_cls_tms = |
297 val claset_cls_tms = |
292 if run_filter then ResAxioms.clausify_rules_pairs_abs (filter ok claset_thms) |
298 if run_filter then ResAxioms.clausify_rules_pairs_abs (filter ok claset_thms) |
293 else ResAxioms.clausify_rules_pairs_abs claset_thms |
299 else ResAxioms.clausify_rules_pairs_abs claset_thms |