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)
¤
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.
