| author | haftmann |
| Tue, 24 Nov 2009 17:28:25 +0100 | |
| changeset 33955 | fff6f11b1f09 |
| parent 33519 | e31a85f92ce9 |
| permissions | -rw-r--r-- |
|
33308
cf62d1690d04
separate ResBlacklist, based on scalable persistent data -- avoids inefficient hashing later on;
wenzelm
parents:
diff
changeset
|
1 |
(* Title: HOL/Tools/res_blacklist.ML |
|
cf62d1690d04
separate ResBlacklist, based on scalable persistent data -- avoids inefficient hashing later on;
wenzelm
parents:
diff
changeset
|
2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
cf62d1690d04
separate ResBlacklist, based on scalable persistent data -- avoids inefficient hashing later on;
wenzelm
parents:
diff
changeset
|
3 |
Author: Makarius |
|
cf62d1690d04
separate ResBlacklist, based on scalable persistent data -- avoids inefficient hashing later on;
wenzelm
parents:
diff
changeset
|
4 |
|
|
cf62d1690d04
separate ResBlacklist, based on scalable persistent data -- avoids inefficient hashing later on;
wenzelm
parents:
diff
changeset
|
5 |
Theorems blacklisted to sledgehammer. These theorems typically |
|
cf62d1690d04
separate ResBlacklist, based on scalable persistent data -- avoids inefficient hashing later on;
wenzelm
parents:
diff
changeset
|
6 |
produce clauses that are prolific (match too many equality or |
|
cf62d1690d04
separate ResBlacklist, based on scalable persistent data -- avoids inefficient hashing later on;
wenzelm
parents:
diff
changeset
|
7 |
membership literals) and relate to seldom-used facts. Some duplicate |
|
cf62d1690d04
separate ResBlacklist, based on scalable persistent data -- avoids inefficient hashing later on;
wenzelm
parents:
diff
changeset
|
8 |
other rules. |
|
cf62d1690d04
separate ResBlacklist, based on scalable persistent data -- avoids inefficient hashing later on;
wenzelm
parents:
diff
changeset
|
9 |
*) |
|
cf62d1690d04
separate ResBlacklist, based on scalable persistent data -- avoids inefficient hashing later on;
wenzelm
parents:
diff
changeset
|
10 |
|
|
cf62d1690d04
separate ResBlacklist, based on scalable persistent data -- avoids inefficient hashing later on;
wenzelm
parents:
diff
changeset
|
11 |
signature RES_BLACKLIST = |
|
cf62d1690d04
separate ResBlacklist, based on scalable persistent data -- avoids inefficient hashing later on;
wenzelm
parents:
diff
changeset
|
12 |
sig |
|
cf62d1690d04
separate ResBlacklist, based on scalable persistent data -- avoids inefficient hashing later on;
wenzelm
parents:
diff
changeset
|
13 |
val setup: theory -> theory |
|
cf62d1690d04
separate ResBlacklist, based on scalable persistent data -- avoids inefficient hashing later on;
wenzelm
parents:
diff
changeset
|
14 |
val blacklisted: Proof.context -> thm -> bool |
|
cf62d1690d04
separate ResBlacklist, based on scalable persistent data -- avoids inefficient hashing later on;
wenzelm
parents:
diff
changeset
|
15 |
val add: attribute |
|
cf62d1690d04
separate ResBlacklist, based on scalable persistent data -- avoids inefficient hashing later on;
wenzelm
parents:
diff
changeset
|
16 |
val del: attribute |
|
cf62d1690d04
separate ResBlacklist, based on scalable persistent data -- avoids inefficient hashing later on;
wenzelm
parents:
diff
changeset
|
17 |
end; |
|
cf62d1690d04
separate ResBlacklist, based on scalable persistent data -- avoids inefficient hashing later on;
wenzelm
parents:
diff
changeset
|
18 |
|
| 33316 | 19 |
structure Res_Blacklist: RES_BLACKLIST = |
|
33308
cf62d1690d04
separate ResBlacklist, based on scalable persistent data -- avoids inefficient hashing later on;
wenzelm
parents:
diff
changeset
|
20 |
struct |
|
cf62d1690d04
separate ResBlacklist, based on scalable persistent data -- avoids inefficient hashing later on;
wenzelm
parents:
diff
changeset
|
21 |
|
| 33519 | 22 |
structure Data = Generic_Data |
|
33308
cf62d1690d04
separate ResBlacklist, based on scalable persistent data -- avoids inefficient hashing later on;
wenzelm
parents:
diff
changeset
|
23 |
( |
|
cf62d1690d04
separate ResBlacklist, based on scalable persistent data -- avoids inefficient hashing later on;
wenzelm
parents:
diff
changeset
|
24 |
type T = thm Termtab.table; |
|
cf62d1690d04
separate ResBlacklist, based on scalable persistent data -- avoids inefficient hashing later on;
wenzelm
parents:
diff
changeset
|
25 |
val empty = Termtab.empty; |
|
cf62d1690d04
separate ResBlacklist, based on scalable persistent data -- avoids inefficient hashing later on;
wenzelm
parents:
diff
changeset
|
26 |
val extend = I; |
| 33519 | 27 |
fun merge tabs = Termtab.merge (K true) tabs; |
|
33308
cf62d1690d04
separate ResBlacklist, based on scalable persistent data -- avoids inefficient hashing later on;
wenzelm
parents:
diff
changeset
|
28 |
); |
|
cf62d1690d04
separate ResBlacklist, based on scalable persistent data -- avoids inefficient hashing later on;
wenzelm
parents:
diff
changeset
|
29 |
|
|
cf62d1690d04
separate ResBlacklist, based on scalable persistent data -- avoids inefficient hashing later on;
wenzelm
parents:
diff
changeset
|
30 |
fun blacklisted ctxt th = |
|
cf62d1690d04
separate ResBlacklist, based on scalable persistent data -- avoids inefficient hashing later on;
wenzelm
parents:
diff
changeset
|
31 |
Termtab.defined (Data.get (Context.Proof ctxt)) (Thm.full_prop_of th); |
|
cf62d1690d04
separate ResBlacklist, based on scalable persistent data -- avoids inefficient hashing later on;
wenzelm
parents:
diff
changeset
|
32 |
|
|
cf62d1690d04
separate ResBlacklist, based on scalable persistent data -- avoids inefficient hashing later on;
wenzelm
parents:
diff
changeset
|
33 |
fun add_thm th = Data.map (Termtab.update (Thm.full_prop_of th, th)); |
|
cf62d1690d04
separate ResBlacklist, based on scalable persistent data -- avoids inefficient hashing later on;
wenzelm
parents:
diff
changeset
|
34 |
fun del_thm th = Data.map (Termtab.delete_safe (Thm.full_prop_of th)); |
|
cf62d1690d04
separate ResBlacklist, based on scalable persistent data -- avoids inefficient hashing later on;
wenzelm
parents:
diff
changeset
|
35 |
|
|
cf62d1690d04
separate ResBlacklist, based on scalable persistent data -- avoids inefficient hashing later on;
wenzelm
parents:
diff
changeset
|
36 |
val add = Thm.declaration_attribute add_thm; |
|
cf62d1690d04
separate ResBlacklist, based on scalable persistent data -- avoids inefficient hashing later on;
wenzelm
parents:
diff
changeset
|
37 |
val del = Thm.declaration_attribute del_thm; |
|
cf62d1690d04
separate ResBlacklist, based on scalable persistent data -- avoids inefficient hashing later on;
wenzelm
parents:
diff
changeset
|
38 |
|
|
cf62d1690d04
separate ResBlacklist, based on scalable persistent data -- avoids inefficient hashing later on;
wenzelm
parents:
diff
changeset
|
39 |
val setup = |
|
cf62d1690d04
separate ResBlacklist, based on scalable persistent data -- avoids inefficient hashing later on;
wenzelm
parents:
diff
changeset
|
40 |
Attrib.setup @{binding noatp} (Attrib.add_del add del) "sledgehammer blacklisting" #>
|
|
cf62d1690d04
separate ResBlacklist, based on scalable persistent data -- avoids inefficient hashing later on;
wenzelm
parents:
diff
changeset
|
41 |
PureThy.add_thms_dynamic (@{binding noatp}, map #2 o Termtab.dest o Data.get);
|
|
cf62d1690d04
separate ResBlacklist, based on scalable persistent data -- avoids inefficient hashing later on;
wenzelm
parents:
diff
changeset
|
42 |
|
|
cf62d1690d04
separate ResBlacklist, based on scalable persistent data -- avoids inefficient hashing later on;
wenzelm
parents:
diff
changeset
|
43 |
end; |