SSL trigx.pvs   Interaktion und
PortierbarkeitPVS

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