Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: top.pvs Sprache: PVS

Original von: PVS^©

top: THEORY
%------------------------------------------------------------------------
% Elementary properties of reals and operations over reals
%
%  top_sigma      -- provides a family of summation functions
%                    over functions [T FROM int -> real]
%  min_max        -- properties on min,max
%  abs_lems       -- additional properties of abs
%  product_real   -- defines product over functions [int -> real]
%  bounded_reals  -- defines sup, inf, max, min
%  real_sets      -- properties of sup, inf, max, min
%  real_fun_ops,  -- adding, subtracting, etc on functions
%  real_fun_preds -- increasing?, decreasing?, etc on functions
%  real_fun_props -- properties about defs in real_fun_preds
%  exponent_props -- additional properties of expt
%  sqrt           -- properties of square root
%  sqrt_rew       -- REVISED with AUTO_REWRITE+ statements
%                    (See also new strategies (sqrt-rew) and (sqrt-rew-off)
%  sqrt_approx    -- definitions of sqrt_newton and sqrt_bisect
%                    (newton and bisection methods for computing square roots).
%  sq             -- square function and properties
%  sq_rew         -- installs useful AUTO_REWRITE+s
%  sign           -- properties of sign function
%  sign3          -- properties of sign3 function
%  quadratic      -- solution of quadratic equations
%  quadratic_2b   -- a better solution of quadratic equations for 2b
%  quad_minmax    -- minimum and Maximum of quadratic equations
%  binomial,      -- binomial coefficient
%  polynomials   -- polynomials
%  more_polynomial_props
%
%  Version 2.5   1/24/08
%
%  CHANGES:
%
%     8/1/01:
%        sqrt_exists    -- existence proof of sqrt
%        sqrt_approx    -- theory added (by Fleuriot/Geser)
%
%     8/7/01
%        sigma_with, sigma_zero added to sigma
%
%     2/26/02
%        duplications with PVS 2.4 prelude removed
%        predicates over functions given names with ?, e.g. increasing?
%
%     3/14/02: Added quadratic_ax
%
%     2/26/03: Added AUTO_REWRITE+ commands to automate some routine stuff
%
%     3/7/03:  Added quadratic_minmax, new lemmas added to abs_lems
%
%     4/14/03: Duplicate theory problem resolved
%
%     11/3/03: binomial added                    (Lester)
%
%     11/28/03: quadratic_ax is gone (use quadratic instead)
%
%     2/13/04: turned on more auto-rewrites in sq and sqrt
%              (if old proofs fail, add the following to your old proof:
%        (STOP-REWRITE "sq_sqrt" "sq_0" "sq_1" "sq_abs" "sq_abs_neg")
%        (STOP-REWRITE "sqrt_0" "sqrt_1" "sqrt_square" "sqrt_sq" "sqrt_sq_neg")
%     7/8/04:  Added auto-rewrites in factorial
%     3/28/05: Added log_nat and moved bolzano.pvs to Interval package
%              by C. Munoz
%     4/15/05: polynomials moved here from trig_fnd
%     3/27/06: sigma theories generalized by Paul Miner
%     10/28/07: quad_minmax improved, circles_and_lines added
%     11/7/07: sigma theories improved
%     1/24/08: product operator theories added
%
%------------------------------------------------------------------------

BEGIN

  IMPORTING top_sigma,         % set of summation theories
            mixed_products,
            mixed_sigmas,
            old_sigma,
            abs_lems,          % additional properties about absolute value
            binomial,          % Binomial coefficient
            bound_defs,        % upper_bound, lowerbound, lub, glb
            bounded_reals,     % defines sup, inf, max, min
            circles_and_lines, % intersection of dynamic line and a circle
            exponent_props,    % additional properties of expt
            expt_rew,          % usedful auto-rewrites for expt
            factorial_props,   % additional properties of factorial function
            harmonic_polynomials,
     log_nat,           % Natural and real part of a logarithm
            base_repr,         % Base n representation of natural numbers (A. Dutle)
            min_max,           % Min,max properties
            polynomials,       % polynomials
            more_polynomial_props,
            poly_rew,
            bernstein_polynomials,
            quadratic,         % Solution of quadratic equations
     quadratic_2b,      % A better solution of quadratic equations for 2b
            quad_minmax,       % easier to use quadratic_minmax
     convex_functions,  % properties of convex functions
            real_orders,       % real orders <, <=, >=, >
     real_order_ep,     % order defined by floor(abs(x)/epsil) < floor(abs(y)/epsil)
            reals_complete_more, % some additional completness properties
            real_fun_ops,      % adding, subtracting, etc on functions
            real_fun_ops_aux,  % min, max over functions
            real_fun_preds,    % increasing?, decreasing?, etc on functions
            real_fun_orders,   % <, <=, >, >= over functions[T-> real]
            real_fun_props,    % properties about defs in real_fun_preds
            real_sets,         % more properties of bounded sets of reals
            real_facts,        % archimedian field properties, lub, glb
            sign,              % properties of the 2-value sign function
            sign3,             % properties of the 3-value sign function
            sq,                % square function
            sqrt,              % non-axiomatic version of sqrt
            sq_rew,            % useful auto-rewrites for square function
            sqrt_rew,          % useful auto rewrite for sqrt
            sqrt_approx,       % approximation to sqrt
            sqrt_rew,          % auto-rewrites for sqrt
            intervals_real,    % open_intv, closed_intv:  (a,b) or [a,b]

     product,              % generic theory
     product_below,
     product_int,
     product_nat,
     product_posnat,
     product_upto,

            product_seq,       % old theory for products over finite sequence
            product_fseq,
            product_fseq_posnat,

            connected_set,
     RealInt            % Real intervals

%   easy: LEMMA sqrt(2) <= 3/2

END top

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.