src/Pure/search.ML
changeset 5754 98744e38ded1
parent 5693 998af7667fa3
child 5956 ab4d13e9e77a
equal deleted inserted replaced
5753:c90b5f7d0c61 5754:98744e38ded1
    21   val ITER_DEEPEN	: (thm->bool) -> (int->tactic) -> tactic
    21   val ITER_DEEPEN	: (thm->bool) -> (int->tactic) -> tactic
    22   val THEN_ITER_DEEPEN	: tactic -> (thm->bool) -> (int->tactic) -> tactic
    22   val THEN_ITER_DEEPEN	: tactic -> (thm->bool) -> (int->tactic) -> tactic
    23 
    23 
    24   val has_fewer_prems	: int -> thm -> bool   
    24   val has_fewer_prems	: int -> thm -> bool   
    25   val IF_UNSOLVED	: tactic -> tactic
    25   val IF_UNSOLVED	: tactic -> tactic
       
    26   val SOLVE		: tactic -> tactic
    26   val trace_BEST_FIRST	: bool ref
    27   val trace_BEST_FIRST	: bool ref
    27   val BEST_FIRST	: (thm -> bool) * (thm -> int) -> tactic -> tactic
    28   val BEST_FIRST	: (thm -> bool) * (thm -> int) -> tactic -> tactic
    28   val THEN_BEST_FIRST	: tactic -> (thm->bool) * (thm->int) -> tactic
    29   val THEN_BEST_FIRST	: tactic -> (thm->bool) * (thm->int) -> tactic
    29 			  -> tactic
    30 			  -> tactic
    30   val trace_ASTAR	: bool ref
    31   val trace_ASTAR	: bool ref
    62 (*Predicate: Does the rule have fewer than n premises?*)
    63 (*Predicate: Does the rule have fewer than n premises?*)
    63 fun has_fewer_prems n rule = (nprems_of rule < n);
    64 fun has_fewer_prems n rule = (nprems_of rule < n);
    64 
    65 
    65 (*Apply a tactic if subgoals remain, else do nothing.*)
    66 (*Apply a tactic if subgoals remain, else do nothing.*)
    66 val IF_UNSOLVED = COND (has_fewer_prems 1) all_tac;
    67 val IF_UNSOLVED = COND (has_fewer_prems 1) all_tac;
       
    68 
       
    69 (*Force a tactic to solve its goal completely, otherwise fail *)
       
    70 fun SOLVE tac = tac THEN COND (has_fewer_prems 1) all_tac no_tac;
    67 
    71 
    68 (*Execute tac1, but only execute tac2 if there are at least as many subgoals
    72 (*Execute tac1, but only execute tac2 if there are at least as many subgoals
    69   as before.  This ensures that tac2 is only applied to an outcome of tac1.*)
    73   as before.  This ensures that tac2 is only applied to an outcome of tac1.*)
    70 fun (tac1 THEN_MAYBE tac2) st = 
    74 fun (tac1 THEN_MAYBE tac2) st = 
    71     (tac1  THEN  COND (has_fewer_prems (nprems_of st)) all_tac tac2)  st;
    75     (tac1  THEN  COND (has_fewer_prems (nprems_of st)) all_tac tac2)  st;