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