pvsprelude

The PVS Prelude

Sam Owre, John Rushby, and N. Shankar

Computer Science Laboratory

SRI International Menlo Park CA USA

                     booleans

% booleans declares the type boolean and its abbreviation bool, along
% with the usual boolean constants and connectives.  The prover provides
% the meaning for these connectives.
booleans: THEORY
BEGIN
boolean: TYPE
bool: TYPE = boolean
true, false: boolean
not: [bool -> bool]
and, &, or, implies, =>, when, iff, <=>: [bool,bool -> bool]
END booleans

                    equalities
% equalities contains the declaration for =, plus properties stating
% that it is an equivalence relation
equalities [t: TYPE] : THEORY
BEGIN
=: [t, t -> boolean]
reflexivity_of_equals : POSTULATE (FORALL (x : t) : x = x)
transitivity_of_equals : POSTULATE
    (FORALL (x, y, z: t) : x = y AND y = z
                   IMPLIES x = z)
symmetry_of_equals : POSTULATE
    (FORALL (x, y : t) : x = y IMPLIES y = x)
END equalities

                       notequal

% notequal defines /= in terms of =.  It is in a separate theory in
% order to properly bootstrap the system.
notequal [t: TYPE] : THEORY
 BEGIN
  /=: [t, t -> boolean] = (LAMBDA (a,b:t): NOT(a=b))
 END notequal

                        if def
% if_def provides the polymorphic declaration of the IF-THEN-ELSE
% connective, along with some basic properties.  Note that the
% declaration for IF is for a 3-ary function, and that the IF-THEN-ELSE
% form is simply an alternative form.
if_def [t: TYPE] : THEORY
 BEGIN
  IF:[bool,t,t -> t]
  IF_true : POSTULATE
    (FORALL (x, y : t) : IF true THEN x ELSE y ENDIF = x)
  IF_false : POSTULATE
    (FORALL (x, y : t) : IF false THEN x ELSE y ENDIF = y)
  IF_same : LEMMA
    (FORALL (b : bool), (x : t) : IF b THEN x ELSE x ENDIF = x)
 END if_def

                   defined types

% defined_types provides the declarations for types pred and setof
defined_types [t: TYPE] : THEORY
BEGIN
pred: TYPE = [t -> bool]
PRED: TYPE = [t -> bool]
predicate: TYPE = [t -> bool]
PREDICATE: TYPE = [t -> bool]
setof: TYPE = [t -> bool]
SETOF: TYPE = [t -> bool]
END defined_types

                       epsilons

% epsilons provides a "choice" function; given a predicate over a type
% t, epsilon produces an element of t, which satisfies the predicate if
% any element of t does - otherwise it is an arbitrary element of t.
% Note that the original type t must be nonempty.
epsilons [t : TYPE] : THEORY
 BEGIN
  epsilon: [pred[t] -> t]
  epsilon_ax: AXIOM
        FORALL (p: pred[t]) :
                (EXISTS (x: t) : p(x)) => p(epsilon(p))
 END epsilons

                      functions
% functions provides the basic properties of functions.  Because of the
% type equivalence of [[t1,...,tn] -> t] and [t1,...,tn -> t], this
% theory handles any function arity.  Note that the definition of
% inverse uses epsilon; in practice this definition will only be useful
% for injective functions.
functions [dom,rng: TYPE] : THEORY
 BEGIN
  extensionality : AXIOM
     (FORALL (f, g : [dom -> rng]) :
        (FORALL (x : dom) : f(x) = g(x) IMPLIES f = g))
  eta : LEMMA
    (FORALL (f : [dom -> rng]) :
       (LAMBDA (x : dom) : f(x)) = f)
  injective? : pred[[dom -> rng]]
        = (LAMBDA (f:[dom->rng]):
           (FORALL (x,y:dom): (f(x) = f(y) => (x = y))))
  surjective? : pred[[dom -> rng]]
        = (LAMBDA (f:[dom->rng]):
           (FORALL (y:rng): (EXISTS (x:dom): f(x) = y)))

functions (continued)

bijective? : pred[[dom -> rng]]
      = (LAMBDA (f:[dom->rng]): injective?(f) & surjective?(f))
inverse : [[dom -> rng] -> [rng -> dom]]
      = (LAMBDA (f:[dom->rng]): (LAMBDA (y:rng):
              (epsilon(lambda (x:dom): f(x) = y))))
bijective_inverse: LEMMA
  (FORALL (f:(bijective?)),(x:dom),(y:rng):
     inverse(f)(y) = x IFF y = f(x))
