| Quellcodebibliothek Statistik Leitseite 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 sincos_quad.pvs Sprache: PVS |
|||||||||
|
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.14 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28