|
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.19 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
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.
|
