src/HOL/Tools/res_atp.ML
changeset 33022 c95102496490
parent 32994 ccc07fbbfefd
child 33035 15eab423e573
     1.1 --- a/src/HOL/Tools/res_atp.ML	Tue Oct 20 15:03:17 2009 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Tue Oct 20 15:02:48 2009 +0100
     1.3 @@ -38,8 +38,6 @@
     1.4  val pass_mark = 0.5;
     1.5  val convergence = 3.2;    (*Higher numbers allow longer inference chains*)
     1.6  val follow_defs = false;  (*Follow definitions. Makes problems bigger.*)
     1.7 -val include_all = true;
     1.8 -val include_atpset = true;
     1.9    
    1.10  (***************************************************************)
    1.11  (* Relevance Filtering                                         *)
    1.12 @@ -293,15 +291,14 @@
    1.13  
    1.14  (*** white list and black list of lemmas ***)
    1.15  
    1.16 -(*The rule subsetI is frequently omitted by the relevance filter. This could be theory data
    1.17 -  or identified with ATPset (which however is too big currently)*)
    1.18 +(*The rule subsetI is frequently omitted by the relevance filter.*)
    1.19  val whitelist_fo = [subsetI];
    1.20  (* ext has been a 'helper clause', always given to the atps.
    1.21    As such it was not passed to metis, but metis does not include ext (in contrast
    1.22    to the other helper_clauses *)
    1.23  val whitelist_ho = [ResHolClause.ext];
    1.24  
    1.25 -(*** retrieve lemmas from clasimpset and atpset, may filter them ***)
    1.26 +(*** retrieve lemmas and filter them ***)
    1.27  
    1.28  (*Hashing to detect duplicate and variant clauses, e.g. from the [iff] attribute*)
    1.29  
    1.30 @@ -405,18 +402,11 @@
    1.31        (warning ("No name for theorem " ^ Display.string_of_thm_without_context th); false)
    1.32    | check_named _ = true;
    1.33  
    1.34 -(* get lemmas from claset, simpset, atpset and extra supplied rules *)
    1.35 -fun get_clasimp_atp_lemmas ctxt =
    1.36 +fun get_all_lemmas ctxt =
    1.37    let val included_thms =
    1.38 -    if include_all
    1.39 -    then (tap (fn ths => ResAxioms.trace_msg
    1.40 -                 (fn () => ("Including all " ^ Int.toString (length ths) ^ " theorems")))
    1.41 -              (name_thm_pairs ctxt))
    1.42 -    else
    1.43 -    let val atpset_thms =
    1.44 -            if include_atpset then ResAxioms.atpset_rules_of ctxt
    1.45 -            else []
    1.46 -    in  atpset_thms  end
    1.47 +        tap (fn ths => ResAxioms.trace_msg
    1.48 +                     (fn () => ("Including all " ^ Int.toString (length ths) ^ " theorems")))
    1.49 +            (name_thm_pairs ctxt)
    1.50    in
    1.51      filter check_named included_thms
    1.52    end;
    1.53 @@ -524,7 +514,7 @@
    1.54    let
    1.55      val thy = ProofContext.theory_of ctxt
    1.56      val isFO = isFO thy goal_cls
    1.57 -    val included_thms = get_clasimp_atp_lemmas ctxt
    1.58 +    val included_thms = get_all_lemmas ctxt
    1.59      val included_cls = included_thms |> ResAxioms.cnf_rules_pairs thy |> make_unique
    1.60                                       |> restrict_to_logic thy isFO
    1.61                                       |> remove_unwanted_clauses