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