Reply-To: info-hol@ted
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@ted.cs.uidaho.edu
Message-Id: <9111070329.AA11762@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 PST." <199111070123.AA09813@panther.cs.uidaho.edu>
Date: Wed, 06 Nov 91 20:29:41 MST
From: jimaf@edu.uidaho.cs.ted

> g(
> "? x:* . I x = x"
> );;
>
> Is this a theorem?????  I just ran up against it and its time to go home,
> so I haven't had time to think it through.  I believe its a theorem, but...

As a first pass:

I is a predefined ML identifier, not HOL identifier. I can use it in tactics
but not in goals (I believe).

Anyway if you define IDENT

let IDENT = new_definition(`IDENT`,"!x:*. IDENT x = x");;

then using IDENT instead of I, you can always use REWRITE_TAC[IDENT].
There has to be a better way, and I know you probably want to use the
built in identity function, but I'm not sure how you can get ML to
evaluate the term to reduce I x to x.

-Jim AF