src/HOL/Tools/res_atp.ML
changeset 24286 7619080e49f0
parent 24215 5458fbf18276
child 24287 c857dac06da6
     1.1 --- a/src/HOL/Tools/res_atp.ML	Wed Aug 15 09:02:11 2007 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Wed Aug 15 12:52:56 2007 +0200
     1.3 @@ -260,152 +260,6 @@
     1.4    or identified with ATPset (which however is too big currently)*)
     1.5  val whitelist = [subsetI];
     1.6  
     1.7 -(*Names of theorems and theorem lists to be blacklisted.
     1.8 -
     1.9 -  These theorems typically produce clauses that are prolific (match too many equality or
    1.10 -  membership literals) and relate to seldom-used facts. Some duplicate other rules.
    1.11 -  FIXME: this blacklist needs to be maintained using theory data and added to using
    1.12 -  an attribute.*)
    1.13 -val blacklist = 
    1.14 -  ["Datatype.prod.size",
    1.15 -   "Divides.dvd_0_left_iff",
    1.16 -   "Finite_Set.card_0_eq",
    1.17 -   "Finite_Set.card_infinite",
    1.18 -   "Finite_Set.Max_ge",
    1.19 -   "Finite_Set.Max_in",
    1.20 -   "Finite_Set.Max_le_iff",
    1.21 -   "Finite_Set.Max_less_iff",
    1.22 -   "Finite_Set.max.f_below_strict_below.below_f_conv", (*duplicates in Orderings.*)
    1.23 -   "Finite_Set.max.f_below_strict_below.strict_below_f_conv", (*duplicates in Orderings.*)
    1.24 -   "Finite_Set.Min_ge_iff",
    1.25 -   "Finite_Set.Min_gr_iff",
    1.26 -   "Finite_Set.Min_in",
    1.27 -   "Finite_Set.Min_le",
    1.28 -   "Finite_Set.min.f_below_strict_below.below_f_conv",        (*duplicates in Orderings.*)
    1.29 -   "Finite_Set.min.f_below_strict_below.strict_below_f_conv", (*duplicates in Orderings.*)
    1.30 -   "Fun.vimage_image_eq",   (*involves an existential quantifier*)
    1.31 -   "HOL.split_if_asm",     (*splitting theorem*)
    1.32 -   "HOL.split_if",         (*splitting theorem*)
    1.33 -   "HOL.All_def",          (*far worse than useless!!*)
    1.34 -   "IntDef.abs_split",
    1.35 -   "IntDef.Integ.Abs_Integ_inject",
    1.36 -   "IntDef.Integ.Abs_Integ_inverse",
    1.37 -   "IntDiv.zdvd_0_left",
    1.38 -   "List.append_eq_append_conv",
    1.39 -   "List.hd_Cons_tl",   (*Says everything is [] or Cons. Probably prolific.*)
    1.40 -   "List.in_listsD",
    1.41 -   "List.in_listsI",
    1.42 -   "List.lists.Cons",
    1.43 -   "List.listsE",
    1.44 -   "Nat.less_one", (*not directional? obscure*)
    1.45 -   "Nat.not_gr0",
    1.46 -   "Nat.one_eq_mult_iff", (*duplicate by symmetry*)
    1.47 -   "Nat.of_nat_0_eq_iff",
    1.48 -   "Nat.of_nat_eq_0_iff",
    1.49 -   "Nat.of_nat_le_0_iff",
    1.50 -   "NatSimprocs.divide_le_0_iff_number_of",  (*too many clauses*)
    1.51 -   "NatSimprocs.divide_less_0_iff_number_of",
    1.52 -   "NatSimprocs.equation_minus_iff_1",  (*not directional*)
    1.53 -   "NatSimprocs.equation_minus_iff_number_of", (*not directional*)
    1.54 -   "NatSimprocs.le_minus_iff_1", (*not directional*)
    1.55 -   "NatSimprocs.le_minus_iff_number_of",  (*not directional*)
    1.56 -   "NatSimprocs.less_minus_iff_1", (*not directional*)
    1.57 -   "NatSimprocs.less_minus_iff_number_of", (*not directional*)
    1.58 -   "NatSimprocs.minus_equation_iff_number_of", (*not directional*)
    1.59 -   "NatSimprocs.minus_le_iff_1", (*not directional*)
    1.60 -   "NatSimprocs.minus_le_iff_number_of", (*not directional*)
    1.61 -   "NatSimprocs.minus_less_iff_1", (*not directional*)
    1.62 -   "NatSimprocs.mult_le_cancel_left_number_of", (*excessive case analysis*)
    1.63 -   "NatSimprocs.mult_le_cancel_right_number_of", (*excessive case analysis*)
    1.64 -   "NatSimprocs.mult_less_cancel_left_number_of", (*excessive case analysis*)
    1.65 -   "NatSimprocs.mult_less_cancel_right_number_of", (*excessive case analysis*)
    1.66 -   "NatSimprocs.zero_le_divide_iff_number_of", (*excessive case analysis*)
    1.67 -   "NatSimprocs.zero_less_divide_iff_number_of",
    1.68 -   "OrderedGroup.abs_0_eq", (*duplicate by symmetry*)
    1.69 -   "OrderedGroup.diff_eq_0_iff_eq", (*prolific?*)
    1.70 -   "OrderedGroup.sup_0_eq_0",
    1.71 -   "OrderedGroup.inf_0_eq_0",
    1.72 -   "OrderedGroup.pprt_eq_0",   (*obscure*)
    1.73 -   "OrderedGroup.pprt_eq_id",   (*obscure*)
    1.74 -   "OrderedGroup.pprt_mono",   (*obscure*)
    1.75 -   "Orderings.split_max",      (*splitting theorem*)
    1.76 -   "Orderings.split_min",      (*splitting theorem*)
    1.77 -   "Power.zero_less_power_abs_iff",
    1.78 -   "Product_Type.split_eta_SetCompr",   (*involves an existential quantifier*)
    1.79 -   "Product_Type.split_paired_Ball_Sigma",     (*splitting theorem*)
    1.80 -   "Product_Type.split_paired_Bex_Sigma",      (*splitting theorem*)
    1.81 -   "Product_Type.split_split_asm",             (*splitting theorem*)
    1.82 -   "Product_Type.split_split",                 (*splitting theorem*)
    1.83 -   "Product_Type.unit_abs_eta_conv",
    1.84 -   "Product_Type.unit_induct",
    1.85 -   "Relation.diagI",
    1.86 -   "Relation.Domain_def",   (*involves an existential quantifier*)
    1.87 -   "Relation.Image_def",   (*involves an existential quantifier*)
    1.88 -   "Relation.ImageI",
    1.89 -   "Ring_and_Field.divide_cancel_left", (*fields are seldom used & often prolific*)
    1.90 -   "Ring_and_Field.divide_cancel_right",
    1.91 -   "Ring_and_Field.divide_divide_eq_left",
    1.92 -   "Ring_and_Field.divide_divide_eq_right",
    1.93 -   "Ring_and_Field.divide_eq_0_iff",
    1.94 -   "Ring_and_Field.divide_eq_1_iff",
    1.95 -   "Ring_and_Field.divide_eq_eq_1",
    1.96 -   "Ring_and_Field.divide_le_0_1_iff",
    1.97 -   "Ring_and_Field.divide_le_eq_1_neg",  (*obscure and prolific*)
    1.98 -   "Ring_and_Field.divide_le_eq_1_pos",  (*obscure and prolific*)
    1.99 -   "Ring_and_Field.divide_less_0_1_iff",
   1.100 -   "Ring_and_Field.divide_less_eq_1_neg",  (*obscure and prolific*)
   1.101 -   "Ring_and_Field.divide_less_eq_1_pos",  (*obscure and prolific*)
   1.102 -   "Ring_and_Field.eq_divide_eq_1", (*duplicate by symmetry*)
   1.103 -   "Ring_and_Field.field_mult_cancel_left",
   1.104 -   "Ring_and_Field.field_mult_cancel_right",
   1.105 -   "Ring_and_Field.inverse_le_iff_le_neg",
   1.106 -   "Ring_and_Field.inverse_le_iff_le",
   1.107 -   "Ring_and_Field.inverse_less_iff_less_neg",
   1.108 -   "Ring_and_Field.inverse_less_iff_less",
   1.109 -   "Ring_and_Field.le_divide_eq_1_neg", (*obscure and prolific*)
   1.110 -   "Ring_and_Field.le_divide_eq_1_pos", (*obscure and prolific*)
   1.111 -   "Ring_and_Field.less_divide_eq_1_neg", (*obscure and prolific*)
   1.112 -   "Ring_and_Field.less_divide_eq_1_pos", (*obscure and prolific*)
   1.113 -   "Ring_and_Field.one_eq_divide_iff",  (*duplicate by symmetry*)
   1.114 -   "Set.ball_simps", "Set.bex_simps",  (*quantifier rewriting: useless*)
   1.115 -   "Set.Collect_bex_eq",   (*involves an existential quantifier*)
   1.116 -   "Set.Collect_ex_eq",   (*involves an existential quantifier*)
   1.117 -   "Set.Diff_eq_empty_iff", (*redundant with paramodulation*)
   1.118 -   "Set.Diff_insert0",
   1.119 -   "Set.empty_Union_conv",   (*redundant with paramodulation*)
   1.120 -   "Set.full_SetCompr_eq",   (*involves an existential quantifier*)
   1.121 -   "Set.image_Collect",      (*involves Collect and a boolean variable...*)
   1.122 -   "Set.image_def",          (*involves an existential quantifier*)
   1.123 -   "Set.disjoint_insert", "Set.insert_disjoint",
   1.124 -   "Set.Int_UNIV",  (*redundant with paramodulation*)
   1.125 -   "Set.Inter_UNIV_conv",
   1.126 -   "Set.Inter_iff", (*We already have InterI, InterE*)
   1.127 -   "Set.psubsetE",    (*too prolific and obscure*)
   1.128 -   "Set.psubsetI",
   1.129 -   "Set.singleton_insert_inj_eq'",
   1.130 -   "Set.singleton_insert_inj_eq",
   1.131 -   "Set.singletonD",  (*these two duplicate some "insert" lemmas*)
   1.132 -   "Set.singletonI",
   1.133 -   "Set.Un_empty", (*redundant with paramodulation*)
   1.134 -   "Set.UNION_def",   (*involves an existential quantifier*)
   1.135 -   "Set.Union_empty_conv", (*redundant with paramodulation*)
   1.136 -   "Set.Union_iff",              (*We already have UnionI, UnionE*)
   1.137 -   "SetInterval.atLeastAtMost_iff", (*obscure and prolific*)
   1.138 -   "SetInterval.atLeastLessThan_iff", (*obscure and prolific*)
   1.139 -   "SetInterval.greaterThanAtMost_iff", (*obscure and prolific*)
   1.140 -   "SetInterval.greaterThanLessThan_iff", (*obscure and prolific*)
   1.141 -   "SetInterval.ivl_subset"];  (*excessive case analysis*)
   1.142 -
   1.143 -(*These might be prolific but are probably OK, and min and max are basic.
   1.144 -   "Orderings.max_less_iff_conj",
   1.145 -   "Orderings.min_less_iff_conj",
   1.146 -   "Orderings.min_max.below_inf.below_inf_conv",
   1.147 -   "Orderings.min_max.below_sup.above_sup_conv",
   1.148 -Very prolific and somewhat obscure:
   1.149 -   "Set.InterD",
   1.150 -   "Set.UnionI",
   1.151 -*)
   1.152 -
   1.153  (*** retrieve lemmas from clasimpset and atpset, may filter them ***)
   1.154  
   1.155  (*Hashing to detect duplicate and variant clauses, e.g. from the [iff] attribute*)
   1.156 @@ -473,9 +327,7 @@
   1.157  
   1.158  fun all_valid_thms ctxt =
   1.159    let
   1.160 -    val banned_tab = foldl setinsert Symtab.empty blacklist
   1.161 -    fun blacklisted s = !run_blacklist_filter andalso
   1.162 -                        (isSome (Symtab.lookup banned_tab s) orelse is_package_def s)
   1.163 +    fun blacklisted s = !run_blacklist_filter andalso is_package_def s
   1.164  
   1.165      fun extern_valid space (name, ths) =
   1.166        let
   1.167 @@ -514,10 +366,16 @@
   1.168  
   1.169  fun is_multi (a, ths) = length ths > 1 orelse String.isSuffix ".axioms" a;
   1.170  
   1.171 -(*The single theorems go BEFORE the multiple ones*)
   1.172 +(*The single theorems go BEFORE the multiple ones. Blacklist is applied to all.*)
   1.173  fun name_thm_pairs ctxt =
   1.174    let val (mults,singles) = List.partition is_multi (all_valid_thms ctxt)
   1.175 -  in  foldl add_single_names  (foldl add_multi_names [] mults) singles end;
   1.176 +      val ht = mk_clause_table 900   (*ht for blacklisted theorems*)
   1.177 +      fun blacklisted x = !run_blacklist_filter andalso isSome (Polyhash.peek ht x)
   1.178 +  in
   1.179 +      app (fn th => ignore (Polyhash.peekInsert ht (th,()))) (ResBlacklist.get ctxt);
   1.180 +      filter (not o blacklisted o #2)
   1.181 +        (foldl add_single_names (foldl add_multi_names [] mults) singles)
   1.182 +  end;
   1.183  
   1.184  fun check_named ("",th) = (warning ("No name for theorem " ^ string_of_thm th); false)
   1.185    | check_named (_,th) = true;