Via:  uk.ac.nsf; 1 Jun 89 22:10 BST  (UK.AC.Cam.Cl.scaup)
From: mcvax!win.icl.stc.co.uk!rbj@net.uu.uunet
Date: Wed, 31 May 89 10:41:42 GMT
Message-Id: <8905311041.AA03121@plug.win.icl.stc.co.uk>
To: info-hol@edu.ucdavis.clover
Subject: STRIP_ASSUME_TAC and derivatives
Sender: "mcvax!win.icl.stc.co.uk!rbj" <mcvax!win.icl.stc.co.uk!rbj%net.uu.uunet@edu.ucdavis.clover>
Status: R

A Conundrum for HOL HACKERS
+++++++++++++++++++++++++++


I have recently noticed a little problem with STRIP_ASSUME_TAC
and things which use it (like STRIP_TAC).

When chosing witnesses for existential quantifiers (which it conveniently
eliminates), it does not always succeed in chosing witnesses which occur
nowhere as free variables.
The immediate effect of this may be pleasant,
since this may shorten the following proof,
but the ultimate effect not so pleasant,
since "save_top_thm" will fail to validate the proof.

The problem occurs when there are nested existentials using the same name
which are both eliminated by STRIP_ASSUME_TAC.

e.g. in "?x. ((x=2) /\ ?x.~(x=2))"
(STRIP_ASSUME_TAC on this theorem should shorten any proof wonderfully,
up to a point)

Looking at STRIP_ASSUME_TAC it isn't at all clear how to fix the problem.
I got round it in my proof by writing a little conversion which eliminates
nested bindings of the same variable by alpha conversion.
Incorporating this into STRIP_ASSUME_TAC would however slow down all uses
of STRIP_ASSUME_TAC which didn't need it.
We could add a variant called STEALTHY_STRIP_ASSUME_TAC, but when I was
on the point of producing this tactic I realised that my conversion doesn't
do enough.

The problem isn't confined to nested bindings, or even to bindings.
I would guess that even "(x=2) /\ ?x.~(x=2)" would fail, or possibly
even "(x'=2) /\ ?x.~(x=2)" (where there are no name clashes at all)
if "x" occurred free in the list of assumptions. (I haven't tried them however)

Can anyone solve this problem?

(I'll send out my conversion if anyone wants it)

Roger Jones