Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
From: David Shepherd <des@com.inmos>
Message-Id: <19698.9201071728@frogland.inmos.co.uk>
Subject: Re: your mail
To: toal@edu.ucla.cs (Ray J. Toal)
Date: Tue, 7 Jan 92 17:28:22 GMT
In-Reply-To: <9201071551.AA29698@maui.cs.ucla.edu>; from "Ray J. Toal" at Jan 7, 92 7:51 am

Ray J. Toal has said:
> Has anyone a rule (or conversion?) for the following?
>
> I would like to remove all existentially quantified variables (xi)
> in a theorem that appear free in a subterm "t = xi" of the body.
> For example, from
>
>   |-  ?x y z w. (a = y) /\ (b = w) /\ (f w ==> g z y x)
>
> one should obtain
>
>   |-  ?x z. f b ==> g z a x
>
> I hope that this is an interesting problem and that I am not incorrect
> in thinking that it is logically possible.  It may even be easy.
> The following (inefficient) function may be of use:

1) load the "convert" library
2) apply conversion (DOWN_CONV SYM_CONV)
3) apply conversion PRUNE_CONV

(step 2 is needed as prune expects equalities the other way round)

the convert library contains, among others, my tidy ups of the original
unwind, unfold and pruning rules and conversions which have been in
HOL since the beginning (they date back to LCF_LSM !).

unfortunately with the current "complete" documentation its much more
difficult to find out about rules like these than it was in the "good
old days" when you just had about 20 pages that contained all the
useful stuff! (btw i personnally still use the old pre-HOL88
documentation first when i'm looking up rules or conversions as theres
less to wade through!)

--------------------------------------------------------------------------
david shepherd: des@inmos.co.uk or des@inmos.com    tel: 0454-616616 x 625
                inmos ltd, 1000 aztec west, almondsbury, bristol, bs12 4sq
                "five,  four,  three,  two,  one,   thunderbirds are go !"