1(* app load ["bitsLib","bitsTheory","word32Theory"]; *) 2open bitsLib simpLib HolKernel boolLib bossLib Parse Q arithmeticTheory whileTheory bitsTheory word32Theory; 3 4val _ = type_abbrev("word", ``:word32``); 5 6val std_ss = std_ss ++ boolSimps.LET_ss; 7val arith_ss = arith_ss ++ boolSimps.LET_ss; 8 9(* -------------------------------------------------------- *) 10(* WL must be even *) 11 12val WL_EVEN = prove( 13 `WL MOD 2 = 0`, 14 SIMP_TAC arith_ss [WL_def,HB_def] 15); 16 17(* -------------------------------------------------------- *) 18 19val _ = new_theory "booth"; 20 21(* -------------------------------------------------------- *) 22 23val _ = Hol_datatype `state_BOOTH = BOOTH of num=>num=>bool=>num=>word=>word`; 24(* mul,mul2,borrow2,mshift,rm,rd *) 25 26(* -------------------------------------------------------- *) 27 28val MOD_CNTW_def = Define `MOD_CNTW n = n MOD (WL DIV 2)`; 29 30(* -------------------------------------------------------- *) 31 32 33 34val MSHIFT_def = Define` 35 MSHIFT borrow mul count1 = 36 count1 * 2 + 37 if borrow /\ (mul = 1) \/ ~borrow /\ (mul = 2) then 1 else 0`; 38 39val ALU_def = Define` 40 ALU borrow2 mul alua alub = 41 if ~borrow2 /\ (mul = 0) \/ borrow2 /\ (mul = 3) then 42 alua 43 else if borrow2 /\ (mul = 0) \/ (mul = 1) then 44 alua + alub 45 else 46 alua - alub`; 47 48val INIT_def = Define` 49 INIT a rm rs rn = 50 let mul1 = w2n rs 51 and alub = rn 52 and borrow = F 53 and count1 = 0 in 54 let rd = if a then alub else 0w 55 and borrow2 = borrow 56 and mul = BITS 1 0 mul1 57 and mul2 = BITS HB 2 mul1 in 58 let mshift = if mul = 2 then 1 else 0 in 59 BOOTH mul mul2 borrow2 mshift rm rd`; 60 61val INIT = save_thm("INIT",SIMP_RULE std_ss [GSYM WORD_BITS_def] INIT_def); 62 63val NEXT_def = Define` 64 NEXT (BOOTH mul mul2 borrow2 mshift rm rd) = 65 let mul1 = BITS (HB - 2) 0 mul2 66 and alub = rm << mshift 67 and alua = rd 68 and borrow = BIT 1 mul 69 and count1 = MOD_CNTW (mshift DIV 2 + 1) in 70 let rd' = ALU borrow2 mul alua alub 71 and borrow2' = borrow 72 and mul' = BITS 1 0 mul1 73 and mul2' = BITS HB 2 mul1 in 74 let mshift' = MSHIFT borrow mul' count1 75 in 76 BOOTH mul' mul2' borrow2' mshift' rm rd'`; 77 78val NEXT = save_thm("NEXT",SIMP_RULE std_ss [] NEXT_def); 79 80val STATE_def = Define` 81 (STATE 0 a rm rs rn = INIT a rm rs rn) /\ 82 (STATE (SUC t) a rm rs rn = NEXT (STATE t a rm rs rn))`; 83 84(* -------------------------------------------------------- *) 85 86val BORROW2_def = Define` 87 BORROW2 rs n = ~(n = 0) /\ WORD_BIT (2 * n - 1) rs`; 88 89(* 90val DONE_def = Define` 91 DONE rs n = (WORD_BITS HB (2 * n) rs = 0) /\ ~BORROW2 rs n \/ ~(2 * n < WL)`; 92 93With the ARM6, 1 cycle is taken in the rs = word_0 case. This is used for CPSR update. 94*) 95 96val DONE_def = Define` 97 DONE rs n = ~(n = 0) /\ (WORD_BITS HB (2 * n) rs = 0) /\ ~BORROW2 rs n \/ ~(2 * n < WL)`; 98 99val DUR_def = Define`DUR rs = LEAST n. DONE rs n`; 100 101val PROJ_RD_def = Define` 102 PROJ_RD (BOOTH mul mul2 borrow2 mshift rm rd) = rd`; 103 104val BOOTHMULTIPLY_def = Define` 105 BOOTHMULTIPLY a rm rs rn = PROJ_RD (STATE (DUR rs) a rm rs rn)`; 106 107(* -------------------------------------------------------- *) 108 109(* 110 and mulz = (BITS (HB - 2) 0 mul2 = 0 in 111 let mulx = (mulz /\ ~borrow) \/ (BITS CNTW 1 mshift = 15) in 112*) 113 114val INVARIANT_def = Define` 115 INVARIANT a rm rs rn n = 116 let mul = BITS 1 0 (WORD_BITS HB (2 * n) rs) 117 and mul2 = WORD_BITS HB (2 * (n + 1)) rs 118 and borrow2 = BORROW2 rs n in 119 BOOTH mul mul2 borrow2 120 (2 * (MOD_CNTW n) + if borrow2 /\ (mul = 1) \/ 121 ~borrow2 /\ (mul = 2) then 1 else 0) 122 rm ((if borrow2 then 123 rm * n2w (w2n rs MOD 2 ** (2 * n)) - rm << (2 * n) 124 else 125 rm * n2w (w2n rs MOD 2 ** (2 * n))) + (if a then rn else 0w))`; 126 127val INVARIANT = save_thm("INVARIANT",SIMP_RULE std_ss [] INVARIANT_def); 128 129(* -------------------------------------------------------- *) 130 131val MIN_HB_1 = prove( 132 `MIN HB 1 = 1`, 133 SIMP_TAC arith_ss [MIN_DEF,HB_def] 134); 135 136val MOD_4_BITS = prove( 137 `!a. a MOD 4 = BITS 1 0 a`, 138 SIMP_TAC arith_ss [BITS_ZERO3] 139); 140 141val w2n_DIV_THM = prove( 142 `!n rs. w2n rs DIV 2 ** n = WORD_BITS HB n rs`, 143 REPEAT STRIP_TAC 144 THEN STRUCT_CASES_TAC (SPEC `rs` word_nchotomy) 145 THEN SIMP_TAC arith_ss [BITS_COMP_THM2,MIN_DEF,WORD_BITS_def,w2n_EVAL,MOD_WL_THM,BITS_DIV_THM] 146); 147 148val w2n_DIV_4 = (numLib.REDUCE_RULE o SPEC `2`) w2n_DIV_THM; 149 150val MIN_LEM = prove( 151 `(!x t. MIN x (x - 2 + 2 * (t + 1)) = x) /\ 152 (!x t. MIN x (x + 2 * (t + 1)) = x)`, 153 RW_TAC arith_ss [MIN_DEF] 154); 155 156val TWO_T_PLUS_TWO = DECIDE ``!t. 2 * (t + 1) + 2 = 2 * (t + 2)``; 157 158val BORROW2 = prove( 159 `!n rs. BORROW2 rs n = ~(n = 0) /\ BIT 1 (w2n rs DIV 2 ** (2 * (n - 1)))`, 160 Cases THEN SIMP_TAC arith_ss [BORROW2_def] 161 THEN SIMP_TAC arith_ss [WORD_BIT_def,ADD1,BIT_def,BITS_THM,DIV_DIV_DIV_MULT, 162 ZERO_LT_TWOEXP,LEFT_ADD_DISTRIB] 163 THEN SIMP_TAC (bool_ss++numSimps.ARITH_AC_ss) [GSYM EXP,ADD1] 164); 165 166(* -------------------------------------------------------- *) 167 168val COMM_MULT_DIV = ONCE_REWRITE_RULE [MULT_COMM] MULT_DIV; 169val COMM_DIV_MULT = ONCE_REWRITE_RULE [MULT_COMM] DIV_MULT; 170 171val MSHIFT_THM = prove( 172 `!t. 2 * (t + 1) <= HB + 1 ==> (MOD_CNTW t = t)`, 173 RW_TAC arith_ss [MOD_CNTW_def,WL_def,ADD1] 174 THEN IMP_RES_TAC ((SIMP_RULE arith_ss [] o SPEC `2`) DIV_LE_MONOTONE) 175 THEN FULL_SIMP_TAC arith_ss [COMM_MULT_DIV,LESS_MOD] 176); 177 178val WL_GE_2 = prove( 179 `2 <= HB + 1`, 180 SIMP_TAC arith_ss [WL_def,HB_def] 181); 182 183val MSHIFT_0 = (SIMP_RULE arith_ss [WL_GE_2] o SPEC `0`) MSHIFT_THM; 184 185val state_BOOTH_11 = theorem("state_BOOTH_11"); 186 187(* -------------------------------------------------------- *) 188 189val BIT_1_BITS = prove( 190 `!t x rs. 2 * (t + 1) <= x + 1 ==> 191 (BIT 1 (WORD_BITS x (2 * t) rs) = 192 BIT 1 (WORD_BITS (2 * t + 1) (2 * t) rs))`, 193 RW_TAC arith_ss [BIT_def,WORD_BITS_COMP_THM2,MIN_DEF] 194); 195 196val TIME_LT_WL_MIN = prove( 197 `!t x. 2 * (t + 1) <= x + 1 ==> (MIN x (2 * t + 1) = 2 * t + 1)`, 198 RW_TAC arith_ss [MIN_DEF] 199); 200 201val BIT_CONST = prove( 202 `~(BIT 1 0) /\ ~(BIT 1 1) /\ (BIT 1 2) /\ (BIT 1 3)`, 203 EVAL_TAC 204); 205 206val DIV_2_BITS = (GEN_ALL o SYM o numLib.REDUCE_RULE o INST [`n` |-> `1`] o SPEC_ALL) WORD_BITS_DIV_THM; 207 208val BIT_VAR = prove( 209 `!t x. ~(WORD_BITS (t + 1) t x = 0) /\ ~(WORD_BITS (t + 1) t x = 1) ==> 210 BIT 1 (WORD_BITS (t + 1) t x)`, 211 RW_TAC arith_ss [BIT_def,WORD_BITS_COMP_THM2,MIN_DEF,DIV_2_BITS] 212 THEN Cases_on `WORD_BITS (t + 1) t x = 2` 213 THEN1 ASM_SIMP_TAC arith_ss [] 214 THEN Cases_on `WORD_BITS (t + 1) t x = 3` 215 THEN1 ASM_SIMP_TAC arith_ss [] 216 THEN ASSUME_TAC ((SIMP_RULE arith_ss [ADD1] o SPECL [`t + 1`,`t`,`x`]) WORD_BITSLT_THM) 217 THEN DECIDE_TAC 218); 219 220val MUST_BE_TWO = prove( 221 `!t x. ~(WORD_BITS (t + 1) t x = 0) /\ 222 ~(WORD_BITS (t + 1) t x = 1) /\ 223 ~(WORD_BITS (t + 1) t x = 3) ==> 224 (WORD_BITS (t + 1) t x = 2)`, 225 REPEAT STRIP_TAC 226 THEN Cases_on `WORD_BITS (t + 1) t x = 2` 227 THEN1 ASM_REWRITE_TAC [] 228 THEN ASSUME_TAC ((SIMP_RULE arith_ss [ADD1] o SPECL [`t + 1`,`t`,`x`]) WORD_BITSLT_THM) 229 THEN DECIDE_TAC 230); 231 232val MUST_BE_THREE = prove( 233 `!t x. ~(WORD_BITS (t + 1) t x = 0) /\ 234 ~(WORD_BITS (t + 1) t x = 1) /\ 235 ~(WORD_BITS (t + 1) t x = 2) ==> 236 (WORD_BITS (t + 1) t x = 3)`, 237 REPEAT STRIP_TAC 238 THEN Cases_on `WORD_BITS (t + 1) t x = 3` 239 THEN1 ASM_REWRITE_TAC [] 240 THEN ASSUME_TAC ((SIMP_RULE arith_ss [ADD1] o SPECL [`t + 1`,`t`,`x`]) WORD_BITSLT_THM) 241 THEN DECIDE_TAC 242); 243 244(* -------------------------------------------------------- *) 245 246val ssd = simpLib.SSFRAG {ac = [(SPEC_ALL WORD_ADD_ASSOC, SPEC_ALL WORD_ADD_COMM), 247 (SPEC_ALL WORD_MULT_ASSOC, SPEC_ALL WORD_MULT_COMM)], 248 congs = [], convs = [], dprocs = [], filter = NONE, rewrs = []}; 249val word_ss = bool_ss++ssd; 250 251val SPEC_SLICE_COMP = prove( 252 `!t a. ~(t = 0) ==> 253 (a MOD 2 ** (2 * (t + 1)) = 254 SLICE (2 * t + 1) (2 * t) a + a MOD 2 ** (2 * t))`, 255 REPEAT STRIP_TAC 256 THEN IMP_RES_TAC NOT_ZERO_ADD1 257 THEN ASM_SIMP_TAC arith_ss [DECIDE (Term `!p. 2 * SUC p = SUC (2 * p + 1)`), 258 GSYM BITS_ZERO3,GSYM SLICE_ZERO_THM,SLICE_COMP_RWT] 259 THEN SIMP_TAC arith_ss [SLICE_ZERO_THM,BITS_ZERO3,ADD1,LEFT_ADD_DISTRIB] 260); 261 262val MULT_MOD_SUC_T = prove( 263 `!t a b. a * n2w (w2n b MOD 2 ** (2 * (t + 1))) = 264 (a * n2w (w2n b MOD 2 ** (2 * t))) + (a * n2w (WORD_SLICE (2 * t + 1) (2 * t) b))`, 265 REPEAT STRIP_TAC 266 THEN Cases_on `t = 0` 267 THEN1 ASM_SIMP_TAC arith_ss [WORD_MULT_CLAUSES,WORD_ADD_CLAUSES, 268 MOD_4_BITS,GSYM WORD_BITS_def,WORD_SLICE_ZERO_THM] 269 THEN ASM_SIMP_TAC bool_ss [SPEC_SLICE_COMP,GSYM WORD_SLICE_def,GSYM ADD_EVAL, 270 WORD_LEFT_ADD_DISTRIB,WORD_ADD_COMM] 271); 272 273val MULT_LEM = prove( 274 `!a b c. a * n2w (b * c) = (a * n2w c) * n2w b`, 275 SIMP_TAC word_ss [GSYM MUL_EVAL] 276); 277 278val MULT_MOD_SUC_T = REWRITE_RULE [MULT_LEM,WORD_SLICE_THM,GSYM word_lsl] MULT_MOD_SUC_T; 279 280val WORD_DOUBLE = prove( 281 `!a. a + a = a * 2w`, 282 STRIP_TAC THEN STRUCT_CASES_TAC (SPEC `a` word_nchotomy) 283 THEN SIMP_TAC arith_ss [(* MULT_COMM,*)ADD_EVAL,MUL_EVAL] 284); 285 286val MULT_FOUR = prove( 287 `!a. a * 4w = (a * 2w) + (a * 2w)`, 288 STRIP_TAC THEN STRUCT_CASES_TAC (SPEC `a` word_nchotomy) 289 THEN SIMP_TAC arith_ss [ADD_EVAL,MUL_EVAL] 290); 291 292val MULT_TWO_LSL = prove( 293 `!rm t. (rm << (2 * t)) * 2w = rm << (2 * t + 1)`, 294 SIMP_TAC arith_ss [word_lsl,GSYM WORD_MULT_ASSOC,MUL_EVAL,GSYM ADD1,EXP]); 295 296 (*,MULT_COMM]*) 297 298val MULT_FOUR_LSL = prove( 299 `!t rm. rm << (2 * (t + 1)) = (rm << (2 * t)) * 4w`, 300 SIMP_TAC arith_ss [word_lsl,GSYM WORD_MULT_ASSOC,MUL_EVAL,LEFT_ADD_DISTRIB,EXP_ADD] 301); 302 303val lem2 = prove( 304 `!a. a * 4w = (a * 3w) + a`, 305 STRIP_TAC THEN STRUCT_CASES_TAC (SPEC `a` word_nchotomy) 306 THEN REWRITE_TAC [MUL_EVAL,ADD_EVAL,DECIDE (Term `a * 4 = a * 3 + a`)] 307); 308 309val lem3 = prove( 310 `!a b. (a + (b * 3w)) - (b * 4w) = a - b`, 311 REWRITE_TAC [lem2,WORD_ADD_SUB_ASSOC,WORD_ADD_SUB3,GSYM word_sub] 312); 313 314val MULT_THREE_LSL = prove( 315 `!t x rm. x + rm << (2 * t) * 3w - rm << (2 * (t + 1)) = 316 x - rm << (2 * t)`, 317 REWRITE_TAC [MULT_FOUR_LSL,lem3] 318); 319 320val MULT_TWO_LSL2a = prove( 321 `!t x rm. x + rm << (2 * t + 1) - rm << (2 * (t + 1)) = 322 x - rm << (2 * t + 1)`, 323 REWRITE_TAC [GSYM MULT_TWO_LSL,MULT_FOUR_LSL] 324 THEN REWRITE_TAC [MULT_FOUR,WORD_SUB_PLUS,WORD_ADD_SUB] 325); 326 327val MULT_TWO_LSL2b = prove( 328 `!t x rm. x - rm << (2 * t) - rm << (2 * t) = 329 x - rm << (2 * t + 1)`, 330 REWRITE_TAC [GSYM WORD_SUB_PLUS,WORD_DOUBLE,GSYM MULT_TWO_LSL] 331); 332 333val MULT_ONE_LSL = prove( 334 `!t x rm. x + rm << (2 * t + 1) - rm << (2 * t) = 335 x + rm << (2 * t)`, 336 REWRITE_TAC [WORD_ADD_ASSOC,GSYM MULT_TWO_LSL,GSYM WORD_DOUBLE,WORD_ADD_SUB] 337); 338 339val MULT_TWO_LSL2a_0 = (numLib.REDUCE_RULE o SPEC `0`) MULT_TWO_LSL2a; 340val MULT_TWO_LSL2b_0 = (REWRITE_RULE [WORD_ADD_CLAUSES] o SPEC `0w`) MULT_TWO_LSL2a_0; 341 342val LSL_CONST = prove( 343 `(!a. a * 2w = a << 1) /\ 344 (!a. a * 4w = a << 2)`, 345 SIMP_TAC arith_ss [word_lsl] 346); 347 348val MULT_THREE_LSL_0 = (SIMP_RULE arith_ss [WORD_ADD_0,ZERO_SHIFT2] o SPEC `0`) MULT_THREE_LSL; 349val MULT_THREE_LSL_0b = (REWRITE_RULE [WORD_ADD_CLAUSES] o SPEC `0w`) MULT_THREE_LSL_0; 350 351val WORD_ADD_COMM_ASSOC = prove( 352 `!c a b. (a + b) + c = (a + c) + b`, 353 SIMP_TAC word_ss [] 354); 355 356val MOVE_RM = (GEN_ALL o SPEC `x << n` o GSYM) WORD_ADD_COMM_ASSOC; 357val MOVE_RM2 = (GEN_ALL o INST [`b` |-> `x * 3w`] o SPEC_ALL) WORD_ADD_COMM_ASSOC; 358 359(* -------------------------------------------------------- *) 360 361val INVARIANT_CORRECT = store_thm("INVARIANT_CORRECT", 362 `!t a rm rs rn. 2 * t <= WL ==> (STATE t a rm rs rn = INVARIANT a rm rs rn t)`, 363 REWRITE_TAC [WL_def] 364 THEN Induct 365 THEN1 SIMP_TAC arith_ss [WORD_BITS_COMP_THM2,MIN_HB_1,WORD_MULT_CLAUSES, 366 WORD_ADD_CLAUSES,MSHIFT_0,BITS_ZERO2,STATE_def,COND_RAND,INIT,INVARIANT,BORROW2_def] 367 THEN ASM_SIMP_TAC arith_ss [STATE_def, INVARIANT, NEXT, WORD_BITS_COMP_THM2, MSHIFT_THM, 368 BORROW2, ADD1, TIME_LT_WL_MIN, w2n_DIV_THM, 369 TWO_T_PLUS_TWO, MSHIFT_def, BIT_1_BITS, MIN_LEM, state_BOOTH_11] 370 THEN REPEAT STRIP_TAC 371 THEN1 RW_TAC arith_ss [COMM_MULT_DIV,COMM_DIV_MULT] 372 THEN RW_TAC arith_ss [ALU_def,WORD_EQ_ADD_RCANCEL] 373 THEN FULL_SIMP_TAC arith_ss [BIT_CONST,MOD_4_BITS,GSYM WORD_BITS_def] 374 THEN IMP_RES_TAC BIT_VAR 375 THEN FULL_SIMP_TAC bool_ss [MULT_MOD_SUC_T,MOVE_RM,MOVE_RM2, 376 WORD_MULT_CLAUSES,WORD_ADD_CLAUSES,ZERO_SHIFT2, 377 MUST_BE_TWO,MUST_BE_THREE,GSYM WORD_ADD_SUB_SYM,WORD_ADD_SUB, 378 MULT_ONE_LSL,MULT_TWO_LSL,MULT_TWO_LSL2a,MULT_TWO_LSL2b,MULT_THREE_LSL] 379 THEN TRY (PAT_ASSUM `t = 0` (fn th => RULE_ASSUM_TAC (SIMP_RULE arith_ss [th]))) 380 THEN ASM_SIMP_TAC word_ss [LSL_CONST,WORD_MULT_CLAUSES,MULT_TWO_LSL2a_0, 381 MULT_TWO_LSL2b_0,MULT_THREE_LSL_0,MULT_THREE_LSL_0b, 382 (numLib.REDUCE_RULE o SPEC `0`) MUST_BE_THREE] 383); 384 385(* -------------------------------------------------------- *) 386 387val EXISTS_DONE = prove( 388 `!rs. ?n. DONE rs n`, 389 RW_TAC bool_ss [DONE_def] 390 THEN EXISTS_TAC `WL DIV 2` 391 THEN SIMP_TAC arith_ss [DIV_MULT_THM2,WL_EVEN] 392); 393 394val lem = (SIMP_RULE bool_ss [EXISTS_DONE] o SPECL [`\x. 2 * x <= WL`,`DONE rs`]) LEAST_ELIM; 395 396val SPEC_LESS_MULT_MONO = (GEN_ALL o numLib.REDUCE_RULE o INST [`n` |-> `1`] o SPEC_ALL) LESS_MULT_MONO; 397 398val DIV_TWO_MONO_EVEN = prove( 399 `!a b. a < 2 * b = a DIV 2 < b`, 400 REPEAT STRIP_TAC 401 THEN Cases_on `EVEN a` 402 THENL [ 403 IMP_RES_TAC EVEN_EXISTS 404 THEN ASM_SIMP_TAC arith_ss [COMM_MULT_DIV,SPEC_LESS_MULT_MONO], 405 RULE_ASSUM_TAC (REWRITE_RULE [GSYM ODD_EVEN]) 406 THEN IMP_RES_TAC ODD_EXISTS 407 THEN ASM_SIMP_TAC arith_ss [ADD1,COMM_DIV_MULT,SPEC_LESS_MULT_MONO] 408 ] 409); 410 411val WL_DIV_MULT_TWO_ID = (SYM o ONCE_REWRITE_RULE [MULT_COMM] o SIMP_RULE arith_ss [WL_EVEN] o 412 CONJUNCT1 o SPEC `WL` o numLib.REDUCE_RULE o SPEC `2`) DIVISION; 413 414val DONE_LESS_EQUAL_WL = prove( 415 `!n. (!m. m < n ==> ~DONE rs m) /\ DONE rs n ==> 2 * n <= WL`, 416 RW_TAC bool_ss [DONE_def,NOT_LESS] 417 THENL [ 418 FULL_SIMP_TAC arith_ss [BORROW2_def] 419 THEN SPOSE_NOT_THEN STRIP_ASSUME_TAC 420 THEN RULE_ASSUM_TAC (REWRITE_RULE [NOT_LESS_EQUAL]) 421 THEN IMP_RES_TAC DIV_TWO_MONO_EVEN 422 THEN PAT_ASSUM `!m. m < n ==> P` IMP_RES_TAC 423 THEN `2 * (WL DIV 2) = (WL DIV 2) * 2` by PROVE_TAC [MULT_COMM] 424 THEN FULL_SIMP_TAC arith_ss [WL_DIV_MULT_TWO_ID] 425 , 426 Cases_on `2 * n = WL` THEN1 ASM_SIMP_TAC arith_ss [] 427 THEN `WL < 2 * n` by DECIDE_TAC 428 THEN IMP_RES_TAC DIV_TWO_MONO_EVEN 429 THEN PAT_ASSUM `!m. m < n ==> P` IMP_RES_TAC 430 THEN `2 * (WL DIV 2) = WL DIV 2 * 2` by PROVE_TAC [MULT_COMM] 431 THEN FULL_SIMP_TAC arith_ss [WL_DIV_MULT_TWO_ID] 432 ]); 433 434 435 436 437val DUR_LT_EQ_HWL = prove( 438 `!rs. 2 * (DUR rs) <= WL`, 439 REWRITE_TAC [DUR_def] 440 THEN CONV_TAC (DEPTH_CONV ETA_CONV) 441 THEN PROVE_TAC [DONE_LESS_EQUAL_WL,lem] 442); 443 444(* -------------------------------------------------------- *) 445 446val lem = (SIMP_RULE bool_ss [EXISTS_DONE] o 447 SPECL [`\x. 2 * x < WL ==> ~(BORROW2 rs x)`,`DONE rs`]) LEAST_ELIM; 448 449val DONE_EARLY_NOT_BORROW = prove( 450 `!n. (!m. m < n ==> ~DONE rs m) /\ DONE rs n ==> 451 2 * n < WL ==> 452 ~BORROW2 rs n`, 453 RW_TAC arith_ss [DONE_def,BORROW2_def] 454 THEN FULL_SIMP_TAC bool_ss [] 455); 456 457val DONE_EARLY_NOT_BORROW2 = prove( 458 `!rs. 2 * (DUR rs) < WL ==> ~BORROW2 rs (DUR rs)`, 459 REWRITE_TAC [DUR_def] 460 THEN CONV_TAC (DEPTH_CONV ETA_CONV) 461 THEN PROVE_TAC [MATCH_MP lem DONE_EARLY_NOT_BORROW] 462); 463 464val BORROW_IMP_WL = prove( 465 `!rs. BORROW2 rs (DUR rs) ==> (2 * (DUR rs) = WL)`, 466 REPEAT STRIP_TAC 467 THEN Cases_on `2 * (DUR rs) < WL` 468 THEN1 IMP_RES_TAC DONE_EARLY_NOT_BORROW2 469 THEN ASSUME_TAC (SPEC `rs` DUR_LT_EQ_HWL) 470 THEN DECIDE_TAC 471); 472 473val lem = (SIMP_RULE bool_ss [EXISTS_DONE] o 474 SPECL [`\x. w2n rs MOD 2 ** (2 * x) = w2n rs`,`DONE rs`]) LEAST_ELIM; 475 476val ZERO_LT_WL = simpLib.SIMP_PROVE arith_ss [WL_def] ``0 < WL``; 477 478val DONE_IMP_ZERO_MSBS = prove( 479 `!n. (!m. m < n ==> ~DONE rs m) /\ DONE rs n ==> 480 (w2n rs MOD 2 ** (2 * n) = w2n rs)`, 481 STRUCT_CASES_TAC (SPEC `rs` word_nchotomy) 482 THEN RW_TAC arith_ss [WL_def,SUC_SUB1,w2n_EVAL,DONE_def,MOD_WL_THM,WORD_BITS_def,BITS_COMP_THM2] 483 THENL [ 484 Cases_on `n'` THEN1 FULL_SIMP_TAC arith_ss [ZERO_MOD] 485 THEN FULL_SIMP_TAC bool_ss [GSYM BITS_ZERO3,DECIDE ``!n. 2 * SUC n = SUC (2 * n + 1)``] 486 THEN RW_TAC arith_ss [BITS_COMP_THM2,MIN_DEF] 487 THEN Cases_on `2 * n'' + 1 = HB` THEN1 ASM_REWRITE_TAC [] 488 THEN `2 * n'' + 2 <= HB` by FULL_SIMP_TAC arith_ss [NOT_LESS] 489 THEN `SLICE HB (SUC (2 * n'' + 1)) n = 0` by ASM_SIMP_TAC arith_ss [SLICE_THM] 490 THEN IMP_RES_TAC ((GSYM o SIMP_RULE arith_ss [ADD1,SLICE_ZERO_THM] o 491 SPECL [`HB`,`2 * n'' + 1`,`0`]) SLICE_COMP_THM) 492 THEN POP_ASSUM (ASSUME_TAC o SPEC `n`) 493 THEN FULL_SIMP_TAC arith_ss [ADD1], 494 FULL_SIMP_TAC bool_ss [NOT_LESS] 495 THEN IMP_RES_TAC LESS_EQUAL_ADD 496 THEN STRIP_ASSUME_TAC (REWRITE_RULE [ADD,WL_def] (MATCH_MP LESS_ADD_1 ZERO_LT_WL)) 497 THEN ASM_SIMP_TAC bool_ss [ADD_SUB,DECIDE ``!a b. a + 1 + b = SUC (a + b)``,GSYM BITS_ZERO3] 498 THEN RW_TAC arith_ss [BITS_COMP_THM2,MIN_DEF] 499 THEN `p = 0` by DECIDE_TAC 500 THEN FULL_SIMP_TAC arith_ss [ADD1] 501 ] 502); 503 504val DUR_IMP_ZERO_MSBS = prove( 505 `!rs. w2n rs MOD 2 ** (2 * (DUR rs)) = w2n rs`, 506 REWRITE_TAC [DUR_def] 507 THEN CONV_TAC (DEPTH_CONV ETA_CONV) 508 THEN PROVE_TAC [MATCH_MP lem DONE_IMP_ZERO_MSBS] 509); 510 511val SPEC_LSL_LIMIT = (GEN_ALL o REWRITE_RULE [GSYM WL_def] o 512 SIMP_RULE arith_ss [WL_def] o SPECL [`a`,`WL`]) LSL_LIMIT; 513 514(* -------------------------------------------------------- *) 515 516val CORRECT = store_thm("CORRECT", 517 `!a rm rs rn. BOOTHMULTIPLY a rm rs rn = 518 rm * rs + (if a then rn else 0w)`, 519 SIMP_TAC bool_ss [DUR_LT_EQ_HWL,BOOTHMULTIPLY_def,INVARIANT_CORRECT,INVARIANT,PROJ_RD_def,BORROW_IMP_WL, 520 DUR_IMP_ZERO_MSBS,w2n_ELIM,SPEC_LSL_LIMIT,WORD_SUB_RZERO] 521); 522 523(* -------------------------------------------------------- *) 524 525val if_swp = PROVE [] ``!a b c. (if ~a then b else c) = (if a then c else b)``; 526 527val SPEC_BIT_BITS_THM = 528 (GEN_ALL o SYM o REWRITE_RULE [BITS_ZERO2,BIT_ZERO] o INST [`b` |-> `0`] o SPEC_ALL) BIT_BITS_THM; 529 530val EXTEND_ONE_BIT = prove( 531 `!h l n. l < h /\ (l2 = SUC l) ==> (~(BITS h l2 n = 0) \/ BIT l n = ~(BITS h l n = 0))`, 532 RW_TAC bool_ss [GSYM LESS_EQ,SPEC_BIT_BITS_THM] 533 THEN EQ_TAC THEN RW_TAC arith_ss [] 534 THENL [ 535 EXISTS_TAC `x` THEN ASM_SIMP_TAC arith_ss [], 536 EXISTS_TAC `l` THEN ASM_SIMP_TAC arith_ss [], 537 Cases_on `l = x` THEN1 ASM_REWRITE_TAC [] 538 THEN DISJ1_TAC THEN EXISTS_TAC `x` THEN ASM_SIMP_TAC arith_ss [] 539 ] 540); 541 542val DUR_EVAL = save_thm("DUR_EVAL", 543 (GEN_ALL o SIMP_RULE std_ss [if_swp,EXTEND_ONE_BIT] o 544 SIMP_RULE arith_ss [HB_def,GSYM BIT_def,WL_def]) 545 (funpow 17 (ONCE_REWRITE_RULE [WHILE]) 546 ((SIMP_RULE arith_ss [LEAST_DEF,DONE_def,BORROW2_def,BIT_def,MIN_DEF, 547 BITS_EVAL,BIT_EVAL,MOD_WL_THM,BITS_COMP_THM2] o SPEC `n2w n`) DUR_def)) 548); 549 550(* -------------------------------------------------------- *) 551 552 553val _ = export_theory(); 554