|
%----------------------------------------------------------------------------
%
% Authors: Cesar Munoz, Alfons Geser NASA ICASE
%
% NOTE:
% Introduced root(a,b,c,eps). x1 and x2 are defined as macros for
% backward compatibility.
% Predicate solvable has been eliminated.
% not_solvable_quadratic is a LEMMA rather than an AXIOM
% Definitions of x1 and x2 revised.
% bac renamed discr
% Consequences of canonical_sq added.
% Vieta's equations (lemma vieta1 and vieta2) added.
% x1_eq_x2 added.
%
%----------------------------------------------------------------------------
quadratic : THEORY
BEGIN
IMPORTING sqrt, sign
a : VAR nonzero_real
aa,b,c : VAR real
x : VAR real
eps : VAR Sign
k : VAR nzreal
canonical_sq : LEMMA
a*sq(x) + b*x + c =
a*sq(x + b/(2*a)) + (4*a*c - sq(b))/(4*a)
discr(a,b,c) : real = sq(b) - 4*a*c
discr_symm : LEMMA
discr(a,b,c) = discr(-a,-b,-c)
discr_scalar : LEMMA
discr(k*a,k*b,k*c) = sq(k)*discr(a,b,c)
a_gt_0_discr_gt_0 : LEMMA
a > 0 AND a*sq(x) + b*x + c < 0 IMPLIES
discr(a,b,c) > 0
a_gt_0_discr_ge_0 : LEMMA
a > 0 AND a*sq(x) + b*x + c <= 0 IMPLIES
discr(a,b,c) >= 0
a_lt_0_discr_gt_0 : LEMMA
a < 0 AND a*sq(x) + b*x + c > 0 IMPLIES
discr(a,b,c) > 0
a_lt_0_discr_ge_0 : LEMMA
a < 0 AND a*sq(x) + b*x + c >= 0 IMPLIES
discr(a,b,c) >= 0
discr_ge_0 : LEMMA
a*sq(x) + b*x + c = 0 IMPLIES
discr(a,b,c) >= 0
root(a:nonzero_real,b:real,c:real|discr(a,b,c)>=0,eps:Sign):real =
(-b + eps*sqrt(discr(a,b,c)))/(2*a)
root_symm : LEMMA
discr(a,b,c) >= 0 IMPLIES
root(a,b,c,eps) = root(-a,-b,-c,-eps)
root_scalar : LEMMA
discr(a,b,c) >= 0 IMPLIES
root(k*a,k*b,k*c,eps) = root(a,b,c,sign(k)*eps)
x1(a:nonzero_real,b:real,c:real|discr(a,b,c)>=0) : MACRO real =
root(a,b,c,1)
x2(a:nonzero_real,b:real,c:real|discr(a,b,c)>=0) : MACRO real =
root(a,b,c,-1)
vieta1: LEMMA
discr(a,b,c) >= 0 =>
x1(a,b,c)+x2(a,b,c) = -b/a
vieta_add: LEMMA
discr(a,b,c) >= 0 =>
root(a,b,c,eps)+root(a,b,c,-eps) = -b/a
vieta2: LEMMA
discr(a,b,c) >= 0 =>
x1(a,b,c)*x2(a,b,c) = c/a
vieta_mult: LEMMA
discr(a,b,c) >= 0 =>
root(a,b,c,eps)*root(a,b,c,-eps) = c/a
root_neq_0 : LEMMA
discr(a,b,c) >= 0 AND
c /= 0 IMPLIES
root(a,b,c,eps) /= 0
root_eq_0 : LEMMA
discr(a,b,c) >= 0 IMPLIES
(c = 0 AND (b = 0 OR eps = sign(b)) IFF
root(a,b,c,eps) = 0)
c_eq_0 : LEMMA
discr(a,b,c) >= 0 AND
b = 0 AND
a*c >= 0
IMPLIES
c = 0
root_eq : LEMMA
discr(a,b,c) >= 0 IMPLIES
(discr(a,b,c) = 0 IFF x1(a,b,c) = x2(a,b,c))
roots_eq_0 : LEMMA
discr(a,b,c) >= 0 IMPLIES
(b = 0 AND a*c >= 0
IFF
root(a,b,c,-eps) = 0 AND root(a,b,c,eps) = 0)
root_inv : LEMMA
discr(a,b,c) >= 0 AND
c /= 0 IMPLIES
root(a,b,c,eps) = 1/root(c,b,a,-eps)
root_le : LEMMA
discr(a,b,c) >= 0 IMPLIES
root(a,b,c,-sign(a)) <= root(a,b,c,sign(a))
root_lt : LEMMA
discr(a,b,c) > 0 IMPLIES
root(a,b,c,-sign(a)) < root(a,b,c,sign(a))
roots_le_ge_0 : LEMMA
discr(a,b,c) >= 0 IMPLIES
(a*c <= 0 AND
(c=0 AND b=0 OR eps=sign(a))
IFF
root(a,b,c,-eps) <= 0 AND
root(a,b,c,eps) >= 0)
roots_lt_gt_0 : LEMMA
discr(a,b,c) >= 0 IMPLIES
(a*c < 0 AND eps=sign(a)
IFF
root(a,b,c,-eps) < 0 AND
root(a,b,c,eps) > 0)
sign_ab_roots_ge_0 : LEMMA
discr(a,b,c) >= 0 AND
a*c >= 0
IMPLIES
-sign(a*b)*root(a,b,c,eps) >= 0
roots_ge_0 : LEMMA
discr(a,b,c) >= 0
IMPLIES
(a*c >= 0 AND a*b <= 0
IFF
root(a,b,c,-eps) >= 0 AND
root(a,b,c,eps) >= 0)
roots_le_0 : LEMMA
discr(a,b,c) >= 0 IMPLIES
(a*c >= 0 AND a*b >= 0
IFF
root(a,b,c,-eps) <= 0 AND
root(a,b,c,eps) <= 0)
sign_ab_roots_gt_0 : LEMMA
discr(a,b,c) >= 0 AND
a*c > 0
IMPLIES
-sign(a*b)*root(a,b,c,eps) > 0
roots_gt_0 : LEMMA
discr(a,b,c) >= 0 IMPLIES
(a*c > 0 AND a*b <= 0
IFF
root(a,b,c,-eps) > 0 AND
root(a,b,c,eps) > 0)
roots_lt_0 : LEMMA
discr(a,b,c) >= 0 IMPLIES
(a*c > 0 AND a*b >= 0
IFF
root(a,b,c,-eps) < 0 AND
root(a,b,c,eps) < 0)
root_gt_0 : LEMMA
discr(a,b,c) >= 0 IMPLIES
((a*c > 0 AND a*b <= 0) OR
(a*c <= 0 AND eps=sign(a) AND (c /= 0 OR a*b < 0))
IFF
root(a,b,c,eps) > 0)
root_ge_0 : LEMMA
discr(a,b,c) >= 0 IMPLIES
((a*c >= 0 AND a*b <= 0) OR
(a*c <= 0 AND eps = sign(a))
IFF
root(a,b,c,eps) >= 0)
root_lt_0 : LEMMA
discr(a,b,c) >= 0 IMPLIES
((a*c > 0 AND a*b >= 0) OR
(a*c <= 0 AND eps=-sign(a) AND (c /= 0 OR a*b > 0))
IFF
root(a,b,c,eps) < 0)
root_le_0 : LEMMA
discr(a,b,c) >= 0 IMPLIES
((a*c >= 0 AND a*b >= 0) OR
(a*c <= 0 AND eps = -sign(a))
IFF
root(a,b,c,eps) <= 0)
quadratic_aux : LEMMA
discr(a,b,c) >= 0 =>
a*sq(x)+b*x+c = a*(x-x1(a,b,c))*(x-x2(a,b,c))
quadratic_eq_0 : LEMMA
(a*sq(x) + b*x + c = 0 IFF
discr(a,b,c) >= 0 AND
(x = x1(a,b,c) OR
x = x2(a,b,c)))
solvable_quadratic : LEMMA
discr(a,b,c) >= 0 IFF
EXISTS (x) : a*sq(x) + b*x + c = 0
not_solvable_quadratic : LEMMA
NOT discr(a,b,c) >= 0 =>
((FORALL(x) : a * sq(x) + b*x + c > 0) OR
(FORALL(x) : a * sq(x) + b*x + c < 0))
quadratic_le_0 : LEMMA
a*sq(x) + b*x + c <= 0 IFF
((discr(a,b,c) >= 0 AND
((a > 0 AND x2(a,b,c) <= x AND x <= x1(a,b,c)) OR
(a < 0 AND (x <= x1(a,b,c) OR x2(a,b,c) <= x)))) OR
(discr(a,b,c) < 0 AND c <= 0))
quadratic_lt_0 : LEMMA
a*sq(x) + b*x + c < 0 IFF
((discr(a,b,c) >= 0 AND
((a > 0 AND x2(a,b,c) < x AND x < x1(a,b,c)) OR
(a < 0 AND ((x < x1(a,b,c) AND x < x2(a,b,c)) OR
(x1(a,b,c) < x AND x2(a,b,c) < x))))) OR
(discr(a,b,c) < 0 AND c < 0))
quadratic_ge_0 : LEMMA
a*sq(x) + b*x + c >= 0 IFF
((discr(a,b,c) >= 0 AND
((a < 0 AND x1(a,b,c) <= x AND x <= x2(a,b,c)) OR
(a > 0 AND (x <= x2(a,b,c) OR x1(a,b,c) <= x)))) OR
(discr(a,b,c) < 0 AND c >= 0))
quadratic_gt_0 : LEMMA
a*sq(x) + b*x + c > 0 IFF
((discr(a,b,c) >= 0 AND
((a < 0 AND x1(a,b,c) < x AND x < x2(a,b,c)) OR
(a > 0 AND (x < x2(a,b,c) OR x1(a,b,c) < x)))) OR
(discr(a,b,c) < 0 AND c > 0))
%% quadratic equations that may collapse to linear equations
%% and the solutions of such equations
solvable?(aa,b,c): bool =
(aa = 0 AND b /= 0 OR aa /= 0 AND discr(aa,b,c) >= 0)
solution(aa,b,(c | solvable?(aa,b,c)), eps: Sign): real =
IF aa = 0 THEN -c/b ELSE root(aa,b,c,eps) ENDIF
quadratic_eq_0_full: THEOREM
aa*sq(x) + b*x + c = 0 IFF
aa = 0 AND b = 0 AND c = 0 OR
solvable?(aa,b,c) AND (x = solution(aa,b,c,-1) OR x = solution(aa,b,c,1))
%% --- Some unexpanded forms ---
quadratic(a,b,c: real)(x): real = a*sq(x) + b*x + c
complete_square : LEMMA
quadratic(a,b,c)(x) = a * sq(x + b/(2*a)) + (4*a*c - sq(b))/(4*a)
quad_eq_0 : THEOREM
quadratic(a,b,c)(x) = 0 IFF
discr(a,b,c) >= 0 AND EXISTS (eps): x = root(a,b,c,eps)
quad_eq_0_full: THEOREM
quadratic(aa,b,c)(x) = 0 IFF
aa = 0 AND b = 0 AND c = 0 OR
solvable?(aa,b,c) AND EXISTS (eps): x = solution(aa,b,c,eps)
END quadratic
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.24Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
Ziele
Entwicklung einer Software für die statische Quellcodeanalyse
|
