1\DOC arith_ss 2 3\TYPE {arith_ss : simpset} 4 5\SYNOPSIS 6Simplification set for arithmetic. 7 8\KEYWORDS 9simplification, arithmetic. 10 11\DESCRIBE 12The simplification set {arith_ss} is a version of {std_ss} enhanced for 13arithmetic. It includes many arithmetic rewrites, an evaluation mechanism for 14ground arithmetic terms, and a decision procedure for linear arithmetic. 15It also incorporates a cache of successfully solved conditions proved when 16conditional rewrite rules are successfully applied. 17 18The following rewrites are currently used to augment those already present 19from {std_ss}: 20{ 21 |- !m n. (m * n = 0) = (m = 0) \/ (n = 0) 22 |- !m n. (0 = m * n) = (m = 0) \/ (n = 0) 23 |- !m n. (m + n = 0) = (m = 0) /\ (n = 0) 24 |- !m n. (0 = m + n) = (m = 0) /\ (n = 0) 25 |- !x y. (x * y = 1) = (x = 1) /\ (y = 1) 26 |- !x y. (1 = x * y) = (x = 1) /\ (y = 1) 27 |- !m. m * 0 = 0 28 |- !m. 0 * m = 0 29 |- !x y. (x * y = SUC 0) = (x = SUC 0) /\ (y = SUC 0) 30 |- !x y. (SUC 0 = x * y) = (x = SUC 0) /\ (y = SUC 0) 31 |- !m. m * 1 = m 32 |- !m. 1 * m = m 33 |- !x.((SUC x = 1) = (x = 0)) /\ ((1 = SUC x) = (x = 0)) 34 |- !x.((SUC x = 2) = (x = 1)) /\ ((2 = SUC x) = (x = 1)) 35 |- !m n. (m + n = m) = (n = 0) 36 |- !m n. (n + m = m) = (n = 0) 37 |- !c. c - c = 0 38 |- !m. SUC m - 1 = m 39 |- !m. (0 - m = 0) /\ (m - 0 = m) 40 |- !a c. a + c - c = a 41 |- !m n. (m - n = 0) = m <= n 42 |- !m n. (0 = m - n) = m <= n 43 |- !n m. n - m <= n 44 |- !n m. SUC n - SUC m = n - m 45 |- !m n p. m - n > p = m > n + p 46 |- !m n p. m - n < p = m < n + p /\ 0 < p 47 |- !m n p. m - n >= p = m >= n + p \/ 0 >= p 48 |- !m n p. m - n <= p = m <= n + p 49 |- !n. n <= 0 = (n = 0) 50 |- !m n p. m + p < n + p = m < n 51 |- !m n p. p + m < p + n = m < n 52 |- !m n p. m + n <= m + p = n <= p 53 |- !m n p. n + m <= p + m = n <= p 54 |- !m n p. (m + p = n + p) = (m = n) 55 |- !m n p. (p + m = p + n) = (m = n) 56 |- !x y w. x + y < w + x = y < w 57 |- !x y w. y + x < x + w = y < w 58 |- !m n. (SUC m = SUC n) = (m = n) 59 |- !m n. SUC m < SUC n = m < n 60 |- !n m. SUC n <= SUC m = n <= m 61 |- !m i n. SUC n * m < SUC n * i = m < i 62 |- !p m n. (n * SUC p = m * SUC p) = (n = m) 63 |- !m i n. (SUC n * m = SUC n * i) = (m = i) 64 |- !n m. ~(SUC n <= m) = m <= n 65 |- !p q n m. (n * SUC q ** p = m * SUC q ** p) = (n = m) 66 |- !m n. ~(SUC n ** m = 0) 67 |- !n m. ~(SUC (n + n) = m + m) 68 |- !m n. ~(SUC (m + n) <= m) 69 |- !n. ~(SUC n <= 0) 70 |- !n. ~(n < 0) 71 |- !n. (MIN n 0 = 0) /\ (MIN 0 n = 0) 72 |- !n. (MAX n 0 = n) /\ (MAX 0 n = n) 73 |- !n. MIN n n = n 74 |- !n. MAX n n = n 75 |- !n m. MIN m n <= m /\ MIN m n <= n 76 |- !n m. m <= MAX m n /\ n <= MAX m n 77 |- !n m. (MIN m n < m = ~(m = n) /\ (MIN m n = n)) /\ 78 (MIN m n < n = ~(m = n) /\ (MIN m n = m)) /\ 79 (m < MIN m n = F) /\ (n < MIN m n = F) 80 |- !n m. (m < MAX m n = ~(m = n) /\ (MAX m n = n)) /\ 81 (n < MAX m n = ~(m = n) /\ (MAX m n = m)) /\ 82 (MAX m n < m = F) /\ (MAX m n < n = F) 83 |- !m n. (MIN m n = MAX m n) = (m = n) 84 |- !m n. MIN m n < MAX m n = ~(m = n) 85} 86 87The decision procedure proves valid purely univeral formulas 88constructed using variables and the operators {SUC,PRE,+,-,<,>,<=,>=}. 89Multiplication by constants is accomodated by translation to repeated 90addition. An attempt is made to generalize sub-formulas of type {num} 91not fitting into this syntax. 92 93\COMMENTS 94The philosophy behind this simpset is fairly conservative. For example, 95some potential rewrite rules, e.g., the recursive clauses for addition 96and multiplication, are not included, since it was felt that their 97incorporation too often resulted in formulas becoming more complex 98rather than simpler. Also, transitivity theorems are avoided because 99they tend to make simplification diverge. 100 101\SEEALSO 102BasicProvers.RW_TAC, BasicProvers.SRW_TAC, 103simpLib.SIMP_TAC, simpLib.SIMP_CONV, simpLib.SIMP_RULE, 104BasicProvers.bool_ss, bossLib.std_ss, bossLib.list_ss. 105 106\ENDDOC 107