% 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
% Lemmas about 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_add: LEMMA member(x, a) IMPLIES add(x, a) = a
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_add: LEMMA choose(add(x, a)) = x OR member(choose(add(x, a)), 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
exponent_adjust: LEMMA b^i+b^(i-pm) < b^(i+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_add: LEMMA
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
add_first_rest: LEMMA add(first(seq), rest(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[0]): 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
ELSE add(n, zero, zero)
ENDIF
ELSIF n = 0 THEN add(m, add(1,zero,zero),zero)
ELSE add(m, add(1,zero,zero), add(n,zero, zero))
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],
cons(x, y): add(x, list2set(y))
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[256]):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