int_bitwiseScript.sml

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