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; Thu, 1 Jul 1993 11:40:31 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA19381;
          Thu, 1 Jul 93 03:32:39 -0700
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA19376;
          Thu, 1 Jul 93 03:32:33 -0700
Received: from auk.cl.cam.ac.uk (user jrh (rfc931)) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) to cl; Thu, 1 Jul 1993 11:32:35 +0100
To: shaw@cs.ucdavis.edu (Rob Shaw)
Cc: info-hol@ted.cs.uidaho.edu
Subject: Re: proof state on the fly?
In-Reply-To: Your message of "Thu, 01 Jul 93 01:31:54 PDT." <9307010831.AA11247@toadflax.cs.ucdavis.edu>
Date: Thu, 01 Jul 93 11:32:30 +0100
From: John Harrison <John.Harrison@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:049080:930701103241"@cl.cam.ac.uk>


Rob Shaw asks:

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

Yes, a tactic is just a function which is applied to a goal, so you can simply
re-use its argument to get at the terms you want, by defining a tactic as:

  (\(asl,w). <tactic calculated from assumption list (asl) and conclusion (w)>
             (asl,w))

For example, here is a tactic which does case analysis over all the free
variables in the conclusion of a goal (it could be the core of a baby tautology
checker for purely propositional terms):

  (\(asl,w). MAP_EVERY BOOL_CASES_TAC (frees w) (asl,w))

I prefer to use the duplicator combinator |W|:

  let W f x   = f x x

for such things, giving the alternative definition:

  W(MAP_EVERY BOOL_CASES_TAC o frees o snd)

Overuse of this technique may render your proofs unreadable to others, but that
never bothers me much.

John.