src/Pure/search.ML

 
 infix 1 THEN_MAYBE THEN_MAYBE';
 
 signature SEARCH =
   sig
+  val DEEPEN  	        : int*int -> (int->int->tactic) -> int -> int -> tactic
+
   val THEN_MAYBE	: tactic * tactic -> tactic
   val THEN_MAYBE'	: ('a -> tactic) * ('a -> tactic) -> ('a -> tactic)
 
   val trace_DEPTH_FIRST	: bool ref
   val DEPTH_FIRST	: (thm -> bool) -> tactic -> tactic

 (*Uses depth-first search to solve ALL subgoals*)
 val DEPTH_SOLVE = DEPTH_FIRST (has_fewer_prems 1);
 
 
 
-(**** Iterative deepening ****)
+(**** Iterative deepening with pruning ****)
 
 fun has_vars (Var _) = true
   | has_vars (Abs (_,_,t)) = has_vars t
   | has_vars (f$t) = has_vars f orelse has_vars t
   | has_vars _ = false;

   in depth (0,5) [] end);
 
 val ITER_DEEPEN = THEN_ITER_DEEPEN all_tac;
 
 
+(*Simple iterative deepening tactical.  It merely "deepens" any search tactic
+  using increment "inc" up to limit "lim". *)
+fun DEEPEN (inc,lim) tacf m i = 
+  let fun dpn m = STATE(fn state => 
+			if has_fewer_prems i state then no_tac
+			else if m>lim then 
+			     (writeln "Giving up..."; no_tac)
+			else (writeln ("Depth = " ^ string_of_int m);
+			      tacf m i  ORELSE  dpn (m+inc)))
+  in  dpn m  end;
+
 (*** Best-first search ***)
 
 val trace_BEST_FIRST = ref false;
 
 (*Insertion into priority queue of states *)