added SOLVE tactical
authoroheimb
Fri Oct 23 20:34:59 1998 +0200 (1998-10-23)
changeset 575498744e38ded1
parent 5753 c90b5f7d0c61
child 5755 22081de41254
added SOLVE tactical
doc-src/Ref/tctical.tex
src/Pure/search.ML
     1.1 --- a/doc-src/Ref/tctical.tex	Fri Oct 23 20:28:33 1998 +0200
     1.2 +++ b/doc-src/Ref/tctical.tex	Fri Oct 23 20:34:59 1998 +0200
     1.3 @@ -254,6 +254,7 @@
     1.4  \begin{ttbox} 
     1.5  COND        : (thm->bool) -> tactic -> tactic -> tactic
     1.6  IF_UNSOLVED : tactic -> tactic
     1.7 +SOLVE       : tactic -> tactic
     1.8  DETERM      : tactic -> tactic
     1.9  \end{ttbox}
    1.10  \begin{ttdescription}
    1.11 @@ -268,6 +269,10 @@
    1.12  returns the proof state otherwise.  Many common tactics, such as {\tt
    1.13  resolve_tac}, fail if applied to a proof state that has no subgoals.
    1.14  
    1.15 +\item[\ttindexbold{SOLVE} {\it tac}] 
    1.16 +applies {\it tac\/} to the proof state and then fails iff there are subgoals
    1.17 +left.
    1.18 +
    1.19  \item[\ttindexbold{DETERM} {\it tac}] 
    1.20  applies {\it tac\/} to the proof state and returns the head of the
    1.21  resulting sequence.  {\tt DETERM} limits the search space by making its
     2.1 --- a/src/Pure/search.ML	Fri Oct 23 20:28:33 1998 +0200
     2.2 +++ b/src/Pure/search.ML	Fri Oct 23 20:34:59 1998 +0200
     2.3 @@ -23,6 +23,7 @@
     2.4  
     2.5    val has_fewer_prems	: int -> thm -> bool   
     2.6    val IF_UNSOLVED	: tactic -> tactic
     2.7 +  val SOLVE		: tactic -> tactic
     2.8    val trace_BEST_FIRST	: bool ref
     2.9    val BEST_FIRST	: (thm -> bool) * (thm -> int) -> tactic -> tactic
    2.10    val THEN_BEST_FIRST	: tactic -> (thm->bool) * (thm->int) -> tactic
    2.11 @@ -65,6 +66,9 @@
    2.12  (*Apply a tactic if subgoals remain, else do nothing.*)
    2.13  val IF_UNSOLVED = COND (has_fewer_prems 1) all_tac;
    2.14  
    2.15 +(*Force a tactic to solve its goal completely, otherwise fail *)
    2.16 +fun SOLVE tac = tac THEN COND (has_fewer_prems 1) all_tac no_tac;
    2.17 +
    2.18  (*Execute tac1, but only execute tac2 if there are at least as many subgoals
    2.19    as before.  This ensures that tac2 is only applied to an outcome of tac1.*)
    2.20  fun (tac1 THEN_MAYBE tac2) st =