[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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



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
-------------------------------------------

Thanks in advance for your answer.


Cheers,

Ronny Wichers Schreur