Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.4) outside ac.uk; Tue, 9 Mar 1993 18:35:32 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA03035; Tue, 9 Mar 93 10:07:01 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from leopard.cs.uidaho.edu by ted.cs.uidaho.edu (16.6/1.34) id AA03025; Tue, 9 Mar 93 10:06:34 -0800 Received: from swan.cl.cam.ac.uk by leopard.cs.uidaho.edu (16.7/1.34) id AA22528; Tue, 9 Mar 93 01:03:47 -0800 Received: from razorbill.cl.cam.ac.uk (user jg (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.4) to cl; Tue, 9 Mar 1993 08:53:14 +0000 To: shb@com.oracorp Cc: info-hol@edu.uidaho.cs.ted Subject: Re: Way around X_FUN_EQ_CONV restriction? In-Reply-To: Your message of Mon, 08 Mar 93 17:14:41 -0500. <9303082214.AA05144@sparta.oracorp.com> Date: Tue, 09 Mar 93 08:53:08 +0000 From: Jim Grundy Message-Id: <"swan.cl.ca.893:09.03.93.08.53.17"@cl.cam.ac.uk> > Is there any reasonably convenient way around the restriction in > X_FUN_EQ_CONV to using a single variable in replacing function equality > with an extensionally equivalent universal equality of terms? I'm > trying to show equality of complicated functions given by lambda > expressions, functions whose arguments are pairs, and for clarity I'd > like to give meaningful names to the components of arbitrary arguments > to these functions, not simply have them as FST p and SND p for an > arbitrary pair named p; I'd then prove equality for all possible > values of all the components. There ought to be an easy way to do > this, but I haven't been able to find it. > > Steve Brackin > ORA You probably want to use the function P_FUN_EQ_CONV from the pair Library released with HOL2.01. You may need to ftp a patch for the library from ftp.cl.cam.ac.uk:hvg/contrib/bugfixes/pair_lib before it works properly though. The pair library is intended to provide a version of every HOL function that works with abstractions and quantifications to work with paired (an arbitrary pair structure) abstractions and qauntifications. Its not quite there yet, but it does have about 90% of functions covered, including the one you want. Since you are using pairs, you will probably find the other functions in the library helpful as well. Jim