top: THEORY %------------------------------------------------------------------------ % % A Foundational Theory of Trigonometry % % 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 % David Lester Manchester University % % 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/30/04 inverse equivalences done (DRL) % % Version 1.4 1/5/05 update to analysis name changes % % Version 1.5 4/21/05 atan2_props added and minor things % % Version 1.6 1/8/08 cleaned up types of inverse functions % % INDEX: % ------ % % trig_basic: % ----------- % - definition of pi with c % - 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_inverses % ------------- % - 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
exp_term,
trig_approx, % taylor series approximations to trig functions:
tan_approx, % Approximations for tangent
atan_approx, % Approximations for atan
law_cosines, % law of cosines
trig_degree, % conversions to degrees
trig_inverses, % inverse functions
trig_rew, % auto-rewrites
% ---------------------- Foundational Development -----------------------
sincos, % continuity and differentiability of sin, cos
acos, % arc cosine (from arc tangent)
asin, % arc sine (from arc tangent)
atan, % one-argument arc tangent (from integral)
atan_values, % special values of atan
atan2, % two-argument arc tangent
atan2_props, % additional properties of atan2
jatan2, % Java atan2
to2pi, % normalization of radians to 2pi
sincos_phase, % sin and cos from infinite series
sincos, % continuity, differentiality, and bounds
sincos_quad, % basic properties of sin cos
deriv_sincos, % convenient forms over T from real
integral_sincos, % convenient forms over T from real
integral_indef_sincos, % sin/cos indefinite integral properties
tan_quad % definiton of tan from atan
% ---- type simplifications % % NOTE: real_abs_lt_pi: NONEMPTY_TYPE = {x:real | abs(x) < pi/2} was % renamed to real_abs_lt_pi2 which is much more conistent!!! % % in atan: % % >real_abs_lt_pi2: NONEMPTY_TYPE = {x | abs(x) < pi/2} % real_abs_lt_pi2: NONEMPTY_TYPE = {x | -pi/2 < x AND x < pi/2} % % in asin: % % >real_abs_le1: NONEMPTY_TYPE = {x:real | abs(x) <= 1} % >real_abs_lt1: NONEMPTY_TYPE = {x:real | abs(x) < 1} % >real_abs_le_pi2: NONEMPTY_TYPE = {x:real | abs(x) <= pi/2} % real_abs_le1: NONEMPTY_TYPE = {x:real | -1 <= x AND x <= 1} % real_abs_lt1: NONEMPTY_TYPE = {x:real | -1 < x AND x < 1} % real_abs_le_pi2: NONEMPTY_TYPE = {x:real | -pi/2 <= x AND x <= pi/2} % % in sincos_quad: % % >real_abs_lt_pi: NONEMPTY_TYPE = {x:real | abs(x) < pi/2} % real_abs_lt_pi2: NONEMPTY_TYPE = {x:real | -pi/2 < x AND x < pi/2}
¤ 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.0.11Bemerkung:
(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.
