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