Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: old_sigma.pvs Sprache: SML

Original von: PVS^©

%----------------------------------------------------------------------------
%
%  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

¤ Dauer der Verarbeitung: 0.22 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.