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