Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/PVS/trig_fnd/ (Beweissystem der NASA Version 6.0.9^©) Datei vom 28.9.2014 mit Größe 5 kB

Quelle trig_basic.pvs Sprache: PVS

trig_basic : THEORY
%-----------------------------------------------------------------------------
%     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
%
%   Version 1.1 27/10/03 Foundational Version David Lester
%
%   CHANGES
%         - Oct 21 2004 (C. Munoz) Moved pi_lb, pi_ub, pi_bound to atan_approx
%
%-----------------------------------------------------------------------------
BEGIN

  IMPORTING reals@sqrt, sincos_def, atan_approx

  a,b,c,d           : VAR real
  nnc               : VAR nonneg_real
  j                 : VAR integer

% This is now in atan_approx.pvs
%
%  pi_lb  : real = 31415926/10000000
%
%  pi_ub  : real = 31415927/10000000
%
%  pi_bound : JUDGEMENT pi HAS_TYPE {r:posreal | pi_lb < r AND r < pi_ub}

% -------------------- definition of sin and cos --------------------
%
% This is now in sincos_def.pvs
%
%  trig_range  : TYPE = {a | -1 <= a AND a <= 1}
%
%  sin(x:real) : real = sin_phase(x-2*pi*floor(x/(2*pi)))
%  cos(x:real) : real = cos_phase(x-2*pi*floor(x/(2*pi)))
%
%  sin_range_ax: LEMMA -1 <= sin(a) AND sin(a) <= 1
%  cos_range_ax: LEMMA -1 <= cos(a) AND cos(a) <= 1
%
%  sin_range   : JUDGEMENT sin(a) HAS_TYPE trig_range
%  cos_range   : JUDGEMENT cos(a) HAS_TYPE trig_range
%
%  Tan?(a)        : bool = cos(a) /= 0
%
%  tan(a:(Tan?))  : real = sin(a)/cos(a)

% -------------------- Pythagorean Property --------------------

  sin2_cos2    : LEMMA sq(sin(a)) + sq(cos(a)) = 1

  cos2         : LEMMA sq(cos(a)) = 1 - sq(sin(a))

  sin2         : LEMMA sq(sin(a)) = 1 - sq(cos(a))

% --------------------- Basic Values ----------------------------

  cos_0         : LEMMA cos(0) = 1

  sin_0         : LEMMA sin(0) = 0

  sin_pi2       : LEMMA sin(pi/2) = 1

  cos_pi2       : LEMMA cos(pi/2) = 0

  tan_0         : LEMMA tan(0) = 0

% --------------------- Negative Properties ----------------------

  sin_neg : LEMMA sin(-a) = -sin(a)
  cos_neg : LEMMA cos(-a) = cos(a)
  tan_neg : LEMMA FORALL(a:(Tan?)): tan(-a) = -tan(a)

% -------------------- Co-Function Identities -----------------------

  cos_sin    : LEMMA cos(a) = sin(a+pi/2)
  sin_cos    : LEMMA sin(a) = -cos(a+pi/2)
  sin_shift  : LEMMA sin(pi/2 - a) = cos(a)
  cos_shift  : LEMMA cos(pi/2 - a) = sin(a)

% --------------------- Arguments involving pi ---------------------

  neg_cos     : LEMMA -cos(a) = cos(a+pi)
  neg_sin     : LEMMA -sin(a) = sin(a+pi)

  sin_pi      : LEMMA sin(pi) = 0
  cos_pi      : LEMMA cos(pi) = -1
  tan_pi      : LEMMA tan(pi) = 0
  sin_3pi2    : LEMMA sin(3*pi/2) = -1
  cos_3pi2    : LEMMA cos(3*pi/2) = 0
  sin_2pi     : LEMMA sin(2*pi) = 0
  cos_2pi     : LEMMA cos(2*pi) = 1
  tan_2pi     : LEMMA tan(2*pi) = 0

