src/HOL/Tools/ATP/res_clasimpset.ML
changeset 19317 3d383e78b6f4
parent 19209 27b91724809f
child 19320 d3688974a063
     1.1 --- a/src/HOL/Tools/ATP/res_clasimpset.ML	Wed Mar 22 12:32:44 2006 +0100
     1.2 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML	Wed Mar 22 12:33:44 2006 +0100
     1.3 @@ -6,6 +6,7 @@
     1.4  signature RES_CLASIMP = 
     1.5    sig
     1.6    val blacklist : string list ref (*Theorems forbidden in the output*)
     1.7 +  val whitelist : thm list ref    (*Theorems required in the output*)
     1.8    val use_simpset: bool ref
     1.9    val get_clasimp_atp_lemmas : 
    1.10        Proof.context ->
    1.11 @@ -18,6 +19,8 @@
    1.12  struct
    1.13  val use_simpset = ref false;   (*Performance is much better without simprules*)
    1.14  
    1.15 +(*The rule subsetI is frequently omitted by the relevance filter.*)
    1.16 +val whitelist = ref [subsetI]; 
    1.17  
    1.18  (*In general, these produce clauses that are prolific (match too many equality or
    1.19    membership literals) and relate to seldom-used facts. Some duplicate other rules.
    1.20 @@ -285,7 +288,10 @@
    1.21  	      map put_name_pair (ResAxioms.atpset_rules_of_ctxt ctxt)
    1.22  	  else []
    1.23        val _ = warning_thms atpset_thms
    1.24 -      val user_rules = map put_name_pair user_thms
    1.25 +      val user_rules = 
    1.26 +	  case user_thms of  (*use whitelist if there are no user-supplied rules*)
    1.27 +	       [] => map (put_name_pair o ResAxioms.pairname) (!whitelist)
    1.28 +	     | _  => map put_name_pair user_thms
    1.29        val banned = make_banned_test (map #1 (user_rules@atpset_thms@claset_thms@simpset_thms))
    1.30        fun ok (a,_) = not (banned a) 	   
    1.31        val claset_cls_tms =