Quelle  hyperbolicx.pvs   Sprache: PVS

%------------------------------------------------------------------------------
% Hyperbolic functions
%
%     Author: David Lester, Manchester University
%
%     Version 1.0            18/2/09   Initial Release Version
%------------------------------------------------------------------------------

hyperbolicx: THEORY

BEGIN

  IMPORTING lnexp_fnd@hyperbolic, log, exp

  x:    VAR real
  nzx:  VAR nzreal
  sx:   VAR smallreal
  cx:   VAR cauchy_real
  cnzx: VAR cauchy_nzreal
  csx:  VAR cauchy_smallreal

  cauchy_sinh(cx):  [nat->int]
   = cauchy_div2n(cauchy_sub(cauchy_exp(cx),cauchy_exp(cauchy_neg(cx))),1)
  cauchy_cosh(cx):  [nat->int]
   = cauchy_div2n(cauchy_add(cauchy_exp(cx),cauchy_exp(cauchy_neg(cx))),1)

  sinh_lemma: LEMMA cauchy_prop(x,cx) => cauchy_prop(sinh(x),cauchy_sinh(cx))
  cosh_lemma: LEMMA cauchy_prop(x,cx) => cauchy_prop(cosh(x),cauchy_cosh(cx))

  cauchy_sinh_type: JUDGEMENT cauchy_sinh(cx)   HAS_TYPE cauchy_real
  cauchy_cosh_type: JUDGEMENT cauchy_cosh(cx)   HAS_TYPE cauchy_posreal

  cauchy_coth(cnzx):[nat->int]
   = cauchy_div(cauchy_cosh(cnzx),cauchy_sinh(cnzx))

  cauchy_tanh(cx):  [nat->int] = cauchy_div(cauchy_sinh(cx),cauchy_cosh(cx))
  cauchy_csch(cnzx):[nat->int] = cauchy_inv(cauchy_sinh(cnzx))
  cauchy_sech(cx)  :[nat->int] = cauchy_inv(cauchy_cosh(cx))

  tanh_lemma: LEMMA cauchy_prop(x,cx) => cauchy_prop(tanh(x),cauchy_tanh(cx))
  sech_lemma: LEMMA cauchy_prop(x,cx) => cauchy_prop(sech(x),cauchy_sech(cx))
  coth_lemma: LEMMA cauchy_prop(nzx,cnzx)
                                   => cauchy_prop(coth(nzx),cauchy_coth(cnzx))
  csch_lemma: LEMMA cauchy_prop(nzx,cnzx)
                                   => cauchy_prop(csch(nzx),cauchy_csch(cnzx))

  cauchy_tanh_type: JUDGEMENT cauchy_tanh(cx)   HAS_TYPE cauchy_smallreal
  cauchy_coth_type: JUDGEMENT cauchy_coth(cnzx) HAS_TYPE cauchy_nzreal
  cauchy_csch_type: JUDGEMENT cauchy_csch(cnzx) HAS_TYPE cauchy_nzreal
  cauchy_sech_type: JUDGEMENT cauchy_sech(cx)   HAS_TYPE cauchy_posreal


  cauchy_ge1?(c:[nat->int]):bool = EXISTS (x:posreal_ge1): cauchy_prop(x,c)

  cauchy_ge1: TYPE+ = (cauchy_ge1?) CONTAINING cauchy_int(1)

  JUDGEMENT cauchy_ge1 SUBTYPE_OF cauchy_posreal

  ge1x:  VAR posreal_ge1
  cge1x: VAR cauchy_ge1

  cauchy_asinh(cx):[nat->int]
   = cauchy_ln(cauchy_add(cx,cauchy_sqrt(cauchy_add(cauchy_mul(cx,cx),
                                                    cauchy_int(1)))))

  cauchy_acosh(cge1x):[nat->int]
   = cauchy_ln(cauchy_add(cge1x,cauchy_sqrt(cauchy_sub(cauchy_mul(cge1x,cge1x),
                                                       cauchy_int(1)))))

  cauchy_atanh(csx):[nat->int]
   = cauchy_div2n(cauchy_ln(cauchy_div(cauchy_add(cauchy_int(1),csx),
                                       cauchy_sub(cauchy_int(1),csx))),1)

  asinh_lemma: LEMMA cauchy_prop(x,cx) =>
                     cauchy_prop(asinh(x),cauchy_asinh(cx))
  acosh_lemma: LEMMA cauchy_prop(ge1x,cge1x) =>
                     cauchy_prop(acosh(ge1x),cauchy_acosh(cge1x))
  atanh_lemma: LEMMA cauchy_prop(sx,csx) =>
                     cauchy_prop(atanh(sx),cauchy_atanh(csx))

  cauchy_asinh_type: JUDGEMENT cauchy_asinh(cx)    HAS_TYPE cauchy_real
  cauchy_acosh_type: JUDGEMENT cauchy_acosh(cge1x) HAS_TYPE cauchy_nnreal
  cauchy_atanh_type: JUDGEMENT cauchy_atanh(csx)   HAS_TYPE cauchy_real

END hyperbolicx