src/Pure/search.ML
changeset 3538 ed9de44032e0
parent 2869 acee08856cc9
child 4270 957c887b89b5
equal deleted inserted replaced
3537:79ac9b475621 3538:ed9de44032e0
    64 (*Apply a tactic if subgoals remain, else do nothing.*)
    64 (*Apply a tactic if subgoals remain, else do nothing.*)
    65 val IF_UNSOLVED = COND (has_fewer_prems 1) all_tac;
    65 val IF_UNSOLVED = COND (has_fewer_prems 1) all_tac;
    66 
    66 
    67 (*Execute tac1, but only execute tac2 if there are at least as many subgoals
    67 (*Execute tac1, but only execute tac2 if there are at least as many subgoals
    68   as before.  This ensures that tac2 is only applied to an outcome of tac1.*)
    68   as before.  This ensures that tac2 is only applied to an outcome of tac1.*)
    69 fun tac1 THEN_MAYBE tac2 = STATE
    69 fun (tac1 THEN_MAYBE tac2) st = 
    70     (fn st => tac1  THEN  
    70     (tac1  THEN  COND (has_fewer_prems (nprems_of st)) all_tac tac2)  st;
    71 	 COND (has_fewer_prems (nprems_of st)) all_tac tac2);
       
    72 
    71 
    73 fun (tac1 THEN_MAYBE' tac2) x = tac1 x THEN_MAYBE tac2 x;
    72 fun (tac1 THEN_MAYBE' tac2) x = tac1 x THEN_MAYBE tac2 x;
    74 
    73 
    75 (*Tactical to reduce the number of premises by 1.
    74 (*Tactical to reduce the number of premises by 1.
    76   If no subgoals then it must fail! *)
    75   If no subgoals then it must fail! *)
    77 fun DEPTH_SOLVE_1 tac = STATE
    76 fun DEPTH_SOLVE_1 tac st = st |>
    78  (fn st => 
       
    79     (case nprems_of st of
    77     (case nprems_of st of
    80 	0 => no_tac
    78 	0 => no_tac
    81       | n => DEPTH_FIRST (has_fewer_prems n) tac));
    79       | n => DEPTH_FIRST (has_fewer_prems n) tac);
    82 
    80 
    83 (*Uses depth-first search to solve ALL subgoals*)
    81 (*Uses depth-first search to solve ALL subgoals*)
    84 val DEPTH_SOLVE = DEPTH_FIRST (has_fewer_prems 1);
    82 val DEPTH_SOLVE = DEPTH_FIRST (has_fewer_prems 1);
    85 
    83 
    86 
    84 
   164 
   162 
   165 
   163 
   166 (*Simple iterative deepening tactical.  It merely "deepens" any search tactic
   164 (*Simple iterative deepening tactical.  It merely "deepens" any search tactic
   167   using increment "inc" up to limit "lim". *)
   165   using increment "inc" up to limit "lim". *)
   168 fun DEEPEN (inc,lim) tacf m i = 
   166 fun DEEPEN (inc,lim) tacf m i = 
   169   let fun dpn m = STATE(fn state => 
   167   let fun dpn m st = st |> (if has_fewer_prems i st then no_tac
   170 			if has_fewer_prems i state then no_tac
   168 			    else if m>lim then 
   171 			else if m>lim then 
   169 				(writeln "Giving up..."; no_tac)
   172 			     (writeln "Giving up..."; no_tac)
   170 				 else (writeln ("Depth = " ^ string_of_int m);
   173 			else (writeln ("Depth = " ^ string_of_int m);
   171 				       tacf m i  ORELSE  dpn (m+inc)))
   174 			      tacf m i  ORELSE  dpn (m+inc)))
       
   175   in  dpn m  end;
   172   in  dpn m  end;
   176 
   173 
   177 (*** Best-first search ***)
   174 (*** Best-first search ***)
   178 
   175 
   179 val trace_BEST_FIRST = ref false;
   176 val trace_BEST_FIRST = ref false;