1open HolKernel Parse boolLib bossLib; 2open arithmeticTheory 3open logrootTheory 4open listTheory 5open alistTheory 6open pred_setTheory 7open dep_rewrite 8 9val _ = new_theory "sptree"; 10 11(* A log-time random-access, extensible array implementation with union. 12 13 The "array" can be gappy: there doesn't have to be an element at 14 any particular index, and, being a finite thing, there is obviously 15 a maximum index past which there are no elements at all. It is 16 possible to update at an index past the current maximum index. It 17 is also possible to delete values at any index. 18 19 Should EVAL well. 20 21 The insert, delete and union operations all preserve a 22 well-formedness condition ("wf") that ensures there is only one 23 possible representation for any given finite-map. 24 25 It is tricky to traverse the array and extract a list of elements. 26 There are three array->list operations defined: 27 - toSortedAList: produces an assocation list in index order. 28 - toAList: produces an association list in a mixed-up order. Defined via 29 foldi, and related to foldi and mapi by theorems. Slowest to EVAL. 30 - toList: roughly equals MAP SND (toAList t), although in a different mixed 31 up order. By far the fastest to EVAL. 32*) 33 34val _ = Datatype`spt = LN | LS 'a | BN spt spt | BS spt 'a spt` 35(* Leaf-None, Leaf-Some, Branch-None, Branch-Some *) 36 37Type num_map[pp] = ���:'a spt��� 38Type num_set[pp] = ���:unit spt��� 39 40val _ = overload_on ("isEmpty", ``\t. t = LN``) 41 42val wf_def = Define` 43 (wf LN <=> T) /\ 44 (wf (LS a) <=> T) /\ 45 (wf (BN t1 t2) <=> wf t1 /\ wf t2 /\ ~(isEmpty t1 /\ isEmpty t2)) /\ 46 (wf (BS t1 a t2) <=> wf t1 /\ wf t2 /\ ~(isEmpty t1 /\ isEmpty t2)) 47`; 48 49fun tzDefine s q = Lib.with_flag (computeLib.auto_import_definitions,false) (tDefine s q) 50val lookup_def = tzDefine "lookup" ` 51 (lookup k LN = NONE) /\ 52 (lookup k (LS a) = if k = 0 then SOME a else NONE) /\ 53 (lookup k (BN t1 t2) = 54 if k = 0 then NONE 55 else lookup ((k - 1) DIV 2) (if EVEN k then t1 else t2)) /\ 56 (lookup k (BS t1 a t2) = 57 if k = 0 then SOME a 58 else lookup ((k - 1) DIV 2) (if EVEN k then t1 else t2)) 59` (WF_REL_TAC `measure FST` >> simp[DIV_LT_X]) 60 61val insert_def = tzDefine "insert" ` 62 (insert k a LN = if k = 0 then LS a 63 else if EVEN k then BN (insert ((k-1) DIV 2) a LN) LN 64 else BN LN (insert ((k-1) DIV 2) a LN)) /\ 65 (insert k a (LS a') = 66 if k = 0 then LS a 67 else if EVEN k then BS (insert ((k-1) DIV 2) a LN) a' LN 68 else BS LN a' (insert ((k-1) DIV 2) a LN)) /\ 69 (insert k a (BN t1 t2) = 70 if k = 0 then BS t1 a t2 71 else if EVEN k then BN (insert ((k - 1) DIV 2) a t1) t2 72 else BN t1 (insert ((k - 1) DIV 2) a t2)) /\ 73 (insert k a (BS t1 a' t2) = 74 if k = 0 then BS t1 a t2 75 else if EVEN k then BS (insert ((k - 1) DIV 2) a t1) a' t2 76 else BS t1 a' (insert ((k - 1) DIV 2) a t2)) 77` (WF_REL_TAC `measure FST` >> simp[DIV_LT_X]); 78 79val insert_ind = theorem "insert_ind"; 80 81val mk_BN_def = Define ` 82 (mk_BN LN LN = LN) /\ 83 (mk_BN t1 t2 = BN t1 t2)`; 84 85val mk_BS_def = Define ` 86 (mk_BS LN x LN = LS x) /\ 87 (mk_BS t1 x t2 = BS t1 x t2)`; 88 89val delete_def = zDefine` 90 (delete k LN = LN) /\ 91 (delete k (LS a) = if k = 0 then LN else LS a) /\ 92 (delete k (BN t1 t2) = 93 if k = 0 then BN t1 t2 94 else if EVEN k then 95 mk_BN (delete ((k - 1) DIV 2) t1) t2 96 else 97 mk_BN t1 (delete ((k - 1) DIV 2) t2)) /\ 98 (delete k (BS t1 a t2) = 99 if k = 0 then BN t1 t2 100 else if EVEN k then 101 mk_BS (delete ((k - 1) DIV 2) t1) a t2 102 else 103 mk_BS t1 a (delete ((k - 1) DIV 2) t2)) 104`; 105 106val fromList_def = Define` 107 fromList l = SND (FOLDL (\(i,t) a. (i + 1, insert i a t)) (0,LN) l) 108`; 109 110val size_def = Define` 111 (size LN = 0) /\ 112 (size (LS a) = 1) /\ 113 (size (BN t1 t2) = size t1 + size t2) /\ 114 (size (BS t1 a t2) = size t1 + size t2 + 1) 115`; 116val _ = export_rewrites ["size_def"] 117 118val insert_notEmpty = store_thm( 119 "insert_notEmpty", 120 ``~isEmpty (insert k a t)``, 121 Cases_on `t` >> rw[Once insert_def]); 122 123val wf_insert = store_thm( 124 "wf_insert", 125 ``!k a t. wf t ==> wf (insert k a t)``, 126 ho_match_mp_tac (theorem "insert_ind") >> 127 rpt strip_tac >> 128 simp[Once insert_def] >> rw[wf_def, insert_notEmpty] >> fs[wf_def]); 129 130val mk_BN_thm = prove( 131 ``!t1 t2. mk_BN t1 t2 = 132 if isEmpty t1 /\ isEmpty t2 then LN else BN t1 t2``, 133 REPEAT Cases >> EVAL_TAC); 134 135val mk_BS_thm = prove( 136 ``!t1 t2. mk_BS t1 x t2 = 137 if isEmpty t1 /\ isEmpty t2 then LS x else BS t1 x t2``, 138 REPEAT Cases >> EVAL_TAC); 139 140val wf_delete = store_thm( 141 "wf_delete", 142 ``!t k. wf t ==> wf (delete k t)``, 143 Induct >> rw[wf_def, delete_def, mk_BN_thm, mk_BS_thm] >> 144 rw[wf_def] >> rw[] >> fs[] >> metis_tac[]); 145 146val lookup_insert1 = store_thm( 147 "lookup_insert1[simp]", 148 ``!k a t. lookup k (insert k a t) = SOME a``, 149 ho_match_mp_tac (theorem "insert_ind") >> rpt strip_tac >> 150 simp[Once insert_def] >> rw[lookup_def]); 151 152val DIV2_EQ_DIV2 = prove( 153 ``(m DIV 2 = n DIV 2) <=> 154 (m = n) \/ 155 (n = m + 1) /\ EVEN m \/ 156 (m = n + 1) /\ EVEN n``, 157 `0 < 2` by simp[] >> 158 map_every qabbrev_tac [`nq = n DIV 2`, `nr = n MOD 2`] >> 159 qspec_then `2` mp_tac DIVISION >> asm_simp_tac bool_ss [] >> 160 disch_then (qspec_then `n` mp_tac) >> asm_simp_tac bool_ss [] >> 161 map_every qabbrev_tac [`mq = m DIV 2`, `mr = m MOD 2`] >> 162 qspec_then `2` mp_tac DIVISION >> asm_simp_tac bool_ss [] >> 163 disch_then (qspec_then `m` mp_tac) >> asm_simp_tac bool_ss [] >> 164 rw[] >> markerLib.RM_ALL_ABBREVS_TAC >> 165 simp[EVEN_ADD, EVEN_MULT] >> 166 `!p. p < 2 ==> (EVEN p <=> (p = 0))` 167 by (rpt strip_tac >> `(p = 0) \/ (p = 1)` by decide_tac >> simp[]) >> 168 simp[]); 169 170val EVEN_PRE = prove( 171 ``x <> 0 ==> (EVEN (x - 1) <=> ~EVEN x)``, 172 Induct_on `x` >> simp[] >> Cases_on `x` >> fs[] >> 173 simp_tac (srw_ss()) [EVEN]); 174 175val lookup_insert = store_thm( 176 "lookup_insert", 177 ``!k2 v t k1. lookup k1 (insert k2 v t) = 178 if k1 = k2 then SOME v else lookup k1 t``, 179 ho_match_mp_tac (theorem "insert_ind") >> rpt strip_tac >> 180 simp[Once insert_def] >> rw[lookup_def] >> simp[] >| [ 181 fs[lookup_def] >> pop_assum mp_tac >> Cases_on `k1 = 0` >> simp[] >> 182 COND_CASES_TAC >> simp[lookup_def, DIV2_EQ_DIV2, EVEN_PRE], 183 fs[lookup_def] >> pop_assum mp_tac >> Cases_on `k1 = 0` >> simp[] >> 184 COND_CASES_TAC >> simp[lookup_def, DIV2_EQ_DIV2, EVEN_PRE] >> 185 rpt strip_tac >> metis_tac[EVEN_PRE], 186 fs[lookup_def] >> COND_CASES_TAC >> 187 simp[lookup_def, DIV2_EQ_DIV2, EVEN_PRE], 188 fs[lookup_def] >> COND_CASES_TAC >> 189 simp[lookup_def, DIV2_EQ_DIV2, EVEN_PRE] >> 190 rpt strip_tac >> metis_tac[EVEN_PRE], 191 simp[DIV2_EQ_DIV2, EVEN_PRE], 192 simp[DIV2_EQ_DIV2, EVEN_PRE] >> COND_CASES_TAC 193 >- metis_tac [EVEN_PRE] >> simp[], 194 simp[DIV2_EQ_DIV2, EVEN_PRE], 195 simp[DIV2_EQ_DIV2, EVEN_PRE] >> COND_CASES_TAC 196 >- metis_tac [EVEN_PRE] >> simp[] 197 ]) 198 199val union_def = Define` 200 (union LN t = t) /\ 201 (union (LS a) t = 202 case t of 203 | LN => LS a 204 | LS b => LS a 205 | BN t1 t2 => BS t1 a t2 206 | BS t1 _ t2 => BS t1 a t2) /\ 207 (union (BN t1 t2) t = 208 case t of 209 | LN => BN t1 t2 210 | LS a => BS t1 a t2 211 | BN t1' t2' => BN (union t1 t1') (union t2 t2') 212 | BS t1' a t2' => BS (union t1 t1') a (union t2 t2')) /\ 213 (union (BS t1 a t2) t = 214 case t of 215 | LN => BS t1 a t2 216 | LS a' => BS t1 a t2 217 | BN t1' t2' => BS (union t1 t1') a (union t2 t2') 218 | BS t1' a' t2' => BS (union t1 t1') a (union t2 t2')) 219`; 220 221val isEmpty_union = store_thm( 222 "isEmpty_union", 223 ``isEmpty (union m1 m2) <=> isEmpty m1 /\ isEmpty m2``, 224 map_every Cases_on [`m1`, `m2`] >> simp[union_def]); 225 226val wf_union = store_thm( 227 "wf_union", 228 ``!m1 m2. wf m1 /\ wf m2 ==> wf (union m1 m2)``, 229 Induct >> simp[wf_def, union_def] >> 230 Cases_on `m2` >> simp[wf_def,isEmpty_union] >> 231 metis_tac[]); 232 233val optcase_lemma = prove( 234 ``(case opt of NONE => NONE | SOME v => SOME v) = opt``, 235 Cases_on `opt` >> simp[]); 236 237val lookup_union = store_thm( 238 "lookup_union", 239 ``!m1 m2 k. lookup k (union m1 m2) = 240 case lookup k m1 of 241 NONE => lookup k m2 242 | SOME v => SOME v``, 243 Induct >> simp[lookup_def] >- simp[union_def] >> 244 Cases_on `m2` >> simp[lookup_def, union_def] >> 245 rw[optcase_lemma]); 246 247val inter_def = Define` 248 (inter LN t = LN) /\ 249 (inter (LS a) t = 250 case t of 251 | LN => LN 252 | LS b => LS a 253 | BN t1 t2 => LN 254 | BS t1 _ t2 => LS a) /\ 255 (inter (BN t1 t2) t = 256 case t of 257 | LN => LN 258 | LS a => LN 259 | BN t1' t2' => mk_BN (inter t1 t1') (inter t2 t2') 260 | BS t1' a t2' => mk_BN (inter t1 t1') (inter t2 t2')) /\ 261 (inter (BS t1 a t2) t = 262 case t of 263 | LN => LN 264 | LS a' => LS a 265 | BN t1' t2' => mk_BN (inter t1 t1') (inter t2 t2') 266 | BS t1' a' t2' => mk_BS (inter t1 t1') a (inter t2 t2')) 267`; 268 269val inter_eq_def = Define` 270 (inter_eq LN t = LN) /\ 271 (inter_eq (LS a) t = 272 case t of 273 | LN => LN 274 | LS b => if a = b then LS a else LN 275 | BN t1 t2 => LN 276 | BS t1 b t2 => if a = b then LS a else LN) /\ 277 (inter_eq (BN t1 t2) t = 278 case t of 279 | LN => LN 280 | LS a => LN 281 | BN t1' t2' => mk_BN (inter_eq t1 t1') (inter_eq t2 t2') 282 | BS t1' a t2' => mk_BN (inter_eq t1 t1') (inter_eq t2 t2')) /\ 283 (inter_eq (BS t1 a t2) t = 284 case t of 285 | LN => LN 286 | LS a' => if a' = a then LS a else LN 287 | BN t1' t2' => mk_BN (inter_eq t1 t1') (inter_eq t2 t2') 288 | BS t1' a' t2' => 289 if a' = a then 290 mk_BS (inter_eq t1 t1') a (inter_eq t2 t2') 291 else mk_BN (inter_eq t1 t1') (inter_eq t2 t2'))`; 292 293val difference_def = Define` 294 (difference LN t = LN) /\ 295 (difference (LS a) t = 296 case t of 297 | LN => LS a 298 | LS b => LN 299 | BN t1 t2 => LS a 300 | BS t1 b t2 => LN) /\ 301 (difference (BN t1 t2) t = 302 case t of 303 | LN => BN t1 t2 304 | LS a => BN t1 t2 305 | BN t1' t2' => mk_BN (difference t1 t1') (difference t2 t2') 306 | BS t1' a t2' => mk_BN (difference t1 t1') (difference t2 t2')) /\ 307 (difference (BS t1 a t2) t = 308 case t of 309 | LN => BS t1 a t2 310 | LS a' => BN t1 t2 311 | BN t1' t2' => mk_BS (difference t1 t1') a (difference t2 t2') 312 | BS t1' a' t2' => mk_BN (difference t1 t1') (difference t2 t2'))`; 313 314val wf_mk_BN = prove( 315 ``!t1 t2. wf (mk_BN t1 t2) <=> wf t1 /\ wf t2``, 316 map_every Cases_on [`t1`,`t2`] >> fs [mk_BN_def,wf_def]); 317 318val wf_mk_BS = prove( 319 ``!t1 x t2. wf (mk_BS t1 x t2) <=> wf t1 /\ wf t2``, 320 map_every Cases_on [`t1`,`t2`] >> fs [mk_BS_def,wf_def]); 321 322val wf_inter = store_thm( 323 "wf_inter[simp]", 324 ``!m1 m2. wf (inter m1 m2)``, 325 Induct >> simp[wf_def, inter_def] >> 326 Cases_on `m2` >> simp[wf_def,wf_mk_BS,wf_mk_BN]); 327 328val lookup_mk_BN = prove( 329 ``lookup k (mk_BN t1 t2) = lookup k (BN t1 t2)``, 330 map_every Cases_on [`t1`,`t2`] >> fs [mk_BN_def,lookup_def]); 331 332val lookup_mk_BS = prove( 333 ``lookup k (mk_BS t1 x t2) = lookup k (BS t1 x t2)``, 334 map_every Cases_on [`t1`,`t2`] >> fs [mk_BS_def,lookup_def]); 335 336val lookup_inter = store_thm( 337 "lookup_inter", 338 ``!m1 m2 k. lookup k (inter m1 m2) = 339 case (lookup k m1,lookup k m2) of 340 | (SOME v, SOME w) => SOME v 341 | _ => NONE``, 342 Induct >> simp[lookup_def] >> Cases_on `m2` >> 343 simp[lookup_def, inter_def, lookup_mk_BS, lookup_mk_BN] >> 344 rw[optcase_lemma] >> BasicProvers.CASE_TAC); 345 346val lookup_inter_eq = store_thm( 347 "lookup_inter_eq", 348 ``!m1 m2 k. lookup k (inter_eq m1 m2) = 349 case lookup k m1 of 350 | NONE => NONE 351 | SOME v => (if lookup k m2 = SOME v then SOME v else NONE)``, 352 Induct >> simp[lookup_def] >> Cases_on `m2` >> 353 simp[lookup_def, inter_eq_def, lookup_mk_BS, lookup_mk_BN] >> 354 rw[optcase_lemma] >> REPEAT BasicProvers.CASE_TAC >> 355 fs [lookup_def, lookup_mk_BS, lookup_mk_BN]); 356 357val lookup_inter_EQ = store_thm("lookup_inter_EQ", 358 ``((lookup x (inter t1 t2) = SOME y) <=> 359 (lookup x t1 = SOME y) /\ lookup x t2 <> NONE) /\ 360 ((lookup x (inter t1 t2) = NONE) <=> 361 (lookup x t1 = NONE) \/ (lookup x t2 = NONE))``, 362 fs [lookup_inter] \\ BasicProvers.EVERY_CASE_TAC); 363 364val lookup_inter_assoc = store_thm("lookup_inter_assoc", 365 ``lookup x (inter t1 (inter t2 t3)) = 366 lookup x (inter (inter t1 t2) t3)``, 367 fs [lookup_inter] \\ BasicProvers.EVERY_CASE_TAC) 368 369val lookup_difference = store_thm( 370 "lookup_difference", 371 ``!m1 m2 k. lookup k (difference m1 m2) = 372 if lookup k m2 = NONE then lookup k m1 else NONE``, 373 Induct >> simp[lookup_def] >> Cases_on `m2` >> 374 simp[lookup_def, difference_def, lookup_mk_BS, lookup_mk_BN] >> 375 rw[optcase_lemma] >> REPEAT BasicProvers.CASE_TAC >> 376 fs [lookup_def, lookup_mk_BS, lookup_mk_BN]) 377 378val lrnext_real_def = tzDefine "lrnext" ` 379 lrnext n = if n = 0 then 1 else 2 * lrnext ((n - 1) DIV 2)` 380 (WF_REL_TAC `measure I` \\ fs [DIV_LT_X] \\ REPEAT STRIP_TAC \\ DECIDE_TAC) ; 381 382val lrnext_def = prove( 383 ``(lrnext ZERO = 1) /\ 384 (!n. lrnext (BIT1 n) = 2 * lrnext n) /\ 385 (!n. lrnext (BIT2 n) = 2 * lrnext n)``, 386 REPEAT STRIP_TAC 387 THEN1 (fs [Once ALT_ZERO,Once lrnext_real_def]) 388 THEN1 389 (full_simp_tac (srw_ss()) [Once BIT1,Once lrnext_real_def] 390 \\ AP_TERM_TAC \\ simp_tac (srw_ss()) [Once BIT1] 391 \\ full_simp_tac (srw_ss()) [ADD_ASSOC,DECIDE ``n+n=n*2``,MULT_DIV]) 392 THEN1 393 (simp_tac (srw_ss()) [Once BIT2,Once lrnext_real_def] 394 \\ AP_TERM_TAC \\ simp_tac (srw_ss()) [Once BIT2] 395 \\ `n + (n + 2) - 1 = n * 2 + 1` by DECIDE_TAC 396 \\ asm_simp_tac (srw_ss()) [DIV_MULT])) 397val lrnext' = prove( 398 ``(!a. lrnext 0 = 1) /\ (!n a. lrnext (NUMERAL n) = lrnext n)``, 399 simp[NUMERAL_DEF, GSYM ALT_ZERO, lrnext_def]) 400val lrnext_thm = save_thm( 401 "lrnext_thm", 402 LIST_CONJ (CONJUNCTS lrnext' @ CONJUNCTS lrnext_def)) 403val _ = computeLib.add_persistent_funs ["lrnext_thm"] 404 405val domain_def = zDefine` 406 (domain LN = {}) /\ 407 (domain (LS _) = {0}) /\ 408 (domain (BN t1 t2) = 409 IMAGE (\n. 2 * n + 2) (domain t1) UNION 410 IMAGE (\n. 2 * n + 1) (domain t2)) /\ 411 (domain (BS t1 _ t2) = 412 {0} UNION IMAGE (\n. 2 * n + 2) (domain t1) UNION 413 IMAGE (\n. 2 * n + 1) (domain t2)) 414`; 415val _ = export_rewrites ["domain_def"] 416 417val FINITE_domain = store_thm( 418 "FINITE_domain[simp]", 419 ``FINITE (domain t)``, 420 Induct_on `t` >> simp[]); 421 422val DIV2 = DIVISION |> Q.SPEC `2` |> REWRITE_RULE [DECIDE ``0 < 2``] 423 424val even_lem = Q.prove( 425 `EVEN k /\ k <> 0 ==> (2 * ((k - 1) DIV 2) + 2 = k)`, 426 qabbrev_tac `k0 = k - 1` >> 427 strip_tac >> `k = k0 + 1` by simp[Abbr`k0`] >> 428 pop_assum SUBST_ALL_TAC >> qunabbrev_tac `k0` >> 429 fs[EVEN_ADD] >> 430 assume_tac (Q.SPEC `k0` DIV2) >> 431 map_every qabbrev_tac [`q = k0 DIV 2`, `r = k0 MOD 2`] >> 432 markerLib.RM_ALL_ABBREVS_TAC >> 433 fs[EVEN_ADD, EVEN_MULT] >> 434 `(r = 0) \/ (r = 1)` by simp[] >> fs[]) 435 436val odd_lem = Q.prove( 437 `~EVEN k /\ k <> 0 ==> (2 * ((k - 1) DIV 2) + 1 = k)`, 438 qabbrev_tac `k0 = k - 1` >> 439 strip_tac >> `k = k0 + 1` by simp[Abbr`k0`] >> 440 pop_assum SUBST_ALL_TAC >> qunabbrev_tac `k0` >> 441 fs[EVEN_ADD] >> 442 assume_tac (Q.SPEC `k0` DIV2) >> 443 map_every qabbrev_tac [`q = k0 DIV 2`, `r = k0 MOD 2`] >> 444 markerLib.RM_ALL_ABBREVS_TAC >> 445 fs[EVEN_ADD, EVEN_MULT] >> 446 `(r = 0) \/ (r = 1)` by simp[] >> fs[]) 447 448val even_lem' = CONV_RULE (RAND_CONV (ONCE_REWRITE_CONV [EQ_SYM_EQ])) even_lem 449val odd_lem' = CONV_RULE (RAND_CONV (ONCE_REWRITE_CONV [EQ_SYM_EQ])) odd_lem 450 451val even_imposs = Q.prove( 452 ���EVEN n ==> !m. n <> 2 * m + 1���, 453 rpt strip_tac >> fs[EVEN_ADD, EVEN_MULT]); 454val odd_imposs = Q.prove( 455 ���~EVEN n ==> !m. n <> 2 * m + 2���, 456 rpt strip_tac >> fs[EVEN_ADD, EVEN_MULT]); 457 458fun writeL th = CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [th])) 459 460Theorem IN_domain: 461 !n x t1 t2. 462 (n IN domain LN <=> F) /\ 463 (n IN domain (LS x) <=> (n = 0)) /\ 464 (n IN domain (BN t1 t2) <=> 465 n <> 0 /\ (if EVEN n then ((n-1) DIV 2) IN domain t1 466 else ((n-1) DIV 2) IN domain t2)) /\ 467 (n IN domain (BS t1 x t2) <=> 468 (n = 0) \/ (if EVEN n then ((n-1) DIV 2) IN domain t1 469 else ((n-1) DIV 2) IN domain t2)) 470Proof 471 simp[domain_def] >> rpt strip_tac >> Cases_on ���n = 0��� >> simp[] >> 472 Cases_on ���EVEN n��� >> simp[] >> 473 (drule_then assume_tac even_imposs ORELSE drule_then assume_tac odd_imposs) >> 474 simp[] >> 475 (drule_all_then writeL even_lem' ORELSE drule_all_then writeL odd_lem') >> 476 simp[] 477QED 478 479val size_insert = Q.store_thm( 480 "size_insert", 481 `!k v m. size (insert k v m) = if k IN domain m then size m else size m + 1`, 482 ho_match_mp_tac insert_ind >> rpt conj_tac >> simp[] >> 483 rpt strip_tac >> simp[Once insert_def] 484 >- rw[] 485 >- rw[] 486 >- (Cases_on `k = 0` >> simp[] >> fs[] >> Cases_on `EVEN k` >> fs[] 487 >- (`!n. k <> 2 * n + 1` by (rpt strip_tac >> fs[EVEN_ADD, EVEN_MULT]) >> 488 qabbrev_tac `k2 = (k - 1) DIV 2` >> 489 `k = 2 * k2 + 2` suffices_by rw[] >> 490 simp[Abbr`k2`, even_lem]) >> 491 `!n. k <> 2 * n + 2` by (rpt strip_tac >> fs[EVEN_ADD, EVEN_MULT]) >> 492 qabbrev_tac `k2 = (k - 1) DIV 2` >> 493 `k = 2 * k2 + 1` suffices_by rw[] >> 494 simp[Abbr`k2`, odd_lem]) 495 >- (Cases_on `k = 0` >> simp[] >> fs[] >> Cases_on `EVEN k` >> fs[] 496 >- (`!n. k <> 2 * n + 1` by (rpt strip_tac >> fs[EVEN_ADD, EVEN_MULT]) >> 497 qabbrev_tac `k2 = (k - 1) DIV 2` >> 498 `k = 2 * k2 + 2` suffices_by rw[] >> 499 simp[Abbr`k2`, even_lem]) >> 500 `!n. k <> 2 * n + 2` by (rpt strip_tac >> fs[EVEN_ADD, EVEN_MULT]) >> 501 qabbrev_tac `k2 = (k - 1) DIV 2` >> 502 `k = 2 * k2 + 1` suffices_by rw[] >> 503 simp[Abbr`k2`, odd_lem])) 504 505val lookup_fromList = store_thm( 506 "lookup_fromList", 507 ``lookup n (fromList l) = if n < LENGTH l then SOME (EL n l) 508 else NONE``, 509 simp[fromList_def] >> 510 `!i n t. lookup n (SND (FOLDL (\ (i,t) a. (i+1,insert i a t)) (i,t) l)) = 511 if n < i then lookup n t 512 else if n < LENGTH l + i then SOME (EL (n - i) l) 513 else lookup n t` 514 suffices_by (simp[] >> strip_tac >> simp[lookup_def]) >> 515 Induct_on `l` >> simp[] >> pop_assum kall_tac >> 516 rw[lookup_insert] >> 517 full_simp_tac (srw_ss() ++ ARITH_ss) [] >> 518 `0 < n - i` by simp[] >> 519 Cases_on `n - i` >> fs[] >> 520 qmatch_assum_rename_tac `n - i = SUC nn` >> 521 `nn = n - (i + 1)` by decide_tac >> simp[]); 522 523val bit_cases = prove( 524 ``!n. (n = 0) \/ (?m. n = 2 * m + 1) \/ (?m. n = 2 * m + 2)``, 525 Induct >> simp[] >> fs[] 526 >- (disj2_tac >> qexists_tac `m` >> simp[]) 527 >- (disj1_tac >> qexists_tac `SUC m` >> simp[])) 528 529val oddevenlemma = prove( 530 ``2 * y + 1 <> 2 * x + 2``, 531 disch_then (mp_tac o AP_TERM ``EVEN``) >> 532 simp[EVEN_ADD, EVEN_MULT]); 533 534val MULT2_DIV' = prove( 535 ``(2 * m DIV 2 = m) /\ ((2 * m + 1) DIV 2 = m)``, 536 simp[DIV_EQ_X]); 537 538val domain_lookup = store_thm( 539 "domain_lookup", 540 ``!t k. k IN domain t <=> ?v. lookup k t = SOME v``, 541 Induct >> simp[domain_def, lookup_def] >> rpt gen_tac >> 542 qspec_then `k` STRUCT_CASES_TAC bit_cases >> 543 simp[oddevenlemma, EVEN_ADD, EVEN_MULT, 544 EQ_MULT_LCANCEL, MULT2_DIV']); 545 546val lookup_inter_alt = store_thm("lookup_inter_alt", 547 ``lookup x (inter t1 t2) = 548 if x IN domain t2 then lookup x t1 else NONE``, 549 fs [lookup_inter,domain_lookup] 550 \\ Cases_on `lookup x t2` \\ fs [] \\ Cases_on `lookup x t1` \\ fs []); 551 552val lookup_NONE_domain = store_thm( 553 "lookup_NONE_domain", 554 ``(lookup k t = NONE) <=> k NOTIN domain t``, 555 simp[domain_lookup] >> Cases_on `lookup k t` >> simp[]); 556 557val domain_union = store_thm( 558 "domain_union", 559 ``domain (union t1 t2) = domain t1 UNION domain t2``, 560 simp[EXTENSION, domain_lookup, lookup_union] >> 561 qx_gen_tac `k` >> Cases_on `lookup k t1` >> simp[]); 562 563val domain_inter = store_thm( 564 "domain_inter", 565 ``domain (inter t1 t2) = domain t1 INTER domain t2``, 566 simp[EXTENSION, domain_lookup, lookup_inter] >> 567 rw [] >> Cases_on `lookup x t1` >> fs[] >> 568 BasicProvers.CASE_TAC); 569 570val domain_insert = store_thm( 571 "domain_insert[simp]", 572 ``domain (insert k v t) = k INSERT domain t``, 573 simp[domain_lookup, EXTENSION, lookup_insert] >> 574 metis_tac[]); 575 576val domain_difference = Q.store_thm( 577 "domain_difference", 578 `!t1 t2 . domain (difference t1 t2) = (domain t1) DIFF (domain t2)`, 579 simp[EXTENSION, domain_lookup, lookup_difference] >> 580 rw [] >> Cases_on `lookup x t1` 581 >> fs[] >> Cases_on `lookup x t2` >> rw[]); 582 583val domain_sing = save_thm( 584 "domain_sing", 585 domain_insert |> Q.INST [`t` |-> `LN`] |> SIMP_RULE bool_ss [domain_def]); 586 587val domain_fromList = store_thm( 588 "domain_fromList", 589 ``domain (fromList l) = count (LENGTH l)``, 590 simp[fromList_def] >> 591 `!i t. domain (SND (FOLDL (\ (i,t) a. (i + 1, insert i a t)) (i,t) l)) = 592 domain t UNION IMAGE ((+) i) (count (LENGTH l))` 593 suffices_by (simp[] >> strip_tac >> simp[EXTENSION]) >> 594 Induct_on `l` >> simp[EXTENSION, EQ_IMP_THM] >> 595 rpt strip_tac >> simp[DECIDE ``(x = x + y) <=> (y = 0)``] >> 596 qmatch_assum_rename_tac `nn < SUC (LENGTH l)` >> 597 Cases_on `nn` >> fs[] >> metis_tac[ADD1]); 598 599val ODD_IMP_NOT_ODD = prove( 600 ``!k. ODD k ==> ~(ODD (k-1))``, 601 Cases >> fs [ODD]); 602 603val lookup_delete = store_thm( 604 "lookup_delete", 605 ``!t k1 k2. 606 lookup k1 (delete k2 t) = if k1 = k2 then NONE 607 else lookup k1 t``, 608 Induct >> simp[delete_def, lookup_def] 609 >> rw [lookup_def,lookup_mk_BN,lookup_mk_BS] 610 >> sg `(k1 - 1) DIV 2 <> (k2 - 1) DIV 2` 611 >> simp[DIV2_EQ_DIV2, EVEN_PRE] 612 >> fs [] >> CCONTR_TAC >> fs [] >> srw_tac [] [] 613 >> fs [EVEN_ODD] >> imp_res_tac ODD_IMP_NOT_ODD); 614 615val domain_delete = store_thm( 616 "domain_delete[simp]", 617 ``domain (delete k t) = domain t DELETE k``, 618 simp[EXTENSION, domain_lookup, lookup_delete] >> 619 metis_tac[]); 620 621val foldi_def = Define` 622 (foldi f i acc LN = acc) /\ 623 (foldi f i acc (LS a) = f i a acc) /\ 624 (foldi f i acc (BN t1 t2) = 625 let inc = lrnext i 626 in 627 foldi f (i + inc) (foldi f (i + 2 * inc) acc t1) t2) /\ 628 (foldi f i acc (BS t1 a t2) = 629 let inc = lrnext i 630 in 631 foldi f (i + inc) (f i a (foldi f (i + 2 * inc) acc t1)) t2) 632`; 633 634val spt_acc_def = tDefine"spt_acc"` 635 (spt_acc i 0 = i) /\ 636 (spt_acc i (SUC k) = spt_acc (i + if EVEN (SUC k) then 2 * lrnext i else lrnext i) (k DIV 2))` 637 (WF_REL_TAC`measure SND` 638 \\ simp[DIV_LT_X]); 639 640val spt_acc_thm = Q.store_thm("spt_acc_thm", 641 `spt_acc i k = if k = 0 then i else spt_acc (i + if EVEN k then 2 * lrnext i else lrnext i) ((k-1) DIV 2)`, 642 rw[spt_acc_def] \\ Cases_on`k` \\ fs[spt_acc_def]); 643 644val lemmas = prove( 645 ``(!x. EVEN (2 * x + 2)) /\ 646 (!x. ODD (2 * x + 1))``, 647 conj_tac >- ( 648 simp[EVEN_EXISTS] >> rw[] >> 649 qexists_tac`SUC x` >> simp[] ) >> 650 simp[ODD_EXISTS,ADD1] >> 651 metis_tac[] ) 652 653val bit_induction = prove( 654 ``!P. P 0 /\ (!n. P n ==> P (2 * n + 1)) /\ 655 (!n. P n ==> P (2 * n + 2)) ==> 656 !n. P n``, 657 gen_tac >> strip_tac >> completeInduct_on `n` >> simp[] >> 658 qspec_then `n` strip_assume_tac bit_cases >> simp[]); 659 660val lrnext212 = prove( 661 ``(lrnext (2 * m + 1) = 2 * lrnext m) /\ 662 (lrnext (2 * m + 2) = 2 * lrnext m)``, 663 conj_tac >| [ 664 `2 * m + 1 = BIT1 m` suffices_by simp[lrnext_thm] >> 665 simp_tac bool_ss [BIT1, TWO, ONE, MULT_CLAUSES, ADD_CLAUSES], 666 `2 * m + 2 = BIT2 m` suffices_by simp[lrnext_thm] >> 667 simp_tac bool_ss [BIT2, TWO, ONE, MULT_CLAUSES, ADD_CLAUSES] 668 ]); 669 670val lrlemma1 = prove( 671 ``lrnext (i + lrnext i) = 2 * lrnext i``, 672 qid_spec_tac `i` >> ho_match_mp_tac bit_induction >> 673 simp[lrnext212, lrnext_thm] >> conj_tac 674 >- (gen_tac >> 675 `2 * i + (2 * lrnext i + 1) = 2 * (i + lrnext i) + 1` 676 by decide_tac >> simp[lrnext212]) >> 677 qx_gen_tac `i` >> 678 `2 * i + (2 * lrnext i + 2) = 2 * (i + lrnext i) + 2` 679 by decide_tac >> 680 simp[lrnext212]); 681 682val lrlemma2 = prove( 683 ``lrnext (i + 2 * lrnext i) = 2 * lrnext i``, 684 qid_spec_tac `i` >> ho_match_mp_tac bit_induction >> 685 simp[lrnext212, lrnext_thm] >> conj_tac 686 >- (qx_gen_tac `i` >> 687 `2 * i + (4 * lrnext i + 1) = 2 * (i + 2 * lrnext i) + 1` 688 by decide_tac >> simp[lrnext212]) >> 689 gen_tac >> 690 `2 * i + (4 * lrnext i + 2) = 2 * (i + 2 * lrnext i) + 2` 691 by decide_tac >> simp[lrnext212]) 692 693val spt_acc_eqn = Q.store_thm("spt_acc_eqn", 694 `!k i. spt_acc i k = lrnext i * k + i`, 695 ho_match_mp_tac bit_induction 696 \\ rw[] 697 >- rw[spt_acc_def] 698 >- ( 699 rw[Once spt_acc_thm] 700 >- fs[EVEN_ODD,lemmas] 701 \\ simp[MULT2_DIV'] 702 \\ simp[lrlemma1] ) 703 >- ( 704 ONCE_REWRITE_TAC[spt_acc_thm] 705 \\ simp[] 706 \\ reverse(rw[]) 707 >- fs[EVEN_ODD,lemmas] 708 \\ simp[MULT2_DIV'] 709 \\ simp[lrlemma2])); 710 711val spt_acc_0 = Q.store_thm("spt_acc_0", 712 `!k. spt_acc 0 k = k`, rw[spt_acc_eqn,lrnext_thm]); 713 714val set_foldi_keys = store_thm( 715 "set_foldi_keys", 716 ``!t a i. foldi (\k v a. k INSERT a) i a t = 717 a UNION IMAGE (\n. i + lrnext i * n) (domain t)``, 718 Induct_on `t` >> simp[foldi_def, GSYM IMAGE_COMPOSE, 719 combinTheory.o_ABS_R] 720 >- simp[Once INSERT_SING_UNION, UNION_COMM] 721 >- (simp[EXTENSION] >> rpt gen_tac >> 722 Cases_on `x IN a` >> simp[lrlemma1, lrlemma2, LEFT_ADD_DISTRIB]) >> 723 simp[EXTENSION] >> rpt gen_tac >> 724 Cases_on `x IN a'` >> simp[lrlemma1, lrlemma2, LEFT_ADD_DISTRIB]) 725 726val domain_foldi = save_thm( 727 "domain_foldi", 728 set_foldi_keys |> SPEC_ALL |> Q.INST [`i` |-> `0`, `a` |-> `{}`] 729 |> SIMP_RULE (srw_ss()) [lrnext_thm] 730 |> SYM); 731val _ = computeLib.add_persistent_funs ["domain_foldi"] 732 733val mapi0_def = Define` 734 (mapi0 f i LN = LN) /\ 735 (mapi0 f i (LS a) = LS (f i a)) /\ 736 (mapi0 f i (BN t1 t2) = 737 let inc = lrnext i in 738 mk_BN (mapi0 f (i + 2 * inc) t1) (mapi0 f (i + inc) t2)) /\ 739 (mapi0 f i (BS t1 a t2) = 740 let inc = lrnext i in 741 mk_BS (mapi0 f (i + 2 * inc) t1) (f i a) (mapi0 f (i + inc) t2)) 742`; 743val _ = export_rewrites ["mapi0_def"] 744val mapi_def = Define`mapi f pt = mapi0 f 0 pt`; 745 746val lookup_mapi0 = Q.store_thm("lookup_mapi0", 747 `!pt i k. 748 lookup k (mapi0 f i pt) = 749 case lookup k pt of NONE => NONE 750 | SOME v => SOME (f (spt_acc i k) v)`, 751 Induct \\ rw[mapi0_def,lookup_def,lookup_mk_BN,lookup_mk_BS] \\ fs[] 752 \\ TRY (simp[spt_acc_eqn] \\ NO_TAC) 753 \\ CASE_TAC \\ simp[Once spt_acc_thm,SimpRHS]); 754 755val lookup_mapi = Q.store_thm("lookup_mapi", 756 `lookup k (mapi f pt) = OPTION_MAP (f k) (lookup k pt)`, 757 rw[mapi_def,lookup_mapi0,spt_acc_0] 758 \\ CASE_TAC \\ fs[]); 759 760val toAList_def = Define ` 761 toAList = foldi (\k v a. (k,v)::a) 0 []` 762 763val set_toAList_lemma = prove( 764 ``!t a i. set (foldi (\k v a. (k,v) :: a) i a t) = 765 set a UNION IMAGE (\n. (i + lrnext i * n, 766 THE (lookup n t))) (domain t)``, 767 Induct_on `t` 768 \\ fs [foldi_def,GSYM IMAGE_COMPOSE,lookup_def] 769 THEN1 fs [Once INSERT_SING_UNION, UNION_COMM] 770 THEN1 (simp[EXTENSION] \\ rpt gen_tac \\ 771 Cases_on `MEM x a` \\ simp[lrlemma1, lrlemma2, LEFT_ADD_DISTRIB] 772 \\ fs [MULT2_DIV',EVEN_ADD,EVEN_DOUBLE]) 773 \\ simp[EXTENSION] \\ rpt gen_tac 774 \\ Cases_on `MEM x a'` \\ simp[lrlemma1, lrlemma2, LEFT_ADD_DISTRIB] 775 \\ fs [MULT2_DIV',EVEN_ADD,EVEN_DOUBLE]) 776 |> Q.SPECL [`t`,`[]`,`0`] |> GEN_ALL 777 |> SIMP_RULE (srw_ss()) [GSYM toAList_def,lrnext_thm,MEM,LIST_TO_SET, 778 UNION_EMPTY,EXTENSION, 779 pairTheory.FORALL_PROD] 780 781val MEM_toAList = store_thm("MEM_toAList", 782 ``!t k v. MEM (k,v) (toAList t) <=> (lookup k t = SOME v)``, 783 fs [set_toAList_lemma,domain_lookup] \\ REPEAT STRIP_TAC 784 \\ Cases_on `lookup k t` \\ fs [] 785 \\ REPEAT STRIP_TAC \\ EQ_TAC \\ fs []); 786 787val ALOOKUP_toAList = store_thm("ALOOKUP_toAList", 788 ``!t x. ALOOKUP (toAList t) x = lookup x t``, 789 strip_tac>>strip_tac>>Cases_on `lookup x t` >- 790 simp[ALOOKUP_FAILS,MEM_toAList] >> 791 Cases_on`ALOOKUP (toAList t) x`>- 792 fs[ALOOKUP_FAILS,MEM_toAList] >> 793 imp_res_tac ALOOKUP_MEM >> 794 fs[MEM_toAList]) 795 796val insert_union = store_thm("insert_union", 797 ``!k v s. insert k v s = union (insert k v LN) s``, 798 completeInduct_on`k` >> simp[Once insert_def] >> rw[] >> 799 simp[Once union_def] >> 800 Cases_on`s`>>simp[Once insert_def] >> 801 simp[Once union_def] >> 802 first_x_assum match_mp_tac >> 803 simp[arithmeticTheory.DIV_LT_X]) 804 805val domain_empty = store_thm("domain_empty", 806 ``!t. wf t ==> ((t = LN) <=> (domain t = EMPTY))``, 807 simp[] >> Induct >> simp[wf_def] >> metis_tac[]) 808 809val toAList_append = prove( 810 ``!t n ls. 811 foldi (\k v a. (k,v)::a) n ls t = 812 foldi (\k v a. (k,v)::a) n [] t ++ ls``, 813 Induct 814 >- simp[foldi_def] 815 >- simp[foldi_def] 816 >- ( 817 simp_tac std_ss [foldi_def,LET_THM] >> rpt gen_tac >> 818 first_assum(fn th => 819 CONV_TAC(LAND_CONV(RATOR_CONV(RAND_CONV(REWR_CONV th))))) >> 820 first_assum(fn th => 821 CONV_TAC(LAND_CONV(REWR_CONV th))) >> 822 first_assum(fn th => 823 CONV_TAC(RAND_CONV(LAND_CONV(REWR_CONV th)))) >> 824 metis_tac[APPEND_ASSOC] ) >> 825 simp_tac std_ss [foldi_def,LET_THM] >> rpt gen_tac >> 826 first_assum(fn th => 827 CONV_TAC(LAND_CONV(RATOR_CONV(RAND_CONV(RAND_CONV(REWR_CONV th)))))) >> 828 first_assum(fn th => 829 CONV_TAC(LAND_CONV(REWR_CONV th))) >> 830 first_assum(fn th => 831 CONV_TAC(RAND_CONV(LAND_CONV(REWR_CONV th)))) >> 832 metis_tac[APPEND_ASSOC,APPEND] ) 833 834val toAList_inc = prove( 835 ``!t n. 836 foldi (\k v a. (k,v)::a) n [] t = 837 MAP (\(k,v). (n + lrnext n * k,v)) (foldi (\k v a. (k,v)::a) 0 [] t)``, 838 Induct 839 >- simp[foldi_def] 840 >- simp[foldi_def] 841 >- ( 842 simp_tac std_ss [foldi_def,LET_THM] >> rpt gen_tac >> 843 CONV_TAC(LAND_CONV(REWR_CONV toAList_append)) >> 844 CONV_TAC(RAND_CONV(RAND_CONV(REWR_CONV toAList_append))) >> 845 first_assum(fn th => 846 CONV_TAC(LAND_CONV(LAND_CONV(REWR_CONV th)))) >> 847 first_assum(fn th => 848 CONV_TAC(LAND_CONV(RAND_CONV(REWR_CONV th)))) >> 849 first_assum(fn th => 850 CONV_TAC(RAND_CONV(RAND_CONV(LAND_CONV(REWR_CONV th))))) >> 851 first_assum(fn th => 852 CONV_TAC(RAND_CONV(RAND_CONV(RAND_CONV(REWR_CONV th))))) >> 853 rpt(pop_assum kall_tac) >> 854 simp[MAP_MAP_o,combinTheory.o_DEF,APPEND_11_LENGTH] >> 855 simp[MAP_EQ_f] >> 856 simp[lrnext_thm,pairTheory.UNCURRY,pairTheory.FORALL_PROD] >> 857 simp[lrlemma1,lrlemma2] ) 858 >- ( 859 simp_tac std_ss [foldi_def,LET_THM] >> rpt gen_tac >> 860 CONV_TAC(LAND_CONV(REWR_CONV toAList_append)) >> 861 CONV_TAC(RAND_CONV(RAND_CONV(REWR_CONV toAList_append))) >> 862 first_assum(fn th => 863 CONV_TAC(LAND_CONV(LAND_CONV(REWR_CONV th)))) >> 864 first_assum(fn th => 865 CONV_TAC(LAND_CONV(RAND_CONV(RAND_CONV(REWR_CONV th))))) >> 866 first_assum(fn th => 867 CONV_TAC(RAND_CONV(RAND_CONV(LAND_CONV(REWR_CONV th))))) >> 868 first_assum(fn th => 869 CONV_TAC(RAND_CONV(RAND_CONV(RAND_CONV(RAND_CONV(REWR_CONV th)))))) >> 870 rpt(pop_assum kall_tac) >> 871 simp[MAP_MAP_o,combinTheory.o_DEF,APPEND_11_LENGTH] >> 872 simp[MAP_EQ_f] >> 873 simp[lrnext_thm,pairTheory.UNCURRY,pairTheory.FORALL_PROD] >> 874 simp[lrlemma1,lrlemma2] )) 875 876val ALL_DISTINCT_MAP_FST_toAList = store_thm("ALL_DISTINCT_MAP_FST_toAList", 877 ``!t. ALL_DISTINCT (MAP FST (toAList t))``, 878 simp[toAList_def] >> 879 Induct >> simp[foldi_def] >- ( 880 CONV_TAC(RAND_CONV(RAND_CONV(RATOR_CONV(RAND_CONV(REWR_CONV toAList_inc))))) >> 881 CONV_TAC(RAND_CONV(RAND_CONV(REWR_CONV toAList_append))) >> 882 CONV_TAC(RAND_CONV(RAND_CONV(LAND_CONV(REWR_CONV toAList_inc)))) >> 883 simp[MAP_MAP_o,combinTheory.o_DEF,pairTheory.UNCURRY,lrnext_thm] >> 884 simp[ALL_DISTINCT_APPEND] >> 885 rpt conj_tac >- ( 886 qmatch_abbrev_tac`ALL_DISTINCT (MAP f ls)` >> 887 `MAP f ls = MAP (\x. 2 * x + 1) (MAP FST ls)` by ( 888 simp[MAP_MAP_o,combinTheory.o_DEF,Abbr`f`] ) >> 889 pop_assum SUBST1_TAC >> qunabbrev_tac`f` >> 890 match_mp_tac ALL_DISTINCT_MAP_INJ >> 891 simp[] ) 892 >- ( 893 qmatch_abbrev_tac`ALL_DISTINCT (MAP f ls)` >> 894 `MAP f ls = MAP (\x. 2 * x + 2) (MAP FST ls)` by ( 895 simp[MAP_MAP_o,combinTheory.o_DEF,Abbr`f`] ) >> 896 pop_assum SUBST1_TAC >> qunabbrev_tac`f` >> 897 match_mp_tac ALL_DISTINCT_MAP_INJ >> 898 simp[] ) >> 899 simp[MEM_MAP,PULL_EXISTS,pairTheory.EXISTS_PROD] >> 900 metis_tac[ODD_EVEN,lemmas] ) >> 901 gen_tac >> 902 CONV_TAC(RAND_CONV(RAND_CONV(RATOR_CONV(RAND_CONV(RAND_CONV(REWR_CONV toAList_inc)))))) >> 903 CONV_TAC(RAND_CONV(RAND_CONV(REWR_CONV toAList_append))) >> 904 CONV_TAC(RAND_CONV(RAND_CONV(LAND_CONV(REWR_CONV toAList_inc)))) >> 905 simp[MAP_MAP_o,combinTheory.o_DEF,pairTheory.UNCURRY,lrnext_thm] >> 906 simp[ALL_DISTINCT_APPEND] >> 907 rpt conj_tac >- ( 908 qmatch_abbrev_tac`ALL_DISTINCT (MAP f ls)` >> 909 `MAP f ls = MAP (\x. 2 * x + 1) (MAP FST ls)` by ( 910 simp[MAP_MAP_o,combinTheory.o_DEF,Abbr`f`] ) >> 911 pop_assum SUBST1_TAC >> qunabbrev_tac`f` >> 912 match_mp_tac ALL_DISTINCT_MAP_INJ >> 913 simp[] ) 914 >- ( simp[MEM_MAP] ) 915 >- ( 916 qmatch_abbrev_tac`ALL_DISTINCT (MAP f ls)` >> 917 `MAP f ls = MAP (\x. 2 * x + 2) (MAP FST ls)` by ( 918 simp[MAP_MAP_o,combinTheory.o_DEF,Abbr`f`] ) >> 919 pop_assum SUBST1_TAC >> qunabbrev_tac`f` >> 920 match_mp_tac ALL_DISTINCT_MAP_INJ >> 921 simp[] ) >> 922 simp[MEM_MAP,PULL_EXISTS,pairTheory.EXISTS_PROD] >> 923 metis_tac[ODD_EVEN,lemmas] ) 924 925val _ = remove_ovl_mapping "lrnext" {Name = "lrnext", Thy = "sptree"} 926 927val foldi_FOLDR_toAList_lemma = prove( 928 ``!t n a ls. foldi f n (FOLDR (UNCURRY f) a ls) t = 929 FOLDR (UNCURRY f) a (foldi (\k v a. (k,v)::a) n ls t)``, 930 Induct >> simp[foldi_def] >> 931 rw[] >> pop_assum(assume_tac o GSYM) >> simp[]) 932 933val foldi_FOLDR_toAList = store_thm("foldi_FOLDR_toAList", 934 ``!f a t. foldi f 0 a t = FOLDR (UNCURRY f) a (toAList t)``, 935 simp[toAList_def,GSYM foldi_FOLDR_toAList_lemma]) 936 937val toListA_def = Define` 938 (toListA acc LN = acc) /\ 939 (toListA acc (LS a) = a::acc) /\ 940 (toListA acc (BN t1 t2) = toListA (toListA acc t2) t1) /\ 941 (toListA acc (BS t1 a t2) = toListA (a :: toListA acc t2) t1) 942`; 943 944local open listTheory rich_listTheory in 945val toListA_append = store_thm("toListA_append", 946 ``!t acc. toListA acc t = toListA [] t ++ acc``, 947 Induct >> REWRITE_TAC[toListA_def] 948 >> metis_tac[APPEND_ASSOC,CONS_APPEND,APPEND]) 949end 950 951val isEmpty_toListA = store_thm("isEmpty_toListA", 952 ``!t acc. wf t ==> ((t = LN) <=> (toListA acc t = acc))``, 953 Induct >> simp[toListA_def,wf_def] >> 954 rw[] >> fs[] >> 955 fs[Once toListA_append] >> 956 simp[Once toListA_append,SimpR``$++``]) 957 958val toList_def = Define`toList m = toListA [] m` 959 960val isEmpty_toList = store_thm("isEmpty_toList", 961 ``!t. wf t ==> ((t = LN) <=> (toList t = []))``, 962 rw[toList_def,isEmpty_toListA]) 963 964val lem2 = 965 SIMP_RULE (srw_ss()) [] (Q.SPECL[`2`,`1`]DIV_MULT) 966 967fun tac () = ( 968 (disj2_tac >> qexists_tac`0` >> simp[] >> NO_TAC) ORELSE 969 (disj2_tac >> 970 qexists_tac`2*k+1` >> simp[] >> 971 REWRITE_TAC[Once MULT_COMM] >> simp[MULT_DIV] >> 972 rw[] >> `F` suffices_by rw[] >> pop_assum mp_tac >> 973 simp[lemmas,GSYM ODD_EVEN] >> NO_TAC) ORELSE 974 (disj2_tac >> 975 qexists_tac`2*k+2` >> simp[] >> 976 REWRITE_TAC[Once MULT_COMM] >> simp[lem2] >> 977 rw[] >> `F` suffices_by rw[] >> pop_assum mp_tac >> 978 simp[lemmas] >> NO_TAC) ORELSE 979 (metis_tac[])) 980 981val MEM_toListA = prove( 982 ``!t acc x. MEM x (toListA acc t) <=> (MEM x acc \/ ?k. lookup k t = SOME x)``, 983 Induct >> simp[toListA_def,lookup_def] >- metis_tac[] >> 984 rw[EQ_IMP_THM] >> rw[] >> pop_assum mp_tac >> rw[] 985 >- (tac()) 986 >- (tac()) 987 >- (tac()) 988 >- (tac()) 989 >- (tac()) 990 >- (tac()) 991 >- (tac()) 992 >- (tac()) 993 >- (tac())) 994 995val MEM_toList = store_thm("MEM_toList", 996 ``!x t. MEM x (toList t) <=> ?k. lookup k t = SOME x``, 997 rw[toList_def,MEM_toListA]) 998 999val div2_even_lemma = prove( 1000 ``!x. ?n. (x = (n - 1) DIV 2) /\ EVEN n /\ 0 < n``, 1001 Induct >- ( qexists_tac`2` >> simp[] ) >> fs[] >> 1002 qexists_tac`n+2` >> 1003 simp[ADD1,EVEN_ADD] >> 1004 Cases_on`n`>>fs[EVEN,EVEN_ODD,ODD_EXISTS,ADD1] >> 1005 simp[] >> rw[] >> 1006 qspec_then`2`mp_tac ADD_DIV_ADD_DIV >> simp[] >> 1007 disch_then(qspecl_then[`m`,`3`]mp_tac) >> 1008 simp[] >> disch_then kall_tac >> 1009 qspec_then`2`mp_tac ADD_DIV_ADD_DIV >> simp[] >> 1010 disch_then(qspecl_then[`m`,`1`]mp_tac) >> 1011 simp[]) 1012 1013val div2_odd_lemma = prove( 1014 ``!x. ?n. (x = (n - 1) DIV 2) /\ ODD n /\ 0 < n``, 1015 Induct >- ( qexists_tac`1` >> simp[] ) >> fs[] >> 1016 qexists_tac`n+2` >> 1017 simp[ADD1,ODD_ADD] >> 1018 fs[ODD_EXISTS,ADD1] >> 1019 simp[] >> rw[] >> 1020 qspec_then`2`mp_tac ADD_DIV_ADD_DIV >> simp[] >> 1021 disch_then(qspecl_then[`m`,`2`]mp_tac) >> 1022 simp[] >> disch_then kall_tac >> 1023 qspec_then`2`mp_tac ADD_DIV_ADD_DIV >> simp[] >> 1024 disch_then(qspecl_then[`m`,`0`]mp_tac) >> 1025 simp[]) 1026 1027val spt_eq_thm = store_thm("spt_eq_thm", 1028 ``!t1 t2. wf t1 /\ wf t2 ==> 1029 ((t1 = t2) <=> !n. lookup n t1 = lookup n t2)``, 1030 Induct >> simp[wf_def,lookup_def] 1031 >- ( 1032 rw[EQ_IMP_THM] >> rw[lookup_def] >> 1033 `domain t2 = {}` by ( 1034 simp[EXTENSION] >> 1035 metis_tac[lookup_NONE_domain] ) >> 1036 Cases_on`t2`>>fs[domain_def,wf_def] >> 1037 metis_tac[domain_empty] ) 1038 >- ( 1039 rw[EQ_IMP_THM] >> rw[lookup_def] >> 1040 Cases_on`t2`>>fs[lookup_def] 1041 >- (first_x_assum(qspec_then`0`mp_tac)>>simp[]) 1042 >- (first_x_assum(qspec_then`0`mp_tac)>>simp[]) >> 1043 fs[wf_def] >> 1044 rfs[domain_empty] >> 1045 fs[GSYM MEMBER_NOT_EMPTY] >> 1046 fs[domain_lookup] >| 1047 [ qspec_then`x`strip_assume_tac div2_even_lemma 1048 , qspec_then`x`strip_assume_tac div2_odd_lemma 1049 ] >> 1050 first_x_assum(qspec_then`n`mp_tac) >> 1051 fs[ODD_EVEN] >> simp[] ) 1052 >- ( 1053 rw[EQ_IMP_THM] >> rw[lookup_def] >> 1054 rfs[domain_empty] >> 1055 fs[GSYM MEMBER_NOT_EMPTY] >> 1056 fs[domain_lookup] >> 1057 Cases_on`t2`>>fs[] >> 1058 TRY ( 1059 first_x_assum(qspec_then`0`mp_tac) >> 1060 simp[lookup_def] >> NO_TAC) >> 1061 TRY ( 1062 qspec_then`x`strip_assume_tac div2_even_lemma >> 1063 first_x_assum(qspec_then`n`mp_tac) >> fs[] >> 1064 simp[lookup_def] >> NO_TAC) >> 1065 TRY ( 1066 qspec_then`x`strip_assume_tac div2_odd_lemma >> 1067 first_x_assum(qspec_then`n`mp_tac) >> fs[ODD_EVEN] >> 1068 simp[lookup_def] >> NO_TAC) >> 1069 qmatch_assum_rename_tac`wf (BN s1 s2)` >> 1070 `wf s1 /\ wf s2` by fs[wf_def] >> 1071 first_x_assum(qspec_then`s2`mp_tac) >> 1072 first_x_assum(qspec_then`s1`mp_tac) >> 1073 simp[] >> ntac 2 strip_tac >> 1074 fs[lookup_def] >> rw[] >> 1075 metis_tac[prim_recTheory.LESS_REFL,div2_even_lemma,div2_odd_lemma 1076 ,EVEN_ODD] ) 1077 >- ( 1078 rw[EQ_IMP_THM] >> rw[lookup_def] >> 1079 rfs[domain_empty] >> 1080 fs[GSYM MEMBER_NOT_EMPTY] >> 1081 fs[domain_lookup] >> 1082 Cases_on`t2`>>fs[] >> 1083 TRY ( 1084 first_x_assum(qspec_then`0`mp_tac) >> 1085 simp[lookup_def] >> NO_TAC) >> 1086 TRY ( 1087 qspec_then`x`strip_assume_tac div2_even_lemma >> 1088 first_x_assum(qspec_then`n`mp_tac) >> fs[] >> 1089 simp[lookup_def] >> NO_TAC) >> 1090 TRY ( 1091 qspec_then`x`strip_assume_tac div2_odd_lemma >> 1092 first_x_assum(qspec_then`n`mp_tac) >> fs[ODD_EVEN] >> 1093 simp[lookup_def] >> NO_TAC) >> 1094 qmatch_assum_rename_tac`wf (BS s1 z s2)` >> 1095 `wf s1 /\ wf s2` by fs[wf_def] >> 1096 first_x_assum(qspec_then`s2`mp_tac) >> 1097 first_x_assum(qspec_then`s1`mp_tac) >> 1098 simp[] >> ntac 2 strip_tac >> 1099 fs[lookup_def] >> rw[] >> 1100 metis_tac[prim_recTheory.LESS_REFL,div2_even_lemma,div2_odd_lemma 1101 ,EVEN_ODD,optionTheory.SOME_11] )) 1102 1103val mk_wf_def = Define ` 1104 (mk_wf LN = LN) /\ 1105 (mk_wf (LS x) = LS x) /\ 1106 (mk_wf (BN t1 t2) = mk_BN (mk_wf t1) (mk_wf t2)) /\ 1107 (mk_wf (BS t1 x t2) = mk_BS (mk_wf t1) x (mk_wf t2))`; 1108 1109val wf_mk_wf = store_thm("wf_mk_wf[simp]", 1110 ``!t. wf (mk_wf t)``, 1111 Induct \\ fs [wf_def,mk_wf_def,wf_mk_BS,wf_mk_BN]); 1112 1113val wf_mk_id = store_thm("wf_mk_id[simp]", 1114 ``!t. wf t ==> (mk_wf t = t)``, 1115 Induct \\ srw_tac [] [wf_def,mk_wf_def,mk_BS_thm,mk_BN_thm]); 1116 1117val lookup_mk_wf = store_thm("lookup_mk_wf[simp]", 1118 ``!x t. lookup x (mk_wf t) = lookup x t``, 1119 Induct_on `t` \\ fs [mk_wf_def,lookup_mk_BS,lookup_mk_BN] 1120 \\ srw_tac [] [lookup_def]); 1121 1122val domain_mk_wf = store_thm("domain_mk_wf[simp]", 1123 ``!t. domain (mk_wf t) = domain t``, 1124 fs [EXTENSION,domain_lookup]); 1125 1126val mk_wf_eq = store_thm("mk_wf_eq[simp]", 1127 ``!t1 t2. (mk_wf t1 = mk_wf t2) <=> !x. lookup x t1 = lookup x t2``, 1128 metis_tac [spt_eq_thm,wf_mk_wf,lookup_mk_wf]); 1129 1130val inter_eq = store_thm("inter_eq[simp]", 1131 ``!t1 t2 t3 t4. 1132 (inter t1 t2 = inter t3 t4) <=> 1133 !x. lookup x (inter t1 t2) = lookup x (inter t3 t4)``, 1134 metis_tac [spt_eq_thm,wf_inter]); 1135 1136val union_mk_wf = store_thm("union_mk_wf[simp]", 1137 ``!t1 t2. union (mk_wf t1) (mk_wf t2) = mk_wf (union t1 t2)``, 1138 REPEAT STRIP_TAC 1139 \\ `union (mk_wf t1) (mk_wf t2) = mk_wf (union (mk_wf t1) (mk_wf t2))` by 1140 metis_tac [wf_union,wf_mk_wf,wf_mk_id] 1141 \\ POP_ASSUM (fn th => once_rewrite_tac [th]) 1142 \\ ASM_SIMP_TAC std_ss [mk_wf_eq] \\ fs [lookup_union]); 1143 1144val inter_mk_wf = store_thm("inter_mk_wf[simp]", 1145 ``!t1 t2. inter (mk_wf t1) (mk_wf t2) = mk_wf (inter t1 t2)``, 1146 REPEAT STRIP_TAC 1147 \\ `inter (mk_wf t1) (mk_wf t2) = mk_wf (inter (mk_wf t1) (mk_wf t2))` by 1148 metis_tac [wf_inter,wf_mk_wf,wf_mk_id] 1149 \\ POP_ASSUM (fn th => once_rewrite_tac [th]) 1150 \\ ASM_SIMP_TAC std_ss [mk_wf_eq] \\ fs [lookup_inter]); 1151 1152val insert_mk_wf = store_thm("insert_mk_wf[simp]", 1153 ``!x v t. insert x v (mk_wf t) = mk_wf (insert x v t)``, 1154 REPEAT STRIP_TAC 1155 \\ `insert x v (mk_wf t) = mk_wf (insert x v (mk_wf t))` by 1156 metis_tac [wf_insert,wf_mk_wf,wf_mk_id] 1157 \\ POP_ASSUM (fn th => once_rewrite_tac [th]) 1158 \\ ASM_SIMP_TAC std_ss [mk_wf_eq] \\ fs [lookup_insert]); 1159 1160val delete_mk_wf = store_thm("delete_mk_wf[simp]", 1161 ``!x t. delete x (mk_wf t) = mk_wf (delete x t)``, 1162 REPEAT STRIP_TAC 1163 \\ `delete x (mk_wf t) = mk_wf (delete x (mk_wf t))` by 1164 metis_tac [wf_delete,wf_mk_wf,wf_mk_id] 1165 \\ POP_ASSUM (fn th => once_rewrite_tac [th]) 1166 \\ ASM_SIMP_TAC std_ss [mk_wf_eq] \\ fs [lookup_delete]); 1167 1168val union_LN = store_thm("union_LN[simp]", 1169 ``!t. (union t LN = t) /\ (union LN t = t)``, 1170 Cases \\ fs [union_def]); 1171 1172val inter_LN = store_thm("inter_LN[simp]", 1173 ``!t. (inter t LN = LN) /\ (inter LN t = LN)``, 1174 Cases \\ fs [inter_def]); 1175 1176val union_assoc = store_thm("union_assoc", 1177 ``!t1 t2 t3. union t1 (union t2 t3) = union (union t1 t2) t3``, 1178 Induct \\ Cases_on `t2` \\ Cases_on `t3` \\ fs [union_def]); 1179 1180val inter_assoc = store_thm("inter_assoc", 1181 ``!t1 t2 t3. inter t1 (inter t2 t3) = inter (inter t1 t2) t3``, 1182 fs [lookup_inter] \\ REPEAT STRIP_TAC 1183 \\ Cases_on `lookup x t1` \\ fs [] 1184 \\ Cases_on `lookup x t2` \\ fs [] 1185 \\ Cases_on `lookup x t3` \\ fs []); 1186 1187val numeral_div0 = prove( 1188 ``(BIT1 n DIV 2 = n) /\ 1189 (BIT2 n DIV 2 = SUC n) /\ 1190 (SUC (BIT1 n) DIV 2 = SUC n) /\ 1191 (SUC (BIT2 n) DIV 2 = SUC n)``, 1192 REWRITE_TAC[GSYM DIV2_def, numeralTheory.numeral_suc, 1193 REWRITE_RULE [NUMERAL_DEF] 1194 numeralTheory.numeral_div2]) 1195val BIT0 = prove( 1196 ``BIT1 n <> 0 /\ BIT2 n <> 0``, 1197 REWRITE_TAC[BIT1, BIT2, 1198 ADD_CLAUSES, numTheory.NOT_SUC]); 1199 1200val PRE_BIT1 = prove( 1201 ``BIT1 n - 1 = 2 * n``, 1202 REWRITE_TAC [BIT1, NUMERAL_DEF, 1203 ALT_ZERO, ADD_CLAUSES, 1204 BIT2, SUB_MONO_EQ, 1205 MULT_CLAUSES, SUB_0]); 1206 1207val PRE_BIT2 = prove( 1208 ``BIT2 n - 1 = 2 * n + 1``, 1209 REWRITE_TAC [BIT1, NUMERAL_DEF, 1210 ALT_ZERO, ADD_CLAUSES, 1211 BIT2, SUB_MONO_EQ, 1212 MULT_CLAUSES, SUB_0]); 1213 1214val BITDIV = prove( 1215 ``((BIT1 n - 1) DIV 2 = n) /\ ((BIT2 n - 1) DIV 2 = n)``, 1216 simp[PRE_BIT1, PRE_BIT2] >> simp[DIV_EQ_X]); 1217 1218fun computerule th q = 1219 th 1220 |> CONJUNCTS 1221 |> map SPEC_ALL 1222 |> map (Q.INST [`k` |-> q]) 1223 |> map (CONV_RULE 1224 (RAND_CONV (SIMP_CONV bool_ss 1225 ([numeral_div0, BIT0, PRE_BIT1, 1226 numTheory.NOT_SUC, BITDIV, 1227 EVAL ``SUC 0 DIV 2``, 1228 numeralTheory.numeral_evenodd, 1229 EVEN]) THENC 1230 SIMP_CONV bool_ss [ALT_ZERO]))) 1231 1232val lookup_compute = save_thm( 1233 "lookup_compute", 1234 LIST_CONJ (prove (``lookup (NUMERAL n) t = lookup n t``, 1235 REWRITE_TAC [NUMERAL_DEF]) :: 1236 computerule lookup_def `0` @ 1237 computerule lookup_def `ZERO` @ 1238 computerule lookup_def `BIT1 n` @ 1239 computerule lookup_def `BIT2 n`)) 1240val _ = computeLib.add_persistent_funs ["lookup_compute"] 1241 1242val insert_compute = save_thm( 1243 "insert_compute", 1244 LIST_CONJ (prove (``insert (NUMERAL n) a t = insert n a t``, 1245 REWRITE_TAC [NUMERAL_DEF]) :: 1246 computerule insert_def `0` @ 1247 computerule insert_def `ZERO` @ 1248 computerule insert_def `BIT1 n` @ 1249 computerule insert_def `BIT2 n`)) 1250val _ = computeLib.add_persistent_funs ["insert_compute"] 1251 1252val delete_compute = save_thm( 1253 "delete_compute", 1254 LIST_CONJ ( 1255 prove(``delete (NUMERAL n) t = delete n t``, 1256 REWRITE_TAC [NUMERAL_DEF]) :: 1257 computerule delete_def `0` @ 1258 computerule delete_def `ZERO` @ 1259 computerule delete_def `BIT1 n` @ 1260 computerule delete_def `BIT2 n`)) 1261val _ = computeLib.add_persistent_funs ["delete_compute"] 1262 1263val fromAList_def = Define ` 1264 (fromAList [] = LN) /\ 1265 (fromAList ((x,y)::xs) = insert x y (fromAList xs))`; 1266 1267val fromAList_ind = theorem "fromAList_ind" 1268 1269val lookup_fromAList = store_thm("lookup_fromAList", 1270 ``!ls x.lookup x (fromAList ls) = ALOOKUP ls x``, 1271 ho_match_mp_tac fromAList_ind >> 1272 rw[fromAList_def,lookup_def] >> 1273 fs[lookup_insert]>> simp[EQ_SYM_EQ]) 1274 1275val domain_fromAList = store_thm("domain_fromAList", 1276 ``!ls. domain (fromAList ls) = set (MAP FST ls)``, 1277 simp[EXTENSION,domain_lookup,lookup_fromAList, 1278 MEM_MAP,pairTheory.EXISTS_PROD]>> 1279 metis_tac[ALOOKUP_MEM,ALOOKUP_FAILS, 1280 optionTheory.option_CASES, 1281 optionTheory.NOT_SOME_NONE]) 1282 1283val lookup_fromAList_toAList = store_thm("lookup_fromAList_toAList", 1284 ``!t x. lookup x (fromAList (toAList t)) = lookup x t``, 1285 simp[lookup_fromAList,ALOOKUP_toAList]) 1286 1287val wf_fromAList = store_thm("wf_fromAList", 1288 ``!ls. wf (fromAList ls)``, 1289 Induct >> 1290 rw[fromAList_def,wf_def]>> 1291 Cases_on`h`>> 1292 rw[fromAList_def]>> 1293 simp[wf_insert]) 1294 1295val fromAList_toAList = store_thm("fromAList_toAList", 1296 ``!t. wf t ==> (fromAList (toAList t) = t)``, 1297 metis_tac[wf_fromAList,lookup_fromAList_toAList,spt_eq_thm]) 1298 1299Theorem union_insert_LN: 1300 !x y t2. union (insert x y LN) t2 = insert x y t2 1301Proof 1302 recInduct insert_ind 1303 \\ rw[] 1304 \\ rw[Once insert_def] 1305 \\ rw[Once insert_def,SimpRHS] 1306 \\ rw[union_def] 1307QED 1308 1309Theorem fromAList_append: 1310 !l1 l2. fromAList (l1 ++ l2) = union (fromAList l1) (fromAList l2) 1311Proof 1312 recInduct fromAList_ind 1313 \\ rw[fromAList_def] 1314 \\ rw[Once insert_union] 1315 \\ rw[union_assoc] 1316 \\ AP_THM_TAC 1317 \\ AP_TERM_TAC 1318 \\ rw[union_insert_LN] 1319QED 1320 1321val map_def = Define` 1322 (map f LN = LN) /\ 1323 (map f (LS a) = (LS (f a))) /\ 1324 (map f (BN t1 t2) = BN (map f t1) (map f t2)) /\ 1325 (map f (BS t1 a t2) = BS (map f t1) (f a) (map f t2))` 1326 1327val toList_map = store_thm("toList_map", 1328 ``!s. toList (map f s) = MAP f (toList s)``, 1329 Induct >> 1330 fs[toList_def,map_def,toListA_def] >> 1331 simp[Once toListA_append] >> 1332 simp[Once toListA_append,SimpRHS]) 1333 1334val domain_map = store_thm("domain_map", 1335 ``!s. domain (map f s) = domain s``, 1336 Induct >> simp[map_def]) 1337 1338val lookup_map = store_thm("lookup_map", 1339 ``!s x. lookup x (map f s) = OPTION_MAP f (lookup x s)``, 1340 Induct >> simp[map_def,lookup_def] >> rw[]) 1341 1342val map_LN = store_thm("map_LN[simp]", 1343 ``!t. (map f t = LN) <=> (t = LN)``, 1344 Cases \\ EVAL_TAC); 1345 1346val wf_map = store_thm("wf_map[simp]", 1347 ``!t f. wf (map f t) = wf t``, 1348 Induct \\ fs [wf_def,map_def]); 1349 1350val map_map_o = store_thm("map_map_o", 1351 ``!t f g. map f (map g t) = map (f o g) t``, 1352 Induct >> fs[map_def]) 1353 1354val map_insert = store_thm("map_insert", 1355 ``!f x y z. 1356 map f (insert x y z) = insert x (f y) (map f z)``, 1357 completeInduct_on`x`>> 1358 Induct_on`z`>> 1359 rw[]>> 1360 simp[Once map_def,Once insert_def]>> 1361 simp[Once insert_def,SimpRHS]>> 1362 BasicProvers.EVERY_CASE_TAC>>fs[map_def]>> 1363 `(x-1) DIV 2 < x` by 1364 (`0 < (2:num)` by fs[] >> 1365 imp_res_tac DIV_LT_X>> 1366 first_x_assum match_mp_tac>> 1367 DECIDE_TAC)>> 1368 fs[map_def]); 1369 1370Theorem map_fromAList: 1371 map f (fromAList ls) = fromAList (MAP (\ (k,v). (k, f v)) ls) 1372Proof 1373 Induct_on`ls` >> simp[fromAList_def] >> 1374 Cases >> simp[fromAList_def] >> 1375 simp[wf_fromAList,map_insert] 1376QED 1377 1378val insert_insert = store_thm("insert_insert", 1379 ``!x1 x2 v1 v2 t. 1380 insert x1 v1 (insert x2 v2 t) = 1381 if x1 = x2 then insert x1 v1 t else insert x2 v2 (insert x1 v1 t)``, 1382 rpt strip_tac 1383 \\ qspec_tac (`x1`,`x1`) 1384 \\ qspec_tac (`v1`,`v1`) 1385 \\ qspec_tac (`t`,`t`) 1386 \\ qspec_tac (`v2`,`v2`) 1387 \\ qspec_tac (`x2`,`x2`) 1388 \\ recInduct insert_ind \\ rpt strip_tac \\ 1389 (Cases_on `k = 0` \\ fs [] THEN1 1390 (once_rewrite_tac [insert_def] \\ fs [] \\ rw [] 1391 THEN1 (once_rewrite_tac [insert_def] \\ fs []) 1392 \\ once_rewrite_tac [insert_def] \\ fs [] \\ rw []) 1393 \\ once_rewrite_tac [insert_def] \\ fs [] \\ rw [] 1394 \\ simp [Once insert_def] 1395 \\ once_rewrite_tac [EQ_SYM_EQ] 1396 \\ simp [Once insert_def] 1397 \\ Cases_on `x1` \\ fs [ADD1] 1398 \\ Cases_on `k` \\ fs [ADD1] 1399 \\ rw [] \\ fs [EVEN_ADD] 1400 \\ fs [GSYM ODD_EVEN] 1401 \\ fs [EVEN_EXISTS,ODD_EXISTS] \\ rpt BasicProvers.var_eq_tac 1402 \\ fs [ADD1,DIV_MULT|>ONCE_REWRITE_RULE[MULT_COMM], 1403 MULT_DIV|>ONCE_REWRITE_RULE[MULT_COMM]])); 1404 1405val insert_shadow = store_thm("insert_shadow", 1406 ``!t a b c. insert a b (insert a c t) = insert a b t``, 1407 once_rewrite_tac [insert_insert] \\ simp []); 1408 1409(* the sub-map relation, a partial order *) 1410 1411val spt_left_def = Define ` 1412 (spt_left LN = LN) /\ 1413 (spt_left (LS x) = LN) /\ 1414 (spt_left (BN t1 t2) = t1) /\ 1415 (spt_left (BS t1 x t2) = t1)` 1416 1417val spt_right_def = Define ` 1418 (spt_right LN = LN) /\ 1419 (spt_right (LS x) = LN) /\ 1420 (spt_right (BN t1 t2) = t2) /\ 1421 (spt_right (BS t1 x t2) = t2)` 1422 1423val spt_center_def = Define ` 1424 (spt_center (LS x) = SOME x) /\ 1425 (spt_center (BS t1 x t2) = SOME x) /\ 1426 (spt_center _ = NONE)` 1427 1428val subspt_eq = Define ` 1429 (subspt LN t <=> T) /\ 1430 (subspt (LS x) t <=> (spt_center t = SOME x)) /\ 1431 (subspt (BN t1 t2) t <=> 1432 subspt t1 (spt_left t) /\ subspt t2 (spt_right t)) /\ 1433 (subspt (BS t1 x t2) t <=> 1434 (spt_center t = SOME x) /\ 1435 subspt t1 (spt_left t) /\ subspt t2 (spt_right t))` 1436 1437val _ = save_thm("subspt_eq",subspt_eq); 1438 1439val subspt_lookup_lemma = Q.prove( 1440 `(!x y. ((if x = 0:num then SOME a else f x) = SOME y) ==> p x y) 1441 <=> 1442 p 0 a /\ (!x y. x <> 0 /\ (f x = SOME y) ==> p x y)`, 1443 metis_tac [optionTheory.SOME_11]); 1444 1445val subspt_lookup = Q.store_thm("subspt_lookup", 1446 `!t1 t2. 1447 subspt t1 t2 <=> 1448 !x y. (lookup x t1 = SOME y) ==> (lookup x t2 = SOME y)`, 1449 Induct 1450 \\ fs [lookup_def,subspt_eq] 1451 THEN1 (Cases_on `t2` \\ fs [lookup_def,spt_center_def]) 1452 \\ rw [] 1453 THEN1 1454 (Cases_on `t2` 1455 \\ fs [lookup_def,spt_center_def,spt_left_def,spt_right_def] 1456 \\ eq_tac \\ rw [] 1457 \\ TRY (Cases_on `x = 0` \\ fs [] \\ rw [] \\ fs [] \\ NO_TAC) 1458 \\ TRY (first_x_assum (fn th => qspec_then `2 * x + 1` mp_tac th THEN 1459 qspec_then `(2 * x + 1) + 1` mp_tac th)) 1460 \\ fs [MULT_DIV |> ONCE_REWRITE_RULE [MULT_COMM], 1461 DIV_MULT |> ONCE_REWRITE_RULE [MULT_COMM]] 1462 \\ fs [EVEN_ADD,EVEN_DOUBLE]) 1463 \\ Cases_on `spt_center t2` \\ fs [] 1464 THEN1 1465 (qexists_tac `0` \\ fs [] 1466 \\ Cases_on `t2` \\ fs [spt_center_def,lookup_def]) 1467 \\ reverse (Cases_on `x = a`) \\ fs [] 1468 THEN1 1469 (qexists_tac `0` \\ fs [] 1470 \\ Cases_on `t2` \\ fs [spt_center_def,lookup_def]) 1471 \\ BasicProvers.var_eq_tac 1472 \\ fs [subspt_lookup_lemma] 1473 \\ `lookup 0 t2 = SOME a` by 1474 (Cases_on `t2` \\ fs [spt_center_def,lookup_def]) 1475 \\ fs [] 1476 \\ Cases_on `t2` 1477 \\ fs [lookup_def,spt_center_def,spt_left_def,spt_right_def] 1478 \\ eq_tac \\ rw [] 1479 \\ TRY (Cases_on `x = 0` \\ fs [] \\ rw [] \\ fs [] \\ NO_TAC) 1480 \\ TRY (first_x_assum (fn th => qspec_then `2 * x + 1` mp_tac th THEN 1481 qspec_then `(2 * x + 1) + 1` mp_tac th)) 1482 \\ fs [MULT_DIV |> ONCE_REWRITE_RULE [MULT_COMM], 1483 DIV_MULT |> ONCE_REWRITE_RULE [MULT_COMM]] 1484 \\ fs [EVEN_ADD,EVEN_DOUBLE]); 1485 1486val subspt_domain = Q.store_thm("subspt_domain", 1487 `!t1 (t2:unit spt). 1488 subspt t1 t2 <=> domain t1 SUBSET domain t2`, 1489 fs [subspt_lookup,domain_lookup,SUBSET_DEF]); 1490 1491val subspt_def = Q.store_thm("subspt_def", 1492 `!sp1 sp2. 1493 subspt sp1 sp2 <=> 1494 !k. k IN domain sp1 ==> k IN domain sp2 /\ 1495 (lookup k sp2 = lookup k sp1)`, 1496 fs [subspt_lookup,domain_lookup] 1497 \\ metis_tac [optionTheory.SOME_11]); 1498 1499val subspt_refl = Q.store_thm( 1500 "subspt_refl[simp]", 1501 `subspt sp sp`, 1502 simp[subspt_def]) 1503 1504val subspt_trans = Q.store_thm( 1505 "subspt_trans", 1506 `subspt sp1 sp2 /\ subspt sp2 sp3 ==> subspt sp1 sp3`, 1507 simp [subspt_lookup]); 1508 1509val subspt_LN = Q.store_thm( 1510 "subspt_LN[simp]", 1511 `(subspt LN sp <=> T) /\ (subspt sp LN <=> (domain sp = {}))`, 1512 simp[subspt_def, EXTENSION]); 1513 1514Theorem subspt_union: subspt s (union s t) 1515Proof fs[subspt_lookup,lookup_union] 1516QED 1517 1518Theorem subspt_FOLDL_union: 1519 !ls t. subspt t (FOLDL union t ls) 1520Proof 1521 Induct \\ rw[] \\ metis_tac[subspt_union,subspt_trans] 1522QED 1523 1524Theorem domain_mapi[simp]: 1525 domain (mapi f x) = domain x 1526Proof fs [domain_lookup,EXTENSION,lookup_mapi] 1527QED 1528 1529Theorem lookup_FOLDL_union: 1530 lookup k (FOLDL union t ls) = 1531 FOLDL OPTION_CHOICE (lookup k t) (MAP (lookup k) ls) 1532Proof 1533 qid_spec_tac���t��� >> Induct_on���ls��� >> rw[lookup_union] >> 1534 BasicProvers.TOP_CASE_TAC >> simp[] 1535QED 1536 1537Theorem map_union: 1538 !t1 t2. map f (union t1 t2) = union (map f t1) (map f t2) 1539Proof 1540 Induct >> rw[map_def,union_def] >> 1541 BasicProvers.TOP_CASE_TAC >> rw[map_def,union_def] 1542QED 1543 1544Theorem domain_eq: 1545 !t1 t2. (domain t1 = domain t2) <=> 1546 !k. (lookup k t1 = NONE) <=> (lookup k t2 = NONE) 1547Proof 1548 rw [domain_lookup,EXTENSION] \\ eq_tac \\ rw [] 1549 >- (pop_assum (qspec_then `k` mp_tac) 1550 \\ Cases_on `lookup k t1` \\ fs [] 1551 \\ Cases_on `lookup k t2` \\ fs []) 1552 >- (pop_assum (qspec_then `x` mp_tac) 1553 \\ Cases_on `lookup x t1` \\ fs [] 1554 \\ Cases_on `lookup x t2` \\ fs []) 1555QED 1556 1557(* filter values stored in sptree *) 1558 1559val filter_v_def = Define ` 1560 (filter_v f LN = LN) /\ 1561 (filter_v f (LS x) = if f x then LS x else LN) /\ 1562 (filter_v f (BN l r) = mk_BN (filter_v f l) (filter_v f r)) /\ 1563 (filter_v f (BS l x r) = 1564 if f x then mk_BS (filter_v f l) x (filter_v f r) 1565 else mk_BN (filter_v f l) (filter_v f r))`; 1566 1567val lookup_filter_v = store_thm("lookup_filter_v", 1568 ``!k t f. lookup k (filter_v f t) = case lookup k t of 1569 | SOME v => if f v then SOME v else NONE 1570 | NONE => NONE``, 1571 ho_match_mp_tac (theorem "lookup_ind") \\ rpt strip_tac \\ 1572 rw [filter_v_def, lookup_mk_BS, lookup_mk_BN] \\ rw [lookup_def] \\ fs []); 1573 1574val wf_filter_v = store_thm("wf_filter_v", 1575 ``!t f. wf t ==> wf (filter_v f t)``, 1576 Induct \\ rw [filter_v_def, wf_def, mk_BN_thm, mk_BS_thm] \\ fs []); 1577 1578val wf_mk_BN = Q.store_thm( 1579 "wf_mk_BN", 1580 `wf t1 /\ wf t2 ==> wf (mk_BN t1 t2)`, 1581 map_every Cases_on [`t1`, `t2`] >> simp[mk_BN_def, wf_def]) 1582 1583val wf_mk_BS = Q.store_thm( 1584 "wf_mk_BS", 1585 `wf t1 /\ wf t2 ==> wf (mk_BS t1 a t2)`, 1586 map_every Cases_on [`t1`, `t2`] >> simp[mk_BS_def, wf_def]) 1587 1588val wf_mapi = Q.store_thm( 1589 "wf_mapi", 1590 `wf (mapi f pt)`, 1591 simp[mapi_def] >> 1592 `!n. wf (mapi0 f n pt)` suffices_by simp[] >> Induct_on `pt` >> 1593 simp[wf_def, wf_mk_BN, wf_mk_BS]); 1594 1595val ALOOKUP_MAP_lemma = Q.prove( 1596 `ALOOKUP (MAP (\kv. (FST kv, f (FST kv) (SND kv))) al) n = 1597 OPTION_MAP (\v. f n v) (ALOOKUP al n)`, 1598 Induct_on `al` >> simp[pairTheory.FORALL_PROD] >> rw[]); 1599 1600val lookup_mk_BN = Q.store_thm( 1601 "lookup_mk_BN", 1602 `lookup i (mk_BN t1 t2) = 1603 if i = 0 then NONE 1604 else lookup ((i - 1) DIV 2) (if EVEN i then t1 else t2)`, 1605 map_every Cases_on [`t1`, `t2`] >> simp[mk_BN_def, lookup_def]); 1606 1607val MAP_foldi = Q.store_thm( 1608 "MAP_foldi", 1609 `!n acc. MAP f (foldi (\k v a. (k,v)::a) n acc pt) = 1610 foldi (\k v a. (f (k,v)::a)) n (MAP f acc) pt`, 1611 Induct_on `pt` >> simp[foldi_def]); 1612 1613val mapi_Alist = Q.store_thm( 1614 "mapi_Alist", 1615 `mapi f pt = 1616 fromAList (MAP (\kv. (FST kv,f (FST kv) (SND kv))) (toAList pt))`, 1617 simp[spt_eq_thm, wf_mapi, wf_fromAList, lookup_fromAList] >> 1618 srw_tac[boolSimps.ETA_ss][lookup_mapi, ALOOKUP_MAP_lemma, ALOOKUP_toAList]); 1619 1620val size_domain = Q.store_thm("size_domain", 1621 `!t. size t = CARD (domain t)`, 1622 Induct_on `t` 1623 >- rw[size_def, domain_def] 1624 >- rw[size_def, domain_def] 1625 >> rw[CARD_UNION_EQN, CARD_INJ_IMAGE] 1626 >- 1627 (`IMAGE (\n. 2 * n + 2) (domain t) INTER 1628 IMAGE (\n. 2 * n + 1) (domain t') = {}` 1629 by (rw[GSYM DISJOINT_DEF, IN_DISJOINT] 1630 >> Cases_on `ODD x` 1631 >> fs[ODD_EXISTS, ADD1, oddevenlemma]) 1632 >> simp[]) >> 1633 `(({0} INTER IMAGE (\n. 2 * n + 2) (domain t)) = {}) /\ 1634 (({0} UNION (IMAGE (\n. 2 * n + 2) (domain t))) 1635 INTER (IMAGE (\n. 2 * n + 1) (domain t')) = {})` 1636 by (rw[GSYM DISJOINT_DEF, IN_DISJOINT] 1637 >> Cases_on `ODD x` 1638 >> fs[ODD_EXISTS, ADD1, oddevenlemma]) 1639 >> simp[]); 1640 1641val num_set_domain_eq = Q.store_thm("num_set_domain_eq", 1642 `!t1 t2:unit spt. 1643 wf t1 /\ wf t2 ==> 1644 ((domain t1 = domain t2) <=> (t1 = t2))`, 1645 rw[] >> EQ_TAC >> rw[spt_eq_thm] >> 1646 fs[EXTENSION, domain_lookup] >> 1647 pop_assum (qspec_then `n` mp_tac) >> strip_tac >> 1648 Cases_on `lookup n t1` >> fs[] >> Cases_on `lookup n t2` >> fs[]); 1649 1650val union_num_set_sym = Q.store_thm ("union_num_set_sym", 1651 `!(t1:unit spt) t2. union t1 t2 = union t2 t1`, 1652 Induct >> fs[union_def] >> rw[] >> CASE_TAC >> fs[union_def]); 1653 1654val difference_sub = Q.store_thm("difference_sub", 1655 `(difference a b = LN) ==> (domain a SUBSET domain b)`, 1656 rw[] >> 1657 `(domain (difference a b) = {})` by rw[domain_def] >> 1658 fs[EXTENSION, domain_difference, SUBSET_DEF] >> 1659 metis_tac[]); 1660 1661val wf_difference = Q.store_thm("wf_difference", 1662 `!t1 t2. wf t1 /\ wf t2 ==> wf (difference t1 t2)`, 1663 Induct >> rw[difference_def, wf_def] >> CASE_TAC >> fs[wf_def] 1664 >> rw[wf_def, wf_mk_BN, wf_mk_BS]); 1665 1666val delete_fail = Q.store_thm ("delete_fail", 1667 `!n t. wf t ==> (~(n IN domain t) <=> (delete n t = t))`, 1668 simp[domain_lookup] >> 1669 recInduct (fetch "-" "lookup_ind") >> 1670 rw[lookup_def, wf_def, delete_def, mk_BN_thm, mk_BS_thm]); 1671 1672val size_delete = Q.store_thm ( "size_delete", 1673 `!n t . size (delete n t) = 1674 if lookup n t = NONE then size t else size t - 1`, 1675 rw[size_def] >> fs[lookup_NONE_domain] >> 1676 TRY (qpat_assum `n NOTIN d` (qspecl_then [] mp_tac)) >> 1677 rfs[delete_fail, size_def] >> 1678 fs[size_domain,lookup_NONE_domain,size_domain]); 1679 1680val lookup_fromList_outside = Q.store_thm("lookup_fromList_outside", 1681 `!k. LENGTH args <= k ==> (lookup k (fromList args) = NONE)`, 1682 SIMP_TAC std_ss [lookup_fromList] \\ DECIDE_TAC); 1683 1684val lemmas = Q.prove( 1685 `(2 + 2 * n - 1 = 2 * n + 1:num) /\ 1686 ((2 + 2 * n' = 2 * n'' + 2) <=> (n' = n'':num)) /\ 1687 ((2 * m = 2 * n) <=> (m = n)) /\ 1688 ((2 * n'' + 1) DIV 2 = n'') /\ 1689 ((2 * n) DIV 2 = n) /\ 1690 (2 + 2 * n' <> 2 * n'' + 1) /\ 1691 (2 * m + 1 <> 2 * n' + 2)`, 1692 REPEAT STRIP_TAC \\ SIMP_TAC std_ss [] \\ fs [] 1693 \\ full_simp_tac(srw_ss())[ONCE_REWRITE_RULE [MULT_COMM] MULT_DIV] 1694 \\ full_simp_tac(srw_ss())[ONCE_REWRITE_RULE [MULT_COMM] DIV_MULT] 1695 \\ IMP_RES_TAC (METIS_PROVE [] ``(m = n) ==> (m MOD 2 = n MOD 2)``) 1696 \\ POP_ASSUM MP_TAC \\ SIMP_TAC std_ss [] 1697 \\ ONCE_REWRITE_TAC [MATCH_MP (GSYM MOD_PLUS) (DECIDE ``0 < 2:num``)] 1698 \\ EVAL_TAC \\ fs[MOD_EQ_0,ONCE_REWRITE_RULE [MULT_COMM] MOD_EQ_0]); 1699 1700val IN_domain = Q.store_thm("IN_domain", 1701 `!n x t1 t2. 1702 (n IN domain LN <=> F) /\ 1703 (n IN domain (LS x) <=> (n = 0)) /\ 1704 (n IN domain (BN t1 t2) <=> 1705 (n <> 0 /\ (if EVEN n then ((n-1) DIV 2) IN domain t1 1706 else ((n-1) DIV 2) IN domain t2))) /\ 1707 (n IN domain (BS t1 x t2) <=> 1708 ((n = 0) \/ (if EVEN n then ((n-1) DIV 2) IN domain t1 1709 else ((n-1) DIV 2) IN domain t2)))`, 1710 full_simp_tac(srw_ss())[domain_def] \\ REPEAT STRIP_TAC 1711 \\ Cases_on `n = 0` \\ full_simp_tac(srw_ss())[] 1712 \\ Cases_on `EVEN n` \\ full_simp_tac(srw_ss())[] 1713 \\ full_simp_tac(srw_ss())[GSYM ODD_EVEN] 1714 \\ IMP_RES_TAC EVEN_ODD_EXISTS 1715 \\ full_simp_tac(srw_ss())[ADD1] \\ full_simp_tac(srw_ss())[lemmas] 1716 \\ Cases_on `m` \\ full_simp_tac(srw_ss())[MULT_CLAUSES] 1717 \\ REPEAT STRIP_TAC \\ EQ_TAC \\ REPEAT STRIP_TAC 1718 \\ full_simp_tac(srw_ss())[lemmas]) 1719 1720val map_map_K = Q.store_thm("map_map_K", 1721 `!t. map (K a) (map f t) = map (K a) t`, 1722 Induct \\ full_simp_tac(srw_ss())[map_def]); 1723 1724val lookup_map_K = Q.store_thm("lookup_map_K", 1725 `!t n. lookup n (map (K x) t) = if n IN domain t then SOME x else NONE`, 1726 Induct \\ full_simp_tac(srw_ss())[IN_domain,map_def,lookup_def] 1727 \\ REPEAT STRIP_TAC \\ Cases_on `n = 0` \\ full_simp_tac(srw_ss())[] 1728 \\ Cases_on `EVEN n` \\ full_simp_tac(srw_ss())[]); 1729 1730val spt_fold_def = Define ` 1731 (spt_fold f acc LN = acc) /\ 1732 (spt_fold f acc (LS a) = f a acc) /\ 1733 (spt_fold f acc (BN t1 t2) = spt_fold f (spt_fold f acc t1) t2) /\ 1734 (spt_fold f acc (BS t1 a t2) = spt_fold f (f a (spt_fold f acc t1)) t2)` 1735 1736val IMP_size_LESS_size = store_thm("IMP_size_LESS_size", 1737 ``!x y. subspt x y /\ domain x <> domain y ==> size x < size y``, 1738 fs [size_domain,domain_difference] \\ rw [] 1739 \\ `?t. (domain y = domain x UNION t) /\ t <> EMPTY /\ 1740 (domain x INTER t = EMPTY)` by 1741 (qexists_tac `domain y DIFF domain x` 1742 \\ fs [EXTENSION] 1743 \\ qsuff_tac `domain x SUBSET domain y` 1744 THEN1 (fs [EXTENSION,SUBSET_DEF] \\ metis_tac []) 1745 \\ fs [domain_lookup,subspt_lookup,SUBSET_DEF] 1746 \\ rw [] \\ res_tac \\ fs []) 1747 \\ asm_rewrite_tac [] 1748 \\ `FINITE (domain y)` by fs [FINITE_domain] 1749 \\ `FINITE t` by metis_tac [FINITE_UNION] 1750 \\ fs [CARD_UNION_EQN] 1751 \\ `CARD t <> 0` by metis_tac [CARD_EQ_0] \\ fs []); 1752 1753val size_diff_less = store_thm("size_diff_less", 1754 ``!x y z t. 1755 domain z SUBSET domain y /\ t IN domain y /\ 1756 ~(t IN domain z) /\ t IN domain x ==> 1757 size (difference x y) < size (difference x z)``, 1758 rw [] 1759 \\ match_mp_tac IMP_size_LESS_size 1760 \\ fs [domain_difference,EXTENSION] 1761 \\ reverse conj_tac THEN1 metis_tac [] 1762 \\ fs [subspt_lookup,lookup_difference] 1763 \\ rw [] \\ fs [SUBSET_DEF,domain_lookup,PULL_EXISTS] 1764 \\ CCONTR_TAC 1765 \\ Cases_on `lookup x' z` \\ fs [] 1766 \\ res_tac \\ fs []); 1767 1768val inter_eq_LN = store_thm("inter_eq_LN", 1769 ``!x y. (inter x y = LN) <=> DISJOINT (domain x) (domain y)``, 1770 fs [spt_eq_thm,wf_inter,wf_def,lookup_def,lookup_inter_alt] 1771 \\ fs [domain_lookup,IN_DISJOINT] 1772 \\ metis_tac [optionTheory.NOT_SOME_NONE,optionTheory.SOME_11, 1773 optionTheory.option_CASES]); 1774 1775val list_to_num_set_def = Define ` 1776 (list_to_num_set [] = LN) /\ 1777 (list_to_num_set (n::ns) = insert n () (list_to_num_set ns))`; 1778 1779val list_insert_def = Define ` 1780 (list_insert [] t = t) /\ 1781 (list_insert (n::ns) t = list_insert ns (insert n () t))`; 1782 1783Theorem domain_list_to_num_set: 1784 !xs. x IN domain (list_to_num_set xs) <=> MEM x xs 1785Proof 1786 Induct \\ full_simp_tac(srw_ss())[list_to_num_set_def] 1787QED 1788 1789Theorem domain_list_insert: 1790 !xs x t. 1791 x IN domain (list_insert xs t) <=> MEM x xs \/ x IN domain t 1792Proof 1793 Induct \\ full_simp_tac(srw_ss())[list_insert_def] \\ METIS_TAC [] 1794QED 1795 1796Theorem domain_FOLDR_delete: 1797 !ls live. domain (FOLDR delete live ls) = (domain live) DIFF (set ls) 1798Proof 1799 Induct>> full_simp_tac(srw_ss())[DIFF_INSERT,EXTENSION]>> metis_tac[] 1800QED 1801 1802Theorem lookup_list_to_num_set: 1803 !xs. lookup x (list_to_num_set xs) = if MEM x xs then SOME () else NONE 1804Proof 1805 Induct \\ srw_tac [] [list_to_num_set_def,lookup_def,lookup_insert] \\ 1806 full_simp_tac(srw_ss())[] 1807QED 1808 1809Theorem list_to_num_set_append: 1810 !l1 l2. list_to_num_set (l1 ++ l2) = 1811 union (list_to_num_set l1) (list_to_num_set l2) 1812Proof 1813 Induct \\ rw[list_to_num_set_def] 1814 \\ rw[Once insert_union] 1815 \\ rw[Once insert_union,SimpRHS] 1816 \\ rw[union_assoc] 1817QED 1818 1819Theorem map_map_K[simp]: 1820 !t. map (K a) (map f t) = map (K a) t 1821Proof Induct \\ fs[map_def] 1822QED 1823 1824Theorem lookup_map_K: 1825 !t n. lookup n (map (K x) t) = if n IN domain t then SOME x else NONE 1826Proof 1827 Induct >> fs[IN_domain,map_def,lookup_def] >> 1828 rpt strip_tac >> Cases_on `n = 0` >> fs[] >> 1829 Cases_on `EVEN n` >> fs[] 1830QED 1831 1832val alist_insert_def = Define ` 1833 (alist_insert [] xs t = t) /\ 1834 (alist_insert vs [] t = t) /\ 1835 (alist_insert (v::vs) (x::xs) t = insert v x (alist_insert vs xs t))` 1836 1837val alist_insert_ind = theorem "alist_insert_ind"; 1838 1839Theorem lookup_alist_insert: 1840 !x y t z. 1841 (LENGTH x = LENGTH y) ==> 1842 (lookup z (alist_insert x y t) = 1843 case ALOOKUP (ZIP(x,y)) z of SOME a => SOME a | NONE => lookup z t) 1844Proof 1845 ho_match_mp_tac alist_insert_ind >> 1846 srw_tac[][] >- fs[LENGTH,alist_insert_def] >> 1847 Cases_on`z=x`>> srw_tac[][lookup_def,alist_insert_def]>> 1848 full_simp_tac(srw_ss())[lookup_insert] 1849QED 1850 1851Theorem domain_alist_insert: 1852 !a b locs. (LENGTH a = LENGTH b) ==> 1853 (domain (alist_insert a b locs) = domain locs UNION set a) 1854Proof 1855 Induct_on`a`>>Cases_on`b`>>full_simp_tac(srw_ss())[alist_insert_def]>> 1856 srw_tac[][]>> metis_tac[INSERT_UNION_EQ,UNION_COMM] 1857QED 1858 1859Theorem alist_insert_append: 1860 !a1 a2 s b1 b2. 1861 (LENGTH a1 = LENGTH a2) ==> 1862 (alist_insert (a1++b1) (a2++b2) s = 1863 alist_insert a1 a2 (alist_insert b1 b2 s)) 1864Proof 1865 ho_match_mp_tac alist_insert_ind 1866 \\ simp[alist_insert_def,LENGTH_NIL_SYM] 1867QED 1868 1869Theorem wf_LN[simp]: wf LN 1870Proof rw[wf_def] 1871QED 1872 1873val splem1 = Q.prove(` 1874 a <> 0 ==> (a-1) DIV 2 < a`, 1875 simp[DIV_LT_X]); 1876 1877val DIV2_P_UNIV = 1878 DIV_P_UNIV |> SPEC_ALL |> Q.INST [`n` |-> `2`] |> SIMP_RULE (srw_ss()) [] 1879 |> EQ_IMP_RULE |> #2 |> Q.GENL [`P`, `m`] 1880 1881val splem3 = Q.prove( 1882 `(EVEN c /\ EVEN a \/ ODD a /\ ODD c) /\ a <> c /\ a <> 0 /\ c <> 0 ==> 1883 (a-1) DIV 2 <> (c-1) DIV 2`, 1884 map_every Cases_on [`a`, `c`] >> 1885 simp[DIV_LT_X, EVEN, ODD] >> DEEP_INTRO_TAC DIV2_P_UNIV >> rpt gen_tac >> 1886 rw[] >> fs[EVEN_ADD, EVEN_MULT, ODD_ADD, ODD_MULT] >> 1887 DEEP_INTRO_TAC DIV2_P_UNIV >> rw[] >> 1888 fs[EVEN_ADD, EVEN_MULT, ODD_ADD, ODD_MULT] >> 1889 rpt (rename [���x < 2���] >> ���(x = 0) \/ (x = 1)��� by simp[] >> fs[])); 1890 1891Theorem insert_swap: 1892 !t a b c d. 1893 a <> c ==> (insert a b (insert c d t) = insert c d (insert a b t)) 1894Proof 1895 completeInduct_on`a`>> 1896 completeInduct_on`c`>> 1897 Induct>> 1898 rw[]>> 1899 simp[Once insert_def,SimpRHS]>> 1900 simp[Once insert_def]>> 1901 ntac 2 IF_CASES_TAC>> 1902 fs[]>> 1903 rw[]>> 1904 simp[Once insert_def,SimpRHS]>> 1905 simp[Once insert_def]>> 1906 imp_res_tac splem1>> 1907 imp_res_tac splem3>> 1908 metis_tac[EVEN_ODD] 1909QED 1910 1911Theorem alist_insert_pull_insert: 1912 !xs ys z. ~MEM x xs ==> 1913 (alist_insert xs ys (insert x y z) = 1914 insert x y (alist_insert xs ys z)) 1915Proof 1916 ho_match_mp_tac alist_insert_ind 1917 \\ simp[alist_insert_def] \\ rw[] \\ fs[] 1918 \\ metis_tac[insert_swap] 1919QED 1920 1921Theorem alist_insert_REVERSE: 1922 !xs ys s. 1923 ALL_DISTINCT xs /\ (LENGTH xs = LENGTH ys) ==> 1924 (alist_insert (REVERSE xs) (REVERSE ys) s = alist_insert xs ys s) 1925Proof 1926 Induct \\ simp[alist_insert_def] 1927 \\ gen_tac \\ Cases \\ simp[alist_insert_def] 1928 \\ simp[alist_insert_append,alist_insert_def] 1929 \\ rw[] \\ simp[alist_insert_pull_insert] 1930QED 1931 1932Theorem insert_unchanged: 1933 !t x. 1934 (lookup x t = SOME y) ==> (insert x y t = t) 1935Proof 1936 completeInduct_on`x`>> Induct>> fs[lookup_def]>>rw[]>> 1937 simp[Once insert_def,SimpRHS]>> simp[Once insert_def]>> imp_res_tac splem1>> 1938 metis_tac[] 1939QED 1940 1941Triviality delete_mk_BN: 1942 (delete 0 (mk_BN t1 t2) = mk_BN t1 t2) /\ 1943 (k <> 0 ==> delete k (mk_BN t1 t2) = delete k (BN t1 t2)) 1944Proof 1945 Cases_on `t1` \\ Cases_on `t2` \\ fs [mk_BN_def] 1946 \\ fs [delete_def,mk_BN_def] 1947QED 1948 1949Triviality delete_mk_BS: 1950 (delete 0 (mk_BS t1 s t2) = mk_BN t1 t2) /\ 1951 (k <> 0 ==> delete k (mk_BS t1 s t2) = delete k (BS t1 s t2)) 1952Proof 1953 Cases_on `t1` \\ Cases_on `t2` \\ fs [mk_BS_def] 1954 \\ fs [delete_def,mk_BS_def,mk_BN_def] 1955QED 1956 1957Triviality DIV_2_lemma: 1958 n DIV 2 = m DIV 2 /\ EVEN m = EVEN n ==> m = n 1959Proof 1960 rw [] 1961 \\ `0 < 2n` by fs [] \\ drule DIVISION 1962 \\ fs [EVEN_MOD2] 1963 \\ disch_then (fn th => once_rewrite_tac [th]) \\ fs [] 1964 \\ Cases_on `m MOD 2 = 0` \\ fs [] 1965 \\ `n MOD 2 < 2` by fs [MOD_LESS] 1966 \\ `m MOD 2 < 2` by fs [MOD_LESS] 1967 \\ decide_tac 1968QED 1969 1970Theorem delete_delete: 1971 !f n k. 1972 delete n (delete k f) = 1973 if n = k then delete n f else delete k (delete n f) 1974Proof 1975 Induct \\ fs [delete_def] 1976 \\ rw [] \\ fs [delete_def] 1977 \\ simp [delete_mk_BN,delete_mk_BS] 1978 \\ rpt (qpat_x_assum `!x. _` (mp_tac o GSYM)) \\ rw [] \\ fs [delete_def] 1979 \\ rpt (qpat_x_assum `!x. _` (fn th => simp [Once (GSYM th)])) \\ rw [] 1980 \\ rpt (rename [`kk <> 0`] \\ Cases_on `kk` \\ fs []) 1981 \\ drule DIV_2_lemma \\ fs [EVEN] 1982QED 1983 1984Theorem size_zero_empty: 1985 !x. size x = 0 <=> domain x = EMPTY 1986Proof 1987 Induct \\ fs [size_def] 1988QED 1989 1990Theorem list_size_APPEND: 1991 list_size f (xs ++ ys) = list_size f xs + list_size f ys 1992Proof 1993 Induct_on `xs` \\ fs [list_size_def] 1994QED 1995 1996val spt_size_def = definition "spt_size_def"; 1997 1998Theorem SUM_MAP_same_LE: 1999 EVERY (\x. f x <= g x) xs 2000 ==> 2001 SUM (MAP f xs) <= SUM (MAP g xs) 2002Proof 2003 Induct_on `xs` \\ rw [] \\ fs [] 2004QED 2005 2006Theorem SUM_MAP_same_LESS: 2007 EVERY (\x. f x <= g x) xs /\ EXISTS (\x. f x < g x) xs 2008 ==> 2009 SUM (MAP f xs) < SUM (MAP g xs) 2010Proof 2011 Induct_on `xs` \\ rw [] \\ imp_res_tac SUM_MAP_same_LE \\ fs [] 2012QED 2013 2014Theorem lookup_0_spt_center: 2015 !spt. lookup 0 spt = spt_center spt 2016Proof 2017 Cases \\ EVAL_TAC 2018QED 2019 2020Theorem lookup_spt_right: 2021 lookup i (spt_right spt) = lookup ((i * 2) + 1) spt 2022Proof 2023 ASSUME_TAC (Q.SPEC `2` MULT_DIV) 2024 \\ Cases_on `spt` \\ fs [spt_right_def, lookup_def] 2025 \\ fs [EVEN_MULT, EVEN_ADD] 2026QED 2027 2028Theorem lookup_spt_left: 2029 lookup i (spt_left spt) = lookup ((i * 2) + 2) spt 2030Proof 2031 ASSUME_TAC (Q.SPEC `2` MULT_DIV) 2032 \\ Cases_on `spt` \\ fs [spt_left_def, lookup_def] 2033 \\ fs [EVEN_MULT, EVEN_ADD, ADD_DIV_RWT] 2034QED 2035 2036Definition combine_rle_def: 2037 combine_rle _ [] = [] /\ 2038 combine_rle _ [t] = [t] /\ 2039 combine_rle P ((i, x) :: (j, y) :: xs) = 2040 if P x /\ x = y then combine_rle P ((i + j, x) :: xs) 2041 else (i, x) :: combine_rle P ((j, y) :: xs) 2042End 2043 2044Theorem combine_rle_ind2 = combine_rle_ind 2045 |> Q.SPEC `\P2 xs. P2 = P3 ==> P4 xs` |> SIMP_RULE bool_ss [] 2046 |> Q.GENL [`P3`, `P4`] 2047 2048Definition apsnd_cons_def: 2049 apsnd_cons x (y, xs) = (y, x :: xs) 2050End 2051 2052Definition spt_centers_def: 2053 (spt_centers i [] = (i, [])) /\ 2054 (spt_centers i ((j, x) :: xs) = case spt_center x of 2055 | NONE => spt_centers (i + j) xs 2056 | SOME y => apsnd_cons (i, y) (spt_centers (i + j) xs)) 2057End 2058 2059Theorem sum_size_combine_rle_LE: 2060 !P xs. SUM (MAP (f o SND) (combine_rle P xs)) <= SUM (MAP (f o SND) xs) 2061Proof 2062 ho_match_mp_tac combine_rle_ind 2063 \\ rw [combine_rle_def] 2064 \\ rfs [] 2065QED 2066 2067Triviality combine_rle_LESS_TRANS = MATCH_MP 2068 (LESS_LESS_EQ_TRANS |> RES_CANON |> last) 2069 (SPEC_ALL sum_size_combine_rle_LE) 2070 2071Definition spts_to_alist_def: 2072 spts_to_alist i xs = 2073 let ys = combine_rle isEmpty xs in 2074 if EVERY (isEmpty o SND) ys then [] else 2075 let (j, centers) = spt_centers i ys in 2076 let rights = MAP (\(i, t). (i, spt_right t)) ys in 2077 let lefts = MAP (\(i, t). (i, spt_left t)) ys in 2078 centers ++ spts_to_alist j (rights ++ lefts) 2079Termination 2080 WF_REL_TAC `measure (SUM o MAP (spt_size (K 0) o SND) o SND)` 2081 \\ rw [MAP_MAP_o, SUM_APPEND, GSYM SUM_MAP_PLUS] 2082 \\ irule (combine_rle_LESS_TRANS |> REWRITE_RULE [combinTheory.o_DEF]) 2083 \\ qexists_tac `isEmpty` 2084 \\ irule SUM_MAP_same_LESS 2085 \\ fs [EVERY_MEM, EXISTS_MEM] 2086 \\ rw [] \\ TRY (qexists_tac `e`) 2087 \\ pairarg_tac \\ fs [] 2088 \\ rename [`spt_size _ (spt_left spt)`] \\ Cases_on `spt` 2089 \\ fs [spt_size_def, spt_left_def, spt_right_def] 2090End 2091 2092Definition toSortedAList_def: 2093 toSortedAList spt = spts_to_alist 0 [(1, spt)] 2094End 2095 2096Definition expand_rle_def: 2097 expand_rle xs = FLAT (MAP (\(i, t). REPLICATE i t) xs) 2098End 2099 2100Theorem expand_rle_combine_rle: 2101 !P xs. expand_rle (combine_rle P xs) = expand_rle xs 2102Proof 2103 ho_match_mp_tac combine_rle_ind 2104 \\ rw [expand_rle_def, combine_rle_def, rich_listTheory.REPLICATE_APPEND] 2105 \\ rfs [] 2106QED 2107 2108Theorem EVERY_combine_rle: 2109 !P xs. EVERY (Q o SND) (combine_rle P xs) <=> EVERY (Q o SND) xs 2110Proof 2111 ho_match_mp_tac combine_rle_ind 2112 \\ rw [combine_rle_def] 2113 \\ rfs [] 2114 \\ metis_tac [] 2115QED 2116 2117Theorem EVERY_empty_SND_combine: 2118 !xs. EVERY (isEmpty o SND) xs ==> 2119 xs = [] \/ 2120 (?n. combine_rle isEmpty xs = [(n, LN)] /\ expand_rle xs = REPLICATE n LN) 2121Proof 2122 ho_match_mp_tac (Q.ISPEC `isEmpty` combine_rle_ind2) 2123 \\ simp [combine_rle_def] 2124 \\ simp [pairTheory.FORALL_PROD, expand_rle_def, 2125 rich_listTheory.REPLICATE_APPEND] 2126QED 2127 2128Theorem lookup_SOME_left_right_cases: 2129 lookup i spt = SOME v <=> 2130 (i = 0 /\ spt_center spt = SOME v) \/ 2131 (?j. i = j * 2 + 1 /\ lookup j (spt_right spt) = SOME v) \/ 2132 (?j. i = j * 2 + 2 /\ lookup j (spt_left spt) = SOME v) 2133Proof 2134 qspec_then `i` assume_tac bit_cases 2135 \\ fs [lookup_0_spt_center, lookup_spt_right, lookup_spt_left] 2136 \\ simp [oddevenlemma] 2137QED 2138 2139Theorem expand_rle_append: 2140 expand_rle (xs ++ ys) = expand_rle xs ++ expand_rle ys 2141Proof 2142 simp [expand_rle_def] 2143QED 2144 2145Theorem expand_rle_map: 2146 expand_rle (MAP (\(i, x). (i, f x)) xs) = MAP f (expand_rle xs) 2147Proof 2148 simp [expand_rle_def, MAP_FLAT, MAP_MAP_o, combinTheory.o_DEF] 2149 \\ simp [pairTheory.ELIM_UNCURRY] 2150QED 2151 2152Theorem apsnd_cons_is_case: 2153 apsnd_cons x t = (case t of (y, xs) => (y, x :: xs)) 2154Proof 2155 CASE_TAC \\ simp [apsnd_cons_def] 2156QED 2157 2158Triviality fst_spt_centers_imp_lemma: 2159 !i xs j ys. spt_centers i xs = (j, ys) ==> i + LENGTH (expand_rle xs) = j 2160Proof 2161 ho_match_mp_tac spt_centers_ind 2162 \\ rw [spt_centers_def, expand_rle_def, apsnd_cons_is_case] 2163 \\ BasicProvers.EVERY_CASE_TAC 2164 \\ fs [] 2165QED 2166 2167Theorem fst_spt_centers_imp = 2168 REWRITE_RULE [Q.ISPEC `_ + _` EQ_SYM_EQ] fst_spt_centers_imp_lemma 2169 2170Overload rle_wf[local] = ``EVERY (\(j, spt). j > 0 /\ (spt <> LN ==> j = 1))`` 2171 2172Theorem spt_centers_expand_rle: 2173 !i xs. rle_wf xs ==> 2174 !j x. MEM (j, x) (SND (spt_centers i xs)) = 2175 (?k. j = i + k /\ k < LENGTH (expand_rle xs) /\ 2176 spt_center (EL k (expand_rle xs)) = SOME x) 2177Proof 2178 ho_match_mp_tac spt_centers_ind 2179 \\ simp [spt_centers_def, expand_rle_def, apsnd_cons_is_case] 2180 \\ rw [] \\ fs [] 2181 \\ BasicProvers.EVERY_CASE_TAC 2182 \\ simp [] 2183 \\ Cases_on `x = LN` \\ fs [spt_center_def] 2184 \\ EQ_TAC 2185 \\ rw [EL_APPEND_EQN] 2186 \\ BasicProvers.EVERY_CASE_TAC 2187 \\ fs [rich_listTheory.EL_REPLICATE, spt_center_def] 2188 \\ simp [Q.SPEC `a` EQ_SYM_EQ |> Q.ISPEC `b + c`, EVAL ``REPLICATE 1 v``] 2189 \\ rename [`EL (a - b) _`] 2190 \\ qexists_tac `a - b` 2191 \\ simp [] 2192QED 2193 2194Theorem spt_centers_expand_rle_imp: 2195 !n xs. spt_centers n xs = (n2, centers) /\ 2196 rle_wf xs ==> 2197 !j x. MEM (j, x) centers = 2198 (?k. j = n + k /\ k < LENGTH (expand_rle xs) /\ 2199 spt_center (EL k (expand_rle xs)) = SOME x) 2200Proof 2201 rw [pairTheory.PAIR_FST_SND_EQ] 2202 \\ DEP_REWRITE_TAC [spt_centers_expand_rle] 2203 \\ simp [] 2204QED 2205 2206Theorem combine_rle_props: 2207 !xs. rle_wf xs ==> 2208 rle_wf (combine_rle isEmpty xs) /\ 2209 rle_wf (MAP (\(i,t). (i,spt_right t)) (combine_rle isEmpty xs)) /\ 2210 rle_wf (MAP (\(i,t). (i,spt_left t)) (combine_rle isEmpty xs)) 2211Proof 2212 ho_match_mp_tac (Q.ISPEC `isEmpty` combine_rle_ind2) 2213 \\ simp [combine_rle_def, pairTheory.FORALL_PROD] 2214 \\ rw [] 2215 \\ rfs [] 2216 \\ rename [`_ t <> LN`] 2217 \\ Cases_on `t` \\ fs [spt_left_def, spt_right_def] 2218QED 2219 2220Triviality less_two_times_lemma: 2221 !i j. (j < 2 * i) = (j < i \/ (?j'. j' < i /\ j = i + j')) 2222Proof 2223 rw [] 2224 \\ Cases_on `j < i` 2225 \\ fs [] 2226 \\ EQ_TAC 2227 \\ rw [] 2228 \\ qexists_tac `j - i` 2229 \\ simp [] 2230QED 2231 2232Theorem MEM_spts_to_alist: 2233 !n xs i x. 2234 rle_wf xs ==> 2235 (MEM (i, x) (spts_to_alist n xs) = 2236 (?j k. j < LENGTH (expand_rle xs) 2237 /\ lookup k (EL j (expand_rle xs)) = SOME x 2238 /\ i = n + j + (k * LENGTH (expand_rle xs)))) 2239Proof 2240 ho_match_mp_tac spts_to_alist_ind 2241 \\ rw [] 2242 \\ simp [Once spts_to_alist_def] 2243 \\ BasicProvers.TOP_CASE_TAC 2244 >- ( 2245 fs [EVERY_combine_rle] 2246 \\ imp_res_tac EVERY_empty_SND_combine 2247 \\ fs [expand_rle_def] 2248 \\ rw [] 2249 \\ rename [`idx < len`] 2250 \\ Cases_on `idx < len` \\ simp [rich_listTheory.EL_REPLICATE, lookup_def] 2251 ) 2252 \\ simp [Once lookup_SOME_left_right_cases] 2253 \\ pairarg_tac \\ fs [] 2254 \\ imp_res_tac fst_spt_centers_imp 2255 \\ drule spt_centers_expand_rle_imp 2256 \\ fs [combine_rle_props, expand_rle_combine_rle, 2257 expand_rle_append, expand_rle_map] 2258 \\ simp [Q.SPEC `LENGTH _` less_two_times_lemma] 2259 \\ simp [RIGHT_AND_OVER_OR, LEFT_AND_OVER_OR, EXISTS_OR_THM] 2260 \\ csimp [PULL_EXISTS, EL_APPEND_EQN, LEFT_ADD_DISTRIB] 2261 \\ metis_tac [EL_MAP] 2262QED 2263 2264Theorem spt_centers_ord: 2265 !n xs n2 ys. spt_centers n xs = (n2, ys) /\ rle_wf xs ==> 2266 SORTED (<) (MAP FST ys) /\ 2267 (!k. k <= n ==> EVERY (\t. FST t >= k) ys) /\ 2268 EVERY (\t. FST t < n2) ys 2269Proof 2270 ho_match_mp_tac spt_centers_ind 2271 \\ simp [spt_centers_def, apsnd_cons_is_case] 2272 \\ rw [] 2273 \\ BasicProvers.EVERY_CASE_TAC 2274 \\ rw [] 2275 \\ fs [sortingTheory.SORTED_EQ, MEM_MAP, PULL_EXISTS] 2276 \\ rfs [] 2277 \\ first_x_assum (qspec_then `j + n` assume_tac) 2278 \\ imp_res_tac fst_spt_centers_imp 2279 \\ fs [EVERY_MEM] 2280 \\ rw [] 2281 \\ res_tac 2282 \\ simp [] 2283QED 2284 2285Theorem SORTED_spts_to_alist_lemma: 2286 !n xs. rle_wf xs ==> SORTED (<) (MAP FST (spts_to_alist n xs)) /\ 2287 (!k. k <= n ==> EVERY (\t. FST t >= k) (spts_to_alist n xs)) 2288Proof 2289 ho_match_mp_tac spts_to_alist_ind 2290 \\ rw [] 2291 \\ simp [Once spts_to_alist_def] 2292 \\ BasicProvers.TOP_CASE_TAC 2293 \\ simp [] 2294 \\ pairarg_tac \\ fs [] 2295 \\ imp_res_tac fst_spt_centers_imp 2296 \\ drule spt_centers_ord 2297 \\ rw [] 2298 \\ rfs [combine_rle_props] 2299 \\ irule sortingTheory.SORTED_APPEND_IMP 2300 \\ fs [combine_rle_props, expand_rle_combine_rle] 2301 \\ last_x_assum (qspec_then `n + LENGTH (expand_rle xs)` mp_tac) 2302 \\ fs [EVERY_MEM, MEM_MAP, PULL_EXISTS, pairTheory.FORALL_PROD] 2303 \\ rw [] \\ res_tac \\ simp [] 2304QED 2305 2306Theorem MEM_toSortedAList: 2307 MEM (i, x) (toSortedAList spt) = (lookup i spt = SOME x) 2308Proof 2309 simp [toSortedAList_def, MEM_spts_to_alist, EVAL ``expand_rle [(1, v)]``, 2310 Q.prove (`j < 1 <=> j = (0 : num)`, simp [])] 2311QED 2312 2313Theorem SORTED_toSortedAList: 2314 SORTED (<) (MAP FST (toSortedAList spt)) 2315Proof 2316 fs [toSortedAList_def, SORTED_spts_to_alist_lemma] 2317QED 2318 2319Theorem ALOOKUP_toSortedAList: 2320 ALOOKUP (toSortedAList spt) i = lookup i spt 2321Proof 2322 Cases_on `lookup i spt` 2323 >- ( 2324 Cases_on `ALOOKUP (toSortedAList spt) i` 2325 \\ simp [] 2326 \\ imp_res_tac ALOOKUP_MEM 2327 \\ rfs [MEM_toSortedAList] 2328 ) 2329 \\ irule ALOOKUP_ALL_DISTINCT_MEM 2330 \\ simp [MEM_toSortedAList] 2331 \\ irule sortingTheory.SORTED_ALL_DISTINCT 2332 \\ qexists_tac `(<)` 2333 \\ simp [SORTED_toSortedAList, relationTheory.irreflexive_def] 2334QED 2335 2336val _ = let 2337 open sptreepp 2338in 2339 add_ML_dependency "sptreepp"; 2340 add_user_printer ("sptreepp.sptreepp", ���x : 'a spt���) 2341end 2342 2343val _ = export_theory(); 2344