Reply-To: info-hol@ted
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@ted.cs.uidaho.edu
To: info-hol@edu.uidaho.cs.ted
Subject: Re: referring to assumptions cont'ed
In-Reply-To: Your message of Thu, 31 Oct 91 21:42:52 -0100. <9110312242.AA06641@esat.kuleuven.ac.be>
Date: Fri, 01 Nov 91 12:17:23 +0000
From: Tom.Melham@uk.ac.cam.cl
Message-Id: <"swan.cl.ca.483:01.10.91.12.17.32"@cl.cam.ac.uk>

In a recent message, Wim gave the following example:

>  say you are proving
>
>    P[alfa]
>      [as1(alfa)]
>      [as2]
>       ...
>      [P [x]]
>       ...
>      [asn]
>
>  and you have the theorem
>
>    thm1 |-as1(alfa) /\ as2 ==> x = alfa
>
>  you can write
>
>   e(IMP_RES_TAC thm1 THEN
>     FIRST_ASSUM (SUBS1_TAC o SYM) THEN
>     FIRST_ASSUM ACCEPT_TAC);;

And in a later message, Phil says:

> Next time you do something really clever, post it to info-hol.  I promise
> that there are a lot of things that may seem trivial, but are real eye
> openers to others.

Well, the following isn't _really_ clever, but it's a useful little trick.
To solve the goal wim describes above, try:

    e(REPEAT_GTCL IMP_RES_THEN SUBST_ALL_TAC thm1);;
    e(FIRST_ASSUM ACCEPT_TAC);;

This won't necessarily always work, but it works very well sometimes.

Tom