Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: continuous_functions.pvs Sprache: PVS

Original von: PVS^©

%----------------------------------------------------------------------------
%  Continuous functions [ T -> real]
%
%  Defines:
%      continuous?(f, x0)                  ---- continuity at a point
%      continuous?(f, E)                   ---- continuity on a set
%
%  I some cases PVS has trouble disambiguating these, so the following are
%  defined which helps.  See cont_if_fun for an example.
%
%      continuous_at?(f, x0)               ---- continuity at a point
%      continuous_on?(f, E)                ---- continuity on a set
%
%
%
%----------------------------------------------------------------------------

continuous_functions [ T : TYPE FROM real ] : THEORY
BEGIN

  IMPORTING % lim_of_functions
            reals@real_fun_ops

  f, f1, f2      : VAR [T -> real]
  g              : VAR [T -> nzreal]
  u              : VAR real
  x, x0          : VAR T
  epsilon, delta : VAR posreal
  n              : VAR nat

  %--------------------
  %  Continuity at x0
  %--------------------

  continuous?(f, x0) : bool =
            FORALL epsilon : EXISTS delta : FORALL x :
                abs(x - x0) < delta IMPLIES abs(f(x) - f(x0)) < epsilon

  continuous_at?(f, x0) : MACRO bool = continuous?(f, x0)

  %--- equivalent definitions ---%

  % continuity_def : LEMMA
  %       continuous?(f, x0) IFF convergence(f, x0, f(x0))

  % continuity_def2 : LEMMA
  %       continuous?(f, x0) IFF convergent?(f, x0)

  %---------------------------------------------
  %  Continuity of f in a subset of its domain
  %---------------------------------------------

  E: VAR setof[T]

  continuous_on?(f, E): bool = FORALL (x0: (E)): FORALL epsilon:
     EXISTS delta: FORALL (x:(E)): abs(x - x0) < delta IMPLIES abs(f(x) - f(x0)) < epsilon

  % continuous_on_def: LEMMA
  %     continuous_on?(f, E) IFF FORALL (y: (E)): convergence(f, E, y, f(y))

  %------------------------------------------
  %  Operations preserving continuity at x0
  %------------------------------------------

  sum_continuous  : AXIOM continuous?(f1, x0) AND continuous?(f2, x0)
                           IMPLIES continuous?(f1 + f2, x0)

  diff_continuous : AXIOM continuous?(f1, x0) AND continuous?(f2, x0)
                           IMPLIES continuous?(f1 - f2, x0)

  prod_continuous : AXIOM continuous?(f1, x0) AND continuous?(f2, x0)
                           IMPLIES continuous?(f1 * f2, x0)

  const_continuous: AXIOM continuous?(const_fun(u), x0)

  scal_continuous : AXIOM continuous?(f, x0) IMPLIES continuous?(u * f, x0)

  neg_continuous  : AXIOM continuous?(f, x0) IMPLIES continuous?(- f, x0)

  div_continuous  : AXIOM continuous?(f, x0) AND continuous?(g, x0)
                            IMPLIES continuous?(f/g, x0)

  inv_continuous  : AXIOM continuous?(g, x0) IMPLIES continuous?(1/g, x0)

  identity_continuous: AXIOM continuous?(I[T], x0)

  expt_continuous : LEMMA continuous?(f, x0) IMPLIES continuous?(f^n, x0)

  %---------------------------------------------
  %  Continuity of f in a subset of its domain
  %---------------------------------------------

  F: VAR setof[real]

  %--- Operation preserving continuity in E ---%

  sum_set_continuous :  AXIOM continuous_on?(f1, E) AND continuous_on?(f2, E)
                               IMPLIES continuous_on?(f1 + f2, E)

  diff_set_continuous : AXIOM continuous_on?(f1, E) AND continuous_on?(f2, E)
                               IMPLIES continuous_on?(f1 - f2, E)

  prod_set_continuous : AXIOM continuous_on?(f1, E) AND continuous_on?(f2, E)
                               IMPLIES continuous_on?(f1 * f2, E)

  const_set_continuous: LEMMA continuous_on?(const_fun(u), E)

  scal_set_continuous : AXIOM continuous_on?(f, E) IMPLIES continuous_on?(u * f, E)

  neg_set_continuous  : AXIOM continuous_on?(f, E) IMPLIES continuous_on?(- f, E)

  div_set_continuous  : AXIOM continuous_on?(f, E) AND continuous_on?(g, E)
                              IMPLIES continuous_on?(f/g, E)

  inv_set_continuous  : AXIOM continuous_on?(g, E) IMPLIES continuous_on?(1/g, E)

  identity_set_continuous: LEMMA continuous_on?(I[T], E)


  %---------------------------------
  %  Continuity of f in its domain
  %---------------------------------

  continuous?(f): bool = FORALL x0: continuous?(f, x0)

  continuous_def2: LEMMA continuous?(f) IFF continuous_on?(f, T_pred)

  continuity_subset2: LEMMA continuous?(f) IMPLIES continuous_on?(f, E)

  %--- Properties ---%

  continuous_fun: TYPE+ = { f | continuous?(f) }

  nz_continuous_fun: TYPE = { g | continuous?(g) }

  h, h1, h2: VAR continuous_fun
  h3: VAR nz_continuous_fun

  sum_fun_continuous : JUDGEMENT  +(h1, h2) HAS_TYPE continuous_fun

  diff_fun_continuous: JUDGEMENT  -(h1, h2) HAS_TYPE continuous_fun

  prod_fun_continuous: JUDGEMENT  *(h1, h2) HAS_TYPE continuous_fun

  const_fun_continuous: JUDGEMENT const_fun(u) HAS_TYPE continuous_fun

  scal_fun_continuous: JUDGEMENT  *(u, h) HAS_TYPE continuous_fun

  neg_fun_continuous  : JUDGEMENT -(h) HAS_TYPE continuous_fun

  div_fun_continuous : JUDGEMENT /(h, h3) HAS_TYPE continuous_fun

  id_fun_continuous  : JUDGEMENT I[T] HAS_TYPE continuous_fun

  inv_fun_continuous : LEMMA continuous?(1/h3)

  m,b: VAR real
  linear_fun_cont    : LEMMA continuous?(LAMBDA x: m*x + b) %% BUTLER

  one_over_x_cont    : LEMMA (FORALL x: x /= 0) IMPLIES
                                       continuous?((LAMBDA x: 1 / x))

  x_to_n_continuous  : LEMMA continuous?(LAMBDA x: x^n)   %% BUTLER

  expt_fun_continuous: LEMMA continuous?(f) IMPLIES continuous?(f^n)

% ------------ Alternate forms and names for convenience ---------------

  sum_cont_fun  : LEMMA continuous?(f1) AND continuous?(f2)
                           IMPLIES continuous?(f1 + f2)

  diff_cont_fun : LEMMA continuous?(f1) AND continuous?(f2)
                           IMPLIES continuous?(f1 - f2)

  prod_cont_fun : LEMMA continuous?(f1) AND continuous?(f2)
                           IMPLIES continuous?(f1 * f2)

  const_cont_fun: LEMMA continuous?(const_fun(u))

  scal_cont_fun : LEMMA continuous?(f) IMPLIES continuous?(u * f)

  neg_cont_fun    : LEMMA continuous?(f) IMPLIES continuous?(- f)

  div_cont_fun  : LEMMA continuous?(f) AND continuous?(g)
                            IMPLIES continuous?(f/g)

  inv_cont_fun  : LEMMA continuous?(g) IMPLIES continuous?(1/g)

  identity_cont_fun: LEMMA continuous?(I[T])

%  id_cont_fun      : LEMMA continuous?(LAMBDA (t: posreal): t)

  expt_cont_fun    : LEMMA continuous?(f) IMPLIES continuous?(f^n)

END continuous_functions

¤ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.