Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
To: win0109!R.B.Jones@uk.ac.cam.cl
Cc: info-hol@edu.uidaho.cs.ted, Tom.Melham@uk.ac.cam.cl
Subject: Re: stripping failure
In-Reply-To: Your message of Thu, 30 Jul 92 15:46:23 +0100.
Date: Sun, 02 Aug 92 17:41:46 +0100
From: Tom Melham <Tom.Melham@uk.ac.cam.cl>
Message-Id: <"swan.cl.ca.423:02.07.92.16.42.12"@cl.cam.ac.uk>


Roger 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;;
> 
> with:
> 
> evaluation failed    check valid -- CHOOSE


I assume we actually mean 

    "(?x:*.(?(y:*)(x:*). P x y) /\ Q (x:*)) ==> F"

here, in which case I thought this problem looked vaguely familiar. 
Checking my "bugs" directory, I discovered that I had come across
this bug and developed a fix for it back in 1987 ... but never installed
it!  Moreover, it came up again (from Roger Jones) in 1989 and again
failed to get installed.  For information, my email to info-hol on
the matter dated 1 June 1989 is attached.

The change will be installed in version 2.01, unless someone can find
a problem with it.  It also fixes Gavin's problem, by the way.

I also have a related uninstalled bugfix for DISJ_CASES_THEN2.

Tom

=== info-hol message of 89.06.01 ==========================================


RE: Roger Jones' recently reported bug.
=======================================

I can help with this one.  The problem Roger mentioned looked vaguely
familiar, so I had a look in my "bugs" archive.  Sure enough, I found
something that's relevant.  In fact, as it happens, I spotted this bug a while
ago (in 1987, actually) developed a peliminary fix for it.  I then forgot to
install it!  Sorry about that.

The problem is due to a bug in X_CHOOSE_THEN, which just throws away the
assumptions of its input theorem.  Here is the original code (defined in
tacont.ml):

let X_CHOOSE_THEN y ttac xth :tactic =
    let x,body = dest_exists (concl xth) ? failwith `X_CHOOSE_THEN` in
    \(asl,w). 
        let gl,prf = ttac (ASSUME (subst [y,x] body)) (asl,w) in
	gl, (CHOOSE (y, xth)) o prf;;

Here is the bug fix I developed, but forgot to install:

let X_CHOOSE_THEN y ttac xth :tactic =
    let x,body = dest_exists (concl xth) ? failwith `X_CHOOSE_THEN` in
    \(asl,w). 
	let th = itlist ADD_ASSUM (hyp xth) (ASSUME (subst [y,x] body)) in
        let gl,prf = ttac th (asl,w) in
	gl, (CHOOSE (y, xth)) o prf;;

I think this is right.  I'll have another careful look at it, and (if it's ok)
we'll install it in the next release.  Meanwhile, to patch your system, just
replace X_CHOOSE_THEN as shown above.  Let me know if there are any problems.

Tom