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

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

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


Ronny Wichers Schreur

typepred: THEORY
     T: TYPE = {MinusOne, Zero, One}

     ordinal (t:T): nat
         =   CASES t OF
                 MinusOne: 0,
                 Zero: 1,
                 One: 2

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