Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Tue, 15 Jun 1993 23:55:11 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA12604;
          Tue, 15 Jun 93 15:48:40 -0700
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA12598;
          Tue, 15 Jun 93 15:48:33 -0700
Received: from auk.cl.cam.ac.uk (user jrh (rfc931)) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) to cl; Tue, 15 Jun 1993 23:48:40 +0100
To: toal@cs.ucla.edu (Ray Toal)
Cc: info-hol@ted.cs.uidaho.edu
Subject: Re: A simple question
In-Reply-To: Your message of "Tue, 15 Jun 93 13:48:20 PDT." <9306152048.AA10755@makaha.cs.ucla.edu>
Date: Tue, 15 Jun 93 23:48:36 +0100
From: John Harrison <John.Harrison@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:056210:930615224844"@cl.cam.ac.uk>


Ray Toal asks:

> The following question seems simple, but I'm missing something obvious
> (I think).  I'd like to extend EXISTS_TAC to instantiate a particular
> bound variable, for example
> 
>      ?x1 ... xn. t
> ========================    NEW_EXISTS_TAC xi u
> ?x1..x(i-1)x(i+1)..xn. t[u/xi]

One possibility is to bubble the required variable to the front of the
list of existential quantifiers using |SWAP_EXISTS_CONV|, then just use
|EXISTS_TAC| as usual. A very crude implementation might be:

  let NEW_EXISTS_TAC xv =
    $THEN (CONV_TAC(DEPTH_CONV(SWAP_EXISTS_CONV o assert
          (\tm. fst(dest_exists(snd(dest_exists tm))) = xv ? false)))) o 
    EXISTS_TAC;;

To cover cases where the body of the goal also contains similar terms,
you should really use something more precise than |DEPTH_CONV|, but the
above is probably adequate for most purposes.

John.