|
%% Sign definition
%% Created by Cesar Munoz
%% Updated by Alfons Geser
sign : THEORY
BEGIN
IMPORTING sq
Sign : TYPE = {i:nzint|i=1 OR i=-1}
sign(x:real): Sign = IF x >= 0 THEN 1 ELSE -1 ENDIF
eps,
eps1,eps2 : VAR Sign
x,y,z : VAR real
nnx : VAR nnreal
nx : VAR negreal
n : VAR nat
sign_mult_clos: JUDGEMENT *(eps1,eps2) HAS_TYPE Sign
sign_div_clos : JUDGEMENT /(eps1,eps2) HAS_TYPE Sign
sign_neg_clos : JUDGEMENT -(eps1) HAS_TYPE Sign
sign_sq_clos : JUDGEMENT sq(eps1) HAS_TYPE Sign
sign_id : LEMMA sign(eps) = eps
sign_pos : LEMMA sign(x)*x >= 0
sign_eq_1 : LEMMA sign(nnx) = 1
sign_eq_neg1 : LEMMA sign(nx) = -1
sign_nat : LEMMA sign(n) = 1
sign_abs : LEMMA abs(x) = sign(x)*x
sign_nneg : LEMMA sign(x)*x >= 0
square_eps : LEMMA eps*eps = 1
sq_eps : LEMMA sq(eps) = 1
sq_eq_sign : LEMMA sq(x) = sq(y) IFF (EXISTS eps: x = eps*y)
sq_sign : LEMMA sq(sign(x)) = 1
sign_sign : LEMMA sign(x)*sign(x) = 1
sign_times_abs: LEMMA sign(x)*abs(x) = x
abs_sign : LEMMA eps*x >= 0 IMPLIES eps*x = abs(x)
abs_pos : LEMMA abs(x) > 0 IFF x /= 0
sign_neg : LEMMA x /= 0 IMPLIES sign(-x) = -sign(x)
sign_minus : LEMMA x /= y IMPLIES -sign(x-y) = sign(y-x)
sign_mult : LEMMA x /= 0 and y/=0 IMPLIES sign(x*y) = sign(x)*sign(y)
sign_div : LEMMA y /= 0 AND x /= 0 IMPLIES sign(x/y) = sign(x)*sign(y)
sign_mult_pos : LEMMA x > 0 IMPLIES sign(x*y) = sign(y)
sign_div_pos1 : LEMMA x > 0 AND y /= 0 IMPLIES sign(x/y) = sign(y)
sign_div_pos2 : LEMMA y > 0 IMPLIES sign(x/y) = sign(x)
sign_mult_neg : LEMMA x < 0 IMPLIES sign(x*y) = sign(-y)
sign_div_neg1 : LEMMA x < 0 AND y /= 0 IMPLIES sign(x/y) = -sign(y)
sign_div_neg2 : LEMMA y < 0 IMPLIES sign(x/y) = sign(-x)
sign_div_mult : LEMMA sign(x)/sign(y) = sign(x)*sign(y)
sign_and_abs : LEMMA sign(x) = sign(y) AND abs(x) = abs(y) IFF x = y
sign_le : LEMMA
x <= y IMPLIES sign(x) <= sign(y)
sign_ge : LEMMA
x >= y IMPLIES sign(x) >= sign(y)
sign_dichotomy : LEMMA
sign(x)=sign(y) OR sign(x)=-sign(y)
AUTO_REWRITE+ sign_nat
sign_ext(x): {sig:real|(sig=-1 OR sig=1 OR sig=0) AND sig*x=abs(x)} =
IF x<0 THEN -1
ELSIF x>0 THEN 1
ELSE 0 ENDIF
sign_ext_mult: LEMMA FORALL (x,y:real): sign_ext(x*y) = sign_ext(x)*sign_ext(y)
END sign
¤ Dauer der Verarbeitung: 0.20 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.
|
