```% The PVS prelude.

% The prelude consists of theories that are built in to the PVS system.
% It is typechecked the same as any other PVS theory, but there are hooks
% in the typechecker that require most of these theories to be available,
% hence the order of the theories is important.  For example, no formulas
% may be declared before the booleans are available, as the formula is
% expected to have type bool.  Since definitions implicitly involve both
% formulas and equality, the booleans theory may not include any
% definitions.  Formulas are given below as AXIOMs, POSTULATEs, and LEMMAs.
% POSTULATEs are formulas that can be proved using the decision procedures,
% but would have to be given as axioms in a pure development of the theory.
% AXIOMs are formulas that cannot be proved, and LEMMAS are formulas that
% have been proved.

% booleans declares the type boolean and its abbreviation bool, along
% with the boolean constants true and false and the boolean connectives.
% The properties of the connectives are given later, but the connectives
% are built in to the typechecker so must be provided early on.
% Note: the boolean type could be defined as the enumeration type {false,
% true}, but booleans are primitive; the correct handling of enumeration
% types requires the boolean type.

booleans: THEORY
BEGIN

boolean: NONEMPTY_TYPE
bool: NONEMPTY_TYPE = boolean
FALSE, TRUE: bool
NOT: [bool -> bool]
AND, &, OR, IMPLIES, =>, WHEN, IFF, <=>: [bool, bool -> bool]

END booleans

% equalities contains the declaration for =.  It has a single type
% parameter.  Properties of equality are given in equality_props.

equalities [T: TYPE]: THEORY
BEGIN

=: [T, T -> boolean]

END equalities

notequal[T: TYPE]: THEORY
BEGIN
x, y: VAR T

/=(x, y): boolean = NOT (x = y)
END notequal

% if_def provides the polymorphic declaration of the IF-THEN-ELSE
% connective.  Note that the declaration for IF is for a 3-ary function,
% and that the IF-THEN-ELSE form is simply an alternative.

if_def [T: TYPE]: THEORY
BEGIN

IF:[boolean, T, T -> T]

END if_def

% boolean_props provides lemmas about the boolean constants and
% connectives.  The lemmas define them in terms of IF-THEN-ELSE, though
% these lemmas should never be needed since the prover "knows" the
% connectives as primitives.  WHEN is a special case - it is translated to
% IMPLIES with the arguments reversed by the typechecker.

boolean_props: THEORY
BEGIN
A, B: VAR bool

bool_exclusive: POSTULATE not (false = true)
bool_inclusive: POSTULATE A = false or A = true

not_def:       POSTULATE (not A) = IF A THEN false ELSE true ENDIF
and_def:       POSTULATE (A and B) = IF A THEN B ELSE false ENDIF
syand_def:     POSTULATE & = and
or_def:        POSTULATE (A or B) = IF A THEN true ELSE B ENDIF
implies_def:   POSTULATE (A implies B) = IF A THEN B ELSE true ENDIF
syimplies_def: POSTULATE => = implies
when_def:      POSTULATE (A when B) = (B implies A)
iff_def:       POSTULATE (A iff B) = ((A and B) or (not A and not B))
syiff_def:     POSTULATE <=> = iff

excluded_middle: LEMMA A OR NOT A

END boolean_props

% xor_def provides the definition for XOR.  Note that this is not built in
% to the prover, so this definition will need to be expanded in order to use
% it.

xor_def: THEORY
BEGIN
A, B: VAR bool
XOR(A, B): bool = (A /= B)

xor_def: LEMMA (A xor B) = IF A THEN NOT B ELSE B ENDIF
END xor_def

% quantifier_props defines some useful properties of quantifiers.  Note
% that these work well with the higher-order matching facility of the prover.

quantifier_props [t: TYPE]: THEORY
BEGIN
x: VAR t
p, q: VAR [t -> bool]

not_exists: LEMMA (EXISTS x: p(x)) = NOT (FORALL x: NOT p(x))

exists_not: LEMMA (EXISTS x: NOT p(x)) = NOT (FORALL x: p(x))

exists_or: LEMMA
(EXISTS x: p(x) OR q(x)) = ((EXISTS x: p(x)) OR (EXISTS x: q(x)))

exists_implies: LEMMA
(EXISTS x: p(x) IMPLIES q(x)) = ((EXISTS x: NOT p(x)) OR (EXISTS x: q(x)))

exists_and: LEMMA
(EXISTS x: p(x) AND q(x)) IMPLIES ((EXISTS x: p(x)) AND (EXISTS x: q(x)))

not_forall: LEMMA (FORALL x: p(x)) = NOT (EXISTS x: NOT p(x))

forall_not: LEMMA (FORALL x: NOT p(x)) = NOT (EXISTS x: p(x))

forall_and: LEMMA
(FORALL x: p(x) AND q(x)) = ((FORALL x: p(x)) AND (FORALL x: q(x)))

forall_or: LEMMA
((FORALL x: p(x)) OR (FORALL x: q(x))) IMPLIES (FORALL x: p(x) OR q(x))

END quantifier_props

% 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

% exists1 provides a unique existence function; it takes a predicate
% and asserts that there is one and only one element of the type that
% satisfies the predicate.  The expression "exists1! (x:t): p(x)" is
% translated to "exists1(LAMBDA (x:t): p(x))".

exists1 [T: TYPE]: THEORY
BEGIN
x, y: VAR T
p, q: VAR pred[T]

unique?(p): bool = FORALL x, y: p(x) AND p(y) IMPLIES x = y

exists1(p): bool = (EXISTS x: p(x)) AND unique?(p)

unique_lem: LEMMA
(FORALL x: p(x) IMPLIES q(x)) IMPLIES (unique?(q) IMPLIES unique?(p))

exists1_lem: LEMMA (exists1! x: p(x)) IMPLIES (EXISTS x: p(x))

END exists1

% equality_props provides the declaration for /= and some properties of
% =.

equality_props[T: TYPE]: THEORY
BEGIN

x, y, z: VAR T
b: VAR bool

IF_true: POSTULATE IF true THEN x ELSE y ENDIF = x

IF_false: POSTULATE IF false THEN x ELSE y ENDIF = y

IF_same: LEMMA IF b THEN x ELSE x ENDIF = x

reflexivity_of_equals: POSTULATE x = x

transitivity_of_equals: POSTULATE x = y AND y = z IMPLIES x = z

symmetry_of_equals: POSTULATE x = y IMPLIES y = x

END equality_props

% if_props

if_props [s, t: TYPE]: THEORY
BEGIN
a, b, c: VAR bool
x, y: VAR s
f: VAR [s -> t]

lift_if1: LEMMA
f(IF a THEN x ELSE y ENDIF) = IF a THEN f(x) ELSE f(y) ENDIF

lift_if2: LEMMA
IF (IF a THEN b ELSE c ENDIF) THEN x ELSE y ENDIF
= IF a THEN (IF b THEN x ELSE y ENDIF)
ELSE (IF c THEN x ELSE y ENDIF) ENDIF

END if_props

% 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.  However, this doesn't handle
% dependent function types, since the domain and range can't be separated.

functions [D, R: TYPE]: THEORY
BEGIN
f, g: VAR [D -> R]
x, x1, x2: VAR D
y: VAR R
Drel: VAR PRED[[D, D]]
Rrel: VAR PRED[[R, R]]

extensionality: POSTULATE
(FORALL (x: D): f(x) = g(x)) IMPLIES f = g

congruence: LEMMA f = g AND x1 = x2 IMPLIES f(x1) = g(x2)

eta: LEMMA (LAMBDA (x: D): f(x)) = f

injective?(f): bool = (FORALL x1, x2: (f(x1) = f(x2) => (x1 = x2)))

surjective?(f): bool = (FORALL y: (EXISTS x: f(x) = y))

bijective?(f): bool = injective?(f) & surjective?(f)

domain(f): TYPE = D

range(f): TYPE = R

graph(f)(x, y): bool = (f(x) = y)

preserves(f, Drel, Rrel): bool =
FORALL x1, x2: Drel(x1, x2) IMPLIES Rrel(f(x1), f(x2))

inverts(f, Drel, Rrel): bool =
FORALL x1, x2: Drel(x1, x2) IMPLIES Rrel(f(x2), f(x1))

END functions

% restrict is the restriction operator on functions, allowing a
% function defined on a supertype to be applied to a subtype.  Note
% that it is a conversion, so will be inserted automatically when needed.

restrict [T: TYPE, S: TYPE FROM T, R: TYPE]: THEORY
BEGIN

f: VAR [T -> R]
s: VAR S

restrict(f)(s): R = f(s)
CONVERSION restrict

injective_restrict: LEMMA
injective?(f) IMPLIES injective?(restrict(f))

END restrict

% extend is the inverse of restrict.  The difference is that a default
% value must be provided, which keeps it from being a conversion, in
% general (but see extend_bool).

extend [T: TYPE, S: TYPE FROM T, R: TYPE, d: R]: THEORY
BEGIN

f: VAR [S -> R]
t: VAR T

extend(f)(t): R = IF S_pred(t) THEN f(t) ELSE d ENDIF

restrict_extend: LEMMA restrict[T,S,R](extend(f)) = f

END extend

% extend_bool provides a conversion for boolean valued extensions,
% providing the default value of false.  Thus a set of nats "is" a set
% of ints.

extend_bool [T: TYPE, S: TYPE FROM T]: THEORY
BEGIN

CONVERSION extend[T, S, bool, false]

END extend_bool

% identity simply defines the identity function.  The identity is used for
% conversion expressions.  For example, "foo: T" is translated to
% "(LAMBDA (x:T): x)(foo)"

identity [T: TYPE]: THEORY
BEGIN
x: VAR T
I: (bijective?[T, T]) = (LAMBDA x: x)
id: (bijective?[T, T]) = (LAMBDA x: x)
identity: (bijective?[T, T]) = (LAMBDA x: x)
END identity

% relations defines properties that are useful in specifying binary
% relations.

relations [T: TYPE]: THEORY
BEGIN

R: VAR PRED[[T, T]]
x, y, z: VAR T

eq: pred[[T, T]] = (LAMBDA x, y: x = y)

reflexive?(R): bool = FORALL x: R(x, x)

irreflexive?(R): bool = FORALL x: NOT R(x, x)

symmetric?(R): bool = FORALL x, y: R(x, y) IMPLIES R(y, x)

antisymmetric?(R): bool = FORALL x, y: R(x, y) & R(y, x) => x = y

connected?(R): bool = FORALL x, y: x /= y IMPLIES R(x, y) OR R(y, x)

transitive?(R): bool = FORALL x, y, z: R(x, y) & R(y, z) => R(x, z)

equivalence?(R): bool = reflexive?(R) AND symmetric?(R) AND transitive?(R)

END relations

% orders defines the usual ordering relations.  Be careful not to read too
% much into these definitions; < and <= are variables ranging over binary
% relations, not actual orders.  Their use below is suggestive of the
% defining properties.

orders [T: TYPE]: THEORY
BEGIN
x, y: VAR T
<=, < : VAR pred[[T, T]]
p: VAR pred[T]

preorder?(<=): bool = reflexive?(<=) & transitive?(<=)

partial_order?(<=): bool = preorder?(<=) & antisymmetric?(<=)

strict_order?(<): bool = irreflexive?(<) & transitive?(<)

dichotomous?(<=): bool = (FORALL x, y: (x <= y OR y <= x))

total_order?(<=): bool = partial_order?(<=) & dichotomous?(<=)

linear_order?(<=): bool = total_order?(<=)

trichotomous?(<): bool = (FORALL x, y: x < y OR y < x OR x = y)

strict_total_order?(<): bool = strict_order?(<) & trichotomous?(<)

well_founded?(<): bool =
(FORALL p:
(EXISTS y: p(y))
IMPLIES (EXISTS (y:(p)): (FORALL (x:(p)): (NOT x < y))))

pe: VAR {p: pred[T] | EXISTS (x: T): p(x)}

upper_bound?(<)(x, pe): bool = FORALL (y: (pe)): y < x

lower_bound?(<)(x, pe): bool = FORALL (y: (pe)): x < y

least_upper_bound?(<)(x, pe): bool =
upper_bound?(<)(x, pe) AND
FORALL y: upper_bound?(<)(y, pe) IMPLIES (x < y OR x = y)

greatest_lower_bound?(<)(x, pe): bool =
lower_bound?(<)(x, pe) AND
FORALL y: lower_bound?(<)(y, pe) IMPLIES (y < x OR x = y)

END orders

% wf_induction defines induction for any type that has a well-founded
% relation.

wf_induction [T: TYPE, <: (well_founded?[T])]: THEORY
BEGIN

wf_induction: LEMMA
(FORALL (p: pred[T]):
(FORALL (x: T):
(FORALL (y: T): y M], <: (well_founded?[M])]: THEORY
BEGIN

measure_induction: LEMMA
(FORALL (p: pred[T]):
(FORALL (x: T):
(FORALL (y: T): m(y) < m(x) IMPLIES  p(y))
IMPLIES p(x))
IMPLIES (FORALL (x: T): p(x)))

END measure_induction

% epsilons provides a "choice" function that does not have a nonemptiness
% requirement.  Given a predicate over the type t, epsilon produces an
% element of satisfying that predicate if one exists, and otherwise
% produces an arbitrary element of that type.
% "epsilon! (x:t): p(x)" is translated to "epsilon(LAMBDA (x:t): p(x))".
% Note that the type parameter is given as nonempty, whihc means that
% there is an nonempty ASSUMPTION automatically generated for this theory.

epsilons [T: NONEMPTY_TYPE]: THEORY
BEGIN
p: VAR pred[T]
x: VAR T

epsilon(p): T

epsilon_ax: AXIOM (EXISTS x: p(x)) => p(epsilon(p))

END epsilons

% sets provides the polymorphic set type, along with the usual set
% operations.  It is important to bear in mind that a set is just
% a predicate.

sets [T: TYPE]: THEORY
BEGIN

set: TYPE = setof[T]

x, y: VAR T

a, b, c: VAR set

p: VAR PRED[T]

member(x, a): bool = a(x)

empty?(a): bool = (FORALL x: NOT member(x, a))

emptyset: set = {x | false}

nonempty?(a): bool = NOT empty?(a)

fullset: set = {x | true}

subset?(a, b): bool = (FORALL x: member(x, a) => member(x, b))

strict_subset?(a, b): bool = subset?(a, b) & a /= b

union(a, b): set = {x | member(x, a) OR member(x, b)}

intersection(a, b): set = {x | member(x, a) AND member(x, b)}

disjoint?(a, b): bool = empty?(intersection(a, b))

complement(a): set = {x | NOT member(x, a)}

difference(a, b): set = {x | member(x, a) AND NOT member(x, b)}

symmetric_difference(a, b): set =
union(difference(a, b), difference(b, a))

every(p)(a): bool = FORALL (x:(a)): p(x)

every(p, a): bool = FORALL (x:(a)): p(x)

some(p)(a): bool = EXISTS (x:(a)): p(x)

some(p, a): bool = EXISTS (x:(a)): p(x)

singleton(x): set = {y | y = x}

add(x, a): set = {y | x = y OR member(y, a)}

remove(x, a): set = {y | x /= y AND member(y, a)}

% A choice function for nonempty sets
choose(p: (nonempty?)): (p) = epsilon(p)

rest(a): set = IF empty?(a) THEN a ELSE remove(choose(a), a) ENDIF

END sets

sets_lemmas [T: TYPE]: THEORY
BEGIN

a, b, c: VAR set[T]
x: VAR T

extensionality: LEMMA
(FORALL x: member(x, a) IFF member(x, b)) IMPLIES (a = b)

emptyset_is_empty?: LEMMA  empty?(a) IFF a = emptyset

empty_no_members: LEMMA NOT member(x, emptyset)

nonempty_member: LEMMA nonempty?(a) IFF EXISTS x: member(x, a)

fullset_member: LEMMA member(x, fullset)

nonempty_exists: LEMMA nonempty?(a) IFF EXISTS (x: (a)): TRUE

subset_reflexive: LEMMA subset?(a, a)

subset_antisymmetric: LEMMA subset?(a, b) AND subset?(b, a) IMPLIES a = b

subset_transitive: LEMMA
subset?(a, b) AND subset?(b, c) IMPLIES subset?(a, c)

subset_partial_order: LEMMA partial_order?(subset?[T])

subset_emptyset: LEMMA subset?(emptyset, a)

subset_fullset: LEMMA subset?(a, fullset)

union_idempotent: LEMMA union(a, a) = a

union_commutative: LEMMA union(a, b) = union(b, a)

union_associative: LEMMA union(union(a, b), c) = union(a, union(b, c))

union_empty: LEMMA union(a, emptyset) = a

union_full: LEMMA union(a, fullset) = fullset

union_subset1: LEMMA subset?(a, union(a, b))

union_subset2: LEMMA subset?(a, b) IMPLIES union(a, b) = b

intersection_idempotent: LEMMA intersection(a, a) = a

intersection_commutative: LEMMA intersection(a, b) = intersection(b, a)

intersection_associative: LEMMA
intersection(intersection(a, b), c) = intersection(a, intersection(b, c))

intersection_empty: LEMMA intersection(a, emptyset) = emptyset

intersection_full: LEMMA intersection(a, fullset) = a

intersection_subset1: LEMMA subset?(intersection(a, b), a)

intersection_subset2: LEMMA subset?(a, b) IMPLIES intersection(a, b) = a

distribute_intersection_union: LEMMA
intersection(a, union(b, c))
= union(intersection(a, b), intersection(a, c))

distribute_union_intersection: LEMMA
union(a, intersection(b, c)) = intersection(union(a, b), union(a, c))

complement_emptyset: LEMMA complement(emptyset[T]) = fullset

complement_fullset: LEMMA complement(fullset[T]) = emptyset

complement_complement: LEMMA complement(complement(a)) = a

subset_complement: LEMMA
subset?(complement(a), complement(b)) IFF subset?(b, a)

demorgan1: LEMMA
complement(union(a, b)) = intersection(complement(a), complement(b))

demorgan2: LEMMA
complement(intersection(a, b)) = union(complement(a), complement(b))

difference_emptyset1: LEMMA difference(a, emptyset) = a

difference_emptyset2: LEMMA difference(emptyset, a) = emptyset

difference_fullset1: LEMMA difference(a, fullset) = emptyset

difference_fullset2: LEMMA difference(fullset, a) = complement(a)

difference_intersection: LEMMA
difference(a, b) = intersection(a, complement(b))

difference_difference1: LEMMA
difference(difference(a, b), c) = difference(a, union(b, c))

difference_difference2: LEMMA
difference(a, difference(b, c))
= union(difference(a, b), intersection(a, c))

member_remove: LEMMA NOT member(x, a) IMPLIES remove(x, a) = a

choose_rest: LEMMA NOT empty?(a) IMPLIES add(choose(a), rest(a)) = a

choose_member: LEMMA NOT empty?(a) IMPLIES member(choose(a), a)

choose_not_member: LEMMA
NOT empty?(a) IMPLIES NOT member(choose(a), rest(a))

rest_not_equal: LEMMA NOT empty?(a) IMPLIES rest(a) /= a

rest_member: LEMMA member(x,rest(a)) IMPLIES member(x,a)

choose_rest_or: LEMMA
member(x,a) IMPLIES member(x,rest(a)) OR x = choose(a)

choose_singleton: LEMMA choose(singleton(x)) = x

rest_singleton: LEMMA rest(singleton(x)) = emptyset[T]

rest_empty_lem: LEMMA NOT empty?(a) AND empty?(rest(a))
IMPLIES a = singleton(choose(a))

END sets_lemmas

% function_inverse.  In practice this definition will only be useful
% for injective functions.  This is not defined in functions because the
% epsilon! operator forces the domain type to be nonempty.  Note
% that this theory may not be instantiated through dependent function
% types.

function_inverse[D: NONEMPTY_TYPE, R: TYPE]: THEORY
BEGIN
x: VAR D
y: VAR R
f: VAR [D -> R]
g: VAR [R -> D]

inverse(f)(y): D = (epsilon! x: f(x) = y)

surjective_inverse: LEMMA
(FORALL (f:(surjective?[D, R])):
inverse(f)(y) = x IMPLIES y = f(x))

injective_inverse: LEMMA
(FORALL (f:(injective?[D, R])):
y = f(x) IMPLIES inverse(f)(y) = x)

bijective_inverse: LEMMA
(FORALL (f:(bijective?[D, R])):
inverse(f)(y) = x IFF y = f(x))

bij_inv_is_bij: LEMMA
bijective?(f) IMPLIES bijective?(inverse(f))

left_inverse?(g, f): bool = (FORALL x: g(f(x)) = x)

right_inverse?(g, f): bool = (FORALL y: f(g(y)) = y)

surj_right: LEMMA surjective?(f) IFF right_inverse?(inverse(f), f)

inj_left: LEMMA injective?(f) IFF left_inverse?(inverse(f), f)

inj_inv: LEMMA surjective?(f) IMPLIES injective?(inverse(f))

surj_inv: LEMMA injective?(f) IMPLIES surjective?(inverse(f))

END function_inverse

% 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, and returns a set.

function_image [D, R: TYPE]: THEORY
BEGIN
f: VAR [D -> R]
X, X1, X2: VAR set[D]
Y, Y1, Y2: VAR set[R]

image(f, X): set[R] = {y: R | (EXISTS (x:(X)): y = f(x))}

inverse_image(f, Y): set[D] = {x: D | member(f(x), Y)}

image_inverse_image: LEMMA
subset?(image(f, inverse_image(f, Y)), Y)

inverse_image_image: LEMMA
subset?(X, inverse_image(f, image(f, X)))

image_subset: LEMMA
subset?(X1, X2) IMPLIES subset?(image(f, X1), image(f, X2))

inverse_image_subset: LEMMA
subset?(Y1, Y2) IMPLIES subset?(inverse_image(f, Y1), inverse_image(f, Y2))

image_union: LEMMA
image(f, union(X1, X2)) = union(image(f, X1), image(f, X2))

image_intersection: LEMMA
subset?(image(f, intersection(X1, X2)),
intersection(image(f, X1), image(f, X2)))

inverse_image_union: LEMMA
inverse_image(f, union(Y1, Y2))
= union(inverse_image(f, Y1), inverse_image(f, Y2))

inverse_image_intersection: LEMMA
inverse_image(f, intersection(Y1, Y2))
= intersection(inverse_image(f, Y1), inverse_image(f, Y2))

inverse_image_complement: LEMMA
inverse_image(f, complement(Y)) = complement(inverse_image(f, Y))

END function_image

% functions_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
x: VAR T1
f1: VAR [T1 -> T2]
f2: VAR [T2 -> T3]
X: VAR set[T1]
T1rel: VAR PRED[[T1, T1]]
T2rel: VAR PRED[[T2, T2]]
T3rel: VAR PRED[[T3, T3]]

o(f2, f1)(x): T3 = f2(f1(x))

image_composition: LEMMA
image(f2, image(f1, X)) = image(f2 o f1, X)

preserves_composition: LEMMA
preserves(f1, T1rel, T2rel) AND preserves(f2, T2rel, T3rel)
IMPLIES preserves(f2 o f1, T1rel, T3rel)

inverts_composition1: LEMMA
preserves(f1, T1rel, T2rel) AND inverts(f2, T2rel, T3rel)
IMPLIES inverts(f2 o f1, T1rel, T3rel)

inverts_composition2: LEMMA
inverts(f1, T1rel, T2rel) AND preserves(f2, T2rel, T3rel)
IMPLIES inverts(f2 o f1, T1rel, T3rel)

END function_props

% 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
f1: VAR [T1 -> T2]
f2: VAR [T2 -> T3]
f3: VAR [T3 -> T4]

assoc: LEMMA (f3 o f2) o f1 = f3 o (f2 o f1)
END function_props2

% relation_defs defines operators on relations between possibly different
% types.  Note that some of the names are overloaded with those given in
% functions - in practice this should not cause any problems.

relation_defs [T1, T2: TYPE]: THEORY
BEGIN
R: VAR pred[[T1, T2]]
X: VAR set[T1]

image(R, X): set[T2] = {y: T2 | (EXISTS (x: (X)): R(x, y))}

converse(R): pred[[T2, T1]] = (LAMBDA (y: T2), (x: T1): R(x, y))

isomorphism?(R): bool =
(EXISTS (f: (bijective?[T1, T2])): R = graph(f))

domain(R): TYPE = T1

range(R): TYPE = T2

END relation_defs

% relational_composition

relational_composition [T1, T2, T3: TYPE]: THEORY
BEGIN
R1: VAR pred[[T1, T2]]
R2: VAR pred[[T2, T3]]

o(R1, R2): pred[[T1, T3]] =
(LAMBDA (x: T1), (z: T3): (EXISTS (y: T2): R1(x, y) AND R2(y, z)))

END relational_composition

% operator_defs

operator_defs[T: TYPE]: THEORY
BEGIN
o, *: VAR [T, T -> T]
-: VAR [T -> T]
x, y, z: VAR T

commutative?(o):     bool = (FORALL x, y: x o y = y o x)

associative?(o):     bool = (FORALL x, y, z: (x o y) o z = x o (y o z))

left_identity?(o)(y): bool = (FORALL x: y o x = x)

right_identity?(o)(y): bool = (FORALL x: x o y = x)

identity?(o)(y):     bool = (FORALL x: x o y = x AND y o x = x)

has_identity?(o):    bool = (EXISTS y: identity?(o)(y))

zero?(o)(y):         bool = (FORALL x: x o y = y AND y o x = y)

has_zero?(o):        bool = (EXISTS y: zero?(o)(y))

inverses?(o)(-)(y):  bool = (FORALL x: x o -x = y AND -x o x = y)

has_inverses?(o):    bool = (EXISTS -, y: inverses?(o)(-)(y))

distributive?(*, o): bool = (FORALL x, y, z: x * (y o z) = (x * y) o (x * z))

END operator_defs

% numbers provides the number type, which is the highest numeric type.
% Though not explicitly specified, once the number type is declared all
% numeric constants are known to be of type number.  We include the
% postulate 0 /= 1 so that the nonzero subtypes declared later can be
% shown to be nonempty.

numbers: THEORY
BEGIN

number: NONEMPTY_TYPE

% Imagine the following declarations here
% 0, 1, 2, ... : number
% AXIOM 0 /= 1 AND 0 /= 2 AND 1 /= 2 AND ...

END numbers

% reals defines the real numbers as an uninterpreted subtype of
% number.  Note that / is defined only when the second argument is
% nonzero.  This theory should not generally be used in auto-rewrite,
% since the inequalities are already known to the decision procedures,
% and tend to get rewritten to disjunctions, which are slightly harder
% to work with.

reals: THEORY
BEGIN

real: NONEMPTY_TYPE FROM number

real?(n:number): bool = real_pred(n)

% The following declarations, if they could be expanded, are built in to
%  the typechecker and prover:
% AXIOM real_pred(0) AND real_pred(1) AND real_pred(2) AND ...
% JUDGEMENT 0, 1, 2, ... HAS_TYPE real

nonzero_real: NONEMPTY_TYPE = {r: real | r /= 0} CONTAINING 1
nzreal: NONEMPTY_TYPE = nonzero_real

x, y: VAR real

+, -, *: [real, real -> real]
/: [real, nzreal -> real]
-: [real -> real]

<(x, y):  bool
<=(x, y): bool = x < y OR x = y;
>(x, y):  bool = y < x;
>=(x, y): bool = y <= x

reals_totally_ordered: POSTULATE strict_total_order?(<)

% Built in:
% AXIOM 0 < 1 AND 1 < 2 AND ...

END reals

% real_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.

real_axioms: THEORY
BEGIN
x, y, z: VAR real
n0x: VAR nzreal

% Field Axioms

commutative_add: POSTULATE x + y = y + x

associative_add: POSTULATE x + (y + z) = (x + y) + z

identity_add: POSTULATE x + 0 = x

inverse_add: POSTULATE x + -x = 0

minus_add: POSTULATE x - y = x + -y

commutative_mult: POSTULATE x * y = y * x

associative_mult: POSTULATE x * (y * z) =  (x * y) * z

identity_mult: POSTULATE 1 * x = x

inverse_mult: POSTULATE n0x * (1/n0x) = 1

div_def: POSTULATE y/n0x = y * (1/n0x)

distributive: POSTULATE x * (y + z) = (x * y) + (x * z)

% Order Axioms

posreal_add_closed: POSTULATE x > 0 AND y > 0 IMPLIES x + y > 0

posreal_mult_closed: AXIOM x > 0 AND y > 0 IMPLIES x * y > 0

posreal_neg: POSTULATE x > 0 IMPLIES NOT -x > 0

trichotomy: POSTULATE x > 0 OR x = 0 OR 0 > x

% Completeness Axiom

real_complete: AXIOM
FORALL (S: (nonempty?[real])):
(EXISTS y: upper_bound?(<=)(y, S)) IMPLIES
(EXISTS y: least_upper_bound?(<=)(y, S))

END real_axioms

% reals_types declares some useful subtypes of the reals and some
% associated judgements.

real_types: THEORY
BEGIN
x: VAR real

nonneg_real: NONEMPTY_TYPE = {x: real        | x >= 0} CONTAINING 0
nonpos_real: NONEMPTY_TYPE = {x: real        | x <= 0} CONTAINING 0
posreal:     NONEMPTY_TYPE = {x: nonneg_real | x > 0}  CONTAINING 1
negreal:     NONEMPTY_TYPE = {x: nonpos_real | x < 0}  CONTAINING -1

JUDGEMENT posreal SUBTYPE_OF nzreal

nnx, nny: VAR nonneg_real
npx, npy: VAR nonpos_real
nx, ny: VAR negreal

nonneg_real_add_closed: LEMMA nnx + nny >= 0
nonpos_real_add_closed: LEMMA npx + npy <= 0
negreal_add_closed: LEMMA nx + ny < 0

nonneg_real_mult_closed: LEMMA nnx * nny >= 0

JUDGEMENT +, * HAS_TYPE [nonneg_real, nonneg_real -> nonneg_real]
JUDGEMENT / HAS_TYPE [nonneg_real, posreal -> nonneg_real]

JUDGEMENT *, / HAS_TYPE [nzreal, nzreal -> nzreal]
JUDGEMENT - HAS_TYPE [nzreal -> nzreal]

JUDGEMENT +, * HAS_TYPE [posreal, posreal -> posreal]
JUDGEMENT / HAS_TYPE [posreal, posreal -> posreal]

END real_types

% 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: NONEMPTY_TYPE FROM real
rat: NONEMPTY_TYPE = rational

rational?(n: number): bool = real_pred(n) AND rational_pred(n)

% The following declarations, if they could be expanded, are built in to
%  the typechecker:
% AXIOM rational_pred(0) AND rational_pred(1) AND rational_pred(2) AND ...
% JUDGEMENT 0, 1, 2, ... HAS_TYPE rational

nonzero_rational: NONEMPTY_TYPE = {r: rational | r /= 0} CONTAINING 1
nzrat: NONEMPTY_TYPE = nonzero_rational
JUDGEMENT nonzero_rational SUBTYPE_OF nonzero_real

x, y: VAR rat
n0z: VAR nzrat

closed_plus:    AXIOM rational_pred(x + y)
closed_minus:   AXIOM rational_pred(x - y)
closed_times:   AXIOM rational_pred(x * y)
closed_divides: AXIOM rational_pred(x / n0z)
closed_neg:     AXIOM rational_pred(-x)

JUDGEMENT +, -, * HAS_TYPE [rat, rat -> rat]
JUDGEMENT / HAS_TYPE [rat, nzrat -> rat]

JUDGEMENT - HAS_TYPE [rat -> rat]

nonneg_rat: NONEMPTY_TYPE = {r: rational   | r >= 0} CONTAINING 0
nonpos_rat: NONEMPTY_TYPE = {r: rational   | r <= 0} CONTAINING 0
posrat:     NONEMPTY_TYPE = {r: nonneg_rat | r > 0}  CONTAINING 1
negrat:     NONEMPTY_TYPE = {r: nonpos_rat | r < 0}  CONTAINING -1

JUDGEMENT nonneg_rat SUBTYPE_OF nonneg_real
JUDGEMENT posrat     SUBTYPE_OF posreal
JUDGEMENT posrat     SUBTYPE_OF nzrat

JUDGEMENT *, / HAS_TYPE [nzrat, nzrat -> nzrat]
JUDGEMENT - HAS_TYPE [nzrat -> nzrat]

JUDGEMENT +, * HAS_TYPE [nonneg_rat, nonneg_rat -> nonneg_rat]
JUDGEMENT / HAS_TYPE [nonneg_rat, posrat -> nonneg_rat]

JUDGEMENT +, * HAS_TYPE [posrat, posrat -> posrat]
JUDGEMENT / HAS_TYPE [posrat, posrat -> posrat]

END rationals

% 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: NONEMPTY_TYPE FROM rational
int: NONEMPTY_TYPE = integer

integer?(n:number): bool =
real_pred(n) AND rational_pred(n) AND integer_pred(n)

% The following declarations, if they could be expanded, are built in to
%  the typechecker:
% AXIOM integer_pred(0) AND integer_pred(1) AND integer_pred(2) AND ...
% JUDGEMENT 0, 1, 2, ... HAS_TYPE integer

nonzero_integer: NONEMPTY_TYPE = {i: int | i /= 0} CONTAINING 1
nzint: NONEMPTY_TYPE = nonzero_integer
JUDGEMENT nonzero_integer SUBTYPE_OF nonzero_rational

i, j: VAR int

closed_plus:  AXIOM integer_pred(i + j)
closed_minus: AXIOM integer_pred(i - j)
closed_times: AXIOM integer_pred(i * j)
closed_neg:   AXIOM integer_pred(-i)

JUDGEMENT +, -, * HAS_TYPE [int, int -> int]

JUDGEMENT - HAS_TYPE [int -> int]
JUDGEMENT - HAS_TYPE [nzint -> nzint]

upfrom(i): NONEMPTY_TYPE = {s: int | s >= i} CONTAINING i
above(i):  NONEMPTY_TYPE = {s: int | s > i} CONTAINING i + 1
nonneg_int: NONEMPTY_TYPE = {i: int        | i >= 0} CONTAINING 0
nonpos_int: NONEMPTY_TYPE = {i: int        | i <= 0} CONTAINING 0
posint:     NONEMPTY_TYPE = {i: nonneg_int | i > 0}  CONTAINING 1
negint:     NONEMPTY_TYPE = {i: nonpos_int | i < 0}  CONTAINING -1

posnat: NONEMPTY_TYPE = posint

% Built in:
% JUDGEMENT 1, 2, 3, ... HAS_TYPE posint

JUDGEMENT nonneg_int SUBTYPE_OF nonneg_rat
JUDGEMENT posint     SUBTYPE_OF posrat
JUDGEMENT posint     SUBTYPE_OF nzint

JUDGEMENT * HAS_TYPE [nzint, nzint -> nzint]
JUDGEMENT +, * HAS_TYPE [posint, posint -> posint]

subrange(i, j): TYPE = {k: int | i <= k AND k <= j}

even?(i): bool = EXISTS j: i = j * 2
odd?(i): bool  = EXISTS j: i = j * 2 + 1

even_int: NONEMPTY_TYPE = (even?) CONTAINING 0
odd_int:  NONEMPTY_TYPE = (odd?) CONTAINING 1

JUDGEMENT odd_int SUBTYPE_OF nzint

JUDGEMENT +, -, * HAS_TYPE [even_int, even_int -> even_int]
JUDGEMENT +, - HAS_TYPE [odd_int, odd_int -> even_int]
JUDGEMENT * HAS_TYPE [odd_int, odd_int -> odd_int]
JUDGEMENT - HAS_TYPE [even_int -> even_int]
JUDGEMENT - HAS_TYPE [odd_int -> odd_int]

% Note that there are no built-in judgements for 0, 1, 2, ...

END integers

% 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: NONEMPTY_TYPE = {i:integer | i >= 0} CONTAINING 0
nat: NONEMPTY_TYPE = naturalnumber

% The following declaration, if it could be expanded, is built in to
%  the typechecker:
% JUDGEMENT 0, 1, 2, ... HAS_TYPE naturalnumber

i, j, k: VAR nat

upto(i):   NONEMPTY_TYPE = {s: nat | s <= i} CONTAINING i
below(i):  TYPE = {s: nat | s < i}

JUDGEMENT +, * HAS_TYPE [nat, nat -> nat]

succ(i): nat = i + 1

pred(i): nat = IF i > 0 THEN i - 1 ELSE 0 ENDIF;

~(i, j): nat = IF i > j THEN i - j ELSE 0 ENDIF

wf_nat: AXIOM well_founded?(LAMBDA i, j: i < j)

p: VAR pred[nat]

nat_induction: LEMMA
(p(0) AND (FORALL j: p(j) IMPLIES p(j+1)))
IMPLIES (FORALL i: p(i))

% Strong induction on naturals.

NAT_induction: LEMMA
(FORALL j: (FORALL k: k < j IMPLIES p(k)) IMPLIES p(j))
IMPLIES (FORALL i: p(i))

END naturalnumbers

% real_defs defines some useful real functions and
% provides all the judgements for the subtypes nzreal, nonneg_real,
% posreal, rat, nzrat, nonneg_rat, posrat, int, nzint, nat, and posint.
% For abs, we don't declare all these possibilities, since abs is the
% identity on the nonneg and pos number types.  Note that for abs, max,
% and min the range type is dependent on the domain, providing information
% in the type that is usually provided through separate lemmas.

real_defs: THEORY
BEGIN
m, n: VAR real

abs(m): {n: nonneg_real | n >= m}
= IF m < 0 THEN -m ELSE m ENDIF

JUDGEMENT abs HAS_TYPE [x: nzreal -> {y: posreal | y >= x}]
JUDGEMENT abs HAS_TYPE [q: rat -> {r: nonneg_rat | r >= q}]
JUDGEMENT abs HAS_TYPE [q: nzrat -> {r: posrat | r >= q}]
JUDGEMENT abs HAS_TYPE [i: int -> {j: nonneg_int | j >= i}]
JUDGEMENT abs HAS_TYPE [i: nzint -> {j: posint | j >= i}]

max(m, n): {p: real | p >= m AND p >= n}
= IF m < n THEN n ELSE m ENDIF

min(m, n): {p: real | p <= m AND p <= n}
= IF m > n THEN n ELSE m ENDIF

% real subtype judgements

JUDGEMENT max HAS_TYPE
[x: nzreal, y: nzreal -> {z: nzreal | z >= x AND z >= y}]
JUDGEMENT min HAS_TYPE
[x: nzreal, y: nzreal -> {z: nzreal | z <= x AND z <= y}]

JUDGEMENT max HAS_TYPE
[x: nonneg_real, y: nonneg_real -> {z: nonneg_real | z >= x AND z >= y}]
JUDGEMENT min HAS_TYPE
[x: nonneg_real, y: nonneg_real -> {z: nonneg_real | z <= x AND z <= y}]

JUDGEMENT max HAS_TYPE
[x: posreal, y: posreal -> {z: posreal | z >= x AND z >= y}]
JUDGEMENT min HAS_TYPE
[x: posreal, y: posreal -> {z: posreal | z <= x AND z <= y}]

% rat subtype judgements

JUDGEMENT max HAS_TYPE [q: rat, r: rat -> {s: rat | s >= q AND s >= r}]
JUDGEMENT min HAS_TYPE [q: rat, r: rat -> {s: rat | s <= q AND s <= r}]

JUDGEMENT max HAS_TYPE [q: nzrat, r: nzrat -> {s: nzrat | s >= q AND s >= r}]
JUDGEMENT min HAS_TYPE [q: nzrat, r: nzrat -> {s: nzrat | s <= q AND s <= r}]

JUDGEMENT max HAS_TYPE
[q: nonneg_rat, r: nonneg_rat -> {s: nonneg_rat | s >= q AND s >= r}]
JUDGEMENT min HAS_TYPE
[q: nonneg_rat, r: nonneg_rat -> {s: nonneg_rat | s <= q AND s <= r}]

JUDGEMENT max HAS_TYPE
[q: posrat, r: posrat -> {s: posrat | s >= q AND s >= r}]
JUDGEMENT min HAS_TYPE
[q: posrat, r: posrat -> {s: posrat | s <= q AND s <= r}]

% int subtype judgements

JUDGEMENT max HAS_TYPE [i: int, j: int -> {k: int | i <= k AND j <= k}]
JUDGEMENT min HAS_TYPE [i: int, j: int -> {k: int | k <= i AND k <= j}]

JUDGEMENT max HAS_TYPE [i: nzint, j: nzint -> {k: nzint | i <= k AND j <= k}]
JUDGEMENT min HAS_TYPE [i: nzint, j: nzint -> {k: nzint | k <= i AND k <= j}]

JUDGEMENT max HAS_TYPE [i: nat, j: nat -> {k: nat | i <= k AND j <= k}]
JUDGEMENT min HAS_TYPE [i: nat, j: nat -> {k: nat | k <= i AND k <= j}]

JUDGEMENT max HAS_TYPE
[i: posint, j: posint -> {k: posint | i <= k AND j <= k}]
JUDGEMENT min HAS_TYPE
[i: posint, j: posint -> {k: posint | k <= i AND k <= j}]

END real_defs

% real_props contains useful properties about real numbers.  Most of
% these are known to the decision procedures of PVS, but there are some
% nonlinear ones that cannot be gotten automatically.  Nonlinear
% expressions are those that involve multiplication or division by two
% non-numeric terms.  Thus x*y and x/c are nonlinear, while 2001*x + 39*z is
% linear.  Note that it doesn't matter whether the terms are constants
% or variables, only whether they are actual numbers.

real_props: THEORY
BEGIN
w, x, y, z: VAR real
n0w, n0x, n0y, n0z: VAR nonzero_real
nnw, nnx, nny, nnz: VAR nonneg_real
pw, px, py, pz: VAR posreal
npw, npx, npy, npz: VAR nonpos_real
nw, nx, ny, nz: VAR negreal

inv_ne_0: LEMMA 1/n0x /= 0

% Cancellation Laws for equality

both_sides_plus1: LEMMA (x + z = y + z) IFF x = y

both_sides_plus2: LEMMA (z + x = z + y) IFF x = y

both_sides_minus1: LEMMA (x - z = y - z) IFF x = y

both_sides_minus2: LEMMA (z - x = z - y) IFF x = y

both_sides_times1: LEMMA (x * n0z = y * n0z) IFF x = y

both_sides_times2: LEMMA (n0z * x = n0z * y) IFF x = y

both_sides_div1: LEMMA (x/n0z = y/n0z) IFF x = y

both_sides_div2: LEMMA (n0z/n0x = n0z/n0y) IFF n0x = n0y

times_plus: LEMMA (x + y) * (z + w) = x*z + x*w + y*z + y*w

times_div1: LEMMA x * (y/n0z) = (x * y)/n0z

times_div2: LEMMA (x/n0z) * y = (x * y)/n0z

div_times: LEMMA (x/n0x) * (y/n0y) = (x*y)/(n0x*n0y)

div_eq_zero: LEMMA x/n0z = 0 IFF x = 0

div_simp: LEMMA n0x/n0x = 1

div_cancel1: LEMMA n0z * (x/n0z) = x

div_cancel2: LEMMA (x/n0z) * n0z = x

div_cancel3: LEMMA x/n0z = y IFF x = y * n0z

cross_mult: LEMMA (x/n0x = y/n0y) IFF (x * n0y = y * n0x)

add_div: LEMMA (x/n0x) + (y/n0y) = (x * n0y + y * n0x)/(n0x * n0y)

minus_div1: LEMMA (x/n0x) - (y/n0y) = (x * n0y - y * n0x)/(n0x * n0y)

minus_div2: LEMMA (x/n0x - y/n0x) = (x - y)/n0x

div_distributes: LEMMA (x/n0z) + (y/n0z) =  (x + y)/n0z

div_distributes_minus: LEMMA (x/n0z) - (y/n0z) =  (x - y)/n0z

div_div1: LEMMA (x / (n0y / n0z)) = ((x * n0z) / n0y)

div_div2: LEMMA ((x / n0y) / n0z) = (x / (n0y * n0z))

idem_add_is_zero: LEMMA x + x = x IMPLIES x = 0

zero_times1: LEMMA 0 * x = 0

zero_times2: LEMMA x * 0 = 0

zero_times3: LEMMA x * y = 0 IFF x = 0 OR y = 0

neg_times_neg: LEMMA (-x) * (-y) = x * y

zero_is_neg_zero: LEMMA -0 = 0

% Order lemmas for <

strict_lt : LEMMA strict_total_order?(<)

trich_lt: LEMMA x < y OR x = y OR y < x

tri_unique_lt1: LEMMA x < y IMPLIES (x /= y AND NOT(y < x))

tri_unique_lt2: LEMMA x = y IMPLIES (NOT(x < y) AND NOT(y < x))

zero_not_lt_zero: LEMMA NOT 0 < 0

neg_lt: LEMMA 0 < -x IFF x < 0

pos_times_lt: LEMMA 0 < x * y IFF (0 < x AND 0 < y) OR (x < 0 AND y < 0)

neg_times_lt: LEMMA x * y < 0 IFF (0 < x AND y < 0) OR (x < 0 AND 0 < y)

quotient_pos_lt: FORMULA 0 < 1/n0x IFF 0 < n0x

quotient_neg_lt: FORMULA 1/n0x < 0 IFF n0x < 0

pos_div_lt: LEMMA 0 < x/n0y IFF (0 < x AND 0 < n0y) OR (x < 0 AND n0y < 0)

neg_div_lt: LEMMA x/n0y < 0 IFF (0 < x AND n0y < 0) OR (x < 0 AND 0 < n0y)

div_mult_pos_lt1: LEMMA z/py < x IFF z < x * py

div_mult_pos_lt2: LEMMA x < z/py IFF x * py < z

div_mult_neg_lt1: LEMMA z/ny < x IFF x * ny < z

div_mult_neg_lt2: LEMMA x < z/ny IFF z < x * ny

% Cancellation laws for <

both_sides_plus_lt1: LEMMA x + z < y + z IFF x < y

both_sides_plus_lt2: LEMMA z + x < z + y IFF x < y

both_sides_minus_lt1: LEMMA x - z < y - z IFF x < y

both_sides_minus_lt2: LEMMA z - x < z - y IFF y < x

both_sides_times_pos_lt1: LEMMA x * pz < y * pz IFF x < y

both_sides_times_pos_lt2: LEMMA pz * x < pz * y IFF x < y

both_sides_times_neg_lt1: LEMMA x * nz < y * nz IFF y < x

both_sides_times_neg_lt2: LEMMA nz * x < nz * y IFF y < x

both_sides_div_pos_lt1: LEMMA x/pz < y/pz IFF x < y

both_sides_div_pos_lt2: LEMMA pz/px < pz/py IFF py < px

both_sides_div_pos_lt3: LEMMA nz/px < nz/py IFF px < py

both_sides_div_neg_lt1: LEMMA x/nz < y/nz IFF y < x

both_sides_div_neg_lt2: LEMMA pz/nx < pz/ny IFF ny < nx

both_sides_div_neg_lt3: LEMMA nz/nx < nz/ny IFF nx < ny

%  lt_plus_lt: LEMMA x < y AND z < w IMPLIES x + z < y + w

lt_plus_lt1: LEMMA x <= y AND z < w IMPLIES x + z < y + w

lt_plus_lt2: LEMMA x < y AND z <= w IMPLIES x + z < y + w

%  lt_minus_lt: LEMMA x < y AND w < z IMPLIES x - z < y - w

lt_minus_lt1: LEMMA x <= y AND w < z IMPLIES x - z < y - w

lt_minus_lt2: LEMMA x < y AND w <= z IMPLIES x - z < y - w

%  lt_times_lt_pos: LEMMA nnx < y AND nnz < w IMPLIES nnx * nnz < y * w

lt_times_lt_pos1: LEMMA px <= y AND nnz < w IMPLIES px * nnz < y * w

lt_times_lt_pos2: LEMMA nnx < y AND pz <= w IMPLIES nnx * pz < y * w

%  lt_div_lt_pos: LEMMA nnx < y AND pz < w IMPLIES nnx/w < y/pz

lt_div_lt_pos1: LEMMA px <= y AND pz < w IMPLIES px/w < y/pz

lt_div_lt_pos2: LEMMA nnx < y AND pz <= w IMPLIES nnx/w < y/pz

%  lt_times_lt_neg: LEMMA x < npy AND z < npw IMPLIES npy * npw < x * z

lt_times_lt_neg1: LEMMA x <= ny AND z < npw IMPLIES ny * npw < x * z

lt_times_lt_neg2: LEMMA x < npy AND z <= nw IMPLIES npy * nw < x * z

%  lt_div_lt_neg: LEMMA x < npy AND z < nw IMPLIES npy/z < x/nw

lt_div_lt_neg1: LEMMA x <= ny AND z < nw IMPLIES ny/z < x/nw

lt_div_lt_neg2: LEMMA x < npy AND z <= nw IMPLIES npy/z < x/nw

% Order lemmas for <=

total_le: LEMMA total_order?(<=)

dich_le: LEMMA x <= y OR y <= x

zero_le_zero: LEMMA 0 <= 0

neg_le: LEMMA 0 <= -x IFF x <= 0

pos_times_le: LEMMA 0 <= x * y IFF (0 <= x AND 0 <= y) OR (x <= 0 AND y <= 0)

neg_times_le: LEMMA x * y <= 0 IFF (0 <= x AND y <= 0) OR (x <= 0 AND 0 <= y)

quotient_pos_le: FORMULA 0 <= 1/n0x IFF 0 <= n0x

quotient_neg_le: FORMULA 1/n0x <= 0 IFF n0x <= 0

pos_div_le: LEMMA
0 <= x/n0y IFF (0 <= x AND 0 <= n0y) OR (x <= 0 AND n0y <= 0)

neg_div_le: LEMMA
x/n0y <= 0 IFF (0 <= x AND n0y <= 0) OR (x <= 0 AND 0 <= n0y)

div_mult_pos_le1: LEMMA z/py <= x IFF z <= x * py

div_mult_pos_le2: LEMMA x <= z/py IFF x * py <= z

div_mult_neg_le1: LEMMA z/ny <= x IFF x * ny <= z

div_mult_neg_le2: LEMMA x <= z/ny IFF z <= x * ny

% Cancellation laws for <=

both_sides_plus_le1: LEMMA x + z <= y + z IFF x <= y

both_sides_plus_le2: LEMMA z + x <= z + y IFF x <= y

both_sides_minus_le1: LEMMA x - z <= y - z IFF x <= y

both_sides_minus_le2: LEMMA z - x <= z - y IFF y <= x

both_sides_times_pos_le1: LEMMA x * pz <= y * pz IFF x <= y

both_sides_times_pos_le2: LEMMA pz * x <= pz * y IFF x <= y

both_sides_times_neg_le1: LEMMA x * nz <= y * nz IFF y <= x

both_sides_times_neg_le2: LEMMA nz * x <= nz * y IFF y <= x

both_sides_div_pos_le1: LEMMA x/pz <= y/pz IFF x <= y

both_sides_div_pos_le2: LEMMA pz/px <= pz/py IFF py <= px

both_sides_div_pos_le3: LEMMA nz/px <= nz/py IFF px <= py

both_sides_div_neg_le1: LEMMA x/nz <= y/nz IFF y <= x

both_sides_div_neg_le2: LEMMA pz/nx <= pz/ny IFF ny <= nx

both_sides_div_neg_le3: LEMMA nz/nx <= nz/ny IFF nx <= ny

le_plus_le: LEMMA x <= y AND z <= w IMPLIES x + z <= y + w

le_minus_le: LEMMA x <= y AND w <= z IMPLIES x - z <= y - w

le_times_le_pos: LEMMA nnx <= y AND nnz <= w IMPLIES nnx * nnz <= y * w

le_div_le_pos: LEMMA nnx <= y AND pz <= w IMPLIES nnx/w <= y/pz

le_times_le_neg: LEMMA x <= npy AND z <= npw IMPLIES npy * npw <= x * z

le_div_le_neg: LEMMA x <= npy AND z <= nw IMPLIES npy/z <= x/nw

% Order lemmas for >

strict_gt : LEMMA strict_total_order?(>)

trich_gt: LEMMA x > y OR x = y OR y > x

tri_unique_gt1: LEMMA x > y IMPLIES (x /= y AND NOT(y > x))

tri_unique_gt2: LEMMA x = y IMPLIES (NOT(x > y) AND NOT(y > x))

zero_not_gt_zero: LEMMA NOT 0 > 0

neg_gt: LEMMA 0 > -x IFF x > 0

pos_times_gt: LEMMA x * y > 0 IFF (0 > x AND 0 > y) OR (x > 0 AND y > 0)

neg_times_gt: LEMMA 0 > x * y IFF (0 > x AND y > 0) OR (x > 0 AND 0 > y)

quotient_pos_gt: FORMULA 1/n0x > 0 IFF n0x > 0

quotient_neg_gt: FORMULA 0 > 1/n0x IFF 0 > n0x

pos_div_gt: LEMMA x/n0y > 0 IFF (0 > x AND 0 > n0y) OR (x > 0 AND n0y > 0)

neg_div_gt: LEMMA 0 > x/n0y IFF (0 > x AND n0y > 0) OR (x > 0 AND 0 > n0y)

div_mult_pos_gt1: LEMMA x > z/py IFF x * py > z

div_mult_pos_gt2: LEMMA z/py > x IFF z > x * py

div_mult_neg_gt1: LEMMA x > z/ny IFF z > x * ny

div_mult_neg_gt2: LEMMA z/ny > x IFF x * ny > z

% Cancellation laws for >

both_sides_plus_gt1: LEMMA x + z > y + z IFF x > y

both_sides_plus_gt2: LEMMA z + x > z + y IFF x > y

both_sides_minus_gt1: LEMMA x - z > y - z IFF x > y

both_sides_minus_gt2: LEMMA z - x > z - y IFF y > x

both_sides_times_pos_gt1: LEMMA x * pz > y * pz IFF x > y

both_sides_times_pos_gt2: LEMMA pz * x > pz * y IFF x > y

both_sides_times_neg_gt1: LEMMA x * nz > y * nz IFF y > x

both_sides_times_neg_gt2: LEMMA nz * x > nz * y IFF y > x

both_sides_div_pos_gt1: LEMMA x/pz > y/pz IFF x > y

both_sides_div_pos_gt2: LEMMA pz/px > pz/py IFF py > px

both_sides_div_pos_gt3: LEMMA nz/px > nz/py IFF px > py

both_sides_div_neg_gt1: LEMMA x/nz > y/nz IFF y > x

both_sides_div_neg_gt2: LEMMA pz/nx > pz/ny IFF ny > nx

both_sides_div_neg_gt3: LEMMA nz/nx > nz/ny IFF nx > ny

%  gt_plus_gt: LEMMA x > y AND z > w IMPLIES x + z > y + w

gt_plus_gt1: LEMMA x >= y AND z > w IMPLIES x + z > y + w

gt_plus_gt2: LEMMA x > y AND z >= w IMPLIES x + z > y + w

%  gt_minus_gt: LEMMA x > y AND w > z IMPLIES x - z > y - w

gt_minus_gt1: LEMMA x >= y AND w > z IMPLIES x - z > y - w

gt_minus_gt2: LEMMA x > y AND w >= z IMPLIES x - z > y - w

%  gt_times_gt_pos: LEMMA x > nny AND z > nnw IMPLIES x * z > nny * nnw

gt_times_gt_pos1: LEMMA x >= py AND z > nnw IMPLIES x * z > py * nnw

gt_times_gt_pos2: LEMMA x > nny AND z >= pw IMPLIES x * z > nny * pw

%  gt_div_gt_pos: LEMMA x > nny AND z > pw IMPLIES x/pw > nny/z

gt_div_gt_pos1: LEMMA x >= py AND z > pw IMPLIES x/pw > py/z

gt_div_gt_pos2: LEMMA x > nny AND z >= pw IMPLIES x/pw > nny/z

%  gt_times_gt_neg: LEMMA npx > y AND npz > w IMPLIES y * w > npx * npz

gt_times_gt_neg1: LEMMA nx >= y AND npz > w IMPLIES y * w > nx * npz

gt_times_gt_neg2: LEMMA npx > y AND nz >= w IMPLIES y * w > npx * nz

%  gt_div_gt_neg: LEMMA npx > y AND nz > w IMPLIES y/nz > npx/w

gt_div_gt_neg1: LEMMA nx >= y AND nz > w IMPLIES y/nz > nx/w

gt_div_gt_neg2: LEMMA npx > y AND nz >= w IMPLIES y/nz > npx/w

% Order lemmas for >=

strict_ge : LEMMA total_order?(>=)

dich_ge: LEMMA x >= y OR y >= x

zero_ge_zero: LEMMA 0 >= 0

neg_ge: LEMMA 0 >= -x IFF x >= 0

pos_times_ge: LEMMA x * y >= 0 IFF (0 >= x AND 0 >= y) OR (x >= 0 AND y >= 0)

neg_times_ge: LEMMA 0 >= x * y IFF (0 >= x AND y >= 0) OR (x >= 0 AND 0 >= y)

quotient_pos_ge: FORMULA 1/n0x >= 0 IFF n0x >= 0

quotient_neg_ge: FORMULA 0 >= 1/n0x IFF 0 >= n0x

pos_div_ge: LEMMA
x/n0y >= 0 IFF (0 >= x AND 0 >= n0y) OR (x >= 0 AND n0y >= 0)

neg_div_ge: LEMMA
0 >= x/n0y IFF (0 >= x AND n0y >= 0) OR (x >= 0 AND 0 >= n0y)

div_mult_pos_ge1: LEMMA z/py >= x IFF z >= x * py

div_mult_pos_ge2: LEMMA x >= z/py IFF x * py >= z

div_mult_neg_ge1: LEMMA z/ny >= x IFF x * ny >= z

div_mult_neg_ge2: LEMMA x >= z/ny IFF z >= x * ny

% Cancellation laws for >=

both_sides_plus_ge1: LEMMA x + z >= y + z IFF x >= y

both_sides_plus_ge2: LEMMA z + x >= z + y IFF x >= y

both_sides_minus_ge1: LEMMA x - z >= y - z IFF x >= y

both_sides_minus_ge2: LEMMA z - x >= z - y IFF y >= x

both_sides_times_pos_ge1: LEMMA x * pz >= y * pz IFF x >= y

both_sides_times_pos_ge2: LEMMA pz * x >= pz * y IFF x >= y

both_sides_times_neg_ge1: LEMMA x * nz >= y * nz IFF y >= x

both_sides_times_neg_ge2: LEMMA nz * x >= nz * y IFF y >= x

both_sides_div_pos_ge1: LEMMA x/pz >= y/pz IFF x >= y

both_sides_div_pos_ge2: LEMMA pz/px >= pz/py IFF py >= px

both_sides_div_pos_ge3: LEMMA nz/px >= nz/py IFF px >= py

both_sides_div_neg_ge1: LEMMA x/nz >= y/nz IFF y >= x

both_sides_div_neg_ge2: LEMMA pz/nx >= pz/ny IFF ny >= nx

both_sides_div_neg_ge3: LEMMA nz/nx >= nz/ny IFF nx >= ny

ge_plus_ge: LEMMA x >= y AND z >= w IMPLIES x + z >= y + w

ge_minus_ge: LEMMA x >= y AND w >= z IMPLIES x - z >= y - w

ge_times_ge_pos: LEMMA x >= nny AND z >= nnw IMPLIES x * z >= nny * nnw

ge_div_ge_pos: LEMMA x >= nny AND z >= pw IMPLIES x/pw >= nny/z

ge_times_ge_neg: LEMMA npx >= y AND npz >= w IMPLIES y * w >= npx * npz

ge_div_ge_neg: LEMMA npx >= y AND nz >= w IMPLIES y/nz >= npx/w

%

nonzero_times1: LEMMA n0x * y = 0 IFF y = 0

nonzero_times2: LEMMA x * n0y = 0 IFF x = 0

nonzero_times3: LEMMA n0x * n0y = 0 IFF FALSE

% Useful lemmas about the multiplicative identity

eq1_gt: FORMULA x > 1 AND x * y = 1 IMPLIES y < 1

eq1_ge: FORMULA x >= 1 AND x * y = 1 IMPLIES y <= 1

eqm1_gt: FORMULA x > 1 AND x * y = -1 IMPLIES y > -1

eqm1_ge: FORMULA x >= 1 AND x * y = -1 IMPLIES y >= -1

eqm1_lt: FORMULA x < -1 AND x * y = -1 IMPLIES y < 1

eqm1_le: FORMULA x <= -1 AND x * y = -1 IMPLIES y <= 1

sqrt_1: LEMMA x * x = 1 IFF x = 1 OR x = -1

idem_mult: LEMMA x * x = x IFF x = 0 OR x = 1

% Lower bounds and completeness

real_lower_complete: LEMMA
FORALL (S: (nonempty?[real])):
(EXISTS (y : real) : lower_bound?(<=)(y, S)) IMPLIES
(EXISTS (x: real): greatest_lower_bound?(<=)(x, S))

i, j: VAR int

product_1: LEMMA i >= 0 AND j >= 0 AND i*j = 1 IMPLIES i = 1 AND j = 1

product_m1: LEMMA i >= 0 AND j <= 0 AND i*j = -1 IMPLIES i = 1 AND j = -1

% Properties of absolute value

triangle: LEMMA abs(x+y) <= abs(x) + abs(y)

abs_mult: LEMMA abs(x * y) = abs(x) * abs(y)

abs_limits: LEMMA -(abs(x) + abs(y)) <= x + y AND x + y <= abs(x) + abs(y)

% Properties of min and max

min_is_le: LEMMA min(x, y) <= x

max_is_ge: LEMMA max(x, y) >= x

min_le_max: LEMMA min(x, y) <= max(x, y)

% lub and glb

S: VAR (nonempty?[real])

bounded_above?(S): bool = (EXISTS x: upper_bound?(<=)(x, S))

bounded_below?(S): bool = (EXISTS x: lower_bound?(<=)(x, S))

bounded?(S): bool = bounded_above?(S) AND bounded_below?(S)

bounded_set: TYPE = (bounded?)

SA: VAR (bounded_above?)

lub_exists: LEMMA (EXISTS x: least_upper_bound?(<=)(x, SA))

lub(SA): {x | least_upper_bound?(<=)(x, SA)}

lub_lem: LEMMA lub(SA) = x IFF least_upper_bound?(<=)(x, SA)

SB: VAR (bounded_below?)

glb_exists: LEMMA (EXISTS x: greatest_lower_bound?(<=)(x, SB))

glb(SB): {x | greatest_lower_bound?(<=)(x, SB)}

glb_lem: LEMMA glb(SB) = x IFF greatest_lower_bound?(<=)(x, SB)

% The axiom of Archimedes

axiom_of_archimedes: LEMMA EXISTS i: x < i

END real_props

% rational_props contains the properties of rational numbers.  This mostly
% consists of subtypes and judgements, as most of the properties given in
% real_props are inherited.

rational_props: THEORY
BEGIN
x, y: VAR real
i: VAR int
n0j: VAR nzint
r: VAR rat

rational_pred_ax: AXIOM EXISTS i, n0j: r = i/n0j

density: AXIOM x < y IMPLIES (EXISTS r: x <= r AND r <= y)

END rational_props

% integer_props contains the properties of integers and naturalnumbers.

integer_props: THEORY
BEGIN
m, n: VAR nat
i, j: VAR int

N: VAR (nonempty?[nat])

I: VAR (nonempty?[int])

integer_pred_ax: LEMMA EXISTS n: i = n OR i = -n

lub_nat: LEMMA
upper_bound?((LAMBDA m, n: m <= n))(m, N)
=> EXISTS (n:(N)): least_upper_bound?((LAMBDA m, n: m <= n))(n, N)

lub_int: LEMMA
upper_bound?((LAMBDA i, j: i <= j))(i, I)
=> EXISTS (j:(I)): least_upper_bound?((LAMBDA i, j: i <= j))(j, I)

END integer_props

% The definitions for floor and ceiling, courtesy of
%   Paul S. Miner   		           email: p.s.miner@larc.nasa.gov
%   Mail Stop 130			     fax: (804) 864-4234
%   NASA Langley Research Center	   phone: (804) 864-6201
%   Hampton, Virginia 23681-0001

floor_ceil: THEORY
BEGIN

x, y: VAR real

i: VAR integer

floor_exists: LEMMA EXISTS i: i <= x & x < i + 1

ceiling_exists: LEMMA EXISTS i: x <= i & i < x + 1

floor(x): {i | i <= x & x < i + 1}

fractional(x): {x | 0 <= x & x < 1} = x - floor(x)

ceiling(x): {i | x <= i & i < x + 1}

floor_def: LEMMA floor(x) <= x & x < floor(x) + 1

ceiling_def: LEMMA x <= ceiling(x) & ceiling(x) < x + 1

floor_ceiling_reflect1: LEMMA floor(-x) = -ceiling(x)

floor_ceiling_reflect2: LEMMA ceiling(-x) = -floor(x)

JUDGEMENT floor, ceiling HAS_TYPE [nonneg_real -> nat]

floor_int: LEMMA floor(i) = i

ceiling_int: LEMMA ceiling(i) = i

floor_plus_int: LEMMA floor(x + i) = floor(x) + i

ceiling_plus_int: LEMMA ceiling(x + i) = ceiling(x) + i

floor_ceiling_nonint: LEMMA NOT integer?(x) => ceiling(x) - floor(x) = 1

floor_ceiling_int: lemma floor(i)=ceiling(i)

floor_neg: LEMMA
floor(x) = IF integer?(x) THEN -floor(-x) ELSE -floor(-x) - 1 ENDIF

real_parts: LEMMA x = floor(x) + fractional(x)

floor_plus: LEMMA
floor(x + y) = floor(x) + floor(y) + floor(fractional(x) + fractional(y))

ceiling_plus: LEMMA
ceiling(x + y) = floor(x) + floor(y) + ceiling(fractional(x) + fractional(y))

floor_split: lemma i = floor(i/2)+ceiling(i/2)

floor_within_1: lemma x - floor(x) < 1

ceiling_within_1: lemma ceiling(x) - x < 1

END floor_ceil

% exponentiation provides the definitions expt and ^.  expt multiplies a
% real by itself the number of times specified, where 0 times returns a 1
% (thus expt(0,0) = 1).  ^ is defined in terms of expt to work for
% integers, but in this case if the integer negative then the real
% argument must be nonzero; this leads to the dependent type given below.

exponentiation: THEORY
BEGIN
r: VAR real
m, n: VAR nat
pm, pn: VAR posnat
i, j: VAR int
n0i, n0j: VAR nzint
x, y: VAR real
px, py: VAR posreal
n0x, n0y: VAR nzreal
gt1x, gt1y: VAR {r: posreal | r > 1}
lt1x, lt1y: VAR {r: posreal | r < 1}
ge1x, ge1y: VAR {r: posreal | r >= 1}
le1x, le1y: VAR {r: posreal | r <= 1}

expt(r, n): RECURSIVE real =
IF n = 0 THEN 1
ELSE r * expt(r, n-1)
ENDIF
MEASURE n;

expt_pos_aux: LEMMA expt(px, n) > 0

expt_nonzero_aux: LEMMA expt(n0x, n) /= 0;

JUDGEMENT expt HAS_TYPE [nonneg_real, nat -> nonneg_real]
JUDGEMENT expt HAS_TYPE [posreal, nat -> posreal]
JUDGEMENT expt HAS_TYPE [rational, nat -> rational]
JUDGEMENT expt HAS_TYPE [nonneg_rat, nat -> nonneg_rat]
JUDGEMENT expt HAS_TYPE [posrat, nat -> posrat]
JUDGEMENT expt HAS_TYPE [integer, nat -> integer]
JUDGEMENT expt HAS_TYPE [nat, nat -> nat]
JUDGEMENT expt HAS_TYPE [posint, nat -> posint]

^(r: real, i:{i:int | r /= 0 OR i >= 0}): real
= IF i >= 0 THEN expt(r, i) ELSE 1/expt(r, -i) ENDIF

expt_pos: LEMMA px^i > 0

expt_nonzero: LEMMA n0x^i /= 0

JUDGEMENT ^ HAS_TYPE [nr:nonneg_real, {i:int | nr /= 0 OR i >= 0} -> nonneg_real]
JUDGEMENT ^ HAS_TYPE [pr:posreal, {i:int | pr /= 0 OR i >= 0} -> posreal]
JUDGEMENT ^ HAS_TYPE [q:rational, {i:int | q /= 0 OR i >= 0} -> rational]
JUDGEMENT ^ HAS_TYPE [nq:nonneg_rat, {i:int | nq /= 0 OR i >= 0} -> nonneg_rat]
JUDGEMENT ^ HAS_TYPE [pq:posrat, {i:int | pq /= 0 OR i >= 0} -> posrat]
JUDGEMENT ^ HAS_TYPE [integer, nat -> integer]
JUDGEMENT ^ HAS_TYPE [nat, nat -> nat]
JUDGEMENT ^ HAS_TYPE [posint, nat -> posint]

% Properties of expt

expt_x0_aux: LEMMA expt(x, 0) = 1

expt_x1_aux: LEMMA expt(x, 1) = x

expt_1n_aux: LEMMA expt(1, n) = 1

increasing_expt_aux: LEMMA expt(gt1x, m+2) > gt1x

decreasing_expt_aux: LEMMA expt(lt1x, m+2) < lt1x

expt_1_aux: LEMMA expt(px, n + 1) = 1 IFF px = 1

expt_plus_aux: LEMMA expt(n0x, m + n) = expt(n0x, m) * expt(n0x, n)

expt_minus_aux: LEMMA
m >= n IMPLIES expt(n0x, m - n) = expt(n0x, m)/expt(n0x, n)

expt_times_aux: LEMMA expt(n0x, m * n) = expt(expt(n0x, m), n)

expt_divide_aux: LEMMA 1/expt(n0x, m * n) = expt(1/expt(n0x, m), n)

both_sides_expt1_aux: LEMMA expt(px, m+1) = expt(px, n+1) IFF m = n OR px = 1

both_sides_expt2_aux: LEMMA expt(px, pm) = expt(py, pm) IFF px = py

both_sides_expt_pos_lt_aux: LEMMA
expt(px, m+1) < expt(py, m+1) IFF px < py

both_sides_expt_gt1_lt_aux: LEMMA
expt(gt1x, m+1) < expt(gt1x, n+1) IFF m < n

both_sides_expt_lt1_lt_aux: LEMMA
expt(lt1x, m+1) < expt(lt1x, n+1) IFF n < m

both_sides_expt_pos_le_aux: LEMMA
expt(px, m+1) <= expt(py, m+1) IFF px <= py

both_sides_expt_gt1_le_aux: LEMMA
expt(gt1x, m+1) <= expt(gt1x, n+1) IFF m <= n

both_sides_expt_lt1_le_aux: LEMMA
expt(lt1x, m+1) <= expt(lt1x, n+1) IFF n <= m

both_sides_expt_pos_gt_aux: LEMMA
expt(px, m+1) > expt(py, m+1) IFF px > py

both_sides_expt_gt1_gt_aux: LEMMA
expt(gt1x, m+1) > expt(gt1x, n+1) IFF m > n

both_sides_expt_lt1_gt_aux: LEMMA
expt(lt1x, m+1) > expt(lt1x, n+1) IFF n > m

both_sides_expt_pos_ge_aux: LEMMA
expt(px, m+1) >= expt(py, m+1) IFF px >= py

both_sides_expt_gt1_ge_aux: LEMMA
expt(gt1x, m+1) >= expt(gt1x, n+1) IFF m >= n

both_sides_expt_lt1_ge_aux: LEMMA
expt(lt1x, m+1) >= expt(lt1x, n+1) IFF n >= m

% Properties of ^

expt_x0: LEMMA x^0 = 1

expt_x1: LEMMA x^1 = x

expt_1i: LEMMA 1^i = 1

expt_plus: LEMMA n0x^(i + j) = n0x^i * n0x^j

expt_times: LEMMA n0x^(i * j) = (n0x^i)^j

expt_inverse: LEMMA n0x^(-i) = 1/(n0x^i)

expt_div: LEMMA n0x^i/n0x^j = n0x^(i-j)

both_sides_expt1: LEMMA px ^ n0i = px ^ n0j IFF n0i = n0j OR px = 1

both_sides_expt2: LEMMA px ^ n0i = py ^ n0i IFF px = py

b: VAR above(1)

pos_expt_gt: LEMMA n < b^n

expt_ge1: LEMMA b^n >= 1

both_sides_expt_pos_lt: LEMMA px ^ pm < py ^ pm IFF px < py

both_sides_expt_gt1_lt: LEMMA gt1x ^ i < gt1x ^ j IFF i < j

both_sides_expt_lt1_lt: LEMMA lt1x ^ i < lt1x ^ j IFF j < i

both_sides_expt_pos_le: LEMMA px ^ pm <= py ^ pm IFF px <= py

both_sides_expt_gt1_le: LEMMA gt1x ^ i <= gt1x ^ j IFF i <= j

both_sides_expt_lt1_le: LEMMA lt1x ^ i <= lt1x ^ j IFF j <= i

both_sides_expt_pos_gt: LEMMA px ^ pm > py ^ pm IFF px > py

both_sides_expt_gt1_gt: LEMMA gt1x ^ i > gt1x ^ j IFF i > j

both_sides_expt_lt1_gt: LEMMA lt1x ^ i > lt1x ^ j IFF j > i

both_sides_expt_pos_ge: LEMMA px ^ pm >= py ^ pm IFF px >= py

both_sides_expt_gt1_ge: LEMMA gt1x ^ i >= gt1x ^ j IFF i >= j

both_sides_expt_lt1_ge: LEMMA lt1x ^ i >= lt1x ^ j IFF j >= i

expt_gt1_pos: LEMMA gt1x^pm >= gt1x

expt_gt1_neg: LEMMA gt1x^(-pm) < 1

expt_gt1_nonpos: LEMMA gt1x^(-m) <= 1

exp_of_exists: lemma exists i: b^i <= py & py < b^(i+1)

END exponentiation

% subrange_induction defines induction schemas for subranges.  This is a
% parameterized theory so that it may be used as a name to the prover
% induction commands.  subrange_induction is the weak form, and
% SUBRANGE_induction is the strong form of induction.

subrange_inductions[i: int, j: upfrom(i)]: THEORY
BEGIN
k, m: VAR subrange(i, j)
p: VAR pred[subrange(i, j)]

subrange_induction: LEMMA
(p(i) AND (FORALL k: k < j AND p(k) IMPLIES p(k + 1)))
IMPLIES (FORALL k: p(k))

SUBRANGE_induction: LEMMA
(FORALL k: (FORALL m: m < k IMPLIES p(m)) IMPLIES p(k))
IMPLIES (FORALL k: p(k))

END subrange_inductions

% bounded_int_inductions provides the weak and strong forms of induction for
% the various bounded subtypes of int.

bounded_int_inductions[m: int]: THEORY
BEGIN
pf: VAR pred[upfrom(m)]
jf, kf: VAR upfrom(m)

upfrom_induction: LEMMA
(pf(m) AND (FORALL jf: pf(jf) IMPLIES pf(jf + 1)))
IMPLIES (FORALL jf: pf(jf))

UPFROM_induction: LEMMA
(FORALL jf: (FORALL kf: kf < jf IMPLIES pf(kf)) IMPLIES pf(jf))
IMPLIES (FORALL jf: pf(jf))

pa: VAR pred[above(m)]
ja, ka: VAR above(m)

above_induction: LEMMA
(pa(m+1) AND (FORALL ja: pa(ja) IMPLIES pa(ja + 1)))
IMPLIES (FORALL ja: pa(ja))

ABOVE_induction: LEMMA
(FORALL ja: (FORALL ka: ka < ja IMPLIES pa(ka)) IMPLIES pa(ja))
IMPLIES (FORALL ja: pa(ja))

END bounded_int_inductions

% bounded_nat_inductions provides the weak and strong forms of induction for
% the various bounded subtypes of nat.

bounded_nat_inductions[m: nat]: THEORY
BEGIN
pt: VAR pred[upto(m)]
jt, kt: VAR upto(m)

upto_induction: LEMMA
(pt(0) AND (FORALL jt: jt < m AND pt(jt) IMPLIES pt(jt + 1)))
IMPLIES (FORALL jt: pt(jt))

UPTO_induction: LEMMA
(FORALL jt: (FORALL kt: kt < jt IMPLIES pt(kt)) IMPLIES pt(jt))
IMPLIES (FORALL jt: pt(jt))

pb: VAR pred[below(m)]
jb, kb: VAR below(m)

below_induction: LEMMA
((m > 0 IMPLIES pb(0))
AND (FORALL jb: jb < m - 1 AND pb(jb) IMPLIES pb(jb + 1)))
IMPLIES (FORALL jb: pb(jb))

BELOW_induction: LEMMA
(FORALL jb: (FORALL kb: kb < jb IMPLIES pb(kb)) IMPLIES pb(jb))
IMPLIES (FORALL jb: pb(jb))

END bounded_nat_inductions

% int_types defines the subrange type as a parameterized type.

subrange_type[m, n: int] : THEORY
BEGIN
subrange: TYPE = subrange(m, n)
END subrange_type

% int_types defines some useful subtypes of the integers for
% backward compatibility.

int_types[m: int] : THEORY
BEGIN
upfrom: NONEMPTY_TYPE = upfrom(m)
above:  NONEMPTY_TYPE = above(m)
END int_types

% nat_types defines some useful subtypes of the natural numbers for
% backward compatibility.

nat_types[m: nat] : THEORY
BEGIN
upto:   NONEMPTY_TYPE = upto(m)
below:  TYPE = below(m)
END nat_types

% 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
f: VAR [T -> T]
m, n: VAR nat
x: VAR T

iterate(f, n)(x): RECURSIVE T =
IF n = 0 THEN x ELSE f(iterate(f, n-1)(x)) ENDIF
MEASURE n

iterate(f, m) o iterate(f, n) = iterate(f, m + n)

iterate_mult: LEMMA
iterate(iterate(f, m), n) = iterate(f, m * n)

iterate_invariant: LEMMA
f(iterate(f, n)(x)) = iterate(f, n)(f(x))

END function_iterate

% 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]
i, n: VAR nat
x: VAR T
p: VAR pred[T]
seq: VAR sequence
Trel: VAR PRED[[T, T]]

nth(seq, n): T = seq(n)

suffix(seq, n): sequence =
(LAMBDA i: seq(i+n))

first(seq): T = nth(seq, 0)

rest(seq): sequence = suffix(seq, 1)

delete(n, seq): sequence =
(LAMBDA i: (IF i < n THEN seq(i) ELSE seq(i + 1) ENDIF))

insert(x, n, seq): sequence =
(LAMBDA i: (IF i < n THEN seq(i)
ELSIF i = n THEN x
ELSE seq(i - 1) ENDIF))

add(x, seq): sequence = insert(x, 0, seq)

insert_delete: LEMMA insert(nth(seq, n), n, delete(n, seq)) = seq

every(p)(seq): bool = (FORALL n: p(nth(seq, n)))

every(p, seq): bool = (FORALL n: p(nth(seq, n)))

some(p)(seq): bool = (EXISTS n: p(nth(seq, n)))

some(p, seq): bool = (EXISTS n: p(nth(seq, n)))

sequence_induction: LEMMA
p(nth(seq, 0)) AND (FORALL n: p(nth(seq, n)) IMPLIES p(nth(seq, n + 1)))
IMPLIES every(p)(seq)

ascends?(seq, Trel): bool = preserves(seq, (LAMBDA i, n: i <= n), Trel)

descends?(seq, Trel): bool = inverts(seq, (LAMBDA i, n: i <= n), Trel)

END sequences

% seq_functions defines the map function that generates the image of a
% sequence under a function.

seq_functions[D, R: TYPE]: THEORY
BEGIN
f: VAR [D -> R]
s: VAR sequence[D]
n: VAR nat

map(f)(s): sequence[R] = (LAMBDA n: f(nth(s, n)))

map(f, s): sequence[R] = (LAMBDA n: f(nth(s, n)))

END seq_functions

% This theory defines finite sequences as a dependent type.  Two finite
% sequences are concatenated with the operator 'o', and a subsequence can be
% extracted with the operator '^'.  Note that ^ allows any natural numbers
% m and n to define the range; if m > n then the empty sequence is returned

finite_sequences [T: TYPE]: THEORY
BEGIN
finite_sequence: TYPE = [# length: nat, seq: [below[length] -> T] #]
finseq: TYPE = finite_sequence

fs, fs1, fs2, fs3: VAR finseq
m, n: VAR nat

empty_seq: finseq =
(# length := 0,
seq := (LAMBDA (x: below): epsilon! (t:T): true) #)

finseq_appl(fs): [below[length(fs)] -> T] = seq(fs);

CONVERSION finseq_appl

o(fs1, fs2): finseq =
LET l1 = length(fs1),
lsum = l1 + length(fs2)
IN (# length := lsum,
seq := (LAMBDA (n:below[lsum]):
IF n < l1
THEN seq(fs1)(n)
ELSE seq(fs2)(n-l1)
ENDIF) #);

p: VAR [nat, nat]

^(fs, p): finseq =
LET (m, n) = p
IN IF m > n OR m >= length(fs)
THEN empty_seq
ELSE LET len = min(n - m + 1, length(fs) - m)
IN (# length := len,
seq := (LAMBDA (x: below[len]): seq(fs)(x + m)) #)
ENDIF

extract1(fs:{fs | length(fs) = 1}): T = seq(fs)(0)

CONVERSION extract1

o_assoc: LEMMA fs1 o (fs2 o fs3) = (fs1 o fs2) o fs3

END finite_sequences

% ordstruct provides the building blocks for defining the
% ordinals up to epsilon_0.

ordstruct: DATATYPE
BEGIN
zero: zero?
add(coef: posnat, exp: ordstruct, rest: ordstruct): nonzero?
END ordstruct

% ordinals uses the ordstruct datatype to define the ordinals up to
% epsilon_0, by providing an ordering on ordstruct and defining the
% ordinals to be those elements of type ordstruct that are in a
% Cantor normal form with respect to the ordering.  Thus
%    add(i, u, v) = i.omega^u + v
%    add(i, u, add(j, v, w)) = i.omega^u + j.w^v + w, where u>v.

ordinals: THEORY
BEGIN
i, j, k: VAR posnat
m, n, o: VAR nat
u, v, w, x, y, z: VAR ordstruct
size: [ordstruct->nat] = reduce[nat](0, (LAMBDA i, m, n: 1 + m+n));

<(x, y): RECURSIVE bool =
CASES x OF
zero: NOT zero?(y),
add(i, u, v): CASES y OF
zero: FALSE,
add(j, z, w): (u(x, y): bool = y < x;
<=(x, y): bool = x < y OR x = y;
>=(x, y): bool = y < x OR y = x

ordinal?(x): RECURSIVE bool =
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: NONEMPTY_TYPE = (ordinal?)

r, s, t: VAR ordinal

ordinal_irreflexive: LEMMA NOT r < r

ordinal_antisym: LEMMA r < s IMPLIES NOT s < r

ordinal_antisymmetric: LEMMA r <= s AND s <= r IMPLIES r = s

ordinal_transitive: LEMMA r < s AND s < t IMPLIES r < t

ordinal_trichotomy: LEMMA r < s OR r = s OR s < r

p: VAR pred[ordinal]

ordinal_induction: AXIOM
(FORALL r: (FORALL s: s < r IMPLIES p(s)) IMPLIES p(r))
IMPLIES (FORALL r: p(r))

well_founded_le: LEMMA
well_founded?(LAMBDA (r, s: (ordinal?)): r < s)

END ordinals

% lex2 provides a lexical ordering for pairs of natural numbers.
% This illustrates the use of ordinals.

lex2: THEORY
BEGIN

i, j, m, n: VAR nat

lex2(m, n): ordinal =
(IF m=0
THEN IF n = 0
THEN zero
ENDIF
ENDIF)

lex2_lt: LEMMA
lex2(i, j) < lex2(m, n) =
(i < m OR (i = m AND j < n))

END lex2

% list provides the datatype definition for lists.

list [T: TYPE]: DATATYPE
BEGIN
null: null?
cons (car: T, cdr:list):cons?

END list

% list_props provides the length, append, and reverse functions.
% These could have been defined using the reduce function generated
% for the list datatype, but this is harder to work with in an
% interactive proof.

list_props [T: TYPE]: THEORY
BEGIN
l, l1, l2, l3: VAR list[T]
x: VAR T

length(l): RECURSIVE nat =
CASES l OF
null: 0,
cons(x, y): length(y) + 1
ENDCASES
MEASURE reduce_nat(0, (LAMBDA (x: T), (n: nat): n + 1))

member(x, l): RECURSIVE bool =
CASES l OF
null: FALSE,
cons(hd, tl): x = hd OR member(x, tl)
ENDCASES
MEASURE length(l)

nth(l, (n:below[length(l)])): RECURSIVE T =
IF n = 0 THEN car(l) ELSE nth(cdr(l), n-1) ENDIF
MEASURE length(l)

append(l1, l2): RECURSIVE list[T] =
CASES l1 OF
null: l2,
cons(x, y): cons(x, append(y, l2))
ENDCASES
MEASURE length(l1)

reverse(l): RECURSIVE list[T] =
CASES l OF
null: l,
cons(x, y): append(reverse(y), cons(x, null))
ENDCASES
MEASURE length

append_null: LEMMA append(l, null) = l

append_assoc: LEMMA
append(l1, append(l2, l3)) = append(append(l1, l2), l3)

reverse_append: LEMMA
reverse(append(l1, l2)) = append(reverse(l2), reverse(l1))

reverse_reverse: LEMMA reverse(reverse(l)) = l

a, b, c: VAR T

list_rep: LEMMA (: a, b, c :) = cons(a, cons(b, cons(c, null)))

END list_props

% map_props gives the commutativity properties of composition and map,
% for both sequences and lists.

map_props [T1, T2, T3: TYPE]: THEORY
BEGIN
f1: VAR [T1 -> T2]
f2: VAR [T2 -> T3]
s: VAR sequence[T1]
l: VAR list[T1]

map_list_composition: LEMMA map(f2)(map(f1)(l)) = map(f2 o f1)(l)

map_seq_composition: LEMMA map(f2)(map(f1)(s)) = map(f2 o f1)(s)

END map_props

% 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.  Both the curried and uncurried forms are
% given.  Note that filter on lists could be defined using reduce, but
% becomes harder to work with in an interactive proof.

filters[T: TYPE]: THEORY
BEGIN
s: VAR set[T]
l: VAR list[T]
p: VAR pred[T]

filter(s, p): set[T] = {x: T | s(x) & p(x)}

filter(p)(s): set[T] = {x: T | s(x) & p(x)}

filter(l, p): 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 length(l)

filter(p)(l): RECURSIVE list[T] =
CASES l OF
null: null,
cons(x, y): IF p(x) THEN cons(x, filter(p)(y)) ELSE filter(p)(y) ENDIF
ENDCASES
MEASURE length(l)
END filters

% list2finseq

list2finseq[T: TYPE]: THEORY
BEGIN
l: VAR list[T]
fs: VAR finseq[T]
n: VAR nat

list2finseq(l): finseq[T] =
(# length := length(l),
seq := (LAMBDA (x: below[length(l)]): nth(l, x)) #)

finseq2list_rec(fs, (n: nat | n <= length(fs))): RECURSIVE list[T] =
IF n = 0
THEN null
ELSE cons(seq(fs)(n-1), finseq2list_rec(fs, n-1))
ENDIF
MEASURE n

finseq2list(fs): list[T] = finseq2list_rec(fs, length(fs))

CONVERSION list2finseq, finseq2list

END list2finseq

% list2set

list2set[T:TYPE]: THEORY
BEGIN
l: VAR list[T]
x: VAR T

list2set(l) : RECURSIVE set[T] =
CASES l OF
null: emptyset[T],
ENDCASES
MEASURE length

CONVERSION list2set

END list2set

% characters - this follows the ASCII control codes, of which only the
% first 128 are defined:
%
%     |  0 NUL|  1 SOH|  2 STX|  3 ETX|  4 EOT|  5 ENQ|  6 ACK|  7 BEL|
%     |  8 BS |  9 HT | 10 NL | 11 VT | 12 NP | 13 CR | 14 SO | 15 SI |
%     | 16 DLE| 17 DC1| 18 DC2| 19 DC3| 20 DC4| 21 NAK| 22 SYN| 23 ETB|
%     | 24 CAN| 25 EM | 26 SUB| 27 ESC| 28 FS | 29 GS | 30 RS | 31 US |
%     | 32 SP | 33  ! | 34  " | 35  # | 36  \$ | 37  % | 38  & | 39  ' |
%     | 40  ( | 41  ) | 42  * | 43  + | 44  , | 45  - | 46  . | 47  / |
%     | 48  0 | 49  1 | 50  2 | 51  3 | 52  4 | 53  5 | 54  6 | 55  7 |
%     | 56  8 | 57  9 | 58  : | 59  ; | 60  < | 61  = | 62  > | 63  ? |
%     | 64  @ | 65  A | 66  B | 67  C | 68  D | 69  E | 70  F | 71  G |
%     | 72  H | 73  I | 74  J | 75  K | 76  L | 77  M | 78  N | 79  O |
%     | 80  P | 81  Q | 82  R | 83  S | 84  T | 85  U | 86  V | 87  W |
%     | 88  X | 89  Y | 90  Z | 91  [ | 92  \ | 93  ] | 94  ^ | 95  _ |
%     | 96  ` | 97  a | 98  b | 99  c |100  d |101  e |102  f |103  g |
%     |104  h |105  i |106  j |107  k |108  l |109  m |110  n |111  o |
%     |112  p |113  q |114  r |115  s |116  t |117  u |118  v |119  w |
%     |120  x |121  y |122  z |123  { |124  | |125  } |126  ~ |127 DEL|

