Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
X400-Received: by mta eros.uknet.ac.uk in /PRMD=UK.AC/ADMD=GOLD 400/C=GB/;
               Relayed; Thu, 30 Jul 1992 15:48:32 +0100
X400-Received: by /PRMD=icl/ADMD=gold 400/C=GB/; converted (ia5); Relayed;
               Thu, 30 Jul 1992 15:46:23 +0100
Date: Thu, 30 Jul 1992 15:46:23 +0100
X400-Originator: R.B.Jones@uucp.win0109
X400-Mts-Identifier: [/PRMD=icl/ADMD=gold 400/C=GB/;win0109 0000012600001759]
Original-Encoded-Information-Types: undefined
X400-Content-Type: P2-1984 (2)
Content-Identifier: 1759
From: R.B.Jones@uucp.win0109
Message-Id: <"1759*/I=RB/S=Jones/OU=win0109/O=icl/PRMD=icl/ADMD=gold 400/C=GB/"@MHS>
To: info-hol@edu.uidaho.cs.ted
Subject: stripping failure


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;;

with:

evaluation failed    check valid -- CHOOSE

We can't see an easy and efficient way to fix this and intend to make the error 

message more friendly.  There are circumventions in ProofPower, however I don't 

know any equivalent for Cambridge HOL.

(In ProofPower using "step_strip_tac" a few times achieves the required effect 
reliably.  "step_strip_tac" is like "strip_tac" (which is the closest thing we 
have to STRIP_TAC) except that it steps the stripping of assumptions while they 

are still on the left hand side of an implication in the conclusion of the goal.
  
Also we have "rename_tac" which renames the bound variables in the goal so that 

the problem does arise with "strip_tac" either.)

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)


Roger Jones,
International Computers Limited