src/HOL/Tools/res_atp.ML
changeset 22382 dbf09db0a40d
parent 22217 a5d983f7113f
child 22422 ee19cdb07528
--- a/src/HOL/Tools/res_atp.ML	Fri Mar 02 12:35:20 2007 +0100
+++ b/src/HOL/Tools/res_atp.ML	Fri Mar 02 12:37:34 2007 +0100
@@ -311,7 +311,7 @@
 (*The rule subsetI is frequently omitted by the relevance filter.*)
 val whitelist = ref [subsetI];
 
-(*Names of theorems (not theorem lists! See multi_blacklist below) to be banned.
+(*Names of theorems and theorem lists to be blacklisted.
 
   These theorems typically produce clauses that are prolific (match too many equality or
   membership literals) and relate to seldom-used facts. Some duplicate other rules.
@@ -418,6 +418,7 @@
    "Ring_and_Field.less_divide_eq_1_neg", (*obscure and prolific*)
    "Ring_and_Field.less_divide_eq_1_pos", (*obscure and prolific*)
    "Ring_and_Field.one_eq_divide_iff",  (*duplicate by symmetry*)
+   "Set.ball_simps", "Set.bex_simps",  (*quantifier rewriting: useless*)
    "Set.Collect_bex_eq",   (*involves an existential quantifier*)
    "Set.Collect_ex_eq",   (*involves an existential quantifier*)
    "Set.Diff_eq_empty_iff", (*redundant with paramodulation*)
@@ -426,7 +427,9 @@
    "Set.full_SetCompr_eq",   (*involves an existential quantifier*)
    "Set.image_Collect",      (*involves Collect and a boolean variable...*)
    "Set.image_def",          (*involves an existential quantifier*)
+   "Set.disjoint_insert", "Set.insert_disjoint",
    "Set.Int_UNIV",  (*redundant with paramodulation*)
+   "Set.Inter_UNIV_conv",
    "Set.Inter_iff", (*We already have InterI, InterE*)
    "Set.psubsetE",    (*too prolific and obscure*)
    "Set.psubsetI",
@@ -444,7 +447,6 @@
    "SetInterval.greaterThanLessThan_iff", (*obscure and prolific*)
    "SetInterval.ivl_subset"];  (*excessive case analysis*)
 
-
 (*These might be prolific but are probably OK, and min and max are basic.
    "Orderings.max_less_iff_conj",
    "Orderings.min_less_iff_conj",
@@ -459,7 +461,7 @@
 
 (*Hashing to detect duplicate and variant clauses, e.g. from the [iff] attribute*)
 
-exception HASH_CLAUSE and HASH_STRING;
+fun setinsert (x,s) = Symtab.update (x,()) s;
 
 (*Reject theorems with names like "List.filter.filter_list_def" or
   "Accessible_Part.acc.defs", as these are definitions arising from packages.*)
@@ -471,13 +473,6 @@
      String.isSuffix "_def" a  orelse  String.isSuffix "_defs" a
   end;
 
-fun make_banned_test xs =
-  let val ht = Polyhash.mkTable (Polyhash.hash_string, op =) (6000, HASH_STRING)
-      fun banned s = isSome (Polyhash.peek ht s) orelse is_package_def s
-  in  app (fn x => Polyhash.insert ht (x,())) (!blacklist);
-      banned
-  end;
-
 (** a hash function from Term.term to int, and also a hash table **)
 val xor_words = List.foldl Word.xorb 0w0;
 
@@ -495,6 +490,8 @@
 
 fun equal_thm (thm1,thm2) = Term.aconv(prop_of thm1, prop_of thm2);
 
+exception HASH_CLAUSE;
+
 (*Create a hash table for clauses, of the given size*)
 fun mk_clause_table n =
       Polyhash.mkTable (hash_term o prop_of, equal_thm)
@@ -526,36 +523,52 @@
   white_cls @ (ReduceAxiomsN.relevance_filter thy cls_thms goals);
 
 fun all_valid_thms ctxt =
-  PureThy.thms_containing (ProofContext.theory_of ctxt) ([], []) @
-  filter (ProofContext.valid_thms ctxt)
-    (FactIndex.find (ProofContext.fact_index_of ctxt) ([], []));
+  let
+    val banned_tab = foldl setinsert Symtab.empty (!blacklist) 
+    fun blacklisted s = !run_blacklist_filter andalso
+                        (isSome (Symtab.lookup banned_tab s) orelse is_package_def s)
+
+    fun extern_valid space (name, ths) =
+      let
+        val is_valid = ProofContext.valid_thms ctxt;
+        val xname = NameSpace.extern space name;
+      in
+        if blacklisted name then I
+        else if is_valid (xname, ths) then cons (xname, ths)
+        else if is_valid (name, ths) then cons (name, ths)
+        else I
+      end;
+    val thy = ProofContext.theory_of ctxt;
+    val all_thys = thy :: Theory.ancestors_of thy;
+
+    fun dest_valid (space, tab) = Symtab.fold (extern_valid space) tab [];
+  in
+    maps (dest_valid o PureThy.theorems_of) all_thys @
+    fold (extern_valid (#1 (ProofContext.theorems_of ctxt)))
+      (FactIndex.find (ProofContext.fact_index_of ctxt) ([], [])) []
+  end;
 
 fun multi_name a (th, (n,pairs)) =
   (n+1, (a ^ "(" ^ Int.toString n ^ ")", th) :: pairs)
 
-fun add_multi_names_aux ((a, []), pairs) = pairs
-  | add_multi_names_aux ((a, [th]), pairs) = (a,th)::pairs
-  | add_multi_names_aux ((a, ths), pairs) = #2 (foldl (multi_name a) (1,pairs) ths);
-
-val multi_blacklist =
-  ["Set.ball_simps", "Set.bex_simps",  (*quantifier rewriting: useless*)
-   "Set.disjoint_insert", "Set.insert_disjoint", "Set.Inter_UNIV_conv"];
+fun add_single_names ((a, []), pairs) = pairs
+  | add_single_names ((a, [th]), pairs) = (a,th)::pairs
+  | add_single_names ((a, ths), pairs) = #2 (foldl (multi_name a) (1,pairs) ths);
 
 val multi_base_blacklist =
   ["defs","select_defs","update_defs","induct","inducts","split","splits","split_asm"];
 
-(*Ignore blacklisted theorem lists*)
+(*Ignore blacklisted basenames*)
 fun add_multi_names ((a, ths), pairs) =
-  if a mem_string multi_blacklist orelse (Sign.base_name a) mem_string multi_base_blacklist
-  then pairs
-  else add_multi_names_aux ((a, ths), pairs);
+  if (Sign.base_name a) mem_string multi_base_blacklist  then pairs
+  else add_single_names ((a, ths), pairs);
 
 fun is_multi (a, ths) = length ths > 1 orelse String.isSuffix ".axioms" a;
 
 (*The single theorems go BEFORE the multiple ones*)
 fun name_thm_pairs ctxt =
   let val (mults,singles) = List.partition is_multi (all_valid_thms ctxt)
-  in  foldl add_multi_names (foldl add_multi_names [] mults) singles  end;
+  in  foldl add_single_names  (foldl add_multi_names [] mults) singles end;
 
 fun check_named ("",th) = (warning ("No name for theorem " ^ string_of_thm th); false)
   | check_named (_,th) = true;
@@ -582,32 +595,16 @@
             val _ = (Output.debug (fn () => "ATP theorems: ");  app display_thm atpset_thms)
         in  claset_thms @ simpset_thms @ atpset_thms  end
       val user_rules = filter check_named
-                         (map (ResAxioms.pairname)
+                         (map ResAxioms.pairname
                            (if null user_thms then !whitelist else user_thms))
   in
       (filter check_named included_thms, user_rules)
   end;
 
-(*Remove lemmas that are banned from the backlist. Also remove duplicates. *)
-fun blacklist_filter ths =
-  if !run_blacklist_filter then
-      let val banned = make_banned_test (map #1 ths)
-          fun ok (a,_) = not (banned a)
-          val (good,bad) = List.partition ok ths
-      in
-        Output.debug (fn () => "blacklist filter gets " ^ Int.toString (length ths) ^ " theorems");
-        Output.debug (fn () => "filtered: " ^ space_implode ", " (map #1 bad));
-        Output.debug (fn () => "...and returns " ^ Int.toString (length good));
-        good 
-      end
-  else ths;
-
 (***************************************************************)
 (* Type Classes Present in the Axiom or Conjecture Clauses     *)
 (***************************************************************)
 
-fun setinsert (x,s) = Symtab.update (x,()) s;
-
 fun add_classes (sorts, cset) = foldl setinsert cset (List.concat sorts);
 
 (*Remove this trivial type class*)
@@ -654,8 +651,8 @@
 val linkup_logic_mode = ref Auto;
 
 (*Ensures that no higher-order theorems "leak out"*)
-fun restrict_to_logic logic cls =
-  if is_fol_logic logic then filter (Meson.is_fol_term o prop_of o fst) cls
+fun restrict_to_logic thy logic cls =
+  if is_fol_logic logic then filter (Meson.is_fol_term thy o prop_of o fst) cls
                         else cls;
 
 (**** Predicates to detect unwanted clauses (prolific or likely to cause unsoundness) ****)
@@ -725,17 +722,17 @@
         val hyp_cls = cnf_hyps_thms ctxt
         val goal_cls = conj_cls@hyp_cls
         val goal_tms = map prop_of goal_cls
+        val thy = ProofContext.theory_of ctxt
         val logic = case mode of
                             Auto => problem_logic_goals [goal_tms]
                           | Fol => FOL
                           | Hol => HOL
         val (included_thms,user_rules) = get_clasimp_atp_lemmas ctxt user_thms
-        val cla_simp_atp_clauses = included_thms |> blacklist_filter
+        val cla_simp_atp_clauses = included_thms 
                                      |> ResAxioms.cnf_rules_pairs |> make_unique
-                                     |> restrict_to_logic logic
+                                     |> restrict_to_logic thy logic
                                      |> remove_unwanted_clauses
         val user_cls = ResAxioms.cnf_rules_pairs user_rules
-        val thy = ProofContext.theory_of ctxt
         val axclauses = make_unique (get_relevant_clauses thy cla_simp_atp_clauses user_cls goal_tms)
         val subs = tfree_classes_of_terms goal_tms
         and axtms = map (prop_of o #1) axclauses
@@ -840,9 +837,8 @@
               | Fol => FOL
               | Hol => HOL
       val (included_thms,white_thms) = get_clasimp_atp_lemmas ctxt []
-      val included_cls = included_thms |> blacklist_filter
-                                       |> ResAxioms.cnf_rules_pairs |> make_unique
-                                       |> restrict_to_logic logic
+      val included_cls = included_thms |> ResAxioms.cnf_rules_pairs |> make_unique
+                                       |> restrict_to_logic thy logic
                                        |> remove_unwanted_clauses
       val _ = Output.debug (fn () => "included clauses = " ^ Int.toString(length included_cls))
       val white_cls = ResAxioms.cnf_rules_pairs white_thms