END functions

                       sets
% sets provides the polymorphic set type, along with the usual set
% operations.  It is important to bear in mind that a set is equivalent
% to a predicate.
sets [T: TYPE] : THEORY
BEGIN
set: TYPE = setof[T]
member(x:T,a:set): bool = a(x)
union(a,b:set): set =
  {x:T | member(x,a) OR member(x, b)}
intersection(a,b:set): set =
  {x:T | member(x,a) AND member(x, b)}
difference(a,b:set) : set =
  {x:T | member(x,a) AND NOT member(x, b)}
add(x:T,a:set) : set =
  {y:T | x = y OR member(y, a)}

pvsprelude 10

sets (continued)

remove(x:T,a:set) : set =
  {y:T | x /= y AND member(y, a)}
singleton(x:T) : set = {y:T | y = x}
subset?(a,b:set) : bool = (FORALL (z:T) : member(z, a) => member(z, b))
strict_subset?(a,b:set) : bool = subset?(a, b) & a /= b
empty?(a:set) : bool = (FORALL (x:T) : NOT member(x,a))
emptyset: set = {x:T | false}
nonempty?(a:set) : bool = NOT empty?(a)
fullset: set = {x:T | true}
disjoint?(a,b:set) : bool = empty?(intersection(a,b))
extensionality: LEMMA
  FORALL (a,b: set) :
    (FORALL (x:T) : member(x, a) = member(x, b)) => (a = b)
END sets

pvsprelude 11

                     identity

% identity simply defines the identity function.
identity[t:TYPE] : THEORY
BEGIN
I: (bijective?[t,t]) = (LAMBDA (x:t): x)
id: (bijective?[t,t]) = I
identity: (bijective?[t,t]) = I
END identity

                    function image

% function_image provides the image and inverse_image functions.
% inverse_image is not the same as inverse; it is defined for all
% functions, not just injections.
function_image [dom, rng : TYPE] : THEORY
 BEGIN
  image : [[dom -> rng], set[dom] -> set[rng]]
        = (LAMBDA (f:[dom->rng]),(X:set[dom]):
            {y:rng | (EXISTS (x:(X)): y = f(x))})
  inverse_image : [[dom -> rng], set[rng] -> set[dom]]
        = (LAMBDA (f:[dom->rng]),(Y:set[rng]):
            {x:dom | member(f(x), Y)})
END function_image

                    function props

% function_props defines function composition.  It can't be defined in
% functions because it involves three type parameters.
function_props [t1,t2,t3: TYPE] : THEORY
 BEGIN
  o(f:[t2->t3],g:[t1->t2]): [t1->t3] = (LAMBDA (x:t1): f(g(x)))
 END function_props

                   function props2

% function_props2 defines the associativity of function composition.  It
% can't be defined in function_props because it involves four type
% parameters.
function_props2 [t1,t2,t3,t4: TYPE] : THEORY
 BEGIN
  assoc: LEMMA (FORALL (f:[t3->t4]),(g:[t2->t3]),(h:[t1->t2]):
                 (f o g) o h = f o (g o h))
 END function_props2

                      numbers
% numbers is the most general of the numeric types.  It defines the
% usual operators.  Note that the type of the denominator is nonzero,
% and that '-' is overloaded.
numbers: THEORY
BEGIN
number: TYPE
nonzero_number: TYPE = {r: number | r /= 0} CONTAINING 1;
+: [number,number -> number]
-: [number,number -> number]
*: [number,number -> number]
/: [number,nonzero_number -> number]
-: [number -> number]
<: [number,number -> bool]
<=(x,y:number): bool = x < y OR x = y;
>(x,y:number): bool = y < x;
>=(x,y:number): bool = y <= x;
END numbers

                       reals
% reals defines the real numbers as an uninterpreted subtype of number.
% The basic number operations are redeclared in order to specify that
% they are closed, e.g. the sum of two reals is a real number.
reals: THEORY
BEGIN
real: TYPE FROM number
nonzero_real: TYPE = {r: real | r /= 0} CONTAINING 1;
nzreal: TYPE = nonzero_real
closed_plus: AXIOM (FORALL (x,y:real): real_pred(x + y))
closed_minus: AXIOM (FORALL (x,y:real): real_pred(x - y))
closed_times: AXIOM (FORALL (x,y:real): real_pred(x * y))
closed_divides: AXIOM (FORALL (x:real),(y:nzreal): real_pred(x / y))
closed_neg: AXIOM (FORALL (x:real): real_pred(-x)) ;
+(x,y:real): real = numbers.+(x,y) ;
-(x,y:real): real = numbers.-(x,y) ;
*(x,y:real): real = numbers.*(x,y) ;
/(x:real, y:nzreal): real = numbers./(x,y) ;
-(x:real): real = numbers.-(x) ;
END reals

                     rationals

