Theory "intExtension"

Parents numRing integerRing Omega int_arith

Signature

Constant	Type
SGN	:int -> int

SGN_def

|- !x. SGN x = (if x = 0 then 0 else (if x < 0 then ~1 else 1))

INT_SGN_TOTAL

|- !a. (SGN a = ~1) \/ (SGN a = 0) \/ (SGN a = 1)

INT_SGN_MUL2

|- !x y. SGN (x * y) = SGN x * SGN y

INT_SGN_MUL

|- !x1 x2 y1 y2. (SGN x1 = y1) ==> (SGN x2 = y2) ==> (SGN (x1 * x2) = y1 * y2)

INT_SGN_CLAUSES

|- !x.
     ((SGN x = ~1) = x < 0) /\ ((SGN x = 0) = (x = 0)) /\
     ((SGN x = 1) = x > 0)

INT_NOT0_SGNNOT0

|- !x. ~(x = 0) ==> ~(SGN x = 0)

INT_ABS_CALCULATE_POS

|- !a. 0 < a ==> (ABS a = a)

INT_ABS_CALCULATE_0

|- ABS 0 = 0

INT_ABS_CALCULATE_NEG

|- !a. a < 0 ==> (ABS a = ~a)

INT_GT_RMUL_EXP

|- !a b n. 0 < n ==> (a > b = a * n > b * n)

INT_LT_RMUL_EXP

|- !a b n. 0 < n ==> (a < b = a * n < b * n)

INT_EQ_RMUL_EXP

|- !a b n. 0 < n ==> ((a = b) = (a * n = b * n))

LESS_IMP_NOT_0

|- !n. 0 < n ==> ~(n = 0)

INT_MUL_POS_SIGN

|- !a b. 0 < a ==> 0 < b ==> 0 < a * b

INT_NE_IMP_LTGT

|- !x. ~(x = 0) = 0 < x \/ x < 0

INT_NOTGT_IMP_EQLT

|- !n. ~(n < 0) = (0 = n) \/ 0 < n

INT_NO_ZERODIV

|- !x y. (x = 0) \/ (y = 0) = (x * y = 0)

INT_NOTPOS0_NEG

|- !a. ~(0 < a) ==> ~(a = 0) ==> 0 < ~a

INT_NOT0_MUL

|- !a b. ~(a = 0) ==> ~(b = 0) ==> ~(a * b = 0)

INT_GT0_IMP_NOT0

|- !a. 0 < a ==> ~(a = 0)

INT_NOTLTEQ_GT

|- !a. ~(a < 0) ==> ~(a = 0) ==> 0 < a

INT_ABS_NOT0POS

|- !x. ~(x = 0) ==> 0 < ABS x

INT_SGN_NOTPOSNEG

|- !x. ~(SGN x = ~1) ==> ~(SGN x = 1) ==> (SGN x = 0)

INT_SGN_CASES

|- !a P.
     ((SGN a = ~1) ==> P) /\ ((SGN a = 0) ==> P) /\ ((SGN a = 1) ==> P) ==> P

INT_LT_ADD_NEG

|- !x y. x < 0 /\ y < 0 ==> x + y < 0