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

```There is a strategy in PVS called all-typepreds that is supposed to do
that. However, in your example, we get everything but N >= 0:

Rule? (all-typepreds 1)
Generating typepreds for expressions:
0
3
N
>=
this simplifies to:
below :

{-1}  total_order?[real](>=)
{-2}  N < 3
{-3}  3 > 0
{-4}  odd?(3)
{-5}  0 >= 0
{-6}  even?(0)
|-------
[1]   N >= 0

Cesar
On Thu, 2006-12-14 at 13:04, Ronny Wichers Schreur wrote:
> Hello,
>
> I'd like to know how to make all type predicates explicit.
> Consider the following theory:
> -------------------------------------------
> typepreds: THEORY
> BEGIN
>      nat: LEMMA
>          FORALL (n: nat):
>              n >= 0
>
>      below: LEMMA
>          FORALL (n: below (3)):
>              n >= 0
> END typepreds
> -------------------------------------------
>
> and the following proof for "nat":
>
> -------------------------------------------
> nat :
>    |-------
> {1}   FORALL (n: nat): n >= 0
>
> Rule? (skolem + "N")
> For the top quantifier in +, we introduce Skolem constants: N,
> this simplifies to:
> nat :
>    |-------
> {1}   N >= 0
>
> Rule? (typepred "N")
> Adding type constraints for  N,
> this simplifies to:
> nat :
> {-1}  N >= 0
>    |-------
> [1]   N >= 0
>
> which is trivially true.
> Q.E.D.
> -------------------------------------------
>
> If I use the same proof steps for "below" I get:
>
> -------------------------------------------
> below :
>    |-------
> {1}   FORALL (n: below(3)): n >= 0
>
> Rule? (skolem + "N")
> For the top quantifier in +, we introduce Skolem constants: N,
> this simplifies to:
> below :
>    |-------
> {1}   N >= 0
>
> Rule? (typepred "N")
> Adding type constraints for  N,
> this simplifies to:
> below :
> {-1}  N < 3
>    |-------
> [1]   N >= 0
> -------------------------------------------
>
> Now below(3) = {s: nat | s < 3} so the type predicate "N >= 0"
> also holds, but PVS doesn't show it. Evidently PVS does know
> the predicate, because an assert proves the lemma.
>
> -------------------------------------------
> below :
> {-1}  N < 3
>    |-------
> [1]   N >= 0
> Rule? (assert)
> Simplifying, rewriting, and recording with decision procedures,
> Q.E.D.
> -------------------------------------------
>
> My question is how to make all type predicates explicit,
> so that the sequent is:
>
> -------------------------------------------
> {-1}  N < 3
> {-2}  N >= 0
>    |-------
> [1]   N >= 0
> -------------------------------------------
>