Quelle real_continuity.pvs Sprache: PVS

%------------------------------------------------------------------------------
% Continuous functions [T->real]
%
%     Author: David Lester, Manchester University
%
%     Version 1.0            15/09/08  Initial Version
%------------------------------------------------------------------------------

real_continuity[T:TYPE,(IMPORTING metric_def[T]) d:metric]: THEORY

BEGIN

  IMPORTING
    metric_continuity[T,d,real,(lambda (x,y:real): abs(x-y))],
    topology@constant_continuity[T,metric_induced_topology[T,d],
                                 real,metric_induced_topology[real,
                                            (lambda (x,y:real) :abs(x-y))]],
    reals@real_fun_ops_aux[T],
    power@real_expt,
    power@log,
    power@real_fun_power[T]

  g,g1,g2: VAR metric_continuous
  n: VAR nat
  u: VAR sequence[metric_continuous]
  c: VAR real
  a: VAR posreal
  x: VAR T
  h: VAR {g | FORALL x: g(x) >= 0}

%;
%  ^(g,a): MACRO [T->real] = real_fun_power.^(g,a);

  sum_continuous:       JUDGEMENT +(g1,g2)     HAS_TYPE metric_continuous
  opp_continuous:       JUDGEMENT -(g)         HAS_TYPE metric_continuous
  diff_continuous:      JUDGEMENT -(g1,g2)     HAS_TYPE metric_continuous
  scal_continuous:      JUDGEMENT *(c,g)       HAS_TYPE metric_continuous
  abs_continuous:       JUDGEMENT abs(g)       HAS_TYPE metric_continuous
  expt_real_continuous: JUDGEMENT ^(h,a)       HAS_TYPE metric_continuous
  expt_nat_continuous:  JUDGEMENT expt(g,n)    HAS_TYPE metric_continuous
  sq_continuous:        JUDGEMENT sq(g)        HAS_TYPE metric_continuous
  min_continuous:       JUDGEMENT min(g1,g2)   HAS_TYPE metric_continuous
  max_continuous:       JUDGEMENT max(g1,g2)   HAS_TYPE metric_continuous
  minimum_continuous:   JUDGEMENT minimum(u,n) HAS_TYPE metric_continuous
  maximum_continuous:   JUDGEMENT maximum(u,n) HAS_TYPE metric_continuous
  plus_continuous:      JUDGEMENT plus(g)      HAS_TYPE metric_continuous
  minus_continuous:     JUDGEMENT minus(g)     HAS_TYPE metric_continuous
  prod_continuous:      JUDGEMENT *(g1,g2)     HAS_TYPE metric_continuous

END real_continuity

quality95%

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