Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Tue, 23 Nov 1993 14:03:29 +0000
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA27876;
          Tue, 23 Nov 1993 06:53:02 -0700
Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: bulk
Received: from swan.cl.cam.ac.uk by leopard.cs.byu.edu 
          with SMTP (1.37.109.8/16.2) id AA27872;
          Tue, 23 Nov 1993 06:52:55 -0700
Received: from guillemot.cl.cam.ac.uk (user jrh (rfc931)) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) to cl; Tue, 23 Nov 1993 13:50:20 +0000
To: info-hol@leopard.cs.byu.edu
Subject: Re: Problem porting
In-Reply-To: Your message of "Tue, 23 Nov 93 09:44:49 +0100." <93Nov23.094500met.8087@sunbroy14.informatik.tu-muenchen.de>
Date: Tue, 23 Nov 93 13:50:14 +0000
From: John Harrison <John.Harrison@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:192670:931123135023"@cl.cam.ac.uk>


Konrad writes:

| [...] However, the conversion *ought* to work; the
| reason it doesn't is that, at a crucial point, the author of the
| conversion didn't check for alpha-convertibility, only equality.
| (Note: this conversion fairly cries out for higher-order matching!)

Coincidentally I hit this problem in HOL-88 v2.01 very recently, and 
came up with the following fix, which will appear (more or less) in 
version 2.02.

  let SELECT_CONV =
    let SELECT_THM =
      let th1 = AP_THM EXISTS_DEF "P:*->bool" in
      let th2 = BETA_CONV(rhs(concl th1)) in
      GEN "P:*->bool" (SYM(th1 TRANS th2)) in
    \tm. let is_epsok t = is_select t &
                          let bv,bod = dest_select t in
                          aconv tm (subst [t,bv] bod) in
         let pickeps = find_term is_epsok tm in
         let th2 = ISPEC (rand pickeps) SELECT_THM in
         let th1 = SYM(BETA_CONV(lhs(concl th2))) in
         let th0 = ALPHA tm (lhs(concl th1)) in
         th0 TRANS th1 TRANS th2;;

The crucial change is using |aconv| instead of |=|.

John.