numeral_bitScript.sml
1(* ========================================================================= *)
2(* FILE : numeral_bitScript.sml *)
3(* DESCRIPTION : Theorems providing numeral based evaluation of *)
4(* functions in bitTheory *)
5(* AUTHOR : (c) Anthony Fox, University of Cambridge *)
6(* DATE : 2001-2005 *)
7(* ========================================================================= *)
8Theory numeral_bit[bare]
9Ancestors
10 arithmetic numeral bit
11Libs
12 HolKernel Parse boolLib BasicProvers metisLib simpLib numSimps
13 numLib
14
15
16(* ------------------------------------------------------------------------- *)
17
18val BIT1n =
19 METIS_PROVE [ONE, ADD_ASSOC, BIT1, TIMES2] ``!n. BIT1 n = 2 * n + 1``
20
21val BIT2n =
22 METIS_PROVE [ADD_ASSOC,ADD1,ADD,BIT2,TIMES2] ``!n. BIT2 n = 2 * (SUC n)``
23
24val ONE_LT_TWO = METIS_PROVE [ONE, TWO, prim_recTheory.LESS_SUC_REFL] ``1 < 2``
25
26val ONE_LT_TWOEXP =
27 METIS_PROVE [EXP_BASE_LT_MONO, EXP, ONE_LT_TWO, prim_recTheory.LESS_0]
28 ``!n. 1 < 2 ** SUC n``
29
30val ZERO_LT_TWO = METIS_PROVE [TWO, prim_recTheory.LESS_0] ``0 < 2``
31
32val ZERO_LT_TWOEXP =
33 (GEN_ALL o REWRITE_RULE [GSYM TWO] o Q.SPECL [`n`,`1`]) ZERO_LESS_EXP
34
35val DOUBLE_LT_COR =
36 METIS_PROVE [DOUBLE_LT, LT_MULT_LCANCEL, ZERO_LT_TWO]
37 ``!a b. a < b ==> 2 * a + 1 < 2 * b``
38
39Theorem NUMERAL_MOD_2EXP[local]:
40 (!n. MOD_2EXP 0 n = ZERO) /\
41 (!x n. MOD_2EXP x ZERO = ZERO) /\
42 (!x n. MOD_2EXP (SUC x) (BIT1 n) = BIT1 (MOD_2EXP x n)) /\
43 (!x n. MOD_2EXP (SUC x) (BIT2 n) = numeral$iDUB (MOD_2EXP x (SUC n)))
44Proof
45 RW_TAC bool_ss [MOD_2EXP_def, iDUB, GSYM DIV2_def, EXP, MOD_1, GSYM TIMES2,
46 REWRITE_RULE [SYM ALT_ZERO, NUMERAL_DEF, ADD1] numeral_div2]
47 THENL [
48 REWRITE_TAC [ALT_ZERO],
49 METIS_TAC [ALT_ZERO, ZERO_MOD, ZERO_LT_TWOEXP],
50 STRIP_ASSUME_TAC (Q.SPEC `x` num_CASES)
51 THENL [
52 ASM_REWRITE_TAC [EXP, MULT_RIGHT_1, MOD_1]
53 \\ SUBST1_TAC (Q.SPEC `n` BIT1n)
54 \\ SIMP_TAC bool_ss
55 [ONE_LT_TWO, MOD_MULT, Q.SPEC `0` BIT1n,
56 ONCE_REWRITE_RULE [GSYM MULT_COMM] MOD_MULT, MULT_0, ADD],
57 POP_ASSUM SUBST1_TAC
58 \\ SUBST1_TAC (Q.SPEC `n` BIT1n)
59 \\ SIMP_TAC bool_ss [Once (GSYM MOD_PLUS), ZERO_LT_TWOEXP, GSYM EXP]
60 \\ SIMP_TAC bool_ss
61 [Once EXP, GSYM MOD_COMMON_FACTOR, ZERO_LT_TWOEXP, ZERO_LT_TWO]
62 \\ SIMP_TAC bool_ss [LESS_MOD, ONE_LT_TWOEXP]
63 \\ METIS_TAC
64 [BIT1n, DOUBLE_LT_COR, LESS_MOD, EXP, DIVISION, ZERO_LT_TWOEXP]
65 ],
66 Q.SPEC_THEN `n` SUBST1_TAC BIT2n
67 \\ METIS_TAC
68 [MOD_COMMON_FACTOR, TWO, prim_recTheory.LESS_0, ZERO_LT_TWOEXP]
69 ]
70QED
71
72Definition iMOD_2EXP[nocompute]: iMOD_2EXP = MOD_2EXP
73End
74
75val BIT1n = REWRITE_RULE [GSYM ADD1] BIT1n
76
77Theorem numeral_imod_2exp:
78 (!n. iMOD_2EXP 0 n = ZERO) /\
79 (!x n. iMOD_2EXP x ZERO = ZERO) /\
80 (!x n. iMOD_2EXP (NUMERAL (BIT1 x)) (BIT1 n) =
81 BIT1 (iMOD_2EXP (NUMERAL (BIT1 x) - 1) n)) /\
82 (!x n. iMOD_2EXP (NUMERAL (BIT2 x)) (BIT1 n) =
83 BIT1 (iMOD_2EXP (NUMERAL (BIT1 x)) n)) /\
84 (!x n. iMOD_2EXP (NUMERAL (BIT1 x)) (BIT2 n) =
85 numeral$iDUB (iMOD_2EXP (NUMERAL (BIT1 x) - 1) (SUC n))) /\
86 !x n. iMOD_2EXP (NUMERAL (BIT2 x)) (BIT2 n) =
87 numeral$iDUB (iMOD_2EXP (NUMERAL (BIT1 x)) (SUC n))
88Proof
89 RW_TAC bool_ss [iMOD_2EXP, NUMERAL_MOD_2EXP]
90 \\ SUBST1_TAC (Q.SPEC `BIT1 x` NUMERAL_DEF)
91 \\ SUBST1_TAC (Q.SPEC `BIT2 x` NUMERAL_DEF)
92 \\ SUBST1_TAC (Q.SPEC `x` BIT1n)
93 \\ SUBST1_TAC (Q.SPEC `x` ((GSYM o hd o tl o CONJUNCTS) numeral_suc))
94 \\ SIMP_TAC bool_ss [NUMERAL_MOD_2EXP, SUC_SUB1, GSYM BIT1n]
95QED
96
97Theorem MOD_2EXP =
98 CONJ (REWRITE_RULE [ALT_ZERO] (hd (tl (CONJUNCTS NUMERAL_MOD_2EXP))))
99 (METIS_PROVE [NUMERAL_DEF, iMOD_2EXP]
100 ``!x n. MOD_2EXP x (NUMERAL n) = NUMERAL (iMOD_2EXP x n)``)
101
102Theorem DIV_2EXP:
103 !n x. DIV_2EXP n x = FUNPOW DIV2 n x
104Proof
105 Induct
106 \\ ASM_SIMP_TAC bool_ss
107 [DIV_2EXP_def, CONJUNCT1 FUNPOW, FUNPOW_SUC, CONJUNCT1 EXP, DIV_1]
108 \\ POP_ASSUM
109 (fn th =>
110 SIMP_TAC bool_ss
111 [GSYM th, EXP_1, ADD1, EXP_ADD, DIV2_def, DIV_2EXP_def,
112 DIV_DIV_DIV_MULT, ZERO_LT_TWO, ZERO_LT_TWOEXP])
113QED
114
115(* ------------------------------------------------------------------------- *)
116
117Theorem numeral_mod2:
118 (0 MOD 2 = 0) /\
119 (!n. NUMERAL (BIT1 n) MOD 2 = 1) /\
120 (!n. NUMERAL (BIT2 n) MOD 2 = 0)
121Proof
122 SRW_TAC [] []
123 >| [`NUMERAL (BIT1 n) = 2 * n + 1`
124 by metisLib.METIS_TAC [NUMERAL_DEF, ONE, ADD_ASSOC, BIT1, TIMES2],
125 `NUMERAL (BIT2 n) = 2 * (SUC n)`
126 by metisLib.METIS_TAC [NUMERAL_DEF, ADD_ASSOC, ADD1, ADD, BIT2, TIMES2]]
127 \\ POP_ASSUM SUBST1_TAC
128 \\ SRW_TAC [numSimps.MOD_ss] []
129QED
130
131Theorem iDUB_NUMERAL:
132 numeral$iDUB (NUMERAL i) = NUMERAL (numeral$iDUB i)
133Proof
134 REWRITE_TAC [arithmeticTheory.NUMERAL_DEF]
135QED
136
137Definition BIT_REV_def[nocompute]:
138 (BIT_REV 0 x y = y) /\
139 (BIT_REV (SUC n) x y =
140 BIT_REV n (x DIV 2) (2 * y + SBIT (ODD x) 0))
141End
142
143val BIT_R = ``\(x,y). (x DIV 2, 2 * y + SBIT (BIT 0 x) 0)``
144
145Theorem BIT_R_FUNPOW[local]:
146 !n x y.
147 FUNPOW ^BIT_R (SUC n) (x,y) =
148 (x DIV 2 ** (SUC n),
149 2 * (SND (FUNPOW ^BIT_R n (x, y))) + SBIT (BIT n x) 0)
150Proof
151 Induct
152 >- SIMP_TAC arith_ss [FUNPOW]
153 \\ `!x n. BIT 0 (x DIV 2 ** n) = BIT n x`
154 by SIMP_TAC std_ss [BIT_def, BITS_THM, BITS_COMP_THM2, DIV_1, SUC_SUB]
155 \\ ASM_SIMP_TAC std_ss [FUNPOW_SUC, DIV_DIV_DIV_MULT, ZERO_LT_TWOEXP,
156 (GSYM o ONCE_REWRITE_RULE [MULT_COMM]) EXP]
157QED
158
159Theorem BIT_R_BIT_REV[local]:
160 !n a y. SND (FUNPOW ^BIT_R n (a, y)) = BIT_REV n a y
161Proof
162 Induct
163 >- SIMP_TAC std_ss [FUNPOW, BIT_REV_def]
164 \\ ASM_SIMP_TAC std_ss [FUNPOW, BIT_REV_def, GSYM BIT0_ODD]
165QED
166
167Theorem BIT_REVERSE_REV[local]:
168 !m n. BIT_REVERSE m n = SND (FUNPOW ^BIT_R m (n, 0))
169Proof
170 Induct
171 >- SIMP_TAC std_ss [BIT_REVERSE_def, FUNPOW]
172 \\ ASM_SIMP_TAC arith_ss [BIT_REVERSE_def, BIT_R_FUNPOW]
173QED
174
175Theorem BIT_REVERSE_EVAL =
176 REWRITE_RULE [BIT_R_BIT_REV] BIT_REVERSE_REV
177
178(* ------------------------------------------------------------------------- *)
179
180Definition BIT_MODF_def[nocompute]:
181 (BIT_MODF 0 f x b e y = y) /\
182 (BIT_MODF (SUC n) f x b e y =
183 BIT_MODF n f (x DIV 2) (b + 1) (2 * e)
184 (if f b (ODD x) then e + y else y))
185End
186
187val BIT_M =
188 ``\(y,f,x,b,e).
189 (if f b (BIT 0 x) then e + y else y, f, x DIV 2, b + 1, 2 * e)``
190
191Theorem BIT_M_FUNPOW[local]:
192 !n f x b e y. FUNPOW ^BIT_M (SUC n) (y,f,x,b,e) =
193 (if f (b + n) (BIT n x)
194 then 2 ** n * e + FST (FUNPOW ^BIT_M n (y,f,x,b,e))
195 else FST (FUNPOW ^BIT_M n (y,f,x,b,e)),
196 f, x DIV 2 ** (SUC n), b + SUC n, 2 ** SUC n * e)
197Proof
198 Induct
199 >- SIMP_TAC arith_ss [FUNPOW]
200 \\ `!x n. BIT 0 (x DIV 2 ** n) = BIT n x`
201 by SIMP_TAC std_ss [BIT_def, BITS_THM, BITS_COMP_THM2, DIV_1, SUC_SUB]
202 \\ ASM_SIMP_TAC arith_ss
203 [FUNPOW_SUC, DIV_DIV_DIV_MULT, ZERO_LT_TWOEXP,
204 (GSYM o ONCE_REWRITE_RULE [MULT_COMM]) EXP]
205 \\ SIMP_TAC (std_ss++numSimps.ARITH_AC_ss) [EXP]
206QED
207
208Theorem BIT_M_BIT_MODF[local]:
209 !n f x b e y. FST (FUNPOW ^BIT_M n (y,f,x,b,e)) = BIT_MODF n f x b e y
210Proof
211 Induct
212 >- SIMP_TAC std_ss [FUNPOW, BIT_MODF_def]
213 \\ ASM_SIMP_TAC std_ss [FUNPOW, BIT_MODF_def, GSYM BIT0_ODD]
214QED
215
216Theorem BIT_MODIFY_MODF[local]:
217 !m f n. BIT_MODIFY m f n = FST (FUNPOW ^BIT_M m (0,f,n,0,1))
218Proof
219 Induct
220 >- SIMP_TAC std_ss [BIT_MODIFY_def, FUNPOW]
221 \\ RW_TAC arith_ss [SBIT_def, BIT_MODIFY_def, BIT_M_FUNPOW]
222QED
223
224Theorem BIT_MODIFY_EVAL =
225 REWRITE_RULE [BIT_M_BIT_MODF] BIT_MODIFY_MODF
226
227(* ------------------------------------------------------------------------- *)
228
229val SUC_RULE = CONV_RULE numLib.SUC_TO_NUMERAL_DEFN_CONV
230
231val iBITWISE_def =
232 Definition.new_definition("iBITWISE_def", ``iBITWISE = BITWISE``)
233
234val SIMP_BIT1 = (GSYM o SIMP_RULE arith_ss []) BIT1
235
236Theorem iBITWISE[local]:
237 (!opr a b. iBITWISE 0 opr a b = ZERO) /\
238 (!x opr a b.
239 iBITWISE (SUC x) opr a b =
240 let w = iBITWISE x opr (DIV2 a) (DIV2 b) in
241 if opr (ODD a) (ODD b) then BIT1 w else numeral$iDUB w)
242Proof
243 RW_TAC arith_ss [iBITWISE_def, iDUB, SIMP_BIT1, SBIT_def, EXP,
244 BIT0_ODD, GSYM DIV2_def, BITWISE_EVAL, LET_THM]
245 \\ REWRITE_TAC [BITWISE_def, ALT_ZERO]
246QED
247
248Theorem iBITWISE = SUC_RULE iBITWISE
249
250Theorem NUMERAL_BITWISE:
251 (!x f a. BITWISE x f 0 0 = NUMERAL (iBITWISE x f 0 0)) /\
252 (!x f a. BITWISE x f (NUMERAL a) 0 =
253 NUMERAL (iBITWISE x f (NUMERAL a) 0)) /\
254 (!x f b. BITWISE x f 0 (NUMERAL b) =
255 NUMERAL (iBITWISE x f 0 (NUMERAL b))) /\
256 !x f a b. BITWISE x f (NUMERAL a) (NUMERAL b) =
257 NUMERAL (iBITWISE x f (NUMERAL a) (NUMERAL b))
258Proof
259 REWRITE_TAC [iBITWISE_def, NUMERAL_DEF]
260QED
261
262Theorem NUMERAL_BIT_REV[local]:
263 (!x y. BIT_REV 0 x y = y) /\
264 (!n y. BIT_REV (SUC n) 0 y = BIT_REV n 0 (numeral$iDUB y)) /\
265 (!n x y. BIT_REV (SUC n) (NUMERAL x) y =
266 BIT_REV n (DIV2 (NUMERAL x))
267 (if ODD x then BIT1 y else numeral$iDUB y))
268Proof
269 RW_TAC bool_ss [BIT_REV_def, SBIT_def, NUMERAL_DEF, DIV2_def,
270 ADD, ADD_0, BIT2, BIT1, iDUB, ALT_ZERO]
271 \\ FULL_SIMP_TAC arith_ss []
272QED
273
274Theorem NUMERAL_BIT_REV = SUC_RULE NUMERAL_BIT_REV
275
276Theorem NUMERAL_BIT_REVERSE:
277 (!m. BIT_REVERSE (NUMERAL m) 0 = NUMERAL (BIT_REV (NUMERAL m) 0 ZERO)) /\
278 !n m. BIT_REVERSE (NUMERAL m) (NUMERAL n) =
279 NUMERAL (BIT_REV (NUMERAL m) (NUMERAL n) ZERO)
280Proof
281 SIMP_TAC bool_ss [NUMERAL_DEF, ALT_ZERO, BIT_REVERSE_EVAL]
282QED
283
284Theorem NUMERAL_BIT_MODF[local]:
285 (!f x b e y. BIT_MODF 0 f x b e y = y) /\
286 (!n f b e y.
287 BIT_MODF (SUC n) f 0 b (NUMERAL e) y =
288 BIT_MODF n f 0 (b + 1) (NUMERAL (numeral$iDUB e))
289 (if f b F then (NUMERAL e) + y else y)) /\
290 (!n f x b e y.
291 BIT_MODF (SUC n) f (NUMERAL x) b (NUMERAL e) y =
292 BIT_MODF n f (DIV2 (NUMERAL x)) (b + 1) (NUMERAL (numeral$iDUB e))
293 (if f b (ODD x) then (NUMERAL e) + y else y))
294Proof
295 RW_TAC bool_ss [BIT_MODF_def, SBIT_def, NUMERAL_DEF, DIV2_def,
296 ADD, ADD_0, BIT2, BIT1, iDUB, ALT_ZERO]
297 \\ FULL_SIMP_TAC arith_ss []
298QED
299
300Theorem NUMERAL_BIT_MODF = SUC_RULE NUMERAL_BIT_MODF
301
302Theorem NUMERAL_BIT_MODIFY:
303 (!m f. BIT_MODIFY (NUMERAL m) f 0 = BIT_MODF (NUMERAL m) f 0 0 1 0) /\
304 !m f n. BIT_MODIFY (NUMERAL m) f (NUMERAL n) =
305 BIT_MODF (NUMERAL m) f (NUMERAL n) 0 1 0
306Proof
307 SIMP_TAC bool_ss [NUMERAL_DEF, ALT_ZERO, BIT_MODIFY_EVAL]
308QED
309
310(* ------------------------------------------------------------------------- *)
311
312val iSUC_def = Definition.new_definition ("iSUC",``iSUC = SUC``)
313
314val iDIV2_def = Definition.new_definition ("iDIV2",``iDIV2 = DIV2``)
315
316Definition SFUNPOW_def[nocompute]:
317 (SFUNPOW f 0 x = x) /\
318 (SFUNPOW f (SUC n) x = if x = 0n then 0n else SFUNPOW f n (f x))
319End
320
321Definition FDUB_def[nocompute]:
322 (FDUB f 0 = 0n) /\
323 (FDUB f (SUC n) = f (f (SUC n)))
324End
325
326Theorem FDUB_lem[local]:
327 !f. (f 0 = 0n) ==> (FDUB f = (\x.f (f x)))
328Proof
329 REWRITE_TAC [FUN_EQ_THM]
330 \\ GEN_TAC
331 \\ DISCH_TAC
332 \\ BETA_TAC
333 \\ Cases
334 \\ ASM_REWRITE_TAC [FDUB_def]
335QED
336
337Theorem SFUNPOW_strict[local]:
338 !n f x. SFUNPOW f n 0 = 0
339Proof
340 Cases \\ REWRITE_TAC [SFUNPOW_def]
341QED
342
343Theorem SFUNPOW_BIT1_lem[local]:
344 !n f x.
345 (f 0 = 0) ==>
346 (SFUNPOW f (NUMERAL (BIT1 n)) x = SFUNPOW (FDUB f) n (f x))
347Proof
348 REWRITE_TAC [NUMERAL_DEF, BIT1, ADD_CLAUSES]
349 \\ Induct
350 \\ REPEAT STRIP_TAC
351 \\ REWRITE_TAC [NUMERAL_DEF, BIT1, ADD_CLAUSES]
352 >- (IMP_RES_TAC FDUB_lem \\ ASM_REWRITE_TAC [SFUNPOW_def] \\ PROVE_TAC [])
353 \\ ONCE_REWRITE_TAC [SFUNPOW_def]
354 \\ ONCE_REWRITE_TAC [SFUNPOW_def]
355 \\ RES_TAC
356 \\ RW_TAC std_ss []
357 \\ IMP_RES_TAC FDUB_lem
358 \\ PROVE_TAC []
359QED
360
361Theorem SFUNPOW_BIT2_lem[local]:
362 !n f x.
363 (f 0 = 0) ==>
364 (SFUNPOW f (NUMERAL (BIT2 n)) x = SFUNPOW (FDUB f) n (f (f x)))
365Proof
366 `!n. NUMERAL (BIT2 n) = SUC (NUMERAL (BIT1 n))`
367 by REWRITE_TAC [NUMERAL_DEF, BIT1, BIT2, ADD_CLAUSES]
368 \\ REPEAT STRIP_TAC
369 \\ IMP_RES_TAC SFUNPOW_BIT1_lem
370 \\ ASM_REWRITE_TAC [SFUNPOW_def]
371 \\ RW_TAC std_ss [SFUNPOW_strict]
372QED
373
374Theorem NUMERAL_SFUNPOW[local]:
375 !f. (f 0 = 0) ==>
376 (!x. SFUNPOW f 0 x = x) /\
377 (!y. SFUNPOW f y 0 = 0) /\
378 (!n x. SFUNPOW f (NUMERAL (BIT1 n)) x =
379 SFUNPOW (FDUB f) (NUMERAL n) (f x)) /\
380 (!n x. SFUNPOW f (NUMERAL (BIT2 n)) x =
381 SFUNPOW (FDUB f) (NUMERAL n) (f (f x)))
382Proof
383 REPEAT STRIP_TAC
384 \\ MAP_EVERY IMP_RES_TAC [SFUNPOW_BIT1_lem, SFUNPOW_BIT2_lem]
385 \\ ASM_REWRITE_TAC [SFUNPOW_strict, SFUNPOW_def, NUMERAL_DEF]
386QED
387
388Theorem NUMERAL_TIMES_2EXP:
389 (!n. TIMES_2EXP n 0 = 0) /\
390 (!n x. TIMES_2EXP n (NUMERAL x) = NUMERAL (SFUNPOW numeral$iDUB n x))
391Proof
392 CONJ_TAC
393 \\ REWRITE_TAC [TIMES_2EXP_def, MULT_CLAUSES]
394 \\ Induct
395 \\ REWRITE_TAC [EXP, SFUNPOW_def, MULT_CLAUSES, MULT_ASSOC]
396 \\ POP_ASSUM (ASSUME_TAC o GSYM)
397 \\ RW_TAC std_ss []
398 \\ ASM_REWRITE_TAC [NUMERAL_DEF, BIT1, BIT2, iDUB, ALT_ZERO, ADD_CLAUSES]
399 \\ RW_TAC arith_ss []
400QED
401
402Theorem NUMERAL_iDIV2:
403 (iDIV2 ZERO = ZERO) /\
404 (iDIV2 (iSUC ZERO) = ZERO) /\
405 (iDIV2 (BIT1 n) = n) /\
406 (iDIV2 (iSUC (BIT1 n)) = iSUC n) /\
407 (iDIV2 (BIT2 n) = iSUC n) /\
408 (iDIV2 (iSUC (BIT2 n)) = iSUC n) /\
409 (NUMERAL (iSUC n) = NUMERAL (SUC n))
410Proof
411 REWRITE_TAC [ALT_ZERO, BIT1, BIT2, iDIV2_def, iSUC_def, ADD_CLAUSES]
412 \\ REWRITE_TAC [DIV2_def, GSYM TIMES2]
413 \\ `0 < 2 /\ 1 < 2` by DECIDE_TAC
414 \\ MAP_EVERY IMP_RES_TAC
415 [ZERO_DIV, ADD_DIV_RWT, DIV_LESS,
416 LESS_DIV_EQ_ZERO, ONCE_REWRITE_RULE [MULT_COMM] MULT_DIV]
417 \\ RULE_ASSUM_TAC (REWRITE_RULE [GSYM EVEN_MOD2])
418 \\ RW_TAC arith_ss [ADD1, EVEN_DOUBLE]
419QED
420
421Theorem NUMERAL_DIV_2EXP:
422 (!n. DIV_2EXP n 0 = 0) /\
423 (!n x. DIV_2EXP n (NUMERAL x) = NUMERAL (SFUNPOW iDIV2 n x))
424Proof
425 CONJ_TAC
426 \\ REWRITE_TAC [DIV_2EXP_def]
427 >- (STRIP_TAC \\ MATCH_MP_TAC ZERO_DIV \\ RW_TAC std_ss [ZERO_LT_TWOEXP])
428 \\ Induct
429 \\ REWRITE_TAC [EXP, SFUNPOW_def, DIV_1]
430 \\ `!x. NUMERAL x DIV 2 = NUMERAL (x DIV 2)` by REWRITE_TAC [NUMERAL_DEF]
431 \\ RW_TAC arith_ss
432 [ZERO_LT_TWOEXP, GSYM DIV_DIV_DIV_MULT, SFUNPOW_strict, iDIV2_def,
433 DIV2_def]
434QED
435
436Theorem NUMERAL_SFUNPOW_iDIV2 =
437 MATCH_MP (SPEC_ALL NUMERAL_SFUNPOW)
438 (Q.prove(`iDIV2 0 = 0`, RW_TAC arith_ss [iDIV2_def, DIV2_def]))
439
440Theorem NUMERAL_SFUNPOW_iDUB =
441 MATCH_MP (SPEC_ALL NUMERAL_SFUNPOW)
442 (Q.prove(`numeral$iDUB 0 = 0`, RW_TAC arith_ss [iDUB]))
443
444Theorem NUMERAL_SFUNPOW_FDUB =
445 GEN_ALL (MATCH_MP (SPEC_ALL NUMERAL_SFUNPOW)
446 (SPEC_ALL (CONJUNCT1 FDUB_def)))
447
448Theorem FDUB_iDIV2:
449 !x. FDUB iDIV2 x = iDIV2 (iDIV2 x)
450Proof
451 Cases \\ RW_TAC arith_ss [FDUB_def, iDIV2_def, DIV2_def]
452QED
453
454Theorem FDUB_iDUB:
455 !x. FDUB numeral$iDUB x = numeral$iDUB (numeral$iDUB x)
456Proof
457 Cases \\ RW_TAC arith_ss [FDUB_def, iDUB]
458QED
459
460Theorem FDUB_FDUB:
461 (FDUB (FDUB f) ZERO = ZERO) /\
462 (!x. FDUB (FDUB f) (iSUC x) = FDUB f (FDUB f (iSUC x))) /\
463 (!x. FDUB (FDUB f) (BIT1 x) = FDUB f (FDUB f (BIT1 x))) /\
464 (!x. FDUB (FDUB f) (BIT2 x) = FDUB f (FDUB f (BIT2 x)))
465Proof
466 REWRITE_TAC [BIT1, BIT2, iSUC_def, FDUB_def, ALT_ZERO, ADD_CLAUSES]
467QED
468
469(* ------------------------------------------------------------------------- *)
470
471Theorem LOG_compute:
472 !m n. LOG m n =
473 if m < 2 \/ (n = 0) then
474 FAIL LOG ^(mk_var("base < 2 or n = 0", bool)) m n
475 else
476 if n < m then
477 0
478 else
479 SUC (LOG m (n DIV m))
480Proof
481 SRW_TAC [ARITH_ss] [logrootTheory.LOG_RWT, combinTheory.FAIL_THM]
482QED
483
484val iLOG2_def =
485 Definition.new_definition("iLOG2_def", ``iLOG2 n = LOG2 (n + 1)``)
486
487val LOG2_1 = (SIMP_RULE arith_ss [] o Q.SPECL [`1`,`0`]) LOG2_UNIQUE
488
489Theorem numeral_ilog2:
490 (iLOG2 ZERO = 0) /\
491 (!n. iLOG2 (BIT1 n) = 1 + iLOG2 n) /\
492 (!n. iLOG2 (BIT2 n) = 1 + iLOG2 n)
493Proof
494 RW_TAC bool_ss [ALT_ZERO, NUMERAL_DEF, BIT1, BIT2, iLOG2_def]
495 \\ SIMP_TAC arith_ss [LOG2_1]
496 >| [
497 MATCH_MP_TAC
498 ((SIMP_RULE arith_ss [] o Q.SPECL [`2 * n + 2`, `LOG2 (n + 1) + 1`])
499 LOG2_UNIQUE)
500 \\ SIMP_TAC arith_ss [EXP_ADD, LOG2_def]
501 \\ SIMP_TAC arith_ss
502 [GSYM ADD1, EXP, logrootTheory.LOG,
503 DECIDE ``(2 * n + 2 = (n + 1) * 2) /\
504 (2 * a < 4 * b <=> a < 2 * b)``]
505 \\ SIMP_TAC arith_ss [GSYM EXP, logrootTheory.LOG],
506 MATCH_MP_TAC
507 ((SIMP_RULE arith_ss [] o Q.SPECL [`2 * n + 3`, `LOG2 (n + 1) + 1`])
508 LOG2_UNIQUE)
509 \\ SIMP_TAC arith_ss [EXP_ADD, LOG2_def]
510 \\ SIMP_TAC arith_ss
511 [GSYM ADD1, EXP, logrootTheory.LOG,
512 DECIDE ``(2 * n + 3 = 2 * (n + 1) + 1)``,
513 DECIDE ``a <= b ==> 2 * a <= SUC (2 * b)``]
514 \\ SIMP_TAC arith_ss
515 [DECIDE ``a < 2 * b ==> SUC (2 * a) < 4 * b``,
516 (Once o GSYM) EXP, logrootTheory.LOG]
517 ]
518QED
519
520Theorem numeral_log2:
521 (!n. LOG2 (NUMERAL (BIT1 n)) = iLOG2 (numeral$iDUB n)) /\
522 (!n. LOG2 (NUMERAL (BIT2 n)) = iLOG2 (BIT1 n))
523Proof
524 RW_TAC bool_ss [ALT_ZERO, NUMERAL_DEF, BIT1, BIT2, iLOG2_def,
525 numeralTheory.iDUB]
526 \\ SIMP_TAC arith_ss []
527QED
528
529(* ------------------------------------------------------------------------- *)
530
531Theorem MOD_2EXP_EQ:
532 (!a b. MOD_2EXP_EQ 0 a b = T) /\
533 (!n a b.
534 MOD_2EXP_EQ (SUC n) a b <=>
535 (ODD a = ODD b) /\ MOD_2EXP_EQ n (DIV2 a) (DIV2 b)) /\
536 (!n a. MOD_2EXP_EQ n a a = T)
537Proof
538 SRW_TAC [] [MOD_2EXP_EQ_def, MOD_2EXP_def, GSYM BITS_ZERO3]
539 \\ Cases_on `n`
540 \\ FULL_SIMP_TAC std_ss [GSYM BITS_ZERO3, GSYM BIT0_ODD,
541 GSYM BIT_BITS_THM, BIT_DIV2, DIV2_def]
542 \\ EQ_TAC
543 \\ RW_TAC arith_ss []
544 \\ Cases_on `x`
545 \\ RW_TAC arith_ss []
546QED
547
548Theorem lem[local]:
549 !n. BITS n 0 (2 ** SUC n - 1) = 2 ** SUC n - 1
550Proof
551 STRIP_TAC
552 \\ MATCH_MP_TAC BITS_ZEROL
553 \\ SIMP_TAC std_ss [ZERO_LT_TWOEXP]
554QED
555
556Theorem MOD_2EXP_MAX:
557 (!a. MOD_2EXP_MAX 0 a = T) /\
558 (!n a. MOD_2EXP_MAX (SUC n) a <=> ODD a /\ MOD_2EXP_MAX n (DIV2 a))
559Proof
560 SRW_TAC [] [MOD_2EXP_MAX_def, MOD_2EXP_def, GSYM BITS_ZERO3]
561 \\ Cases_on `n`
562 >- SIMP_TAC std_ss [SYM BIT0_ODD, BIT_def]
563 \\ ONCE_REWRITE_TAC [GSYM lem]
564 \\ SIMP_TAC std_ss
565 [GSYM BITS_ZERO3, SYM BIT0_ODD, GSYM BIT_BITS_THM, BIT_DIV2, DIV2_def]
566 \\ EQ_TAC
567 \\ RW_TAC arith_ss [BIT_EXP_SUB1]
568 \\ Cases_on `x`
569 \\ RW_TAC arith_ss []
570QED
571
572(* ------------------------------------------------------------------------- *)
573
574val LEAST_BIT_INTRO =
575 (SIMP_RULE (srw_ss()) [] o Q.SPEC `\i. BIT i n`) WhileTheory.LEAST_INTRO
576
577Theorem LOWEST_SET_BIT:
578 !n. n <> 0 ==>
579 (LOWEST_SET_BIT n = if ODD n then 0 else 1 + LOWEST_SET_BIT (DIV2 n))
580Proof
581 SRW_TAC [ARITH_ss] [LOWEST_SET_BIT_def, DIV2_def, ADD1]
582 \\ MATCH_MP_TAC LEAST_THM
583 \\ SRW_TAC [] [BIT0_ODD]
584 >| [
585 Cases_on `(LEAST i. BIT i (n DIV 2)) = 0`
586 >- FULL_SIMP_TAC (srw_ss()) [DECIDE ``m < 1 ==> (m = 0)``, BIT0_ODD]
587 \\ IMP_RES_TAC (DECIDE ``~(a = 0) /\ m < a + 1 ==> (m - 1 < a)``)
588 \\ IMP_RES_TAC WhileTheory.LESS_LEAST
589 \\ FULL_SIMP_TAC (srw_ss()) [BIT_DIV2]
590 \\ Cases_on `m = 0`
591 \\ FULL_SIMP_TAC (srw_ss())
592 [BIT0_ODD, DECIDE ``~(m = 0) ==> (SUC (m - 1) = m)``],
593 SRW_TAC [] [GSYM ADD1, GSYM BIT_DIV2]
594 \\ MATCH_MP_TAC LEAST_BIT_INTRO
595 \\ `~(n DIV 2 = 0)`
596 by (Cases_on `n = 1`
597 \\ FULL_SIMP_TAC arith_ss
598 [(SIMP_RULE (srw_ss()) [DECIDE ``0 < n <=> n <> 0``] o
599 Q.SPECL [`0`,`n`,`2`]) X_LT_DIV])
600 \\ METIS_TAC [BIT_LOG2]
601 ]
602QED
603
604Theorem LOWEST_SET_BIT_compute = (
605 let
606 open numeralTheory
607 val rule = (GEN_ALL o SIMP_RULE (srw_ss())
608 [DECIDE ``1 + n = SUC n``, numeral_eq, numeral_distrib,
609 numeral_evenodd, numeral_div2])
610 in
611 CONJ ((rule o Q.SPEC `NUMERAL (BIT2 n)`) LOWEST_SET_BIT)
612 ((rule o Q.SPEC `NUMERAL (BIT1 n)`) LOWEST_SET_BIT)
613 end)
614
615(* ------------------------------------------------------------------------- *)
616
617val () =
618 List.app (fn s => remove_ovl_mapping s {Name = s, Thy = "numeral_bit"})
619 ["iBITWISE", "iSUC", "iDIV2", "iLOG2", "iMOD_2EXP"]