Reply-To: info-hol@ted
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@ted.cs.uidaho.edu
To: info-hol@edu.uidaho.cs.ted
Subject: Re: witnesses
In-Reply-To: Your message of Wed, 06 Nov 91 17:23:07 -0800. <199111070123.AA09813@panther.cs.uidaho.edu>
Date: Thu, 07 Nov 91 14:34:20 +0000
From: Tom.Melham@uk.ac.cam.cl
Message-Id: <"swan.cl.ca.784:07.10.91.14.34.30"@cl.cam.ac.uk>


Polymorphic existential witnesses.
----------------------------------

In general, when you have a goal of the form

    [1]      ?x:*. P[x]

you must supply as a witness some term of type *.  It is just not
possible to instantiate the type * to some type ty in the hope of
supplying a witness this type.  The goal [1] behaves as if there
is a universal quantification over the type variable *.

For the special case in Phil's query:

    [2]      ?x:*. I x = x

the constant I (defined in the theory combin) has the property that

    [3]      |- !x. I x = x             (called I_THM)

so rewriting with this theorem will solve [2].  Note that I is BOTH
the name of an ML function and the name of a logical constant in the
built-in theory hierarchy. Another proof would be

    EXISTS_TAC "foo:*" THEN MATCH_ACCEPT_TAC I_THM

In this case, it doesn't really matter what you supply as the witness,
since the equation I x = x  is true for all values of x.  In particular,
you don't need to use epsilon.

Tom