Re: [PVS-Help] Showing all type predicates for a skolem constant

[Sam Owre <owre@xxxxxxxxxxx>]

Hi Ronny,

Sorry I couldn't answer earlier - I'm on vacation with a connection that
is not so good.

The all-typepreds command basically tries to bring in typepreds that
would not otherwise be processed by the ground-prover, in particular, 
defined predicates, propositional connectives (aside from conjunction),
and quantified expressions will be added, but all others ignored.
I'm going to update the document string for all-typepreds to make this
clear.

If you want more capabilities, you can look at all-typepreds in the
src/prover/strategies.lisp file, and make your own strategy based on it.
Feel free to ask if you have any questions.

Regards,
Sam

Ronny Wichers Schreur <ronny@cs.ru.nl> wrote:

> Hello Cesar,
> 
> You write:
> > It may be that the strategy all-typepreds only displays user  defined
> > type predicates. I'm not sure how to get the implicit  predicate N >= 0.
> 
> I get the same behaviour with a user-defined type (see below).
> 
> 
> Cheers,
> 
> Ronny Wichers Schreur
> 
> --------------------------------------
> typepred: THEORY
> BEGIN
>      T: TYPE = {MinusOne, Zero, One}
> 
>      ordinal (t:T): nat
>          =   CASES t OF
>                  MinusOne: 0,
>                  Zero: 1,
>                  One: 2
>              ENDCASES
> 
>      ;< (x,y: T): bool
>          =    ordinal (x) < ordinal (y)
>      ;>=(x,y: T): bool
>          =    ordinal (x) >= ordinal (y)
> 
>      natT: NONEMPTY_TYPE = {x: T | x >= Zero} CONTAINING Zero
>      belowT(i: T): TYPE = {s: T | s < i}  % may be empty
> 
>      natL: LEMMA
>          FORALL (n: natT):
>              n >= Zero
> 
>      belowL: LEMMA
>          FORALL (n: belowT (One)):
>              n >= Zero
> 
> END typepred
> --------------------------------------