Quelle  util.pvs  Sprache: unbekannt

util : THEORY
BEGIN

  IMPORTING reals@sign,
            reals@sqrt
  
  b,d   : VAR nnreal
  a,c,e : VAR real

  % An algebraic way to determine a*sqrt(b) = e
  eq(a,b,e) : bool = 
    a*e >= 0 AND sq(a)*b = sq(e)

  eq_correct_1 : LEMMA
    eq(a,b,e) IFF a*sqrt(b) = e

  eq_neg : LEMMA
    eq(-a,b,-e) = eq(a,b,e)

  % An algebraic way to determine a*sqrt(b) > e
  gt(a,b,e) : bool =
    IF a >= 0 THEN
      e < 0 OR sq(a)*b > sq(e)
    ELSE
      e < 0 AND sq(a)*b < sq(e) 
    ENDIF

  gt_correct_1 : LEMMA
    gt(a,b,e) IFF a*sqrt(b) > e

  % An algebraic way to determine a*sqrt(b) < e
  lt(a,b,e) : bool =
    gt(-a,b,-e)

  lt_correct_1 : LEMMA
    lt(a,b,e) IFF a*sqrt(b) < e

  % An algebraic way to determine a*sqrt(b) >= e
  ge(a,b,e) : bool =
    NOT lt(a,b,e)

  ge_correct_1 : LEMMA
    ge(a,b,e) IFF a*sqrt(b) >= e

  % An algebraic way to determine a*sqrt(b) <= e
  le(a,b,e) : bool =
    NOT gt(a,b,e)

  le_correct_1 : LEMMA
    le(a,b,e) IFF a*sqrt(b) <= e

  % An algebraic way to determine if a*sqrt(b) > c*sqrt(d)+e
  gt(a,b,c,d,e) : bool =
    IF a >= 0 THEN
      lt(c,d,-e) OR lt(2*e*c,d,sq(a)*b-sq(c)*d-sq(e))
    ELSE
      lt(c,d,-e) AND gt(2*e*c,d,sq(a)*b-sq(c)*d-sq(e))
    ENDIF

  gt_correct_2 : LEMMA
    gt(a,b,c,d,e) IFF a*sqrt(b) > c*sqrt(d)+e

  % An algebraic way to determine a*sqrt(b) < c*sqrt(d)+e
  lt(a,b,c,d,e) : bool =
    gt(-a,b,-c,d,-e)

  lt_correct_2 : LEMMA
    lt(a,b,c,d,e) IFF a*sqrt(b) < c*sqrt(d)+e

  % An algebraic way to determine a*sqrt(b) >= c*sqrt(d)+e
  ge(a,b,c,d,e) : bool =
    NOT lt(a,b,c,d,e)

  ge_correct_2 : LEMMA
    ge(a,b,c,d,e) IFF a*sqrt(b) >= c*sqrt(d)+e

  % An algebraic way to determine a*sqrt(b) <= c*sqrt(d)+e
  le(a,b,c,d,e) : bool =
    NOT gt(a,b,c,d,e)

  le_correct_2 : LEMMA
    le(a,b,c,d,e) IFF a*sqrt(b) <= c*sqrt(d)+e

END util