integer_wordScript.sml
1(* ========================================================================= *)
2(* Theory of 2's complement representation of integers *)
3(* ========================================================================= *)
4Theory integer_word
5Ancestors
6 arithmetic bit words integer
7Libs
8 wordsLib stringLib intLib
9
10
11val _ = ParseExtras.temp_loose_equality()
12
13(* ------------------------------------------------------------------------- *)
14
15Definition toString_def:
16 toString (i : int) =
17 if i < 0 then
18 "~" ++ num_to_dec_string (Num ~i)
19 else
20 num_to_dec_string (Num i)
21End
22
23Definition fromString_def:
24 (fromString (#"~"::t) = ~&(num_from_dec_string t)) /\
25 (fromString (#"-"::t) = ~&(num_from_dec_string t)) /\
26 (fromString s = &(num_from_dec_string s))
27End
28
29Definition i2w_def:
30 i2w (i : int) : 'a word =
31 if i < 0 then -(n2w (Num(-i))) else n2w (Num i)
32End
33
34Definition w2i_def:
35 w2i w = if word_msb w then ~(int_of_num (w2n (word_2comp w)))
36 else int_of_num (w2n w)
37End
38
39Definition UINT_MAX_def:
40 UINT_MAX (:'a) :int = &(dimword(:'a)) - 1
41End
42
43Definition INT_MAX_def:
44 INT_MAX (:'a) :int = &(words$INT_MIN(:'a)) - 1
45End
46
47Definition INT_MIN_def:
48 INT_MIN (:'a) = ~INT_MAX(:'a) - 1
49End
50
51Definition saturate_i2w_def:
52 saturate_i2w i : 'a word =
53 if UINT_MAX (:'a) <= i then
54 word_T
55 else if i < 0 then
56 0w
57 else
58 n2w (Num i)
59End
60
61Definition saturate_i2sw_def:
62 saturate_i2sw i : 'a word =
63 if INT_MAX (:'a) <= i then
64 word_H
65 else if i <= INT_MIN (:'a) then
66 word_L
67 else
68 i2w i
69End
70
71Definition saturate_sw2sw_def:
72 saturate_sw2sw (w: 'a word) = saturate_i2sw (w2i w)
73End
74
75Definition saturate_w2sw_def:
76 saturate_w2sw (w: 'a word) = saturate_i2sw (&w2n w)
77End
78
79Definition saturate_sw2w_def:
80 saturate_sw2w (w: 'a word) = saturate_i2w (w2i w)
81End
82
83Definition signed_saturate_add_def:
84 signed_saturate_add (a: 'a word) (b: 'a word) =
85 saturate_i2sw (w2i a + w2i b) : 'a word
86End
87
88Definition signed_saturate_sub_def:
89 signed_saturate_sub (a: 'a word) (b: 'a word) =
90 saturate_i2sw (w2i a - w2i b) : 'a word
91End
92
93Definition word_sdiv_def:
94 word_sdiv (a : 'a word) (b : 'a word) = i2w (w2i a / w2i b) : 'a word
95End
96
97Definition word_smod_def:
98 word_smod (a : 'a word) (b : 'a word) = i2w (w2i a % w2i b) : 'a word
99End
100
101(* ------------------------------------------------------------------------- *)
102
103(*
104val INT_MAX_32 = store_thm(
105 "INT_MAX_32",
106 ``INT_MAX (:32) = 2147483647``,
107 SRW_TAC [][INT_MAX_def, dimindex_32, wordsTheory.INT_MIN_def]);
108val _ = export_rewrites ["INT_MAX_32"]
109
110val INT_MIN_32 = store_thm(
111 "INT_MIN_32",
112 ``INT_MIN (:32) = ~2147483648``,
113 SRW_TAC [][INT_MIN_def]);
114val _ = export_rewrites ["INT_MIN_32"]
115
116val UINT_MAX_32 = store_thm(
117 "UINT_MAX_32",
118 ``UINT_MAX (: 32) = 4294967295``,
119 SRW_TAC [][UINT_MAX_def, dimindex_32, dimword_def]);
120val _ = export_rewrites ["UINT_MAX_32"]
121*)
122
123Theorem ONE_LE_TWOEXP = bitTheory.ONE_LE_TWOEXP
124
125Theorem w2i_w2n_pos:
126 !w n. ~word_msb w /\ w2i w < &n ==> w2n w < n
127Proof
128 SRW_TAC [] [w2i_def]
129QED
130
131Theorem w2i_n2w_pos:
132 !n. n < INT_MIN (:'a) ==>
133 (w2i (n2w n : bool ** 'a) = &n)
134Proof
135 SRW_TAC [][w2i_def, word_msb_n2w, bitTheory.BIT_def, INT_SUB, dimword_def,
136 bitTheory.BITS_def, DECIDE ``SUC x - x = 1``,
137 wordsTheory.INT_MIN_def, DIV_2EXP_def, MOD_2EXP_def,
138 w2n_n2w, INT_MAX_def, bitTheory.ZERO_LT_TWOEXP,
139 DECIDE ``0n < y ==> (x <= y - 1 = x < y)``] THEN
140 FULL_SIMP_TAC (srw_ss()) [LESS_DIV_EQ_ZERO] THEN
141 MATCH_MP_TAC LESS_TRANS THEN
142 Q.EXISTS_TAC `2 ** (dimindex (:'a) - 1)` THEN
143 SRW_TAC [ARITH_ss][DIMINDEX_GT_0, bitTheory.TWOEXP_MONO]
144QED
145
146Theorem w2i_n2w_neg:
147 !n. INT_MIN (:'a) <= n /\ n < dimword (:'a) ==>
148 (w2i (n2w n : 'a word) = ~ &(dimword(:'a) - n))
149Proof
150 SRW_TAC [ARITH_ss][w2i_def, word_msb_n2w, bitTheory.BIT_def, dimword_def,
151 bitTheory.BITS_def, DECIDE ``SUC x - x = 1``,
152 wordsTheory.INT_MIN_def, DIV_2EXP_def, MOD_2EXP_def,
153 w2n_n2w, word_2comp_n2w]
154 THENL [
155 Q_TAC SUFF_TAC `0n < 2 ** (dimindex (:'a) - 1)` THEN1 DECIDE_TAC THEN
156 SRW_TAC [][],
157 Q_TAC SUFF_TAC
158 `~(2 ** (dimindex(:'a) - 1) <= n /\ n < 2 ** dimindex(:'a))`
159 THEN1 METIS_TAC [] THEN STRIP_TAC THEN
160 `n DIV 2 ** (dimindex (:'a) - 1) = 1`
161 by (MATCH_MP_TAC DIV_UNIQUE THEN
162 Q.EXISTS_TAC `n - 2 ** (dimindex (:'a) - 1)` THEN
163 SRW_TAC [ARITH_ss][bitTheory.ZERO_LT_TWOEXP] THEN
164 SRW_TAC [][GSYM (CONJUNCT2 EXP)] THEN
165 Q_TAC SUFF_TAC `SUC (dimindex (:'a) - 1) =
166 dimindex (:'a)` THEN1 SRW_TAC [][] THEN
167 Q_TAC SUFF_TAC `0 < dimindex (:'a)` THEN1 DECIDE_TAC THEN
168 SRW_TAC [][DIMINDEX_GT_0]) THEN
169 FULL_SIMP_TAC (srw_ss()) []
170 ]
171QED
172
173Theorem i2w_w2i[simp]:
174 !w. i2w (w2i w) = w
175Proof
176 SRW_TAC [][i2w_def, w2i_def] THEN FULL_SIMP_TAC (srw_ss()) []
177QED
178
179Theorem w2i_i2w:
180 !i. INT_MIN (:'a) <= i /\ i <= INT_MAX (:'a)
181 ==>
182 (w2i (i2w i : 'a word) = i)
183Proof
184 STRIP_TAC THEN SIMP_TAC (srw_ss()) [INT_MIN_def, INT_MAX_def] THEN
185 `dimword(:'a) = 2 * INT_MIN(:'a)` by ACCEPT_TAC dimword_IS_TWICE_INT_MIN THEN
186 `0 < dimword(:'a)` by ACCEPT_TAC ZERO_LT_dimword THEN
187 `1n <= INT_MIN(:'a) /\ 1 <= dimword(:'a)` by DECIDE_TAC THEN
188 ASM_SIMP_TAC std_ss [w2i_def, i2w_def, WORD_NEG_NEG, word_2comp_n2w,
189 INT_LE, INT_SUB, INT_LE_SUB_RADD,
190 NOT_LESS_EQUAL] THEN
191 Cases_on `i < 0` THENL [
192 `?n. ~(n = 0) /\ (i = ~&n)`
193 by (Q.SPEC_THEN `i` STRIP_ASSUME_TAC INT_NUM_CASES THEN
194 FULL_SIMP_TAC (srw_ss()) []) THEN
195 ASM_SIMP_TAC std_ss [word_msb_n2w_numeric, word_2comp_n2w] THEN
196 ASM_SIMP_TAC (srw_ss()) [] THEN
197 STRIP_TAC THEN
198 `n MOD (2 * INT_MIN(:'a)) = n` by (MATCH_MP_TAC MOD_UNIQUE THEN
199 Q.EXISTS_TAC `0` THEN DECIDE_TAC) THEN
200 `2 * INT_MIN(:'a) - n < 2 * INT_MIN(:'a)` by DECIDE_TAC THEN
201 ASM_SIMP_TAC (srw_ss() ++ ARITH_ss) [LESS_MOD],
202 `?n. i = &n`
203 by (Q.SPEC_THEN `i` STRIP_ASSUME_TAC INT_NUM_CASES THEN
204 FULL_SIMP_TAC (srw_ss()) []) THEN
205 ASM_SIMP_TAC (srw_ss()) [word_msb_n2w_numeric, word_2comp_n2w] THEN
206 STRIP_TAC THEN
207 `n MOD (2 * INT_MIN(:'a)) = n` by (MATCH_MP_TAC MOD_UNIQUE THEN
208 Q.EXISTS_TAC `0` THEN DECIDE_TAC) THEN
209 ASM_SIMP_TAC (srw_ss() ++ ARITH_ss) []
210 ]
211QED
212
213Theorem word_msb_i2w:
214 !i. word_msb (i2w i : 'a word) = &(INT_MIN(:'a)) <= i % &(dimword(:'a))
215Proof
216 STRIP_TAC THEN
217 `dimword(:'a) = 2 * INT_MIN(:'a)` by ACCEPT_TAC dimword_IS_TWICE_INT_MIN THEN
218 `0 < dimword(:'a)` by ACCEPT_TAC ZERO_LT_dimword THEN
219 `1n <= INT_MIN(:'a) /\ 1 <= dimword(:'a)` by DECIDE_TAC THEN
220 ASM_SIMP_TAC (srw_ss()) [i2w_def] THEN
221 Cases_on `i < 0` THENL [
222 `?n. (i = ~&n) /\ ~(n = 0)`
223 by (Q.SPEC_THEN `i` STRIP_ASSUME_TAC INT_NUM_CASES THEN
224 FULL_SIMP_TAC (srw_ss()) []) THEN
225 `n MOD (2 * INT_MIN(:'a)) < 2 * INT_MIN(:'a)`
226 by SRW_TAC [ARITH_ss][DIVISION] THEN
227 `~(&(2 * INT_MIN(:'a)) = 0)` by SRW_TAC [ARITH_ss][] THEN
228 `(& (2 * INT_MIN(:'a)) - &n) % &(2 * INT_MIN(:'a)) =
229 (&(2 * INT_MIN(:'a)) - &n % &(2 * INT_MIN(:'a))) % &(2 * INT_MIN(:'a))`
230 by METIS_TAC [INT_MOD_MOD, INT_MOD_SUB] THEN
231 ASM_SIMP_TAC (srw_ss() ++ ARITH_ss) [word_2comp_n2w, word_msb_n2w_numeric,
232 INT_MOD_NEG_NUMERATOR, INT_MOD,
233 INT_SUB],
234 `?n. (i = &n)`
235 by (Q.SPEC_THEN `i` STRIP_ASSUME_TAC INT_NUM_CASES THEN
236 FULL_SIMP_TAC (srw_ss()) []) THEN
237 ASM_SIMP_TAC (srw_ss() ++ ARITH_ss) [word_msb_n2w_numeric, INT_MOD]
238 ]
239QED
240
241Theorem w2i_11[simp]:
242 !v w. (w2i v = w2i w) <=> (v = w)
243Proof
244 rpt strip_tac >> eq_tac >> rw[w2i_def]
245QED
246
247Theorem int_word_nchotomy:
248 !w. ?i. w = i2w i
249Proof PROVE_TAC [i2w_w2i]
250QED
251
252Theorem w2i_le:
253 !w:'a word. w2i w <= INT_MAX (:'a)
254Proof
255 SRW_TAC [] [w2i_def, INT_MAX_def, ZERO_LT_INT_MIN,
256 intLib.ARITH_PROVE ``0n < i ==> 0 <= &i - 1``,
257 intLib.ARITH_PROVE ``0i <= x ==> -&n <= x``]
258 THEN FULL_SIMP_TAC arith_ss [dimword_def, wordsTheory.INT_MIN_def,
259 WORD_LO, WORD_NOT_LOWER_EQUAL, WORD_MSB_INT_MIN_LS, word_L_def,
260 w2n_n2w, LESS_MOD, EXP_BASE_LT_MONO, DIMINDEX_GT_0]
261 THEN intLib.ARITH_TAC
262QED
263
264Theorem w2i_ge:
265 !w:'a word. INT_MIN (:'a) <= w2i w
266Proof
267 Tactical.REVERSE (SRW_TAC []
268 [w2i_def, INT_MIN_def, INT_MAX_def, INT_SUB_LNEG, INT_LE_REDUCE])
269 THEN1 intLib.ARITH_TAC
270 THEN IMP_RES_TAC TWO_COMP_NEG
271 THEN POP_ASSUM MP_TAC
272 THEN SRW_TAC [] []
273 THEN FULL_SIMP_TAC std_ss []
274 THENL [
275 Cases_on `w`
276 THEN `dimindex(:'a) = 1` by FULL_SIMP_TAC arith_ss [DIMINDEX_GT_0]
277 THEN FULL_SIMP_TAC std_ss [dimword_def, wordsTheory.INT_MIN_def]
278 THEN `(n = 0) \/ (n = 1)` by DECIDE_TAC
279 THEN SRW_TAC [] [dimword_def, word_2comp_def],
280 REWRITE_TAC [GSYM WORD_NEG_MUL, WORD_NEG_L]
281 THEN SRW_TAC [] [word_L_def, w2n_n2w, INT_MIN_LT_DIMWORD, LESS_MOD],
282 Q.ABBREV_TAC `x = -1w * w`
283 THEN FULL_SIMP_TAC arith_ss [dimword_def, wordsTheory.INT_MIN_def,
284 WORD_LO, WORD_NOT_LOWER_EQUAL, WORD_MSB_INT_MIN_LS, word_L_def,
285 w2n_n2w, LESS_MOD, EXP_BASE_LT_MONO, DIMINDEX_GT_0]
286 ]
287QED
288
289Theorem ranged_int_word_nchotomy:
290 !w:'a word. ?i. (w = i2w i) /\ INT_MIN (:'a) <= i /\ i <= INT_MAX (:'a)
291Proof
292 STRIP_TAC THEN Q.EXISTS_TAC `w2i w`
293 THEN SRW_TAC [] [i2w_w2i, w2i_le, w2i_ge]
294QED
295
296fun Cases_on_i2w t =
297 Q.ISPEC_THEN t Tactic.FULL_STRUCT_CASES_TAC ranged_int_word_nchotomy
298
299Theorem DIMINDEX_SUB1[local]:
300 2n ** (dimindex (:'a) - 1) < 2 ** dimindex (:'a)
301Proof
302 Cases_on `dimindex (:'a)` \\ FULL_SIMP_TAC arith_ss [DIMINDEX_GT_0]
303QED
304
305Theorem lem[local]:
306 !i. INT_MIN (:'a) <= i /\ i < 0 ==> Num (-i) <= INT_MIN (:'a)
307Proof
308 SRW_TAC [] [INT_MIN_def, INT_MAX_def, wordsTheory.INT_MIN_def]
309 \\ Cases_on `dimindex (:'a)`
310 \\ FULL_SIMP_TAC arith_ss [DIMINDEX_GT_0]
311 \\ intLib.ARITH_TAC
312QED
313
314Theorem lem2[local]:
315 !i. INT_MIN (:'a) <= i /\ i < 0 ==> Num (-i) < dimword(:'a)
316Proof
317 METIS_TAC [lem, wordsTheory.INT_MIN_LT_DIMWORD,
318 arithmeticTheory.LESS_EQ_LESS_TRANS]
319QED
320
321Theorem NEG_INT_ELIM[local]:
322 !i. INT_MIN (:'a) <= i /\ i < 0 /\ dimindex (:'a) <= dimindex(:'b) ==>
323 ?n. INT_MIN (:'a) <= n /\ n < dimword (:'a) /\
324 (-n2w (Num (-i)) = n2w n : 'a word) /\
325 (-n2w (Num (-i)) =
326 n2w (2 ** dimindex (:'b) - 2 ** dimindex (:'a) + n) : 'b word)
327Proof
328 REPEAT STRIP_TAC
329 \\ Q.EXISTS_TAC `dimword (:'a) - Num (-i)`
330 \\ SRW_TAC [ARITH_ss]
331 [wordsTheory.ONE_LT_dimword, ZERO_LT_INT_MIN, word_2comp_def, lem2]
332 \\ IMP_RES_TAC lem
333 THENL [
334 ASM_SIMP_TAC arith_ss
335 [wordsTheory.dimword_IS_TWICE_INT_MIN, wordsTheory.ZERO_LT_INT_MIN],
336 intLib.ARITH_TAC,
337 FULL_SIMP_TAC arith_ss [dimword_def, wordsTheory.INT_MIN_def]
338 \\ `2n ** dimindex (:'a) <= 2 ** dimindex (:'b)`
339 by METIS_TAC [bitTheory.TWOEXP_MONO2]
340 \\ `Num (-i) < 2n ** dimindex (:'a) /\
341 Num (-i) < 2n ** dimindex (:'b)`
342 by METIS_TAC [DIMINDEX_SUB1, arithmeticTheory.LESS_EQ_LESS_TRANS,
343 arithmeticTheory.LESS_LESS_EQ_TRANS]
344 \\ ASM_SIMP_TAC arith_ss [bitTheory.ZERO_LT_TWOEXP,
345 DECIDE ``c < b /\ b <= a ==> (a - b + (b - c) = a - c : num)``,
346 wordsTheory.MOD_COMPLEMENT |> Q.SPECL [`n`,`1`] |> GSYM
347 |> REWRITE_RULE [arithmeticTheory.MULT_LEFT_1]]
348 ]
349QED
350
351Theorem sw2sw_i2w:
352 !j. INT_MIN (:'b) <= j /\ j <= INT_MAX (:'b) /\
353 dimindex (:'b) <= dimindex (:'a) ==>
354 (sw2sw (i2w j : 'b word) = i2w j : 'a word)
355Proof
356 SRW_TAC [WORD_BIT_EQ_ss] [i2w_def]
357 THENL [
358 `?n. INT_MIN (:'b) <= n /\ n < dimword (:'b) /\
359 (-n2w (Num (-j)) = n2w n : 'b word) /\
360 (-n2w (Num (-j)) =
361 n2w (2 ** dimindex (:'a) - 2 ** dimindex (:'b) + n) : 'a word)`
362 by METIS_TAC [NEG_INT_ELIM]
363 \\ SRW_TAC [fcpLib.FCP_ss,ARITH_ss] [word_index, BIT_def]
364 THENL [
365 `2n ** dimindex (:'a) MOD 2 ** SUC i = 0`
366 by (`?k. dimindex (:'a) = k + SUC i`
367 by METIS_TAC [LESS_ADD_1, ADD_COMM, ADD_ASSOC, ADD1]
368 \\ ASM_SIMP_TAC arith_ss
369 [EXP_ADD, bitTheory.ZERO_LT_TWOEXP, MOD_EQ_0])
370 \\ `2n ** dimindex (:'b) MOD 2 ** SUC i = 0`
371 by (`?k. dimindex (:'b) = k + SUC i`
372 by METIS_TAC [LESS_ADD_1, ADD_COMM, ADD_ASSOC, ADD1]
373 \\ ASM_SIMP_TAC arith_ss
374 [EXP_ADD, bitTheory.ZERO_LT_TWOEXP, MOD_EQ_0])
375 \\ `2n ** dimindex (:'a) - 2 ** dimindex (:'b) =
376 (2n ** (dimindex (:'a) - SUC i) -
377 2n ** (dimindex (:'b) - SUC i)) * 2 ** SUC i`
378 by SRW_TAC [ARITH_ss]
379 [arithmeticTheory.RIGHT_SUB_DISTRIB, arithmeticTheory.EXP_SUB,
380 bitTheory.DIV_MULT_THM]
381 \\ ASM_SIMP_TAC std_ss [bitTheory.BITS_SUM2],
382 FULL_SIMP_TAC std_ss [NOT_LESS]
383 \\ `2n ** dimindex (:'a) MOD 2 ** i = 0`
384 by (`?k. dimindex (:'a) = k + i` by METIS_TAC [LESS_ADD]
385 \\ ASM_SIMP_TAC std_ss [EXP_ADD, bitTheory.ZERO_LT_TWOEXP, MOD_EQ_0])
386 \\ `2n ** i < 2 ** dimindex (:'a) /\
387 2n ** dimindex (:'b) <= 2 ** i`
388 by METIS_TAC [bitTheory.TWOEXP_MONO, bitTheory.TWOEXP_MONO2]
389 \\ `2n ** dimindex (:'a) - 2 ** dimindex (:'b) =
390 (2n ** (dimindex (:'a) - i) - 1) * 2 ** i +
391 (2 ** i - 2 ** dimindex (:'b))`
392 by SRW_TAC [ARITH_ss]
393 [arithmeticTheory.RIGHT_SUB_DISTRIB, arithmeticTheory.EXP_SUB,
394 bitTheory.DIV_MULT_THM,
395 DECIDE ``b < a /\ c <= b ==> (a - b + (b - c) = a - c : num)``]
396 \\ `2n ** i - 2 ** dimindex (:'b) + n < 2 ** i`
397 by METIS_TAC [dimword_def, bitTheory.TWOEXP_MONO2,
398 DECIDE ``b <= a /\ c < b ==> a - b + c < a : num``]
399 \\ ASM_SIMP_TAC std_ss [GSYM ADD_ASSOC, bitTheory.BITS_SUM,
400 bitTheory.BITS_ZERO4, REWRITE_RULE [BIT_def] bitTheory.BIT_EXP_SUB1]
401 \\ NTAC 8 (POP_ASSUM (K ALL_TAC))
402 \\ ASM_SIMP_TAC arith_ss []
403 \\ `?m. m < 2 ** (dimindex (:'b) - 1) /\
404 (n = 1 * 2 ** (dimindex (:'b) - 1) + m)`
405 by
406 (FULL_SIMP_TAC std_ss [wordsTheory.INT_MIN_def]
407 \\ Q.PAT_X_ASSUM `2n ** x <= n` (fn th => STRIP_ASSUME_TAC
408 (MATCH_MP arithmeticTheory.LESS_EQUAL_ADD th))
409 \\ Q.EXISTS_TAC `p`
410 \\ SRW_TAC [] []
411 \\ `2 ** (dimindex (:'b) - 1) + 2 ** (dimindex (:'b) - 1) =
412 dimword (:'b)`
413 by (SIMP_TAC std_ss [dimword_def]
414 \\ Cases_on `dimindex (:'b)`
415 \\ SIMP_TAC arith_ss [EXP]
416 \\ METIS_TAC [DIMINDEX_GT_0, DECIDE ``0n < n ==> ~(n = 0)``])
417 \\ FULL_SIMP_TAC arith_ss
418 [DECIDE ``p + b < c /\ (b + b = c) ==> p < b : num``])
419 \\ ASM_SIMP_TAC bool_ss [bitTheory.BITS_SUM]
420 \\ SIMP_TAC std_ss [GSYM BIT_def, bitTheory.BIT_B]
421 ],
422 SRW_TAC [fcpLib.FCP_ss] [word_index]
423 \\ `0 < i`
424 by (SPOSE_NOT_THEN ASSUME_TAC \\ `dimindex (:'b) = 0` by DECIDE_TAC
425 \\ METIS_TAC [DIMINDEX_GT_0, DECIDE ``(0n < i) = (i <> 0)``])
426 \\ FULL_SIMP_TAC std_ss
427 [INT_MAX_def, wordsTheory.INT_MIN_def, NOT_LESS,
428 integerTheory.INT_NOT_LT, intLib.ARITH_PROVE ``x <= y - 1i = x < y``]
429 \\ `Num j < 2n ** (dimindex (:'b) - 1)` by intLib.ARITH_TAC
430 \\ `2n ** (dimindex (:'b) - 1) < 2 ** i` by SRW_TAC [ARITH_ss] []
431 \\ `Num j < 2n ** i` by METIS_TAC [arithmeticTheory.LESS_TRANS]
432 \\ ASM_SIMP_TAC std_ss [bitTheory.NOT_BIT_GT_TWOEXP]
433 ]
434QED
435
436Theorem w2w_i2w:
437 !i. dimindex(:'a) <= dimindex(:'b) ==>
438 (w2w (i2w i : 'b word) = i2w i : 'a word)
439Proof
440 SRW_TAC [] [i2w_def, wordsTheory.w2w_n2w, wordsTheory.word_2comp_def]
441 \\ `?q. 0n < q /\ Num (-i) MOD (q * dimword (:'a)) < q * dimword (:'a) /\
442 (dimword (:'b) = q * dimword (:'a))`
443 by (IMP_RES_TAC arithmeticTheory.LESS_EQUAL_ADD
444 \\ Q.EXISTS_TAC `2n ** p`
445 \\ FULL_SIMP_TAC arith_ss [ZERO_LT_TWOEXP, dimword_def, GSYM EXP_ADD])
446 \\ ASM_SIMP_TAC arith_ss [wordsTheory.MOD_COMPLEMENT,
447 wordsTheory.ZERO_LT_dimword,
448 ONCE_REWRITE_RULE [MULT_COMM] arithmeticTheory.MOD_MULT_MOD]
449QED
450
451Theorem WORD_LTi: !a b. a < b = w2i a < w2i b
452Proof
453 reverse (RW_TAC std_ss [WORD_LT, GSYM WORD_LO, INT_LT_CALCULATE,
454 WORD_NEG_EQ_0, w2i_def, w2n_eq_0])
455 >- (strip_tac >> fs[]) >>
456 SRW_TAC [boolSimps.LET_ss] [word_lo_def,nzcv_def,
457 Once (DECIDE ``w2n (-b) + a = a + w2n (-b)``)] >>
458 Cases_on `~BIT (dimindex (:'a)) (w2n a + w2n (-b))` >>
459 FULL_SIMP_TAC std_ss [] >>
460 FULL_SIMP_TAC (std_ss++fcpLib.FCP_ss) [word_0, word_msb_def] >>
461 METIS_TAC [DECIDE ``0n < n ==> n - 1 < n``, DIMINDEX_GT_0]
462QED
463
464Theorem WORD_GTi:
465 !a b. a > b = w2i a > w2i b
466Proof
467 REWRITE_TAC [WORD_GREATER, int_gt, WORD_LTi]
468QED
469
470Theorem WORD_LEi:
471 !a b. a <= b = w2i a <= w2i b
472Proof
473 REWRITE_TAC [WORD_LESS_OR_EQ, INT_LE_LT, WORD_LTi, w2i_11]
474QED
475
476Theorem WORD_GEi:
477 !a b. a >= b = w2i a >= w2i b
478Proof
479 REWRITE_TAC [WORD_GREATER_EQ, int_ge, WORD_LEi]
480QED
481
482val sum_num = intLib.COOPER_PROVE
483 ``(Num (&a + &b) = a + b) /\
484 (-&a + -&b = -&(a + b)) /\
485 ~(&a + &b < 0i) /\
486 (-&a + &b < 0i = b < a:num) /\
487 (&a + -&b < 0i = a < b:num) /\
488 (&a - &b < 0i = a < b:num) /\
489 (~(&a + -&b < 0i) = b <= a:num) /\
490 (~(-&a + &b < 0i) = a <= b:num) /\
491 (~(&a - &b < 0i) = b <= a:num) /\
492 (~(-&a - &b < 0i) = (a = 0) /\ (b = 0))``
493
494val word_literal_sub =
495 METIS_PROVE [arithmeticTheory.NOT_LESS_EQUAL, WORD_LITERAL_ADD]
496 ``(m < n ==> (-n2w (n - m) = n2w m + -n2w n)) /\
497 (n <= m ==> (n2w (m - n) = n2w m + -n2w n))``
498
499Theorem word_add_i2w_w2n:
500 !a b. i2w (&w2n a + &w2n b) = a + b
501Proof
502 SRW_TAC [] [i2w_def, word_add_def, sum_num]
503QED
504
505Theorem word_add_i2w:
506 !a b. i2w (w2i a + w2i b) = a + b
507Proof
508 SRW_TAC [] [i2w_def, w2i_def]
509 THEN FULL_SIMP_TAC (srw_ss()++ARITH_ss)
510 [WORD_LEFT_ADD_DISTRIB, GSYM word_add_def, sum_num, word_literal_sub,
511 intLib.COOPER_PROVE
512 ``(&y < &x ==> (Num (-(-&x + &y)) = x - y)) /\
513 (&x < &y ==> (Num (-(&x + -&y)) = y - x)) /\
514 (~(&y < &x) ==> (Num (-&x + &y) = y - x)) /\
515 (~(&x < &y) ==> (Num (&x + -&y) = x - y))``]
516QED
517
518Theorem word_sub_i2w_w2n:
519 !a b. i2w (&w2n a - &w2n b) = a - b
520Proof
521 SRW_TAC [] [i2w_def, intLib.COOPER_PROVE
522 ``(&x - &y < 0i ==> (Num ((&y - &x)) = y - x)) /\
523 (~(&x - &y < 0i) ==> (Num ((&x - &y)) = x - y))``]
524 THEN FULL_SIMP_TAC (srw_ss()) [sum_num, word_literal_sub]
525QED
526
527Theorem word_sub_i2w:
528 !a b. i2w (w2i a - w2i b) = a - b
529Proof
530 SRW_TAC [] [i2w_def, w2i_def]
531 THEN FULL_SIMP_TAC (srw_ss()++ARITH_ss)
532 [WORD_LEFT_ADD_DISTRIB, GSYM word_add_def, sum_num, word_literal_sub,
533 intLib.COOPER_PROVE
534 ``(&x < &y ==> (Num (&y - &x) = y - x)) /\
535 (~(&x < &y) ==> (Num (&x - &y) = x - y))``]
536QED
537
538Theorem word_mul_i2w_w2n:
539 !a b. i2w (&w2n a * &w2n b) = a * b
540Proof
541 SRW_TAC [] [i2w_def]
542 THEN FULL_SIMP_TAC (srw_ss()++ARITH_ss)
543 [GSYM word_mul_def, INT_MUL_CALCULATE]
544QED
545
546Theorem word_mul_i2w:
547 !a b. i2w (w2i a * w2i b) = a * b
548Proof
549 SRW_TAC [] [i2w_def, w2i_def]
550 THEN FULL_SIMP_TAC (srw_ss()++ARITH_ss)
551 [GSYM word_mul_def, INT_MUL_CALCULATE]
552QED
553
554(* ------------------------------------------------------------------------- *)
555
556val word_literal_sub =
557 METIS_PROVE [arithmeticTheory.NOT_LESS_EQUAL, WORD_LITERAL_ADD]
558 ``(m < n ==> (n2w m + -n2w n = -n2w (n - m))) /\
559 (n <= m ==> (n2w m + -n2w n = n2w (m - n)))``
560
561val sum_num = intLib.ARITH_PROVE
562 ``(a < 0 /\ b < 0 ==> (Num (-a) + Num (-b) = Num (-(a + b)))) /\
563 (0 <= a /\ 0 <= b ==> (Num a + Num b = Num (a + b))) /\
564 (0 <= b /\ a + b < 0 ==> (Num (-a) - Num b = Num (-(a + b)))) /\
565 (a < 0 /\ 0 <= b /\ 0 <= a + b ==> (Num b - Num (-a) = Num (a + b))) /\
566 (0 <= a /\ b < 0 /\ a + b < 0 ==> (Num (-b) - Num a = Num (-(a + b)))) /\
567 (b < 0 /\ 0 <= a + b ==> (Num a - Num (-b) = Num (a + b)))``
568
569Theorem word_i2w_add:
570 !a b. i2w a + i2w b = i2w (a + b)
571Proof
572 SRW_TAC [] [i2w_def, w2i_def]
573 THEN FULL_SIMP_TAC (srw_ss()++INT_ARITH_ss)
574 [integerTheory.INT_NOT_LT, word_add_n2w, word_literal_sub, sum_num,
575 EQT_ELIM (wordsLib.WORD_ARITH_CONV
576 ``(-a + -b = -c : 'a word) = (a + b = c)``)]
577 THENL [
578 `Num b < Num (-a)` by intLib.ARITH_TAC,
579 `Num (-a) <= Num b` by intLib.ARITH_TAC,
580 `Num a < Num (-b)` by intLib.ARITH_TAC,
581 `Num (-b) <= Num a` by intLib.ARITH_TAC]
582 THEN ASM_SIMP_TAC std_ss [word_literal_sub, sum_num]
583QED
584
585Theorem mult_num[local]:
586 (!i j. 0 <= i /\ 0 <= j ==> (Num i * Num j = Num (i * j))) /\
587 (!i j. 0 <= i /\ j < 0 ==> (Num i * Num (-j) = Num (-(i * j))))
588Proof
589 STRIP_TAC THEN Cases_on `i` THEN Cases_on `j`
590 THEN SRW_TAC [] [NUM_OF_INT, INT_NEG_RMUL]
591QED
592
593Theorem mult_lt[local]:
594 (!i:int j. 0 <= i /\ j < 0 ==> i * j <= 0) /\
595 (!i:int j. i < 0 /\ 0 <= j ==> i * j <= 0)
596Proof
597 STRIP_TAC THEN Cases_on `i` THEN Cases_on `j`
598 THEN SRW_TAC [] [NUM_OF_INT, INT_MUL_CALCULATE]
599QED
600
601Theorem word_i2w_mul:
602 !a b. i2w a * i2w b = i2w (a * b)
603Proof
604 SRW_TAC [] [i2w_def, w2i_def]
605 THEN FULL_SIMP_TAC (srw_ss()++INT_ARITH_ss)
606 [integerTheory.INT_NOT_LT, word_mul_n2w, WORD_LITERAL_MULT, mult_num,
607 integerTheory.INT_MUL_SIGN_CASES, INT_MUL_CALCULATE,
608 AC INT_MUL_COMM INT_MUL_ASSOC]
609 THEN IMP_RES_TAC mult_lt
610 THEN `a * b = 0` by intLib.ARITH_TAC
611 THEN ASM_SIMP_TAC (srw_ss()) []
612QED
613
614(* ------------------------------------------------------------------------- *)
615
616Theorem MINUS_ONE[local]:
617 -1w = i2w (-1)
618Proof SRW_TAC [] [i2w_def]
619QED
620
621Theorem MULT_MINUS_ONE:
622 !i. -1w * i2w i = i2w (-i)
623Proof
624 REWRITE_TAC [MINUS_ONE, word_i2w_mul, GSYM INT_NEG_MINUS1]
625QED
626
627Theorem word_0_w2i:
628 w2i 0w = 0
629Proof
630 SRW_TAC [] [i2w_def, w2i_def]
631QED
632
633Theorem w2i_eq_0:
634 !w : 'a word. (w2i w = 0) = (w = 0w)
635Proof
636 SRW_TAC [] [i2w_def, w2i_def]
637QED
638
639(* ------------------------------------------------------------------------- *)
640
641Theorem DIV_POS[local]:
642 !i n. ~(i < 0) /\ 0n < n ==> ~(i / &n < 0)
643Proof
644 Cases \\ SRW_TAC [ARITH_ss] [integerTheory.INT_DIV_CALCULATE]
645QED
646
647Theorem DIV_NEG[local]:
648 !i n. i < 0i /\ 0n < n ==> i / &n < 0
649Proof
650 Cases \\ SRW_TAC [ARITH_ss] [integerTheory.INT_DIV_CALCULATE]
651 \\ `&n' <> 0` by intLib.ARITH_TAC
652 \\ SRW_TAC [] [integerTheory.int_div]
653 THENL [
654 Cases_on `n < n'`
655 \\ FULL_SIMP_TAC arith_ss [NOT_LESS]
656 \\ IMP_RES_TAC LESS_EQUAL_ADD
657 \\ POP_ASSUM SUBST1_TAC
658 \\ ASM_SIMP_TAC arith_ss [arithmeticTheory.ADD_DIV_RWT],
659 intLib.ARITH_TAC
660 ]
661QED
662
663Theorem DIV_NUM_POS[local]:
664 !i j. 0 < j /\ 0i <= i ==> (Num (i / &j) = Num i DIV j)
665Proof
666 Cases \\ SRW_TAC [ARITH_ss] [integerTheory.INT_DIV_CALCULATE]
667QED
668
669Theorem DIV_NUM_NEG[local]:
670 !i j. 0 < j /\ i < 0i ==>
671 (Num (-(i / &j)) =
672 Num (-i) DIV j + (if Num (-i) MOD j = 0 then 0 else 1))
673Proof
674 Cases \\ SRW_TAC [ARITH_ss] [integerTheory.INT_DIV_CALCULATE]
675 \\ `&j <> 0` by intLib.ARITH_TAC
676 \\ SRW_TAC [] [integerTheory.int_div, integerTheory.INT_NEG_ADD]
677 \\ intLib.ARITH_TAC
678QED
679
680Theorem NEG_NUM_LT_INT_MIN[local]:
681 !i. INT_MIN (:'a) <= i /\ i < 0 ==> Num (-i) <= INT_MIN (:'a)
682Proof
683 SRW_TAC [] [INT_MIN_def, INT_MAX_def, wordsTheory.INT_MIN_def]
684 \\ Cases_on `dimindex (:'a)`
685 \\ FULL_SIMP_TAC arith_ss [DIMINDEX_GT_0]
686 \\ intLib.ARITH_TAC
687QED
688
689Theorem NEG_NUM_LT_DIMWORD[local]:
690 !i. INT_MIN (:'a) <= i /\ i < 0 ==> Num (-i) < dimword(:'a)
691Proof
692 METIS_TAC [NEG_NUM_LT_INT_MIN, wordsTheory.INT_MIN_LT_DIMWORD,
693 arithmeticTheory.LESS_EQ_LESS_TRANS]
694QED
695
696Theorem NEG_MSB[local]:
697 !i. i < 0i /\ INT_MIN (:'a) <= i ==>
698 BIT (dimindex (:'a) - 1) (2 ** dimindex (:'a) - Num (-i))
699Proof
700 SRW_TAC [] [INT_MIN_def, INT_MAX_def, wordsTheory.INT_MIN_def]
701 \\ `Num (-i) <= 2n ** (dimindex (:'a) - 1)` by intLib.ARITH_TAC
702 \\ Cases_on `dimindex (:'a)`
703 \\ FULL_SIMP_TAC arith_ss [wordsTheory.DIMINDEX_GT_0,
704 DECIDE ``0n < n ==> n <> 0``]
705 \\ IMP_RES_TAC LESS_EQUAL_ADD
706 \\ `Num (-i) = 2 ** n - p` by DECIDE_TAC
707 \\ POP_ASSUM SUBST1_TAC
708 \\ `p < 2 ** n` by intLib.ARITH_TAC
709 \\ Q.PAT_X_ASSUM `x = y + z : num` (K ALL_TAC)
710 \\ ASM_SIMP_TAC bool_ss [EXP, BIT_def,
711 DECIDE ``p < n ==> (2n * n - (n - p) = n + p)``,
712 bitTheory.BITS_SUM |> Q.SPECL [`n`,`n`,`1`] |> SIMP_RULE std_ss []]
713 \\ SIMP_TAC std_ss [GSYM BIT_def, bitTheory.BIT_B]
714QED
715
716Theorem DIMINDEX_SUB1[local]:
717 2n ** (dimindex (:'a) - 1) < 2 ** dimindex (:'a)
718Proof
719 Cases_on `dimindex (:'a)` \\ FULL_SIMP_TAC arith_ss [DIMINDEX_GT_0]
720QED
721
722Theorem i2w_DIV:
723 !n i.
724 n < dimindex (:'a) /\ INT_MIN (:'a) <= i /\ i <= INT_MAX (:'a) ==>
725 (i2w (i / 2 ** n) : 'a word = i2w i >> n)
726Proof
727 SRW_TAC [wordsLib.WORD_BIT_EQ_ss]
728 [i2w_def, DIV_POS, word_2comp_n2w, DIV_NEG, word_index]
729 \\ FULL_SIMP_TAC std_ss
730 [DIV_NUM_POS, DIV_NUM_NEG, ZERO_LT_TWOEXP, integerTheory.INT_NOT_LT]
731 THENL [
732 IMP_RES_TAC NEG_NUM_LT_DIMWORD
733 \\ FULL_SIMP_TAC std_ss [dimword_def]
734 \\ `Num (-i) < 2n ** dimindex (:'a)` by intLib.ARITH_TAC
735 \\ Cases_on `dimindex (:'a) <= i' + n`
736 \\ FULL_SIMP_TAC arith_ss [arithmeticTheory.NOT_LESS_EQUAL, BIT_SHIFT_THM5]
737 \\ `Num (-i) <> 0` by intLib.ARITH_TAC
738 \\ SRW_TAC [ARITH_ss] [BIT_COMPLEMENT, NEG_MSB, DIV_LT]
739 THENL [
740 METIS_TAC [MOD_ZERO_GT, DIV_GT0, ZERO_LT_TWOEXP,
741 DECIDE ``0n < x ==> (x <> 0)``],
742 IMP_RES_TAC MOD_ZERO_GT
743 \\ IMP_RES_TAC DIV_SUB1
744 \\ `Num (-i) < 2 ** (i' + n)`
745 by METIS_TAC [TWOEXP_MONO2, arithmeticTheory.LESS_LESS_EQ_TRANS]
746 \\ `Num (-i) - 1 < 2n ** (i' + n)` by DECIDE_TAC
747 \\ ASM_SIMP_TAC arith_ss [BIT_SHIFT_THM4, bitTheory.NOT_BIT_GT_TWOEXP],
748 IMP_RES_TAC NEG_NUM_LT_INT_MIN
749 \\ FULL_SIMP_TAC std_ss [wordsTheory.INT_MIN_def]
750 \\ `1n < 2 ** n` by ASM_SIMP_TAC arith_ss [arithmeticTheory.ONE_LT_EXP]
751 \\ `Num (-i) DIV 2 ** n < Num (-i)`
752 by ASM_SIMP_TAC arith_ss [arithmeticTheory.DIV_LESS, ZERO_LT_TWOEXP]
753 \\ `Num (-i) DIV 2 ** n + 1 <= Num (-i)` by DECIDE_TAC
754 \\ `Num (-i) DIV 2 ** n + 1 < 2 ** dimindex (:'a)`
755 by METIS_TAC [arithmeticTheory.LESS_EQ_TRANS,
756 arithmeticTheory.LESS_EQ_LESS_TRANS,
757 DIMINDEX_SUB1, TWOEXP_MONO]
758 \\ ASM_SIMP_TAC arith_ss [],
759 `Num (-i) < 2 ** (i' + n)`
760 by METIS_TAC [TWOEXP_MONO2, arithmeticTheory.LESS_LESS_EQ_TRANS]
761 \\ `1n < 2 ** n` by ASM_SIMP_TAC arith_ss [arithmeticTheory.ONE_LT_EXP]
762 \\ `Num (-i) DIV 2 ** n < Num (-i)`
763 by ASM_SIMP_TAC arith_ss [arithmeticTheory.DIV_LESS, ZERO_LT_TWOEXP]
764 \\ `Num (-i) DIV 2 ** n + 1 <= Num (-i)` by DECIDE_TAC
765 \\ `Num (-i) DIV 2 ** n + 1 < 2 ** dimindex (:'a)`
766 by METIS_TAC [arithmeticTheory.LESS_EQ_TRANS,
767 arithmeticTheory.LESS_EQ_LESS_TRANS,
768 DIMINDEX_SUB1, TWOEXP_MONO]
769 \\ ASM_SIMP_TAC arith_ss [BIT_SHIFT_THM4, bitTheory.NOT_BIT_GT_TWOEXP]
770 ],
771 SRW_TAC [ARITH_ss] [BIT_SHIFT_THM4]
772 \\ FULL_SIMP_TAC std_ss [INT_MAX_def, wordsTheory.INT_MIN_def,
773 intLib.ARITH_PROVE ``i <= &n - 1 = i < &n``]
774 \\ `Num i < 2n ** (dimindex (:'a) - 1)` by intLib.ARITH_TAC
775 \\ `dimindex (:'a) - 1 < i' + n` by DECIDE_TAC
776 \\ `Num i < 2n ** (i' + n)` by METIS_TAC [TWOEXP_MONO, LESS_TRANS]
777 \\ SRW_TAC [] [bitTheory.NOT_BIT_GT_TWOEXP]
778 ]
779QED
780
781(* ------------------------------------------------------------------------- *)
782
783Theorem INT_MIN_MONOTONIC:
784 dimindex (:'a) <= dimindex (:'b) ==> INT_MIN (:'b) <= INT_MIN (:'a) : int
785Proof
786 SRW_TAC [] [INT_MIN_def, INT_MAX_def, wordsTheory.INT_MIN_def]
787 \\ intLib.ARITH_TAC
788QED
789
790Theorem INT_MAX_MONOTONIC:
791 dimindex (:'a) <= dimindex (:'b) ==> INT_MAX (:'a) <= INT_MAX (:'b) : int
792Proof
793 SRW_TAC [] [INT_MAX_def, wordsTheory.INT_MIN_def,
794 intLib.ARITH_PROVE ``x - 1 <= y - 1i = x <= y``]
795 \\ intLib.ARITH_TAC
796QED
797
798Theorem w2i_sw2sw_bounds:
799 !w : 'a word.
800 INT_MIN (:'a) <= w2i (sw2sw w : 'b word) /\
801 w2i (sw2sw w : 'b word) <= INT_MAX (:'a)
802Proof
803 STRIP_TAC \\ Cases_on `dimindex (:'b) <= dimindex (:'a)`
804 THENL [
805 IMP_RES_TAC INT_MIN_MONOTONIC
806 \\ IMP_RES_TAC INT_MAX_MONOTONIC
807 \\ Q.ISPEC_THEN `sw2sw w : 'b word` ASSUME_TAC w2i_le
808 \\ Q.ISPEC_THEN `sw2sw w : 'b word` ASSUME_TAC w2i_ge
809 \\ intLib.ARITH_TAC,
810 FULL_SIMP_TAC std_ss [arithmeticTheory.NOT_LESS_EQUAL]
811 \\ Cases_on_i2w `w : 'a word`
812 \\ `dimindex (:'a) <= dimindex (:'b)` by DECIDE_TAC
813 \\ IMP_RES_TAC INT_MIN_MONOTONIC
814 \\ IMP_RES_TAC INT_MAX_MONOTONIC
815 \\ SRW_TAC [intLib.INT_ARITH_ss] [sw2sw_i2w, w2i_i2w]
816 ]
817QED
818
819Theorem w2i_i2w_id:
820 !i. INT_MIN (:'a) <= i /\ i <= INT_MAX (:'a) /\
821 dimindex (:'b) <= dimindex (:'a) ==>
822 ((i = w2i (i2w i : 'b word)) =
823 (i2w i = sw2sw (i2w i : 'b word) : 'a word))
824Proof
825 STRIP_TAC
826 \\ Cases_on `INT_MIN (:'b) <= i /\ i <= INT_MAX (:'b)`
827 \\ SRW_TAC [ARITH_ss] [sw2sw_i2w, w2i_i2w]
828 \\ METIS_TAC [w2i_le, w2i_ge, w2i_sw2sw_bounds, w2i_i2w]
829QED
830
831Theorem w2i_11_lift:
832 !a:'a word b:'b word.
833 dimindex (:'a) <= dimindex (:'c) /\ dimindex (:'b) <= dimindex (:'c) ==>
834 ((w2i a = w2i b) = (sw2sw a = sw2sw b : 'c word))
835Proof
836 REPEAT STRIP_TAC
837 \\ IMP_RES_TAC INT_MIN_MONOTONIC
838 \\ IMP_RES_TAC INT_MAX_MONOTONIC
839 \\ Cases_on_i2w `a:'a word`
840 \\ Cases_on_i2w `b:'b word`
841 \\ SRW_TAC [] [dimindex_dimword_le_iso, w2i_i2w, sw2sw_i2w]
842 \\ `INT_MIN (:'c) <= i /\ i <= INT_MAX (:'c)` by intLib.ARITH_TAC
843 \\ `INT_MIN (:'c) <= i' /\ i' <= INT_MAX (:'c)` by intLib.ARITH_TAC
844 \\ METIS_TAC[w2i_11, w2i_i2w]
845QED
846
847Theorem w2i_n2w_mod:
848 !n m. n < dimword (:'a) /\ m <= dimindex (:'a) ==>
849 (Num (w2i (n2w n : 'a word) % 2 ** m) = n MOD 2 ** m)
850Proof
851 REPEAT STRIP_TAC
852 \\ `&(dimword (:'a) - n) = &dimword (:'a) - &n`
853 by SRW_TAC [ARITH_ss] [integerTheory.INT_SUB]
854 \\ `?q. dimword (:'a) = q * 2 ** m`
855 by (IMP_RES_TAC LESS_EQUAL_ADD
856 \\ Q.EXISTS_TAC `2n ** p`
857 \\ ASM_SIMP_TAC arith_ss [dimword_def, EXP_ADD])
858 \\ Cases_on `n < INT_MIN (:'a)`
859 \\ FULL_SIMP_TAC arith_ss
860 [NOT_LESS, w2i_n2w_neg, w2i_n2w_pos,
861 simpLib.SIMP_PROVE (srw_ss()) [] ``2i ** n = &(2n ** n)``,
862 integerTheory.NUM_OF_INT, int_arithTheory.INT_SUB_SUB3,
863 integerTheory.INT_MOD_CALCULATE, integerTheory.INT_MOD_NEG_NUMERATOR]
864 \\ `0i <> &(2n ** m)` by SRW_TAC [] []
865 \\ ASM_SIMP_TAC arith_ss
866 [Once (GSYM integerTheory.INT_MOD_SUB), integerTheory.INT_MOD_CALCULATE,
867 arithmeticTheory.MOD_EQ_0, integerTheory.INT_SUB_RZERO,
868 integerTheory.INT_MOD_ADD_MULTIPLES
869 |> Q.INST [`q` |-> `1i`]
870 |> REWRITE_RULE [integerTheory.INT_MUL_LID],
871 integerTheory.NUM_OF_INT]
872QED
873
874Theorem word_abs_w2i:
875 !w. word_abs w = n2w (Num (ABS (w2i w)))
876Proof
877 STRIP_TAC \\ Cases_on_i2w `w : 'a word`
878 \\ SRW_TAC [] [w2i_i2w, word_abs_def, WORD_LTi, word_0_w2i]
879 \\ SRW_TAC [] [i2w_def, intLib.ARITH_PROVE ``~(i < 0) ==> (ABS i = i)``,
880 intLib.ARITH_PROVE ``i < 0 ==> (ABS i = -i)``,
881 wordsTheory.WORD_LITERAL_MULT]
882QED
883
884Theorem word_abs_i2w:
885 !i. INT_MIN (:'a) <= i /\ i <= INT_MAX (:'a) ==>
886 (word_abs (i2w i) = n2w (Num (ABS i)) : 'a word)
887Proof
888 SRW_TAC [] [word_abs_w2i, w2i_i2w]
889QED
890
891(* ------------------------------------------------------------------------- *)
892
893Theorem INT_MIN[simp]:
894 INT_MIN (:'a) = -&words$INT_MIN (:'a)
895Proof
896 SRW_TAC [] [INT_MIN_def, INT_MAX_def, wordsTheory.INT_MIN_def]
897QED
898
899Theorem INT_MAX[simp]:
900 INT_MAX (:'a) = &words$INT_MAX (:'a)
901Proof
902 SRW_TAC [] [INT_MAX_def, wordsTheory.INT_MAX_def, int_arithTheory.INT_NUM_SUB]
903 \\ FULL_SIMP_TAC arith_ss [wordsTheory.ZERO_LT_INT_MIN]
904QED
905
906Theorem UINT_MAX[simp]:
907 UINT_MAX (:'a) = &words$UINT_MAX (:'a)
908Proof
909 SRW_TAC [] [UINT_MAX_def, wordsTheory.UINT_MAX_def,
910 int_arithTheory.INT_NUM_SUB]
911 \\ ASSUME_TAC wordsTheory.ZERO_LT_dimword
912 \\ DECIDE_TAC
913QED
914
915Theorem INT_BOUND_ORDER:
916 INT_MIN (:'a) < INT_MAX (:'a) : int /\
917 INT_MAX (:'a) < UINT_MAX (:'a) : int /\
918 UINT_MAX (:'a) < &dimword (:'a)
919Proof
920 SRW_TAC [ARITH_ss] [BOUND_ORDER]
921QED
922
923Theorem INT_ZERO_LT_INT_MIN[simp]:
924 INT_MIN (:'a) < 0
925Proof
926 SRW_TAC [ARITH_ss] [ZERO_LT_INT_MIN]
927QED
928
929Theorem INT_ZERO_LT_INT_MAX:
930 1 < dimindex(:'a) ==> 0i < INT_MAX (:'a)
931Proof
932 SRW_TAC [ARITH_ss] [ZERO_LT_INT_MAX]
933QED
934
935Theorem INT_ZERO_LE_INT_MAX:
936 0i <= INT_MAX (:'a)
937Proof
938 SRW_TAC [ARITH_ss] [ZERO_LE_INT_MAX]
939QED
940
941Theorem INT_ZERO_LT_UINT_MAX[simp]:
942 0i < UINT_MAX (:'a)
943Proof
944 SRW_TAC [ARITH_ss] [ZERO_LT_UINT_MAX]
945QED
946
947Theorem w2i_1:
948 w2i (1w:'a word) = if dimindex(:'a) = 1 then -1 else 1
949Proof
950 srw_tac [ARITH_ss]
951 [wordsTheory.word_2comp_dimindex_1, w2i_def, word_msb_def,
952 wordsTheory.word_index]
953 \\ full_simp_tac (srw_ss()) [DECIDE ``0n < n /\ n <> 1 ==> ~(n <= 1)``]
954QED
955
956Theorem w2i_INT_MINw:
957 w2i (INT_MINw: 'a word) = INT_MIN (:'a)
958Proof
959 SRW_TAC [ARITH_ss] [w2i_n2w_neg, word_L_def, INT_MIN_LT_DIMWORD,
960 dimword_sub_int_min]
961QED
962
963Theorem w2i_UINT_MAXw:
964 w2i (UINT_MAXw: 'a word) = -1i
965Proof
966 SRW_TAC [ARITH_ss] [w2i_n2w_neg, word_T_def, BOUND_ORDER]
967 \\ SRW_TAC [] [wordsTheory.UINT_MAX_def,
968 DECIDE ``0n < n ==> (n - (n - 1) = 1)``]
969QED
970
971Theorem w2i_INT_MAXw:
972 w2i (INT_MAXw: 'a word) = INT_MAX (:'a)
973Proof
974 RW_TAC arith_ss [w2i_n2w_pos, word_H_def, BOUND_ORDER]
975 \\ SRW_TAC [] []
976QED
977
978Theorem w2i_minus_1 =
979 SIMP_RULE (srw_ss()) [] w2i_UINT_MAXw
980
981Theorem w2i_lt_0:
982 !w: 'a word. w2i w < 0 = w < 0w
983Proof
984 STRIP_TAC \\ Cases_on_i2w `w: 'a word`
985 \\ SRW_TAC [] [w2i_i2w, word_0_w2i, WORD_LTi]
986QED
987
988Theorem w2i_neg:
989 !w:'a word. w <> INT_MINw ==> (w2i (-w) = -w2i w)
990Proof
991 SRW_TAC [] [w2i_def]
992 \\ IMP_RES_TAC TWO_COMP_POS
993 \\ IMP_RES_TAC TWO_COMP_NEG
994 \\ NTAC 2 (POP_ASSUM MP_TAC)
995 \\ SRW_TAC [ARITH_ss] []
996 >- (Cases_on `w`
997 \\ `dimindex(:'a) = 1`
998 by metis_tac [DECIDE ``0n < i /\ i <= 1 ==> (i = 1)``,
999 wordsTheory.DIMINDEX_GT_0]
1000 \\ fs [wordsTheory.word_L_def, wordsTheory.INT_MIN_def,
1001 wordsTheory.dimword_def])
1002 \\ FULL_SIMP_TAC (srw_ss()) []
1003QED
1004
1005Theorem i2w_0:
1006 i2w 0 = 0w
1007Proof
1008 SRW_TAC [] [i2w_def]
1009QED
1010
1011Theorem i2w_minus_1:
1012 i2w (-1) = -1w
1013Proof
1014 SRW_TAC [] [i2w_def]
1015QED
1016
1017Theorem i2w_INT_MIN:
1018 i2w (INT_MIN (:'a)) = INT_MINw : 'a word
1019Proof
1020 `INT_MIN (:'a) <= INT_MAX (:'a) : int`
1021 by SRW_TAC [intLib.INT_ARITH_ss] [INT_BOUND_ORDER]
1022 \\ RW_TAC (std_ss++intLib.INT_ARITH_ss) [GSYM w2i_11, w2i_INT_MINw, w2i_i2w]
1023QED
1024
1025Theorem i2w_INT_MAX:
1026 i2w (INT_MAX (:'a)) = INT_MAXw : 'a word
1027Proof
1028 `INT_MIN (:'a) <= INT_MAX (:'a) : int`
1029 by SRW_TAC [intLib.INT_ARITH_ss] [INT_BOUND_ORDER]
1030 \\ RW_TAC (std_ss++intLib.INT_ARITH_ss) [GSYM w2i_11, w2i_INT_MAXw, w2i_i2w]
1031QED
1032
1033Theorem i2w_UINT_MAX:
1034 i2w (UINT_MAX (:'a)) = UINT_MAXw : 'a word
1035Proof
1036 rw_tac (std_ss++intLib.INT_ARITH_ss) [GSYM w2i_11, w2i_UINT_MAXw, i2w_def]
1037 \\ full_simp_tac std_ss [INT_ZERO_LT_UINT_MAX,
1038 intLib.ARITH_PROVE ``0i < n ==> ~(n < 0i)``]
1039 \\ fsrw_tac [] [GSYM wordsTheory.word_T_def, w2i_minus_1]
1040QED
1041
1042Theorem word_msb_i2w_lt_0:
1043 !i. INT_MIN (:'a) <= i /\ i <= INT_MAX (:'a) ==>
1044 (word_msb (i2w i : 'a word) = i < 0)
1045Proof
1046 Cases
1047 \\ srw_tac [intSimps.INT_ARITH_ss]
1048 [i2w_def, wordsTheory.word_2comp_n2w, wordsTheory.word_msb_n2w_numeric,
1049 arithmeticTheory.NOT_LESS_EQUAL]
1050 \\ `n < dimword(:'a)`
1051 by metis_tac
1052 [wordsTheory.INT_MIN_LT_DIMWORD, wordsTheory.INT_MAX_LT_DIMWORD,
1053 arithmeticTheory.LESS_EQ_LESS_TRANS]
1054 >- (`n < INT_MIN(:'a)`
1055 by metis_tac [arithmeticTheory.LESS_EQ_LESS_TRANS,
1056 wordsTheory.BOUND_ORDER]
1057 \\ simp [])
1058 \\ simp [arithmeticTheory.SUB_LEFT_LESS_EQ,
1059 wordsTheory.dimword_IS_TWICE_INT_MIN]
1060QED
1061
1062Theorem lem1[local]:
1063 !n. n <= INT_MIN (:'a) ==> (w2n (i2w (&n) : 'a word) = n)
1064Proof
1065 rw [wordsTheory.w2n_eq_0, i2w_def]
1066 \\ `n < dimword(:'a)`
1067 by metis_tac [wordsTheory.INT_MIN_LT_DIMWORD,
1068 arithmeticTheory.LESS_EQ_LESS_TRANS]
1069 \\ simp []
1070QED
1071
1072Theorem lem2[local]:
1073 !n. n <= INT_MAX (:'a) ==> (w2n (i2w (&n) : 'a word) = n)
1074Proof
1075 rw [wordsTheory.w2n_eq_0, i2w_def]
1076 \\ `n < dimword(:'a)`
1077 by metis_tac [wordsTheory.INT_MAX_LT_DIMWORD,
1078 arithmeticTheory.LESS_EQ_LESS_TRANS]
1079 \\ simp []
1080QED
1081
1082Theorem lem3[local]:
1083 !a b. (-1w * a = -1w * b) = (a = b)
1084Proof
1085 srw_tac [wordsLib.WORD_CANCEL_ss] []
1086QED
1087
1088Theorem i2w_pos:
1089 !n. i2w (&n) = n2w n
1090Proof
1091 rw [i2w_def]
1092QED
1093
1094Theorem word_quot:
1095 !a b. b <> 0w ==> (word_quot a b = i2w (w2i a quot w2i b))
1096Proof
1097 rpt strip_tac
1098 \\ Cases_on_i2w `a`
1099 \\ Cases_on_i2w `b`
1100 \\ qmatch_goalsub_rename_tac `i2w i / i2w j : 'a word`
1101 \\ `j <> 0` by (spose_not_then assume_tac \\ fs [i2w_0])
1102 \\ simp [w2i_i2w, word_msb_i2w_lt_0, word_quot_def, word_div_def]
1103 \\ rw [MULT_MINUS_ONE]
1104 \\ full_simp_tac (int_ss++intSimps.COOPER_ss) []
1105 \\ Cases_on `i`
1106 \\ Cases_on `j`
1107 \\ fs [i2w_0, arithmeticTheory.ZERO_DIV, lem1, lem2, lem3,
1108 GSYM MULT_MINUS_ONE]
1109 \\ simp [i2w_pos]
1110QED
1111
1112Theorem word_rem:
1113 !a b. b <> 0w ==> (word_rem a b = i2w (w2i a rem w2i b))
1114Proof
1115 rpt strip_tac
1116 \\ Cases_on_i2w `a`
1117 \\ Cases_on_i2w `b`
1118 \\ qmatch_goalsub_rename_tac `word_rem (i2w i) (i2w j) : 'a word`
1119 \\ `j <> 0` by (spose_not_then assume_tac \\ fs [i2w_0])
1120 \\ simp [w2i_i2w, word_msb_i2w_lt_0, word_rem_def, word_mod_def]
1121 \\ rw [MULT_MINUS_ONE]
1122 \\ full_simp_tac (int_ss++intSimps.COOPER_ss) []
1123 \\ Cases_on `i`
1124 \\ Cases_on `j`
1125 \\ fs [i2w_0, arithmeticTheory.ZERO_DIV, lem1, lem2, lem3,
1126 GSYM MULT_MINUS_ONE]
1127 \\ simp [i2w_pos]
1128QED
1129
1130Theorem saturate_i2w_0:
1131 saturate_i2w 0 = 0w
1132Proof
1133 SRW_TAC [ARITH_ss] [saturate_i2w_def, wordsTheory.ZERO_LT_UINT_MAX]
1134QED
1135
1136Theorem saturate_i2sw_0:
1137 saturate_i2sw 0 = 0w
1138Proof
1139 SRW_TAC [ARITH_ss] [i2w_0, saturate_i2sw_def]
1140 \\ FULL_SIMP_TAC arith_ss
1141 [wordsTheory.ZERO_LT_INT_MIN, DECIDE ``0n < n ==> n <> 0``]
1142 \\ Cases_on `1 < dimindex(:'a)`
1143 \\ FULL_SIMP_TAC arith_ss
1144 [wordsTheory.ZERO_LT_INT_MAX, DECIDE ``0n < n ==> n <> 0``]
1145 \\ `dimindex (:'a) = 1`
1146 by SRW_TAC [] [DECIDE ``0n < n /\ ~(1 < n) ==> (n = 1)``]
1147 \\ SRW_TAC [] [word_L_def, wordsTheory.INT_MIN_def]
1148QED
1149
1150(* ------------------------------------------------------------------------- *)
1151
1152Theorem saturate_w2sw:
1153 !w: 'a word.
1154 saturate_w2sw w : 'b word =
1155 if dimindex(:'b) <= dimindex(:'a) /\ w2w (word_H: 'b word) <=+ w then
1156 word_H
1157 else
1158 w2w w
1159Proof
1160 Cases
1161 \\ SIMP_TAC (srw_ss()++ARITH_ss) [word_H_def, w2w_def, word_ls_n2w,
1162 wordsTheory.INT_MAX_def, wordsTheory.INT_MIN_LT_DIMWORD,
1163 INT_MAX_def, INT_MIN_def, saturate_w2sw_def, saturate_i2sw_def, i2w_def]
1164 \\ SIMP_TAC (std_ss++INT_ARITH_ss) []
1165 \\ `INT_MIN (:'b) < dimword (:'b)`
1166 by METIS_TAC [arithmeticTheory.LESS_EQ_LESS_TRANS, BOUND_ORDER]
1167 \\ Cases_on `dimindex (:'b) <= dimindex (:'a)`
1168 \\ IMP_RES_TAC wordsTheory.dimindex_dimword_le_iso
1169 \\ ASM_SIMP_TAC (srw_ss()++ARITH_ss)
1170 [ARITH_PROVE ``&m - 1i <= &n = m <= n + 1n``]
1171 \\ Cases_on `n = INT_MIN (:'b) - 1`
1172 \\ ASM_SIMP_TAC arith_ss []
1173 \\ `~(INT_MIN (:'b) <= n + 1)`
1174 by (
1175 `dimword(:'a) <= INT_MIN (:'b)`
1176 by SRW_TAC [ARITH_ss] [dimword_def, wordsTheory.INT_MIN_def]
1177 \\ ASM_SIMP_TAC arith_ss [NOT_LESS_EQUAL, wordsTheory.ZERO_LT_INT_MIN]
1178 )
1179 \\ ASM_REWRITE_TAC []
1180QED
1181
1182Theorem saturate_i2sw:
1183 !i. saturate_i2w i = if i < 0 then 0w else saturate_n2w (Num i)
1184Proof
1185 Cases
1186 \\ ASM_SIMP_TAC (arith_ss++INT_ARITH_ss)
1187 [integerTheory.INT_LE, integerTheory.NUM_OF_INT,
1188 wordsTheory.ZERO_LT_dimword, ZERO_LT_UINT_MAX,
1189 saturate_i2w_def, saturate_n2w_def, UINT_MAX,
1190 DECIDE ``0n < n ==> n <> 0``]
1191 \\ ASM_SIMP_TAC std_ss
1192 [intLib.ARITH_PROVE ``n <> 0n ==> -&n < 0``,
1193 intLib.ARITH_PROVE ``n <> 0n ==> ~(&m <= -&n)``]
1194 \\ Cases_on `n = UINT_MAX (:'a)`
1195 \\ ASM_SIMP_TAC arith_ss [BOUND_ORDER, word_T_def]
1196 \\ `UINT_MAX (:'a) <= n /\ n <> UINT_MAX (:'a) = dimword (:'a) <= n`
1197 by SIMP_TAC (srw_ss()) [wordsTheory.UINT_MAX_def,
1198 DECIDE ``0n < m ==> (m <= 1 + n /\ n <> m - 1 = m <= n)``]
1199 \\ METIS_TAC []
1200QED
1201
1202Theorem saturate_sw2w:
1203 !w: 'a word.
1204 saturate_sw2w w : 'b word =
1205 if w < 0w then
1206 0w
1207 else
1208 saturate_w2w w
1209Proof
1210 STRIP_TAC
1211 \\ SIMP_TAC arith_ss
1212 [w2i_lt_0, saturate_w2w, saturate_sw2w_def, saturate_i2sw]
1213 \\ Cases_on `w < 0w : 'a word`
1214 \\ ASM_SIMP_TAC std_ss []
1215 \\ Cases_on `w`
1216 \\ FULL_SIMP_TAC arith_ss [w2i_n2w_pos, wordsTheory.w2n_n2w, saturate_n2w_def,
1217 WORD_NOT_LESS, wordsTheory.WORD_ZERO_LE, GSYM MOD_DIMINDEX, w2w_n2w,
1218 integerTheory.NUM_OF_INT]
1219 \\ Cases_on `dimindex (:'b) <= dimindex (:'a)`
1220 \\ ASM_SIMP_TAC arith_ss []
1221 THENL [
1222 `UINT_MAX (:'b) < dimword (:'b)` by METIS_TAC [BOUND_ORDER]
1223 \\ IMP_RES_TAC wordsTheory.dimindex_dimword_le_iso
1224 \\ `UINT_MAX (:'b) < dimword (:'a)` by DECIDE_TAC
1225 \\ ASM_SIMP_TAC arith_ss
1226 [w2w_n2w, word_T_def, word_ls_n2w, GSYM MOD_DIMINDEX]
1227 \\ Cases_on `n < UINT_MAX (:'b)`
1228 \\ FULL_SIMP_TAC arith_ss [NOT_LESS]
1229 \\ Cases_on `n = UINT_MAX (:'b)`
1230 \\ ASM_SIMP_TAC arith_ss []
1231 \\ `dimword (:'b) <= n` by FULL_SIMP_TAC arith_ss [wordsTheory.UINT_MAX_def]
1232 \\ ASM_REWRITE_TAC [],
1233 FULL_SIMP_TAC arith_ss [NOT_LESS_EQUAL, wordsTheory.dimindex_dimword_lt_iso]
1234 ]
1235QED
1236
1237Theorem saturate_sw2sw:
1238 !w: 'a word.
1239 saturate_sw2sw w : 'b word =
1240 if dimindex(:'a) <= dimindex(:'b) then
1241 sw2sw w
1242 else if sw2sw (word_H: 'b word) <= w then
1243 word_H
1244 else if w <= sw2sw (word_L: 'b word) then
1245 word_L
1246 else
1247 w2w w
1248Proof
1249 STRIP_TAC \\ Cases_on_i2w `w:'a word`
1250 \\ ASM_SIMP_TAC std_ss [saturate_sw2sw_def, saturate_i2sw_def, w2i_i2w]
1251 \\ Cases_on `dimindex (:'a) <= dimindex (:'b)`
1252 \\ IMP_RES_TAC INT_MAX_MONOTONIC
1253 \\ IMP_RES_TAC INT_MIN_MONOTONIC
1254 \\ ASM_SIMP_TAC arith_ss [sw2sw_i2w, w2w_i2w]
1255 THENL [
1256 SRW_TAC [] [word_H_def, word_L_def]
1257 THENL [
1258 `i <= INT_MAX (:'b)` by intLib.ARITH_TAC
1259 \\ `i = INT_MAX (:'b)` by FULL_SIMP_TAC (srw_ss()++INT_ARITH_ss) []
1260 \\ ASM_SIMP_TAC (srw_ss()) [i2w_def],
1261 `INT_MIN (:'b) <= i` by intLib.ARITH_TAC
1262 \\ `i = INT_MIN (:'b)` by FULL_SIMP_TAC (srw_ss()++INT_ARITH_ss) []
1263 \\ ASM_SIMP_TAC (srw_ss()) [i2w_def, DECIDE ``0n < n ==> (n <> 0)``]
1264 \\ SIMP_TAC std_ss [GSYM word_L_def, wordsTheory.WORD_NEG_L]
1265 ],
1266 FULL_SIMP_TAC std_ss [NOT_LESS_EQUAL]
1267 \\ `n2w (INT_MAX (:'b)) : 'b word = i2w (&INT_MAX (:'b))`
1268 by SRW_TAC [] [i2w_def]
1269 \\ `n2w (INT_MIN (:'b)) : 'b word = i2w (-&INT_MIN (:'b))`
1270 by (SRW_TAC [ARITH_ss] [i2w_def]
1271 THEN1 SIMP_TAC std_ss [GSYM word_L_def, wordsTheory.WORD_NEG_L]
1272 \\ FULL_SIMP_TAC (srw_ss()) [])
1273 \\ `INT_MIN (:'b) <= &(INT_MAX (:'b) : num) /\
1274 &(INT_MAX (:'b) : num) <= INT_MAX (:'b)`
1275 by SRW_TAC [INT_ARITH_ss] []
1276 \\ `INT_MIN (:'b) <= -&(INT_MIN (:'b) : num) /\
1277 -&(INT_MIN (:'b) : num) <= INT_MAX (:'b)`
1278 by SRW_TAC [INT_ARITH_ss] []
1279 \\ `INT_MAX (:'b) < INT_MAX (:'a) : int /\
1280 INT_MIN (:'a) < INT_MIN (:'b) : int`
1281 by SRW_TAC [] [GSYM dimindex_int_max_lt_iso, GSYM dimindex_int_min_lt_iso]
1282 \\ `INT_MIN (:'a) <= &(INT_MAX (:'b) : num) /\
1283 &(INT_MAX (:'b) : num) <= INT_MAX (:'a)`
1284 by intLib.ARITH_TAC
1285 \\ `INT_MIN (:'a) <= -&(INT_MIN (:'b) : num) /\
1286 -&(INT_MIN (:'b) : num) <= INT_MAX (:'a)`
1287 by intLib.ARITH_TAC
1288 \\ ASM_SIMP_TAC arith_ss
1289 [word_H_def, word_L_def, sw2sw_i2w, WORD_LEi, w2i_i2w]
1290 \\ SIMP_TAC (srw_ss()) []
1291 ]
1292QED
1293
1294(* ------------------------------------------------------------------------- *)
1295
1296Theorem signed_saturate_sub:
1297 !a b:'a word.
1298 signed_saturate_sub a b =
1299 if b = INT_MINw then
1300 if 0w <= a then
1301 INT_MAXw
1302 else
1303 a + INT_MINw
1304 else if dimindex(:'a) = 1 then
1305 a && ~b
1306 else
1307 signed_saturate_add a (-b)
1308Proof
1309 srw_tac [] [signed_saturate_add_def, signed_saturate_sub_def]
1310 \\ rule_assum_tac
1311 (REWRITE_RULE [GSYM w2i_11, word_0_w2i, WORD_LEi, w2i_INT_MINw])
1312 THENL [
1313 (* Case 1 *)
1314 Cases_on_i2w `a:'a word`
1315 \\ srw_tac [ARITH_ss] [w2i_i2w, saturate_i2sw_def, w2i_INT_MINw]
1316 \\ full_simp_tac (srw_ss())
1317 [w2i_i2w, integerTheory.INT_NOT_LE, wordsTheory.INT_MAX_def,
1318 int_arithTheory.INT_NUM_SUB, DECIDE ``0n < n ==> ~(n < 1)``,
1319 intLib.ARITH_PROVE ``i + &n < &n - 1 = i < -1i``,
1320 wordsTheory.ZERO_LT_INT_MIN,
1321 intLib.ARITH_PROVE ``i < -1i ==> ~(0 <= i)``,
1322 intLib.ARITH_PROVE ``0n < n /\ i + &n <= -&n ==> ~(-&n <= i : int)``],
1323 (* Case 2 *)
1324 Cases_on_i2w `a:'a word`
1325 \\ srw_tac [ARITH_ss] [w2i_i2w, saturate_i2sw_def, w2i_INT_MINw]
1326 \\ full_simp_tac (srw_ss())
1327 [w2i_i2w, integerTheory.INT_NOT_LE, wordsTheory.INT_MAX_def,
1328 int_arithTheory.INT_NUM_SUB, DECIDE ``0n < n ==> ~(n < 1)``]
1329 THENL [
1330 `i = -1i` by intLib.ARITH_TAC \\ asm_rewrite_tac [i2w_minus_1],
1331 spose_not_then (K ALL_TAC) \\ intLib.ARITH_TAC,
1332 srw_tac [] [GSYM word_i2w_add,
1333 wordsLib.WORD_ARITH_PROVE ``(a + b = c + a) = (b = c : 'a word)``]
1334 \\ once_rewrite_tac [GSYM wordsTheory.WORD_NEG_L]
1335 \\ rewrite_tac
1336 [wordsLib.WORD_ARITH_PROVE ``(a = -b : 'a word) = (-1w * a = b)``,
1337 MULT_MINUS_ONE, GSYM INT_MIN, i2w_INT_MIN]
1338 ],
1339 (* Case 3 *)
1340 imp_res_tac dimindex_1_cases
1341 \\ pop_assum (fn th => assume_tac (Q.SPEC `a:'a word` th) \\
1342 assume_tac (Q.SPEC `b:'a word` th))
1343 \\ full_simp_tac (srw_ss())
1344 [saturate_i2sw_0, word_0_w2i, w2i_1, w2i_minus_1]
1345 \\ srw_tac []
1346 [saturate_i2sw_def, word_L_def, wordsTheory.INT_MIN_def, i2w_def]
1347 \\ pop_assum mp_tac
1348 \\ srw_tac [] [wordsTheory.INT_MAX_def, wordsTheory.INT_MIN_def],
1349 (* Case 4 *)
1350 `1 < dimindex(:'a)` by srw_tac [] [DECIDE ``0n < n /\ n <> 1 ==> (1 < n)``]
1351 \\ imp_res_tac (REWRITE_RULE [w2i_INT_MINw] (REWRITE_RULE[GSYM w2i_11]w2i_neg))
1352 \\ fs[GSYM integerTheory.int_sub]
1353 ]
1354QED
1355
1356Theorem add_min_overflow[local]:
1357 !i j.
1358 i + j < INT_MIN (:'a) /\
1359 INT_MIN (:'a) <= i /\ i < 0 /\
1360 INT_MIN (:'a) <= j /\ j <= INT_MAX (:'a) ==>
1361 0 <= w2i (i2w (i + j) : 'a word)
1362Proof
1363 srw_tac [] [w2i_def, WORD_MSB_INT_MIN_LS]
1364 \\ spose_not_then kall_tac
1365 \\ `i + j < 0` by intLib.ARITH_TAC
1366 \\ `2i * -&INT_MIN (:'a) <= i + j` by intLib.ARITH_TAC
1367 \\ rule_assum_tac
1368 (ONCE_REWRITE_RULE [intLib.ARITH_PROVE ``-x <= y = -y <= x : int``] o
1369 REWRITE_RULE [GSYM dimword_IS_TWICE_INT_MIN,
1370 intLib.ARITH_PROVE ``2i * -&n = -&(2n * n)``])
1371 \\ `Num (-(i + j)) <= dimword (:'a)` by intLib.ARITH_TAC
1372 \\ fsrw_tac [ARITH_ss]
1373 [INT_MIN_LT_DIMWORD, i2w_def, word_2comp_n2w, word_L_def, word_ls_n2w]
1374 \\ Cases_on `Num (-(i + j)) = dimword (:'a)`
1375 >- fsrw_tac [ARITH_ss] [DECIDE ``0 < n ==> n <> 0n``]
1376 \\ `Num (-(i + j)) < dimword (:'a)` by DECIDE_TAC
1377 \\ `INT_MIN (:'a) < Num (-(i + j))` by intLib.ARITH_TAC
1378 \\ fsrw_tac [ARITH_ss] [dimword_IS_TWICE_INT_MIN]
1379QED
1380
1381Theorem add_max_overflow[local]:
1382 !i j.
1383 INT_MAX (:'a) < i + j /\
1384 0 <= i /\ i <= INT_MAX (:'a) /\
1385 INT_MIN (:'a) <= j /\ j <= INT_MAX (:'a) ==>
1386 w2i (i2w (i + j) : 'a word) < 0
1387Proof
1388 srw_tac [] [] \\ srw_tac [] [w2i_def, WORD_MSB_INT_MIN_LS]
1389 >| [
1390 spose_not_then strip_assume_tac
1391 \\ fsrw_tac []
1392 [REWRITE_RULE [GSYM wordsTheory.WORD_NOT_LOWER_EQUAL]
1393 wordsTheory.ZERO_LO_INT_MIN],
1394 pop_assum mp_tac \\ rewrite_tac []
1395 \\ `~(i + j < 0)` by intLib.ARITH_TAC
1396 \\ `i + j <= 2 * &INT_MAX (:'a)` by intLib.ARITH_TAC
1397 \\ `2 * &INT_MAX (:'a) < &dimword (:'a)`
1398 by srw_tac [] [dimword_IS_TWICE_INT_MIN, wordsTheory.INT_MAX_def]
1399 \\ `Num (i + j) < dimword (:'a)` by intLib.ARITH_TAC
1400 \\ fsrw_tac [ARITH_ss] [wordsTheory.INT_MIN_LT_DIMWORD,
1401 i2w_def, word_L_def, wordsTheory.word_ls_n2w]
1402 \\ fsrw_tac [ARITH_ss]
1403 [wordsTheory.INT_MAX_def,
1404 intLib.ARITH_PROVE ``~(y < 0i) ==> (&x < y = x < Num y)``]
1405 ]
1406QED
1407
1408val srw_add_min_overflow = SIMP_RULE (srw_ss()) [] add_min_overflow
1409val srw_add_max_overflow = SIMP_RULE (srw_ss()) [] add_max_overflow
1410
1411Theorem signed_saturate_add:
1412 !a b:'a word.
1413 signed_saturate_add a b =
1414 let sum = a + b and msba = word_msb a in
1415 if (msba = word_msb b) /\ (msba <> word_msb sum) then
1416 if msba then INT_MINw else INT_MAXw
1417 else
1418 sum
1419Proof
1420 ntac 2 strip_tac
1421 \\ Cases_on_i2w `a : 'a word`
1422 \\ Cases_on_i2w `b : 'a word`
1423 \\ fsrw_tac [boolSimps.LET_ss] [w2i_i2w, word_i2w_add,
1424 wordsTheory.word_msb_neg, signed_saturate_add_def,
1425 integerTheory.INT_NOT_LT, WORD_LEi, WORD_LTi, word_0_w2i]
1426 \\ srw_tac [] []
1427 >| [
1428 (* Case 1 *)
1429 `i < 0i` by metis_tac []
1430 \\ `i + i' < INT_MAX (:'a)`
1431 by srw_tac [intLib.INT_ARITH_ss] [INT_ZERO_LE_INT_MAX]
1432 \\ `i + i' <= INT_MAX (:'a)` by intLib.ARITH_TAC
1433 \\ `i + i' < INT_MIN (:'a)`
1434 by (spose_not_then
1435 (assume_tac o SIMP_RULE std_ss [integerTheory.INT_NOT_LT])
1436 \\ full_simp_tac std_ss [w2i_i2w]
1437 \\ intLib.ARITH_TAC)
1438 \\ fsrw_tac [intLib.INT_ARITH_ss] [saturate_i2sw_def],
1439 (* Case 2 *)
1440 `~(i < 0i)` by metis_tac []
1441 \\ fsrw_tac [intLib.INT_ARITH_ss] [integerTheory.INT_NOT_LT]
1442 \\ `INT_MIN (:'a) <= i + i'` by srw_tac [intLib.INT_ARITH_ss] []
1443 \\ `INT_MAX (:'a) < i + i'`
1444 by (spose_not_then
1445 (assume_tac o SIMP_RULE std_ss [integerTheory.INT_NOT_LT])
1446 \\ full_simp_tac std_ss [w2i_i2w]
1447 \\ intLib.ARITH_TAC)
1448 \\ asm_simp_tac std_ss [integerTheory.INT_LT_IMP_LE, saturate_i2sw_def]
1449 \\ srw_tac [] [],
1450 (* Case 3 *)
1451 `~(INT_MAX (:'a) < i + i') /\ ~(i + i' < INT_MIN (:'a))`
1452 by (fsrw_tac [intLib.INT_ARITH_ss] [integerTheory.INT_NOT_LT]
1453 \\ Cases_on `i < 0i`
1454 \\ fsrw_tac [intLib.INT_ARITH_ss] [integerTheory.INT_NOT_LT]
1455 \\ spose_not_then (assume_tac o
1456 SIMP_RULE(srw_ss()) [integerTheory.INT_NOT_LE]) >>
1457 (drule_all srw_add_min_overflow ORELSE drule_all srw_add_max_overflow)>>
1458 simp[integerTheory.INT_NOT_LE, integerTheory.INT_NOT_LT] >>
1459 first_x_assum irule >> srw_tac[intLib.INT_ARITH_ss][])
1460 \\ simp_tac std_ss [saturate_i2sw_def]
1461 \\ Cases_on `INT_MAX (:'a) = i + i'`
1462 \\ full_simp_tac std_ss [integerTheory.INT_LE_REFL, GSYM i2w_INT_MAX]
1463 \\ `~(INT_MAX (:'a) <= i + i')` by intLib.ARITH_TAC
1464 \\ asm_rewrite_tac []
1465 \\ Cases_on `i + i' = INT_MIN (:'a)`
1466 \\ full_simp_tac std_ss [integerTheory.INT_LE_REFL, GSYM i2w_INT_MIN]
1467 \\ `~(i + i' <= INT_MIN (:'a))` by intLib.ARITH_TAC
1468 \\ asm_rewrite_tac []
1469 ]
1470QED
1471
1472(* ------------------------------------------------------------------------- *)
1473
1474Theorem different_sign_then_no_overflow:
1475 !x y. word_msb x <> word_msb y ==> (w2i (x + y) = w2i x + w2i y)
1476Proof
1477 rw [GSYM word_add_i2w, wordsTheory.word_msb_neg, GSYM w2i_lt_0]
1478 \\ match_mp_tac w2i_i2w
1479 \\ qspec_then `x` assume_tac w2i_ge
1480 \\ qspec_then `x` assume_tac w2i_le
1481 \\ qspec_then `y` assume_tac w2i_ge
1482 \\ qspec_then `y` assume_tac w2i_le
1483 \\ intLib.ARITH_TAC
1484QED
1485
1486Theorem w2i_i2w_pos:
1487 !n. n <= INT_MAX (:'a) ==> (w2i (i2w (&n) : 'a word) = &n)
1488Proof
1489 ntac 2 strip_tac \\ match_mp_tac w2i_i2w
1490 \\ fsrw_tac [intLib.INT_ARITH_ss] []
1491QED
1492
1493Theorem w2i_i2w_neg:
1494 !n. n <= INT_MIN (:'a) ==> (w2i (i2w (-&n) : 'a word) = -&n)
1495Proof
1496 ntac 2 strip_tac \\ match_mp_tac w2i_i2w
1497 \\ fsrw_tac [intLib.INT_ARITH_ss] []
1498QED
1499
1500Theorem lem_pos[local]:
1501 !n:num. n <= INT_MAX (:'a) ==> ~(INT_MIN (:'a) <= n)
1502Proof
1503 lrw [wordsTheory.BOUND_ORDER, arithmeticTheory.NOT_LESS_EQUAL]
1504QED
1505
1506Theorem lem_neg[local]:
1507 !n. n <> 0n /\ n <= INT_MIN (:'a) ==>
1508 &INT_MIN (:'a) <= (&dimword (:'a) - &n) % &dimword (:'a)
1509Proof
1510 REPEAT strip_tac
1511 \\ `&n:int < &dimword (:'a)` by lrw [wordsTheory.BOUND_ORDER]
1512 \\ `0i <= &dimword (:'a) - &n /\ &dimword (:'a) - &n < &dimword (:'a) : int`
1513 by intLib.ARITH_TAC
1514 \\ lfs [integerTheory.INT_LESS_MOD, integerTheory.INT_SUB,
1515 wordsTheory.dimword_IS_TWICE_INT_MIN]
1516QED
1517
1518Theorem lem[local]:
1519 !n. &INT_MIN (:'a) <= &dimword (:'a) - &n : int = n <= INT_MIN (:'a)
1520Proof
1521 srw_tac [intLib.INT_ARITH_ss]
1522 [intLib.ARITH_PROVE ``a <= b - c = c <= b - a : int``,
1523 intLib.ARITH_PROVE ``&(2n * a) - &a = &a : int``,
1524 wordsTheory.dimword_IS_TWICE_INT_MIN]
1525QED
1526
1527Theorem overflow:
1528 !x y. w2i (x + y) <> w2i x + w2i y =
1529 ((word_msb x = word_msb y) /\ word_msb x <> word_msb (x + y))
1530Proof
1531 ntac 2 strip_tac
1532 \\ Cases_on `word_msb x = word_msb y`
1533 \\ simp [different_sign_then_no_overflow]
1534 \\ Cases_on_i2w `x`
1535 \\ Cases_on_i2w `y`
1536 \\ fs [w2i_i2w, word_i2w_add, word_msb_i2w]
1537 \\ `i < &dimword (:'a) /\ i' < &dimword (:'a)`
1538 by (ASSUME_TAC wordsTheory.INT_MAX_LT_DIMWORD \\ intLib.ARITH_TAC)
1539 \\ `&dimword (:'a) <> 0i /\ INT_MIN (:'a) <> 0n`
1540 by lfs [DECIDE ``0 < n ==> n <> 0n``]
1541 \\ Cases_on `i`
1542 \\ Cases_on `i'`
1543 \\ fsrw_tac [intLib.INT_ARITH_ss]
1544 [integerTheory.INT_MOD_NEG_NUMERATOR, integerTheory.INT_LESS_MOD,
1545 i2w_0, word_0_w2i, arithmeticTheory.NOT_LESS_EQUAL,
1546 w2i_i2w_pos, w2i_i2w_neg, lem_pos, lem_neg]
1547 \\ `&n + &n' <> 0i` by intLib.ARITH_TAC
1548 >- (`&n + &n' < &dimword (:'a) : int`
1549 by (lrw [integerTheory.INT_ADD, wordsTheory.dimword_IS_TWICE_INT_MIN]
1550 \\ metis_tac [wordsTheory.BOUND_ORDER,
1551 DECIDE ``a <= n /\ b <= n /\ n < m ==> a + b < 2n * m``])
1552 \\ lrw [integerTheory.INT_LESS_MOD, integerTheory.INT_ADD,
1553 arithmeticTheory.NOT_LESS_EQUAL]
1554 \\ Cases_on `n + n' <= INT_MAX (:'a)` \\ simp [w2i_i2w_pos]
1555 >- metis_tac [arithmeticTheory.LESS_EQ_LESS_TRANS, wordsTheory.BOUND_ORDER]
1556 \\ `INT_MIN (:'a) <= n + n'`
1557 by lfs [arithmeticTheory.NOT_LESS_EQUAL, wordsTheory.INT_MAX_def]
1558 \\ simp [i2w_def]
1559 \\ lfs [integerTheory.INT_ADD, w2i_def, wordsTheory.word_msb_n2w_numeric])
1560 \\ Cases_on `n + n' = dimword (:'a)`
1561 \\ simp [integerTheory.INT_ADD_CALCULATE, integerTheory.INT_MOD_NEG_NUMERATOR]
1562 >- lrw [word_0_w2i, i2w_def, n2w_dimword]
1563 \\ `&dimword (:'a) - &(n + n') < &dimword (:'a) : int` by intLib.ARITH_TAC
1564 \\ `&(n + n') < &dimword (:'a) : int`
1565 by lrw [integerTheory.INT_ADD, wordsTheory.dimword_IS_TWICE_INT_MIN]
1566 \\ `0i <= &dimword (:'a) - &(n + n')` by intLib.ARITH_TAC
1567 \\ lrw [integerTheory.INT_ADD_CALCULATE, integerTheory.INT_MOD_NEG_NUMERATOR,
1568 integerTheory.INT_LESS_MOD, lem]
1569 \\ Cases_on `n + n' <= INT_MIN (:'a)`
1570 \\ simp [w2i_i2w_neg]
1571 \\ `INT_MIN (:'a) < n + n'` by intLib.ARITH_TAC
1572 \\ lfs [i2w_def, wordsTheory.word_2comp_n2w]
1573 \\ imp_res_tac arithmeticTheory.LESS_ADD
1574 \\ `p' < INT_MIN (:'a)` by lrw [wordsTheory.dimword_IS_TWICE_INT_MIN]
1575 \\ qpat_x_assum `a + b = dimword(:'a)` (SUBST1_TAC o SYM)
1576 \\ lrw [w2i_def, wordsTheory.word_msb_n2w_numeric]
1577QED
1578
1579Theorem sub_overflow:
1580 !x y : 'a word.
1581 (w2i (x - y) <> w2i x - w2i y) =
1582 ((word_msb x <> word_msb y) /\ word_msb x <> word_msb (x - y))
1583Proof
1584 REPEAT strip_tac
1585 \\ Cases_on `y = 0w`
1586 >- simp [word_0_w2i]
1587 \\ Cases_on `y = INT_MINw`
1588 >- (
1589 assume_tac wordsTheory.word_msb_add_word_L
1590 \\ `!a: 'a word. a - INT_MINw = a + INT_MINw`
1591 by simp_tac std_ss [wordsTheory.word_sub_def, wordsTheory.WORD_NEG_L]
1592 \\ asm_simp_tac std_ss
1593 [wordsTheory.WORD_L_NEG, DECIDE ``a <> ~(a : bool)``]
1594 \\ rw_tac std_ss
1595 [w2i_def, wordsTheory.WORD_L_NEG,
1596 wordsTheory.WORD_NEG_L, integerTheory.INT_SUB_RNEG,
1597 wordsTheory.WORD_NEG_SUB, integerTheory.INT_ADD,
1598 intLib.ARITH_PROVE ``(i = -j + x : int) = (i + j = x)``,
1599 intLib.ARITH_PROVE ``(-i = j : int) = (i + j = 0)``]
1600 \\ full_simp_tac intSimps.int_ss [wordsTheory.w2n_eq_0]
1601 \\ Cases_on `x = 0w`
1602 \\ asm_simp_tac std_ss
1603 [wordsTheory.WORD_NEG_0, wordsTheory.WORD_ADD_0,
1604 wordsTheory.word_0_n2w]
1605 \\ Cases_on `x = INT_MINw`
1606 >- (`INT_MINw + INT_MINw = 0w : 'a word`
1607 by metis_tac [wordsTheory.WORD_SUM_ZERO, wordsTheory.WORD_NEG_L]
1608 \\ asm_simp_tac std_ss
1609 [wordsTheory.WORD_NEG_L, wordsTheory.word_0_n2w])
1610 \\ `~word_msb (-x) /\ ~word_msb (x + INT_MINw)`
1611 by metis_tac [wordsTheory.TWO_COMP_POS_NEG]
1612 \\ metis_tac [wordsTheory.w2n_add, wordsTheory.WORD_ADD_LINV,
1613 wordsTheory.WORD_ADD_0, wordsTheory.WORD_ADD_ASSOC]
1614 )
1615 \\ metis_tac
1616 [overflow
1617 |> Q.SPECL [`x`, `-y`]
1618 |> Q.DISCH `y <> 0w /\ y <> INT_MINw`
1619 |> SIMP_RULE arith_ss
1620 [GSYM wordsTheory.word_sub_def, w2i_neg,
1621 GSYM integerTheory.int_sub, GSYM wordsTheory.TWO_COMP_POS_NEG]]
1622QED
1623
1624Theorem n2w_add_dimword[local]:
1625 !n. n2w (dimword(:'a) + n) = n2w n : 'a word
1626Proof
1627 simp []
1628QED
1629
1630Theorem overflow_add:
1631 !x y. w2i (x + y) <> w2i x + w2i y = OVERFLOW x y F
1632Proof
1633 simp [overflow, wordsTheory.add_with_carry_def, GSYM wordsTheory.word_add_def]
1634QED
1635
1636Theorem overflow_sub:
1637 !x y. w2i (x - y) <> w2i x - w2i y = OVERFLOW x (~y) T
1638Proof
1639 rw [sub_overflow, wordsTheory.add_with_carry_def, wordsTheory.WORD_MSB_1COMP]
1640 \\ Cases_on `word_msb x`
1641 \\ Cases_on `word_msb y`
1642 \\ rw [wordsTheory.w2n_plus1, GSYM wordsTheory.word_add_def, n2w_add_dimword,
1643 METIS_PROVE [wordsTheory.WORD_NEG_1, wordsTheory.WORD_NOT_T,
1644 wordsTheory.WORD_NOT_NOT] ``(~y = -1w) = (y = 0w)``]
1645 \\ simp [wordsTheory.WORD_NOT]
1646QED
1647
1648(* ------------------------------------------------------------------------- *)
1649
1650Theorem i2w_w2n_w2w[simp]:
1651 !w : 'a word. i2w (&w2n w) = w2w w : 'b word
1652Proof
1653 fs [i2w_def, wordsTheory.w2w_def]
1654QED
1655
1656Theorem i2w_w2n:
1657 i2w (&w2n w) = w
1658Proof
1659 fs [i2w_def]
1660QED
1661
1662Theorem w2n_i2w:
1663 &w2n ((i2w n):'a word) = n % (& dimword (:'a))
1664Proof
1665 fs [i2w_def] \\ Cases_on `n` \\ fs []
1666 \\ `dimword (:'a) <> 0` by (assume_tac ZERO_LT_dimword \\ decide_tac)
1667 \\ imp_res_tac integerTheory.INT_MOD \\ fs []
1668 \\ fs [word_2comp_n2w]
1669 \\ fs [INT_MOD_NEG_NUMERATOR]
1670 \\ `&dimword (:'a) <> 0i` by fs []
1671 \\ imp_res_tac (UNDISCH INT_MOD_SUB |> GSYM |> DISCH_ALL)
1672 \\ pop_assum (fn th => once_rewrite_tac [th]) \\ fs []
1673 \\ fs [INT_MOD_NEG_NUMERATOR]
1674 \\ rename1 `k <> 0n` \\ pop_assum mp_tac
1675 \\ rename1 `n <> 0n` \\ pop_assum mp_tac \\ rw []
1676 \\ `n MOD k < k` by fs [MOD_LESS]
1677 \\ `n MOD k <= k` by fs []
1678 \\ fs [INT_SUB]
1679QED
1680
1681Theorem w2i_eq_w2n:
1682 w2i (w:'a word) =
1683 if w2n w < INT_MIN (:'a) then & (w2n w) else & (w2n w) - & dimword (:'a)
1684Proof
1685 Cases_on `w` \\ rw [w2i_n2w_pos]
1686 \\ fs [NOT_LESS] \\ fs [w2i_n2w_neg]
1687 \\ `n <= dimword (:'a)` by decide_tac
1688 \\ imp_res_tac (GSYM INT_SUB) \\ fs []
1689QED
1690