Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Wed, 25 May 1994 17:37:02 +0100
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA15191;
          Wed, 25 May 1994 10:34:52 -0600
Sender: hol2000-request@lal.cs.byu.edu
Errors-To: hol2000-request@lal.cs.byu.edu
Precedence: bulk
Received: from puma.cs.byu.edu by leopard.cs.byu.edu 
          with SMTP (1.37.109.8/16.2) id AA15187;
          Wed, 25 May 1994 10:34:52 -0600
From: Paul "E." Black <black@lal.cs.byu.edu>
Received: by puma.cs.byu.edu (1.38.193.4/CS-Client) id AA27350;
          Wed, 25 May 1994 10:36:19 -0600
Date: Wed, 25 May 1994 10:36:19 -0600
Message-Id: <9405251636.AA27350@puma.cs.byu.edu>
To: hol2000@leopard.cs.byu.edu
Subject: Accessing Assumptions

     Kelly Hall <hall@leopard.cs.byu.edu> wrote
          b) numbering assumptions and using their index in rewrite rules is
             easier than FIRST_ASSUM and ASSUM_LIST, although it makes a proof
             more 'brittle'.

I've thought about the assumption list, too.  One would like to refer
to assumptions by the content, something like "... the assumption
about m < x ..."  My suggestion is to refer to assumptions by a
*signature* rather than a literal match (a textual copy) or an index.
Hopefully the signature would change less often than either of those.

Here are some proposed requirements.  The signature should be
  * fairly short, say, no more than 6 or 8 digits.
  * not very sensitive to variable name changes (so tactics need not
        change for alpha renaming).
  * not very sensitive to order differences in commutative operators
        (so minor changes such as from "P /\ Q" to "Q /\ P" don't
         change the signature).

The signature should be slightly sensitive to name changes so we can
distinguish "[HD l] = l" from "[HD m] = m".  I was thinking of a two
part signature (xxxxxx, xxx) where the first part is a "hash function"
of the structure and the second part is a function of the variable
names.  The first part could be used alone if no two assumptions had
the same structural signature.

In display it might look something like this:
"Q x"
    [ "!x. P x ==> Q x" ]	(23, 12)
    [ "P x" ]			(7, 1)
then one could write something like
	e(UNDISCH_TAC (ASSUMP 7) THEN ASM_REWRITE_TAC[]);;

Paul E. Black                   Laboratory for Applied Logic
black@lal.cs.byu.edu            3308 TMCB
p.black@ieee.org                Brigham Young University
voice: +1 801 378 8113          Provo, Utah   84602
<A href="http://lal.cs.byu.edu/people/black.html">Mosaic page</A>