src/HOL/Tools/res_atp.ML
changeset 20444 6c5e38a73db0
parent 20423 593053389701
child 20446 7e616709bca2
     1.1 --- a/src/HOL/Tools/res_atp.ML	Thu Aug 31 10:17:19 2006 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Thu Aug 31 10:18:26 2006 +0200
     1.3 @@ -300,7 +300,10 @@
     1.4  (*The rule subsetI is frequently omitted by the relevance filter.*)
     1.5  val whitelist = ref [subsetI]; 
     1.6  
     1.7 -(*In general, these produce clauses that are prolific (match too many equality or
     1.8 +(*Names of theorems and theorem lists to be banned. The final numeric suffix of
     1.9 +  theorem lists is first removed.
    1.10 +
    1.11 +  These theorems typically produce clauses that are prolific (match too many equality or
    1.12    membership literals) and relate to seldom-used facts. Some duplicate other rules.
    1.13    FIXME: this blacklist needs to be maintained using theory data and added to using
    1.14    an attribute.*)
    1.15 @@ -310,8 +313,7 @@
    1.16     "Datatype.unit.induct",
    1.17     "Datatype.unit.inducts",
    1.18     "Datatype.unit.split",
    1.19 -   "Datatype.unit.splits_1",
    1.20 -   "Datatype.unit.splits_2",
    1.21 +   "Datatype.unit.splits",
    1.22     "Product_Type.unit_abs_eta_conv",
    1.23     "Product_Type.unit_induct",
    1.24  
    1.25 @@ -407,17 +409,15 @@
    1.26     "Ring_and_Field.less_divide_eq_1_neg", (*obscure and prolific*)
    1.27     "Ring_and_Field.less_divide_eq_1_pos", (*obscure and prolific*)
    1.28     "Ring_and_Field.one_eq_divide_iff",  (*duplicate by symmetry*)
    1.29 +   "Set.disjoint_insert",
    1.30 +   "Set.insert_disjoint",
    1.31 +   "Set.Inter_UNIV_conv",
    1.32 +   "Set.ball_simps", "Set.bex_simps",   (*quantifier rewriting: useless*)
    1.33     "Set.Diff_eq_empty_iff", (*redundant with paramodulation*)
    1.34     "Set.Diff_insert0",
    1.35 -   "Set.disjoint_insert_1",
    1.36 -   "Set.disjoint_insert_2",
    1.37     "Set.empty_Union_conv", (*redundant with paramodulation*)
    1.38 -   "Set.insert_disjoint_1",
    1.39 -   "Set.insert_disjoint_2",
    1.40     "Set.Int_UNIV", (*redundant with paramodulation*)
    1.41     "Set.Inter_iff",              (*We already have InterI, InterE*)
    1.42 -   "Set.Inter_UNIV_conv_1",
    1.43 -   "Set.Inter_UNIV_conv_2",
    1.44     "Set.psubsetE",    (*too prolific and obscure*)
    1.45     "Set.psubsetI",
    1.46     "Set.singleton_insert_inj_eq'",
    1.47 @@ -472,10 +472,23 @@
    1.48        Polyhash.insert ht (x^"_iff2", ()); 
    1.49        Polyhash.insert ht (x^"_dest", ())); 
    1.50  
    1.51 +(*Are all characters in this string digits?*)
    1.52 +fun all_numeric s = null (String.tokens Char.isDigit s);
    1.53 +
    1.54 +(*Delete a suffix of the form _\d+*)
    1.55 +fun delete_numeric_suffix s =
    1.56 +  case rev (String.fields (fn c => c = #"_") s) of
    1.57 +      last::rest => 
    1.58 +          if all_numeric last 
    1.59 +          then [s, String.concatWith "_" (rev rest)]
    1.60 +          else [s]
    1.61 +    | [] => [s];
    1.62 +
    1.63  fun make_banned_test xs = 
    1.64    let val ht = Polyhash.mkTable (Polyhash.hash_string, op =)
    1.65                                  (6000, HASH_STRING)
    1.66 -      fun banned s = isSome (Polyhash.peek ht s)
    1.67 +      fun banned s = exists (fn s' => isSome (Polyhash.peek ht s')) 
    1.68 +                            (delete_numeric_suffix s)
    1.69    in  app (fn x => Polyhash.insert ht (x,())) (!blacklist);
    1.70        app (insert_suffixed_names ht) (!blacklist @ xs); 
    1.71        banned
    1.72 @@ -616,6 +629,7 @@
    1.73  (*Called by the oracle-based methods declared in res_atp_methods.ML*)
    1.74  fun write_subgoal_file dfg mode ctxt conjectures user_thms n =
    1.75      let val conj_cls = make_clauses conjectures 
    1.76 +                         |> ResAxioms.assume_abstract_list |> Meson.finish_cnf
    1.77  	val hyp_cls = cnf_hyps_thms ctxt
    1.78  	val goal_cls = conj_cls@hyp_cls
    1.79  	val (included_thms,user_rules) = get_clasimp_atp_lemmas ctxt user_thms
    1.80 @@ -735,7 +749,8 @@
    1.81  	      let val st = Seq.hd (EVERY' [rtac ccontr, ObjectLogic.atomize_tac, 
    1.82  	                                   skolemize_tac] n th)
    1.83  		  val negs = Option.valOf (metahyps_thms n st)
    1.84 -		  val negs_clauses = make_clauses (ResAxioms.assume_abstract negs)
    1.85 +		  val negs_clauses = make_clauses negs |> ResAxioms.assume_abstract_list
    1.86 +		                       |> Meson.finish_cnf
    1.87  	      in
    1.88  		  negs_clauses :: get_neg_subgoals (n-1)
    1.89  	      end