Delivery-Date: 
Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: bulk
From: David Shepherd <des@inmos.co.uk>
Message-Id: <18097.9401200948@frogland.inmos.co.uk>
Subject: Re: X_EXISTS_TAC
To: windley@leopard.cs.byu.edu (Phil Windley)
Date: Thu, 20 Jan 1994 09:48:49 +0000 (GMT)
Cc: info-hol@cs.uidaho.edu (info-hol mailing list)
In-Reply-To: <24553.199401200535@ganymede.inmos.co.uk> from "Phil Windley" at Jan 19, 94 08:41:43 pm
Content-Type: text
Content-Length: 1197

Phil Windley has said:
> Does anyone have a tactic that behaves like EXISTS_TAC but allows you to
> pick which existentially quantified variable to provide a witness for?  For
> example, suppose I have:
> 
> g
> "? w x y z . t[w,x,y,z]";;
> 
> e(
> X_EXISTS_TAC "y" "witness"
> );;
> 
> would yield
> 
> "? w x z . t[w,x,witness,z]"
> 
> Of course, a conversion that proves permuting the variables doesn't change
> the meaning would be as good.

A conversion that pulls an existential quantification out of a list
would be (in HOL90 terms) is


fun PULL_OUT_EXISTS_CONV x t =
    let val {Bvar,Body} = dest_exists t
    in
	if (Bvar = x) then ALL_CONV t
	else
	    ((RAND_CONV o ABS_CONV)(PULL_OUT_EXISTS_CONV x)
	     THENC SWAP_EXISTS_CONV)t
    end;
    

# PULL_OUT_EXISTS_CONV (--`y:'c`--)
                       (--`? (w:'a) (x:'b) (y:'c) (z:'d). P`--);

val it = |- (?w x y z. P) = (?y w x z. P) : thm


--------------------------------------------------------------------------
david shepherd: des@inmos.co.uk                     tel: 0454-616616 x 625
                inmos ltd, 1000 aztec west, almondsbury, bristol, bs12 4sq
		"you might think that   ---   I couldn't possibly comment"