Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Fri, 19 Nov 1993 16:16:54 +0000 Received: by leopard.cs.byu.edu (1.37.109.7/16.2) id AA07140; Fri, 19 Nov 93 07:59:55 -0700 Sender: info-hol-request@leopard.cs.byu.edu Errors-To: info-hol-request@leopard.cs.byu.edu Precedence: bulk Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu with SMTP (1.37.109.7/16.2) id AA07136; Fri, 19 Nov 93 07:59:47 -0700 Received: from infix.cs.ruu.nl by dworshak.cs.uidaho.edu with SMTP (1.37.109.4/16.2) id AA25347; Fri, 19 Nov 93 06:57:47 -0800 Received: by infix.cs.ruu.nl id AA11133 (5.65c/IDA-1.4.4 for info-hol@ted.cs.uidaho.edu); Fri, 19 Nov 1993 15:57:31 +0100 From: Wishnu Prasetya Message-Id: <199311191457.AA11133@infix.cs.ruu.nl> Subject: Help: how to define the following in HOL To: info-hol@cs.uidaho.edu (hol mailing list) Date: Fri, 19 Nov 1993 15:57:30 +0100 (MET) X-Mailer: ELM [version 2.4 PL23] Mime-Version: 1.0 Content-Type: text/plain; charset=US-ASCII Content-Transfer-Encoding: 7bit Content-Length: 1013 Hi! I want to define a predicate that characterizes a class of function, say a class of indentity-like function. My informal idea is as follows: id is an IDENTITish function iff (id o f) o (id o g) = (f o g) how can I define the predicate INDENTITish in HOL? Anyone can help? Thanks. -Wishnu- ----------------------------------------------------------------------- PS1: f and g do not necessarily have the same type, although of course they should be compatible.) ----------------------------------------------------------------------- PS2: naively translating above informal definition fails: #new_definition (`IDENTITish`, "IDENTITish id = !(f:*B->*C) (g:*A->*B). ((id o f) o (id o g)) = (f o g)") ;; ##Badly typed application of: "$o id" which has type: ":(*A -> *C) -> (*A -> ?)" to the argument term: "g" which has type: ":*A -> *B" evaluation failed mk_comb in quotation -----------------------------------------------------------------------