Quelle  sign3.pvs   Sprache: PVS

%% 3-valued sign

%% Created by Cesar Munoz

sign3 : THEORY
BEGIN

  IMPORTING sign,sq

  Sign3 : TYPE = {i:int |i=1 OR i=-1 OR i=0} 

  sign3(x:real): Sign3 = IF x = 0 THEN 0
                         ELSIF x > 0 THEN 1
                         ELSE -1 ENDIF
  eps,
  eps1,eps2 : VAR Sign3
  epsnz     : VAR Sign 
  x,y,z     : VAR real

  sign3_mult_clos: JUDGEMENT *(eps1,eps2) HAS_TYPE Sign3

  sign3_div_clos : JUDGEMENT  /(eps,epsnz) HAS_TYPE Sign3

  sign3_neg_clos : JUDGEMENT  -(eps1) HAS_TYPE Sign3

  sign3_sq_clos  : JUDGEMENT   sq(eps1) HAS_TYPE Sign3

  sign3_sign     : LEMMA x /= 0 IMPLIES sign3(x)=sign(x)

  sign3_id       : LEMMA sign3(eps) = eps

  sign3_0        : LEMMA sign3(0) = 0

  sign3_eq_1     : LEMMA x > 0 IMPLIES sign3(x) = 1

  sign3_eq_neg1  : LEMMA x < 0 IMPLIES sign3(x) = -1

  sign3_pos      : LEMMA sign3(x)*x >= 0

  sign3_abs      : LEMMA abs(x) = sign3(x)*x

  sign3_nneg     : LEMMA sign3(x)*x >= 0

  square_eps     : LEMMA eps*eps <= 1

  sq_eps         : LEMMA sq(eps) <= 1

  sq_sign3       : LEMMA sq(sign3(x)) <= 1

  sign3_times_abs: LEMMA sign3(x)*abs(x) = x

  abs_sign3      : LEMMA eps*x > 0 IMPLIES eps*x = abs(x)

  sign3_neg      : LEMMA -sign3(x) = sign3(-x)

  sign3_minus    : LEMMA -sign3(x-y) = sign3(y-x)

  sign3_mult     : LEMMA  sign3(x*y) = sign3(x)*sign3(y)

  sign3_div      : LEMMA  y /= 0 IMPLIES sign3(x/y) = sign3(x)*sign3(y)

  sign3_mult_pos : LEMMA x > 0 IMPLIES sign3(x*y) = sign3(y)

  sign3_div_pos1 : LEMMA x > 0 AND y /= 0 IMPLIES sign3(x/y) = sign3(y)

  sign3_div_pos2 : LEMMA y > 0 IMPLIES sign3(x/y) = sign3(x)

  sign3_mult_neg : LEMMA x < 0 IMPLIES sign3(x*y) = -sign3(y)

  sign3_div_neg1 : LEMMA x < 0 AND y /= 0 IMPLIES sign3(x/y) = -sign3(y)

  sign3_div_neg2 : LEMMA y < 0 IMPLIES sign3(x/y) = -sign3(x)

  sign3_div_mult : LEMMA 
    y /= 0 IMPLIES sign3(x)/sign3(y) = sign3(x)*sign3(y)

  sign3_and_abs  : LEMMA sign3(x) = sign3(y) AND abs(x) = abs(y) IFF x = y

  sign3_le : LEMMA
    x <= y IMPLIES sign3(x) <= sign3(y)

  sign3_ge : LEMMA
    x >= y IMPLIES sign3(x) >= sign3(y)

  AUTO_REWRITE+ sign3_0

END sign3