Top File of PVS ints Library

 
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

The tag identifies links that are outside the NASA domain