PVS: real_props - Theory from Prelude

FDL > PVS > Prelude > real_props : Theory
PVS-2.4 prelude.pvs

 real_props contains useful properties about real numbers.  Most of
 these are known to the decision procedures of PVS, but there are some
 nonlinear ones that cannot be gotten automatically.  Nonlinear
 expressions are those that involve multiplication or division by two
 non-numeric terms.  Thus x*y and x/c are nonlinear, while 2001*x + 39*z is
 linear.  Note that it doesn't matter whether the terms are constants
 or variables, only whether they are actual numbers.

real_props : THEORY
BEGIN

w: VAR real

x: VAR real

y: VAR real

z: VAR real

n0w: VAR nonzero real

n0x: VAR nonzero real

n0y: VAR nonzero real

n0z: VAR nonzero real

nnw: VAR nonneg real

nnx: VAR nonneg real

nny: VAR nonneg real

nnz: VAR nonneg real

pw: VAR posreal

px: VAR posreal

py: VAR posreal

pz: VAR posreal

npw: VAR nonpos real

npx: VAR nonpos real

npy: VAR nonpos real

npz: VAR nonpos real

nw: VAR negreal

nx: VAR negreal

ny: VAR negreal

nz: VAR negreal

inv ne 0: LEMMA (1 / n0x) /= 0

both sides plus1: LEMMA ((x + z) = (y + z)) IFF (x = y)

both sides plus2: LEMMA ((z + x) = (z + y)) IFF (x = y)

both sides minus1: LEMMA ((x - z) = (y - z)) IFF (x = y)

both sides minus2: LEMMA ((z - x) = (z - y)) IFF (x = y)

both sides times1: LEMMA ((x * n0z) = (y * n0z)) IFF (x = y)

both sides times2: LEMMA ((n0z * x) = (n0z * y)) IFF (x = y)

both sides div1: LEMMA ((x / n0z) = (y / n0z)) IFF (x = y)

both sides div2: LEMMA ((n0z / n0x) = (n0z / n0y)) IFF (n0x = n0y)

times plus: LEMMA ((x + y) * (z + w)) = ((x * z) + (x * w) + (y * z) + (y * w))

times div1: LEMMA (x * (y / n0z)) = ((x * y) / n0z)

times div2: LEMMA ((x / n0z) * y) = ((x * y) / n0z)

div times: LEMMA ((x / n0x) * (y / n0y)) = ((x * y) / (n0x * n0y))

div eq zero: LEMMA ((x / n0z) = 0) IFF (x = 0)

div simp: LEMMA (n0x / n0x) = 1

div cancel1: LEMMA (n0z * (x / n0z)) = x

div cancel2: LEMMA ((x / n0z) * n0z) = x

div cancel3: LEMMA ((x / n0z) = y) IFF (x = (y * n0z))

cross mult: LEMMA ((x / n0x) = (y / n0y)) IFF ((x * n0y) = (y * n0x))

add div: LEMMA ((x / n0x) + (y / n0y)) = (((x * n0y) + (y * n0x)) / (n0x * n0y))

minus div1: LEMMA ((x / n0x) - (y / n0y)) = (((x * n0y) - (y * n0x)) / (n0x * n0y))

minus div2: LEMMA ((x / n0x) - (y / n0x)) = ((x - y) / n0x)

div distributes: LEMMA ((x / n0z) + (y / n0z)) = ((x + y) / n0z)

div distributes minus: LEMMA ((x / n0z) - (y / n0z)) = ((x - y) / n0z)

div div1: LEMMA (x / (n0y / n0z)) = ((x * n0z) / n0y)

div div2: LEMMA (x / n0y / n0z) = (x / (n0y * n0z))

idem add is zero: LEMMA ((x + x) = x) IMPLIES (x = 0)

zero times1: LEMMA (0 * x) = 0

zero times2: LEMMA (x * 0) = 0

zero times3: LEMMA ((x * y) = 0) IFF ((x = 0) OR (y = 0))

