blastScript.sml
1(* ========================================================================= *)
2(* FILE : blastScript.sml *)
3(* DESCRIPTION : A bitwise treatment of addition, multiplication *)
4(* and shifting. *)
5(* AUTHOR : Anthony Fox, University of Cambridge *)
6(* DATE : 2010,2011 *)
7(* ========================================================================= *)
8Theory blast
9Ancestors
10 arithmetic bit words
11Libs
12 fcpLib wordsLib
13
14
15(* -------------------------------------------------------------------------
16 Ripple carry addition
17 ------------------------------------------------------------------------- *)
18
19(* --------------------------------------------------------
20 "BCARRY i x y c" is the i-th carry-out bit for the
21 summuation of bit streams "x" and "y" with carry-in "c"
22 -------------------------------------------------------- *)
23
24Definition bcarry_def[nocompute]:
25 bcarry x y c <=> x /\ y \/ (x \/ y) /\ c
26End
27
28Definition BCARRY_def:
29 (BCARRY 0 x y c = c) /\
30 (BCARRY (SUC i) x y c = bcarry (x i) (y i) (BCARRY i x y c))
31End
32
33(* --------------------------------------------------------
34 "BSUM i x y c" is the i-th bit for the summuation of
35 bit streams "x" and "y" with carry-in "c"
36 -------------------------------------------------------- *)
37
38Definition bsum_def[nocompute]:
39 bsum (x:bool) y c = ((x = ~y) = ~c)
40End
41
42Definition BSUM_def[nocompute]:
43 BSUM i x y c = bsum (x i) (y i) (BCARRY i x y c)
44End
45
46(* ------------------------------------------------------------------------- *)
47
48Theorem BIT_CASES[local]:
49 !b n. (BITS b b n = 0) \/ (BITS b b n = 1)
50Proof
51 SIMP_TAC std_ss [GSYM NOT_BITS2]
52QED
53
54val BITS_SUC_cor =
55 BITS_SUC |> Q.SPECL [`n`,`0`,`x`]
56 |> SIMP_RULE std_ss []
57 |> GSYM
58 |> GEN_ALL
59
60val BITS_SUM_cor =
61 BITS_SUM |> SPEC_ALL
62 |> Q.INST [`a` |-> `1`]
63 |> SIMP_RULE std_ss []
64 |> GEN_ALL
65
66val lem =
67 bitTheory.TWOEXP_MONO
68 |> Q.SPECL [`0`,`n`]
69 |> SIMP_RULE bool_ss [ZERO_LESS_EQ, EXP]
70 |> GEN_ALL
71
72Theorem lem1[local]:
73 !n. 0 < n ==> 2 ** n + 1 < 2 ** SUC n
74Proof
75 SRW_TAC [] [EXP, TIMES2, lem]
76QED
77
78val lem2 =
79 NOT_BIT_GT_TWOEXP
80 |> Q.SPECL [`SUC n`,`1`]
81 |> SIMP_RULE std_ss [lem]
82 |> GEN_ALL
83
84Theorem BCARRY_LEM:
85 !i x y c.
86 0 < i ==>
87 (BCARRY i (\i. BIT i x) (\i. BIT i y) c =
88 BIT i (BITS (i - 1) 0 x + BITS (i - 1) 0 y + (if c then 1 else 0)))
89Proof
90 Induct
91 \\ SRW_TAC [] [BCARRY_def, bcarry_def]
92 \\ Cases_on `i`
93 >| [SRW_TAC [] [BCARRY_def, BIT_def]
94 \\ Q.SPECL_THEN [`0`,`x`] STRIP_ASSUME_TAC BIT_CASES
95 \\ Q.SPECL_THEN [`0`,`y`] STRIP_ASSUME_TAC BIT_CASES
96 \\ ASM_SIMP_TAC std_ss [BITS_THM],
97
98 POP_ASSUM (fn th => SIMP_TAC std_ss [th])
99 \\ Q.SPECL_THEN [`n`,`0`,`x`] (ASSUME_TAC o SIMP_RULE std_ss [])
100 BITSLT_THM
101 \\ Q.SPECL_THEN [`n`,`0`,`y`] (ASSUME_TAC o SIMP_RULE std_ss [])
102 BITSLT_THM
103 \\ `BITS n 0 x + BITS n 0 y + 1 < 2 * 2 ** SUC n` by DECIDE_TAC
104 \\ Cases_on `BIT (SUC n) x`
105 \\ Cases_on `BIT (SUC n) y`
106 \\ FULL_SIMP_TAC arith_ss
107 [BITS_SUC_cor, SBIT_def, BIT_def, GSYM EXP, BITS_SUM_cor]
108 \\ FULL_SIMP_TAC std_ss [GSYM BIT_def, BIT_B, NOT_BIT_GT_TWOEXP]
109 \\ `BITS n 0 x + (BITS n 0 y + 1) = BITS n 0 x + BITS n 0 y + 1`
110 by DECIDE_TAC
111 \\ POP_ASSUM SUBST_ALL_TAC
112 \\ Cases_on `BITS n 0 x + BITS n 0 y = 0`
113 \\ ASM_SIMP_TAC std_ss [lem1, lem2, BIT_ZERO, NOT_BIT_GT_TWOEXP]
114 \\ (Cases_on `BIT (SUC n) (BITS n 0 x + BITS n 0 y + 1)`
115 \\ ASM_SIMP_TAC std_ss []
116 >| [IMP_RES_TAC
117 (METIS_PROVE [NOT_BIT_GT_TWOEXP, NOT_LESS]
118 ``BIT i (a + b + 1) ==> 2 ** i <= (a + b + 1)``)
119 \\ IMP_RES_TAC LESS_EQUAL_ADD
120 \\ `p < 2 ** SUC (SUC n)`
121 by FULL_SIMP_TAC arith_ss []
122 \\ Q.PAT_ASSUM `a + b = c + d:num` SUBST1_TAC
123 \\ ASM_SIMP_TAC arith_ss [BIT_def, GSYM EXP,
124 ONCE_REWRITE_RULE [ADD_COMM] BITS_SUM_cor]
125 \\ SIMP_TAC std_ss [GSYM BIT_def, BIT_B],
126 `BITS n 0 x + BITS n 0 y + 1 <> 0`
127 by DECIDE_TAC
128 \\ `BITS n 0 x + BITS n 0 y + 1 < 2 ** SUC n`
129 by METIS_TAC [NOT_LESS, LOG2_UNIQUE, BIT_LOG2]
130 \\ `2 ** SUC n + (BITS n 0 x + BITS n 0 y + 1) < 2 * 2 ** SUC n`
131 by DECIDE_TAC
132 \\ FULL_SIMP_TAC std_ss [GSYM EXP, NOT_BIT_GT_TWOEXP]]),
133
134 SRW_TAC [] [BCARRY_def, BIT_def]
135 \\ Q.SPECL_THEN [`0`,`x`] STRIP_ASSUME_TAC BIT_CASES
136 \\ Q.SPECL_THEN [`0`,`y`] STRIP_ASSUME_TAC BIT_CASES
137 \\ ASM_SIMP_TAC std_ss [BITS_THM],
138
139 POP_ASSUM (fn th => SIMP_TAC std_ss [th])
140 \\ Q.SPECL_THEN [`n`,`0`,`x`] (ASSUME_TAC o SIMP_RULE std_ss [])
141 BITSLT_THM
142 \\ Q.SPECL_THEN [`n`,`0`,`y`] (ASSUME_TAC o SIMP_RULE std_ss [])
143 BITSLT_THM
144 \\ `BITS n 0 x + BITS n 0 y < 2 * 2 ** SUC n` by DECIDE_TAC
145 \\ Cases_on `BIT (SUC n) x`
146 \\ Cases_on `BIT (SUC n) y`
147 \\ FULL_SIMP_TAC arith_ss
148 [BITS_SUC_cor, SBIT_def, BIT_def, GSYM EXP, BITS_SUM_cor]
149 \\ FULL_SIMP_TAC std_ss [GSYM BIT_def, BIT_B, NOT_BIT_GT_TWOEXP]
150 \\ Cases_on `BITS n 0 x + BITS n 0 y = 0`
151 \\ ASM_SIMP_TAC std_ss [BIT_ZERO, NOT_BIT_GT_TWOEXP]
152 \\ (Cases_on `BIT (SUC n) (BITS n 0 x + BITS n 0 y)`
153 \\ ASM_SIMP_TAC std_ss []
154 >| [IMP_RES_TAC
155 (METIS_PROVE [NOT_BIT_GT_TWOEXP, NOT_LESS]
156 ``BIT i (a + b) ==> 2 ** i <= (a + b)``)
157 \\ IMP_RES_TAC LESS_EQUAL_ADD
158 \\ `p < 2 ** SUC (SUC n)`
159 by FULL_SIMP_TAC arith_ss []
160 \\ Q.PAT_ASSUM `a + b = c + d:num` SUBST1_TAC
161 \\ ASM_SIMP_TAC arith_ss [BIT_def, GSYM EXP,
162 ONCE_REWRITE_RULE [ADD_COMM] BITS_SUM_cor]
163 \\ SIMP_TAC std_ss [GSYM BIT_def, BIT_B],
164 `BITS n 0 x + BITS n 0 y < 2 ** SUC n`
165 by METIS_TAC [NOT_LESS, LOG2_UNIQUE, BIT_LOG2]
166 \\ `2 ** SUC n + (BITS n 0 x + BITS n 0 y) < 2 * 2 ** SUC n`
167 by DECIDE_TAC
168 \\ FULL_SIMP_TAC std_ss [GSYM EXP, NOT_BIT_GT_TWOEXP]
169 ])
170 ]
171QED
172
173(* ------------------------------------------------------------------------ *)
174
175Theorem BCARRY_EQ:
176 !n c x1 x2 y1 y2.
177 (!i. i < n ==> (x1 i = x2 i) /\ (y1 i = y2 i)) ==>
178 (BCARRY n x1 y1 c = BCARRY n x2 y2 c)
179Proof
180 Induct \\ SRW_TAC [] [BCARRY_def]
181 \\ `!i. i < n ==> (x1 i = x2 i) /\ (y1 i = y2 i)`
182 by ASM_SIMP_TAC arith_ss []
183 \\ RES_TAC \\ ASM_REWRITE_TAC []
184QED
185
186Theorem BSUM_EQ:
187 !n c x1 x2 y1 y2.
188 (!i. i <= n ==> (x1 i = x2 i) /\ (y1 i = y2 i)) ==>
189 (BSUM n x1 y1 c = BSUM n x2 y2 c)
190Proof
191 SRW_TAC [] [BSUM_def]
192 \\ `!i. i < n ==> (x1 i = x2 i) /\ (y1 i = y2 i)`
193 by ASM_SIMP_TAC arith_ss []
194 \\ IMP_RES_TAC BCARRY_EQ
195 \\ ASM_REWRITE_TAC []
196QED
197
198val word_1comp =
199 word_1comp_def |> SIMP_RULE (std_ss++fcpLib.FCP_ss) [] |> GSYM
200
201Theorem BCARRY_BIT_EQ[local]:
202 !n x y c.
203 n <= dimindex (:'a) /\ y < dimword (:'a) ==>
204 (BCARRY n ($' (n2w x :'a word)) ($~ o $' (n2w y :'a word)) c =
205 BCARRY n (\i. BIT i x) (\i. BIT i (dimword (:'a) - 1 - y)) c)
206Proof
207 REPEAT STRIP_TAC \\ MATCH_MP_TAC BCARRY_EQ
208 \\ REPEAT STRIP_TAC
209 \\ ASM_SIMP_TAC arith_ss [word_1comp, word_1comp_n2w]
210 \\ SRW_TAC [fcpLib.FCP_ss, numSimps.ARITH_ss] [word_index]
211QED
212
213Theorem BSUM_BIT_EQ[local]:
214 !n x y c.
215 n < dimindex (:'a) ==>
216 (BSUM n ($' (n2w x :'a word)) ($' (n2w y :'a word)) c =
217 BSUM n (\i. BIT i x) (\i. BIT i y) c)
218Proof
219 REPEAT STRIP_TAC \\ MATCH_MP_TAC BSUM_EQ
220 \\ SRW_TAC [fcpLib.FCP_ss, numSimps.ARITH_ss] [word_index]
221QED
222
223(* ------------------------------------------------------------------------ *)
224
225val BITS_DIVISION =
226 DIVISION |> Q.SPEC `2 ** SUC n`
227 |> SIMP_RULE std_ss [ZERO_LT_TWOEXP, GSYM BITS_ZERO3]
228 |> GEN_ALL
229
230val _ = diminish_srw_ss ["MOD"]
231Theorem ADD_BITS_SUC_CIN[local]:
232 !n a b.
233 BITS (SUC n) (SUC n) (a + b + 1) =
234 (BITS (SUC n) (SUC n) a + BITS (SUC n) (SUC n) b +
235 BITS (SUC n) (SUC n) (BITS n 0 a + BITS n 0 b + 1)) MOD 2
236Proof
237 REPEAT STRIP_TAC
238 \\ Q.SPECL_THEN [`n`,`a`] ASSUME_TAC BITS_DIVISION
239 \\ POP_ASSUM (fn th => CONV_TAC (LHS_CONV (ONCE_REWRITE_CONV [th])))
240 \\ Q.SPECL_THEN [`n`,`b`] ASSUME_TAC BITS_DIVISION
241 \\ POP_ASSUM (fn th => CONV_TAC (LHS_CONV (ONCE_REWRITE_CONV [th])))
242 \\ SRW_TAC [] [BITS_THM, SUC_SUB]
243 \\ Cases_on `(a DIV 2 ** SUC n) MOD 2 = 1`
244 \\ Cases_on `(b DIV 2 ** SUC n) MOD 2 = 1`
245 \\ FULL_SIMP_TAC arith_ss [NOT_MOD2_LEM2, ADD_MODULUS]
246 \\ REWRITE_TAC [DECIDE ``a * n + (b * n + c) = (a + b) * n + c:num``]
247 \\ SIMP_TAC std_ss [ADD_DIV_ADD_DIV, ZERO_LT_TWOEXP]
248 \\ CONV_TAC (LHS_CONV
249 (SIMP_CONV std_ss [Once (GSYM MOD_PLUS), ZERO_LT_TWOEXP]))
250 \\ CONV_TAC (LHS_CONV (RATOR_CONV
251 (SIMP_CONV std_ss [Once (GSYM MOD_PLUS), ZERO_LT_TWOEXP])))
252 \\ ASM_SIMP_TAC arith_ss []
253QED
254
255Theorem ADD_BIT_SUC_CIN[local]:
256 !n a b.
257 BIT (SUC n) (a + b + 1) =
258 if BIT (SUC n) (BITS n 0 a + BITS n 0 b + 1) then
259 BIT (SUC n) a = BIT (SUC n) b
260 else
261 BIT (SUC n) a <> BIT (SUC n) b
262Proof
263 SRW_TAC [] [BIT_def]
264 \\ CONV_TAC (LHS_CONV (SIMP_CONV std_ss [Once ADD_BITS_SUC_CIN]))
265 \\ Cases_on `BITS (SUC n) (SUC n) a = 1`
266 \\ Cases_on `BITS (SUC n) (SUC n) b = 1`
267 \\ FULL_SIMP_TAC std_ss [NOT_BITS2]
268QED
269
270Theorem BSUM_LEM:
271 !i x y c.
272 BSUM i (\i. BIT i x) (\i. BIT i y) c =
273 BIT i (x + y + if c then 1 else 0)
274Proof
275 Induct
276 >| [SRW_TAC [] [ADD_BIT0, BSUM_def, BCARRY_def, bsum_def, bcarry_def,
277 BIT_def, BITS_THM2]
278 \\ DECIDE_TAC,
279 SRW_TAC [] [BSUM_def, BCARRY_LEM]
280 \\ FULL_SIMP_TAC std_ss [BITS_COMP_THM2, BIT_OF_BITS_THM2, bsum_def]
281 \\ METIS_TAC [ADD_BIT_SUC,ADD_BIT_SUC_CIN]]
282QED
283
284(* ------------------------------------------------------------------------ *)
285
286Theorem BITWISE_ADD:
287 !x y. x + y = FCP i. BSUM i ($' x) ($' y) F
288Proof
289 Cases \\ Cases
290 \\ SRW_TAC [fcpLib.FCP_ss] [word_add_n2w, word_index, BSUM_LEM, BSUM_BIT_EQ]
291QED
292
293val BSUM_LEM_COR =
294 BSUM_LEM |> SPEC_ALL |> SYM |> Q.INST [`c` |-> `T`] |> SIMP_RULE std_ss []
295
296Theorem BITWISE_SUB:
297 !x y. x - y = FCP i. BSUM i ($' x) ((~) o ($' y)) T
298Proof
299 Cases \\ Cases
300 \\ REWRITE_TAC [word_sub_def, word_add_n2w, word_1comp_n2w, WORD_NEG]
301 \\ SRW_TAC [fcpLib.FCP_ss] [word_index, ADD_ASSOC, BSUM_LEM_COR]
302 \\ MATCH_MP_TAC BSUM_EQ
303 \\ SRW_TAC [numSimps.ARITH_ss] [word_index, word_1comp, word_1comp_n2w]
304QED
305
306(* ------------------------------------------------------------------------ *)
307
308val SUB1_SUC = DECIDE (Term `!n. 0 < n ==> (SUC (n - 1) = n)`)
309
310Theorem BITWISE_LO:
311 !x y:'a word. x <+ y <=> ~BCARRY (dimindex (:'a)) ($' x) ((~) o ($' y)) T
312Proof
313 Cases \\ Cases
314 \\ SRW_TAC [fcpLib.FCP_ss, boolSimps.LET_ss]
315 [DIMINDEX_GT_0, word_lo_def, nzcv_def, BCARRY_BIT_EQ, BCARRY_LEM]
316 \\ Cases_on `n' = 0`
317 \\ FULL_SIMP_TAC arith_ss [dimword_def, bitTheory.BITS_ZERO3, SUB1_SUC,
318 DIMINDEX_GT_0, word_2comp_n2w, w2n_n2w]
319 \\ ASM_SIMP_TAC std_ss [BIT_def,
320 BITS_SUM |> SPEC_ALL |> Q.INST [`a` |-> `1n`]
321 |> SIMP_RULE std_ss [Once ADD_COMM]]
322 \\ SIMP_TAC std_ss [GSYM BIT_def, BIT_B]
323QED
324
325(* ------------------------------------------------------------------------- *)
326
327val COUNT_LIST_compute = numLib.SUC_RULE rich_listTheory.COUNT_LIST_def
328
329Theorem BITWISE_MUL_lem[local]:
330 !n w m : 'a word.
331 0 < n /\ n <= dimindex(:'a) ==>
332 (FOLDL (\a j. a + FCP i. w ' j /\ (m << j) ' i) 0w (COUNT_LIST n) =
333 (n - 1 -- 0) w * m)
334Proof
335 Induct_on `n`
336 \\ SRW_TAC [] [rich_listTheory.COUNT_LIST_SNOC, listTheory.FOLDL_SNOC]
337 \\ Cases_on `n = 0`
338 >| [
339 Cases_on `w` \\ Cases_on `m`
340 \\ SRW_TAC [fcpLib.FCP_ss]
341 [COUNT_LIST_compute, word_bits_n2w, word_mul_n2w,
342 word_index, BITS_THM, bitTheory.BIT0_ODD, bitTheory.ODD_MOD2_LEM]
343 \\ Cases_on `n' MOD 2 = 1`
344 \\ FULL_SIMP_TAC std_ss [bitTheory.NOT_MOD2_LEM2, bitTheory.BIT_ZERO],
345 `0 < n` by DECIDE_TAC
346 \\ `(n '' n) w && (n - 1 -- 0) w = 0w`
347 by (SRW_TAC [wordsLib.WORD_BIT_EQ_ss, ARITH_ss] []
348 \\ Cases_on `i = n` \\ SRW_TAC [ARITH_ss] []
349 \\ Cases_on `i < n` \\ SRW_TAC [ARITH_ss] [])
350 \\ IMP_RES_TAC wordsTheory.WORD_ADD_OR
351 \\ `(n -- 0) w = (n '' n) w + (n - 1 -- 0) w`
352 by (SRW_TAC [wordsLib.WORD_BIT_EQ_ss] []
353 \\ Cases_on `i = n` \\ SRW_TAC [ARITH_ss] []
354 \\ Cases_on `i < n` \\ SRW_TAC [ARITH_ss] [])
355 \\ POP_ASSUM SUBST1_TAC
356 \\ SRW_TAC [ARITH_ss] [wordsTheory.WORD_LEFT_ADD_DISTRIB,
357 EQT_ELIM (wordsLib.WORD_ARITH_CONV
358 ``(a + b = b + c) = (a = c : 'a word)``)]
359 \\ Cases_on `w` \\ Cases_on `m`
360 \\ SRW_TAC [fcpLib.FCP_ss, ARITH_ss]
361 [word_mul_n2w, word_slice_n2w, word_index, word_lsl_n2w, MIN_DEF]
362 >| [ALL_TAC,
363 `dimindex(:'a) - 1 = n` by SRW_TAC [ARITH_ss] []
364 \\ FULL_SIMP_TAC std_ss []
365 ]
366 \\ Cases_on `BIT n n'`
367 \\ FULL_SIMP_TAC (srw_ss())
368 [bitTheory.SLICE_ZERO2, bitTheory.BIT_SLICE_THM2,
369 bitTheory.BIT_SLICE_THM3]
370 ]
371QED
372
373Theorem BITWISE_MUL_lem2[local]:
374 !w m : 'a word.
375 w * m =
376 FOLDL (\a j. a + FCP i. w ' j /\ (m << j) ' i) 0w
377 (COUNT_LIST (dimindex(:'a)))
378Proof
379 SRW_TAC [wordsLib.WORD_EXTRACT_ss] [BITWISE_MUL_lem]
380 \\ SRW_TAC [] [GSYM wordsTheory.WORD_w2w_EXTRACT, w2w_id]
381QED
382
383Theorem BITWISE_MUL:
384 !w m : 'a word.
385 w * m =
386 FOLDL (\a j. a + FCP i. w ' j /\ j <= i /\ m ' (i - j)) 0w
387 (COUNT_LIST (dimindex(:'a)))
388Proof
389 SRW_TAC [] [BITWISE_MUL_lem2]
390 \\ MATCH_MP_TAC listTheory.FOLDL_CONG
391 \\ SRW_TAC [] [FUN_EQ_THM, rich_listTheory.MEM_COUNT_LIST]
392 \\ SRW_TAC [fcpLib.FCP_ss] [word_lsl_def]
393QED
394
395(* ------------------------------------------------------------------------ *)
396
397Theorem word_bv_fold_zero[local]:
398 !P n f.
399 (!j. j < n ==> ~P j) ==>
400 (FOLDL (\a j. a \/ P j /\ f j) F (COUNT_LIST n) = F)
401Proof
402 Induct_on `n`
403 \\ SRW_TAC [] [rich_listTheory.COUNT_LIST_SNOC, listTheory.FOLDL_SNOC]
404 \\ `!j. j < n ==> ~P j` by SRW_TAC [ARITH_ss] []
405 \\ METIS_TAC []
406QED
407
408fun DROPN_TAC n = NTAC n (POP_ASSUM (K ALL_TAC))
409
410Theorem word_bv_lem[local]:
411 !f P i n.
412 i < n /\ P i /\
413 (!i j. P i /\ P j /\ i < n /\ j < n ==> (i = j)) ==>
414 (FOLDL (\a j. a \/ P j /\ (f j)) F (COUNT_LIST n) = f i)
415Proof
416 Induct_on `n`
417 \\ SRW_TAC [] [rich_listTheory.COUNT_LIST_SNOC, listTheory.FOLDL_SNOC]
418 \\ `!i j. P i /\ P j /\ i < n /\ j < n ==> (i = j)` by SRW_TAC [ARITH_ss] []
419 \\ Cases_on `i < n`
420 >| [
421 `(FOLDL (\a j. a \/ P j /\ f j) F (COUNT_LIST n) <=> f i)` by METIS_TAC []
422 \\ ASM_SIMP_TAC std_ss []
423 \\ Q.PAT_ASSUM `!i j. P i /\ P j /\ i < SUC n /\ j < SUC n ==> x`
424 (Q.SPECL_THEN [`n`,`i`] (IMP_RES_TAC o SIMP_RULE arith_ss []))
425 \\ METIS_TAC [],
426 `i = n` by DECIDE_TAC
427 \\ FULL_SIMP_TAC arith_ss []
428 \\ `!j. j < n ==> ~P j`
429 by (REPEAT STRIP_TAC
430 \\ `j < SUC n` by DECIDE_TAC
431 \\ Q.PAT_ASSUM `!i j. P i /\ P j /\ i < SUC n /\ j < SUC n ==> x`
432 (Q.SPECL_THEN [`j`,`n`] (IMP_RES_TAC o SIMP_RULE arith_ss []))
433 \\ `j <> n` by DECIDE_TAC
434 \\ METIS_TAC [])
435 \\ ASM_SIMP_TAC std_ss [word_bv_fold_zero]
436 ]
437QED
438
439(* ------------------------------------------------------------------------ *)
440
441Theorem lem[local]:
442 !h w P a:'a word.
443 (((dimindex(:'a) - 1) -- h + 1) w = 0w) ==>
444 (((h -- 0) a = w) /\ (((dimindex(:'a) - 1) -- h + 1) a = 0w) <=> (a = w))
445Proof
446 STRIP_TAC
447 \\ Cases_on `dimindex(:'a) - 1 < h + 1`
448 \\ SRW_TAC [wordsLib.WORD_EXTRACT_ss, ARITH_ss] []
449 \\ `h + 1 <= dimindex(:'a) - 1` by SRW_TAC [ARITH_ss] []
450 \\ IMP_RES_TAC
451 (wordsTheory.EXTRACT_JOIN_ADD
452 |> Q.SPECL [`dimindex(:'a) - 1`, `h`, `h + 1`, `0`, `h + 1`, `a`]
453 |> Thm.INST_TYPE [Type.beta |-> Type.alpha]
454 |> SIMP_RULE std_ss [GSYM wordsTheory.WORD_w2w_EXTRACT, w2w_id]
455 |> GSYM)
456 \\ POP_ASSUM (Q.SPEC_THEN `a`
457 (fn thm => CONV_TAC (RHS_CONV (LHS_CONV (REWR_CONV thm)))))
458 \\ Cases_on `(dimindex (:'a) - 1 >< h + 1) a = 0w : 'a word`
459 \\ SRW_TAC [] []
460 \\ SRW_TAC [wordsLib.WORD_EXTRACT_ss] []
461 \\ FULL_SIMP_TAC (srw_ss()++wordsLib.WORD_BIT_EQ_ss) []
462 \\ Q.EXISTS_TAC `h + (i + 1)`
463 \\ SRW_TAC [ARITH_ss] []
464 \\ METIS_TAC []
465QED
466
467Theorem lem2[local]:
468 !l i p b.
469 (FOLDL (\a j. a \/ p j) i l /\ b <=>
470 FOLDL (\a j. a \/ b /\ p j) (i /\ b) l)
471Proof
472 Induct \\ SRW_TAC [] [listTheory.FOLDL,
473 DECIDE ``((i \/ p h) /\ b <=> i /\ b \/ b /\ p h)``]
474QED
475
476Theorem FOLDL_LOG2_INTRO[local]:
477 !P n m:'a word.
478 1 < n /\ n <= dimindex (:'a) ==>
479 (FOLDL (\a j. a \/ (m = n2w j) /\ P j) F (COUNT_LIST n) <=>
480 FOLDL (\a j. a \/ ((LOG2 (n - 1) -- 0) m = n2w j) /\ P j) F
481 (COUNT_LIST n) /\
482 ((dimindex(:'a) - 1 -- LOG2 (n - 1) + 1) m = 0w))
483Proof
484 SRW_TAC [] [lem2]
485 \\ MATCH_MP_TAC listTheory.FOLDL_CONG
486 \\ SRW_TAC [] [FUN_EQ_THM, rich_listTheory.MEM_COUNT_LIST]
487 \\ Cases_on `P x` \\ Cases_on `a` \\ SRW_TAC [] []
488 \\ `x <= n - 1` by DECIDE_TAC
489 \\ `0 < n - 1` by DECIDE_TAC
490 \\ IMP_RES_TAC (logrootTheory.LOG |> Q.SPEC `2` |> SIMP_RULE std_ss [])
491 \\ `x < 2 ** (LOG2 (n - 1) + 1)`
492 by METIS_TAC [LOG2_def, ADD1, arithmeticTheory.LESS_EQ_LESS_TRANS]
493 \\ `((dimindex(:'a) - 1) -- LOG2 (n - 1) + 1) (n2w x) = 0w : 'a word`
494 by SRW_TAC [] [word_bits_n2w, bitTheory.BITS_LT_LOW]
495 \\ METIS_TAC [lem]
496QED
497
498(* ------------------------------------------------------------------------ *)
499
500Theorem word_lsl_bv_expand[local]:
501 !w m. word_lsl_bv (w:'a word) m =
502 FCP k.
503 FOLDL (\a j. a \/ (m = n2w j) /\ ((j <= k) /\ w ' (k - j))) F
504 (COUNT_LIST (dimindex(:'a)))
505Proof
506 Cases_on `m`
507 \\ SRW_TAC [fcpLib.FCP_ss] [word_lsl_bv_def, word_lsl_def]
508 \\ Q.ABBREV_TAC `P = (\j. n = j MOD dimword(:'a))`
509 \\ Cases_on `n < dimindex (:'a)`
510 >| [
511 `P n` by SRW_TAC [] [Abbr `P`]
512 \\ `!i j. P i /\ P j /\ i < dimindex(:'a) /\ j < dimindex(:'a) ==> (i = j)`
513 by (SRW_TAC [] [Abbr `P`] \\ FULL_SIMP_TAC arith_ss [dimindex_lt_dimword])
514 \\ Q.SPECL_THEN [`\j. j <= i /\ w ' (i - j)`, `P`, `n`, `dimindex(:'a)`]
515 IMP_RES_TAC word_bv_lem
516 \\ DROPN_TAC 17
517 \\ FULL_SIMP_TAC std_ss [Abbr `P`],
518 `!j. j < n ==> ~P j` by SRW_TAC [ARITH_ss] [Abbr `P`]
519 \\ ASM_SIMP_TAC arith_ss [word_0, word_bv_fold_zero]
520 ]
521QED
522
523Theorem word_lsl_bv_expand:
524 !w m.
525 word_lsl_bv (w:'a word) m =
526 if dimindex(:'a) = 1 then
527 $FCP (K (~m ' 0 /\ w ' 0))
528 else
529 FCP k.
530 FOLDL (\a j. a \/ ((LOG2 (dimindex(:'a) - 1) -- 0) m = n2w j) /\
531 ((j <= k) /\ w ' (k - j))) F
532 (COUNT_LIST (dimindex(:'a))) /\
533 ((dimindex(:'a) - 1 -- LOG2 (dimindex(:'a) - 1) + 1) m = 0w)
534Proof
535 SRW_TAC [] [word_lsl_bv_expand]
536 THEN1 SRW_TAC [wordsLib.WORD_BIT_EQ_ss] [COUNT_LIST_compute]
537 \\ `1 < dimindex(:'a)` by SRW_TAC [] [DECIDE ``0n < n /\ n <> 1 ==> 1 < n``]
538 \\ ONCE_REWRITE_TAC [fcpTheory.CART_EQ]
539 \\ SRW_TAC [] [fcpTheory.FCP_BETA]
540 \\ METIS_TAC [arithmeticTheory.LESS_EQ_REFL, FOLDL_LOG2_INTRO]
541QED
542
543Theorem word_lsr_bv_expand[local]:
544 !w m. word_lsr_bv (w:'a word) m =
545 FCP k.
546 FOLDL (\a j. a \/ (m = n2w j) /\ k + j < dimindex(:'a) /\
547 w ' (k + j)) F
548 (COUNT_LIST (dimindex(:'a)))
549Proof
550 Cases_on `m`
551 \\ SRW_TAC [fcpLib.FCP_ss] [word_lsr_bv_def, word_lsr_def]
552 \\ Q.ABBREV_TAC `P = (\j. n = j MOD dimword(:'a))`
553 \\ Cases_on `n < dimindex (:'a)`
554 >| [
555 `P n` by SRW_TAC [] [Abbr `P`]
556 \\ `!i j. P i /\ P j /\ i < dimindex(:'a) /\ j < dimindex(:'a) ==> (i = j)`
557 by (SRW_TAC [] [Abbr `P`] \\ FULL_SIMP_TAC arith_ss [dimindex_lt_dimword])
558 \\ Q.SPECL_THEN [`\j. i + j < dimindex(:'a) /\ w ' (i + j)`, `P`, `n`,
559 `dimindex(:'a)`] IMP_RES_TAC word_bv_lem
560 \\ DROPN_TAC 17
561 \\ FULL_SIMP_TAC std_ss [Abbr `P`],
562 `!j. j < n ==> ~P j` by SRW_TAC [ARITH_ss] [Abbr `P`]
563 \\ ASM_SIMP_TAC arith_ss [word_bv_fold_zero]
564 ]
565QED
566
567Theorem word_lsr_bv_expand:
568 !w m.
569 word_lsr_bv (w:'a word) m =
570 if dimindex(:'a) = 1 then
571 $FCP (K (~m ' 0 /\ w ' 0))
572 else
573 FCP k.
574 FOLDL (\a j. a \/ ((LOG2 (dimindex(:'a) - 1) -- 0) m = n2w j) /\
575 k + j < dimindex(:'a) /\ w ' (k + j)) F
576 (COUNT_LIST (dimindex(:'a))) /\
577 ((dimindex(:'a) - 1 -- LOG2 (dimindex(:'a) - 1) + 1) m = 0w)
578Proof
579 SRW_TAC [] [word_lsr_bv_expand]
580 THEN1 SRW_TAC [wordsLib.WORD_BIT_EQ_ss] [COUNT_LIST_compute]
581 \\ `1 < dimindex(:'a)` by SRW_TAC [] [DECIDE ``0n < n /\ n <> 1 ==> 1 < n``]
582 \\ ONCE_REWRITE_TAC [fcpTheory.CART_EQ]
583 \\ SRW_TAC [] [fcpTheory.FCP_BETA]
584 \\ METIS_TAC [arithmeticTheory.LESS_EQ_REFL, FOLDL_LOG2_INTRO]
585QED
586
587Theorem word_asr_bv_expand[local]:
588 !w m. word_asr_bv (w:'a word) m =
589 (FCP k.
590 FOLDL (\a j. a \/ (m = n2w j) /\ (w >> j) ' k) F
591 (COUNT_LIST (dimindex(:'a)))) ||
592 ($FCP (K (n2w (dimindex(:'a) - 1) <+ m /\ word_msb w)))
593Proof
594 `dimindex(:'a) - 1 < dimword(:'a)` by SRW_TAC [ARITH_ss] [dimindex_lt_dimword]
595 \\ Cases_on `m`
596 \\ SRW_TAC [fcpLib.FCP_ss, ARITH_ss]
597 [word_asr_bv_def, word_or_def, word_lo_n2w, dimindex_lt_dimword]
598 \\ Q.ABBREV_TAC `P = (\i. n = i MOD dimword(:'a))`
599 \\ Cases_on `n < dimindex (:'a)`
600 >| [
601 `P n` by SRW_TAC [] [Abbr `P`]
602 \\ `!i j. P i /\ P j /\ i < dimindex(:'a) /\ j < dimindex(:'a) ==> (i = j)`
603 by (SRW_TAC [] [Abbr `P`] \\ FULL_SIMP_TAC arith_ss [dimindex_lt_dimword])
604 \\ Q.SPECL_THEN [`\j. (w >> j) ' i`, `P`, `n`, `dimindex(:'a)`]
605 IMP_RES_TAC word_bv_lem
606 \\ DROPN_TAC 17
607 \\ FULL_SIMP_TAC arith_ss [Abbr `P`],
608 `!j. j < n ==> ~P j` by SRW_TAC [ARITH_ss] [Abbr `P`]
609 \\ ASM_SIMP_TAC arith_ss [ASR_LIMIT, word_bv_fold_zero]
610 \\ SRW_TAC [] [SIMP_RULE (srw_ss()) [] word_T, word_0]
611 ]
612QED
613
614Theorem fcp_or[local]:
615 !b g. $FCP f || $FCP g = $FCP (\i. f i \/ g i)
616Proof
617 SRW_TAC [fcpLib.FCP_ss] [word_or_def]
618QED
619
620Theorem word_asr_bv_expand[local]:
621 !w m.
622 word_asr_bv (w:'a word) m =
623 if dimindex(:'a) = 1 then
624 $FCP (K (w ' 0))
625 else
626 (FCP k.
627 FOLDL (\a j. a \/ ((LOG2 (dimindex(:'a) - 1) -- 0) m = n2w j) /\
628 (w >> j) ' k) F (COUNT_LIST (dimindex(:'a))) /\
629 ((dimindex(:'a) - 1 -- LOG2 (dimindex(:'a) - 1) + 1) m = 0w)) ||
630 ($FCP (K (n2w (dimindex(:'a) - 1) <+ m /\ word_msb w)))
631Proof
632 SRW_TAC [] [word_asr_bv_expand, fcp_or]
633 >| [
634 Cases_on `m`
635 \\ `(n = 0) \/ (n = 1)`
636 by Q.PAT_ASSUM `x = 1` (fn th => FULL_SIMP_TAC arith_ss [dimword_def,th])
637 \\ SRW_TAC [wordsLib.WORD_BIT_EQ_ss]
638 [wordsTheory.word_lo_n2w, COUNT_LIST_compute],
639 `1 < dimindex(:'a)` by SRW_TAC [] [DECIDE ``0n < n /\ n <> 1 ==> 1 < n``]
640 \\ ONCE_REWRITE_TAC [fcpTheory.CART_EQ]
641 \\ SRW_TAC [] [fcpTheory.FCP_BETA]
642 \\ METIS_TAC [arithmeticTheory.LESS_EQ_REFL, FOLDL_LOG2_INTRO]
643 ]
644QED
645
646Theorem word_asr_bv_expand =
647 SIMP_RULE std_ss [fcp_or, word_msb_def] word_asr_bv_expand
648
649Theorem word_ror_bv_expand:
650 !w m.
651 word_ror_bv (w:'a word) m =
652 FCP k.
653 FOLDL (\a j. a \/ (word_mod m (n2w (dimindex(:'a))) = n2w j) /\
654 w ' ((j + k) MOD dimindex(:'a))) F (COUNT_LIST (dimindex(:'a)))
655Proof
656 Cases_on `m`
657 \\ SRW_TAC [ARITH_ss] [word_mod_def, mod_dimindex, dimindex_lt_dimword]
658 \\ SRW_TAC [fcpLib.FCP_ss] [word_ror_bv_def, word_ror_def]
659 \\ Q.ABBREV_TAC `P = (\j. n MOD dimindex(:'a) = j MOD dimword(:'a))`
660 \\ `P (n MOD dimindex(:'a))` by SRW_TAC [] [Abbr `P`, mod_dimindex]
661 \\ `!i j. P i /\ P j /\ i < dimindex(:'a) /\ j < dimindex(:'a) ==> (i = j)`
662 by (SRW_TAC [] [Abbr `P`] \\ FULL_SIMP_TAC arith_ss [dimindex_lt_dimword])
663 \\ `n MOD dimindex(:'a) < dimindex(:'a)`
664 by SRW_TAC [] [DIMINDEX_GT_0, arithmeticTheory.MOD_LESS]
665 \\ Q.SPECL_THEN [`\j. w ' ((j + i) MOD dimindex(:'a))`, `P`,
666 `n MOD dimindex (:'a)`, `dimindex(:'a)`]
667 IMP_RES_TAC word_bv_lem
668 \\ DROPN_TAC 2
669 \\ FULL_SIMP_TAC std_ss [Abbr `P`, AC ADD_COMM ADD_ASSOC,
670 MOD_PLUS_RIGHT, DIMINDEX_GT_0]
671QED
672
673Theorem word_rol_bv_expand:
674 !w m.
675 word_rol_bv (w:'a word) m =
676 FCP k.
677 FOLDL
678 (\a j. a \/ (word_mod m (n2w (dimindex(:'a))) = n2w j) /\
679 w ' ((k + (dimindex(:'a) - j) MOD dimindex(:'a)) MOD dimindex(:'a)))
680 F (COUNT_LIST (dimindex(:'a)))
681Proof
682 Cases_on `m`
683 \\ SRW_TAC [ARITH_ss] [word_mod_def, mod_dimindex, dimindex_lt_dimword]
684 \\ SRW_TAC [fcpLib.FCP_ss] [word_rol_bv_def, word_rol_def, word_ror_def]
685 \\ Q.ABBREV_TAC `P = (\j. n MOD dimindex(:'a) = j MOD dimword(:'a))`
686 \\ `P (n MOD dimindex(:'a))` by SRW_TAC [] [Abbr `P`, mod_dimindex]
687 \\ `!i j. P i /\ P j /\ i < dimindex(:'a) /\ j < dimindex(:'a) ==> (i = j)`
688 by (SRW_TAC [] [Abbr `P`] \\ FULL_SIMP_TAC arith_ss [dimindex_lt_dimword])
689 \\ `n MOD dimindex(:'a) < dimindex(:'a)`
690 by SRW_TAC [] [DIMINDEX_GT_0, arithmeticTheory.MOD_LESS]
691 \\ Q.SPECL_THEN
692 [`\j. w ' ((i + (dimindex (:'a) - j) MOD dimindex (:'a))
693 MOD dimindex (:'a))`, `P`, `n MOD dimindex (:'a)`,
694 `dimindex(:'a)`] IMP_RES_TAC word_bv_lem
695 \\ DROPN_TAC 2
696 \\ FULL_SIMP_TAC std_ss [Abbr `P`, MOD_PLUS_RIGHT, DIMINDEX_GT_0]
697QED
698
699(* ------------------------------------------------------------------------- *)
700