string_numScript.sml
1Theory string_num
2Ancestors
3 string arithmetic
4Libs
5 markerLib
6
7Definition n2s_def:
8 n2s n = if n = 0 then ""
9 else let r0 = n MOD 256 in
10 let r = if r0 = 0 then 256 else r0 in
11 let s0 = n2s ((n - r) DIV 256)
12 in
13 STRING (CHR (r - 1)) s0
14End
15
16Definition s2n_def:
17 (s2n "" = 0) /\
18 (s2n (STRING c s) = s2n s * 256 + ORD c + 1)
19End
20
21Theorem s2n_n2s[simp]:
22 !n. s2n (n2s n) = n
23Proof
24 completeInduct_on `n` THEN ONCE_REWRITE_TAC [n2s_def] THEN
25 SRW_TAC [][] THEN SRW_TAC [][s2n_def] THEN
26 `n MOD 256 < 256` by SRW_TAC [][DIVISION] THEN
27 `(n - r) DIV 256 < n`
28 by (MATCH_MP_TAC LESS_EQ_LESS_TRANS THEN
29 Q.EXISTS_TAC `n DIV 256` THEN
30 SRW_TAC [ARITH_ss][DIV_LE_MONOTONE,
31 DIV_LESS]) THEN
32 `s2n s0 = (n - r) DIV 256` by (SRW_TAC [][Abbr`s0`]) THEN
33 `r - 1 < 256`
34 by (SRW_TAC [][Abbr`r`, Abbr`r0`] THEN
35 DECIDE_TAC) THEN
36 POP_ASSUM (fn th => SRW_TAC [][th]) THEN
37 `0 < r` by SRW_TAC [ARITH_ss][Abbr`r`] THEN
38 Cases_on `r0 = 0` THENL [
39 `?q. n = q * 256`
40 by METIS_TAC [DIVISION, ADD_CLAUSES,
41 DECIDE ``0 < 256``] THEN
42 `~(q = 0)` by (STRIP_TAC THEN FULL_SIMP_TAC (srw_ss()) []) THEN
43 `r = 256` by SRW_TAC [][Abbr`r`] THEN
44 RM_ALL_ABBREVS_TAC THEN FULL_SIMP_TAC (srw_ss()) [] THEN
45 `q * 256 - 256 = (q - 1) * 256` by DECIDE_TAC THEN
46 SRW_TAC [][MULT_DIV] THEN
47 DECIDE_TAC,
48
49 Q.UNABBREV_TAC `r` THEN FULL_SIMP_TAC (srw_ss()) [] THEN
50 `(n - r0) DIV 256 = n DIV 256`
51 by (MATCH_MP_TAC DIV_UNIQUE THEN
52 Q.EXISTS_TAC `0` THEN
53 SRW_TAC [][Abbr`r0`, SUB_RIGHT_EQ] THEN
54 METIS_TAC [DECIDE ``0 < 256``, DIVISION, ADD_COMM]) THEN
55 SRW_TAC [ARITH_ss][MULT_DIV, Abbr`r0`] THEN
56 METIS_TAC [DECIDE ``0 < 256``, DIVISION, MULT_COMM]
57 ]
58QED
59
60Theorem n2s_s2n[simp]:
61 n2s (s2n s) = s
62Proof
63 Induct_on `s` THEN ASM_SIMP_TAC (srw_ss()) [s2n_def, Once n2s_def] THEN
64 Q.X_GEN_TAC `c` THEN SRW_TAC [][] THEN
65 `r0 = (ORD c + 1) MOD 256`
66 by (SRW_TAC [][Abbr`r0`] THEN
67 SRW_TAC [][GSYM ADD_ASSOC, MOD_TIMES]) THEN
68 RM_ABBREV_TAC "r0" THEN
69 Cases_on `r0 = 0` THENL [
70 `ORD c < 256` by SRW_TAC [][ORD_BOUND] THEN
71 `?q. ORD c + 1 = q * 256`
72 by METIS_TAC [DIVISION, ADD_CLAUSES, DECIDE ``0 < 256``] THEN
73 `q = 1` by DECIDE_TAC THEN
74 FULL_SIMP_TAC (srw_ss()) [] THEN
75 `ORD c = 255` by DECIDE_TAC THEN
76 `c = CHR 255` by METIS_TAC [CHR_ORD] THEN
77 SRW_TAC [ARITH_ss][Abbr`r`, Abbr`s0`] THEN
78 METIS_TAC [MULT_DIV, MULT_COMM, DECIDE ``0 < 256``],
79
80 Q.UNABBREV_TAC `r` THEN FULL_SIMP_TAC (srw_ss()) [] THEN
81 `ORD c + 1 < 256`
82 by (SPOSE_NOT_THEN ASSUME_TAC THEN
83 Q.SPEC_THEN `c` ASSUME_TAC ORD_BOUND THEN
84 `ORD c = 255` by DECIDE_TAC THEN
85 FULL_SIMP_TAC (srw_ss()) []) THEN
86 FULL_SIMP_TAC (srw_ss() ++ ARITH_ss) [DIVISION, CHR_ORD] THEN
87 METIS_TAC [MULT_COMM, MULT_DIV, DECIDE ``0 < 256``]
88 ]
89QED
90
91Theorem n2s_11[simp]:
92 (n2s x = n2s y) = (x = y)
93Proof
94 METIS_TAC [s2n_n2s]
95QED
96Theorem s2n_11[simp]:
97 (s2n x = s2n y) = (x = y)
98Proof
99 METIS_TAC [n2s_s2n]
100QED
101
102Theorem n2s_onto:
103 !s. ?n. s = n2s n
104Proof
105 METIS_TAC [n2s_s2n]
106QED
107
108Theorem s2n_onto:
109 !n. ?s. n = s2n s
110Proof
111 METIS_TAC [s2n_n2s]
112QED
113
114
115
116Definition n2nsum_def:
117 n2nsum n = if ODD n then INL (n DIV 2) else INR (n DIV 2)
118End
119
120Definition nsum2n_def[simp]:
121 (nsum2n (INL n) = 2 * n + 1) /\
122 (nsum2n (INR n) = 2 * n)
123End
124
125Theorem div_lemma[local]:
126 (2 * x DIV 2 = x) /\ ((2 * x + 1) DIV 2 = x)
127Proof
128 `0 < 2 /\ (1 DIV 2 = 0)` by simp[] >>
129 metis_tac[MULT_DIV, ADD_DIV_ADD_DIV, MULT_COMM, ADD_CLAUSES]
130QED
131
132Theorem odd_lemma[local]:
133 (ODD x ==> (2 * (x DIV 2) + 1 = x)) /\
134 (~ODD x ==> (2 * (x DIV 2) = x))
135Proof
136 conj_tac
137 >- dsimp[ODD_EXISTS, ADD1, div_lemma]
138 >- dsimp[GSYM EVEN_ODD, EVEN_EXISTS, div_lemma]
139QED
140
141Theorem n2nsum_nsum2n[simp]:
142 n2nsum (nsum2n ns) = ns
143Proof
144 Cases_on `ns` >> simp[n2nsum_def, div_lemma, ODD_ADD, ODD_MULT]
145QED
146
147Theorem nsum2n_n2nsum[simp]:
148 nsum2n (n2nsum n) = n
149Proof
150 rw[n2nsum_def, odd_lemma]
151QED
152
153Definition s2ssum_def:
154 s2ssum s = SUM_MAP n2s n2s (n2nsum (s2n s))
155End
156
157Definition ssum2s_def:
158 ssum2s sm = n2s (nsum2n (SUM_MAP s2n s2n sm))
159End
160
161Theorem sumpp_compose[local]:
162 SUM_MAP f g (SUM_MAP a b x) = SUM_MAP (f o a) (g o b) x
163Proof
164 Cases_on `x` >> simp[]
165QED
166
167Theorem sumpp_I[local]:
168 SUM_MAP (\x. x) (\x. x) y = y
169Proof
170 Cases_on `y` >> simp[]
171QED
172
173Theorem s2ssum_ssum2s[simp]:
174 s2ssum (ssum2s sm) = sm
175Proof
176 simp[s2ssum_def, ssum2s_def, sumpp_compose, combinTheory.o_DEF, sumpp_I]
177QED
178
179Theorem ssum2s_s2ssum[simp]:
180 ssum2s (s2ssum s) = s
181Proof
182 simp[s2ssum_def, ssum2s_def, sumpp_compose, combinTheory.o_DEF, sumpp_I]
183QED