src/HOL/Tools/ATP/res_clasimpset.ML
changeset 19480 868cf5051ff5
parent 19356 794802e95d35
child 19675 a4894fb2a5f2
     1.1 --- a/src/HOL/Tools/ATP/res_clasimpset.ML	Thu Apr 27 12:10:47 2006 +0200
     1.2 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML	Thu Apr 27 12:11:05 2006 +0200
     1.3 @@ -27,15 +27,7 @@
     1.4    FIXME: this blacklist needs to be maintained using theory data and added to using
     1.5    an attribute.*)
     1.6  val blacklist = ref
     1.7 -  ["Datatype.not_None_eq",    (*Says everything is None or Some. Probably prolific.*)
     1.8 -   "Datatype.not_Some_eq_D",  (*Says everything is None or Some. Probably prolific.*)
     1.9 -   "Datatype.not_Some_eq",    (*Says everything is None or Some. Probably prolific.*)
    1.10 -   "Datatype.option.size_1",
    1.11 -   "Datatype.option.size_2",
    1.12 -   "Datatype.prod.size",
    1.13 -   "Datatype.sum.size_1",
    1.14 -   "Datatype.sum.size_2",
    1.15 -   "Datatype.unit.size",
    1.16 +  ["Datatype.prod.size",
    1.17     "Divides.dvd_0_left_iff",
    1.18     "Finite_Set.card_0_eq",
    1.19     "Finite_Set.card_infinite",
    1.20 @@ -53,31 +45,23 @@
    1.21     "Finite_Set.min_max.below_inf_sup_Inf_Sup.sup_Inf_absorb", 
    1.22     "Finite_Set.min.f_below_strict_below.below_f_conv",        (*duplicates in Orderings.*)
    1.23     "Finite_Set.min.f_below_strict_below.strict_below_f_conv", (*duplicates in Orderings.*)
    1.24 -   "Infinite_Set.atmost_one_unique",
    1.25 -   "IntArith.zabs_less_one_iff",
    1.26     "IntDef.Integ.Abs_Integ_inject",
    1.27     "IntDef.Integ.Abs_Integ_inverse",
    1.28     "IntDiv.zdvd_0_left",
    1.29 -   "IntDiv.zero_less_zpower_abs_iff",
    1.30     "List.append_eq_append_conv",
    1.31 -   "List.Cons_in_lex",
    1.32     "List.hd_Cons_tl",   (*Says everything is [] or Cons. Probably prolific.*)
    1.33     "List.in_listsD",
    1.34     "List.in_listsI",
    1.35     "List.lists.Cons",
    1.36     "List.listsE",
    1.37 -   "List.take_eq_Nil",
    1.38 -   "Nat.less_one",
    1.39     "Nat.less_one", (*not directional? obscure*)
    1.40     "Nat.not_gr0",
    1.41     "Nat.one_eq_mult_iff", (*duplicate by symmetry*)
    1.42     "NatArith.of_nat_0_eq_iff",
    1.43     "NatArith.of_nat_eq_0_iff",
    1.44     "NatArith.of_nat_le_0_iff",
    1.45 -   "NatSimprocs.divide_le_0_iff_number_of",  (*seldom used; often prolific*)
    1.46     "NatSimprocs.divide_le_0_iff_number_of",  (*too many clauses*)
    1.47     "NatSimprocs.divide_less_0_iff_number_of",
    1.48 -   "NatSimprocs.divide_less_0_iff_number_of",   (*too many clauses*)
    1.49     "NatSimprocs.equation_minus_iff_1",  (*not directional*)
    1.50     "NatSimprocs.equation_minus_iff_number_of", (*not directional*)
    1.51     "NatSimprocs.le_minus_iff_1", (*not directional*)
    1.52 @@ -92,11 +76,8 @@
    1.53     "NatSimprocs.mult_le_cancel_right_number_of", (*excessive case analysis*)
    1.54     "NatSimprocs.mult_less_cancel_left_number_of", (*excessive case analysis*)
    1.55     "NatSimprocs.mult_less_cancel_right_number_of", (*excessive case analysis*)
    1.56 -   "NatSimprocs.zero_le_divide_iff_number_of",
    1.57     "NatSimprocs.zero_le_divide_iff_number_of", (*excessive case analysis*)
    1.58     "NatSimprocs.zero_less_divide_iff_number_of",
    1.59 -   "NatSimprocs.zero_less_divide_iff_number_of", (*excessive case analysis*)
    1.60 -   "OrderedGroup.abs_0_eq",
    1.61     "OrderedGroup.abs_0_eq", (*duplicate by symmetry*)
    1.62     "OrderedGroup.diff_eq_0_iff_eq", (*prolific?*)
    1.63     "OrderedGroup.join_0_eq_0",
    1.64 @@ -106,8 +87,6 @@
    1.65     "OrderedGroup.pprt_mono",   (*obscure*)
    1.66     "Parity.even_nat_power",   (*obscure, somewhat prolilfic*)
    1.67     "Parity.power_eq_0_iff_number_of",
    1.68 -   "Parity.power_eq_0_iff_number_of",
    1.69 -   "Parity.power_le_zero_eq_number_of",
    1.70     "Parity.power_le_zero_eq_number_of",   (*obscure and prolific*)
    1.71     "Parity.power_less_zero_eq_number_of",
    1.72     "Parity.zero_le_power_eq_number_of",   (*obscure and prolific*)
    1.73 @@ -123,15 +102,11 @@
    1.74     "Ring_and_Field.divide_eq_1_iff",
    1.75     "Ring_and_Field.divide_eq_eq_1",
    1.76     "Ring_and_Field.divide_le_0_1_iff",
    1.77 -   "Ring_and_Field.divide_le_eq_1_neg",
    1.78     "Ring_and_Field.divide_le_eq_1_neg",  (*obscure and prolific*)
    1.79 -   "Ring_and_Field.divide_le_eq_1_pos",
    1.80     "Ring_and_Field.divide_le_eq_1_pos",  (*obscure and prolific*)
    1.81     "Ring_and_Field.divide_less_0_1_iff",
    1.82     "Ring_and_Field.divide_less_eq_1_neg",  (*obscure and prolific*)
    1.83 -   "Ring_and_Field.divide_less_eq_1_pos",
    1.84     "Ring_and_Field.divide_less_eq_1_pos",  (*obscure and prolific*)
    1.85 -   "Ring_and_Field.eq_divide_eq_1",
    1.86     "Ring_and_Field.eq_divide_eq_1", (*duplicate by symmetry*)
    1.87     "Ring_and_Field.field_mult_cancel_left",
    1.88     "Ring_and_Field.field_mult_cancel_right",
    1.89 @@ -139,13 +114,9 @@
    1.90     "Ring_and_Field.inverse_le_iff_le",
    1.91     "Ring_and_Field.inverse_less_iff_less_neg",
    1.92     "Ring_and_Field.inverse_less_iff_less",
    1.93 -   "Ring_and_Field.le_divide_eq_1_neg",
    1.94     "Ring_and_Field.le_divide_eq_1_neg", (*obscure and prolific*)
    1.95 -   "Ring_and_Field.le_divide_eq_1_pos",
    1.96     "Ring_and_Field.le_divide_eq_1_pos", (*obscure and prolific*)
    1.97 -   "Ring_and_Field.less_divide_eq_1_neg",
    1.98     "Ring_and_Field.less_divide_eq_1_neg", (*obscure and prolific*)
    1.99 -   "Ring_and_Field.less_divide_eq_1_pos",
   1.100     "Ring_and_Field.less_divide_eq_1_pos", (*obscure and prolific*)
   1.101     "Ring_and_Field.one_eq_divide_iff",  (*duplicate by symmetry*)
   1.102     "Set.Diff_eq_empty_iff", (*redundant with paramodulation*)
   1.103 @@ -172,10 +143,8 @@
   1.104     "SetInterval.atLeastLessThan_iff", (*obscure and prolific*)
   1.105     "SetInterval.greaterThanAtMost_iff", (*obscure and prolific*)
   1.106     "SetInterval.greaterThanLessThan_iff", (*obscure and prolific*)
   1.107 -   "SetInterval.ivl_subset", (*excessive case analysis*)
   1.108 -   "Sum_Type.InlI",
   1.109 -   "Sum_Type.InrI"];
   1.110 -   
   1.111 +   "SetInterval.ivl_subset"];  (*excessive case analysis*)
   1.112 +    
   1.113  (*These might be prolific but are probably OK, and min and max are basic.
   1.114     "Orderings.max_less_iff_conj", 
   1.115     "Orderings.min_less_iff_conj",