Return-Path: <john.harrison-request@uk.ac.cam.cl>
Delivery-Date: 
Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) 
          id <24079-0@swan.cl.cam.ac.uk>; Tue, 28 Jul 1992 22:50:09 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA01939;
          Tue, 28 Jul 92 14:43:41 -0700
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Received: from Ucthpx.UCT.AC.ZA by ted.cs.uidaho.edu (16.6/1.34) id AA01934;
          Tue, 28 Jul 92 14:43:21 -0700
Received: by ucthpx.uct.ac.za (/\==/\ Smail3.1.24.1 #24.2) id m0mCzHu-000O3TC;
          Tue, 28 Jul 92 23:40 SAST
Received: by UCT_elc.mth.uct.ac.za (4.1/SMI-4.1) id AA03441;
          Tue, 28 Jul 92 23:36:26+020
Date: Tue, 28 Jul 92 23:36:26+020
From: gavan@za.ac.uct.mth.UCT_elc (Gavan Tredoux)
Message-Id: <9207282136.AA03441@UCT_elc.mth.uct.ac.za>
To: info-hol@edu.uidaho.cs.ted
Subject: CHOOSE breaks

In the process of complex proof, I've managed to break
REPEAT STRIP_TAC, due to an error in CHOOSE. Here's a
cut and paste of the error - the goal won't make much sense
because it depends on all sorts of theories.

------------------------------------------------------------------------------

"(c1 e /\ ~TERM e \/
  (?e1 e2.
    c1 e1 /\ TERM e1 /\ c2 e2 /\ (first e2 = last e1) /\ (e = e1 <*> e2))) /\
 ~TERM e \/
 (?e1 e2.
   (c1 e1 /\ ~TERM e1 \/
    (?e1' e2.
      c1 e1' /\
      TERM e1' /\
      c2 e2 /\
      (first e2 = last e1') /\
      (e1 = e1' <*> e2))) /\
   TERM e1 /\
   c3 e2 /\
   (first e2 = last e1) /\
   (e = e1 <*> e2)) ==>
 c1 e /\ ~TERM e \/
 (?e1 e2.
   c1 e1 /\
   TERM e1 /\
   (c2 e2 /\ ~TERM e2 \/
    (?e1 e2'.
      c2 e1 /\
      TERM e1 /\
      c3 e2' /\
      (first e2' = last e1) /\
      (e2 = e1 <*> e2'))) /\
   (first e2 = last e1) /\
   (e = e1 <*> e2))"

() : void

REPEAT STRIP_TAC;;
- : tactic

e it;;
OK..
evaluation failed     check_valid -- CHOOSE

STRIP_TAC;;
e it;;
- : tactic

OK..
evaluation failed     check_valid -- CHOOSE

DISCH_THEN STRIP_ASSUME_TAC;;
- : tactic

e it;;
OK..
evaluation failed     check_valid -- CHOOSE

--------------------------------------------------------------------------------

STRIP_TAC fails too, as does DISCH_THEN STRIP_ASSUME_TAC
I did prove the goal though, by manually cutting it
up. REPEAT STRIP_TAC should never fail, not should
STRIP_ASSUME_TAC th for any th. 

I'm running on a SUN SPARC (ELC), HOL version 2.0, built
with AKCL 1.605 . Duplicating this would require
ftp-ing a whole series of theories and some other ML code
from me, so I can't give more detail than I have.

Suggestions?

Gavan Tredoux
Dept Math / Dept Philosophy
UCT