Quelle trigx.pvs Sprache: PVS

%------------------------------------------------------------------------------
% 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

quality98%

¤ Dauer der Verarbeitung: 0.11 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.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.