Delivery-Date: 
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
To: shaw@cs.ucdavis.edu (Rob Shaw)
Cc: info-hol@ted.cs.uidaho.edu, Tom.Melham@cl.cam.ac.uk
Subject: Re: manipulate several subgoals?
In-Reply-To: Your message of "Sun, 13 Jun 93 20:37:32 PDT." <9306140337.AA23785@toadflax.cs.ucdavis.edu>
Date: Mon, 14 Jun 93 14:45:16 +0100
From: Tom Melham <Tom.Melham@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:049100:930614134536"@cl.cam.ac.uk>


Rob Shaw asks:

> What is the usual way to manipulate more than just the top subgoal of
> the stack? 

As Wai points out, you can use THENL to apply different tactics to
different subgoals.  Note however, that this really has nothing to
do with the goal stack.  I always like to think of it this way: 
the goal stack, expand, expandf, and all the rest of the subgoal
package is really just a handy tool for helping you to discover or
develop tactics; normally, the "deliverable" or "product" of a
tactic-hacking session should be a composite tactic that proves
the desired theorem (more precisely, a file containing several such
tactics).  See any of the sources that create the built-in theories
for examples --- you won't find "expand" anywhere there, though it
was of course used all the time when these files were being written
and debugged.

Regarding the actual questiom, here is one possible approach. The
question was how to treat the case where TACTIC1 (say) produces six
subgoals, the first five of which are proved with

    ASSUME_TAC (el index (CONJUNCTS validAexpr)) THEN
    POP_ASSUM (\thm. REWRITE_TAC [thm]))

Well, first of all the following would work:

    TACTIC1 THEN REWRITE_TAC [validAexpr]

provided rewriting with validAexpr doesn't mess up the sixth subgoal.
(And provided validAexpr does not give rise to a non-terminating 
set of rewrites, etc). But suupose, for the sake of illustration, we 
wanted to solve the problem as posed.  Then the following 
quick-and-dirty hack would work:

   TACTIC1 THENL 
   (let ths = CONJUNCTS validAexpr in
    (MAP_EVERY (\th. REWRITE_TAC [th]) ths @ [ALL_TAC]))

This is the same as saying

   TACTIC1 THENL
    [REWRITE_TAC [el 1 (CONJUNCTS validAexpr)];	 % tactic for subgoal 1 %
     REWRITE_TAC [el 2 (CONJUNCTS validAexpr)];	 % tactic for subgoal 2 %   
     ...
     REWRITE_TAC [el 5 (CONJUNCTS validAexpr)];	 % tactic for subgoal 5 %   
     ALL_TAC]					 % do nothing to subgoal 6 %

Tom