|
%------------------------------------------------------------------------------
% Generalized Root function
%
% Author: David Lester, Manchester University & NIA
%
% Version 1.0 19/08/08 Initial version (DRL)
%
% (We can take nth-roots of negative numbers provided n is odd.
% I could believe that the type-constraints make this unusable;
% feedback appreciated.)
%------------------------------------------------------------------------------
root: THEORY
BEGIN
IMPORTING reals@sign,
nn_root
x,y,z: VAR real
epsilon,
delta: VAR posreal
pm,pn: VAR posnat
nx: VAR nnreal
root(x:real,pn:{pm | x >= 0 OR odd?(pm)}):real = nn_root(abs(x),pn)*sign(x)
root_0n: LEMMA root(0,pn) = 0
root_1n: LEMMA root(1,pn) = 1
root_x1: LEMMA root(x,1) = x
root_nn_root_rew: LEMMA root(nx,pn) = nn_root(nx,pn)
root_expt: LEMMA FORALL (x:real,pn:{pm | x >= 0 OR odd?(pm)}):
root(x^pn,pn) = x
expt_root: LEMMA FORALL (x:real,pn:{pm | x >= 0 OR odd?(pm)}):
root(x,pn)^pn = x
root_is_0: LEMMA FORALL (x:real,pn:{pm | x >= 0 OR odd?(pm)}):
root(x,pn) = 0 IFF x = 0
root_pos: LEMMA FORALL (x:real,pn:{pm | x >= 0 OR odd?(pm)}):
root(x,pn) > 0 IFF x > 0
root_neg: LEMMA FORALL (x:real,pn:{pm | x >= 0 OR odd?(pm)}):
root(x,pn) < 0 IFF x < 0
root_gt1: LEMMA FORALL (x:real,pn:{pm | x >= 0 OR odd?(pm)}):
root(x,pn) > 1 IFF x > 1
root_lt1: LEMMA FORALL (x:real,pn:{pm | x >= 0 OR odd?(pm)}):
root(x,pn) < 1 IFF x < 1
neg_root: LEMMA odd?(pn) => root(-x,pn) = -root(x,pn)
mult_root: LEMMA FORALL (x,y:real,pn:{pm | x >= 0 AND y >= 0 OR odd?(pm)}):
root(x*y,pn) = root(x,pn)*root(y,pn)
inv_root: LEMMA FORALL (n0x:nzreal,pn:{pm | n0x >= 0 OR odd?(pm)}):
root(1/n0x,pn) = 1/root(n0x,pn)
div_root: LEMMA FORALL (x:real,n0y:nzreal,
pn:{pm | x >= 0 AND n0y >= 0 OR odd?(pm)}):
root(x/n0y,pn) = root(x,pn)/root(n0y,pn)
root_mult: LEMMA FORALL (x:real,pm,pn:{i:posnat | x >= 0 OR odd?(i)}):
root(x,pn*pm) = root(root(x,pn),pm)
root_increasing: LEMMA ((0 < x AND x < 1) OR
(odd?(pn) AND odd?(pm) AND x < -1)) AND
pn < pm => root(x,pn) < root(x,pm)
root_decreasing: LEMMA (1 < x OR
(odd?(pn) AND odd?(pm) AND -1 < x AND x < 0)) AND
pn < pm => root(x,pn) > root(x,pm)
continuous_alt_root:
LEMMA FORALL (x:real,epsilon:posreal,
pn:{pm | x >= 0 AND y >= 0 OR odd?(pm)}):
EXISTS delta: FORALL (y:{z | z >= 0 OR odd?(pn)}):
abs(x-y) < delta
=> abs(root(x,pn)-root(y,pn)) < epsilon
END root
¤ Dauer der Verarbeitung: 0.18 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.
|
