Delivery-Date: 
Sender: hol2000-request@lal.cs.byu.edu
Errors-To: hol2000-request@lal.cs.byu.edu
Precedence: bulk
To: hol2000@leopard.cs.byu.edu
Cc: Paul.Curzon@cl.cam.ac.uk
Subject: Re: Accessing Assumptions
Date: Wed, 25 May 94 18:07:46 +0100
From: Paul Curzon <Paul.Curzon@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:262260:940525170756"@cl.cam.ac.uk>

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


I have been wondering about better ways of accessing assumptions for some
time.

My favoured option is that you give assumptions names at the time they become
an assumption ie bind them to an ML local variable. That way the name you
give them can be meaningful to you, it is resistant to change since it is
not dependent on the contents at all, it is easy to refer to the particular
assumption. Furthermore it can make it easy to single step through tactics
when you've made a change to the goal, or are applying it to something new for
which it doesnt quite work. I do that all the time so it is very important.
Use of DISCH_THEN makes it very difficult to do.

I have toyed with ways of doing this, the easiest was just
to store the ASSUMED assumption in an assignable variable when you eg do
DISCH_TAC and then bind that to a name of choice. This just involves making
minor changes to various tactics, but is very hacky. Maybe if you were doing
things from scratch in HOL2000 it could be done more cleanly.
You then get proofs such as:

val Lemma = prove(
(--`!n. PSIG2LEN n n d ==> ..... `--),

GEN_TAC THEN
CATCH_DISCH_TAC THENA (fn _ => 
  let val psig2len = new_assumption();
      val th1 = REWRITE_RULE[....] psig2len
in
REPEAT STRIP_TAC THEN
IMP_RES_TAC th1 THEN
...
end)
);

CATCH_DISCH_TAC is DISCH_TAC but catching the assumption in an assignable
variable
new_assumption() gives the most recent assumption
THENA is needed to make sure the assignment happens first

Thus the style is similar to use of DISCH_THEN but you can develop it a step
at a time and then rerun it a step at a time very easily.


Paul Curzon.