top: THEORY %------------------------------------------------------------------------- % Integers library % % Authors: Rick Butler NASA Langley % Paul Miner NASA Langley % Bruno Dutertre Royal Holloway & Bedford New College % Alfons Geser HTWK Leipzig, Germany % % Date: May, 2009 %------------------------------------------------------------------------------
% % Defines "div" according to the Ada Reference Manual % % div -- Ada Reference Manual division theory % rem -- Ada Reference Manual rem theory % % This div truncates toward zero on a negative argument. % % Version 1.2 Changed mod to mod_ in PVS4.0 because PVS no longer allows you to % redefine a theory defined in the prelude. % Version 1.3 Changed "divides" to "divides?" so as to not conflict with % prelude definition % Version 1.4 Moved all of number_theory library to ints library % % NOTE: The old approach of having two different definitions of "div" % and "mod" defined in different theories is no longer reasonable % given that "mod" is now defined in the prelude. The alternate % definitions are now named "tdiv" and "tmod" % % NOTE: mod_ has been removed since it is now in prelude. The additional lemmas % not in prelude are now in mod_lems % % % Version 1.5 product operator theories added % %------------------------------------------------------------------------- BEGIN IMPORTING div, % integer division
rem, % old version of "rem", prelude version supercedes
mod_div_lems, % modular arithmetic lemmas that involve div
mod_lems, % modular arithmetic lemmas
gcd, % greatest common divisor
gcd_fractions, % division by gcd
tdiv, tmod, % versions that trunc away from zero for neg arg
max_upto, % max of a set of upto
max_below, % max of a set of below
div_nat, % integer division over nats
mod_nat, % mod over nats
abstract_min, % defines min over type T satisfying P
abstract_max, % defines max over type T satisfying P
floor_div_lems,
floor_more,
max_below,
max_bounded_posnat,
max_finite_set_nat,
min_nat, % minimum value in a set of naturals
min_posnat, % minimum value in a set of positive naturals
nat_fun_props, % injective/surgective functions over nats
primes, % definition of prime numbers
factorial, % factorial function (moved from reals library)
pigeonhole, % The pigeonhole principle
%% Since int is a subtype of reals these are really just special %% cases of the theories in the reals library. However, there is %% a bug in the PVS judgments system that makes these still useful %% As soon as that bug is fixed, these will be removed.
product, % generic theory
product_below,
product_int,
product_nat,
product_posnat,
product_upto,
well_nat % contains an AXIOM that is proved in the orders library
END top
¤ Dauer der Verarbeitung: 0.11 Sekunden
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
