Delivery-Date: 
Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: bulk
From: Konrad Slind <slind@informatik.tu-muenchen.de>
To: info-hol@leopard.cs.byu.edu, toshok@cs.uidaho.edu
In-Reply-To: Chris Toshok's message of Tue, 23 Nov 1993 06:10:31 +0100 <199311230510.AA20737@panther.cs.uidaho.edu>
Subject: Problem porting
Message-Id: <93Nov23.094500met.8087@sunbroy14.informatik.tu-muenchen.de>
Date: Tue, 23 Nov 1993 09:44:49 +0100


Chris Toshok writes with regards to the (somewhat edited) term

    "Next(\t'. T)(n,(@t. Next(\t'. T)(n,t)))"

>
> I use the following command in both versions:
> 
>       e (CONV_TAC (DEPTH_CONV SELECT_CONV));;
> 
> and hol88 spits out:
>
>      OK..
>      "?t. Next(\t'. T)(n,t)"
>
> while hol90 gives me the same term back:

Chris must be using a different version of hol88 than 2.01, which is
what I have. In 2.01, hol88 gives the same answer as hol90: the
conversion makes no change. 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!)

Here's the fix: it replaces the definition of SELECT_CONV in
src/1/conv.sml. If you don't want to take the time to re-build the
system, then put it in your hol-init file (but you'll have to define
CONV_ERR as follows

    fun CONV_ERR{function,message} =
         HOL_ERR{origin_structure = "Conv",
                 origin_function = function,
                 message = message};
).

local
val f = mk_var{Name="f",Ty= ==`:'a->bool`==} 
val th1 = AP_THM Exists.EXISTS_DEF f 
val th2 = CONV_RULE (RAND_CONV BETA_CONV) th1 
val tyv = Type.mk_vartype "'a" 
fun EXISTS_CONV{Bvar,Body} = 
   let val ty = type_of Bvar
       val ins = INST_TYPE [{redex=tyv, residue=ty}] th2
       val th = INST[{redex=inst[{redex=tyv,residue=ty}] f,
                      residue=mk_abs{Bvar=Bvar,Body=Body}}] ins
   in CONV_RULE (RAND_CONV BETA_CONV) th
   end
fun find_first p tm =
   if (p tm)
   then tm 
   else if (is_abs tm)
        then find_first p (body tm) 
        else if is_comb tm 
             then let val {Rator,Rand} = dest_comb tm 
                  in (find_first p Rator) handle _ => (find_first p Rand)
                  end
             else raise CONV_ERR{function="SELECT_CONV.find_first",message=""}
in
fun SELECT_CONV tm =
   let fun right t = 
          let val {Bvar,Body} = dest_select t
          in (Term.aconv (subst[{redex=Bvar,residue=t}] Body) tm)
          end handle _ => false
       val epi = find_first right tm 
   in
   SYM (EXISTS_CONV (dest_select epi))
   end
   handle _ => raise CONV_ERR{function="SELECT_CONV",message=""}
end;