neg times neg: LEMMA ((-x) * (-y)) = (x * y)

zero is neg zero: LEMMA (-0) = 0

strict lt: LEMMA strict total order?( < )

trich lt: LEMMA (x < y) OR (x = y) OR (y < x)

tri unique lt1: LEMMA (x < y) IMPLIES ((x /= y) AND (NOT (y < x)))

tri unique lt2: LEMMA (x = y) IMPLIES ((NOT (x < y)) AND (NOT (y < x)))

zero not lt zero: LEMMA NOT (0 < 0)

neg lt: LEMMA (0 < (-x)) IFF (x < 0)

pos times lt: LEMMA (0 < (x * y)) IFF (((0 < x) AND (0 < y)) OR ((x < 0) AND (y < 0)))

neg times lt: LEMMA ((x * y) < 0) IFF (((0 < x) AND (y < 0)) OR ((x < 0) AND (0 < y)))

quotient pos lt: FORMULA (0 < (1 / n0x)) IFF (0 < n0x)

quotient neg lt: FORMULA ((1 / n0x) < 0) IFF (n0x < 0)

pos div lt: LEMMA (0 < (x / n0y)) IFF (((0 < x) AND (0 < n0y)) OR ((x < 0) AND (n0y < 0)))

neg div lt: LEMMA ((x / n0y) < 0) IFF (((0 < x) AND (n0y < 0)) OR ((x < 0) AND (0 < n0y)))

div mult pos lt1: LEMMA ((z / py) < x) IFF (z < (x * py))

div mult pos lt2: LEMMA (x < (z / py)) IFF ((x * py) < z)

div mult neg lt1: LEMMA ((z / ny) < x) IFF ((x * ny) < z)

div mult neg lt2: LEMMA (x < (z / ny)) IFF (z < (x * ny))

both sides plus lt1: LEMMA ((x + z) < (y + z)) IFF (x < y)

both sides plus lt2: LEMMA ((z + x) < (z + y)) IFF (x < y)

both sides minus lt1: LEMMA ((x - z) < (y - z)) IFF (x < y)

both sides minus lt2: LEMMA ((z - x) < (z - y)) IFF (y < x)

both sides times pos lt1: LEMMA ((x * pz) < (y * pz)) IFF (x < y)

both sides times pos lt2: LEMMA ((pz * x) < (pz * y)) IFF (x < y)

both sides times neg lt1: LEMMA ((x * nz) < (y * nz)) IFF (y < x)

both sides times neg lt2: LEMMA ((nz * x) < (nz * y)) IFF (y < x)

both sides div pos lt1: LEMMA ((x / pz) < (y / pz)) IFF (x < y)

both sides div pos lt2: LEMMA ((pz / px) < (pz / py)) IFF (py < px)

both sides div pos lt3: LEMMA ((nz / px) < (nz / py)) IFF (px < py)

both sides div neg lt1: LEMMA ((x / nz) < (y / nz)) IFF (y < x)

both sides div neg lt2: LEMMA ((pz / nx) < (pz / ny)) IFF (ny < nx)

both sides div neg lt3: LEMMA ((nz / nx) < (nz / ny)) IFF (nx < ny)

lt plus lt1: LEMMA ((x < = y) AND (z < w)) IMPLIES ((x + z) < (y + w))

lt plus lt2: LEMMA ((x < y) AND (z < = w)) IMPLIES ((x + z) < (y + w))

lt minus lt1: LEMMA ((x < = y) AND (w < z)) IMPLIES ((x - z) < (y - w))

lt minus lt2: LEMMA ((x < y) AND (w < = z)) IMPLIES ((x - z) < (y - w))

lt times lt pos1: LEMMA ((px < = y) AND (nnz < w)) IMPLIES ((px * nnz) < (y * w))

lt times lt pos2: LEMMA ((nnx < y) AND (pz < = w)) IMPLIES ((nnx * pz) < (y * w))

%%(TCC) lt_div_lt_pos1_TCC1: OBLIGATION

