Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
To: toal@edu.ucla.cs (Ray J. Toal)
Cc: info-hol@edu.uidaho.cs.ted
In-Reply-To: Your message of Tue, 07 Jan 92 07:51:38 -0800. <9201071551.AA29698@maui.cs.ucla.edu>
Date: Tue, 07 Jan 92 17:30:36 +0000
From: Richard.Boulton@uk.ac.cam.cl
Message-Id: <"swan.cl.ca.204:07.00.92.17.32.05"@cl.cam.ac.uk>

Ray Toal writes:

> 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

Ray, the operations you wish to perform are known as `unwinding' (the equations
are used to substitute for the bound variables) and `pruning' (the bound
variables that can be are eliminated). There is a library called `unwind' in
the HOL system which contains tools for doing this. Unfortunately the tools
expect the equations to be the other way round to the way you have them, i.e.

   |-  ?x y z w. (y = a) /\ (w = b) /\ (f w ==> g z y x)

Here's a session which illustrates this:

#load_library `unwind`;;
Loading library `unwind` ...
Updating help search path
..................................
Library `unwind` loaded.
() : void

#let tm =
# "?(x:*) (y:**) (z:***) (w:****). (a = y) /\ (b = w) /\ (f w ==> g z y x)";;
tm = "?x y z w. (a = y) /\ (b = w) /\ (f w ==> g z y x)" : term

#let tm' =
# "?(x:*) (y:**) (z:***) (w:****). (y = a) /\ (w = b) /\ (f w ==> g z y x)";;
tm' = "?x y z w. (y = a) /\ (w = b) /\ (f w ==> g z y x)" : term

#EXPAND_AUTO_CONV [] tm';;
|- (?x y z w. (y = a) /\ (w = b) /\ (f w ==> g z y x)) =
   (?x z. f b ==> g z a x)

#EXPAND_AUTO_CONV [] tm;;
|- (?x y z w. (a = y) /\ (b = w) /\ (f w ==> g z y x)) =
   (?x y z w. (a = y) /\ (b = w) /\ (f w ==> g z y x))

As you can see, the tools don't work on your term. If it is feasible you
would probably find it worthwhile arranging for your equations to appear the
opposite way round. If not, here is a simple solution which works for your
example:

#(ONCE_DEPTH_CONV SYM_CONV THENC EXPAND_AUTO_CONV []) tm;;
|- (?x y z w. (a = y) /\ (b = w) /\ (f w ==> g z y x)) =
   (?x z. f b ==> g z a x)

This works by first flipping the equations using SYM_CONV. This is very
naive since it will flip all equations paying no attention to whether they
are already in the right order or not. A somewhat less naive solution is to
use the following function:

#let SYM_EXISTENTIALS_CONV tm =
 let vars = fst (strip_exists tm)
 in  let conv t =
        if (is_eq t) & (mem (rand t) vars)
        then SYM_CONV t
        else fail
 in  ONCE_DEPTH_CONV conv tm;;
######SYM_EXISTENTIALS_CONV = - : conv

This binds `vars' to the existentially quantified variables and then
constructs a conversion which only flips equations that have one of the bound
variables as the RHS.

So, now we can say:

#(SYM_EXISTENTIALS_CONV THENC EXPAND_AUTO_CONV []) tm;;
|- (?x y z w. (a = y) /\ (b = w) /\ (f w ==> g z y x)) =
   (?x z. f b ==> g z a x)

which also works for tm':

#(SYM_EXISTENTIALS_CONV THENC EXPAND_AUTO_CONV []) tm';;
|- (?x y z w. (y = a) /\ (w = b) /\ (f w ==> g z y x)) =
   (?x z. f b ==> g z a x)

I hope this helps.

Richard Boulton (rjb@cl.cam.ac.uk)