| products/sources/formale Sprachen/PVS/reals/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: flags.ml Sprache: UnknownOriginal 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.35 Sekunden (vorverarbeitet) ¤ |
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