lt div lt pos1: LEMMA ((px < = y) AND (pz < w)) IMPLIES ((px / w) < (y / pz))

%%(TCC) lt_div_lt_pos2_TCC1: OBLIGATION

lt div lt pos2: LEMMA ((nnx < y) AND (pz < = w)) IMPLIES ((nnx / w) < (y / pz))

lt times lt neg1: LEMMA ((x < = ny) AND (z < npw)) IMPLIES ((ny * npw) < (x * z))

lt times lt neg2: LEMMA ((x < npy) AND (z < = nw)) IMPLIES ((npy * nw) < (x * z))

%%(TCC) lt_div_lt_neg1_TCC1: OBLIGATION

lt div lt neg1: LEMMA ((x < = ny) AND (z < nw)) IMPLIES ((ny / z) < (x / nw))

%%(TCC) lt_div_lt_neg2_TCC1: OBLIGATION

lt div lt neg2: LEMMA ((x < npy) AND (z < = nw)) IMPLIES ((npy / z) < (x / nw))

total le: LEMMA total order?( < =)

dich le: LEMMA (x < = y) OR (y < = x)

zero le zero: LEMMA 0 < = 0

neg le: LEMMA (0 < = (-x)) IFF (x < = 0)

pos times le: LEMMA (0 < = (x * y)) IFF (((0 < = x) AND (0 < = y)) OR ((x < = 0) AND (y < = 0)))

neg times le: LEMMA ((x * y) < = 0) IFF (((0 < = x) AND (y < = 0)) OR ((x < = 0) AND (0 < = y)))

quotient pos le: FORMULA (0 < = (1 / n0x)) IFF (0 < = n0x)

quotient neg le: FORMULA ((1 / n0x) < = 0) IFF (n0x < = 0)

pos div le: LEMMA (0 < = (x / n0y)) IFF (((0 < = x) AND (0 < = n0y)) OR ((x < = 0) AND (n0y < = 0)))

neg div le: LEMMA ((x / n0y) < = 0) IFF (((0 < = x) AND (n0y < = 0)) OR ((x < = 0) AND (0 < = n0y)))

div mult pos le1: LEMMA ((z / py) < = x) IFF (z < = (x * py))

div mult pos le2: LEMMA (x < = (z / py)) IFF ((x * py) < = z)

div mult neg le1: LEMMA ((z / ny) < = x) IFF ((x * ny) < = z)

div mult neg le2: LEMMA (x < = (z / ny)) IFF (z < = (x * ny))

both sides plus le1: LEMMA ((x + z) < = (y + z)) IFF (x < = y)

both sides plus le2: LEMMA ((z + x) < = (z + y)) IFF (x < = y)

both sides minus le1: LEMMA ((x - z) < = (y - z)) IFF (x < = y)

both sides minus le2: LEMMA ((z - x) < = (z - y)) IFF (y < = x)

both sides times pos le1: LEMMA ((x * pz) < = (y * pz)) IFF (x < = y)

both sides times pos le2: LEMMA ((pz * x) < = (pz * y)) IFF (x < = y)

both sides times neg le1: LEMMA ((x * nz) < = (y * nz)) IFF (y < = x)

both sides times neg le2: LEMMA ((nz * x) < = (nz * y)) IFF (y < = x)

both sides div pos le1: LEMMA ((x / pz) < = (y / pz)) IFF (x < = y)

both sides div pos le2: LEMMA ((pz / px) < = (pz / py)) IFF (py < = px)

both sides div pos le3: LEMMA ((nz / px) < = (nz / py)) IFF (px < = py)

both sides div neg le1: LEMMA ((x / nz) < = (y / nz)) IFF (y < = x)

both sides div neg le2: LEMMA ((pz / nx) < = (pz / ny)) IFF (ny < = nx)

both sides div neg le3: LEMMA ((nz / nx) < = (nz / ny)) IFF (nx < = ny)

le plus le: LEMMA ((x < = y) AND (z < = w)) IMPLIES ((x + z) < = (y + w))

