|
trig_inverses: THEORY
%----------------------------------------------------------------------------
% Interface to Inverse Trig Function
%
% Rick Butler 1/8/08
%----------------------------------------------------------------------------
BEGIN
IMPORTING trig_basic, asin, acos, atan, atan2
a: VAR real
atan_prep: LEMMA FORALL (x: real_abs_lt_pi2): Tan?(x);
% nnreal_quad1_closed: NONEMPTY_TYPE = {x:nnreal | x <= pi/2}
% nnreal_quad1_open: NONEMPTY_TYPE = {x:nnreal | x < pi/2}
% real_abs_lt_pi: NONEMPTY_TYPE = {x:real | -pi/2 < x AND x < pi/2}
% posreal_lt_pi: NONEMPTY_TYPE = {x:posreal| x < pi}
% nnreal_le_pi : NONEMPTY_TYPE = {x:nnreal | x <= pi}
% 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}
% ---------- ArcSine ----------------- (See asin.pvs)
%
% asin(x:real_abs_le1): real_abs_le_pi2
%
% asin_0: LEMMA asin(0) = 0
% asin_sqrt_half: LEMMA asin(sqrt(1/2)) = pi/4
% asin_1: LEMMA asin(1) = pi/2
% asin_neg: LEMMA asin(-x) = -asin(x)
% asin_minus1: LEMMA asin(-1) = -pi/2
% asin_minus_sqrt_half: LEMMA asin(-sqrt(1/2)) = -pi/4
AUTO_REWRITE+ asin_0
AUTO_REWRITE+ asin_1
% ---------- ArcCosine ----------------- (See acos.pvs)
%
% acos(x:real_abs_le1): nnreal_le_pi = pi/2 - asin(x)
%
% acos_neg: LEMMA acos(-x) = pi-acos(x)
% acos_0: LEMMA acos(0) = pi/2
% acos_sqrt_half: LEMMA acos(sqrt(1/2)) = pi/4
% acos_1: LEMMA acos(1) = 0
% acos_minus1: LEMMA acos(-1) = pi
% acos_minus_sqrt_half: LEMMA acos(-sqrt(1/2)) = 3*pi/4
AUTO_REWRITE+ acos_0
AUTO_REWRITE+ acos_1
% ---------- ArcTangent ----------------- (See atan.pvs)
%
% atan(x:real): real_abs_lt_pi2
%
% atan_0 : LEMMA atan(0) = 0
% atan_inv : LEMMA atan(1/px) = pi/2-atan(px)
% atan_inv_neg : LEMMA atan(1/nx) = -pi/2-atan(nx)
% atan_neg : LEMMA atan(-x) = -atan(x)
% acot_neg : LEMMA acot(-nzx) = -acot(nzx)
AUTO_REWRITE+ atan_0
% --------- Inverse Relationships (From sincos_def)
x: VAR trig_range
sin_asin: AXIOM sin(asin(x)) = x
cos_acos: AXIOM cos(acos(x)) = x
tan_atan: AXIOM tan(atan(a)) = a
asin_sin: AXIOM FORALL (x:real_abs_le_pi2): asin(sin(x)) = x
acos_cos: AXIOM FORALL (x:nnreal_le_pi): acos(cos(x)) = x
atan_tan: AXIOM FORALL (x:real_abs_lt_pi2): atan(tan(x)) = x
% --- The following provide additional names for the inverse functions
% --- that include their basic property in the type. These are included
% --- for upward compatibility.
% -------------------- Arcsin --------------------
arcsin(y: real_abs_le1): {x: real_abs_le_pi2 | y = sin(x)} = asin(y)
sin_arcsin: AXIOM (FORALL (y: real_abs_le1): sin(arcsin(y)) = y)
arcsin_sin: AXIOM (FORALL (x: real_abs_lt_pi2): arcsin(sin(x)) = x)
% -------------------- Arccos --------------------
arccos(y: real_abs_le1): {x: nnreal_le_pi | y = cos(x)} = acos(y)
cos_arccos: AXIOM (FORALL (y: real_abs_le1): cos(arccos(y)) = y)
arccos_cos: AXIOM (FORALL (x: nnreal_le_pi): arccos(cos(x)) = x)
% -------------------- Arctan --------------------
arctan_prep: LEMMA FORALL (x: real_abs_lt_pi2): Tan?(x);
arctan(y: real): {x: real_abs_lt_pi2 | y = tan(x)} = atan(y)
tan_arctan: AXIOM (FORALL (y: real): tan(arctan(y)) = y)
arctan_tan: AXIOM (FORALL (x: real_abs_lt_pi2): arctan(tan(x)) = x)
END trig_inverses
¤ Dauer der Verarbeitung: 0.18 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.
|
