Added filter_prems_tac
authornipkow
Thu Nov 26 12:18:08 1998 +0100 (1998-11-26)
changeset 59746acf3ff0f486
parent 5973 040f6d2af50d
child 5975 cd19eaa90f45
Added filter_prems_tac
src/Pure/tactic.ML
     1.1 --- a/src/Pure/tactic.ML	Wed Nov 25 20:55:25 1998 +0100
     1.2 +++ b/src/Pure/tactic.ML	Thu Nov 26 12:18:08 1998 +0100
     1.3 @@ -40,7 +40,8 @@
     1.4    val eq_assume_tac	: int -> tactic   
     1.5    val ematch_tac	: thm list -> int -> tactic
     1.6    val eresolve_tac	: thm list -> int -> tactic
     1.7 -  val eres_inst_tac	: (string*string)list -> thm -> int -> tactic   
     1.8 +  val eres_inst_tac	: (string*string)list -> thm -> int -> tactic
     1.9 +  val filter_prems_tac  : (term -> bool) -> int -> tactic  
    1.10    val filter_thms	: (term*term->bool) -> int*term*thm list -> thm list
    1.11    val filt_resolve_tac	: thm list -> int -> int -> tactic
    1.12    val flexflex_tac	: tactic
    1.13 @@ -563,6 +564,20 @@
    1.14  fun rotate_tac 0 i = all_tac
    1.15    | rotate_tac k i = PRIMITIVE (rotate_rule k i);
    1.16  
    1.17 +(* remove premises that do not satisfy p; fails if all prems satisfy p *)
    1.18 +fun filter_prems_tac p =
    1.19 +  let fun Then None tac = Some tac
    1.20 +        | Then (Some tac) tac' = Some(tac THEN' tac');
    1.21 +      fun thins ((tac,n),H) =
    1.22 +        if p H then (tac,n+1)
    1.23 +        else (Then tac (rotate_tac n THEN' etac thin_rl),0);
    1.24 +  in SUBGOAL(fn (subg,n) =>
    1.25 +       let val Hs = Logic.strip_assums_hyp subg
    1.26 +       in case fst(foldl thins ((None,0),Hs)) of
    1.27 +            None => no_tac | Some tac => tac n
    1.28 +       end)
    1.29 +  end;
    1.30 +
    1.31  end;
    1.32  
    1.33  open Tactic;