le minus le: LEMMA ((x < = y) AND (w < = z)) IMPLIES ((x - z) < = (y - w))

le times le pos: LEMMA ((nnx < = y) AND (nnz < = w)) IMPLIES ((nnx * nnz) < = (y * w))

%%(TCC) le_div_le_pos_TCC1: OBLIGATION

le div le pos: LEMMA ((nnx < = y) AND (pz < = w)) IMPLIES ((nnx / w) < = (y / pz))

le times le neg: LEMMA ((x < = npy) AND (z < = npw)) IMPLIES ((npy * npw) < = (x * z))

%%(TCC) le_div_le_neg_TCC1: OBLIGATION

le div le neg: LEMMA ((x < = npy) AND (z < = nw)) IMPLIES ((npy / z) < = (x / nw))

strict gt: LEMMA strict total order?( > )

trich gt: LEMMA (x > y) OR (x = y) OR (y > x)

tri unique gt1: LEMMA (x > y) IMPLIES ((x /= y) AND (NOT (y > x)))

tri unique gt2: LEMMA (x = y) IMPLIES ((NOT (x > y)) AND (NOT (y > x)))

zero not gt zero: LEMMA NOT (0 > 0)

neg gt: LEMMA (0 > (-x)) IFF (x > 0)

pos times gt: LEMMA ((x * y) > 0) IFF (((0 > x) AND (0 > y)) OR ((x > 0) AND (y > 0)))

neg times gt: LEMMA (0 > (x * y)) IFF (((0 > x) AND (y > 0)) OR ((x > 0) AND (0 > y)))

quotient pos gt: FORMULA ((1 / n0x) > 0) IFF (n0x > 0)

quotient neg gt: FORMULA (0 > (1 / n0x)) IFF (0 > n0x)

pos div gt: LEMMA ((x / n0y) > 0) IFF (((0 > x) AND (0 > n0y)) OR ((x > 0) AND (n0y > 0)))

neg div gt: LEMMA (0 > (x / n0y)) IFF (((0 > x) AND (n0y > 0)) OR ((x > 0) AND (0 > n0y)))

div mult pos gt1: LEMMA (x > (z / py)) IFF ((x * py) > z)

div mult pos gt2: LEMMA ((z / py) > x) IFF (z > (x * py))

div mult neg gt1: LEMMA (x > (z / ny)) IFF (z > (x * ny))

div mult neg gt2: LEMMA ((z / ny) > x) IFF ((x * ny) > z)

both sides plus gt1: LEMMA ((x + z) > (y + z)) IFF (x > y)

both sides plus gt2: LEMMA ((z + x) > (z + y)) IFF (x > y)

both sides minus gt1: LEMMA ((x - z) > (y - z)) IFF (x > y)

both sides minus gt2: LEMMA ((z - x) > (z - y)) IFF (y > x)

both sides times pos gt1: LEMMA ((x * pz) > (y * pz)) IFF (x > y)

both sides times pos gt2: LEMMA ((pz * x) > (pz * y)) IFF (x > y)

both sides times neg gt1: LEMMA ((x * nz) > (y * nz)) IFF (y > x)

both sides times neg gt2: LEMMA ((nz * x) > (nz * y)) IFF (y > x)

both sides div pos gt1: LEMMA ((x / pz) > (y / pz)) IFF (x > y)

both sides div pos gt2: LEMMA ((pz / px) > (pz / py)) IFF (py > px)

both sides div pos gt3: LEMMA ((nz / px) > (nz / py)) IFF (px > py)

both sides div neg gt1: LEMMA ((x / nz) > (y / nz)) IFF (y > x)

both sides div neg gt2: LEMMA ((pz / nx) > (pz / ny)) IFF (ny > nx)

both sides div neg gt3: LEMMA ((nz / nx) > (nz / ny)) IFF (nx > ny)

gt plus gt1: LEMMA ((x > = y) AND (z > w)) IMPLIES ((x + z) > (y + w))

gt plus gt2: LEMMA ((x > y) AND (z > = w)) IMPLIES ((x + z) > (y + w))

