|
%------------------------------------------------------------------------------
% sec/cosec/cot
%
% Author: David Lester, Manchester University
%
% Version 1.0 18/2/09 Initial Release Version
%------------------------------------------------------------------------------
trigx: THEORY
BEGIN
IMPORTING sincosx
x: VAR real
c: VAR [nat->int]
sin_nz: TYPE+ = {x | sin(x) /= 0} CONTAINING pi/2
cos_nz: TYPE+ = {x | cos(x) /= 0} CONTAINING 0
nsx: VAR sin_nz
ncx: VAR cos_nz
cauchy_sin_nz?(c):bool = EXISTS nsx: cauchy_prop(nsx,c)
cauchy_cos_nz?(c):bool = EXISTS ncx: cauchy_prop(ncx,c)
cauchy_sin_nz: TYPE+ = (cauchy_sin_nz?) CONTAINING cauchy_div2n(cauchy_pi,1)
cauchy_cos_nz: TYPE+ = (cauchy_cos_nz?) CONTAINING cauchy_zero
JUDGEMENT cauchy_sin_nz SUBTYPE_OF cauchy_real
JUDGEMENT cauchy_cos_nz SUBTYPE_OF cauchy_real
cnsx: VAR cauchy_sin_nz
cncx: VAR cauchy_cos_nz
cauchy_sec(cncx): cauchy_nzreal = cauchy_inv(cauchy_cos(cncx))
cauchy_cosec(cnsx):cauchy_nzreal = cauchy_inv(cauchy_sin(cnsx))
cauchy_tan(cncx):cauchy_real = cauchy_div(cauchy_sin(cncx),cauchy_cos(cncx))
cauchy_cot(cnsx):cauchy_real = cauchy_div(cauchy_cos(cnsx),cauchy_sin(cnsx))
% The following should be in the trig/trig_fnd library ...
sec(ncx): nzreal = 1/cos(ncx)
cosec(nsx):nzreal = 1/sin(nsx)
cot(nsx): real = cos(nsx)/sin(nsx)
sec_lemma: LEMMA cauchy_prop(ncx,cncx) =>
cauchy_prop(sec(ncx),cauchy_sec(cncx))
cosec_lemma: LEMMA cauchy_prop(nsx,cnsx) =>
cauchy_prop(cosec(nsx),cauchy_cosec(cnsx))
tan_lemma: LEMMA cauchy_prop(ncx,cncx) =>
cauchy_prop(tan(ncx),cauchy_tan(cncx))
cot_lemma: LEMMA cauchy_prop(nsx,cnsx) =>
cauchy_prop(cot(nsx),cauchy_cot(cnsx))
END trigx
¤ Dauer der Verarbeitung: 0.15 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.
|
