intReduceScript.sml

1Theory intReduce
2Ancestors
3  integer numeral arithmetic
4Libs
5  intSyntax simpLib Arithconv tautLib
6
7Theorem INT_LE_CONV_tth =
8  TAUT ‘(F /\ F <=> F) /\ (F /\ T <=> F) /\
9        (T /\ F <=> F) /\ (T /\ T <=> T)’;
10Theorem INT_LE_CONV_nth = TAUT ‘(~T <=> F) /\ (~F <=> T)’;
11
12Theorem INT_LE_CONV_pth:
13  (~(&m) <= &n <=> T) /\
14  (&m <= (&n : int) <=> m <= n) /\
15  (~(&m) <= ~(&n) <=> n <= m) /\
16  (&m <= ~(&n) <=> (m = 0) /\ (n = 0))
17Proof
18  REWRITE_TAC[INT_LE_NEG]
19  >> REWRITE_TAC[INT_LE_LNEG, INT_LE_RNEG]
20  >> REWRITE_TAC[INT_OF_NUM_ADD, INT_OF_NUM_LE, LE_0]
21  >> REWRITE_TAC[LE, ADD_EQ_0]
22QED
23
24Theorem INT_LT_CONV_pth:
25  (&m < ~(&n) <=> F) /\
26  (&m < (&n :int) <=> m < n) /\
27  (~(&m) < ~(&n) <=> n < m) /\
28  (~(&m) < &n <=> ~((m = 0) /\ (n = 0)))
29Proof
30  REWRITE_TAC[INT_LE_CONV_pth, GSYM NOT_LE, INT_LT2] THEN
31  TAUT_TAC
32QED
33
34Theorem INT_GE_CONV_pth:
35  (&m >= ~(&n) <=> T) /\
36  (&m >= (&n :int) <=> n <= m) /\
37  (~(&m) >= ~(&n) <=> m <= n) /\
38  (~(&m) >= &n <=> (m = 0) /\ (n = 0))
39Proof
40  REWRITE_TAC[INT_LE_CONV_pth, INT_GE] THEN
41  TAUT_TAC
42QED
43
44Theorem INT_GT_CONV_pth:
45  (~(&m) > &n <=> F) /\
46  (&m > (&n :int) <=> n < m) /\
47  (~(&m) > ~(&n) <=> m < n) /\
48  (&m > ~(&n) <=> ~((m = 0) /\ (n = 0)))
49Proof
50  REWRITE_TAC[INT_LT_CONV_pth, INT_GT] THEN
51  TAUT_TAC
52QED
53
54Theorem INT_EQ_CONV_pth:
55  ((&m = (&n :int)) <=> (m = n)) /\
56  ((~(&m) = ~(&n)) <=> (m = n)) /\
57  ((~(&m) = &n) <=> (m = 0) /\ (n = 0)) /\
58  ((&m = ~(&n)) <=> (m = 0) /\ (n = 0))
59Proof
60  REWRITE_TAC[GSYM INT_LE_ANTISYM, GSYM LE_ANTISYM]
61  \\ REWRITE_TAC[INT_LE_CONV_pth, LE, LE_0]
62  \\ CONV_TAC tautLib.TAUT_CONV
63QED
64
65Theorem INT_NEG_CONV_pth:
66  (-(&0) = &0) /\ (-(-(&x)) = &x)
67Proof
68  REWRITE_TAC[INT_NEG_NEG, INT_NEG_0]
69QED
70
71Theorem INT_ADD_CONV_pth0:
72  (-(&m) + &m = &0) /\ (&m + -(&m) = &0)
73Proof
74  REWRITE_TAC[INT_ADD_LINV, INT_ADD_RINV]
75QED
76
77Theorem INT_ADD_CONV_pth1:
78  (-(&m) + -(&n):int = -(&(m + n))) /\
79  (-(&m) + &(m + n):int = &n) /\
80  (-(&(m + n)) + (&m :int) = -(&n)) /\
81  (&(m + n) + -(&m):int = &n) /\
82  (&m + -(&(m + n)):int = -(&n)) /\
83  (&m + &n = &(m + n):int)
84Proof
85  REWRITE_TAC[GSYM INT_OF_NUM_ADD, INT_NEG_ADD] THEN
86  REWRITE_TAC[INT_ADD_ASSOC, INT_ADD_LINV, INT_ADD_LID] THEN
87  REWRITE_TAC[INT_ADD_RINV, INT_ADD_LID] THEN
88  ONCE_REWRITE_TAC[INT_ADD_SYM] THEN
89  REWRITE_TAC[INT_ADD_ASSOC, INT_ADD_LINV, INT_ADD_LID] THEN
90  REWRITE_TAC[INT_ADD_RINV, INT_ADD_LID]
91QED
92
93Theorem INT_MUL_CONV_pth0:
94  (&0 * &x = &0 :int) /\
95  (&0 * -(&x) = &0 :int) /\
96  (&x * &0 = &0 :int) /\
97  (-(&x) * &0 = &0 :int)
98Proof
99  REWRITE_TAC[INT_MUL_LZERO, INT_MUL_RZERO]
100QED
101
102Theorem INT_MUL_CONV_pth1:
103  ((&m * &n = &(m * n) :int) /\
104   (-(&m) * -(&n) = &(m * n) :int)) /\
105  ((-(&m) * &n = -(&(m * n)) :int) /\
106   (&m * -(&n) = -(&(m * n)) :int))
107Proof
108  REWRITE_TAC[INT_MUL_LNEG, INT_MUL_RNEG, INT_NEG_NEG] THEN
109  REWRITE_TAC[INT_OF_NUM_MUL]
110QED
111
112Theorem INT_POW_CONV_pth:
113  (&x ** n = &(x ** n) :int) /\
114  ((-(&x):int) ** n = if EVEN n then &(x ** n) else -(&(x ** n)))
115Proof
116  REWRITE_TAC[INT_OF_NUM_POW, INT_POW_NEG]
117QED
118
119Theorem INT_POW_CONV_tth:
120  ((if T then (x:int) else y) = x) /\ ((if F then (x:int) else y) = y)
121Proof
122  REWRITE_TAC[]
123QED
124