gt minus gt1: LEMMA ((x > = y) AND (w > z)) IMPLIES ((x - z) > (y - w))

gt minus gt2: LEMMA ((x > y) AND (w > = z)) IMPLIES ((x - z) > (y - w))

gt times gt pos1: LEMMA ((x > = py) AND (z > nnw)) IMPLIES ((x * z) > (py * nnw))

gt times gt pos2: LEMMA ((x > nny) AND (z > = pw)) IMPLIES ((x * z) > (nny * pw))

%%(TCC) gt_div_gt_pos1_TCC1: OBLIGATION

gt div gt pos1: LEMMA ((x > = py) AND (z > pw)) IMPLIES ((x / pw) > (py / z))

%%(TCC) gt_div_gt_pos2_TCC1: OBLIGATION

gt div gt pos2: LEMMA ((x > nny) AND (z > = pw)) IMPLIES ((x / pw) > (nny / z))

gt times gt neg1: LEMMA ((nx > = y) AND (npz > w)) IMPLIES ((y * w) > (nx * npz))

gt times gt neg2: LEMMA ((npx > y) AND (nz > = w)) IMPLIES ((y * w) > (npx * nz))

%%(TCC) gt_div_gt_neg1_TCC1: OBLIGATION

gt div gt neg1: LEMMA ((nx > = y) AND (nz > w)) IMPLIES ((y / nz) > (nx / w))

%%(TCC) gt_div_gt_neg2_TCC1: OBLIGATION

gt div gt neg2: LEMMA ((npx > y) AND (nz > = w)) IMPLIES ((y / nz) > (npx / w))

strict ge: LEMMA total order?( > =)

dich ge: LEMMA (x > = y) OR (y > = x)

zero ge zero: LEMMA 0 > = 0

neg ge: LEMMA (0 > = (-x)) IFF (x > = 0)

pos times ge: LEMMA ((x * y) > = 0) IFF (((0 > = x) AND (0 > = y)) OR ((x > = 0) AND (y > = 0)))

neg times ge: LEMMA (0 > = (x * y)) IFF (((0 > = x) AND (y > = 0)) OR ((x > = 0) AND (0 > = y)))

quotient pos ge: FORMULA ((1 / n0x) > = 0) IFF (n0x > = 0)

quotient neg ge: FORMULA (0 > = (1 / n0x)) IFF (0 > = n0x)

pos div ge: LEMMA ((x / n0y) > = 0) IFF (((0 > = x) AND (0 > = n0y)) OR ((x > = 0) AND (n0y > = 0)))

neg div ge: LEMMA (0 > = (x / n0y)) IFF (((0 > = x) AND (n0y > = 0)) OR ((x > = 0) AND (0 > = n0y)))

div mult pos ge1: LEMMA ((z / py) > = x) IFF (z > = (x * py))

div mult pos ge2: LEMMA (x > = (z / py)) IFF ((x * py) > = z)

div mult neg ge1: LEMMA ((z / ny) > = x) IFF ((x * ny) > = z)

div mult neg ge2: LEMMA (x > = (z / ny)) IFF (z > = (x * ny))

both sides plus ge1: LEMMA ((x + z) > = (y + z)) IFF (x > = y)

both sides plus ge2: LEMMA ((z + x) > = (z + y)) IFF (x > = y)

both sides minus ge1: LEMMA ((x - z) > = (y - z)) IFF (x > = y)

both sides minus ge2: LEMMA ((z - x) > = (z - y)) IFF (y > = x)

both sides times pos ge1: LEMMA ((x * pz) > = (y * pz)) IFF (x > = y)

both sides times pos ge2: LEMMA ((pz * x) > = (pz * y)) IFF (x > = y)

both sides times neg ge1: LEMMA ((x * nz) > = (y * nz)) IFF (y > = x)

both sides times neg ge2: LEMMA ((nz * x) > = (nz * y)) IFF (y > = x)

both sides div pos ge1: LEMMA ((x / pz) > = (y / pz)) IFF (x > = y)