% rationals defines the rational numbers as an uninterpreted subtype of real.
% The basic number operations are redeclared in order to specify that
% they are closed, e.g. the sum of two rationals is a rational.
rationals: THEORY
BEGIN
rational: TYPE FROM real
rat: TYPE = rational
nonzero_rational: TYPE = {r: rational | r /= 0} CONTAINING 1
nzrat: TYPE = nonzero_rational
closed_plus: AXIOM (FORALL (x,y:rat): rational_pred(x + y))
closed_minus: AXIOM (FORALL (x,y:rat): rational_pred(x - y))
closed_times: AXIOM (FORALL (x,y:rat): rational_pred(x * y))
closed_divides: AXIOM (FORALL (x:rat),(y:nzrat): rational_pred(x / y))
closed_neg: AXIOM (FORALL (x:rat): rational_pred(-x)) ;
+(x,y:rat): rat = numbers.+(x,y);
-(x,y:rat): rat = numbers.-(x,y);
*(x,y:rat): rat = numbers.*(x,y);
/(x:rat,y:nzrat): rat = numbers./(x,y);
-(x:rat): rat = numbers.-(x);
END rationals

                     integers

% integers defines the integers as an uninterpreted subtype of rational.
% The basic number operations are redeclared in order to specify that
% they are closed, e.g. the sum of two integers is an integer.
integers: THEORY
BEGIN
integer: TYPE FROM rational
int: TYPE = integer
closed_plus: AXIOM (FORALL (x,y:int): integer_pred(x + y))
closed_minus: AXIOM (FORALL (x,y:int): integer_pred(x - y))
closed_times: AXIOM (FORALL (x,y:int): integer_pred(x * y))
closed_neg: AXIOM (FORALL (x:int): integer_pred(-x)) ;
+(x,y:int): int = numbers.+(x,y) ;
-(x,y:int): int = numbers.-(x,y) ;
*(x,y:int): int = numbers.*(x,y) ;
-(x:int): int = numbers.-(x) ;
END integers

                  naturalnumbers

% naturalnumbers defines the natural numbers as a subtype of integer.
% The sum and product operations are redeclared in order to specify that
% they are closed, e.g. the sum of two natural numbers is a natural
% number.  The posnat type is defined here, as are the successor and
% predecessor functions.
naturalnumbers: THEORY
BEGIN
naturalnumber: TYPE = {x:integer | x >= 0} CONTAINING 0
nat : TYPE = naturalnumber
posnat: TYPE = {n:nat | n > 0}
posint: TYPE = posnat
+(x,y:nat): nat = numbers.+(x,y) ;
*(x,y:nat): nat = numbers.*(x,y) ;
suc(x:nat): nat = x + 1
prd(x:nat): nat = IF x > 0 THEN x - 1 ELSE 0 ENDIF
END naturalnumbers

                     nat types

% nat_types defines some useful subtypes of the natural numbers.
nat_types[m: nat] : THEORY
BEGIN
upto:   TYPE = {s: nat | s <= m} CONTAINING m
upfrom: TYPE = {s: nat | s >= m} CONTAINING m
below:  TYPE = {s: nat | s < m}
above:  TYPE = {s: nat | s > m} CONTAINING m + 1
END nat_types

                   function iterate

% function_iterate provides the iterate function, which composes a
% function with itself a specified number of times.  The function must
% have the same domain and range.  Two useful properties of iterate are
% also provided.
function_iterate[t: TYPE] : THEORY
 BEGIN
  iterate(f: [t -> t], n: nat): RECURSIVE [t -> t] =
    (LAMBDA (x: t):
       IF n = 0 THEN x ELSE iterate(f, n-1)(f(x)) ENDIF)
    MEASURE (LAMBDA (f: [t -> t]), (n: nat): n)
  iterate_add: LEMMA
    (FORALL (f: [t -> t]), (m, n: nat):
      iterate(f,m) o iterate(f,n) = iterate(f, m + n))
  iterate_mult: LEMMA
    (FORALL (f: [t -> t]), (m, n: nat):
      iterate(iterate(f,m), n) = iterate(f, m * n))
 END function_iterate

                     sequences
