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