bitScript.sml
1(* ========================================================================= *)
2(* FILE : bitScript.sml *)
3(* DESCRIPTION : Support for bitwise operations over the natural numbers. *)
4(* AUTHOR : (c) Anthony Fox, University of Cambridge *)
5(* DATE : 2000-2005 *)
6(* ========================================================================= *)
7Theory bit[bare]
8Ancestors
9 arithmetic logroot
10Libs
11 HolKernel Parse boolLib BasicProvers metisLib simpLib numSimps
12 numLib
13
14
15(* ------------------------------------------------------------------------- *)
16
17val LEFT_REWRITE_TAC =
18 GEN_REWRITE_TAC (RATOR_CONV o DEPTH_CONV) empty_rewrites
19
20val POP_LAST_TAC = POP_ASSUM (K ALL_TAC)
21
22(* ------------------------------------------------------------------------- *)
23
24Definition MOD_2EXP_def[nocompute]: MOD_2EXP x n = n MOD 2 ** x
25End
26
27Definition DIV_2EXP_def[nocompute]: DIV_2EXP x n = n DIV 2 ** x
28End
29
30Definition TIMES_2EXP_def[nocompute]: TIMES_2EXP x n = n * 2 ** x
31End
32
33Definition DIVMOD_2EXP_def[nocompute]:
34 DIVMOD_2EXP x n = (n DIV 2 ** x,n MOD 2 ** x)
35End
36
37Definition SBIT_def[nocompute]: SBIT b n = if b then 2 ** n else 0
38End
39
40Definition BITS_def[nocompute]:
41 BITS h l n = MOD_2EXP (SUC h - l) (DIV_2EXP l n)
42End
43
44Definition BITV_def[nocompute]: BITV n b = BITS b b n
45End
46
47Definition BIT_def[nocompute]: BIT b n = (BITS b b n = 1)
48End
49
50Definition SLICE_def[nocompute]:
51 SLICE h l n = MOD_2EXP (SUC h) n - MOD_2EXP l n
52End
53
54Definition LOG2_def[nocompute]: LOG2 = LOG 2
55End
56
57Definition LOWEST_SET_BIT_def[nocompute]: LOWEST_SET_BIT n = LEAST i. BIT i n
58End
59
60Definition BIT_REVERSE_def[nocompute]:
61 (BIT_REVERSE 0 x = 0) /\
62 (BIT_REVERSE (SUC n) x = (BIT_REVERSE n x) * 2 + SBIT (BIT n x) 0)
63End
64
65Definition BITWISE_def[nocompute]:
66 (BITWISE 0 op x y = 0) /\
67 (BITWISE (SUC n) op x y =
68 BITWISE n op x y + SBIT (op (BIT n x) (BIT n y)) n)
69End
70
71Definition BIT_MODIFY_def[nocompute]:
72 (BIT_MODIFY 0 f x = 0) /\
73 (BIT_MODIFY (SUC n) f x = BIT_MODIFY n f x + SBIT (f n (BIT n x)) n)
74End
75
76Definition SIGN_EXTEND_def[nocompute]:
77 SIGN_EXTEND l h n =
78 let m = n MOD 2 ** l in
79 if BIT (l - 1) n then 2 ** h - 2 ** l + m else m
80End
81
82Definition MOD_2EXP_EQ_def[nocompute]:
83 MOD_2EXP_EQ n a b = (MOD_2EXP n a = MOD_2EXP n b)
84End
85
86Definition MOD_2EXP_MAX_def[nocompute]:
87 MOD_2EXP_MAX n a = (MOD_2EXP n a = (2 ** n - 1))
88End
89
90(* ------------------------------------------------------------------------- *)
91
92(* This is the original definition of BIT mentioned in HOL Description *)
93Theorem BIT_DEF :
94 !b n. BIT b n = ((n DIV 2 ** b) MOD 2 = 1)
95Proof
96 SRW_TAC [ARITH_ss] [BIT_def, BITS_def, MOD_2EXP_def, DIV_2EXP_def]
97QED
98
99Theorem LESS_MULT_MONO2:
100 !a b x y:num. a < x /\ b < y ==> a * b < x * y
101Proof
102 REPEAT STRIP_TAC
103 \\ IMP_RES_TAC LESS_ADD_1
104 \\ SRW_TAC [ARITH_ss] []
105QED
106
107(* |- !n p. 2 ** p <= n /\ n < 2 ** SUC p ==> (LOG2 n = p) *)
108Theorem LOG2_UNIQUE =
109 (REWRITE_RULE [GSYM LOG2_def] o Q.SPEC `2`) LOG_UNIQUE
110
111Theorem LOG2_TWOEXP:
112 !n. LOG2 (2 ** n) = n
113Proof
114 STRIP_TAC
115 \\ MATCH_MP_TAC LOG2_UNIQUE
116 \\ SRW_TAC [] []
117QED
118
119(* |- !x n. DIVMOD_2EXP x n = (DIV_2EXP x n,MOD_2EXP x n) *)
120Theorem DIVMOD_2EXP =
121 REWRITE_RULE [GSYM DIV_2EXP_def, GSYM MOD_2EXP_def] DIVMOD_2EXP_def
122
123(* |- !a. SUC a - a = 1 *)
124Theorem SUC_SUB = arithmeticTheory.SUC_SUB;
125
126(* |- !n r. r < n ==> ((n + r) DIV n = 1) *)
127Theorem DIV_MULT_1 =
128 (GEN_ALL o SIMP_RULE arith_ss [] o Q.INST [`q` |-> `1`] o SPEC_ALL
129 o CONV_RULE (ONCE_DEPTH_CONV RIGHT_IMP_FORALL_CONV)) DIV_MULT
130
131(* |- !m. ~(m = 0) ==> ?p. m = SUC p *)
132Theorem NOT_ZERO_ADD1 =
133 (GEN_ALL o REWRITE_RULE [GSYM NOT_ZERO_LT_ZERO, GSYM ADD1, ADD] o
134 Q.SPECL [`m`, `0`]) LESS_ADD_1
135
136(* |- !n. 0 < 2 ** n *)
137Theorem ZERO_LT_TWOEXP[simp] =
138 GEN_ALL (numLib.REDUCE_RULE (Q.SPECL [`n`, `1`] ZERO_LESS_EXP))
139
140Theorem ONE_LE_TWOEXP[simp]:
141 !n. 1n <= 2 ** n
142Proof SRW_TAC [] [DECIDE ``1n <= x <=> 0 < x``]
143QED
144
145(* |- !n. 2 ** n <> 0 *)
146Theorem TWOEXP_NOT_ZERO = REWRITE_RULE [GSYM NOT_ZERO_LT_ZERO] ZERO_LT_TWOEXP
147
148local
149 val th =
150 (SPEC_ALL o REWRITE_RULE [ZERO_LT_TWOEXP] o Q.SPEC `2 ** n`) DIVISION
151in
152(* |- !n k. k MOD 2 ** n < 2 ** n *)
153Theorem MOD_2EXP_LT = (GEN_ALL o CONJUNCT2) th
154
155(* |- !n k. k = k DIV 2 ** n * 2 ** n + k MOD 2 ** n *)
156Theorem TWOEXP_DIVISION = (GEN_ALL o CONJUNCT1) th;
157end
158
159Theorem TWOEXP_MONO:
160 !a b. a < b ==> 2 ** a < 2 ** b
161Proof
162 SRW_TAC [] []
163QED
164
165Theorem TWOEXP_MONO2:
166 !a b. a <= b ==> 2 ** a <= 2 ** b
167Proof
168 SRW_TAC [] []
169QED
170
171Theorem EXP_SUB_LESS_EQ:
172 !a b. 2 ** (a - b) <= 2 ** a
173Proof
174 RW_TAC bool_ss [SUB_LESS_EQ, TWOEXP_MONO2]
175QED
176
177Theorem MOD_LEQ:
178 !a b. 0 < b ==> a MOD b <= a
179Proof
180 REPEAT STRIP_TAC
181 \\ IMP_RES_TAC DIVISION
182 \\ POP_ASSUM (K ALL_TAC)
183 \\ POP_ASSUM (Q.SPEC_THEN `a` SUBST1_TAC)
184 \\ SRW_TAC [] [MOD_TIMES]
185QED
186
187(* ------------------------------------------------------------------------- *)
188
189Theorem BITS_THM =
190 REWRITE_RULE [DIV_2EXP_def, MOD_2EXP_def] BITS_def
191
192Theorem BITSLT_THM:
193 !h l n. BITS h l n < 2 ** (SUC h-l)
194Proof
195 RW_TAC bool_ss [BITS_THM, ZERO_LT_TWOEXP, DIVISION]
196QED
197
198Theorem BITSLT_THM2:
199 !h l n. BITS h l n < 2 ** SUC h
200Proof
201 REPEAT STRIP_TAC
202 \\ `BITS h l n < 2 ** (SUC h - l)` by REWRITE_TAC [BITSLT_THM]
203 \\ METIS_TAC [EXP_SUB_LESS_EQ, LESS_LESS_EQ_TRANS]
204QED
205
206Theorem DIV_MULT_LEM[local]:
207 !m n. 0 < n ==> m DIV n * n <= m
208Proof
209 RW_TAC std_ss [LESS_EQ_EXISTS]
210 \\ Q.EXISTS_TAC `m MOD n`
211 \\ RW_TAC std_ss [GSYM DIVISION]
212QED
213
214(* |- !x n. n DIV 2 ** x * 2 ** x <= n *)
215val DIV_MULT_LESS_EQ =
216 DIV_MULT_LEM |> Q.SPECL [`n`, `2 ** x`]
217 |> SIMP_RULE bool_ss [ZERO_LT_TWOEXP]
218 |> GEN_ALL
219
220Theorem MOD_2EXP_LEM[local]:
221 !n x. n MOD 2 ** x = n - n DIV 2 ** x * 2 ** x
222Proof
223 RW_TAC arith_ss
224 [DIV_MULT_LESS_EQ, GSYM ADD_EQ_SUB, ZERO_LT_TWOEXP, GSYM DIVISION]
225QED
226
227Theorem DIV_MULT_LEM2[local]:
228 !a b p. a DIV 2 ** (b + p) * 2 ** (p + b) <= a DIV 2 ** b * 2 ** b
229Proof
230 RW_TAC bool_ss
231 [Q.SPECL [`a DIV 2 ** b`, `2 ** p`] DIV_MULT_LEM, EXP_ADD, MULT_ASSOC,
232 GSYM DIV_DIV_DIV_MULT, ZERO_LT_TWOEXP, LESS_MONO_MULT]
233QED
234
235Theorem MOD_EXP_ADD[local]:
236 !a b p.
237 a MOD 2 ** (b + p) = a MOD 2 ** b + (a DIV 2 ** b) MOD 2 ** p * 2 ** b
238Proof
239 REPEAT STRIP_TAC
240 \\ SIMP_TAC bool_ss [MOD_2EXP_LEM, RIGHT_SUB_DISTRIB, DIV_DIV_DIV_MULT,
241 ZERO_LT_TWOEXP, GSYM MULT_ASSOC, GSYM EXP_ADD]
242 \\ ASM_SIMP_TAC arith_ss
243 [DIV_MULT_LEM2, DIV_MULT_LEM, ZERO_LT_TWOEXP, SUB_ADD,
244 (GSYM o Q.SPECL [`a DIV 2 ** (b + p) * 2 ** (p + b)`,
245 `a DIV 2 ** b * 2 ** b`]) LESS_EQ_ADD_SUB]
246QED
247
248val DIV_MOD_MOD_DIV2 =
249 (SIMP_RULE std_ss [ZERO_LT_TWOEXP, GSYM EXP_ADD] o
250 Q.SPECL [`a`, `2 ** b`, `2 ** p`]) DIV_MOD_MOD_DIV
251
252Theorem DIV_MOD_MOD_DIV3[local]:
253 !a b c. (a DIV 2 ** b) MOD 2 ** (c - b) = (a MOD 2 ** c) DIV 2 ** b
254Proof
255 REPEAT STRIP_TAC
256 \\ Cases_on `c <= b`
257 >| [
258 POP_ASSUM
259 (fn th => REWRITE_TAC [REWRITE_RULE [GSYM SUB_EQ_0] th, EXP, MOD_1]
260 \\ ASSUME_TAC (MATCH_MP TWOEXP_MONO2 th))
261 \\ ASSUME_TAC (Q.SPECL [`c`, `a`] MOD_2EXP_LT)
262 \\ IMP_RES_TAC LESS_LESS_EQ_TRANS
263 \\ ASM_SIMP_TAC bool_ss [LESS_DIV_EQ_ZERO],
264 RULE_ASSUM_TAC (REWRITE_RULE [NOT_LESS_EQUAL])
265 \\ IMP_RES_TAC LESS_ADD
266 \\ POP_ASSUM (fn th => SIMP_TAC arith_ss [SYM th, DIV_MOD_MOD_DIV2])
267 ]
268QED
269
270Theorem BITS_THM2:
271 !h l n. BITS h l n = (n MOD 2 ** SUC h) DIV 2 ** l
272Proof
273 RW_TAC bool_ss [BITS_THM, DIV_MOD_MOD_DIV3]
274QED
275
276Theorem BITS_LEQ:
277 !h l n. BITS h l n <= n
278Proof
279 SRW_TAC [numSimps.ARITH_ss] [BITS_THM2]
280 \\ `n MOD 2 ** SUC h DIV 2 ** l <= n MOD 2 ** SUC h`
281 by SRW_TAC [] [DIV_LESS_EQ, ZERO_LT_TWOEXP]
282 \\ `n MOD 2 ** SUC h <= n` by SRW_TAC [] [MOD_LEQ, ZERO_LT_TWOEXP]
283 \\ DECIDE_TAC
284QED
285
286Theorem BITS_COMP_LEM[local]:
287 !h1 l1 h2 l2 n.
288 h2 + l1 <= h1 ==>
289 (((n DIV 2 ** l1) MOD 2 ** (h1 - l1) DIV 2 ** l2) MOD 2 ** (h2 - l2) =
290 (n DIV 2 ** (l2 + l1)) MOD 2 ** ((h2 + l1) - (l2 + l1)))
291Proof
292 REPEAT STRIP_TAC
293 \\ REWRITE_TAC
294 [Q.SPECL [`(n DIV 2 ** l1) MOD 2 ** (h1 - l1)`, `l2`, `h2`]
295 DIV_MOD_MOD_DIV3]
296 \\ IMP_RES_TAC LESS_EQUAL_ADD
297 \\ POP_ASSUM
298 (fn t => SIMP_TAC arith_ss [EXP_ADD, MOD_MULT_MOD, ZERO_LT_TWOEXP, t])
299 \\ REWRITE_TAC [DIV_MOD_MOD_DIV2]
300 \\ SIMP_TAC arith_ss [DIV_DIV_DIV_MULT, ZERO_LT_TWOEXP, GSYM EXP_ADD]
301 \\ REWRITE_TAC
302 [SIMP_RULE arith_ss []
303 (Q.SPECL [`n`, `l1 + l2`, `h2 + l1`] DIV_MOD_MOD_DIV3)]
304QED
305
306Theorem BITS_COMP_THM:
307 !h1 l1 h2 l2 n.
308 h2 + l1 <= h1 ==> (BITS h2 l2 (BITS h1 l1 n) = BITS (h2+l1) (l2+l1) n)
309Proof
310 REPEAT STRIP_TAC
311 \\ IMP_RES_TAC LESS_EQ_MONO
312 \\ FULL_SIMP_TAC bool_ss [BITS_THM, GSYM ADD_CLAUSES, BITS_COMP_LEM]
313QED
314
315Theorem BITS_DIV_THM:
316 !h l x n. (BITS h l x) DIV 2 ** n = BITS h (l + n) x
317Proof
318 RW_TAC bool_ss [BITS_THM2, EXP_ADD, ZERO_LT_TWOEXP, DIV_DIV_DIV_MULT]
319QED
320
321Theorem BITS_LT_HIGH:
322 !h l n. n < 2 ** SUC h ==> (BITS h l n = n DIV 2 ** l)
323Proof
324 RW_TAC bool_ss [BITS_THM2, LESS_MOD]
325QED
326
327(* ------------------------------------------------------------------------- *)
328
329Theorem BITS_ZERO:
330 !h l n. h < l ==> (BITS h l n = 0)
331Proof
332 REPEAT STRIP_TAC
333 \\ IMP_RES_TAC LESS_ADD_1
334 \\ POP_ASSUM (fn th => REWRITE_TAC [th])
335 \\ ASSUME_TAC
336 ((REWRITE_RULE [EXP, SUB, SUB_EQUAL_0] o
337 ONCE_REWRITE_RULE [SUB_PLUS] o REWRITE_RULE [ADD1] o
338 Q.SPECL [`h`, `h + 1 + p`, `n`]) BITSLT_THM)
339 \\ FULL_SIMP_TAC arith_ss []
340QED
341
342Theorem BITS_ZERO2:
343 !h l. BITS h l 0 = 0
344Proof
345 RW_TAC bool_ss [BITS_THM2, ZERO_MOD, ZERO_DIV, ZERO_LT_TWOEXP]
346QED
347
348(* |- !h n. BITS h 0 n = n MOD 2 ** SUC h *)
349Theorem BITS_ZERO3 =
350 (GEN_ALL o SIMP_RULE bool_ss [CONJUNCT1 EXP, DIV_1] o
351 Q.SPECL [`h`, `0`]) BITS_THM2
352
353Theorem BITS_ZERO4:
354 !h l a. l <= h ==> (BITS h l (a * 2 ** l) = BITS (h - l) 0 a)
355Proof
356 RW_TAC arith_ss [BITS_THM, MULT_DIV, ZERO_LT_TWOEXP, SUB]
357QED
358
359Theorem BITS_ZEROL:
360 !h a. a < 2 ** SUC h ==> (BITS h 0 a = a)
361Proof
362 RW_TAC bool_ss [BITS_ZERO3, LESS_MOD]
363QED
364
365Theorem BITS_LOG2_ZERO_ID:
366 !n. 0 < n ==> (BITS (LOG2 n) 0 n = n)
367Proof
368 REPEAT STRIP_TAC
369 \\ MATCH_MP_TAC BITS_ZEROL
370 \\ SRW_TAC [] [logrootTheory.LOG, LOG2_def]
371QED
372
373Theorem BITS_LT_LOW:
374 !h l n. n < 2 ** l ==> (BITS h l n = 0)
375Proof
376 REPEAT STRIP_TAC
377 \\ Cases_on `h < l`
378 >- ASM_SIMP_TAC bool_ss [BITS_ZERO]
379 \\ `l < SUC h` by DECIDE_TAC
380 \\ IMP_RES_TAC TWOEXP_MONO
381 \\ `n < 2 ** SUC h` by DECIDE_TAC
382 \\ ASM_SIMP_TAC std_ss [BITS_LT_HIGH, LESS_DIV_EQ_ZERO]
383QED
384
385Theorem BIT_ZERO:
386 !b. ~BIT b 0
387Proof REWRITE_TAC [BIT_def, BITS_ZERO2, DECIDE ``~(0 = 1)``]
388QED
389
390Theorem BIT_B:
391 !b. BIT b (2 ** b)
392Proof
393 SIMP_TAC arith_ss [BIT_def, BITS_THM, DIVMOD_ID, ZERO_LT_TWOEXP, SUC_SUB]
394QED
395
396Theorem BIT_TWO_POW[simp]:
397 !n m. BIT n (2 ** m) = (m = n)
398Proof
399 REPEAT STRIP_TAC
400 \\ Cases_on `m = n` >- ASM_REWRITE_TAC [BIT_B]
401 \\ REWRITE_TAC [BIT_def, BITS_THM, SUC_SUB, EXP_1]
402 \\ IMP_RES_TAC (DECIDE ``!(a:num) b. ~(b = a) ==> (a < b) \/ (b < a)``)
403 >| [
404 IMP_RES_TAC LESS_ADD_1
405 \\ ASM_SIMP_TAC std_ss [ONCE_REWRITE_RULE [MULT_COMM] MULT_DIV,
406 EXP_ADD, MOD_EQ_0, ZERO_LT_TWOEXP],
407 IMP_RES_TAC TWOEXP_MONO
408 \\ ASM_SIMP_TAC std_ss [LESS_DIV_EQ_ZERO]
409 ]
410QED
411
412Theorem BIT_B_NEQ =
413 METIS_PROVE [BIT_TWO_POW] ``!a b. ~(a = b) ==> ~BIT a (2 ** b)``
414
415(* ------------------------------------------------------------------------- *)
416
417Theorem BITS_COMP_THM2:
418 !h1 l1 h2 l2 n.
419 BITS h2 l2 (BITS h1 l1 n) = BITS (MIN h1 (h2 + l1)) (l2 + l1) n
420Proof
421 RW_TAC bool_ss [MIN_DEF, REWRITE_RULE [GSYM NOT_LESS] BITS_COMP_THM]
422 \\ Cases_on `h2 = 0`
423 >- FULL_SIMP_TAC arith_ss [BITS_ZERO, BITS_ZERO2]
424 \\ RULE_ASSUM_TAC (REWRITE_RULE [NOT_ZERO_LT_ZERO])
425 \\ Cases_on `h1 < l1`
426 >- FULL_SIMP_TAC arith_ss [BITS_ZERO, BITS_ZERO2]
427 \\ RULE_ASSUM_TAC (ONCE_REWRITE_RULE [ADD_COMM])
428 \\ IMP_RES_TAC SUB_RIGHT_LESS
429 \\ POP_ASSUM
430 (fn t =>
431 ASSUME_TAC
432 (MATCH_MP TWOEXP_MONO (ONCE_REWRITE_RULE [GSYM LESS_MONO_EQ] t)))
433 \\ ASSUME_TAC (Q.SPECL [`h1`, `l1`, `n`] BITSLT_THM)
434 \\ Cases_on `h1 = l1`
435 >| [
436 FULL_SIMP_TAC bool_ss [SUC_SUB, SUB_EQUAL_0, SYM ONE]
437 \\ `BITS l1 l1 n < 2 ** SUC h2` by IMP_RES_TAC LESS_TRANS
438 \\ ASM_SIMP_TAC arith_ss [BITS_LT_HIGH, BITS_DIV_THM],
439 `~(h1 <= l1)` by DECIDE_TAC
440 \\ POP_ASSUM
441 (fn th => RULE_ASSUM_TAC (SIMP_RULE bool_ss [th, SUB_LEFT_SUC]))
442 \\ `BITS h1 l1 n < 2 ** SUC h2` by IMP_RES_TAC LESS_TRANS
443 \\ ASM_SIMP_TAC arith_ss [BITS_LT_HIGH, BITS_DIV_THM]
444 ]
445QED
446
447(* ------------------------------------------------------------------------- *)
448
449Theorem NOT_MOD2_LEM:
450 !n. ~(n MOD 2 = 0) = (n MOD 2 = 1)
451Proof RW_TAC arith_ss [MOD_2]
452QED
453
454Theorem NOT_MOD2_LEM2:
455 !n. ~(n MOD 2 = 1) = (n MOD 2 = 0)
456Proof RW_TAC bool_ss [GSYM NOT_MOD2_LEM]
457QED
458
459Theorem ODD_MOD2_LEM:
460 !n. ODD n = ((n MOD 2) = 1)
461Proof RW_TAC arith_ss [ODD_EVEN, MOD_2]
462QED
463
464Theorem ODD_MOD_2[simp]:
465 ODD (x MOD 2) = ODD x
466Proof
467 RW_TAC arith_ss [ODD_MOD2_LEM]
468QED
469
470(* ------------------------------------------------------------------------- *)
471
472Theorem DIV_MULT_THM:
473 !x n. n DIV 2 ** x * 2 ** x = n - n MOD 2 ** x
474Proof
475 RW_TAC arith_ss [DIV_MULT_LESS_EQ, MOD_2EXP_LEM, SUB_SUB]
476QED
477
478(* |- !n. 2 * (n DIV 2) = n - n MOD 2 *)
479Theorem DIV_MULT_THM2 =
480 ONCE_REWRITE_RULE [MULT_COMM]
481 (REWRITE_RULE [EXP_1] (Q.SPEC `1` DIV_MULT_THM))
482
483Theorem LESS_EQ_EXP_MULT:
484 !a b. a <= b ==> ?p. 2 ** b = p * 2 ** a
485Proof
486 REPEAT STRIP_TAC
487 \\ IMP_RES_TAC LESS_EQUAL_ADD
488 \\ Q.EXISTS_TAC `2 ** p`
489 \\ FULL_SIMP_TAC arith_ss [EXP_ADD]
490QED
491
492val LESS_EXP_MULT =
493 simpLib.SIMP_PROVE bool_ss [LESS_IMP_LESS_OR_EQ, LESS_EQ_EXP_MULT]
494 ``!a b. a < b ==> ?p. 2 ** b = p * 2 ** a``
495
496(* ------------------------------------------------------------------------- *)
497
498Theorem SLICE_LEM1[local]:
499 !a x y. a DIV 2 ** (x + y) * 2 ** (x + y) =
500 a DIV 2 ** x * 2 ** x - (a DIV 2 ** x) MOD 2 ** y * 2 ** x
501Proof
502 REPEAT STRIP_TAC
503 \\ REWRITE_TAC [EXP_ADD]
504 \\ SUBST_OCCS_TAC [([2], Q.SPECL [`2 ** x`, `2 ** y`] MULT_COMM)]
505 \\ SIMP_TAC bool_ss
506 [ZERO_LT_TWOEXP, GSYM DIV_DIV_DIV_MULT, MULT_ASSOC,
507 Q.SPECL [`y`, `a DIV 2 ** x`] DIV_MULT_THM, RIGHT_SUB_DISTRIB]
508QED
509
510Theorem SLICE_LEM2[local]:
511 !a x y. n MOD 2 ** (x + y) =
512 n MOD 2 ** x + (n DIV 2 ** x) MOD 2 ** y * 2 ** x
513Proof
514 REPEAT STRIP_TAC
515 \\ SIMP_TAC bool_ss [DIV_MULT_LESS_EQ, MOD_2EXP_LEM, SLICE_LEM1,
516 RIGHT_SUB_DISTRIB, SUB_SUB, SUB_LESS_EQ]
517 \\ Cases_on `n = n DIV 2 ** x * 2 ** x`
518 >- POP_ASSUM (fn th => SIMP_TAC arith_ss [SYM th])
519 \\ ASSUME_TAC (REWRITE_RULE [GSYM NOT_LESS] DIV_MULT_LESS_EQ)
520 \\ IMP_RES_TAC LESS_CASES_IMP
521 \\ RW_TAC bool_ss [SUB_RIGHT_ADD]
522 \\ PROVE_TAC [GSYM NOT_LESS_EQUAL]
523QED
524
525Theorem SLICE_LEM3[local]:
526 !n h l. l < h ==> n MOD 2 ** SUC l <= n MOD 2 ** h
527Proof
528 REPEAT STRIP_TAC
529 \\ IMP_RES_TAC LESS_ADD_1
530 \\ POP_ASSUM (fn th => REWRITE_TAC [th])
531 \\ REWRITE_TAC [GSYM ADD1, GSYM ADD_SUC, GSYM (CONJUNCT2 ADD)]
532 \\ SIMP_TAC arith_ss [SLICE_LEM2]
533QED
534
535Theorem SLICE_THM:
536 !n h l. SLICE h l n = BITS h l n * 2 ** l
537Proof
538 REPEAT STRIP_TAC
539 \\ REWRITE_TAC [SLICE_def, BITS_def, MOD_2EXP_def, DIV_2EXP_def]
540 \\ Cases_on `h < l`
541 >| [
542 IMP_RES_TAC SLICE_LEM3
543 \\ POP_ASSUM (fn th => ASSUME_TAC (Q.SPEC `n` th))
544 \\ IMP_RES_TAC LESS_OR
545 \\ IMP_RES_TAC SUB_EQ_0
546 \\ ASM_SIMP_TAC arith_ss [EXP, MOD_1, MULT_CLAUSES],
547 REWRITE_TAC [DIV_MOD_MOD_DIV3]
548 \\ RULE_ASSUM_TAC (REWRITE_RULE [NOT_LESS])
549 \\ SUBST_OCCS_TAC
550 [([1], Q.SPECL [`l`, `n MOD 2 ** SUC h`] TWOEXP_DIVISION)]
551 \\ IMP_RES_TAC LESS_EQUAL_ADD
552 \\ POP_ASSUM (fn th => SUBST_OCCS_TAC [([2], th)])
553 \\ SIMP_TAC bool_ss
554 [ADD_SUC, ADD_SUB, MOD_MULT_MOD, ZERO_LT_TWOEXP, EXP_ADD]
555 ]
556QED
557
558Theorem SLICELT_THM:
559 !h l n. SLICE h l n < 2 ** SUC h
560Proof
561 REPEAT STRIP_TAC
562 \\ ASSUME_TAC (Q.SPECL [`SUC h`, `n`] MOD_2EXP_LT)
563 \\ RW_TAC arith_ss [SLICE_def, MOD_2EXP_def, ZERO_LT_TWOEXP, SUB_RIGHT_LESS]
564QED
565
566Theorem BITS_SLICE_THM:
567 !h l n. BITS h l (SLICE h l n) = BITS h l n
568Proof
569 RW_TAC bool_ss
570 [SLICELT_THM, BITS_LT_HIGH, ZERO_LT_TWOEXP, SLICE_THM, MULT_DIV]
571QED
572
573Theorem BITS_SLICE_THM2:
574 !h h2 l n. h <= h2 ==> (BITS h2 l (SLICE h l n) = BITS h l n)
575Proof
576 REPEAT STRIP_TAC
577 \\ LEFT_REWRITE_TAC [BITS_THM]
578 \\ SIMP_TAC bool_ss [SLICE_THM, ZERO_LT_TWOEXP, MULT_DIV]
579 \\ `SUC h - l <= SUC h2 - l` by DECIDE_TAC
580 \\ IMP_RES_TAC TWOEXP_MONO2
581 \\ POP_LAST_TAC
582 \\ ASSUME_TAC (Q.SPECL [`h`, `l`, `n`] BITSLT_THM)
583 \\ IMP_RES_TAC LESS_LESS_EQ_TRANS
584 \\ ASM_SIMP_TAC bool_ss [LESS_MOD]
585QED
586
587Theorem SLICE_ZERO_THM =
588 (GEN_ALL o REWRITE_RULE [MULT_RIGHT_1, EXP] o Q.SPECL [`n`, `h`, `0`])
589 SLICE_THM
590
591Theorem MOD_2EXP_MONO:
592 !n h l. l <= h ==> n MOD 2 ** l <= n MOD 2 ** SUC h
593Proof
594 REPEAT STRIP_TAC
595 \\ drule_then (Q.X_CHOOSE_THEN ‘p’ assume_tac) (iffLR LESS_EQ_EXISTS)
596 \\ ASM_SIMP_TAC arith_ss [SLICE_LEM2, SUC_ADD_SYM]
597QED
598
599Theorem SLICE_COMP_THM:
600 !h m l n.
601 (SUC m) <= h /\ l <= m ==>
602 (SLICE h (SUC m) n + SLICE m l n = SLICE h l n)
603Proof
604 RW_TAC bool_ss
605 [SLICE_def, MOD_2EXP_def, MOD_2EXP_MONO, GSYM LESS_EQ_ADD_SUB, SUB_ADD]
606QED
607
608Theorem SLICE_COMP_RWT:
609 !h m' m l n.
610 l <= m /\ (m' = m + 1) /\ m < h ==>
611 (SLICE h m' n + SLICE m l n = SLICE h l n)
612Proof
613 RW_TAC arith_ss [SLICE_COMP_THM, GSYM ADD1]
614QED
615
616Theorem SLICE_ZERO:
617 !h l n. h < l ==> (SLICE h l n = 0)
618Proof
619 RW_TAC arith_ss [SLICE_THM, BITS_ZERO]
620QED
621
622Theorem SLICE_ZERO2 =
623 GEN_ALL (SIMP_CONV std_ss [SLICE_THM, BITS_ZERO2] ``SLICE h l 0``)
624
625(* ------------------------------------------------------------------------- *)
626
627Theorem BITS_SUM:
628 !h l a b.
629 b < 2 ** l ==> (BITS h l (a * 2 ** l + b) = BITS h l (a * 2 ** l))
630Proof
631 RW_TAC bool_ss [BITS_THM, DIV_MULT, MULT_DIV, ZERO_LT_TWOEXP]
632QED
633
634Theorem BITS_SUM2:
635 !h l a b. BITS h l (a * 2 ** SUC h + b) = BITS h l b
636Proof
637 RW_TAC bool_ss [BITS_THM2, MOD_TIMES, ZERO_LT_TWOEXP]
638QED
639
640Theorem SLICE_TWOEXP[local]:
641 !h l a n. SLICE (h + n) (l + n) (a * 2 ** n) = (SLICE h l a) * 2 ** n
642Proof
643 REPEAT STRIP_TAC
644 \\ SUBST1_TAC (Q.SPECL [`l`, `n`] ADD_COMM)
645 \\ RW_TAC bool_ss [(GSYM o CONJUNCT2) ADD, SLICE_THM, BITS_THM, MULT_DIV,
646 EXP_ADD, GSYM DIV_DIV_DIV_MULT, ZERO_LT_TWOEXP]
647 \\ SIMP_TAC arith_ss []
648QED
649
650val SPEC_SLICE_TWOEXP =
651 (GEN_ALL o SIMP_RULE arith_ss [] o Q.DISCH `n <= l /\ n <= h` o
652 Q.SPECL [`h - n`, `l - n`, `a`, `n`]) SLICE_TWOEXP
653
654Theorem SLICE_COMP_THM2:
655 !h l x y n. h <= x /\ y <= l ==> (SLICE h l (SLICE x y n) = SLICE h l n)
656Proof
657 REPEAT STRIP_TAC
658 \\ Cases_on `h < l`
659 >- ASM_SIMP_TAC bool_ss [SLICE_ZERO]
660 \\ `y <= h` by DECIDE_TAC
661 \\ SUBST1_TAC (Q.SPECL [`n`, `x`, `y`] SLICE_THM)
662 \\ ASM_SIMP_TAC bool_ss [SPEC_SLICE_TWOEXP]
663 \\ ASM_SIMP_TAC arith_ss
664 [ONCE_REWRITE_RULE [MULT_COMM] SLICE_THM, BITS_COMP_THM2, MIN_DEF]
665 \\ ASM_SIMP_TAC arith_ss [GSYM EXP_ADD]
666QED
667
668Theorem BITS_SUM3:
669 !h a b. BITS h 0 (BITS h 0 a + BITS h 0 b) = BITS h 0 (a + b)
670Proof
671 SRW_TAC [] [BITS_ZERO3, ZERO_LT_TWOEXP, MOD_PLUS]
672QED
673
674Theorem BITS_MUL:
675 !h a b. BITS h 0 (BITS h 0 a * BITS h 0 b) = BITS h 0 (a * b)
676Proof
677 SRW_TAC [] [BITS_ZERO3, ZERO_LT_TWOEXP, MOD_TIMES2]
678QED
679
680(* ------------------------------------------------------------------------- *)
681
682Theorem lem[local]:
683 !c a b. (a = b) ==> (a DIV c = b DIV c)
684Proof RW_TAC arith_ss []
685QED
686
687Theorem lem2[local]:
688 !a b c. a * (b * c) = a * c * b
689Proof SIMP_TAC arith_ss []
690QED
691
692Theorem lem3[local]:
693 !a m n. n <= m ==> (a * 2 ** m DIV 2 ** n = a * 2 ** (m - n))
694Proof
695 REPEAT STRIP_TAC
696 \\ IMP_RES_TAC LESS_EQUAL_ADD
697 \\ ASM_SIMP_TAC std_ss [EXP_ADD, MULT_DIV, ZERO_LT_TWOEXP, lem2]
698QED
699
700(* |- !a m n. n < m ==> (a * 2 ** m DIV 2 ** n = a * 2 ** (m - n)) *)
701val lem4 =
702 simpLib.SIMP_PROVE std_ss [LESS_IMP_LESS_OR_EQ, lem3]
703 ``!a m n. n < m ==> (a * 2 ** m DIV 2 ** n = a * 2 ** (m - n))``
704
705Theorem BIT_COMP_THM3:
706 !h m l n.
707 SUC m <= h /\ l <= m ==>
708 (BITS h (SUC m) n * 2 ** (SUC m - l) + BITS m l n = BITS h l n)
709Proof
710 REPEAT STRIP_TAC
711 \\ IMP_RES_TAC (REWRITE_RULE [SLICE_THM] SLICE_COMP_THM)
712 \\ POP_LAST_TAC
713 \\ POP_ASSUM (fn th => th |> Q.SPEC `n`
714 |> MATCH_MP (Q.SPEC `2 ** l` lem)
715 |> Q.INST [`l'` |-> `l`]
716 |> ONCE_REWRITE_RULE [ADD_COMM]
717 |> ASSUME_TAC)
718 \\ `l < SUC m` by ASM_SIMP_TAC arith_ss []
719 \\ FULL_SIMP_TAC arith_ss [lem4, ADD_DIV_ADD_DIV, MULT_DIV, ZERO_LT_TWOEXP]
720QED
721
722(* ------------------------------------------------------------------------- *)
723
724Theorem NOT_BIT:
725 !n a. ~BIT n a = (BITS n n a = 0)
726Proof
727 RW_TAC bool_ss [BIT_def, BITS_THM, SUC_SUB, EXP_1, GSYM NOT_MOD2_LEM]
728QED
729
730Theorem NOT_BITS:
731 !n a. ~(BITS n n a = 0) = (BITS n n a = 1)
732Proof
733 RW_TAC bool_ss [GSYM NOT_BIT, GSYM BIT_def]
734QED
735
736Theorem NOT_BITS2:
737 !n a. ~(BITS n n a = 1) = (BITS n n a = 0)
738Proof
739 RW_TAC bool_ss [GSYM NOT_BITS]
740QED
741
742Theorem BIT_SLICE:
743 !n a b. (BIT n a = BIT n b) = (SLICE n n a = SLICE n n b)
744Proof
745 REPEAT STRIP_TAC
746 \\ EQ_TAC
747 >- (Cases_on `BIT n a`
748 \\ FULL_SIMP_TAC arith_ss [BIT_def, SLICE_THM, NOT_BITS2])
749 \\ Cases_on `BITS n n a = 1`
750 \\ Cases_on `BITS n n b = 1`
751 \\ FULL_SIMP_TAC arith_ss
752 [BIT_def, SLICE_THM, NOT_BITS2, MULT_CLAUSES,
753 REWRITE_RULE [GSYM NOT_ZERO_LT_ZERO] ZERO_LT_TWOEXP]
754QED
755
756Theorem BIT_SLICE_LEM:
757 !y x n. SBIT (BIT x n) (x + y) = (SLICE x x n) * 2 ** y
758Proof
759 RW_TAC arith_ss [SBIT_def, BIT_SLICE, SLICE_THM, BIT_def, EXP_ADD]
760 \\ FULL_SIMP_TAC bool_ss [GSYM NOT_BITS]
761QED
762
763(* |- !x n. SBIT (BIT x n) x = SLICE x x n *)
764Theorem BIT_SLICE_THM =
765 SIMP_RULE arith_ss [EXP] (Q.SPEC `0` BIT_SLICE_LEM)
766
767Theorem BIT_SLICE_THM2:
768 !b n. BIT b n = (SLICE b b n = 2 ** b)
769Proof
770 RW_TAC bool_ss [SBIT_def, GSYM BIT_SLICE_THM, TWOEXP_NOT_ZERO]
771QED
772
773Theorem BIT_SLICE_THM3:
774 !b n. ~BIT b n = (SLICE b b n = 0)
775Proof
776 RW_TAC bool_ss [SBIT_def, GSYM BIT_SLICE_THM, TWOEXP_NOT_ZERO]
777QED
778
779Theorem BIT_SLICE_THM4:
780 !b h l n. BIT b (SLICE h l n) <=> l <= b /\ b <= h /\ BIT b n
781Proof
782 REPEAT STRIP_TAC
783 \\ Cases_on `l <= b /\ b <= h`
784 \\ RW_TAC arith_ss [BIT_SLICE_THM2, SLICE_COMP_THM2]
785 \\ REWRITE_TAC [GSYM BIT_SLICE_THM2]
786 \\ FULL_SIMP_TAC arith_ss
787 [SLICE_THM, BIT_def, NOT_LESS_EQUAL, Q.SPECL [`b`, `b`] BITS_THM,
788 SUC_SUB, NOT_MOD2_LEM2]
789 >| [
790 IMP_RES_TAC LESS_ADD_1
791 \\ ASM_SIMP_TAC arith_ss [ONCE_REWRITE_RULE [ADD_COMM] EXP_ADD]
792 \\ SIMP_TAC std_ss
793 [MULT_DIV, ZERO_LT_TWOEXP, DECIDE ``a * (b * c) = (a * c) * b``]
794 \\ METIS_TAC [MOD_EQ_0, DECIDE ``0 < 2``, MULT_ASSOC, MULT_COMM],
795 `SUC h <= b` by DECIDE_TAC
796 \\ `2 ** l * BITS h l n < 2 ** b`
797 by METIS_TAC [TWOEXP_MONO2, GSYM SLICE_THM, SLICELT_THM,
798 LESS_LESS_EQ_TRANS, MULT_COMM]
799 \\ ASM_SIMP_TAC std_ss [LESS_DIV_EQ_ZERO]
800 ]
801QED
802
803Theorem SUB_BITS[local]:
804 !h l a b.
805 (BITS (SUC h) l a = BITS (SUC h) l b) ==> (BITS h l a = BITS h l b)
806Proof
807 REPEAT STRIP_TAC
808 \\ Cases_on `h < l`
809 >- RW_TAC bool_ss [BITS_ZERO]
810 \\ RULE_ASSUM_TAC (REWRITE_RULE [NOT_LESS])
811 \\ POP_ASSUM
812 (fn th => ONCE_REWRITE_TAC
813 [(GSYM o SIMP_RULE arith_ss [th, SUB_ADD] o
814 Q.SPECL [`SUC h`, `l`, `h - l`, `0`]) BITS_COMP_THM])
815 \\ ASM_REWRITE_TAC []
816QED
817
818Theorem SBIT_DIV:
819 !b m n. n < m ==> (SBIT b (m - n) = SBIT b m DIV 2 ** n)
820Proof
821 RW_TAC bool_ss [SBIT_def, ZERO_DIV, ZERO_LT_TWOEXP,
822 SIMP_RULE arith_ss [] (Q.SPEC `1` lem4)]
823QED
824
825Theorem BITS_SUC:
826 !h l n.
827 l <= SUC h ==>
828 (SBIT (BIT (SUC h) n) (SUC h - l) + BITS h l n = BITS (SUC h) l n)
829Proof
830 REPEAT STRIP_TAC
831 \\ Cases_on `l = SUC h`
832 >| [
833 RW_TAC arith_ss [EXP, BITS_ZERO, SBIT_def, BIT_def]
834 \\ FULL_SIMP_TAC bool_ss [NOT_BITS2],
835 `l <= h` by ASM_SIMP_TAC arith_ss []
836 \\ IMP_RES_TAC LESS_EQ_IMP_LESS_SUC
837 \\ ASM_SIMP_TAC arith_ss
838 [SBIT_DIV, BIT_SLICE_THM, SLICE_THM,
839 ONCE_REWRITE_RULE [MULT_COMM] lem4,
840 (ONCE_REWRITE_RULE [MULT_COMM] o Q.SPECL [`SUC h`, `h`])
841 BIT_COMP_THM3]]
842QED
843
844Theorem BITS_SUC_THM:
845 !h l n.
846 BITS (SUC h) l n =
847 if SUC h < l then 0 else SBIT (BIT (SUC h) n) (SUC h - l) + BITS h l n
848Proof
849 RW_TAC arith_ss [BITS_ZERO, BITS_SUC]
850QED
851
852Theorem DECEND_LEMMA[local]:
853 !P l y.
854 (!x. l <= x /\ x <= SUC y ==> P x) ==> (!x. l <= x /\ x <= y ==> P x)
855Proof
856 RW_TAC arith_ss []
857QED
858
859Theorem BIT_BITS_LEM[local]:
860 !h l a b. l <= h ==> (BITS h l a = BITS h l b) ==> (BIT h a = BIT h b)
861Proof
862 RW_TAC bool_ss [BIT_SLICE, SLICE_THM]
863 \\ Q.PAT_ASSUM `l <= h`
864 (fn th => ONCE_REWRITE_TAC
865 [(GSYM o SIMP_RULE arith_ss [th, SUB_ADD] o
866 Q.SPECL [`h`, `l`, `h - l`, `h - l`]) BITS_COMP_THM])
867 \\ ASM_REWRITE_TAC []
868QED
869
870Theorem BIT_BITS_THM:
871 !h l a b. (!x. l <= x /\ x <= h ==> (BIT x a = BIT x b)) =
872 (BITS h l a = BITS h l b)
873Proof
874 Induct_on `h`
875 \\ REPEAT STRIP_TAC
876 >- (Cases_on `l = 0`
877 \\ RW_TAC arith_ss [BIT_SLICE, SLICE_THM, EXP, Q.SPEC `0` BITS_ZERO,
878 NOT_ZERO_LT_ZERO])
879 \\ EQ_TAC
880 \\ REPEAT STRIP_TAC
881 >| [
882 RW_TAC bool_ss [BITS_SUC_THM]
883 \\ RULE_ASSUM_TAC (REWRITE_RULE [NOT_LESS])
884 \\ Q.PAT_ASSUM `!x. l <= x /\ x <= SUC h ==> (BIT x a = BIT x b)`
885 (fn th =>
886 ASM_SIMP_TAC bool_ss [SIMP_RULE arith_ss [] (Q.SPEC `SUC h` th)]
887 \\ ASSUME_TAC
888 (MATCH_MP ((BETA_RULE o
889 Q.SPECL [`\x. BIT x a = BIT x b`, `l`, `h`])
890 DECEND_LEMMA) th))
891 \\ FIRST_ASSUM (fn th => ASSUME_TAC (Q.SPECL [`l`, `a`, `b`] th))
892 \\ FULL_SIMP_TAC bool_ss [],
893 IMP_RES_TAC SUB_BITS
894 \\ FIRST_ASSUM
895 (fn th => RULE_ASSUM_TAC
896 (REWRITE_RULE [SYM (Q.SPECL [`l`, `a`, `b`] th)]))
897 \\ Cases_on `x <= h` \\ ASM_SIMP_TAC bool_ss []
898 \\ `x = SUC h` by ASM_SIMP_TAC arith_ss []
899 \\ Cases_on `l = SUC h`
900 >- FULL_SIMP_TAC bool_ss [BIT_def]
901 \\ `l <= SUC h` by ASM_SIMP_TAC arith_ss []
902 \\ POP_ASSUM (fn th => ASSUME_TAC (SIMP_RULE bool_ss [th]
903 (Q.SPECL [`SUC h`, `l`, `a`, `b`] BIT_BITS_LEM)))
904 \\ FULL_SIMP_TAC bool_ss []
905 ]
906QED
907
908Theorem BITS_ZERO5:
909 !n m. (!i. i <= n ==> ~BIT i m) ==> (BITS n 0 m = 0)
910Proof
911 REPEAT STRIP_TAC
912 \\ Q.SPECL_THEN [`n`, `0`]
913 (fn thm => CONV_TAC (RHS_CONV (REWR_CONV (SYM thm)))) BITS_ZERO2
914 \\ SRW_TAC [] [GSYM BIT_BITS_THM, BIT_ZERO]
915QED
916
917(* ------------------------------------------------------------------------- *)
918
919Theorem BIT0_ODD:
920 BIT 0 = ODD
921Proof
922 ONCE_REWRITE_TAC [FUN_EQ_THM]
923 \\ SIMP_TAC arith_ss [ODD_MOD2_LEM, BIT_def, BITS_THM2, EXP, DIV_1]
924QED
925
926Theorem BITV_THM:
927 !b n. BITV n b = SBIT (BIT b n) 0
928Proof
929 RW_TAC arith_ss [BITV_def, BIT_def, SBIT_def]
930 \\ FULL_SIMP_TAC bool_ss [NOT_BITS2]
931QED
932
933Theorem ADD_BIT0 = REWRITE_RULE [GSYM BIT0_ODD] ODD_ADD
934
935val BITS_DIVISION =
936 DIVISION |> Q.SPEC `2 ** SUC n`
937 |> SIMP_RULE std_ss [ZERO_LT_TWOEXP, GSYM BITS_ZERO3]
938 |> GEN_ALL
939
940val _ = diminish_srw_ss ["MOD"]
941Theorem ADD_BITS_SUC:
942 !n a b.
943 BITS (SUC n) (SUC n) (a + b) =
944 (BITS (SUC n) (SUC n) a + BITS (SUC n) (SUC n) b +
945 BITS (SUC n) (SUC n) (BITS n 0 a + BITS n 0 b)) MOD 2
946Proof
947 REPEAT STRIP_TAC
948 \\ Q.SPECL_THEN [`n`, `a`] ASSUME_TAC BITS_DIVISION
949 \\ POP_ASSUM (fn th => CONV_TAC (LHS_CONV (ONCE_REWRITE_CONV [th])))
950 \\ Q.SPECL_THEN [`n`, `b`] ASSUME_TAC BITS_DIVISION
951 \\ POP_ASSUM (fn th => CONV_TAC (LHS_CONV (ONCE_REWRITE_CONV [th])))
952 \\ SRW_TAC [] [BITS_THM, SUC_SUB]
953 \\ Cases_on `(a DIV 2 ** SUC n) MOD 2 = 1`
954 \\ Cases_on `(b DIV 2 ** SUC n) MOD 2 = 1`
955 \\ FULL_SIMP_TAC arith_ss [NOT_MOD2_LEM2, ADD_MODULUS]
956 \\ REWRITE_TAC [DECIDE ``a * n + (b * n + c) = (a + b) * n + c:num``]
957 \\ SIMP_TAC std_ss [ADD_DIV_ADD_DIV, ZERO_LT_TWOEXP]
958 \\ CONV_TAC
959 (LHS_CONV (SIMP_CONV std_ss [Once (GSYM MOD_PLUS), ZERO_LT_TWOEXP]))
960 \\ CONV_TAC (LHS_CONV (RATOR_CONV
961 (SIMP_CONV std_ss [Once (GSYM MOD_PLUS), ZERO_LT_TWOEXP])))
962 \\ ASM_SIMP_TAC arith_ss []
963QED
964
965Theorem ADD_BIT_SUC:
966 !n a b.
967 BIT (SUC n) (a + b) =
968 if BIT (SUC n) (BITS n 0 a + BITS n 0 b) then
969 BIT (SUC n) a = BIT (SUC n) b
970 else
971 BIT (SUC n) a <> BIT (SUC n) b
972Proof
973 SRW_TAC [] [BIT_def]
974 \\ CONV_TAC (LHS_CONV (SIMP_CONV std_ss [Once ADD_BITS_SUC]))
975 \\ Cases_on `BITS (SUC n) (SUC n) a = 1`
976 \\ Cases_on `BITS (SUC n) (SUC n) b = 1`
977 \\ FULL_SIMP_TAC std_ss [NOT_BITS2]
978QED
979
980(* ------------------------------------------------------------------------- *)
981
982Theorem BITWISE_LT_2EXP:
983 !n op a b. BITWISE n op a b < 2 ** n
984Proof
985 Induct_on `n`
986 \\ RW_TAC bool_ss [ADD_0, TIMES2, LESS_IMP_LESS_ADD, LESS_MONO_ADD,
987 BITWISE_def, SBIT_def, EXP]
988 \\ numLib.REDUCE_TAC
989QED
990
991Theorem LESS_EXP_MULT2[local]:
992 !a b. a < b ==> ?p. 2 ** b = 2 ** (p + 1) * 2 ** a
993Proof
994 REPEAT STRIP_TAC
995 \\ IMP_RES_TAC LESS_ADD_1
996 \\ Q.EXISTS_TAC `p`
997 \\ FULL_SIMP_TAC arith_ss [EXP_ADD]
998QED
999
1000Theorem BITWISE_LEM[local]:
1001 !n op a b. BIT n (BITWISE (SUC n) op a b) = op (BIT n a) (BIT n b)
1002Proof
1003 RW_TAC arith_ss [SBIT_def, BITWISE_def, NOT_BIT]
1004 >- SIMP_TAC arith_ss
1005 [BIT_def, BITS_THM, SUC_SUB,
1006 REWRITE_RULE [BITWISE_LT_2EXP]
1007 (Q.SPECL [`BITWISE n op a b`, `2 ** n`] DIV_MULT_1)]
1008 \\ SIMP_TAC arith_ss [BITS_THM, LESS_DIV_EQ_ZERO, BITWISE_LT_2EXP, SUC_SUB]
1009QED
1010
1011val TWO_SUC_SUB =
1012 GEN_ALL (SIMP_CONV bool_ss [SUC_SUB, EXP_1] ``2 ** (SUC x - x)``)
1013
1014Theorem BITWISE_THM:
1015 !x n op a b. x < n ==> (BIT x (BITWISE n op a b) = op (BIT x a) (BIT x b))
1016Proof
1017 Induct_on `n`
1018 \\ REPEAT STRIP_TAC
1019 >- FULL_SIMP_TAC arith_ss []
1020 \\ Cases_on `x = n`
1021 >- ASM_REWRITE_TAC [BITWISE_LEM]
1022 \\ `x < n` by ASM_SIMP_TAC arith_ss []
1023 \\ RW_TAC arith_ss [BITWISE_def, SBIT_def]
1024 \\ LEFT_REWRITE_TAC [BIT_def]
1025 \\ ASM_REWRITE_TAC [BITS_THM]
1026 \\ IMP_RES_TAC LESS_EXP_MULT2
1027 \\ POP_LAST_TAC
1028 \\ ASM_SIMP_TAC bool_ss [ZERO_LT_TWOEXP, ADD_DIV_ADD_DIV,
1029 TWO_SUC_SUB, GSYM ADD1, EXP, ONCE_REWRITE_RULE [MULT_COMM]
1030 (REWRITE_RULE [DECIDE (Term `0 < 2`)] (Q.SPEC `2` MOD_TIMES))]
1031 \\ SUBST_OCCS_TAC [([2], SYM (Q.SPEC `x` TWO_SUC_SUB))]
1032 \\ ASM_SIMP_TAC bool_ss [GSYM BITS_THM, GSYM BIT_def]
1033QED
1034
1035Theorem BITWISE_COR:
1036 !x n op a b. x < n ==> op (BIT x a) (BIT x b) ==>
1037 ((BITWISE n op a b DIV 2 ** x) MOD 2 = 1)
1038Proof
1039 NTAC 6 STRIP_TAC
1040 \\ IMP_RES_TAC BITWISE_THM
1041 \\ NTAC 2 (WEAKEN_TAC (K true))
1042 \\ POP_ASSUM (fn th => REWRITE_TAC [GSYM th])
1043 \\ ASM_REWRITE_TAC [BITS_THM, BIT_def, DIV_1, EXP_1, SUC_SUB]
1044QED
1045
1046Theorem BITWISE_NOT_COR:
1047 !x n op a b.
1048 x < n ==> ~op (BIT x a) (BIT x b) ==>
1049 ((BITWISE n op a b DIV 2 ** x) MOD 2 = 0)
1050Proof
1051 NTAC 6 STRIP_TAC
1052 \\ IMP_RES_TAC BITWISE_THM
1053 \\ NTAC 2 (WEAKEN_TAC (K true))
1054 \\ POP_ASSUM (fn th => REWRITE_TAC [GSYM th])
1055 \\ ASM_REWRITE_TAC
1056 [BITS_THM, BIT_def, GSYM NOT_MOD2_LEM, DIV_1, EXP_1, SUC_SUB]
1057QED
1058
1059Theorem BITWISE_BITS:
1060 !wl op a b.
1061 BITWISE (SUC wl) op (BITS wl 0 a) (BITS wl 0 b) = BITWISE (SUC wl) op a b
1062Proof
1063 Induct
1064 \\ FULL_SIMP_TAC arith_ss [BITWISE_def, BIT_def, BITS_COMP_THM2, MIN_DEF]
1065 \\ POP_ASSUM (fn th => ONCE_REWRITE_TAC [GSYM th])
1066 \\ SIMP_TAC arith_ss [BITS_COMP_THM2, MIN_DEF]
1067QED
1068
1069(* ------------------------------------------------------------------------- *)
1070
1071Theorem NOT_BIT_GT_TWOEXP:
1072 !i n. n < 2 ** i ==> ~BIT i n
1073Proof
1074 SRW_TAC [ARITH_ss] [BIT_def, BITS_THM, LESS_DIV_EQ_ZERO]
1075QED
1076
1077Theorem BIT_IMP_GE_TWOEXP:
1078 !i n. BIT i n ==> 2 ** i <= n
1079Proof
1080 METIS_TAC [NOT_BIT_GT_TWOEXP, NOT_LESS_EQUAL]
1081QED
1082
1083Theorem BITS_SUC2[local]:
1084 !n a. BITS (SUC n) 0 a = SLICE (SUC n) (SUC n) a + BITS n 0 a
1085Proof
1086 RW_TAC arith_ss [GSYM SLICE_ZERO_THM, SLICE_COMP_THM]
1087QED
1088
1089Theorem lem[local]:
1090 !n a. a < 2 ** SUC n ==> ~(2 ** SUC n < a + 1)
1091Proof
1092 RW_TAC arith_ss [NOT_LESS, EXP]
1093QED
1094
1095val lem2 =
1096 MATCH_MP lem (REWRITE_RULE [SUB_0] (Q.SPECL [`n`, `0`, `a`] BITSLT_THM))
1097
1098Theorem BITWISE_ONE_COMP_LEM:
1099 !n a b. BITWISE (SUC n) (\x y. ~x) a b = 2 ** (SUC n) - 1 - BITS n 0 a
1100Proof
1101 Induct_on `n`
1102 \\ REPEAT STRIP_TAC
1103 >- RW_TAC arith_ss [SBIT_def, BIT_def, BITWISE_def, NOT_BITS2]
1104 \\ RW_TAC arith_ss
1105 [BITWISE_def, SBIT_def, REWRITE_RULE [SLICE_THM] BITS_SUC2]
1106 \\ RULE_ASSUM_TAC (SIMP_RULE bool_ss [NOT_BIT, NOT_BITS, BIT_def])
1107 \\ ASM_SIMP_TAC arith_ss [MULT_CLAUSES]
1108 >| [
1109 Cases_on `2 ** SUC n = BITS n 0 a + 1`
1110 >- ASM_SIMP_TAC arith_ss [SUB_RIGHT_ADD, EXP]
1111 \\ ASSUME_TAC lem2
1112 \\ `~(2 ** SUC n <= BITS n 0 a + 1)` by ASM_SIMP_TAC arith_ss []
1113 \\ ASM_SIMP_TAC arith_ss [SUB_RIGHT_ADD, EXP],
1114 REWRITE_TAC
1115 [REWRITE_CONV [ADD_SUB, TIMES2] (Term`2 * a - a`), SUB_PLUS, EXP]
1116 ]
1117QED
1118
1119Theorem ONE_COMP[local]:
1120 !i n a b.
1121 i < SUC n ==> (~BIT i a = BIT i (BITWISE (SUC n) (\x y. ~x) a b))
1122Proof
1123 SRW_TAC [] [BITWISE_THM]
1124QED
1125
1126Theorem BIT_COMPLEMENT_LEM[local]:
1127 !n i a. i < n /\ a MOD 2 ** n <> 0 ==>
1128 (BIT i (2 ** n - a MOD 2 ** n) = ~BIT i (a MOD 2 ** n - 1))
1129Proof
1130 Cases
1131 \\ SRW_TAC [] []
1132 \\ `~BIT i (a MOD 2 ** SUC n' - 1) =
1133 BIT i (BITWISE (SUC n') (\x y. ~x) (a MOD 2 ** SUC n' - 1) 0)`
1134 by METIS_TAC [ONE_COMP]
1135 \\ POP_ASSUM SUBST1_TAC
1136 \\ `a MOD 2 ** SUC n' - 1 < 2 ** SUC n'`
1137 by SRW_TAC [ARITH_ss] [MOD_2EXP_LT, DECIDE ``a < b ==> a < b + 1n``]
1138 \\ ASM_SIMP_TAC std_ss
1139 [BITWISE_ONE_COMP_LEM, BITS_ZEROL,
1140 DECIDE ``b <> 0 ==> (a - 1 - (b - 1n) = a - b)``]
1141QED
1142
1143Theorem BIT_COMPLEMENT:
1144 !n i a.
1145 (BIT i (2 ** n - a MOD 2 ** n) =
1146 ((a MOD 2 ** n = 0) /\ (i = n) \/
1147 (a MOD 2 ** n <> 0) /\ (i < n) /\ ~BIT i (a MOD 2 ** n - 1)))
1148Proof
1149 REPEAT STRIP_TAC
1150 \\ Cases_on `a MOD 2 ** n = 0`
1151 \\ ASM_SIMP_TAC std_ss []
1152 >| [
1153 Cases_on `i = n`
1154 \\ SRW_TAC [] [BIT_B_NEQ, BIT_B],
1155 Cases_on `i < n`
1156 \\ FULL_SIMP_TAC std_ss []
1157 >| [
1158 ASM_SIMP_TAC std_ss [BIT_COMPLEMENT_LEM],
1159 `2n ** n <= 2 ** i` by METIS_TAC [NOT_LESS, TWOEXP_MONO2]
1160 \\ `2n ** n - a MOD 2 ** n < 2 ** n`
1161 by SRW_TAC [ARITH_ss] [ZERO_LT_TWOEXP]
1162 \\ `2n ** n - a MOD 2 ** n < 2 ** i`
1163 by METIS_TAC [arithmeticTheory.LESS_LESS_EQ_TRANS]
1164 \\ ASM_SIMP_TAC std_ss [NOT_BIT_GT_TWOEXP]
1165 ]
1166 ]
1167QED
1168
1169(* ------------------------------------------------------------------------- *)
1170
1171Theorem BIT_OF_BITS_THM:
1172 !n h l a. l + n <= h ==> (BIT n (BITS h l a) = BIT (l + n) a)
1173Proof
1174 RW_TAC arith_ss [BIT_def, BITS_COMP_THM]
1175QED
1176
1177Theorem BIT_SHIFT_THM:
1178 !n a s. BIT (n + s) (a * 2 ** s) = BIT n a
1179Proof
1180 RW_TAC std_ss [BIT_def, BITS_def, MOD_2EXP_def, DIV_2EXP_def]
1181 \\ RW_TAC arith_ss [SUC_SUB, EXP_ADD]
1182 \\ METIS_TAC [GSYM DIV_DIV_DIV_MULT, ZERO_LT_TWOEXP, MULT_DIV, MULT_SYM]
1183QED
1184
1185Theorem BIT_SHIFT_THM2:
1186 !n a s. s <= n ==> (BIT n (a * 2 ** s) = BIT (n - s) a)
1187Proof
1188 RW_TAC arith_ss [GSYM (Q.SPECL [`n-s`, `a`, `s`] BIT_SHIFT_THM)]
1189QED
1190
1191Theorem BIT_SHIFT_THM3:
1192 !n a s. (n < s) ==> ~BIT n (a * 2 ** s)
1193Proof
1194 RW_TAC std_ss [BIT_def, BITS_def, MOD_2EXP_def, DIV_2EXP_def]
1195 \\ RW_TAC arith_ss [SUC_SUB, NOT_MOD2_LEM2, GSYM EVEN_MOD2]
1196 \\ RW_TAC arith_ss [DIV_P, ZERO_LT_TWOEXP]
1197 \\ Q.EXISTS_TAC `a * 2 ** (s - n)`
1198 \\ Q.EXISTS_TAC `0`
1199 \\ RW_TAC std_ss [ZERO_LT_TWOEXP, GSYM MULT_ASSOC, GSYM EXP_ADD, EVEN_MULT]
1200 \\ ASM_SIMP_TAC arith_ss [EVEN_EXP]
1201QED
1202
1203Theorem BIT_OF_BITS_THM2:
1204 !h l x n. h < l + x ==> ~BIT x (BITS h l n)
1205Proof
1206 RW_TAC arith_ss [MIN_DEF, BIT_def, BITS_COMP_THM2, BITS_ZERO]
1207QED
1208
1209Theorem BIT_DIV2:
1210 !n i. BIT n (i DIV 2) = BIT (SUC n) i
1211Proof
1212 RW_TAC arith_ss [BIT_def, BITS_THM, EXP, ZERO_LT_TWOEXP, DIV_DIV_DIV_MULT]
1213QED
1214
1215Theorem BIT_SHIFT_THM4:
1216 !n i a. BIT i (a DIV 2 ** n) = BIT (i + n) a
1217Proof
1218 Induct
1219 \\ SRW_TAC [] [arithmeticTheory.ADD_CLAUSES, GSYM BIT_DIV2]
1220 \\ POP_ASSUM
1221 (fn th => SIMP_TAC std_ss [arithmeticTheory.DIV_DIV_DIV_MULT, GSYM th,
1222 ZERO_LT_TWOEXP, EXP])
1223QED
1224
1225Theorem MOD0_MONO[local]:
1226 !n m a. n < m /\ (a MOD 2 ** m = 0) ==> (a MOD 2 ** n = 0)
1227Proof
1228 Cases
1229 \\ Cases
1230 \\ SRW_TAC [] []
1231 \\ FULL_SIMP_TAC std_ss [GSYM BITS_ZERO3]
1232 \\ `n' <= n` by DECIDE_TAC
1233 \\ Q.SPECL_THEN [`n`, `0`, `n'`, `0`, `a`]
1234 (IMP_RES_TAC o SIMP_RULE std_ss []) BITS_COMP_THM
1235 \\ METIS_TAC [BITS_ZERO2]
1236QED
1237
1238Theorem DIV_LT:
1239 !n m a. n < m /\ a < 2 ** m ==> a DIV 2 ** n < 2 ** m
1240Proof
1241 Cases
1242 \\ SRW_TAC [] []
1243 \\ Cases_on `a`
1244 \\ SRW_TAC [] [ZERO_LT_TWOEXP, arithmeticTheory.ZERO_DIV]
1245 \\ `1n < 2 ** SUC n'`
1246 by SRW_TAC [] [EXP, ZERO_LT_TWOEXP, DECIDE ``0 < n ==> 1n < 2 * n``]
1247 \\ METIS_TAC [prim_recTheory.LESS_0, LESS_TRANS,
1248 arithmeticTheory.DIV_LESS, ZERO_LT_TWOEXP]
1249QED
1250
1251Theorem MOD_ZERO_GT:
1252 !n a. a <> 0 /\ (a MOD 2 ** n = 0) ==> 2 ** n <= a
1253Proof
1254 SRW_TAC [] []
1255 \\ SPOSE_NOT_THEN
1256 (ASSUME_TAC o REWRITE_RULE [arithmeticTheory.NOT_LESS_EQUAL])
1257 \\ FULL_SIMP_TAC arith_ss []
1258QED
1259
1260Theorem DIV_GT0:
1261 !a b. b <= a /\ 0 < b ==> (0 < a DIV b)
1262Proof
1263 SRW_TAC [] [arithmeticTheory.X_LT_DIV]
1264QED
1265
1266Theorem DIV_SUB1:
1267 !a b. 2 ** b <= a /\ (a MOD 2 ** b = 0) ==>
1268 (a DIV 2 ** b - 1 = (a - 1) DIV 2 ** b)
1269Proof
1270 SRW_TAC [] [ZERO_LT_TWOEXP,
1271 arithmeticTheory.DIV_SUB
1272 |> Q.INST [`q` |-> `1`] |> SIMP_RULE std_ss [] |> GSYM]
1273 \\ Cases_on `2 ** b = a`
1274 \\ SRW_TAC [ARITH_ss] [ZERO_LT_TWOEXP, arithmeticTheory.ZERO_DIV,
1275 arithmeticTheory.LESS_DIV_EQ_ZERO]
1276 \\ `2 ** b < a` by DECIDE_TAC
1277 \\ IMP_RES_TAC LESS_ADD
1278 \\ POP_ASSUM (SUBST_ALL_TAC o SYM)
1279 \\ ASM_SIMP_TAC arith_ss []
1280 \\ FULL_SIMP_TAC arith_ss
1281 [arithmeticTheory.ADD_MODULUS_LEFT, ZERO_LT_TWOEXP,
1282 arithmeticTheory.ADD_DIV_RWT, arithmeticTheory.LESS_DIV_EQ_ZERO,
1283 DECIDE ``0 < x ==> (p + x - 1 = p + (x - 1n))``]
1284QED
1285
1286Theorem DIV_SUB0[local]:
1287 !a b. a MOD 2 ** b <> 0 ==> (a DIV 2 ** b = (a - 1) DIV 2 ** b)
1288Proof
1289 REPEAT STRIP_TAC
1290 \\ Q.SPECL_THEN [`b`, `a`] ASSUME_TAC TWOEXP_DIVISION
1291 \\ POP_ASSUM SUBST1_TAC
1292 \\ ASM_SIMP_TAC std_ss
1293 [arithmeticTheory.ADD_DIV_ADD_DIV, ZERO_LT_TWOEXP,
1294 DECIDE ``n <> 0n ==> (x + n - 1 = x + (n - 1))``]
1295 \\ `a MOD 2 ** b - 1 < 2 ** b`
1296 by METIS_TAC [DECIDE ``n <> 0n ==> (n - 1 < n)``, MOD_2EXP_LT, LESS_TRANS]
1297 \\ ASM_SIMP_TAC arith_ss [arithmeticTheory.LESS_DIV_EQ_ZERO, ZERO_LT_TWOEXP]
1298QED
1299
1300Theorem BIT_EXP_SUB1:
1301 !b n. BIT b (2 ** n - 1) <=> b < n
1302Proof
1303 REPEAT STRIP_TAC
1304 \\ Cases_on `n` >- SIMP_TAC std_ss [BIT_ZERO]
1305 \\ REWRITE_TAC [(GSYM o SIMP_RULE std_ss [BITS_ZERO2] o
1306 Q.SPECL [`n`, `0`, `ARB`]) BITWISE_ONE_COMP_LEM]
1307 \\ Cases_on `b < SUC n'`
1308 \\ SRW_TAC [ARITH_ss] [BITWISE_THM, BIT_ZERO]
1309 \\ FULL_SIMP_TAC std_ss [NOT_LESS, BIT_def]
1310 \\ `BITWISE (SUC n') (\x y. ~x) 0 ARB < 2 ** b`
1311 by METIS_TAC [BITWISE_LT_2EXP, LESS_LESS_EQ_TRANS, TWOEXP_MONO2]
1312 \\ SRW_TAC [] [BITS_LT_LOW]
1313QED
1314
1315Theorem BIT_SHIFT_THM5:
1316 !n m i a.
1317 i + n < m /\ a < 2 ** m ==>
1318 (BIT i (2 ** m -
1319 (a DIV 2 ** n + if a MOD 2 ** n = 0 then 0 else 1) MOD 2 ** m) =
1320 BIT (i + n) (2 ** m - a MOD 2 ** m))
1321Proof
1322 REPEAT STRIP_TAC
1323 \\ SIMP_TAC arith_ss [BIT_COMPLEMENT]
1324 \\ Cases_on `a MOD 2 ** m = 0`
1325 \\ ASM_SIMP_TAC arith_ss [GSYM BIT_SHIFT_THM4]
1326 >- Q.PAT_ASSUM `a < 2 ** m`
1327 (fn th => FULL_SIMP_TAC arith_ss
1328 [th, ZERO_LT_TWOEXP, arithmeticTheory.ZERO_DIV])
1329 \\ `n < m` by DECIDE_TAC
1330 \\ SRW_TAC [ARITH_ss] [DIV_LT]
1331 >| [
1332 `a <> 0` by (STRIP_TAC \\ FULL_SIMP_TAC arith_ss [])
1333 \\ `2 ** n <= a` by IMP_RES_TAC MOD_ZERO_GT
1334 \\ `0 < a DIV 2 ** n` by METIS_TAC [DIV_GT0, ZERO_LT_TWOEXP]
1335 \\ ASM_SIMP_TAC arith_ss [DIV_SUB1],
1336 Cases_on `a DIV 2 ** n = 2 ** m - 1`
1337 \\ SRW_TAC [ARITH_ss]
1338 [ZERO_LT_TWOEXP, DECIDE ``0n < n ==> (n - 1 + 1 = n)``]
1339 >- ASM_SIMP_TAC arith_ss [GSYM DIV_SUB0, BIT_EXP_SUB1]
1340 \\ `a DIV 2 ** n < 2 ** m` by METIS_TAC [DIV_LT]
1341 \\ `a DIV 2 ** n + 1 < 2 ** m` by DECIDE_TAC
1342 \\ ASM_SIMP_TAC arith_ss [DIV_SUB0]
1343 ]
1344QED
1345
1346(* ------------------------------------------------------------------------- *)
1347
1348Theorem BIT_SET_NOT_ZERO[local]:
1349 !a. (a MOD 2 = 1) ==> (1 <= a)
1350Proof
1351 SPOSE_NOT_THEN STRIP_ASSUME_TAC
1352 \\ `a = 0` by DECIDE_TAC
1353 \\ FULL_SIMP_TAC arith_ss [ZERO_MOD]
1354QED
1355
1356Theorem BIT_SET_NOT_ZERO_COR[local]:
1357 !x n op a b.
1358 x < n ==> op (BIT x a) (BIT x b) ==>
1359 (1 <= (BITWISE n op a b DIV 2 ** x))
1360Proof
1361 REPEAT STRIP_TAC
1362 \\ ASM_SIMP_TAC bool_ss [BITWISE_COR, BIT_SET_NOT_ZERO]
1363QED
1364
1365val BIT_SET_NOT_ZERO_COR2 =
1366 REWRITE_RULE [DIV_1, EXP] (Q.SPEC `0` BIT_SET_NOT_ZERO_COR)
1367
1368Theorem SBIT_MULT:
1369 !b m n. (SBIT b n) * 2 ** m = SBIT b (n + m)
1370Proof
1371 RW_TAC arith_ss [SBIT_def, EXP_ADD]
1372QED
1373
1374Theorem lemma1[local]:
1375 !a b n. 0 < n ==> ((a + SBIT b n) DIV 2 = a DIV 2 + SBIT b (n - 1))
1376Proof
1377 RW_TAC arith_ss [SBIT_def]
1378 \\ IMP_RES_TAC LESS_ADD_1
1379 \\ FULL_SIMP_TAC arith_ss
1380 [GSYM ADD1, EXP, (SIMP_RULE arith_ss [] o Q.SPEC `2`) ADD_DIV_ADD_DIV]
1381QED
1382
1383val lemma2 =
1384 (ONCE_REWRITE_RULE [MULT_COMM] o REWRITE_RULE [EXP_1] o
1385 Q.INST [`m` |-> `1`] o SPEC_ALL) SBIT_MULT
1386
1387Theorem lemma3[local]:
1388 !n op a b.
1389 0 < n ==> (BITWISE n op a b MOD 2 = SBIT (op (ODD a) (ODD b)) 0)
1390Proof
1391 RW_TAC bool_ss [GSYM BIT0_ODD]
1392 \\ POP_ASSUM
1393 (fn th =>
1394 ONCE_REWRITE_TAC [MATCH_MP ((GSYM o Q.SPEC `0`) BITWISE_THM) th])
1395 \\ RW_TAC bool_ss [BIT0_ODD, ODD_MOD2_LEM, SBIT_def, EXP]
1396 \\ FULL_SIMP_TAC bool_ss [GSYM NOT_MOD2_LEM]
1397QED
1398
1399Theorem lemma4[local]:
1400 !n op a b. 0 < n /\ BITWISE n op a b <= SBIT (op (ODD a) (ODD b)) 0 ==>
1401 (BITWISE n op a b = SBIT (op (ODD a) (ODD b)) 0)
1402Proof
1403 RW_TAC arith_ss [GSYM BIT0_ODD, SBIT_def, EXP]
1404 \\ IMP_RES_TAC BIT_SET_NOT_ZERO_COR2
1405 \\ ASM_SIMP_TAC arith_ss []
1406QED
1407
1408Theorem BITWISE_ISTEP[local]:
1409 !n op a b.
1410 0 < n ==>
1411 (BITWISE n op (a DIV 2) (b DIV 2) =
1412 (BITWISE n op a b) DIV 2 + SBIT (op (BIT n a) (BIT n b)) (n - 1))
1413Proof
1414 Induct_on `n`
1415 \\ REPEAT STRIP_TAC
1416 >- FULL_SIMP_TAC arith_ss []
1417 \\ Cases_on `n = 0`
1418 >- RW_TAC arith_ss [BITWISE_def, SBIT_def, BIT_DIV2]
1419 \\ FULL_SIMP_TAC bool_ss
1420 [NOT_ZERO_LT_ZERO, BITWISE_def, SUC_SUB1, BIT_DIV2, lemma1]
1421QED
1422
1423Theorem BITWISE_EVAL:
1424 !n op a b.
1425 BITWISE (SUC n) op a b =
1426 2 * (BITWISE n op (a DIV 2) (b DIV 2)) + SBIT (op (ODD a) (ODD b)) 0
1427Proof
1428 REPEAT STRIP_TAC
1429 \\ Cases_on `n = 0`
1430 >- RW_TAC arith_ss [BITWISE_def, MULT_CLAUSES, GSYM BIT0_ODD]
1431 \\ FULL_SIMP_TAC arith_ss
1432 [BITWISE_def, NOT_ZERO_LT_ZERO, BITWISE_ISTEP, DIV_MULT_THM2,
1433 LEFT_ADD_DISTRIB, SUB_ADD, lemma2, lemma3]
1434 \\ RW_TAC arith_ss [SUB_RIGHT_ADD, lemma4]
1435QED
1436
1437(* ------------------------------------------------------------------------- *)
1438
1439Theorem MOD_PLUS_RIGHT:
1440 !n j k. ((j + (k MOD n)) MOD n) = ((j + k) MOD n)
1441Proof
1442 let
1443 fun SUBS th = SUBST_OCCS_TAC [([2], th)]
1444 in
1445 REPEAT STRIP_TAC
1446 \\ Cases_on `n = 0`
1447 >- (ASM_REWRITE_TAC [MOD_0,MULT_CLAUSES,ADD_CLAUSES])
1448 \\ dxrule_then assume_tac $ iffLR NOT_ZERO_LT_ZERO
1449 \\ PURE_ONCE_REWRITE_TAC [ADD_SYM]
1450 \\ IMP_RES_THEN (TRY o SUBS o Q.SPEC (`k:num`)) DIVISION
1451 \\ ASM_REWRITE_TAC [SYM (SPEC_ALL ADD_ASSOC),MOD_TIMES]
1452 end
1453QED
1454
1455Theorem MOD_PLUS_LEFT =
1456 ONCE_REWRITE_RULE [ADD_COMM] MOD_PLUS_RIGHT
1457
1458Theorem MOD_LESS[local]:
1459 !n a. 0 < n ==> a MOD n < n
1460Proof PROVE_TAC [DIVISION]
1461QED
1462
1463Theorem MOD_LESS1[local]:
1464 !n. 0 < n ==> a MOD n + 1 <= n
1465Proof
1466 REPEAT STRIP_TAC
1467 \\ IMP_RES_TAC MOD_LESS
1468 \\ POP_ASSUM (fn th => ASSUME_TAC (Q.SPEC `a` th))
1469 \\ RW_TAC arith_ss []
1470QED
1471
1472Theorem MOD_ZERO[local]:
1473 !n. 0 < n /\ 0 < a /\ a <= n /\ (a MOD n = 0) ==> (a = n)
1474Proof
1475 REPEAT STRIP_TAC
1476 \\ Cases_on `a < n`
1477 \\ FULL_SIMP_TAC arith_ss [LESS_MOD, GSYM NOT_ZERO_LT_ZERO]
1478QED
1479
1480Theorem MOD_PLUS_1:
1481 !n. 0 < n ==> !x. ((x + 1) MOD n = 0) = (x MOD n + 1 = n)
1482Proof
1483 REPEAT STRIP_TAC
1484 \\ Cases_on `n = 1`
1485 >- ASM_SIMP_TAC arith_ss [MOD_1]
1486 \\ ONCE_REWRITE_TAC [GSYM MOD_PLUS]
1487 \\ `1 < n` by ASM_SIMP_TAC arith_ss []
1488 \\ ASM_SIMP_TAC bool_ss [LESS_MOD]
1489 \\ EQ_TAC
1490 \\ STRIP_TAC
1491 >| [
1492 `0 < x MOD n + 1` by SIMP_TAC arith_ss []
1493 \\ IMP_RES_TAC MOD_LESS1
1494 \\ POP_ASSUM (fn th => ASSUME_TAC (Q.SPEC `x` th))
1495 \\ IMP_RES_TAC MOD_ZERO,
1496 ASM_SIMP_TAC bool_ss [ADD_EQ_SUB, SUB_ADD, DIVMOD_ID]
1497 ]
1498QED
1499
1500Theorem MOD_ADD_1:
1501 !n. 0 < n ==> !x. ~((x + 1) MOD n = 0) ==> ((x + 1) MOD n = x MOD n + 1)
1502Proof
1503 RW_TAC bool_ss [MOD_PLUS_1]
1504 \\ IMP_RES_TAC (Q.SPEC `n` DIVISION)
1505 \\ Q.PAT_ASSUM `!k. k = k DIV n * n + k MOD n`
1506 (fn th => SUBST_OCCS_TAC [([1], Q.SPEC `x` th)])
1507 \\ ONCE_REWRITE_TAC [GSYM ADD_ASSOC]
1508 \\ POP_ASSUM (fn th => ASSUME_TAC (Q.SPEC `x` th))
1509 \\ `x MOD n + 1 < n` by ASM_SIMP_TAC arith_ss []
1510 \\ ASM_SIMP_TAC bool_ss [MOD_TIMES, LESS_MOD]
1511QED
1512
1513(* ------------------------------------------------------------------------- *)
1514
1515val SPEC_EXP1_RULE = (REWRITE_RULE [EXP_1] o Q.SPECL [`x`, `1`])
1516
1517Theorem BIT_REVERSE_THM:
1518 !x n a. x < n ==> (BIT x (BIT_REVERSE n a) = BIT (n - 1 - x) a)
1519Proof
1520 Induct_on `n`
1521 >- REWRITE_TAC [prim_recTheory.NOT_LESS_0]
1522 \\ RW_TAC std_ss [BIT_REVERSE_def]
1523 \\ Cases_on `x = 0`
1524 >| [
1525 `2 = 2 ** (SUC 0)` by numLib.REDUCE_TAC \\ POP_ASSUM SUBST1_TAC
1526 \\ ASM_SIMP_TAC bool_ss [BIT_def, BITS_SUM2]
1527 \\ RW_TAC arith_ss [SBIT_def, BITS_THM],
1528 `!y m n. BIT x (m + n) = BIT (x - 1) (BITS x 1 (m + n))`
1529 by RW_TAC arith_ss [BIT_def, BITS_COMP_THM2, MIN_DEF]
1530 \\ `!b. SBIT b 0 < 2` by RW_TAC arith_ss [SBIT_def]
1531 \\ `!y b. BIT x (y * 2 + SBIT b 0) = BIT (x - 1) y`
1532 by (ASM_SIMP_TAC arith_ss
1533 [SPEC_EXP1_RULE BITS_SUM, SPEC_EXP1_RULE BITS_ZERO4]
1534 \\ SIMP_TAC arith_ss [BIT_def, BITS_COMP_THM2])
1535 \\ `x - 1 < n` by DECIDE_TAC
1536 \\ ASM_SIMP_TAC std_ss []
1537 \\ Cases_on `n = 0` >- ASM_SIMP_TAC arith_ss []
1538 \\ `1 <= n /\ 1 <= x` by DECIDE_TAC
1539 \\ ASM_SIMP_TAC std_ss [ADD1, SUB_SUB, ADD_SUB, SUB_ADD]
1540 ]
1541QED
1542
1543(* ------------------------------------------------------------------------- *)
1544
1545(* |- !x y. 0 < x ==> x <= y ==> LOG2 x <= LOG2 y *)
1546Theorem LOG2_LE_MONO =
1547 logrootTheory.LOG_LE_MONO
1548 |> Q.SPEC `2`
1549 |> SIMP_RULE std_ss [GSYM LOG2_def]
1550
1551(* |- (!x y. 2 ** x <= y ==> x <= LOG2 y) /\
1552 !y x. 0 < x ==> x <= 2 ** y ==> LOG2 x <= y *)
1553Theorem TWOEXP_LE_IMP_LE_LOG2 =
1554 CONJ
1555 (LOG2_LE_MONO
1556 |> Q.SPEC `2 ** x`
1557 |> SIMP_RULE std_ss [ZERO_LT_TWOEXP, LOG2_TWOEXP]
1558 |> Q.GEN `x`)
1559 (LOG2_LE_MONO
1560 |> Q.SPECL [`x`, `2 ** y`]
1561 |> SIMP_RULE std_ss [ZERO_LT_TWOEXP, LOG2_TWOEXP]
1562 |> Q.GEN `x` |> Q.GEN `y`)
1563
1564Theorem NOT_BIT_GT_LOG2:
1565 !i n. LOG2 n < i ==> ~BIT i n
1566Proof
1567 NTAC 3 STRIP_TAC
1568 \\ MATCH_MP_TAC NOT_BIT_GT_TWOEXP
1569 \\ Cases_on `n = 0`
1570 >- ASM_SIMP_TAC std_ss [ZERO_LT_TWOEXP]
1571 \\ `0 < n /\ SUC (LOG2 n) <= i` by DECIDE_TAC
1572 \\ Q.SPECL_THEN [`2`, `n`] ASSUME_TAC logrootTheory.LOG
1573 \\ FULL_SIMP_TAC arith_ss [LOG2_def]
1574 \\ RES_TAC
1575 \\ `2n ** SUC (LOG 2 n) <= 2 ** i` by IMP_RES_TAC TWOEXP_MONO2
1576 \\ DECIDE_TAC
1577QED
1578
1579Theorem NOT_BIT_GT_BITWISE:
1580 !i n op a b. n <= i ==> ~BIT i (BITWISE n op a b)
1581Proof
1582 NTAC 6 STRIP_TAC
1583 \\ `BITWISE n op a b < 2 ** i`
1584 by METIS_TAC [BITWISE_LT_2EXP, TWOEXP_MONO2, ZERO_LT_TWOEXP,
1585 LESS_LESS_EQ_TRANS]
1586 \\ ASM_SIMP_TAC std_ss [NOT_BIT_GT_TWOEXP]
1587QED
1588
1589Theorem LT_TWOEXP:
1590 !x n. x < 2 ** n <=> (x = 0) \/ LOG2 x < n
1591Proof
1592 Cases
1593 \\ SRW_TAC [] [ZERO_LT_TWOEXP, LOG2_def]
1594 \\ EQ_TAC
1595 \\ SRW_TAC [] []
1596 >| [
1597 ONCE_REWRITE_TAC [(GSYM o SIMP_RULE bool_ss [DECIDE ``1 < 2``] o
1598 Q.SPEC `2`) EXP_BASE_LT_MONO]
1599 \\ `2 ** LOG 2 (SUC n) <= SUC n` by SRW_TAC [] [logrootTheory.LOG]
1600 \\ METIS_TAC [LESS_EQ_LESS_TRANS],
1601 `SUC (LOG 2 (SUC n)) <= n'` by DECIDE_TAC
1602 \\ IMP_RES_TAC TWOEXP_MONO2
1603 \\ `SUC n < 2 ** SUC (LOG 2 (SUC n))` by SRW_TAC [] [logrootTheory.LOG]
1604 \\ METIS_TAC [LESS_LESS_EQ_TRANS]
1605 ]
1606QED
1607
1608(* ------------------------------------------------------------------------- *)
1609
1610Theorem BIT_MODIFY_LT_2EXP[local]:
1611 !n f a. BIT_MODIFY n f a < 2 ** n
1612Proof
1613 Induct_on `n`
1614 \\ RW_TAC bool_ss [ADD_0, TIMES2, LESS_IMP_LESS_ADD, LESS_MONO_ADD,
1615 BIT_MODIFY_def, SBIT_def, EXP]
1616 \\ numLib.REDUCE_TAC
1617QED
1618
1619Theorem BIT_MODIFY_LEM[local]:
1620 !n f a. BIT n (BIT_MODIFY (SUC n) f a) = f n (BIT n a)
1621Proof
1622 RW_TAC arith_ss [SBIT_def, BIT_MODIFY_def, NOT_BIT]
1623 >- SIMP_TAC arith_ss
1624 [BIT_def, BITS_THM, SUC_SUB,
1625 REWRITE_RULE [BIT_MODIFY_LT_2EXP]
1626 (Q.SPECL [`BIT_MODIFY n f a`, `2 ** n`] DIV_MULT_1)]
1627 \\ SIMP_TAC arith_ss
1628 [BITS_THM, LESS_DIV_EQ_ZERO, BIT_MODIFY_LT_2EXP, SUC_SUB]
1629QED
1630
1631Theorem BIT_MODIFY_THM:
1632 !x n f a. x < n ==> (BIT x (BIT_MODIFY n f a) = f x (BIT x a))
1633Proof
1634 Induct_on `n`
1635 \\ REPEAT STRIP_TAC
1636 >- FULL_SIMP_TAC arith_ss []
1637 \\ Cases_on `x = n`
1638 >- ASM_REWRITE_TAC [BIT_MODIFY_LEM]
1639 \\ `x < n` by ASM_SIMP_TAC arith_ss []
1640 \\ RW_TAC arith_ss [BIT_MODIFY_def, SBIT_def]
1641 \\ LEFT_REWRITE_TAC [BIT_def]
1642 \\ ASM_REWRITE_TAC [BITS_THM]
1643 \\ IMP_RES_TAC LESS_EXP_MULT2
1644 \\ POP_LAST_TAC
1645 \\ ASM_SIMP_TAC bool_ss
1646 [ZERO_LT_TWOEXP, ADD_DIV_ADD_DIV, TWO_SUC_SUB, GSYM ADD1, EXP,
1647 ONCE_REWRITE_RULE [MULT_COMM]
1648 (REWRITE_RULE [DECIDE (Term `0 < 2`)] (Q.SPEC `2` MOD_TIMES))]
1649 \\ SUBST_OCCS_TAC [([2], SYM (Q.SPEC `x` TWO_SUC_SUB))]
1650 \\ ASM_SIMP_TAC bool_ss [GSYM BITS_THM, GSYM BIT_def]
1651QED
1652
1653(* ------------------------------------------------------------------------- *)
1654
1655Theorem SUB1_EXP_MOD2[local]:
1656 !n. ~(n = 0) ==> ((2 ** n - 1) MOD 2 = 1)
1657Proof
1658 Induct
1659 \\ SRW_TAC [] [EXP, DECIDE ``2 * a - 1 = a + (a - 1)``]
1660 \\ Cases_on `n` >- computeLib.EVAL_TAC
1661 \\ `2 ** SUC n' + (2 ** SUC n' - 1) = 2 ** n' * 2 + (2 ** SUC n' - 1)`
1662 by SIMP_TAC arith_ss [EXP]
1663 \\ ASM_SIMP_TAC std_ss [MOD_TIMES]
1664 \\ FULL_SIMP_TAC arith_ss []
1665QED
1666
1667Theorem BIT_SIGN_EXTEND:
1668 !l h n i.
1669 ~(l = 0) ==>
1670 (BIT i (SIGN_EXTEND l h n) =
1671 if (l <= h) ==> i < l then
1672 BIT i (n MOD 2 ** l)
1673 else
1674 i < h /\ BIT (l - 1) n)
1675Proof
1676 REPEAT STRIP_TAC
1677 \\ SRW_TAC [boolSimps.LET_ss] [IMP_DISJ_THM, SIGN_EXTEND_def]
1678 \\ FULL_SIMP_TAC std_ss [NOT_LESS, NOT_LESS_EQUAL, TWOEXP_MONO,
1679 DECIDE ``a < b ==> (a - b + c = c:num)``]
1680 >| [
1681 Cases_on `h < l`
1682 \\ FULL_SIMP_TAC std_ss [NOT_LESS, TWOEXP_MONO, BIT_def,
1683 DECIDE ``a < b ==> (a - b + c = c:num)``]
1684 \\ drule_then (Q.X_CHOOSE_THEN ‘p’ ASSUME_TAC) (iffLR LESS_EQ_EXISTS)
1685 \\ ASM_SIMP_TAC arith_ss [EXP_ADD, ZERO_LT_TWOEXP,
1686 DECIDE ``0 < b ==> (a * b - a = (b - 1) * a)``]
1687 \\ `?q. l = q + SUC i` by (IMP_RES_TAC LESS_ADD_1
1688 \\ Q.EXISTS_TAC `p'`
1689 \\ DECIDE_TAC)
1690 \\ ASM_SIMP_TAC arith_ss [EXP_ADD, BITS_SUM2],
1691 Cases_on `l`
1692 \\ FULL_SIMP_TAC arith_ss [GSYM BITS_ZERO3, BIT_def, BITS_COMP_THM2]
1693 \\ Cases_on `i < h`
1694 \\ FULL_SIMP_TAC arith_ss [NOT_LESS]
1695 >| [
1696 `2 ** i < 2 ** h` by METIS_TAC [TWOEXP_MONO]
1697 \\ `2 ** SUC n' <= 2 ** i` by METIS_TAC [TWOEXP_MONO2]
1698 \\ `2 ** h MOD 2 ** i = 0`
1699 by (`?q. h = q + i` by METIS_TAC [LESS_ADD]
1700 \\ ASM_SIMP_TAC std_ss [EXP_ADD, MOD_EQ_0, ZERO_LT_TWOEXP])
1701 \\ `2 ** h - 2 ** i = (2 ** (h - i) - 1) * 2 ** i`
1702 by ASM_SIMP_TAC arith_ss [RIGHT_SUB_DISTRIB, EXP_SUB, DIV_MULT_THM]
1703 \\ `2 ** h - 2 ** SUC n' + BITS n' 0 n =
1704 2 ** h - 2 ** i + (2 ** i - 2 ** SUC n' + BITS n' 0 n)`
1705 by ASM_SIMP_TAC std_ss
1706 [DECIDE ``l <= i /\ i < h ==>
1707 (h - l + x = h - i + (i - l + x:num))``]
1708 \\ Q.SPECL_THEN [`n'`, `0`, `n`]
1709 (ASSUME_TAC o REWRITE_RULE [SUB_0]) BITSLT_THM
1710 \\ `~(h - i = 0)` by (NTAC 6 (POP_ASSUM (K ALL_TAC)) \\ DECIDE_TAC)
1711 \\ ASM_SIMP_TAC std_ss
1712 [BITS_SUM, BITS_ZERO4, BITS_ZERO3, SUB1_EXP_MOD2,
1713 DECIDE ``a <= x /\ b < a ==> x - a + b < x:num``],
1714 Q.SPECL_THEN [`n'`, `0`, `n`]
1715 (ASSUME_TAC o REWRITE_RULE [SUB_0]) BITSLT_THM
1716 \\ `2 ** h <= 2 ** i` by METIS_TAC [TWOEXP_MONO2]
1717 \\ `2 ** SUC n' <= 2 ** h` by METIS_TAC [TWOEXP_MONO2]
1718 \\ `2 ** h - 2 ** SUC n' + BITS n' 0 n < 2 ** i` by DECIDE_TAC
1719 \\ ASM_SIMP_TAC std_ss [BITS_LT_LOW]
1720 ],
1721 Cases_on `l`
1722 \\ FULL_SIMP_TAC arith_ss
1723 [MIN_DEF, GSYM BITS_ZERO3, BITS_ZERO, BIT_def, BITS_COMP_THM2]
1724 ]
1725QED
1726
1727(* ------------------------------------------------------------------------- *)
1728
1729Theorem BIT_LOG2:
1730 !n. ~(n = 0) ==> BIT (LOG2 n) n
1731Proof
1732 SRW_TAC [] [BIT_def, BITS_THM, SUC_SUB]
1733 \\ `0 < n` by DECIDE_TAC
1734 \\ IMP_RES_TAC logrootTheory.LOG_MOD
1735 \\ `n DIV 2 ** LOG2 n = (2 ** LOG 2 n + n MOD 2 ** LOG 2 n) DIV 2 ** LOG2 n`
1736 by METIS_TAC []
1737 \\ POP_ASSUM SUBST1_TAC
1738 \\ SRW_TAC [] [LOG2_def, DIV_MULT_1]
1739QED
1740
1741Theorem EXISTS_BIT_IN_RANGE:
1742 !a b n. n <> 0 /\ 2 ** a <= n /\ n < 2 ** b ==>
1743 ?i. a <= i /\ i < b /\ BIT i n
1744Proof
1745 SRW_TAC [] []
1746 \\ Q.EXISTS_TAC `LOG2 n`
1747 \\ `0 < n` by DECIDE_TAC
1748 \\ SRW_TAC [ARITH_ss] [BIT_LOG2, TWOEXP_LE_IMP_LE_LOG2]
1749 \\ FULL_SIMP_TAC arith_ss [LT_TWOEXP]
1750QED
1751
1752Theorem EXISTS_BIT_LT =
1753 EXISTS_BIT_IN_RANGE
1754 |> Q.SPEC `0`
1755 |> SIMP_RULE (arith_ss++boolSimps.CONJ_ss) []
1756
1757Theorem LEAST_THM:
1758 !n P. (!m. m < n ==> ~P m) /\ P n ==> ($LEAST P = n)
1759Proof
1760 REPEAT STRIP_TAC
1761 \\ IMP_RES_TAC WhileTheory.FULL_LEAST_INTRO
1762 \\ Cases_on `$LEAST P = n`
1763 >- ASM_REWRITE_TAC []
1764 \\ `$LEAST P < n` by DECIDE_TAC
1765 \\ PROVE_TAC []
1766QED
1767
1768(* ------------------------------------------------------------------------- *)
1769
1770fun simp thl = simpLib.ASM_SIMP_TAC (srw_ss() ++ numSimps.ARITH_ss) thl
1771
1772Theorem BIT_TIMES2:
1773 BIT z (2 * n) <=> 0 < z /\ BIT (z-1) n
1774Proof
1775 Cases_on`z` >> simp[] >- (
1776 simp[BIT0_ODD] >>
1777 simp[arithmeticTheory.ODD_EVEN] >>
1778 simp[arithmeticTheory.EVEN_DOUBLE]) >>
1779 Q.RENAME_TAC [‘BIT (SUC z) (2 * n) <=> BIT z n’] >>
1780 Q.SPECL_THEN[‘z’,‘n’,‘1’]mp_tac BIT_SHIFT_THM >>
1781 simp[arithmeticTheory.ADD1]
1782QED
1783
1784Theorem BIT_TIMES2_1:
1785 !n z. BIT z (2 * n + 1) <=> (z=0) \/ BIT z (2 * n)
1786Proof
1787 Induct >> simp_tac std_ss [] >- (
1788 simp_tac std_ss [BIT_ZERO] >>
1789 Cases_on`z`>>simp_tac std_ss [BIT0_ODD] >>
1790 simp_tac arith_ss [GSYM BIT_DIV2,BIT_ZERO] ) >>
1791 Cases >> simp_tac std_ss [BIT0_ODD] >- (
1792 simp_tac std_ss [arithmeticTheory.ODD_EXISTS,arithmeticTheory.ADD1] >>
1793 METIS_TAC[] ) >>
1794 simp_tac std_ss [GSYM BIT_DIV2] >>
1795 Q.SPEC_THEN ‘2’ mp_tac arithmeticTheory.ADD_DIV_RWT >>
1796 simp[] >>
1797 disch_then(Q.SPECL_THEN[‘2 * SUC n’,‘1’]mp_tac) >>
1798 simp_tac std_ss []
1799QED
1800
1801Theorem BITWISE_COMM:
1802 (!m. m <= n ==> op (BIT m x) (BIT m y) = op (BIT m y) (BIT m x))
1803 ==> BITWISE n op x y = BITWISE n op y x
1804Proof
1805 Induct_on`n`
1806 \\ SRW_TAC[][BITWISE_def]
1807 \\ first_assum(Q.SPEC_THEN`n`mp_tac)
1808 \\ impl_tac >- SRW_TAC[][]
1809 \\ disch_then SUBST1_TAC
1810 \\ simp[]
1811 \\ first_x_assum irule
1812 \\ SRW_TAC[][]
1813 \\ first_x_assum irule
1814 \\ simp[]
1815QED
1816
1817Theorem BITWISE_AND_0_lemma[local]:
1818 BITWISE w $/\ x 0 = 0
1819Proof
1820 Q.ID_SPEC_TAC`x`
1821 \\ Induct_on`w`
1822 \\ SRW_TAC[][BITWISE_def, SBIT_def, BIT_ZERO]
1823QED
1824
1825Theorem BITWISE_AND_0[simp]:
1826 BITWISE w $/\ x 0 = 0 /\
1827 BITWISE w $/\ 0 x = 0
1828Proof
1829 Q.SPECL_THEN[`$/\`,`0`,`x`,`w`]mp_tac(Q.GENL[`op`,`x`,`y`,`n`]BITWISE_COMM)
1830 \\ impl_tac >- SRW_TAC[][BIT_ZERO]
1831 \\ disch_then SUBST1_TAC
1832 \\ SRW_TAC[][BITWISE_AND_0_lemma]
1833QED
1834
1835Theorem BITWISE_AND_SHIFT_EQ_0:
1836 !w x y n.
1837 x < 2 ** n ==>
1838 BITWISE w $/\ x (y * 2 ** n) = 0
1839Proof
1840 Induct \\ SRW_TAC[][BITWISE_def, SBIT_def]
1841 \\ strip_tac
1842 \\ Cases_on`w < n`
1843 >- ( drule BIT_SHIFT_THM3 \\ simp[]
1844 \\ Q.EXISTS_TAC`y` \\ simp[])
1845 \\ FULL_SIMP_TAC(srw_ss())[NOT_LESS]
1846 \\ drule TWOEXP_MONO2 \\ strip_tac
1847 \\ `x < 2 ** w` by METIS_TAC[LESS_LESS_EQ_TRANS]
1848 \\ drule NOT_BIT_GT_TWOEXP
1849 \\ simp[]
1850QED