Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/GAP/tst/testspecial/ (Algebra von RWTH Aachen Version 4.15.1^©) Datei vom 18.9.2025 mit Größe 442 B

Quelle trigx.pvs Sprache: unbekannt

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