Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) id <18882-0@swan.cl.cam.ac.uk>; Fri, 31 Jul 1992 15:11:37 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA07223; Fri, 31 Jul 92 06:54:45 -0700 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Received: from air52.larc.nasa.gov by ted.cs.uidaho.edu (16.6/1.34) id AA07218; Fri, 31 Jul 92 06:54:37 -0700 Received: by air52.larc.nasa.gov (5.65.1/lanleaf2.4) id AA09835; Fri, 31 Jul 92 09:54:29 -0400 Message-Id: <9207311354.AA09835@air52.larc.nasa.gov> Date: Fri, 31 Jul 92 09:54:29 -0400 From: Victor "A." Carreno To: info-hol@edu.uidaho.cs.ted Subject: Re: stripping failure R.B.Jones writes: > The following simple example fails with HOL88v1.11 and its equivalent fails > also with ICL HOL (now known as ProofPower). > set_goal([],"?(x:*).(?(y:*)(x:*). P x y) /\ Q (x:*) ==> F");; > e STRIP_TAC;; [deleted] > Incidentally, can anyone explain why the last type cast (i.e., the fourth ":*") > in the above term is necessary? (it fails "types indeterminate" without it) the following term parses: set_goal([],"?(x:*).(?(y:*)(z:*). P z y) /\ Q x ==> F");; and so does: set_goal([],"?x.(?(y:*)(x:*). P x y) /\ Q (x:*) ==> F");; It appears there is a conflict between the variable "x" in the first quantification and the variable "x" in the second. This term produces the message: let t = "~(!x:**.(?(y:*)(x:*). P x y) /\ Q x)";; evaluation failed types in quotation and so does: let t = "~(!x:**.(?(y:*)(x:*). P x y) /\ Q (x:**))";; evaluation failed types in quotation In general: let t = "!x:*. P x /\ (!x:**. Q x)";; evaluation failed types in quotation let t = "!x:*. P x /\ (!z:**. Q z)";; t = "!x. P x /\ (!z. Q z)" : term Doesn't the "x" in "Q x" supposed to be bound by the second quantification and unaffected by the first ? Victor.