ASCIInumbersScript.sml

1(* =========================================================================
2   String-to-from-Number maps
3   ========================================================================= *)
4Theory ASCIInumbers
5Ancestors
6  string numposrep arithmetic list combin pair num rich_list
7  logroot bit
8Libs
9  metisLib simpLib listSimps stringLib listSimps
10
11
12(* ------------------------------------------------------------------------- *)
13
14Definition s2n_def:
15  s2n b f (s:string) = l2n b (MAP f (REVERSE s))
16End
17
18Definition n2s_def[nocompute]:
19  n2s b f n : string = REVERSE (MAP f (n2l b n))
20End
21
22Definition HEX[nocompute]:
23  HEX n = if n < 10 then CHR (ORD #"0" + n) else
24          if n < 16 then CHR (ORD #"A" + (n - 10)) else CHR 0
25End
26
27Theorem HEX_def[compute]:
28  (HEX 0 = #"0") /\
29  (HEX 1 = #"1") /\
30  (HEX 2 = #"2") /\
31  (HEX 3 = #"3") /\
32  (HEX 4 = #"4") /\
33  (HEX 5 = #"5") /\
34  (HEX 6 = #"6") /\
35  (HEX 7 = #"7") /\
36  (HEX 8 = #"8") /\
37  (HEX 9 = #"9") /\
38  (HEX 10 = #"A") /\
39  (HEX 11 = #"B") /\
40  (HEX 12 = #"C") /\
41  (HEX 13 = #"D") /\
42  (HEX 14 = #"E") /\
43  (HEX 15 = #"F")
44Proof
45  rewrite_tac [HEX] \\ EVAL_TAC
46QED
47
48Definition UNHEX[nocompute]:
49  UNHEX c =
50    let n = ORD c in
51      if ORD #"0" <= n /\ n <= ORD #"9" then n - ORD #"0" else
52      if ORD #"a" <= n /\ n <= ORD #"f" then 10 + n - ORD #"a" else
53      if ORD #"A" <= n /\ n <= ORD #"F" then 10 + n - ORD #"A" else 0
54End
55
56Theorem UNHEX_def[compute]:
57  UNHEX #"0" = 0 /\ UNHEX #"1" = 1 /\
58  UNHEX #"2" = 2 /\ UNHEX #"3" = 3 /\
59  UNHEX #"4" = 4 /\ UNHEX #"5" = 5 /\
60  UNHEX #"6" = 6 /\ UNHEX #"7" = 7 /\
61  UNHEX #"8" = 8 /\ UNHEX #"9" = 9 /\
62  UNHEX #"a" = 10 /\ UNHEX #"b" = 11 /\ UNHEX #"c" = 12 /\
63  UNHEX #"d" = 13 /\ UNHEX #"e" = 14 /\ UNHEX #"f" = 15 /\
64  UNHEX #"A" = 10 /\ UNHEX #"B" = 11 /\ UNHEX #"C" = 12 /\
65  UNHEX #"D" = 13 /\ UNHEX #"E" = 14 /\ UNHEX #"F" = 15
66Proof
67  rewrite_tac [UNHEX] \\ EVAL_TAC
68QED
69
70Definition num_from_bin_string_def:   num_from_bin_string = s2n 2 UNHEX
71End
72Definition num_from_oct_string_def:   num_from_oct_string = s2n 8 UNHEX
73End
74Definition num_from_dec_string_def:   num_from_dec_string = s2n 10 UNHEX
75End
76Definition num_from_hex_string_def:   num_from_hex_string = s2n 16 UNHEX
77End
78
79Definition num_to_bin_string_def[nocompute]: num_to_bin_string = n2s 2 HEX
80End
81Definition num_to_oct_string_def[nocompute]: num_to_oct_string = n2s 8 HEX
82End
83Definition num_to_dec_string_def[nocompute]: num_to_dec_string = n2s 10 HEX
84End
85Definition num_to_hex_string_def[nocompute]: num_to_hex_string = n2s 16 HEX
86End
87
88Theorem s2n_leading_zeroes:
89  0 < b ==> s2n b UNHEX (#"0" :: t) = s2n b UNHEX t
90Proof
91  simp[s2n_def, UNHEX_def, l2n_APPEND, l2n_def]
92QED
93
94Theorem num_from_X_string_leading_zeroes[simp]:
95  num_from_bin_string (#"0" :: t) = num_from_bin_string t /\
96  num_from_oct_string (#"0" :: t) = num_from_oct_string t /\
97  num_from_dec_string (#"0" :: t) = num_from_dec_string t /\
98  num_from_hex_string (#"0" :: t) = num_from_hex_string t
99Proof
100  simp[num_from_bin_string_def, num_from_oct_string_def,
101       num_from_dec_string_def, num_from_hex_string_def, s2n_leading_zeroes]
102QED
103
104Theorem num_to_dec_string_compute[compute]:
105  num_to_dec_string = n2lA [] HEX 10
106Proof
107  simp[num_to_dec_string_def, n2lA_n2l, n2s_def, FUN_EQ_THM, MAP_REVERSE]
108QED
109
110Definition fromBinString_def:
111   fromBinString s =
112      if s <> "" /\ EVERY (\c. (c = #"0") \/ (c = #"1")) s then
113         SOME (num_from_bin_string s)
114      else NONE
115End
116
117Definition fromDecString_def:
118   fromDecString s =
119      if s <> "" /\ EVERY isDigit s then SOME (num_from_dec_string s) else NONE
120End
121
122Definition fromHexString_def:
123   fromHexString s =
124      if s <> "" /\ EVERY isHexDigit s then
125         SOME (num_from_hex_string s)
126      else NONE
127End
128
129(* ------------------------------------------------------------------------- *)
130
131Theorem s2n_compute:
132   s2n b f s = l2n b (MAP f (REVERSE (EXPLODE s)))
133Proof
134  SRW_TAC [] [stringTheory.IMPLODE_EXPLODE_I, s2n_def]
135QED
136
137Theorem n2s_compute:
138   n2s b f n = IMPLODE (REVERSE (MAP f (n2l b n)))
139Proof
140  SRW_TAC [] [stringTheory.IMPLODE_EXPLODE_I, n2s_def]
141QED
142
143val LESS_THM =
144  CONV_RULE numLib.SUC_TO_NUMERAL_DEFN_CONV prim_recTheory.LESS_THM;
145
146Theorem UNHEX_HEX:
147    !n. n < 16 ==> (UNHEX (HEX n) = n)
148Proof SRW_TAC [] [LESS_THM] \\ EVAL_TAC
149QED
150
151Theorem HEX_UNHEX:
152    !c. isHexDigit c ==> (HEX (UNHEX c) = toUpper c)
153Proof
154  Cases
155  \\ SRW_TAC [] [isHexDigit_def]
156  \\ Q.PAT_ASSUM `n < 256` (K ALL_TAC)
157  >| [`n < 58` by DECIDE_TAC, `n < 103` by DECIDE_TAC,
158      `n < 71` by DECIDE_TAC]
159  \\ FULL_SIMP_TAC std_ss [LESS_THM]
160  \\ FULL_SIMP_TAC arith_ss []
161  \\ EVAL_TAC
162QED
163
164Theorem DEC_UNDEC:
165    !c. isDigit c ==> (HEX (UNHEX c) = c)
166Proof
167  Cases
168  \\ SRW_TAC [] [isDigit_def]
169  \\ Q.PAT_ASSUM `n < 256` (K ALL_TAC)
170  \\ `n < 58` by DECIDE_TAC
171  \\ FULL_SIMP_TAC std_ss [LESS_THM]
172  \\ FULL_SIMP_TAC arith_ss []
173  \\ EVAL_TAC
174QED
175
176Theorem MAP_ID[local]:
177   !l. EVERY (\x. f x = x) l ==> (MAP f l = l)
178Proof
179  Induct \\ SRW_TAC [] []
180QED
181
182Theorem s2n_n2s:
183   !c2n n2c b n. 1 < b /\ (!x. x < b ==> (c2n (n2c x) = x)) ==>
184      (s2n b c2n (n2s b n2c n) = n)
185Proof
186  SRW_TAC [] [s2n_def, n2s_def, MAP_MAP_o]
187  \\ `MAP (c2n o n2c) (n2l b n) = n2l b n`
188        suffices_by SRW_TAC [ARITH_ss] [l2n_n2l]
189  \\ MATCH_MP_TAC MAP_ID \\ simp[]
190  \\ `!x. ($> b) x ==> (\x. c2n (n2c x) = x) x` by METIS_TAC [GREATER_DEF]
191  \\ IMP_RES_TAC EVERY_MONOTONIC
192  \\ POP_ASSUM MATCH_MP_TAC
193  \\ METIS_TAC [n2l_BOUND, DECIDE ``1 < b ==> 0 < b``]
194QED
195
196(* ......................................................................... *)
197
198Theorem REVERSE_LASTN[local]:
199   !n l. n <= LENGTH l ==> (LASTN n l = REVERSE (TAKE n (REVERSE l)))
200Proof
201  SRW_TAC [] [FIRSTN_REVERSE]
202QED
203
204Theorem n2s_s2n:
205   !c2n n2c b s.
206     1 < b /\ EVERY ($> b o c2n) s ==>
207     (n2s b n2c (s2n b c2n s) =
208       if s2n b c2n s = 0 then STRING (n2c 0) ""
209       else MAP (n2c o c2n) (LASTN (SUC (LOG b (s2n b c2n s))) s))
210Proof
211  SRW_TAC [] [s2n_def, n2s_def]
212    >- SRW_TAC [ARITH_ss] [l2n_def, Once n2l_def]
213    \\ Q.ABBREV_TAC `l = MAP c2n (REVERSE s)`
214    \\ `~(l = [])` by (STRIP_TAC \\ FULL_SIMP_TAC std_ss [l2n_def])
215    \\ `EVERY ($> b) l` by (Q.UNABBREV_TAC `l`
216          \\ SRW_TAC [] [EVERY_MAP, ALL_EL_REVERSE,
217                         simpLib.SIMP_PROVE std_ss [FUN_EQ_THM]
218                           ``(\x:char. b:num > c2n x) = ($> b o c2n)``])
219    \\ SRW_TAC [] [n2l_l2n]
220    \\ IMP_RES_TAC LENGTH_l2n
221    \\ `SUC (LOG b (l2n b l)) <= LENGTH s`
222    by METIS_TAC [LENGTH_MAP, LENGTH_REVERSE]
223    \\ Q.UNABBREV_TAC `l`
224    \\ SRW_TAC [] [GSYM MAP_REVERSE, REVERSE_LASTN, GSYM MAP_TAKE, MAP_MAP_o]
225QED
226
227(* ----------------------------------------------------------------------
228    toString and toNum as overloads for the above (decimal notation)
229   ---------------------------------------------------------------------- *)
230
231Overload toString = “num_to_dec_string”
232Overload toNum = “num_from_dec_string”
233
234Theorem toNum_toString[simp]:
235  !n. toNum (toString n) = n
236Proof
237  STRIP_TAC THEN
238  SRW_TAC [][num_to_dec_string_def, num_from_dec_string_def] THEN
239  MATCH_MP_TAC s2n_n2s THEN SIMP_TAC (srw_ss()) [] THEN
240  Q.X_GEN_TAC `n` THEN STRIP_TAC THEN
241  `(n = 0) \/ (n = 1) \/ (n = 2) \/ (n = 3) \/ (n = 4) \/
242   (n = 5) \/ (n = 6) \/ (n = 7) \/ (n = 8) \/ (n = 9)` by DECIDE_TAC THEN
243  SRW_TAC [][HEX_def, UNHEX_def]
244QED
245
246Theorem toString_toNum_cancel = toNum_toString
247
248Theorem toString_inj[simp]: !n m. toString n = toString m <=> n = m
249Proof METIS_TAC [toNum_toString]
250QED
251Theorem toString_11 = toString_inj
252
253Theorem STRCAT_toString_inj:
254     !n m s. (STRCAT s (toString n) = STRCAT s (toString m)) = (n = m)
255Proof
256   SRW_TAC [] []
257QED
258
259(* ------------------------------------------------------------------------- *)
260
261Theorem BIT_num_from_bin_string:
262    !x s. EVERY ($> 2 o UNHEX) s /\ x < STRLEN s ==>
263          (BIT x (num_from_bin_string s) =
264           (UNHEX (SUB (s, PRE (STRLEN s - x))) = 1))
265Proof
266   SRW_TAC [ARITH_ss] [num_from_bin_string_def, s2n_def]
267   \\ `x < LENGTH (MAP UNHEX (REVERSE s)) /\ x < LENGTH (REVERSE s)`
268   by SRW_TAC [] [LENGTH_MAP, LENGTH_REVERSE]
269   \\ `EVERY ($> 2) (MAP UNHEX (REVERSE s))`
270   by SRW_TAC [] [EVERY_MAP, ALL_EL_REVERSE,
271                  simpLib.SIMP_PROVE std_ss [FUN_EQ_THM]
272                     ``(\x. 2 > UNHEX x) = ($> 2 o UNHEX)``]
273   \\ SRW_TAC [ARITH_ss]
274        [l2n_DIGIT, EL_MAP, EL_REVERSE, SUC_SUB, BIT_def, BITS_THM, SUB_def]
275QED
276
277Theorem SUB_num_to_bin_string:
278    !x n. x < STRLEN (num_to_bin_string n) ==>
279          (SUB (num_to_bin_string n, x) =
280           HEX (BITV n (PRE (STRLEN (num_to_bin_string n) - x))))
281Proof
282   SRW_TAC [ARITH_ss]
283       [num_to_bin_string_def, n2s_def, SUB_def, BITV_def, BIT_def, BITS_THM,
284        LENGTH_REVERSE, LENGTH_MAP, SUC_SUB]
285   \\ `PRE (LENGTH (n2l 2 n) - x) < LENGTH (n2l 2 n)`
286   by (SIMP_TAC arith_ss [PRE_SUB1] \\ SIMP_TAC arith_ss [LENGTH_n2l])
287   \\ SRW_TAC [ARITH_ss] [EL_REVERSE, EL_MAP, EL_n2l, SUC_SUB]
288QED
289
290val tac =
291   SRW_TAC [ARITH_ss]
292    [FUN_EQ_THM, UNHEX_HEX, s2n_n2s,
293     num_from_bin_string_def, num_from_oct_string_def, num_from_dec_string_def,
294     num_from_hex_string_def, num_to_bin_string_def, num_to_oct_string_def,
295     num_to_dec_string_def, num_to_hex_string_def]
296
297Theorem num_bin_string:
298   num_from_bin_string o num_to_bin_string = I
299Proof tac
300QED
301Theorem num_oct_string:
302   num_from_oct_string o num_to_oct_string = I
303Proof tac
304QED
305Theorem num_dec_string:
306   num_from_dec_string o num_to_dec_string = I
307Proof tac
308QED
309Theorem num_hex_string:
310   num_from_hex_string o num_to_hex_string = I
311Proof tac
312QED
313
314(* ------------------------------------------------------------------------- *)
315
316fun nil_tac n =
317  rw[num_to_bin_string_def,
318     num_to_oct_string_def,
319     num_to_dec_string_def,
320     num_to_hex_string_def]
321  \\ rw[n2s_def]
322  \\ qspecl_then[n,`n`]mp_tac LENGTH_n2l
323  \\ rw[] \\ CCONTR_TAC \\ fs[];
324
325Theorem num_to_bin_string_nil[simp]:
326  ~(num_to_bin_string n = [])
327Proof nil_tac `2`
328QED
329
330Theorem num_to_oct_string_nil[simp]:
331  ~(num_to_oct_string n = [])
332Proof nil_tac `8`
333QED
334
335Theorem num_to_dec_string_nil[simp]:
336  ~(num_to_dec_string n = [])
337Proof nil_tac `10`
338QED
339
340Theorem num_to_hex_string_nil[simp]:
341  ~(num_to_hex_string n = [])
342Proof nil_tac `16`
343QED
344
345
346Theorem isDigit_HEX:
347  !n. n < 10 ==> isDigit (HEX n)
348Proof
349  REWRITE_TAC[GSYM MEM_COUNT_LIST]
350  \\ gen_tac
351  \\ CONV_TAC(LAND_CONV EVAL)
352  \\ simp[]
353  \\ strip_tac \\ BasicProvers.VAR_EQ_TAC
354  \\ EVAL_TAC
355QED
356
357Theorem isHexDigit_HEX:
358  !n. n < 16 ==> isHexDigit (HEX n) /\
359                 (isAlpha (HEX n) ==> isUpper (HEX n))
360Proof
361  REWRITE_TAC[GSYM MEM_COUNT_LIST]
362  \\ gen_tac
363  \\ CONV_TAC(LAND_CONV EVAL)
364  \\ strip_tac \\ BasicProvers.VAR_EQ_TAC
365  \\ EVAL_TAC
366QED
367
368Theorem EVERY_isDigit_num_to_dec_string:
369  !n. EVERY isDigit (num_to_dec_string n)
370Proof
371  rw[num_to_dec_string_def,n2s_def]
372  \\ rw[EVERY_REVERSE,EVERY_MAP]
373  \\ simp[EVERY_MEM]
374  \\ gen_tac\\ strip_tac
375  \\ match_mp_tac isDigit_HEX
376  \\ qspecl_then[`10`,`n`]mp_tac n2l_BOUND
377  \\ rw[EVERY_MEM]
378  \\ res_tac
379  \\ decide_tac
380QED
381
382Theorem EVERY_isHexDigit_num_to_hex_string:
383  !n. EVERY (\c. isHexDigit c /\ (isAlpha c ==> isUpper c))
384            (num_to_hex_string n)
385Proof
386  rw[num_to_hex_string_def,n2s_def]
387  \\ rw[EVERY_REVERSE,EVERY_MAP]
388  \\ simp[EVERY_MEM]
389  \\ gen_tac\\ strip_tac
390  \\ match_mp_tac isHexDigit_HEX
391  \\ qspecl_then[`16`,`n`]mp_tac n2l_BOUND
392  \\ rw[EVERY_MEM]
393  \\ res_tac
394  \\ decide_tac
395QED
396
397Theorem LENGTH_num_to_dec_string:
398  LENGTH (num_to_dec_string n) = if n = 0 then 1 else LOG 10 n + 1
399Proof
400  simp[num_to_dec_string_def, n2s_def, LENGTH_n2l]
401QED
402
403Theorem LENGTH_num_to_hex_string:
404  LENGTH (num_to_hex_string n) = if n = 0 then 1 else LOG 16 n + 1
405Proof
406  simp[num_to_hex_string_def, n2s_def, LENGTH_n2l]
407QED
408
409Theorem LENGTH_num_to_bin_string:
410  LENGTH (num_to_bin_string n) = if n = 0 then 1 else LOG 2 n + 1
411Proof
412  simp[num_to_bin_string_def, n2s_def, LENGTH_n2l]
413QED
414
415Theorem LENGTH_num_to_oct_string:
416  LENGTH (num_to_oct_string n) = if n = 0 then 1 else LOG 8 n + 1
417Proof
418  simp[num_to_oct_string_def, n2s_def, LENGTH_n2l]
419QED