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

quality93%

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