Quelle exponent_props.pvs Sprache: PVS

exponent_props : THEORY
%-------------------------------------------------------------------------
%  More properties of expt
%
%      by Bruno Dutertre    Royal Holloway & Bedford New College
%
%     9/10/00  -- removed duplications with prelude  RWB
%                 changed names of
%
%                    expt_mult --> expt_of_mult
%                    expt_div  --> expt_of_div
%                    expt_inv  --> expt_of_inv
%
%                 to eliminate duplications with prelude
%
%  Note. This library is retained for upward compatibility only.  New
%        users should use the prelude theorems.
%-------------------------------------------------------------------------
BEGIN

  n, m: VAR nat
  p: VAR posnat
  x, y: VAR real
  z: VAR nzreal
  n0x, n0y: VAR nzreal

%  JUDGEMENT expt(z: nzreal, m: nat) HAS_TYPE nzreal

  abs_expt    : LEMMA abs(expt(x, n)) = expt(abs(x), n)

  expt_ne_0:    LEMMA expt(z, n) /= 0;

%% The following is named abs_of_expt_inv in prelude

  abs_expt_inv: LEMMA abs(1 / expt(z, n)) = 1 / expt(abs(z),n)

  i:  VAR int
  pn: VAR posnat

% The following all appear in the prelude under different names

  zero_hat : LEMMA 0^pn = 0

  mult_hat : LEMMA (n0x * n0y) ^i = n0x^i * n0y^i

  div_hat  : LEMMA (n0x / n0y)^i = n0x^i / n0y^i

  inv_hat  : LEMMA (1 / n0x)^i = 1 / n0x^i

  abs_hat  : LEMMA abs(n0x^i) = abs(n0x)^i

  AUTO_REWRITE+ expt_x0         % LEMMA x^0 = 1
  AUTO_REWRITE+ expt_x1         % LEMMA x^1 = x
  AUTO_REWRITE+ expt_1i         % LEMMA 1^i = 1
  AUTO_REWRITE+ zero_hat

%%  a, b: VAR posreal
%%  lt1x: VAR { a | a < 1}
%%  gt1x: VAR { a | 1 < a }
%%  expt_lt1_bound1 : LEMMA  expt(lt1x, n) <= 1   %%  In Prelude
%%  expt_lt1_bound2 : LEMMA  expt(lt1x, p) < 1    %%  In Prelude
%%  expt_gt1_bound1 : LEMMA  1 <= expt(gt1x, n)  %%  In Prelude
%%  expt_gt1_bound2 : LEMMA  1 < expt(gt1x, p)   %%  In Prelude
%%  nnx: VAR nonneg_real
%%  expt_lt1_le     : LEMMA nnx < 1 => nnx^pn <= nnx %%  In Prelude
%%  large_expt      : LEMMA 1 < a  IMPLIES (FORALL b: EXISTS n: b < expt(a, n))
%%  small_expt      : LEMMA a < 1  IMPLIES (FORALL b: EXISTS n: expt(a, n) < b)
END exponent_props

quality95%

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