1(* ========================================================================= *) 2(* FILE : alignmentScript.sml *) 3(* DESCRIPTION : Theory for address alignment. *) 4(* ========================================================================= *) 5 6open HolKernel Parse boolLib bossLib Q dep_rewrite 7open wordsLib 8 9val () = new_theory "alignment"; 10 11val ERR = mk_HOL_ERR "alignmentScript" 12 13(* ------------------------------------------------------------------------- 14 Constant definitions 15 ------------------------------------------------------------------------- *) 16 17val align_def = Define `align p (w: 'a word) = (dimindex (:'a) - 1 '' p) w` 18val aligned_def = Define `aligned p w = (align p w = w)` 19 20val byte_align_def = Define` 21 byte_align (w: 'a word) = align (LOG2 (dimindex(:'a) DIV 8)) w` 22 23val byte_aligned_def = Define` 24 byte_aligned (w: 'a word) = aligned (LOG2 (dimindex(:'a) DIV 8)) w` 25 26(* ------------------------------------------------------------------------- 27 Theorems 28 ------------------------------------------------------------------------- *) 29 30val align_0 = Q.store_thm("align_0", 31 `!w. align 0 w = w`, 32 lrw [wordsTheory.WORD_SLICE_BITS_THM, wordsTheory.WORD_ALL_BITS, align_def] 33 ) 34 35val align_align = Q.store_thm("align_align", 36 `!p w. align p (align p w) = align p w`, 37 srw_tac [wordsLib.WORD_BIT_EQ_ss, boolSimps.CONJ_ss] [align_def] 38 ) 39 40val aligned_align = Q.store_thm ("aligned_align", 41 `!p w. aligned p (align p w)`, 42 rewrite_tac [aligned_def, align_align] 43 ) 44 45val align_aligned = Q.store_thm ("align_aligned", 46 `!p w. aligned p w ==> (align p w = w)`, 47 rewrite_tac [aligned_def] 48 ) 49 50val align_bitwise_and = Q.store_thm("align_bitwise_and", 51 `!p w. align p w = w && UINT_MAXw << p`, 52 srw_tac [wordsLib.WORD_BIT_EQ_ss] [align_def] 53 \\ decide_tac 54 ) 55 56val align_shift = Q.store_thm("align_shift", 57 `!p w. align p w = w >>> p << p`, 58 srw_tac [wordsLib.WORD_BIT_EQ_ss] [align_def] 59 \\ Cases_on `p <= i` 60 \\ simp [] 61 ) 62 63val align_w2n = Q.store_thm("align_w2n", 64 `!p w. align p w = n2w (w2n w DIV 2 ** p * 2 ** p)`, 65 strip_tac 66 \\ Cases 67 \\ lrw [align_shift, GSYM wordsTheory.n2w_DIV, wordsTheory.word_lsl_n2w, 68 wordsTheory.dimword_def] 69 \\ `dimindex(:'a) <= p` by decide_tac 70 \\ imp_res_tac arithmeticTheory.LESS_EQUAL_ADD 71 \\ simp [arithmeticTheory.EXP_ADD, arithmeticTheory.MOD_EQ_0] 72 ) 73 74val ths = [GSYM wordsTheory.WORD_w2w_EXTRACT, wordsTheory.w2w_id] 75 76val lem = 77 wordsTheory.EXTRACT_JOIN_ADD 78 |> Thm.INST_TYPE [Type.beta |-> Type.alpha] 79 |> Q.SPECL [`dimindex(:'a) - 1`, `p - 1`, `p`, `0`, `p`, `w`] 80 |> Q.DISCH `0 < p` 81 |> SIMP_RULE (srw_ss()) (DECIDE ``0 < p ==> (p = p - 1 + 1)`` :: ths) 82 |> GSYM 83 84val align_sub = Q.store_thm("align_sub", 85 `!p w. align p w = if p = 0 then w else w - (p - 1 >< 0) w`, 86 rw_tac bool_ss [align_0] 87 \\ Cases_on `dimindex(:'a) <= p - 1` 88 >- ( 89 `(p - 1 >< 0) w : 'a word = (dimindex (:'a) - 1 >< 0) w` 90 by simp [wordsTheory.WORD_EXTRACT_MIN_HIGH] 91 \\ rule_assum_tac (SIMP_RULE (srw_ss()) ths) 92 \\ asm_rewrite_tac [] 93 \\ srw_tac [wordsLib.WORD_BIT_EQ_ss] [align_def] 94 ) 95 \\ Cases_on `p = dimindex(:'a)` 96 >- srw_tac [wordsLib.WORD_BIT_EQ_ss] (align_def :: ths) 97 \\ `0 < p /\ p <= dimindex (:'a) - 1` by decide_tac 98 \\ imp_res_tac lem 99 \\ pop_assum (qspec_then `w` (CONV_TAC o Conv.PATH_CONV "rlr" o Lib.K)) 100 \\ srw_tac [wordsLib.WORD_EXTRACT_ss] [align_def] 101 ) 102 103Theorem aligned_extract: 104 !p w. aligned p (w: 'a word) <=> (p = 0) \/ ((p - 1 >< 0) w = 0w: 'a word) 105Proof 106 rewrite_tac [aligned_def] 107 \\ Cases 108 >- rewrite_tac [align_0] 109 \\ srw_tac [wordsLib.WORD_BIT_EQ_ss] [align_def] 110 \\ eq_tac 111 \\ lrw [] 112 \\ res_tac 113 \\ Cases_on `i <= n` 114 \\ Cases_on `w ' i` 115 \\ fs [] 116 \\ decide_tac 117QED 118 119val aligned_0 = Q.store_thm ("aligned_0", 120 `(!p. aligned p 0w) /\ (!w. aligned 0 w)`, 121 srw_tac [wordsLib.WORD_BIT_EQ_ss] [aligned_extract] 122 ) 123 124val aligned_1_lsb = Q.store_thm ("aligned_1_lsb", 125 `!w. aligned 1 w = ~word_lsb w`, 126 srw_tac [wordsLib.WORD_BIT_EQ_ss] [aligned_extract] 127 ) 128 129val aligned_ge_dim = Q.store_thm ("aligned_ge_dim", 130 `!p w:'a word. dimindex(:'a) <= p ==> (aligned p w = (w = 0w))`, 131 Cases \\ srw_tac [wordsLib.WORD_BIT_EQ_ss] [aligned_extract] 132 ) 133 134val aligned_bitwise_and = Q.store_thm("aligned_bitwise_and", 135 `!p w. aligned p (w: 'a word) = (w && n2w (2 ** p - 1) = 0w)`, 136 simp [aligned_def, align_bitwise_and] 137 \\ srw_tac [wordsLib.WORD_BIT_EQ_ss] 138 [wordsTheory.word_index, bitTheory.BIT_EXP_SUB1] 139 \\ eq_tac 140 \\ lrw [] 141 \\ res_tac 142 \\ Cases_on `i < SUC n` 143 \\ Cases_on `w ' i` 144 \\ fs [] 145 \\ decide_tac 146 ) 147 148val aligned_bit_count_upto = Q.store_thm ("aligned_bit_count_upto", 149 `!p w. 150 aligned p (w: 'a word) = (bit_count_upto (MIN (dimindex(:'a)) p) w = 0)`, 151 lrw [aligned_extract, wordsTheory.bit_count_upto_is_zero] 152 \\ srw_tac [wordsLib.WORD_BIT_EQ_ss] [] 153 \\ Cases_on `p = 0` 154 \\ simp [] 155 \\ eq_tac 156 \\ lrw [] 157 \\ res_tac 158 >- decide_tac 159 \\ Cases_on `i < p` 160 \\ fs [] 161 \\ decide_tac 162 ) 163 164val aligned_add_sub = Q.store_thm("aligned_add_sub", 165 `!p a: 'a word b. 166 aligned p b ==> 167 (aligned p (a + b) = aligned p a) /\ 168 (aligned p (a - b) = aligned p a)`, 169 strip_tac 170 \\ Cases_on `dimindex(:'a) <= p` 171 >- simp [aligned_ge_dim] 172 \\ `p < dimindex(:'a)` by decide_tac 173 \\ Cases_on `p` 174 \\ simp [aligned_extract] 175 \\ Cases_on `SUC n = dimindex(:'a)` 176 \\ srw_tac [wordsLib.WORD_EXTRACT_ss] [] 177 \\ simp [Once (GSYM wordsTheory.WORD_EXTRACT_OVER_ADD2), 178 Once (GSYM wordsTheory.WORD_EXTRACT_OVER_MUL2)] 179 \\ lrw [wordsTheory.WORD_EXTRACT_COMP_THM, arithmeticTheory.MIN_DEF] 180 \\ metis_tac [arithmeticTheory.SUC_SUB1] 181 ) 182 183val aligned_add_sub_cor = Q.store_thm("aligned_add_sub_cor", 184 `!p a: 'a word b. 185 aligned p a /\ aligned p b ==> aligned p (a + b) /\ aligned p (a - b)`, 186 metis_tac [aligned_add_sub] 187 ) 188 189val aligned_mul_shift_1 = Q.store_thm ("aligned_mul_shift_1", 190 `!p w: 'a word. aligned p (1w << p * w)`, 191 strip_tac 192 \\ Cases_on `dimindex(:'a) <= p` 193 >- simp [aligned_ge_dim] 194 \\ `p < dimindex(:'a)` by decide_tac 195 \\ Cases_on `p` 196 \\ srw_tac [ARITH_ss] 197 [aligned_extract, 198 Once (GSYM wordsTheory.WORD_EXTRACT_OVER_MUL2)] 199 \\ `(n >< 0) ((1w:'a word) << SUC n) = 0w: 'a word` 200 by lrw [wordsTheory.WORD_MUL_LSL, wordsTheory.word_extract_n2w, 201 arithmeticTheory.MIN_DEF, 202 bitTheory.BITS_SUM2 203 |> Q.SPECL [`n`, `0`, `1`, `0`] 204 |> SIMP_RULE (srw_ss()) []] 205 \\ simp [wordsTheory.WORD_EXTRACT_COMP_THM, arithmeticTheory.MIN_DEF] 206 ) 207 208val aligned_add_sub_prod = Q.store_thm("aligned_add_sub_prod", 209 `!p w: 'a word x. 210 (aligned p (w + (1w << p) * x) = aligned p w) /\ 211 (aligned p (w - (1w << p) * x) = aligned p w)`, 212 metis_tac [aligned_add_sub, aligned_mul_shift_1, wordsTheory.WORD_ADD_COMM] 213 ) 214 215val aligned_imp = Q.store_thm("aligned_imp", 216 `!p q w. p < q /\ aligned q w ==> aligned p w`, 217 srw_tac [wordsLib.WORD_BIT_EQ_ss] [aligned_extract] 218 >- fs [] 219 \\ Cases_on `p` 220 \\ lrw [] 221 \\ res_tac 222 \\ simp [] 223 ) 224 225val align_add_aligned = Q.store_thm("align_add_aligned", 226 `!p a b : 'a word. 227 aligned p a /\ w2n b < 2 ** p ==> (align p (a + b) = a)`, 228 strip_tac 229 \\ Cases_on `dimindex(:'a) <= p` 230 >- (`w2n b < 2 ** p` 231 by metis_tac [wordsTheory.w2n_lt, wordsTheory.dimword_def, 232 bitTheory.TWOEXP_MONO2, arithmeticTheory.LESS_LESS_EQ_TRANS] 233 \\ simp [aligned_ge_dim, align_w2n, arithmeticTheory.LESS_DIV_EQ_ZERO]) 234 \\ fs [arithmeticTheory.NOT_LESS_EQUAL] 235 \\ rw [aligned_extract, align_sub, wordsTheory.WORD_EXTRACT_COMP_THM, 236 arithmeticTheory.MIN_DEF, 237 Once (GSYM wordsTheory.WORD_EXTRACT_OVER_ADD2), 238 wordsTheory.WORD_EXTRACT_ID 239 |> Q.SPECL [`w`, `p - 1`] 240 |> Q.DISCH `p <> 0n` 241 |> SIMP_RULE std_ss [DECIDE ``p <> 0n ==> (SUC (p - 1) = p)``] 242 ] 243 \\ fs [DECIDE ``(a < 1n) = (a = 0n)``, wordsTheory.w2n_eq_0] 244 ) 245 246Theorem lt_align_eq_0: 247 w2n a < 2 ** p ==> (align p a = 0w) 248Proof 249 Cases_on`a` \\ fs[] 250 \\ rw[align_w2n] 251 \\ Cases_on`p = 0` \\ fs[] 252 \\ `1 < 2 ** p` by fs[arithmeticTheory.ONE_LT_EXP] 253 \\ `n DIV 2 ** p = 0` by fs[arithmeticTheory.DIV_EQ_0] 254 \\ fs[] 255QED 256 257Theorem aligned_or: 258 aligned n (w || v) <=> aligned n w /\ aligned n v 259Proof 260 Cases_on `n = 0` 261 \\ srw_tac [WORD_BIT_EQ_ss] [aligned_extract] 262 \\ metis_tac [] 263QED 264 265Theorem aligned_w2n: 266 aligned k w <=> (w2n (w:'a word) MOD 2 ** k = 0) 267Proof 268 Cases_on `w` 269 \\ fs [aligned_def,align_w2n] 270 \\ `0n < 2 ** k` by simp [] 271 \\ drule arithmeticTheory.DIVISION 272 \\ disch_then (qspec_then `n` assume_tac) 273 \\ `(n DIV 2 ** k * 2 ** k) < dimword (:'a)` by decide_tac 274 \\ asm_simp_tac std_ss [] \\ decide_tac 275QED 276 277Theorem MOD_0_aligned: 278 !n p. (n MOD 2 ** p = 0) ==> aligned p (n2w n) 279Proof 280 fs [aligned_bitwise_and] 281 \\ once_rewrite_tac [wordsTheory.WORD_AND_COMM] 282 \\ fs [wordsTheory.WORD_AND_EXP_SUB1] 283QED 284 285Theorem aligned_lsl_leq: 286 k <= l ==> aligned k (w << l) 287Proof 288 fs [aligned_def,align_def] 289 \\ fs [fcpTheory.CART_EQ,wordsTheory.word_lsl_def, 290 wordsTheory.word_slice_def,fcpTheory.FCP_BETA] 291 \\ rw [] \\ eq_tac \\ fs [] 292QED 293 294Theorem aligned_lsl[simp]: 295 aligned k (w << k) 296Proof match_mp_tac aligned_lsl_leq \\ fs[] 297QED 298 299Theorem align_align_MAX: 300 !k l w. align k (align l w) = align (MAX k l) w 301Proof 302 fs[align_def,fcpTheory.CART_EQ,wordsTheory.word_slice_def,fcpTheory.FCP_BETA] 303 \\ rw [] \\ eq_tac \\ fs [] 304QED 305 306Theorem pow2_eq_0: 307 dimindex (:'a) <= k ==> (n2w (2 ** k) = 0w:'a word) 308Proof 309 fs [wordsTheory.dimword_def] \\ fs [arithmeticTheory.LESS_EQ_EXISTS] 310 \\ rw [] \\ fs [arithmeticTheory.EXP_ADD,arithmeticTheory.MOD_EQ_0] 311QED 312 313Theorem aligned_pow2: 314 aligned k (n2w (2 ** k)) 315Proof 316 Cases_on `k < dimindex (:'a)` 317 \\ fs [arithmeticTheory.NOT_LESS,pow2_eq_0,aligned_0] 318 \\ `2 ** k < dimword (:'a)` by fs [wordsTheory.dimword_def] 319 \\ fs [aligned_def,align_w2n] 320QED 321 322Theorem word_msb_align: 323 p < dimindex(:'a) ==> (word_msb (align p w) = word_msb (w:'a word)) 324Proof 325 rw[align_bitwise_and,wordsTheory.word_msb] 326 \\ rw[wordsTheory.word_bit_and] 327 \\ rw[wordsTheory.word_bit_lsl] 328 \\ rw[wordsTheory.word_bit_test, 329 arithmeticTheory.MOD_EQ_0_DIVISOR, 330 wordsTheory.dimword_def] 331QED 332 333Theorem align_ls: 334 align p n <=+ n 335Proof 336 simp[wordsTheory.WORD_LS] 337 \\ Cases_on`n` 338 \\ fs[align_w2n] 339 \\ qmatch_asmsub_rename_tac`n < _` 340 \\ DEP_REWRITE_TAC[arithmeticTheory.LESS_MOD] 341 \\ conj_asm2_tac >- fs[] 342 \\ DEP_REWRITE_TAC[GSYM arithmeticTheory.X_LE_DIV] 343 \\ simp[] 344QED 345 346Theorem align_lo: 347 ~aligned p n ==> align p n <+ n 348Proof 349 simp[wordsTheory.WORD_LO] 350 \\ Cases_on`n` 351 \\ fs[align_w2n, aligned_def] 352 \\ strip_tac 353 \\ qmatch_goalsub_abbrev_tac`a < b` 354 \\ `a <= b` suffices_by fs[] 355 \\ qmatch_asmsub_rename_tac`n < _` 356 \\ simp[Abbr`a`] 357 \\ DEP_REWRITE_TAC[arithmeticTheory.LESS_MOD] 358 \\ conj_asm2_tac >- fs[] 359 \\ DEP_REWRITE_TAC[GSYM arithmeticTheory.X_LE_DIV] 360 \\ simp[] 361QED 362 363Theorem aligned_between: 364 ~aligned p n /\ aligned p m /\ align p n <+ m ==> n <+ m 365Proof 366 rw[wordsTheory.WORD_LO] 367 \\ fs[align_w2n, aligned_def] 368 \\ Cases_on`n` \\ Cases_on`m` \\ fs[] 369 \\ CCONTR_TAC \\ fs[arithmeticTheory.NOT_LESS] 370 \\ qmatch_asmsub_abbrev_tac`n DIV d * d` 371 \\ `n DIV d * d <= n` by ( 372 DEP_REWRITE_TAC[GSYM arithmeticTheory.X_LE_DIV] \\ fs[Abbr`d`] ) 373 \\ fs[] 374 \\ qmatch_asmsub_rename_tac`(d * (m DIV d)) MOD _` 375 \\ `m DIV d * d <= m` by ( 376 DEP_REWRITE_TAC[GSYM arithmeticTheory.X_LE_DIV] \\ fs[Abbr`d`] ) 377 \\ fs[] 378 \\ `d * (n DIV d) <= m` by metis_tac[] 379 \\ pop_assum mp_tac 380 \\ simp_tac pure_ss [Once arithmeticTheory.MULT_COMM] 381 \\ DEP_REWRITE_TAC[GSYM arithmeticTheory.X_LE_DIV] 382 \\ conj_tac >- simp[Abbr`d`] 383 \\ simp[arithmeticTheory.NOT_LESS_EQUAL] 384 \\ `d * (m DIV d) < d * (n DIV d)` suffices_by fs[] 385 \\ metis_tac[] 386QED 387 388local 389 val aligned_add_mult_lemma = Q.prove( 390 `aligned k (w + n2w (2 ** k)) = aligned k w`, 391 fs [aligned_add_sub,aligned_pow2]) |> GEN_ALL 392 val aligned_add_mult_any = Q.prove( 393 `!n w. aligned k (w + n2w (n * 2 ** k)) = aligned k w`, 394 Induct \\ fs [arithmeticTheory.MULT_CLAUSES, 395 GSYM wordsTheory.word_add_n2w] 396 \\ rw [] 397 \\ pop_assum (qspec_then `w + n2w (2 ** k)` mp_tac) 398 \\ fs [aligned_add_mult_lemma]) |> GEN_ALL 399in 400 val aligned_add_pow = save_thm("aligned_add_pow[simp]", 401 CONJ aligned_add_mult_lemma aligned_add_mult_any) 402end 403 404Theorem align_add_aligned_gen: 405 !a. aligned p a ==> (align p (a + b) = a + align p b) 406Proof 407 completeInduct_on`w2n b` 408 \\ rw[] 409 \\ Cases_on`w2n b < 2 ** p` 410 >- ( 411 simp[align_add_aligned] 412 \\ `align p b = 0w` by simp[lt_align_eq_0] 413 \\ simp[] ) 414 \\ fs[arithmeticTheory.NOT_LESS] 415 \\ Cases_on`w2n b = 2 ** p` 416 >- ( 417 `aligned p b` by( 418 simp[aligned_def,align_w2n] 419 \\ metis_tac[wordsTheory.n2w_w2n] ) 420 \\ `aligned p (a + b)` by metis_tac[aligned_add_sub_cor] 421 \\ fs[aligned_def]) 422 \\ fs[arithmeticTheory.LESS_EQ_EXISTS] 423 \\ qmatch_asmsub_rename_tac`w2n b = z + _` 424 \\ first_x_assum(qspec_then`z`mp_tac) 425 \\ impl_keep_tac >- fs[] 426 \\ `z < dimword(:'a)` by metis_tac[wordsTheory.w2n_lt, arithmeticTheory.LESS_TRANS] 427 \\ disch_then(qspec_then`n2w z`mp_tac) 428 \\ impl_tac >- simp[] 429 \\ strip_tac 430 \\ first_assum(qspec_then`a + n2w (2 ** p)`mp_tac) 431 \\ impl_tac >- fs[] 432 \\ rewrite_tac[wordsTheory.word_add_n2w, GSYM wordsTheory.WORD_ADD_ASSOC] 433 \\ Cases_on`b` \\ fs[GSYM wordsTheory.word_add_n2w] 434 \\ strip_tac 435 \\ first_x_assum(qspec_then`n2w (2**p)`mp_tac) 436 \\ impl_tac >- fs[aligned_w2n] 437 \\ simp[] 438QED 439 440Theorem byte_align_aligned: 441 byte_aligned x <=> (byte_align x = x) 442Proof EVAL_TAC 443QED 444 445Theorem byte_aligned_add: 446 byte_aligned x /\ byte_aligned y ==> byte_aligned (x+y) 447Proof 448 rw[byte_aligned_def] 449 \\ metis_tac[aligned_add_sub_cor] 450QED 451 452(* ------------------------------------------------------------------------- 453 Theorems for standard alignment lengths of 1, 2 and 3 bits 454 ------------------------------------------------------------------------- *) 455 456fun f p = 457 let 458 val th1 = 459 aligned_add_sub_prod 460 |> Q.SPEC p 461 |> SIMP_RULE std_ss [fcpTheory.DIMINDEX_GE_1, wordsTheory.word_1_lsl] 462 val th2 = th1 |> Q.SPEC `0w` |> SIMP_RULE (srw_ss()) [aligned_0] 463 in 464 [th1, th2] 465 end 466 467val aligned_add_sub_123 = save_thm ("aligned_add_sub_123", 468 LIST_CONJ (List.concat (List.map f [`1`, `2`, `3`])) 469 ) 470 471local 472 val bit_lem = Q.prove( 473 `(!x. NUMERAL (BIT2 x) = 2 * (x + 1)) /\ 474 (!x. NUMERAL (BIT1 x) = 2 * x + 1) /\ 475 (!x. NUMERAL (BIT1 (BIT1 x)) = 4 * x + 3) /\ 476 (!x. NUMERAL (BIT1 (BIT2 x)) = 4 * (x + 1) + 1) /\ 477 (!x. NUMERAL (BIT2 (BIT1 x)) = 4 * (x + 1)) /\ 478 (!x. NUMERAL (BIT2 (BIT2 x)) = 4 * (x + 1) + 2) /\ 479 (!x. NUMERAL (BIT1 (BIT1 (BIT1 x))) = 8 * x + 7) /\ 480 (!x. NUMERAL (BIT1 (BIT1 (BIT2 x))) = 8 * (x + 1) + 3) /\ 481 (!x. NUMERAL (BIT1 (BIT2 (BIT1 x))) = 8 * (x + 1) + 1) /\ 482 (!x. NUMERAL (BIT1 (BIT2 (BIT2 x))) = 8 * (x + 1) + 5) /\ 483 (!x. NUMERAL (BIT2 (BIT1 (BIT1 x))) = 8 * (x + 1)) /\ 484 (!x. NUMERAL (BIT2 (BIT1 (BIT2 x))) = 8 * (x + 1) + 4) /\ 485 (!x. NUMERAL (BIT2 (BIT2 (BIT1 x))) = 8 * (x + 1) + 2) /\ 486 (!x. NUMERAL (BIT2 (BIT2 (BIT2 x))) = 8 * (x + 1) + 6)`, 487 REPEAT strip_tac 488 \\ CONV_TAC (Conv.LHS_CONV 489 (REWRITE_CONV [arithmeticTheory.BIT1, arithmeticTheory.BIT2, 490 arithmeticTheory.NUMERAL_DEF])) 491 \\ decide_tac 492 ) 493 val (_, _, dest_num, _) = HolKernel.syntax_fns1 "arithmetic" "NUMERAL" 494in 495 fun bit_lem_conv tm = 496 let 497 val x = dest_num (fst (wordsSyntax.dest_n2w tm)) 498 in 499 if List.null (Term.free_vars x) 500 then raise ERR "bit_lem_conv" "" 501 else Conv.RAND_CONV (ONCE_REWRITE_CONV [bit_lem]) tm 502 end 503end 504 505val aligned_numeric = Q.store_thm("aligned_numeric", 506 `(!x. aligned 3 (n2w (NUMERAL (BIT2 (BIT1 (BIT1 x)))))) /\ 507 (!x. aligned 2 (n2w (NUMERAL (BIT2 (BIT1 x))))) /\ 508 (!x. aligned 1 (n2w (NUMERAL (BIT2 x)))) /\ 509 (!x. aligned 3 (-n2w (NUMERAL (BIT2 (BIT1 (BIT1 x)))))) /\ 510 (!x. aligned 2 (-n2w (NUMERAL (BIT2 (BIT1 x))))) /\ 511 (!x. aligned 1 (-n2w (NUMERAL (BIT2 x)))) /\ 512 (!x y f. aligned 3 (y + n2w (NUMERAL (BIT1 (BIT1 (BIT1 (f x)))))) = 513 aligned 3 (y + 7w)) /\ 514 (!x y f. aligned 3 (y + n2w (NUMERAL (BIT1 (BIT1 (BIT2 x))))) = 515 aligned 3 (y + 3w)) /\ 516 (!x y f. aligned 3 (y + n2w (NUMERAL (BIT1 (BIT2 (BIT1 x))))) = 517 aligned 3 (y + 1w)) /\ 518 (!x y f. aligned 3 (y + n2w (NUMERAL (BIT1 (BIT2 (BIT2 x))))) = 519 aligned 3 (y + 5w)) /\ 520 (!x y f. aligned 3 (y + n2w (NUMERAL (BIT2 (BIT1 (BIT1 x))))) = 521 aligned 3 (y)) /\ 522 (!x y f. aligned 3 (y + n2w (NUMERAL (BIT2 (BIT1 (BIT2 x))))) = 523 aligned 3 (y + 4w)) /\ 524 (!x y f. aligned 3 (y + n2w (NUMERAL (BIT2 (BIT2 (BIT1 x))))) = 525 aligned 3 (y + 2w)) /\ 526 (!x y f. aligned 3 (y + n2w (NUMERAL (BIT2 (BIT2 (BIT2 x))))) = 527 aligned 3 (y + 6w)) /\ 528 (!x y f. aligned 3 (y - n2w (NUMERAL (BIT1 (BIT1 (BIT1 (f x)))))) = 529 aligned 3 (y - 7w)) /\ 530 (!x y f. aligned 3 (y - n2w (NUMERAL (BIT1 (BIT1 (BIT2 x))))) = 531 aligned 3 (y - 3w)) /\ 532 (!x y f. aligned 3 (y - n2w (NUMERAL (BIT1 (BIT2 (BIT1 x))))) = 533 aligned 3 (y - 1w)) /\ 534 (!x y f. aligned 3 (y - n2w (NUMERAL (BIT1 (BIT2 (BIT2 x))))) = 535 aligned 3 (y - 5w)) /\ 536 (!x y f. aligned 3 (y - n2w (NUMERAL (BIT2 (BIT1 (BIT1 x))))) = 537 aligned 3 (y)) /\ 538 (!x y f. aligned 3 (y - n2w (NUMERAL (BIT2 (BIT1 (BIT2 x))))) = 539 aligned 3 (y - 4w)) /\ 540 (!x y f. aligned 3 (y - n2w (NUMERAL (BIT2 (BIT2 (BIT1 x))))) = 541 aligned 3 (y - 2w)) /\ 542 (!x y f. aligned 3 (y - n2w (NUMERAL (BIT2 (BIT2 (BIT2 x))))) = 543 aligned 3 (y - 6w)) /\ 544 (!x y f. aligned 2 (y + n2w (NUMERAL (BIT1 (BIT1 (f x))))) = 545 aligned 2 (y + 3w)) /\ 546 (!x y. aligned 2 (y + n2w (NUMERAL (BIT1 (BIT2 x)))) = 547 aligned 2 (y + 1w)) /\ 548 (!x y. aligned 2 (y + n2w (NUMERAL (BIT2 (BIT1 x)))) = 549 aligned 2 (y)) /\ 550 (!x y. aligned 2 (y + n2w (NUMERAL (BIT2 (BIT2 x)))) = 551 aligned 2 (y + 2w)) /\ 552 (!x y f. aligned 2 (y - n2w (NUMERAL (BIT1 (BIT1 (f x))))) = 553 aligned 2 (y - 3w)) /\ 554 (!x y. aligned 2 (y - n2w (NUMERAL (BIT1 (BIT2 x)))) = 555 aligned 2 (y - 1w)) /\ 556 (!x y. aligned 2 (y - n2w (NUMERAL (BIT2 (BIT1 x)))) = 557 aligned 2 (y)) /\ 558 (!x y. aligned 2 (y - n2w (NUMERAL (BIT2 (BIT2 x)))) = 559 aligned 2 (y - 2w)) /\ 560 (!x y f. aligned 1 (y + n2w (NUMERAL (BIT1 (f x)))) = 561 aligned 1 (y + 1w)) /\ 562 (!x y f. aligned 1 (y - n2w (NUMERAL (BIT1 (f x)))) = 563 aligned 1 (y - 1w)) /\ 564 (!x y. aligned 1 (y + n2w (NUMERAL (BIT2 x))) = aligned 1 y) /\ 565 (!x y. aligned 1 (y - n2w (NUMERAL (BIT2 x))) = aligned 1 y)`, 566 REPEAT strip_tac 567 \\ CONV_TAC (DEPTH_CONV bit_lem_conv) 568 \\ rewrite_tac 569 [GSYM wordsTheory.word_mul_n2w, GSYM wordsTheory.word_add_n2w, 570 wordsLib.WORD_DECIDE ``a + (b * c + d) : 'a word = (a + d) + b * c``, 571 wordsLib.WORD_DECIDE ``a - (b * c + d) : 'a word = (a - d) - b * c``, 572 wordsTheory.WORD_NEG_LMUL, aligned_add_sub_123] 573 ) 574 575(* ------------------------------------------------------------------------- *) 576 577val () = export_theory () 578