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: Tue, 10 Mar 92 00:11:36 +0000
From: John.Harrison@uk.ac.cam.cl
Message-Id: <"swan.cl.ca.479:10.02.92.00.11.48"@cl.cam.ac.uk>


Steve Brackin writes:

> 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?

Tom Melham suggests:

>    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;;

I use the following idiom in such circumstances:

  TRY(tac THEN NO_TAC)

I think this does what you are asking - the idea being that the tactic
in parentheses will fail unless "tac" reduces the goal to the empty set
of subgoals.

This is probably less efficient than Tom's suggestion, but it saves
having to write nontrivial ML.

John.