bossLib.arith

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.