Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.2); Tue, 6 Oct 1992 12:16:17 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA22660; Tue, 6 Oct 92 03:57:35 -0700 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 AA22655; Tue, 6 Oct 92 03:57:25 -0700 Received: from guillemot.cl.cam.ac.uk (user tfm) by swan.cl.cam.ac.uk with SMTP (PP-6.2) to cl; Tue, 6 Oct 1992 11:55:00 +0100 To: Wishnu Prasetya Cc: info-hol@edu.uidaho.cs.ted (hol mailing list), Tom.Melham@uk.ac.cam.cl Subject: Re: QUESTION: unbound type variable in new_definition In-Reply-To: Your message of Mon, 05 Oct 92 15:19:12 +0700. <199210051419.AA24627@infix.cs.ruu.nl> Date: Tue, 06 Oct 92 11:54:29 +0100 From: Tom Melham Message-Id: <"swan.cl.ca.453:06.09.92.10.55.12"@cl.cam.ac.uk> > I try to define DISJ_REL (disjunctive relation) as follows: > > let DISJ_REL = new_definition > (`DISJ_REL`, > "DISJ_REL (R:(*->bool)->(*->bool)->bool) = > !p (W:**->(*->bool)). (!i:**. R (W i) p) ==> R (\s:*. ?i. W i s) p") ;; > > but this is of no success. I get the following error: > > evaluation failed ** an unbound type variable in definition > > which I don't really understand why. The closer hint I gather from the > referrence is that applying new_definition to OP x y = t may fail if > there is a type in x, y, or t that does not occur in OP. But this > doesn't seem the case here. See the side conditions for new_definition in DESCRIPTION. One of them is that in a constant definition |- c : ty = all the type variables that appear *anywhere* in "" must be included in the type variables that appear in the type "ty". Chapter 10 of DESCRIPTION ("Theories") explains why. The problem above is that DISJ_REL has type (*->bool)->(*->bool)->bool -> bool but the corresponding contains the type varaible **. Tom PS: see also my paper in this year's HOL user meeting.