1open HolKernel Parse boolLib bossLib; 2open integerTheory arithmeticTheory bitTheory intLib listTheory; 3 4infix \\ 5val op \\ = op THEN; 6 7val _ = new_theory "int_bitwise"; 8 9val int_not_def = Define ` 10 int_not i = 0 - i - 1`; 11 12val int_not_not = store_thm("int_not_not", 13 ``!i. int_not (int_not i) = i``, 14 srw_tac [] [int_not_def] \\ fs [] \\ intLib.COOPER_TAC); 15 16val int_bit_def = Define ` 17 int_bit b (i:int) = 18 if i < 0 then ~(BIT b (Num (int_not i))) else BIT b (Num i)`; 19 20val int_bit_not = store_thm("int_bit_not", 21 ``!b i. int_bit b (int_not i) = ~(int_bit b i)``, 22 srw_tac [] [int_bit_def,int_not_not] 23 \\ fs [int_not_def] \\ `F` by intLib.COOPER_TAC); 24 25val bits_of_num_def = Define ` 26 bits_of_num (n:num) = 27 if n = 0 then [] 28 else ODD n :: bits_of_num (n DIV 2)`; 29 30val bits_of_int_def = Define ` 31 bits_of_int i = 32 if i < 0 then 33 (MAP (~) (bits_of_num (Num (int_not i))),T) 34 else 35 (bits_of_num (Num i), F)`; 36 37val num_of_bits_def = Define ` 38 (num_of_bits [] = 0:num) /\ 39 (num_of_bits (F::bs) = 2 * num_of_bits bs) /\ 40 (num_of_bits (T::bs) = 1 + 2 * num_of_bits bs)`; 41 42val int_of_bits_def = Define ` 43 int_of_bits (bs,rest) = 44 if rest then 45 int_not (& (num_of_bits (MAP (~) bs))) 46 else & (num_of_bits bs)`; 47 48val bits_bitwise_def = Define ` 49 (bits_bitwise f ([],r1) ([],r2) = ([],f r1 r2)) /\ 50 (bits_bitwise f ([],r1) (b2::bs2,r2) = 51 let (bs,r) = bits_bitwise f ([],r1) (bs2,r2) in 52 (f r1 b2 :: bs, r)) /\ 53 (bits_bitwise f (b1::bs1,r1) ([],r2) = 54 let (bs,r) = bits_bitwise f (bs1,r1) ([],r2) in 55 (f b1 r2 :: bs, r)) /\ 56 (bits_bitwise f (b1::bs1,r1) (b2::bs2,r2) = 57 let (bs,r) = bits_bitwise f (bs1,r1) (bs2,r2) in 58 (f b1 b2 :: bs, r))` 59 60val int_bitwise_def = Define ` 61 int_bitwise f i j = 62 int_of_bits (bits_bitwise f (bits_of_int i) (bits_of_int j))`; 63 64val int_and_def = Define ` 65 int_and = int_bitwise (/\)`; 66 67val int_or_def = Define ` 68 int_or = int_bitwise (\/)`; 69 70val int_xor_def = Define ` 71 int_xor = int_bitwise (<>)`; 72 73val MOD2 = prove( 74 ``n MOD 2 = if ODD n then 1 else 0``, 75 srw_tac [] [] \\ fs [ODD_EVEN,EVEN_MOD2] 76 \\ STRIP_ASSUME_TAC (Q.SPEC `n` (MATCH_MP DIVISION (DECIDE ``0<2:num``))) 77 \\ decide_tac); 78 79val num_of_bits_bits_of_num = prove( 80 ``!n. num_of_bits (bits_of_num n) = n``, 81 completeInduct_on `n` 82 \\ ONCE_REWRITE_TAC [bits_of_num_def] 83 \\ Cases_on `n = 0` \\ fs [num_of_bits_def] 84 \\ Cases_on `ODD n` \\ fs [num_of_bits_def] 85 \\ `n DIV 2 < n` by (fs [DIV_LT_X] \\ decide_tac) 86 \\ res_tac \\ fs [] 87 \\ STRIP_ASSUME_TAC (Q.SPEC `n` (MATCH_MP DIVISION (DECIDE ``0<2:num``))) 88 \\ Q.PAT_X_ASSUM `n = kkk:num` (fn th => CONV_TAC 89 (RAND_CONV (ONCE_REWRITE_CONV [th]))) 90 \\ ASSUME_TAC MOD2 91 \\ fs []); 92 93val bits_bitwise_NIL = prove( 94 ``!xs rest f. bits_bitwise f ([],F) (xs,rest) = (MAP (f F) xs,f F rest)``, 95 Induct \\ fs [bits_bitwise_def,LET_DEF]); 96 97val int_not = store_thm("int_not", 98 ``int_not = int_bitwise (\x y. ~y) 0``, 99 fs [int_bitwise_def,FUN_EQ_THM,EVAL ``bits_of_int 0``] 100 \\ fs [bits_of_int_def] \\ srw_tac [] [bits_bitwise_NIL] 101 \\ fs [MAP_MAP_o,combinTheory.o_DEF,int_of_bits_def,num_of_bits_bits_of_num] 102 \\ fs [int_not_def] \\ intLib.COOPER_TAC); 103 104val int_shift_left_def = Define ` 105 int_shift_left n i = 106 let (bs,r) = bits_of_int i in 107 int_of_bits (GENLIST (K F) n ++ bs,r)`; 108 109val int_shift_right_def = Define ` 110 int_shift_right n i = 111 let (bs,r) = bits_of_int i in 112 int_of_bits (DROP n bs,r)`; 113 114val int_not_lemma = prove( 115 ``!n. int_not (& n) < 0``, 116 fs [int_not_def] \\ intLib.COOPER_TAC); 117 118val BIT_lemmas = prove( 119 ``(BIT 0 (2 * k) = F) /\ 120 (BIT 0 (1 + 2 * k) = T) /\ 121 (BIT (SUC n) (2 * k) = BIT n k) /\ 122 (BIT (SUC n) (1 + 2 * k) = BIT n k)``, 123 simp_tac (srw_ss()) [GSYM BIT_DIV2] 124 \\ ONCE_REWRITE_TAC [ADD_COMM] 125 \\ ONCE_REWRITE_TAC [MULT_COMM] 126 \\ simp_tac (srw_ss()) [DIV_MULT,MULT_DIV] 127 \\ simp_tac (srw_ss()) [BIT_def,BITS_THM] 128 \\ rw [MOD_TIMES,MOD_EQ_0]); 129 130val BIT_num_of_bits = prove( 131 ``!bs n. BIT n (num_of_bits bs) = n < LENGTH bs /\ EL n bs``, 132 Induct \\ srw_tac [] [num_of_bits_def,BIT_ZERO] 133 \\ Cases_on `h` \\ srw_tac [] [num_of_bits_def] 134 \\ Cases_on `n` \\ fs [BIT_lemmas]); 135 136val int_bit_int_of_bits = store_thm("int_bit_int_of_bits", 137 ``int_bit n (int_of_bits b) = 138 if n < LENGTH (FST b) then EL n (FST b) else SND b``, 139 Cases_on `b` \\ Cases_on `r` \\ fs [int_of_bits_def] 140 \\ fs [int_bit_def,int_not_not] 141 \\ fs [int_not_def,int_not_lemma,BIT_num_of_bits] 142 \\ Cases_on `n < LENGTH q` \\ fs [EL_MAP]); 143 144val int_of_bits_bits_of_int = store_thm("int_of_bits_bits_of_int", 145 ``!i. int_of_bits (bits_of_int i) = i``, 146 srw_tac [] [int_of_bits_def,bits_of_int_def] 147 \\ fs [MAP_MAP_o,combinTheory.o_DEF,int_of_bits_def,num_of_bits_bits_of_num] 148 \\ fs [int_not_def] \\ intLib.COOPER_TAC); 149 150val int_bit_bitwise = store_thm("int_bit_bitwise", 151 ``!n f i j. int_bit n (int_bitwise f i j) = f (int_bit n i) (int_bit n j)``, 152 fs [int_bitwise_def,int_bit_int_of_bits] \\ REPEAT STRIP_TAC 153 \\ CONV_TAC (RAND_CONV (ONCE_REWRITE_CONV [GSYM int_of_bits_bits_of_int])) 154 \\ fs [int_bit_int_of_bits] 155 \\ Q.SPEC_TAC (`n`,`n`) 156 \\ Q.SPEC_TAC (`f`,`f`) 157 \\ Q.SPEC_TAC (`bits_of_int j`,`ys`) 158 \\ Q.SPEC_TAC (`bits_of_int i`,`xs`) 159 \\ fs [pairTheory.FORALL_PROD] 160 \\ Induct THEN1 161 (fs [LENGTH] \\ Induct_on `p_1'` \\ fs [bits_bitwise_def] 162 \\ REPEAT STRIP_TAC 163 \\ Cases_on `bits_bitwise f ([],p_2) (p_1',p_2')` 164 \\ fs [LET_DEF] \\ Cases_on `n` \\ fs [] 165 \\ FIRST_X_ASSUM (MP_TAC o Q.SPECL [`p_2`,`p_2'`,`f`,`n'`]) 166 \\ fs []) 167 \\ Cases_on `p_1'` 168 \\ fs [bits_bitwise_def] \\ REPEAT STRIP_TAC THEN1 169 (Cases_on `bits_bitwise f (p_1,p_2) ([],p_2')` 170 \\ fs [LET_DEF] \\ Cases_on `n` \\ fs [] 171 \\ FIRST_X_ASSUM (MP_TAC o Q.SPECL [`p_2`,`[]`,`p_2'`,`f`,`n'`]) \\ fs []) 172 THEN1 173 (Cases_on `bits_bitwise f (p_1,p_2) (t,p_2')` 174 \\ fs [LET_DEF] \\ Cases_on `n` \\ fs [] 175 \\ FIRST_X_ASSUM (MP_TAC o Q.SPECL [`p_2`,`t`,`p_2'`,`f`,`n'`]) \\ fs [])); 176 177val int_bit_and = save_thm("int_bit_and", 178 ``int_bit n (int_and i j)`` 179 |> SIMP_CONV std_ss [int_and_def,int_bit_bitwise] |> Q.GENL [`j`,`i`,`n`]); 180 181val int_bit_or = save_thm("int_bit_or", 182 ``int_bit n (int_or i j)`` 183 |> SIMP_CONV std_ss [int_or_def,int_bit_bitwise] |> Q.GENL [`j`,`i`,`n`]); 184 185val int_bit_xor = save_thm("int_bit_xor", 186 ``int_bit n (int_xor i j)`` 187 |> SIMP_CONV std_ss [int_xor_def,int_bit_bitwise] |> Q.GENL [`j`,`i`,`n`]); 188 189val LAST_bits_of_num = prove( 190 ``!n. LENGTH (bits_of_num n) <> 0 ==> 191 EL (LENGTH (bits_of_num n) - 1) (bits_of_num n)``, 192 HO_MATCH_MP_TAC (fetch "-" "bits_of_num_ind") 193 \\ REPEAT STRIP_TAC \\ ONCE_REWRITE_TAC [bits_of_num_def] 194 \\ Cases_on `n = 0` \\ fs [EVAL ``bits_of_num 0``] 195 \\ Cases_on `bits_of_num (n DIV 2)` \\ fs [] 196 \\ Cases_on `n = 1` \\ fs [] 197 \\ fs[Once bits_of_num_def] 198 \\ `~(n < 2)` by decide_tac 199 \\ fs [DIV_EQ_X]); 200 201val int_not_lemma = prove( 202 ``(int_not (& n) <> & m) /\ ((int_not i = int_not j) <=> (i = j))``, 203 fs [int_not_def] \\ COOPER_TAC); 204 205val int_of_bits_11_lemma = prove( 206 ``(int_of_bits (bits_of_int i) = int_of_bits (bits_of_int j)) <=> 207 (bits_of_int i = bits_of_int j)``, 208 eq_tac \\ srw_tac [] [] \\ fs [bits_of_int_def] 209 \\ srw_tac [] [] \\ fs [] \\ fs [int_of_bits_def,int_not_lemma] 210 \\ fs [MAP_MAP_o,combinTheory.o_DEF,int_of_bits_def,num_of_bits_bits_of_num]); 211 212val bits_of_int_LAST = prove( 213 ``!i bs r. (bits_of_int i = (bs,r)) /\ (bs <> []) ==> 214 EL (LENGTH bs - 1) bs <> r``, 215 srw_tac [] [bits_of_int_def,EL_MAP,LENGTH_MAP] 216 \\ fs [MAP_EQ_NIL] \\ full_simp_tac std_ss [GSYM LENGTH_NIL] 217 \\ imp_res_tac (DECIDE ``n <> 0 ==> n - 1 < n:num``) 218 \\ fs [bits_of_int_def,EL_MAP,LENGTH_MAP] 219 \\ match_mp_tac LAST_bits_of_num \\ fs []); 220 221val int_bit_equiv = store_thm("int_bit_equiv", 222 ``!i j. (i = j) <=> !n. int_bit n i = int_bit n j``, 223 ONCE_REWRITE_TAC [GSYM int_of_bits_bits_of_int] 224 \\ fs [int_bit_int_of_bits,int_of_bits_11_lemma] 225 \\ srw_tac [] [] \\ Cases_on `bits_of_int i` \\ Cases_on `bits_of_int j` 226 \\ fs [] \\ eq_tac \\ REVERSE (srw_tac [] []) 227 \\ `r' = r` by (POP_ASSUM (MP_TAC o Q.SPEC `LENGTH (q:bool list) + 228 LENGTH (q':bool list)`) 229 \\ fs [DECIDE ``~(m+n<n) /\ ~(m+n<m:num)``]) 230 \\ srw_tac [] [] 231 \\ `LENGTH q' = LENGTH q` suffices_by 232 (STRIP_TAC THEN fs [] \\ match_mp_tac LIST_EQ 233 \\ fs [] \\ rpt strip_tac 234 \\ first_x_assum (mp_tac o Q.SPEC `x`) 235 \\ fs []) 236 \\ CCONTR_TAC 237 \\ Q.MATCH_ASSUM_RENAME_TAC `LENGTH bs2 <> LENGTH bs1` 238 \\ `LENGTH bs1 < LENGTH bs2 \/ LENGTH bs2 < LENGTH bs1` by DECIDE_TAC 239 \\ IMP_RES_TAC bits_of_int_LAST 240 THEN1 (Cases_on `bs2 = []` \\ fs [LENGTH] 241 \\ FIRST_X_ASSUM (MP_TAC o Q.SPEC `LENGTH (bs2:bool list) - 1`) 242 \\ fs [] \\ srw_tac [] [] \\ `F` by intLib.COOPER_TAC) 243 THEN1 (Cases_on `bs1 = []` \\ fs [LENGTH] 244 \\ FIRST_X_ASSUM (MP_TAC o Q.SPEC `LENGTH (bs1:bool list) - 1`) 245 \\ fs [] \\ srw_tac [] [] \\ `F` by intLib.COOPER_TAC)); 246 247val int_bit_shift_left_lemma1 = prove( 248 ``!b n i. int_bit (b + n) (int_shift_left n i) = int_bit b i``, 249 fs [int_shift_left_def] \\ rpt strip_tac 250 \\ Cases_on `bits_of_int i` 251 \\ CONV_TAC (RAND_CONV (ONCE_REWRITE_CONV [GSYM int_of_bits_bits_of_int])) 252 \\ fs [LET_DEF,int_bit_int_of_bits] 253 \\ srw_tac [] [LENGTH_GENLIST,rich_listTheory.EL_APPEND2]); 254 255val int_bit_shift_left_lemma2 = prove( 256 ``!b n i. b < n ==> ~int_bit b (int_shift_left n i)``, 257 fs [int_shift_left_def] \\ rpt strip_tac 258 \\ Cases_on `bits_of_int i` 259 \\ fs [LET_DEF,int_bit_int_of_bits] 260 \\ `b < n + LENGTH q` by decide_tac \\ fs [] 261 \\ qpat_x_assum `EL _ _` MP_TAC 262 \\ fs [rich_listTheory.EL_APPEND1,LENGTH_GENLIST]); 263 264val int_bit_shift_left = store_thm("int_bit_shift_left", 265 ``!b n i. int_bit b (int_shift_left n i) = n <= b /\ int_bit (b - n) i``, 266 REPEAT STRIP_TAC \\ Cases_on `b < n` 267 \\ asm_simp_tac (srw_ss()) [int_bit_shift_left_lemma2] THEN1 decide_tac 268 \\ fs [NOT_LESS] \\ imp_res_tac LESS_EQUAL_ADD 269 \\ fs [] \\ ONCE_REWRITE_TAC [ADD_COMM] 270 \\ simp_tac (srw_ss()) [int_bit_shift_left_lemma1]); 271 272val int_bit_shift_right = store_thm("int_bit_shift_right", 273 ``!b n i. int_bit b (int_shift_right n i) = int_bit (b + n) i``, 274 fs [int_shift_right_def] \\ rpt strip_tac 275 \\ Cases_on `bits_of_int i` 276 \\ CONV_TAC (RAND_CONV (ONCE_REWRITE_CONV [GSYM int_of_bits_bits_of_int])) 277 \\ fs [LET_DEF,int_bit_int_of_bits] 278 \\ srw_tac [] [rich_listTheory.EL_DROP] 279 \\ fs [NOT_LESS] \\ `F` by decide_tac); 280 281val _ = export_theory(); 282