% ----------------- Sum and Difference of Two Angles ----------------

  sin_plus  : LEMMA sin(a + b) = sin(a)*cos(b) + cos(a)*sin(b)
  sin_minus : LEMMA sin(a - b) = sin(a)*cos(b) - sin(b)*cos(a)

  cos_plus  : LEMMA cos(a + b) = cos(a)*cos(b) - sin(a)*sin(b)
  cos_minus : LEMMA cos(a - b) = cos(a)*cos(b) + sin(a)*sin(b)

  tan_plus  : LEMMA Tan?(a) AND Tan?(b) AND Tan?(a+b) AND
                    tan(a) * tan(b) /= 1 IMPLIES
                      tan(a + b) = (tan(a) + tan(b))/(1 - tan(a)*tan(b))

  tan_minus : LEMMA Tan?(a) AND Tan?(b) AND Tan?(a-b) AND
                    tan(a) * tan(b) /= -1 IMPLIES
                      tan(a - b) = (tan(a) - tan(b))/(1 + tan(a)*tan(b))

  arc_sin_cos  : LEMMA sq(a)+sq(b)=sq(c) IMPLIES
                            EXISTS d: a = c*cos(d) AND b = c*sin(d)

  pythagorean  : LEMMA sq(a)+sq(b)=sq(nnc) IMPLIES
                            EXISTS(alpha:real): nnc=a*cos(alpha)+b*sin(alpha)

% -------------------- Double Angle Formulas --------------------

   sin_2a     : LEMMA sin(2*a) = 2 * sin(a) * cos(a)
   cos_2a     : LEMMA cos(2*a) = cos(a)*cos(a) - sin(a)*sin(a)
   cos_2a_cos : LEMMA cos(2*a) = 2 * cos(a)*cos(a) - 1
   cos_2a_sin : LEMMA cos(2*a) = 1 - 2 * sin(a)*sin(a)
   tan_2a     : LEMMA Tan?(a) AND Tan?(2*a) AND
                      tan(a) * tan(a) /= 1 IMPLIES
                        tan(2*a) = 2 * tan(a)/(1 - tan(a) * tan(a))

% ------------------------- Periodicity -----------------------------

%  IMPORTING reals@prelude_aux_reals

  n: VAR nat
  k: VAR integer

  sin_period  : LEMMA sin(a) = sin(a + 2 * j * pi)
  cos_period  : LEMMA cos(a) = cos(a + 2 * j * pi)
  tan_period  : LEMMA Tan?(a) IMPLIES tan(a) = tan(a + j * pi)

  sin_k_pi    : LEMMA sin(k*pi) = 0
  cos_2k_pi   : LEMMA cos(2*k*pi) = 1
  cos_k_pi    : LEMMA cos(k*pi) = (-1)^(k)
  sin_k_pi2   : LEMMA sin(k*pi + pi/2) = (-1)^k
  tan_k_pi    : LEMMA tan(k*pi) = 0

% -------------------- Characterization of zeroes -------------------

  sin_eq_0_2pi : COROLLARY 0 <= a AND a <= 2*pi IMPLIES
                    (sin(a)=0 IFF a=0 OR a=pi OR a=2*pi)

  cos_eq_0_2pi : COROLLARY 0 <= a AND a <= 2*pi IMPLIES
                    (cos(a)=0 IFF a=pi/2 OR a=3*pi/2)

  sin_eq_0     : LEMMA sin(a) = 0 IFF EXISTS (i: int): a = i * pi

  cos_eq_0     : LEMMA cos(a) = 0 IFF EXISTS (i: int): a = i * pi + pi/2

% ---------------------- Maximum Points -----------------------------

  sin_eq_1     : LEMMA sin(a) = 1 IFF EXISTS (i: int): a = 2 * i * pi + pi/2
  cos_eq_1     : LEMMA cos(a) = 1 IFF EXISTS (i: int): a = 2 * i * pi

END trig_basic

quality98%

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.