# HG changeset patch
# User blanchet
# Date 1406283648 -7200
# Node ID 47336af5d2b26a3e6963a4eda817af8e537c6b2b
# Parent  3bad83e01ec2d26398baa731dd5927bc34f903b3
faster minimization by not adding facts that are already in the simpset

diff -r 3bad83e01ec2 -r 47336af5d2b2 src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML	Fri Jul 25 11:31:20 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML	Fri Jul 25 12:20:48 2014 +0200
@@ -21,6 +21,7 @@
 structure Sledgehammer_Isar_Minimize : SLEDGEHAMMER_ISAR_MINIMIZE =
 struct
 
+open Sledgehammer_Util
 open Sledgehammer_Proof_Methods
 open Sledgehammer_Isar_Proof
 open Sledgehammer_Isar_Preplay
@@ -35,10 +36,12 @@
 val slack = seconds 0.025
 
 fun minimize_isar_step_dependencies ctxt preplay_data
-      (step as Prove (qs, xs, l, t, subproofs, (lfs0, gfs0), meths as meth :: _, comment)) =
+      (step as Prove (qs, xs, l, t, subproofs, (lfs0, gfs00), meths as meth :: _, comment)) =
     (case Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth) of
       Played time =>
       let
+        val gfs0 = filter (influence_proof_method ctxt meth o thms_of_name ctxt) gfs00
+
         fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, (lfs, gfs), meths, comment)
 
         fun minimize_facts _ min_facts [] time = (min_facts, time)
diff -r 3bad83e01ec2 -r 47336af5d2b2 src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Fri Jul 25 11:31:20 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Fri Jul 25 12:20:48 2014 +0200
@@ -36,6 +36,7 @@
   val is_proof_method_direct : proof_method -> bool
   val string_of_proof_method : Proof.context -> string list -> proof_method -> string
   val tac_of_proof_method : Proof.context -> thm list * thm list -> proof_method -> int -> tactic
+  val influence_proof_method : Proof.context -> proof_method -> thm list -> bool
   val string_of_play_outcome : play_outcome -> string
   val play_outcome_ord : play_outcome * play_outcome -> order
   val one_line_proof_text : Proof.context -> int -> one_line_params -> string
@@ -136,6 +137,16 @@
     | Presburger_Method => Cooper.tac true [] [] ctxt
     | Algebra_Method => Groebner.algebra_tac [] [] ctxt))
 
+val simp_based_methods =
+  [Simp_Method, Simp_Size_Method, Auto_Method, Fastforce_Method, Force_Method]
+
+fun influence_proof_method ctxt meth ths =
+  not (member (op =) simp_based_methods meth) orelse
+  let val ctxt' = silence_methods ctxt in
+    (* unfortunate pointer comparison -- but it's always safe to consider a theorem useful *)
+    not (pointer_eq (ctxt' addsimps ths, ctxt'))
+  end
+
 fun string_of_play_outcome (Played time) = string_of_ext_time (false, time)
   | string_of_play_outcome (Play_Timed_Out time) =
     if time = Time.zeroTime then "" else string_of_ext_time (true, time) ^ ", timed out"