src/HOL/Tools/res_atp.ML
changeset 22382 dbf09db0a40d
parent 22217 a5d983f7113f
child 22422 ee19cdb07528
     1.1 --- a/src/HOL/Tools/res_atp.ML	Fri Mar 02 12:35:20 2007 +0100
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Fri Mar 02 12:37:34 2007 +0100
     1.3 @@ -311,7 +311,7 @@
     1.4  (*The rule subsetI is frequently omitted by the relevance filter.*)
     1.5  val whitelist = ref [subsetI];
     1.6  
     1.7 -(*Names of theorems (not theorem lists! See multi_blacklist below) to be banned.
     1.8 +(*Names of theorems and theorem lists to be blacklisted.
     1.9  
    1.10    These theorems typically produce clauses that are prolific (match too many equality or
    1.11    membership literals) and relate to seldom-used facts. Some duplicate other rules.
    1.12 @@ -418,6 +418,7 @@
    1.13     "Ring_and_Field.less_divide_eq_1_neg", (*obscure and prolific*)
    1.14     "Ring_and_Field.less_divide_eq_1_pos", (*obscure and prolific*)
    1.15     "Ring_and_Field.one_eq_divide_iff",  (*duplicate by symmetry*)
    1.16 +   "Set.ball_simps", "Set.bex_simps",  (*quantifier rewriting: useless*)
    1.17     "Set.Collect_bex_eq",   (*involves an existential quantifier*)
    1.18     "Set.Collect_ex_eq",   (*involves an existential quantifier*)
    1.19     "Set.Diff_eq_empty_iff", (*redundant with paramodulation*)
    1.20 @@ -426,7 +427,9 @@
    1.21     "Set.full_SetCompr_eq",   (*involves an existential quantifier*)
    1.22     "Set.image_Collect",      (*involves Collect and a boolean variable...*)
    1.23     "Set.image_def",          (*involves an existential quantifier*)
    1.24 +   "Set.disjoint_insert", "Set.insert_disjoint",
    1.25     "Set.Int_UNIV",  (*redundant with paramodulation*)
    1.26 +   "Set.Inter_UNIV_conv",
    1.27     "Set.Inter_iff", (*We already have InterI, InterE*)
    1.28     "Set.psubsetE",    (*too prolific and obscure*)
    1.29     "Set.psubsetI",
    1.30 @@ -444,7 +447,6 @@
    1.31     "SetInterval.greaterThanLessThan_iff", (*obscure and prolific*)
    1.32     "SetInterval.ivl_subset"];  (*excessive case analysis*)
    1.33  
    1.34 -
    1.35  (*These might be prolific but are probably OK, and min and max are basic.
    1.36     "Orderings.max_less_iff_conj",
    1.37     "Orderings.min_less_iff_conj",
    1.38 @@ -459,7 +461,7 @@
    1.39  
    1.40  (*Hashing to detect duplicate and variant clauses, e.g. from the [iff] attribute*)
    1.41  
    1.42 -exception HASH_CLAUSE and HASH_STRING;
    1.43 +fun setinsert (x,s) = Symtab.update (x,()) s;
    1.44  
    1.45  (*Reject theorems with names like "List.filter.filter_list_def" or
    1.46    "Accessible_Part.acc.defs", as these are definitions arising from packages.*)
    1.47 @@ -471,13 +473,6 @@
    1.48       String.isSuffix "_def" a  orelse  String.isSuffix "_defs" a
    1.49    end;
    1.50  
    1.51 -fun make_banned_test xs =
    1.52 -  let val ht = Polyhash.mkTable (Polyhash.hash_string, op =) (6000, HASH_STRING)
    1.53 -      fun banned s = isSome (Polyhash.peek ht s) orelse is_package_def s
    1.54 -  in  app (fn x => Polyhash.insert ht (x,())) (!blacklist);
    1.55 -      banned
    1.56 -  end;
    1.57 -
    1.58  (** a hash function from Term.term to int, and also a hash table **)
    1.59  val xor_words = List.foldl Word.xorb 0w0;
    1.60  
    1.61 @@ -495,6 +490,8 @@
    1.62  
    1.63  fun equal_thm (thm1,thm2) = Term.aconv(prop_of thm1, prop_of thm2);
    1.64  
    1.65 +exception HASH_CLAUSE;
    1.66 +
    1.67  (*Create a hash table for clauses, of the given size*)
    1.68  fun mk_clause_table n =
    1.69        Polyhash.mkTable (hash_term o prop_of, equal_thm)
    1.70 @@ -526,36 +523,52 @@
    1.71    white_cls @ (ReduceAxiomsN.relevance_filter thy cls_thms goals);
    1.72  
    1.73  fun all_valid_thms ctxt =
    1.74 -  PureThy.thms_containing (ProofContext.theory_of ctxt) ([], []) @
    1.75 -  filter (ProofContext.valid_thms ctxt)
    1.76 -    (FactIndex.find (ProofContext.fact_index_of ctxt) ([], []));
    1.77 +  let
    1.78 +    val banned_tab = foldl setinsert Symtab.empty (!blacklist) 
    1.79 +    fun blacklisted s = !run_blacklist_filter andalso
    1.80 +                        (isSome (Symtab.lookup banned_tab s) orelse is_package_def s)
    1.81 +
    1.82 +    fun extern_valid space (name, ths) =
    1.83 +      let
    1.84 +        val is_valid = ProofContext.valid_thms ctxt;
    1.85 +        val xname = NameSpace.extern space name;
    1.86 +      in
    1.87 +        if blacklisted name then I
    1.88 +        else if is_valid (xname, ths) then cons (xname, ths)
    1.89 +        else if is_valid (name, ths) then cons (name, ths)
    1.90 +        else I
    1.91 +      end;
    1.92 +    val thy = ProofContext.theory_of ctxt;
    1.93 +    val all_thys = thy :: Theory.ancestors_of thy;
    1.94 +
    1.95 +    fun dest_valid (space, tab) = Symtab.fold (extern_valid space) tab [];
    1.96 +  in
    1.97 +    maps (dest_valid o PureThy.theorems_of) all_thys @
    1.98 +    fold (extern_valid (#1 (ProofContext.theorems_of ctxt)))
    1.99 +      (FactIndex.find (ProofContext.fact_index_of ctxt) ([], [])) []
   1.100 +  end;
   1.101  
   1.102  fun multi_name a (th, (n,pairs)) =
   1.103    (n+1, (a ^ "(" ^ Int.toString n ^ ")", th) :: pairs)
   1.104  
   1.105 -fun add_multi_names_aux ((a, []), pairs) = pairs
   1.106 -  | add_multi_names_aux ((a, [th]), pairs) = (a,th)::pairs
   1.107 -  | add_multi_names_aux ((a, ths), pairs) = #2 (foldl (multi_name a) (1,pairs) ths);
   1.108 -
   1.109 -val multi_blacklist =
   1.110 -  ["Set.ball_simps", "Set.bex_simps",  (*quantifier rewriting: useless*)
   1.111 -   "Set.disjoint_insert", "Set.insert_disjoint", "Set.Inter_UNIV_conv"];
   1.112 +fun add_single_names ((a, []), pairs) = pairs
   1.113 +  | add_single_names ((a, [th]), pairs) = (a,th)::pairs
   1.114 +  | add_single_names ((a, ths), pairs) = #2 (foldl (multi_name a) (1,pairs) ths);
   1.115  
   1.116  val multi_base_blacklist =
   1.117    ["defs","select_defs","update_defs","induct","inducts","split","splits","split_asm"];
   1.118  
   1.119 -(*Ignore blacklisted theorem lists*)
   1.120 +(*Ignore blacklisted basenames*)
   1.121  fun add_multi_names ((a, ths), pairs) =
   1.122 -  if a mem_string multi_blacklist orelse (Sign.base_name a) mem_string multi_base_blacklist
   1.123 -  then pairs
   1.124 -  else add_multi_names_aux ((a, ths), pairs);
   1.125 +  if (Sign.base_name a) mem_string multi_base_blacklist  then pairs
   1.126 +  else add_single_names ((a, ths), pairs);
   1.127  
   1.128  fun is_multi (a, ths) = length ths > 1 orelse String.isSuffix ".axioms" a;
   1.129  
   1.130  (*The single theorems go BEFORE the multiple ones*)
   1.131  fun name_thm_pairs ctxt =
   1.132    let val (mults,singles) = List.partition is_multi (all_valid_thms ctxt)
   1.133 -  in  foldl add_multi_names (foldl add_multi_names [] mults) singles  end;
   1.134 +  in  foldl add_single_names  (foldl add_multi_names [] mults) singles end;
   1.135  
   1.136  fun check_named ("",th) = (warning ("No name for theorem " ^ string_of_thm th); false)
   1.137    | check_named (_,th) = true;
   1.138 @@ -582,32 +595,16 @@
   1.139              val _ = (Output.debug (fn () => "ATP theorems: ");  app display_thm atpset_thms)
   1.140          in  claset_thms @ simpset_thms @ atpset_thms  end
   1.141        val user_rules = filter check_named
   1.142 -                         (map (ResAxioms.pairname)
   1.143 +                         (map ResAxioms.pairname
   1.144                             (if null user_thms then !whitelist else user_thms))
   1.145    in
   1.146        (filter check_named included_thms, user_rules)
   1.147    end;
   1.148  
   1.149 -(*Remove lemmas that are banned from the backlist. Also remove duplicates. *)
   1.150 -fun blacklist_filter ths =
   1.151 -  if !run_blacklist_filter then
   1.152 -      let val banned = make_banned_test (map #1 ths)
   1.153 -          fun ok (a,_) = not (banned a)
   1.154 -          val (good,bad) = List.partition ok ths
   1.155 -      in
   1.156 -        Output.debug (fn () => "blacklist filter gets " ^ Int.toString (length ths) ^ " theorems");
   1.157 -        Output.debug (fn () => "filtered: " ^ space_implode ", " (map #1 bad));
   1.158 -        Output.debug (fn () => "...and returns " ^ Int.toString (length good));
   1.159 -        good 
   1.160 -      end
   1.161 -  else ths;
   1.162 -
   1.163  (***************************************************************)
   1.164  (* Type Classes Present in the Axiom or Conjecture Clauses     *)
   1.165  (***************************************************************)
   1.166  
   1.167 -fun setinsert (x,s) = Symtab.update (x,()) s;
   1.168 -
   1.169  fun add_classes (sorts, cset) = foldl setinsert cset (List.concat sorts);
   1.170  
   1.171  (*Remove this trivial type class*)
   1.172 @@ -654,8 +651,8 @@
   1.173  val linkup_logic_mode = ref Auto;
   1.174  
   1.175  (*Ensures that no higher-order theorems "leak out"*)
   1.176 -fun restrict_to_logic logic cls =
   1.177 -  if is_fol_logic logic then filter (Meson.is_fol_term o prop_of o fst) cls
   1.178 +fun restrict_to_logic thy logic cls =
   1.179 +  if is_fol_logic logic then filter (Meson.is_fol_term thy o prop_of o fst) cls
   1.180                          else cls;
   1.181  
   1.182  (**** Predicates to detect unwanted clauses (prolific or likely to cause unsoundness) ****)
   1.183 @@ -725,17 +722,17 @@
   1.184          val hyp_cls = cnf_hyps_thms ctxt
   1.185          val goal_cls = conj_cls@hyp_cls
   1.186          val goal_tms = map prop_of goal_cls
   1.187 +        val thy = ProofContext.theory_of ctxt
   1.188          val logic = case mode of
   1.189                              Auto => problem_logic_goals [goal_tms]
   1.190                            | Fol => FOL
   1.191                            | Hol => HOL
   1.192          val (included_thms,user_rules) = get_clasimp_atp_lemmas ctxt user_thms
   1.193 -        val cla_simp_atp_clauses = included_thms |> blacklist_filter
   1.194 +        val cla_simp_atp_clauses = included_thms 
   1.195                                       |> ResAxioms.cnf_rules_pairs |> make_unique
   1.196 -                                     |> restrict_to_logic logic
   1.197 +                                     |> restrict_to_logic thy logic
   1.198                                       |> remove_unwanted_clauses
   1.199          val user_cls = ResAxioms.cnf_rules_pairs user_rules
   1.200 -        val thy = ProofContext.theory_of ctxt
   1.201          val axclauses = make_unique (get_relevant_clauses thy cla_simp_atp_clauses user_cls goal_tms)
   1.202          val subs = tfree_classes_of_terms goal_tms
   1.203          and axtms = map (prop_of o #1) axclauses
   1.204 @@ -840,9 +837,8 @@
   1.205                | Fol => FOL
   1.206                | Hol => HOL
   1.207        val (included_thms,white_thms) = get_clasimp_atp_lemmas ctxt []
   1.208 -      val included_cls = included_thms |> blacklist_filter
   1.209 -                                       |> ResAxioms.cnf_rules_pairs |> make_unique
   1.210 -                                       |> restrict_to_logic logic
   1.211 +      val included_cls = included_thms |> ResAxioms.cnf_rules_pairs |> make_unique
   1.212 +                                       |> restrict_to_logic thy logic
   1.213                                         |> remove_unwanted_clauses
   1.214        val _ = Output.debug (fn () => "included clauses = " ^ Int.toString(length included_cls))
   1.215        val white_cls = ResAxioms.cnf_rules_pairs white_thms