Return-Path: <john.harrison-request@uk.ac.cam.cl>
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 01:58:20 +0000
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA17161;
          Mon, 8 Mar 93 17:42:10 -0800
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA17155;
          Mon, 8 Mar 93 17:42:01 -0800
Received: from auk.cl.cam.ac.uk (user jrh (rfc931)) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.4) to cl; Tue, 9 Mar 1993 01:40:59 +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 01:40:48 +0000
From: John Harrison <John.Harrison@uk.ac.cam.cl>
Message-Id: <"swan.cl.ca.245:09.03.93.01.41.02"@cl.cam.ac.uk>


Steve Brackin asks:

> 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?

This does seem rather awkward. It's probably easy enough using the "pair"
library. Alternatively the following is a nonce function which I think will
work OK:

  let PX_FUN_EQ_CONV =
    letrec pairup(ptm,vtm) =
      if is_pair ptm then
        let pl,pr = dest_pair ptm in
        let th = ISPEC vtm PAIR in
        let op,[vl;vr] = (strip_comb o lhs o concl) th in
        let thl,vll,fsl = pairup(pl,vl)
        and thr,vlr,fsr = pairup(pr,vr) in
        (TRANS (MK_COMB(AP_TERM op thl,thr)) th,vll@vlr,fsl@fsr)
      else (REFL vtm,[ptm],[vtm]) in
    \vs tm.
      let gv = genvar(type_of vs) in
      let gth,vls,gls = pairup(vs,gv) in
      let th1 = GENL vls (AP_THM (ASSUME tm) vs) in
      let th2 = (EXT o GEN gv o SUBS[gth] o SPECL gls o ASSUME o concl) th1 in
      IMP_ANTISYM_RULE (DISCH_ALL th1) (DISCH_ALL th2);;

e.g:

  #PX_FUN_EQ_CONV "t:num" "x:num->bool = y";;
  |- (x = y) = (!t. x t = y t)

  #PX_FUN_EQ_CONV "(a:num,((b:bool,c:(*)list),d:num#num))"
  #               "s:num#(bool#(*)list)#(num#num) -> num = t";;
  |- (s = t) = (!a b c d. s(a,(b,c),d) = t(a,(b,c),d))

John.