----------------------------------------------------------------------
arith_ss                                                     (bossLib)
----------------------------------------------------------------------
arith_ss : simpset

SYNOPSIS
Simplification set for arithmetic.

KEYWORDS
simplification, arithmetic.

DESCRIBE
The simplification set {arith_ss} is a version of {std_ss} enhanced for
arithmetic. It includes many arithmetic rewrites, an evaluation mechanism for
ground arithmetic terms, and a decision procedure for linear arithmetic.
It also incorporates a cache of successfully solved conditions proved when
conditional rewrite rules are successfully applied.

The following rewrites are currently used to augment those already present
from {std_ss}:

   |- !m n. (m * n = 0) = (m = 0) \/ (n = 0)
   |- !m n. (0 = m * n) = (m = 0) \/ (n = 0)
   |- !m n. (m + n = 0) = (m = 0) /\ (n = 0)
   |- !m n. (0 = m + n) = (m = 0) /\ (n = 0)
   |- !x y. (x * y = 1) = (x = 1) /\ (y = 1)
   |- !x y. (1 = x * y) = (x = 1) /\ (y = 1)
   |- !m. m * 0 = 0
   |- !m. 0 * m = 0
   |- !x y. (x * y = SUC 0) = (x = SUC 0) /\ (y = SUC 0)
   |- !x y. (SUC 0 = x * y) = (x = SUC 0) /\ (y = SUC 0)
   |- !m. m * 1 = m
   |- !m. 1 * m = m
   |- !x.((SUC x = 1) = (x = 0)) /\ ((1 = SUC x) = (x = 0))
   |- !x.((SUC x = 2) = (x = 1)) /\ ((2 = SUC x) = (x = 1))
   |- !m n. (m + n = m) = (n = 0)
   |- !m n. (n + m = m) = (n = 0)
   |- !c. c - c = 0
   |- !m. SUC m - 1 = m
   |- !m. (0 - m = 0) /\ (m - 0 = m)
   |- !a c. a + c - c = a
   |- !m n. (m - n = 0) = m <= n
   |- !m n. (0 = m - n) = m <= n
   |- !n m. n - m <= n
   |- !n m. SUC n - SUC m = n - m
   |- !m n p. m - n > p = m > n + p
   |- !m n p. m - n < p = m < n + p /\ 0 < p
   |- !m n p. m - n >= p = m >= n + p \/ 0 >= p
   |- !m n p. m - n <= p = m <= n + p
   |- !n. n <= 0 = (n = 0)
   |- !m n p. m + p < n + p = m < n
   |- !m n p. p + m < p + n = m < n
   |- !m n p. m + n <= m + p = n <= p
   |- !m n p. n + m <= p + m = n <= p
   |- !m n p. (m + p = n + p) = (m = n)
   |- !m n p. (p + m = p + n) = (m = n)
   |- !x y w. x + y < w + x = y < w
   |- !x y w. y + x < x + w = y < w
   |- !m n. (SUC m = SUC n) = (m = n)
   |- !m n. SUC m < SUC n = m < n
   |- !n m. SUC n <= SUC m = n <= m
   |- !m i n. SUC n * m < SUC n * i = m < i
   |- !p m n. (n * SUC p = m * SUC p) = (n = m)
   |- !m i n. (SUC n * m = SUC n * i) = (m = i)
   |- !n m. ~(SUC n <= m) = m <= n
   |- !p q n m. (n * SUC q ** p = m * SUC q ** p) = (n = m)
   |- !m n. ~(SUC n ** m = 0)
   |- !n m. ~(SUC (n + n) = m + m)
   |- !m n. ~(SUC (m + n) <= m)
   |- !n. ~(SUC n <= 0)
   |- !n. ~(n < 0)
   |- !n. (MIN n 0 = 0) /\ (MIN 0 n = 0)
   |- !n. (MAX n 0 = n) /\ (MAX 0 n = n)
   |- !n. MIN n n = n
   |- !n. MAX n n = n
   |- !n m. MIN m n <= m /\ MIN m n <= n
   |- !n m. m <= MAX m n /\ n <= MAX m n
   |- !n m. (MIN m n < m = ~(m = n) /\ (MIN m n = n)) /\
            (MIN m n < n = ~(m = n) /\ (MIN m n = m)) /\
            (m < MIN m n = F) /\ (n < MIN m n = F)
   |- !n m. (m < MAX m n = ~(m = n) /\ (MAX m n = n)) /\
            (n < MAX m n = ~(m = n) /\ (MAX m n = m)) /\
            (MAX m n < m = F) /\ (MAX m n < n = F)
   |- !m n. (MIN m n = MAX m n) = (m = n)
   |- !m n. MIN m n < MAX m n = ~(m = n)


The decision procedure proves valid purely univeral formulas
constructed using variables and the operators {SUC,PRE,+,-,<,>,<=,>=}.
Multiplication by constants is accomodated by translation to repeated
addition. An attempt is made to generalize sub-formulas of type {num}
not fitting into this syntax.

COMMENTS
The philosophy behind this simpset is fairly conservative. For example,
some potential rewrite rules, e.g., the recursive clauses for addition
and multiplication, are not included, since it was felt that their
incorporation too often resulted in formulas becoming more complex
rather than simpler. Also, transitivity theorems are avoided because
they tend to make simplification diverge.

SEEALSO
BasicProvers.RW_TAC, BasicProvers.SRW_TAC, simpLib.SIMP_TAC,
simpLib.SIMP_CONV, simpLib.SIMP_RULE, BasicProvers.bool_ss,
bossLib.std_ss, bossLib.list_ss.

----------------------------------------------------------------------