# Re: [PVS-Help] elementary prove questions

```
As Cesar's response indicates, an uninterpreted type, i.e., one that is
is declared without a definition, can be empty (under a theory interpretation)
so that declaring a constant of that type is potentially problematic.

For the second part of your question, you can do
M-x show-skolem-constants
to see the active skolem constants so that you can use it to
instantiate the antecedent universal quantifier.  Thanks to a
complaint of Mooij and Wesselink,  there is a
fix in the forthcoming version of PVS to automatically use skolem
constants for heuristic instantiation in commands like inst? and grind.
With this,  (lemma "c") (grind) gets it.

Cheers,
Shankar

>
> Since PVS 2.?, types can be empty. Then
> t:TYPE
> does not guarantee that exists an element of type t.
>
> To get around this problem you have to explicitly declare t to be a
> non-empty type, e.g.,
>
> t:TYPE+
>
> then you can define
> a:t
>
> and no tcc will be generated.
>
> Cesar
>
> On Tue, 2005-11-15 at 14:04, Vladimir Voevodsky wrote:
> > Hello,
> >
> > questions:
> >
> > 1. I am looking at the theory:
> >
> > try1: theory
> > begin
> > t:type
> > a:t
> > end try1
> >
> > When I try to typecheck I get a tcc asking me to prove that t is non-
> > empty. On the other hand looking at the examples in the wift-tutorial
> > (e.g. the phonebook) I got the impression that a:t would be treated
> > as a declaration of a member in t and that it would imply rather than
> > require that t is non-empty.
> >
> > 2. I am looking at the theory
> >
> > try2: Theory
> > Begin
> >    t: type
> >    c: axiom exists (x: t): true
> >    a: bool = (Forall (x: t): x/=x)
> >    b: Theorem not a
> > End try2
> >
> > How can I prove the theorem? If I add a line d:t then I get (as in 1)
> > a tcc which I can then prove using c. After that (grind) proves the
> > theorem. But I was not able to use c directly without an explicit
> > line saying d:t.
> >
> > Thank you,