% 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.
% --------------------------------------------------------------------
% PVS
% Copyright (C) 2006, SRI International. All Rights Reserved.
% This program is free software; you can redistribute it and/or
% modify it under the terms of the GNU General Public License
% as published by the Free Software Foundation; either version 2
% of the License, or (at your option) any later version.
% This program is distributed in the hope that it will be useful,
% but WITHOUT ANY WARRANTY; without even the implied warranty of
% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
% GNU General Public License for more details.
% You should have received a copy of the GNU General Public License
% along with this program; if not, write to the Free Software
% Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
% --------------------------------------------------------------------
% 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);
≠: [T, T -> bool] = /=
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 syntax.
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 some properties of IF and =.
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: POSTULATE
(FORALL (x: D): f(x) = g(x)) IFF f = g
% The extensionality lemma is provided as it is easier to use
% as a rewrite than the above postulate.
extensionality: LEMMA
(FORALL (x: D): f(x) = g(x)) IMPLIES f = g
congruence: POSTULATE 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)
bij_is_inj: JUDGEMENT (bijective?) SUBTYPE_OF (injective?)
bij_is_surj: JUDGEMENT (bijective?) SUBTYPE_OF (surjective?)
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))
% Curried form
preserves(Drel, Rrel)(f): bool = preserves(f, Drel, Rrel)
inverts(f, Drel, Rrel): bool =
FORALL x1, x2: Drel(x1, x2) IMPLIES Rrel(f(x2), f(x1))
% Curried form
inverts(Drel, Rrel)(f): bool = inverts(f, Drel, Rrel)
END functions
functions_alt [D, R: TYPE, Drel: PRED[[D, D]], Rrel: PRED[[R, R]]]: THEORY
BEGIN
f: VAR [D -> R]
preserves: [[D -> R] -> bool] = preserves(Drel, Rrel)
inverts: [[D -> R] -> bool] = inverts(Drel, Rrel)
END functions_alt
transpose[T1, T2, T3: TYPE]: THEORY
BEGIN
f: VAR [T1 -> [T2 -> T3]]
x: VAR T1
y: VAR T2
transpose(f)(y)(x): T3 = f(x)(y)
END transpose
% 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.
% Note also that the typechecker expands restrict automatically in some
% cases if it is fully applied, i.e., restrict(f)(x) is replaced with f(x).
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))
restrict_of_inj_is_inj: JUDGEMENT
restrict(f: (injective?[T,R])) HAS_TYPE (injective?[S,R])
END restrict
% restrict_props provides the lemma that extending a function from a given
% domain type to the same type is the identity. This usually comes about
% because of theory instantiation, and the typechecker has this rule built
% in, so it won't be needed in general.
restrict_props[T: TYPE, R: TYPE]: THEORY
BEGIN
f: VAR [T -> R]
restrict_full: LEMMA restrict[T, T, R](f) = f
END restrict_props
% 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
% extend_props provides the lemma that extending a function from a given
% domain type to the same type is the identity. This usually comes about
% because of theory instantiation, and the typechecker has this rule built
% in, so it won't be needed in general.
extend_props [T: TYPE, R: TYPE, d: R]: THEORY
BEGIN
f: VAR [T -> R]
extend_full: LEMMA extend[T, T, R, d](f) = f
END extend_props
%-------------------------------------------------------------------------
%
% Cases in which the introduction of extend preserves properties.
%
% ---------------------------------------------------------------------
% Author: Jerry James (jamesj@acm.org), University of Kansas
%
% extend_func_props
%-------------------------------------------------------------------------
extend_func_props[T: TYPE, S: TYPE FROM T, R: TYPE, d: R]: THEORY
BEGIN
surjective_extend: JUDGEMENT
extend[T, S, R, d](f: (surjective?[S, R])) HAS_TYPE (surjective?[T, R])
END extend_func_props
% The K combinator is used to trigger lambda conversions.
% Due to user demand, it is turned off by default.
K_conversion [T1, T2: TYPE]: THEORY
BEGIN
K_conversion(x:T1)(y:T2): T1 = x
% CONVERSION K_conversion
END K_conversion
K_props [T1, T2: TYPE, S: TYPE FROM T1]: THEORY
BEGIN
K_preserves: JUDGEMENT K_conversion[T1, T2](x:S)(y:T2) HAS_TYPE S
K_preserves1: JUDGEMENT K_conversion[T1, T2](x:S) HAS_TYPE [T2 -> S]
END K_props
% 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
identity_props [T: TYPE, S: TYPE FROM T]: THEORY
BEGIN
x: VAR S
I_preserves: JUDGEMENT I[T](x) HAS_TYPE S
id_preserves: JUDGEMENT id[T](x) HAS_TYPE S
identity_preserves: JUDGEMENT identity[T](x) HAS_TYPE S
END identity_props
% 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)
equivalence: TYPE = (equivalence?)
equiv_is_reflexive: JUDGEMENT (equivalence?) SUBTYPE_OF (reflexive?)
equiv_is_symmetric: JUDGEMENT (equivalence?) SUBTYPE_OF (symmetric?)
equiv_is_transitive: JUDGEMENT (equivalence?) SUBTYPE_OF (transitive?)
% Reflexive closure
RC(R)(x, y): bool = (x = y) OR R(x, y)
% Transitive closure
TC(R)(x, y): INDUCTIVE bool = R(x,y) OR (EXISTS z: TC(R)(x,z) AND TC(R)(z,y))
% Reflexive-transitive closure
RTC(R)(x, y): bool = (x = y) OR TC(R)(x, y)
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?(<=)
preorder_is_reflexive: JUDGEMENT (preorder?) SUBTYPE_OF (reflexive?[T])
preorder_is_transitive: JUDGEMENT (preorder?) SUBTYPE_OF (transitive?[T])
equiv_is_preorder: JUDGEMENT (equivalence?[T]) SUBTYPE_OF (preorder?)
partial_order?(<=): bool = preorder?(<=) & antisymmetric?(<=)
po_is_preorder: JUDGEMENT (partial_order?) SUBTYPE_OF (preorder?)
po_is_antisymmetric: JUDGEMENT
(partial_order?) SUBTYPE_OF (antisymmetric?[T])
strict_order?(<): bool = irreflexive?(<) & transitive?(<)
strict_is_irreflexive: JUDGEMENT
(strict_order?) SUBTYPE_OF (irreflexive?[T])
strict_order_is_antisymmetric: JUDGEMENT
(strict_order?) SUBTYPE_OF (antisymmetric?[T])
strict_is_transitive: JUDGEMENT
(strict_order?) SUBTYPE_OF (transitive?[T])
dichotomous?(<=): bool = (FORALL x, y: (x <= y OR y <= x))
total_order?(<=): bool = partial_order?(<=) & dichotomous?(<=)
total_is_po: JUDGEMENT (total_order?) SUBTYPE_OF (partial_order?)
total_is_dichotomous: JUDGEMENT (total_order?) SUBTYPE_OF (dichotomous?)
linear_order?(<=): bool = total_order?(<=)
linear_is_total: JUDGEMENT (linear_order?) SUBTYPE_OF (total_order?)
total_is_linear: JUDGEMENT (total_order?) SUBTYPE_OF (linear_order?)
trichotomous?(<): bool = (FORALL x, y: x < y OR y < x OR x = y)
strict_total_order?(<): bool = strict_order?(<) & trichotomous?(<)
strict_total_is_strict: JUDGEMENT
(strict_total_order?) SUBTYPE_OF (strict_order?)
strict_total_is_trichotomous: JUDGEMENT
(strict_total_order?) SUBTYPE_OF (trichotomous?)
well_founded?(<): bool =
(FORALL p:
(EXISTS y: p(y))
IMPLIES (EXISTS (y:(p)): (FORALL (x:(p)): (NOT x < y))))
strict_well_founded?(<): bool = strict_order?(<) & well_founded?(<)
strict_well_founded_is_strict: JUDGEMENT
(strict_well_founded?) SUBTYPE_OF (strict_order?)
strict_well_founded_is_well_founded: JUDGEMENT
(strict_well_founded?) SUBTYPE_OF (well_founded?)
well_ordered?(<): bool = strict_total_order?(<) & well_founded?(<)
well_ordered_is_strict_total: JUDGEMENT
(well_ordered?) SUBTYPE_OF (strict_total_order?)
well_ordered_is_well_founded: JUDGEMENT
(well_ordered?) SUBTYPE_OF (well_founded?)
nonempty_pred: TYPE = {p: pred[T] | EXISTS (x: T): p(x)}
pe: VAR pred[T]
upper_bound?(<)(x, pe): bool = FORALL (y: (pe)): y < x
upper_bound?(<)(pe)(x): bool = upper_bound?(<)(x, pe)
lower_bound?(<)(x, pe): bool = FORALL (y: (pe)): x < y
lower_bound?(<)(pe)(x): bool = lower_bound?(<)(x, pe)
least_upper_bound?(<)(x, pe): bool =
upper_bound?(<)(x, pe) AND
FORALL y: upper_bound?(<)(y, pe) IMPLIES (x < y OR x = y)
least_upper_bound?(<)(pe)(x): bool = least_upper_bound?(<)(x, pe)
greatest_lower_bound?(<)(x, pe): bool =
lower_bound?(<)(x, pe) AND
FORALL y: lower_bound?(<)(y, pe) IMPLIES (y < x OR x = y)
greatest_lower_bound?(<)(pe)(x): bool = greatest_lower_bound?(<)(x, pe)
END orders
orders_alt [T: TYPE, < : pred[[T, T]], pe: nonempty_pred[T]]: THEORY
BEGIN
x: VAR T
upper_bound?: [T -> bool] = upper_bound?(<)(pe)
least_upper_bound?: [T -> bool] = least_upper_bound?(<)(pe)
lower_bound?: [T -> bool] = lower_bound?(<)(pe)
greatest_lower_bound?: [T -> bool] = greatest_lower_bound?(<)(pe)
least_upper_bound_is_upper_bound: JUDGEMENT
(least_upper_bound?) SUBTYPE_OF (upper_bound?)
greatest_lower_bound_is_lower_bound: JUDGEMENT
(greatest_lower_bound?) SUBTYPE_OF (lower_bound?)
END orders_alt
%-------------------------------------------------------------------------
%
% Cases in which the introduction of restrict preserves properties.
%
% ---------------------------------------------------------------------
% Author: Jerry James (jamesj@acm.org), University of Kansas
%
% restrict_order_props
%-------------------------------------------------------------------------
restrict_order_props[T: TYPE, S: TYPE FROM T]: THEORY
BEGIN
reflexive_restrict: JUDGEMENT
restrict(R: (reflexive?[T])) HAS_TYPE (reflexive?[S])
irreflexive_restrict: JUDGEMENT
restrict(R: (irreflexive?[T])) HAS_TYPE (irreflexive?[S])
symmetric_restrict: JUDGEMENT
restrict(R: (symmetric?[T])) HAS_TYPE (symmetric?[S])
antisymmetric_restrict: JUDGEMENT
restrict(R: (antisymmetric?[T])) HAS_TYPE (antisymmetric?[S])
connected_restrict: JUDGEMENT
restrict(R: (connected?[T])) HAS_TYPE (connected?[S])
transitive_restrict: JUDGEMENT
restrict(R: (transitive?[T])) HAS_TYPE (transitive?[S])
equivalence_restrict: JUDGEMENT
restrict(R: (equivalence?[T])) HAS_TYPE (equivalence?[S])
preorder_restrict: JUDGEMENT
restrict(R: (preorder?[T])) HAS_TYPE (preorder?[S])
partial_order_restrict: JUDGEMENT
restrict(R: (partial_order?[T])) HAS_TYPE (partial_order?[S])
strict_order_restrict: JUDGEMENT
restrict(R: (strict_order?[T])) HAS_TYPE (strict_order?[S])
dichotomous_restrict: JUDGEMENT
restrict(R: (dichotomous?[T])) HAS_TYPE (dichotomous?[S])
total_order_restrict: JUDGEMENT
restrict(R: (total_order?[T])) HAS_TYPE (total_order?[S])
trichotomous_restrict: JUDGEMENT
restrict(R: (trichotomous?[T])) HAS_TYPE (trichotomous?[S])
strict_total_order_restrict: JUDGEMENT
restrict(R: (strict_total_order?[T])) HAS_TYPE (strict_total_order?[S])
well_founded_restrict: JUDGEMENT
restrict(R: (well_founded?[T])) HAS_TYPE (well_founded?[S])
well_ordered_restrict: JUDGEMENT
restrict(R: (well_ordered?[T])) HAS_TYPE (well_ordered?[S])
END restrict_order_props
% Courtesy of Jerry James
extend_order_props[T: TYPE, S: TYPE FROM T]: THEORY
BEGIN
irreflexive_extend: JUDGEMENT
extend[[T, T], [S, S], bool, FALSE](R: (irreflexive?[S]))
HAS_TYPE (irreflexive?[T])
symmetric_extend: JUDGEMENT
extend[[T, T], [S, S], bool, FALSE](R: (symmetric?[S]))
HAS_TYPE (symmetric?[T])
antisymmetric_extend: JUDGEMENT
extend[[T, T], [S, S], bool, FALSE](R: (antisymmetric?[S]))
HAS_TYPE (antisymmetric?[T])
transitive_extend: JUDGEMENT
extend[[T, T], [S, S], bool, FALSE](R: (transitive?[S]))
HAS_TYPE (transitive?[T])
strict_order_extend: JUDGEMENT
extend[[T, T], [S, S], bool, FALSE](R: (strict_order?[S]))
HAS_TYPE (strict_order?[T])
END extend_order_props
% 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<x IMPLIES p(y))
IMPLIES p(x))
IMPLIES
(FORALL (x:T): p(x)))
END wf_induction
% measure_induction builds on well-founded induction. It allows
% induction over a type T for which a measure function m is defined.
measure_induction [T: TYPE, M: TYPE, m: [T -> M], < : (well_founded?[M])]: THEORY
BEGIN
measure_induction: LEMMA
(FORALL (p: pred[T]):
(FORALL (x: T):
(FORALL (y: T): m(y) < m(x) 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 on the predicate. 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, which 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
% The axiom below deals with nonempty types in decl parameters.
% Theory parameters add an existence assumption, but there's No way to do
% this with declaration parameters. Note that this relies on the way PVS
% tracks nonempty types. In general, this is only useful for types declared
% to be nonempty, For example, in a declaration such as
% f[T: TYPE+, S: TYPE](x: T, y: S): int = ...
% nonempty_ax[T] can be used as a lemma. nonempty_ax[S] can also be tried,
% but since S is not known to be nonempty in this example, it will generate
% a TCC that looks circular.
decl_params: THEORY
BEGIN
nonempty_ax[T: TYPE+]: AXIOM EXISTS (x: T): TRUE
END decl_params
% 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);
∈(x, a): bool = a(x);
∉(x, a): bool = ¬ a(x);
empty?(a): bool = (FORALL x: NOT member(x, a))
emptyset: set = {x | false};
∅: set = {x | false};
nonempty?(a): bool = NOT empty?(a)
nonempty_set: TYPE = (nonempty?)
full?(a): bool = (FORALL x: member(x, a))
fullset: set = {x | true}
nontrivial?(a): bool = a /= emptyset & a /= fullset
subset?(a, b): bool = (FORALL x: member(x, a) => member(x, b));
⊆(a, b): bool = ∀ x: x ∈ a => x ∈ b;
strict_subset?(a, b): bool = subset?(a, b) & a /= b;
⊂(a, b): bool = ⊆(a, b) ∧ a /= b;
union(a, b): set = {x | member(x, a) OR member(x, b)};
∪(a, b): set = {x | x ∈ a ∨ x ∈ b};
intersection(a, b): set = {x | member(x, a) AND member(x, b)};
∩(a, b): set = {x | x ∈ a ∧ 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?(a): bool = (EXISTS (x:(a)): (FORALL (y:(a)): x = y))
singleton(x): (singleton?) = {y | y = x}
% CONVERSION+ singleton
add(x, a): (nonempty?) = {y | x = y OR member(y, a)}
remove(x, a): set = {y | x /= y AND member(y, a)}
% A choice function for nonempty sets
% No longer defined, so that grind will not expand epsilon.
% It's generally easier to use typepred on choose than to bring in epsilon_ax
% Can always bring in choose_is_epsilon axiom if the expansion is desired.
choose(p: (nonempty?)): (p) % = epsilon(p)
choose_is_epsilon: AXIOM FORALL (p: (nonempty?)): choose(p) = epsilon(p)
the(p: (singleton?)): (p)
the_lem: LEMMA FORALL (p: (singleton?)): the(p) = epsilon(p)
the_prop: LEMMA FORALL (p: (singleton?)): p(the(p))
singleton_elt(a: (singleton?)): T = the! x: member(x, a)
CONVERSION+ singleton_elt
is_singleton: LEMMA
FORALL a: (nonempty?(a) AND FORALL x, y: a(x) AND a(y) IMPLIES (x=y))
IMPLIES singleton?(a)
singleton_elt_lem: LEMMA singleton?(a) and a(x) IMPLIES singleton_elt(a) = x
singleton_elt_def: LEMMA singleton?(a) IMPLIES singleton_elt(a) = choose(a)
singleton_singleton: LEMMA singleton?(a) IMPLIES (EXISTS x: a = singleton(x))
singleton_rew: LEMMA singleton_elt(singleton(x)) = x
AUTO_REWRITE+ singleton_rew
rest(a): set = IF empty?(a) THEN a ELSE remove(choose(a), a) ENDIF
setofsets: TYPE = setof[setof[T]]
A, B : Var setofsets
powerset(a): setofsets = {b | subset?(b, a)};
𝒫(a): setofsets = {b | b ⊆ a};
Union(A): set = {x | EXISTS (a: (A)): a(x)}
Intersection(A): set = {x | FORALL (a: (A)): a(x)}
nonempty_singleton: JUDGEMENT (singleton?) SUBTYPE_OF (nonempty?)
nonempty_union1: JUDGEMENT union(a: (nonempty?), b: set) HAS_TYPE (nonempty?)
nonempty_union2: JUDGEMENT union(a: set, b: (nonempty?)) HAS_TYPE (nonempty?)
END sets
% Lemmas about sets - many of these came from Bruno Dutertre in the
% more_set_lemmas theory of the finite_sets library
sets_lemmas [T: TYPE]: THEORY
BEGIN
x, y: VAR T
a, b, c: VAR set[T]
A, B : Var setofsets[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)
emptyset_min: LEMMA subset?(a, emptyset) IMPLIES a = emptyset
nonempty_member: LEMMA nonempty?(a) IFF EXISTS x: member(x, a)
fullset_member: LEMMA member(x, fullset)
fullset_max: LEMMA subset?(fullset, a) IMPLIES a = fullset
fullset_is_full?: LEMMA full?(a) IFF a = fullset
nonempty_exists: LEMMA nonempty?(a) IFF EXISTS (x: (a)): TRUE
subset_emptyset: LEMMA subset?(emptyset, a)
subset_fullset: LEMMA subset?(a, fullset)
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_is_partial_order: JUDGEMENT
subset?[T] HAS_TYPE (partial_order?[set[T]])
strict_subset_irreflexive: LEMMA NOT strict_subset?(a, a)
strict_subset_transitive: LEMMA
strict_subset?(a, b) AND strict_subset?(b, c) IMPLIES
strict_subset?(a, c)
strict_subset_strict_order: LEMMA strict_order?(strict_subset?[T])
strict_subset_is_strict_order: JUDGEMENT
strict_subset?[T] HAS_TYPE (strict_order?[set[T]])
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
subset_union: LEMMA subset?(union(a, b), c) = (subset?(a, c) AND subset?(b, c))
union_upper_bound : LEMMA
subset?(a, c) and subset?(b, c) IMPLIES subset?(union(a, b), c)
union_difference: LEMMA union(a, b) = union(a, difference(b, a))
union_diff_subset: LEMMA subset?(a, b) IMPLIES union(a, difference(b, a)) = 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
intersection_lower_bound: LEMMA
subset?(c, a) and subset?(c, b) IMPLIES subset?(c, intersection(a, b))
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
complement_equal: LEMMA complement(a) = complement(b) IFF a = b
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))
difference_subset : LEMMA subset?(difference(a, b), a)
difference_subset2: LEMMA
subset?(a, b) IMPLIES difference(a, b) = emptyset
difference_disjoint: LEMMA disjoint?(a, difference(b, a))
difference_disjoint2: LEMMA disjoint?(a, b) IMPLIES difference(a, b) = a
diff_union_inter: LEMMA
difference(union(a, b), a) = difference(b, intersection(a, b))
nonempty_add: LEMMA NOT empty?(add(x, a))
member_add: LEMMA member(x, a) IMPLIES add(x, a) = a
member_add_reduce: LEMMA member(x, add(y, a)) = (x = y or member(x, a))
member_remove: LEMMA NOT member(x, a) IMPLIES remove(x, a) = a
add_remove_member: LEMMA member(x, a) IMPLIES add(x, remove(x, a)) = a
remove_add_member: LEMMA NOT member(x, a) IMPLIES remove(x, add(x, a)) = a
subset_add: LEMMA subset?(a, add(x, a))
add_as_union: LEMMA add(x, a) = union(a, singleton(x))
singleton_as_add: LEMMA singleton(x) = add(x, emptyset)
subset_remove: LEMMA subset?(remove(x, a), a)
remove_as_difference: LEMMA remove(x, a) = difference(a, singleton(x))
remove_member_singleton: LEMMA remove(x, singleton(x)) = emptyset
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)
rest_subset : LEMMA subset?(rest(a), 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]
singleton_subset: LEMMA member(x, a) IFF subset?(singleton(x), a)
rest_empty_lem: LEMMA NOT empty?(a) AND empty?(rest(a))
IMPLIES a = singleton(choose(a))
singleton_disjoint: LEMMA NOT member(x, a) IMPLIES disjoint?(singleton(x), a)
disjoint_remove_left: LEMMA
disjoint?(a, b) IMPLIES disjoint?(remove(x, a), b)
disjoint_remove_right: LEMMA
disjoint?(a, b) IMPLIES disjoint?(a, remove(x, b))
union_disj_remove_left: LEMMA
disjoint?(a, b) AND a(x) IMPLIES
union(remove(x, a), b) = remove(x, union(a, b))
union_disj_remove_right: LEMMA
disjoint?(a, b) AND b(x) IMPLIES
union(a, remove(x, b)) = remove(x, union(a, b))
subset_powerset: LEMMA subset?(a, b) IFF member(a, powerset(b))
empty_powerset: LEMMA empty?(a) IFF singleton?(powerset(a))
powerset_emptyset: LEMMA member(emptyset, powerset(a))
nonempty_powerset: JUDGEMENT powerset(a) HAS_TYPE (nonempty?[set[T]])
powerset_union: LEMMA Union(powerset(a)) = a
powerset_intersection: LEMMA empty?(Intersection(powerset(a)))
powerset_subset: LEMMA subset?(a, b) IFF subset?(powerset(a), powerset(b))
Union_empty: LEMMA empty?(Union(A)) IFF empty?(A) OR every(empty?)(A)
Union_full: LEMMA
full?(Union(A)) IFF (FORALL x: EXISTS (a: (A)): member(x, a))
Union_member: LEMMA member(x,Union(A)) IFF (EXISTS (a:(A)): member(x,a))
Union_subset: LEMMA FORALL (a: (A)): subset?(a, Union(A))
Union_surjective: JUDGEMENT
Union HAS_TYPE (surjective?[setofsets[T], set[T]])
Union_emptyset_rew: LEMMA Union(emptyset[set[T]]) = emptyset
Union_union_rew: LEMMA nonempty?(A) IMPLIES
Union(A) = union(choose(A), Union(rest(A)))
Intersection_empty: LEMMA
empty?(Intersection(A)) IFF
(FORALL x: EXISTS (a: (A)): NOT member(x, a))
Intersection_full: LEMMA full?(Intersection(A)) IFF every(full?)(A)
Intersection_member: LEMMA
member(x,Intersection(A)) IFF (FORALL (a:(A)): member(x,a))
%% The Intersection function should only be applied to nonempty sets of
%% sets. This is why.
Intersection_empty_full: COROLLARY full?(Intersection(emptyset[set[T]]))
Intersection_surjective: JUDGEMENT
Intersection HAS_TYPE (surjective?[setofsets[T], set[T]])
Intersection_intersection_rew: LEMMA
nonempty?(A) IMPLIES
Intersection(A) = intersection(choose(A), Intersection(rest(A)))
Complement(A): setofsets[T] = {a | EXISTS (b: (A)): a = complement(b)}
Complement_empty: LEMMA empty?(Complement(A)) IFF empty?(A)
Complement_full: LEMMA full?(Complement(A)) IFF full?(A)
Complement_Complement: LEMMA Complement(Complement(A)) = A
subset_Complement: LEMMA
subset?(Complement(A), Complement(B)) IFF subset?(A, B)
Complement_bijective: JUDGEMENT
Complement HAS_TYPE (bijective?[setofsets[T], setofsets[T]])
Demorgan1: LEMMA complement(Union(A)) = Intersection(Complement(A))
Demorgan2: LEMMA complement(Intersection(A)) = Union(Complement(A))
END sets_lemmas
%-------------------------------------------------------------------------
%
% An alternate formulation of function inverses. The version above
% requires that the domain type be nonempty. This causes two
% difficulties:
%
% (1) Functions from empty types to empty types have inverses, but the
% function_inverse theory cannot describe them.
%
% (2) Bijections always have inverses, but function_inverse (uselessly)
% generates TCCs requiring that the domain type be nonempty.
%
% Furthermore, for non-injective functions, the function_inverse theory
% only gives a way of generating *some* inverse, using the Axiom of Choice.
% There is no way to ask whether some function *is* an inverse of the given
% function.
%
% This theory is presented in two parts. The first part makes no
% assumptions about the domain and range types at all. It presents
% basic definitions, and some results that can be proven with no
% information on the types. The second part uses an assumption on the
% input types, which is constructed to be as easily satisfiable as
% possible. However, this is still not as convenient as the
% function_inverse version when the domain type is known to be nonempty.
%
% ---------------------------------------------------------------------
% Author: Jerry James (jamesj@acm.org), University of Kansas
%-------------------------------------------------------------------------
function_inverse_def[D: TYPE, R: TYPE]: THEORY
BEGIN
d: VAR D
r: VAR R
f: VAR [D -> R]
g: VAR [R -> D]
left_inverse?(g, f): bool = FORALL d: g(f(d)) = d
right_inverse?(g, f): bool = FORALL r: f(g(r)) = r
inverse?(g, f): bool = FORALL r: (EXISTS d: f(d) = r) => f(g(r)) = r
left_inverse?(f)(g): MACRO bool = left_inverse?(g, f)
right_inverse?(f)(g): MACRO bool = right_inverse?(g, f)
inverse?(f)(g): MACRO bool = inverse?(g, f)
%%% Left inverses / injective functions
left_inverse_is_inverse: LEMMA
FORALL f, (g: (left_inverse?(f))): inverse?(g, f)
left_inj_surj: LEMMA
FORALL f, (g: (left_inverse?(f))): injective?(f) AND surjective?(g)
inj_left_alt: LEMMA
FORALL (f: (injective?[D, R])), (g: (inverse?(f))): left_inverse?(g, f)
surj_inv_alt: COROLLARY
FORALL (f: (injective?[D, R])), (g: (inverse?(f))): surjective?(g)
injective_inverse_alt: LEMMA
FORALL (f: (injective?[D, R])), (g: (inverse?(f))): r = f(d) => g(r) = d
comp_inverse_left_inj_alt: LEMMA
FORALL (f: (injective?[D, R])), (g: (inverse?(f))): g(f(d)) = d
noninjective_inverse_exists: LEMMA
FORALL f: injective?(f) OR (EXISTS g: inverse?(g, f))
%%% Right inverses / surjective functions
right_inverse_is_inverse: LEMMA
FORALL f, (g: (right_inverse?(f))): inverse?(g, f)
right_surj_inj: LEMMA
FORALL f, (g: (right_inverse?(f))): surjective?(f) AND injective?(g)
surj_right_alt: LEMMA
FORALL (f: (surjective?[D, R])), (g: (inverse?(f))): right_inverse?(g, f)
inj_inv_alt: COROLLARY
FORALL (f: (surjective?[D, R])), (g: (inverse?(f))): injective?(g)
surjective_inverse_alt: LEMMA
FORALL (f: (surjective?[D, R])), (g: (inverse?(f))): g(r) = d => r = f(d)
comp_inverse_right_surj_alt: LEMMA
FORALL (f: (surjective?[D, R])), (g: (inverse?(f))): f(g(r)) = r
surjective_inverse_exists: LEMMA
FORALL (f: (surjective?[D, R])): EXISTS g: inverse?(g, f)
%%% Left-right inverses / bijective functions
left_right_bij: COROLLARY
FORALL f, g:
right_inverse?(g, f) AND left_inverse?(g, f) =>
bijective?(f) AND bijective?(g)
bij_left_right: COROLLARY
FORALL (f: (bijective?[D, R])), (g: (inverse?(f))):
right_inverse?(g, f) AND left_inverse?(g, f)
bij_inv_is_bij_alt: COROLLARY
FORALL (f: (bijective?[D, R])), (g: (inverse?(f))): bijective?(g)
bijective_inverse_alt: COROLLARY
FORALL (f: (bijective?[D, R])), (g: (inverse?(f))): g(r) = d IFF r = f(d)
comp_inverse_right_alt: COROLLARY
FORALL (f: (bijective?[D, R])), (g: (inverse?(f))): f(g(r)) = r
comp_inverse_left_alt: COROLLARY
FORALL (f: (bijective?[D, R])), (g: (inverse?(f))): g(f(d)) = d
bijective_inverse_exists: LEMMA
FORALL (f: (bijective?[D, R])): exists1(inverse?(f))
% The following are provided as support for discharging the
% assumption TCCs arising from the use of function_inverse_alt
exists_inv1: LEMMA
(EXISTS g: TRUE) IFF ((EXISTS (d: D): TRUE) OR (FORALL (r: R): FALSE))
exists_inv2: LEMMA
(EXISTS (f: (surjective?[D, R])): TRUE) =>
((EXISTS (d: D): TRUE) OR (FORALL (r: R): FALSE))
exists_inv3: LEMMA
(EXISTS f: NOT injective?(f)) =>
((EXISTS (d: D): TRUE) OR (FORALL (r: R): FALSE))
END function_inverse_def
% 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)
unique_bijective_inverse: JUDGEMENT
inverse(f:(bijective?[D,R]))(y) HAS_TYPE {x:D | f(x) = y}
bijective_inverse_is_bijective: JUDGEMENT
inverse(f:(bijective?[D,R])) HAS_TYPE (bijective?[R,D])
surjective_inverse: LEMMA
FORALL (f:(surjective?[D, R])):
inverse(f)(y) = x IMPLIES y = f(x)
inverse_surjective: LEMMA
FORALL (f:(surjective?[D, R])):
f(inverse(f)(y)) = y
injective_inverse: LEMMA
FORALL (f:(injective?[D, R])):
y = f(x) IMPLIES inverse(f)(y) = x
inverse_injective: LEMMA
FORALL (f:(injective?[D, R])):
inverse(f)(f(x)) = 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))
inv_inj_is_surj: JUDGEMENT
inverse(f: (injective?[D, R])) HAS_TYPE (surjective?[R, D])
inv_surj_is_inj: JUDGEMENT
inverse(f: (surjective?[D, R])) HAS_TYPE (injective?[R, D])
comp_inverse_right_surj: LEMMA
FORALL (f:(surjective?[D,R])): f(inverse(f)(y)) = y
comp_inverse_left_inj: LEMMA
FORALL (f:(injective?[D,R])): inverse(f)(f(x)) = x
comp_inverse_right: LEMMA
FORALL (f:(bijective?[D,R])): f(inverse(f)(y)) = y
comp_inverse_left: LEMMA
FORALL (f:(bijective?[D,R])): inverse(f)(f(x)) = x
END function_inverse
% This theory was provided by Jerry James
function_inverse_alt[D: TYPE, R: TYPE]: THEORY
BEGIN
ASSUMING
% The function_inverse theory, in effect, forces its users to prove the
% first disjunction; however, any of them give us the ability to define
% inverses. Note that the first two disjunctions are implied by each of
% the others. The axiom is expressed this way for the convenience of its
% users, who may have any one of these pieces of evidence of invertibility
% at hand.
inverse_types: ASSUMPTION
(EXISTS (d: D): TRUE) OR
(FORALL (r: R): FALSE)
ENDASSUMING
d: VAR D
r: VAR R
f: VAR [D -> R]
g: VAR [R -> D]
inverses(f): TYPE+ = (inverse?(f))
inverse_alt(f): inverses(f) = choose({g: inverses(f) | TRUE})
bijective_inverse_is_inverse_alt: COROLLARY
FORALL (f: (bijective?[D, R])), (g: inverses(f)): g = inverse_alt(f)
unique_bijective_inverse_alt: JUDGEMENT
inverse_alt(f: (bijective?[D,R]))(r) HAS_TYPE {d | f(d) = r}
bijective_inverse_alt_is_bijective: JUDGEMENT
inverse_alt(f: (bijective?[D,R])) HAS_TYPE (bijective?[R,D])
inv_inj_is_surj_alt: JUDGEMENT
inverse_alt(f: (injective?[D, R])) HAS_TYPE (surjective?[R, D])
inv_surj_is_inj_alt: JUDGEMENT
inverse_alt(f: (surjective?[D, R])) HAS_TYPE (injective?[R, D])
END function_inverse_alt
% 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: VAR D
y: VAR R
X, X1, X2: VAR set[D]
Y, Y1, Y2: VAR set[R]
fun_exists: LEMMA (EXISTS y: TRUE) OR (NOT EXISTS x: TRUE)
IMPLIES (EXISTS f: TRUE)
image(f, X): set[R] = {y: R | (EXISTS (x:(X)): y = f(x))}
image(f)(X): set[R] = image(f, X)
inverse_image(f, Y): set[D] = {x: D | member(f(x), Y)}
inverse_image(f)(Y): set[D] = inverse_image(f, 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]
R1: VAR PRED[[T1, T1]]
R2: VAR PRED[[T2, T2]]
R3: VAR PRED[[T3, T3]]
o(f2, f1)(x): T3 = f2(f1(x))
composition_injective: JUDGEMENT
o(f2: (injective?[T2, T3]), f1: (injective?[T1, T2]))
HAS_TYPE (injective?[T1, T3])
composition_surjective: JUDGEMENT
o(f2: (surjective?[T2, T3]), f1: (surjective?[T1, T2]))
HAS_TYPE (surjective?[T1, T3])
composition_bijective: JUDGEMENT
o(f2: (bijective?[T2, T3]), f1: (bijective?[T1, T2]))
HAS_TYPE (bijective?[T1, T3])
image_composition: LEMMA
image(f2, image(f1, X)) = image(f2 o f1, X)
preserves_composition: LEMMA
preserves(f1, R1, R2) AND preserves(f2, R2, R3)
IMPLIES preserves(f2 o f1, R1, R3)
inverts_composition1: LEMMA
preserves(f1, R1, R2) AND inverts(f2, R2, R3)
IMPLIES inverts(f2 o f1, R1, R3)
inverts_composition2: LEMMA
inverts(f1, R1, R2) AND preserves(f2, R2, R3)
IMPLIES inverts(f2 o f1, R1, R3)
END function_props
function_props_alt [T1, T2, T3: TYPE, R1: PRED[[T1, T1]],
R2: PRED[[T2, T2]], R3: PRED[[T3, T3]]]: THEORY
BEGIN
composition_preserves: JUDGEMENT
o(f2: (preserves[T2, T3, R2, R3]), f1: (preserves[T1, T2, R1, R2]))
HAS_TYPE (preserves[T1, T3, R1, R3])
composition_inverts1: JUDGEMENT
o(f2: (preserves[T2, T3, R2, R3]), f1: (inverts[T1, T2, R1, R2]))
HAS_TYPE (inverts[T1, T3, R1, R3])
composition_inverts2: JUDGEMENT
o(f2: (inverts[T2, T3, R2, R3]), f1: (preserves[T1, T2, R1, R2]))
HAS_TYPE (inverts[T1, T3, R1, R3])
END function_props_alt
% 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, S: VAR pred[[T1, T2]]
x: VAR T1
y: VAR T2
X: VAR set[T1]
Y: VAR set[T2]
domain?(R)(x: T1): bool = EXISTS (y: T2): R(x, y)
range?(R)(y: T2): bool = EXISTS (x: T1): R(x, y)
domain(R): TYPE = {x: T1 | EXISTS (y: T2): R(x, y)}
range(R): TYPE = {y: T2 | EXISTS (x: T1): R(x, y)}
rinverse(R)(y, x): bool = R(x, y)
rcomplement(R)(x, y): bool = NOT R(x, y)
runion(R, S)(x, y): bool = R(x, y) OR S(x, y)
rintersection(R, S)(x, y): bool = R(x, y) AND S(x, y)
image(R, X): set[T2] = {y: T2 | EXISTS (x: (X)): R(x, y)}
image(R)(X): set[T2] = image(R, X)
preimage(R, Y): set[T1] = {x: T1 | EXISTS (y: (Y)): R(x, y)}
preimage(R)(Y): set[T1] = preimage(R, Y)
postcondition(R, X): set[T2] = {y: T2 | EXISTS (x: (X)): R(x, y)}
postcondition(R)(X): set[T2] = postcondition(R, X)
precondition(R, Y): set[T1] = {x: T1 | FORALL (y: T2 | R(x, y)): Y(y)}
precondition(R)(Y): set[T1] = precondition(R, 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))
total?(R): bool = FORALL (x: T1): EXISTS (y: T2): R(x, y)
onto?(R): bool = FORALL (y: T2): EXISTS (x: T1): R(x, y)
END relation_defs
% relation_props
relation_props [T1, T2, T3: TYPE]: THEORY
BEGIN
R1: VAR pred[[T1, T2]]
R2: VAR pred[[T2, T3]]
x: VAR T1
y: VAR T2
z: VAR T3
o(R1, R2)(x, z): bool = EXISTS y: R1(x, y) AND R2(y, z)
total_composition: LEMMA total?(R1) & total?(R2) => total?(R1 o R2)
onto_composition: LEMMA onto?(R1) & onto?(R2) => onto?(R1 o R2)
composition_total: JUDGEMENT
o(R1: (total?[T1, T2]), R2: (total?[T2, T3])) HAS_TYPE (total?[T1, T3])
composition_onto: JUDGEMENT
o(R1: (onto?[T1, T2]), R2: (onto?[T2, T3])) HAS_TYPE (onto?[T1, T3])
END relation_props
relation_props2 [T1, T2, T3, T4: TYPE]: THEORY
BEGIN
R1: VAR pred[[T1, T2]]
R2: VAR pred[[T2, T3]]
R3: VAR pred[[T3, T4]]
assoc: LEMMA (R1 o R2) o R3 = R1 o (R2 o R3)
END relation_props2
%-------------------------------------------------------------------------
%
% Properties of converses of relations on a single type.
%
% ---------------------------------------------------------------------
% Author: Jerry James (jamesj@acm.org), University of Kansas
%
%-------------------------------------------------------------------------
relation_converse_props[T: TYPE]: THEORY
BEGIN
reflexive_converse: JUDGEMENT
converse(R: (reflexive?[T])) HAS_TYPE (reflexive?[T])
irreflexive_converse: JUDGEMENT
converse(R: (irreflexive?[T])) HAS_TYPE (irreflexive?[T])
symmetric_converse: JUDGEMENT
converse(R: (symmetric?[T])) HAS_TYPE (symmetric?[T])
antisymmetric_converse: JUDGEMENT
converse(R: (antisymmetric?[T])) HAS_TYPE (antisymmetric?[T])
connected_converse: JUDGEMENT
converse(R: (connected?[T])) HAS_TYPE (connected?[T])
transitive_converse: JUDGEMENT
converse(R: (transitive?[T])) HAS_TYPE (transitive?[T])
equivalence_converse: JUDGEMENT
converse(R: (equivalence?[T])) HAS_TYPE (equivalence?[T])
preorder_converse: JUDGEMENT
converse(R: (preorder?[T])) HAS_TYPE (preorder?[T])
partial_order_converse: JUDGEMENT
converse(R: (partial_order?[T])) HAS_TYPE (partial_order?[T])
strict_order_converse: JUDGEMENT
converse(R: (strict_order?[T])) HAS_TYPE (strict_order?[T])
dichotomous_converse: JUDGEMENT
converse(R: (dichotomous?[T])) HAS_TYPE (dichotomous?[T])
total_order_converse: JUDGEMENT
converse(R: (total_order?[T])) HAS_TYPE (total_order?[T])
trichotomous_converse: JUDGEMENT
converse(R: (trichotomous?[T])) HAS_TYPE (trichotomous?[T])
strict_total_order_converse: JUDGEMENT
converse(R: (strict_total_order?[T])) HAS_TYPE (strict_total_order?[T])
END relation_converse_props
indexed_sets[index, T: TYPE]: THEORY
BEGIN
i: VAR index
x: VAR T
A, B: VAR [index -> set[T]]
S: VAR set[T]
IUnion(A): set[T] = {x | EXISTS i: A(i)(x)}
IIntersection(A): set[T] = {x | FORALL i: A(i)(x)}
IUnion_Union: LEMMA
IUnion(A) = Union(image(A)(fullset[index]))
IIntersection_Intersection: LEMMA
IIntersection(A) = Intersection(image(A)(fullset[index]))
IUnion_union: LEMMA
IUnion(LAMBDA i: union(A(i), B(i))) = union(IUnion(A), IUnion(B))
IIntersection_intersection: LEMMA
IIntersection(LAMBDA i: intersection(A(i), B(i)))
= intersection(IIntersection(A), IIntersection(B))
IUnion_intersection: LEMMA
IUnion(LAMBDA i: intersection(A(i), S))
= intersection(IUnion(A), S)
IIntersection_union: LEMMA
IIntersection(LAMBDA i: union(A(i), S))
= union(IIntersection(A), S)
END indexed_sets
% 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.
% Its primary purpose is to provide a way to extend the reals, for
% example, the extended reals can be declared as a subtype of number that
% contains all the reals and the points at infinity.
numbers: THEORY
BEGIN
number: NONEMPTY_TYPE
END numbers
% number-fields provides the field axioms. This allows development of,
% for example, complex numbers or nonstandard reals as subtypes, without
% having to extend the field operators. Extended reals are not a subtype
% of number_field, as division by zero is allowed in the extended reals.
% Note that order relations are not defined here.
number_fields: THEORY
BEGIN
number_field: NONEMPTY_TYPE FROM number
numfield: NONEMPTY_TYPE = number_field
number_field?(n: number): bool = number_field_pred(n)
% The following declarations, if they could be expanded, are built in to
% the typechecker and prover:
% 0, 1, 2, ... : number_field
% AXIOM 0 /= 1 AND 0 /= 2 AND 1 /= 2 AND ...
nonzero_number: NONEMPTY_TYPE = {r: number_field | r /= 0} CONTAINING 1
nznum: NONEMPTY_TYPE = nonzero_number
+, -, *: [numfield, numfield -> numfield]
/: [numfield, nznum -> numfield]
-: [numfield -> numfield]
% Field Axioms - these are not provable using the decision
% procedures, as the operators are translated to uninterpreted
% functions, so that x * x = -1 is consistent. When the
% arguments are (a subtype of) real, then the translation is to
% interpreted symbols.
x, y, z: VAR numfield
n0x: VAR nznum
commutative_add : POSTULATE x + y = y + x
associative_add : POSTULATE x + (y + z) = (x + y) + z
identity_add : POSTULATE x + 0 = x
inverse_add : AXIOM x + -x = 0
minus_add : AXIOM x - y = x + -y
commutative_mult: AXIOM x * y = y * x
associative_mult: AXIOM x * (y * z) = (x * y) * z
identity_mult : AXIOM 1 * x = x
inverse_mult : AXIOM n0x * (1/n0x) = 1
div_def : AXIOM y/n0x = y * (1/n0x)
distributive : POSTULATE x * (y + z) = (x * y) + (x * z)
END number_fields
% reals defines the real numbers as an uninterpreted subtype of number.
% Though not explicitly specified, all numeric constants are known to be
% of type real (hence 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, and leads to
% unnecessary case splits.
reals: THEORY
BEGIN
real: NONEMPTY_TYPE FROM number_field;
ℝ: TYPE = real;
real?(n:number): bool = number_field_pred(n) AND real_pred(n)
% The following declarations, if they could be expanded, are built in to
% the typechecker:
% 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
% nzreal_is_nznum: JUDGEMENT nonzero_real SUBTYPE_OF nonzero_number
x, y: VAR real
n0z: VAR nzreal
closed_plus: AXIOM real_pred(x + y)
closed_minus: AXIOM real_pred(x - y)
closed_times: AXIOM real_pred(x * y)
closed_divides: AXIOM real_pred(x / n0z)
closed_neg: AXIOM real_pred(-x)
real_plus_real_is_real: JUDGEMENT +(x,y) HAS_TYPE real
real_minus_real_is_real: JUDGEMENT -(x,y) HAS_TYPE real
real_times_real_is_real: JUDGEMENT *(x,y) HAS_TYPE real
real_div_nzreal_is_real: JUDGEMENT /(x,n0z) HAS_TYPE real
minus_real_is_real: JUDGEMENT -(x) HAS_TYPE 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. These axioms were taken from
% Royden's "Real Analysis" pp.29-31
real_axioms: THEORY
BEGIN
x, y, z: VAR real
n0x: VAR nzreal
% Field Axioms are now in number_fields
% 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 defined in bounded_reals
END real_axioms
bounded_real_defs: THEORY
BEGIN
x, y: VAR real
% Completeness Axiom
S: VAR (nonempty?[real])
upper_bound?(x, S): bool = FORALL (s: (S)): s <= x
upper_bound?(S)(x): bool = upper_bound?(x, S)
lower_bound?(x, S): bool = FORALL (s: (S)): x <= s
lower_bound?(S)(x): bool = lower_bound?(x, S)
least_upper_bound?(x, S): bool =
upper_bound?(x, S) AND
FORALL y: upper_bound?(y, S) IMPLIES (x <= y)
least_upper_bound?(S)(x): bool = least_upper_bound?(x, S)
greatest_lower_bound?(x, S): bool =
lower_bound?(x, S) AND
FORALL y: lower_bound?(y, S) IMPLIES (y <= x)
greatest_lower_bound?(S)(x): bool = greatest_lower_bound?(x, S)
real_complete: AXIOM
FORALL S:
(EXISTS y: upper_bound?(y, S)) IMPLIES
(EXISTS y: least_upper_bound?(y, S))
real_lower_complete: LEMMA
FORALL S:
(EXISTS y: lower_bound?(y, S)) IMPLIES
(EXISTS x: greatest_lower_bound?(x, S))
% lub and glb
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)
END bounded_real_defs
bounded_real_defs_alt [S: (nonempty?[real])]: THEORY
BEGIN
x: VAR real
upper_bound?: [real -> bool] = upper_bound?(S)
lower_bound?: [real -> bool] = lower_bound?(S)
least_upper_bound?: [real -> bool] = least_upper_bound?(S)
greatest_lower_bound?: [real -> bool] = greatest_lower_bound?(S)
lub_is_upper_bound: JUDGEMENT
(least_upper_bound?) SUBTYPE_OF (upper_bound?)
glb_is_lower_bound: JUDGEMENT
(greatest_lower_bound?) SUBTYPE_OF (lower_bound?)
END bounded_real_defs_alt
% 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
nnreal: TYPE = nonneg_real
npreal: TYPE = nonpos_real
posreal_is_nzreal: JUDGEMENT posreal SUBTYPE_OF nzreal
negreal_is_nzreal: JUDGEMENT negreal SUBTYPE_OF nzreal
nzx, nzy: VAR nzreal
px, py: VAR posreal
nx, ny: VAR negreal
nnx, nny: VAR nonneg_real
npx, npy: VAR nonpos_real
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
nzreal_times_nzreal_is_nzreal: JUDGEMENT *(nzx, nzy) HAS_TYPE nzreal
nzreal_div_nzreal_is_nzreal: JUDGEMENT /(nzx, nzy) HAS_TYPE nzreal
minus_nzreal_is_nzreal: JUDGEMENT -(nzx) HAS_TYPE nzreal
nnreal_plus_nnreal_is_nnreal: JUDGEMENT +(nnx, nny) HAS_TYPE nnreal
nnreal_times_nnreal_is_nnreal: JUDGEMENT *(nnx, nny) HAS_TYPE nnreal
nnreal_div_posreal_is_nnreal: JUDGEMENT /(nnx, py) HAS_TYPE nnreal
nnreal_div_negreal_is_npreal: JUDGEMENT /(nnx, ny) HAS_TYPE npreal
npreal_plus_npreal_is_npreal: JUDGEMENT +(npx, npy) HAS_TYPE npreal
npreal_times_npreal_is_nnreal: JUDGEMENT *(npx, npy) HAS_TYPE nnreal
npreal_div_posreal_is_npreal: JUDGEMENT /(npx, py) HAS_TYPE npreal
npreal_div_negreal_is_nnreal: JUDGEMENT /(npx, ny) HAS_TYPE nnreal
posreal_plus_nnreal_is_posreal: JUDGEMENT +(px, nny) HAS_TYPE posreal
nnreal_plus_posreal_is_posreal: JUDGEMENT +(nnx, py) HAS_TYPE posreal
posreal_times_posreal_is_posreal: JUDGEMENT *(px, py) HAS_TYPE posreal
posreal_div_posreal_is_posreal: JUDGEMENT /(px, py) HAS_TYPE posreal
negreal_plus_negreal_is_negreal: JUDGEMENT +(nx, ny) HAS_TYPE negreal
negreal_times_negreal_is_posreal: JUDGEMENT *(nx, ny) HAS_TYPE posreal
negreal_div_negreal_is_posreal: JUDGEMENT /(nx, ny) HAS_TYPE 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 =
number_field_pred(n) AND 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
% nzrat_is_nzreal: 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)
rat_plus_rat_is_rat: JUDGEMENT +(x,y) HAS_TYPE rat
rat_minus_rat_is_rat: JUDGEMENT -(x,y) HAS_TYPE rat
rat_times_rat_is_rat: JUDGEMENT *(x,y) HAS_TYPE rat
rat_div_nzrat_is_rat: JUDGEMENT /(x,n0z) HAS_TYPE rat
minus_rat_is_rat: JUDGEMENT -(x) HAS_TYPE 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
nnrat: NONEMPTY_TYPE = nonneg_rat
nprat: NONEMPTY_TYPE = nonpos_rat
nnx, nny: VAR nonneg_rat
npx, npy: VAR nonpos_rat
px, py: VAR posrat
nx, ny: VAR negrat
n0x, n0y: VAR nzrat
% nnrat_is_nnreal: JUDGEMENT nonneg_rat SUBTYPE_OF nonneg_real
% nprat_is_npreal: JUDGEMENT nonpos_rat SUBTYPE_OF nonpos_real
% posrat_is_posreal: JUDGEMENT posrat SUBTYPE_OF posreal
% negrat_is_negreal: JUDGEMENT negrat SUBTYPE_OF negreal
posrat_is_nzrat: JUDGEMENT posrat SUBTYPE_OF nzrat
negrat_is_nzrat: JUDGEMENT negrat SUBTYPE_OF nzrat
nzrat_times_nzrat_is_nzrat: JUDGEMENT *(n0x, n0y) HAS_TYPE nzrat
nzrat_div_nzrat_is_nzrat: JUDGEMENT /(n0x, n0y) HAS_TYPE nzrat
minus_nzrat_is_nzrat: JUDGEMENT -(n0x) HAS_TYPE nzrat
nnrat_plus_nnrat_is_nnrat: JUDGEMENT +(nnx, nny) HAS_TYPE nonneg_rat
nnrat_times_nnrat_is_nnrat: JUDGEMENT *(nnx, nny) HAS_TYPE nonneg_rat
nnrat_div_posrat_is_nnrat: JUDGEMENT /(nnx, py) HAS_TYPE nonneg_rat
nnrrat_div_negrat_is_nprat: JUDGEMENT /(nnx, ny) HAS_TYPE nprat
nprat_plus_nprat_is_nprat: JUDGEMENT +(npx, npy) HAS_TYPE nprat
nprat_times_nprat_is_nnrat: JUDGEMENT *(npx, npy) HAS_TYPE nnrat
nprat_div_posrat_is_nprat: JUDGEMENT /(npx, py) HAS_TYPE nprat
nprat_div_negrat_is_nnrat: JUDGEMENT /(npx, ny) HAS_TYPE nnrat
posrat_plus_nnrat_is_posrat: JUDGEMENT +(px, nny) HAS_TYPE posrat
nnrat_plus_posrat_is_posrat: JUDGEMENT +(nnx, py) HAS_TYPE posrat
posrat_times_posrat_is_posrat: JUDGEMENT *(px, py) HAS_TYPE posrat
posrat_div_posrat_is_posrat: JUDGEMENT /(px, py) HAS_TYPE posrat
negrat_plus_negrat_is_negrat: JUDGEMENT +(nx, ny) HAS_TYPE negrat
negrat_times_negrat_is_posrat: JUDGEMENT *(nx, ny) HAS_TYPE posrat
negrat_div_negrat_is_posrat: JUDGEMENT /(nx, ny) HAS_TYPE 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 =
number_field_pred(n) AND 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
% nzint_is_nzrat: JUDGEMENT nonzero_integer SUBTYPE_OF nonzero_rational
i, j: VAR int
n0i, n0j: VAR nzint
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)
upfrom(i): NONEMPTY_TYPE = {s: int | s >= i} CONTAINING i
above(i): NONEMPTY_TYPE = {s: int | s > i} CONTAINING i + 1
int_plus_int_is_int: JUDGEMENT +(i,j) HAS_TYPE int
int_minus_int_is_int: JUDGEMENT -(i,j) HAS_TYPE int
int_times_int_is_int: JUDGEMENT *(i,j) HAS_TYPE int
minus_int_is_int: JUDGEMENT -(i) HAS_TYPE int
minus_nzint_is_nzint: JUDGEMENT -(n0i) HAS_TYPE nzint
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
nni, nnj: VAR nonneg_int
npi, npj: VAR nonpos_int
pi, pj: VAR posint
ni, nj: VAR negint
% Built in:
% JUDGEMENT 1, 2, 3, ... HAS_TYPE posint
% nnint_is_nnrat: JUDGEMENT nonneg_int SUBTYPE_OF nonneg_rat
% npint_is_nprat: JUDGEMENT nonpos_int SUBTYPE_OF nonpos_rat
% posint_is_posrat: JUDGEMENT posint SUBTYPE_OF posrat
% negint_is_negrat: JUDGEMENT negint SUBTYPE_OF negrat
posint_is_nzint: JUDGEMENT posint SUBTYPE_OF nzint
negint_is_nzint: JUDGEMENT negint SUBTYPE_OF nzint
nzint_times_nzint_is_nzint: JUDGEMENT *(n0i, n0j) HAS_TYPE nzint
nnint_plus_nnint_is_nnint: JUDGEMENT +(nni, nnj) HAS_TYPE nonneg_int
nnint_times_nnint_is_nnint: JUDGEMENT *(nni, nnj) HAS_TYPE nonneg_int
npint_plus_npint_is_npint: JUDGEMENT +(npi, npj) HAS_TYPE nonpos_int
npint_times_npint_is_nnint: JUDGEMENT *(npi, npj) HAS_TYPE nonneg_int
posint_plus_nnint_is_posint: JUDGEMENT +(pi, nnj) HAS_TYPE posint
nnint_plus_posint_is_posint: JUDGEMENT +(nni, pj) HAS_TYPE posint
posint_times_posint_is_posint: JUDGEMENT *(pi, pj) HAS_TYPE posint
negint_plus_negint_is_negint: JUDGEMENT +(ni, nj) HAS_TYPE negint
negint_times_negint_is_posint: JUDGEMENT *(ni, nj) HAS_TYPE posint
% Note: subrange may be an empty type
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
% The following declarations, if they could be expanded, are built in to
% the typechecker:
% JUDGEMENT 0, 2, 4, ... HAS_TYPE even_int
% JUDGEMENT 1, 3, 5, ... HAS_TYPE odd_int
e1, e2: VAR even_int
o1, o2: VAR odd_int
odd_is_nzint: JUDGEMENT odd_int SUBTYPE_OF nzint
even_plus_even_is_even: JUDGEMENT +(e1,e2) HAS_TYPE even_int
even_minus_even_is_even: JUDGEMENT -(e1,e2) HAS_TYPE even_int
odd_plus_odd_is_even: JUDGEMENT +(o1,o2) HAS_TYPE even_int
odd_minus_odd_is_even: JUDGEMENT -(o1,o2) HAS_TYPE even_int
odd_plus_even_is_odd: JUDGEMENT +(o1,e2) HAS_TYPE odd_int
odd_minus_even_is_odd: JUDGEMENT -(o1,e2) HAS_TYPE odd_int
even_plus_odd_is_odd: JUDGEMENT +(e1,o2) HAS_TYPE odd_int
even_minus_odd_is_odd: JUDGEMENT -(e1,o2) HAS_TYPE odd_int
even_times_int_is_even: JUDGEMENT *(e1,i) HAS_TYPE even_int
int_times_even_is_even: JUDGEMENT *(i,e2) HAS_TYPE even_int
odd_times_odd_is_odd: JUDGEMENT *(o1,o2) HAS_TYPE odd_int
minus_even_is_even: JUDGEMENT -(e1) HAS_TYPE even_int
minus_odd_is_odd: JUDGEMENT -(o1) HAS_TYPE odd_int
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 successor and predecessor functions are defined here.
naturalnumbers: THEORY
BEGIN
naturalnumber: TYPE = nonneg_int
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
n: VAR posnat
upfrom_nat_is_nat: JUDGEMENT upfrom(i) SUBTYPE_OF nat
upfrom_posnat_is_posnat: JUDGEMENT upfrom(n) SUBTYPE_OF posnat
above_nat_is_posnat: JUDGEMENT above(i) SUBTYPE_OF posnat
subrange_nat_is_nat: JUDGEMENT subrange(i,j) SUBTYPE_OF nat
subrange_posnat_is_posnat: JUDGEMENT subrange(n,j) SUBTYPE_OF posnat
upto(i): NONEMPTY_TYPE = {s: nat | s <= i} CONTAINING i
below(i): TYPE = {s: nat | s < i} % may be empty
% nat_plus_nat_is_nat: JUDGEMENT +(i,j) HAS_TYPE nat
% nat_times_nat_is_nat: JUDGEMENT *(i,j) HAS_TYPE 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))
% Provide some intersection types, so that judgements can find a minimal type
even_nat: NONEMPTY_TYPE = {i| even?(i)} CONTAINING 0
even_posnat: NONEMPTY_TYPE = {n| even?(n)} CONTAINING 2
odd_posnat: NONEMPTY_TYPE = {n| odd?(n)} CONTAINING 1
even_negint: NONEMPTY_TYPE = {n: negint | even?(n)} CONTAINING -2
odd_negint: NONEMPTY_TYPE = {n: negint | odd?(n)} CONTAINING -1
% This seems out of place - it is here so we can prove it by induction
x: VAR int
even_or_odd: THEOREM even?(x) IFF NOT odd?(x)
odd_iff_not_even: LEMMA odd?(x) IFF NOT even?(x)
even_iff_not_odd: LEMMA even?(x) IFF NOT odd?(x)
odd_or_even_int: LEMMA odd?(x) OR even?(x)
odd_iff_even_succ: LEMMA odd?(x) IFF even?(x+1)
even_iff_odd_succ: LEMMA even?(x) IFF odd?(x+1)
even_plus1: LEMMA even?(x) IFF NOT even?(x+1)
odd_plus1: LEMMA odd?(x) IFF NOT odd?(x+1)
even_div2: LEMMA even?(x) IMPLIES integer_pred(x/2)
odd_div2: LEMMA odd?(x) IMPLIES integer_pred((x-1)/2)
END naturalnumbers
min_nat[T: TYPE FROM nat]: THEORY
BEGIN
S: VAR (nonempty?[T])
a, x: VAR T
min(S): {a | S(a) AND (FORALL x: S(x) IMPLIES a <= x)}
minimum?(a, S) : bool = S(a) AND (FORALL x: S(x) IMPLIES a <= x)
min_def : LEMMA
FORALL (S: (nonempty?[T])) : min(S) = a IFF minimum?(a, S)
END min_nat
% 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
sgn(m): int = IF m >= 0 THEN 1 ELSE -1 ENDIF
abs(m): {n: nonneg_real | n >= m AND n >= -m}
= IF m < 0 THEN -m ELSE m ENDIF
nonzero_abs_is_pos: JUDGEMENT abs(x:nzreal) HAS_TYPE {y: posreal | y >= x}
rat_abs_is_nonneg: JUDGEMENT abs(q:rat) HAS_TYPE {r: nonneg_rat | r >= q}
nzrat_abs_is_pos: JUDGEMENT abs(q:nzrat) HAS_TYPE {r: posrat | r >= q}
int_abs_is_nonneg: JUDGEMENT abs(i:int) HAS_TYPE {j: nonneg_int | j >= i}
nzint_abs_is_pos: JUDGEMENT abs(i:nzint) HAS_TYPE {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
nzreal_max: JUDGEMENT
max(x,y:nzreal) HAS_TYPE {z: nzreal | z >= x AND z >= y}
nzreal_min: JUDGEMENT
min(x,y:nzreal) HAS_TYPE {z: nzreal | z <= x AND z <= y}
nonneg_real_max: JUDGEMENT
max(x,y:nonneg_real) HAS_TYPE {z: nonneg_real | z >= x AND z >= y}
nonneg_real_min: JUDGEMENT
min(x,y:nonneg_real) HAS_TYPE {z: nonneg_real | z <= x AND z <= y}
posreal_max: JUDGEMENT
max(x,y:posreal) HAS_TYPE {z: posreal | z >= x AND z >= y}
posreal_min: JUDGEMENT
min(x,y:posreal) HAS_TYPE {z: posreal | z <= x AND z <= y}
% rat subtype judgements
rat_max: JUDGEMENT
max(q,r:rat) HAS_TYPE {s: rat | s >= q AND s >= r}
rat_min: JUDGEMENT
min(q,r:rat) HAS_TYPE {s: rat | s <= q AND s <= r}
nzrat_max: JUDGEMENT
max(q,r:nzrat) HAS_TYPE {s: nzrat | s >= q AND s >= r}
nzrat_min: JUDGEMENT
min(q,r:nzrat) HAS_TYPE {s: nzrat | s <= q AND s <= r}
nonneg_rat_max: JUDGEMENT
max(q,r:nonneg_rat) HAS_TYPE {s: nonneg_rat | s >= q AND s >= r}
nonneg_rat_min: JUDGEMENT
min(q,r:nonneg_rat) HAS_TYPE {s: nonneg_rat | s <= q AND s <= r}
posrat_max: JUDGEMENT
max(q,r:posrat) HAS_TYPE {s: posrat | s >= q AND s >= r}
posrat_min: JUDGEMENT
min(q,r:posrat) HAS_TYPE {s: posrat | s <= q AND s <= r}
% int subtype judgements
int_max: JUDGEMENT
max(i,j:int) HAS_TYPE {k: int | i <= k AND j <= k}
int_min: JUDGEMENT
min(i,j:int) HAS_TYPE {k: int | k <= i AND k <= j}
nzint_max: JUDGEMENT
max(i,j:nzint) HAS_TYPE {k: nzint | i <= k AND j <= k}
nzint_min: JUDGEMENT
min(i,j:nzint) HAS_TYPE {k: nzint | k <= i AND k <= j}
nat_max: JUDGEMENT
max(i,j:nat) HAS_TYPE {k: nat | i <= k AND j <= k}
nat_min: JUDGEMENT
min(i,j:nat) HAS_TYPE {k: nat | k <= i AND k <= j}
posint_max: JUDGEMENT
max(i,j:posint) HAS_TYPE {k: posint | i <= k AND j <= k}
posint_min: JUDGEMENT
min(i,j:posint) HAS_TYPE {k: posint | k <= i AND k <= j}
% Useful facts about maximum and minimum of two reals
%
% Author : Alfons Geser, National Institute of Aerospace
% Date : Aug 26, 2003
a,b,c : VAR real
min_le : LEMMA min(a,b) <= c IFF (a <= c OR b <= c)
min_lt : LEMMA min(a,b) < c IFF (a < c OR b < c)
min_ge : LEMMA min(a,b) >= c IFF (a >= c AND b >= c)
min_gt : LEMMA min(a,b) > c IFF (a > c AND b > c)
le_min : LEMMA a <= min(b,c) IFF (a <= b AND a <= c)
lt_min : LEMMA a < min(b,c) IFF (a < b AND a < c)
ge_min : LEMMA a >= min(b,c) IFF (a >= b OR a >= c)
gt_min : LEMMA a > min(b,c) IFF (a > b OR a > c)
max_le : LEMMA max(a,b) <= c IFF (a <= c AND b <= c)
max_lt : LEMMA max(a,b) < c IFF (a < c AND b < c)
max_ge : LEMMA max(a,b) >= c IFF (a >= c OR b >= c)
max_gt : LEMMA max(a,b) > c IFF (a > c OR b > c)
le_max : LEMMA a <= max(b,c) IFF (a <= b OR a <= c)
lt_max : LEMMA a < max(b,c) IFF (a < b OR a < c)
ge_max : LEMMA a >= max(b,c) IFF (a >= b AND a >= c)
gt_max : LEMMA a > max(b,c) IFF (a > b AND a > c)
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
div_cancel4: LEMMA x = y/n0z IFF x * n0z = y
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_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_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_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_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_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_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)
% 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_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_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_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_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_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_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 >=
total_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
sqrt_1_lt: LEMMA x * x < 1 IMPLIES abs(x) < 1
sqrt_1_le: LEMMA x * x <= 1 IMPLIES abs(x) <= 1
idem_mult: LEMMA x * x = x IFF x = 0 OR x = 1
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_div: LEMMA abs(x / n0y) = abs(x) / abs(n0y)
abs_abs: LEMMA abs(abs(x)) = abs(x)
abs_square: LEMMA abs(x * x) = x * x
abs_limits: LEMMA -(abs(x) + abs(y)) <= x + y AND x + y <= abs(x) + abs(y)
% The axiom of Archimedes
axiom_of_archimedes: LEMMA
FORALL (x: real): EXISTS (i: int): x < i
archimedean: LEMMA
FORALL (px: posreal): EXISTS (n: posnat): 1/n < px
real_lt_is_strict_total_order: JUDGEMENT
< HAS_TYPE (strict_total_order?[real])
real_le_is_total_order: JUDGEMENT <= HAS_TYPE (total_order?[real])
real_gt_is_strict_total_order: JUDGEMENT
> HAS_TYPE (strict_total_order?[real])
real_ge_is_total_order: JUDGEMENT >= HAS_TYPE (total_order?[real])
END real_props
%% Contains extra properties about reals needed by the formula
%% manipulation strategies in package Manip. Can be seen as an
%% extension of the real_props theory in the prelude.
extra_real_props: THEORY
BEGIN
%% Same variable declarations as real_props in the prelude:
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
%% Lemmas used to handle cases where a multiplier or divisor can be
%% either positive or negative.
pos_neg_split: LEMMA EXISTS px, nx: n0x = px or n0x = nx
div_mult_pos_neg_lt1: LEMMA
z/n0y < x IFF IF n0y > 0 THEN z < x * n0y ELSE x * n0y < z ENDIF
div_mult_pos_neg_lt2: LEMMA
x < z/n0y IFF IF n0y > 0 THEN x * n0y < z ELSE z < x * n0y ENDIF
div_mult_pos_neg_le1: LEMMA
z/n0y <= x IFF IF n0y > 0 THEN z <= x * n0y ELSE x * n0y <= z ENDIF
div_mult_pos_neg_le2: LEMMA
x <= z/n0y IFF IF n0y > 0 THEN x * n0y <= z ELSE z <= x * n0y ENDIF
div_mult_pos_neg_gt1: LEMMA
z/n0y > x IFF IF n0y > 0 THEN z > x * n0y ELSE x * n0y > z ENDIF
div_mult_pos_neg_gt2: LEMMA
x > z/n0y IFF IF n0y > 0 THEN x * n0y > z ELSE z > x * n0y ENDIF
div_mult_pos_neg_ge1: LEMMA
z/n0y >= x IFF IF n0y > 0 THEN z >= x * n0y ELSE x * n0y >= z ENDIF
div_mult_pos_neg_ge2: LEMMA
x >= z/n0y IFF IF n0y > 0 THEN x * n0y >= z ELSE z >= x * n0y ENDIF
both_sides_times_pos_neg_lt1: LEMMA
IF n0z > 0 THEN x * n0z < y * n0z ELSE y * n0z < x * n0z ENDIF IFF x < y
both_sides_times_pos_neg_lt2: LEMMA
IF n0z > 0 THEN n0z * x < n0z * y ELSE n0z * y < n0z * x ENDIF IFF x < y
both_sides_times_pos_neg_le1: LEMMA
IF n0z > 0 THEN x * n0z <= y * n0z ELSE y * n0z <= x * n0z ENDIF IFF x <= y
both_sides_times_pos_neg_le2: LEMMA
IF n0z > 0 THEN n0z * x <= n0z * y ELSE n0z * y <= n0z * x ENDIF IFF x <= y
both_sides_times_pos_neg_gt1: LEMMA
IF n0z > 0 THEN x * n0z > y * n0z ELSE y * n0z > x * n0z ENDIF IFF x > y
both_sides_times_pos_neg_gt2: LEMMA
IF n0z > 0 THEN n0z * x > n0z * y ELSE n0z * y > n0z * x ENDIF IFF x > y
both_sides_times_pos_neg_ge1: LEMMA
IF n0z > 0 THEN x * n0z >= y * n0z ELSE y * n0z >= x * n0z ENDIF IFF x >= y
both_sides_times_pos_neg_ge2: LEMMA
IF n0z > 0 THEN n0z * x >= n0z * y ELSE n0z * y >= n0z * x ENDIF IFF x >= y
%% The naming scheme below follows that of the both_sides_div_+/-_R1/2/3
%% series in real_props as consistently as possible.
both_sides_div_pos_neg_lt1: LEMMA
IF n0z > 0 THEN x/n0z < y/n0z ELSE y/n0z < x/n0z ENDIF IFF x < y
both_sides_div_pos_neg_lt2: LEMMA
IF n0z > 0 THEN n0z/px < n0z/py ELSE n0z/py < n0z/px ENDIF IFF py < px
both_sides_div_pos_neg_lt3: LEMMA
IF n0z > 0 THEN n0z/nx < n0z/ny ELSE n0z/ny < n0z/nx ENDIF IFF ny < nx
both_sides_div_pos_neg_le1: LEMMA
IF n0z > 0 THEN x/n0z <= y/n0z ELSE y/n0z <= x/n0z ENDIF IFF x <= y
both_sides_div_pos_neg_le2: LEMMA
IF n0z > 0 THEN n0z/px <= n0z/py ELSE n0z/py <= n0z/px ENDIF IFF py <= px
both_sides_div_pos_neg_le3: LEMMA
IF n0z > 0 THEN n0z/nx <= n0z/ny ELSE n0z/ny <= n0z/nx ENDIF IFF ny <= nx
both_sides_div_pos_neg_gt1: LEMMA
IF n0z > 0 THEN x/n0z > y/n0z ELSE y/n0z > x/n0z ENDIF IFF x > y
both_sides_div_pos_neg_gt2: LEMMA
IF n0z > 0 THEN n0z/px > n0z/py ELSE n0z/py > n0z/px ENDIF IFF py > px
both_sides_div_pos_neg_gt3: LEMMA
IF n0z > 0 THEN n0z/nx > n0z/ny ELSE n0z/ny > n0z/nx ENDIF IFF ny > nx
both_sides_div_pos_neg_ge1: LEMMA
IF n0z > 0 THEN x/n0z >= y/n0z ELSE y/n0z >= x/n0z ENDIF IFF x >= y
both_sides_div_pos_neg_ge2: LEMMA
IF n0z > 0 THEN n0z/px >= n0z/py ELSE n0z/py >= n0z/px ENDIF IFF py >= px
both_sides_div_pos_neg_ge3: LEMMA
IF n0z > 0 THEN n0z/nx >= n0z/ny ELSE n0z/ny >= n0z/nx ENDIF IFF ny >= nx
%% Less restrictive lemmas used by strategy MULT-BY than the
%% both_sides_times series in real_props. Allows multiplier to be
%% zero in some cases. Variable z changed to w so it would
%% precede x,y during INST and make all lemmas consistent.
both_sides_times1_imp: LEMMA x = y IMPLIES x * w = y * w
both_sides_times2_imp: LEMMA x = y IMPLIES w * x = w * y
both_sides_times_pos_le1_imp: LEMMA x <= y IMPLIES x * nnw <= y * nnw
both_sides_times_pos_le2_imp: LEMMA x <= y IMPLIES nnw * x <= nnw * y
both_sides_times_neg_le1_imp: LEMMA y <= x IMPLIES x * npw <= y * npw
both_sides_times_neg_le2_imp: LEMMA y <= x IMPLIES npw * x <= npw * y
both_sides_times_pos_ge1_imp: LEMMA x >= y IMPLIES x * nnw >= y * nnw
both_sides_times_pos_ge2_imp: LEMMA x >= y IMPLIES nnw * x >= nnw * y
both_sides_times_neg_ge1_imp: LEMMA y >= x IMPLIES x * npw >= y * npw
both_sides_times_neg_ge2_imp: LEMMA y >= x IMPLIES npw * x >= npw * y
both_sides_times_pos_neg_le1_imp: LEMMA
x <= y IMPLIES IF w >= 0 THEN x * w <= y * w ELSE y * w <= x * w ENDIF
both_sides_times_pos_neg_le2_imp: LEMMA
x <= y IMPLIES IF w >= 0 THEN w * x <= w * y ELSE w * y <= w * x ENDIF
both_sides_times_pos_neg_ge1_imp: LEMMA
x >= y IMPLIES IF w >= 0 THEN x * w >= y * w ELSE y * w >= x * w ENDIF
both_sides_times_pos_neg_ge2_imp: LEMMA
x >= y IMPLIES IF w >= 0 THEN w * x >= w * y ELSE w * y >= w * x ENDIF
%% Additional lemmas needed to fill in gaps left by real_props.
zero_times4: LEMMA 0 = x * y IFF x = 0 OR y = 0
times_div_cancel1: LEMMA (n0z * x) / n0z = x
times_div_cancel2: LEMMA (x * n0z) / n0z = x
%% Replacements for real_props lemmas to correct inconsistent naming.
div_mult_pos_gt1: LEMMA z/py > x IFF z > x * py
div_mult_pos_gt2: LEMMA x > z/py IFF x * py > z
div_mult_neg_gt1: LEMMA z/ny > x IFF x * ny > z
div_mult_neg_gt2: LEMMA x > z/ny IFF z > x * ny
%% Transitivity lemmas for inequality reasoning. Normally unnecessary
%% but sometimes helpful for forcing case splits.
lt_cut: LEMMA x < y AND y < z IMPLIES x < z
le_cut: LEMMA x <= y AND y <= z IMPLIES x <= z
gt_cut: LEMMA x > y AND y > z IMPLIES x > z
ge_cut: LEMMA x >= y AND y >= z IMPLIES x >= z
%% Rules used to deduce inequalities on products of reals. These rules
%% stipulate only sufficient conditions for the inequalities to hold.
%% The most common and useful cases are included, although additional
%% cases might be desirable later.
le_times_le_any1: LEMMA
IF w >= 0 IFF x >= 0
THEN IF y >= 0 IFF z >= 0
THEN abs(w) <= abs(y) AND abs(x) <= abs(z)
ELSE (w = 0 OR x = 0) AND (y = 0 OR z = 0)
ENDIF
ELSE IF y >= 0 IFF z >= 0
THEN true
ELSE abs(w) >= abs(y) AND abs(x) >= abs(z)
ENDIF
ENDIF
IMPLIES w * x <= y * z
ge_times_ge_any1: LEMMA
IF y >= 0 IFF z >= 0
THEN IF w >= 0 IFF x >= 0
THEN abs(w) >= abs(y) AND abs(x) >= abs(z)
ELSE (w = 0 OR x = 0) AND (y = 0 OR z = 0)
ENDIF
ELSE IF w >= 0 IFF x >= 0
THEN true
ELSE abs(w) <= abs(y) AND abs(x) <= abs(z)
ENDIF
ENDIF
IMPLIES w * x >= y * z
lt_times_lt_any1: LEMMA
IF w = 0 OR x = 0
THEN 0 < y AND 0 < z OR y < 0 AND z < 0
ELSIF w > 0 IFF x > 0
THEN (y > 0 IFF z > 0) AND
(abs(w) <= abs(y) AND abs(x) < abs(z) OR
abs(w) < abs(y) AND abs(x) <= abs(z))
ELSIF y > 0 IFF z > 0
THEN true
ELSE abs(w) >= abs(y) AND abs(x) > abs(z) OR
abs(w) > abs(y) AND abs(x) >= abs(z)
ENDIF
IMPLIES w * x < y * z
gt_times_gt_any1: LEMMA
IF y = 0 OR z = 0
THEN 0 < w AND 0 < x OR w < 0 AND x < 0
ELSIF y > 0 IFF z > 0
THEN (w > 0 IFF x > 0) AND
(abs(w) >= abs(y) AND abs(x) > abs(z) OR
abs(w) > abs(y) AND abs(x) >= abs(z))
ELSIF w > 0 IFF x > 0
THEN true
ELSE abs(w) <= abs(y) AND abs(x) < abs(z) OR
abs(w) < abs(y) AND abs(x) <= abs(z)
ENDIF
IMPLIES w * x > y * z
%% Contrapositive forms of series R_times_R_any1. They stipulate
%% necessary conditions for the inequalities to hold.
le_times_le_any2: LEMMA
w * x <= y * z IMPLIES
IF y = 0 OR z = 0
THEN (0 >= w OR 0 >= x) AND (w >= 0 OR x >= 0)
ELSIF y > 0 IFF z > 0
THEN (w > 0 IFF x > 0) IMPLIES
(abs(w) < abs(y) OR abs(x) <= abs(z)) AND
(abs(w) <= abs(y) OR abs(x) < abs(z))
ELSE NOT (w > 0 IFF x > 0) AND
(abs(w) > abs(y) OR abs(x) >= abs(z)) AND
(abs(w) >= abs(y) OR abs(x) > abs(z))
ENDIF
ge_times_ge_any2: LEMMA
w * x >= y * z IMPLIES
IF w = 0 OR x = 0
THEN (0 >= y OR 0 >= z) AND (y >= 0 OR z >= 0)
ELSIF w > 0 IFF x > 0
THEN (y > 0 IFF z > 0) IMPLIES
(abs(w) > abs(y) OR abs(x) >= abs(z)) AND
(abs(w) >= abs(y) OR abs(x) > abs(z))
ELSE NOT (y > 0 IFF z > 0) AND
(abs(w) < abs(y) OR abs(x) <= abs(z)) AND
(abs(w) <= abs(y) OR abs(x) < abs(z))
ENDIF
lt_times_lt_any2: LEMMA
w * x < y * z IMPLIES
IF y >= 0 IFF z >= 0
THEN IF w >= 0 IFF x >= 0
THEN abs(w) < abs(y) OR abs(x) < abs(z)
ELSE (w /= 0 AND x /= 0) OR (y /= 0 AND z /= 0)
ENDIF
ELSE NOT (w >= 0 IFF x >= 0) AND
(abs(w) > abs(y) OR abs(x) > abs(z))
ENDIF
gt_times_gt_any2: LEMMA
w * x > y * z IMPLIES
IF w >= 0 IFF x >= 0
THEN IF y >= 0 IFF z >= 0
THEN abs(w) > abs(y) OR abs(x) > abs(z)
ELSE (w /= 0 AND x /= 0) OR (y /= 0 AND z /= 0)
ENDIF
ELSE NOT (y >= 0 IFF z >= 0) AND
(abs(w) < abs(y) OR abs(x) < abs(z))
ENDIF
END extra_real_props
%%% This file contains some simplification rules missing in real_props.
%%% Part of the Field package of Cesar Munoz
extra_tegies : THEORY
BEGIN
x,y : VAR real
n0z : VAR nzreal
neg_mult : LEMMA
-x*y = -(x*y)
mult_neg : LEMMA
x*-y = -(x*y)
neg_add : LEMMA
-x + y = y - x
add_neg : LEMMA
x + -y = x - y
neg_div : LEMMA
-x/n0z = -(x/n0z)
div_neg : LEMMA
x/-n0z = -(x/n0z)
one_times: LEMMA
1*x = x
neg_one_times: LEMMA
-1*x = -x
zero_div: LEMMA
0/n0z = 0
neg_neg: LEMMA
--x = x
END extra_tegies
% 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
p: VAR posnat
r: VAR rat
rational_pred_ax: AXIOM EXISTS i, n0j: r = i/n0j
rational_pred_ax2: LEMMA EXISTS i, p: r = i/p
density_positive : LEMMA
0 <= x AND x < y IMPLIES (EXISTS r: x < r AND r < y)
density: LEMMA 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, k: VAR int
n0j: VAR nzint
N: VAR (nonempty?[nat])
I: VAR (nonempty?[int])
integer_pred_ax: LEMMA EXISTS n: i = n OR i = -n
div_simple: LEMMA (EXISTS k: i = k*n0j) = integer_pred(i/n0j)
lub_nat: LEMMA
upper_bound?(m, N)
=> EXISTS (n:(N)): least_upper_bound?(n, N)
lub_int: LEMMA
upper_bound?(i, I)
=> EXISTS (j:(I)): least_upper_bound?(j, I)
glb_nat: LEMMA
EXISTS (n:(N)): greatest_lower_bound?(n, N)
glb_int: LEMMA
lower_bound?(i, I)
=> EXISTS (j:(I)): greatest_lower_bound?(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
py: VAR posreal
j: VAR nonzero_integer
i, k: 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)
nonneg_floor_is_nat: JUDGEMENT floor(x:nonneg_real) HAS_TYPE nat
nonneg_ceiling_is_nat: JUDGEMENT ceiling(x:nonneg_real) HAS_TYPE 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
floor_val: LEMMA i >= k*j AND i < (k+1)*j IMPLIES floor(i/j) = k
floor_small: LEMMA abs(i) < abs(j) IMPLIES
floor(i/j) = IF i/j >= 0 THEN 0 ELSE -1 ENDIF
floor_eq_0: LEMMA floor(x) = 0 IMPLIES x >= 0 AND x < 1
fractional_plus: LEMMA
fractional(x+y) = fractional(fractional(x) + fractional(y))
floor_div: LEMMA floor(x/py) = i IFF py*i <= x AND x < py*(i+1)
floor_0: LEMMA floor(x) = 0 IFF 0 <= x AND 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
q: VAR rat
nnq: VAR nonneg_rat
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;
nnreal_expt: JUDGEMENT expt(x:nnreal, n:nat) HAS_TYPE nnreal
posreal_expt: JUDGEMENT expt(x:posreal, n:nat) HAS_TYPE posreal
nzreal_expt: JUDGEMENT expt(x:nzreal, n:nat) HAS_TYPE nzreal
rat_expt: JUDGEMENT expt(x:rat, n:nat) HAS_TYPE rat
nnrat_expt: JUDGEMENT expt(x:nnrat, n:nat) HAS_TYPE nnrat
posrat_expt: JUDGEMENT expt(x:posrat, n:nat) HAS_TYPE posrat
int_expt: JUDGEMENT expt(x:int, n:nat) HAS_TYPE int
nat_expt: JUDGEMENT expt(x:nat, n:nat) HAS_TYPE nat
posnat_expt: JUDGEMENT expt(x:posnat, n:nat) HAS_TYPE posnat
^(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
nnreal_exp: JUDGEMENT ^(x:nnreal, i:int | x/=0 OR i>=0) HAS_TYPE nnreal
posreal_exp: JUDGEMENT ^(x:posreal, i:int) HAS_TYPE posreal
nzreal_exp: JUDGEMENT ^(x:nzreal, i:int) HAS_TYPE nzreal
rat_exp: JUDGEMENT ^(x:rat, i:int | x/=0 OR i>=0) HAS_TYPE rat
nnrat_exp: JUDGEMENT ^(x:nnrat, i:int | x/=0 OR i>=0) HAS_TYPE nnrat
posrat_exp: JUDGEMENT ^(x:posrat, i:int) HAS_TYPE posrat
int_exp: JUDGEMENT ^(x:int, n:nat) HAS_TYPE int
nat_exp: JUDGEMENT ^(x:nat, n:nat) HAS_TYPE nat
posint_exp: JUDGEMENT ^(x:posint, n:nat) HAS_TYPE 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
expt_of_mult: LEMMA expt(x * y, n) = expt(x, n) * expt(y, n)
expt_of_div: LEMMA expt(x / n0y, n) = expt(x, n) / expt(n0y, n)
expt_of_inv: LEMMA expt(1 / n0x, n) = 1 / expt(n0x, n)
expt_of_abs: LEMMA expt(abs(x), n) = abs(expt(x, n))
abs_of_expt_inv: LEMMA abs(1 / expt(n0x, n)) = 1 / expt(abs(n0x),n)
% Properties of ^
expt_x0: LEMMA x^0 = 1
expt_x1: LEMMA x^1 = x
expt_x2: LEMMA x^2 = x*x
expt_x3: LEMMA x^3 = x*x*x
expt_x4: LEMMA x^4 = x*x*x*x
expt_1i: LEMMA 1^i = 1
expt_eq_0: LEMMA x^pn = 0 IFF x = 0
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
mult_expt: LEMMA (n0x * n0y) ^i = n0x^i * n0y^i
div_expt : LEMMA (n0x / n0y)^i = n0x^i / n0y^i
inv_expt : LEMMA (1 / n0x)^i = 1 / n0x^i
abs_expt: LEMMA abs(n0x)^i = abs(n0x^i)
abs_hat_nat : LEMMA abs(x)^n = abs(x^n)
expt_minus1_abs: LEMMA abs((-1)^i) = 1
even_m1_pow: LEMMA even?(i) IMPLIES (-1)^i = 1
not_even_m1_pow: LEMMA NOT even?(i) IMPLIES (-1)^i = -1
expt_lt1_bound1: LEMMA expt(lt1x, n) <= 1
expt_lt1_bound2: LEMMA expt(lt1x, pn) < 1
expt_gt1_bound1: LEMMA 1 <= expt(gt1x, n)
expt_gt1_bound2: LEMMA 1 < expt(gt1x, pn)
large_expt: LEMMA 1 < px IMPLIES (FORALL py: EXISTS n: py < expt(px, n))
small_expt: LEMMA px < 1 IMPLIES (FORALL py: EXISTS n: expt(px, n) < py)
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
% Euclidean division courtesy of Bruno Dutertre
euclidean_division : THEORY
BEGIN
a, i : VAR nat
b : VAR posnat
n : VAR int
%-----------------------------------------------
% Type mod(b) = 0.. b-1
% (replace below[b] to reduce number of TCCs)
%-----------------------------------------------
mod(b) : NONEMPTY_TYPE = { i | i < b}
%-----------------------
% Euclidean division
%-----------------------
euclid_nat : LEMMA
EXISTS (q : nat), (r : mod(b)) : a = b * q + r
euclid_int : PROPOSITION
EXISTS (q : int), (r : mod(b)) : n = b * q + r
unique_quotient : PROPOSITION
FORALL (q1, q2 : int), (r1, r2 : mod(b)) :
b * q1 + r1 = b * q2 + r2 IMPLIES q1 = q2
unique_remainder : COROLLARY
FORALL (q1, q2 : int), (r1, r2 : mod(b)) :
b * q1 + r1 = b * q2 + r2 IMPLIES r1 = r2
unique_division : COROLLARY
FORALL (q1, q2 : int), (r1, r2 : mod(b)) :
b * q1 + r1 = b * q2 + r2 IMPLIES q1 = q2 AND r1 = r2
END euclidean_division
% Divisibility relation
% For integers and natural numbers
% Provided by Bruno Dutertre
divides : THEORY
BEGIN
n, m, l, x, y : VAR int
p, q : VAR nat
nz : VAR nzint
%--------------------
% Divides relation
%--------------------
divides(n, m): bool = EXISTS x : m = n * x
divides(n)(m): bool = divides(n, m)
mult_divides1: JUDGEMENT *(n, m) HAS_TYPE (divides(n))
mult_divides2: JUDGEMENT *(n, m) HAS_TYPE (divides(m))
%----------------
% Easy lemmas
%----------------
divides_sum : LEMMA
divides(x, n) AND divides(x, m) IMPLIES divides(x, n + m)
divides_diff : LEMMA
divides(x, n) AND divides(x, m) IMPLIES divides(x, n - m)
divides_opposite : LEMMA
divides(x, - n) IFF divides(x, n)
opposite_divides : LEMMA
divides(- x, n) IFF divides(x, n)
divides_prod1 : LEMMA
divides(x, n) IMPLIES divides(x, n * m)
divides_prod2 : LEMMA
divides(x, n) IMPLIES divides(x, m * n)
%---------------
% Elimination
%---------------
divides_prod_elim1 : LEMMA
divides(nz * n, nz * m) IFF divides(n, m)
divides_prod_elim2 : LEMMA
divides(n* nz, m * nz) IFF divides(n, m)
%------------------------------------
% Reflexivity and transitivity
%------------------------------------
divides_reflexive: LEMMA divides(n, n)
divides_transitive: LEMMA
divides(n, m) AND divides(m, l) IMPLIES divides(n, l)
%-----------------------------------------
% Mutual divisors are equal or opposite
%-----------------------------------------
product_one : LEMMA
x * y = 1 IFF (x = 1 AND y = 1) OR (x = -1 AND y = -1)
mutual_divisors : LEMMA
divides(n, m) AND divides(m, n) IMPLIES n = m OR n = - m
mutual_divisors_nat: LEMMA
divides(p, q) AND divides(q, p) IMPLIES p = q
%--------------------------------------
% special properties of zero and one
%--------------------------------------
one_divides : LEMMA divides(1, n)
divides_zero : LEMMA divides(n, 0)
zero_div_zero : LEMMA divides(0, n) IFF n = 0
divisors_of_one : LEMMA divides(n, 1) IFF n = 1 OR n = -1
one_div_one : LEMMA divides(p, 1) IFF p = 1
%--------------------------------
% comparisons divisor/multiple
%--------------------------------
divisor_smaller: LEMMA divides(p, q) IMPLIES q=0 OR p <= q
divides_next: LEMMA divides(n, n + 1) IFF n = 1 OR n = -1
p1: VAR above(1)
divides_plus_1: LEMMA
divides(p1, nz) => NOT divides(p1, nz + 1)
END divides
% Modulo arithmetic defines rem and associated properties
% Provided by Bruno Dutertre
modulo_arithmetic : THEORY
BEGIN
x, y, z, t, q, i : VAR int
n0x : VAR nzint
nx: VAR nat
px, py, b: VAR posnat
n: VAR nat
%---------------------
% Remainder of x/b
%---------------------
% qdiv(nx, b): {q : nat | nx >= b * q AND nx - b*q < b}
nrem(x, b): {r: mod(b) | EXISTS q: x = b * q + r}
rem(b)(x): {r: mod(b) | EXISTS q: x = b * q + r}
rem_def: LEMMA
FORALL (r : mod(b)): rem(b)(x) = r IFF EXISTS q: x = b * q + r
rem_def2: LEMMA
FORALL (r : mod(b)): rem(b)(x) = r IFF divides(b, x - r)
rem_def3: LEMMA
FORALL (r : mod(b)): rem(b)(x) = r IFF divides(b, r - x)
rem_nrem0: LEMMA rem = LAMBDA b: LAMBDA x: nrem(x, b)
rem_nrem: LEMMA rem(b)(x) = nrem(x, b)
%------------------------
% Remainder for easy x
%------------------------
rem_mod: LEMMA FORALL (r : mod(b)): rem(b)(r) = r
rem_mod2: LEMMA 0 <= x AND x < b IMPLIES rem(b)(x) = x
rem_zero: LEMMA rem(b)(0) = 0
rem_self: LEMMA rem(b)(b) = 0
rem_multiple1: LEMMA rem(b)(b * x) = 0
rem_multiple2: LEMMA rem(b)(x * b) = 0
rem_one: LEMMA b /= 1 IMPLIES rem(b)(1) = 1
rem_minus_one: LEMMA rem(b)(-1) = b-1
%-------------------------
% Congruence properties
%-------------------------
same_remainder: LEMMA
rem(b)(x) = rem(b)(y) IFF divides(b, x - y)
rem_rem: LEMMA rem(b)(rem(b)(x)) = rem(b)(x)
rem_sum: LEMMA
rem(b)(x) = rem(b)(y) AND rem(b)(z) = rem(b)(t)
IMPLIES rem(b)(x + z) = rem(b)(y + t)
rem_sum1: LEMMA rem(b)(rem(b)(x) + y) = rem(b)(x + y)
rem_sum2: LEMMA rem(b)(x + rem(b)(y)) = rem(b)(x + y)
rem_diff: LEMMA
rem(b)(x) = rem(b)(y) AND rem(b)(z) = rem(b)(t)
IMPLIES rem(b)(x - z) = rem(b)(y - t)
rem_diff1: LEMMA rem(b)(rem(b)(x) - y) = rem(b)(x - y)
rem_diff2: LEMMA rem(b)(x - rem(b)(y)) = rem(b)(x - y)
rem_prod1: LEMMA rem(b)(rem(b)(x) * y) = rem(b)(x * y)
rem_prod2: LEMMA rem(b)(x * rem(b)(y)) = rem(b)(x * y)
rem_prod: LEMMA
rem(b)(x) = rem(b)(y) AND rem(b)(z) = rem(b)(t)
IMPLIES rem(b)(x * z) = rem(b)(y * t)
rem_expt: LEMMA
rem(b)(x) = rem(b)(y) IMPLIES rem(b)(expt(x, n)) = rem(b)(expt(y, n))
rem_expt1: LEMMA rem(b)(expt(rem(b)(x), n)) = rem(b)(expt(x, n))
rem_sum_elim1: LEMMA
rem(b)(x + y) = rem(b)(x + z) IFF rem(b)(y) = rem(b)(z)
rem_sum_elim2: LEMMA
rem(b)(y + x) = rem(b)(z + x) IFF rem(b)(y) = rem(b)(z)
rem_diff_elim1: LEMMA
rem(b)(x - y) = rem(b)(x - z) IFF rem(b)(y) = rem(b)(z)
rem_diff_elim2: LEMMA
rem(b)(y - x) = rem(b)(z - x) IFF rem(b)(y) = rem(b)(z)
rem_opposite_elim: LEMMA
rem(b)(- x) = rem(b)(- y) IFF rem(b)(x) = rem(b)(y)
% Provide a name for the function asserted to exist by euclid_int
ndiv(x,b) : {q: int | x = b * q + rem(b)(x)}
ndiv_lt: LEMMA ndiv(x,b) <= x/b
JUDGEMENT ndiv(n,b) HAS_TYPE upto(n)
rem_floor: LEMMA FORALL b, x: x = rem(b)(x) + b * floor(x / b)
rem_base: LEMMA
FORALL b, x, i, n:
rem(b)(x) = rem(b + n)(x + i) IFF divides(b + n, i - n * floor(x / b))
rem_sum_floor: LEMMA
FORALL b, x, i:
rem(b)(x + i) = rem(b)(x) + i - b * floor((rem(b)(x) + i) / b)
rem_sum_assoc: COROLLARY
FORALL b, x, n: rem(b)(x + n) = rem(b)(x) + n IFF rem(b)(x) < b - n
rem_add_one: LEMMA
FORALL b, x:
rem(b)(x + 1) = rem(b)(x) + 1 OR
(rem(b)(x) = b - 1 AND rem(b)(x + 1) = 0)
rem_wrap: LEMMA
FORALL b, x, (n: below(b)):
rem(b)(x) < rem(b)(x + n) IFF rem(b)(x) < b - n AND n > 0
rem_wrap_eq: COROLLARY
FORALL b, x, (n: below(b)):
rem(b)(x) <= rem(b)(x + n) IFF rem(b)(x) < b - n OR divides(b, n)
END modulo_arithmetic
% 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
everybelow : THEORY
BEGIN
everybelow(n : nat, P : PRED[below(n)])(i : upto(n)): RECURSIVE bool
= (IF i = 0 THEN TRUE
ELSE P(i-1) AND everybelow(n, P)(i-1)
ENDIF)
MEASURE i
forall_everybelow: LEMMA %transforms universal quantifer into an unfoldable conjunction
(FORALL (n : nat), (P :PRED[below(n)]) : (FORALL (i : below(n)): P(i)) => (FORALL (j : upto(n)): everybelow(n, P)(j)))
forall_everybelow_full: LEMMA
(FORALL (n : nat), (P :PRED[below(n)]) : (FORALL (i : below(n)): P(i)) => everybelow(n, P)(n))
END everybelow
% subrange_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
exp2: THEORY
BEGIN
n,m, x1, x2: VAR nat
exp2(n: nat): RECURSIVE posnat = IF n = 0 THEN 1 ELSE 2 * exp2(n - 1) ENDIF
MEASURE n
JUDGEMENT exp2(n: nat) HAS_TYPE above(n)
% === Properties of exp2 ===================================================
exp2_def : LEMMA exp2(n) = 2^n
exp2_pos : LEMMA exp2(n) > 0
exp2_n : LEMMA exp2(n+1) = 2*exp2(n)
exp2_sum : LEMMA exp2(n + m) = exp2(n) * exp2(m)
exp2_minus : LEMMA (FORALL n,(k:upto(n)): exp2(n-k)=exp2(n)/exp2(k))
exp2_strictpos : LEMMA n > 0 IMPLIES exp2(n) > 1
exp2_lt : LEMMA n < m IMPLIES exp2(n) < exp2(m)
exp_prop : LEMMA x1 < exp2(n) AND x2 < exp2(m)
IMPLIES x1 * exp2(m) + x2 < exp2(n + m)
log2(n: nat): RECURSIVE nat = IF n = 0 THEN 0 ELSE log2(ndiv(n, 2)) + 1 ENDIF
MEASURE n
END exp2
integertypes: THEORY
%------------------------------------------------------------------------
% Author: Natarajan Shankar
%
% Machine integer types and operations to support PVS2C code generation
%------------------------------------------------------------------------
BEGIN
uint8: TYPE = below(exp2(8))
uint16: TYPE = upto(exp2(16) - 1)
uint32: TYPE = upto(exp2(32) - 1)
uint64: TYPE = upto(exp2(64) - 1)
max8: uint8 = 255
max16: uint16 = 65535
max32: uint32 = 4294967295
max64: uint64 = (9223372036854775807 * 2) + 1
% = 18446744073709551615, but C compiler won't accept this
int8: TYPE = subrange(-exp2(7), exp2(7) - 1)
int16: TYPE = subrange(-exp2(15), exp2(15) - 1)
int32: TYPE = subrange(-exp2(31), exp2(31) - 1)
int64: TYPE = subrange(-exp2(63), exp2(63) - 1)
% Provide some intersection types, so that judgements can find a minimal type
pos_uint8: TYPE = {x: uint8 | x > 0}
pos_uint16: TYPE = {x: uint16 | x > 0}
pos_uint32: TYPE = {x: uint32 | x > 0}
pos_uint64: TYPE = {x: uint64 | x > 0}
neg_int8: TYPE = {x: int8 | x < 0}
neg_int16: TYPE = {x: int16 | x < 0}
neg_int32: TYPE = {x: int32 | x < 0}
neg_int64: TYPE = {x: int64 | x < 0}
% Now the even and odd forms of these
even_uint8: TYPE = {x: uint8 | even?(x)} % Only needed for 0, hence no odd_uint8
even_pos_uint8: TYPE = {x: uint8 | x > 0 and even?(x)}
even_pos_uint16: TYPE = {x: uint16 | x > 0 and even?(x)}
even_pos_uint32: TYPE = {x: uint32 | x > 0 and even?(x)}
even_pos_uint64: TYPE = {x: uint64 | x > 0 and even?(x)}
even_neg_int8: TYPE = {x: int8 | x < 0 and even?(x)}
even_neg_int16: TYPE = {x: int16 | x < 0 and even?(x)}
even_neg_int32: TYPE = {x: int32 | x < 0 and even?(x)}
even_neg_int64: TYPE = {x: int64 | x < 0 and even?(x)}
odd_pos_uint8: TYPE = {x: uint8 | x > 0 and odd?(x)}
odd_pos_uint16: TYPE = {x: uint16 | x > 0 and odd?(x)}
odd_pos_uint32: TYPE = {x: uint32 | x > 0 and odd?(x)}
odd_pos_uint64: TYPE = {x: uint64 | x > 0 and odd?(x)}
odd_neg_int8: TYPE = {x: int8 | x < 0 and odd?(x)}
odd_neg_int16: TYPE = {x: int16 | x < 0 and odd?(x)}
odd_neg_int32: TYPE = {x: int32 | x < 0 and odd?(x)}
odd_neg_int64: TYPE = {x: int64 | x < 0 and odd?(x)}
even_pos_uint8_is_nzint: JUDGEMENT even_pos_uint8 SUBTYPE_OF nzint
even_pos_uint16_is_nzint: JUDGEMENT even_pos_uint16 SUBTYPE_OF nzint
even_pos_uint32_is_nzint: JUDGEMENT even_pos_uint32 SUBTYPE_OF nzint
even_pos_uint64_is_nzint: JUDGEMENT even_pos_uint64 SUBTYPE_OF nzint
even_neg_int8_is_nzint: JUDGEMENT even_neg_int8 SUBTYPE_OF nzint
even_neg_int16_is_nzint: JUDGEMENT even_neg_int16 SUBTYPE_OF nzint
even_neg_int32_is_nzint: JUDGEMENT even_neg_int32 SUBTYPE_OF nzint
even_neg_int64_is_nzint: JUDGEMENT even_neg_int64 SUBTYPE_OF nzint
odd_pos_uint8_is_nzint: JUDGEMENT odd_pos_uint8 SUBTYPE_OF nzint
odd_pos_uint16_is_nzint: JUDGEMENT odd_pos_uint16 SUBTYPE_OF nzint
odd_pos_uint32_is_nzint: JUDGEMENT odd_pos_uint32 SUBTYPE_OF nzint
odd_pos_uint64_is_nzint: JUDGEMENT odd_pos_uint64 SUBTYPE_OF nzint
odd_neg_int8_is_nzint: JUDGEMENT odd_neg_int8 SUBTYPE_OF nzint
odd_neg_int16_is_nzint: JUDGEMENT odd_neg_int16 SUBTYPE_OF nzint
odd_neg_int32_is_nzint: JUDGEMENT odd_neg_int32 SUBTYPE_OF nzint
odd_neg_int64_is_nzint: JUDGEMENT odd_neg_int64 SUBTYPE_OF nzint
mini8: int8 = -exp2(7)
mini16: int16 = -exp2(15)
mini32: int32 = -exp2(31)
mini64: int64 = -exp2(63)
maxi8: int8 = exp2(7) - 1
maxi16: int16 = exp2(15) - 1
maxi32: int32 = exp2(31) - 1
maxi64: int64 = exp2(63) - 1
maxsize: MACRO uint32 = exp2(28) %max array size
size: TYPE = upto(maxsize)
maxindex: MACRO uint32 = exp2(28) - 1 %max array index
index: TYPE = below(maxsize) %array index supertype
ux8, uy8, uz8: VAR uint8
ux16, uy16, uz16: VAR uint16
ux32, uy32, uz32: VAR uint32
ux64, uy64, uz64: VAR uint64
x8, y8, z8: VAR int8
x16, y16, z16: VAR int16
x32, y32, z32: VAR int32
x64, y64, z64: VAR int64
subtype_u8_u16: JUDGEMENT uint8 SUBTYPE_OF uint16
subtype_u8_i16: JUDGEMENT uint8 SUBTYPE_OF int16
subtype_u16_u32: JUDGEMENT uint16 SUBTYPE_OF uint32
subtype_u16_i32: JUDGEMENT uint16 SUBTYPE_OF int32
subtype_u32_u64: JUDGEMENT uint32 SUBTYPE_OF uint64
subtype_u32_i64: JUDGEMENT uint32 SUBTYPE_OF int64
plus_u8_u8: JUDGEMENT +(ux8, uy8) HAS_TYPE uint16
plus_u16_u16: JUDGEMENT +(ux16, uy16) HAS_TYPE uint32
plus_u32_u32: JUDGEMENT +(ux32, uy32) HAS_TYPE uint64
plus_u8_i8: JUDGEMENT +(ux8, y8) HAS_TYPE int16
plus_i8_u8: JUDGEMENT +(x8, uy8) HAS_TYPE int16
plus_u16_i16: JUDGEMENT +(ux16, y16) HAS_TYPE int32
plus_i16_u16: JUDGEMENT +(x16, uy16) HAS_TYPE int32
plus_u32_i32: JUDGEMENT +(ux32, y32) HAS_TYPE int64
plus_i32_u32: JUDGEMENT +(x32, uy32) HAS_TYPE int64
u8plus(ux8, uy8): uint8 =
LET gap:uint8 = max8 - ux8
IN IF uy8 <= gap THEN ux8 + uy8 ELSE uy8 - gap - 1 ENDIF
u16plus(ux16, uy16): uint16 =
LET gap:uint16 = max16 - ux16
IN IF uy16 <= gap THEN ux16 + uy16 ELSE uy16 - gap - 1 ENDIF
u32plus(ux32, uy32): uint32 =
LET gap:uint32 = max32 - ux32
IN IF uy32 <= gap THEN ux32 + uy32 ELSE uy32 - gap - 1 ENDIF
u64plus(ux64, uy64): uint64 =
LET gap:uint64 = max64 - ux64
IN IF uy64 <= gap THEN ux64 + uy64 ELSE uy64 - gap - 1 ENDIF
minus_u8_u8: JUDGEMENT -(ux8, uy8) HAS_TYPE int16
minus_u16_u16: JUDGEMENT -(ux16, uy16) HAS_TYPE int32
minus_u32_u32: JUDGEMENT -(ux32, uy32) HAS_TYPE int64
minus_u8_i8: JUDGEMENT -(ux8, y8) HAS_TYPE int16
minus_i8_u8: JUDGEMENT -(x8, uy8) HAS_TYPE int16
minus_u16_i16: JUDGEMENT -(ux16, y16) HAS_TYPE int32
minus_i16_u16: JUDGEMENT -(x16, uy16) HAS_TYPE int32
minus_u32_i32: JUDGEMENT -(ux32, y32) HAS_TYPE int64
minus_i32_u32: JUDGEMENT -(x32, uy32) HAS_TYPE int64
u8minus(ux8, uy8): uint8 =
IF uy8 <= ux8 THEN ux8 - uy8 ELSE max8 - uy8 + ux8 + 1 ENDIF
u16minus(ux16, uy16): uint16 =
IF uy16 <= ux16 THEN ux16 - uy16 ELSE max16 - uy16 + ux16 + 1 ENDIF
u32minus(ux32, uy32): uint32 =
IF uy32 <= ux32 THEN ux32 - uy32 ELSE max32 - uy32 + ux32 + 1 ENDIF
u64minus(ux64, uy64): uint64 =
IF uy64 <= ux64 THEN ux64 - uy64 ELSE max64 - uy64 + ux64 + 1 ENDIF
u8pow2(n: below(8)): uint8 =
exp2(n)
u16pow2(n: below(16)): uint16 =
exp2(n)
u32pow2(n: below(32)): uint32 =
exp2(n)
u64pow2(n: below(64)): uint64 =
exp2(n)
u8lshift(ux8, (n: upto(8))): uint8 =
LET x: below(exp2(8 - n)) = nrem(ux8, exp2(8 - n))
IN x * exp2(n)
k : VAR nat
u8lshift_bound: JUDGEMENT
u8lshift(ux8, (n: upto(8))) HAS_TYPE upto(exp2(8) - exp2(n))
u16lshift(ux16, (n: upto(16))): uint16 =
LET x: below(exp2(16 - n)) = nrem(ux16, exp2(16 - n))
IN x * exp2(n)
% Counterexample: n = 0, ux16 = exp2(16) - 1
% u16lshift_bound: JUDGEMENT
% u16lshift(ux16, (n: upto(8))) HAS_TYPE upto(exp2(8 + n) - exp2(n))
u32lshift(ux32, (n: upto(32))): uint32 =
LET x: below(exp2(32 - n)) = nrem(ux32, exp2(32 - n))
IN x * exp2(n)
% Counterexample: n = 0, ux32 = exp2(32) - 1
% u32lshift_bound: JUDGEMENT
% u32lshift(ux32 , (n: upto(24))) HAS_TYPE upto(exp2(8 + n) - exp2(n))
u64lshift(ux64, (n: upto(64))): uint64 =
LET x: below(exp2(64-n)) = nrem(ux64, exp2(64-n))
IN x * exp2(n)
% Counterexample: n = 0, ux64 = exp2(64) - 1
% u64lshift_bound: JUDGEMENT
% u64lshift(ux64, (n: upto(56))) HAS_TYPE upto(exp2(8 + n) - exp2(n))
u8rshift(ux8, (n: upto(8))): uint8 =
ndiv(ux8, exp2(n))
u8rshift_bound: JUDGEMENT
u8rshift(ux8, (n: upto(8))) HAS_TYPE below(exp2(8 - n))
u16rshift(ux16, (n: upto(16))): uint16 =
ndiv(ux16, exp2(n))
u16rshift_bound: JUDGEMENT
u16rshift(ux16, (n: upto(16))) HAS_TYPE below(exp2(16 - n))
u32rshift(ux32, (n: upto(32))): uint32 =
ndiv(ux32, exp2(n))
u32rshift_bound: JUDGEMENT
u32rshift(ux32, (n: upto(32))) HAS_TYPE below(exp2(32 - n))
u64rshift(ux64, (n: upto(64))): uint64 =
ndiv(ux64, exp2(n))
u64rshift_bound: JUDGEMENT
u64rshift(ux64, (n: upto(64))) HAS_TYPE below(exp2(64 - n))
times_u8_u8: JUDGEMENT *(ux8, uy8) HAS_TYPE uint16
times_u16_u16: JUDGEMENT *(ux16, uy16) HAS_TYPE uint32
times_u32_u32: JUDGEMENT *(ux32, uy32) HAS_TYPE uint64
times_u8_i8: JUDGEMENT *(ux8, y8) HAS_TYPE int16
times_i8_u8: JUDGEMENT *(x8, uy8) HAS_TYPE int16
times_u16_i16: JUDGEMENT *(ux16, y16) HAS_TYPE int32
times_i16_u16: JUDGEMENT *(x16, uy16) HAS_TYPE int32
times_u32_i32: JUDGEMENT *(ux32, y32) HAS_TYPE int64
times_i32_u32: JUDGEMENT *(x32, uy32) HAS_TYPE int64
u8times(ux8, uy8): uint8 =
LET ux16 = ux8 * uy8 IN nrem(ux16, exp2(8))
u16times(ux16, uy16): uint16 =
LET ux32 = ux16 * uy16 IN nrem(ux32, exp2(16))
u32times(ux32, uy32): uint32 =
LET ux64 = ux32 * uy32 IN nrem(ux64, exp2(32))
u64times(ux64, uy64): uint64 =
nrem(ux64 * uy64, exp2(64))
nzu8: VAR {ux8 | ux8 /= 0}
nz8: VAR {x8 | x8 /= 0}
nzu16: VAR {ux16 | ux16 /= 0}
nz16: VAR {x16 | x16 /= 0}
nzu32: VAR {ux32 | ux32 /= 0}
nz32: VAR {x32 | x32 /= 0}
nzu64: VAR {ux64 | ux64 /= 0}
nz64: VAR {x64 | x64 /= 0}
div_u8_u8: JUDGEMENT ndiv(ux8, nzu8) HAS_TYPE uint8
div_u16_u16: JUDGEMENT ndiv(ux16, nzu16) HAS_TYPE uint16
div_u32_u32: JUDGEMENT ndiv(ux32, nzu32) HAS_TYPE uint32
div_u64_u64: JUDGEMENT ndiv(ux64, nzu64) HAS_TYPE uint64
u8div(ux8, (uy8 | uy8 /= 0)): uint8 =
ndiv(ux8, uy8)
u16div(ux16, (uy16 | uy16 /= 0)): uint16 =
ndiv(ux16, uy16)
u32div(ux32, (uy32 | uy32 /= 0)): uint32 =
ndiv(ux32, uy32)
u64div(ux64, (uy64 | uy64 /= 0)): uint64 =
ndiv(ux64, uy64)
u8rem(ux8, (uy8 | uy8 /= 0)): uint8 =
nrem(ux8, uy8)
u16rem(ux16, (uy16 | uy16 /= 0)): uint16 =
nrem(ux16, uy16)
u32rem(ux32, (uy32 | uy32 /= 0)): uint32 =
nrem(ux32, uy32)
u64rem(ux64, (uy64 | uy64 /= 0)): uint64 =
nrem(ux64, uy64)
u8max(ux8, uy8): uint8 = max(ux8, uy8)
u16max(ux16, uy16): uint16 = max(ux16, uy16)
u32max(ux32, uy32): uint32 = max(ux32, uy32)
u64max(ux64, uy64): uint64 = max(ux64, uy64)
i8max(x8, y8): int8 = max(x8, y8)
i16max(x16, y16): int16 = max(x16, y16)
i32max(x32, y32): int32 = max(x32, y32)
i64max(x64, y64): int64 = max(x64, y64)
u8min(ux8, uy8): uint8 = min(ux8, uy8)
u16min(ux16, uy16): uint16 = min(ux16, uy16)
u32min(ux32, uy32): uint32 = min(ux32, uy32)
u64min(ux64, uy64): uint64 = min(ux64, uy64)
i8min(x8, y8): int8 = min(x8, y8)
i16min(x16, y16): int16 = min(x16, y16)
i32min(x32, y32): int32 = min(x32, y32)
i64min(x64, y64): int64 = min(x64, y64)
x : VAR real
u8ceiling(x | 0 <= x AND x <= max8): uint8 = ceiling(x)
u16ceiling(x | 0 <= x AND x <= max16): uint16 = ceiling(x)
u32ceiling(x | 0 <= x AND x <= max32): uint32 = ceiling(x)
u64ceiling(x | 0 <= x AND x <= max64): uint64 = ceiling(x)
u8floor(x | 0 <= x AND x <= max8): uint8 = floor(x)
u16floor(x | 0 <= x AND x <= max16): uint16 = floor(x)
u32floor(x | 0 <= x AND x <= max32): uint32 = floor(x)
u64floor(x | 0 <= x AND x <= max64): uint64 = floor(x)
i8ceiling(x | mini8 <= x AND x <= maxi8): int8 = ceiling(x)
i16ceiling(x | mini16 <= x AND x <= maxi16): int16 = ceiling(x)
i32ceiling(x | mini32 <= x AND x <= maxi32): int32 = ceiling(x)
i64ceiling(x | mini64 <= x AND x <= maxi64): int64 = ceiling(x)
i8floor(x | mini8 <= x AND x <= maxi8): int8 = floor(x)
i16floor(x | mini16 <= x AND x <= maxi16): int16 = floor(x)
i32floor(x | mini32 <= x AND x <= maxi32): int32 = floor(x)
i64floor(x | mini64 <= x AND x <= maxi64): int64 = floor(x)
END integertypes
nat_fun_props : THEORY
%------------------------------------------------------------------------
% Author: Bruno Dutertre
%
% Special properties of injective/surjective functions over nats
%------------------------------------------------------------------------
BEGIN
n, m : VAR nat
injection_n_to_m: THEOREM
(EXISTS (f: [below(n) -> below(m)]): injective?(f)) IMPLIES n <= m
injection_n_to_m_var: THEOREM
(EXISTS (f: [below(n) -> below(m)]): injective?(f)) IFF n <= m
surjection_n_to_m: THEOREM
(EXISTS (f: [below(n) -> below(m)]): surjective?(f)) IMPLIES m <= n
surjection_n_to_m_var: THEOREM
(EXISTS (f: [below(n) -> below(m)]): surjective?(f)) IFF
(m > 0 AND m <= n) OR (m = 0 AND n = 0)
bijection_n_to_m: THEOREM
(EXISTS (f: [below(n) -> below(m)]): bijective?(f)) IFF n = m
injection_n_to_m2: THEOREM
(EXISTS (f: [upto(n) -> upto(m)]): injective?(f)) IFF n <= m
surjection_n_to_m2: THEOREM
(EXISTS (f: [upto(n) -> upto(m)]): surjective?(f)) IFF m <= n
bijection_n_to_m2: THEOREM
(EXISTS (f: [upto(n) -> upto(m)]): bijective?(f)) IFF n = m
surj_equiv_inj: THEOREM
FORALL (f: [below(n) -> below(n)]): surjective?(f) IFF injective?(f)
inj_equiv_bij: THEOREM
FORALL (f: [below(n) -> below(n)]): bijective?(f) IFF injective?(f)
surj_equiv_bij: THEOREM
FORALL (f: [below(n) -> below(n)]): bijective?(f) IFF surjective?(f)
surj_equiv_inj2: THEOREM
FORALL (f: [upto(n) -> upto(n)]): surjective?(f) IFF injective?(f)
inj_equiv_bij2: THEOREM
FORALL (f: [upto(n) -> upto(n)]): bijective?(f) IFF injective?(f)
surj_equiv_bij2: THEOREM
FORALL (f: [upto(n) -> upto(n)]): bijective?(f) IFF surjective?(f)
END nat_fun_props
%------------------------------------------------------------------------
%
% finite sets (basic definitions and closure properties)
% -----------------------------------------------------
% Authors: Damir Jamsek
% Ricky W. Butler
% Sam Owre
% C. Michael Holloway
%
% This theory defines finite sets as the subtype of sets[T] that
% satisfy the predicate "is_finite". This predicate states
% that there is an injective function into below[N] for some N.
%
%------------------------------------------------------------------------
%
% finite_sets_def, card_def, and finite_sets are combined here to make
% things a bit more backward compatible. These were all originally
% part of the finite_sets library.
finite_sets[T: TYPE]: THEORY
% beginning of original finite_sets_def theory
BEGIN
x, y, z: VAR T
s: VAR set[T]
N: VAR nat
is_finite(s): bool = (EXISTS N, (f: [(s) -> below[N]]):
injective?(f))
finite_set: TYPE = (is_finite) CONTAINING emptyset[T]
non_empty_finite_set: TYPE = {s: finite_set | NOT empty?(s)}
is_finite_surj: LEMMA (EXISTS (N: nat), (f: [below[N] -> (s)]):
surjective?(f)) IFF is_finite(s)
A, B: VAR finite_set
NA, NB: VAR non_empty_finite_set
finite_subset: LEMMA subset?(s,A) IMPLIES is_finite(s)
finite_intersection: LEMMA is_finite(intersection(A,B))
finite_add: LEMMA is_finite(add(x,A))
% -------- Judgements --------------------------------------------------
nonempty_finite_is_nonempty: JUDGEMENT
non_empty_finite_set SUBTYPE_OF (nonempty?[T])
finite_singleton: JUDGEMENT singleton(x) HAS_TYPE finite_set
finite_union: JUDGEMENT union(A, B) HAS_TYPE finite_set
finite_intersection1: JUDGEMENT intersection(s, A) HAS_TYPE finite_set
finite_intersection2: JUDGEMENT intersection(A, s) HAS_TYPE finite_set
finite_difference: JUDGEMENT difference(A, s) HAS_TYPE finite_set
nonempty_finite_union1: JUDGEMENT union(NA, B) HAS_TYPE non_empty_finite_set
nonempty_finite_union2: JUDGEMENT union(A, NB) HAS_TYPE non_empty_finite_set
nonempty_add_finite: JUDGEMENT add(x, A) HAS_TYPE non_empty_finite_set
finite_remove: JUDGEMENT remove(x, A) HAS_TYPE finite_set
finite_rest: JUDGEMENT rest(A) HAS_TYPE finite_set
finite_emptyset: JUDGEMENT emptyset HAS_TYPE finite_set
nonempty_singleton_finite: JUDGEMENT
singleton(x) HAS_TYPE non_empty_finite_set
% -------- Base type is finite -----------------------------------------
is_finite_type: bool = (EXISTS N, (g:[T -> below[N]]): injective?(g))
finite_full: LEMMA is_finite_type IFF is_finite(fullset[T])
finite_type_set: LEMMA is_finite_type IMPLIES is_finite(s)
finite_complement: LEMMA is_finite_type IMPLIES is_finite(complement(s))
% end of original finite_sets_def
% beginning of original card_def theory
%------------------------------------------------------------------------
%
% Fundamental definition of card
%
% Authors: Bruno Dutertre
% Ricky W. Butler
%------------------------------------------------------------------------
S, S2: VAR finite_set
n, m: VAR nat
p : VAR posnat
inj_set(S): (nonempty?[nat]) =
{ n | EXISTS (f : [(S)->below[n]]) : injective?(f) }
Card(S): nat = min(inj_set(S))
inj_Card : LEMMA Card(S) = n IMPLIES
(EXISTS (f : [(S) -> below[n]]) : injective?(f))
reduce_inj : LEMMA (FORALL (f : [(S)->below[p]]) :
injective?(f) AND NOT surjective?(f) IMPLIES
(EXISTS (g: [(S)->below[p-1]]): injective?(g)))
Card_injection: LEMMA (EXISTS (f : [(S)->below[n]]) : injective?(f))
IMPLIES Card(S) <= n
Card_surjection : LEMMA (EXISTS (f : [(S)->below[n]]) : surjective?(f))
IMPLIES n <= Card(S)
Card_bijection : THEOREM
Card(S) = n IFF (EXISTS (f : [(S)->below[n]]) : bijective?(f))
Card_disj_union: THEOREM disjoint?(S,S2) IMPLIES
Card(union(S,S2)) = Card(S) + Card(S2)
% ------------------------------------------------------------------------
card(S): {n: nat| n = Card(S)} % inhibit expansion
card_def : THEOREM card(S) = Card(S) % But if you really need to
% end of original card_def theory
% beginning of original finite_sets theory
card_emptyset : THEOREM card(emptyset[T]) = 0
empty_card : THEOREM empty?(S) IFF card(S) = 0
card_empty? : THEOREM (card(S) = 0) = empty?(S)
card_is_0 : THEOREM (card(S) = 0) = (S = emptyset)
nonempty_card : THEOREM nonempty?(S) IFF card(S) > 0
card_singleton : THEOREM card(singleton(x)) = 1
card_one : THEOREM card(S) = 1 IFF (EXISTS x : S = singleton(x))
card_disj_union : THEOREM disjoint?(A,B) IMPLIES
card(union(A,B)) = card(A) + card(B)
card_diff_subset: THEOREM subset?(A, B) IMPLIES
card(difference(B, A)) = card(B) - card(A)
card_subset : THEOREM subset?(A,B) IMPLIES card(A) <= card(B)
card_plus : THEOREM card(A) + card(B) =
card(union(A, B)) + card(intersection(A,B))
card_union : THEOREM card(union(A,B)) = card(A) + card(B) -
card(intersection(A,B))
card_add : THEOREM card(add(x, S)) = card(S)
+ IF S(x) THEN 0 ELSE 1 ENDIF
card_add_gt0 : THEOREM card(add(x,S)) > 0
card_remove : THEOREM card(remove(x, S)) = card(S)
- IF S(x) THEN 1 ELSE 0 ENDIF
card_rest : THEOREM NOT empty?(S) IMPLIES card(rest(S)) = card(S) - 1
same_card_subset: THEOREM subset?(A, B) AND card(A) = card(B)
IMPLIES A = B
smaller_card_subset : THEOREM subset?(A, B) AND card(A) < card(B) IMPLIES
(EXISTS x : member(x, B) AND NOT member(x, A))
card_strict_subset: THEOREM strict_subset?(A,B) IMPLIES card(A) < card(B)
card_1_has_1 : THEOREM card(S) >= 1 IFF (EXISTS (x: T): S(x))
card_2_has_2 : THEOREM card(S) >= 2 IFF
(EXISTS (x,y: T): x /= y AND S(x) AND S(y))
card_intersection_le: THEOREM card(intersection(A,B)) <= card(A) AND
card(intersection(A,B)) <= card(B)
card_bij : THEOREM card(S) = N
IFF (EXISTS (f: [(S) -> below[N]]): bijective?(f))
card_bij_inv : THEOREM card(S) = N
IFF (EXISTS (f: [below[N] -> (S)]): bijective?(f))
bij_exists : COROLLARY (EXISTS (f: [(S) -> below(card(S))]):
bijective?(f))
bij(S: finite_set): {f:[(S) -> below(card(S))] | bijective?(f)}
ibij(S: non_empty_finite_set): {f:[below(card(S)) -> (S)] | bijective?(f)} =
inverse(bij(S))
bij_ibij: LEMMA FORALL (S: non_empty_finite_set, ii: below(card(S))):
bij(S)(ibij(S)(ii)) = ii
ibij_bij: LEMMA FORALL (S: non_empty_finite_set, x:T):
S(x) IMPLIES ibij(S)(bij(S)(x)) = x
is_finite_exists_N: LEMMA FORALL (g: [below[N] -> T]):
is_finite({r: T | EXISTS (n: below[N]): r = g(n)})
% card_n_has_n : THEOREM card(S) >= n IMPLIES
% (EXISTS (X: [below[N] -> T]):
% (FORALL (i: below[N]): S(X(i))) AND
% (FORALL (i,j: below[N]): X(i) /= X(j)))
P, P1, P2: VAR pred[T]
finite_pred: LEMMA is_finite(fullset[T]) IMPLIES
is_finite[T]({x: T | P(x)})
finite_pred2: LEMMA is_finite(P) IMPLIES
is_finite[T]({x: T | P(x)})
card_implies: LEMMA is_finite(fullset[T]) AND
(FORALL (x: T): P1(x) IMPLIES P2(x))
IMPLIES card({x: T | P1(x)}) <= card({x: T | P2(x)})
finite_induction: THEOREM
FORALL (p: pred[set[T]]):
(FORALL (n: nat), (S: set[T]):
(EXISTS (f: [(S) -> below[n]]): injective?(f)) => p(S))
=> (FORALL (FS: finite_set): p(FS))
END finite_sets
% Courtesy Jerry James
restrict_set_props[T: TYPE, S: TYPE FROM T]: THEORY
BEGIN
restrict_finite: LEMMA
FORALL (a: set[T]): is_finite(a) => is_finite(restrict[T, S, bool](a))
finite_restrict: JUDGEMENT
restrict[T, S, bool](a: finite_set[T]) HAS_TYPE finite_set[S]
empty_restrict: JUDGEMENT
restrict[T, S, bool](a: (empty?[T])) HAS_TYPE (empty?[S])
card_restrict: LEMMA
FORALL (a: finite_set[T]): card(restrict[T, S, bool](a)) <= card(a)
END restrict_set_props
% Courtesy Jerry James
extend_set_props[T: TYPE, S: TYPE FROM T]: THEORY
BEGIN
finite_extension: LEMMA
FORALL (a: set[S]):
is_finite(extend[T, S, bool, FALSE](a)) IFF is_finite(a)
finite_extend: JUDGEMENT
extend[T, S, bool, FALSE](a: finite_set[S]) HAS_TYPE finite_set[T]
empty_extend: JUDGEMENT
extend[T, S, bool, FALSE](a: (empty?[S])) HAS_TYPE (empty?[T])
nonempty_extend: JUDGEMENT
extend[T, S, bool, FALSE](a: (nonempty?[S])) HAS_TYPE (nonempty?[T])
singleton_extend: JUDGEMENT
extend[T, S, bool, FALSE](a: (singleton?[S])) HAS_TYPE (singleton?[T])
card_extend: LEMMA
FORALL (a: finite_set[S]): card(extend[T, S, bool, FALSE](a)) = card(a)
empty?_extend: LEMMA
FORALL (a: set[S]):
empty?(extend[T, S, bool, FALSE](a)) IFF empty?(a)
nonempty?_extend: LEMMA
FORALL (a: set[S]):
nonempty?(extend[T, S, bool, FALSE](a)) IFF nonempty?(a)
singleton?_extend: LEMMA
FORALL (a: set[S]):
singleton?(extend[T, S, bool, FALSE](a)) IFF singleton?(a)
subset_extend: LEMMA
FORALL (a, b: set[S]):
subset?(extend[T, S, bool, FALSE](a), extend[T, S, bool, FALSE](b)) IFF
subset?(a, b)
union_extend: LEMMA
FORALL (a, b: set[S]):
union(extend[T, S, bool, FALSE](a), extend[T, S, bool, FALSE](b))
= extend[T, S, bool, FALSE](union(a, b))
intersection_extend: LEMMA
FORALL (a, b: set[S]):
intersection(extend[T, S, bool, FALSE](a), extend[T, S, bool, FALSE](b))
= extend[T, S, bool, FALSE](intersection(a, b))
difference_extend: LEMMA
FORALL (a, b: set[S]):
difference(extend[T, S, bool, FALSE](a), extend[T, S, bool, FALSE](b))
= extend[T, S, bool, FALSE](difference(a, b))
add_extend: LEMMA
FORALL (x: S, a: set[S]):
add(x, extend[T, S, bool, FALSE](a))
= extend[T, S, bool, FALSE](add(x, a))
remove_extend: LEMMA
FORALL (x: S, a: set[S]):
remove(x, extend[T, S, bool, FALSE](a))
= extend[T, S, bool, FALSE](remove(x, a))
END extend_set_props
%-------------------------------------------------------------------------
%
% Additions to the function_image theory. These additions
% show that the image of a finite set is finite, and that any injective
% function is bijective with its image.
%
% ---------------------------------------------------------------------
% Author: Jerry James (jamesj@acm.org), University of Kansas
%-------------------------------------------------------------------------
function_image_aux[D: TYPE, R: TYPE]: THEORY
BEGIN
S: VAR finite_set[D]
f: VAR [D -> R]
inj: VAR (injective?[D, R])
finite_image: JUDGEMENT image(f, S) HAS_TYPE finite_set[R]
card_image: LEMMA FORALL f, S: card(image(f, S)) <= card(S)
card_injective_image: LEMMA FORALL inj, S: card(image(inj, S)) = card(S)
bijective_image: LEMMA
FORALL inj: bijective?[D, (image(inj, fullset[D]))](inj)
END function_image_aux
% 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_add_applied: LEMMA
iterate(f,m)(iterate(f, n)(x)) = iterate(f, m + n)(x)
iterate_add_one: LEMMA
iterate(f, n)(f(x)) = iterate(f, n+1)(x)
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] = fs`seq;
CONVERSION finseq_appl;
every(P: [T->bool])(fs): bool = (FORALL (i: below(fs`length)): P(fs`seq(i)));
some(P: [T->bool])(fs): bool = (EXISTS (i: below(fs`length)): P(fs`seq(i)));
o(fs1, fs2): finseq =
LET l1 = fs1`length,
lsum = l1 + fs2`length
IN (# length := lsum,
seq := (LAMBDA (n:below[lsum]):
IF n < l1
THEN fs1`seq(n)
ELSE fs2`seq(n-l1)
ENDIF) #);
P: VAR [T -> bool]
every_compose: LEMMA
every(P)(fs1 o fs2) = (every(P)(fs1) AND every(P)(fs2))
some_compose: LEMMA
some(P)(fs1 o fs2) = (some(P)(fs1) OR some(P)(fs2))
p: VAR [nat, nat]
^(fs, p): finseq =
LET (m, n) = p
IN IF m > n OR m >= fs`length
THEN empty_seq
ELSE LET len = min(n - m + 1, fs`length - m)
IN (# length := len,
seq := (LAMBDA (x: below[len]): fs`seq(x + m)) #)
ENDIF;
% This is the same as above, but returns domain [m..n-1] rather than [m..n]
% More generally useful, but the above is kept for backward compatibility
^^(fs, p): finseq =
LET (m, n) = p
IN IF m >= n OR m >= fs`length
THEN empty_seq
ELSE LET len = min(n - m, fs`length - m)
IN (# length := len,
seq := (LAMBDA (x: below[len]): fs`seq(x + m)) #)
ENDIF
extract1(fs:{fs | fs`length = 1}): T = fs`seq(0)
CONVERSION extract1
o_assoc: LEMMA fs1 o (fs2 o fs3) = (fs1 o fs2) o fs3
END finite_sequences
more_finseq [T: TYPE]: THEORY
BEGIN
seq: TYPE = finseq[T]
rr, ss, tt: VAR seq
x, y, z: VAR T
prefix?(rr, ss): bool =
rr`length <= ss`length AND
(FORALL (i: below(rr`length)): rr`seq(i) = ss`seq(i))
prefix_closed?(X : set[seq]): bool =
FORALL ss: X(ss) IMPLIES (FORALL (rr | prefix?(rr, ss)): X(rr))
add(x, rr): finseq[T] =
rr WITH [`length := rr`length + 1,
`seq(rr`length) |-> x]
END more_finseq
array_sequences [T: TYPE]: THEORY
BEGIN
arrayseq: TYPE = [# length: size, seq: ARRAY[below[length] -> T] #]
aseq: TYPE = arrayseq
a, b, c: VAR aseq
m, n: VAR nat
empty_aseq: aseq =
(# length := 0,
seq := (LAMBDA (x: below[0]): epsilon! (t:T): true) #)
full_aseq?(a): bool = (a`length = maxsize)
aseq_appl(a): [below[length(a)] -> T] = a`seq;
% Causes problems with finseq_appl conversion
% CONVERSION aseq_appl;
aseq_finseq: JUDGEMENT aseq SUBTYPE_OF finseq[T]
add_aseq: JUDGEMENT add(x : T, (a | NOT full_aseq?(a))) HAS_TYPE aseq
END array_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) = (omega^u)*i + v
% add(i, u, add(j, v, w)) = (omega^u)*i + (omega^v)*j + 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<z) OR
(u=z) AND (i<j) OR
(u=z) AND (i=j) AND (v<w)
ENDCASES
ENDCASES
MEASURE size(x);
>(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
% lex3 provides a lexical ordering for triples of natural numbers.
lex3: THEORY
BEGIN
i, j, k, m, n, p: VAR nat
lex3(m, n, p): ordinal =
IF (m = 0)
THEN lex2(n, p)
ELSE add(m, add(2, add(2, zero, zero), zero), lex2(n, p))
ENDIF
wtf?: LEMMA
NOT (add(2, add(2, zero, zero), zero) = add(1, zero, zero))
lex3_lt: LEMMA
(lex3(i, j, k) < lex3(m, n, p)) =
((i < m) OR ((i = m) AND (lex2(j,k) < lex2(n, p))))
END lex3
% lex4 provides a lexical ordering for quadruples of natural numbers.
lex4: THEORY
BEGIN
i, j, k, l, m, n, p, q: VAR nat
lex4(m, n, p, q): ordinal =
IF (m = 0)
THEN lex3(n, p, q)
ELSE add(m, add(3, add(2, add(1, zero, zero), zero), zero), lex3(n, p, q))
ENDIF
wtf?: LEMMA
NOT (add(3, add(2, add(1, zero, zero), zero), zero) = add(1, zero, zero))
same_coefs: LEMMA
∀ (A, B:ordinal) : nonzero?(A) ∧ nonzero?(B) ⇒ (A = B ⇒ coef(A) = coef(B))
lex4_lt: LEMMA
(lex4(i, j, k, l) < lex4(m, n, p, q)) =
((i < m) OR ((i = m) AND (lex3(j, k, l) < lex3(n, p, q))))
END lex4
% 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
P, Q: VAR PRED[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)
member_null: LEMMA member(x, l) IMPLIES NOT null?(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(append(l1, l2), l3) = append(l1, append(l2, l3))
reverse_append: LEMMA
reverse(append(l1, l2)) = append(reverse(l2), reverse(l1))
reverse_reverse: LEMMA reverse(reverse(l)) = l
length_append: LEMMA length(append(l1, l2)) = length(l1) + length(l2)
length_reverse: LEMMA length(reverse(l)) = length(l)
member_nth: LEMMA member(x, l) IFF EXISTS (i: below(length(l))): x = nth(l, i)
nth_append: LEMMA
FORALL (i: below(length(append(l1, l2)))):
nth(append(l1, l2), i)
= IF i < length(l1) THEN nth(l1, i) ELSE nth(l2, i - length(l1)) ENDIF
nth_reverse: LEMMA
FORALL (i: below(length(l1))):
nth(reverse(l1), i) = nth(l1, length(l1) - i - 1)
a, b, c: VAR T
list_rep: LEMMA (: a, b, c :) = cons(a, cons(b, cons(c, null)))
every_unc_eq_cur: LEMMA
every(P, l) = every(P)(l)
every_append: LEMMA
every(P)(append(l1, l2)) IFF (every(P)(l1) AND every(P)(l2))
some_append: LEMMA
some(P)(append(l1, l2)) IFF (some(P)(l1) OR some(P)(l2))
every_disjunct1: LEMMA
every(P)(l) IMPLIES every(LAMBDA (x: T): P(x) OR Q(x))(l)
some_disjunct1: LEMMA
some(P)(l) IMPLIES some(LAMBDA (x : T): P(x) OR Q(x))(l)
every_disjunct2: LEMMA
every(Q)(l) IMPLIES every(LAMBDA (x: T): P(x) OR Q(x))(l)
some_disjunct2: LEMMA
some(Q)(l) IMPLIES some(LAMBDA (x : T): P(x) OR Q(x))(l)
every_conjunct: LEMMA
every(LAMBDA (x: T): P(x) AND Q(x))(l) => (every(P)(l) AND every(Q)(l))
some_conjunct: LEMMA
some(LAMBDA (x: T): P(x) AND Q(x))(l) => (some(P)(l) AND some(Q)(l))
every_conjunct2: LEMMA
(every(P)(l) AND every(Q)(l)) => every(LAMBDA (x: T): P(x) AND Q(x))(l)
every_member: LEMMA every({c: T | member(c, l)})(l)
every_nth: LEMMA
every(P)(l) IFF FORALL (i:below(length(l))): P(nth(l,i))
some_nth: LEMMA
some(P)(l) IFF EXISTS (i:below(length(l))): P(nth(l,i))
every_implies: LEMMA
(FORALL x: P(x) => Q(x))
AND every(P)(l)
=> every(Q)(l)
some_implies: LEMMA
(FORALL x: P(x) => Q(x))
AND some(P)(l)
=> some(Q)(l)
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
more_map_props [T1, T2: TYPE]: THEORY
BEGIN
f: VAR [T1 -> T2]
l, l1, l2: VAR list[T1]
g: VAR [T1 -> list[T2]]
P: VAR pred[list[T2]]
map_length: LEMMA length(map(f)(l)) = length(l)
map_nth_rw: LEMMA
FORALL (i: below(length(l))):
nth(map(f)(l), i) = f(nth(l, i))
map_unc_eq_cur: LEMMA map(f, l) = map(f)(l)
every_map: LEMMA every(P)(map(g)(l)) = every(P o g)(l)
map_append: LEMMA map(f)(append(l1, l2)) = append(map(f)(l1), map(f)(l2))
END more_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, q: 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_adt[T].every(p)) =
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_adt[T].every(p)) =
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)
every_filter_uncurried: LEMMA
FORALL (x : (list_adt[T].every(p))): every(p)(filter(x, q))
every_filter: LEMMA
FORALL (x : (list_adt[T].every(p))): every(p)(filter(q)(x))
length_filter: LEMMA (FORALL (p: PRED[T]): length(filter(l, p)) <= length(l))
END filters
% list2finseq
list2finseq[T: TYPE]: THEORY
BEGIN
l, l1, l2: VAR list[T]
fs: VAR finseq[T]
n, i: VAR nat
a, b, c, c1, c2: VAR T
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(fs`seq(length(fs) - n),
finseq2list_rec(fs, n-1))
ENDIF
MEASURE n
finseq2list(fs): list[T] = finseq2list_rec(fs, length(fs))
CONVERSION list2finseq, finseq2list
finseq2list_length_rec: LEMMA
n <= fs`length IMPLIES length(finseq2list_rec(fs, n)) = n
finseq2list_length: LEMMA
length(finseq2list(fs)) = fs`length
finseq2list_nth_rec: LEMMA
n <= fs`length AND i < n IMPLIES
nth(finseq2list_rec(fs, n), i) = fs`seq(fs`length - n + i)
finseq2list_nth: LEMMA
FORALL (i: below(fs`length)):
nth(finseq2list(fs), i) = fs`seq(i)
list2finseq_finseq2list: LEMMA
list2finseq(finseq2list(fs)) = fs
list2finseq_inj: LEMMA
(list2finseq(l1) = list2finseq(l2)) = (l1 = l2)
finseq2list_list2finseq: LEMMA
finseq2list(list2finseq(l)) = l
fseq_lem: LEMMA
(list2finseq(l1) = list2finseq(l2)) = (l1 = l2)
cons_lem: LEMMA (cons(c1,l1) = cons(c2,l2)) = (c1 = c2 & l1 = l2)
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
% The disjointness theory defines the pairwise_disjoint? function.
% This is used in generating the disjointness axiom for large datatypes
% or enumeration types. This is because for N constructors, N(N-1)/2
% terms need to be constructed. Thus care must be taken if the list
% is longer than a few hundred elements.
disjointness: THEORY
BEGIN
l: VAR list[bool]
pairwise_disjoint?(l): RECURSIVE boolean =
cases l of
null: true,
cons(x,y): every(LAMBDA (z:bool): NOT (x AND z))(y)
AND pairwise_disjoint?(y)
endcases
MEASURE length(l)
END disjointness
% characters - this follows Unicode UTF8 standard,
% where the first 128 are the ASCII chars:
%
% | 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|
% Characters may be given in PVS between single quotes, e.g.,
% 'a' 'α' '̆\\n'
character: DATATYPE
BEGIN
char(code:below[0x110000]):char?
END character
% strings - the strings theory introduces the char type and represents
% strings as a finite sequence of chars. The lemmas are useful for
% rewriting. This theory is useful to auto-rewrite with, but make sure
% that list2finseq is not also an auto-rewrite rule.
%
% 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 \0 followed by an octal number (< 0400), a \ followed by
% a decimal number (< 256) or a \x or \X followed by a
% hexidecimal number (< FF) represents that character number.
% Decimal numbers must be written without leading zeros, as
% otherwise they will get interpreted as octal (for instance
% "\065" = "\53" = "\x35"). If the character following such an escape
% is a digit one has to use the maximal number of digits in the escape
% (for instance "\00530" = "50" while "\0530" is illegal). Therefore,
% if one wants to put escape (\27) followed by a 0 into a string one
% has to use two escapes ("\27\30") or an octal or hex escape
% ("\00330" = "\x1b0") because \270 is illegal (270 > 255) and
% \027 is interpreted as octal.
% 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
char: TYPE = (char?)
string: TYPE = finite_sequence[char]
l1, l2: VAR list[char]
c1, c2: VAR char
fseq_lem: LEMMA
(list2finseq(l1) = list2finseq(l2)) = (l1 = l2)
cons_lem: LEMMA (cons(c1,l1) = cons(c2,l2)) = (c1 = c2 & l1 = l2)
char_lem: LEMMA (c1 = c2) = (code(c1) = code(c2))
make_string(i:index, s : ARRAY[below(i)->char]): string
= (# length := i, seq := (LAMBDA (j:below(i)): s(j)) #)
END strings
gen_strings : THEORY
BEGIN
s, s1, s2: VAR string
c, c1, c2: VAR char
length(s): nat = s`length
get(s, (i: below(length(s)))): char = s`seq(i)
empty: string = (# length := 0, seq := (LAMBDA (i: below(0)): char(0)) #)
length_empty: lemma length(empty) = 0
unit(c): string = (# length := 1, seq := (LAMBDA (i: below(1)): c) #)
length_unit: LEMMA length(unit(c)) = 1
unit_ax: LEMMA get(unit(c), 0) = c
extensionality: LEMMA
s1 = s2 IFF (length(s1) = length(s2) AND ∀ (i:below(length(s1))): get(s1, i) = get(s2, i));
length_concat: LEMMA length(s1 o s2) = length(s1) + length(s2)
char_concat: LEMMA
(FORALL (i: below(length(s1) + length(s2))):
get(s1 o s2, i) =
IF i < length(s1)
THEN get(s1, i)
ELSE get(s2, i - length(s1))
ENDIF)
strdiff_rec(s1, s2, (i : upto(min(length(s1), length(s2))))): RECURSIVE
upto(min(length(s1), length(s2)))
= (IF i = length(s1) OR i = length(s2) OR get(s1, i) /= get(s2, i)
THEN i
ELSE strdiff_rec(s1, s2, i + 1)
ENDIF)
MEASURE min(length(s1), length(s2)) - i
strdiff(s1, s2): upto(min(length(s1), length(s2))) = strdiff_rec(s1, s2, 0)
strdiff_eq: LEMMA
FORALL (j: below(strdiff(s1, s2))): get(s1, j) = get(s2, j)
strdiff_neq: LEMMA
(LET i = strdiff(s1, s2) IN
i < min(length(s1), length(s2)) => get(s1, i) /= get(s2, i))
strcmp(s1, s2): subrange(-1, 1) =
(LET i = strdiff(s1, s2)
IN IF i = min(length(s1), length(s2))
THEN IF length(s1) < length(s2) THEN -1 ELSIF length(s1) > length(s2) THEN 1 ELSE 0 ENDIF
ELSIF code(get(s1, i)) < code(get(s2, i)) THEN -1 ELSE 1 ENDIF)
strcmp_eq: LEMMA
strcmp(s1, s2) = 0 => s1 = s2
strcmp_lt: LEMMA
strcmp(s1, s2) = -1 =>
(LET i = strdiff(s1, s2) IN
i < length(s2) AND (i < length(s1) => code(get(s1, i)) < code(get(s2, i))))
strcmp_gt: LEMMA
strcmp(s1, s2) = 1 =>
(LET i = strdiff(s1, s2) IN
i < length(s1) AND (i < length(s2) => code(get(s2, i)) < code(get(s1, i))))
prefix(s, (i: upto(length(s)))): string =
(IF i = length(s) THEN s ELSE (# length := i, seq := (LAMBDA (j : below(i)): get(s, j)) #) ENDIF)
length_prefix: LEMMA
(FORALL (i: upto(length(s))):
length(prefix(s, i)) = i)
prefix_ax: LEMMA
FORALL (i: upto(length(s))), (j : below(i)):
get(prefix(s, i), j) = get(s, j)
suffix(s, (i: upto(length(s)))): string =
(IF i = 0 THEN s ELSE (# length := length(s) - i, seq := (LAMBDA (j : below(length(s) - i)): get(s, i + j)) #) ENDIF)
length_suffix: LEMMA
(FORALL (i: upto(length(s))):
length(suffix(s, i)) = length(s) - i)
suffix_ax: LEMMA
FORALL (i: upto(length(s))), (j : below(length(s) - i)):
get(suffix(s, i), j) = get(s, i + j)
substr(s, (i: upto(length(s))), j: subrange(i, length(s))): {s1 | length(s1) = j - i}
= prefix(suffix(s, i), j - i)
END gen_strings
charstrings: THEORY
BEGIN
charstring_bound: MACRO uint32 = exp2(28) %same as index, but only used in types
charstring: TYPE = [# length : index, %below(charstring_bound)
seq : ARRAY[below(length) -> char] #]
c, c1, c2: VAR char
s, s1, s2: VAR charstring
length(s): index = s`length %below(charstring_bound)
cget(s, (i: below(length(s)))): char = s`seq(i)
null: charstring = (# length := 0, seq := (LAMBDA (i: below(0)): char(0)) #)
length_null: LEMMA length(null) = 0
addchar(c, (s | length(s) + 1 < charstring_bound)): charstring =
(# length := s`length + 1,
seq := (LAMBDA (i:below(s`length + 1)): IF i = s`length THEN c ELSE get(s, i) ENDIF)
#)
unit(c): charstring = (# length := 1, seq := (LAMBDA (i:below(1)): c) #)
CONVERSION+ charstrings.unit
length_unit: LEMMA length(unit(c)) = 1
unit_ax: LEMMA cget(unit(c), 0) = c
extensionality: LEMMA
s1 = s2 IFF (length(s1) = length(s2) AND ∀ (i:below(length(s1))): cget(s1, i) = cget(s2, i));
cstring: TYPE = {cs : string | cs`length < charstring_bound}
mk_charstring(cs: cstring): charstring =
(# length := cs`length,
seq := (LAMBDA (i: below(cs`length::below(charstring_bound))): get(cs, i)) #);
++(s1, (s2 | s2`length + s1`length < charstring_bound)): charstring =
IF s1`length = 0 THEN s2
ELSIF s2`length = 0 THEN s1
ELSE (LET n : below(charstring_bound) = s1`length + s2`length
IN (# length := n,
seq := (LAMBDA (i:below(n)): IF i < s1`length THEN cget(s1, i) ELSE cget(s2, i - s1`length) ENDIF)
#))
ENDIF
length_concat: LEMMA
FORALL (s1, (s2 | s2`length + s1`length < charstring_bound)):
length(s1 ++ s2) = length(s1) + length(s2)
char_concat: LEMMA
(FORALL s1, (s2 | s2`length + s1`length < charstring_bound), (i: below(length(s1) + length(s2))):
cget(s1 o s2, i) =
IF i < length(s1)
THEN cget(s1, i)
ELSE cget(s2, i - length(s1))
ENDIF)
strdiff_rec(s1, s2, (i : upto(min(length(s1), length(s2))))): RECURSIVE
upto(min(length(s1), length(s2)))
= (IF i = length(s1) OR i = length(s2) OR cget(s1, i) /= cget(s2, i)
THEN i
ELSE strdiff_rec(s1, s2, i + 1)
ENDIF)
MEASURE min(length(s1), length(s2)) - i
strdiff(s1, s2): upto(min(length(s1), length(s2))) = strdiff_rec(s1, s2, 0)
strdiff_eq: LEMMA
FORALL (j: below(strdiff(s1, s2))): cget(s1, j) = cget(s2, j)
strdiff_neq: LEMMA
(LET i = strdiff(s1, s2) IN
i < min(length(s1), length(s2)) => cget(s1, i) /= cget(s2, i))
strcmp(s1, s2): subrange(-1, 1) =
(LET i = strdiff(s1, s2)
IN IF i = min(length(s1), length(s2))
THEN IF length(s1) < length(s2) THEN -1 ELSIF length(s1) > length(s2) THEN 1 ELSE 0 ENDIF
ELSIF code(cget(s1, i)) < code(cget(s2, i)) THEN -1 ELSE 1 ENDIF)
strcmp_eq: LEMMA
strcmp(s1, s2) = 0 => s1 = s2
strcmp_lt: LEMMA
strcmp(s1, s2) = -1 =>
(LET i = strdiff(s1, s2) IN
i < length(s2) AND (i < length(s1) => code(cget(s1, i)) < code(cget(s2, i))))
strcmp_gt: LEMMA
strcmp(s1, s2) = 1 =>
(LET i = strdiff(s1, s2) IN
i < length(s1) AND (i < length(s2) => code(cget(s2, i)) < code(cget(s1, i))))
prefix(s, (i: upto(length(s)))): charstring =
(IF i = length(s) THEN s ELSE (# length := i, seq := (LAMBDA (j : below(i)): cget(s, j)) #) ENDIF)
length_prefix: LEMMA
(FORALL (i: upto(length(s))):
length(prefix(s, i)) = i)
prefix_ax: LEMMA
FORALL (i: upto(length(s))), (j : below(i)):
cget(prefix(s, i), j) = cget(s, j)
suffix(s, (i: upto(length(s)))): charstring =
IF i = 0
THEN s
ELSE (# length := length(s) - i,
seq := (LAMBDA (j : below(length(s) - i)): cget(s, i + j)) #)
ENDIF
length_suffix: LEMMA
(FORALL (i: upto(length(s))):
length(suffix(s, i)) = length(s) - i)
suffix_ax: LEMMA
FORALL (i: upto(length(s))), (j : below(length(s) - i)):
cget(suffix(s, i), j) = cget(s, i + j)
substr(s, (i: upto(length(s))), j: subrange(i, length(s))): {s1 | length(s1) = j - i}
= prefix(suffix(s, i), j - i)
ascii_charstring?(s): bool = FORALL (i : below(length(s))): code(cget(s, i)) < 128
ascii_charstring: TYPE = (ascii_charstring?)
END charstrings
bytestrings: THEORY
BEGIN
byte : TYPE+ = uint8
bytestring_bound: MACRO uint32 = exp2(28) % 0x100000000
b, b1, b2: VAR byte
bytestring: TYPE = [# length : index, %below(bytestring_bound),
seq : ARRAY[below(length) -> byte] #]
s, s1, s2: VAR bytestring
length(s): index = s`length %below(bytestring_bound)
get(s, (i: below(length(s)))): byte = s`seq(i)
null: bytestring = (# length := 0, seq := (LAMBDA (i: below(0))->byte: 0) #)
length_null: LEMMA length(null) = 0
unit(b): bytestring = (# length := 1, seq := (LAMBDA (i : below(1))->byte: b) #)
% CONVERSION+ bytestrings.unit
length_unit: LEMMA length(unit(b)) = 1
unit_ax: LEMMA get(unit(b), 0) = b
extensionality: LEMMA
s1 = s2 IFF (length(s1) = length(s2) AND ∀ (i:below(length(s1))): get(s1, i) = get(s2, i));
bstring: TYPE = {cs : string | cs`length < bytestring_bound AND (∀ (i : below(cs`length)): code(get(cs, i)) < 256)}
mk_bytestring(cs: bstring): bytestring =
(# length := cs`length,
seq := (LAMBDA (i: below(cs`length::below(bytestring_bound)))-> byte: code(get(cs, i))) #)
CONVERSION+ mk_bytestring;
++(s1, (s2 | s2`length + s1`length < bytestring_bound)): bytestring =
IF s1`length = 0 THEN s2
ELSIF s2`length = 0 THEN s1
ELSE (LET n : below(bytestring_bound) = s1`length + s2`length
IN (# length := n,
seq := (LAMBDA (i:below(n))->byte: IF i < s1`length THEN get(s1, i) ELSE get(s2, i - s1`length) ENDIF)
#))
ENDIF
length_concat: LEMMA
FORALL (s2 | s2`length + s1`length < bytestring_bound):
length(s1 ++ s2) = length(s1) + length(s2)
char_concat: LEMMA
(FORALL s1, (s2 | s2`length + s1`length < bytestring_bound), (i: below(length(s1) + length(s2))):
get(s1 o s2, i) =
IF i < length(s1)
THEN get(s1, i)
ELSE get(s2, i - length(s1))
ENDIF)
strdiff_rec(s1, s2, (i : upto(length(s1)) | i <= length(s2))): RECURSIVE
{i : upto(length(s1)) | i <= length(s2)}
= (IF i = length(s1) OR i = length(s2) OR get(s1, i) /= get(s2, i)
THEN i
ELSE strdiff_rec(s1, s2, i + 1)
ENDIF)
MEASURE min(length(s1), length(s2)) - i
strdiff(s1, s2): {i : upto(length(s1)) | i <= length(s2)} = strdiff_rec(s1, s2, 0)
strdiff_eq: LEMMA
FORALL (j: below(strdiff(s1, s2))): get(s1, j) = get(s2, j)
strdiff_neq: LEMMA
(LET i = strdiff(s1, s2) IN
i < min(length(s1), length(s2)) => get(s1, i) /= get(s2, i))
strcmp(s1, s2): subrange(-1, 1) =
(LET i = strdiff(s1, s2)
IN IF (i = length(s1) OR i = length(s2))
THEN IF length(s1) < length(s2) THEN -1 ELSIF length(s1) > length(s2) THEN 1 ELSE 0 ENDIF
ELSIF get(s1, i) < get(s2, i) THEN -1 ELSE 1 ENDIF)
strcmp_eq: LEMMA
strcmp(s1, s2) = 0 => s1 = s2
strcmp_lt: LEMMA
strcmp(s1, s2) = -1 =>
(LET i = strdiff(s1, s2) IN
i < length(s2) AND (i < length(s1) => get(s1, i) < get(s2, i)))
strcmp_gt: LEMMA
strcmp(s1, s2) = 1 =>
(LET i = strdiff(s1, s2) IN
i < length(s1) AND (i < length(s2) => get(s2, i) < get(s1, i)))
prefix(s, (i: upto(length(s)))): bytestring =
(IF i = length(s) THEN s ELSE (# length := i, seq := (LAMBDA (j : below(i))->byte: get(s, j)) #) ENDIF)
length_prefix: LEMMA
(FORALL (i: upto(length(s))):
length(prefix(s, i)) = i)
prefix_ax: LEMMA
FORALL (i: upto(length(s))), (j : below(i)):
get(prefix(s, i), j) = get(s, j)
suffix(s, (i: upto(length(s)))): bytestring =
IF i = 0
THEN s
ELSE (# length := s`length - i,
seq := (LAMBDA (j: below(length(s) - i))->byte: get(s, i + j)) #)
ENDIF
length_suffix: LEMMA
(FORALL (i: upto(length(s))):
length(suffix(s, i)) = length(s) - i)
suffix_ax: LEMMA
FORALL (i: upto(length(s))), (j : below(length(s) - i)):
get(suffix(s, i), j) = get(s, i + j)
substr(s, (i: upto(length(s))), j: subrange(i, length(s))): {s1 | length(s1) = j - i}
= prefix(suffix(s, i), j - i)
ascii_bytestring?(s): bool = FORALL (i : below(length(s))): get(s, i) < 128
ascii_bytestring: TYPE = (ascii_bytestring?)
END bytestrings
% utf8: THEORY
% BEGIN
% utf8_char : TYPE+ = below(0x110000) CONTAINING 0
% % Bounded by bytestring_bound/4, since up to 4 bytes needed for each utf8_char
% utf8_string_bound: MACRO nat = bytestring_bound / 4
% utf8_string: THEORY = gen_strings[utf8_char, <]{{gen_string ::= utf8_string}}
% % utf8_string: TYPE+ = {s: UTF8_string | length(s) < utf8_string_bound}
% % CONTAINING utf8_string.empty
% ascii_utf8_string?(s: utf8_string): bool = FORALL (i : below(length(s))): get(s, i) < 128
% ascii_utf8_string: TYPE+ = (ascii_utf8_string?) CONTAINING utf8_string.empty
% s, s1, s2: VAR bytestring
% b, b1, b2: VAR byte
% u, u1, u2: VAR utf8_string
% c, c1, c2: VAR utf8_char % below(0x110000)
% % Layout of UTF-8 byte sequences - "cp" = "code point"
% % | # bytes | First cp | Last cp | Byte 1 | Byte 2 | Byte 3 | Byte 4 |
% % | 1 | U+0000 | U+007F | 0xxxxxxx | | | |
% % | 2 | U+0080 | U+07FF | 110xxxxx | 10xxxxxx | | |
% % | 3 | U+0800 | U+FFFF | 1110xxxx | 10xxxxxx | 10xxxxxx | |
% % | 4 | U+10000 | U+10FFFF | 11110xxx | 10xxxxxx | 10xxxxxx | 10xxxxxx |
% utf8_ascii_byte?(b): bool = b <= 0x7F
% utf8_two_first_byte?(b): bool = 0xC0 <= b <= 0xDF
% utf8_three_first_byte?(b): bool = 0xE0 <= b <= 0xEF
% utf8_four_first_byte?(b): bool = 0xF0 <= b <= 0xF7
% utf8_trailer_byte?(b): bool = 0x80 <= b <= 0xBF
% at_utf8_ascii_char?(s: bytestring, idx: below(length(s))): bool =
% length(s) > idx and utf8_ascii_byte?(get(s, idx))
% at_utf8_two_byte_char?(s: bytestring, idx: below(length(s))): bool = length(s) > idx+1 and
% utf8_two_first_byte?(get(s, idx)) and utf8_trailer_byte?(get(s, idx+1))
% at_utf8_three_byte_char?(s: bytestring, idx: below(length(s))): bool = length(s) > idx+2 and
% utf8_three_first_byte?(get(s, idx)) and
% utf8_trailer_byte?(get(s, idx+1)) and utf8_trailer_byte?(get(s, idx+2))
% at_utf8_four_byte_char?(s: bytestring, idx: below(length(s))): bool = length(s) > idx+3 and
% utf8_four_first_byte?(get(s, idx)) and utf8_trailer_byte?(get(s, idx+1)) and
% utf8_trailer_byte?(get(s, idx+2)) and utf8_trailer_byte?(get(s, idx+3))
% next_code_point(bs: bytestring, idx: below(length(bs))):
% [utf8_char, {x: upto(4) | idx + x < length(bs)}] =
% if at_utf8_ascii_char?(bs, idx) then (get(bs, idx), 1)
% elsif at_utf8_two_byte_char?(bs, idx)
% then ((get(bs, idx) - 0xc0) * 0x40 + (get(bs, idx+1) - 0x80), 2)
% elsif at_utf8_three_byte_char?(bs, idx)
% then ((get(bs, idx) - 0xe0) * 0x1000 + (get(bs, idx+1) - 0x80) * 0x40 + (get(bs, idx+2) - 0x80), 3)
% elsif at_utf8_four_byte_char?(bs, idx)
% then let cp = (get(bs, idx) - 0xf0) * 0x40000 + (get(bs, idx+1) - 0x80) * 0x1000
% + (get(bs, idx+2) - 0x80) * 0x40 + (get(bs, idx+3) - 0x80)
% % could be larger, but by RCF 3629 it matches limits of utf-16
% in if cp < 0x110000
% then (cp, 4)
% else (0, 0)
% endif
% else (0, 0)
% endif
% bytestring_to_utf8_string_rec(s: bytestring | length(s) < utf8_string_bound - 1,
% idx: upto(length(s)),
% u: utf8_string | length(u) <= idx):
% recursive utf8_string =
% if idx = length(s)
% then u
% else let (ch, len) = next_code_point(s, idx)
% in if len = 0 % not a valid UTF-8 bytestring at this point
% then utf8_string.empty
% else bytestring_to_utf8_string_rec(s, idx + len, u + utf8_string.unit(ch))
% endif
% endif
% measure length(s) - idx
% % Takes a random bytestring, returns a utf8_string if it's a valid utf8 bytestring
% % returns empty otherwise.
% bytestring_to_utf8_string(s: bytestring | length(s) < utf8_string_bound - 1): utf8_string =
% bytestring_to_utf8_string_rec(s, 0, utf8_string.empty)
% %%
% codepoint_to_bytestring(cp: below(0x110000)): {s: bytestring | 1 <= length(s) <= 4} =
% if cp < 0x80 then unit(cp)
% elsif cp < 0x800
% then let % 11 bits, 5 in first byte, 6 in second
% b1 = 0xC0 + ndiv(cp, 64),
% b2 = 0x80 + nrem(cp, 64)
% in unit(b1) + unit(b2)
% elsif cp < 0x10000
% then let % 16 bits, 4 in first byte, 6 in each of rest
% b1 = 0xE0 + ndiv(cp, 0x1000), %exp2(12)
% b12 = nrem(cp, 0x1000),
% b2 = 0x80 + ndiv(b12, 64),
% b3 = 0x80 + nrem(b12, 64)
% in unit(b1) + unit(b2) + unit(b3)
% else
% let % 21 bits, 3 in first byte, 6 in each of rest
% b1 = 0xF0 + ndiv(cp, 0x40000), % exp2(18)
% b18 = nrem(cp, 0x40000),
% b2 = 0x80 + ndiv(b18, 0x1000), % exp2(12)
% b12 = nrem(b18, 0x1000),
% b3 = 0x80 + ndiv(b12, 64),
% b4 = 0x80 + nrem(b12, 64)
% in unit(b1) + unit(b2) + unit(b3) + unit(b4)
% endif
% utf8_string_to_bytestring_rec(u: utf8_string | 4*length(u) < 0x100000000 - 4,
% idx: upto(length(u)),
% s: bytestring | length(s) <= 4*idx):
% recursive bytestring =
% if idx = length(u)
% then s
% else utf8_string_to_bytestring_rec(u, idx + 1, s + codepoint_to_bytestring(get(u, idx)))
% endif
% measure length(u) - idx
% utf8_string_to_bytestring(u: utf8_string | 4*length(u) < 0x100000000 - 4): bytestring =
% utf8_string_to_bytestring_rec(u, 0, empty)
% END utf8
% string_map: THEORY
% BEGIN
% s, s1, s2: VAR string
% c, c1, c2: VAR char
% string_to_utf8_string_rec(s: string | s`length < utf8_string_bound,
% idx: upto(s`length),
% u: utf8_string | length(u) = idx)
% : RECURSIVE {u1: utf8_string | length(u1) = s`length}
% = if idx = s`length
% then u
% else string_to_utf8_string_rec(s, idx + 1, u + unit(code(s`seq(idx))))
% endif
% measure s`length - idx
% string_to_utf8_string(s: string | s`length < utf8_string_bound)
% : {u: utf8_string | length(u) = s`length}
% = string_to_utf8_string_rec(s, 0, empty)
% utf8_string_to_string_rec(u: utf8_string,
% idx: upto(length(u)),
% s: string | s`length = idx)
% : RECURSIVE {s1: string | s1`length = length(u)}
% = if idx = length(u)
% then s
% else utf8_string_to_string_rec(u, idx + 1, add(char(get(u, idx)), s))
% endif
% measure length(u) - idx
% utf8_string_to_string(u: utf8_string) : {s: string | length(u) = s`length}
% = utf8_string_to_string_rec(u, 0, empty_seq)
% get(s, (i: below(length(s)))): char = s`seq(i);
% <(c1, c2): bool = code(c1) < code(c2);
% <=(c1, c2): bool = code(c1) <= code(c2);
% >(c1, c2): bool = code(c1) > code(c2);
% >=(c1, c2): bool = code(c1) >= code(c2);
% strdiff_rec(s1, s2, (idx: upto(min(length(s1), length(s2))))):
% recursive subrange(idx, min(length(s1), length(s2))) =
% if idx < min(length(s1), length(s2))
% then if s1`seq(idx) = s2`seq(idx)
% then strdiff_rec(s1, s2, idx+1)
% else idx
% endif
% else idx
% endif
% measure min(length(s1), length(s2)) - idx
% strdiff_eq_rec: LEMMA
% FORALL (i: upto(min(length(s1), length(s2)))):
% i < strdiff_rec(s1, s2, i) => s1`seq(i) = s2`seq(i)
% strdiff_eq_rec2: LEMMA
% LET i = strdiff_rec(s1, s2, 0)
% IN FORALL (k: below(i)): strdiff_rec(s1, s2, k) = i
% strdiff_eq_rec2a: LEMMA
% FORALL (i: upto(min(length(s1), length(s2)))):
% i <= strdiff_rec(s1, s2, i)
% strdiff_eq_rec2b: LEMMA
% FORALL (i: upto(min(length(s1), length(s2)))):
% i = strdiff_rec(s1, s2, 0) =>
% i = strdiff_rec(s1, s2, i)
% strdiff_eq_rec3: LEMMA
% LET i = strdiff_rec(s1, s2, 0)
% IN i < min(length(s1), length(s2)) => s1`seq(i) /= s2`seq(i)
% strdiff(s1, s2): upto(min(length(s1), length(s2))) =
% strdiff_rec(s1, s2, 0)
% strcmp(s1, s2): subrange(-1, 1) =
% IF s1 = s2 THEN 0
% ELSE LET i = strdiff(s1, s2),
% minl = min(length(s1), length(s2))
% IN IF i < minl
% THEN IF get(s1, i) < get(s2, i) THEN -1 ELSE 1 ENDIF
% ELSIF length(s1) < length(s2) THEN -1 ELSE 1 ENDIF
% ENDIF
% prefix(s, (i: upto(length(s)))): string = s^^(0, i)
% suffix(s, (i: upto(length(s)))): string = s^^(i, length(s))
% importing gen_strings[char, <]
% {{gen_string := string,
% length(s) := s`length,
% get := get,
% empty := "",
% unit(c) := add(c, ""),
% + := o,
% strdiff := strdiff,
% strcmp := strcmp,
% prefix := prefix,
% suffix := suffix}}
% END string_map
lift[T: TYPE]: DATATYPE
BEGIN
bottom: bottom?
up(down: T): up?
END lift
union[T1, T2: TYPE]: DATATYPE
BEGIN
inl(left: T1): inl?
inr(right: T2): inr?
END union
tostring[T: TYPE]: THEORY
BEGIN
%This theory and the tostring operation are just place-holders for semantic attachment.
%If the result is too big to fit within the bytestring limit, then we assume that the
%operation only retains a portion of the true string output. There is no claim that this
%operation is injective.
tostring(x: T): bytestring
END tostring
file: THEORY
BEGIN
% void_action: TYPE+
% null_action: void_action
% file_descriptor : TYPE+ %uninterpreted
file: TYPE+ %= [# name: bytestring, capacity: index,
% fd : file_descriptor, contents : bytestring #]
% max_file_size: uint32 %defined by semantic attachment in c-primitive-attachments
lifted_file: DATATYPE
BEGIN
fail: fail?
pass(contents: file): pass?
END lifted_file
f, f1, f2: VAR file
open?(f): bool % semantically attached predicate that checks if a file handle is open
name(f): bytestring
file_size(f: file): index
%The operations open, setbyte, and append can fail if the file parameter is live beyond the operation
open(name: bytestring): lifted_file %uninterpreted with semantic attachment
% don't need to close the file. This is handled by reference counting.
%Same as open, but creates a new file or overwrites an existing one
create(name: bytestring): lifted_file %uninterpreted with semantic attachment
setbyte(f: file, (i : below(file_size(f))), (b: byte)): lifted_file
append(f: file, b : bytestring): lifted_file % adds to the end of a writable file by remapping if needed.
%These file operations are benign and can appear anywhere.
getbyte(f: file, (i : below(file_size(f)))): byte
%The signature for the size parameter has to be detectably uint32 for the C attachment to work
getbytestring(f: file, (i : upto(file_size(f))), (size : upto(file_size(f)) | size <= file_size(f) - i)):
{bystr: bytestring | bystr`length = size}
readline(f: file, (i : below(file_size(f)))): bytestring
printc(b : bytestring): bytestring %prints characters
printh(b : bytestring): bytestring %prints bytes
END file
% Defines fixpoints for sets, needed to support the mucalculus model checker.
mucalculus[T:TYPE]: THEORY
BEGIN
s: VAR T
p, p1, p2: VAR pred[T]
predicate_transformer: TYPE = [pred[T]->pred[T]]
pt: VAR predicate_transformer
setofpred: VAR pred[pred[T]]
<=(p1,p2): bool = FORALL s: p1(s) IMPLIES p2(s)
monotonic?(pt): bool =
FORALL p1, p2: p1 <= p2 IMPLIES pt(p1) <= pt(p2)
pp: VAR (monotonic?)
fixpoint?(pp, p): bool = (pp(p) = p)
fixpoint?(pp)(p): bool = fixpoint?(pp, p)
glb(setofpred): pred[T] =
LAMBDA s: (FORALL p: member(p,setofpred) IMPLIES p(s))
% least fixpoint
lfp(pp): pred[T] = glb({p | pp(p) <= p})
lfp_induction: FORMULA pp(p) <= p IMPLIES lfp(pp) <= p
mu(pp): pred[T] = lfp(pp)
lfp?(pp, p1): bool =
fixpoint?(pp, p1) AND FORALL p2: fixpoint?(pp,p2) IMPLIES p1 <= p2
lfp?(pp)(p1): bool = lfp?(pp, p1)
lub(setofpred): pred[T] = LAMBDA s: EXISTS p: member(p,setofpred) AND p(s)
% greatest fixpoint
gfp(pp): pred[T] = lub({p | p <= (pp(p))})
gfp_induction: FORMULA p <= pp(p) IMPLIES p <= gfp(pp)
nu(pp): pred[T] = gfp(pp)
gfp?(pp, p1): bool =
fixpoint?(pp,p1) AND FORALL p2: fixpoint?(pp,p2) IMPLIES p2 <= p1
gfp?(pp)(p1): bool = gfp?(pp, p1)
END mucalculus
% Basic CTL temporal operators (without fairness) defined in mu-calculus
ctlops[state : TYPE]: THEORY
BEGIN
u,v,w: VAR state
f,g,Q,P,p1,p2: VAR pred[state]
Z: VAR pred[[state, state]]
N: VAR [state, state -> bool]
CONVERSION+ K_conversion
EX(N,f)(u):bool = (EXISTS v: (f(v) AND N(u, v)))
EG(N,f):pred[state] = nu(LAMBDA Q: (f AND EX(N,Q)))
EU(N,f,g):pred[state] = mu(LAMBDA Q: (g OR (f AND EX(N,Q))))
% Other operator definitions
EF(N,f):pred[state] = EU(N, TRUE, f)
AX(N,f):pred[state] = NOT EX(N, NOT f)
AF(N,f):pred[state] = NOT EG(N, NOT f)
AG(N,f):pred[state] = NOT EF(N, NOT f)
AU(N,f,g):pred[state] = NOT EU(N, NOT g, (NOT f AND NOT g)) AND AF(N, g)
CONVERSION- K_conversion
END ctlops
% Fair versions of CTL operators where
% fairAG(N, f)(Ff)(s) means f always holds along every N-path
% from s along which the fairness predicate Ff holds infinitely
% often. This is different from the usual linear-time notion of
% fairness where the strong form asserts that if an action A is
% enabled infinitely often, it is taken infinitely often, and the
% weak form asserts that if any action that is continuously enabled
% is taken infinitely often.
fairctlops [ state : TYPE ]: THEORY
BEGIN
u,v,w: VAR state
f,g,Q,P,p1,p2: VAR pred[state]
N: VAR [state, state->bool]
Ff: VAR pred[state] % Fair formula
CONVERSION+ K_conversion
fairEG(N, f)(Ff): pred[state] =
nu(LAMBDA P: EU(N, f, f AND Ff AND EX(N, P)))
fairAF(N,f)(Ff):pred[state] = NOT fairEG(N, NOT f)(Ff)
fair?(N,Ff):pred[state] = fairEG(N,LAMBDA u: TRUE)(Ff)
fairEX(N,f)(Ff):pred[state] = EX(N,f AND fair?(N,Ff))
fairEU(N,f,g)(Ff):pred[state] = EU(N,f,g AND fair?(N,Ff))
fairEF(N,f)(Ff):pred[state] = EF(N,f AND fair?(N,Ff))
fairAX(N,f)(Ff):pred[state] = NOT fairEX(N, NOT f)(Ff)
fairAG(N,f)(Ff):pred[state] = NOT fairEF(N,NOT f)(Ff)
fairAU(N,f,g)(Ff):pred[state] =
NOT fairEU(N,NOT g,NOT f AND NOT g)(Ff)
AND fairAF(N,g)(Ff)
CONVERSION- K_conversion
END fairctlops
% Fair versions of CTL operators with lists of fairness conditions.
% FairAG(N,f)(Fflist)(s) means f always holds on every N-path from
% s along which each predicate in Fflist holds infinitely often.
Fairctlops[state : TYPE]: THEORY
BEGIN
u,v,w: VAR state
f,g,Q,P,p1,p2: VAR pred[state]
N: VAR [state, state->bool]
Fflist, Gflist: VAR list[pred[state]] % Fair formula
CONVERSION+ K_conversion
CheckFair(Q, N, f, Fflist): RECURSIVE pred[state] =
(CASES Fflist OF
cons(Ff, Gflist):
EU(N, f, f AND Ff AND
EX(N, CheckFair(Q, N, f, Gflist))),
null : Q
ENDCASES)
MEASURE length(Fflist)
FairEG(N, f)(Fflist): pred[state] =
nu(LAMBDA P: CheckFair(P, N, f, Fflist))
FairAF(N,f)(Fflist):pred[state] = NOT FairEG(N, NOT f)(Fflist)
Fair?(N,Fflist):pred[state] = FairEG(N,LAMBDA u: TRUE)(Fflist)
FairEX(N,f)(Fflist):pred[state] = EX(N,f AND Fair?(N,Fflist))
FairEU(N,f,g)(Fflist):pred[state] = EU(N,f,g AND Fair?(N,Fflist))
FairEF(N,f)(Fflist):pred[state] = EF(N,f AND Fair?(N,Fflist))
FairAX(N,f)(Fflist):pred[state] = NOT FairEX(N, NOT f)(Fflist)
FairAG(N,f)(Fflist):pred[state] = NOT FairEF(N,NOT f)(Fflist)
FairAU(N,f,g)(Fflist):pred[state] =
NOT FairEU(N,NOT g,NOT f AND NOT g)(Fflist)
AND FairAF(N,g)(Fflist)
% Turn off K_conversion so that it is not a conversion by default.
CONVERSION- K_conversion
END Fairctlops
bit: THEORY
% -----------------------------------------------------------------------
% The bit theory defines bits and their properties. Bits are interpreted
% as the natural numbers 0 and 1.
% -----------------------------------------------------------------------
BEGIN
bit : TYPE = bool
nbit : TYPE = below(2) % could be {n: nat | n = 0 OR n = 1}
b: VAR bit
bit_cases: LEMMA b = FALSE OR b = TRUE
b0: [below(1) -> bit] = (LAMBDA (i: below(1)): FALSE)
b1: [below(1) -> bit] = (LAMBDA (i: below(1)): TRUE)
b2n(b:bool) : nbit = IF b THEN 1 ELSE 0 ENDIF
n2b(nb: nbit) : bool = (nb = 1)
%CONVERSION b2n
END bit
%------------------------------------------------------------------------
%
% Definition of a bitvector
% -----------------------------------------
%
% Defines:
%
% bvec: TYPE = [below(N) -> bit]
%
% ^(bv, (i: below(N))): bit
%
% Establishes:
%
%
%------------------------------------------------------------------------
bv[N: nat]: THEORY
BEGIN
CONVERSION+ b2n
bvec : TYPE = [below(N) -> bit]
b: VAR bit
bv: VAR bvec
i: VAR below[N]
bvec0(i): bit = FALSE
bvec1(i): bit = TRUE
fill(b)(i): bit = b;
%-----------------------------------------------------------------------
% The implementation of the bitvector can be hidden through use of
% the ^ function below.
%-----------------------------------------------------------------------
^(bv, i): bit = bv(i)
CONVERSION- b2n
END bv
% bv_cnv: THEORY
% BEGIN
% CONVERSION fill[1]
% END bv_cnv
bv_concat_def [n:nat, m:nat ]: THEORY
%------------------------------------------------------------------------
% This theory defines the concatenation operator o for bitvectors:
%
% o: [bvec[n], bvec[m] -> bvec[n+m]]
%
% The theory is instantiated with the sizes of the input bit vectors.
%------------------------------------------------------------------------
BEGIN
o(bvn: bvec[n], bvm: bvec[m]): bvec[n+m] =
(LAMBDA (nm: below(n+m)): IF nm < m THEN bvm(nm)
ELSE bvn(nm - m)
ENDIF)
END bv_concat_def
bv_bitwise [N: nat] : THEORY
% -----------------------------------------------------------------------
% Defines bit-wise logical operations on bit vectors.
%
% Introduces:
% OR : bv1 OR bv2
% & : bv1 & bv2
% IFF: bv1 IFF bv2
% NOT: NOT bv1
% XOR: bv1 XOR bv2
% -----------------------------------------------------------------------
BEGIN
i: VAR below(N)
OR(bv1,bv2: bvec[N]) : bvec[N] = (LAMBDA i: bv1(i) OR bv2(i));
AND(bv1,bv2: bvec[N]): bvec[N] = (LAMBDA i: bv1(i) AND bv2(i)) ;
IFF(bv1,bv2: bvec[N]): bvec[N] = (LAMBDA i: bv1(i) IFF bv2(i)) ;
NOT(bv: bvec[N]) : bvec[N] = (LAMBDA i: NOT bv(i)) ;
XOR(bv1,bv2: bvec[N]): bvec[N] = (LAMBDA i: XOR(bv1(i),bv2(i))) ;
% === The following lemmas can be used to hide the implementation
% details of the bitvector
bv, bv1, bv2: VAR bvec[N]
bv_OR : LEMMA (bv1 OR bv2)^i = (bv1^i OR bv2^i)
bv_AND : LEMMA (bv1 AND bv2)^i = (bv1^i AND bv2^i)
bv_IFF : LEMMA (bv1 IFF bv2)^i = (bv1^i IFF bv2^i)
bv_XOR : LEMMA XOR(bv1,bv2)^i = XOR(bv1^i,bv2^i)
bv_NOT : LEMMA (NOT bv)^i = NOT(bv^i)
END bv_bitwise
%------------------------------------------------------------------------
%
% Interpretation of a bitvector as a natural number
% -------------------------------------------------
%
% Defines:
%
% bv2nat: function[bvec[N] -> below(exp2(N))]
% nat2bv: function[below(exp2(N)) -> bvec[N]]
%
% Establishes:
%
% bv2nat_bij: THEOREM bijective?(bv2nat)
% bv2nat_inv: THEOREM bv2nat(nat2bv(val)) = val
%
%
% See note at end of theory for reasons why nat2bv should be avoided
% in specifications.
%
%------------------------------------------------------------------------
bv_nat[N: nat]: THEORY
BEGIN
CONVERSION+ b2n
% === Interpretation of a bit vector as a natural number ================
bv2nat_rec(n: upto(N), bv:bvec[N]): RECURSIVE nat =
IF n = 0 THEN 0
ELSE exp2(n-1) * bv^(n-1) + bv2nat_rec(n - 1, bv)
ENDIF
MEASURE n
bv_lem: LEMMA FORALL (n: below(N), bv: bvec[N]): bv(n) = FALSE OR bv(n) = TRUE
bv2nat_rec_bound: LEMMA FORALL (n: upto(N), bv: bvec[N]):
bv2nat_rec(n, bv) < exp2(n)
bv2nat(bv:bvec[N]): below(exp2(N)) = bv2nat_rec(N, bv)
% ===== Properties of bv2nat ===================================
n : VAR upto(N)
val : VAR below(exp2(N))
bv, bv1, bv2: VAR bvec[N]
bv2nat_inj_rec: LEMMA
bv2nat_rec(n, bv1) = bv2nat_rec(n, bv2)
<=> (FORALL (m: below(N)): (m < n) IMPLIES bv1(m) = bv2(m))
bv2nat_surj_rec: LEMMA FORALL (y:below(exp2(n))):
EXISTS bv:bv2nat_rec(n, bv) = y
bv2nat_inj : THEOREM % injective?(bv2nat)
(FORALL (x, y: bvec[N]): (bv2nat(x) = bv2nat(y)
IMPLIES (x = y)))
bv2nat_surj : THEOREM % surjective?(bv2nat)
(FORALL (y: below(exp2(N))):
(EXISTS (x: bvec[N]): bv2nat(x) = y))
bv2nat_bij : THEOREM bijective?(bv2nat)
bv2nat_rec_fill_F : LEMMA bv2nat_rec(n, fill[N](FALSE)) = 0
bv2nat_rec_fill_T : LEMMA bv2nat_rec(n, fill[N](TRUE)) = exp2(n)-1
bv2nat_fill_F : LEMMA bv2nat(fill[N](FALSE)) = 0
bv2nat_fill_T : LEMMA bv2nat(fill[N](TRUE)) = exp2(N)-1
bv2nat_eq0 : LEMMA bv2nat(bv) = 0 IMPLIES (bv = fill[N](FALSE))
bv2nat_eq_max : LEMMA bv2nat(bv) = exp2(N)-1 IMPLIES bv = (fill[N](TRUE))
bv2nat_top_bit : THEOREM N > 0 IMPLIES
IF bv2nat(bv) < exp2(N-1) THEN bv^(N-1) = FALSE
ELSE bv^(N-1) = TRUE ENDIF
bv2nat_topbit : THEOREM N > 0 IMPLIES bv^(N-1) = (bv2nat(bv) >= exp2(N-1))
% =================== Properties of nat2bv ===================================
nat2bv(val: below(exp2(N))): {bv: bvec[N] | bv2nat(bv) = val}
nat2bv_def : LEMMA nat2bv = inverse(bv2nat)
nat2bv_bij : THEOREM bijective?[below(exp2(N)),bvec[N]](nat2bv)
nat2bv_inv : THEOREM nat2bv(bv2nat(bv)) = bv
nat2bv_rew : LEMMA nat2bv(val) = bv IFF bv2nat(bv) = val
bv2nat_inv : THEOREM bv2nat(nat2bv(val)) = val
CONVERSION- b2n
END bv_nat
empty_bv: THEORY
BEGIN
empty_bv: [below[0] -> bool] = (LAMBDA (x: below[0]): TRUE) ;
END empty_bv
bv_caret[N: nat]: THEORY
%-----------------------------------------------------------------------
% An extractor operation decomposes a bvec into smaller
% bit vectors. In the following, we define a number of
% extractors for bvec.
%
% Introduces:
% bv^(m,n) creates bv[m-n+1] from bits m through n
%
% bv^^(m,n) can return an empty bitvector if n > m
%
%-----------------------------------------------------------------------
BEGIN
%-----------------------------------------------------------------------
% The following operator (^) extracts a contiguous fragment of
% a bit vector between two given positions.
%-----------------------------------------------------------------------
% ^(bv: bvec[N], p:[m: below(N), upto(m)]): bvec[LET (m, n) = p IN m - n + 1] =
% LET (m, n) = p IN
% (LAMBDA (ii: below(m - n + 1)): bv(ii + n)) ;
^(bv: bvec[N], sp:[i1: below(N), upto(i1)]): bvec[proj_1(sp)-proj_2(sp)+1] =
(LAMBDA (ii: below(proj_1(sp) - proj_2(sp) + 1)):
bv(ii + proj_2(sp))) ;
% ^^(bv: bvec[N], p:[m:below[N],nat]): bvec[LET (m, n) = p IN
% IF m < n THEN 0 ELSE m - n + 1 ENDIF] =
% LET (m, n) = p IN
% IF m < n THEN empty_bv
% ELSE (LAMBDA (ii: below[m-n+1]): bv(ii + n))
% ENDIF
% === Useful Lemmas and Theorems =========================================
bv: VAR bvec[N]
bv_caret_all : LEMMA N > 0 IMPLIES bv^(N-1, 0) = bv
% dcaret_lem : LEMMA (FORALL (i: below(N), j: upto(i)): bv^^(i,j) = bv^(i,j))
bv_caret_ii_0 : LEMMA (FORALL (i: below(N)): bv^(i,i)^0 = bv^i)
bv_caret_elim : LEMMA (FORALL (i: below(N), j: upto(i), k: below(i-j+1)):
bv ^ (i, j) ^ k = bv^(j+k))
END bv_caret
integer_bv_ops: THEORY
BEGIN
x8, y8, z8: VAR uint8
x16, y16, z16: VAR uint16
x32, y32, z32: VAR uint32
x64, y64, z64: VAR uint64
u8xor(x8, y8): uint8 = bv2nat[8](XOR(nat2bv(x8), nat2bv(y8)))
u16xor(x16, y16): uint16 = bv2nat[16](XOR(nat2bv(x16), nat2bv(y16)))
u32xor(x32, y32): uint32 = bv2nat[32](XOR(nat2bv(x32), nat2bv(y32)))
u64xor(x64, y64): uint64 = bv2nat[64](XOR(nat2bv(x64), nat2bv(y64)))
u8and(x8, y8): uint8 = bv2nat[8](AND(nat2bv(x8), nat2bv(y8)))
u16and(x16, y16): uint16 = bv2nat[16](AND(nat2bv(x16), nat2bv(y16)))
u32and(x32, y32): uint32 = bv2nat[32](AND(nat2bv(x32), nat2bv(y32)))
u64and(x64, y64): uint64 = bv2nat[64](AND(nat2bv(x64), nat2bv(y64)))
u8or(x8, y8): uint8 = bv2nat[8](OR(nat2bv(x8), nat2bv(y8)))
u16or(x16, y16): uint16 = bv2nat[16](OR(nat2bv(x16), nat2bv(y16)))
u32or(x32, y32): uint32 = bv2nat[32](OR(nat2bv(x32), nat2bv(y32)))
u64or(x64, y64): uint64 = bv2nat[64](OR(nat2bv(x64), nat2bv(y64)))
u8not(x8): uint8 = bv2nat(NOT(nat2bv(x8)));
u16not(x16): uint16 = bv2nat(NOT nat2bv[16](x16));
u32not(x32): uint32 = bv2nat(NOT(nat2bv[32](x32)));
u64not(x64): uint64 = bv2nat(NOT(nat2bv[64](x64)));
END integer_bv_ops
mod: THEORY
%------------------------------------------------------------------------
%
% mod function as defined in `Concrete Mathematics'
% The Ada definition of mod is consistent with this definition
%
% Author:
% Paul S. Miner | email: p.s.miner@larc.nasa.gov
% 1 South Wright St. / MS 130 | fax: (804) 864-4234
% NASA Langley Research Center | phone: (804) 864-6201
% Hampton, Virginia 23681 |
%------------------------------------------------------------------------
BEGIN
i,k,cc: VAR int
m: VAR posnat
n,a,b,c,x: VAR nat
j: VAR nonzero_integer
ml3: LEMMA abs(i - m * floor(i/m)) < m
ml4: LEMMA abs(i + m * floor(-i/m)) < m
mod(i,j): {k| abs(k) < abs(j)} = i-j*floor(i/j)
mod_pos: LEMMA mod(i,m) >= 0 AND mod(i,m) < m
JUDGEMENT mod(i:int, m: posnat) HAS_TYPE below(m)
mod_even : LEMMA integer_pred(i/j) IMPLIES mod(i,j) = 0
mod_neg : LEMMA mod(-i,j) = IF integer_pred(i/j) THEN 0
ELSE j - mod(i,j)
ENDIF
mod_neg_d : LEMMA mod(i,-j) = IF integer_pred(i/j) THEN 0
ELSE mod(i,j) - j
ENDIF
mod_eq_arg : LEMMA mod(j,j) = 0
mod_lt : LEMMA abs(i) < abs(j) IMPLIES mod(i,j) =
IF sgn(i) = sgn(j) OR i = 0 THEN i
ELSE i + j
ENDIF
mod_lt_nat : LEMMA n < m IMPLIES mod(n,m) = n
mod_lt_int : LEMMA -m < i AND i < m IMPLIES mod(i,m) =
IF i >= 0 THEN i ELSE i + m
ENDIF
mod_sum_pos: LEMMA mod(i+k*m,m) = mod(i,m)
mod_gt : LEMMA m <= i AND i < 2*m IMPLIES mod(i,m) = i-m
mod_sum : LEMMA mod(i+k*j,j) = mod(i,j)
mod_sum_nat: LEMMA (FORALL (n1,n2: below(m)):
mod(n1+n2,m) = IF n1 + n2 < m THEN n1+n2
ELSE n1 + n2 - m
ENDIF)
mod_it_is : LEMMA a = b + m*c AND b < m IMPLIES
b = mod(a,m)
mod_zero : LEMMA mod(0,j) = 0
mod_one : LEMMA mod(1,j) = IF abs(j) = 1 THEN 0
ELSIF j > 0 THEN 1
ELSE j + 1
ENDIF
mod_of_mod : LEMMA mod(i + mod(k,m), m) = mod(i+k, m)
mod_of_mod_neg : LEMMA mod(i - mod(k,m), m) = mod(i-k, m)
mod_inj_plus : LEMMA a < m AND n < m AND c < m AND
mod(a + n, m) = mod(a + c, m) IMPLIES n = c
mod_inj_minus : LEMMA a < m AND n < m AND c < m AND
mod(a - n, m) = mod(a - c, m) IMPLIES n = c
mod_wrap_around: LEMMA n < m AND (c <= m AND c >= m-n) IMPLIES
mod(n+c, m) = n - (m-c)
mod_wrap2: LEMMA c < m IMPLIES mod(m+c, m) = c
% Injection-like properties for mod for limited ranges
mod_inj1: LEMMA x < m AND n < m AND c < m AND
mod(x + n, m) = mod(x + c, m) IMPLIES n = c
mod_inj2: LEMMA x < m AND n < m AND c < m AND
mod(x - n, m) = mod(x - c, m) IMPLIES n = c
mod_wrap_inj: LEMMA n < m AND a < m AND b < m AND a > 0 AND
mod(n + a, m) = mod(n - b, m) IMPLIES a + b = m
mod_wrap_inj_eq: LEMMA
x < m AND a < m AND b < m AND a > 0
IMPLIES (mod(x + a, m) = mod(x - b, m)) = (a + b = m)
kk, vv: VAR nat
mod_neg_limited: LEMMA 0 <= kk AND kk < m AND vv < m AND
vv - kk < 0 IMPLIES mod(vv - kk,m) = m + vv - kk
odd_mod: LEMMA even?(m) => (odd?(mod(i, m)) IFF odd?(i))
even_mod: LEMMA even?(m) => (even?(mod(i, m)) IFF even?(i))
mj: VAR posnat
mod_mult : LEMMA mod(mod(i,mj*m),m) = mod(i,m)
END mod
%------------------------------------------------------------------------
%
% Natural arithmetic over bitvectors
% -----------------------------------------
%
% Defines:
%
% > : bv1 > bv2
% >=: bv1 >= bv2
% < : bv1 < bv2
% <=: bv1 <= bv1
% + : bv1 + i
% - : bv1 - i
% + : bv1 + bv2
% * : bv1 * bv2
%
% Establishes:
%
% bv_plus : LEMMA bv2nat(bv + i) = mod(bv2nat(bv) + i, exp2(N)))
%
% bv_add : LEMMA bv2nat(bv1 + bv2) =
% IF bv2nat(bv1) + bv2nat(bv2) < exp2(N)
% THEN bv2nat(bv1) + bv2nat(bv2)
% ELSE bv2nat(bv1) + bv2nat(bv2) - exp2(N) ENDIF
%
%
% Note that + has been defined in a manner that avoids the introduction of
% nat2bv. Also nat2bv has been defined in a manner that prevents GRIND from
% expanding nat2bv into an expression involving "epsilon". The needed
% property about nat2bv is available in its type.
%
%------------------------------------------------------------------------
bv_arith_nat_defs[N: nat]: THEORY
BEGIN
% ----- Definition of inequalities over the bit vectors.
< (bv1: bvec[N], bv2: bvec[N]): bool = bv2nat(bv1) < bv2nat(bv2) ;
<=(bv1: bvec[N], bv2: bvec[N]): bool = bv2nat(bv1) <= bv2nat(bv2) ;
> (bv1: bvec[N], bv2: bvec[N]): bool = bv2nat(bv1) > bv2nat(bv2) ;
>=(bv1: bvec[N], bv2: bvec[N]): bool = bv2nat(bv1) >= bv2nat(bv2) ;
% ----- Increments a bit vector by a integer modulo 2**N
+(bv: bvec[N], i: int): {bvn: bvec[N] |
bv2nat(bvn) = mod(bv2nat(bv) + i, exp2(N))}
bv_plus : LEMMA (FORALL (bv: bvec[N], i: int):
bv2nat(bv + i) = mod(bv2nat(bv) + i, exp2(N))) ;
% ----- Decrements a bit vector by a integer modulo 2**N.
-(bv: bvec[N], i: int): bvec[N] = bv + (-i) ;
bv_minus : LEMMA (FORALL (bv: bvec[N], i: int):
bv2nat(bv - i) = mod(bv2nat(bv) - i, exp2(N))) ;
% ----- Addition of two bit vectors interpreted as natural numbers.
+(bv1: bvec[N], bv2: bvec[N]): {bv: bvec[N] | bv2nat(bv) =
IF bv2nat(bv1) + bv2nat(bv2) < exp2(N)
THEN bv2nat(bv1) + bv2nat(bv2)
ELSE bv2nat(bv1) + bv2nat(bv2) - exp2(N)
ENDIF}
% ----- Multiplication of two bit vectors interpreted as natural numbers.
*(bv1: bvec[N], bv2: bvec[N]): {bv: bvec[2*N] | bv2nat(bv) =
bv2nat(bv1) * bv2nat(bv2)} ;
% Properties of these functions are in the bitvector library
END bv_arith_nat_defs
%------------------------------------------------------------------------
%
% Integer interpretation of a bitvector (twos-complement interpretation)
% ----------------------------------------------------------------------
%
% Defines:
%
% minint: int = -exp2(N-1)
% maxint: int = exp2(N-1) - 1
% rng_2s_comp: TYPE = {i: int | minint <= i AND i <= maxint}
% bv2int : [bvec[N] -> rng_2s_comp]
% int2bv : [rng_2s_comp -> bvec[N]]
%
% Establishes:
%
% bv2int_bij : THEOREM bijective?(bv2int)
% bv2int_inv : THEOREM bv2int(int2bv(iv))=iv
%
% Note. The int2bv should be avoided in practice. It is necessary
% for the development of the library.
%
%------------------------------------------------------------------------
bv_int_defs[N: posnat]: THEORY
BEGIN
minint: int = -exp2(N-1)
maxint: int = exp2(N-1) - 1
bv_maxint_to_minint: LEMMA maxint = -minint - 1
bv_minint_to_maxint: LEMMA minint = -maxint - 1
in_rng_2s_comp(i: int): bool = (minint <= i AND i <= maxint)
rng_2s_comp: TYPE = {i: int | minint <= i AND i <= maxint}
bv2int(bv: bvec[N]): rng_2s_comp = IF bv2nat(bv) < exp2(N-1) THEN bv2nat(bv)
ELSE bv2nat(bv) - exp2(N) ENDIF
int2bv(iv: rng_2s_comp): {bv: bvec[N] | bv2int(bv) = iv}
END bv_int_defs
%------------------------------------------------------------------------
%
% Defines functions over bit vectors interpreted as natural numbers.
%
% Introduces:
%
% - : bv1 - bv2
% - : [bvec -> bvec]
% - : [bvec, bvec -> bvec]
% overflow : [bvec, bvec -> bool]
% underflow : [bvec, bvec -> bool]
%
%------------------------------------------------------------------------
bv_arithmetic_defs[N: posnat]: THEORY
BEGIN
bv, bv1, bv2 : VAR bvec[N]
% ---------- 2's complement negation of a bit vector ----------
-(bv: bvec[N]): { bvn: bvec[N] | bv2int(bvn) =
IF bv2int(bv) = minint[N] THEN bv2int(bv)
ELSE -(bv2int(bv)) ENDIF}
% ---------- 2's complement subtraction of two bit vectors ----------
-(bv1, bv2): bvec[N] = (bv1 + (-bv2))
% ---------- Define conditions for 2's complement overflow ----------
overflow(bv1,bv2): bool = (bv2int(bv1) + bv2int(bv2)) > maxint[N]
OR (bv2int(bv1) + bv2int(bv2)) < minint[N]
% === Properties of these additional functions in lib/bitvectors/bv_arithmetic=
% ---------- Integer <, <=, >, >=, +, * ----------
% Note that we can't use these operators, as they will always be ambiguous
bv_slt(bv1, bv2): bool = bv2int(bv1) < bv2int(bv2)
bv_sle(bv1, bv2): bool = bv2int(bv1) <= bv2int(bv2)
bv_sgt(bv1, bv2): bool = bv2int(bv1) > bv2int(bv2)
bv_sge(bv1, bv2): bool = bv2int(bv1) >= bv2int(bv2)
bv_splus(bv1, (bv2 | NOT overflow(bv1, bv2))): bvec[N] =
int2bv(bv2int(bv1) + bv2int(bv2))
mult_overflow(bv1, bv2): bool = (bv2int(bv1) * bv2int(bv2)) > maxint[N]
OR (bv2int(bv1) * bv2int(bv2)) < minint[N]
bv_stimes(bv1, (bv2 | NOT mult_overflow(bv1, bv2))): bvec[N] =
int2bv(bv2int(bv1) * bv2int(bv2))
% Executable version of nat2bv (named bv for short)
nat2bv_rec(n: below(exp2(N)), bv: bvec[N], idx: below(N)): recursive bvec[N] =
let nbv = bv WITH [(idx) := mod(n, 2) = 1]
in if idx = 0
then nbv
else nat2bv_rec(ndiv(n, 2), nbv, idx - 1)
endif
measure idx
% The bv conversion allows easy creation of literal bitvectors, e.g., bv[8](0b11001010)
% It is also the form output by the ground evaluator.
bv(n: below(exp2(N))): bvec[N] = nat2bv_rec(n, lambda (i: below(N)): false, N-1)
CONVERSION+ bv
END bv_arithmetic_defs
bv_extend_defs [N: posnat] : THEORY
% -----------------------------------------------------------------------
% Introduces:
% zero_extend: [k: above(N) -> [bvec[N] -> bvec[l]]] =
% sign_extend: [k: above(N) -> [bvec[N] -> bvec[l]]] =
% zero_extend_lsend: [k: above(N) -> [bvec[N] -> bvec[l]]]
% lsb_extend: [k: above(N) -> [bvec[N] -> bvec[l]]] =
%
% -----------------------------------------------------------------------
BEGIN
bv: VAR bvec[N]
k: VAR above(N)
%------------------------------------------------------------------------
% zero_extend returns a function that extends a bit vector to length k
% such that its interpretation as a natural number remains unchanged.
% That is, it fills 0's at the most significant positions.
%------------------------------------------------------------------------
zero_extend(k: above(N)): [bvec[N] -> bvec[k]] =
(LAMBDA bv: fill[k-N](FALSE) o bv )
%------------------------------------------------------------------------
% sign_extend returns a function that extends a bit vector to length k
% by repeating the most significant bit of the given bit vector.
% The set above(N) contains nat numbers greater than n.
%------------------------------------------------------------------------
sign_extend(k: above(N)): [bvec[N] -> bvec[k]] =
(LAMBDA bv: fill[k-N](bv^(N-1)) o bv )
%------------------------------------------------------------------------
% zero_extend_lsend returns a function that extends a bit vector to
% length k by padding 0's at the least significant end of bvec.
% That is, the bv2nat interpretation of the argument increases by 2**(k-N)
%------------------------------------------------------------------------
zero_extend_lsend(k: above(N)): [bvec[N] -> bvec[k]] =
(LAMBDA bv: bv o fill[k-N](FALSE))
%------------------------------------------------------------------------
% lsb_extend returns a function that extends a bit vector to
% length k by repeating the lsb of the bit vector at its
% least significant end.
%------------------------------------------------------------------------
lsb_extend(k: above(N)): [bvec[N] -> bvec[k]] =
(LAMBDA bv: bv o fill[k-N](bv^0))
pad_left(k: above(N), b: bit)(bv): bvec[k] = fill[k-N](b) o bv
pad_right(k: above(N), b: bit)(bv): bvec[k] = bv o fill[k-N](b)
END bv_extend_defs
%-------------------------------------------------------------------------
%
% Basic properties of infinite sets. This theory defines infinite sets
% as the subtype of set[T] that satisfies the predicate "is_infinite".
% This predicate states that there is no injective function into below[N]
% for any N.
%
% ---------------------------------------------------------------------
% Author: Jerry James (jamesj@acm.org), University of Kansas
%
%-------------------------------------------------------------------------
infinite_sets_def[T: TYPE]: THEORY
BEGIN
S, R: VAR set[T]
% ==========================================================================
% The main definition
% ==========================================================================
is_infinite(S): MACRO bool = NOT is_finite(S)
infinite_set: TYPE = {S | NOT is_finite(S)}
Inf: VAR infinite_set
Fin: VAR finite_set[T]
t: VAR T
% ==========================================================================
% Properties of infinite sets
% ==========================================================================
infinite_nonempty: JUDGEMENT infinite_set SUBTYPE_OF (nonempty?[T])
infinite_add: JUDGEMENT add(t, Inf) HAS_TYPE infinite_set
infinite_remove: JUDGEMENT remove(t, Inf) HAS_TYPE infinite_set
infinite_superset: THEOREM FORALL Inf, S: subset?(Inf, S) => is_infinite(S)
infinite_union_left: JUDGEMENT union(Inf, S) HAS_TYPE infinite_set
infinite_union_right: JUDGEMENT union(S, Inf) HAS_TYPE infinite_set
infinite_union: THEOREM
FORALL S, R:
is_infinite(union(S, R)) => is_infinite(S) OR is_infinite(R)
infinite_intersection: THEOREM
FORALL S, R:
is_infinite(intersection(S, R)) => is_infinite(S) AND is_infinite(R)
infinite_difference: JUDGEMENT difference(Inf, Fin) HAS_TYPE infinite_set
infinite_rest: JUDGEMENT rest(Inf) HAS_TYPE infinite_set
infinite_fullset: THEOREM
(EXISTS S: is_infinite(S)) => is_infinite(fullset[T])
END infinite_sets_def
finite_sets_of_sets[T: TYPE]: THEORY
BEGIN
a: VAR set[T]
powerset_natfun_rec(A: finite_set[T],
n: upto(card(A)),
f: (bijective?[(A), below(card(A))]),
B: (powerset(A))):
RECURSIVE nat =
IF n = 0 THEN 0
ELSE LET nval = exp2(n-1) * IF member(inverse(f)(n-1), B) THEN 1 ELSE 0 ENDIF
IN nval + powerset_natfun_rec(A, n-1, f, B)
ENDIF
MEASURE n
powerset_natfun_rec_bound: LEMMA
FORALL (A: finite_set[T],
n: upto(card(A)),
f: (bijective?[(A), below(card(A))]),
B: (powerset(A))):
powerset_natfun_rec(A, n, f, B) < exp2(n)
powerset_natfun(A: finite_set[T])(B: (powerset(A))): below(exp2(card(A))) =
LET f = choose(bijective?[(A), below(card(A))])
IN powerset_natfun_rec(A, card(A), f, B)
powerset_natfun_inj_rec: LEMMA
FORALL (A: finite_set[T],
n: upto(card(A)),
f: (bijective?[(A), below(card(A))]),
B1, B2: (powerset(A))):
powerset_natfun_rec(A, n, f, B1) = powerset_natfun_rec(A, n, f, B2)
<=> (FORALL (m: upto(card(A))):
(m < n) IMPLIES
(member(inverse(f)(m), B1) IFF member(inverse(f)(m), B2)))
powerset_natfun_inj: LEMMA
FORALL (A: finite_set[T]):
FORALL (B1, B2: (powerset(A))):
powerset_natfun(A)(B1) = powerset_natfun(A)(B2) IMPLIES B1 = B2
powerset_finite: JUDGEMENT
powerset(A: finite_set[T]) HAS_TYPE finite_set[set[T]]
powerset_finite2: JUDGEMENT
powerset(A: finite_set[T]) HAS_TYPE finite_set[finite_set[T]]
SS: VAR setofsets[T]
Union_finite: THEOREM
FORALL SS: is_finite(Union(SS)) IFF is_finite(SS) AND every(is_finite)(SS)
finite_Union_finite: LEMMA is_finite(SS) AND every(is_finite[T])(SS) IMPLIES
is_finite(Union(SS))
Union_infinite: COROLLARY
FORALL SS:
is_infinite(Union(SS)) IFF is_infinite(SS) OR some(is_infinite)(SS)
Intersection_finite: THEOREM
FORALL SS:
nonempty?(SS) AND every(is_finite)(SS) => is_finite(Intersection(SS))
Intersection_infinite: COROLLARY
FORALL SS: is_infinite(Intersection(SS)) => every(is_infinite)(SS)
Complement_finite: THEOREM
FORALL SS: is_finite(Complement(SS)) IFF is_finite(SS)
Complement_is_finite: JUDGEMENT
Complement(SS: finite_set[set[T]]) HAS_TYPE finite_set[set[T]]
Complement_infinite: COROLLARY
FORALL SS: is_infinite(Complement(SS)) IFF is_infinite(SS)
Complement_is_infinite: JUDGEMENT
Complement(SS: infinite_set[set[T]]) HAS_TYPE infinite_set[set[T]]
END finite_sets_of_sets
% Equivalence classes, quotient types, etc.
%
% Bart Jacobs, Dep. Comp. Sci., Univ. Nijmegen.
%
% With suggestions and remarks from:
% Ulrich Hensel, Marieke Huisman, Hendrik Tews.
%
% With modifications and additions by Sam Owre, SRI International
EquivalenceClosure[T : TYPE] : THEORY
BEGIN
R, S : VAR PRED[[T, T]]
x, y : VAR T
% Higher order definition of equivalence relation closure.
EquivClos(R) : equivalence[T] =
{ (x, y) | FORALL(S : equivalence[T]) : subset?(R, S) IMPLIES S(x, y) }
EquivClosSuperset : LEMMA
subset?(R, EquivClos(R))
EquivClosMonotone : LEMMA
subset?(R, S) IMPLIES subset?(EquivClos(R), EquivClos(S))
EquivClosLeast : LEMMA
equivalence?(S) AND subset?(R, S) IMPLIES subset?(EquivClos(R), S)
EquivClosIdempotent : LEMMA
EquivClos(EquivClos(R)) = EquivClos(R)
EquivalenceCharacterization : LEMMA
equivalence?(S) IFF (S = EquivClos(S))
END EquivalenceClosure
QuotientDefinition[T : TYPE] : THEORY
BEGIN
R : VAR set[[T, T]]
S : VAR equivalence[T]
x, y, z : VAR T
EquivClass(R)(x) : set[T] = { z | R(x, z) }
EquivClassNonEmpty : LEMMA
nonempty?[T](EquivClass(S)(x))
EquivClassEq : LEMMA
EquivClass(S)(x) = EquivClass(S)(y) IFF S(x, y)
repEC(S)(x): T = choose(EquivClass(S)(x))
% The next two lemmas facilitate working with representatives.
EquivClassChoose : LEMMA
S(x, repEC(S)(x))
ChooseEquivClassChoose : LEMMA
EquivClass(S)(repEC(S)(x)) = EquivClass(S)(x)
Quotient(S) : TYPE =
{ P : set[T] | EXISTS x : P = EquivClass(S)(x) }
rep(S)(P: Quotient(S)): T = choose(P)
rep_is_repEC: LEMMA
rep(S)(EquivClass(S)(x)) = repEC(S)(x)
rep_lemma: LEMMA
EquivClass(S)(x)(rep(S)(EquivClass(S)(x)))
% Note that quotient_map has a different range type than EquivClass,
% and EquivClass(S) is not surjective.
quotient_map(S)(x) : Quotient(S) =
EquivClass(S)(x)
quotient_map_surjective : LEMMA
surjective?(quotient_map(S))
% Quotients are also defined for arbitrary relations, via the
% Equivalence Closure (EC).
ECQuotient(R) : TYPE =
Quotient(EquivClos(R))
ECquotient_map(R)(x) : ECQuotient(R) =
quotient_map(EquivClos(R))(x)
END QuotientDefinition
KernelDefinition[X: TYPE, X1: TYPE FROM X, Y : TYPE] : THEORY
BEGIN
f : VAR [X1 -> Y]
R : VAR PRED[[X, X]]
x1, x2 : VAR X1
% The following definition would be part of the 'functions' theory
% but equivalence is defined afterwards.
EquivalenceKernel(f) : equivalence[X1] =
{ (x1, x2) | f(x1) = f(x2) }
PreservesEq(R)(f) : bool =
subset?(restrict[[X, X],[X1, X1], bool](R), EquivalenceKernel(f))
PreservesEqClosure : LEMMA
PreservesEq(R) = PreservesEq(EquivClos[X1](R))
PreservesEq_is_preserving: LEMMA
PreservesEq(R) = preserves(restrict[[X, X], [X1, X1], bool](R), =[Y])
END KernelDefinition
QuotientKernelProperties[X : TYPE, X1: TYPE FROM X] : THEORY
BEGIN
S : VAR equivalence[X1]
R : VAR PRED[[X, X]]
Kernel_quotient_map : LEMMA
EquivalenceKernel[X, X1, Quotient(S)](quotient_map(S)) = S
PreservesEq_quotient_map : LEMMA
PreservesEq[X, X1, Quotient(S)](S)(quotient_map(S))
quotient_map_is_Quotient_EqivalenceRespecting: JUDGEMENT
quotient_map(S) HAS_TYPE (PreservesEq[X, X1, Quotient(S)](S))
Kernel_ECquotient_map : LEMMA
EquivalenceKernel[X, X1, ECQuotient(S)](quotient_map(S)) = S
PreservesEq_ECquotient_map : LEMMA
PreservesEq[X, X1, ECQuotient(S)](S)(quotient_map(S))
quotient_map_is_ECQuotient_EqivalenceRespecting: JUDGEMENT
quotient_map(S) HAS_TYPE (PreservesEq[X, X1, ECQuotient(S)](S))
END QuotientKernelProperties
QuotientSubDefinition[X : TYPE, X1: TYPE FROM X] : THEORY
BEGIN
x: VAR X1
S : VAR {R: equivalence[X] | PreservesEq[X, X, bool](R)(X1_pred)}
QuotientSub(S) : TYPE =
{ P :set[X] | EXISTS x : P = EquivClass(S)(x) }
quotient_sub_map(S)(x) : QuotientSub(S) =
EquivClass(S)(x)
END QuotientSubDefinition
QuotientExtensionProperties[X : TYPE, X1: TYPE FROM X, Y : TYPE] : THEORY
BEGIN
S : VAR {R: equivalence[X] | PreservesEq[X, X, bool](R)(X1_pred)}
lift(S)
(g : (PreservesEq[X, X1, Y](S)))
(P : QuotientSub[X, X1](S))
: Y
= g(rep(S)(P))
lift_commutation : LEMMA
FORALL (S),
(g : (PreservesEq[X, X1, Y](S))) :
lift(S)(g) o quotient_sub_map[X, X1](S) = g
lift_unicity : LEMMA
FORALL (S | PreservesEq[X, X, bool](S)(X1_pred)),
(g : (PreservesEq[X, X1, Y](S))) :
FORALL(h : [QuotientSub[X, X1](S) -> Y]) :
h o quotient_sub_map[X, X1](S) = g IMPLIES h = lift(S)(g)
END QuotientExtensionProperties
QuotientDistributive[X, Y: TYPE] : THEORY
BEGIN
% This theory makes clear that quotients commute with products: there is an isomorphism
%
% [X/S, Y] iso [X,Y]/EqualityExtension(S)
%
% given by the canonical map (from right to left). Such distributivity
% results can be used to define functions with several parameters on a
% quotient. In the presence of function types, this can also be done
% via Currying. The result is included here mainly as a test for the
% formalisation of quotients.
%
S : VAR equivalence[X]
z, w : VAR [X, Y]
EqualityExtension(S) : set[[[X, Y], [X, Y]]] =
{ (z, w) | S(z`1, w`1) AND z`2 = w`2 }
EqualityExtension_is_equivalence: JUDGEMENT
EqualityExtension(S) HAS_TYPE equivalence[[X, Y]]
EqualityExtensionPreservesEq : LEMMA
PreservesEq[[X, Y], [X, Y], [Quotient(S), Y]]
(EqualityExtension(S))
(LAMBDA(x : X, y : Y) : (quotient_map(S)(x), y))
QuotientDistributive : LEMMA
bijective?[Quotient(EqualityExtension(S)), [Quotient(S), Y]]
(lift[[X, Y], [X, Y], [Quotient(S), Y]](EqualityExtension(S))
(LAMBDA(x : X, y : Y) : (quotient_map(S)(x), y)))
% [X/S, Y/R] iso [X,Y]/RelExtension(S,R)
R: VAR equivalence[Y]
RelExtension(S, R) : equivalence[[X, Y]] =
{ (z, w) | S(z`1, w`1) AND R(z`2, w`2) }
RelExtensionPreservesEq : LEMMA
PreservesEq[[X, Y], [X, Y], [Quotient(S), Quotient(R)]]
(RelExtension(S,R))
(LAMBDA(x : X, y : Y) : (quotient_map(S)(x), quotient_map(R)(y)))
RelQuotientDistributive : LEMMA
bijective?[Quotient(RelExtension(S,R)), [Quotient(S), Quotient(R)]]
(lift[[X, Y], [X, Y], [Quotient(S), Quotient(R)]](RelExtension(S, R))
(LAMBDA(x : X, y : Y) : (quotient_map(S)(x), quotient_map(R)(y))))
% F: [X -> equivalence[Y]]
% [x:X -> Y/F(x)] iso [X -> Y]/FunExtension(F)
F: VAR [X -> equivalence[Y]]
f, g : VAR [X -> Y]
FunExtension(F) : equivalence[[X -> Y]] =
{ (f, g) | FORALL (x : X) : F(x)(f(x), g(x)) }
FunExtensionPreservesEq : LEMMA
PreservesEq[[X -> Y], [X -> Y], [x : X -> Quotient(F(x))]]
(FunExtension(F))
(LAMBDA(f : [X -> Y]) : LAMBDA (x : X) : quotient_map(F(x))(f(x)))
FunQuotientDistributive : LEMMA
bijective?[Quotient(FunExtension(F)), [x : X -> Quotient(F(x))]]
(lift[[X -> Y], [X -> Y], [x : X -> Quotient(F(x))]](FunExtension(F))
(LAMBDA(f : [X -> Y]) : (LAMBDA (x : X): (quotient_map(F(x))(f(x))))))
END QuotientDistributive
QuotientIteration[X : TYPE] : THEORY
BEGIN
% In this theory it will be shown how successive quotients can be reduced
% to a single quotient:
%
% (X/S)/R iso X/action(S)(R)
%
% again via the canonical map.
S : VAR equivalence[X]
x, y : VAR X
action(S)(R : equivalence[Quotient(S)])(x, y) : bool =
R(EquivClass(S)(x), EquivClass(S)(y))
action_equivalence_is_equivalence: JUDGEMENT
action(S)(R : equivalence[Quotient(S)]) HAS_TYPE equivalence[X]
QuotientAction : LEMMA
FORALL(R : equivalence[Quotient(S)]) :
bijective?[Quotient(R), Quotient(action(S)(R))]
(lift[Quotient(S), Quotient(S), Quotient(action(S)(R))](R)
(lift[X, X, Quotient(action(S)(R))](S)
(quotient_map[X](action(S)(R)))))
END QuotientIteration
% The following theory illustrates how the lift type can be used
% to describe partial functions from X to Y, namely as total
% functions from X to lift[Y].
PartialFunctionDefinitions[X, Y : TYPE] : THEORY
BEGIN
% Two representations of partial functions are described,
% and shown to be isomorphic. In practice, the formulation
% based on lift is more convenient, because definitions
% are easier and fewer TCCs are generated.
SubsetPartialFunction : TYPE =
[# dom : PRED[X], fun : [(dom) -> Y] #]
LiftPartialFunction : TYPE =
[X -> lift[Y]]
f : VAR LiftPartialFunction
g : VAR SubsetPartialFunction
h : VAR [X -> Y]
SPartFun_appl(g): [(dom(g)) -> Y] = g`fun
SPartFun_to_LPartFun(g) : LiftPartialFunction =
LAMBDA(x : X) : IF dom(g)(x) THEN up(fun(g)(x)) ELSE bottom ENDIF
LPartFun_to_SPartFun(f) : SubsetPartialFunction =
(#
dom := {x : X | up?(f(x))},
fun := LAMBDA(y : {x : X | up?(f(x))}) : down(f(y))
#)
TotalFun_to_SPartFun(h): SubsetPartialFunction =
(#
dom := {x : X | TRUE},
fun := h
#)
TotalFun_to_LPartFun(h): LiftPartialFunction =
LAMBDA(x : X) : up(h(x))
CONVERSION SPartFun_appl,
SPartFun_to_LPartFun, LPartFun_to_SPartFun,
TotalFun_to_SPartFun, TotalFun_to_LPartFun
SPartFun_to_LPartFun_to_SPartFun : LEMMA
LPartFun_to_SPartFun(SPartFun_to_LPartFun(g)) = g
LPartFun_to_SPartFun_to_LPartFun : LEMMA
SPartFun_to_LPartFun(LPartFun_to_SPartFun(f)) = f
END PartialFunctionDefinitions
PartialFunctionComposition[X, Y, Z : TYPE] : THEORY
BEGIN
f : VAR LiftPartialFunction[X, Y]
g : VAR LiftPartialFunction[Y, Z]
o(g, f) : LiftPartialFunction[X, Z] =
LAMBDA(x : X) :
CASES f(x) OF
bottom : bottom,
up(y) : g(y)
ENDCASES
h : VAR SubsetPartialFunction[X, Y]
k : VAR SubsetPartialFunction[Y, Z]
CompDom(k, h) : PRED[X] =
{ x : X | dom(h)(x) AND dom(k)(fun(h)(x)) };
o(k, h) : SubsetPartialFunction[X, Z] =
(#
dom := CompDom(k, h),
fun := LAMBDA(x : (CompDom(k, h))) : fun(k)(fun(h)(x))
#)
SPartFun_to_LPartFun_CompositionPreservation : LEMMA
SPartFun_to_LPartFun(k o h)
= SPartFun_to_LPartFun(k) o SPartFun_to_LPartFun(h)
LPartFun_to_SPartFun_CompositionPreservation : LEMMA
LPartFun_to_SPartFun(g o f)
= LPartFun_to_SPartFun(g) o LPartFun_to_SPartFun(f)
END PartialFunctionComposition