% sequences provides the polymorphic sequence type, as a function from
% nat to the base type.  The usual sequence functions are also provided.
% Note that these are infinite sequences, and do not contain finite
% sequences as a subtype.
sequences[t: TYPE] : THEORY
BEGIN
sequence : TYPE = [nat->t]
nth(seq: sequence, n: nat): t = seq(n)
suffix(seq:sequence, n:nat): sequence =
  (LAMBDA (i:nat): seq(i+n))
first(seq: sequence): t = nth(seq, 0)
rest(seq: sequence): sequence = suffix(seq, 1)
delete(n : nat, seq : sequence) : sequence =
    (LAMBDA (i : nat) :
           (IF i < n THEN seq(i)
               ELSE seq(i + 1) ENDIF))

pvsprelude 23

sequences (continued)

insert(x:t, n:nat, seq:sequence) : sequence =
       (LAMBDA (i : nat) :
           (IF i < n THEN seq(i)
             ELSIF i = n THEN x
               ELSE seq(i - 1) ENDIF))
add(x:t, seq:sequence) : sequence =
   insert(x, 0, seq)
insert_delete : LEMMA
  (FORALL (n : nat), (seq : sequence) :
    insert(nth(seq, n), n, delete(n, seq)) = seq)
add_first_rest : LEMMA
  (FORALL (seq : sequence) :
    add(first(seq), rest(seq)) = seq)
every(p: pred[t], seq: sequence): bool =
  (FORALL (n:nat): p(nth(seq, n)))
seq_induction : LEMMA
  (FORALL (p: pred[t]), (seq: sequence) :
       p(nth(seq,0)) AND
       (FORALL (n : nat) : p(nth(seq, n)) IMPLIES p(nth(seq, n + 1)))
    IMPLIES every(p, seq))
END sequences

                    seq functions

% seq_functions defines the map function that generates the image of a
% sequence under a function.
seq_functions[t1,t2: TYPE] : THEORY
 BEGIN
  map(f: [t1 -> t2], s: sequence[t1]): sequence[t2] =
    (LAMBDA (n: nat): f(nth(s,n)))
 END seq_functions

                     relations

% relations defines properties that are useful in specifying binary
% relations.
relations [T : TYPE] : THEORY
BEGIN
reflexive?(R: pred[[T,T]]) : bool =
  FORALL (x:T) : R(x, x)
irreflexive?(R: pred[[T,T]]) : bool =
  FORALL (x:T) : NOT R(x, x)
symmetric?(R: pred[[T,T]]) : bool =
  FORALL (x, y:T) : R(x, y) IMPLIES R(y, x)
antisymmetric?(R: pred[[T,T]]) : bool =
  FORALL (x,y:T) : R(x, y) & R(y, x) => x = y
transitive?(R: pred[[T,T]]) : bool =
  FORALL (x,y,z:T) : (R(x, y) & R(y, z) => R(x, z))
END relations

                   relation image

% relation_image defines the image and the converse of a relation.
relation_image [dom, rng : TYPE] : THEORY
BEGIN
image(R : pred[[dom, rng]], D : set[dom]) : set[rng] =
  {y : rng | (EXISTS (x : (D)) : R(x, y))}
converse(R : pred[[dom, rng]]) : pred[[rng, dom]] =
  (LAMBDA (y : rng), (x : dom) : R(x, y))
isomorphism?(R : pred[[dom, rng]]) : bool =
  (EXISTS (f : (bijective?[dom, rng])):
    (FORALL (x: dom) :(FORALL (y:rng): R(x, y) IFF f(x) = y)))
END relation_image

                      orders

% orders defines the usual ordering relations.
orders [T : TYPE] : THEORY
BEGIN
pre_order?(<=: pred[[T,T]]) : bool =
  reflexive?(<=) & transitive?(<=)
partial_order?(<=: pred[[T,T]]) : bool =
 pre_order?(<=) &
 antisymmetric?(<=)
strict_order?(<: pred[[T,T]]) : bool =
  irreflexive?(<) & antisymmetric?(<) & transitive?(<)
total_order?(<=: pred[[T,T]]) : bool =
  partial_order?(<=) & FORALL (x,y:T) : x <= y OR y <= x
tricotomous?(<: pred[[T,T]]) : bool =
  FORALL (x,y:T) : x < y OR y < x OR x = y
strict_total_order?(<: pred[[T,T]]) : bool =
  strict_order?(<) & tricotomous?(<)

