# HG changeset patch
# User nipkow
# Date 912079088 -3600
# Node ID 6acf3ff0f4865fac7525b58358d51e1a527a4489
# Parent  040f6d2af50d28bacbbc7d1fa588721619021538
Added filter_prems_tac

diff -r 040f6d2af50d -r 6acf3ff0f486 src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Wed Nov 25 20:55:25 1998 +0100
+++ b/src/Pure/tactic.ML	Thu Nov 26 12:18:08 1998 +0100
@@ -40,7 +40,8 @@
   val eq_assume_tac	: int -> tactic   
   val ematch_tac	: thm list -> int -> tactic
   val eresolve_tac	: thm list -> int -> tactic
-  val eres_inst_tac	: (string*string)list -> thm -> int -> tactic   
+  val eres_inst_tac	: (string*string)list -> thm -> int -> tactic
+  val filter_prems_tac  : (term -> bool) -> int -> tactic  
   val filter_thms	: (term*term->bool) -> int*term*thm list -> thm list
   val filt_resolve_tac	: thm list -> int -> int -> tactic
   val flexflex_tac	: tactic
@@ -563,6 +564,20 @@
 fun rotate_tac 0 i = all_tac
   | rotate_tac k i = PRIMITIVE (rotate_rule k i);
 
+(* remove premises that do not satisfy p; fails if all prems satisfy p *)
+fun filter_prems_tac p =
+  let fun Then None tac = Some tac
+        | Then (Some tac) tac' = Some(tac THEN' tac');
+      fun thins ((tac,n),H) =
+        if p H then (tac,n+1)
+        else (Then tac (rotate_tac n THEN' etac thin_rl),0);
+  in SUBGOAL(fn (subg,n) =>
+       let val Hs = Logic.strip_assums_hyp subg
+       in case fst(foldl thins ((None,0),Hs)) of
+            None => no_tac | Some tac => tac n
+       end)
+  end;
+
 end;
 
 open Tactic;