patricia_castsScript.sml
1(* ========================================================================= *)
2(* FILE : patricia_castsScript.sml *)
3(* DESCRIPTION : Support for maps 'a word |-> 'b and string |-> 'a *)
4(* ========================================================================= *)
5Theory patricia_casts
6Ancestors
7 arithmetic list rich_list pred_set bit words patricia numposrep
8 ASCIInumbers
9Libs
10 Q wordsLib
11
12
13val _ = wordsLib.deprecate_word();
14val _ = ParseExtras.temp_loose_equality()
15
16(* ------------------------------------------------------------------------- *)
17
18val _ = set_fixity "IN_PTREEw" (Infix (NONASSOC, 425));
19val _ = set_fixity "IN_PTREEs" (Infix (NONASSOC, 425));
20val _ = set_fixity "INSERT_PTREEw" (Infixr 490);
21val _ = set_fixity "INSERT_PTREEs" (Infixr 490);
22val _ = set_fixity "UNION_PTREEw" (Infixl 500);
23val _ = set_fixity "UNION_PTREEs" (Infixl 500);
24
25Definition SKIP1_def: SKIP1 (STRING c s) = s
26End
27
28Definition string_to_num_def:
29 string_to_num s = s2n 256 ORD (STRING (CHR 1) s)
30End
31
32Definition num_to_string_def: num_to_string n = SKIP1 (n2s 256 CHR n)
33End
34
35Definition PEEKs_def: PEEKs t w = PEEK t (string_to_num w)
36End
37Definition FINDs_def: FINDs t w = THE (PEEKs t w)
38End
39Definition ADDs_def: ADDs t (w,d) = ADD t (string_to_num w,d)
40End
41Definition ADD_LISTs_def: ADD_LISTs = FOLDL ADDs
42End
43Definition REMOVEs_def: REMOVEs t w = REMOVE t (string_to_num w)
44End
45
46Overload "'" = Term`$PEEKs`
47Overload "|+" = Term`$ADDs`
48Overload "|++" = Term`$ADD_LISTs`
49Overload "\\\\" = Term`$REMOVEs`
50
51Definition TRAVERSEs_def:
52 TRAVERSEs t = MAP num_to_string (TRAVERSE t)
53End
54
55Definition KEYSs_def: KEYSs t = QSORT $< (TRAVERSEs t)
56End
57
58Definition IN_PTREEs_def:
59 $IN_PTREEs w t = (string_to_num w) IN_PTREE t
60End
61
62Definition INSERT_PTREEs_def:
63 $INSERT_PTREEs w t = (string_to_num w) INSERT_PTREE t
64End
65
66Definition STRINGSET_OF_PTREE_def:
67 STRINGSET_OF_PTREE (t:unit ptree) = LIST_TO_SET (TRAVERSEs t)
68End
69
70Definition PTREE_OF_STRINGSET_def:
71 PTREE_OF_STRINGSET t s = PTREE_OF_NUMSET t (IMAGE string_to_num s)
72End
73
74(* ......................................................................... *)
75
76Datatype: word_ptree = Word_ptree ('a -> unit) ('b ptree)
77End
78
79Type word_ptreeset = ``:('a, unit) word_ptree``
80
81Definition THE_PTREE_def[simp]: THE_PTREE (Word_ptree a t) = t
82End
83
84Definition SOME_PTREE_def[nocompute]: SOME_PTREE t = Word_ptree (K ()) t
85End
86
87Definition WordEmpty_def: WordEmpty = SOME_PTREE Empty
88End
89
90
91Definition PEEKw_def:
92 PEEKw (t:('a,'b) word_ptree) (w:'a word) = PEEK (THE_PTREE t) (w2n w)
93End
94
95Definition FINDw_def: FINDw t w = THE (PEEKw t w)
96End
97
98Definition ADDw_def:
99 ADDw (t:('a,'b) word_ptree) (w:'a word,d) =
100 SOME_PTREE (ADD (THE_PTREE t) (w2n w,d)) : ('a,'b) word_ptree
101End
102
103Definition ADD_LISTw_def: ADD_LISTw = FOLDL ADDw
104End
105
106Definition REMOVEw_def:
107 REMOVEw (t:('a,'b) word_ptree) (w:'a word) =
108 SOME_PTREE (REMOVE (THE_PTREE t) (w2n w)) : ('a,'b) word_ptree
109End
110
111Overload "'" = Term`$PEEKw`
112Overload "|+" = Term`$ADDw`
113Overload "|++" = Term`$ADD_LISTw`
114Overload "\\\\" = Term`$REMOVEw`
115
116Definition TRAVERSEw_def:
117 TRAVERSEw (t:('a, 'b) word_ptree) =
118 MAP (n2w:num->'a word) (TRAVERSE (THE_PTREE t))
119End
120
121Definition KEYSw_def: KEYSw t = QSORT $<+ (TRAVERSEw t)
122End
123
124Definition TRANSFORMw_def:
125 TRANSFORMw (f:'a->'b) (t:('c,'a) word_ptree) =
126 SOME_PTREE (TRANSFORM f (THE_PTREE t)) : ('c,'b) word_ptree
127End
128
129Definition EVERY_LEAFw_def:
130 EVERY_LEAFw P (t:('a, 'b) word_ptree) =
131 EVERY_LEAF (\k d. P (n2w k : 'a word) d) (THE_PTREE t)
132End
133
134Definition EXISTS_LEAFw_def:
135 EXISTS_LEAFw P (t:('a, 'b) word_ptree) =
136 EXISTS_LEAF (\k d. P (n2w k : 'a word) d) (THE_PTREE t)
137End
138
139Definition SIZEw_def: SIZEw t = SIZE (THE_PTREE t)
140End
141Definition DEPTHw_def: DEPTHw t = DEPTH (THE_PTREE t)
142End
143
144Definition IN_PTREEw_def:
145 $IN_PTREEw (w:'a word) (t:('a,unit) word_ptree) =
146 (w2n w) IN_PTREE (THE_PTREE t)
147End
148
149Definition INSERT_PTREEw_def:
150 $INSERT_PTREEw (w:'a word) (t:('a,unit) word_ptree) =
151 SOME_PTREE ((w2n w) INSERT_PTREE (THE_PTREE t)) : ('a,unit) word_ptree
152End
153
154Definition WORDSET_OF_PTREE_def:
155 WORDSET_OF_PTREE (t:('a,unit) word_ptree) = LIST_TO_SET (TRAVERSEw t)
156End
157
158Definition UNION_PTREEw_def:
159 $UNION_PTREEw t1 t2 =
160 SOME_PTREE ($UNION_PTREE (THE_PTREE t1) (THE_PTREE t2))
161End
162
163Definition PTREE_OF_WORDSET_def:
164 PTREE_OF_WORDSET (t:('a, unit) word_ptree) (s:'a word set) =
165 SOME_PTREE (PTREE_OF_NUMSET (THE_PTREE t) (IMAGE w2n s))
166 : ('a, unit) word_ptree
167End
168
169Overload "|++" = Term`$PTREE_OF_WORDSET`
170Overload "|++" = Term`$PTREE_OF_STRINGSET`
171
172(* ------------------------------------------------------------------------- *)
173
174Theorem ADD_INSERT_STRING =
175 (GEN_ALL o SIMP_CONV (srw_ss()) [GSYM INSERT_PTREEs_def, oneTheory.one])
176 ``ADDs t (w,v:unit)``;
177
178(*
179val PTREE_OF_STRINGSET_EMPTY = store_thm("PTREE_OF_STRINGSET_EMPTY",
180 `PTREE_OF_STRINGSET t {} = t`,
181 SRW_TAC [] [PTREE_OF_STRINGSET_def, PTREE_OF_NUMSET_EMPTY]);
182
183val PTREE_OF_STRINGSET_INSERT = store_thm("PTREE_OF_STRINGSET_INSERT",
184 `!t s. IS_PTREE t /\ FINITE s ==>
185 (PTREE_OF_STRINGSET t (x INSERT s) =
186 x INSERT_PTREEs (PTREE_OF_STRINGSET t s))`,
187 SRW_TAC [] [PTREE_OF_STRINGSET_def, INSERT_PTREEs_def, PTREE_OF_NUMSET_INSERT]
188);
189*)
190
191Theorem EVERY_MAP_ORD:
192 !l. EVERY ($> 256) (MAP ORD l)
193Proof
194 Induct \\ SRW_TAC [] [GREATER_DEF, stringTheory.ORD_BOUND]
195QED
196
197Theorem MAP_11:
198 !f l1 l2.
199 (!x y. (f x = f y) = (x = y)) ==>
200 ((MAP f l1 = MAP f l2) = (l1 = l2))
201Proof
202 Induct_on `l1` \\ Induct_on `l2` \\ SRW_TAC [] []
203QED
204
205Theorem REVERSE_11:
206 !l1 l2. ((REVERSE l1 = REVERSE l2) = (l1 = l2))
207Proof
208 Induct_on `l1` \\ Induct_on `l2`
209 \\ SRW_TAC [] [] \\ PROVE_TAC []
210QED
211
212Theorem string_to_num_11:
213 !s t. (string_to_num s = string_to_num t) = (s = t)
214Proof
215 REPEAT STRIP_TAC \\ EQ_TAC
216 \\ SRW_TAC [] [string_to_num_def, s2n_def]
217 \\ SPECL_THEN [`256`, `MAP ORD (REVERSE s)`,
218 `MAP ORD (REVERSE t)`]
219 (IMP_RES_TAC o SIMP_RULE (srw_ss()) [EVERY_MAP_ORD]) l2n_11
220 \\ FULL_SIMP_TAC (srw_ss()) [REVERSE_11,
221 (SIMP_RULE (srw_ss()) [stringTheory.ORD_11] o ISPEC `ORD`) MAP_11]
222QED
223
224Theorem n2l_NOT_NULL[local]:
225 !b n. ~(n2l b n = [])
226Proof SRW_TAC [] [Once n2l_def]
227QED
228
229Theorem STRING_SKIP1[local]:
230 !l c. EVERY ($> 256) l ==>
231 ((STRING c (SKIP1 (MAP CHR l)) = MAP CHR l) =
232 ~(l = []) /\ (l = ORD c::TL l))
233Proof
234 Induct \\ SRW_TAC [] [SKIP1_def]
235 \\ Cases_on `c` \\ SRW_TAC [ARITH_ss] [stringTheory.CHR_11]
236QED
237
238Theorem EVERY_CHR_LT_256[local]:
239 !n. EVERY ($> 256) (REVERSE (n2l 256 n))
240Proof
241 SRW_TAC [] [ALL_EL_REVERSE, n2l_BOUND]
242QED
243
244Theorem TL_APPEND[local]:
245 !l1 l2. ~(l1 = []) ==> (TL (l1 ++ l2) = TL l1 ++ l2)
246Proof
247 Induct \\ SRW_TAC [] []
248QED
249
250Theorem TL_REVERSE[local]:
251 !l. ~(l = []) ==> (TL (REVERSE l) = REVERSE (FRONT l))
252Proof
253 Induct \\ SRW_TAC [] [Once FRONT_DEF, TL_APPEND, REVERSE_EQ_NIL]
254QED
255
256Theorem TL_REVERSE_LAST[local]:
257 !l h. ~(l = []) ==> ((REVERSE l = h :: TL (REVERSE l)) = (h = LAST l))
258Proof
259 Induct \\ SRW_TAC [] [LAST_DEF] >- METIS_TAC []
260 \\ PAT_X_ASSUM `!h. P` IMP_RES_TAC
261 \\ NTAC 2 (POP_ASSUM (K ALL_TAC))
262 \\ POP_ASSUM (SPEC_THEN `h'` (SUBST1_TAC o SYM))
263 \\ SRW_TAC [] [TL_REVERSE, TL_APPEND, REVERSE_EQ_NIL]
264 \\ METIS_TAC [APPEND, APPEND_11]
265QED
266
267Theorem LENGTH_n2l_256[local]:
268 !n. 0 < LENGTH (n2l 256 n)
269Proof SRW_TAC [] [LENGTH_n2l]
270QED
271
272val LOG_ADD_COMM = ONCE_REWRITE_RULE [ADD_COMM] logrootTheory.LOG_ADD;
273
274Theorem STRING1_SKIP1[local]:
275 !n. 256 <= n /\ (n DIV 256 ** LOG 256 n = 1) ==>
276 (STRING (CHR 1) (SKIP1 (n2s 256 CHR n)) = n2s 256 CHR n)
277Proof
278 REPEAT STRIP_TAC
279 \\ `n = (n DIV (256 ** LOG 256 n)) * (256 ** LOG 256 n) +
280 n MOD (256 ** LOG 256 n)`
281 by METIS_TAC [DECIDE ``0 < 256``, DIVISION, ZERO_LT_EXP]
282 \\ POP_ASSUM SUBST1_TAC
283 \\ SRW_TAC [] [GSYM MAP_REVERSE, REVERSE_EQ_NIL, n2l_NOT_NULL, n2s_def,
284 STRING_SKIP1, EVERY_CHR_LT_256, TL_REVERSE_LAST]
285 \\ SRW_TAC [] [DECIDE ``0 < n ==> PRE n < n``, n2l_NOT_NULL,
286 GSYM EL_PRE_LENGTH, LENGTH_n2l_256, EL_n2l]
287 \\ SRW_TAC [ARITH_ss] [LENGTH_n2l, DIV_MULT_1, LOG_ADD_COMM]
288QED
289
290Theorem string_to_num_num_to_string[local]:
291 !n. (n = 1) \/ (256 <= n) /\ (n DIV 256 ** LOG 256 n = 1) ==>
292 (string_to_num (num_to_string n) = n)
293Proof
294 SRW_TAC [] [string_to_num_def, num_to_string_def] >- EVAL_TAC
295 \\ SRW_TAC [] [STRING1_SKIP1, stringTheory.ORD_CHR_RWT, s2n_n2s]
296QED
297
298Theorem s2n_STRING_STRING[local]:
299 !f b c1 c2 s.
300 1 < b /\ 0 < (f c1 MOD b) ==>
301 b <= s2n b f (STRING c1 (STRING c2 s))
302Proof
303 SRW_TAC [ARITH_ss] [EXP_ADD, s2n_def, l2n_def, Once l2n_APPEND]
304 \\ MATCH_MP_TAC (DECIDE ``a <= b ==> a <= b + c``)
305 \\ REWRITE_TAC [GSYM MULT_ASSOC]
306 \\ SRW_TAC [ARITH_ss] [ZERO_LESS_MULT, ZERO_LT_EXP]
307QED
308
309val s2n_STRING_STRING1 =
310 (SIMP_RULE (srw_ss()) [EVAL ``ORD (CHR 1)``] o
311 SPECL [`ORD`,`256`,`CHR 1`]) s2n_STRING_STRING;
312
313Theorem IMAGE_string_to_num:
314 !n. (n = 1) \/ (256 <= n) /\ (n DIV 256 ** LOG 256 n = 1) =
315 n IN IMAGE string_to_num UNIV
316Proof
317 SRW_TAC [] [IN_IMAGE] \\ EQ_TAC \\ SRW_TAC [] []
318 >| [
319 EXISTS_TAC `""` \\ EVAL_TAC,
320 METIS_TAC [string_to_num_num_to_string],
321 `(x = "") \/ ?c s. x = STRING c s`
322 by METIS_TAC [TypeBase.nchotomy_of ``:string``]
323 \\ SRW_TAC [] [string_to_num_def, s2n_STRING_STRING1]
324 >- EVAL_TAC
325 \\ DISJ2_TAC
326 \\ `LENGTH (MAP ORD (REVERSE s) ++ [ORD c]) = LENGTH s + 1`
327 by SRW_TAC [] []
328 \\ `l2n 256 (MAP ORD (REVERSE s) ++ [ORD c]) < 256 ** (LENGTH s + 1)`
329 by METIS_TAC [l2n_lt, DECIDE ``0 < 256``]
330 \\ SRW_TAC [ARITH_ss] [s2n_def, LOG_ADD_COMM, DIV_MULT_1,
331 SPECL [`256`, `a ++ b`] l2n_APPEND]
332 ]
333QED
334
335Theorem string_to_num_num_to_string =
336 REWRITE_RULE [IMAGE_string_to_num] string_to_num_num_to_string;
337
338Theorem num_to_string_string_to_num:
339 !s. num_to_string (string_to_num s) = s
340Proof
341 SRW_TAC [] [GSYM string_to_num_11, string_to_num_num_to_string, IMAGE_IN]
342QED
343
344(* ------------------------------------------------------------------------- *)
345
346Theorem ADD_INSERT_WORD =
347 (GEN_ALL o SIMP_CONV (srw_ss()) [GSYM INSERT_PTREEw_def, oneTheory.one])
348 ``ADDw t (w,v:unit)``;
349
350Theorem THE_PTREE_SOME_PTREE[simp]:
351 !t. THE_PTREE (SOME_PTREE t) = t
352Proof
353 SRW_TAC [] [SOME_PTREE_def]
354QED
355
356
357(*
358val PTREE_OF_WORDSET_EMPTY = store_thm("PTREE_OF_WORDSET_EMPTY",
359 `PTREE_OF_WORDSET (SOME_PTREE t) {} = SOME_PTREE t`,
360 SRW_TAC [] [PTREE_OF_WORDSET_def, PTREE_OF_NUMSET_EMPTY]);
361
362val PTREE_OF_WORDSET_INSERT = store_thm("PTREE_OF_WORDSET_INSERT",
363 `!t s. IS_PTREE (THE_PTREE t) /\ FINITE s ==>
364 (PTREE_OF_WORDSET t (x INSERT s) =
365 x INSERT_PTREEw (PTREE_OF_WORDSET t s))`,
366 SRW_TAC [] [PTREE_OF_WORDSET_def, INSERT_PTREEw_def, PTREE_OF_NUMSET_INSERT]);
367
368val PTREE_OF_WORDSET_UNION = store_thm("PTREE_OF_WORDSET_UNION",
369 `!t s1 s2. IS_PTREE (THE_PTREE t) /\ FINITE s1 /\ FINITE s2 ==>
370 (PTREE_OF_WORDSET t (s1 UNION s2) =
371 PTREE_OF_WORDSET (PTREE_OF_WORDSET t s1) s2)`,
372 SRW_TAC [] [PTREE_OF_WORDSET_def, UNION_PTREEw_def, PTREE_OF_NUMSET_UNION]);
373*)
374
375(* ------------------------------------------------------------------------- *)
376
377val _ = add_listform {leftdelim = [TOK "+{"], rightdelim = [TOK "}+"],
378 separator = [TOK ";", BreakSpace(1,0)],
379 cons = "INSERT_PTREEw", nilstr = "WordEmpty",
380 block_info = (PP.INCONSISTENT, 0)};
381
382val _ = add_listform {leftdelim = [TOK "-{"], rightdelim = [TOK "}-"],
383 separator = [TOK ";", BreakSpace(1,0)],
384 cons = "INSERT_PTREEs", nilstr = "Empty",
385 block_info = (PP.INCONSISTENT, 0)};
386
387val _ = computeLib.add_persistent_funs
388 ["pred_set.IMAGE_EMPTY",
389 "pred_set.IMAGE_INSERT",
390 "pred_set.IMAGE_UNION",
391 "ADD_INSERT_WORD",
392 "ADD_INSERT_STRING",
393 "THE_PTREE_SOME_PTREE"];
394
395(* ------------------------------------------------------------------------- *)