orders (continued)

well_founded?(<=: pred[[T,T]]): bool =
   (FORALL (p: pred[T]):
      (EXISTS (y:T): p(y))
         IMPLIES (EXISTS (y:(p)):
                    (FORALL (x:(p)): (x <= y IMPLIES x = y))))
END orders

                     wf induction

% wf_induction defines induction for any type that has a well-founded
% relation.
wf_induction [T: type, <= : (well_founded?[T])] : THEORY
 BEGIN
  wf_induction: AXIOM
    (FORALL (p : pred[T]):
      (FORALL (x : T):
        (FORALL (y : T): y<=x AND y/= x IMPLIES p(y))
           IMPLIES p(x))
    IMPLIES
      (FORALL (x:T): p(x)))
 END wf_induction

                  measure induction

% measure_induction builds on well-founded induction.  It allows
% induction over a type T for which a measure function m is defined.
measure_induction
  [T, M : TYPE, m : [T -> M], <= : (well_founded?[M])] :  THEORY
 BEGIN
 measure_induction : LEMMA
  (FORALL (p : pred[T]) :
     (FORALL (x : T) :
         (FORALL (y : T): m(y) <= m(x) AND m(y) /= m(x) IMPLIES  p(y))
             IMPLIES p(x))
    IMPLIES (FORALL (x : T) : p(x)))
 END measure_induction

                   nat induction

% nat_induction provides both weak and strong induction on natural numbers.
nat_induction : THEORY
BEGIN
wf_nat: AXIOM well_founded?(LAMBDA (m,n:nat): m <= n)
nat_induction: LEMMA
  (FORALL (p: pred[nat]) :
     (p(0) AND (FORALL (j: nat): p(j) IMPLIES p(j+1)))
         IMPLIES (FORALL (i: nat):p(i)))
%Strong induction on naturals.
NAT_induction : LEMMA
  (FORALL (p: pred[nat]) :
      (FORALL (j: nat): (FORALL (k : nat) : k < j IMPLIES p(k)) IMPLIES p(j))
         IMPLIES (FORALL (i: nat):p(i)))
END nat_induction

                 bounded induction
% bounded induction provides induction over bounded natural numbers.
bounded_induction [m: nat] : THEORY
BEGIN
upto_induction: LEMMA
  (FORALL (p : pred[upto[m]]), (s: upto[m]):
    (p(0) AND (FORALL (r: upto[m]): r < m AND p(r) IMPLIES p(r + 1)))
        IMPLIES p(s))
upfrom_induction: LEMMA
  (FORALL (p : pred[upfrom[m]]), (s: upfrom[m]):
    (p(m) AND (FORALL (r: upfrom[m]): p(r) IMPLIES p(r + 1)))
         IMPLIES p(s))
below_induction: LEMMA
  (FORALL (p : pred[below[m]]), (s: below[m]):
    (m > 0 IMPLIES
       (p(0) AND (FORALL (r: below[m]): r < m - 1 AND p(r) IMPLIES p(r + 1)))
           IMPLIES p(s)))
above_induction: LEMMA
  (FORALL (p : pred[above[m]]), (s: above[m]):
    (p(m+1) AND (FORALL (r: above[m]): p(r) IMPLIES p(r + 1)))
        IMPLIES p(s))
END bounded_induction

                     cardinality
% cardinality provides the card function, which gives the cardinality of
% a finite set.  The f parameter gives a mapping from the naturals to
% the base type of the sets, and the m parameter gives an upper bound on
% the cardinality.  This is the most general cardinality function,
% making no assumptions on the base type T.  If T is known to be
% countable or finite, then the corresponding cardinality theories are
% probably more appropriate.
cardinality[T: TYPE, m : nat, f : [below[m] -> T]] : THEORY
 BEGIN
  fin : TYPE =
    {s : set[T] | (FORALL (x: (s)): (EXISTS (i:below[m]): f(i) = x)) AND
                  (FORALL (i, j: below[m]): s(f(i)) AND
                                       f(i) = f(j) IMPLIES i = j)}
         CONTAINING emptyset[T]
  cardi(s: fin, i: below[m]) : RECURSIVE nat =
    (IF i = 0 THEN IF s(f(i)) THEN 1 ELSE 0 ENDIF
              ELSIF s(f(i)) THEN cardi(s, i-1) + 1
              ELSE cardi(s, i-1) ENDIF)
    MEASURE (LAMBDA (s: fin), (i: below[m]): i)
  card(s: fin) : nat = IF m = 0 THEN 0 ELSE cardi(s, m-1) ENDIF
 END cardinality

                countable cardinality

