|
%------------------------------------------------------------------------------
% Generalized Power function (without ln/exp)
%
% Author: David Lester, Manchester University & NIA
%
% Version 1.0 19/08/08 Initial version (DRL)
%
% (Note: we follow the prelude, and define 0^0 = 1)
%
%------------------------------------------------------------------------------
real_expt: THEORY
BEGIN
IMPORTING nnreal_expt,
root
x,y: VAR nnreal
a,b: VAR real
i: VAR int
pn: VAR posnat
na: VAR negreal
n0x: VAR nzreal
pa,pb,px,py,r: VAR posreal
gt1x: VAR {r | r > 1}
lt1x: VAR {r | r < 1}
^(x:nnreal,a:{a | a >= 0 OR x > 0}):nnreal
= IF a >= 0 THEN nnreal_expt(x,a) ELSE nnreal_expt(1/x,-a) ENDIF
real_expt_nnreal_rew: LEMMA x^y = nnreal_expt(x,y)
real_expt_int_rew: LEMMA FORALL (i:{i | x /= 0 OR i >= 0}):
x^i = exponentiation.^(x,i)
real_expt_root_rew: LEMMA x^(1/pn) = root(x,pn)
real_expt_x0: LEMMA x^0 = 1
real_expt_1a: LEMMA 1^a = 1
real_expt_0x: LEMMA 0^x = IF x = 0 THEN 1 ELSE 0 ENDIF
real_expt_x1: LEMMA x^1 = x
real_expt_pos: LEMMA px^a > 0
real_expt_is_0: LEMMA FORALL (x:nnreal,a:{a | a >= 0 OR x > 0}):
x^a = 0 IFF x = 0 AND a > 0
real_expt_gt1: LEMMA FORALL (x:nnreal,a:{a | a >= 0 OR x > 0}):
x^a > 1 IFF (x > 1 AND a > 0 OR x < 1 AND a < 0)
real_expt_lt1: LEMMA FORALL (x:nnreal,a:{a | a >= 0 OR x > 0}):
x^a < 1 IFF (x < 1 AND a > 0 OR x > 1 AND a < 0)
inv_real_expt: LEMMA (1/px)^a = 1/(px^a)
mult_real_expt: LEMMA FORALL (x,y:nnreal,a:{a | a >= 0 OR x > 0 AND y > 0}):
(x*y)^a = x^a * y^a
div_real_expt: LEMMA FORALL (x:nnreal,py:posreal,a:{a | a >= 0 OR x > 0}):
(x/py)^a = x^a / py^a
real_expt_neg: LEMMA px^(-a) = (1/px)^a
real_expt_plus: LEMMA FORALL (x:nnreal,a,b:{a | a >= 0 OR x > 0}):
x^(a+b) = x^a * x^b
real_expt_minus:LEMMA px^(a-b) = px^a / px^b
real_expt_times:LEMMA FORALL (x:nnreal,a:{a | a >= 0 OR x > 0},
b:{b | b >= 0 OR x^a > 0}):
x^(a*b) = (x^a)^b
real_expt_decreasing: LEMMA a < b => lt1x^a > lt1x^b
real_expt_increasing: LEMMA a < b => gt1x^a < gt1x^b
real_expt_strict_increasing: LEMMA x < y => x^pa < y^pa
real_expt_strict_decreasing: LEMMA px < y => px^na > y^na
both_sides_real_expt_lt: LEMMA x^pa < y^pa IFF x < y
both_sides_real_expt_le: LEMMA x^pa <= y^pa IFF x <= y
both_sides_real_expt_gt: LEMMA x^pa > y^pa IFF x > y
both_sides_real_expt_ge: LEMMA x^pa >= y^pa IFF x >= y
both_sides_real_expt: LEMMA x^pa = y^pa IFF x = y
both_sides_real_expt_lt1_lt: LEMMA lt1x^a < lt1x^b IFF b < a
both_sides_real_expt_lt1_le: LEMMA lt1x^a <= lt1x^b IFF b <= a
both_sides_real_expt_lt1_gt: LEMMA lt1x^a > lt1x^b IFF b > a
both_sides_real_expt_lt1_ge: LEMMA lt1x^a >= lt1x^b IFF b >= a
both_sides_real_expt_gt1_lt: LEMMA gt1x^a < gt1x^b IFF a < b
both_sides_real_expt_gt1_le: LEMMA gt1x^a <= gt1x^b IFF a <= b
both_sides_real_expt_gt1_gt: LEMMA gt1x^a > gt1x^b IFF a > b
both_sides_real_expt_gt1_ge: LEMMA gt1x^a >= gt1x^b IFF a >= b
both_sides_real_expt_eq: LEMMA x^pa = x^pb IFF x = 0 OR x = 1 OR pa = pb
END real_expt
¤ Dauer der Verarbeitung: 0.1 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.
|
