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 topThe tag identifies links that are outside the NASA domain