% countable_cardinality provides the ccard function, which gives the
% cardinality of a finite set whose base type is known to be countable.
% The f parameter gives a bijective mapping from the naturals to the base
% type of the sets, and the m parameter gives an upper bound on the
% cardinality.  This form of cardinality is useful when the base type is
% countable, as the finite subsets are easier to deal with.
countable_cardinality[T: TYPE, m: nat, f : (injective?[below[m], T])] : THEORY
 BEGIN
  cfin : TYPE =
    {s : set[T] | (FORALL (x: (s)) :(EXISTS (i: below[m]): f(i) = x))}
    CONTAINING emptyset[T]
  ccardi(s: cfin, i: below[m]) : RECURSIVE nat =
    (IF i = 0 THEN IF s(f(i)) THEN 1 ELSE 0 ENDIF
              ELSIF s(f(i)) THEN ccardi(s, i-1) + 1
              ELSE ccardi(s, i-1) ENDIF)
    MEASURE (LAMBDA (s: cfin), (i: below[m]): i)
  ccard(s: cfin) : nat = IF m = 0 THEN 0 ELSE ccardi(s, m-1) ENDIF
 END countable_cardinality

                  finite cardinality

% finite_cardinality provides the fincard function, which gives the
% cardinality of a finite set whose base type is known to be finite.
% The f parameter gives an injective mapping from the naturals to the base
% type of the sets, and the m parameter gives an upper bound on the
% cardinality.  This form of cardinality is useful when the base type is
% finite, as it is then known that every set defined on that type is
% also finite.
finite_cardinality[T: TYPE, m: nat, f: (bijective?[below[m], T])] : THEORY
 BEGIN
  fincardi(s: set[T], i: below[m]) : RECURSIVE nat =
    (IF i = 0 THEN IF s(f(i)) THEN 1 ELSE 0 ENDIF
              ELSIF s(f(i)) THEN fincardi(s, i-1) + 1
              ELSE fincardi(s, i-1) ENDIF)
    MEASURE (LAMBDA (s: set[T]), (i: below[m]): i)
  fincard(s: set[T]) : nat = IF m = 0 THEN 0 ELSE fincardi(s, m-1) ENDIF
 END finite_cardinality

                   number axioms
% number_axioms provides the usual commutativity, associativity, etc.
% axioms about the real numbers.  Note that many of these properties
% also hold for the rationals, integers, and natural numbers.  These
% properties are all known to the decision procedures of PVS, so should
% rarely need to be cited.
number_axioms : THEORY
BEGIN
% Field Axioms
commutative_add: POSTULATE FORALL (x,y:real): x + y = y + x
associative_add: POSTULATE FORALL (x,y,z:real):
      (x + y) + z = x + (y + z)
identity_add: POSTULATE FORALL (x:real): x + 0 = x
inverse_add: POSTULATE FORALL (x:real): x + -x = 0
minus_add : POSTULATE  FORALL (x, y:real): x - y = x + -y
commutative_mult: POSTULATE FORALL (x,y:real): x * y = y * x

pvsprelude 37

             number axioms (continued)
associative_mult: POSTULATE FORALL (x,y,z:real):
      (x * y) * z = x * (y * z)
unique_identities: POSTULATE 0 /= 1
identity_mult: POSTULATE FORALL (x:real): x * 1 = x
inverse_mult: POSTULATE FORALL (x:nonzero_real): x * (1/x) = 1
distributive: POSTULATE FORALL (x,y,z:real):
  x * (y + z) = (x * y) + (x * z)
% Order Axioms
posreal?(x : real) : bool = x > 0
posreal : TYPE = {x:real | x > 0} CONTAINING 1
posreal_add_closed: POSTULATE FORALL (x,y: posreal): x + y > 0
posreal_mult_closed: AXIOM FORALL (x,y: posreal): x * y > 0
posreal_neg: POSTULATE FORALL (x: posreal): NOT posreal?(-x)

pvsprelude 38

             number axioms (continued)

trichotomy: POSTULATE FORALL (x: real):
  x > 0 OR x = 0 OR 0 > x
% Completeness Axiom
upper_bound?(ub: real, S: (nonempty?[real])): bool =
  (FORALL (x: real): member(x,S) => x <= ub)
least_upper_bound?(lub: real, S: (nonempty?[real])): bool =
  upper_bound?(lub,S) &
    FORALL (x: real): upper_bound?(x, S) => lub <= x
