Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Mon, 14 Jun 1993 04:47:21 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA08602;
          Sun, 13 Jun 93 20:37:19 -0700
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
Received: from [128.120.56.188] by ted.cs.uidaho.edu (16.6/1.34) id AA08597;
          Sun, 13 Jun 93 20:37:15 -0700
Received: by toadflax.cs.ucdavis.edu (4.1/UCD.CS.2.3) id AA23785;
          Sun, 13 Jun 93 20:37:32 PDT
Date: Sun, 13 Jun 93 20:37:32 PDT
From: shaw@cs.ucdavis.edu (Rob Shaw)
Message-Id: <9306140337.AA23785@toadflax.cs.ucdavis.edu>
To: info-hol@ted.cs.uidaho.edu
Subject: manipulate several subgoals?



What is the usual way to manipulate more than just the top subgoal of
the stack? For instance, at one point in a proof, I have six subgoals,
the top five of which are proved with:

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

as "index" takes the successive values 1 thru 5. Naively, (I'm new at this
HOL thing), I tried a MAP_EVERY, not realizing at first that "expand" only
ever gives the top goal to the tactic, and there was no way for the MAP_EVERY
(or REPEAT, etc...) to even see all 5 subgoals, let alone prove them. 

For now I have an ugly hack:

letrec SQUASHL (f:(*->tactic)) (args:((*)list)) =
         if (length args) = 0 then
            ()
         else (
            expand (f (hd args)); 
            SQUASHL f (tl args) 
         )
 ;;

which lets me do what I want via:

SQUASHL
 (\index. 
    ASSUME_TAC (el index (CONJUNCTS validAexpr))
  THEN
    POP_ASSUM (\thm. REWRITE_TAC [thm]))
 [1;2;3;4;5]

But I'm sure there must already be a way to deal with more than just the
top subgoal in a single command ?? I gleaned goal.ml and stack.ml quickly
for clues, but didn't see any... just expand and expandf.

Thanx!

Rob Shaw