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