real_complete: AXIOM FORALL (S: (nonempty?[real])):
  (EXISTS (y : real) : upper_bound?(y, S)) =>
  (EXISTS (x:real): least_upper_bound?(x,S))
END number_axioms

                   number props

% number_props contains useful properties about real numbers.  In
% general these are known to the decision procedures of PVS, but they
% may occasionally be necessary.
number_props : THEORY
BEGIN
strict_lt : LEMMA strict_total_order?(<)
div_prop1: LEMMA FORALL (x,y:real),(z:nonzero_real):
      x * (y/z) = (x * y)/z
div_cancel1: LEMMA FORALL (x:real),(y:nonzero_real):
      y * (x/y) = x
div_cancel2: LEMMA FORALL (x:real),(y:nonzero_real):
      (x/y) * y = x
cancel : LEMMA
  FORALL (x,y, z:real) :
     x = y => (z * x = z * y)

              number props (continued)

both_sides : LEMMA
  FORALL (x,y:real),(z:nonzero_real):
    (z * x = z * y) => x = y
cross_mult : LEMMA
   FORALL (x,y:real),(u, v:nonzero_real):
     (x/u) = (y/v) = (x * v = y * u)
add_div : LEMMA
   FORALL (x,y:real),(u, v:nonzero_real):
     (x/u) + (y/v) = (x * v + y * u)/(u * v)
minus_div : LEMMA
   FORALL (x,y:real),(u, v:nonzero_real):
     (x/u) - (y/v) = (x * v - y * u)/(u * v)

              number props (continued)

div_distributes : LEMMA
    FORALL (x,y:real),(z:nonzero_real):
       (x + y)/z = (x/z) + (y/z)
div_distributes_minus : LEMMA
    FORALL (x,y:real),(z:nonzero_real):
       (x - y)/z = (x/z) - (y/z)
div_div : LEMMA
    FORALL (x: real),(y, z:nonzero_real):
      (x / (y / z)) = ((x * z) / y)
div_div2 : LEMMA
    FORALL (x: real),(y, z:nonzero_real):
      ((x / y) / z) = (x / (y * z))
END number_props

                      ordstruct

% ordstruct provides the building blocks for defining the constructive
% ordinals.
ordstruct: DATATYPE
 BEGIN
  zero: zero?
  add(coef: posnat, exp: ordstruct, rest: ordstruct): nonzero?
 END ordstruct

                     ordinals
% ordinals uses the ordstruct datatype to define the constructive
% ordinals, by providing an ordering on ordstruct and defining the
% ordinals to be those elements of type ordstruct that are in a
% canonical form with respect to the ordering.
ordinals: THEORY
BEGIN
i, j, k: VAR posnat
m,n, o: VAR nat
x, y, z: VAR ordstruct
size: [ordstruct->nat] = ordstruct_rec[nat](0, (LAMBDA i, m, n: 1 + m+n))
r, s, t, u, v, w: VAR ordstruct
<: RECURSIVE [ordstruct, ordstruct -> bool] =
  (LAMBDA x, y:
    (CASES x OF
      zero: NOT zero?(y),
      add(i, u, v): CASES y OF
                   zero: FALSE,
                   add(j, z, w): (u<z) OR
                                 (u=z) AND (i<j) OR
                                 (u=z) AND (i=j) AND (v<w)
                ENDCASES
   ENDCASES))
MEASURE (LAMBDA x, y: size(x));

ordinals (continued)

>(u,v): bool = v < u;
<=(u,v): bool = u < v OR u = v;
>=(u,v): bool = v < u OR v = u;
ordinal?: RECURSIVE pred[ordstruct] =
 (LAMBDA x:
   CASES x OF
    zero: TRUE,
    add(i, u, v): (ordinal?(u) AND ordinal?(v) AND
                    CASES v OF
                      zero: TRUE,
                      add(k,r,s): r < u
                    ENDCASES)
   ENDCASES)
 MEASURE size
ordinal: TYPE = (ordinal?)

ordinals (continued)

irreflexive: LEMMA (FORALL (x:(ordinal?)): NOT x < x)
antisym: LEMMA (FORALL (x,y:(ordinal?)): x < y IMPLIES NOT y < x)
antisymmetric: LEMMA
   (FORALL (x, y: (ordinal?)): x <= y AND y <= x IMPLIES x = y)
transitive: LEMMA
   (FORALL (x,y,z:(ordinal?)): x < y AND y < z IMPLIES x < z)
