Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
To: shb@com.oracorp
Cc: info-hol@edu.uidaho.cs.ted
Subject: Re: "Succeeds" predicate?
In-Reply-To: Your message of Mon, 09 Mar 92 14:18:13 -0500. <9203091918.AA07706@sparta.oracorp.com>
Date: Mon, 09 Mar 92 20:53:02 +0000
From: Tom.Melham@uk.ac.cam.cl
Message-Id: <"swan.cl.ca.211:09.02.92.20.53.09"@cl.cam.ac.uk>


Regarding Steve Brackin's recent query:

> I'd like a function I could apply to a tactic applied to each of a
> number of sugoals with THEN that would cause the tactic to have no
> effect on a subgoal unless it succeeded in proving that subgoal.  (I
> was recently burned by a tactic that succeeded in proving a number of
> subgoals, but transformed one of them so that I didn't recognize it.)
> Such a function would be analogous to TRY, but would check for whatever
> gives rise to a "subgoal proved" message.  Is there such a thing?  Is
> it reasonably easy to write?

There is, as far as I can recall, no such function built-in.  But it
is completely trivial to write in ML.  Here is an implementation:

   let TRY_SOLVE (tac:tactic) (A,g) =
       (let sgs,pf = tac (A,g) in
        if (null sgs) then sgs,pf else fail) ? [A,g],hd;;

TRY_SOLVE tac solves a goal (A,g) if tac does.  But if tac fails
when applied to the goal, or if it merely transforms but does not
solve it, then TRY_SOLVE tac has no effect.  (The action on failure
was not specified in the above message, but what I have done
seems consistent with the intended use.)

Note that it is reduction to the empty list of subgoals that
`gives rise to a "subgoal proved" message'.  The message itself
is merely an artefact of the subgoal package---it really has nothing
to do with the essence of tactics.

Tom