|
sincos_quad: THEORY
%------------------------------------------------------------------------------
%
% A foundational theory of sin(x) and cos(x) for the interval [0,pi/2]
%
% David Lester Manchester University
%
%------------------------------------------------------------------------------
BEGIN
IMPORTING acos, analysis@deriv_domain,
analysis@indefinite_integral
IMPORTING analysis@deriv_domains
nnreal_quad1_closed: NONEMPTY_TYPE = {x:nnreal | x <= pi/2} CONTAINING 0
nnreal_quad1_open: NONEMPTY_TYPE = {x:nnreal | x < pi/2} CONTAINING 0
posreal_lt_pi: NONEMPTY_TYPE = {x:posreal| x < pi} CONTAINING pi/2
noa_real_lt_pi2 : LEMMA not_one_element?[real_abs_lt_pi2]
noa_real_abs_lt1 : LEMMA not_one_element?[real_abs_lt1]
noa_posreal_lt_pi : LEMMA not_one_element?[posreal_lt_pi]
noa_real_abs_lt_pi2: LEMMA not_one_element?[real_abs_lt_pi2];
noa_posreal_lt_pi4 : LEMMA not_one_element?[{x: posreal | x < pi / 4}]
conn_real_lt_pi2 : LEMMA connected?[real_abs_lt_pi2]
conn_real_abs_lt1 : LEMMA connected?[real_abs_lt1]
conn_posreal_lt_pi : LEMMA connected?[posreal_lt_pi]
deriv_domain_real_abs_lt1 : LEMMA deriv_domain?[real_abs_lt1]
deriv_domain_posreal_lt_pi : LEMMA deriv_domain?[posreal_lt_pi]
deriv_domain_abs_lt_pi2 : LEMMA deriv_domain?[real_abs_lt_pi2]
deriv_domain_posreal_lt_pi4: LEMMA deriv_domain?[{x: posreal | x < pi / 4}]
AUTO_REWRITE+ noa_real_lt_pi2
AUTO_REWRITE+ noa_real_abs_lt1
AUTO_REWRITE+ noa_posreal_lt_pi
AUTO_REWRITE+ noa_real_abs_lt_pi2
AUTO_REWRITE+ noa_posreal_lt_pi4
AUTO_REWRITE+ conn_real_lt_pi2
AUTO_REWRITE+ conn_real_abs_lt1
AUTO_REWRITE+ conn_posreal_lt_pi
AUTO_REWRITE+ deriv_domain_real_abs_lt1
AUTO_REWRITE+ deriv_domain_posreal_lt_pi
AUTO_REWRITE+ deriv_domain_abs_lt_pi2
AUTO_REWRITE+ deriv_domain_posreal_lt_pi4
i: VAR int
a,x,y: VAR real
px: VAR posreal
nnx: VAR nnreal
xs: VAR real_abs_le_pi2
xc: VAR nnreal_le_pi
q1,q2: VAR nnreal_quad1_closed
qo1: VAR nnreal_quad1_open
xa: VAR real_abs_le1
% First Quadrant properties:
sin_value:[real_abs_le_pi2->real_abs_le1] = inverse(asin)
cos_value:[nnreal_le_pi->real_abs_le1] = inverse(acos)
sin_value_bij: LEMMA bijective?[real_abs_le_pi2,real_abs_le1](sin_value)
cos_value_bij: LEMMA bijective?[nnreal_le_pi,real_abs_le1](cos_value)
sin_value_strict_increasing: LEMMA strict_increasing?(sin_value)
sin_value_increasing: LEMMA increasing?(sin_value)
cos_value_strict_decreasing: LEMMA strict_decreasing?(cos_value)
cos_value_decreasing: LEMMA decreasing?(cos_value)
sin_value_neg: LEMMA sin_value(-xs) = -sin_value(xs)
cos_value_neg: LEMMA cos_value(pi-xc) = -cos_value(xc)
sin_eqv_cos_value: LEMMA sin_value(xs) = -cos_value(pi/2+xs)
sin_eqv_cos_quad: LEMMA sin_value(q1) = cos_value(pi/2-q1)
cos_eqv_sin_quad: LEMMA cos_value(q1) = sin_value(pi/2-q1)
sin_value_minus_pi2: LEMMA sin_value(-pi/2) = -1
sin_value_0: LEMMA sin_value(0) = 0
sin_value_pi4: LEMMA sin_value(pi/4) = sqrt(1/2)
sin_value_pi2: LEMMA sin_value(pi/2) = 1
cos_value_0: LEMMA cos_value(0) = 1
cos_value_pi4: LEMMA cos_value(pi/4) = sqrt(1/2)
cos_value_pi2: LEMMA cos_value(pi/2) = 0
cos_value_pi: LEMMA cos_value(pi) = -1
asin_sin_value: LEMMA asin(sin_value(xs)) = xs
acos_cos_value: LEMMA acos(cos_value(xc)) = xc
sin_value_asin: LEMMA sin_value(asin(xa)) = xa
cos_value_acos: LEMMA cos_value(acos(xa)) = xa
sin2_cos2_value: LEMMA sq(sin_value(q1))+sq(cos_value(q1)) = 1
sin_eqv_sqrt_cos_value: LEMMA sqrt(1-sq(cos_value(q1))) = sin_value(q1)
cos_eqv_sqrt_sin_value: LEMMA sqrt(1-sq(sin_value(q1))) = cos_value(q1)
atan_tan_value: LEMMA atan(sin_value(qo1)/cos_value(qo1)) = qo1
sin_value_atan: LEMMA sin_value(atan(x)) = x/sqrt(1+sq(x))
cos_value_atan: LEMMA cos_value(atan(nnx)) = 1/sqrt(1+sq(nnx))
sin_value_pi6: LEMMA sin_value(pi/6) = 1/2
cos_value_pi6: LEMMA cos_value(pi/6) = sqrt(3)/2
cos_value_sum: LEMMA cos_value(q1+q2) =
cos_value(q1)*cos_value(q2)-sin_value(q1)*sin_value(q2)
sin_value_diff: LEMMA sin_value(q1-q2) =
sin_value(q1)*cos_value(q2)-cos_value(q1)*sin_value(q2)
sin_value_derivable: LEMMA FORALL (x:real_abs_lt_pi2):
derivable?[real_abs_lt_pi2]((LAMBDA (x:real_abs_lt_pi2): sin_value(x)),x)
sin_value_derivable_fun: LEMMA
derivable?[real_abs_lt_pi2](LAMBDA (x:real_abs_lt_pi2): sin_value(x))
deriv_sin_value : LEMMA
deriv[real_abs_lt_pi2](LAMBDA (x:real_abs_lt_pi2): sin_value(x))
= (LAMBDA (x:real_abs_lt_pi2): cos_value (abs(x)))
sin_value_sum: LEMMA IF q1+q2 <= pi/2 THEN sin_value(q1+q2)
ELSE cos_value(q1+q2-pi/2) ENDIF
= sin_value(q1)*cos_value(q2)+cos_value(q1)*sin_value(q2)
cos_value_diff: LEMMA IF q1-q2 < 0 THEN cos_value(q2-q1)
ELSE cos_value(q1-q2) ENDIF
= cos_value(q1)*cos_value(q2)+sin_value(q1)*sin_value(q2)
cos_value_derivable: LEMMA FORALL (x:posreal_lt_pi):
derivable?[posreal_lt_pi]((LAMBDA (x:posreal_lt_pi): cos_value(x)),x)
cos_value_derivable_fun: LEMMA
derivable?[posreal_lt_pi](LAMBDA (x:posreal_lt_pi): cos_value(x))
deriv_cos_value: LEMMA
deriv[posreal_lt_pi](LAMBDA (x:posreal_lt_pi): cos_value(x))
= (LAMBDA (x:posreal_lt_pi): IF x < pi/2 THEN -sin_value(x)
ELSE -sin_value(pi-x) ENDIF)
END sincos_quad
¤ Dauer der Verarbeitung: 0.2 Sekunden
(vorverarbeitet)
¤
|
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.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