both sides div pos ge2: LEMMA ((pz / px) > = (pz / py)) IFF (py > = px)

both sides div pos ge3: LEMMA ((nz / px) > = (nz / py)) IFF (px > = py)

both sides div neg ge1: LEMMA ((x / nz) > = (y / nz)) IFF (y > = x)

both sides div neg ge2: LEMMA ((pz / nx) > = (pz / ny)) IFF (ny > = nx)

both sides div neg ge3: LEMMA ((nz / nx) > = (nz / ny)) IFF (nx > = ny)

ge plus ge: LEMMA ((x > = y) AND (z > = w)) IMPLIES ((x + z) > = (y + w))

ge minus ge: LEMMA ((x > = y) AND (w > = z)) IMPLIES ((x - z) > = (y - w))

ge times ge pos: LEMMA ((x > = nny) AND (z > = nnw)) IMPLIES ((x * z) > = (nny * nnw))

%%(TCC) ge_div_ge_pos_TCC1: OBLIGATION

ge div ge pos: LEMMA ((x > = nny) AND (z > = pw)) IMPLIES ((x / pw) > = (nny / z))

ge times ge neg: LEMMA ((npx > = y) AND (npz > = w)) IMPLIES ((y * w) > = (npx * npz))

%%(TCC) ge_div_ge_neg_TCC1: OBLIGATION

ge div ge neg: LEMMA ((npx > = y) AND (nz > = w)) IMPLIES ((y / nz) > = (npx / w))

nonzero times1: LEMMA ((n0x * y) = 0) IFF (y = 0)

nonzero times2: LEMMA ((x * n0y) = 0) IFF (x = 0)

nonzero times3: LEMMA ((n0x * n0y) = 0) IFF FALSE

eq1 gt: FORMULA ((x > 1) AND ((x * y) = 1)) IMPLIES (y < 1)

eq1 ge: FORMULA ((x > = 1) AND ((x * y) = 1)) IMPLIES (y < = 1)

eqm1 gt: FORMULA ((x > 1) AND ((x * y) = (-1))) IMPLIES (y > (-1))

eqm1 ge: FORMULA ((x > = 1) AND ((x * y) = (-1))) IMPLIES (y > = (-1))

eqm1 lt: FORMULA ((x < (-1)) AND ((x * y) = (-1))) IMPLIES (y < 1)

eqm1 le: FORMULA ((x < = (-1)) AND ((x * y) = (-1))) IMPLIES (y < = 1)

sqrt 1: LEMMA ((x * x) = 1) IFF ((x = 1) OR (x = (-1)))

sqrt 1 lt: LEMMA ((x * x) < 1) IMPLIES (abs(x) < 1)

sqrt 1 le: LEMMA ((x * x) < = 1) IMPLIES (abs(x) < = 1)

idem mult: LEMMA ((x * x) = x) IFF ((x = 0) OR (x = 1))

i: VAR int

j: VAR int

product 1: LEMMA ((i > = 0) AND (j > = 0) AND ((i * j) = 1)) IMPLIES ((i = 1) AND (j = 1))

product m1: LEMMA ((i > = 0) AND (j < = 0) AND ((i * j) = (-1))) IMPLIES ((i = 1) AND (j = (-1)))

triangle: LEMMA abs(x + y) < = (abs(x) + abs(y))

abs mult: LEMMA abs(x * y) = (abs(x) * abs(y))

abs div: LEMMA abs(x / n0y) = (abs(x) / abs(n0y))

abs abs: LEMMA abs(abs(x)) = abs(x)

abs square: LEMMA abs(x * x) = (x * x)

abs limits: LEMMA ((-(abs(x) + abs(y))) < = (x + y)) AND ((x + y) < = (abs(x) + abs(y)))

axiom of archimedes: LEMMA FORALL (x:real) : EXISTS (i:int) : x < i

archimedean: LEMMA FORALL (px:posreal) : EXISTS (n:posnat) : (1 / n) < px

END real_props