character: DATATYPE
BEGIN
char(code:below):char?
END character

% strings - strings are input as a sequence of characters between double
% quotes.  The \ is an escape character, whose value depends on the
% following character(s).  \" and \\ are used to embed a " and \ in a string.
% A \ followed by a decimal number (< 256) or a \x or \X followed by a
% hexidecimal number (< FF) represents that character number.  The other
% possibilities are:
%  \a  - 007 (C-g, Bell)
%  \b  - 008 (C-h, Backspace)
%  \t  - 009 (C-i, Tab)
%  \n  - 010 (C-j, Newline)
%  \v  - 011 (C-k, VT)
%  \f  - 012 (C-l, Newpage)
%  \r  - 013 (C-m, Return)

strings: THEORY
BEGIN
string: TYPE = finite_sequence[character]

string_rep: LEMMA
"foo" = list2finseq(cons(char(102),
cons(char(111),
cons(char(111), null))))
END strings

% The rest of the prelude contains examples meant to illustrate language
% features not illustrated in the preceding theories.  Note that these
% theories are not meant to be imported.

% Tuples - this is just an example that both indicates what is known by
% the theorem prover, and provides an example.

tuple_prelude_example: THEORY
BEGIN
T_prelude: TYPE = [a: int, b: {x: int | x < a}]
t1, t2: VAR T_prelude

T_prelude_extensionality: POSTULATE
(PROJ_1(t1) = PROJ_1(t2) AND PROJ_2(t1) = PROJ_2(t2)) IMPLIES t1 = t2

t_prelude: T_prelude = (3, 2)

tupaccess_prelude: FORMULA PROJ_1(3,2) = PROJ_2((7,3))

tupform_prelude: FORMULA t_prelude WITH [1 := 4] = (4, 2)
END tuple_prelude_example

% Records - this is just an example that both indicates what is known by
% the theorem prover, and provides an example.

record_prelude_example: THEORY
BEGIN
R_prelude: TYPE = [# a: int, b: {x: int | x < a} #]
r1, r2: VAR R_prelude

R_prelude_extensionality: POSTULATE
(a(r1) = a(r2) AND b(r1) = b(r2))
IMPLIES r1 = r2

r_prelude: R_prelude = (# a := 3, b := 2 #)

recform_prelude: FORMULA r_prelude WITH [a := 4] = (# a := 4, b := 2 #)
END record_prelude_example
```