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

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
  >=
Adding type information on subexpressions,
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
> -------------------------------------------
> 
> Thanks in advance for your answer.
> 
> 
> Cheers,
> 
> Ronny Wichers Schreur
-- 
Cesar A. Munoz H., Senior Staff Scientist     mailto:munoz@nianet.org
National Institute of Aerospace        mailto:C.A.Munoz@larc.nasa.gov
100 Exploration Way, Room 214       http://research.nianet.org/~munoz
Hampton, VA 23666, USA   Tel. +1 (757) 325 6907 Fax +1 (757) 325 6988
GPGP Finger Print: 9F10 F3DF 9D76 1377 BCB6  1A18 6000 89F5 C114 E6C4