ordinal_induction: AXIOM
   (FORALL (p: pred[ordinal]):
     (FORALL (x:ordinal): (FORALL (y:ordinal): y < x IMPLIES p(y))
                             IMPLIES p(x))
       IMPLIES (FORALL (x:ordinal): p(x)))
well_founded_le : LEMMA
  well_founded?(LAMBDA (x, y: (ordinal?)) : x <= y)
END ordinals

                        lists

% list provides the datatype definition for lists.
list[t:TYPE] : DATATYPE
 BEGIN
  null: null?
  cons (car: t, cdr :list) :cons?
 END list

                   list props

% list_props provides the length function and the function every, which
% tests a predicate against every element of a list.
list_props[t:TYPE] : THEORY
BEGIN
length(l:list[t]): RECURSIVE nat =
CASES l OF
  null: 0,
  cons(x,y): length(y) + 1
ENDCASES
MEASURE list_nat_rec(0, (LAMBDA (x: t), (n: nat): n + 1))
every(p: pred[t], l: list[t]): RECURSIVE bool =
CASES l OF
  null: true,
  cons(x, y): p(x) & every(p, y)
ENDCASES
MEASURE (LAMBDA (p: pred[t]), (l: list[t]): length(l))
END list_props

                        lists

% lists defines the map function, which maps a function over a list,
% returning a list.
lists[t1,t2:TYPE] : THEORY
 BEGIN
  map(f: [t1 -> t2], l: list[t1]): RECURSIVE list[t2] =
    CASES l OF
      null: null,
      cons(x,y): cons(f(x), map(f, cdr(l)))
    ENDCASES
    MEASURE (LAMBDA (f: [t1 -> t2]), (l: list[t1]): length(l))
 END lists

                      map props

% map_props gives the commutativity properties of composition and map,
% for both sequences and lists.
map_props[t1,t2,t3: TYPE] : THEORY
 BEGIN
  map_prop1: LEMMA
    (FORALL (f: [t1 -> t2]),(g: [t2 -> t3]),(s: sequence[t1]):
      map(g, map(f, s)) = map(g o f, s))
  map_prop2: LEMMA
    (FORALL (f: [t1 -> t2]),(g: [t2 -> t3]),(s: list[t1]):
      map(g, map(f, s)) = map(g o f, s))
 END map_props

                       filters

% filters defines filter functions for sets and lists, which take a set
% (list) and a predicate and return the set (list) of those elements
% that satisfy the predicate.
filters[t: TYPE] : THEORY
 BEGIN
  filter(s: set[t], p: pred[t]): set[t] =
    {x: t | s(x) & p(x)}
  filter(l: list[t], p: pred[t]): RECURSIVE list[t] =
    CASES l OF
      null: null,
      cons(x, y): IF p(x) THEN cons(x, filter(y, p)) ELSE filter(y, p) ENDIF
    ENDCASES
    MEASURE (LAMBDA (l: list[t]), (p: pred[t]): length(l))
 END filters

                     card set

% card_set provides a small set of standard lemmas
% regarding finite cardinality, filters, and sets.
card_set[T: TYPE, n:posnat, f:(bijective?[below[n],T])] : THEORY
BEGIN
IMPORTING finite_cardinality[T,n,f],
          filters[below[n]]
fullset_fincard: LEMMA fincard(fullset[T]) = n
fincard_non_empty: LEMMA
  (FORALL (m:setof[T]):
    (EXISTS (z:T): m(z)) IFF fincard(m) /= 0)
fincard_filter: LEMMA
  (FORALL (m1,m2:setof[T]):
    fincard(filter(m1,m2)) <= fincard(m1))
zero_fincard: LEMMA
  (FORALL (y:T),(m1,m2:setof[T]):
     m1(y) AND fincard(filter(m1,m2)) <= 0 IMPLIES NOT m2(y))

card set (continued)

remove_prop: LEMMA
(FORALL (y,z:T),(m:setof[T]):
m(z) AND (NOT y=z) IMPLIES remove(y, m)(z))
fincard_remove: LEMMA
(FORALL (z:T),(m:setof[T]):
IF m(z)
THEN fincard(remove(z, m)) = fincard(m) - 1
ELSE fincard(remove(z, m)) = fincard(m)
ENDIF)
remove_comm: LEMMA
(FORALL (z:T),(m1,m2:setof[T]):
filter(remove(z, m1),m2) = remove(z, filter(m1,m2)))
END card_set