Delivery-Date: 
Sender: info-hol-request@cs.uidaho.edu
Errors-To: info-hol-request@cs.uidaho.edu
Precedence: bulk
From: David Shepherd <des@inmos.co.uk>
Message-Id: <14971.9309210942@frogland.inmos.co.uk>
Subject: Re: A simple question
To: info-hol@cs.uidaho.edu (info-hol mailing list)
Date: Tue, 21 Sep 1993 10:42:24 +0100 (BST)
In-Reply-To: <9309210923.AA13389@maui.cs.ucla.edu> from "chou@cs.ucla.edu" at Sep 21, 93 02:23:02 am
Content-Type: text
Content-Length: 1223

chou@cs.ucla.edu has said:
> 
> Suppose that
> 
>     ~(NULL x)
> 
> is among the assumptions of my goal, where x may be a complex term.
> I wish to add the following conclusion to the assumption list:
> 
>     x = CONS h t
> 
> where h and t are two fresh variables, using the following theorem:
> 
>     |- !l. NULL l \/ (?h t. l = CONS h t)
> 
> What is the simplest way to do this?
> 
> The simplest way I can think of is to first rewrite the theorem above
> into the following form:
> 
>     |- !l. ~(NULL l) ==> (?t h. l = CONS h t)
> 
> and then use IMP_RES_TAC.


Assuming the theorem is called THM, then (in hol90 syntax)

(STRIP_ASSUME_TAC o REWRITE_RULE[ASSUME(--`~(NULL x)`--)] o SPEC(--`x`--))THM

-- n.b. you'll have to add some type annotations to the `x`'s

Or, at the risk of a bit of unwanted resolution

STRIP_ASSUME_TAC(SPEC(--`x`--)THM)
THEN RES_TAC


--------------------------------------------------------------------------
david shepherd: des@inmos.co.uk                     tel: 0454-616616 x 625
                inmos ltd, 1000 aztec west, almondsbury, bristol, bs12 4sq
		"They didn't like the rates, they don't like the poll tax,
		 and they won't like the council tax."   - Nicholas Ridley