Delivery-Date: 
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
Date: Thu, 1 Jul 93 01:31:54 PDT
From: shaw@cs.ucdavis.edu (Rob Shaw)
Message-Id: <9307010831.AA11247@toadflax.cs.ucdavis.edu>
To: info-hol@ted.cs.uidaho.edu
Subject: proof state on the fly?


The main question is how to get at subgoals that are generated while
a tactic is in progress?

Alot of the proving I'm doing involves case analysis, where two or three
different tactics are enough to prove the, say, ten cases. Occasionally,
however, these tactics may need to differ at some step like an ABBREV_TAC
because a different term should be passed to it, depending upon the
current case. Clearly, I don't want to duplicate a twenty-step tactic
ten times when each one is only going to differ at one term given to an
ABBREV_TAC. 

Suppose the desired term is, say, 

  (fst (dest_eq (concl (el 1 <assumptions>))))

but by the time the proof is at this step (which it visits several times,
once for each case) the assumptions are nothing like the state of the
proof when I invoked expand. How can I get the "current" goal or assumptions
to pick out subterms on the fly? Are there calls to do this? Obviously
POP_ASSUM_LIST is ugly, because I'd have to (re)ASSUME_TAC them all.
Also, something like

 map (\tm. ..... ABBREV_TAC tm var ..... ) [... precomputed terms..]

is not desirable, because the number of cases is going to grow over time,
while the proof methods will remain the same. Everytime we add a new
constructor for a certain type, I don't want to have to go and update all
those "[... precomputed terms..]" lists, adding in the new ones.
Secondly, I don't want to do the precomputing when I know that a particular
subterm of the goal at that point will be the term I need.

Is there any way to get at the truly "current" state of the proof, and not
its state at the outset of the expand, via ML functions, rather than 
something like POP_ASSUM_LIST?

Thanx again.

Rob