src/HOL/Tools/ATP/res_clasimpset.ML
changeset 19156 bdaa8a980431
parent 19010 fef9e4881e83
child 19201 294448903a66
     1.1 --- a/src/HOL/Tools/ATP/res_clasimpset.ML	Tue Feb 28 11:09:50 2006 +0100
     1.2 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML	Tue Feb 28 11:10:51 2006 +0100
     1.3 @@ -6,8 +6,6 @@
     1.4  signature RES_CLASIMP = 
     1.5    sig
     1.6    val blacklist : string list ref (*Theorems forbidden in the output*)
     1.7 -  val theory_blacklist : string list ref (*entire blacklisted theories*)
     1.8 -  val relevant : int ref
     1.9    val use_simpset: bool ref
    1.10    val get_clasimp_lemmas : 
    1.11           Proof.context -> term list -> 
    1.12 @@ -182,13 +180,6 @@
    1.13     "Set.UnionI",
    1.14  *)
    1.15  
    1.16 -val theory_blacklist = ref
    1.17 -  ["Datatype_Universe.",    (*unnecessary in virtually all proofs*)
    1.18 -   "Equiv_Relations."]  
    1.19 -
    1.20 -
    1.21 -val relevant = ref 0;  (*Relevance filtering is off by default*)
    1.22 -
    1.23  (*The "name" of a theorem is its statement, if nothing else is available.*)
    1.24  val plain_string_of_thm =
    1.25      setmp show_question_marks false 
    1.26 @@ -215,12 +206,10 @@
    1.27        Polyhash.insert ht (x^"_iff2", ()); 
    1.28        Polyhash.insert ht (x^"_dest", ())); 
    1.29  
    1.30 -fun banned_theory s = exists (fn thy => String.isPrefix thy s) (!theory_blacklist);
    1.31 -
    1.32  fun make_banned_test xs = 
    1.33    let val ht = Polyhash.mkTable (Polyhash.hash_string, op =)
    1.34                                  (6000, HASH_STRING)
    1.35 -      fun banned s = isSome (Polyhash.peek ht s) orelse banned_theory s
    1.36 +      fun banned s = isSome (Polyhash.peek ht s)
    1.37    in  app (fn x => Polyhash.insert ht (x,())) (!blacklist);
    1.38        app (insert_suffixed_names ht) (!blacklist @ xs); 
    1.39        banned
    1.40 @@ -235,9 +224,7 @@
    1.41  fun make_unique ht xs = 
    1.42        (app (ignore o Polyhash.peekInsert ht) xs;  Polyhash.listItems ht);
    1.43  
    1.44 -(*Write out the claset and simpset rules of the supplied theory.
    1.45 -  FIXME: argument "goal" is a hack to allow relevance filtering.
    1.46 -  To reduce the number of clauses produced, set ResClasimp.relevant:=1*)
    1.47 +(*Write out the claset and simpset rules of the supplied theory.*)
    1.48  fun get_clasimp_lemmas ctxt goals = 
    1.49    let val claset_thms =
    1.50  	  map put_name_pair (ResAxioms.claset_rules_of_ctxt ctxt)
    1.51 @@ -249,10 +236,10 @@
    1.52        fun ok (a,_) = not (banned a)
    1.53        val claset_cls_thms = ResAxioms.clausify_rules_pairs (filter ok claset_thms)
    1.54        val simpset_cls_thms = ResAxioms.clausify_rules_pairs (filter ok simpset_thms)
    1.55 - 
    1.56        val cls_thms_list = make_unique (mk_clause_table 2200) 
    1.57                                        (List.concat (simpset_cls_thms@claset_cls_thms))
    1.58 -      val relevant_cls_thms_list = ReduceAxiomsN.relevance_filter (ProofContext.theory_of ctxt) cls_thms_list goals
    1.59 +      val relevant_cls_thms_list =
    1.60 +          ReduceAxiomsN.relevance_filter (ProofContext.theory_of ctxt) cls_thms_list goals
    1.61    in  (* create array of put clausename, number pairs into it *)
    1.62        (Array.fromList relevant_cls_thms_list, map #1 (relevant_cls_thms_list))
    1.63    end;