# HG changeset patch
# User paulson
# Date 826911548 -3600
# Node ID bc902840aab572d066ca394a8c9d6242a4fe6826
# Parent  97a305db0c9e8979227dd64998fa69f696ec6ef8
Search tacticals moved to search.ML

diff -r 97a305db0c9e -r bc902840aab5 src/Pure/tctical.ML
--- a/src/Pure/tctical.ML	Fri Mar 15 18:38:24 1996 +0100
+++ b/src/Pure/tctical.ML	Fri Mar 15 18:39:08 1996 +0100
@@ -6,7 +6,7 @@
 Tacticals
 *)
 
-infix 1 THEN THEN' THEN_BEST_FIRST;
+infix 1 THEN THEN';
 infix 0 ORELSE APPEND INTLEAVE ORELSE' APPEND' INTLEAVE';
 
 infix 0 THEN_ELSE;
@@ -19,13 +19,8 @@
   val ALLGOALS		: (int -> tactic) -> tactic   
   val APPEND		: tactic * tactic -> tactic
   val APPEND'		: ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
-  val BEST_FIRST	: (thm -> bool) * (thm -> int) -> tactic -> tactic
-  val BREADTH_FIRST	: (thm -> bool) -> tactic -> tactic
   val CHANGED		: tactic -> tactic
   val COND		: (thm -> bool) -> tactic -> tactic -> tactic   
-  val DEPTH_FIRST	: (thm -> bool) -> tactic -> tactic
-  val DEPTH_SOLVE	: tactic -> tactic
-  val DEPTH_SOLVE_1	: tactic -> tactic
   val DETERM		: tactic -> tactic
   val EVERY		: tactic list -> tactic   
   val EVERY'		: ('a -> tactic) list -> 'a -> tactic
@@ -36,8 +31,6 @@
   val FIRST1		: (int -> tactic) list -> tactic
   val FIRSTGOAL		: (int -> tactic) -> tactic
   val goals_limit	: int ref
-  val has_fewer_prems	: int -> thm -> bool   
-  val IF_UNSOLVED	: tactic -> tactic
   val INTLEAVE		: tactic * tactic -> tactic
   val INTLEAVE'		: ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
   val METAHYPS		: (thm list -> tactic) -> int -> tactic
@@ -63,13 +56,9 @@
   val suppress_tracing	: bool ref
   val THEN		: tactic * tactic -> tactic
   val THEN'		: ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
-  val THEN_BEST_FIRST	: tactic * ((thm->bool) * (thm->int) * tactic) 
-			  -> tactic
   val THEN_ELSE		: tactic * (tactic*tactic) -> tactic
   val traced_tac	: (thm -> (thm * thm Sequence.seq) option) -> tactic
   val tracify		: bool ref -> tactic -> thm -> thm Sequence.seq
-  val trace_BEST_FIRST	: bool ref
-  val trace_DEPTH_FIRST	: bool ref
   val trace_REPEAT	: bool ref
   val TRY		: tactic -> tactic
   val TRYALL		: (int -> tactic) -> tactic   
@@ -201,8 +190,6 @@
 
 (*Tracing flags*)
 val trace_REPEAT= ref false
-and trace_DEPTH_FIRST = ref false
-and trace_BEST_FIRST = ref false
 and suppress_tracing = ref false;
 
 (*Handle all tracing commands for current state and tactic *)
@@ -272,95 +259,6 @@
 fun REPEAT1 tac = tac THEN REPEAT tac;
 
 
-(** Search tacticals **)
-
-(*Searches until "satp" reports proof tree as satisfied.
-  Suppresses duplicate solutions to minimize search space.*)
-fun DEPTH_FIRST satp tac = 
- let val tac = tracify trace_DEPTH_FIRST tac
-     fun depth used [] = None
-       | depth used (q::qs) =
-	  case Sequence.pull q of
-	      None         => depth used qs
-	    | Some(st,stq) => 
-		if satp st andalso not (gen_mem eq_thm (st, used))
-		then Some(st, Sequence.seqof
-			         (fn()=> depth (st::used) (stq::qs)))
-		else depth used (tac st :: stq :: qs)
-  in  traced_tac (fn st => depth [] ([Sequence.single st]))  end;
-
-
-
-(*Predicate: Does the rule have fewer than n premises?*)
-fun has_fewer_prems n rule = (nprems_of rule < n);
-
-(*Apply a tactic if subgoals remain, else do nothing.*)
-val IF_UNSOLVED = COND (has_fewer_prems 1) all_tac;
-
-(*Tactical to reduce the number of premises by 1.
-  If no subgoals then it must fail! *)
-fun DEPTH_SOLVE_1 tac = STATE
- (fn st => 
-    (case nprems_of st of
-	0 => no_tac
-      | n => DEPTH_FIRST (has_fewer_prems n) tac));
-
-(*Uses depth-first search to solve ALL subgoals*)
-val DEPTH_SOLVE = DEPTH_FIRST (has_fewer_prems 1);
-
-(*** Best-first search ***)
-
-(*Insertion into priority queue of states *)
-fun insert (nth: int*thm, []) = [nth]
-  | insert ((m,th), (n,th')::nths) = 
-      if  n<m then (n,th') :: insert ((m,th), nths)
-      else if  n=m andalso eq_thm(th,th')
-              then (n,th')::nths
-              else (m,th)::(n,th')::nths;
-
-(*For creating output sequence*)
-fun some_of_list []     = None
-  | some_of_list (x::l) = Some (x, Sequence.seqof (fn () => some_of_list l));
-
-
-(* Best-first search for a state that satisfies satp (incl initial state)
-  Function sizef estimates size of problem remaining (smaller means better).
-  tactic tac0 sets up the initial priority queue, which is searched by tac. *)
-fun tac0 THEN_BEST_FIRST (satp, sizef, tac1) = 
-  let val tac = tracify trace_BEST_FIRST tac1
-      fun pairsize th = (sizef th, th);
-      fun bfs (news,nprfs) =
-	   (case  partition satp news  of
-		([],nonsats) => next(foldr insert
-					(map pairsize nonsats, nprfs)) 
-	      | (sats,_)  => some_of_list sats)
-      and next [] = None
-        | next ((n,prf)::nprfs) =
-	    (if !trace_BEST_FIRST 
-	       then writeln("state size = " ^ string_of_int n ^ 
-		         "  queue length =" ^ string_of_int (length nprfs))  
-               else ();
-	     bfs (Sequence.list_of_s (tac prf), nprfs))
-      fun btac st = bfs (Sequence.list_of_s (tac0 st),  [])
-  in traced_tac btac end;
-
-(*Ordinary best-first search, with no initial tactic*)
-fun BEST_FIRST (satp,sizef) tac = all_tac THEN_BEST_FIRST (satp,sizef,tac);
-
-(*Breadth-first search to satisfy satpred (including initial state) 
-  SLOW -- SHOULD NOT USE APPEND!*)
-fun BREADTH_FIRST satpred tac = 
-  let val tacf = Sequence.list_of_s o tac;
-      fun bfs prfs =
-	 (case  partition satpred prfs  of
-	      ([],[]) => []
-	    | ([],nonsats) => 
-		  (prs("breadth=" ^ string_of_int(length nonsats) ^ "\n");
-		   bfs (flat (map tacf nonsats)))
-	    | (sats,_)  => sats)
-  in (fn st => Sequence.s_of_list (bfs [st])) end;
-
-
 (** Filtering tacticals **)
 
 (*Returns all states satisfying the predicate*)