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; Mon, 22 Nov 1993 21:06:06 +0000
Received: by leopard.cs.byu.edu (1.37.109.7/16.2) id AA22412;
          Mon, 22 Nov 93 11:51:06 -0700
Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: bulk
Received: from air52.larc.nasa.gov by leopard.cs.byu.edu 
          with SMTP (1.37.109.7/16.2) id AA22407; Mon, 22 Nov 93 11:50:54 -0700
Received: by air52.larc.nasa.gov (5.65.1/lanleaf2.4) id AA04016;
          Mon, 22 Nov 93 13:47:01 -0500
Message-Id: <9311221847.AA04016@air52.larc.nasa.gov>
Date: Mon, 22 Nov 93 13:47:01 -0500
From: Victor "A." Carreno <vac@air16.larc.nasa.gov>
To: info-hol@leopard.cs.byu.edu
Subject: Re: Help: how to define the following in HOL
In-Reply-To: Mail from 'Victor A. Carreno <vac>' dated: Mon, 22 Nov 93 13:31:04 -0500


>  IDENTish(id) = (!f. id o f = f) /\ (!g. g o id = g)
>
>Unfortunately it's not possible to do it, because in a definition all type
>variables free in the RHS must be free in the LHS.

One possible way of doing the specification is to declare a variable with
such a type and not use it:

#new_definition (`IDENTITish2`,
    "IDENTITish2 id (x:*B) = !(f:*B -> *C). (id o f) = f");;

|- !id x. IDENTITish2 id x = (!f. id o f = f)

or restrict the variable type (probably not what Wishnu was looking for)

#new_definition (`IDENTITish`,
    "IDENTITish id = !(f:*C -> *C).((id o f) = f) /\ (f = (f o id))");;

|- !id. IDENTITish id = (!f. (id o f = f) /\ (f = f o id))

but this one is commutative ;-)


Victor.