| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/reals/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 2 kB |
|
SSL top.pvs Sprache: PVS |
|||||||||
|
top: THEORY
%------------------------------------------------------------------------ % % An Axiomatic Theory of Trigonometry (Demonstrated to be sound in trig_fnd % library) % % by Cesar Munoz Langley ICASE Institute % Victor Carreno NASA Langley % Ricky Butler NASA Langley % Gilles Dowek INRIA, Domaine de Voluceau % Alfons Geser Langley ICASE Institute % Ben Di Vito NASA Langley % % Version 1.0 3/27/01 % Version 1.1 6/27/01 New lemmas added: % -------------------------------- % tan_period, sin_k_pi , cos_2k_pi, % cos_k_pi , sin_k_pi2, tan_k_pi, % sin_eq_1 , cos_eq_1 , sin_eq_sin, % cos_eq_cos, tan_eq_tan, sin_eq_pm1, % cos_eq_pm1, and prelude_aux lemmas % % Version 1.2 6/28/01 Theory "trig_rew" added % % Version 1.3 10/27/03 Corrected, foundational theory % (David Lester) % % Version 1.31 11/29/03 Renamed PI to pi (Cesar A. Munoz) % % Version 1.32 2/6/04 Theory "tan_approx" added (C. Munoz) % % Version 1.33 5/23/04 atan2 added (D Lester) % % Version 1.34 5/30/04 atan/asin/acos added (D Lester) % % Version 1.4 4/15/05 approx made consistent with trig_fnd % % INDEX: % ------ % % % trig_basic: % ----------- % - definition of pi with crude upper and lower bounds % - definition of sin, cos, and tan % - pythagorean properties: sq(sin(a)) + sq(cos(a)) = 1 % - sum and difference of two angles % - double angle formulas % - negative properties, e.g. sin(-a) % - periodicity, e.g. sin(a) = sin(a + 2 * j * pi) % - co-function identities, e.g. sin(pi/2 - a) = cos(a) % - location of zeros of trig functions % % trig_values Lemma names % ----------- ------------------------------------ % - trig functions at 0 : sin_0 , cos_0 , tan_0 % - trig functions at pi/6 : sin_pi6 , cos_pi6 , tan_pi6 % - trig functions at pi/4 : sin_pi4 , cos_pi4 , tan_pi4 % - trig functions at pi/3 : sin_pi3 , cos_pi3 , tan_pi3 % - trig functions at pi/2 : sin_pi2 , cos_pi2 , tan_pi2 % - trig functions at pi : sin_pi , cos_pi , tan_pi % - trig functions at 2*pi/3 : sin_2pi3 , cos_2pi3 , tan_2pi3 % - trig functions at 3*pi/4 : sin_3pi4 , cos_3pi4 , tan_3pi4 % - trig functions at 5*pi/4 : sin_5pi4 , cos_5pi4 , tan_5pi4 % % trig_ineq % --------- % - regions where functions are greater than 0 % - regions where functions are less than 0 % - regions where functions are increasing % - regions where functions are decreasing % % trig_extra % ---------- % - reduction theorems % - sum and product identities % - half-angle identities and zeros % - triple angle formulas % % trig_approx % ----------- % - taylor series approximations to trig functions: % sin_approx(a,n): sum first n terms of taylor expansion of sin % cos_approx(a,n): sum first n terms of taylor expansion of cos % % tan_approx % ---------- % - taylor series approximations for tangent % % law_cosines % ----------- % - the law of cosines in a coordinate geometry formulation % % trig_degree % ----------- % - trig functions that take arguments in degrees: sind, cosd % - defines conversions toRad, toDeg % % trig_inv % ------------- % - provides interface to atan, asin, acos, atan2 % % ------------- % - defines inverse trig functions: arcsin, arccos, and arctan % % trig_rew % ------------- % - Experimental auto-rewrite-theory background library % % %------------------------------------------------------------------------ BEGIN IMPORTING trig_doc, % Some more documentation (Rationale) trig, % typical needs trig_full, % everything % --------------------- The above import the following ------------------ trig_basic, % basic properties trig_values, % values of functions for special arguments trig_ineq, % trig inequalities trig_extra, % sum and product, half-angle, reductions and zeros trig_approx, % taylor series approximations to trig functions: tan_approx, % approximatan2_propsations fprior tangent law_cosines, % law of cosines trig_degree, % conversions to degrees trig_inverses, % interface to atan, asin, acos, atan2 trig_rew, % auto-rewrites asin, % asin properties acos, % acos properties atan, % atan properties atan_values, % atan for specific values atan2, % two-argument arc tangent atan2_props, % additional properties of atan2 and values jatan2, % Java atan2 to2pi, % normalization of radians to 2pi sincos, % continuity, derivablility of sin, cos deriv_sincos, integral_sincos, integral_indef_sincos END top ¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28