numposrepScript.sml
1Theory numposrep[bare]
2Ancestors
3 list rich_list logroot arithmetic bit
4Libs
5 HolKernel boolLib Parse BasicProvers simpLib boolSimps numLib
6 TotalDefn metisLib
7
8val ARITH_ss = numSimps.ARITH_ss
9
10val simp = ASM_SIMP_TAC (srw_ss()++ARITH_ss)
11val fs = FULL_SIMP_TAC (srw_ss()++ARITH_ss)
12val rw = SRW_TAC[ARITH_ss]
13
14(* ------------------------------------------------------------------------- *)
15
16Definition l2n_def:
17 (l2n b [] = 0) /\
18 (l2n b (h::t) = h MOD b + b * l2n b t)
19End
20
21Definition n2l_def:
22 n2l b n = if n < b \/ b < 2 then [n MOD b] else n MOD b :: n2l b (n DIV b)
23End
24
25(* related version that gives MS-digit first, using an accumulator, and passes
26 each digit through a function *)
27Definition n2lA_def[nocompute]:
28 n2lA A f b n = if n < b \/ b < 2 then f (n MOD b)::A
29 else n2lA (f (n MOD b) :: A) f b (n DIV b)
30End
31
32Definition num_from_bin_list_def: num_from_bin_list = l2n 2 o REVERSE
33End
34Definition num_from_oct_list_def: num_from_oct_list = l2n 8 o REVERSE
35End
36Definition num_from_dec_list_def: num_from_dec_list = l2n 10 o REVERSE
37End
38Definition num_from_hex_list_def: num_from_hex_list = l2n 16 o REVERSE
39End
40
41Theorem n2lA_10[compute]:
42 n2lA A f 10 n = if n < 10 then f n::A
43 else n2lA (f (n MOD 10) :: A) f 10 (n DIV 10)
44Proof
45 simp[Once n2lA_def, SimpLHS]
46QED
47
48Theorem n2lA_n2l:
49 !A n. n2lA A f b n = MAP f (REVERSE (n2l b n)) ++ A
50Proof
51 completeInduct_on ‘n’ >> simp_tac (srw_ss()) [Once n2lA_def, Once n2l_def] >>
52 rw[] >> simp[GSYM APPEND_ASSOC, Excl "APPEND_ASSOC"]
53QED
54
55Theorem n2l_n2lA:
56 n2l b n = REVERSE (n2lA [] I b n)
57Proof simp[n2lA_n2l]
58QED
59
60
61
62Definition num_to_bin_list_def: num_to_bin_list = REVERSE o n2l 2
63End
64Definition num_to_oct_list_def: num_to_oct_list = REVERSE o n2l 8
65End
66Definition num_to_dec_list_def: num_to_dec_list = REVERSE o n2l 10
67End
68Definition num_to_hex_list_def: num_to_hex_list = REVERSE o n2l 16
69End
70
71Definition BOOLIFY_def:
72 (BOOLIFY 0 m a = a) /\
73 (BOOLIFY (SUC n) m a = BOOLIFY n (DIV2 m) (ODD m::a))
74End
75
76(* ------------------------------------------------------------------------- *)
77
78Theorem LENGTH_n2l:
79 !b n. 1 < b ==> (LENGTH (n2l b n) = if n = 0 then 1 else SUC (LOG b n))
80Proof
81 completeInduct_on `LOG b n`
82 \\ SRW_TAC [ARITH_ss] [Once n2l_def, LOG_RWT]
83 \\ SRW_TAC [ARITH_ss] [LOG_RWT]
84 \\ `0 < n DIV b` by SRW_TAC [ARITH_ss] [X_LT_DIV]
85 \\ DECIDE_TAC
86QED
87
88Theorem LOG_DIV_LESS[local]:
89 !b n. b <= n /\ 1 < b ==> LOG b (n DIV b) < LOG b n
90Proof
91 SRW_TAC [] [] \\ IMP_RES_TAC LOG_DIV \\ DECIDE_TAC
92QED
93
94Theorem l2n_n2l:
95 !b n. 1 < b ==> (l2n b (n2l b n) = n)
96Proof
97 completeInduct_on `LOG b n`
98 \\ SRW_TAC [ARITH_ss] [Once n2l_def, l2n_def]
99 \\ `LOG b (n DIV b) < LOG b n` by SRW_TAC [ARITH_ss] [LOG_DIV_LESS]
100 \\ SRW_TAC [ARITH_ss] [(GSYM o ONCE_REWRITE_RULE [MULT_COMM]) DIVISION]
101QED
102
103Theorem l2n_lt:
104 !l b. 0 < b ==> l2n b l < b ** LENGTH l
105Proof
106 Induct \\ SRW_TAC [] [l2n_def, arithmeticTheory.EXP]
107 \\ RES_TAC
108 \\ IMP_RES_TAC arithmeticTheory.LESS_ADD_1
109 \\ POP_ASSUM (K ALL_TAC)
110 \\ POP_ASSUM SUBST1_TAC
111 \\ SRW_TAC [] [arithmeticTheory.LEFT_ADD_DISTRIB]
112 \\ SRW_TAC [ARITH_ss]
113 [arithmeticTheory.MOD_LESS, DECIDE ``a < b:num ==> (a < b + c)``]
114QED
115
116(* ......................................................................... *)
117
118Theorem LENGTH_l2n:
119 !b l. 1 < b /\ EVERY ($> b) l /\ ~(l2n b l = 0) ==>
120 SUC (LOG b (l2n b l)) <= LENGTH l
121Proof
122 Induct_on `l` \\ SRW_TAC [ARITH_ss] [l2n_def, GREATER_DEF] \\
123 Cases_on ‘h MOD b = 0’ \\ FULL_SIMP_TAC (srw_ss()) []
124 >- (REV_FULL_SIMP_TAC (srw_ss() ++ ARITH_ss) [MOD_EQ_0_DIVISOR] \\
125 FULL_SIMP_TAC (srw_ss()) [LT_MULT_CANCEL_RBARE] \\ SRW_TAC[][] \\
126 SRW_TAC[ARITH_ss][LOG_MULT]) \\
127 ‘h <> 0’ by (STRIP_TAC \\ SRW_TAC[][] \\ REV_FULL_SIMP_TAC (srw_ss()) []) \\
128 ‘0 < h + b * l2n b l’ by DECIDE_TAC \\
129 Cases_on ‘l2n b l = 0’
130 >- (SRW_TAC[][] \\ SRW_TAC[ARITH_ss][LOG_RWT]) \\
131 SRW_TAC[][LOG_RWT] \\
132 ‘(h + b * l2n b l) DIV b = l2n b l’
133 by METIS_TAC[DIV_MULT, MULT_COMM, ADD_COMM] \\
134 SRW_TAC[][]
135QED
136
137Theorem l2n_DIGIT:
138 !b l x. 1 < b /\ EVERY ($> b) l /\ x < LENGTH l ==>
139 ((l2n b l DIV b ** x) MOD b = EL x l)
140Proof
141 Induct_on `l` \\ SRW_TAC [ARITH_ss] [l2n_def, GREATER_DEF]
142 \\ Cases_on `x`
143 \\ SRW_TAC [ARITH_ss]
144 [EXP, GSYM DIV_DIV_DIV_MULT, ZERO_LT_EXP, LESS_DIV_EQ_ZERO,
145 SIMP_RULE arith_ss [] (CONJ MOD_TIMES ADD_DIV_ADD_DIV)]
146QED
147
148Theorem lem[local]:
149 !b n. 1 < b ==> PRE (LENGTH (n2l b n)) <= LENGTH (n2l b (n DIV b))
150Proof
151 SRW_TAC [ARITH_ss] [LENGTH_n2l]
152 >| [
153 `0 <= n DIV b /\ 0 < n` by DECIDE_TAC
154 \\ IMP_RES_TAC DIV_0_IMP_LT
155 \\ SRW_TAC [ARITH_ss] [LOG_RWT],
156 IMP_RES_TAC (METIS_PROVE [LESS_DIV_EQ_ZERO,NOT_LESS_EQUAL]
157 ``!b n. 1 < b /\ ~(n DIV b = 0) ==> b <= n``)
158 \\ SRW_TAC [ARITH_ss] [LOG_DIV]]
159QED
160
161Theorem EL_n2l:
162 !b x n. 1 < b /\ x < LENGTH (n2l b n) ==>
163 (EL x (n2l b n) = (n DIV (b ** x)) MOD b)
164Proof
165 completeInduct_on `LOG b n`
166 \\ SRW_TAC [] []
167 \\ ONCE_REWRITE_TAC [n2l_def]
168 \\ SRW_TAC [ARITH_ss] []
169 >| [
170 IMP_RES_TAC LENGTH_n2l
171 \\ Cases_on `n = 0`
172 \\ FULL_SIMP_TAC arith_ss []
173 >| [ALL_TAC, `LOG b n = 0` by SRW_TAC [ARITH_ss] [LOG_RWT]]
174 \\ `x = 0` by DECIDE_TAC \\ SRW_TAC [ARITH_ss] [EXP],
175 Cases_on `x = 0`
176 \\ SRW_TAC [ARITH_ss] [EXP, EL_CONS]
177 \\ `LOG b (n DIV b) < LOG b n /\ PRE x < x /\ 0 < x`
178 by SRW_TAC [ARITH_ss] [LOG_DIV_LESS]
179 \\ `PRE x < LENGTH (n2l b (n DIV b))`
180 by METIS_TAC [lem, INV_PRE_LESS, LESS_LESS_EQ_TRANS]
181 \\ RES_TAC
182 \\ POP_ASSUM (Q.SPECL_THEN [`n DIV b`,`b`]
183 (ASSUME_TAC o SIMP_RULE std_ss []))
184 \\ POP_ASSUM (Q.SPEC_THEN `PRE x` IMP_RES_TAC)
185 \\ SRW_TAC [ARITH_ss] [GSYM EXP, DIV_DIV_DIV_MULT,
186 DECIDE ``!n. 0 < n ==> (SUC (PRE n) = n)``]]
187QED
188
189Theorem LIST_EQ[local] = iffRL LIST_EQ_REWRITE
190
191Theorem n2l_l2n[local]:
192 !b n l. 1 < b /\ EVERY ($> b) l /\ (n = l2n b l) ==>
193 (n2l b n = if n = 0 then [0] else TAKE (SUC (LOG b n)) l)
194Proof
195 SRW_TAC [] [] >- SRW_TAC [ARITH_ss] [Once n2l_def]
196 \\ MATCH_MP_TAC LIST_EQ \\ IMP_RES_TAC LENGTH_l2n
197 \\ SRW_TAC [ARITH_ss] [LENGTH_n2l,LENGTH_TAKE,EL_TAKE,EL_n2l,l2n_DIGIT]
198QED
199
200Theorem n2l_l2n =
201 n2l_l2n |> Q.SPECL [`b`,`l2n b l`,`l`]
202 |> REWRITE_RULE []
203 |> Q.GEN `l` |> Q.GEN `b`
204
205Theorem l2n_eq_0:
206 !b. 0 < b ==> !l. (l2n b l = 0) <=> EVERY ($= 0 o combin$C $MOD b) l
207Proof
208 NTAC 2 STRIP_TAC THEN Induct THEN simp[l2n_def] THEN
209 Q.X_GEN_TAC`z` THEN Cases_on`0=z MOD b` THEN simp[]
210QED
211
212Theorem l2n_SNOC_0:
213 !b ls. 0 < b ==> (l2n b (SNOC 0 ls) = l2n b ls)
214Proof
215 GEN_TAC THEN Induct THEN simp[l2n_def]
216QED
217
218Theorem MOD_EQ_0_0[local]:
219 !n b. 0 < b ==> (n MOD b = 0) ==> n < b ==> (n = 0)
220Proof
221 SRW_TAC[][MOD_EQ_0_DIVISOR] THEN Cases_on`d` THEN FULL_SIMP_TAC(srw_ss())[]
222QED
223
224Theorem LOG_l2n:
225 !b. 1 < b ==> !l. l <> [] /\ 0 < LAST l /\ EVERY ($> b) l ==>
226 (LOG b (l2n b l) = PRE (LENGTH l))
227Proof
228 NTAC 2 STRIP_TAC THEN Induct THEN simp[l2n_def] THEN
229 rw[] THEN fs[LAST_DEF] THEN
230 Cases_on`l=[]` THEN fs[l2n_def] THEN1 (
231 simp[LOG_EQ_0] ) THEN
232 Q.MATCH_ASSUM_ABBREV_TAC`LOG b z = d` THEN
233 `h + b * z = b * z + h` by simp[] THEN POP_ASSUM SUBST1_TAC THEN
234 Q.SPECL_THEN[`b`,`h`,`z`]MP_TAC LOG_add_digit THEN
235 simp[Abbr`d`] THEN
236 Q_TAC SUFF_TAC`0 < z` THEN1 (
237 simp[] THEN Cases_on`l` THEN fs[] ) THEN
238 simp[Abbr`z`] THEN
239 Cases_on`l2n b l = 0` THEN simp[] THEN
240 `0 < b` by simp[] THEN
241 fs[l2n_eq_0] THEN
242 `?z. MEM z l /\ 0 < z` by (
243 Q.EXISTS_TAC`LAST l` THEN simp[] THEN
244 Cases_on`l` THEN simp[rich_listTheory.MEM_LAST] THEN
245 fs[] ) THEN
246 fs[EVERY_MEM] THEN
247 RES_TAC THEN
248 `z = 0` by METIS_TAC[MOD_EQ_0_0,GREATER_DEF] THEN
249 fs[]
250QED
251
252Theorem l2n_dropWhile_0:
253 !b ls.
254 0 < b ==> (l2n b (REVERSE (dropWhile ($= 0) (REVERSE ls))) = l2n b ls)
255Proof
256 GEN_TAC >> HO_MATCH_MP_TAC SNOC_INDUCT >>
257 simp[dropWhile_def,REVERSE_SNOC] >> rw[] >>
258 rw[] >> rw[l2n_SNOC_0] >> rw[SNOC_APPEND]
259QED
260
261Theorem LOG_l2n_dropWhile:
262 !b l. 1 < b /\ EXISTS ($<> 0) l /\ EVERY ($>b) l ==>
263 (LOG b (l2n b l) = PRE (LENGTH (dropWhile ($= 0) (REVERSE l))))
264Proof
265 Tactical.REPEAT STRIP_TAC >>
266 `0 < b` by simp[] >>
267 simp[Once(GSYM l2n_dropWhile_0)] >>
268 Q.MATCH_ABBREV_TAC`x = PRE (LENGTH y)` >>
269 Q_TAC SUFF_TAC`x = PRE (LENGTH (REVERSE y))` >- rw[] >>
270 markerLib.UNABBREV_ALL_TAC >>
271 MATCH_MP_TAC (MP_CANON LOG_l2n) >>
272 simp[dropWhile_eq_nil,rich_listTheory.EXISTS_REVERSE,
273 rich_listTheory.EVERY_REVERSE,combinTheory.o_DEF] >>
274 fs[EVERY_MEM] >>
275 Tactical.REVERSE CONJ_TAC >- METIS_TAC[MEM_dropWhile_IMP,MEM_REVERSE] >>
276 Q.MATCH_ABBREV_TAC`0:num < LAST (REVERSE ls)` >>
277 Cases_on`ls = []` >- (
278 fs[Abbr`ls`,dropWhile_eq_nil,EVERY_MEM,EXISTS_MEM] >>
279 METIS_TAC[] ) >>
280 simp[LAST_REVERSE] >>
281 Q_TAC SUFF_TAC`~ (($= 0) (HD ls))` >- simp[] >>
282 Q.UNABBREV_TAC`ls` >>
283 MATCH_MP_TAC HD_dropWhile >>
284 fs[EXISTS_MEM] >> METIS_TAC[]
285QED
286
287(* ------------------------------------------------------------------------- *)
288
289Theorem n2l_BOUND:
290 !b n. 0 < b ==> EVERY ($> b) (n2l b n)
291Proof
292 NTAC 2 STRIP_TAC \\ completeInduct_on `LOG b n`
293 \\ SRW_TAC [ARITH_ss] [Once n2l_def, GREATER_DEF]
294 \\ `LOG b (n DIV b) < LOG b n` by SRW_TAC [ARITH_ss] [LOG_DIV_LESS]
295 \\ SRW_TAC [ARITH_ss] []
296QED
297
298(* ------------------------------------------------------------------------- *)
299
300Theorem l2n_pow2_compute:
301 (!p. l2n (2 ** p) [] = 0) /\
302 (!p h t. l2n (2 ** p) (h::t) =
303 MOD_2EXP p h + TIMES_2EXP p (l2n (2 ** p) t))
304Proof
305 SRW_TAC [ARITH_ss] [l2n_def, TIMES_2EXP_def, MOD_2EXP_def]
306QED
307
308val lem = (GEN_ALL o REWRITE_RULE [EXP] o Q.SPECL [`n`,`0`] o
309 REWRITE_RULE [DECIDE ``1 < 2``] o Q.SPEC `2`) EXP_BASE_LT_MONO
310
311Theorem n2l_pow2_compute:
312 !p n. 0 < p ==>
313 (n2l (2 ** p) n =
314 let (q,r) = DIVMOD_2EXP p n in
315 if q = 0 then [r] else r::n2l (2 ** p) q)
316Proof
317 SRW_TAC [] [Once n2l_def, DIVMOD_2EXP_def,
318 DECIDE ``x < 2 <=> (x = 0) \/ (x = 1)``]
319 \\ SRW_TAC [ARITH_ss] [LESS_DIV_EQ_ZERO]
320 \\ FULL_SIMP_TAC arith_ss [lem, DIV_0_IMP_LT]
321QED
322
323Definition l2n2[nocompute]: l2n2 = l2n 2
324End
325
326Theorem l2n2_empty[local]:
327 l2n2 [] = ZERO
328Proof
329 REWRITE_TAC [l2n2, l2n_def, arithmeticTheory.ALT_ZERO]
330QED
331
332val l2n_2 =
333 SIMP_RULE arith_ss [bitTheory.MOD_2EXP_def, bitTheory.TIMES_2EXP_def]
334 (Q.SPEC `1` (Thm.CONJUNCT2 l2n_pow2_compute))
335
336Theorem l2n2_cons0[local]:
337 !t. l2n2 (0::t) = numeral$iDUB (l2n2 t)
338Proof
339 SIMP_TAC arith_ss [l2n2, l2n_2]
340 \\ METIS_TAC [arithmeticTheory.MULT_COMM, arithmeticTheory.TIMES2,
341 numeralTheory.iDUB]
342QED
343
344Theorem l2n2_cons1[local]:
345 !t. l2n2 (1::t) = arithmetic$BIT1 (l2n2 t)
346Proof
347 SIMP_TAC arith_ss [l2n2, l2n_2]
348 \\ METIS_TAC [numLib.DECIDE ``2 * a + 1 = a + (a + SUC 0)``,
349 arithmeticTheory.BIT1]
350QED
351
352Theorem l2n2[local]:
353 (!t. l2n 2 (0::t) = NUMERAL (l2n2 (0::t))) /\
354 (!t. l2n 2 (1::t) = NUMERAL (l2n2 (1::t)))
355Proof
356 REWRITE_TAC [l2n2, arithmeticTheory.NUMERAL_DEF]
357QED
358
359Theorem l2n_2_thms =
360 LIST_CONJ (CONJUNCTS l2n2 @ [l2n2_empty, l2n2_cons0, l2n2_cons1])
361
362val () = Parse.remove_ovl_mapping "l2n2" {Thy = "numposrep", Name = "l2n2"}
363
364(* ------------------------------------------------------------------------- *)
365
366Theorem BIT_l2n_2:
367 !x l. EVERY ($> 2) l ==>
368 (BIT x (l2n 2 l) <=> x < LENGTH l /\ EL x l = 1)
369Proof
370 rpt strip_tac >> Cases_on ‘x < LENGTH l’ >>
371 SRW_TAC [ARITH_ss] [l2n_DIGIT, SUC_SUB, BIT_def, BITS_THM] >>
372 Q.RENAME_TAC [‘l2n 2 l DIV 2 ** x’] >>
373 Q_TAC SUFF_TAC ‘l2n 2 l DIV 2 ** x = 0’ >> simp[] >>
374 MATCH_MP_TAC LESS_DIV_EQ_ZERO >>
375 MATCH_MP_TAC LESS_LESS_EQ_TRANS >> Q.EXISTS_TAC ‘2 ** LENGTH l’ >>
376 SRW_TAC[ARITH_ss][l2n_lt]
377QED
378
379Theorem BIT_num_from_bin_list:
380 !x l. EVERY ($> 2) l /\ x < LENGTH l ==>
381 (BIT x (num_from_bin_list l) = (EL x (REVERSE l) = 1))
382Proof
383 simp[num_from_bin_list_def, BIT_l2n_2]
384QED
385
386Theorem EL_num_to_bin_list:
387 !x n.
388 x < LENGTH (num_to_bin_list n) ==>
389 EL x (REVERSE (num_to_bin_list n)) = BITV n x
390Proof
391 SRW_TAC [ARITH_ss]
392 [num_to_bin_list_def, EL_n2l, SUC_SUB, BITV_def, BIT_def, BITS_THM]
393QED
394
395val tac =
396 SRW_TAC [ARITH_ss]
397 [FUN_EQ_THM, l2n_n2l,
398 num_from_bin_list_def, num_from_oct_list_def, num_from_dec_list_def,
399 num_from_hex_list_def, num_to_bin_list_def, num_to_oct_list_def,
400 num_to_dec_list_def, num_to_hex_list_def]
401
402Theorem num_bin_list:
403 num_from_bin_list o num_to_bin_list = I
404Proof tac
405QED
406Theorem num_oct_list:
407 num_from_oct_list o num_to_oct_list = I
408Proof tac
409QED
410Theorem num_dec_list:
411 num_from_dec_list o num_to_dec_list = I
412Proof tac
413QED
414Theorem num_hex_list:
415 num_from_hex_list o num_to_hex_list = I
416Proof tac
417QED
418
419(* ------------------------------------------------------------------------- *)
420
421Theorem l2n_APPEND:
422 !b l1 l2. l2n b (l1 ++ l2) = l2n b l1 + b ** (LENGTH l1) * l2n b l2
423Proof
424 Induct_on `l1` \\ SRW_TAC [ARITH_ss] [EXP, l2n_def]
425QED
426
427Theorem EXP_MONO[local]:
428 !b m n x. 1 < b /\ m < n /\ x < b ** m ==> (b ** m + x < b ** n)
429Proof
430 Induct_on `n`
431 \\ SRW_TAC [ARITH_ss] [EXP]
432 \\ Cases_on `m = n`
433 \\ SRW_TAC [ARITH_ss] []
434 >| [
435 `?p. b ** m = p + x` by METIS_TAC [LESS_ADD]
436 \\ `?q. b = 1 + (q + 1)` by METIS_TAC [LESS_ADD_1]
437 \\ FULL_SIMP_TAC arith_ss [LEFT_ADD_DISTRIB],
438 `m < n` by DECIDE_TAC \\ RES_TAC
439 \\ `b ** n < b * b ** n` by SRW_TAC [ARITH_ss] []
440 \\ DECIDE_TAC]
441QED
442
443Theorem l2n_b_1[local]:
444 !b. 1 < b ==> (l2n b [1] = 1)
445Proof
446 SRW_TAC [] [l2n_def]
447QED
448
449Theorem l2n_11:
450 !b l1 l2.
451 1 < b /\ EVERY ($> b) l1 /\ EVERY ($> b) l2 ==>
452 ((l2n b (l1 ++ [1]) = l2n b (l2 ++ [1])) = (l1 = l2))
453Proof
454 REPEAT STRIP_TAC \\ EQ_TAC \\ SRW_TAC [] []
455 \\ MATCH_MP_TAC LIST_EQ
456 \\ sg `LENGTH l1 = LENGTH l2`
457 \\ SRW_TAC [] []
458 >| [
459 SPOSE_NOT_THEN STRIP_ASSUME_TAC
460 \\ Q.PAT_X_ASSUM `l2n b x = l2n b y` MP_TAC
461 \\ ASM_SIMP_TAC (srw_ss()++ARITH_ss) [l2n_APPEND, l2n_b_1]
462 \\ `(LENGTH l1 < LENGTH l2) \/ (LENGTH l2 < LENGTH l1)`
463 by METIS_TAC [LESS_LESS_CASES]
464 >| [MATCH_MP_TAC (DECIDE ``a < b ==> ~(a = b + x)``),
465 MATCH_MP_TAC (DECIDE ``b < a ==> ~(a + x = b)``)]
466 \\ MATCH_MP_TAC EXP_MONO
467 \\ ASM_SIMP_TAC (srw_ss()++ARITH_ss) [l2n_lt],
468 `x < LENGTH l1` by DECIDE_TAC
469 \\ IMP_RES_TAC (GSYM l2n_DIGIT)
470 \\ NTAC 2 (POP_ASSUM SUBST1_TAC)
471 \\ FULL_SIMP_TAC (srw_ss()) [l2n_APPEND]]
472QED
473
474Theorem BITWISE_l2n_2:
475 LENGTH l1 = LENGTH l2 ==>
476 BITWISE (LENGTH l1) op (l2n 2 l1) (l2n 2 l2) =
477 l2n 2 (MAP2 (\x y. bool_to_bit $ op (ODD x) (ODD y)) l1 l2)
478Proof
479 Q.ID_SPEC_TAC`l2`
480 \\ Induct_on`l1`
481 \\ simp[BITWISE_EVAL]
482 >- simp[BITWISE_def, l2n_def]
483 \\ Q.X_GEN_TAC`b`
484 \\ Cases \\ fs[BITWISE_EVAL]
485 \\ strip_tac
486 \\ fs[l2n_def]
487 \\ simp[SBIT_def, ODD_ADD, ODD_MULT, GSYM bool_to_bit_def]
488QED
489
490Theorem l2n_2_neg:
491 !ls.
492 EVERY ($> 2) ls ==>
493 l2n 2 (MAP (\x. 1 - x) ls) = 2 ** LENGTH ls - SUC (l2n 2 ls)
494Proof
495 Induct
496 \\ rw[l2n_def]
497 \\ fs[EXP, ADD1]
498 \\ simp[LEFT_SUB_DISTRIB, LEFT_ADD_DISTRIB, SUB_RIGHT_ADD]
499 \\ Q.SPECL_THEN[`ls`,`2`]mp_tac l2n_lt
500 \\ simp[]
501QED
502
503Theorem l2n_max:
504 0 < b ==>
505 !ls. (l2n b ls = b ** (LENGTH ls) - 1) <=>
506 (EVERY ((=) (b - 1) o flip $MOD b) ls)
507Proof
508 strip_tac
509 \\ Induct
510 \\ rw[l2n_def]
511 \\ rw[EXP]
512 \\ Q.MATCH_GOALSUB_ABBREV_TAC`b * l + a`
513 \\ Q.MATCH_GOALSUB_ABBREV_TAC`b ** n`
514 \\ fs[EQ_IMP_THM]
515 \\ conj_tac
516 >- (
517 strip_tac
518 \\ Cases_on`n=0` \\ fs[] >- (fs[Abbr`n`] \\ rw[])
519 \\ `0 < b * b ** n` by simp[]
520 \\ `a + b * l + 1 = b * b ** n` by simp[]
521 \\ `(b * b ** n) DIV b = b ** n` by simp[MULT_TO_DIV]
522 \\ `(b * l + (a + 1)) DIV b = b ** n` by fs[]
523 \\ `(b * l) MOD b = 0` by simp[]
524 \\ `(b * l + (a + 1)) DIV b = (b * l) DIV b + (a + 1) DIV b`
525 by ( irule ADD_DIV_RWT \\ simp[] )
526 \\ pop_assum SUBST_ALL_TAC
527 \\ `(a + 1) DIV b = if a = b - 1 then 1 else 0`
528 by (
529 rw[]
530 \\ `a + 1 < b` suffices_by rw[DIV_EQ_0]
531 \\ simp[Abbr`a`]
532 \\ `h MOD b < b - 1` suffices_by simp[]
533 \\ `h MOD b < b` by simp[]
534 \\ fs[] )
535 \\ `b * l DIV b = l` by simp[MULT_TO_DIV]
536 \\ pop_assum SUBST_ALL_TAC
537 \\ pop_assum SUBST_ALL_TAC
538 \\ `l < b ** n` by ( map_every Q.UNABBREV_TAC[`l`,`n`]
539 \\ irule l2n_lt \\ simp[] )
540 \\ Cases_on`a = b - 1` \\ fs[] )
541 \\ strip_tac
542 \\ rewrite_tac[LEFT_SUB_DISTRIB]
543 \\ Q.PAT_X_ASSUM`_ = a`(SUBST1_TAC o SYM)
544 \\ fs[SUB_LEFT_ADD] \\ rw[]
545 \\ Cases_on`n=0` \\ fs[]
546 \\ `b ** n <= b ** 0` by simp[]
547 \\ fs[EXP_BASE_LE_IFF]
548QED
549
550Theorem l2n_PAD_RIGHT_0[simp]:
551 0 < b ==> l2n b (PAD_RIGHT 0 h ls) = l2n b ls
552Proof
553 Induct_on`ls` \\ rw[l2n_def, PAD_RIGHT, l2n_eq_0, EVERY_GENLIST]
554 \\ fs[PAD_RIGHT, l2n_APPEND]
555 \\ fs[l2n_eq_0, EVERY_GENLIST]
556QED