blacklist of prolific theorems (must be replaced by an attribute later
authorpaulson
Fri Dec 23 17:36:00 2005 +0100 (2005-12-23)
changeset 18509d2d96f12a1fc
parent 18508 c5861e128a95
child 18510 0a6c24f549c3
blacklist of prolific theorems (must be replaced by an attribute later
src/HOL/Tools/ATP/res_clasimpset.ML
     1.1 --- a/src/HOL/Tools/ATP/res_clasimpset.ML	Fri Dec 23 17:34:46 2005 +0100
     1.2 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML	Fri Dec 23 17:36:00 2005 +0100
     1.3 @@ -3,29 +3,22 @@
     1.4      Copyright   2004  University of Cambridge
     1.5  *)
     1.6  
     1.7 -
     1.8  structure ReduceAxiomsN =
     1.9  (* Author: Jia Meng, Cambridge University Computer Laboratory
    1.10     Remove irrelevant axioms used for a proof of a goal, with with iteration control
    1.11 -   
    1.12     Initial version. Needs elaboration. *)
    1.13  
    1.14  struct
    1.15  
    1.16 -fun add_term_consts_rm ncs (Const(c, _)) cs = 
    1.17 -    if (c mem ncs) then cs else (c ins_string cs)
    1.18 +fun add_term_consts_rm ncs (Const(c, _)) cs = if (c mem ncs) then cs else (c ins_string cs)
    1.19    | add_term_consts_rm ncs (t $ u) cs =
    1.20        add_term_consts_rm ncs t (add_term_consts_rm ncs u cs)
    1.21    | add_term_consts_rm ncs (Abs(_,_,t)) cs = add_term_consts_rm ncs t cs
    1.22    | add_term_consts_rm ncs _ cs = cs;
    1.23  
    1.24 -
    1.25  fun term_consts_rm ncs t = add_term_consts_rm ncs t [];
    1.26 -
    1.27  fun thm_consts_rm ncs thm = term_consts_rm ncs (prop_of thm);
    1.28 -
    1.29  fun consts_of_thm (n,thm) = thm_consts_rm ["Trueprop","==>","all","Ex","op &", "op |", "Not", "All", "op -->", "op =", "==", "True", "False"] thm;
    1.30 -
    1.31  fun consts_of_term term = term_consts_rm ["Trueprop","==>","all","Ex","op &", "op |", "Not", "All", "op -->", "op =", "==", "True", "False"] term;
    1.32  
    1.33  fun make_pairs [] _ = []
    1.34 @@ -35,46 +28,30 @@
    1.35    | const_thm_list_aux (thm::thms) cthms =
    1.36      let val consts = consts_of_thm thm
    1.37  	val cthms' = make_pairs consts thm 
    1.38 -    in
    1.39 -	const_thm_list_aux thms (cthms' @ cthms)
    1.40 -    end;
    1.41 -
    1.42 +    in const_thm_list_aux thms (cthms' @ cthms) end;
    1.43  
    1.44  fun const_thm_list thms = const_thm_list_aux thms [];
    1.45  
    1.46 -fun make_thm_table thms  = 
    1.47 -    let val consts_thms = const_thm_list thms
    1.48 -    in
    1.49 -	Symtab.make_multi consts_thms
    1.50 -    end;
    1.51 -
    1.52 +fun make_thm_table thms = Symtab.make_multi (const_thm_list thms);
    1.53  
    1.54  fun consts_in_goal goal = consts_of_term goal;
    1.55  
    1.56  fun axioms_having_consts_aux [] tab thms = thms
    1.57    | axioms_having_consts_aux (c::cs) tab thms =
    1.58 -    let val thms1 = Symtab.lookup tab c
    1.59 -      val thms2 = 
    1.60 -          case thms1 of (SOME x) => x
    1.61 -                      | NONE => []
    1.62 -    in
    1.63 -      axioms_having_consts_aux cs tab (thms2 union thms)
    1.64 -    end;
    1.65 +    let val thms2 = Option.getOpt (Symtab.lookup tab c, [])
    1.66 +    in axioms_having_consts_aux cs tab (thms2 union thms) end;
    1.67  
    1.68  fun axioms_having_consts cs tab = axioms_having_consts_aux cs tab [];
    1.69  
    1.70 -
    1.71  fun relevant_axioms goal thmTab n =  
    1.72 -    let val consts = consts_in_goal goal
    1.73 -	fun relevant_axioms_aux1 cs k =
    1.74 +    let fun relevant_axioms_aux1 cs k =
    1.75  	    let val thms1 = axioms_having_consts cs thmTab
    1.76  		val cs1 = foldl (op union_string) [] (map consts_of_thm thms1)
    1.77  	    in
    1.78 -		if ((cs1 subset cs) orelse n <= k) then (k,thms1) 
    1.79 -		else (relevant_axioms_aux1 (cs1 union cs) (k+1))
    1.80 +		if (cs1 subset cs) orelse n <= k then (k,thms1) 
    1.81 +		else relevant_axioms_aux1 (cs1 union cs) (k+1)
    1.82  	    end
    1.83 -
    1.84 -    in  relevant_axioms_aux1 consts 1  end;
    1.85 +    in  relevant_axioms_aux1 (consts_in_goal goal) 1  end;
    1.86  
    1.87  fun relevant_filter n goal thms = 
    1.88      if n<=0 then thms 
    1.89 @@ -85,22 +62,19 @@
    1.90      let val clasetR = ResAxioms.claset_rules_of_thy thy
    1.91  	val simpsetR = ResAxioms.simpset_rules_of_thy thy	  
    1.92  	val table = make_thm_table (clasetR @ simpsetR)	
    1.93 -    in
    1.94 -	relevant_axioms goal table n
    1.95 -    end;
    1.96 +    in relevant_axioms goal table n end;
    1.97  
    1.98  fun find_axioms_n_c thy goal n =
    1.99      let val current_thms = PureThy.thms_of thy
   1.100  	val table = make_thm_table current_thms
   1.101 -    in
   1.102 -	relevant_axioms goal table n
   1.103 -    end;
   1.104 +    in relevant_axioms goal table n end;
   1.105  
   1.106  end;
   1.107  
   1.108  
   1.109  signature RES_CLASIMP = 
   1.110    sig
   1.111 +  val blacklist : string list ref (*Theorems forbidden in the output*)
   1.112    val relevant : int ref
   1.113    val use_simpset: bool ref
   1.114    val get_clasimp_lemmas : 
   1.115 @@ -112,6 +86,56 @@
   1.116  struct
   1.117  val use_simpset = ref false;   (*Performance is much better without simprules*)
   1.118  
   1.119 +(*In general, these produce clauses that are prolific (match too many equality or
   1.120 +  membership literals) and relate to seldom-used facts. Some duplicate other rules.*)
   1.121 +val blacklist = ref
   1.122 +  ["Finite_Set.Max_ge",
   1.123 +   "Finite_Set.Max_le_iff",
   1.124 +   "Finite_Set.Max_less_iff",
   1.125 +   "Finite_Set.Min_le",
   1.126 +   "Finite_Set.Min_ge_iff",
   1.127 +   "Finite_Set.Min_gr_iff",
   1.128 +   "Finite_Set.min_max.below_inf_sup_Inf_Sup.inf_Sup_absorb",
   1.129 +   "Finite_Set.min_max.below_inf_sup_Inf_Sup.sup_Inf_absorb",
   1.130 +   (*The next four are duplicates of the properties of min and max, from Orderings.*)
   1.131 +   "Finite_Set.max.f_below_strict_below.below_f_conv",
   1.132 +   "Finite_Set.max.f_below_strict_below.strict_below_f_conv",
   1.133 +   "Finite_Set.min.f_below_strict_below.strict_below_f_conv",
   1.134 +   "Finite_Set.min.f_below_strict_below.below_f_conv",
   1.135 +   "Infinite_Set.atmost_one_unique",
   1.136 +   "List.in_listsD",
   1.137 +   "List.in_listsI",
   1.138 +   "List.listsE",
   1.139 +   "List.lists.Cons",
   1.140 +   "Relation.ImageI",
   1.141 +   "Relation.diagI",
   1.142 +   "Set.Diff_insert0",
   1.143 +   "Set.Inter_UNIV_conv_1",
   1.144 +   "Set.Inter_UNIV_conv_2",
   1.145 +   "Set.Inter_iff",              (*We already have InterI, InterE*)
   1.146 +   "Set.Union_iff",              (*We already have UnionI, UnionE*)
   1.147 +   "Datatype.not_None_eq_iff2",
   1.148 +   "Datatype.not_Some_eq",
   1.149 +   "Datatype.not_Some_eq_D",
   1.150 +   "Set.disjoint_insert_1",
   1.151 +   "Set.disjoint_insert_2",
   1.152 +   "Set.insert_disjoint_1",
   1.153 +   "Set.insert_disjoint_2",
   1.154 +   "Set.singletonD",
   1.155 +   "Set.singletonI",
   1.156 +   "Sum_Type.InlI",
   1.157 +   "Sum_Type.InrI",
   1.158 +   "Set.singleton_insert_inj_eq",
   1.159 +   "Set.singleton_insert_inj_eq'"];
   1.160 +
   1.161 +(*These are the defining properties of min and max, but as they are prolific they
   1.162 +  could be included above.
   1.163 +   "Orderings.max_less_iff_conj",
   1.164 +   "Orderings.min_less_iff_conj",
   1.165 +   "Orderings.min_max.below_inf.below_inf_conv",
   1.166 +   "Orderings.min_max.below_sup.above_sup_conv",
   1.167 +*)
   1.168 +
   1.169  val relevant = ref 0;  (*Relevance filtering is off by default*)
   1.170  
   1.171  (*The "name" of a theorem is its statement, if nothing else is available.*)
   1.172 @@ -153,11 +177,14 @@
   1.173        Polyhash.insert ht (x^"_iff2", ()); 
   1.174        Polyhash.insert ht (x^"_dest", ())); 
   1.175  
   1.176 -fun make_suffix_test xs = 
   1.177 +fun make_banned_test xs = 
   1.178    let val ht = Polyhash.mkTable (Polyhash.hash_string, op =)
   1.179                                  (6000, HASH_STRING)
   1.180 -      fun suffixed s = isSome (Polyhash.peek ht s)
   1.181 -  in  app (insert_suffixed_names ht) xs; suffixed  end;
   1.182 +      fun banned s = isSome (Polyhash.peek ht s)
   1.183 +  in  app (fn x => Polyhash.insert ht (x,())) (!blacklist);
   1.184 +      app (insert_suffixed_names ht) (!blacklist @ xs); 
   1.185 +      banned
   1.186 +  end;
   1.187  
   1.188  (*Create a hash table for clauses, of the given size*)
   1.189  fun mk_clause_table n =
   1.190 @@ -182,8 +209,8 @@
   1.191  		    (ReduceAxiomsN.relevant_filter (!relevant) goal
   1.192  		      (ResAxioms.simpset_rules_of_ctxt ctxt))
   1.193  	    else []
   1.194 -      val suffixed = make_suffix_test (map #1 (claset_thms@simpset_thms))
   1.195 -      fun ok (a,_) = not (suffixed a)
   1.196 +      val banned = make_banned_test (map #1 (claset_thms@simpset_thms))
   1.197 +      fun ok (a,_) = not (banned a)
   1.198        val claset_cls_thms = ResAxioms.clausify_rules_pairs (filter ok claset_thms)
   1.199        val simpset_cls_thms = ResAxioms.clausify_rules_pairs (filter ok simpset_thms)
   1.200        val cls_thms_list = make_unique (mk_clause_table 2200)