blacklist experiments
authorpaulson
Fri Jan 13 17:39:41 2006 +0100 (2006-01-13)
changeset 1867701265301db7f
parent 18676 5bce9fddce2e
child 18678 dd0c569fa43d
blacklist experiments
src/HOL/Tools/ATP/res_clasimpset.ML
     1.1 --- a/src/HOL/Tools/ATP/res_clasimpset.ML	Fri Jan 13 17:39:19 2006 +0100
     1.2 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML	Fri Jan 13 17:39:41 2006 +0100
     1.3 @@ -75,6 +75,7 @@
     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 @@ -87,55 +88,173 @@
    1.12  val use_simpset = ref false;   (*Performance is much better without simprules*)
    1.13  
    1.14  (*In general, these produce clauses that are prolific (match too many equality or
    1.15 -  membership literals) and relate to seldom-used facts. Some duplicate other rules.*)
    1.16 +  membership literals) and relate to seldom-used facts. Some duplicate other rules.
    1.17 +  FIXME: this blacklist needs to be maintained using theory data and added to using
    1.18 +  an attribute.*)
    1.19  val blacklist = ref
    1.20 -  ["Finite_Set.Max_ge",
    1.21 +  ["Datatype.not_None_eq_iff2",
    1.22 +   "Datatype.not_Some_eq_D",
    1.23 +   "Datatype.not_Some_eq",
    1.24 +   "Datatype.option.size_1",
    1.25 +   "Datatype.option.size_2",
    1.26 +   "Datatype.prod.size",
    1.27 +   "Datatype.sum.size_1",
    1.28 +   "Datatype.sum.size_2",
    1.29 +   "Datatype.unit.size",
    1.30 +   "Divides.dvd_0_left_iff",
    1.31 +   "Finite_Set.card_0_eq",
    1.32 +   "Finite_Set.card_infinite",
    1.33 +   "Finite_Set.Max_ge",
    1.34 +   "Finite_Set.Max_in",
    1.35     "Finite_Set.Max_le_iff",
    1.36     "Finite_Set.Max_less_iff",
    1.37 -   "Finite_Set.Min_le",
    1.38 +   "Finite_Set.max.f_below_strict_below.below_f_conv", (*duplicates in Orderings.*)
    1.39 +   "Finite_Set.max.f_below_strict_below.strict_below_f_conv", (*duplicates in Orderings.*)
    1.40     "Finite_Set.Min_ge_iff",
    1.41     "Finite_Set.Min_gr_iff",
    1.42 -   "Finite_Set.min_max.below_inf_sup_Inf_Sup.inf_Sup_absorb",
    1.43 -   "Finite_Set.min_max.below_inf_sup_Inf_Sup.sup_Inf_absorb",
    1.44 -   (*The next four are duplicates of the properties of min and max, from Orderings.*)
    1.45 -   "Finite_Set.max.f_below_strict_below.below_f_conv",
    1.46 -   "Finite_Set.max.f_below_strict_below.strict_below_f_conv",
    1.47 -   "Finite_Set.min.f_below_strict_below.strict_below_f_conv",
    1.48 -   "Finite_Set.min.f_below_strict_below.below_f_conv",
    1.49 +   "Finite_Set.Min_in",
    1.50 +   "Finite_Set.Min_le",
    1.51 +   "Finite_Set.min_max.below_inf_sup_Inf_Sup.inf_Sup_absorb", 
    1.52 +   "Finite_Set.min_max.below_inf_sup_Inf_Sup.sup_Inf_absorb", 
    1.53 +   "Finite_Set.min.f_below_strict_below.below_f_conv",        (*duplicates in Orderings.*)
    1.54 +   "Finite_Set.min.f_below_strict_below.strict_below_f_conv", (*duplicates in Orderings.*)
    1.55     "Infinite_Set.atmost_one_unique",
    1.56 +   "IntArith.zabs_less_one_iff",
    1.57 +   "IntDef.Integ.Abs_Integ_inject",
    1.58 +   "IntDef.Integ.Abs_Integ_inverse",
    1.59 +   "IntDiv.zdvd_0_left",
    1.60 +   "IntDiv.zero_less_zpower_abs_iff",
    1.61 +   "List.append_eq_append_conv",
    1.62 +   "List.Cons_in_lex",
    1.63     "List.in_listsD",
    1.64     "List.in_listsI",
    1.65 +   "List.lists.Cons",
    1.66     "List.listsE",
    1.67 -   "List.lists.Cons",
    1.68 +   "List.take_eq_Nil",
    1.69 +   "Nat.less_one",
    1.70 +   "Nat.less_one", (*not directional? obscure*)
    1.71 +   "Nat.not_gr0",
    1.72 +   "Nat.one_eq_mult_iff", (*duplicate by symmetry*)
    1.73 +   "NatArith.of_nat_0_eq_iff",
    1.74 +   "NatArith.of_nat_eq_0_iff",
    1.75 +   "NatArith.of_nat_le_0_iff",
    1.76 +   "NatSimprocs.divide_le_0_iff_number_of",  (*seldom used; often prolific*)
    1.77 +   "NatSimprocs.divide_le_0_iff_number_of",  (*too many clauses*)
    1.78 +   "NatSimprocs.divide_less_0_iff_number_of",
    1.79 +   "NatSimprocs.divide_less_0_iff_number_of",   (*too many clauses*)
    1.80 +   "NatSimprocs.equation_minus_iff_1",  (*not directional*)
    1.81 +   "NatSimprocs.equation_minus_iff_number_of", (*not directional*)
    1.82 +   "NatSimprocs.le_minus_iff_1", (*not directional*)
    1.83 +   "NatSimprocs.le_minus_iff_number_of",  (*not directional*)
    1.84 +   "NatSimprocs.less_minus_iff_1", (*not directional*)
    1.85 +   "NatSimprocs.less_minus_iff_number_of", (*not directional*)
    1.86 +   "NatSimprocs.minus_equation_iff_number_of", (*not directional*)
    1.87 +   "NatSimprocs.minus_le_iff_1", (*not directional*)
    1.88 +   "NatSimprocs.minus_le_iff_number_of", (*not directional*)
    1.89 +   "NatSimprocs.minus_less_iff_1", (*not directional*)
    1.90 +   "NatSimprocs.mult_le_cancel_left_number_of", (*excessive case analysis*)
    1.91 +   "NatSimprocs.mult_le_cancel_right_number_of", (*excessive case analysis*)
    1.92 +   "NatSimprocs.mult_less_cancel_left_number_of", (*excessive case analysis*)
    1.93 +   "NatSimprocs.mult_less_cancel_right_number_of", (*excessive case analysis*)
    1.94 +   "NatSimprocs.zero_le_divide_iff_number_of",
    1.95 +   "NatSimprocs.zero_le_divide_iff_number_of", (*excessive case analysis*)
    1.96 +   "NatSimprocs.zero_less_divide_iff_number_of",
    1.97 +   "NatSimprocs.zero_less_divide_iff_number_of", (*excessive case analysis*)
    1.98 +   "OrderedGroup.abs_0_eq",
    1.99 +   "OrderedGroup.abs_0_eq", (*duplicate by symmetry*)
   1.100 +   "OrderedGroup.diff_eq_0_iff_eq", (*prolific?*)
   1.101 +   "OrderedGroup.join_0_eq_0",
   1.102 +   "OrderedGroup.meet_0_eq_0",
   1.103 +   "OrderedGroup.pprt_eq_0",   (*obscure*)
   1.104 +   "OrderedGroup.pprt_eq_id",   (*obscure*)
   1.105 +   "OrderedGroup.pprt_mono",   (*obscure*)
   1.106 +   "Parity.even_nat_power",   (*obscure, somewhat prolilfic*)
   1.107 +   "Parity.power_eq_0_iff_number_of",
   1.108 +   "Parity.power_eq_0_iff_number_of",
   1.109 +   "Parity.power_le_zero_eq_number_of",
   1.110 +   "Parity.power_le_zero_eq_number_of",   (*obscure and prolific*)
   1.111 +   "Parity.power_less_zero_eq_number_of",
   1.112 +   "Parity.zero_le_power_eq_number_of",   (*obscure and prolific*)
   1.113 +   "Parity.zero_less_power_eq_number_of",   (*obscure and prolific*)
   1.114 +   "Power.zero_less_power_abs_iff",
   1.115 +   "Relation.diagI",
   1.116     "Relation.ImageI",
   1.117 -   "Relation.diagI",
   1.118 +   "Ring_and_Field.divide_cancel_left", (*fields are seldom used & often prolific*)
   1.119 +   "Ring_and_Field.divide_cancel_right",
   1.120 +   "Ring_and_Field.divide_divide_eq_left",
   1.121 +   "Ring_and_Field.divide_divide_eq_right",
   1.122 +   "Ring_and_Field.divide_eq_0_iff",
   1.123 +   "Ring_and_Field.divide_eq_1_iff",
   1.124 +   "Ring_and_Field.divide_eq_eq_1",
   1.125 +   "Ring_and_Field.divide_le_0_1_iff",
   1.126 +   "Ring_and_Field.divide_le_eq_1_neg",
   1.127 +   "Ring_and_Field.divide_le_eq_1_neg",  (*obscure and prolific*)
   1.128 +   "Ring_and_Field.divide_le_eq_1_pos",
   1.129 +   "Ring_and_Field.divide_le_eq_1_pos",  (*obscure and prolific*)
   1.130 +   "Ring_and_Field.divide_less_0_1_iff",
   1.131 +   "Ring_and_Field.divide_less_eq_1_neg",  (*obscure and prolific*)
   1.132 +   "Ring_and_Field.divide_less_eq_1_pos",
   1.133 +   "Ring_and_Field.divide_less_eq_1_pos",  (*obscure and prolific*)
   1.134 +   "Ring_and_Field.eq_divide_eq_1",
   1.135 +   "Ring_and_Field.eq_divide_eq_1", (*duplicate by symmetry*)
   1.136 +   "Ring_and_Field.field_mult_cancel_left",
   1.137 +   "Ring_and_Field.field_mult_cancel_right",
   1.138 +   "Ring_and_Field.inverse_le_iff_le_neg",
   1.139 +   "Ring_and_Field.inverse_le_iff_le",
   1.140 +   "Ring_and_Field.inverse_less_iff_less_neg",
   1.141 +   "Ring_and_Field.inverse_less_iff_less",
   1.142 +   "Ring_and_Field.le_divide_eq_1_neg",
   1.143 +   "Ring_and_Field.le_divide_eq_1_neg", (*obscure and prolific*)
   1.144 +   "Ring_and_Field.le_divide_eq_1_pos",
   1.145 +   "Ring_and_Field.le_divide_eq_1_pos", (*obscure and prolific*)
   1.146 +   "Ring_and_Field.less_divide_eq_1_neg",
   1.147 +   "Ring_and_Field.less_divide_eq_1_neg", (*obscure and prolific*)
   1.148 +   "Ring_and_Field.less_divide_eq_1_pos",
   1.149 +   "Ring_and_Field.less_divide_eq_1_pos", (*obscure and prolific*)
   1.150 +   "Ring_and_Field.one_eq_divide_iff",  (*duplicate by symmetry*)
   1.151 +   "Set.Diff_eq_empty_iff", (*redundant with paramodulation*)
   1.152     "Set.Diff_insert0",
   1.153 +   "Set.disjoint_insert_1",
   1.154 +   "Set.disjoint_insert_2",
   1.155 +   "Set.empty_Union_conv", (*redundant with paramodulation*)
   1.156 +   "Set.insert_disjoint_1",
   1.157 +   "Set.insert_disjoint_2",
   1.158 +   "Set.Int_UNIV", (*redundant with paramodulation*)
   1.159 +   "Set.Inter_iff",              (*We already have InterI, InterE*)
   1.160     "Set.Inter_UNIV_conv_1",
   1.161     "Set.Inter_UNIV_conv_2",
   1.162 -   "Set.Inter_iff",              (*We already have InterI, InterE*)
   1.163 +   "Set.psubsetE",    (*too prolific and obscure*)
   1.164 +   "Set.psubsetI",
   1.165 +   "Set.singleton_insert_inj_eq'",
   1.166 +   "Set.singleton_insert_inj_eq",
   1.167 +   "Set.singletonD",  (*these two duplicate some "insert" lemmas*)
   1.168 +   "Set.singletonI",
   1.169 +   "Set.Un_empty", (*redundant with paramodulation*)
   1.170 +   "Set.Union_empty_conv", (*redundant with paramodulation*)
   1.171     "Set.Union_iff",              (*We already have UnionI, UnionE*)
   1.172 -   "Datatype.not_None_eq_iff2",
   1.173 -   "Datatype.not_Some_eq",
   1.174 -   "Datatype.not_Some_eq_D",
   1.175 -   "Set.disjoint_insert_1",
   1.176 -   "Set.disjoint_insert_2",
   1.177 -   "Set.insert_disjoint_1",
   1.178 -   "Set.insert_disjoint_2",
   1.179 -   "Set.singletonD",
   1.180 -   "Set.singletonI",
   1.181 +   "SetInterval.atLeastAtMost_iff", (*obscure and prolific*)
   1.182 +   "SetInterval.atLeastLessThan_iff", (*obscure and prolific*)
   1.183 +   "SetInterval.greaterThanAtMost_iff", (*obscure and prolific*)
   1.184 +   "SetInterval.greaterThanLessThan_iff", (*obscure and prolific*)
   1.185 +   "SetInterval.ivl_subset", (*excessive case analysis*)
   1.186     "Sum_Type.InlI",
   1.187 -   "Sum_Type.InrI",
   1.188 -   "Set.singleton_insert_inj_eq",
   1.189 -   "Set.singleton_insert_inj_eq'"];
   1.190 -
   1.191 -(*These are the defining properties of min and max, but as they are prolific they
   1.192 -  could be included above.
   1.193 -   "Orderings.max_less_iff_conj",
   1.194 +   "Sum_Type.InrI"];
   1.195 +   
   1.196 +(*These might be prolific but are probably OK, and min and max are basic.
   1.197 +   "Orderings.max_less_iff_conj", 
   1.198     "Orderings.min_less_iff_conj",
   1.199     "Orderings.min_max.below_inf.below_inf_conv",
   1.200     "Orderings.min_max.below_sup.above_sup_conv",
   1.201 +Very prolific and somewhat obscure:
   1.202 +   "Set.InterD",
   1.203 +   "Set.UnionI",
   1.204  *)
   1.205  
   1.206 +val theory_blacklist = ref
   1.207 +  ["Datatype_Universe.",    (*unnecessary in virtually all proofs*)
   1.208 +   "Equiv_Relations."]  
   1.209 +
   1.210 +
   1.211  val relevant = ref 0;  (*Relevance filtering is off by default*)
   1.212  
   1.213  (*The "name" of a theorem is its statement, if nothing else is available.*)
   1.214 @@ -165,9 +284,7 @@
   1.215  	multi (clause, theorem) num_of_cls []
   1.216      end;
   1.217      
   1.218 -(*Hashing to detect duplicate and variant clauses, e.g. from the [iff] attribute
   1.219 -Some primes from http://primes.utm.edu/:
   1.220 -*)
   1.221 +(*Hashing to detect duplicate and variant clauses, e.g. from the [iff] attribute*)
   1.222  
   1.223  exception HASH_CLAUSE and HASH_STRING;
   1.224  
   1.225 @@ -177,10 +294,12 @@
   1.226        Polyhash.insert ht (x^"_iff2", ()); 
   1.227        Polyhash.insert ht (x^"_dest", ())); 
   1.228  
   1.229 +fun banned_theory s = exists (fn thy => String.isPrefix thy s) (!theory_blacklist);
   1.230 +
   1.231  fun make_banned_test xs = 
   1.232    let val ht = Polyhash.mkTable (Polyhash.hash_string, op =)
   1.233                                  (6000, HASH_STRING)
   1.234 -      fun banned s = isSome (Polyhash.peek ht s)
   1.235 +      fun banned s = isSome (Polyhash.peek ht s) orelse banned_theory s
   1.236    in  app (fn x => Polyhash.insert ht (x,())) (!blacklist);
   1.237        app (insert_suffixed_names ht) (!blacklist @ xs); 
   1.238        banned