# HG changeset patch
# User blanchet
# Date 1343050350 -7200
# Node ID 159e320ef851b5ce9a7ba504c4bfed285423db33
# Parent  67a6bcbd358728000818ed8a0e252eaa04eb80c5
identified "evil" theories for MaSh -- this is rather ad hoc, but so is MaSh anyway

diff -r 67a6bcbd3587 -r 159e320ef851 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Mon Jul 23 15:32:30 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Mon Jul 23 15:32:30 2012 +0200
@@ -49,9 +49,6 @@
    del : (Facts.ref * Attrib.src list) list,
    only : bool}
 
-val sledgehammer_prefixes =
-  ["ATP", "Meson", "Metis", "Sledgehammer"] |> map (suffix Long_Name.separator)
-
 (* experimental features *)
 val ignore_no_atp =
   Attrib.setup_config_bool @{binding sledgehammer_ignore_no_atp} (K false)
@@ -147,10 +144,11 @@
 fun multi_base_blacklist ctxt ho_atp =
   ["defs", "select_defs", "update_defs", "split", "splits", "split_asm",
    "cases", "ext_cases", "eq.simps", "eq.refl", "nchotomy", "case_cong",
-   "weak_case_cong"]
+   "weak_case_cong", "nibble_pair_of_char_simps", "nibble.simps",
+   "nibble.distinct"]
   |> not (ho_atp orelse (Config.get ctxt instantiate_inducts)) ?
         append ["induct", "inducts"]
-  |> map (prefix ".")
+  |> map (prefix Long_Name.separator)
 
 val max_lambda_nesting = 3 (*only applies if not ho_atp*)
 
@@ -182,6 +180,11 @@
   apply_depth t > max_apply_depth orelse
   (not ho_atp andalso formula_has_too_many_lambdas [] t)
 
+(* These theories contain auxiliary facts that could positively confuse
+   Sledgehammer if they were included. *)
+val sledgehammer_prefixes =
+  ["ATP", "Meson", "Metis", "Sledgehammer"] |> map (suffix Long_Name.separator)
+
 val exists_sledgehammer_const =
   exists_Const (fn (s, _) =>
       exists (fn pref => String.isPrefix pref s) sledgehammer_prefixes)
diff -r 67a6bcbd3587 -r 159e320ef851 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Jul 23 15:32:30 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Jul 23 15:32:30 2012 +0200
@@ -316,7 +316,7 @@
 
 (* Too many dependencies is a sign that a decision procedure is at work. There
    isn't much too learn from such proofs. *)
-val max_dependencies = 15
+val max_dependencies = 20
 val atp_dependency_default_max_fact = 50
 
 (* "type_definition_xxx" facts are characterized by their use of "CollectI". *)
@@ -689,6 +689,14 @@
           (true, "")
         end)
 
+val evil_theories =
+  ["Code_Evaluation", "DSequence", "Enum", "Lazy_Sequence", "Nitpick",
+   "New_DSequence", "New_Random_Sequence", "Quickcheck",
+   "Quickcheck_Exhaustive", "Quickcheck_Narrowing", "Random_Sequence", "SMT"]
+
+fun fact_has_evil_theory (_, th) =
+  member (op =) evil_theories (Context.theory_name (theory_of_thm th))
+
 fun sendback sub =
   Markup.markup Isabelle_Markup.sendback (sledgehammerN ^ " " ^ sub)
 
@@ -703,7 +711,8 @@
       Time.+ (Timer.checkRealTimer timer, commit_timeout)
     val {fact_G} = mash_get ctxt
     val (old_facts, new_facts) =
-      facts |> List.partition (is_fact_in_graph fact_G)
+      facts |> filter_out fact_has_evil_theory
+            |> List.partition (is_fact_in_graph fact_G)
             ||> sort (thm_ord o pairself snd)
   in
     if null new_facts andalso (not atp orelse null old_facts) then