1(* ========================================================================= *) 2(* FILE : bitstringScript.sml *) 3(* DESCRIPTION : Boolean lists as Bitstrings *) 4(* AUTHOR : (c) Anthony Fox, University of Cambridge *) 5(* ========================================================================= *) 6 7open HolKernel boolLib bossLib 8open bitTheory wordsTheory fcpLib 9open wordsLib 10open numposrepTheory 11 12val _ = new_theory "bitstring" 13 14(* ------------------------------------------------------------------------- *) 15 16(* MSB is head of list, e.g. [T, F] represents 2 *) 17 18val _ = Parse.type_abbrev ("bitstring", ``:bool list``) 19 20val extend_def = Define` 21 (extend _ 0 l = l: bitstring) /\ 22 (extend c (SUC n) l = extend c n (c::l))` 23 24val boolify_def = Define` 25 (boolify a [] = a) /\ 26 (boolify a (n :: l) = boolify ((n <> 0)::a) l)` 27 28val bitify_def = Define` 29 (bitify a [] = a) /\ 30 (bitify a (F :: l) = bitify (0::a) l) /\ 31 (bitify a (T :: l) = bitify (1::a) l)` 32 33val n2v_def = Define` 34 n2v n = boolify [] (num_to_bin_list n)` 35 36val v2n_def = Define` 37 v2n l = num_from_bin_list (bitify [] l)` 38 39val s2v_def = Define` 40 s2v = MAP (\c. (c = #"1") \/ (c = #"T"))` 41 42val v2s_def = Define` 43 v2s = MAP (\b. if b then #"1" else #"0")` 44 45val zero_extend_def = zDefine` 46 zero_extend n v = PAD_LEFT F n v` 47 48val sign_extend_def = zDefine` 49 sign_extend n v = PAD_LEFT (HD v) n v` 50 51val fixwidth_def = zDefine` 52 fixwidth n v = 53 let l = LENGTH v in 54 if l < n then 55 zero_extend n v 56 else 57 DROP (l - n) v` 58 59val shiftl_def = Define` 60 shiftl v m = PAD_RIGHT F (LENGTH v + m) v` 61 62val shiftr_def = Define` 63 shiftr (v: bitstring) m = TAKE (LENGTH v - m) v` 64 65val field_def = Define` 66 field h l v = fixwidth (SUC h - l) (shiftr v l)` 67 68val rotate_def = Define` 69 rotate v m = 70 let l = LENGTH v in 71 let x = m MOD l 72 in 73 if (l = 0) \/ (x = 0) then v else field (x - 1) 0 v ++ field (l - 1) x v` 74 75val testbit_def = zDefine` 76 testbit b v = (field b b v = [T])` 77 78val w2v_def = Define` 79 w2v (w : 'a word) = 80 GENLIST (\i. w ' (dimindex(:'a) - 1 - i)) (dimindex(:'a))` 81 82val v2w_def = zDefine` 83 v2w v : 'a word = FCP i. testbit i v` 84 85val rev_count_list_def = Define` 86 rev_count_list n = GENLIST (\i. n - 1 - i) n` 87 88val modify_def = Define` 89 modify f (v : bitstring) = 90 MAP (UNCURRY f) (ZIP (rev_count_list (LENGTH v), v)) : bitstring` 91 92val field_insert_def = Define` 93 field_insert h l s = 94 modify (\i. COND (l <= i /\ i <= h) (testbit (i - l) s))` 95 96val add_def = Define` 97 add a b = 98 let m = MAX (LENGTH a) (LENGTH b) in 99 zero_extend m (n2v (v2n a + v2n b))` 100 101val bitwise_def = Define` 102 bitwise f v1 v2 = 103 let m = MAX (LENGTH v1) (LENGTH v2) in 104 MAP (UNCURRY f) (ZIP (fixwidth m v1, fixwidth m v2)) : bitstring` 105 106val bnot_def = Define `bnot = MAP (bool$~)` 107val bor_def = Define `bor = bitwise (\/)` 108val band_def = Define `band = bitwise (/\)` 109val bxor_def = Define `bxor = bitwise (<>)` 110 111val bnor_def = Define `bnor = bitwise (\x y. ~(x \/ y))` 112val bxnor_def = Define `bxnor = bitwise (=)` 113val bnand_def = Define `bnand = bitwise (\x y. ~(x /\ y))` 114 115val replicate_def = Define` 116 replicate v n = FLAT (GENLIST (K v) n) : bitstring` 117 118(* ------------------------------------------------------------------------- *) 119 120val wrw = srw_tac [boolSimps.LET_ss, fcpLib.FCP_ss, ARITH_ss] 121 122val extend_cons = Q.store_thm("extend_cons", 123 `!n c l. extend c (SUC n) l = c :: extend c n l`, 124 Induct \\ metis_tac [extend_def]) 125 126val pad_left_extend = Q.store_thm("pad_left_extend", 127 `!n l c. PAD_LEFT c n l = extend c (n - LENGTH l) l`, 128 ntac 2 strip_tac 129 \\ Cases_on `n <= LENGTH l` 130 >- lrw [listTheory.PAD_LEFT, DECIDE ``n <= l ==> (n - l = 0)``, 131 Thm.CONJUNCT1 extend_def] 132 \\ simp[listTheory.PAD_LEFT] 133 \\ Induct_on `n` \\ rw [] 134 \\ Cases_on `LENGTH l = n` 135 \\ lrw [bitTheory.SUC_SUB, 136 extend_cons |> Q.SPEC `0` 137 |> SIMP_RULE std_ss [Thm.CONJUNCT1 extend_def]] 138 \\ `SUC n - LENGTH l = SUC (n - LENGTH l)` by decide_tac 139 \\ simp [extend_cons, listTheory.GENLIST_CONS]) 140 141val extend = Q.store_thm("extend", 142 `(!n v. zero_extend n v = extend F (n - LENGTH v) v) /\ 143 (!n v. sign_extend n v = extend (HD v) (n - LENGTH v) v)`, 144 simp [zero_extend_def, sign_extend_def, pad_left_extend]) 145 146val fixwidth = Q.store_thm("fixwidth", 147 `!n v. 148 fixwidth n v = 149 let l = LENGTH v in 150 if l < n then 151 extend F (n - l) v 152 else 153 DROP (l - n) v`, 154 lrw [fixwidth_def, extend]) 155 156val fixwidth_id = Q.store_thm("fixwidth_id", 157 `!w. fixwidth (LENGTH w) w = w`, 158 lrw [fixwidth_def]) 159 160val fixwidth_id_imp = Theory.save_thm ("fixwidth_id_imp", 161 metisLib.METIS_PROVE [fixwidth_id] 162 ``!n w. (n = LENGTH w) ==> (fixwidth n w = w)``) 163 164val boolify_reverse_map = Q.store_thm("boolify_reverse_map", 165 `!v a. boolify a v = REVERSE (MAP (\n. n <> 0) v) ++ a`, 166 Induct \\ lrw [boolify_def]) 167 168val bitify_reverse_map = Q.store_thm("bitify_reverse_map", 169 `!v a. bitify a v = REVERSE (MAP (\b. if b then 1 else 0) v) ++ a`, 170 Induct \\ lrw [bitify_def]) 171 172val every_bit_bitify = Q.store_thm("every_bit_bitify", 173 `!v. EVERY ($> 2) (bitify [] v)`, 174 lrw [bitify_reverse_map, rich_listTheory.ALL_EL_REVERSE, 175 listTheory.EVERY_MAP] 176 \\ rw [listTheory.EVERY_EL] \\ rw []) 177 178val length_pad_left = Q.store_thm("length_pad_left", 179 `!x n a. LENGTH (PAD_LEFT x n a) = if LENGTH a < n then n else LENGTH a`, 180 lrw [listTheory.PAD_LEFT]) 181 182val length_pad_right = Q.store_thm("length_pad_right", 183 `!x n a. LENGTH (PAD_RIGHT x n a) = if LENGTH a < n then n else LENGTH a`, 184 lrw [listTheory.PAD_RIGHT]) 185 186val length_zero_extend = Q.store_thm("length_zero_extend", 187 `!n v. LENGTH v < n ==> (LENGTH (zero_extend n v) = n)`, 188 lrw [zero_extend_def, length_pad_left]) 189 190val length_sign_extend = Q.store_thm("length_sign_extend", 191 `!n v. LENGTH v < n ==> (LENGTH (sign_extend n v) = n)`, 192 lrw [sign_extend_def, length_pad_left]) 193 194val length_fixwidth = Q.store_thm("length_fixwidth", 195 `!n v. LENGTH (fixwidth n v) = n`, 196 lrw [fixwidth_def, length_zero_extend]) 197 198val length_field = Q.store_thm("length_field", 199 `!h l v. LENGTH (field h l v) = SUC h - l`, 200 rw [field_def, length_fixwidth]) 201 202val length_bitify = Q.store_thm("length_bitify", 203 `!v l. LENGTH (bitify l v) = LENGTH l + LENGTH v`, 204 lrw [bitify_reverse_map]) 205 206val length_bitify_null = Q.store_thm("length_bitify_null", 207 `!v l. LENGTH (bitify [] v) = LENGTH v`, 208 rw [length_bitify]) 209 210val length_shiftr = Q.store_thm("length_shiftr", 211 `!v n. LENGTH (shiftr v n) = LENGTH v - n`, 212 lrw [shiftr_def]) 213 214val length_rev_count_list = Q.store_thm("length_rev_count_list", 215 `!n. LENGTH (rev_count_list n) = n`, 216 Induct \\ lrw [rev_count_list_def]) 217 218val length_w2v = Q.store_thm("length_w2v", 219 `!w:'a word. LENGTH (w2v w) = dimindex(:'a)`, 220 lrw [w2v_def]) 221 222val length_rotate = Q.store_thm("length_rotate", 223 `!v n. LENGTH (rotate v n) = LENGTH v`, 224 simp [rotate_def, LET_THM] 225 \\ srw_tac[][length_field] 226 \\ full_simp_tac (std_ss++ARITH_ss) 227 [DECIDE ``n <> 0n ==> (SUC (n - 1) = n)``, 228 DECIDE ``n:num < l ==> (n + (l - n) = l)``, 229 GSYM listTheory.LENGTH_NIL, 230 arithmeticTheory.NOT_ZERO_LT_ZERO, 231 arithmeticTheory.MOD_LESS]) 232 233val el_rev_count_list = Q.store_thm("el_rev_count_list", 234 `!n i. i < n ==> (EL i (rev_count_list n) = n - 1 - i)`, 235 Induct \\ lrw [rev_count_list_def]) 236 237val el_bitify = Q.prove( 238 `!v i a. i < LENGTH v ==> 239 (EL (LENGTH v - (i + 1)) v = (EL i (bitify a v) = 1))`, 240 lrw [bitify_def, bitify_reverse_map, rich_listTheory.EL_APPEND1, 241 listTheory.EL_REVERSE, listTheory.EL_MAP, arithmeticTheory.PRE_SUB1]) 242 243val el_zero_extend = Q.store_thm("el_zero_extend", 244 `!n i v. EL i (zero_extend n v) = 245 n - LENGTH v <= i /\ EL (i - (n - LENGTH v)) v`, 246 lrw [zero_extend_def, listTheory.PAD_LEFT] 247 \\ Cases_on `i < n - LENGTH v` 248 \\ lrw [rich_listTheory.EL_APPEND1, rich_listTheory.EL_APPEND2]) 249 250val el_sign_extend = Q.store_thm("el_sign_extend", 251 `!n i v. EL i (sign_extend n v) = 252 if i < n - LENGTH v then 253 EL 0 v 254 else 255 EL (i - (n - LENGTH v)) v`, 256 lrw [sign_extend_def, listTheory.PAD_LEFT, 257 rich_listTheory.EL_APPEND1, rich_listTheory.EL_APPEND2]) 258 259val el_fixwidth = Q.store_thm("el_fixwidth", 260 `!i n w. i < n ==> 261 (EL i (fixwidth n w) = 262 if LENGTH w < n then 263 n - LENGTH w <= i /\ EL (i - (n - LENGTH w)) w 264 else 265 EL (i + (LENGTH w - n)) w)`, 266 lrw [fixwidth_def, el_zero_extend, rich_listTheory.EL_DROP]) 267 268val el_field = Q.store_thm("el_field", 269 `!v h l i. i < SUC h - l ==> 270 (EL i (field h l v) = 271 SUC h <= i + LENGTH v /\ EL (i + LENGTH v - SUC h) v)`, 272 lrw [field_def, shiftr_def, el_fixwidth, rich_listTheory.EL_TAKE] 273 \\ Cases_on `l < LENGTH v` \\ lrw [] 274 \\ `LENGTH v - SUC h < LENGTH v - l` by decide_tac 275 \\ lrw [rich_listTheory.EL_TAKE]) 276 277val shiftr_field = Q.prove( 278 `!n l v. LENGTH l <> 0 ==> (shiftr l n = field (LENGTH l - 1) n l)`, 279 rpt strip_tac 280 \\ `SUC (LENGTH l - 1) - n = LENGTH (shiftr l n)` 281 by (rw [length_shiftr] \\ decide_tac) 282 \\ lrw [field_def, fixwidth_id]) 283 284val el_w2v = Q.store_thm("el_w2v", 285 `!w: 'a word n. 286 n < dimindex (:'a) ==> (EL n (w2v w) = w ' (dimindex (:'a) - 1 - n))`, 287 lrw [w2v_def]) 288 289val el_shiftr = Q.store_thm("el_shiftr", 290 `!i v n d. 291 n < d /\ i < d - n /\ 0 < d ==> 292 (EL i (shiftr (fixwidth d v) n) = 293 d <= i + LENGTH v /\ EL (i + LENGTH v - d) v)`, 294 simp_tac(std_ss++ARITH_ss) 295 [shiftr_field, length_fixwidth, el_field, el_fixwidth, 296 arithmeticTheory.ADD1] \\ rw[]) 297 298val shiftr_0 = Q.store_thm("shiftr_0", `!v. shiftr v 0 = v`, lrw [shiftr_def]) 299 300val field_fixwidth = Q.store_thm("field_fixwidth", 301 `!h v. field h 0 v = fixwidth (SUC h) v`, 302 rw [field_def, shiftr_0]) 303 304val testbit = Q.store_thm("testbit", 305 `!b v. testbit b v = let n = LENGTH v in b < n /\ EL (n - 1 - b) v`, 306 lrw [zero_extend_def, testbit_def, field_def, fixwidth_def, shiftr_def, 307 listTheory.PAD_LEFT, arithmeticTheory.SUB_LEFT_SUB, bitTheory.SUC_SUB] 308 \\ Induct_on `v` 309 \\ lrw [listTheory.DROP_def] 310 \\ lfs [arithmeticTheory.NOT_LESS, arithmeticTheory.NOT_LESS_EQUAL, 311 arithmeticTheory.ADD1] 312 >- (`b = LENGTH v` by decide_tac \\ lrw []) 313 \\ imp_res_tac arithmeticTheory.LESS_ADD_1 314 \\ lfs [REWRITE_RULE [arithmeticTheory.ADD1] listTheory.EL_restricted]) 315 316val testbit_geq_len = Q.store_thm("testbit_geq_len", 317 `!v i. LENGTH v <= i ==> ~testbit i v`, 318 simp [testbit, LET_THM]) 319 320val testbit_el = Q.store_thm("testbit_el", 321 `!v i. i < LENGTH v ==> (testbit i v = EL (LENGTH v - 1 - i) v)`, 322 simp [testbit, LET_THM]) 323 324val bit_v2w = Q.store_thm("bit_v2w", 325 `!n v. word_bit n (v2w v : 'a word) = n < dimindex(:'a) /\ testbit n v`, 326 rw [v2w_def, wordsTheory.word_bit_def] 327 \\ Cases_on `n < dimindex(:'a)` 328 \\ wrw [] 329 \\ assume_tac wordsTheory.DIMINDEX_GT_0 330 \\ `~(n <= dimindex(:'a) - 1)` by decide_tac 331 \\ asm_rewrite_tac []) 332 333val word_index_v2w = Q.store_thm("word_index_v2w", 334 `!v i. (v2w v : 'a word) ' i = 335 if i < dimindex(:'a) then 336 testbit i v 337 else 338 FAIL $' ^(Term.mk_var ("index too large", Type.bool)) 339 (v2w v : 'a word) i`, 340 rw [wordsTheory.word_bit, bit_v2w, combinTheory.FAIL_THM]) 341 342val testbit_w2v = Q.store_thm("testbit_w2v", 343 `!n w. testbit n (w2v (w : 'a word)) = word_bit n w`, 344 lrw [w2v_def, testbit, wordsTheory.word_bit_def] 345 \\ Cases_on `n < dimindex(:'a)` 346 \\ lrw [] 347 \\ assume_tac wordsTheory.DIMINDEX_GT_0 348 \\ `~(n <= dimindex(:'a) - 1)` by decide_tac 349 \\ asm_rewrite_tac []) 350 351val word_bit_lem = 352 wordsTheory.word_bit 353 |> Q.SPECL [`w`, `dimindex(:'a) - 1 - i`] 354 |> SIMP_RULE arith_ss [wordsTheory.DIMINDEX_GT_0, 355 DECIDE ``0 < n ==> (0 < i + n)``] 356 |> GEN_ALL 357 358val w2v_v2w = Q.store_thm("w2v_v2w", 359 `!v. w2v (v2w v : 'a word) = fixwidth (dimindex(:'a)) v`, 360 lrw [w2v_def, bit_v2w, testbit, fixwidth_def, zero_extend_def, 361 listTheory.PAD_LEFT, listTheory.LIST_EQ_REWRITE, 362 rich_listTheory.EL_DROP, word_bit_lem] 363 \\ Cases_on `x < dimindex(:'a) - LENGTH v` 364 \\ lrw [rich_listTheory.EL_APPEND1, rich_listTheory.EL_APPEND2]) 365 366val v2w_w2v = Q.store_thm("v2w_w2v", 367 `!w. v2w (w2v w) = w`, 368 wrw [w2v_def, v2w_def, testbit]) 369 370val v2w_fixwidth = Q.store_thm("v2w_fixwidth", 371 `!v. v2w (fixwidth (dimindex(:'a)) v) = v2w v : 'a word`, 372 wrw [v2w_def, testbit, length_fixwidth, el_fixwidth] 373 \\ Cases_on `i < LENGTH v` 374 \\ lrw []) 375 376val fixwidth_fixwidth = Q.store_thm("fixwidth_fixwidth", 377 `!n v. fixwidth n (fixwidth n v) = fixwidth n v`, 378 lrw [fixwidth_def] \\ lfs [length_zero_extend]) 379 380val bitstring_nchotomy = Q.store_thm("bitstring_nchotomy", 381 `!w:'a word. ?v. (w = v2w v)`, metis_tac [v2w_w2v]) 382 383val ranged_bitstring_nchotomy = Q.store_thm("ranged_bitstring_nchotomy", 384 `!w:'a word. ?v. (w = v2w v) /\ (Abbrev (LENGTH v = dimindex(:'a)))`, 385 strip_tac 386 \\ qspec_then `w` STRUCT_CASES_TAC bitstring_nchotomy 387 \\ qexists_tac `fixwidth (dimindex(:'a)) v` 388 \\ rw [markerTheory.Abbrev_def, length_fixwidth, v2w_fixwidth]) 389 390val BACKWARD_LIST_EQ_REWRITE = Q.prove( 391 `!l1 l2. (l1 = l2) = 392 (LENGTH l1 = LENGTH l2) /\ 393 !x. x < LENGTH l1 ==> 394 (EL (LENGTH l1 - 1 - x) l1 = EL (LENGTH l1 - 1 - x) l2)`, 395 lrw [listTheory.LIST_EQ_REWRITE] 396 \\ eq_tac \\ lrw [] 397 \\ `LENGTH l1 - 1 - x < LENGTH l1` by decide_tac 398 \\ res_tac 399 \\ `x < LENGTH l1` by decide_tac 400 \\ lfs []) 401 402val fixwidth_eq = Q.store_thm("fixwidth_eq", 403 `!n v w. (fixwidth n v = fixwidth n w) = 404 (!i. i < n ==> (testbit i v = testbit i w))`, 405 lrw [el_fixwidth, testbit, length_fixwidth, BACKWARD_LIST_EQ_REWRITE] 406 \\ rpt BasicProvers.FULL_CASE_TAC 407 \\ lfs [DECIDE ``v < n ==> (n <= n + v - (i + 1) = i < v)``]) 408 409val v2w_11 = Q.store_thm("v2w_11", 410 `!v w. (v2w v = v2w w : 'a word) = 411 (fixwidth (dimindex(:'a)) v = fixwidth (dimindex(:'a)) w)`, 412 wrw [wordsTheory.word_bit, bit_v2w, fixwidth_eq]) 413 414(* ------------------------------------------------------------------------- *) 415 416val take_id_imp = 417 metisLib.METIS_PROVE [listTheory.TAKE_LENGTH_ID] 418 ``!n w: 'a list. (n = LENGTH w) ==> (TAKE n w = w)`` 419 420val field_concat_right = Q.store_thm("field_concat_right", 421 `!h a b. (LENGTH b = SUC h) ==> (field h 0 (a ++ b) = b)`, 422 lrw [field_def, shiftr_def, take_id_imp] 423 \\ lrw [fixwidth_def, rich_listTheory.DROP_LENGTH_APPEND]) 424 425val field_concat_left = Q.store_thm("field_concat_left", 426 `!h l a b. 427 l <= h /\ LENGTH b <= l ==> 428 (field h l (a ++ b) = field (h - LENGTH b) (l - LENGTH b) a)`, 429 srw_tac [][field_def, shiftr_def] 430 \\ imp_res_tac arithmeticTheory.LESS_EQUAL_ADD 431 \\ pop_assum kall_tac 432 \\ pop_assum SUBST_ALL_TAC 433 \\ lfs [listTheory.TAKE_APPEND1] 434 \\ simp [DECIDE ``p + l <= h ==> (SUC h - (p + l) = SUC (h - l) - p)``]) 435 436val field_id_imp = Q.store_thm("field_id_imp", 437 `!n v. (SUC n = LENGTH v) ==> (field n 0 v = v)`, 438 metis_tac [fixwidth_id_imp, field_fixwidth]) 439 440(* ------------------------------------------------------------------------- *) 441 442val shiftl_replicate_F = Q.store_thm("shiftl_replicate_F", 443 `!v n. shiftl v n = v ++ replicate [F] n`, 444 lrw [shiftl_def, replicate_def, listTheory.PAD_RIGHT] 445 \\ Induct_on `n` 446 \\ lrw [listTheory.GENLIST_CONS]) 447 448(* ------------------------------------------------------------------------- *) 449 450val word_lsb_v2w = Q.store_thm("word_lsb_v2w", 451 `!v. word_lsb (v2w v) = v <> [] /\ LAST v`, 452 lrw [wordsTheory.word_lsb_def, wordsTheory.word_bit, bit_v2w, testbit, 453 rich_listTheory.LENGTH_NOT_NULL, rich_listTheory.NULL_EQ_NIL] 454 \\ Cases_on `v = []` 455 \\ rw [GSYM rich_listTheory.EL_PRE_LENGTH, arithmeticTheory.PRE_SUB1]) 456 457val word_msb_v2w = Q.store_thm("word_msb_v2w", 458 `!v. word_msb (v2w v : 'a word) = testbit (dimindex(:'a) - 1) v`, 459 lrw [wordsTheory.word_msb_def, wordsTheory.word_bit, bit_v2w]) 460 461val w2w_v2w = Q.store_thm("w2w_v2w", 462 `!v. w2w (v2w v : 'a word) : 'b word = 463 v2w (fixwidth (if dimindex(:'b) < dimindex(:'a) then 464 dimindex(:'b) 465 else 466 dimindex(:'a)) v)`, 467 wrw [wordsTheory.w2w] 468 \\ Cases_on `i < dimindex(:'a)` 469 \\ lrw [wordsTheory.word_bit, el_fixwidth, bit_v2w, testbit, 470 length_fixwidth] 471 \\ lfs [arithmeticTheory.NOT_LESS_EQUAL] 472 >| [ 473 `dimindex (:'b) <= LENGTH v + dimindex (:'b) - (i + 1) = i < LENGTH v` 474 by decide_tac, 475 `dimindex (:'a) <= LENGTH v + dimindex (:'a) - (i + 1) = i < LENGTH v` 476 by decide_tac] 477 THEN simp []) 478 479val sw2sw_v2w = Q.store_thm("sw2sw_v2w", 480 `!v. sw2sw (v2w v : 'a word) : 'b word = 481 if dimindex (:'a) < dimindex (:'b) then 482 v2w (sign_extend (dimindex(:'b)) (fixwidth (dimindex(:'a)) v)) 483 else 484 v2w (fixwidth (dimindex(:'b)) v)`, 485 wrw [wordsTheory.sw2sw] 486 \\ lrw [wordsTheory.word_bit, bit_v2w, testbit, word_msb_v2w, 487 length_sign_extend, length_fixwidth, el_sign_extend, el_fixwidth] 488 \\ lfs [arithmeticTheory.NOT_LESS, 489 DECIDE ``0 < d ==> (v - 1 - (d - 1) = v - d)``] 490 >- (Cases_on `i < LENGTH v` \\ lrw []) 491 >- (Cases_on `LENGTH v = 0` 492 \\ lrw [DECIDE ``0n < d ==> ~(d < 1)``, arithmeticTheory.LE_LT1]) 493 \\ Cases_on `i < LENGTH v` \\ lrw []) 494 495val n2w_v2n = Q.store_thm("n2w_v2n", 496 `!v. n2w (v2n v) = v2w v`, 497 wrw [wordsTheory.word_bit, bit_v2w, wordsTheory.word_bit_n2w, v2n_def, 498 testbit] 499 \\ Cases_on `i < LENGTH v` 500 \\ rw [] 501 >| [ 502 `i < LENGTH (bitify [] v)` by metis_tac [length_bitify_null] 503 \\ rw [numposrepTheory.BIT_num_from_bin_list, every_bit_bitify, el_bitify], 504 match_mp_tac bitTheory.NOT_BIT_GT_TWOEXP 505 \\ qspecl_then [`bitify [] v`, `2`] assume_tac l2n_lt 506 \\ fs [arithmeticTheory.NOT_LESS, num_from_bin_list_def] 507 \\ metis_tac [length_bitify_null, bitTheory.TWOEXP_MONO2, 508 arithmeticTheory.LESS_LESS_EQ_TRANS] 509 ]) 510 511val v2n_n2v_lem = Q.prove( 512 `!l. EVERY ($> 2) l ==> 513 (MAP ((\b. if b then 1 else 0) o (\n. n <> 0)) l = l)`, 514 Induct \\ lrw []) 515 516val v2n_n2v = Q.store_thm("v2n_n2v", 517 `!n. v2n (n2v n) = n`, 518 lrw [n2v_def, v2n_def, bitify_def, num_from_bin_list_def, l2n_def, 519 num_to_bin_list_def, bitify_reverse_map, boolify_reverse_map, 520 rich_listTheory.MAP_REVERSE, listTheory.MAP_MAP_o, v2n_n2v_lem, 521 numposrepTheory.n2l_BOUND, numposrepTheory.l2n_n2l]) 522 523val v2w_n2v = Q.store_thm("v2w_n2v", 524 `!n. v2w (n2v n) = n2w n`, 525 rewrite_tac [GSYM n2w_v2n, v2n_n2v]) 526 527val w2n_v2w = Q.store_thm("w2n_v2w", 528 `!v. w2n (v2w v : 'a word) = MOD_2EXP (dimindex(:'a)) (v2n v)`, 529 rw [Once (GSYM n2w_v2n), wordsTheory.MOD_2EXP_DIMINDEX]) 530 531val v2n_lt = Q.store_thm("v2n_lt", 532 `!v. v2n v < 2 ** LENGTH v`, 533 metis_tac [v2n_def, length_bitify_null, num_from_bin_list_def, 534 l2n_lt, DECIDE ``0 < 2n``]) 535 536(* ------------------------------------------------------------------------- *) 537 538fun bitwise_tac x y = 539 qabbrev_tac `l = ZIP (fixwidth (LENGTH ^x) v,fixwidth (LENGTH ^x) w)` 540 \\ `LENGTH (fixwidth (LENGTH ^x) ^y) = LENGTH (fixwidth (LENGTH ^x) ^x)` 541 by rewrite_tac [length_fixwidth] 542 \\ `0 < LENGTH l` 543 by (`0 < LENGTH ^x` by decide_tac 544 \\ fs [Abbr `l`, listTheory.LENGTH_ZIP, length_fixwidth]) 545 \\ `arithmetic$- (LENGTH l) (i + 1n) < LENGTH l` by decide_tac 546 \\ `arithmetic$- (LENGTH l) (i + 1) < LENGTH (fixwidth (LENGTH ^x) v)` 547 by fs [Abbr `l`, listTheory.LENGTH_ZIP, length_fixwidth] 548 \\ lrw [Abbr `l`, listTheory.LENGTH_ZIP, fixwidth_id, el_fixwidth, 549 listTheory.EL_MAP, 550 Q.ISPECL [`fixwidth (LENGTH ^x) v`, `fixwidth (LENGTH ^x) w`] 551 listTheory.EL_ZIP] 552 \\ Cases_on `i < LENGTH ^y` 553 \\ lrw [] 554 555val bitwise_tac = 556 srw_tac [boolSimps.LET_ss, fcpLib.FCP_ss, ARITH_ss, boolSimps.CONJ_ss] 557 [v2w_def, bitwise_def, length_fixwidth, 558 testbit, arithmeticTheory.MAX_DEF, band_def, bor_def, bxor_def, 559 wordsTheory.word_and_def, wordsTheory.word_or_def, 560 wordsTheory.word_xor_def] 561 >- (bitwise_tac ``w:bitstring`` ``v:bitstring``) 562 \\ Cases_on `LENGTH w < LENGTH v` 563 >- (bitwise_tac ``v:bitstring`` ``w:bitstring``) 564 \\ `LENGTH v = LENGTH w` by decide_tac 565 \\ rw [fixwidth_id] 566 \\ Cases_on `LENGTH w = 0` 567 >- fs [listTheory.LENGTH_NIL] 568 \\ `arithmetic$- (LENGTH (ZIP (v,w))) (i + 1) < LENGTH (ZIP (v,w))` 569 by lrw [listTheory.LENGTH_ZIP] 570 \\ lrw [listTheory.LENGTH_ZIP, listTheory.EL_MAP, listTheory.EL_ZIP] 571 \\ decide_tac 572 573val word_and_v2w = Q.store_thm("word_and_v2w", 574 `!v w. v2w v && v2w w = v2w (band v w)`, bitwise_tac) 575 576val word_or_v2w = Q.store_thm("word_or_v2w", 577 `!v w. v2w v || v2w w = v2w (bor v w)`, bitwise_tac) 578 579val word_xor_v2w = Q.store_thm("word_xor_v2w", 580 `!v w. v2w v ?? v2w w = v2w (bxor v w)`, bitwise_tac) 581 582fun bitwise_tac x y = 583 qabbrev_tac `l = ZIP (fixwidth (dimindex(:'a)) v,fixwidth (dimindex(:'a)) w)` 584 \\ `LENGTH (fixwidth (dimindex(:'a)) ^y) = 585 LENGTH (fixwidth (dimindex(:'a)) ^x)` 586 by rewrite_tac [length_fixwidth] 587 \\ `arithmetic$- (LENGTH l) (i + 1n) < LENGTH l` by decide_tac 588 \\ `arithmetic$- (LENGTH l) (i + 1) < LENGTH (fixwidth (LENGTH ^x) v)` 589 by fs [Abbr `l`, listTheory.LENGTH_ZIP, length_fixwidth] 590 \\ lrw [Abbr `l`, listTheory.LENGTH_ZIP, fixwidth_id, el_fixwidth, 591 listTheory.EL_MAP, 592 Q.ISPECL [`fixwidth (LENGTH ^x) v`, `fixwidth (LENGTH ^x) w`] 593 listTheory.EL_ZIP] 594 \\ Cases_on `i < LENGTH ^y` 595 \\ lrw [] 596 597val bitwise_tac = 598 srw_tac [boolSimps.LET_ss, fcpLib.FCP_ss, ARITH_ss, boolSimps.CONJ_ss] 599 [v2w_def, bitwise_def, length_fixwidth, fixwidth_fixwidth, 600 testbit, arithmeticTheory.MAX_DEF, bxnor_def, bnand_def, bnor_def, 601 wordsTheory.word_xnor_def, wordsTheory.word_nand_def, 602 wordsTheory.word_nor_def, 603 listTheory.LENGTH_ZIP, listTheory.EL_MAP, listTheory.EL_ZIP] 604 \\ lrw [el_fixwidth, DECIDE ``0 < d ==> (d <= v + d - (i + 1) = i < v)``] 605 606val word_nand_v2w = Q.store_thm("word_nand_v2w", 607 `!v w. v2w v ~&& (v2w w) : 'a word = 608 v2w (bnand (fixwidth (dimindex(:'a)) v) 609 (fixwidth (dimindex(:'a)) w))`, bitwise_tac) 610 611val word_nor_v2w = Q.store_thm("word_nor_v2w", 612 `!v w. v2w v ~|| (v2w w) : 'a word = 613 v2w (bnor (fixwidth (dimindex(:'a)) v) 614 (fixwidth (dimindex(:'a)) w))`, bitwise_tac) 615 616val word_xnor_v2w = Q.store_thm("word_xnor_v2w", 617 `!v w. v2w v ~?? (v2w w) : 'a word = 618 v2w (bxnor (fixwidth (dimindex(:'a)) v) 619 (fixwidth (dimindex(:'a)) w))`, bitwise_tac) 620 621val word_1comp_v2w = Q.store_thm("word_1comp_v2w", 622 `!v. word_1comp (v2w v : 'a word) = v2w (bnot (fixwidth (dimindex(:'a)) v))`, 623 wrw [v2w_def, bnot_def, wordsTheory.word_1comp_def, testbit, el_fixwidth, 624 length_fixwidth, listTheory.EL_MAP] 625 \\ Cases_on `i < LENGTH v` 626 \\ lrw []) 627 628(* ------------------------------------------------------------------------- *) 629 630val word_lsl_v2w = Q.store_thm("word_lsl_v2w", 631 `!n v. word_lsl (v2w v : 'a word) n = v2w (shiftl v n)`, 632 wrw [wordsTheory.word_lsl_def, shiftl_def, listTheory.PAD_RIGHT] 633 \\ Cases_on `n <= i` 634 \\ lrw [wordsTheory.word_bit, bit_v2w, testbit, length_pad_right] 635 >- (Cases_on `LENGTH v = 0` \\ lrw [rich_listTheory.EL_APPEND1]) 636 \\ lrw [rich_listTheory.EL_APPEND2]) 637 638val word_lsr_v2w = Q.store_thm("word_lsr_v2w", 639 `!n v. word_lsr (v2w v : 'a word) n = 640 v2w (shiftr (fixwidth (dimindex(:'a)) v) n)`, 641 wrw [wordsTheory.word_lsr_def, shiftr_def] 642 \\ Cases_on `i + n < dimindex(:'a)` 643 \\ lrw [wordsTheory.word_bit, bit_v2w, testbit, length_fixwidth, 644 rich_listTheory.EL_TAKE, el_fixwidth, 645 DECIDE ``0 < d ==> (d <= v + d - (i + (n + 1)) = i + n < v)``]) 646 647val word_modify_v2w = Q.store_thm("word_modify_v2w", 648 `!f v. word_modify f (v2w v : 'a word) = 649 v2w (modify f (fixwidth (dimindex(:'a)) v))`, 650 wrw [wordsTheory.word_modify_def] 651 \\ lrw [modify_def, wordsTheory.word_bit, bit_v2w, testbit] 652 \\ `LENGTH (rev_count_list (LENGTH (fixwidth (dimindex (:'a)) v))) = 653 LENGTH (fixwidth (dimindex (:'a)) v)` 654 by rewrite_tac [length_rev_count_list] 655 \\ `LENGTH (ZIP 656 (rev_count_list (LENGTH (fixwidth (dimindex (:'a)) v)), 657 fixwidth (dimindex (:'a)) v)) = dimindex(:'a)` 658 by metis_tac [listTheory.LENGTH_ZIP, length_fixwidth] 659 \\ `dimindex (:'a) - (i + 1) < 660 LENGTH (rev_count_list (LENGTH (fixwidth (dimindex (:'a)) v)))` 661 by lrw [length_rev_count_list, length_fixwidth] 662 \\ lrw [listTheory.EL_MAP, listTheory.EL_ZIP, el_rev_count_list, 663 length_fixwidth, el_fixwidth, 664 DECIDE ``0 < d ==> (d <= v + d - (i + 1) = i < v)``]) 665 666val word_bits_v2w = Q.store_thm("word_bits_v2w", 667 `!h l v. word_bits h l (v2w v : 'a word) = 668 v2w (field h l (fixwidth (dimindex(:'a)) v))`, 669 wrw [wordsTheory.word_bits_def] 670 \\ Cases_on `i + l < dimindex(:'a)` 671 \\ lrw [wordsTheory.word_bit, bit_v2w, length_field, testbit] 672 \\ Cases_on `i < SUC h - l` 673 \\ lrw [el_field, length_fixwidth, el_fixwidth, 674 DECIDE ``0 < d ==> (d <= v + d - (i + (l + 1)) = i + l < v)``]) 675 676val word_extract_v2w = Q.store_thm("word_extract_v2w", 677 `!h l v. word_extract h l (v2w v : 'a word) = 678 w2w (word_bits h l (v2w v : 'a word))`, 679 rw [wordsTheory.word_extract_def]) 680 681val word_slice_v2w = Q.store_thm("word_slice_v2w", 682 `!h l v. word_slice h l (v2w v : 'a word) = 683 v2w (shiftl (field h l (fixwidth (dimindex(:'a)) v)) l)`, 684 rw [wordsTheory.WORD_SLICE_THM, word_bits_v2w, word_lsl_v2w]) 685 686val pad_left_T_or_F = Q.prove( 687 `(v2w (PAD_LEFT F (dimindex (:'a)) [F]) = 0w : 'a word) /\ 688 (v2w (PAD_LEFT T (dimindex (:'a)) [T]) = -1w : 'a word)`, 689 wrw [wordsTheory.WORD_NEG_1_T] 690 \\ wrw [wordsTheory.word_bit, bit_v2w, testbit, listTheory.PAD_LEFT] 691 \\ (Cases_on `dimindex (:'a) - (i + 1) < 692 LENGTH (GENLIST (K F) (dimindex (:'a) - 1))` 693 >| [ 694 pop_assum (fn th => 695 map_every assume_tac 696 [th, REWRITE_RULE [listTheory.LENGTH_GENLIST] th]) 697 \\ lrw [rich_listTheory.EL_APPEND1, listTheory.EL_GENLIST], 698 fs [arithmeticTheory.NOT_LESS, rich_listTheory.EL_APPEND2] 699 \\ `i = 0` by decide_tac 700 \\ lrw [] 701 ])) 702 703val hd_shiftr = 704 el_shiftr 705 |> Q.SPEC `0` 706 |> SIMP_RULE (arith_ss++boolSimps.CONJ_ss) [listTheory.EL] 707 708val word_asr_v2w = Q.store_thm("word_asr_v2w", 709 `!n v. word_asr (v2w v : 'a word) n = 710 let l = fixwidth (dimindex(:'a)) v in 711 v2w (sign_extend (dimindex(:'a)) 712 (if dimindex(:'a) <= n then [HD l] else shiftr l n))`, 713 lrw [wordsTheory.ASR_LIMIT, word_msb_v2w] 714 >| [ 715 simp_tac (arith_ss++boolSimps.LET_ss) 716 [GSYM (Thm.CONJUNCT1 rich_listTheory.EL), el_fixwidth, 717 wordsTheory.DIMINDEX_GT_0, testbit, sign_extend_def] 718 \\ Cases_on `LENGTH v = 0` 719 \\ simp [pad_left_T_or_F] 720 \\ rw [pad_left_T_or_F, DECIDE ``~(v < d) = d < v + 1``, 721 DECIDE ``0 < d ==> (v - 1 - (d - 1) = v - d)``], 722 simp [wordsTheory.word_asr, word_msb_v2w, word_lsr_v2w, testbit] 723 \\ Cases_on `LENGTH v = 0` 724 \\ imp_res_tac listTheory.LENGTH_NIL 725 \\ lrw [hd_shiftr, length_shiftr, length_fixwidth, sign_extend_def, 726 wordsTheory.word_asr, listTheory.PAD_LEFT] 727 \\ fsrw_tac [ARITH_ss] 728 [arithmeticTheory.NOT_LESS, arithmeticTheory.NOT_LESS_EQUAL, 729 word_or_def, word_slice_def] 730 \\ wrw [wordsTheory.word_bit, bit_v2w, testbit, length_shiftr, 731 length_fixwidth, el_shiftr, 732 SIMP_RULE std_ss [wordsTheory.word_bit] WORD_NEG_1_T] 733 \\ Cases_on `dimindex (:'a) - (i + 1) < n` 734 \\ lrw [rich_listTheory.EL_APPEND1, rich_listTheory.EL_APPEND2, el_shiftr] 735 ]) 736 737val word_ror_v2w = Q.store_thm("word_ror_v2w", 738 `!n v. word_ror (v2w v : 'a word) n = 739 v2w (rotate (fixwidth (dimindex(:'a)) v) n)`, 740 wrw [wordsTheory.word_ror, word_or_def, word_lsl_def, word_bits_def, 741 rotate_def, length_fixwidth, v2w_fixwidth] 742 \\ `?p. dimindex(:'a) = i + p + 1` 743 by metis_tac [arithmeticTheory.LESS_ADD_1, arithmeticTheory.ADD_ASSOC] 744 \\ lrw [wordsTheory.word_bit, bit_v2w, testbit] 745 \\ Cases_on `n MOD (i + (p + 1)) = 0` 746 \\ rw [length_field, arithmeticTheory.ADD1] 747 >- (`LENGTH (field 0 0 (fixwidth (i + (p + 1)) v)) = 1` 748 by rw [length_field] 749 \\ lrw [wordsTheory.word_bit, bit_v2w, testbit, el_field, length_fixwidth, 750 el_fixwidth, rich_listTheory.EL_APPEND2, arithmeticTheory.ADD1, 751 DECIDE ``i + (p + 1) <= p + v = i < v``]) 752 \\ qabbrev_tac `q = n MOD (i + (p + 1))` 753 \\ `q < i + p + 1` by lrw [Abbr `q`, arithmeticTheory.MOD_LESS] 754 \\ lrw [wordsTheory.word_bit, bit_v2w, testbit] 755 \\ Cases_on `p < q` 756 \\ lrw [rich_listTheory.EL_APPEND1, rich_listTheory.EL_APPEND2, length_field] 757 >- (lrw [el_field, length_fixwidth, arithmeticTheory.ADD1, el_fixwidth] 758 \\ Cases_on `LENGTH v = 0` 759 \\ lrw [DECIDE ``i + (p + 1) <= i + (2 * p + (v + 1)) - q = 760 i < i + (p + (v + 1)) - q``]) 761 \\ Cases_on `i + q < dimdinex(:'a)` 762 \\ lrw [wordsTheory.word_bit, bit_v2w, testbit, el_field, length_fixwidth, 763 arithmeticTheory.ADD1, el_fixwidth, 764 DECIDE ``i + (p + 1) <= p + v - q = i + q < v``] 765 ) 766 767val word_reverse_v2w = Q.store_thm("word_reverse_v2w", 768 `!v. word_reverse (v2w v : 'a word) = 769 v2w (REVERSE (fixwidth (dimindex(:'a)) v))`, 770 wrw [wordsTheory.word_reverse_def] 771 \\ lrw [wordsTheory.word_bit, bit_v2w, testbit, length_fixwidth, 772 listTheory.EL_REVERSE, DECIDE ``PRE (i + 1) = i``] 773 \\ lrw [el_fixwidth, DECIDE ``0 < d ==> (d <= i + v = d < i + (v + 1))``] 774 \\ Cases_on `LENGTH v = 0` 775 \\ lrw []) 776 777val word_join_v2w = Q.store_thm("word_join_v2w", 778 `!v1 v2. FINITE univ(:'a) /\ FINITE univ(:'b) ==> 779 (word_join (v2w v1 : 'a word) (v2w v2 : 'b word) = 780 v2w (v1 ++ fixwidth (dimindex(:'b)) v2))`, 781 wrw [wordsTheory.word_join_index, fcpTheory.index_sum] 782 \\ wrw [wordsTheory.word_bit, bit_v2w, testbit, length_fixwidth, 783 rich_listTheory.EL_APPEND2, fcpTheory.index_sum] 784 \\ lrw [el_fixwidth, DECIDE ``0 < d ==> (d <= v + d - (i + 1) = i < v)``] 785 \\ Cases_on `LENGTH v1 = 0` \\ lrw [rich_listTheory.EL_APPEND1]) 786 787val word_concat_v2w = Q.store_thm("word_concat_v2w", 788 `!v1 v2. FINITE univ(:'a) /\ FINITE univ(:'b) ==> 789 (word_concat (v2w v1 : 'a word) (v2w v2 : 'b word) : 'c word = 790 v2w (fixwidth (MIN (dimindex(:'c)) (dimindex(:'a) + dimindex(:'b))) 791 (v1 ++ fixwidth (dimindex(:'b)) v2)))`, 792 lrw [wordsTheory.word_concat_def, word_join_v2w, w2w_v2w, 793 arithmeticTheory.MIN_DEF, fcpTheory.index_sum]) 794 795val word_join_v2w_rwt = Q.store_thm("word_join_v2w_rwt", 796 `!v1 v2. word_join (v2w v1 : 'a word) (v2w v2 : 'b word) = 797 if FINITE univ(:'a) /\ FINITE univ(:'b) then 798 v2w (v1 ++ fixwidth (dimindex(:'b)) v2) 799 else 800 FAIL $word_join ^(Term.mk_var("bad domain", Type.bool)) 801 (v2w v1 : 'a word) (v2w v2 : 'b word)`, 802 rw [word_join_v2w, combinTheory.FAIL_THM]) 803 804val word_concat_v2w_rwt = Q.store_thm("word_concat_v2w_rwt", 805 `!v1 v2. 806 word_concat (v2w v1 : 'a word) (v2w v2 : 'b word) : 'c word = 807 if FINITE univ(:'a) /\ FINITE univ(:'b) then 808 v2w (fixwidth (MIN (dimindex(:'c)) (dimindex(:'a) + dimindex(:'b))) 809 (v1 ++ fixwidth (dimindex(:'b)) v2)) 810 else 811 FAIL $word_concat ^(Term.mk_var("bad domain", Type.bool)) 812 (v2w v1 : 'a word) (v2w v2 : 'b word)`, 813 rw [word_concat_v2w, combinTheory.FAIL_THM]) 814 815val genlist_fixwidth = Q.prove( 816 `!d v. 0 < d ==> 817 (GENLIST (\i. (d < i + (LENGTH v + 1) /\ 0 < LENGTH v) /\ 818 EL (LENGTH v - 1 - (d - (i + 1))) v) d = 819 fixwidth d v)`, 820 lrw [listTheory.LIST_EQ_REWRITE, length_fixwidth, el_fixwidth] 821 \\ Cases_on `LENGTH v = 0` 822 \\ lrw [DECIDE ``0 < d ==> (d <= x + v = d < x + (v + 1))``]) 823 824val word_reduce_v2w = Q.store_thm("word_reduce_v2w", 825 `!f v. word_reduce f (v2w v : 'a word) = 826 let l = fixwidth (dimindex(:'a)) v in 827 v2w [FOLDL f (HD l) (TL l)] : 1 word`, 828 wrw [word_reduce_def] 829 \\ lrw [wordsTheory.word_bit, bit_v2w, testbit] 830 \\ match_mp_tac listTheory.FOLDL_CONG 831 \\ lrw [genlist_fixwidth]) 832 833val reduce_and_v2w = 834 wordsTheory.reduce_and_def 835 |> Rewrite.REWRITE_RULE [boolTheory.FUN_EQ_THM] 836 |> Q.SPEC `v2w v` 837 |> Drule.GEN_ALL 838 |> Lib.curry Theory.save_thm "reduce_and_v2w" 839 840val reduce_or_v2w = 841 wordsTheory.reduce_or_def 842 |> Rewrite.REWRITE_RULE [boolTheory.FUN_EQ_THM] 843 |> Q.SPEC `v2w v` 844 |> Drule.GEN_ALL 845 |> Lib.curry Theory.save_thm "reduce_or_v2w" 846 847(* ------------------------------------------------------------------------- *) 848 849val extract_v2w = Q.store_thm("extract_v2w", 850 `!h l v. 851 (LENGTH v <= dimindex(:'a)) /\ (dimindex(:'b) = SUC h - l) /\ 852 dimindex(:'b) <= dimindex(:'a) ==> 853 ((h >< l) (v2w v : 'a word) : 'b word = v2w (field h l v))`, 854 lrw [word_extract_v2w, word_bits_v2w, fixwidth_fixwidth, fixwidth_eq, 855 testbit, w2w_v2w, length_shiftr, length_fixwidth, length_field, v2w_11] 856 \\ `(SUC h - (i + (l + 1))) < (SUC h - l)` by decide_tac 857 \\ qspecl_then [`(SUC h - (i + (l + 1)))`, `(SUC h - l)`] imp_res_tac 858 el_fixwidth 859 \\ ntac 2 (pop_assum (kall_tac)) 860 \\ pop_assum (qspec_then `(field h l (fixwidth (dimindex (:'a)) v))` 861 SUBST1_TAC) 862 \\ simp [length_field, el_field, length_fixwidth, el_fixwidth] 863 \\ Cases_on `EL (LENGTH v - (i + (l + 1))) v` 864 \\ lrw []) 865 866val DROP_LAST = Q.prove( 867 `!l. ~NULL l ==> (DROP (LENGTH l - 1) l = [LAST l])`, 868 rw[rich_listTheory.DROP_LASTN,arithmeticTheory.SUB_LEFT_SUB, 869 rich_listTheory.LASTN_1,rich_listTheory.NULL_EQ_NIL] 870 \\ `(LENGTH l = 0) \/ (LENGTH l = 1)` by decide_tac 871 \\ fs[listTheory.LENGTH_EQ_NUM_compute,rich_listTheory.LASTN_1]); 872 873val word_bit_last_shiftr = Q.store_thm("word_bit_last_shiftr", 874 `!i v. i < dimindex(:'a) ==> 875 (word_bit i (v2w v : 'a word) = 876 let l = shiftr v i in ~NULL l /\ LAST l)`, 877 lrw [bit_v2w, testbit_def, field_def, DECIDE ``SUC i - i = 1``, fixwidth_def] 878 >- (`LENGTH (shiftr v i) = 0` by decide_tac 879 \\ lfs [listTheory.LENGTH_NIL, listTheory.PAD_LEFT, zero_extend_def]) 880 \\ `LENGTH (shiftr v i) <> 0` by decide_tac 881 \\ lfs [GSYM listTheory.NULL_LENGTH, DROP_LAST]) 882 883(* ------------------------------------------------------------------------- *) 884 885val ops_to_v2w = Q.store_thm("ops_to_v2w", 886 `(!v n. v2w v || n2w n = v2w v || v2w (n2v n)) /\ 887 (!v n. n2w n || v2w v = v2w (n2v n) || v2w v) /\ 888 (!v n. v2w v && n2w n = v2w v && v2w (n2v n)) /\ 889 (!v n. n2w n && v2w v = v2w (n2v n) && v2w v) /\ 890 (!v n. v2w v ?? n2w n = v2w v ?? v2w (n2v n)) /\ 891 (!v n. n2w n ?? v2w v = v2w (n2v n) ?? v2w v) /\ 892 (!v n. v2w v ~|| n2w n = v2w v ~|| v2w (n2v n)) /\ 893 (!v n. n2w n ~|| v2w v = v2w (n2v n) ~|| v2w v) /\ 894 (!v n. v2w v ~&& n2w n = v2w v ~&& v2w (n2v n)) /\ 895 (!v n. n2w n ~&& v2w v = v2w (n2v n) ~&& v2w v) /\ 896 (!v n. v2w v ~?? n2w n = v2w v ~?? v2w (n2v n)) /\ 897 (!v n. n2w n ~?? v2w v = v2w (n2v n) ~?? v2w v) /\ 898 (!v n. (v2w v : 'a word) @@ (n2w n : 'b word) = 899 (v2w v : 'a word) @@ (v2w (n2v n) : 'b word)) /\ 900 (!v n. (n2w n : 'a word) @@ (v2w v : 'b word) = 901 (v2w (n2v n) : 'a word) @@ (v2w v : 'b word)) /\ 902 (!v n. word_join (v2w v) (n2w n) = word_join (v2w v) (v2w (n2v n))) /\ 903 (!v n. word_join (n2w n) (v2w v) = word_join (v2w (n2v n)) (v2w v))`, 904 rewrite_tac [v2w_n2v]) 905 906val ops_to_n2w = Q.store_thm("ops_to_n2w", 907 `(!v. word_2comp (v2w v) = word_2comp (n2w (v2n v))) /\ 908 (!v. word_log2 (v2w v) = word_log2 (n2w (v2n v))) /\ 909 (!v n. (v2w v = n2w n : 'a word) = (n2w (v2n v) = n2w n : 'a word)) /\ 910 (!v n. (n2w n = v2w v : 'a word) = (n2w n = n2w (v2n v) : 'a word)) /\ 911 (!v w. (v2w v + w) = (n2w (v2n v) + w)) /\ 912 (!v w. (w + v2w v) = (w + n2w (v2n v))) /\ 913 (!v w. (v2w v - w) = (n2w (v2n v) - w)) /\ 914 (!v w. (w - v2w v) = (w - n2w (v2n v))) /\ 915 (!v w. (v2w v * w) = (n2w (v2n v) * w)) /\ 916 (!v w. (w * v2w v) = (w * n2w (v2n v))) /\ 917 (!v w. (v2w v / w) = (n2w (v2n v) / w)) /\ 918 (!v w. (w / v2w v) = (w / n2w (v2n v))) /\ 919 (!v w. (v2w v // w) = (n2w (v2n v) // w)) /\ 920 (!v w. (w // v2w v) = (w // n2w (v2n v))) /\ 921 (!v w. word_mod (v2w v) w = word_mod (n2w (v2n v)) w) /\ 922 (!v w. word_mod w (v2w v) = word_mod w (n2w (v2n v))) /\ 923 (!v w. (v2w v < w : 'a word) = (n2w (v2n v) < w : 'a word)) /\ 924 (!v w. (w < v2w v : 'a word) = (w < n2w (v2n v) : 'a word)) /\ 925 (!v w. (v2w v > w : 'a word) = (n2w (v2n v) > w : 'a word)) /\ 926 (!v w. (w > v2w v : 'a word) = (w > n2w (v2n v) : 'a word)) /\ 927 (!v w. (v2w v <= w : 'a word) = (n2w (v2n v) <= w : 'a word)) /\ 928 (!v w. (w <= v2w v : 'a word) = (w <= n2w (v2n v) : 'a word)) /\ 929 (!v w. (v2w v >= w : 'a word) = (n2w (v2n v) >= w : 'a word)) /\ 930 (!v w. (w >= v2w v : 'a word) = (w >= n2w (v2n v) : 'a word)) /\ 931 (!v w. (v2w v <+ w : 'a word) = (n2w (v2n v) <+ w : 'a word)) /\ 932 (!v w. (w <+ v2w v : 'a word) = (w <+ n2w (v2n v) : 'a word)) /\ 933 (!v w. (v2w v >+ w : 'a word) = (n2w (v2n v) >+ w : 'a word)) /\ 934 (!v w. (w >+ v2w v : 'a word) = (w >+ n2w (v2n v) : 'a word)) /\ 935 (!v w. (v2w v <=+ w : 'a word) = (n2w (v2n v) <=+ w : 'a word)) /\ 936 (!v w. (w <=+ v2w v : 'a word) = (w <=+ n2w (v2n v) : 'a word)) /\ 937 (!v w. (v2w v >=+ w : 'a word) = (n2w (v2n v) >=+ w : 'a word)) /\ 938 (!v w. (w >=+ v2w v : 'a word) = (w >=+ n2w (v2n v) : 'a word))`, 939 rewrite_tac [n2w_v2n]) 940 941(* ------------------------------------------------------------------------- *) 942 943val () = bossLib.export_rewrites 944 ["length_w2v", "length_fixwidth", "length_field", 945 "length_bitify", "length_shiftr", "length_rotate", 946 "v2w_w2v", "v2n_n2v", "v2w_n2v", 947 "fixwidth_fixwidth", "fixwidth_id_imp"] 948 949val _ = computeLib.add_persistent_funs [ 950 "testbit", 951 "ops_to_v2w", 952 "ops_to_n2w", 953 "fixwidth", 954 "extend", 955 "v2w_11", 956 "bit_v2w", 957 "w2n_v2w", 958 "w2v_v2w", 959 "w2w_v2w", 960 "sw2sw_v2w", 961 "word_index_v2w", 962 "word_lsl_v2w", 963 "word_lsr_v2w", 964 "word_asr_v2w", 965 "word_ror_v2w", 966 "word_1comp_v2w", 967 "word_and_v2w", 968 "word_or_v2w", 969 "word_xor_v2w", 970 "word_nand_v2w", 971 "word_nor_v2w", 972 "word_xnor_v2w", 973 "word_lsb_v2w", 974 "word_msb_v2w", 975 "word_reverse_v2w", 976 "word_modify_v2w", 977 "word_bits_v2w", 978 "word_extract_v2w", 979 "word_slice_v2w", 980 "word_join_v2w_rwt", 981 "word_concat_v2w_rwt", 982 "word_reduce_v2w", 983 "reduce_and_v2w", 984 "reduce_or_v2w" 985 ] 986 987(* 988 989time (List.map EVAL) 990 [``(v2w [T;T;F;F] : word8) ' 2``, 991 ``word_lsb (v2w [T;T;F;F] : word8)``, 992 ``word_msb (v2w [T;T;F;F] : word8)``, 993 ``word_bit 2 (v2w [T;T;F;F] : word8)``, 994 ``word_bits 5 2 (v2w [T;T;F;F] : word8)``, 995 ``word_slice 5 2 (v2w [T;T;F;F] : word8)``, 996 ``word_extract 5 2 (v2w [T;T;F;F] : word8) : word4``, 997 ``word_reverse (v2w [T;T;F;F] : word8)``, 998 ``word_replicate 2 (v2w [T;T;F;F] : word8) : word16``, 999 1000 ``reduce_and (v2w [T;T;F;F] : word8)``, 1001 ``reduce_or (v2w [T;T;F;F] : word8)``, 1002 ``reduce_xor (v2w [T;T;F;F] : word8)``, 1003 ``reduce_nand (v2w [T;T;F;F] : word8)``, 1004 ``reduce_nor (v2w [T;T;F;F] : word8)``, 1005 ``reduce_xnor (v2w [T;T;F;F] : word8)``, 1006 1007 ``(v2w [T;T;F;F] : word4) #>> 3``, 1008 1009 ``(v2w [T;T;F;F] : word8) >>> 2``, 1010 ``(v2w [T;T;F;F] : word8) << 2``, 1011 ``(v2w [T;T;F;F] : word8) >> 2``, 1012 ``(v2w [T;F;F;F;T;T;F;F] : word8) >> 2``, 1013 ``(v2w [T;T;F;F] : word8) #>> 3``, 1014 ``(v2w [T;T;F;F] : word8) #<< 2``, 1015 1016 ``word_modify (\i b. b \/ ODD i) (v2w [T;T;F;F] : word8)``, 1017 1018 ``~(v2w [T;T;F;F] : word8)``, 1019 ``-(v2w [T;T;F;F] : word8)``, 1020 ``word_log2 (v2w [T;T;F;F] : word8)``, 1021 ``word_log2 (v2w [] : word8)``, 1022 1023 ``w2w (v2w [T;T;F;F] : word8) : word12``, 1024 ``w2w (v2w [T;T;F;F] : word8) : word6``, 1025 1026 ``sw2sw (v2w [T;T;F;F] : word8) : word12``, 1027 ``sw2sw (v2w [T;T;F;F] : word8) : word6``, 1028 1029 ``sw2sw (v2w [T;F;F;F;T;T;F;F] : word8) : word12``, 1030 ``sw2sw (v2w [T;F;F;F;T;T;F;F] : word8) : word6``, 1031 1032 ``((v2w [T;T;F;F]:word4) @@ (v2w [T;F;T;F]:word4)) : word8``, 1033 ``((v2w [T;T;F;F]:word4) @@ (10w:word4)) : word8``, 1034 ``((12w:word4) @@ (v2w [T;F;T;F]:word4)) : word8``, 1035 1036 ``v2w [T;T;F;F] = v2w [T;F;T;F] : word8``, 1037 ``v2w [T;T;F;F] = 10w : word8``, 1038 ``12w = v2w [T;F;T;F] : word8``, 1039 1040 ``v2w [T;T;F;F] + v2w [T;F;T;F] : word8``, 1041 ``v2w [T;T;F;F] + 10w : word8``, 1042 ``12w + v2w [T;F;T;F] : word8``, 1043 1044 ``v2w [T;T;F;F] - v2w [T;F;T;F] : word8``, 1045 ``v2w [T;T;F;F] - 10w : word8``, 1046 ``12w - v2w [T;F;T;F] : word8``, 1047 1048 ``v2w [T;T;F;F] * v2w [T;F;T;F] : word8``, 1049 ``v2w [T;T;F;F] * 10w : word8``, 1050 ``12w * v2w [T;F;T;F] : word8``, 1051 1052 ``v2w [T;T;F;F] / v2w [T;F;T;F] : word8``, 1053 ``v2w [T;T;F;F] / 10w : word8``, 1054 ``12w / v2w [T;F;T;F] : word8``, 1055 1056 ``v2w [T;T;F;F] // v2w [T;F;T;F] : word8``, 1057 ``v2w [T;T;F;F] // 10w : word8``, 1058 ``12w // v2w [T;F;T;F] : word8``, 1059 1060 ``v2w [T;T;F;F] < v2w [T;F;T;F] : word8``, 1061 ``v2w [T;T;F;F] < 10w : word8``, 1062 ``12w < v2w [T;F;T;F] : word8``, 1063 1064 ``v2w [T;T;F;F] > v2w [T;F;T;F] : word8``, 1065 ``v2w [T;T;F;F] > 10w : word8``, 1066 ``12w > v2w [T;F;T;F] : word8``, 1067 1068 ``v2w [T;T;F;F] && v2w [T;F;T;F] : word8``, 1069 ``v2w [T;T;F;F] && 10w : word8``, 1070 ``12w && v2w [T;F;T;F] : word8``, 1071 1072 ``v2w [T;T;F;F] || v2w [T;F;T;F] : word8``, 1073 ``v2w [T;T;F;F] || 10w : word8``, 1074 ``12w || v2w [T;F;T;F] : word8``, 1075 1076 ``v2w [T;T;F;F] ?? v2w [T;F;T;F] : word8``, 1077 ``v2w [T;T;F;F] ?? 10w : word8``, 1078 ``12w ?? v2w [T;F;T;F] : word8``, 1079 1080 ``v2w [T;T;F;F] ~&& v2w [T;F;T;F] : word8``, 1081 ``v2w [T;T;F;F] ~&& 10w : word8``, 1082 ``12w ~&& v2w [T;F;T;F] : word8``, 1083 1084 ``v2w [T;T;F;F] ~|| v2w [T;F;T;F] : word8``, 1085 ``v2w [T;T;F;F] ~|| 10w : word8``, 1086 ``12w ~|| v2w [T;F;T;F] : word8``, 1087 1088 ``v2w [T;T;F;F] ~?? v2w [T;F;T;F] : word8``, 1089 ``v2w [T;T;F;F] ~?? 10w : word8``, 1090 ``12w ~?? v2w [T;F;T;F] : word8``] 1091 1092*) 1093 1094(* ------------------------------------------------------------------------- *) 1095 1096val _ = export_theory() 1097