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