1(*****************************************************************************) 2(* signedintScript.sml *) 3(* Creates operators sw2i and i2sw to relate words to signed integers *) 4(* and companion theorems. *) 5(* *) 6(*****************************************************************************) 7 8(* Interactive use only - 9load "wordsTheory"; 10load "intLib"; 11*) 12 13open Theory Thm Term Type Tactic Tactical bossLib Drule 14open Rewrite Conv HolKernel boolSyntax 15open boolTheory 16open wordsTheory arithmeticTheory integerTheory bitTheory intLib; 17 18(* Profiling - 19val list = ref []; 20fun prove x = 21let val s = Time.now(); 22 val r = Tactical.prove x 23 val e = Time.now(); 24 val _ = list := (Time.-(e,s),fst x)::(!list) 25in 26 r 27end; 28fun store_thm (a,b,c) = save_thm(a,prove (b,c)); 29*) 30 31val _ = new_theory "signedint"; 32 33val int_sub_calc1 = prove( 34 ``& a - & b = if b <= a then & (a - b) else ~ &(b - a):int``, 35 RW_TAC int_ss [INT_SUB,ARITH_PROVE ``(a = ~b) = (~a = b:int)``]); 36 37val int_sub_calc2 = prove( 38 ``& a - & b = if b < a then & (a - b) else ~ &(b - a):int``, 39 RW_TAC int_ss [INT_SUB,ARITH_PROVE ``(a = ~b) = (~a = b:int)``]); 40 41val dimword_pos = prove( 42 ``~(& (dimword (:'a)) = 0i) /\ ~(dimword (:'a) = 0n) /\ 0 < dimword (:'a)``, 43 PROVE_TAC [INT_LT_NZ,ZERO_LT_TWOEXP,INT_NZ_IMP_LT, 44 DECIDE ``0 < a = ~(a = 0n)``,dimword_def]); 45 46val w2n_lt_full = save_thm("w2n_lt_full", 47 LIST_CONJ [w2n_lt,REWRITE_RULE [dimword_def] w2n_lt, 48 REWRITE_RULE [dimword_def,GSYM NOT_LESS_EQUAL] w2n_lt]); 49 50val bint_ss = int_ss ++ boolSimps.LET_ss; 51 52val BIT_RWR = 53 save_thm("BIT_RWR",SIMP_RULE arith_ss 54 [BITS_THM2,DECIDE ``(a = 1) = 0 < a /\ a < 2n``, 55 DIV_LT_X,X_LT_DIV,MOD_LESS,GSYM EXP] BIT_def); 56 57val SUC_SUB_INDEX = prove( 58 ``SUC (dimindex (:'a) - 1) = dimindex (:'a)``, 59 RW_TAC arith_ss [DECIDE ``0 < a ==> (SUC (a - 1) = a)``,DIMINDEX_GT_0]); 60 61(*****************************************************************************) 62(* A ?- a < c A ?- a <= c *) 63(* ------------------------ LT ------------------------- LE *) 64(* A ?- ?b. a < b /\ b < c A ?- ?b. a <= b /\ b <= c *) 65(* *) 66(* A ?- a < c A ?- a < c *) 67(* ------------------------ LTLE ------------------------ LELT *) 68(* A ?- ?b. a < b /\ b <= c A ?- ?b. a <= b /\ b < c *) 69(* *) 70(*****************************************************************************) 71 72local 73val q = Q.EXISTS_TAC 74val lelt = DECIDE ``!a b c. a <= b /\ b < c ==> a < c:num`` 75val ltle = DECIDE ``!a b c. a < b /\ b <= c ==> a < c:num`` 76fun try thm = FIRST [MATCH_MP_TAC thm, 77 MATCH_MP_TAC LESS_IMP_LESS_OR_EQ THEN MATCH_MP_TAC thm] 78in 79fun NLT_TRANS_TAC w = try LESS_TRANS THEN q w 80fun NLE_TRANS_TAC w = MATCH_MP_TAC LESS_EQ_TRANS THEN q w 81fun NLELT_TRANS_TAC w = try lelt THEN q w 82fun NLTLE_TRANS_TAC w = try ltle THEN q w 83end; 84 85(*****************************************************************************) 86(* A ?- t *) 87(* ---------------------------------------------------------- *) 88(* A [& c / x] ?- t [& c / x] A [~& c / x] ?- t [~& c / x] *) 89(* *) 90(*****************************************************************************) 91 92local 93val thm1 = ARITH_PROVE ``!a. 0 <= ~a \/ 0 <= a`` 94val thm2 = prove(``!a. 0 <= a ==> ?c. a = & c``, 95 REPEAT STRIP_TAC THEN Q.EXISTS_TAC `Num a` THEN 96 ASM_REWRITE_TAC 97 [ONCE_REWRITE_RULE [ISPEC ``a:int`` EQ_SYM_EQ] INT_OF_NUM, 98 ARITH_PROVE ``(a = ~ & b) = (~a = & b)``]); 99val thm3 = prove(``!a. 0 <= ~a ==> ?c. a = ~ & c``, 100 REPEAT STRIP_TAC THEN Q.EXISTS_TAC `Num ~a` THEN 101 ASM_REWRITE_TAC 102 [ONCE_REWRITE_RULE [ISPEC ``a:int`` EQ_SYM_EQ] INT_OF_NUM, 103 ARITH_PROVE ``(a = ~ & b) = (~a = & b)``]); 104in 105fun INT_CASE_TAC tm = 106 DISJ_CASES_TAC (Q.SPEC tm thm1) THENL [ 107 POP_ASSUM (STRIP_ASSUME_TAC o MATCH_MP thm3), 108 POP_ASSUM (STRIP_ASSUME_TAC o MATCH_MP thm2)] THEN 109 POP_ASSUM SUBST_ALL_TAC 110end; 111 112(*****************************************************************************) 113(* A u {!x. P} ?- t[tm] *) 114(* --------------------------- pTAC tm f *) 115(* A ?- P [f tm / x] ==> t[tm] *) 116(* *) 117(*****************************************************************************) 118 119fun pTAC tm f (a,g) = 120let val x = find_terms (can (match_term tm)) g 121 val t = f (hd x) 122in 123 (PAT_ASSUM ``!m:'a.P`` (MP_TAC o SPEC t)) (a,g) 124end handle e => NO_TAC (a,g) 125 126 127 128(*****************************************************************************) 129(* Bit support theorems: *) 130(* *) 131(* BIT_MOD : |- !a b c. BIT a (b MOD 2 ** c) = a < c /\ BIT a b *) 132(* MOD_HIGH_MOD : |- !a b. b <= a ==> ((2 ** a - 1) MOD 2 ** b = 2 ** b - 1) *) 133(* MOD_HIGH_SUM : |- !a b. 2 ** b - 1 = *) 134(* (2 ** b - 2 ** a + (2 ** a - 1)) MOD 2 ** b *) 135(* MOD_HIGH_EQ_ADD : |- !b c d. (2 ** b - 1 = c MOD 2 ** b + d MOD 2 ** b) = *) 136(* (2 ** b - 1 = (c + d) MOD 2 ** b) *) 137(* *) 138(* BIT_DIV : |- !x m. BIT (SUC m) x = BIT m (x DIV 2) *) 139(* BIT_ZERO_ODD : |- !a. BIT 0 a = ODD a *) 140(* *) 141(* BITWISE_DIV : |- !m op x y. BITWISE (SUC m) op x y = *) 142(* (if op (ODD x) (ODD y) then 1 else 0) + *) 143(* 2 * BITWISE m op (x DIV 2) (y DIV 2)``, *) 144(* BITWISE_ZERO : |- !op x y. BITWISE 0 op x y = 0 *) 145(* *) 146(*****************************************************************************) 147 148val BIT_MOD = store_thm("BIT_MOD", 149 ``!a b c. BIT a (b MOD 2 ** c) = a < c /\ BIT a b``, 150 REPEAT GEN_TAC THEN REWRITE_TAC [BIT_RWR] THEN 151 `a < c \/ c < SUC a` by DECIDE_TAC THEN1 152 (IMP_RES_TAC LESS_ADD_1 THEN 153 RW_TAC arith_ss [DECIDE ``a + (p + 1) = SUC a + p``] THEN 154 RW_TAC arith_ss [ONCE_REWRITE_RULE [MULT_COMM] MOD_MULT_MOD, 155 EXP_ADD]) THEN 156 RW_TAC arith_ss [NOT_LESS_EQUAL] THEN 157 `b MOD 2 ** c < 2 ** a` by NLTLE_TRANS_TAC `2 ** c` THEN 158 RW_TAC arith_ss [MOD_LESS] THEN 159 `b MOD 2 ** c < 2 ** SUC a` by NLT_TRANS_TAC `2 ** a` THEN 160 RW_TAC arith_ss [MOD_LESS]); 161 162val MOD_HIGH_MOD = store_thm("MOD_HIGH_MOD", 163 ``!a b. b <= a ==> ((2 ** a - 1) MOD 2 ** b = 2 ** b - 1)``, 164 Induct THEN RW_TAC arith_ss [EXP] THEN 165 Cases_on `b = SUC a` THEN RW_TAC arith_ss [EXP] THEN 166 `a = b + (a - b)` by DECIDE_TAC THEN 167 ONCE_ASM_REWRITE_TAC [] THEN 168 REWRITE_TAC [MATCH_MP (DISCH_ALL (MATCH_MP 169 (DECIDE ``0 < a ==> (a + a - 1 = a + (a - 1n))``) 170 (UNDISCH (SPEC_ALL LESS_MULT2)))) 171 (CONJ (SPEC_ALL ZERO_LT_TWOEXP) (Q.SPEC `m` ZERO_LT_TWOEXP)), 172 EXP_ADD,TIMES2,ONCE_REWRITE_RULE [MULT_COMM] 173 (MATCH_MP MOD_TIMES (SPEC_ALL ZERO_LT_TWOEXP))] THEN 174 RW_TAC arith_ss [GSYM EXP_ADD]); 175 176val MOD_HIGH_SUM = store_thm("MOD_HIGH_SUM", 177 ``!a b. 2 ** b - 1 = (2 ** b - 2 ** a + (2 ** a - 1)) MOD 2 ** b``, 178 REPEAT GEN_TAC THEN `a <= b \/ b <= a` by DECIDE_TAC THEN 179 METIS_TAC [TWOEXP_MONO2, 180 DECIDE ``a <= b /\ 0 < b /\ 0 < a ==> (b - a + (a - 1) = b - 1n)``, 181 ZERO_LT_TWOEXP,DECIDE ``0 < b ==> (b - 1n < b)``,LESS_MOD,MOD_HIGH_MOD, 182 DECIDE ``b <= a ==> (b - a + c = c:num)``]); 183 184val MOD_HIGH_EQ_ADD = store_thm("MOD_HIGH_EQ_ADD", 185 ``!b c d. (2 ** b - 1 = c MOD 2 ** b + d MOD 2 ** b) = 186 (2 ** b - 1 = (c + d) MOD 2 ** b)``, 187 REPEAT GEN_TAC THEN 188 ONCE_REWRITE_TAC [GSYM (MATCH_MP MOD_PLUS (SPEC_ALL ZERO_LT_TWOEXP))] THEN 189 Q.ABBREV_TAC `A = c MOD 2 ** b` THEN Q.ABBREV_TAC `B = d MOD 2 ** b` THEN 190 Q.ABBREV_TAC `D = 2n ** b` THEN 191 `A < D /\ B < D /\ 0 < D` by METIS_TAC [MOD_LESS,ZERO_LT_TWOEXP] THEN 192 `A + B < D \/ D <= A + B /\ A + B <= 2 * D - 2` by DECIDE_TAC THEN 193 IMP_RES_TAC (Q.SPECL [`A + B`,`D`] (GSYM SUB_MOD)) THEN RW_TAC arith_ss []); 194 195val BIT_DIV = store_thm("BIT_DIV", 196 ``!x m. BIT (SUC m) x = BIT m (x DIV 2)``, 197 RW_TAC arith_ss [BIT_def,BITS_def,MOD_2EXP_def,DIV_2EXP_def, 198 DECIDE ``SUC a - a = 1``,DIV_DIV_DIV_MULT,ZERO_LT_TWOEXP,EXP]); 199 200val BIT_ZERO_ODD = store_thm("BIT_ZERO_ODD", 201 ``!a. BIT 0 a = ODD a``, 202 RW_TAC arith_ss [BIT_def,BITS_THM,ODD_MOD2_LEM]); 203 204val SBIT_DIV = store_thm("SBIT_DIV", 205 ``!x m. 2 * SBIT x m = SBIT x (SUC m)``, 206 RW_TAC arith_ss [SBIT_def,EXP]); 207 208val SBIT_ZERO = store_thm("SBIT_ZERO", 209 ``!b. SBIT b 0 = if b then 1 else 0``, 210 RW_TAC arith_ss [SBIT_def]); 211 212val BITWISE_DIV = store_thm("BITWISE_DIV", 213 ``!m op x y. BITWISE (SUC m) op x y = 214 (if op (ODD x) (ODD y) then 1 else 0) + 215 2 * BITWISE m op (x DIV 2) (y DIV 2)``, 216 RW_TAC int_ss [BITWISE_EVAL,SBIT_def,LSB_def,BIT_ZERO_ODD]); 217 218val BITWISE_ZERO = store_thm("BITWISE_ZERO", 219 ``!op x y. BITWISE 0 op x y = 0``, 220 RW_TAC arith_ss [BITWISE_def,SBIT_DIV,LEFT_ADD_DISTRIB,BIT_DIV]); 221 222(*****************************************************************************) 223(* Word support theorems: *) 224(* TOP_BIT_LE : |- !a. BIT (dimindex (:'a) - 1) (w2n a) = *) 225(* 2 ** (dimindex (:'a) - 1) <= w2n a *) 226(* DIMINDEX_DOUBLE : |- 2n ** (dimindex (:'a)) = *) 227(* 2 * 2 ** (dimindex (:'a) - 1) *) 228(* *) 229(*****************************************************************************) 230val TOP_BIT_LE = store_thm("TOP_BIT_LE", 231 ``!a. BIT (dimindex (:'a) - 1) (w2n (a:'a word)) = 232 2 ** (dimindex (:'a) - 1) <= w2n a``, 233 RW_TAC int_ss [BIT_RWR,DIMINDEX_GT_0,SUC_SUB_INDEX,LESS_MOD,w2n_lt_full]); 234 235val DIMINDEX_DOUBLE = store_thm("DIMINDEX_DOUBLE", 236 ``2n ** (dimindex (:'a)) = 2 * 2 ** (dimindex (:'a) - 1)``, 237 RW_TAC arith_ss [GSYM EXP,DIMINDEX_GT_0,SUC_SUB_INDEX]); 238 239(*****************************************************************************) 240(* Other arithmetic theorems: *) 241(* ODD_TWOEXP : |- !x. ODD (2 ** x) = (x = 0) *) 242(* MOD2_ODD_EVEN : |- (!a. (a MOD 2 = 0) = EVEN a) /\ *) 243(* (!a. (a MOD 2 = 1) = ODD a) *) 244(* EVEN_SUB : |- !a b. EVEN (a - b) = a <= b \/ (EVEN a = EVEN b) *) 245(* ODD_SUB : |- !a b. ODD (a - b) = b < a /\ ~(ODD a = ODD b) *) 246(* *) 247(* DIV2_MULT_SUB1 : |- !a. 0 < a ==> ((2 * a - 1) DIV 2 = a - 1) *) 248(* NOT_MOD2 : |- (!c. ~(c MOD 2 = 0) = (c MOD 2 = 1n)) /\ *) 249(* (!c. ~(c MOD 2 = 1n) = (c MOD 2 = 0n)) *) 250(* BITWISE_TOP : |- !a b. b < 2 ** a ==> (BITWISE a $/\ (2 ** a - 1) b = b) *) 251(* *) 252(*****************************************************************************) 253 254val ODD_TWOEXP = store_thm("ODD_TWOEXP",``!x. ODD (2 ** x) = (x = 0n)``, 255 Induct THEN RW_TAC arith_ss [EXP,EVEN_DOUBLE,GSYM EVEN_ODD]); 256 257val MOD2_ODD_EVEN = store_thm("MOD2_ODD_EVEN", 258 ``(!a. (a MOD 2 = 0) = EVEN a) /\ (!a. (a MOD 2 = 1) = ODD a)``, 259 PROVE_TAC [ODD_MOD2_LEM,MOD_LESS,DECIDE ``0 < 2n``, 260 DECIDE ``a < 2 = (a = 0n) \/ (a = 1n)``, 261 EVEN_ODD,DECIDE ``~(0 = 1n)``]); 262 263val EVEN_SUB = store_thm("EVEN_SUB", 264 ``!a b. EVEN (a - b) = a <= b \/ (EVEN a = EVEN b)``, 265 Induct THEN GEN_TAC THEN EQ_TAC THEN Cases_on `SUC a <= b` THEN 266 RW_TAC arith_ss [EVEN,ADD1] THEN 267 FULL_SIMP_TAC arith_ss [NOT_LESS_EQUAL,ADD1, 268 DECIDE ``(a + 1 <= b) ==> (a + 1 - b = 0n)``] THEN 269 IMP_RES_TAC LESS_EQUAL_ADD THEN POP_ASSUM SUBST_ALL_TAC THEN 270 FULL_SIMP_TAC arith_ss [EVEN_ADD] THEN METIS_TAC []); 271 272val ODD_SUB = store_thm("ODD_SUB", 273 ``!a b. ODD (a - b) = b < a /\ ~(ODD a = ODD b)``, 274 METIS_TAC [NOT_LESS_EQUAL,EVEN_ODD,EVEN_SUB]); 275 276val DIV2_MULT_SUB1 = store_thm("DIV2_MULT_SUB1", 277 ``!a. 0 < a ==> ((2 * a - 1) DIV 2 = a - 1)``, 278 GEN_TAC THEN DISCH_TAC THEN `?b. a = SUC b` by Q.EXISTS_TAC `a - 1` THEN 279 RW_TAC arith_ss [ADD1,LEFT_ADD_DISTRIB, 280 ONCE_REWRITE_RULE [MULT_COMM] DIV_MULT]); 281 282val NOT_MOD2 = store_thm("NOT_MOD", 283 ``(!c. ~(c MOD 2 = 0) = (c MOD 2 = 1n)) /\ 284 (!c. ~(c MOD 2 = 1n) = (c MOD 2 = 0n))``, 285 PROVE_TAC [MOD2_ODD_EVEN,EVEN_OR_ODD,EVEN_ODD]); 286 287val BITWISE_TOP = store_thm("BITWISE_TOP", 288 ``!a b. b < 2 ** a ==> (BITWISE a $/\ (2 ** a - 1) b = b)``, 289 Induct THEN GEN_TAC THEN TRY (POP_ASSUM (MP_TAC o Q.SPEC `b DIV 2`)) THEN 290 RW_TAC int_ss [BITWISE_DIV,BITWISE_ZERO,ODD_SUB,GSYM EVEN_ODD,EVEN_EXP, 291 DIV2_MULT_SUB1,EXP,EVEN_MULT,DIV_LT_X,DIV_MULT_THM2] THEN 292 Cases_on `b` THEN FULL_SIMP_TAC int_ss [GSYM MOD2_ODD_EVEN,NOT_MOD2]); 293 294(*****************************************************************************) 295(* Definitions *) 296(* i2n i l : Convert an integer i to a natural number < 2 ** l *) 297(* extend r l : Sign extend an integer i to fit in l bits *) 298(* *) 299(* sw2i x : Convert the word x to a signed integer *) 300(* i2sw x : Convert the integer x to a word *) 301(* *) 302(* iand a b : Bitwise and of two integers *) 303(* inot a : Bitwise negation of an integer *) 304(* ibit i j : Determine if bit i of integer j is set *) 305(* *) 306(*****************************************************************************) 307 308val i2n_def = Define `i2n i l = 309 Num (if 0 <= i then i % 2 ** l else (i + 1) rem (2 ** l) - 1 + 2 ** l)`; 310 311val extend_def = Define `extend i l = 312 let m = i2n i l in if BIT (l - 1) m then & m - 2 ** l else & m`; 313 314val sw2i_def = Define `sw2i (x:'a word) = 315 (if BIT (dimindex (:'a) - 1) (w2n x) then 316 & (w2n x) - 2 ** dimindex (:'a) 317 else 318 & (w2n x))`; 319 320val i2sw_def = Define `i2sw x = 321 let m = extend x (dimindex (:'b)) 322 in if m < 0 then n2w (Num (m + 2 ** dimindex (:'b))) 323 else n2w (Num m):'b word`; 324 325val iand_def = tDefine "iand" 326 `iand i j = 327 if (i = 0) then 0 328 else if (j = 0) then 0 329 else if (i = ~1) then j 330 else if (j = ~1) then i 331 else let x = 2 * iand (i / 2) (j / 2) 332 in x + (if (i % 2 = 1) /\ (j % 2 = 1) then 1 else 0)` 333 (WF_REL_TAC `measure (Num o ABS o FST)` THEN 334 RW_TAC int_ss [INT_ABS] THEN 335 ONCE_REWRITE_TAC [GSYM INT_LT] THEN 336 RW_TAC std_ss [snd (EQ_IMP_RULE (SPEC_ALL INT_OF_NUM)), 337 ARITH_PROVE ``a < 0 ==> 0i <= ~a``, 338 ARITH_PROVE ``~(a < 0) ==> 0i <= a``] THEN ARITH_TAC); 339 340val inot_def = Define `inot x = ~(x + 1i)`; 341 342val ibit_def = Define `ibit i j = ODD (Num (ABS (j / 2 ** i)))`; 343 344(*****************************************************************************) 345(* I2N_NUM : |- !a b. i2n (& a) b = a MOD 2 ** b *) 346(* EXTEND_LE_ZERO : |- !a b. extend a b < 0 = BIT (b - 1) (i2n a b) *) 347(* EXTEND_ZERO : |- !a b. (extend 0 a = 0) /\ (extend b 0 = 0) *) 348(* *) 349(* EXTEND_POS_EQ : |- !a b. a < 2 ** (b - 1) ==> (extend (& a) b = & a *) 350(* EXTEND_POS_NE : |- !a b. 2 ** (b - 1) < a /\ a < 2 ** b ==> *) 351(* (extend (& a) b = & a - 2 ** b) *) 352(* EXTEND_POS_NEG : |- !b. 0 < b ==> (extend (& (2 ** (b - 1))) b = *) 353(* ~ & (2 ** (b - 1))) *) 354(* EXTEND_POS_REC : |- !a b. 2 ** b <= a ==> (extend (& a) b = *) 355(* extend (& (a - 2 ** b)) b) *) 356(* *) 357(* EXTEND_NEG_EQ : |- !a b. a < 2 ** (b - 1) ==> (extend (~ & a) b = ~ & a) *) 358(* EXTEND_NEG_NE : |- !a b. 2 ** (b - 1) < a /\ a < 2 ** b ==> *) 359(* (extend (~ & a) b = 2 ** b - & a) *) 360(* EXTEND_NEG_NEG : |- !b. 0 < b ==> (extend (~ & (2 ** (b - 1))) b = *) 361(* ~ & (2 ** (b - 1))) *) 362(* EXTEND_NEG_REC : |- !a b. 2 ** b <= a ==> (extend (~ & a) b = *) 363(* extend (~ & (a - 2 ** b)) b) *) 364(* *) 365(* EXTEND_EQ : |- !n a b. (extend a (SUC n) = b) = *) 366(* ~(2 ** n) <= b /\ b < 2 ** n /\ *) 367(* ?m. b = a + m * 2 ** SUC n *) 368(* EXTEND_LIMIT : |- !n a. ~(2 ** n) <= extend a (SUC n) /\ *) 369(* extend a (SUC n) < 2 ** n *) 370(* EXTEND_11 : |- !n a b. (extend a (SUC n) = extend b (SUC n)) = *) 371(* ?m. a = b + m * 2 ** SUC n *) 372(* EXTEND_LINEAR : |- !n m x b. extend (m * extend x (SUC n) + b) (SUC n) = *) 373(* extend (m * x + b) (SUC n) *) 374(* EXTEND_LINEAR_IMP : |- !n f x. (?m b. !x. f x = m * x + b) ==> *) 375(* (extend (f (extend x (SUC n))) (SUC n) = *) 376(* extend (f x) (SUC n)) *) 377(* *) 378(* EXTEND_POS_CALCULATE, EXTEND_NEG_CALCULATE: *) 379(* Calculates extend (& a) b or extend (~& a) b using the above theorems *) 380(* *) 381(*****************************************************************************) 382 383val I2N_NUM = store_thm("I2N_NUM", 384 ``!a b. i2n (& a) b = a MOD 2 ** b``,RW_TAC int_ss [i2n_def]); 385 386val mod_p1_eq = 387 MATCH_MP (DISCH_ALL (MATCH_MP 388 (DECIDE ``a < b ==> (a + 1 < b = ~(a = b - 1n))``) 389 (UNDISCH (SPEC_ALL MOD_LESS)))) (SPEC_ALL ZERO_LT_TWOEXP); 390 391val EXTEND_LE_ZERO = store_thm("EXTEND_LE_ZERO", 392 ``!a b. extend a b < 0 = BIT (b - 1) (i2n a b)``, 393 RW_TAC (int_ss ++ boolSimps.LET_ss) [extend_def,i2n_def] THEN 394 FULL_SIMP_TAC std_ss [] THENL [ 395 `?c. a = & c` by Q.EXISTS_TAC `Num a`, 396 `?c. (a = ~ & c)` by Q.EXISTS_TAC `Num (~a)`] THEN 397 RW_TAC int_ss [INT_OF_NUM,ARITH_PROVE ``(a = ~ & b) = (~a = & b:int)``, 398 ARITH_PROVE ``~(0 <= a) ==> a <= 0i``, 399 ARITH_PROVE ``a - b < 0i = a < b``,MOD_LESS] THEN 400 FULL_SIMP_TAC int_ss [ONCE_REWRITE_RULE [INT_ADD_COMM] (GSYM int_sub), 401 int_sub_calc2,DECIDE ``a < 1 = (a = 0n)``,INT_ADD, 402 ARITH_PROVE ``~a - 1 + b = b - (a + 1i)``, 403 mod_p1_eq] THEN 404 Cases_on `((c - 1) MOD 2 ** b = 2 ** b - 1)` THEN 405 FULL_SIMP_TAC int_ss [MATCH_MP (DECIDE ``0 < b ==> (b - 1 + 1 - b = 0n)``) 406 (SPEC_ALL ZERO_LT_TWOEXP), 407 DECIDE ``a <= a - b = (b = 0n) \/ (a = 0n)``]); 408 409val EXTEND_ZERO = store_thm("EXTEND_ZERO", 410 ``!a b. (extend 0 a = 0) /\ (extend b 0 = 0)``, 411 RW_TAC (int_ss ++ boolSimps.LET_ss) [extend_def,i2n_def,BIT_def,BITS_THM2, 412 ZERO_DIV] THEN 413 FULL_SIMP_TAC bint_ss [GSYM INT_OF_NUM] THEN 414 TRY (POP_ASSUM (SUBST_ALL_TAC o GSYM)) THEN 415 FULL_SIMP_TAC bint_ss [INT_OF_NUM] THEN 416 `?c. b = ~ & c` by Q.EXISTS_TAC `Num (~ b)` THEN 417 TRY (POP_ASSUM SUBST_ALL_TAC THEN Cases_on `c <= 1`) THEN 418 FULL_SIMP_TAC int_ss [ARITH_PROVE ``(b = ~ & a) = (~b = & a)``,INT_OF_NUM, 419 ARITH_PROVE ``~(0 <= b) ==> b <= 0i``,INT_ADD_CALCULATE, 420 INT_SUB_CALCULATE]); 421 422val EXTEND_POS_EQ = store_thm("EXTEND_POS_EQ", 423 ``!a b. a < 2 ** (b - 1) ==> (extend (& a) b = & a)``, 424 REPEAT GEN_TAC THEN Cases_on `b = 0n` THEN 425 RW_TAC bint_ss [extend_def,i2n_def,BIT_RWR,MOD_MOD, 426 DECIDE ``~(b = 0) ==> (SUC (b - 1) = b)``] THEN 427 `a < 2 ** b` by PROVE_TAC [LESS_TRANS,TWOEXP_MONO, 428 DECIDE ``~(b = 0) ==> b - 1n < b``] THEN 429 FULL_SIMP_TAC int_ss [MOD_LESS]); 430 431val EXTEND_POS_NE = store_thm("EXTEND_POS_NE", 432 ``2 ** (b - 1) < a /\ a < 2 ** b ==> (extend (& a) b = & a - 2 ** b)``, 433 Cases_on `b = 0n` THEN 434 RW_TAC bint_ss [extend_def,i2n_def,BIT_RWR,MOD_MOD, 435 DECIDE ``~(b = 0) ==> (SUC (b - 1) = b)``] ); 436 437val EXTEND_POS_NEG = store_thm("EXTEND_POS_NEG", 438 ``0 < b ==> (extend (& (2 ** (b - 1))) b = ~ & (2 ** (b - 1)))``, 439 Cases_on `b` THEN RW_TAC bint_ss [extend_def,i2n_def,BIT_RWR,MOD_MOD] THEN 440 RW_TAC int_ss [EXP,int_sub_calc1]); 441 442val thms = [BIT_MOD,DECIDE ``b - 1 < b = 0n < b``,int_sub_calc1,INT_EXP, 443 DECIDE ``(a - b = 0n) = (a <= b)``, 444 REWRITE_RULE [GSYM NOT_LESS_EQUAL] 445 (MATCH_MP MOD_LESS (SPEC_ALL ZERO_LT_TWOEXP)), 446 extend_def,I2N_NUM,LET_DEF,INT_LE,INT_EQ_CALCULATE]; 447 448val EXTEND_POS_REC = store_thm("EXTEND_POS_REC", 449 ``!a b. 2 ** b <= a ==> (extend (& a) b = extend (& (a - 2 ** b)) b)``, 450 REPEAT GEN_TAC THEN Cases_on `0 < b` THEN 451 TRY (`SUC (b - 1) = b` by DECIDE_TAC) THEN 452 ASM_REWRITE_TAC thms THEN BETA_TAC THEN 453 ASM_REWRITE_TAC (BIT_RWR::thms) THEN 454 REPEAT STRIP_TAC THEN REPEAT IF_CASES_TAC THEN ASM_REWRITE_TAC thms THEN 455 PROVE_TAC [SUB_MOD,ZERO_LT_TWOEXP]); 456 457val EXTEND_POS_CALCULATE = store_thm("EXTEND_POS_CALCULATE", 458 ``extend (& a) b = 459 if a < 2 ** (b - 1) then & a 460 else if (a = 2 ** (b - 1)) /\ 0 < b then ~ & a 461 else if 2 ** (b - 1) < a /\ a < 2 ** b then & a - 2 ** b 462 else extend (& (a - 2 ** b)) b``, 463 RW_TAC bint_ss [EXTEND_POS_NEG,EXTEND_POS_EQ,EXTEND_POS_NE] THEN 464 MATCH_MP_TAC EXTEND_POS_REC THEN 465 REPEAT (FULL_SIMP_TAC arith_ss [NOT_LESS])); 466 467val EXTEND_NEG_EQ = store_thm("EXTEND_NEG_EQ", 468 ``a < 2 ** (b - 1) ==> (extend (~ & a) b = ~ & a)``, 469 REWRITE_TAC [extend_def,i2n_def,BIT_RWR] THEN RW_TAC bint_ss [] THEN 470 FULL_SIMP_TAC bint_ss [ARITH_PROVE ``~a + 1 = 1i - a``] THENL [ 471 ALL_TAC,CCONTR_TAC] THEN 472 `a - 1 < 2 ** b` by NLTLE_TRANS_TAC `2 ** (b - 1)` THEN 473 `1 - & a = ~& (a - 1)` by RW_TAC int_ss [int_sub_calc1] THEN 474 FULL_SIMP_TAC int_ss [ARITH_PROVE ``~a - b + c = c - (a + b):int``,INT_ADD, 475 int_sub_calc1] THEN 476 Cases_on `b` THEN FULL_SIMP_TAC int_ss [NOT_LESS_EQUAL,EXP]); 477 478val EXTEND_NEG_NEG = store_thm("EXTEND_NEG_NEG", 479 ``0 < b ==> (extend (~ & (2 ** (b - 1))) b = ~ & (2 ** (b - 1)))``, 480 RW_TAC bint_ss [BIT_RWR,extend_def,i2n_def,INT_ADD_CALCULATE, 481 INT_SUB_CALCULATE,INT_REM_CALCULATE, 482 DECIDE ``(a <= 1) = ~(0n < a) \/ (a = 1n)``] THEN 483 FULL_SIMP_TAC bint_ss [INT_ADD_CALCULATE,INT_SUB_CALCULATE, 484 DECIDE ``a + 1n <= b = a < b``] THEN 485 Cases_on `b` THEN FULL_SIMP_TAC int_ss [EXP] THEN 486 FULL_SIMP_TAC int_ss [GSYM EXP]); 487 488val EXTEND_NEG_NE = store_thm("EXTEND_NEG_NE", 489 ``2 ** (b - 1) < a /\ a < 2 ** b ==> (extend (~ (& a)) b = 2 ** b - & a)``, 490 Cases_on `b` THEN RW_TAC bint_ss [extend_def,i2n_def,EXTEND_ZERO] THEN 491 Cases_on `a <= 1n` THEN 492 FULL_SIMP_TAC int_ss [INT_SUB_CALCULATE,INT_ADD_CALCULATE,BIT_RWR] THEN 493 FULL_SIMP_TAC int_ss [EXP]); 494 495val lem1 = prove(``2 ** SUC n < a ==> 496 ((~ & (a - 2 ** SUC n) + 1) rem & (2 ** SUC n) = 497 ~&( (a - 1) MOD (2 ** SUC n)))``, 498 RW_TAC int_ss [INT_SUB_CALCULATE,INT_ADD_CALCULATE] THEN 499 (`a = 2 ** SUC n + 1` by DECIDE_TAC ORELSE 500 `a - (2 ** SUC n + 1) = (a - 1) - 2 ** SUC n` by DECIDE_TAC) THEN 501 ASM_REWRITE_TAC [] THEN TRY (MATCH_MP_TAC SUB_MOD) THEN 502 RW_TAC arith_ss []); 503 504val EXTEND_NEG_REC = store_thm("EXTEND_NEG_REC", 505 ``2 ** b <= a ==> (extend (~ & a) b = extend (~ & (a - 2 ** b)) b)``, 506 Cases_on `b` THEN RW_TAC bint_ss [EXTEND_ZERO] THEN 507 `2 <= a /\ 1 <= a` by (Induct_on `n` THEN RW_TAC int_ss [EXP]) THEN 508 `(~ & a + 1 = ~ & (a - 1)) /\ (~ & (a - 1) - 1 = ~ & a)` by 509 RW_TAC int_ss [INT_SUB_CALCULATE,INT_ADD_CALCULATE] THEN 510 RW_TAC (std_ss ++ boolSimps.LET_ss) [extend_def,i2n_def] THEN 511 FULL_SIMP_TAC std_ss [ARITH_PROVE ``(0i <= ~ & a) = (a = 0n)``] THEN 512 TRY (`a = 2 ** SUC n` by DECIDE_TAC) THEN 513 FULL_SIMP_TAC int_ss [BIT_ZERO,BIT_RWR, 514 ARITH_PROVE ``~ & a - 1 + b = b - & (a + 1)``, 515 DECIDE ``0 < a ==> (a - 1 + 1n = a)``,lem1]); 516 517val EXTEND_NEG_CALCULATE = store_thm("EXTEND_NEG_CALCULATE", 518 ``extend (~ & a) b = 519 if a < 2 ** (b - 1) then ~ & a 520 else if (a = 2 ** (b - 1)) /\ 0 < b then ~ & a 521 else if 2 ** (b - 1) < a /\ a < 2 ** b then 2 ** b - & a 522 else extend (~ & (a - 2 ** b)) b``, 523 RW_TAC int_ss [EXTEND_ZERO,EXTEND_NEG_NE,EXTEND_NEG_EQ,EXTEND_NEG_NEG] THEN 524 Cases_on `a` THEN MATCH_MP_TAC EXTEND_NEG_REC THEN 525 FULL_SIMP_TAC int_ss [NOT_LESS]); 526 527val extend_eq_base = prove(``a < 2 ** SUC n ==> 528 (!b. (extend (& a) (SUC n) = b) = 529 ~(2 ** n) <= b /\ b < 2 ** n /\ ?m. b = & a + m * 2 ** SUC n) /\ 530 (!b. (extend (~ & a) (SUC n) = b) = 531 ~ (2 ** n) <= b /\ b < 2 ** n /\ ?m. b = ~ & a + m * 2 ** SUC n)``, 532 ONCE_REWRITE_TAC [EXTEND_POS_CALCULATE,EXTEND_NEG_CALCULATE] THEN 533 RW_TAC int_ss [EXP,ADD1,INT_ADD_CALCULATE,INT_SUB_CALCULATE] THEN 534 EQ_TAC THEN NTAC 2 (RW_TAC int_ss []) THEN 535 TRY (Q.EXISTS_TAC `0` THEN RW_TAC int_ss [] THEN NO_TAC) THEN 536 TRY (Q.EXISTS_TAC `~1` THEN 537 RW_TAC int_ss [INT_MUL_CALCULATE,INT_ADD_CALCULATE] THEN NO_TAC) THEN 538 TRY (Q.EXISTS_TAC `1` THEN 539 RW_TAC int_ss [INT_MUL_CALCULATE,INT_ADD_CALCULATE] THEN NO_TAC) THEN 540 INT_CASE_TAC `m` THEN Cases_on `c` THEN REPEAT (POP_ASSUM MP_TAC) THEN 541 RW_TAC int_ss [LEFT_ADD_DISTRIB,INT_ADD_CALCULATE,INT_MUL_CALCULATE, 542 ADD1,RIGHT_ADD_DISTRIB] THEN 543 Cases_on `n'` THEN 544 FULL_SIMP_TAC int_ss [ADD1,LEFT_ADD_DISTRIB,RIGHT_ADD_DISTRIB]); 545 546val EXTEND_EQ = store_thm("EXTEND_EQ", 547 ``!n a b. (extend a (SUC n) = b) = 548 ~ (2 ** n) <= b /\ b < 2 ** n /\ ?m. b = a + m * 2 ** SUC n``, 549 REPEAT GEN_TAC THEN INT_CASE_TAC `a` THEN completeInduct_on `c` THEN 550 Cases_on `c < 2 ** SUC n` THEN 551 FULL_SIMP_TAC int_ss [extend_eq_base,NOT_LESS, 552 EXTEND_NEG_REC,EXTEND_POS_REC] THEN 553 (Cases_on `c = 0` THEN1 554 (POP_ASSUM SUBST_ALL_TAC THEN EQ_TAC THEN 555 RW_TAC int_ss [EXTEND_ZERO] THEN INT_CASE_TAC `m` THEN 556 TRY (Cases_on `c`) THEN 557 FULL_SIMP_TAC int_ss [])) THEN 558 PAT_ASSUM ``!m:'a.P`` (MP_TAC o Q.SPEC `c - 2 ** SUC n`) THEN 559 RW_TAC int_ss [NOT_LESS_EQUAL] THEN 560 POP_ASSUM (K ALL_TAC) THEN 561 EQ_TAC THEN RW_TAC int_ss [] THENL 562 (map Q.EXISTS_TAC [`m' + 1`,`m - 1`,`m' - 1`,`m + 1`]) THEN 563 RW_TAC int_ss [INT_RDISTRIB,INT_SUB_RDISTRIB,GSYM INT_SUB] THEN 564 RW_TAC int_ss [int_sub] THEN 565 FIRST [CONV_TAC (AC_CONV (INT_ADD_ASSOC,INT_ADD_COMM)),ARITH_TAC]); 566 567val EXTEND_LIMIT = store_thm("EXTEND_LIMIT", 568 ``!n a. ~ (2 ** n) <= extend a (SUC n) /\ extend a (SUC n) < 2 ** n``, 569 REPEAT GEN_TAC THEN INT_CASE_TAC `a` THEN completeInduct_on `c` THEN 570 ONCE_REWRITE_TAC [EXTEND_POS_CALCULATE,EXTEND_NEG_CALCULATE] THEN 571 RW_TAC int_ss [INT_SUB_CALCULATE,INT_ADD_CALCULATE] THEN 572 FULL_SIMP_TAC int_ss [NOT_LESS_EQUAL,NOT_LESS,EXP]); 573 574val lem = prove(``?m''. b + m * n + m' * n = b + m'' * n:int``, 575 Q.EXISTS_TAC `m + m'` THEN RW_TAC int_ss [INT_RDISTRIB,INT_ADD_ASSOC]); 576 577fun CF m tac v1 v2 (a,g) = 578 if exists (free_in m) (g::a) then 579 tac v1 (a,g) 580 else tac v2 (a,g); 581 582val lem2 = prove(``?m. ~ & (2 ** n) <= b + m * & (2 ** SUC n) /\ 583 b + m * & (2 ** SUC n) < & (2 ** n)``, 584 INT_CASE_TAC `b` THEN completeInduct_on `c` THEN 585 (Cases_on `c = 0` THEN1 586 (Q.EXISTS_TAC `0` THEN FULL_SIMP_TAC int_ss [])) THEN 587 `c < 2 ** n \/ (c = 2 ** n) \/ 2 ** n < c /\ 588 c < 2 ** SUC n \/ 2 ** SUC n <= c` by DECIDE_TAC THEN 589 TRY (MAP_FIRST (fn x => Q.EXISTS_TAC x THEN 590 FULL_SIMP_TAC int_ss [EXP,INT_ADD_CALCULATE,INT_SUB_CALCULATE, 591 INT_MUL_CALCULATE, 592 DECIDE ``0 < a ==> (a < 2 * a) /\ ~(2n * a <= a)``] THEN 593 NO_TAC) [`0`,`1`,`~1`]) THEN 594 PAT_ASSUM ``!m:'a. P`` (MP_TAC o Q.SPEC `c - 2 ** SUC n`) THEN 595 RW_TAC int_ss [] THEN 596 FULL_SIMP_TAC int_ss [] THEN IMP_RES_TAC (GSYM INT_SUB) THENL [ 597 CF ``m:int`` Q.EXISTS_TAC `m + 1` `m' + 1`, 598 CF ``m:int`` Q.EXISTS_TAC `m - 1` `m' - 1`] THEN 599 FULL_SIMP_TAC int_ss [INT_RDISTRIB,int_sub,INT_NEG_ADD, 600 INT_ADD_ASSOC,INT_MUL_CALCULATE] THEN 601 METIS_TAC [INT_ADD_ASSOC,INT_ADD_COMM]); 602 603val EXTEND_11 = store_thm("EXTEND_11", 604 ``!n a b. (extend a (SUC n) = extend b (SUC n)) = 605 ?m. a = b + m * 2 ** SUC n``, 606 REPEAT GEN_TAC THEN EQ_TAC THEN RW_TAC int_ss [EXTEND_EQ,EXTEND_LIMIT] THEN 607 RW_TAC int_ss [lem] THEN1 608 (Q.EXISTS_TAC `m' - m` THEN RW_TAC int_ss [INT_SUB_RDISTRIB] THEN 609 ARITH_TAC) THEN 610 STRIP_ASSUME_TAC lem2 THEN 611 Q.EXISTS_TAC `~m + m'` THEN ARITH_TAC); 612 613val EXTEND_LINEAR = store_thm("EXTEND_LINEAR", 614 ``!n m x b. extend (m * (extend x (SUC n)) + b) (SUC n) = 615 extend (m * x + b) (SUC n)``, 616 REPEAT GEN_TAC THEN 617 REWRITE_TAC [EXTEND_11, 618 ARITH_PROVE ``(a + b = c + b + d) = (a = c + d:int)``] THEN 619 SUBGOAL_THEN ``?y. extend x (SUC n) = x + y * 2 ** SUC n`` 620 STRIP_ASSUME_TAC THEN1 621 RW_TAC int_ss [EXTEND_EQ,lem2, 622 prove(``?m. y * b = m * b:int``,Q.EXISTS_TAC `y` THEN REFL_TAC)] THEN 623 Q.EXISTS_TAC `m * y` THEN RW_TAC int_ss [INT_LDISTRIB,INT_MUL_ASSOC]); 624 625val EXTEND_LINEAR_IMP = store_thm("EXTEND_LINEAR_IMP", 626 ``!n f x. (?m b. !x. f x = m * x + b) ==> 627 (extend (f (extend x (SUC n))) (SUC n) = extend (f x) (SUC n))``, 628 NTAC 2 (RW_TAC int_ss [EXTEND_LINEAR])); 629 630(*****************************************************************************) 631(* extend (f (extend a (dimindex (:'a)))) (dimindex (:'a)) *) 632(* ======================================================= EXTEND_CONV *) 633(* extend (f a) (dimindex (:'a)) *) 634(* *) 635(* Provided f is a combination of +,*,-,~ *) 636(* *) 637(*****************************************************************************) 638fun eindex tm = REWRITE_RULE [SUC_SUB_INDEX] (Q.SPEC `dimindex (:'a) - 1` tm); 639 640local 641val linear = ``\f. ?m b. !x. f x = m * x + b:int``; 642val add = prove(``^linear f /\ ^linear g ==> ^linear (\x. f x + g x)``, 643 BETA_TAC THEN REPEAT STRIP_TAC THEN 644 MAP_EVERY Q.EXISTS_TAC [`m + m'`,`b + b'`] THEN 645 RW_TAC int_ss [INT_RDISTRIB] THEN ARITH_TAC); 646val mul1 = prove(``^linear f ==> ^linear (\x. f x * c)``, 647 BETA_TAC THEN REPEAT STRIP_TAC THEN 648 MAP_EVERY Q.EXISTS_TAC [`m * c`,`b * c`] THEN 649 RW_TAC int_ss [INT_RDISTRIB] THEN ARITH_TAC); 650val mul2 = prove(``^linear f ==> ^linear (\x. c * f x)``, 651 BETA_TAC THEN REPEAT STRIP_TAC THEN 652 MAP_EVERY Q.EXISTS_TAC [`m * c`,`b * c`] THEN 653 RW_TAC int_ss [INT_RDISTRIB] THEN ARITH_TAC); 654val sub = prove(``^linear (\x. a x + ~b x) ==> ^linear (\x. a x - b x)``, 655 RW_TAC int_ss [int_sub]); 656val neg = prove(``^linear f ==> ^linear (\x. ~ f x)``, 657 BETA_TAC THEN REPEAT STRIP_TAC THEN MAP_EVERY Q.EXISTS_TAC [`~m`,`~b`] THEN 658 RW_TAC int_ss [INT_RDISTRIB] THEN ARITH_TAC); 659val id = prove(``^linear (\x.x)``, 660 BETA_TAC THEN MAP_EVERY Q.EXISTS_TAC [`1`,`0`] THEN 661 BETA_TAC THEN ARITH_TAC); 662val const = prove(``^linear(\x.c)``, 663 BETA_TAC THEN MAP_EVERY Q.EXISTS_TAC [`0`,`c`] THEN 664 BETA_TAC THEN ARITH_TAC); 665val rules = map (CONV_RULE 666 (TRY_CONV (LAND_CONV (DEPTH_CONV BETA_CONV))) o BETA_RULE) 667 [add,mul1,mul2,neg,sub,id,const]; 668val extend = ``extend a (dimindex (:'a))`` 669fun prove_it tm = 670let val x = fst (dest_forall (snd (strip_exists tm))) 671 val thm1 = STRIP_QUANT_CONV (STRIP_QUANT_CONV 672 (LAND_CONV (UNBETA_CONV x))) tm 673 val thm2 = tryfind (CONV_RULE (RAND_CONV 674 (REWR_CONV (GSYM thm1)) ORELSEC (REWR_CONV (GSYM thm1))) o 675 C (HO_PART_MATCH (snd o strip_imp)) (rhs (concl thm1))) rules 676 val tms = if is_imp_only (concl thm2) then strip_conj 677 (fst (dest_imp (concl thm2))) else [] 678in 679 if null tms then thm2 else MATCH_MP thm2 (LIST_CONJ (map prove_it tms)) 680end; 681fun remove e x = 682let val thm = (RATOR_CONV (RAND_CONV (UNBETA_CONV e)) THENC 683 (UNDISCH o PART_MATCH (lhs o snd o strip_imp) 684 (eindex EXTEND_LINEAR_IMP))) x; 685 val thms1 = map (GSYM o REDEPTH_CONV BETA_CONV) (hyp thm) 686 val thms2 = map (prove_it o lhs o concl) thms1 687 val thms3 = map2 EQ_MP thms1 thms2 688in 689 CONV_RULE (RAND_CONV (RATOR_CONV (RAND_CONV BETA_CONV))) 690 (foldl (uncurry PROVE_HYP) thm thms3) 691end 692in 693fun EXTEND_CONV x = 694let val _ = match_term extend x 695 val extends = find_terms (can (match_term extend)) (rand (rator x)); 696in 697 tryfind (C remove x) extends 698end 699end; 700 701(*****************************************************************************) 702(* Signed integer theorems: *) 703(*****************************************************************************) 704 705val sw2i_thm = store_thm("sw2i_thm", 706 ``sw2i (x:'a word) = extend (& (w2n x)) (dimindex (:'a))``, 707 RW_TAC int_ss [eindex EXTEND_EQ,sw2i_def,BIT_RWR,SUC_SUB_INDEX, 708 INT_SUB_CALCULATE,INT_ADD_CALCULATE,w2n_lt_full] THEN 709 RW_TAC int_ss [DIMINDEX_DOUBLE] THENL [ 710 Q.EXISTS_TAC `~1`,Q.EXISTS_TAC `0`] THEN 711 RW_TAC int_ss [INT_MUL_CALCULATE,GSYM INT_SUB,GSYM DIMINDEX_DOUBLE, 712 w2n_lt_full,INT_SUB_CALCULATE,INT_ADD_CALCULATE]); 713 714val sw2i_LIMIT = Q.GEN `a` 715 (REWRITE_RULE [GSYM sw2i_thm] (Q.SPEC `& (w2n (a:'a word))` 716 (eindex EXTEND_LIMIT))); 717 718val I2N_LT = store_thm("I2N_LT", 719 ``!x b. i2n x b < 2 ** b``, 720 RW_TAC arith_ss [i2n_def] THENL [ 721 `?c. x = & c` by Q.EXISTS_TAC `Num x`, 722 `?c. x = ~ & c` by Q.EXISTS_TAC `Num (~x)`] THEN 723 RW_TAC int_ss [INT_OF_NUM,ARITH_PROVE ``(x = ~ & y) = (~x = & y)``] THEN1 724 ARITH_TAC THEN 725 RW_TAC int_ss [ARITH_PROVE ``~ & c + 1 = 1i - & c``,int_sub_calc1, 726 ARITH_PROVE ``~ & c - 1 + b = b - (1 + & c)``,INT_ADD, 727 DECIDE ``a + 1 <= b = a < b:num``] THEN 728 FULL_SIMP_TAC int_ss [] THEN `c = 1` by DECIDE_TAC THEN 729 RW_TAC int_ss [ARITH_PROVE ``~1 + b = b - 1i``,int_sub_calc1, 730 DECIDE ``1 <= a = 0n < a``]); 731 732(*****************************************************************************) 733(* i2sw_sw2i : |- !x. i2sw (sw2i x) = sw2sw x *) 734(* sw2i_i2sw : |- !x. sw2i ((i2sw x) : 'a word) = extend x (dimindex (:'a)) *) 735(*****************************************************************************) 736 737val rwr1 = prove(``& (w2n (x:'a word)) - & (2 ** dimindex (:'a)):int = 738 ~ & (2 ** dimindex (:'a) - w2n x)``, 739 RW_TAC int_ss [GSYM dimword_def,int_sub_calc1] THEN 740 MATCH_MP_TAC LESS_IMP_LESS_OR_EQ THEN MATCH_ACCEPT_TAC w2n_lt); 741 742val rwra1 = prove(``~ & (dimword (:'a) - w2n x) + 1i = 743 ~ & (dimword (:'a) - w2n (x:'a word) - 1)``, 744 RW_TAC std_ss [int_sub_calc1,ONCE_REWRITE_RULE [INT_ADD_COMM] 745 (GSYM int_sub)] THEN 746 ASSUME_TAC (Q.SPEC `x` w2n_lt) THEN 747 `w2n (x:'a word) = dimword (:'a) - 1` by ARITH_TAC THEN 748 RW_TAC int_ss []); 749 750val mod_add_lem = prove(``0 < a /\ 2 ** (a - 1) <= c /\ c < 2 ** a ==> 751 (2 ** b - ((2 ** a - (c + 1)) MOD 2 ** b + 1) = 752 (2 ** b - 2 ** a + c) MOD 2 ** b)``, 753 `b <= a \/ a <= b` by DECIDE_TAC THEN IMP_RES_TAC TWOEXP_MONO2 THEN 754 RW_TAC arith_ss [LESS_MOD,DECIDE ``b <= a ==> (b - a + c = c:num)``] THEN 755 RW_TAC arith_ss [MOD_LESS,MOD_HIGH_EQ_ADD,MOD_HIGH_MOD, 756 DECIDE ``a < b ==> ((b - (a + 1) = c) = (b - 1n = c + a))``]); 757 758val i2sw = SIMP_RULE (int_ss ++ boolSimps.LET_ss) [] i2sw_def; 759 760val i2sw_sw2i = store_thm("i2sw_sw2i", 761 ``!x. i2sw (sw2i x) = sw2sw (x:'a word) : 'b word``, 762 RW_TAC (int_ss ++ boolSimps.LET_ss) [i2sw,sw2i_def,sw2sw_def, 763 SIGN_EXTEND_def,rwr1,INT_ADD,DECIDE ``~(a - 1 < a) = ~(0n < a)``, 764 EXTEND_LE_ZERO,I2N_NUM,BIT_MOD,DIMINDEX_GT_0,extend_def,n2w_11, 765 MOD_MOD,dimword_def,w2n_lt_full,MOD_LESS] THEN 766 RW_TAC int_ss [i2n_def,ARITH_PROVE ``0i <= ~&a = (a = 0n)``,w2n_lt_full, 767 ARITH_PROVE ``~ & a + 1 = 1i - & a``,int_sub_calc1, 768 REWRITE_RULE [dimword_def] dimword_pos, 769 DECIDE ``a < b ==> (b <= a + 1n = (b = a + 1n))``, 770 ARITH_PROVE ``~1 + a = a - 1i``,DECIDE ``1 <= a = 0n < a``] THENL [ 771 POP_ASSUM (SUBST_ALL_TAC o MATCH_MP (MATCH_MP 772 (DECIDE ``0 < a ==> (a = b + 1) ==> (b = a - 1n)``) 773 (SPEC_ALL ZERO_LT_TWOEXP))) THEN 774 RW_TAC std_ss [ZERO_LT_TWOEXP, 775 DECIDE ``0 < a ==> (a - 1n + 1 = a)``] THEN 776 MATCH_ACCEPT_TAC MOD_HIGH_SUM, 777 RW_TAC int_ss [INT_ADD,int_sub_calc1,ARITH_PROVE ``~a + b = b - a:int``, 778 ARITH_PROVE ``~a - b = ~(a + b:int)``, 779 DECIDE ``a + 1n <= b = a < b``]] THEN 780 MATCH_MP_TAC mod_add_lem THEN 781 FULL_SIMP_TAC arith_ss [DIMINDEX_GT_0,w2n_lt_full, 782 BIT_RWR,SUC_SUB_INDEX]); 783 784val sw2i_i2sw = store_thm("sw2i_i2sw", 785 ``!x. sw2i ((i2sw x):'a word) = extend x (dimindex (:'a))``, 786 RW_TAC (int_ss ++ boolSimps.LET_ss) [i2sw,sw2i_def,sw2sw_def, 787 SIGN_EXTEND_def,rwr1,INT_ADD,dimword_def,w2n_lt_full, 788 EXTEND_LE_ZERO,I2N_NUM,BIT_MOD,DECIDE ``~(a - 1 < a) = ~(0n < a)``, 789 DIMINDEX_GT_0,extend_def,n2w_11,MOD_MOD,MOD_LESS,w2n_n2w,I2N_LT]); 790 791(*****************************************************************************) 792(* sw2i_twocomp : |- !a. sw2i (- a) = extend (~ (sw2i a)) (dimindex (:'a)) *) 793(* sw2i_add : |- !a. sw2i (a + b) = *) 794(* extend (sw2i a + sw2i b) (dimindex (:'a)) *) 795(* sw2i_sub : |- !a. sw2i (a - b) = *) 796(* extend (sw2i a - sw2i b) (dimindex (:'a)) *) 797(*****************************************************************************) 798 799val mod_lem = prove(``0 < b ==> ((?m. & (a MOD b) = c + m * & b) = 800 (?m. & a = c + m * & b))``, 801 completeInduct_on `a` THEN `a < b \/ b <= a` by DECIDE_TAC THEN 802 RW_TAC int_ss [MOD_LESS] THEN 803 PAT_ASSUM ``!a:'a.P`` (MP_TAC o Q.SPEC `a - b`) THEN 804 RW_TAC arith_ss [SUB_MOD] THEN 805 IMP_RES_TAC (GSYM INT_SUB) THEN EQ_TAC THEN REPEAT STRIP_TAC THENL [ 806 Q.EXISTS_TAC `m + 1`,Q.EXISTS_TAC `m - 1`] THEN 807 FULL_SIMP_TAC int_ss [INT_RDISTRIB,INT_SUB_RDISTRIB] THEN ARITH_TAC); 808 809val extend_mod = prove(``!b a. extend (& (a MOD 2 ** SUC b)) (SUC b) = 810 extend (& a) (SUC b)``, 811 RW_TAC int_ss [EXTEND_11,mod_lem] THEN 812 Q.EXISTS_TAC `0` THEN ARITH_TAC); 813 814val sw2i_twocomp = store_thm("sw2i_twocomp", 815 ``!a. sw2i (- a:'a word) = extend (~ (sw2i a)) (dimindex (:'a))``, 816 REWRITE_TAC [sw2i_thm] THEN 817 CONV_TAC (DEPTH_CONV EXTEND_CONV) THEN 818 RW_TAC int_ss [mod_lem,eindex EXTEND_11, 819 word_2comp_def,w2n_n2w,dimword_def] THEN 820 Q.EXISTS_TAC `1` THEN 821 RW_TAC int_ss [INT_ADD_CALCULATE,GSYM NOT_LESS_EQUAL] THEN 822 PROVE_TAC [NOT_LESS_EQUAL,NOT_LESS,LESS_IMP_LESS_OR_EQ,w2n_lt_full]); 823 824val sw2i_add = store_thm("sw2i_add", 825 ``!a b. sw2i (a + (b:'a word)) = 826 extend (sw2i a + sw2i b) (dimindex (:'a))``, 827 REWRITE_TAC [sw2i_thm] THEN CONV_TAC (DEPTH_CONV EXTEND_CONV) THEN 828 REWRITE_TAC [word_add_def,w2n_n2w,INT_ADD] THEN 829 RW_TAC int_ss [eindex EXTEND_11,mod_lem,dimword_def] THEN 830 Q.EXISTS_TAC `0` THEN ARITH_TAC); 831 832val sw2i_sub = store_thm("sw2i_sub", 833 ``!a b. sw2i (a - (b:'a word)) = 834 extend (sw2i a - sw2i b) (dimindex (:'a))``, 835 REWRITE_TAC [sw2i_thm] THEN CONV_TAC (DEPTH_CONV EXTEND_CONV) THEN 836 RW_TAC int_ss [word_sub_def,word_add_def,word_2comp_def,w2n_n2w, 837 dimword_def,eindex EXTEND_11,mod_lem] THEN 838 Cases_on `w2n b = 0` THEN RW_TAC int_ss [] THENL 839 (map Q.EXISTS_TAC [`0`,`1`]) THEN 840 RW_TAC int_ss [w2n_lt_full,ARITH_PROVE ``a - b + c = (a + c) + ~b:int``, 841 INT_ADD_CALCULATE] THEN 842 TRY (MATCH_MP_TAC (DECIDE ``c < b ==> (a + (b - c) = a + b - c:num)``)) THEN 843 PROVE_TAC [w2n_lt_full,NOT_LESS_EQUAL, 844 DECIDE ``a < b ==> ~(c + b < a:num)``]); 845 846val sw2i_mul = store_thm("sw2i_mul", 847 ``!a b. sw2i (a * b : 'a word) = 848 extend (sw2i a * sw2i b) (dimindex (:'a))``, 849 REWRITE_TAC [sw2i_thm,word_mul_def,w2n_n2w,dimword_def] THEN 850 CONV_TAC (DEPTH_CONV EXTEND_CONV) THEN 851 REWRITE_TAC [word_mul_def,w2n_n2w,dimword_def] THEN 852 RW_TAC int_ss [eindex EXTEND_11,mod_lem] THEN 853 Q.EXISTS_TAC `0` THEN ARITH_TAC); 854 855(*****************************************************************************) 856(* IAND_COMM : |- !a b. iand a b = iand b a *) 857(* IAND_ZERO : |- !a. (iand a 0 = 0) /\ (iand 0 a = 0) *) 858(* IAND_ID : |- !a. iand a a = a *) 859(*****************************************************************************) 860 861val bitwise_mod_lem = prove(``BITWISE a b c d MOD 2 ** a = BITWISE a b c d``, 862 PROVE_TAC [BITWISE_LT_2EXP,ZERO_LT_TWOEXP,LESS_MOD]); 863 864val AND_ZERO = prove(``!x a. (BITWISE x $/\ a 0 = 0) /\ 865 (BITWISE x $/\ 0 a = 0)``, 866 Induct THEN RW_TAC int_ss [BITWISE_DIV,BITWISE_ZERO]); 867 868val bitwise_iand1 = prove(``!x a b. a < 2 ** x /\ b < 2 ** x ==> 869 (& (BITWISE x $/\ a b) = iand (& a) (& b))``, 870 Induct THEN ONCE_REWRITE_TAC [iand_def] THEN 871 RW_TAC bint_ss [BITWISE_DIV,BITWISE_ZERO,ODD_MOD2_LEM,AND_ZERO, 872 ARITH_PROVE ``(& (2 * a) = 2i * b) = (& a = b)``, 873 ARITH_PROVE ``(& (2 * a + 1) = 2i * b + 1) = (& a = b)``] THEN 874 FIRST_ASSUM MATCH_MP_TAC THEN RW_TAC int_ss [DIV_LT_X,GSYM EXP]); 875 876val bitwise_iand2 = MATCH_MP bitwise_iand1 877 (REWRITE_RULE [dimword_def] (CONJ (Q.SPEC `a` w2n_lt) (Q.SPEC `b` w2n_lt))); 878 879val bitwise_iand3 = prove(``& (2 ** (dimindex (:'a)) - 880 BITWISE (dimindex (:'a)) $/\ (w2n a) (w2n b)) = 881 2i ** (dimindex (:'a)) - iand (& (w2n (a:'a word))) 882 (& (w2n (b:'a word)))``, 883 RW_TAC int_ss [GSYM bitwise_iand2,int_sub_calc1] THEN 884 METIS_TAC [BITWISE_LT_2EXP,NOT_LESS_EQUAL,LESS_IMP_LESS_OR_EQ]); 885 886val div2_lem = prove(``~ & a / 2 = if EVEN a then ~ & (a DIV 2) else 887 ~ & (a DIV 2 + 1)``, 888 REPEAT (RW_TAC int_ss [MOD2_ODD_EVEN,EVEN,int_div,INT_ADD_CALCULATE] THEN 889 POP_ASSUM MP_TAC)); 890 891val IAND_COMM = store_thm("IAND_COMM",``!a b. iand a b = iand b a``, 892 GEN_TAC THEN INT_CASE_TAC `a` THEN 893 completeInduct_on `c` THEN ONCE_REWRITE_TAC [iand_def] THEN 894 GEN_TAC THEN REPEAT IF_CASES_TAC THEN 895 ASM_REWRITE_TAC [LET_DEF] THEN BETA_TAC THEN 896 REWRITE_TAC [div2_lem] THEN 897 RW_TAC int_ss [ARITH_PROVE ``~(2 * a + 1i = 2 * b)``] THEN 898 TRY (FIRST_ASSUM (MATCH_MP_TAC o CONV_RULE 899 (STRIP_QUANT_CONV RIGHT_IMP_FORALL_CONV))) THEN 900 FULL_SIMP_TAC int_ss [DIV_LT_X,DECIDE ``c < 2 * c = 0n < c``, 901 DECIDE ``0 < b ==> (a + 1 < b = a < b - 1n)``, 902 DECIDE ``c < 2 * (c - 1) = 2n < c``] THEN 903 CCONTR_TAC THEN `c = 2` by DECIDE_TAC THEN POP_ASSUM SUBST_ALL_TAC THEN 904 FULL_SIMP_TAC int_ss [EVEN]); 905 906val IAND_ZERO = store_thm("IAND_ZERO", 907 ``!a. (iand a 0 = 0) /\ (iand 0 a = 0)``, 908 ONCE_REWRITE_TAC [iand_def] THEN RW_TAC int_ss []); 909 910fun two_rule x = REWRITE_RULE [DECIDE ``~(0 = 2n)``,DECIDE ``0 < 2n``] 911 (Q.SPEC `2` x); 912 913val IAND_ID = store_thm("IAND_ID",``!a. iand a a = a``, 914 GEN_TAC THEN INT_CASE_TAC `a` THEN completeInduct_on `c` THEN 915 ONCE_REWRITE_TAC [iand_def] THEN 916 NTAC 2 (RW_TAC bint_ss [DIV_MULT_THM2,INT_ADD_CALCULATE, 917 DECIDE ``(a - b = a) = (a = 0) \/ (b = 0n)``,DIV_LE_X, 918 int_div,int_mod,INT_SUB_CALCULATE,INT_MUL_CALCULATE,NOT_MOD2, 919 IAND_ZERO,DECIDE ``(a DIV b = 0) = (a DIV b <= 0)``] THEN 920 REPEAT (POP_ASSUM MP_TAC)) THEN 921 REPEAT STRIP_TAC THEN 922 Cases_on `c = 2` THEN TRY (POP_ASSUM SUBST_ALL_TAC) THEN 923 FULL_SIMP_TAC int_ss [] THEN 924 TRY (pTAC ``iand a b`` (rand o rand o rand)) THEN 925 FULL_SIMP_TAC int_ss [LEFT_ADD_DISTRIB,DIV_MULT_THM2] THEN 926 DISJ_CASES_TAC (Q.SPEC `c` EVEN_OR_ODD) THEN 927 IMP_RES_TAC EVEN_ODD_EXISTS THEN 928 FULL_SIMP_TAC int_ss [ADD1,ONCE_REWRITE_RULE [MULT_COMM] MOD_MULT, 929 ONCE_REWRITE_RULE [MULT_COMM] MOD_EQ_0]); 930 931(*****************************************************************************) 932(* sw2i_and : |- !a b. sw2i (a && b) = iand (sw2i a) (sw2i b) *) 933(*****************************************************************************) 934 935val exp_add_lem = prove(``!x. (2 ** x + 1) DIV 2 = 2 ** (x - 1)``, 936 Induct THEN RW_TAC arith_ss [EXP,ONCE_REWRITE_RULE [MULT_COMM] DIV_MULT]); 937 938val rwr1 = prove(``!b n. ~ & (2 * 2 ** n - b) / 2 = ~ & (2 ** n - b DIV 2)``, 939 REPEAT GEN_TAC THEN DISJ_CASES_TAC (Q.SPEC `b` EVEN_OR_ODD) THEN 940 IMP_RES_TAC EVEN_ODD_EXISTS THEN 941 Cases_on `2 ** n <= m` THEN 942 RW_TAC int_ss [GSYM LEFT_SUB_DISTRIB,ADD1, 943 DECIDE ``a <= b ==> (a - b = 0n)``, 944 ONCE_REWRITE_RULE [MULT_COMM] MULT_DIV, 945 ONCE_REWRITE_RULE [MULT_COMM] DIV_MULT, 946 DECIDE ``~(a <= b) ==> (2 * a - (2 * b + 1) = 2 * (a - b) - 1n)``] THEN 947 RW_TAC int_ss [int_div,ONCE_REWRITE_RULE [MULT_COMM] MULT_DIV,MOD2_ODD_EVEN, 948 EVEN_MULT,EVEN_SUB,DIV2_MULT_SUB1,INT_ADD_CALCULATE]); 949 950val rwr2 = SIMP_RULE arith_ss [] (Q.SPEC `0` rwr1); 951 952val iand_lem1 = prove(``!a x. a < 2 ** x ==> (iand (~ & (2 ** x - a)) 953 (~ & (2 ** x)) = ~ & (2 ** x))``, 954 completeInduct_on `a` THEN Cases THEN ONCE_REWRITE_TAC [iand_def] THEN 955 RW_TAC bint_ss [rwr1,rwr2,EXP] THEN1 956 FULL_SIMP_TAC int_ss [int_mod,rwr1,rwr2,INT_SUB_CALCULATE, 957 INT_ADD_CALCULATE,INT_MUL_CALCULATE] THEN 958 Cases_on `a = 0` THEN TRY (POP_ASSUM SUBST_ALL_TAC) THEN 959 PAT_ASSUM ``!m:'a. P`` (MP_TAC o Q.SPEC `a DIV 2`) THEN 960 RW_TAC int_ss [DIV_LT_X] THEN 961 FULL_SIMP_TAC int_ss [IAND_ID,INT_MUL_CALCULATE]); 962 963val div2_lem = prove(``!a b. a DIV 2 + b DIV 2 < a + b = 0 < a \/ 0 < b``, 964 REPEAT GEN_TAC THEN EQ_TAC THEN Cases_on `0 < a` THEN Cases_on `0 < b` THEN 965 FULL_SIMP_TAC arith_ss [DECIDE ``~(0 < a) = (a = 0n)``] THEN 966 MATCH_MP_TAC LT_ADD2 THEN RW_TAC arith_ss [DIV_LT_X]); 967 968val iand_top1 = prove(``b < 2 ** a ==> (iand (& (2 ** a - 1)) (& b) = & b)``, 969 `2 ** a - 1 < 2n ** a` by ALL_TAC THEN 970 RW_TAC int_ss [Q.SPECL [`a`,`2 ** a - 1`,`b`] (GSYM bitwise_iand1), 971 BITWISE_TOP]); 972 973val sub_mod_lem = prove(``& a - & (a - a MOD 2) = & (a MOD 2)``, 974 DISJ_CASES_TAC (Q.SPEC `a` EVEN_OR_ODD) THEN Cases_on `a` THEN 975 REPEAT (POP_ASSUM MP_TAC) THEN 976 RW_TAC int_ss [int_sub_calc1,GSYM MOD2_ODD_EVEN]); 977 978val sub_mod_lem2 = prove(``a < 2 * 2 ** n ==> 979 (& (2 * 2 ** n - (a - a MOD 2)) - & (2 * 2 ** n - a) = & (a MOD 2))``, 980 DISJ_CASES_TAC (Q.SPEC `a` EVEN_OR_ODD) THEN Cases_on `a` THEN 981 REPEAT (POP_ASSUM MP_TAC) THEN 982 RW_TAC int_ss [int_sub_calc1,GSYM MOD2_ODD_EVEN]); 983 984val lem2 = prove(``!n a. ~(a = 0) /\ a < 2 * 2 ** n ==> 985 (& (2 * 2 ** n - (a - 1)) - & (2 * 2 ** n - a) = 1)``, 986 Induct THEN 987 RW_TAC int_ss [ARITH_PROVE ``(a - b = c) = (a = b + c:int)``,INT_ADD, 988 INT_EQ_CALCULATE]); 989 990val lem3 = prove(``!a. (2 * 2 ** a - 1) MOD 2 = 1``, 991 Induct THEN RW_TAC arith_ss [MOD2_ODD_EVEN,ODD_SUB,ODD_MULT,EXP, 992 DECIDE ``0 < a ==> 1n < 4 * a``]); 993 994val iand_nbit = prove(``!b n. b < 2 ** n ==> (iand (~ & (2 ** n)) (& b) = 0)``, 995 GEN_TAC THEN completeInduct_on `b` THEN Cases THEN 996 ONCE_REWRITE_TAC [iand_def] THEN 997 RW_TAC bint_ss [int_mod,rwr1,rwr2,EXP,INT_SUB_CALCULATE, 998 INT_ADD_CALCULATE,INT_MUL_CALCULATE] THEN 999 FIRST_ASSUM (MATCH_MP_TAC o CONV_RULE (STRIP_QUANT_CONV 1000 RIGHT_IMP_FORALL_CONV THENC REWRITE_CONV [AND_IMP_INTRO])) THEN 1001 RW_TAC int_ss [DIV_LT_X]); 1002 1003val IAND_NEG_TAC = 1004 NTAC 2 GEN_TAC THEN completeInduct_on `a + b` THEN 1005 ONCE_REWRITE_TAC [iand_def] THEN NTAC 3 STRIP_TAC THEN 1006 POP_ASSUM SUBST_ALL_TAC THEN 1007 Cases THEN REWRITE_TAC [EXP,INT_EQ_CALCULATE,INT_EXP, 1008 DECIDE ``(a - b = 0n) = (a <= b)``,DECIDE ``(a < 1n) = (a = 0n)``, 1009 DECIDE ``(a - b = 1) = (a = 1n + b)``,DECIDE ``~(1 = 0n)``, 1010 SIMP_RULE int_ss [] (Q.SPECL [`i`,`2`] int_mod),LET_DEF, 1011 SIMP_RULE arith_ss [] (Q.SPECL [`i`,`2`] INT_DIV),rwr1,rwr2, 1012 INT_MUL_CALCULATE,INT_ADD_CALCULATE,RIGHT_SUB_DISTRIB, 1013 ONCE_REWRITE_RULE [MULT_COMM] DIV_MULT_THM2] THEN 1014 POP_ASSUM (MP_TAC o Q.SPEC `a DIV 2 + b DIV 2`) THEN1 RW_TAC int_ss [] THEN 1015 REPEAT IF_CASES_TAC THEN BETA_TAC THEN 1016 ASM_REWRITE_TAC [NOT_LESS_EQUAL,two_rule ZERO_DIV, 1017 two_rule (Q.SPECL [`x`,`y`] DIV_LT_X),ADD_CLAUSES,ZERO_LT_TWOEXP, 1018 MULT_CLAUSES,DECIDE ``b < b * 2 = 0n < b``,ZERO_LESS_MULT, 1019 INT_SUB_LZERO,INT_EQ_CALCULATE,DECIDE ``(a = 0) = ~(0n < a)``, 1020 DECIDE ``0 < 2n /\ ~(0 < 0n) /\ 0 < 1n``, 1021 DECIDE ``(1 = 1 - b) = (b = 0n)``,div2_lem,sub_mod_lem, 1022 DECIDE ``b < 1 = (b = 0n)``,SUB_0,INT_ADD_CALCULATE] THEN 1023 RW_TAC int_ss [] THEN 1024 IMP_RES_TAC (REWRITE_RULE [GSYM NOT_LESS_EQUAL] sub_mod_lem2) THEN 1025 FULL_SIMP_TAC int_ss [ARITH_PROVE ``(~& (2 * a) = 2 * b) = (~ & a = b)``, 1026 sub_mod_lem, 1027 ARITH_PROVE ``(2 * i + 1 - & (2 * b) = 2 * j + 1i) = (i - & b = j)``, 1028 ARITH_PROVE ``(2 * i - & (2 * b) = 2i* j) = (i - & b = j)``] THEN 1029 TRY (MAP_FIRST (fn x => x by (RW_TAC arith_ss [DIV_LT_X] THEN NO_TAC) THEN 1030 POP_ASSUM SUBST_ALL_TAC) 1031 [`a DIV 2 < 2 ** n /\ (b = 2 * 2 ** n - 1)`, 1032 `b DIV 2 < 2 ** n /\ (a = 2 * 2 ** n - 1)`]) THEN 1033 TRY (FIRST_ASSUM (MATCH_MP_TAC o CONV_RULE (STRIP_QUANT_CONV 1034 RIGHT_IMP_FORALL_CONV THENC REWRITE_CONV [AND_IMP_INTRO])) THEN 1035 RW_TAC int_ss [DIV_LT_X]) THEN 1036 TRY (MATCH_MP_TAC (GSYM (ONCE_REWRITE_RULE [IAND_COMM] iand_lem1)) THEN 1037 RW_TAC int_ss [DIV_LT_X]) THEN 1038 TRY (MATCH_MP_TAC (GSYM iand_lem1) THEN RW_TAC int_ss [DIV_LT_X]) THEN 1039 REPEAT (PAT_ASSUM ``a = & (b MOD 2)`` (K ALL_TAC)) THEN 1040 PAT_ASSUM ``!m:'a.P`` (K ALL_TAC) THEN 1041 FULL_SIMP_TAC bool_ss [DECIDE ``(a - 1 + 1 = (if 0 < a then a else 1n))``, 1042 ZERO_LESS_MULT,ZERO_LT_TWOEXP,DECIDE ``0 < 2n``, 1043 MATCH_MP DIV2_MULT_SUB1 (SPEC_ALL ZERO_LT_TWOEXP),NOT_MOD2] THEN 1044 RW_TAC std_ss [INT_MUL,iand_top1, 1045 ONCE_REWRITE_RULE [IAND_COMM] iand_top1] THEN 1046 RW_TAC int_ss [INT_EQ_SUB_RADD,INT_ADD_CALCULATE,DIV_MULT_THM2] THEN 1047 TRY (METIS_TAC [REWRITE_RULE [GSYM NOT_LESS_EQUAL] lem2,lem3, 1048 SIMP_RULE arith_ss [EXP,GSYM (CONJUNCT1 NOT_MOD2)] 1049 (Q.SPECL [`SUC n`,`1`] MOD_HIGH_MOD)]); 1050 1051val iand_neg1 = prove(``!a b x. a < 2 ** x /\ b < 2 ** x ==> 1052 (iand (& a) (& b) - & 2 ** x = 1053 iand (~ & (2 ** x - a)) (~ & (2 ** x - b)))``, 1054 IAND_NEG_TAC); 1055 1056val iand_neg2 = prove(``!a b x. a < 2 ** x /\ b < 2 ** x ==> 1057 (iand (& a) (& b) = iand (~ & (2 ** x - a)) (& b))``, 1058 IAND_NEG_TAC THEN MATCH_MP_TAC iand_nbit THEN RW_TAC arith_ss [DIV_LT_X]); 1059 1060 1061val sw2i_and = store_thm("sw2i_and", 1062 ``!a b. sw2i (a && b) = iand (sw2i a) (sw2i b)``, 1063 REWRITE_TAC [REWRITE_RULE [n2w_w2n] 1064 (Q.SPECL [`w2n a`,`w2n b`] word_and_n2w)] THEN 1065 RW_TAC int_ss [sw2i_def,w2n_n2w,BIT_MOD,BITWISE_THM,DIMINDEX_GT_0, 1066 DECIDE ``0 < a ==> (a - 1n < a)``,dimword_def] THEN 1067 FULL_SIMP_TAC int_ss [TOP_BIT_LE,int_sub_calc1,w2n_lt_full, 1068 REWRITE_RULE [GSYM NOT_LESS_EQUAL] MOD_LESS,bitwise_mod_lem, 1069 bitwise_iand2,bitwise_iand3, 1070 REWRITE_RULE [GSYM NOT_LESS_EQUAL,INT_EXP] iand_neg1, 1071 REWRITE_RULE [GSYM NOT_LESS_EQUAL,INT_EXP] iand_neg2, 1072 ONCE_REWRITE_RULE [IAND_COMM] 1073 (REWRITE_RULE [GSYM NOT_LESS_EQUAL,INT_EXP] iand_neg2)]); 1074 1075(*****************************************************************************) 1076(* sw2i_not : |- !a. sw2i (~a) = inot (sw2i a) *) 1077(*****************************************************************************) 1078 1079val sw2i_not = store_thm("sw2i_not",``!a. sw2i (~a) = inot (sw2i a)``, 1080 REWRITE_TAC [inot_def,WORD_NOT,sw2i_sub,sw2i_twocomp] THEN 1081 REWRITE_TAC [sw2i_thm] THEN CONV_TAC (DEPTH_CONV EXTEND_CONV) THEN 1082 RW_TAC int_ss [eindex EXTEND_EQ,eindex EXTEND_LIMIT, 1083 ARITH_PROVE ``a + 1i <= b = a < b``, 1084 ARITH_PROVE ``~(a + 1i) < b = ~b <= a``,word_1_n2w] THEN 1085 RW_TAC int_ss [ARITH_PROVE ``(~(a + 1) = ~b - 1 + m) = (b = a + m)``] THEN 1086 Cases_on `w2n a < 2 ** (dimindex (:'a) - 1)` THENL 1087 (map Q.EXISTS_TAC [`0`,`1`]) THEN 1088 RW_TAC int_ss [GSYM sw2i_thm,sw2i_def,BIT_RWR,SUC_SUB_INDEX,w2n_lt_full]); 1089 1090(*****************************************************************************) 1091(* sw2i_div : |- !a b. ~(b = 0w) ==> (sw2i (a / b) = *) 1092(* extend (sw2i a quot sw2i b) (dimindex (:'a))) *) 1093(*****************************************************************************) 1094 1095val num_msb = REWRITE_RULE [n2w_w2n] (Q.SPEC `w2n a` word_msb_n2w); 1096 1097val lem1 = prove(``~(b = 0w) /\ ~word_msb a /\ ~word_msb b ==> 1098 (& (w2n (a / b)) = & (w2n a) / & (w2n b))``, 1099 REPEAT STRIP_TAC THEN 1100 `0 < w2n b` by METIS_TAC [w2n_eq_0,DECIDE ``~(a = 0) = 0n < a``] THEN 1101 RW_TAC int_ss [word_sdiv_def,word_div_def,w2n_n2w,dimword_def] THEN 1102 NLELT_TRANS_TAC `w2n a` THEN 1103 RW_TAC int_ss [w2n_lt_full,DIV_LESS_EQ]); 1104 1105val plem1 = prove(``!b. ~(b = 0w : 'a word) ==> 1106 ((w2n (a:'a word) DIV w2n b) MOD 2 ** dimindex (:'a) = w2n a DIV w2n b)``, 1107 REPEAT STRIP_TAC THEN MATCH_MP_TAC LESS_MOD THEN 1108 NLELT_TRANS_TAC `w2n a` THEN CONJ_TAC THEN 1109 TRY (MATCH_MP_TAC DIV_LESS_EQ) THEN 1110 RW_TAC int_ss [w2n_lt_full,w2n_eq_0,DECIDE ``0 < b = ~(b = 0n)``]); 1111 1112val plem2 = REWRITE_RULE [WORD_NEG_EQ_0] (Q.SPEC `- b` plem1); 1113 1114val plem3 = prove(``!n. 0 < n ==> (2 ** (n - 1) <= (2 ** n - x) MOD 2 ** n = 1115 0 < x /\ x <= 2 ** (n - 1))``, 1116 Cases THEN Cases_on `x` THEN 1117 RW_TAC int_ss [DIVMOD_ID, 1118 DECIDE ``a <= b - c = a + c <= b:num \/ (a = 0n)``] THEN 1119 RW_TAC int_ss [EXP]); 1120 1121val plem4 = REWRITE_RULE [DIMINDEX_GT_0] (Q.SPEC `dimindex (:'a)` plem3); 1122 1123val plem5 = GSYM (REWRITE_RULE [w2n_n2w] 1124 (PART_MATCH rhs w2n_eq_0 ``n2w a = 0w``)); 1125 1126val plem6 = prove(``0 < b ==> ((a DIV b = 0) = a < b)``, 1127 RW_TAC int_ss [DECIDE ``(a = 0) = a < 1n``,DIV_LT_X]); 1128 1129val slem = prove(``!a b D. 0 < b /\ a:num < D ==> a * D + D < b + D ** 2``, 1130 REPEAT STRIP_TAC THEN IMP_RES_TAC LESS_ADD_1 THEN 1131 REWRITE_TAC [GSYM (EVAL ``1 + 1n``),EXP_ADD,EXP_1] THEN 1132 RW_TAC arith_ss [LEFT_ADD_DISTRIB,RIGHT_ADD_DISTRIB]); 1133 1134val msb_div = prove(``~(b = 0w) /\ ~(b = UINT_MAXw) ==> 1135 (word_msb (a / b) = ~(word_msb a = word_msb b) /\ ~(a / b = 0w))``, 1136 REPEAT STRIP_TAC THEN 1137 `0 < w2n b /\ 0 < w2n (- b)` by METIS_TAC 1138 [DECIDE ``0 < a = ~(a = 0n)``,w2n_eq_0,WORD_NEG_EQ_0] THEN 1139 Cases_on `a / b = 0w` THEN POP_ASSUM MP_TAC THEN 1140 RW_TAC int_ss [WORD_NEG_EQ_0,num_msb,word_sdiv_def,BIT_RWR,SUC_SUB_INDEX, 1141 w2n_lt_full,NOT_LESS_EQUAL,word_div_def,w2n_n2w,dimword_def,plem1, 1142 plem2,plem4,plem5,plem6] THEN 1143 RW_TAC int_ss [word_2comp_n2w,w2n_n2w,dimword_def,plem1,plem2,plem4,plem6, 1144 plem5,X_LT_DIV] THEN 1145 RW_TAC int_ss [DIMINDEX_DOUBLE, 1146 DECIDE ``a <= 2 * a - b = (a = 0n) \/ b <= a``] THENL [ 1147 ALL_TAC,NLE_TRANS_TAC `w2n (- a)`, 1148 NLE_TRANS_TAC `w2n a`,NLELT_TRANS_TAC `w2n a`] THEN 1149 RW_TAC int_ss [DIV_LESS_EQ,word_2comp_def,w2n_n2w, 1150 dimword_def,DIMINDEX_DOUBLE] THEN 1151 `0 < 2 ** dimindex (:'a) - w2n b` by ALL_TAC THEN 1152 Cases_on `w2n a = 0` THEN 1153 RW_TAC int_ss [GSYM DIMINDEX_DOUBLE,DIV_LT_X,w2n_lt_full, 1154 DECIDE ``0n < a - b = b < a``,ZERO_LESS_MULT,LEFT_SUB_DISTRIB] THEN 1155 IMP_RES_TAC LESS_EQUAL_ADD THEN 1156 RW_TAC int_ss [DIMINDEX_DOUBLE,DECIDE ``2 * a < b + a + c = a < b + c:num``, 1157 RIGHT_ADD_DISTRIB] THEN 1158 `p < 2 ** (dimindex (:'a) - 1)` by METIS_TAC [TIMES2,LT_ADD_LCANCEL, 1159 DIMINDEX_DOUBLE,w2n_lt_full] THEN 1160 MATCH_MP_TAC (DECIDE ``(D:num) + a * D < b + D ** 2 /\ a * D < D ** 2 ==> 1161 D < b + (D ** 2 - a * D)``) THEN 1162 REWRITE_TAC [GSYM (EVAL ``1 + 1n``),EXP_ADD,EXP_1] THEN 1163 RW_TAC int_ss [] THEN 1164 Cases_on `p' = 0` THEN RW_TAC int_ss [] THENL [ 1165 REWRITE_TAC [REWRITE_RULE [MULT_CLAUSES] 1166 (GSYM (Q.SPECL [`a`,`1`,`b`] RIGHT_ADD_DISTRIB)), 1167 GSYM (EVAL ``1 + 1n``),EXP_ADD,EXP_1,LT_MULT_RCANCEL] THEN 1168 RW_TAC int_ss [DECIDE ``a + 1 < b = a < b /\ ~(a = b - 1n)``] THEN 1169 CCONTR_TAC THEN 1170 FULL_SIMP_TAC int_ss [GSYM DIMINDEX_DOUBLE,word_T_def, 1171 UINT_MAX_def,dimword_def] THEN 1172 METIS_TAC [n2w_w2n], 1173 MATCH_MP_TAC slem] THEN 1174 RW_TAC int_ss []); 1175 1176val lem2 = prove(``~(b = 0w) /\ (w2n a = 0) ==> (a / b = 0w)``, 1177 `w2n b < 2 ** dimindex (:'a)` by ALL_TAC THEN 1178 RW_TAC int_ss [word_sdiv_def,word_div_def,word_2comp_def,w2n_n2w, 1179 dimword_def,ZERO_DIV,GSYM w2n_eq_0,w2n_lt_full]); 1180 1181val lem3 = prove(``~(a = 0) /\ ~(b = 0) ==> (((2 ** n - a) DIV b) MOD 2 ** n = 1182 (2 ** n - a) DIV b)``, 1183 Cases_on `2 ** n <= a` THEN 1184 RW_TAC int_ss [DECIDE ``a <= b ==> (a - b = 0n)``,ZERO_DIV] THEN 1185 FULL_SIMP_TAC int_ss [NOT_LESS_EQUAL] THEN IMP_RES_TAC LESS_ADD THEN 1186 POP_ASSUM (SUBST_ALL_TAC o GSYM) THEN RW_TAC int_ss [] THEN 1187 NLELT_TRANS_TAC `p` THEN RW_TAC int_ss [DIV_LESS_EQ]); 1188 1189val lem4 = prove(``(w2n a = 0) ==> ~word_msb a``, 1190 RW_TAC int_ss [num_msb,BIT_RWR]); 1191 1192val lem5 = prove(``~(w2n a = 0) ==> (2 ** dimindex (:'a) - w2n (a:'a word)) 1193 DIV (2 ** dimindex (:'a) - w2n (b:'a word)) 1194 < 2 ** dimindex (:'a)``, 1195 DISCH_TAC THEN NLELT_TRANS_TAC `2 ** dimindex (:'a) - w2n a` THEN 1196 RW_TAC int_ss [DIV_LESS_EQ,DECIDE ``a < b ==> 0n < b - a``,w2n_lt_full]); 1197 1198val lem6 = prove(``~(w2n a = 0) ==> ~(w2n b = 0) ==> 1199 (2 ** dimindex (:'a) - w2n (a:'a word)) DIV w2n (b:'a word) 1200 < 2 ** dimindex (:'a)``, 1201 REPEAT DISCH_TAC THEN NLELT_TRANS_TAC `2 ** dimindex (:'a) - w2n a` THEN 1202 RW_TAC int_ss [DIV_LESS_EQ,DECIDE ``a < b ==> 0n < b - a``,w2n_lt_full]); 1203 1204val lem7 = prove(``(2 ** a - b) MOD 2 ** a = if b = 0 then 0 else 2 ** a - b``, 1205 RW_TAC arith_ss []); 1206 1207val lem8 = prove(``~(b = 0) /\ (a DIV b = 0) ==> (a MOD b = a)``, 1208 REPEAT (RW_TAC int_ss [DECIDE ``(a = 0) = a < 1n``,DIV_LT_X, 1209 DECIDE ``~(b = 0n) = 0 < b``] THEN REPEAT (POP_ASSUM MP_TAC))); 1210 1211val lem9 = prove(``~(b = 0) ==> ((a DIV b = 0) = a < b)``, 1212 REPEAT (RW_TAC int_ss [DECIDE ``(a = 0) = a < 1n``,DIV_LT_X, 1213 DECIDE ``~(b = 0n) = 0 < b``] THEN REPEAT (POP_ASSUM MP_TAC))); 1214 1215val slem1 = prove(``a < 2 ** D /\ 2 ** D <= b /\ b < 2 * 2 ** D /\ 1216 ~(b = 2 * 2 ** D - 1) ==> 1217 a < 2n * 2 ** D * (2 * 2 ** D - b)``, 1218 STRIP_TAC THEN NLT_TRANS_TAC `2 * 2 ** D` THEN 1219 RW_TAC int_ss [REWRITE_RULE [MULT_CLAUSES] (Q.SPECL [`D`,`1`,`p`] 1220 LT_MULT_LCANCEL)]); 1221 1222val sw2i_div_1 = prove(``!a b. ~(b = 0w) /\ ~(b = UINT_MAXw) ==> 1223 (sw2i (a / b : 'a word) = (sw2i a) quot (sw2i b))``, 1224 REPEAT GEN_TAC THEN DISCH_TAC THEN 1225 FIRST_ASSUM (STRIP_ASSUME_TAC o MATCH_MP msb_div) THEN 1226 REPEAT (POP_ASSUM MP_TAC) THEN 1227 RW_TAC int_ss [sw2i_def,GSYM num_msb,lem1,msb_div] THEN 1228 REPEAT (POP_ASSUM MP_TAC) THEN RW_TAC std_ss [] THEN 1229 RW_TAC int_ss [word_0_n2w,int_sub_calc1,w2n_lt_full] THEN 1230 `~(w2n b = 0)` by ASM_REWRITE_TAC [w2n_eq_0] THEN 1231 TRY (`~(w2n a = 0)` by (CCONTR_TAC THEN FULL_SIMP_TAC std_ss [] THEN 1232 MAP_EVERY IMP_RES_TAC [lem2,lem4] THEN NO_TAC)) THEN 1233 FIRST_ASSUM (STRIP_ASSUME_TAC o MATCH_MP LESS_MOD o MATCH_MP lem5) THEN 1234 FIRST_ASSUM (STRIP_ASSUME_TAC o MATCH_MP lem6) THEN 1235 POP_ASSUM IMP_RES_TAC THEN RW_TAC int_ss [int_quot,word_div_def, 1236 word_sdiv_def,word_2comp_def,w2n_n2w, 1237 dimword_def,w2n_lt,plem6,lem7] THEN 1238 TRY (PAT_ASSUM ``~(a / b= 0w:'a word)`` MP_TAC) THEN 1239 TRY (PAT_ASSUM ``a / b= 0w:'a word`` MP_TAC) THEN 1240 RW_TAC int_ss [word_div_def,word_sdiv_def,word_2comp_def,w2n_n2w, 1241 dimword_def,w2n_lt_full,GSYM w2n_eq_0,lem7,plem6, 1242 DECIDE ``a < b ==> (0n < b - a)``] THEN 1243 FULL_SIMP_TAC int_ss [plem6,num_msb,BIT_RWR,SUC_SUB_INDEX,w2n_lt_full, 1244 NOT_LESS_EQUAL] THEN 1245 `(w2n a DIV (2 ** dimindex (:'a) - w2n b)) MOD 2 ** dimindex (:'a) = 1246 w2n a DIV (2 ** dimindex (:'a) - w2n b)` by MATCH_MP_TAC LESS_MOD THEN 1247 TRY (NLELT_TRANS_TAC `w2n a` THEN 1248 RW_TAC int_ss [DIV_LESS_EQ,w2n_lt_full, 1249 DECIDE ``a < b ==> 0n < b - a``] THEN NO_TAC) THEN 1250 POP_ASSUM SUBST_ALL_TAC THEN 1251 FULL_SIMP_TAC int_ss [plem6,DECIDE ``a < b ==> 0n < b - a``, 1252 w2n_lt_full,NOT_LESS] THEN 1253 FULL_SIMP_TAC int_ss [X_LE_DIV,DECIDE ``a < b ==> 0n < b - a``,w2n_lt_full, 1254 LEFT_SUB_DISTRIB,DIMINDEX_DOUBLE,EXP_BASE_MULT] THEN 1255 POP_ASSUM MP_TAC THEN REWRITE_TAC [NOT_LESS_EQUAL] THEN 1256 MATCH_MP_TAC (SIMP_RULE int_ss [LEFT_SUB_DISTRIB, 1257 DECIDE ``a < b - c = a + c:num < b``] slem1) THEN 1258 FULL_SIMP_TAC int_ss [GSYM DIMINDEX_DOUBLE,w2n_lt_full,word_T_def, 1259 UINT_MAX_def,dimword_def] THEN 1260 METIS_TAC [n2w_w2n]); 1261 1262val sw2i_word_T = store_thm("sw2i_word_T",``sw2i UINT_MAXw = ~1``, 1263 RW_TAC int_ss [word_T_def,UINT_MAX_def,dimword_def,sw2i_def,w2n_n2w,BIT_RWR, 1264 SUC_SUB_INDEX,INT_SUB_CALCULATE,INT_ADD_CALCULATE] THEN 1265 FULL_SIMP_TAC int_ss [DIMINDEX_DOUBLE,DECIDE ``a <= a - 1n = (a = 0n)``]); 1266 1267val lem1 = prove(``1 MOD 2 ** dimindex (:'a) = 1``, 1268 MATCH_MP_TAC LESS_MOD THEN 1269 RW_TAC int_ss [DIMINDEX_DOUBLE,DECIDE ``1 < 2 * a = 0n < a``]); 1270 1271val sw2i_div_T = prove(``sw2i ((a:'a word) / UINT_MAXw) = 1272 extend (sw2i a quot sw2i (UINT_MAXw:'a word)) (dimindex (:'a))``, 1273 RW_TAC int_ss [sw2i_word_T,sw2i_thm] THEN 1274 CONV_TAC (DEPTH_CONV EXTEND_CONV) THEN 1275 RW_TAC int_ss [eindex EXTEND_11,word_T_def,word_div_def, 1276 word_sdiv_def,num_msb,BIT_RWR,SUC_SUB_INDEX,DIV_1,lem1, 1277 UINT_MAX_def,dimword_def,w2n_n2w,w2n_lt_full,word_2comp_def, 1278 DECIDE ``0 < a ==> (a - (a - 1) = 1n)``] THEN 1279 RULE_ASSUM_TAC (REWRITE_RULE [DIMINDEX_DOUBLE]) THEN 1280 FULL_SIMP_TAC int_ss [] THENL [ 1281 Q.EXISTS_TAC `1`, 1282 Cases_on `w2n a = 0` THENL (map Q.EXISTS_TAC [`0`,`1`])] THEN 1283 RW_TAC int_ss [lem7,INT_ADD_CALCULATE] THEN 1284 FULL_SIMP_TAC int_ss [w2n_lt_full,NOT_LESS_EQUAL, 1285 DECIDE ``a < b = a <= b /\ ~(a = b:num)``]); 1286 1287val sw2i_div = store_thm("sw2i_div", 1288 ``!a b. ~(b = 0w) ==> (sw2i ((a:'a word) / b) = 1289 extend (sw2i a quot sw2i b) (dimindex (:'a)))``, 1290 REPEAT GEN_TAC THEN Cases_on `b = UINT_MAXw` THEN 1291 RW_TAC int_ss [sw2i_div_1,sw2i_div_T] THEN 1292 RW_TAC int_ss [eindex EXTEND_EQ,GSYM sw2i_div_1,sw2i_def,BIT_RWR, 1293 w2n_lt_full,SUC_SUB_INDEX, 1294 INT_ADD_CALCULATE,INT_SUB_CALCULATE] THEN 1295 TRY (Q.EXISTS_TAC `0`) THEN RW_TAC int_ss [DIMINDEX_DOUBLE]); 1296 1297val rwr3 = MATCH_MP LESS_MOD (SPEC_ALL BITWISE_LT_2EXP); 1298 1299val bit_lem = prove(``~BIT (dimindex (:'b) - 1) (w2n (a:'b word) DIV 2)``, 1300 RW_TAC int_ss [BIT_RWR,NOT_LESS_EQUAL,SUC_SUB_INDEX,DIV_MOD_MOD_DIV, 1301 DIV_LT_X,GSYM EXP] THEN 1302 `!a. 2n ** a < 2n ** SUC a` by 1303 METIS_TAC [TWOEXP_MONO,DECIDE ``a < SUC a``] THEN 1304 METIS_TAC [w2n_lt_full,TWOEXP_MONO, 1305 DECIDE ``a < SUC a``,LESS_MOD,LESS_TRANS]); 1306 1307val bitwise_lem = prove(``!n x. x < 2 ** n ==> 1308 (BITWISE (SUC n) $\/ (2 ** n) x = 2 ** n + x)``, 1309 Induct THEN ONCE_REWRITE_TAC [BITWISE_DIV] THEN 1310 RW_TAC int_ss [BITWISE_ZERO,EXP,ODD_MULT, 1311 ONCE_REWRITE_RULE [MULT_COMM] MULT_DIV,ODD_TWOEXP] THEN 1312 FULL_SIMP_TAC int_ss [BITWISE_ZERO] THEN 1313 FULL_SIMP_TAC int_ss [GSYM MOD2_ODD_EVEN,NOT_MOD2] THEN 1314 PAT_ASSUM ``!m:'a.P`` (MP_TAC o Q.SPEC `x DIV 2`) THEN 1315 RW_TAC int_ss [DIV_LT_X,LEFT_ADD_DISTRIB,DIV_MULT_THM2] THEN 1316 Cases_on `x` THEN FULL_SIMP_TAC int_ss []); 1317 1318val rwr4 = REWRITE_RULE [SUC_SUB_INDEX] (MATCH_MP bitwise_lem 1319 (prove(``w2n (a:'a word) DIV 2 < 2 ** (dimindex (:'a) - 1)``, 1320 RW_TAC int_ss [DIV_LT_X,GSYM EXP,SUC_SUB_INDEX,w2n_lt_full]))); 1321 1322val rwr5 = prove(``(dimindex (:'a) = 1) ==> 1323 (w2n (a:'a word) = 0) \/ (w2n a = 1)``, 1324 METIS_TAC [w2n_lt_full,EXP_1,DECIDE ``a < 2 = (a = 0) \/ (a = 1n)``]); 1325 1326val sw2i_asr_1 = prove(``!b a. sw2i (a >> 1) = sw2i a / 2``, 1327 RW_TAC std_ss [REWRITE_RULE [n2w_w2n] 1328 (AP_TERM ``n2w:num -> 'a word`` (SPEC_ALL w2n_lsr)),rwr2,rwr3, 1329 word_asr_n2w,sw2i_def,word_or_n2w,MIN_DEF,dimword_def,w2n_n2w,rwr1, 1330 int_sub_calc1,INT_EXP] THEN 1331 FULL_SIMP_TAC int_ss [word_msb_n2w,w2n_n2w, 1332 REWRITE_RULE [n2w_w2n] (Q.SPEC `w2n w` word_msb_n2w), 1333 REWRITE_RULE [GSYM NOT_LESS_EQUAL] BITWISE_LT_2EXP,rwr1,dimword_def, 1334 rwr3,w2n_lt_full] THEN 1335 FULL_SIMP_TAC int_ss [rwr1,rwr2,rwr3,DIMINDEX_DOUBLE,bit_lem,BITWISE_THM, 1336 BIT_B,DIV_LT_X,MATCH_MP (DECIDE ``0 < a ==> (~(1 < a) = (a = 1n))``) 1337 DIMINDEX_GT_0,BIT_MOD,rwr4,rwr5] THEN 1338 TRY (IMP_RES_TAC rwr5 THEN POP_ASSUM (STRIP_ASSUME_TAC o Q.SPEC `a`) THEN 1339 POP_ASSUM SUBST_ALL_TAC) THEN 1340 FULL_SIMP_TAC int_ss [BIT_RWR,SIMP_RULE arith_ss [] 1341 (PART_MATCH lhs BITWISE_DIV ``BITWISE (SUC 0) a b c``), 1342 BITWISE_ZERO] THEN 1343 NLT_TRANS_TAC `2 ** dimindex (:'b)` THEN 1344 REWRITE_TAC [GSYM (EVAL ``2 * 2n``),GSYM MULT_ASSOC,GSYM (CONJUNCT2 EXP), 1345 SUC_SUB_INDEX] THEN 1346 RW_TAC int_ss [w2n_lt_full]); 1347 1348val pos = prove(``!b a. & a / & (2 ** SUC b) = (& a / 2) / 2 ** b``, 1349 RW_TAC int_ss [int_div,EXP,DIV_DIV_DIV_MULT]); 1350 1351val DIV_PLUS_1 = prove(``(m + 1) DIV 2 ** b = m DIV 2 ** b + 1352 if (m MOD 2 ** b + 1 = 2 ** b) then 1 else 0``, 1353 ONCE_REWRITE_TAC [DECIDE ``(a = b) = a <= b /\ b <= a:num``] THEN 1354 RW_TAC int_ss [DIV_LE_X,X_LE_DIV,LEFT_ADD_DISTRIB,RIGHT_ADD_DISTRIB] THEN 1355 RW_TAC int_ss [DIV_MULT_THM] THEN 1356 Cases_on `m < 2 ** b` THEN FULL_SIMP_TAC int_ss [NOT_LESS] THEN 1357 `m MOD 2 ** b < m` by (NLTLE_TRANS_TAC `2 ** b` THEN RW_TAC int_ss []) THEN 1358 RW_TAC int_ss [DECIDE ``a < b - c = a + c < b:num``, 1359 DECIDE ``a + 1 < b = a < b /\ ~(a + 1n = b)``]); 1360 1361val neg = prove(``!b a. ~ & a / & (2 ** SUC b) = (~ & a / 2) / 2 ** b``, 1362 REPEAT GEN_TAC THEN Cases_on `a = 0` THENL 1363 [ALL_TAC,Cases_on `a MOD 2 = 0`] THEN 1364 ASM_REWRITE_TAC [SIMP_RULE int_ss [] (Q.SPECL [`i`,`2 ** a`] int_div), 1365 INT_EXP,ARITH_PROVE ``0 <= ~ & a = (a = 0n)``,INT_NEGNEG, 1366 NUM_OF_INT,SIMP_RULE int_ss [] (Q.SPECL [`i`,`2`] int_div), 1367 INT_NEG_0,SIMP_RULE arith_ss [] (Q.SPEC `2 ** a` ZERO_DIV), 1368 EVAL ``0 DIV 2``,GSYM INT_NEG_ADD,INT_ADD, 1369 DECIDE ``~(a + 1 = 0n)``,INT_ADD_RID] THEN 1370 RW_TAC int_ss [plem6,EXP,DIV_DIV_DIV_MULT,DIV_MOD_MOD_DIV,GSYM INT_NEG_ADD, 1371 INT_EQ_CALCULATE,INT_ADD, 1372 DECIDE ``a < 2 = (a = 0) \/ (a = 1n)``] THEN 1373 FULL_SIMP_TAC arith_ss [GSYM DIV_DIV_DIV_MULT,ZERO_DIV,MOD2_ODD_EVEN, 1374 GSYM ODD_EVEN] THEN 1375 IMP_RES_TAC EVEN_ODD_EXISTS THEN 1376 FULL_SIMP_TAC int_ss [GSYM MOD_COMMON_FACTOR, 1377 SIMP_RULE arith_ss [] (Q.SPECL [`2`,`1`] DIV_MULT),ADD1,MOD_PLUS_1, 1378 SIMP_RULE arith_ss [EXP] (Q.SPEC `2 ** SUC n` MOD_PLUS_1), 1379 DIV_PLUS_1]); 1380 1381val both = prove(``!a b. a / & (2 ** SUC b) = (a / 2) / 2 ** b``, 1382 GEN_TAC THEN INT_CASE_TAC `a` THEN 1383 RW_TAC arith_ss [pos,neg]); 1384 1385val sw2i_asr = store_thm("sw2i_asr",``!b a. sw2i (a >> b) = sw2i a / 2 ** b``, 1386 Induct THEN RW_TAC int_ss [SHIFT_ZERO,both,GSYM sw2i_asr_1] THEN 1387 REWRITE_TAC [ONCE_REWRITE_RULE [ADD_COMM] ADD1,GSYM ASR_ADD] THEN 1388 POP_ASSUM (MP_TAC o Q.SPEC `a >> 1`) THEN RW_TAC int_ss []); 1389 1390val sw2i_lsl = store_thm("sw2i_lsl", 1391 ``sw2i ((a:'a word) << b) = extend (sw2i a * 2 ** b) (dimindex (:'a))``, 1392 RW_TAC int_ss [REWRITE_RULE [n2w_w2n] (Q.SPECL [`n`,`w2n m`] word_lsl_n2w), 1393 sw2i_thm,word_0_n2w, 1394 EXTEND_ZERO,w2n_n2w] THEN 1395 CONV_TAC (DEPTH_CONV EXTEND_CONV) THEN 1396 RW_TAC int_ss [INT_MUL,eindex EXTEND_EQ,eindex EXTEND_11,dimword_def] THEN 1397 FULL_SIMP_TAC int_ss [DECIDE ``a < b + 1n = a <= b``,mod_lem] THENL [ 1398 Q.EXISTS_TAC `~& (w2n a * 2 ** (b - dimindex (:'a)))`, 1399 Q.EXISTS_TAC `0`,Q.EXISTS_TAC `0`] THEN 1400 IMP_RES_TAC LESS_EQUAL_ADD THEN 1401 RW_TAC int_ss [EXP_ADD,INT_MUL_CALCULATE,INT_ADD_CALCULATE, 1402 INT_SUB_CALCULATE]); 1403 1404val sw2i_msb = store_thm("sw2i_msb", 1405 ``word_msb a = sw2i a < 0``, 1406 RW_TAC int_ss [num_msb,sw2i_def,BIT_RWR,INT_SUB_CALCULATE, 1407 INT_ADD_CALCULATE,w2n_lt_full]); 1408 1409(*****************************************************************************) 1410(* sw2i_bit : |- !a b. b < dimindex (:'a) ==> (a ' b = ibit b (sw2i a)) *) 1411(*****************************************************************************) 1412 1413val lem1 = prove(``b < dimindex (:'a) ==> 1414 (BIT b (w2n (a : 'a word)) = a ' b)``, 1415 ONCE_REWRITE_TAC [SIMP_RULE arith_ss [n2w_w2n] 1416 (Q.SPEC `w2n a` word_index_n2w)] THEN 1417 RW_TAC int_ss []); 1418 1419val lem2 = prove(``ODD (w2n a) = word_lsb a``, 1420 RW_TAC int_ss [GSYM BIT_ZERO_ODD,word_lsb_def,lem1,DIMINDEX_GT_0]); 1421 1422val lem3 = prove(``b < dimindex (:'a) ==> 1423 (ODD (w2n (a >> b)) = 2 ** b <= w2n (a:'a word) MOD 2 ** SUC b)``, 1424 RW_TAC int_ss [lem2,word_lsb_def,fcpTheory.FCP_BETA,word_asr_def] THEN 1425 ONCE_REWRITE_TAC [SIMP_RULE arith_ss [n2w_w2n] 1426 (Q.SPEC `w2n a` word_index_n2w)] THEN 1427 RW_TAC int_ss [BIT_RWR]); 1428 1429val sw2i_bit = store_thm("sw2i_bit", 1430 ``!a b. b < dimindex (:'a) ==> (a ' b = ibit b (sw2i (a:'a word)))``, 1431 ONCE_REWRITE_TAC [SIMP_RULE arith_ss [n2w_w2n] 1432 (Q.SPEC `w2n a` word_index_n2w)] THEN 1433 RW_TAC int_ss [BIT_RWR,ibit_def,REWRITE_RULE [INT_EXP] (GSYM sw2i_asr)] THEN 1434 RW_TAC int_ss [sw2i_def,BIT_RWR,SUC_SUB_INDEX,w2n_lt_full,INT_SUB_CALCULATE, 1435 INT_ADD_CALCULATE,INT_ABS_NEG,INT_ABS_NUM,ODD_SUB,ODD_TWOEXP,lem3]); 1436 1437 1438(*****************************************************************************) 1439(* sw2i_eq : |- !a b. (a = b) = (sw2i a = sw2i b) *) 1440(* sw2i_lt : |- !a b. (a < b) = sw2i a < sw2i b *) 1441(* sw2i_le : |- !a b. (a <= b) = sw2i a <= sw2i b *) 1442(* *) 1443(*****************************************************************************) 1444 1445val sw2i_eq = store_thm("sw2i_eq",``!a b. (a = b) = (sw2i a = sw2i b)``, 1446 RW_TAC int_ss [sw2i_def,INT_SUB_CALCULATE,INT_ADD_CALCULATE,BIT_RWR, 1447 SUC_SUB_INDEX,w2n_lt_full,w2n_11, 1448 DECIDE ``b < a /\ c < a ==> ((a - b = a - c) = (b = c:num))``] THEN 1449 METIS_TAC []); 1450 1451val sw2i_lt = store_thm("sw2i_lt",``!a b. a < b = sw2i a < sw2i b``, 1452 RW_TAC int_ss [WORD_LT,sw2i_def,num_msb,INT_SUB_CALCULATE, 1453 INT_ADD_CALCULATE,w2n_lt_full,DECIDE ``0n < a - b = b < a``, 1454 DECIDE ``b < a /\ c < a ==> (a < b + (a - c) = c < b:num)``]); 1455 1456val sw2i_le = store_thm("sw2i_le",``!a b. a <= b = sw2i a <= sw2i b``, 1457 RW_TAC int_ss [WORD_LESS_OR_EQ,sw2i_lt,INT_LE_LT,sw2i_eq]); 1458 1459(*****************************************************************************) 1460(* sw2i_n2w : |- !a. sw2i (n2w a : 'a word) = extend (& a) (dimindex (:'a)) *) 1461(* *) 1462(*****************************************************************************) 1463 1464val mod_lem = prove(``!a b. 0 < b ==> (a MOD b = a - a DIV b * b)``, 1465 REPEAT STRIP_TAC THEN IMP_RES_TAC DIVISION THEN 1466 FIRST_ASSUM (CONV_TAC o RAND_CONV o LAND_CONV o REWR_CONV) THEN 1467 RW_TAC int_ss []); 1468 1469val sw2i_n2w = store_thm("sw2i_n2w", 1470 ``!a. sw2i (n2w a : 'a word) = extend (& a) (dimindex (:'a))``, 1471 RW_TAC int_ss [sw2i_thm,w2n_n2w,dimword_def,mod_lem, 1472 eindex EXTEND_11] THEN 1473 Q.EXISTS_TAC `~ & (a DIV 2 ** dimindex (:'a))` THEN 1474 RW_TAC int_ss [INT_ADD_CALCULATE,INT_MUL_CALCULATE] THEN 1475 METIS_TAC [ZERO_LT_TWOEXP,X_LE_DIV,LESS_EQ_REFL]); 1476 1477(*****************************************************************************) 1478(* Theorems relating word definitions to definitions using operators *) 1479(* that can be converted to use signed integers. *) 1480(*****************************************************************************) 1481 1482(*****************************************************************************) 1483(* WORD_BITS_THM : |- !h l a. (h -- l) a = *) 1484(* a >>> l && n2w (2 ** (h + 1 - l) - 1) *) 1485(*****************************************************************************) 1486val BIT_SHIFT_THM4 = store_thm("BIT_SHIFT_THM4", 1487 ``BIT i (a * 2 ** b) = BIT (i - b) a /\ b <= i``, 1488 METIS_TAC [BIT_SHIFT_THM3,NOT_LESS_EQUAL,BIT_SHIFT_THM2]); 1489 1490val TOP_BIT_THM = store_thm("TOP_BIT_THM",``!a b. BIT a (2 ** b - 1) = a < b``, 1491 Induct_on `a` THEN Cases THEN 1492 RW_TAC int_ss [BIT_ZERO_ODD,ODD_SUB,ODD_TWOEXP,EXP, 1493 DECIDE ``1 < 2 * n = 0n < n``,BIT_ZERO,BIT_DIV,DIV2_MULT_SUB1]); 1494 1495val BIT_RANGE = store_thm("BIT_RANGE", 1496 ``!h l i. BIT i (2 ** h - 2 ** l) = l <= i /\ i < h``, 1497 REPEAT GEN_TAC THEN Cases_on `l < h` THEN 1498 FULL_SIMP_TAC int_ss [NOT_LESS] THEN 1499 MAP_EVERY IMP_RES_TAC [LESS_ADD_1,LESS_EQUAL_ADD] THEN 1500 RW_TAC int_ss (EXP_ADD::GSYM EXP::BIT_SHIFT_THM4::TOP_BIT_THM::BIT_ZERO:: 1501 DECIDE ``0 < a ==> (1 - a = 0n)``:: 1502 map (GSYM o REWRITE_RULE [MULT_CLAUSES]) 1503 [Q.SPECL [`p`,`1`,`l`] LEFT_SUB_DISTRIB, 1504 Q.SPECL [`1`,`p`,`l`] LEFT_SUB_DISTRIB])); 1505 1506val WORD_BITS_THM = store_thm("WORD_BITS_THM", 1507 ``(h -- l) a = a >>> l && n2w (2 ** (h + 1 - l) - 1)``, 1508 RW_TAC int_ss [fcpTheory.CART_EQ,fcpTheory.FCP_BETA,word_bits_def, 1509 word_and_def,word_lsr_def, 1510 PROVE [word_index_n2w] ``i < dimindex (:'a) ==> 1511 ((n2w n :'a word) ' i = BIT i n)``,word_asr_def, 1512 BIT_RANGE,TOP_BIT_THM] THEN EQ_TAC THEN 1513 RW_TAC int_ss [DECIDE ``i < a + 1 - b = i + b <= a:num``]); 1514 1515val WORD_SLICE_THM = store_thm("WORD_SLICE_THM", 1516 ``(h '' l) a = a && n2w (2 ** SUC h - 2 ** l)``, 1517 RW_TAC int_ss [fcpTheory.CART_EQ,fcpTheory.FCP_BETA,word_bits_def, 1518 word_and_def,word_lsr_def, 1519 PROVE [word_index_n2w] 1520 ``i < dimindex (:'a) ==> ((n2w n :'a word) ' i = BIT i n)``, 1521 word_asr_def, BIT_RANGE,TOP_BIT_THM,word_slice_def] THEN 1522 EQ_TAC THEN RW_TAC int_ss []); 1523 1524val _ = export_theory(); 1525