Reply-To: info-hol@ted
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@ted.cs.uidaho.edu
Date: Thu, 7 Nov 91 10:43:15 PST
From: paul@edu.stanford.cis (Paul N. Loewenstein)
Message-Id: <9111071843.AA23035@cis.Stanford.EDU>
To: info-hol@edu.uidaho.cs.ted
In-Reply-To: "Phil Windley"'s message of Thu, 07 Nov 91 08:07:34 -0800 <199111071607.AA10112@panther.cs.uidaho.edu>
Subject: witnesses


The implicit universal quantification of types does lead to some
inelegant theorems, especially theorems stating counterexamples, where
one would like to existentially quantify the type. In practice, one
can (usually) merely prove the theorem for a specific existential
witness. (The exception would be for non-constructive proofs by
contradiction, but I can't think of any example).  Since types are not
printed by default, the theorem "looks" clean.

The implicit universal quantification of types often precludes the
generation of theorems which are negations of (failed) goals containing
type variables, since it is not possible to propagate the ~ to the
outside of the implicit universal quantifiers.

These circumstances usually occur in the derivation of background theory,
rather than in proofs of hardware correctness.

          Paul.