|
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
¤ Dauer der Verarbeitung: 0.16 Sekunden
(vorverarbeitet)
¤
|
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.
|
