1 2open HolKernel boolLib bossLib Parse; 3open wordsTheory wordsLib bitTheory arithmeticTheory fcpTheory pred_setTheory progTheory; 4 5val _ = new_theory "address"; 6 7infix \\ 8val op \\ = op THEN; 9 10val RW = REWRITE_RULE; 11val RW1 = ONCE_REWRITE_RULE; 12 13 14(* definitions *) 15 16val ALIGNED_def = Define `ALIGNED (x:word32) = (x && 3w = 0w)`; 17 18val ADDR32_def = Define `ADDR32 (x:word30) = (w2w x << 2):word32`; 19val ADDR30_def = Define `ADDR30 (x:word32) = ((31 >< 2) x):word30`; 20 21val CONTAINER_def = Define `CONTAINER x = x:bool`; 22val GUARD_def = Define `GUARD (n:num) x = x:bool`; 23val DUMMY_EQ_def = Define `DUMMY_EQ x y = (x = y:'a)`; 24 25val SING_SET_def = Define `SING_SET x = {x}`; 26 27 28(* theorems *) 29 30val WORD_EQ_XOR_ZERO = store_thm("WORD_EQ_XOR_ZERO", 31 ``!v w. (v ?? w = 0w) = (v = w:'a word)``, 32 SIMP_TAC std_ss [fcpTheory.CART_EQ,word_xor_def,fcpTheory.FCP_BETA,word_0]); 33 34val ZERO_word30 = store_thm("ZERO_word30", 35 ``1073741824w = 0w:word30``, 36 SRW_TAC [WORD_ARITH_EQ_ss] []); 37 38val lem = (GEN_ALL o SIMP_RULE std_ss [AND_IMP_INTRO] o 39 Q.DISCH `dimindex (:'b) - 1 = h` o 40 SIMP_RULE (arith_ss++WORD_EXTRACT_ss) [] o 41 Q.DISCH `dimindex(:'b) < dimindex(:'a)` o SPEC_ALL) WORD_w2w_OVER_ADD; 42 43val lower_ADDR32_ADD = store_thm("lower_ADDR32_ADD", 44 ``!w x. (1 >< 0) (ADDR32 x + w) = ((1 >< 0) w):word2``, 45 SRW_TAC [ARITH_ss, WORD_EXTRACT_ss] [lem, ADDR32_def]); 46 47val ADDR32_eq_0 = store_thm("ADDR32_eq_0", 48 ``!x. (1 >< 0) (ADDR32 x) = 0w:word2``, 49 SRW_TAC [ARITH_ss, WORD_EXTRACT_ss] [ADDR32_def]); 50 51val ADDR32_n2w = store_thm ("ADDR32_n2w", 52 ``!n. (ADDR32 (n2w n) = n2w (4 * n))``, 53 SIMP_TAC (std_ss++WORD_MUL_LSL_ss) [GSYM word_mul_n2w, ADDR32_def] 54 \\ SRW_TAC [WORD_BIT_EQ_ss] [n2w_def]); 55 56val n2w_and_1 = store_thm("n2w_and_1", 57 ``!n. (n2w n) && 1w = n2w (n MOD 2):'a word``, 58 SIMP_TAC std_ss [(SIMP_RULE std_ss [] o GSYM o Q.SPEC `0`) BITS_ZERO3] 59 \\ SRW_TAC [WORD_BIT_EQ_ss, BIT_ss] [n2w_def] 60 \\ Cases_on `i = 0` 61 \\ SRW_TAC [ARITH_ss] [BIT_def, BITS_ZERO, BITS_COMP_THM2]); 62 63val n2w_and_3 = store_thm("n2w_and_3", 64 ``!n. (n2w n) && 3w = n2w (n MOD 4):'a word``, 65 SIMP_TAC std_ss [(SIMP_RULE std_ss [] o GSYM o Q.SPEC `1`) BITS_ZERO3] 66 \\ SRW_TAC [WORD_BIT_EQ_ss, BIT_ss] [n2w_def] 67 \\ Cases_on `i = 0` \\ Cases_on `i = 1` 68 \\ SRW_TAC [ARITH_ss] [BIT_def, BITS_ZERO, BITS_COMP_THM2]); 69 70val n2w_and_7 = store_thm("n2w_and_7", 71 ``!n. (n2w n) && 7w = n2w (n MOD 8):'a word``, 72 SIMP_TAC std_ss [(SIMP_RULE std_ss [] o GSYM o Q.SPEC `2`) BITS_ZERO3] 73 \\ SRW_TAC [WORD_BIT_EQ_ss, BIT_ss] [n2w_def] 74 \\ Cases_on `i = 0` \\ Cases_on `i = 1` \\ Cases_on `i = 2` 75 \\ SRW_TAC [ARITH_ss] [BIT_def, BITS_ZERO, BITS_COMP_THM2]); 76 77val ALIGNED_n2w = store_thm("ALIGNED_n2w", 78 ``!n. ALIGNED (n2w n) = (n MOD 4 = 0)``, 79 STRIP_TAC \\ SIMP_TAC (std_ss++wordsLib.SIZES_ss) [n2w_and_3,ALIGNED_def,n2w_11] 80 \\ `n MOD 4 < 4` by METIS_TAC [DIVISION,DECIDE ``0<4``] 81 \\ `n MOD 4 < 4294967296` by DECIDE_TAC 82 \\ ASM_SIMP_TAC std_ss [LESS_MOD]); 83 84val ALIGNED_MULT = store_thm("ALIGNED_MULT", 85 ``!x y. ALIGNED x ==> ALIGNED (x + 4w * y)``, 86 Cases_word \\ Cases_word 87 \\ REWRITE_TAC [word_add_n2w,word_mul_n2w,ALIGNED_def,n2w_and_3] 88 \\ ONCE_REWRITE_TAC [ADD_COMM] \\ ONCE_REWRITE_TAC [MULT_COMM] 89 \\ SIMP_TAC std_ss [MOD_TIMES]); 90 91val ADDR32_and_3w = store_thm("ADDR32_and_3w", 92 ``!x. (ADDR32 x) && 3w = 0w``, 93 wordsLib.Cases_word \\ REWRITE_TAC [ADDR32_n2w,n2w_and_3] 94 \\ SIMP_TAC std_ss [RW1 [MULT_COMM] MOD_EQ_0]); 95 96val ALIGNED_ADDR32 = store_thm("ALIGNED_ADDR32", 97 ``!x. ALIGNED (ADDR32 x)``, 98 REWRITE_TAC [ALIGNED_def, ADDR32_and_3w]); 99 100val ADDR30_n2w = store_thm("ADDR30_n2w", 101 ``!n. ADDR30 (n2w n) = n2w (n DIV 4)``, 102 SRW_TAC [SIZES_ss] [ADDR30_def, word_extract_n2w, BITS_THM]); 103 104val ADDR30_ADDR32_ADD = store_thm("ADDR30_ADDR32_ADD", 105 ``!x y. ADDR30 (ADDR32 x + y) = x + ADDR30 y``, 106 wordsLib.Cases_word \\ wordsLib.Cases_word 107 \\ REWRITE_TAC [ADDR30_n2w,ADDR32_n2w,word_add_n2w] 108 \\ SIMP_TAC std_ss [ONCE_REWRITE_RULE [MULT_COMM] ADD_DIV_ADD_DIV]); 109 110val ADDR30_ADDR32_LEMMA = prove( 111 ``!a. (ADDR30 (ADDR32 a + 0w) = a) /\ 112 (ADDR30 (ADDR32 a + 1w) = a) /\ 113 (ADDR30 (ADDR32 a + 2w) = a) /\ 114 (ADDR30 (ADDR32 a + 3w) = a)``, 115 SIMP_TAC std_ss [ADDR30_ADDR32_ADD,ADDR30_n2w,WORD_ADD_0]); 116 117val ADDR30_ADDR32 = store_thm("ADDR30_ADDR32", 118 ``!x. (ADDR30 (ADDR32 x) = x) /\ 119 (ADDR30 (ADDR32 x + 0w) = x) /\ 120 (ADDR30 (ADDR32 x + 1w) = x) /\ 121 (ADDR30 (ADDR32 x + 2w) = x) /\ 122 (ADDR30 (ADDR32 x + 3w) = x)``, 123 REWRITE_TAC 124 [REWRITE_RULE [WORD_ADD_0] ADDR30_ADDR32_LEMMA,ADDR30_ADDR32_LEMMA]); 125 126val EXISTS_ADDR30 = store_thm("EXISTS_ADDR30", 127 ``!x. (x && 3w = 0w) ==> ?y. x = ADDR32 y``, 128 SRW_TAC [] [ADDR32_def] \\ Q.EXISTS_TAC `(31 >< 2) x` 129 \\ SRW_TAC [WORD_EXTRACT_ss] [] 130 \\ FULL_SIMP_TAC (std_ss++WORD_BIT_EQ_ss++wordsLib.BIT_ss) [n2w_def]); 131 132val add32_ADDR30 = store_thm("ADDR32_ADDR30", 133 ``!x. (x && 3w = 0w) ==> (ADDR32 (ADDR30 x) = x)``, 134 REPEAT STRIP_TAC \\ IMP_RES_TAC EXISTS_ADDR30 135 \\ ASM_REWRITE_TAC [ADDR30_ADDR32]); 136 137val ADDR32_ADD = store_thm ("ADDR32_ADD", 138 ``!v w. (ADDR32 (v + w) = ADDR32 v + ADDR32 w)``, 139 Cases_word \\ Cases_word 140 \\ REWRITE_TAC [ADDR32_n2w,word_add_n2w,LEFT_ADD_DISTRIB]); 141 142val ADDR32_NEG = store_thm("ADDR32_NEG", 143 ``!w. ADDR32 (- w) = - (ADDR32 w)``, 144 wordsLib.Cases_word \\ REWRITE_TAC [ADDR32_n2w] 145 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [word_2comp_n2w] 146 \\ `(4 * n) < 4294967296` by DECIDE_TAC 147 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [word_2comp_n2w,ADDR32_n2w,LEFT_SUB_DISTRIB]); 148 149val ADDR32_SUB = store_thm ("ADDR32_SUB", 150 ``!v w. (ADDR32 (v - w) = ADDR32 v - ADDR32 w)``, 151 REWRITE_TAC [word_sub_def,ADDR32_ADD,ADDR32_NEG]); 152 153val ADDR32_SUC = store_thm("ADDR32_SUC", 154 ``!p. ADDR32 (p + 1w) = ADDR32 p + 4w``, 155 SIMP_TAC std_ss [ADDR32_ADD,ADDR32_n2w]); 156 157val ADDR30_ADD = store_thm("ADDR30_ADD", 158 ``!x m. ADDR30 x + n2w m = ADDR30 (x + n2w (4 * m))``, 159 Cases_word \\ REWRITE_TAC [ADDR30_n2w,word_add_n2w] 160 \\ ONCE_REWRITE_TAC [ADD_COMM] 161 \\ SIMP_TAC std_ss [GSYM ADD_DIV_ADD_DIV,AC MULT_COMM MULT_ASSOC]); 162 163val ADD_LSL = save_thm("ADD_LSL", WORD_ADD_LSL); 164 165val ADDR32_11 = store_thm("ADDR32_11", 166 ``!a b. ((ADDR32 a = ADDR32 b) = (a = b)) /\ 167 ((ADDR32 a = ADDR32 b + 0w) = (a = b)) /\ 168 ((ADDR32 a + 0w = ADDR32 b) = (a = b)) /\ 169 ((ADDR32 a + 0w = ADDR32 b + 0w) = (a = b)) /\ 170 ((ADDR32 a + 1w = ADDR32 b + 1w) = (a = b)) /\ 171 ((ADDR32 a + 2w = ADDR32 b + 2w) = (a = b)) /\ 172 ((ADDR32 a + 3w = ADDR32 b + 3w) = (a = b))``, 173 SRW_TAC [] [WORD_EQ_ADD_RCANCEL, 174 simpLib.SIMP_PROVE (std_ss++WORD_BIT_EQ_ss) [ADDR32_def] 175 ``(ADDR32 a = ADDR32 b) = (a = b)``]); 176 177val ADDR32_EQ_0 = store_thm("ADDR32_EQ_0", 178 ``!a. (ADDR32 a = 0w) = (a = 0w)``, 179 REWRITE_TAC [SIMP_RULE std_ss [ADDR32_n2w] (Q.SPECL [`a`,`0w`] ADDR32_11)]); 180 181val lem = Q.prove( 182 `(!a. ADDR32 a && 1w = 0w) /\ 183 (!a. ADDR32 a && 2w = 0w) /\ 184 (!a. ADDR32 a && 3w = 0w)`, 185 SRW_TAC [WORD_BIT_EQ_ss] [ADDR32_def]); 186 187val ADDR32_NEQ_ADDR32 = store_thm("ADDR32_NEQ_ADDR32", 188 ``!a b. ~(ADDR32 a + 0w = ADDR32 b + 1w) /\ 189 ~(ADDR32 a + 0w = ADDR32 b + 2w) /\ 190 ~(ADDR32 a + 0w = ADDR32 b + 3w) /\ 191 ~(ADDR32 a + 1w = ADDR32 b + 2w) /\ 192 ~(ADDR32 a + 1w = ADDR32 b + 3w) /\ 193 ~(ADDR32 a + 2w = ADDR32 b + 3w) /\ 194 ~(ADDR32 a + 1w = ADDR32 b + 0w) /\ 195 ~(ADDR32 a + 2w = ADDR32 b + 0w) /\ 196 ~(ADDR32 a + 3w = ADDR32 b + 0w) /\ 197 ~(ADDR32 a + 2w = ADDR32 b + 1w) /\ 198 ~(ADDR32 a + 3w = ADDR32 b + 1w) /\ 199 ~(ADDR32 a + 3w = ADDR32 b + 2w) /\ 200 ~(ADDR32 a + 1w = ADDR32 b) /\ 201 ~(ADDR32 a + 2w = ADDR32 b) /\ 202 ~(ADDR32 a + 3w = ADDR32 b) /\ 203 ~(ADDR32 a = ADDR32 b + 1w) /\ 204 ~(ADDR32 a = ADDR32 b + 2w) /\ 205 ~(ADDR32 a = ADDR32 b + 3w)``, 206 SRW_TAC [] [lem, WORD_ADD_OR] \\ SRW_TAC [WORD_BIT_EQ_ss] [ADDR32_def]); 207 208val EXISTS_ADDR32 = store_thm("EXISTS_ADDR32", 209 ``!p. ?a. (p = ADDR32 a + 0w) \/ (p = ADDR32 a + 1w) \/ 210 (p = ADDR32 a + 2w) \/ (p = ADDR32 a + 3w)``, 211 STRIP_TAC \\ Q.EXISTS_TAC `(31 >< 2) p` 212 \\ SRW_TAC [] [lem, WORD_ADD_OR] 213 \\ SRW_TAC [WORD_BIT_EQ_ss] [ADDR32_def] 214 \\ DECIDE_TAC); 215 216val ADDR32_ABSORB_CONST = store_thm("ADDR32_ABSORB_CONST", 217 ``(ADDR32 x + 0w = ADDR32 x) /\ 218 (ADDR32 x + 4w = ADDR32 (x + 1w)) /\ 219 (ADDR32 x + 8w = ADDR32 (x + 2w)) /\ 220 (ADDR32 x + 12w = ADDR32 (x + 3w)) /\ 221 (ADDR32 x + 16w = ADDR32 (x + 4w)) /\ 222 (ADDR32 x + 20w = ADDR32 (x + 5w)) /\ 223 (ADDR32 x + 24w = ADDR32 (x + 6w)) /\ 224 (ADDR32 x + 28w = ADDR32 (x + 7w)) /\ 225 (ADDR32 x + 32w = ADDR32 (x + 8w)) /\ 226 (ADDR32 x + 36w = ADDR32 (x + 9w)) /\ 227 (ADDR32 x + 40w = ADDR32 (x + 10w)) /\ 228 (ADDR32 x - 0w = ADDR32 (x - 0w)) /\ 229 (ADDR32 x - 4w = ADDR32 (x - 1w)) /\ 230 (ADDR32 x - 8w = ADDR32 (x - 2w)) /\ 231 (ADDR32 x - 12w = ADDR32 (x - 3w)) /\ 232 (ADDR32 x - 16w = ADDR32 (x - 4w)) /\ 233 (ADDR32 x - 20w = ADDR32 (x - 5w)) /\ 234 (ADDR32 x - 24w = ADDR32 (x - 6w)) /\ 235 (ADDR32 x - 28w = ADDR32 (x - 7w)) /\ 236 (ADDR32 x - 32w = ADDR32 (x - 8w)) /\ 237 (ADDR32 x - 36w = ADDR32 (x - 9w)) /\ 238 (ADDR32 x - 40w = ADDR32 (x - 10w))``, 239 SIMP_TAC std_ss [ADDR32_ADD,ADDR32_SUB,ADDR32_n2w,WORD_ADD_0]); 240 241val ADDRESS_ROTATE = store_thm("ADDRESS_ROTATE", 242 ``!q:word32 z:word30. q #>> (8 * w2n ((1 >< 0) (ADDR32 z):word2)) = q``, 243 SIMP_TAC std_ss [ADDR32_eq_0,word_0_n2w] \\ STRIP_TAC \\ EVAL_TAC); 244 245val ADDR30_THM = store_thm("ADDR30_THM", 246 ``!x. ADDR30 x = n2w (w2n x DIV 4)``, 247 Cases_word \\ ASM_SIMP_TAC bool_ss [w2n_n2w,LESS_MOD,ADDR30_n2w]); 248 249val ADDR32_THM = store_thm("ADDR32_THM", 250 ``!x. ADDR32 x = n2w (4 * w2n x)``, 251 Cases_word \\ ASM_SIMP_TAC bool_ss [w2n_n2w,LESS_MOD,ADDR32_n2w]); 252 253val ALIGNED_THM = store_thm("ALIGNED_THM", 254 ``!p. ALIGNED p = ?k. p = k * 4w``, 255 SRW_TAC [] [ALIGNED_def] \\ EQ_TAC \\ SRW_TAC [WORD_MUL_LSL_ss] [] 256 THENL [Q.EXISTS_TAC `(31 >< 2) p`, ALL_TAC] 257 \\ FULL_SIMP_TAC (std_ss++WORD_BIT_EQ_ss++wordsLib.BIT_ss) [n2w_def]); 258 259val ALIGNED_NEG_lemma = prove( 260 ``!x. ALIGNED x ==> ALIGNED (- x)``, 261 ASM_SIMP_TAC std_ss [ALIGNED_THM,w2n_n2w,LESS_MOD] 262 \\ REPEAT STRIP_TAC \\ Q.EXISTS_TAC `n2w (2**30) - k` 263 \\ ASM_SIMP_TAC (std_ss++WORD_ARITH_EQ_ss) [WORD_RIGHT_SUB_DISTRIB] 264 \\ ASM_SIMP_TAC (std_ss++WORD_ss) []); 265 266val ALIGNED_NEG = store_thm("ALIGNED_NEG", 267 ``!x. ALIGNED (- x) = ALIGNED x``, 268 METIS_TAC [ALIGNED_NEG_lemma,WORD_NEG_NEG]); 269 270val ALIGNED_and_1 = store_thm("ALIGNED_and_1", 271 ``!x. ALIGNED x ==> (x && 1w = 0w)``, 272 REWRITE_TAC [ALIGNED_THM] \\ NTAC 2 STRIP_TAC 273 \\ ASM_REWRITE_TAC [] \\ POP_ASSUM (fn th => ALL_TAC) 274 \\ Q.SPEC_TAC (`k`,`k`) \\ Cases 275 \\ REWRITE_TAC [word_mul_n2w,word_add_n2w,n2w_and_1,n2w_11] 276 \\ REWRITE_TAC [GSYM (EVAL ``2*2``),MULT_ASSOC] 277 \\ SIMP_TAC (std_ss++SIZES_ss) [MOD_EQ_0]); 278 279val ALIGNED_add_1_and_1 = store_thm("ALIGNED_add_1_and_1", 280 ``!x. ALIGNED x ==> ~(x + 1w && 1w = 0w)``, 281 REWRITE_TAC [ALIGNED_THM] \\ NTAC 2 STRIP_TAC 282 \\ ASM_REWRITE_TAC [] \\ POP_ASSUM (fn th => ALL_TAC) 283 \\ Q.SPEC_TAC (`k`,`k`) \\ Cases 284 \\ REWRITE_TAC [word_mul_n2w,word_add_n2w,n2w_and_1,n2w_11] 285 \\ REWRITE_TAC [GSYM (EVAL ``2*2``),MULT_ASSOC] 286 \\ SIMP_TAC (std_ss++SIZES_ss) [MOD_TIMES]); 287 288val tac = 289 REWRITE_TAC [ALIGNED_THM] \\ NTAC 2 STRIP_TAC 290 \\ ASM_REWRITE_TAC [] \\ POP_ASSUM (fn th => ALL_TAC) 291 \\ Q.SPEC_TAC (`k`,`k`) \\ Cases 292 \\ REWRITE_TAC [word_mul_n2w,word_add_n2w,n2w_and_3,n2w_11] 293 \\ SIMP_TAC (std_ss++SIZES_ss) [MOD_TIMES]; 294 295val ALIGNED_add_1_and_3 = store_thm("ALIGNED_add_1_and_3", 296 ``!x. ALIGNED x ==> (x + 1w && 3w = 1w)``,tac); 297val ALIGNED_add_2_and_3 = store_thm("ALIGNED_add_2_and_3", 298 ``!x. ALIGNED x ==> (x + 2w && 3w = 2w)``,tac); 299val ALIGNED_add_3_and_3 = store_thm("ALIGNED_add_3_and_3", 300 ``!x. ALIGNED x ==> (x + 3w && 3w = 3w)``,tac); 301 302val ALIGNED_ADD = store_thm("ALIGNED_ADD", 303 ``!x y. ALIGNED x /\ ALIGNED y ==> ALIGNED (x + y)``, 304 REWRITE_TAC [ALIGNED_THM] \\ REPEAT STRIP_TAC 305 \\ ASM_REWRITE_TAC [GSYM WORD_RIGHT_ADD_DISTRIB] \\ METIS_TAC []); 306 307val ALIGNED_SUB = store_thm("ALIGNED_SUB", 308 ``!x y. ALIGNED x /\ ALIGNED y ==> ALIGNED (x - y)``, 309 SIMP_TAC std_ss [word_sub_def] \\ METIS_TAC [ALIGNED_ADD,ALIGNED_NEG]); 310 311 312val word_arith_lemma1 = store_thm("word_arith_lemma1", 313 ``!n m. (n2w n + n2w m = n2w (n + m):'a word) /\ 314 (x + n2w n + n2w m = x + n2w (n + m):'a word) /\ 315 (x - n2w n - n2w m = x - n2w (n + m):'a word)``, 316 REWRITE_TAC [GSYM WORD_SUB_PLUS,word_add_n2w,GSYM WORD_ADD_ASSOC]); 317 318val word_arith_lemma2 = store_thm("word_arith_lemma2", 319 ``!n m. n2w n - (n2w m) :'a word = 320 if n < m then (- (n2w (m-n))) else n2w (n-m)``, 321 REPEAT STRIP_TAC \\ Cases_on `n < m` \\ ASM_REWRITE_TAC [] 322 \\ FULL_SIMP_TAC bool_ss [NOT_LESS,LESS_EQ] 323 \\ FULL_SIMP_TAC bool_ss [LESS_EQ_EXISTS,ADD1,DECIDE ``n+1+p-n = 1+p:num``] 324 \\ REWRITE_TAC [GSYM word_add_n2w,WORD_SUB_PLUS,WORD_SUB_REFL] 325 \\ REWRITE_TAC [GSYM WORD_SUB_PLUS] 326 \\ REWRITE_TAC [word_sub_def,WORD_ADD_0,DECIDE ``m+p-m=p:num``] 327 \\ REWRITE_TAC [GSYM WORD_ADD_ASSOC] \\ ONCE_REWRITE_TAC [WORD_ADD_COMM] 328 \\ REWRITE_TAC [GSYM word_sub_def,WORD_SUB_ADD]); 329 330val word_arith_lemma3 = store_thm("word_arith_lemma3", 331 ``!x n m. x - n2w m + n2w n :'a word = if n < m then x - (n2w (m-n)) else x + n2w (n-m)``, 332 REWRITE_TAC [word_sub_def,GSYM WORD_ADD_ASSOC] 333 \\ REWRITE_TAC [GSYM (RW1 [WORD_ADD_COMM] word_sub_def),word_arith_lemma2] 334 \\ REPEAT STRIP_TAC \\ Cases_on `n<m` \\ ASM_REWRITE_TAC []); 335 336val word_arith_lemma4 = store_thm("word_arith_lemma4", 337 ``!x n m. x + n2w n - n2w m :'a word = if n < m then x - (n2w (m-n)) else x + n2w (n-m)``, 338 REWRITE_TAC [word_sub_def,GSYM WORD_ADD_ASSOC] 339 \\ REWRITE_TAC [GSYM word_sub_def,word_arith_lemma2] 340 \\ REPEAT STRIP_TAC \\ Cases_on `n<m` \\ ASM_REWRITE_TAC [word_sub_def]); 341 342val word_arith_lemma5 = store_thm("word_arith_lemma5", 343 ``!x y m n. (x + n2w n = y + n2w m) = 344 if n < m then (x = y + n2w m - n2w n) else (x + n2w n - n2w m = y)``, 345 ONCE_REWRITE_TAC [GSYM WORD_EQ_SUB_ZERO] 346 \\ SIMP_TAC std_ss [WORD_SUB_PLUS,WORD_SUB_SUB] 347 \\ METIS_TAC [WORD_SUB_PLUS,WORD_ADD_COMM]); 348 349val ADDR32_ADD_EQ_ZERO_LEMMA = prove( 350 ``!x m. 0 < m /\ w2n x + m < dimword (:'a) ==> ~((x:'a word) + n2w m = 0w)``, 351 Cases_word 352 \\ ASM_SIMP_TAC bool_ss [w2n_n2w,LESS_MOD,word_add_n2w,n2w_11,ZERO_LT_dimword] 353 \\ DECIDE_TAC); 354 355val ADDR32_ADD_EQ_ZERO = store_thm("ADDR32_ADD_EQ_ZERO", 356 ``!x. ~(ADDR32 x + 1w = 0w) /\ ~(ADDR32 x + 2w = 0w) /\ ~(ADDR32 x + 3w = 0w)``, 357 Cases_word \\ REWRITE_TAC [ADDR32_n2w] \\ REPEAT STRIP_TAC \\ POP_ASSUM MP_TAC 358 \\ REWRITE_TAC [] \\ MATCH_MP_TAC ADDR32_ADD_EQ_ZERO_LEMMA 359 \\ `4 * n < 4 * dimword (:30)` by DECIDE_TAC 360 \\ FULL_SIMP_TAC (bool_ss++SIZES_ss) [w2n_n2w,LESS_MOD,EVAL ``4 * 1073741824``] 361 \\ DECIDE_TAC); 362 363val word_add_and_3w = store_thm("word_add_and_3w", 364 ``!w. (w + n2w n) && 3w = (w + n2w (n MOD 4)) && 3w``, 365 Cases_word \\ SIMP_TAC std_ss [n2w_and_3,word_add_n2w] 366 \\ `n = n DIV 4 * 4 + n MOD 4` by METIS_TAC [DIVISION,EVAL ``0<4``] 367 \\ ONCE_ASM_REWRITE_TAC [] 368 \\ ONCE_REWRITE_TAC [DECIDE ``m + (k + l) = k + (m + l:num)``] 369 \\ SIMP_TAC std_ss [MOD_TIMES]); 370 371val ALIGNED_CLAUSES = store_thm("ALIGNED_CLAUSES", 372 ``!x a. (ALIGNED (a + 4w * x) = ALIGNED a) /\ (ALIGNED (4w * x + a) = ALIGNED a) /\ 373 (ALIGNED (a + x * 4w) = ALIGNED a) /\ (ALIGNED (x * 4w + a) = ALIGNED a) /\ 374 (ALIGNED (a + 4w) = ALIGNED a) /\ (ALIGNED (4w + a) = ALIGNED a)``, 375 Cases_word \\ SIMP_TAC std_ss [ALIGNED_def,word_mul_n2w] 376 \\ ONCE_REWRITE_TAC [word_add_and_3w] \\ ONCE_REWRITE_TAC [WORD_ADD_COMM] 377 \\ ONCE_REWRITE_TAC [word_add_and_3w] 378 \\ SIMP_TAC std_ss [MOD_EQ_0,RW1 [MULT_COMM] MOD_EQ_0,WORD_ADD_0]); 379 380val NOT_ALIGNED = store_thm("NOT_ALIGNED", 381 ``!a. ALIGNED a ==> ~(ALIGNED (a + 1w)) /\ ~(ALIGNED (a + 2w)) /\ ~(ALIGNED (a + 3w))``, 382 Cases_word \\ SIMP_TAC std_ss [ALIGNED_n2w,word_add_n2w] 383 \\ ONCE_REWRITE_TAC [MATCH_MP (GSYM MOD_PLUS) (DECIDE ``0<4``)] 384 \\ STRIP_TAC \\ ASM_REWRITE_TAC [ADD] \\ EVAL_TAC); 385 386val word32_add_n2w = store_thm("word32_add_n2w", 387 ``!x n. x + (n2w n):word32 = 388 if n < 2**31 then x + n2w n else x - n2w (2**32 - n MOD 2**32)``, 389 Cases_word \\ STRIP_TAC 390 \\ SIMP_TAC (std_ss++wordsLib.SIZES_ss) [word_sub_def,word_2comp_n2w] 391 \\ Cases_on `n' < 2147483648` \\ ASM_REWRITE_TAC [] 392 \\ `n' MOD 4294967296 < 4294967296` by METIS_TAC [arithmeticTheory.DIVISION,EVAL ``0 < 4294967296``] 393 \\ Cases_on `n' MOD 4294967296 = 0` THENL [ 394 ASM_SIMP_TAC (std_ss++wordsLib.SIZES_ss) [] 395 \\ ONCE_REWRITE_TAC [GSYM n2w_mod] 396 \\ ASM_SIMP_TAC (std_ss++wordsLib.SIZES_ss) [], 397 `(4294967296 - n' MOD 4294967296) < 4294967296` by DECIDE_TAC 398 \\ ASM_SIMP_TAC std_ss [] 399 \\ `4294967296 - (4294967296 - n' MOD 4294967296) = n' MOD 4294967296` by DECIDE_TAC 400 \\ ONCE_REWRITE_TAC [GSYM n2w_mod] 401 \\ ASM_SIMP_TAC (std_ss++wordsLib.SIZES_ss) []]); 402 403val two64 = (snd o dest_eq o concl o EVAL) ``(2**64):num`` 404val two63 = (snd o dest_eq o concl o EVAL) ``(2**63):num`` 405val word64_add_n2w = store_thm("word64_add_n2w", 406 ``!x n. x + (n2w n):word64 = 407 if n < 2**63 then x + n2w n else x - n2w (2**64 - n MOD 2**64)``, 408 Cases_word \\ STRIP_TAC 409 \\ SIMP_TAC (std_ss++wordsLib.SIZES_ss) [word_sub_def,word_2comp_n2w] 410 \\ Cases_on `n' < ^two63` \\ ASM_REWRITE_TAC [] 411 \\ `n' MOD ^two64 < ^two64` by METIS_TAC [arithmeticTheory.DIVISION,EVAL ``0 < ^two64``] 412 \\ Cases_on `n' MOD ^two64 = 0` THENL [ 413 ASM_SIMP_TAC (std_ss++wordsLib.SIZES_ss) [] 414 \\ ONCE_REWRITE_TAC [GSYM n2w_mod] 415 \\ ASM_SIMP_TAC (std_ss++wordsLib.SIZES_ss) [], 416 `(^two64 - n' MOD ^two64) < ^two64` by DECIDE_TAC 417 \\ ASM_SIMP_TAC std_ss [] 418 \\ `^two64 - (^two64 - n' MOD ^two64) = n' MOD ^two64` by DECIDE_TAC 419 \\ ONCE_REWRITE_TAC [GSYM n2w_mod] 420 \\ ASM_SIMP_TAC (std_ss++wordsLib.SIZES_ss) []]); 421 422val MOD_EQ_0_IMP = prove( 423 ``!n m. 0 < m ==> ((n MOD m = 0) = ?k. n = k * m)``, 424 METIS_TAC [DIVISION,ADD_0,MOD_EQ_0]); 425 426val ALIGNED_BITS = store_thm("ALIGNED_BITS", 427 ``!x. ALIGNED x = ~(x ' 0) /\ ~(x ' 1)``, 428 Cases_word \\ ONCE_REWRITE_TAC [word_index_n2w] 429 \\ Cases_on `n MOD 4 = 0` \\ ASM_SIMP_TAC std_ss [] 430 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [ALIGNED_n2w,bitTheory.BIT_def] THENL [ 431 ASM_SIMP_TAC std_ss [bitTheory.BITS_THM2] 432 \\ `0 < 4` by EVAL_TAC 433 \\ IMP_RES_TAC MOD_EQ_0_IMP 434 \\ ASM_SIMP_TAC std_ss [] 435 \\ REWRITE_TAC [GSYM (EVAL ``2*2``),MULT_ASSOC] 436 \\ SIMP_TAC std_ss [MOD_EQ_0], 437 ASM_SIMP_TAC std_ss [bitTheory.BITS_THM,GSYM bitTheory.NOT_MOD2_LEM] 438 \\ Cases_on `n MOD 2 = 0` \\ ASM_SIMP_TAC std_ss [] 439 \\ `0 < 2` by EVAL_TAC \\ `?k. n = k * 2` by METIS_TAC [MOD_EQ_0_IMP] 440 \\ FULL_SIMP_TAC std_ss [MOD_EQ_0_IMP,MULT_DIV] 441 \\ FULL_SIMP_TAC bool_ss [GSYM (EVAL ``2*2``),MULT_ASSOC] 442 \\ FULL_SIMP_TAC bool_ss [GSYM (EVAL ``SUC 1``),MULT_SUC_EQ]]); 443 444val ALIGNED_OR = store_thm("ALIGNED_OR", 445 ``!x y. ALIGNED (x || y) = ALIGNED x /\ ALIGNED y``, 446 SIMP_TAC (std_ss++SIZES_ss) [ALIGNED_BITS,word_or_def,fcpTheory.FCP_BETA] 447 \\ METIS_TAC []); 448 449val ADDR32_LESS_EQ = store_thm("ADDR32_LESS_EQ", 450 ``!x y. ADDR32 x <=+ ADDR32 y = x <=+ y``, 451 Cases_word \\ Cases_word 452 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [ADDR32_n2w,WORD_LS,w2n_n2w] 453 \\ `4 * n' < 4294967296 /\ 4 * n < 4294967296` by DECIDE_TAC 454 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [ADDR32_n2w,WORD_LS,w2n_n2w]); 455 456val ADDR32_LESS = store_thm("ADDR32_LESS", 457 ``!x y. ADDR32 x <+ ADDR32 y = x <+ y``, 458 Cases_word \\ Cases_word 459 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [ADDR32_n2w,WORD_LO,w2n_n2w] 460 \\ `4 * n' < 4294967296 /\ 4 * n < 4294967296` by DECIDE_TAC 461 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [ADDR32_n2w,WORD_LS,w2n_n2w]); 462 463val ALIGNED_LESS_ADD = store_thm("ALIGNED_LESS_ADD", 464 ``!x. ALIGNED x /\ ~(x + 4w = 0w) ==> x <+ x + 4w``, 465 REPEAT STRIP_TAC 466 \\ IMP_RES_TAC (RW [GSYM ALIGNED_def] EXISTS_ADDR30) 467 \\ FULL_SIMP_TAC std_ss [GSYM ADDR32_SUC, 468 ADDR32_LESS,GSYM (EVAL ``ADDR32 0w``),ADDR32_11] 469 \\ Q.PAT_X_ASSUM `~(y + 1w = 0w)` MP_TAC 470 \\ REPEAT (POP_ASSUM (K ALL_TAC)) 471 \\ Q.SPEC_TAC (`y`,`y`) \\ Cases_word 472 \\ ASM_SIMP_TAC std_ss [word_add_n2w,n2w_11,ZERO_LT_dimword,WORD_LO,w2n_n2w] 473 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [MOD_EQ_0_IMP] 474 \\ REPEAT STRIP_TAC 475 \\ `~(n + 1 = 1 * 1073741824)` by METIS_TAC [] 476 \\ FULL_SIMP_TAC std_ss [] 477 \\ `n + 1 < 1073741824` by DECIDE_TAC 478 \\ ASM_SIMP_TAC std_ss [] \\ DECIDE_TAC); 479 480val CONTAINER_IF_T = store_thm("CONTAINER_IF_T", 481 ``!x y z. CONTAINER x ==> ((if x then y else z) = y:'a)``, 482 SIMP_TAC std_ss [CONTAINER_def]); 483 484val CONTAINER_IF_F = store_thm("CONTAINER_IF_F", 485 ``!x y z. CONTAINER ~x ==> ((if x then y else z) = z:'a)``, 486 SIMP_TAC std_ss [CONTAINER_def]); 487 488val ALIGNED_ADD_EQ_LEMMA = prove( 489 ``!x y. ALIGNED x ==> (ALIGNED (x + y) = ALIGNED y)``, 490 Cases_word \\ Cases_word 491 \\ SIMP_TAC std_ss [word_add_n2w,ALIGNED_n2w] 492 \\ ONCE_REWRITE_TAC [MATCH_MP (GSYM MOD_PLUS) (DECIDE ``0<4``)] 493 \\ ASM_SIMP_TAC bool_ss [ADD] \\ SIMP_TAC std_ss [MOD_MOD]); 494 495val ALIGNED_ADD_EQ = store_thm("ALIGNED_ADD_EQ", 496 ``!x y. ALIGNED x ==> (ALIGNED (x + y) = ALIGNED y) /\ 497 (ALIGNED (x - y) = ALIGNED y) /\ 498 (ALIGNED (y + x) = ALIGNED y) /\ 499 (ALIGNED (y - x) = ALIGNED y)``, 500 REWRITE_TAC [word_sub_def] 501 \\ SIMP_TAC std_ss [ALIGNED_ADD_EQ_LEMMA,ALIGNED_NEG] 502 \\ ONCE_REWRITE_TAC [WORD_ADD_COMM] 503 \\ SIMP_TAC std_ss [ALIGNED_ADD_EQ_LEMMA,ALIGNED_NEG]); 504 505val ALIGNED_MOD_4 = store_thm("ALIGNED_MOD_4", 506 ``!a n. (ALIGNED (a + n2w n) = ALIGNED (a + n2w (n MOD 4))) /\ 507 (ALIGNED (a - n2w n) = ALIGNED (a - n2w (n MOD 4)))``, 508 NTAC 2 STRIP_TAC 509 \\ STRIP_ASSUME_TAC (Q.SPEC `n` (MATCH_MP DA (DECIDE ``0 < 4``))) 510 \\ ASM_SIMP_TAC std_ss [MOD_MULT] 511 \\ ONCE_REWRITE_TAC [ADD_COMM] \\ ONCE_REWRITE_TAC [MULT_COMM] 512 \\ SIMP_TAC std_ss [GSYM word_add_n2w,WORD_SUB_PLUS,GSYM word_mul_n2w, 513 WORD_ADD_ASSOC,ALIGNED_CLAUSES] 514 \\ REWRITE_TAC [word_sub_def] 515 \\ ONCE_REWRITE_TAC [RW1[WORD_MULT_COMM]WORD_NEG_MUL] 516 \\ REWRITE_TAC [GSYM WORD_MULT_ASSOC,ALIGNED_CLAUSES]); 517 518val ALIGNED_0 = store_thm("ALIGNED_0", 519 ``!a. (ALIGNED (a + 0w) = ALIGNED a) /\ (ALIGNED (a - 0w) = ALIGNED a)``, 520 SIMP_TAC std_ss [WORD_ADD_0,WORD_SUB_RZERO]); 521 522val ALIGNED_SUB_4 = store_thm("ALIGNED_SUB_4", 523 ``!a. ALIGNED (a - 4w) = ALIGNED a``, 524 ONCE_REWRITE_TAC [ALIGNED_MOD_4] \\ SIMP_TAC std_ss [WORD_SUB_RZERO]); 525 526val ALIGNED_INTRO = store_thm("ALIGNED_INTRO", 527 ``!a. ((a && 3w = 0w) = ALIGNED a) /\ ((3w && a = 0w) = ALIGNED a) /\ 528 ((0w = a && 3w) = ALIGNED a) /\ ((0w = 3w && a) = ALIGNED a) /\ 529 ((w2n a MOD 4 = 0) = ALIGNED a) /\ ((0 = w2n a MOD 4) = ALIGNED a)``, 530 Cases_word \\ ASM_SIMP_TAC std_ss [w2n_n2w,GSYM ALIGNED_n2w] 531 \\ REWRITE_TAC [ALIGNED_def] \\ METIS_TAC [WORD_AND_COMM]); 532 533val BIT_LEMMA = prove( 534 ``!x. (NUMERAL (BIT2 (BIT1 x)) = 4 * (x + 1)) /\ 535 (NUMERAL (BIT2 (BIT2 x)) = 4 * (x + 1) + 2) /\ 536 (NUMERAL (BIT1 (BIT2 x)) = 4 * (x + 1) + 1) /\ 537 (NUMERAL (BIT1 (BIT1 x)) = 4 * x + 3)``, 538 REPEAT STRIP_TAC 539 \\ ONCE_REWRITE_TAC [EQ_SYM_EQ] 540 \\ CONV_TAC (RAND_CONV (ONCE_REWRITE_CONV [NUMERAL_DEF])) 541 \\ NTAC 2 (CONV_TAC (RAND_CONV (ONCE_REWRITE_CONV [BIT1,BIT2]))) 542 \\ DECIDE_TAC); 543 544val ALIGNED_SUB_CLAUSES = prove( 545 ``ALIGNED (a - 4w * x) = ALIGNED a``, 546 ONCE_REWRITE_TAC [GSYM ALIGNED_NEG] 547 \\ SIMP_TAC std_ss [WORD_NEG_SUB, word_sub_def, ALIGNED_CLAUSES]); 548 549val ALIGNED = store_thm("ALIGNED", 550 ``!a x. 551 (ALIGNED 0w = T) /\ 552 (ALIGNED (n2w (NUMERAL (BIT2 (BIT1 x)))) = T) /\ 553 (ALIGNED (n2w (NUMERAL (BIT1 (BIT2 x)))) = F) /\ 554 (ALIGNED (n2w (NUMERAL (BIT2 (BIT2 x)))) = F) /\ 555 (ALIGNED (n2w (NUMERAL (BIT1 (BIT1 (BIT1 x))))) = F) /\ 556 (ALIGNED (n2w (NUMERAL (BIT1 (BIT1 (BIT2 x))))) = F) /\ 557 (ALIGNED (a + 0w) = ALIGNED a) /\ 558 (ALIGNED (a + n2w (NUMERAL (BIT2 (BIT1 x)))) = ALIGNED a) /\ 559 (ALIGNED (a + n2w (NUMERAL (BIT1 (BIT2 x)))) = ALIGNED (a + 1w)) /\ 560 (ALIGNED (a + n2w (NUMERAL (BIT2 (BIT2 x)))) = ALIGNED (a + 2w)) /\ 561 (ALIGNED (a + n2w (NUMERAL (BIT1 (BIT1 (BIT1 x))))) = ALIGNED (a + 3w)) /\ 562 (ALIGNED (a + n2w (NUMERAL (BIT1 (BIT1 (BIT2 x))))) = ALIGNED (a + 3w)) /\ 563 (ALIGNED (a - 0w) = ALIGNED a) /\ 564 (ALIGNED (a - n2w (NUMERAL (BIT2 (BIT1 x)))) = ALIGNED a) /\ 565 (ALIGNED (a - n2w (NUMERAL (BIT1 (BIT2 x)))) = ALIGNED (a - 1w)) /\ 566 (ALIGNED (a - n2w (NUMERAL (BIT2 (BIT2 x)))) = ALIGNED (a - 2w)) /\ 567 (ALIGNED (a - n2w (NUMERAL (BIT1 (BIT1 (BIT1 x))))) = ALIGNED (a - 3w)) /\ 568 (ALIGNED (a - n2w (NUMERAL (BIT1 (BIT1 (BIT2 x))))) = ALIGNED (a - 3w))``, 569 PURE_ONCE_REWRITE_TAC [BIT_LEMMA] \\ ONCE_REWRITE_TAC [ADD_COMM] 570 \\ SIMP_TAC std_ss [GSYM word_add_n2w,WORD_ADD_ASSOC,WORD_SUB_PLUS, 571 ALIGNED_CLAUSES,ALIGNED_SUB_CLAUSES,GSYM word_mul_n2w,ALIGNED_0] 572 \\ SIMP_TAC std_ss [ALIGNED_n2w, 573 RW [WORD_ADD_0] (Q.SPECL [`x`,`0w`] ALIGNED_CLAUSES)]); 574 575val WORD_CMP_NORMALISE = save_thm("WORD_CMP_NORMALISE",let 576 val rw = METIS_PROVE [] ``!x:'a y z:'b q. ~(x = y) /\ ~(z = q) = ~(x = y) /\ ~(q = z)`` 577 val nzcv_thm = RW1 [rw] nzcv_def 578 val rw = [nzcv_thm,LET_DEF,GSYM word_add_n2w,n2w_w2n,GSYM word_sub_def,WORD_EQ_SUB_ZERO] 579 val th = SIMP_RULE std_ss (WORD_GREATER_EQ::rw) word_ge_def 580 val th = prove( 581 ``((word_msb (a - b) = ~(word_msb a = word_msb b) /\ ~(word_msb a = word_msb (a - b))) = b <= a) /\ 582 ((word_msb (a - b) = ~(word_msb b = word_msb a) /\ ~(word_msb a = word_msb (a - b))) = b <= a) /\ 583 ((word_msb (a - b) = ~(word_msb a = word_msb b) /\ ~(word_msb (a - b) = word_msb a)) = b <= a) /\ 584 ((word_msb (a - b) = ~(word_msb b = word_msb a) /\ ~(word_msb (a - b) = word_msb a)) = b <= a) /\ 585 ((word_msb (a - b) = ~(word_msb a = word_msb (a - b)) /\ ~(word_msb a = word_msb b)) = b <= a) /\ 586 ((word_msb (a - b) = ~(word_msb a = word_msb (a - b)) /\ ~(word_msb b = word_msb a)) = b <= a) /\ 587 ((word_msb (a - b) = ~(word_msb (a - b) = word_msb a) /\ ~(word_msb a = word_msb b)) = b <= a) /\ 588 ((word_msb (a - b) = ~(word_msb (a - b) = word_msb a) /\ ~(word_msb b = word_msb a)) = b <= a) /\ 589 ((~(word_msb a = word_msb b) /\ ~(word_msb a = word_msb (a - b)) = word_msb (a - b)) = b <= a) /\ 590 ((~(word_msb b = word_msb a) /\ ~(word_msb a = word_msb (a - b)) = word_msb (a - b)) = b <= a) /\ 591 ((~(word_msb a = word_msb b) /\ ~(word_msb (a - b) = word_msb a) = word_msb (a - b)) = b <= a) /\ 592 ((~(word_msb b = word_msb a) /\ ~(word_msb (a - b) = word_msb a) = word_msb (a - b)) = b <= a) /\ 593 ((~(word_msb a = word_msb (a - b)) /\ ~(word_msb a = word_msb b) = word_msb (a - b)) = b <= a) /\ 594 ((~(word_msb a = word_msb (a - b)) /\ ~(word_msb b = word_msb a) = word_msb (a - b)) = b <= a) /\ 595 ((~(word_msb (a - b) = word_msb a) /\ ~(word_msb a = word_msb b) = word_msb (a - b)) = b <= a) /\ 596 ((~(word_msb (a - b) = word_msb a) /\ ~(word_msb b = word_msb a) = word_msb (a - b)) = b <= a:('a word))``, 597 REWRITE_TAC [th] THEN METIS_TAC []) 598 val lemma1 = prove(``!a:'a word b. (b <=+ a) /\ ~(a = b) = b <+ a``, 599 REWRITE_TAC [WORD_LOWER_OR_EQ] THEN METIS_TAC [WORD_LOWER_NOT_EQ]) 600 val lemma2 = prove(``!a:'a word b. ~(a = b) /\ (b <=+ a) = b <+ a``, 601 REWRITE_TAC [WORD_LOWER_OR_EQ] THEN METIS_TAC [WORD_LOWER_NOT_EQ]) 602 val lemma3 = prove(``!a:'a word b. (b <= a) /\ ~(a = b) = b < a``, 603 REWRITE_TAC [WORD_LESS_OR_EQ] THEN METIS_TAC [WORD_LESS_NOT_EQ]) 604 val lemma4 = prove(``!a:'a word b. ~(a = b) /\ (b <= a) = b < a``, 605 REWRITE_TAC [WORD_LESS_OR_EQ] THEN METIS_TAC [WORD_LESS_NOT_EQ]) 606 val ys = [WORD_GREATER_EQ,WORD_GREATER,WORD_NOT_LOWER_EQUAL] 607 val zs = [WORD_NOT_LOWER,GSYM WORD_LOWER_OR_EQ,WORD_NOT_LESS,WORD_NOT_LESS_EQUAL] 608 val qs1 = [GSYM WORD_LESS_OR_EQ, GSYM (RW1 [DISJ_COMM] WORD_LESS_OR_EQ)] 609 val qs2 = [GSYM WORD_LOWER_OR_EQ, GSYM (RW1 [DISJ_COMM] WORD_LOWER_OR_EQ)] 610 val ls = [lemma1,lemma2,lemma3,lemma4,WORD_EQ_SUB_ZERO,WORD_SUB_RZERO] 611 in Q.GEN `a` (Q.GEN `b` (LIST_CONJ (map SPEC_ALL ([th] @ ys @ zs @ qs1 @ qs2 @ ls)))) end) 612 613val word_LSL_n2w = store_thm("word_LSL_n2w", 614 ``!m k. ((n2w m):'a word) << k = n2w (m * 2 ** k)``, 615 SIMP_TAC std_ss [AC MULT_ASSOC MULT_COMM,WORD_MUL_LSL,word_mul_n2w]); 616 617val WORD_EQ_ADD_CANCEL = store_thm("WORD_EQ_ADD_CANCEL", 618 ``!v w x. ((v + w = x + w) = (v = x)) /\ ((w + v = x + w) = (v = x)) /\ 619 ((v + w = w + x) = (v = x)) /\ ((w + v = w + x) = (v = x)) /\ 620 ((w = x + w) = (x = 0w)) /\ ((v + w = w) = (v = 0w)) /\ 621 ((w = w + x) = (x = 0w)) /\ ((w + v = w) = (v = 0w: 'a word))``, 622 METIS_TAC [WORD_ADD_0,WORD_ADD_COMM,WORD_EQ_ADD_LCANCEL]); 623 624val NOT_IF = store_thm("NOT_IF", 625 ``!b x y:'a. (if ~b then x else y) = if b then y else x``, 626 Cases THEN REWRITE_TAC []); 627 628val IF_IF = store_thm("IF_IF", 629 ``!b c x y:'a. 630 ((if b then (if c then x else y) else y) = if b /\ c then x else y) /\ 631 ((if b then (if c then y else x) else y) = if b /\ ~c then x else y) /\ 632 ((if b then x else (if c then x else y)) = if b \/ c then x else y) /\ 633 ((if b then x else (if c then y else x)) = if b \/ ~c then x else y)``, 634 Cases THEN Cases THEN REWRITE_TAC []); 635 636val SING_SET_INTRO = store_thm("SING_SET_INTRO", 637 ``!x:'a s. x INSERT s = SING_SET x UNION s``, 638 REWRITE_TAC [INSERT_UNION_EQ,UNION_EMPTY,SING_SET_def]); 639 640val UNION_CANCEL = store_thm("UNION_CANCEL", 641 ``!x s:'a set. x UNION (x UNION s) = x UNION s``, 642 REWRITE_TAC [UNION_ASSOC,UNION_IDEMPOT]); 643 644val FLATTEN_IF = store_thm("FLATTEN_IF", 645 ``!b x y. (if b then x else y) = (b /\ x) \/ (~b /\ y)``, 646 Cases THEN REWRITE_TAC []); 647 648val PUSH_IF_LEMMA = store_thm("PUSH_IF_LEMMA", 649 ``!b g x y. (b /\ (if g then x else y) = if g then b /\ x else b /\ y) /\ 650 ((if g then x else y) /\ b = if g then b /\ x else b /\ y)``, 651 REPEAT Cases THEN REWRITE_TAC []); 652 653val GUARD_EQ_ZERO = store_thm("GUARD_EQ_ZERO", 654 ``!n b. GUARD n b = GUARD 0 b``, 655 REWRITE_TAC [GUARD_def]); 656 657val extract_byte = store_thm("extract_byte", 658 ``!w. (7 >< 0) w = (w2w:word32->word8) w``, 659 Cases_word 660 \\ SIMP_TAC (std_ss++SIZES_ss) [wordsTheory.word_extract_n2w, 661 wordsTheory.w2w_def,bitTheory.BITS_THM, 662 wordsTheory.w2n_n2w,wordsTheory.n2w_11] 663 \\ REWRITE_TAC [GSYM (EVAL ``256 * 16777216``)] 664 \\ SIMP_TAC bool_ss [arithmeticTheory.MOD_MULT_MOD,EVAL ``0 < 256``, 665 EVAL ``0 < 16777216``]); 666 667val WORD_TIMES2 = store_thm("WORD_TIMES2", 668 ``!w:'a word. 2w * w = w + w``, 669 Cases_word 670 THEN REWRITE_TAC [word_add_n2w,word_mul_n2w,arithmeticTheory.TIMES2]); 671 672val WORD_SUB_INTRO = store_thm("WORD_SUB_INTRO", 673 ``!x y:'a word. 674 ((- y) + x = x - y) /\ 675 (x + (- y) = x - y) /\ 676 ((-1w) * y + x = x - y) /\ 677 (y * (-1w) + x = x - y) /\ 678 (x + (-1w) * y = x - y) /\ 679 (x + y * (-1w) = x - y)``, 680 SIMP_TAC (std_ss++wordsLib.WORD_ss) []); 681 682val WORD_ADD_LEMMA = prove( 683 ``!(x:'a word) n. x + n2w n * x = n2w (n + 1) * x``, 684 Cases_word 685 \\ REWRITE_TAC [word_mul_n2w,word_add_n2w,RIGHT_ADD_DISTRIB,MULT_CLAUSES] 686 \\ SIMP_TAC std_ss [AC ADD_ASSOC ADD_COMM]); 687 688val WORD_ADD_FOLD = store_thm("WORD_ADD_FOLD", 689 ``!(x:'a word) n p. 690 (x + n2w n * x = n2w (n + 1) * x) /\ 691 (x + x * n2w n = n2w (n + 1) * x) /\ 692 (n2w n * x + x = n2w (n + 1) * x) /\ 693 (n2w n * x + x = n2w (n + 1) * x) /\ 694 (p + x + n2w n * x = p + n2w (n + 1) * x) /\ 695 (p + x + x * n2w n = p + n2w (n + 1) * x) /\ 696 (p + n2w n * x + x = p + n2w (n + 1) * x) /\ 697 (p + n2w n * x + x = p + n2w (n + 1) * x)``, 698 REWRITE_TAC [GSYM WORD_ADD_LEMMA] 699 \\ SIMP_TAC std_ss [AC WORD_ADD_ASSOC WORD_ADD_COMM, 700 AC WORD_MULT_ASSOC WORD_MULT_COMM]); 701 702val EXISTS_EQ_LEMMA = store_thm("EXISTS_EQ_LEMMA", 703 ``!v P. (!i. ~(i = v) ==> ~(P i)) ==> ((?i. P i) = P v)``, 704 METIS_TAC []); 705 706val w2w_eq_n2w = store_thm("w2w_eq_n2w", 707 ``!w:word8. (!m. m < 256 ==> ((w2w w = (n2w m):word32) = (w = n2w m))) /\ 708 (w2w ((w2w w):word32) = w)``, 709 Cases_word 710 THEN FULL_SIMP_TAC (std_ss++wordsLib.SIZES_ss) [w2w_def,w2n_n2w,n2w_11] 711 THEN REPEAT STRIP_TAC 712 THEN IMP_RES_TAC (DECIDE ``k < 256 ==> k < 4294967296``) 713 THEN FULL_SIMP_TAC std_ss []); 714 715val w2w_CLAUSES = store_thm("w2w_CLAUSES", 716 ``!b1 b2 h1 h2. 717 ((w2w b1 = (w2w b2):word32) = (b1 = b2:word8)) /\ 718 ((w2w h1 = (w2w h2):word32) = (h1 = h2:word16)) /\ 719 (w2w ((w2w b1):word32) = b1) /\ (w2w ((w2w h1):word32) = h1)``, 720 REPEAT Cases_word 721 \\ FULL_SIMP_TAC (std_ss++wordsLib.SIZES_ss) [w2w_def,n2w_w2n,w2n_n2w,n2w_11] 722 \\ IMP_RES_TAC (DECIDE ``n < 256 ==> n < 4294967296:num``) 723 \\ IMP_RES_TAC (DECIDE ``n < 65536 ==> n < 4294967296:num``) 724 \\ FULL_SIMP_TAC (std_ss++wordsLib.SIZES_ss) [w2w_def,n2w_w2n,w2n_n2w,n2w_11]); 725 726val LESS_SUB_MOD = store_thm("LESS_SUB_MOD", 727 ``!n m k. n < k ==> ((n - m) MOD k = n - m)``, 728 REPEAT STRIP_TAC THEN `n - m < k` by DECIDE_TAC THEN ASM_SIMP_TAC std_ss []); 729 730val _ = export_theory(); 731