Return-Path:
Return-Path: <john.harrison-request@uk.ac.cam.cl>
Received: from cl.cam.ac.uk by swan.cl.cam.ac.uk with SMTP (PP) to cl
          id <06653-0@swan.cl.cam.ac.uk>; Thu, 7 Nov 1991 10:50:23 +0000
To: Phil Windley <windley@edu.uidaho.cs.panther>
cc: info-hol@edu.uidaho.cs.ted, John.Harrison@uk.ac.cam.cl
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 10:50:16 +0000
From: John.Harrison@uk.ac.cam.cl
Message-ID: <"swan.cl.ca.687:07.10.91.10.51.00"@cl.cam.ac.uk>


This particular case:

> #g "?x:*. I x = x";;
> "?x. I x = x"

could be solved just by

> #e(REWRITE_TAC[I_THM]);;
> OK..
> goal proved
> |- ?x. I x = x

In more general cases you can prove something like:

  "(!x. P x) ==> (?x. P x)"

by using just "@x:*.T" (or anything other than T)
as a witness, exploiting the fact that types are
non-empty, e.g.

> #g "!P:*->bool. (!x. P x) ==> (?x. P x)";;
> "!P. (!x. P x) ==> (?x. P x)"
>
> () : void
>
> #e (GEN_TAC THEN DISCH_TAC THEN
> #   EXISTS_TAC "@x:*.T" THEN ASM_REWRITE_TAC[]);;
> OK..
> goal proved
> |- !P. (!x. P x) ==> (?x. P x)
>
> Previous subproof:
> goal proved
> () : void

Maybe it would be easier to use if one proved it in
the form "!P:*->bool. ($! P) ==> ($? P)", then it
could be used as a lemma more easily without worrying
about lambda-conversions.

John.

==============================================================================
John Harrison (jrh@cl.cam.ac.uk)

Hardware Verification Group
University of Cambridge Computer Laboratory
New Museums Site
Pembroke Street
Cambridge CB2 3QG
England.
==============================================================================