1open HolKernel Parse boolLib bossLib; 2open arithmeticTheory 3open logrootTheory 4open listTheory 5open alistTheory 6 7val _ = new_theory "sptree"; 8 9(* A log-time random-access, extensible array implementation with union. 10 11 The "array" can be gappy: there doesn't have to be an element at 12 any particular index, and, being a finite thing, there is obviously 13 a maximum index past which there are no elements at all. It is 14 possible to update at an index past the current maximum index. It 15 is also possible to delete values at any index. 16 17 Should EVAL well. Big drawback is that there doesn't seem to be an 18 efficient way (i.e., O(n)) to do an in index-order traversal of the 19 elements. There is an O(n) fold function that gives you access to 20 all the key-value pairs, but these will come out in an inconvenient 21 order. If you iterate over the keys with an increment, you will get 22 O(n log n) performance. 23 24 The insert, delete and union operations all preserve a 25 well-formedness condition ("wf") that ensures there is only one 26 possible representation for any given finite-map. 27*) 28 29val _ = Datatype`spt = LN | LS 'a | BN spt spt | BS spt 'a spt` 30(* Leaf-None, Leaf-Some, Branch-None, Branch-Some *) 31 32val _ = overload_on ("isEmpty", ``\t. t = LN``) 33 34val wf_def = Define` 35 (wf LN <=> T) /\ 36 (wf (LS a) <=> T) /\ 37 (wf (BN t1 t2) <=> wf t1 /\ wf t2 /\ ~(isEmpty t1 /\ isEmpty t2)) /\ 38 (wf (BS t1 a t2) <=> wf t1 /\ wf t2 /\ ~(isEmpty t1 /\ isEmpty t2)) 39` 40 41fun tzDefine s q = Lib.with_flag (computeLib.auto_import_definitions,false) (tDefine s q) 42val lookup_def = tzDefine "lookup" ` 43 (lookup k LN = NONE) /\ 44 (lookup k (LS a) = if k = 0 then SOME a else NONE) /\ 45 (lookup k (BN t1 t2) = 46 if k = 0 then NONE 47 else lookup ((k - 1) DIV 2) (if EVEN k then t1 else t2)) /\ 48 (lookup k (BS t1 a t2) = 49 if k = 0 then SOME a 50 else lookup ((k - 1) DIV 2) (if EVEN k then t1 else t2)) 51` (WF_REL_TAC `measure FST` >> simp[DIV_LT_X]) 52 53val insert_def = tzDefine "insert" ` 54 (insert k a LN = if k = 0 then LS a 55 else if EVEN k then BN (insert ((k-1) DIV 2) a LN) LN 56 else BN LN (insert ((k-1) DIV 2) a LN)) /\ 57 (insert k a (LS a') = 58 if k = 0 then LS a 59 else if EVEN k then BS (insert ((k-1) DIV 2) a LN) a' LN 60 else BS LN a' (insert ((k-1) DIV 2) a LN)) /\ 61 (insert k a (BN t1 t2) = 62 if k = 0 then BS t1 a t2 63 else if EVEN k then BN (insert ((k - 1) DIV 2) a t1) t2 64 else BN t1 (insert ((k - 1) DIV 2) a t2)) /\ 65 (insert k a (BS t1 a' t2) = 66 if k = 0 then BS t1 a t2 67 else if EVEN k then BS (insert ((k - 1) DIV 2) a t1) a' t2 68 else BS t1 a' (insert ((k - 1) DIV 2) a t2)) 69` (WF_REL_TAC `measure FST` >> simp[DIV_LT_X]); 70 71val insert_ind = theorem "insert_ind"; 72 73val mk_BN_def = Define ` 74 (mk_BN LN LN = LN) /\ 75 (mk_BN t1 t2 = BN t1 t2)`; 76 77val mk_BS_def = Define ` 78 (mk_BS LN x LN = LS x) /\ 79 (mk_BS t1 x t2 = BS t1 x t2)`; 80 81val delete_def = zDefine` 82 (delete k LN = LN) /\ 83 (delete k (LS a) = if k = 0 then LN else LS a) /\ 84 (delete k (BN t1 t2) = 85 if k = 0 then BN t1 t2 86 else if EVEN k then 87 mk_BN (delete ((k - 1) DIV 2) t1) t2 88 else 89 mk_BN t1 (delete ((k - 1) DIV 2) t2)) /\ 90 (delete k (BS t1 a t2) = 91 if k = 0 then BN t1 t2 92 else if EVEN k then 93 mk_BS (delete ((k - 1) DIV 2) t1) a t2 94 else 95 mk_BS t1 a (delete ((k - 1) DIV 2) t2)) 96`; 97 98val fromList_def = Define` 99 fromList l = SND (FOLDL (\(i,t) a. (i + 1, insert i a t)) (0,LN) l) 100`; 101 102val size_def = Define` 103 (size LN = 0) /\ 104 (size (LS a) = 1) /\ 105 (size (BN t1 t2) = size t1 + size t2) /\ 106 (size (BS t1 a t2) = size t1 + size t2 + 1) 107`; 108val _ = export_rewrites ["size_def"] 109 110val insert_notEmpty = store_thm( 111 "insert_notEmpty", 112 ``~isEmpty (insert k a t)``, 113 Cases_on `t` >> rw[Once insert_def]); 114 115val wf_insert = store_thm( 116 "wf_insert", 117 ``!k a t. wf t ==> wf (insert k a t)``, 118 ho_match_mp_tac (theorem "insert_ind") >> 119 rpt strip_tac >> 120 simp[Once insert_def] >> rw[wf_def, insert_notEmpty] >> fs[wf_def]); 121 122val mk_BN_thm = prove( 123 ``!t1 t2. mk_BN t1 t2 = 124 if isEmpty t1 /\ isEmpty t2 then LN else BN t1 t2``, 125 REPEAT Cases >> EVAL_TAC); 126 127val mk_BS_thm = prove( 128 ``!t1 t2. mk_BS t1 x t2 = 129 if isEmpty t1 /\ isEmpty t2 then LS x else BS t1 x t2``, 130 REPEAT Cases >> EVAL_TAC); 131 132val wf_delete = store_thm( 133 "wf_delete", 134 ``!t k. wf t ==> wf (delete k t)``, 135 Induct >> rw[wf_def, delete_def, mk_BN_thm, mk_BS_thm] >> 136 rw[wf_def] >> rw[] >> fs[] >> metis_tac[]); 137 138val lookup_insert1 = store_thm( 139 "lookup_insert1[simp]", 140 ``!k a t. lookup k (insert k a t) = SOME a``, 141 ho_match_mp_tac (theorem "insert_ind") >> rpt strip_tac >> 142 simp[Once insert_def] >> rw[lookup_def]); 143 144val DIV2_EQ_DIV2 = prove( 145 ``(m DIV 2 = n DIV 2) <=> 146 (m = n) \/ 147 (n = m + 1) /\ EVEN m \/ 148 (m = n + 1) /\ EVEN n``, 149 `0 < 2` by simp[] >> 150 map_every qabbrev_tac [`nq = n DIV 2`, `nr = n MOD 2`] >> 151 qspec_then `2` mp_tac DIVISION >> asm_simp_tac bool_ss [] >> 152 disch_then (qspec_then `n` mp_tac) >> asm_simp_tac bool_ss [] >> 153 map_every qabbrev_tac [`mq = m DIV 2`, `mr = m MOD 2`] >> 154 qspec_then `2` mp_tac DIVISION >> asm_simp_tac bool_ss [] >> 155 disch_then (qspec_then `m` mp_tac) >> asm_simp_tac bool_ss [] >> 156 rw[] >> markerLib.RM_ALL_ABBREVS_TAC >> 157 simp[EVEN_ADD, EVEN_MULT] >> 158 `!p. p < 2 ==> (EVEN p <=> (p = 0))` 159 by (rpt strip_tac >> `(p = 0) \/ (p = 1)` by decide_tac >> simp[]) >> 160 simp[]); 161 162val EVEN_PRE = prove( 163 ``x <> 0 ==> (EVEN (x - 1) <=> ~EVEN x)``, 164 Induct_on `x` >> simp[] >> Cases_on `x` >> fs[] >> 165 simp_tac (srw_ss()) [EVEN]); 166 167val lookup_insert = store_thm( 168 "lookup_insert", 169 ``!k2 v t k1. lookup k1 (insert k2 v t) = 170 if k1 = k2 then SOME v else lookup k1 t``, 171 ho_match_mp_tac (theorem "insert_ind") >> rpt strip_tac >> 172 simp[Once insert_def] >> rw[lookup_def] >> simp[] >| [ 173 fs[lookup_def] >> pop_assum mp_tac >> Cases_on `k1 = 0` >> simp[] >> 174 COND_CASES_TAC >> simp[lookup_def, DIV2_EQ_DIV2, EVEN_PRE], 175 fs[lookup_def] >> pop_assum mp_tac >> Cases_on `k1 = 0` >> simp[] >> 176 COND_CASES_TAC >> simp[lookup_def, DIV2_EQ_DIV2, EVEN_PRE] >> 177 rpt strip_tac >> metis_tac[EVEN_PRE], 178 fs[lookup_def] >> COND_CASES_TAC >> 179 simp[lookup_def, DIV2_EQ_DIV2, EVEN_PRE], 180 fs[lookup_def] >> COND_CASES_TAC >> 181 simp[lookup_def, DIV2_EQ_DIV2, EVEN_PRE] >> 182 rpt strip_tac >> metis_tac[EVEN_PRE], 183 simp[DIV2_EQ_DIV2, EVEN_PRE], 184 simp[DIV2_EQ_DIV2, EVEN_PRE] >> COND_CASES_TAC 185 >- metis_tac [EVEN_PRE] >> simp[], 186 simp[DIV2_EQ_DIV2, EVEN_PRE], 187 simp[DIV2_EQ_DIV2, EVEN_PRE] >> COND_CASES_TAC 188 >- metis_tac [EVEN_PRE] >> simp[] 189 ]) 190 191val union_def = Define` 192 (union LN t = t) /\ 193 (union (LS a) t = 194 case t of 195 | LN => LS a 196 | LS b => LS a 197 | BN t1 t2 => BS t1 a t2 198 | BS t1 _ t2 => BS t1 a t2) /\ 199 (union (BN t1 t2) t = 200 case t of 201 | LN => BN t1 t2 202 | LS a => BS t1 a t2 203 | BN t1' t2' => BN (union t1 t1') (union t2 t2') 204 | BS t1' a t2' => BS (union t1 t1') a (union t2 t2')) /\ 205 (union (BS t1 a t2) t = 206 case t of 207 | LN => BS t1 a t2 208 | LS a' => BS t1 a t2 209 | BN t1' t2' => BS (union t1 t1') a (union t2 t2') 210 | BS t1' a' t2' => BS (union t1 t1') a (union t2 t2')) 211`; 212 213val isEmpty_union = store_thm( 214 "isEmpty_union", 215 ``isEmpty (union m1 m2) <=> isEmpty m1 /\ isEmpty m2``, 216 map_every Cases_on [`m1`, `m2`] >> simp[union_def]); 217 218val wf_union = store_thm( 219 "wf_union", 220 ``!m1 m2. wf m1 /\ wf m2 ==> wf (union m1 m2)``, 221 Induct >> simp[wf_def, union_def] >> 222 Cases_on `m2` >> simp[wf_def,isEmpty_union] >> 223 metis_tac[]); 224 225val optcase_lemma = prove( 226 ``(case opt of NONE => NONE | SOME v => SOME v) = opt``, 227 Cases_on `opt` >> simp[]); 228 229val lookup_union = store_thm( 230 "lookup_union", 231 ``!m1 m2 k. lookup k (union m1 m2) = 232 case lookup k m1 of 233 NONE => lookup k m2 234 | SOME v => SOME v``, 235 Induct >> simp[lookup_def] >- simp[union_def] >> 236 Cases_on `m2` >> simp[lookup_def, union_def] >> 237 rw[optcase_lemma]); 238 239val inter_def = Define` 240 (inter LN t = LN) /\ 241 (inter (LS a) t = 242 case t of 243 | LN => LN 244 | LS b => LS a 245 | BN t1 t2 => LN 246 | BS t1 _ t2 => LS a) /\ 247 (inter (BN t1 t2) t = 248 case t of 249 | LN => LN 250 | LS a => LN 251 | BN t1' t2' => mk_BN (inter t1 t1') (inter t2 t2') 252 | BS t1' a t2' => mk_BN (inter t1 t1') (inter t2 t2')) /\ 253 (inter (BS t1 a t2) t = 254 case t of 255 | LN => LN 256 | LS a' => LS a 257 | BN t1' t2' => mk_BN (inter t1 t1') (inter t2 t2') 258 | BS t1' a' t2' => mk_BS (inter t1 t1') a (inter t2 t2')) 259`; 260 261val inter_eq_def = Define` 262 (inter_eq LN t = LN) /\ 263 (inter_eq (LS a) t = 264 case t of 265 | LN => LN 266 | LS b => if a = b then LS a else LN 267 | BN t1 t2 => LN 268 | BS t1 b t2 => if a = b then LS a else LN) /\ 269 (inter_eq (BN t1 t2) t = 270 case t of 271 | LN => LN 272 | LS a => LN 273 | BN t1' t2' => mk_BN (inter_eq t1 t1') (inter_eq t2 t2') 274 | BS t1' a t2' => mk_BN (inter_eq t1 t1') (inter_eq t2 t2')) /\ 275 (inter_eq (BS t1 a t2) t = 276 case t of 277 | LN => LN 278 | LS a' => if a' = a then LS a else LN 279 | BN t1' t2' => mk_BN (inter_eq t1 t1') (inter_eq t2 t2') 280 | BS t1' a' t2' => 281 if a' = a then 282 mk_BS (inter_eq t1 t1') a (inter_eq t2 t2') 283 else mk_BN (inter_eq t1 t1') (inter_eq t2 t2'))`; 284 285val difference_def = Define` 286 (difference LN t = LN) /\ 287 (difference (LS a) t = 288 case t of 289 | LN => LS a 290 | LS b => LN 291 | BN t1 t2 => LS a 292 | BS t1 b t2 => LN) /\ 293 (difference (BN t1 t2) t = 294 case t of 295 | LN => BN t1 t2 296 | LS a => BN t1 t2 297 | BN t1' t2' => mk_BN (difference t1 t1') (difference t2 t2') 298 | BS t1' a t2' => mk_BN (difference t1 t1') (difference t2 t2')) /\ 299 (difference (BS t1 a t2) t = 300 case t of 301 | LN => BS t1 a t2 302 | LS a' => BN t1 t2 303 | BN t1' t2' => mk_BS (difference t1 t1') a (difference t2 t2') 304 | BS t1' a' t2' => mk_BN (difference t1 t1') (difference t2 t2'))`; 305 306val wf_mk_BN = prove( 307 ``!t1 t2. wf (mk_BN t1 t2) <=> wf t1 /\ wf t2``, 308 map_every Cases_on [`t1`,`t2`] >> fs [mk_BN_def,wf_def]); 309 310val wf_mk_BS = prove( 311 ``!t1 x t2. wf (mk_BS t1 x t2) <=> wf t1 /\ wf t2``, 312 map_every Cases_on [`t1`,`t2`] >> fs [mk_BS_def,wf_def]); 313 314val wf_inter = store_thm( 315 "wf_inter[simp]", 316 ``!m1 m2. wf (inter m1 m2)``, 317 Induct >> simp[wf_def, inter_def] >> 318 Cases_on `m2` >> simp[wf_def,wf_mk_BS,wf_mk_BN]); 319 320val lookup_mk_BN = prove( 321 ``lookup k (mk_BN t1 t2) = lookup k (BN t1 t2)``, 322 map_every Cases_on [`t1`,`t2`] >> fs [mk_BN_def,lookup_def]); 323 324val lookup_mk_BS = prove( 325 ``lookup k (mk_BS t1 x t2) = lookup k (BS t1 x t2)``, 326 map_every Cases_on [`t1`,`t2`] >> fs [mk_BS_def,lookup_def]); 327 328val lookup_inter = store_thm( 329 "lookup_inter", 330 ``!m1 m2 k. lookup k (inter m1 m2) = 331 case (lookup k m1,lookup k m2) of 332 | (SOME v, SOME w) => SOME v 333 | _ => NONE``, 334 Induct >> simp[lookup_def] >> Cases_on `m2` >> 335 simp[lookup_def, inter_def, lookup_mk_BS, lookup_mk_BN] >> 336 rw[optcase_lemma] >> BasicProvers.CASE_TAC); 337 338val lookup_inter_eq = store_thm( 339 "lookup_inter_eq", 340 ``!m1 m2 k. lookup k (inter_eq m1 m2) = 341 case lookup k m1 of 342 | NONE => NONE 343 | SOME v => (if lookup k m2 = SOME v then SOME v else NONE)``, 344 Induct >> simp[lookup_def] >> Cases_on `m2` >> 345 simp[lookup_def, inter_eq_def, lookup_mk_BS, lookup_mk_BN] >> 346 rw[optcase_lemma] >> REPEAT BasicProvers.CASE_TAC >> 347 fs [lookup_def, lookup_mk_BS, lookup_mk_BN]); 348 349val lookup_inter_EQ = store_thm("lookup_inter_EQ", 350 ``((lookup x (inter t1 t2) = SOME y) <=> 351 (lookup x t1 = SOME y) /\ lookup x t2 <> NONE) /\ 352 ((lookup x (inter t1 t2) = NONE) <=> 353 (lookup x t1 = NONE) \/ (lookup x t2 = NONE))``, 354 fs [lookup_inter] \\ BasicProvers.EVERY_CASE_TAC); 355 356val lookup_inter_assoc = store_thm("lookup_inter_assoc", 357 ``lookup x (inter t1 (inter t2 t3)) = 358 lookup x (inter (inter t1 t2) t3)``, 359 fs [lookup_inter] \\ BasicProvers.EVERY_CASE_TAC) 360 361val lookup_difference = store_thm( 362 "lookup_difference", 363 ``!m1 m2 k. lookup k (difference m1 m2) = 364 if lookup k m2 = NONE then lookup k m1 else NONE``, 365 Induct >> simp[lookup_def] >> Cases_on `m2` >> 366 simp[lookup_def, difference_def, lookup_mk_BS, lookup_mk_BN] >> 367 rw[optcase_lemma] >> REPEAT BasicProvers.CASE_TAC >> 368 fs [lookup_def, lookup_mk_BS, lookup_mk_BN]) 369 370val lrnext_real_def = tzDefine "lrnext" ` 371 lrnext n = if n = 0 then 1 else 2 * lrnext ((n - 1) DIV 2)` 372 (WF_REL_TAC `measure I` \\ fs [DIV_LT_X] \\ REPEAT STRIP_TAC \\ DECIDE_TAC) ; 373 374val lrnext_def = prove( 375 ``(lrnext ZERO = 1) /\ 376 (!n. lrnext (BIT1 n) = 2 * lrnext n) /\ 377 (!n. lrnext (BIT2 n) = 2 * lrnext n)``, 378 REPEAT STRIP_TAC 379 THEN1 (fs [Once ALT_ZERO,Once lrnext_real_def]) 380 THEN1 381 (full_simp_tac (srw_ss()) [Once BIT1,Once lrnext_real_def] 382 \\ AP_TERM_TAC \\ simp_tac (srw_ss()) [Once BIT1] 383 \\ full_simp_tac (srw_ss()) [ADD_ASSOC,DECIDE ``n+n=n*2``,MULT_DIV]) 384 THEN1 385 (simp_tac (srw_ss()) [Once BIT2,Once lrnext_real_def] 386 \\ AP_TERM_TAC \\ simp_tac (srw_ss()) [Once BIT2] 387 \\ `n + (n + 2) - 1 = n * 2 + 1` by DECIDE_TAC 388 \\ asm_simp_tac (srw_ss()) [DIV_MULT])) 389val lrnext' = prove( 390 ``(!a. lrnext 0 = 1) /\ (!n a. lrnext (NUMERAL n) = lrnext n)``, 391 simp[NUMERAL_DEF, GSYM ALT_ZERO, lrnext_def]) 392val lrnext_thm = save_thm( 393 "lrnext_thm", 394 LIST_CONJ (CONJUNCTS lrnext' @ CONJUNCTS lrnext_def)) 395val _ = computeLib.add_persistent_funs ["lrnext_thm"] 396 397val domain_def = zDefine` 398 (domain LN = {}) /\ 399 (domain (LS _) = {0}) /\ 400 (domain (BN t1 t2) = 401 IMAGE (\n. 2 * n + 2) (domain t1) UNION 402 IMAGE (\n. 2 * n + 1) (domain t2)) /\ 403 (domain (BS t1 _ t2) = 404 {0} UNION IMAGE (\n. 2 * n + 2) (domain t1) UNION 405 IMAGE (\n. 2 * n + 1) (domain t2)) 406`; 407val _ = export_rewrites ["domain_def"] 408 409val FINITE_domain = store_thm( 410 "FINITE_domain[simp]", 411 ``FINITE (domain t)``, 412 Induct_on `t` >> simp[]); 413 414val DIV2 = DIVISION |> Q.SPEC `2` |> REWRITE_RULE [DECIDE ``0 < 2``] 415 416val even_lem = Q.prove( 417 `EVEN k /\ k <> 0 ==> (2 * ((k - 1) DIV 2) + 2 = k)`, 418 qabbrev_tac `k0 = k - 1` >> 419 strip_tac >> `k = k0 + 1` by simp[Abbr`k0`] >> 420 pop_assum SUBST_ALL_TAC >> qunabbrev_tac `k0` >> 421 fs[EVEN_ADD] >> 422 assume_tac (Q.SPEC `k0` DIV2) >> 423 map_every qabbrev_tac [`q = k0 DIV 2`, `r = k0 MOD 2`] >> 424 markerLib.RM_ALL_ABBREVS_TAC >> 425 fs[EVEN_ADD, EVEN_MULT] >> 426 `(r = 0) \/ (r = 1)` by simp[] >> fs[]) 427 428val odd_lem = Q.prove( 429 `~EVEN k /\ k <> 0 ==> (2 * ((k - 1) DIV 2) + 1 = k)`, 430 qabbrev_tac `k0 = k - 1` >> 431 strip_tac >> `k = k0 + 1` by simp[Abbr`k0`] >> 432 pop_assum SUBST_ALL_TAC >> qunabbrev_tac `k0` >> 433 fs[EVEN_ADD] >> 434 assume_tac (Q.SPEC `k0` DIV2) >> 435 map_every qabbrev_tac [`q = k0 DIV 2`, `r = k0 MOD 2`] >> 436 markerLib.RM_ALL_ABBREVS_TAC >> 437 fs[EVEN_ADD, EVEN_MULT] >> 438 `(r = 0) \/ (r = 1)` by simp[] >> fs[]) 439 440val size_insert = Q.store_thm( 441 "size_insert", 442 `!k v m. size (insert k v m) = if k IN domain m then size m else size m + 1`, 443 ho_match_mp_tac insert_ind >> rpt conj_tac >> simp[] >> 444 rpt strip_tac >> simp[Once insert_def] 445 >- rw[] 446 >- rw[] 447 >- (Cases_on `k = 0` >> simp[] >> fs[] >> Cases_on `EVEN k` >> fs[] 448 >- (`!n. k <> 2 * n + 1` by (rpt strip_tac >> fs[EVEN_ADD, EVEN_MULT]) >> 449 qabbrev_tac `k2 = (k - 1) DIV 2` >> 450 `k = 2 * k2 + 2` suffices_by rw[] >> 451 simp[Abbr`k2`, even_lem]) >> 452 `!n. k <> 2 * n + 2` by (rpt strip_tac >> fs[EVEN_ADD, EVEN_MULT]) >> 453 qabbrev_tac `k2 = (k - 1) DIV 2` >> 454 `k = 2 * k2 + 1` suffices_by rw[] >> 455 simp[Abbr`k2`, odd_lem]) 456 >- (Cases_on `k = 0` >> simp[] >> fs[] >> Cases_on `EVEN k` >> fs[] 457 >- (`!n. k <> 2 * n + 1` by (rpt strip_tac >> fs[EVEN_ADD, EVEN_MULT]) >> 458 qabbrev_tac `k2 = (k - 1) DIV 2` >> 459 `k = 2 * k2 + 2` suffices_by rw[] >> 460 simp[Abbr`k2`, even_lem]) >> 461 `!n. k <> 2 * n + 2` by (rpt strip_tac >> fs[EVEN_ADD, EVEN_MULT]) >> 462 qabbrev_tac `k2 = (k - 1) DIV 2` >> 463 `k = 2 * k2 + 1` suffices_by rw[] >> 464 simp[Abbr`k2`, odd_lem])) 465 466val lookup_fromList = store_thm( 467 "lookup_fromList", 468 ``lookup n (fromList l) = if n < LENGTH l then SOME (EL n l) 469 else NONE``, 470 simp[fromList_def] >> 471 `!i n t. lookup n (SND (FOLDL (\ (i,t) a. (i+1,insert i a t)) (i,t) l)) = 472 if n < i then lookup n t 473 else if n < LENGTH l + i then SOME (EL (n - i) l) 474 else lookup n t` 475 suffices_by (simp[] >> strip_tac >> simp[lookup_def]) >> 476 Induct_on `l` >> simp[] >> pop_assum kall_tac >> 477 rw[lookup_insert] >> 478 full_simp_tac (srw_ss() ++ ARITH_ss) [] >> 479 `0 < n - i` by simp[] >> 480 Cases_on `n - i` >> fs[] >> 481 qmatch_assum_rename_tac `n - i = SUC nn` >> 482 `nn = n - (i + 1)` by decide_tac >> simp[]); 483 484val bit_cases = prove( 485 ``!n. (n = 0) \/ (?m. n = 2 * m + 1) \/ (?m. n = 2 * m + 2)``, 486 Induct >> simp[] >> fs[] 487 >- (disj2_tac >> qexists_tac `m` >> simp[]) 488 >- (disj1_tac >> qexists_tac `SUC m` >> simp[])) 489 490val oddevenlemma = prove( 491 ``2 * y + 1 <> 2 * x + 2``, 492 disch_then (mp_tac o AP_TERM ``EVEN``) >> 493 simp[EVEN_ADD, EVEN_MULT]); 494 495val MULT2_DIV' = prove( 496 ``(2 * m DIV 2 = m) /\ ((2 * m + 1) DIV 2 = m)``, 497 simp[DIV_EQ_X]); 498 499val domain_lookup = store_thm( 500 "domain_lookup", 501 ``!t k. k IN domain t <=> ?v. lookup k t = SOME v``, 502 Induct >> simp[domain_def, lookup_def] >> rpt gen_tac >> 503 qspec_then `k` STRUCT_CASES_TAC bit_cases >> 504 simp[oddevenlemma, EVEN_ADD, EVEN_MULT, 505 EQ_MULT_LCANCEL, MULT2_DIV']); 506 507val lookup_inter_alt = store_thm("lookup_inter_alt", 508 ``lookup x (inter t1 t2) = 509 if x IN domain t2 then lookup x t1 else NONE``, 510 fs [lookup_inter,domain_lookup] 511 \\ Cases_on `lookup x t2` \\ fs [] \\ Cases_on `lookup x t1` \\ fs []); 512 513val lookup_NONE_domain = store_thm( 514 "lookup_NONE_domain", 515 ``(lookup k t = NONE) <=> k NOTIN domain t``, 516 simp[domain_lookup] >> Cases_on `lookup k t` >> simp[]); 517 518val domain_union = store_thm( 519 "domain_union", 520 ``domain (union t1 t2) = domain t1 UNION domain t2``, 521 simp[pred_setTheory.EXTENSION, domain_lookup, lookup_union] >> 522 qx_gen_tac `k` >> Cases_on `lookup k t1` >> simp[]); 523 524val domain_inter = store_thm( 525 "domain_inter", 526 ``domain (inter t1 t2) = domain t1 INTER domain t2``, 527 simp[pred_setTheory.EXTENSION, domain_lookup, lookup_inter] >> 528 rw [] >> Cases_on `lookup x t1` >> fs[] >> 529 BasicProvers.CASE_TAC); 530 531val domain_insert = store_thm( 532 "domain_insert[simp]", 533 ``domain (insert k v t) = k INSERT domain t``, 534 simp[domain_lookup, pred_setTheory.EXTENSION, lookup_insert] >> 535 metis_tac[]); 536 537val domain_difference = Q.store_thm( 538 "domain_difference", 539 `!t1 t2 . domain (difference t1 t2) = (domain t1) DIFF (domain t2)`, 540 simp[pred_setTheory.EXTENSION, domain_lookup, lookup_difference] >> 541 rw [] >> Cases_on `lookup x t1` 542 >> fs[] >> Cases_on `lookup x t2` >> rw[]); 543 544val domain_sing = save_thm( 545 "domain_sing", 546 domain_insert |> Q.INST [`t` |-> `LN`] |> SIMP_RULE bool_ss [domain_def]); 547 548val domain_fromList = store_thm( 549 "domain_fromList", 550 ``domain (fromList l) = count (LENGTH l)``, 551 simp[fromList_def] >> 552 `!i t. domain (SND (FOLDL (\ (i,t) a. (i + 1, insert i a t)) (i,t) l)) = 553 domain t UNION IMAGE ((+) i) (count (LENGTH l))` 554 suffices_by (simp[] >> strip_tac >> simp[pred_setTheory.EXTENSION]) >> 555 Induct_on `l` >> simp[pred_setTheory.EXTENSION, EQ_IMP_THM] >> 556 rpt strip_tac >> simp[DECIDE ``(x = x + y) <=> (y = 0)``] >> 557 qmatch_assum_rename_tac `nn < SUC (LENGTH l)` >> 558 Cases_on `nn` >> fs[] >> metis_tac[ADD1]); 559 560val ODD_IMP_NOT_ODD = prove( 561 ``!k. ODD k ==> ~(ODD (k-1))``, 562 Cases >> fs [ODD]); 563 564val lookup_delete = store_thm( 565 "lookup_delete", 566 ``!t k1 k2. 567 lookup k1 (delete k2 t) = if k1 = k2 then NONE 568 else lookup k1 t``, 569 Induct >> simp[delete_def, lookup_def] 570 >> rw [lookup_def,lookup_mk_BN,lookup_mk_BS] 571 >> sg `(k1 - 1) DIV 2 <> (k2 - 1) DIV 2` 572 >> simp[DIV2_EQ_DIV2, EVEN_PRE] 573 >> fs [] >> CCONTR_TAC >> fs [] >> srw_tac [] [] 574 >> fs [EVEN_ODD] >> imp_res_tac ODD_IMP_NOT_ODD); 575 576val domain_delete = store_thm( 577 "domain_delete[simp]", 578 ``domain (delete k t) = domain t DELETE k``, 579 simp[pred_setTheory.EXTENSION, domain_lookup, lookup_delete] >> 580 metis_tac[]); 581 582val foldi_def = Define` 583 (foldi f i acc LN = acc) /\ 584 (foldi f i acc (LS a) = f i a acc) /\ 585 (foldi f i acc (BN t1 t2) = 586 let inc = lrnext i 587 in 588 foldi f (i + inc) (foldi f (i + 2 * inc) acc t1) t2) /\ 589 (foldi f i acc (BS t1 a t2) = 590 let inc = lrnext i 591 in 592 foldi f (i + inc) (f i a (foldi f (i + 2 * inc) acc t1)) t2) 593`; 594 595val spt_acc_def = tDefine"spt_acc"` 596 (spt_acc i 0 = i) /\ 597 (spt_acc i (SUC k) = spt_acc (i + if EVEN (SUC k) then 2 * lrnext i else lrnext i) (k DIV 2))` 598 (WF_REL_TAC`measure SND` 599 \\ simp[DIV_LT_X]); 600 601val spt_acc_thm = Q.store_thm("spt_acc_thm", 602 `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)`, 603 rw[spt_acc_def] \\ Cases_on`k` \\ fs[spt_acc_def]); 604 605val lemmas = prove( 606 ``(!x. EVEN (2 * x + 2)) /\ 607 (!x. ODD (2 * x + 1))``, 608 conj_tac >- ( 609 simp[EVEN_EXISTS] >> rw[] >> 610 qexists_tac`SUC x` >> simp[] ) >> 611 simp[ODD_EXISTS,ADD1] >> 612 metis_tac[] ) 613 614val bit_induction = prove( 615 ``!P. P 0 /\ (!n. P n ==> P (2 * n + 1)) /\ 616 (!n. P n ==> P (2 * n + 2)) ==> 617 !n. P n``, 618 gen_tac >> strip_tac >> completeInduct_on `n` >> simp[] >> 619 qspec_then `n` strip_assume_tac bit_cases >> simp[]); 620 621val lrnext212 = prove( 622 ``(lrnext (2 * m + 1) = 2 * lrnext m) /\ 623 (lrnext (2 * m + 2) = 2 * lrnext m)``, 624 conj_tac >| [ 625 `2 * m + 1 = BIT1 m` suffices_by simp[lrnext_thm] >> 626 simp_tac bool_ss [BIT1, TWO, ONE, MULT_CLAUSES, ADD_CLAUSES], 627 `2 * m + 2 = BIT2 m` suffices_by simp[lrnext_thm] >> 628 simp_tac bool_ss [BIT2, TWO, ONE, MULT_CLAUSES, ADD_CLAUSES] 629 ]); 630 631val lrlemma1 = prove( 632 ``lrnext (i + lrnext i) = 2 * lrnext i``, 633 qid_spec_tac `i` >> ho_match_mp_tac bit_induction >> 634 simp[lrnext212, lrnext_thm] >> conj_tac 635 >- (gen_tac >> 636 `2 * i + (2 * lrnext i + 1) = 2 * (i + lrnext i) + 1` 637 by decide_tac >> simp[lrnext212]) >> 638 qx_gen_tac `i` >> 639 `2 * i + (2 * lrnext i + 2) = 2 * (i + lrnext i) + 2` 640 by decide_tac >> 641 simp[lrnext212]); 642 643val lrlemma2 = prove( 644 ``lrnext (i + 2 * lrnext i) = 2 * lrnext i``, 645 qid_spec_tac `i` >> ho_match_mp_tac bit_induction >> 646 simp[lrnext212, lrnext_thm] >> conj_tac 647 >- (qx_gen_tac `i` >> 648 `2 * i + (4 * lrnext i + 1) = 2 * (i + 2 * lrnext i) + 1` 649 by decide_tac >> simp[lrnext212]) >> 650 gen_tac >> 651 `2 * i + (4 * lrnext i + 2) = 2 * (i + 2 * lrnext i) + 2` 652 by decide_tac >> simp[lrnext212]) 653 654val spt_acc_eqn = Q.store_thm("spt_acc_eqn", 655 `!k i. spt_acc i k = lrnext i * k + i`, 656 ho_match_mp_tac bit_induction 657 \\ rw[] 658 >- rw[spt_acc_def] 659 >- ( 660 rw[Once spt_acc_thm] 661 >- fs[EVEN_ODD,lemmas] 662 \\ simp[MULT2_DIV'] 663 \\ simp[lrlemma1] ) 664 >- ( 665 ONCE_REWRITE_TAC[spt_acc_thm] 666 \\ simp[] 667 \\ reverse(rw[]) 668 >- fs[EVEN_ODD,lemmas] 669 \\ simp[MULT2_DIV'] 670 \\ simp[lrlemma2])); 671 672val spt_acc_0 = Q.store_thm("spt_acc_0", 673 `!k. spt_acc 0 k = k`, rw[spt_acc_eqn,lrnext_thm]); 674 675val set_foldi_keys = store_thm( 676 "set_foldi_keys", 677 ``!t a i. foldi (\k v a. k INSERT a) i a t = 678 a UNION IMAGE (\n. i + lrnext i * n) (domain t)``, 679 Induct_on `t` >> simp[foldi_def, GSYM pred_setTheory.IMAGE_COMPOSE, 680 combinTheory.o_ABS_R] 681 >- simp[Once pred_setTheory.INSERT_SING_UNION, pred_setTheory.UNION_COMM] 682 >- (simp[pred_setTheory.EXTENSION] >> rpt gen_tac >> 683 Cases_on `x IN a` >> simp[lrlemma1, lrlemma2, LEFT_ADD_DISTRIB]) >> 684 simp[pred_setTheory.EXTENSION] >> rpt gen_tac >> 685 Cases_on `x IN a'` >> simp[lrlemma1, lrlemma2, LEFT_ADD_DISTRIB]) 686 687val domain_foldi = save_thm( 688 "domain_foldi", 689 set_foldi_keys |> SPEC_ALL |> Q.INST [`i` |-> `0`, `a` |-> `{}`] 690 |> SIMP_RULE (srw_ss()) [lrnext_thm] 691 |> SYM); 692val _ = computeLib.add_persistent_funs ["domain_foldi"] 693 694val mapi0_def = Define` 695 (mapi0 f i LN = LN) /\ 696 (mapi0 f i (LS a) = LS (f i a)) /\ 697 (mapi0 f i (BN t1 t2) = 698 let inc = lrnext i in 699 mk_BN (mapi0 f (i + 2 * inc) t1) (mapi0 f (i + inc) t2)) /\ 700 (mapi0 f i (BS t1 a t2) = 701 let inc = lrnext i in 702 mk_BS (mapi0 f (i + 2 * inc) t1) (f i a) (mapi0 f (i + inc) t2)) 703`; 704val _ = export_rewrites ["mapi0_def"] 705val mapi_def = Define`mapi f pt = mapi0 f 0 pt`; 706 707val lookup_mapi0 = Q.store_thm("lookup_mapi0", 708 `!pt i k. 709 lookup k (mapi0 f i pt) = 710 case lookup k pt of NONE => NONE 711 | SOME v => SOME (f (spt_acc i k) v)`, 712 Induct \\ rw[mapi0_def,lookup_def,lookup_mk_BN,lookup_mk_BS] \\ fs[] 713 \\ TRY (simp[spt_acc_eqn] \\ NO_TAC) 714 \\ CASE_TAC \\ simp[Once spt_acc_thm,SimpRHS]); 715 716val lookup_mapi = Q.store_thm("lookup_mapi", 717 `lookup k (mapi f pt) = OPTION_MAP (f k) (lookup k pt)`, 718 rw[mapi_def,lookup_mapi0,spt_acc_0] 719 \\ CASE_TAC \\ fs[]); 720 721val toAList_def = Define ` 722 toAList = foldi (\k v a. (k,v)::a) 0 []` 723 724val set_toAList_lemma = prove( 725 ``!t a i. set (foldi (\k v a. (k,v) :: a) i a t) = 726 set a UNION IMAGE (\n. (i + lrnext i * n, 727 THE (lookup n t))) (domain t)``, 728 Induct_on `t` 729 \\ fs [foldi_def,GSYM pred_setTheory.IMAGE_COMPOSE,lookup_def] 730 THEN1 fs [Once pred_setTheory.INSERT_SING_UNION, pred_setTheory.UNION_COMM] 731 THEN1 (simp[pred_setTheory.EXTENSION] \\ rpt gen_tac \\ 732 Cases_on `MEM x a` \\ simp[lrlemma1, lrlemma2, LEFT_ADD_DISTRIB] 733 \\ fs [MULT2_DIV',EVEN_ADD,EVEN_DOUBLE]) 734 \\ simp[pred_setTheory.EXTENSION] \\ rpt gen_tac 735 \\ Cases_on `MEM x a'` \\ simp[lrlemma1, lrlemma2, LEFT_ADD_DISTRIB] 736 \\ fs [MULT2_DIV',EVEN_ADD,EVEN_DOUBLE]) 737 |> Q.SPECL [`t`,`[]`,`0`] |> GEN_ALL 738 |> SIMP_RULE (srw_ss()) [GSYM toAList_def,lrnext_thm,MEM,LIST_TO_SET, 739 pred_setTheory.UNION_EMPTY,pred_setTheory.EXTENSION, 740 pairTheory.FORALL_PROD] 741 742val MEM_toAList = store_thm("MEM_toAList", 743 ``!t k v. MEM (k,v) (toAList t) <=> (lookup k t = SOME v)``, 744 fs [set_toAList_lemma,domain_lookup] \\ REPEAT STRIP_TAC 745 \\ Cases_on `lookup k t` \\ fs [] 746 \\ REPEAT STRIP_TAC \\ EQ_TAC \\ fs []); 747 748val ALOOKUP_toAList = store_thm("ALOOKUP_toAList", 749 ``!t x. ALOOKUP (toAList t) x = lookup x t``, 750 strip_tac>>strip_tac>>Cases_on `lookup x t` >- 751 simp[ALOOKUP_FAILS,MEM_toAList] >> 752 Cases_on`ALOOKUP (toAList t) x`>- 753 fs[ALOOKUP_FAILS,MEM_toAList] >> 754 imp_res_tac ALOOKUP_MEM >> 755 fs[MEM_toAList]) 756 757val insert_union = store_thm("insert_union", 758 ``!k v s. insert k v s = union (insert k v LN) s``, 759 completeInduct_on`k` >> simp[Once insert_def] >> rw[] >> 760 simp[Once union_def] >> 761 Cases_on`s`>>simp[Once insert_def] >> 762 simp[Once union_def] >> 763 first_x_assum match_mp_tac >> 764 simp[arithmeticTheory.DIV_LT_X]) 765 766val domain_empty = store_thm("domain_empty", 767 ``!t. wf t ==> ((t = LN) <=> (domain t = EMPTY))``, 768 simp[] >> Induct >> simp[wf_def] >> metis_tac[]) 769 770val toAList_append = prove( 771 ``!t n ls. 772 foldi (\k v a. (k,v)::a) n ls t = 773 foldi (\k v a. (k,v)::a) n [] t ++ ls``, 774 Induct 775 >- simp[foldi_def] 776 >- simp[foldi_def] 777 >- ( 778 simp_tac std_ss [foldi_def,LET_THM] >> rpt gen_tac >> 779 first_assum(fn th => 780 CONV_TAC(LAND_CONV(RATOR_CONV(RAND_CONV(REWR_CONV th))))) >> 781 first_assum(fn th => 782 CONV_TAC(LAND_CONV(REWR_CONV th))) >> 783 first_assum(fn th => 784 CONV_TAC(RAND_CONV(LAND_CONV(REWR_CONV th)))) >> 785 metis_tac[APPEND_ASSOC] ) >> 786 simp_tac std_ss [foldi_def,LET_THM] >> rpt gen_tac >> 787 first_assum(fn th => 788 CONV_TAC(LAND_CONV(RATOR_CONV(RAND_CONV(RAND_CONV(REWR_CONV th)))))) >> 789 first_assum(fn th => 790 CONV_TAC(LAND_CONV(REWR_CONV th))) >> 791 first_assum(fn th => 792 CONV_TAC(RAND_CONV(LAND_CONV(REWR_CONV th)))) >> 793 metis_tac[APPEND_ASSOC,APPEND] ) 794 795val toAList_inc = prove( 796 ``!t n. 797 foldi (\k v a. (k,v)::a) n [] t = 798 MAP (\(k,v). (n + lrnext n * k,v)) (foldi (\k v a. (k,v)::a) 0 [] t)``, 799 Induct 800 >- simp[foldi_def] 801 >- simp[foldi_def] 802 >- ( 803 simp_tac std_ss [foldi_def,LET_THM] >> rpt gen_tac >> 804 CONV_TAC(LAND_CONV(REWR_CONV toAList_append)) >> 805 CONV_TAC(RAND_CONV(RAND_CONV(REWR_CONV toAList_append))) >> 806 first_assum(fn th => 807 CONV_TAC(LAND_CONV(LAND_CONV(REWR_CONV th)))) >> 808 first_assum(fn th => 809 CONV_TAC(LAND_CONV(RAND_CONV(REWR_CONV th)))) >> 810 first_assum(fn th => 811 CONV_TAC(RAND_CONV(RAND_CONV(LAND_CONV(REWR_CONV th))))) >> 812 first_assum(fn th => 813 CONV_TAC(RAND_CONV(RAND_CONV(RAND_CONV(REWR_CONV th))))) >> 814 rpt(pop_assum kall_tac) >> 815 simp[MAP_MAP_o,combinTheory.o_DEF,APPEND_11_LENGTH] >> 816 simp[MAP_EQ_f] >> 817 simp[lrnext_thm,pairTheory.UNCURRY,pairTheory.FORALL_PROD] >> 818 simp[lrlemma1,lrlemma2] ) 819 >- ( 820 simp_tac std_ss [foldi_def,LET_THM] >> rpt gen_tac >> 821 CONV_TAC(LAND_CONV(REWR_CONV toAList_append)) >> 822 CONV_TAC(RAND_CONV(RAND_CONV(REWR_CONV toAList_append))) >> 823 first_assum(fn th => 824 CONV_TAC(LAND_CONV(LAND_CONV(REWR_CONV th)))) >> 825 first_assum(fn th => 826 CONV_TAC(LAND_CONV(RAND_CONV(RAND_CONV(REWR_CONV th))))) >> 827 first_assum(fn th => 828 CONV_TAC(RAND_CONV(RAND_CONV(LAND_CONV(REWR_CONV th))))) >> 829 first_assum(fn th => 830 CONV_TAC(RAND_CONV(RAND_CONV(RAND_CONV(RAND_CONV(REWR_CONV th)))))) >> 831 rpt(pop_assum kall_tac) >> 832 simp[MAP_MAP_o,combinTheory.o_DEF,APPEND_11_LENGTH] >> 833 simp[MAP_EQ_f] >> 834 simp[lrnext_thm,pairTheory.UNCURRY,pairTheory.FORALL_PROD] >> 835 simp[lrlemma1,lrlemma2] )) 836 837val ALL_DISTINCT_MAP_FST_toAList = store_thm("ALL_DISTINCT_MAP_FST_toAList", 838 ``!t. ALL_DISTINCT (MAP FST (toAList t))``, 839 simp[toAList_def] >> 840 Induct >> simp[foldi_def] >- ( 841 CONV_TAC(RAND_CONV(RAND_CONV(RATOR_CONV(RAND_CONV(REWR_CONV toAList_inc))))) >> 842 CONV_TAC(RAND_CONV(RAND_CONV(REWR_CONV toAList_append))) >> 843 CONV_TAC(RAND_CONV(RAND_CONV(LAND_CONV(REWR_CONV toAList_inc)))) >> 844 simp[MAP_MAP_o,combinTheory.o_DEF,pairTheory.UNCURRY,lrnext_thm] >> 845 simp[ALL_DISTINCT_APPEND] >> 846 rpt conj_tac >- ( 847 qmatch_abbrev_tac`ALL_DISTINCT (MAP f ls)` >> 848 `MAP f ls = MAP (\x. 2 * x + 1) (MAP FST ls)` by ( 849 simp[MAP_MAP_o,combinTheory.o_DEF,Abbr`f`] ) >> 850 pop_assum SUBST1_TAC >> qunabbrev_tac`f` >> 851 match_mp_tac ALL_DISTINCT_MAP_INJ >> 852 simp[] ) 853 >- ( 854 qmatch_abbrev_tac`ALL_DISTINCT (MAP f ls)` >> 855 `MAP f ls = MAP (\x. 2 * x + 2) (MAP FST ls)` by ( 856 simp[MAP_MAP_o,combinTheory.o_DEF,Abbr`f`] ) >> 857 pop_assum SUBST1_TAC >> qunabbrev_tac`f` >> 858 match_mp_tac ALL_DISTINCT_MAP_INJ >> 859 simp[] ) >> 860 simp[MEM_MAP,PULL_EXISTS,pairTheory.EXISTS_PROD] >> 861 metis_tac[ODD_EVEN,lemmas] ) >> 862 gen_tac >> 863 CONV_TAC(RAND_CONV(RAND_CONV(RATOR_CONV(RAND_CONV(RAND_CONV(REWR_CONV toAList_inc)))))) >> 864 CONV_TAC(RAND_CONV(RAND_CONV(REWR_CONV toAList_append))) >> 865 CONV_TAC(RAND_CONV(RAND_CONV(LAND_CONV(REWR_CONV toAList_inc)))) >> 866 simp[MAP_MAP_o,combinTheory.o_DEF,pairTheory.UNCURRY,lrnext_thm] >> 867 simp[ALL_DISTINCT_APPEND] >> 868 rpt conj_tac >- ( 869 qmatch_abbrev_tac`ALL_DISTINCT (MAP f ls)` >> 870 `MAP f ls = MAP (\x. 2 * x + 1) (MAP FST ls)` by ( 871 simp[MAP_MAP_o,combinTheory.o_DEF,Abbr`f`] ) >> 872 pop_assum SUBST1_TAC >> qunabbrev_tac`f` >> 873 match_mp_tac ALL_DISTINCT_MAP_INJ >> 874 simp[] ) 875 >- ( simp[MEM_MAP] ) 876 >- ( 877 qmatch_abbrev_tac`ALL_DISTINCT (MAP f ls)` >> 878 `MAP f ls = MAP (\x. 2 * x + 2) (MAP FST ls)` by ( 879 simp[MAP_MAP_o,combinTheory.o_DEF,Abbr`f`] ) >> 880 pop_assum SUBST1_TAC >> qunabbrev_tac`f` >> 881 match_mp_tac ALL_DISTINCT_MAP_INJ >> 882 simp[] ) >> 883 simp[MEM_MAP,PULL_EXISTS,pairTheory.EXISTS_PROD] >> 884 metis_tac[ODD_EVEN,lemmas] ) 885 886val _ = remove_ovl_mapping "lrnext" {Name = "lrnext", Thy = "sptree"} 887 888val foldi_FOLDR_toAList_lemma = prove( 889 ``!t n a ls. foldi f n (FOLDR (UNCURRY f) a ls) t = 890 FOLDR (UNCURRY f) a (foldi (\k v a. (k,v)::a) n ls t)``, 891 Induct >> simp[foldi_def] >> 892 rw[] >> pop_assum(assume_tac o GSYM) >> simp[]) 893 894val foldi_FOLDR_toAList = store_thm("foldi_FOLDR_toAList", 895 ``!f a t. foldi f 0 a t = FOLDR (UNCURRY f) a (toAList t)``, 896 simp[toAList_def,GSYM foldi_FOLDR_toAList_lemma]) 897 898val toListA_def = Define` 899 (toListA acc LN = acc) /\ 900 (toListA acc (LS a) = a::acc) /\ 901 (toListA acc (BN t1 t2) = toListA (toListA acc t2) t1) /\ 902 (toListA acc (BS t1 a t2) = toListA (a :: toListA acc t2) t1) 903`; 904 905local open listTheory rich_listTheory in 906val toListA_append = store_thm("toListA_append", 907 ``!t acc. toListA acc t = toListA [] t ++ acc``, 908 Induct >> REWRITE_TAC[toListA_def] 909 >> metis_tac[APPEND_ASSOC,CONS_APPEND,APPEND]) 910end 911 912val isEmpty_toListA = store_thm("isEmpty_toListA", 913 ``!t acc. wf t ==> ((t = LN) <=> (toListA acc t = acc))``, 914 Induct >> simp[toListA_def,wf_def] >> 915 rw[] >> fs[] >> 916 fs[Once toListA_append] >> 917 simp[Once toListA_append,SimpR``$++``]) 918 919val toList_def = Define`toList m = toListA [] m` 920 921val isEmpty_toList = store_thm("isEmpty_toList", 922 ``!t. wf t ==> ((t = LN) <=> (toList t = []))``, 923 rw[toList_def,isEmpty_toListA]) 924 925val lem2 = 926 SIMP_RULE (srw_ss()) [] (Q.SPECL[`2`,`1`]DIV_MULT) 927 928fun tac () = ( 929 (disj2_tac >> qexists_tac`0` >> simp[] >> NO_TAC) ORELSE 930 (disj2_tac >> 931 qexists_tac`2*k+1` >> simp[] >> 932 REWRITE_TAC[Once MULT_COMM] >> simp[MULT_DIV] >> 933 rw[] >> `F` suffices_by rw[] >> pop_assum mp_tac >> 934 simp[lemmas,GSYM ODD_EVEN] >> NO_TAC) ORELSE 935 (disj2_tac >> 936 qexists_tac`2*k+2` >> simp[] >> 937 REWRITE_TAC[Once MULT_COMM] >> simp[lem2] >> 938 rw[] >> `F` suffices_by rw[] >> pop_assum mp_tac >> 939 simp[lemmas] >> NO_TAC) ORELSE 940 (metis_tac[])) 941 942val MEM_toListA = prove( 943 ``!t acc x. MEM x (toListA acc t) <=> (MEM x acc \/ ?k. lookup k t = SOME x)``, 944 Induct >> simp[toListA_def,lookup_def] >- metis_tac[] >> 945 rw[EQ_IMP_THM] >> rw[] >> pop_assum mp_tac >> rw[] 946 >- (tac()) 947 >- (tac()) 948 >- (tac()) 949 >- (tac()) 950 >- (tac()) 951 >- (tac()) 952 >- (tac()) 953 >- (tac()) 954 >- (tac())) 955 956val MEM_toList = store_thm("MEM_toList", 957 ``!x t. MEM x (toList t) <=> ?k. lookup k t = SOME x``, 958 rw[toList_def,MEM_toListA]) 959 960val div2_even_lemma = prove( 961 ``!x. ?n. (x = (n - 1) DIV 2) /\ EVEN n /\ 0 < n``, 962 Induct >- ( qexists_tac`2` >> simp[] ) >> fs[] >> 963 qexists_tac`n+2` >> 964 simp[ADD1,EVEN_ADD] >> 965 Cases_on`n`>>fs[EVEN,EVEN_ODD,ODD_EXISTS,ADD1] >> 966 simp[] >> rw[] >> 967 qspec_then`2`mp_tac ADD_DIV_ADD_DIV >> simp[] >> 968 disch_then(qspecl_then[`m`,`3`]mp_tac) >> 969 simp[] >> disch_then kall_tac >> 970 qspec_then`2`mp_tac ADD_DIV_ADD_DIV >> simp[] >> 971 disch_then(qspecl_then[`m`,`1`]mp_tac) >> 972 simp[]) 973 974val div2_odd_lemma = prove( 975 ``!x. ?n. (x = (n - 1) DIV 2) /\ ODD n /\ 0 < n``, 976 Induct >- ( qexists_tac`1` >> simp[] ) >> fs[] >> 977 qexists_tac`n+2` >> 978 simp[ADD1,ODD_ADD] >> 979 fs[ODD_EXISTS,ADD1] >> 980 simp[] >> rw[] >> 981 qspec_then`2`mp_tac ADD_DIV_ADD_DIV >> simp[] >> 982 disch_then(qspecl_then[`m`,`2`]mp_tac) >> 983 simp[] >> disch_then kall_tac >> 984 qspec_then`2`mp_tac ADD_DIV_ADD_DIV >> simp[] >> 985 disch_then(qspecl_then[`m`,`0`]mp_tac) >> 986 simp[]) 987 988val spt_eq_thm = store_thm("spt_eq_thm", 989 ``!t1 t2. wf t1 /\ wf t2 ==> 990 ((t1 = t2) <=> !n. lookup n t1 = lookup n t2)``, 991 Induct >> simp[wf_def,lookup_def] 992 >- ( 993 rw[EQ_IMP_THM] >> rw[lookup_def] >> 994 `domain t2 = {}` by ( 995 simp[pred_setTheory.EXTENSION] >> 996 metis_tac[lookup_NONE_domain] ) >> 997 Cases_on`t2`>>fs[domain_def,wf_def] >> 998 metis_tac[domain_empty] ) 999 >- ( 1000 rw[EQ_IMP_THM] >> rw[lookup_def] >> 1001 Cases_on`t2`>>fs[lookup_def] 1002 >- (first_x_assum(qspec_then`0`mp_tac)>>simp[]) 1003 >- (first_x_assum(qspec_then`0`mp_tac)>>simp[]) >> 1004 fs[wf_def] >> 1005 rfs[domain_empty] >> 1006 fs[GSYM pred_setTheory.MEMBER_NOT_EMPTY] >> 1007 fs[domain_lookup] >| 1008 [ qspec_then`x`strip_assume_tac div2_even_lemma 1009 , qspec_then`x`strip_assume_tac div2_odd_lemma 1010 ] >> 1011 first_x_assum(qspec_then`n`mp_tac) >> 1012 fs[ODD_EVEN] >> simp[] ) 1013 >- ( 1014 rw[EQ_IMP_THM] >> rw[lookup_def] >> 1015 rfs[domain_empty] >> 1016 fs[GSYM pred_setTheory.MEMBER_NOT_EMPTY] >> 1017 fs[domain_lookup] >> 1018 Cases_on`t2`>>fs[] >> 1019 TRY ( 1020 first_x_assum(qspec_then`0`mp_tac) >> 1021 simp[lookup_def] >> NO_TAC) >> 1022 TRY ( 1023 qspec_then`x`strip_assume_tac div2_even_lemma >> 1024 first_x_assum(qspec_then`n`mp_tac) >> fs[] >> 1025 simp[lookup_def] >> NO_TAC) >> 1026 TRY ( 1027 qspec_then`x`strip_assume_tac div2_odd_lemma >> 1028 first_x_assum(qspec_then`n`mp_tac) >> fs[ODD_EVEN] >> 1029 simp[lookup_def] >> NO_TAC) >> 1030 qmatch_assum_rename_tac`wf (BN s1 s2)` >> 1031 `wf s1 /\ wf s2` by fs[wf_def] >> 1032 first_x_assum(qspec_then`s2`mp_tac) >> 1033 first_x_assum(qspec_then`s1`mp_tac) >> 1034 simp[] >> ntac 2 strip_tac >> 1035 fs[lookup_def] >> rw[] >> 1036 metis_tac[prim_recTheory.LESS_REFL,div2_even_lemma,div2_odd_lemma 1037 ,EVEN_ODD] ) 1038 >- ( 1039 rw[EQ_IMP_THM] >> rw[lookup_def] >> 1040 rfs[domain_empty] >> 1041 fs[GSYM pred_setTheory.MEMBER_NOT_EMPTY] >> 1042 fs[domain_lookup] >> 1043 Cases_on`t2`>>fs[] >> 1044 TRY ( 1045 first_x_assum(qspec_then`0`mp_tac) >> 1046 simp[lookup_def] >> NO_TAC) >> 1047 TRY ( 1048 qspec_then`x`strip_assume_tac div2_even_lemma >> 1049 first_x_assum(qspec_then`n`mp_tac) >> fs[] >> 1050 simp[lookup_def] >> NO_TAC) >> 1051 TRY ( 1052 qspec_then`x`strip_assume_tac div2_odd_lemma >> 1053 first_x_assum(qspec_then`n`mp_tac) >> fs[ODD_EVEN] >> 1054 simp[lookup_def] >> NO_TAC) >> 1055 qmatch_assum_rename_tac`wf (BS s1 z s2)` >> 1056 `wf s1 /\ wf s2` by fs[wf_def] >> 1057 first_x_assum(qspec_then`s2`mp_tac) >> 1058 first_x_assum(qspec_then`s1`mp_tac) >> 1059 simp[] >> ntac 2 strip_tac >> 1060 fs[lookup_def] >> rw[] >> 1061 metis_tac[prim_recTheory.LESS_REFL,div2_even_lemma,div2_odd_lemma 1062 ,EVEN_ODD,optionTheory.SOME_11] )) 1063 1064val mk_wf_def = Define ` 1065 (mk_wf LN = LN) /\ 1066 (mk_wf (LS x) = LS x) /\ 1067 (mk_wf (BN t1 t2) = mk_BN (mk_wf t1) (mk_wf t2)) /\ 1068 (mk_wf (BS t1 x t2) = mk_BS (mk_wf t1) x (mk_wf t2))`; 1069 1070val wf_mk_wf = store_thm("wf_mk_wf[simp]", 1071 ``!t. wf (mk_wf t)``, 1072 Induct \\ fs [wf_def,mk_wf_def,wf_mk_BS,wf_mk_BN]); 1073 1074val wf_mk_id = store_thm("wf_mk_id[simp]", 1075 ``!t. wf t ==> (mk_wf t = t)``, 1076 Induct \\ srw_tac [] [wf_def,mk_wf_def,mk_BS_thm,mk_BN_thm]); 1077 1078val lookup_mk_wf = store_thm("lookup_mk_wf[simp]", 1079 ``!x t. lookup x (mk_wf t) = lookup x t``, 1080 Induct_on `t` \\ fs [mk_wf_def,lookup_mk_BS,lookup_mk_BN] 1081 \\ srw_tac [] [lookup_def]); 1082 1083val domain_mk_wf = store_thm("domain_mk_wf[simp]", 1084 ``!t. domain (mk_wf t) = domain t``, 1085 fs [pred_setTheory.EXTENSION,domain_lookup]); 1086 1087val mk_wf_eq = store_thm("mk_wf_eq[simp]", 1088 ``!t1 t2. (mk_wf t1 = mk_wf t2) <=> !x. lookup x t1 = lookup x t2``, 1089 metis_tac [spt_eq_thm,wf_mk_wf,lookup_mk_wf]); 1090 1091val inter_eq = store_thm("inter_eq[simp]", 1092 ``!t1 t2 t3 t4. 1093 (inter t1 t2 = inter t3 t4) <=> 1094 !x. lookup x (inter t1 t2) = lookup x (inter t3 t4)``, 1095 metis_tac [spt_eq_thm,wf_inter]); 1096 1097val union_mk_wf = store_thm("union_mk_wf[simp]", 1098 ``!t1 t2. union (mk_wf t1) (mk_wf t2) = mk_wf (union t1 t2)``, 1099 REPEAT STRIP_TAC 1100 \\ `union (mk_wf t1) (mk_wf t2) = mk_wf (union (mk_wf t1) (mk_wf t2))` by 1101 metis_tac [wf_union,wf_mk_wf,wf_mk_id] 1102 \\ POP_ASSUM (fn th => once_rewrite_tac [th]) 1103 \\ ASM_SIMP_TAC std_ss [mk_wf_eq] \\ fs [lookup_union]); 1104 1105val inter_mk_wf = store_thm("union_mk_wf[simp]", 1106 ``!t1 t2. inter (mk_wf t1) (mk_wf t2) = mk_wf (inter t1 t2)``, 1107 REPEAT STRIP_TAC 1108 \\ `inter (mk_wf t1) (mk_wf t2) = mk_wf (inter (mk_wf t1) (mk_wf t2))` by 1109 metis_tac [wf_inter,wf_mk_wf,wf_mk_id] 1110 \\ POP_ASSUM (fn th => once_rewrite_tac [th]) 1111 \\ ASM_SIMP_TAC std_ss [mk_wf_eq] \\ fs [lookup_inter]); 1112 1113val insert_mk_wf = store_thm("insert_mk_wf[simp]", 1114 ``!x v t. insert x v (mk_wf t) = mk_wf (insert x v t)``, 1115 REPEAT STRIP_TAC 1116 \\ `insert x v (mk_wf t) = mk_wf (insert x v (mk_wf t))` by 1117 metis_tac [wf_insert,wf_mk_wf,wf_mk_id] 1118 \\ POP_ASSUM (fn th => once_rewrite_tac [th]) 1119 \\ ASM_SIMP_TAC std_ss [mk_wf_eq] \\ fs [lookup_insert]); 1120 1121val delete_mk_wf = store_thm("delete_mk_wf[simp]", 1122 ``!x t. delete x (mk_wf t) = mk_wf (delete x t)``, 1123 REPEAT STRIP_TAC 1124 \\ `delete x (mk_wf t) = mk_wf (delete x (mk_wf t))` by 1125 metis_tac [wf_delete,wf_mk_wf,wf_mk_id] 1126 \\ POP_ASSUM (fn th => once_rewrite_tac [th]) 1127 \\ ASM_SIMP_TAC std_ss [mk_wf_eq] \\ fs [lookup_delete]); 1128 1129val union_LN = store_thm("union_LN[simp]", 1130 ``!t. (union t LN = t) /\ (union LN t = t)``, 1131 Cases \\ fs [union_def]); 1132 1133val inter_LN = store_thm("inter_LN[simp]", 1134 ``!t. (inter t LN = LN) /\ (inter LN t = LN)``, 1135 Cases \\ fs [inter_def]); 1136 1137val union_assoc = store_thm("union_assoc", 1138 ``!t1 t2 t3. union t1 (union t2 t3) = union (union t1 t2) t3``, 1139 Induct \\ Cases_on `t2` \\ Cases_on `t3` \\ fs [union_def]); 1140 1141val inter_assoc = store_thm("inter_assoc", 1142 ``!t1 t2 t3. inter t1 (inter t2 t3) = inter (inter t1 t2) t3``, 1143 fs [lookup_inter] \\ REPEAT STRIP_TAC 1144 \\ Cases_on `lookup x t1` \\ fs [] 1145 \\ Cases_on `lookup x t2` \\ fs [] 1146 \\ Cases_on `lookup x t3` \\ fs []); 1147 1148val numeral_div0 = prove( 1149 ``(BIT1 n DIV 2 = n) /\ 1150 (BIT2 n DIV 2 = SUC n) /\ 1151 (SUC (BIT1 n) DIV 2 = SUC n) /\ 1152 (SUC (BIT2 n) DIV 2 = SUC n)``, 1153 REWRITE_TAC[GSYM DIV2_def, numeralTheory.numeral_suc, 1154 REWRITE_RULE [NUMERAL_DEF] 1155 numeralTheory.numeral_div2]) 1156val BIT0 = prove( 1157 ``BIT1 n <> 0 /\ BIT2 n <> 0``, 1158 REWRITE_TAC[BIT1, BIT2, 1159 ADD_CLAUSES, numTheory.NOT_SUC]); 1160 1161val PRE_BIT1 = prove( 1162 ``BIT1 n - 1 = 2 * n``, 1163 REWRITE_TAC [BIT1, NUMERAL_DEF, 1164 ALT_ZERO, ADD_CLAUSES, 1165 BIT2, SUB_MONO_EQ, 1166 MULT_CLAUSES, SUB_0]); 1167 1168val PRE_BIT2 = prove( 1169 ``BIT2 n - 1 = 2 * n + 1``, 1170 REWRITE_TAC [BIT1, NUMERAL_DEF, 1171 ALT_ZERO, ADD_CLAUSES, 1172 BIT2, SUB_MONO_EQ, 1173 MULT_CLAUSES, SUB_0]); 1174 1175val BITDIV = prove( 1176 ``((BIT1 n - 1) DIV 2 = n) /\ ((BIT2 n - 1) DIV 2 = n)``, 1177 simp[PRE_BIT1, PRE_BIT2] >> simp[DIV_EQ_X]); 1178 1179fun computerule th q = 1180 th 1181 |> CONJUNCTS 1182 |> map SPEC_ALL 1183 |> map (Q.INST [`k` |-> q]) 1184 |> map (CONV_RULE 1185 (RAND_CONV (SIMP_CONV bool_ss 1186 ([numeral_div0, BIT0, PRE_BIT1, 1187 numTheory.NOT_SUC, BITDIV, 1188 EVAL ``SUC 0 DIV 2``, 1189 numeralTheory.numeral_evenodd, 1190 EVEN]) THENC 1191 SIMP_CONV bool_ss [ALT_ZERO]))) 1192 1193val lookup_compute = save_thm( 1194 "lookup_compute", 1195 LIST_CONJ (prove (``lookup (NUMERAL n) t = lookup n t``, 1196 REWRITE_TAC [NUMERAL_DEF]) :: 1197 computerule lookup_def `0` @ 1198 computerule lookup_def `ZERO` @ 1199 computerule lookup_def `BIT1 n` @ 1200 computerule lookup_def `BIT2 n`)) 1201val _ = computeLib.add_persistent_funs ["lookup_compute"] 1202 1203val insert_compute = save_thm( 1204 "insert_compute", 1205 LIST_CONJ (prove (``insert (NUMERAL n) a t = insert n a t``, 1206 REWRITE_TAC [NUMERAL_DEF]) :: 1207 computerule insert_def `0` @ 1208 computerule insert_def `ZERO` @ 1209 computerule insert_def `BIT1 n` @ 1210 computerule insert_def `BIT2 n`)) 1211val _ = computeLib.add_persistent_funs ["insert_compute"] 1212 1213val delete_compute = save_thm( 1214 "delete_compute", 1215 LIST_CONJ ( 1216 prove(``delete (NUMERAL n) t = delete n t``, 1217 REWRITE_TAC [NUMERAL_DEF]) :: 1218 computerule delete_def `0` @ 1219 computerule delete_def `ZERO` @ 1220 computerule delete_def `BIT1 n` @ 1221 computerule delete_def `BIT2 n`)) 1222val _ = computeLib.add_persistent_funs ["delete_compute"] 1223 1224val fromAList_def = Define ` 1225 (fromAList [] = LN) /\ 1226 (fromAList ((x,y)::xs) = insert x y (fromAList xs))`; 1227 1228val lookup_fromAList = store_thm("lookup_fromAList", 1229 ``!ls x.lookup x (fromAList ls) = ALOOKUP ls x``, 1230 ho_match_mp_tac (fetch "-" "fromAList_ind")>> 1231 rw[fromAList_def,lookup_def]>> 1232 fs[lookup_insert]>> simp[EQ_SYM_EQ]) 1233 1234val domain_fromAList = store_thm("domain_fromAList", 1235 ``!ls. domain (fromAList ls) = set (MAP FST ls)``, 1236 simp[pred_setTheory.EXTENSION,domain_lookup,lookup_fromAList, 1237 MEM_MAP,pairTheory.EXISTS_PROD]>> 1238 metis_tac[ALOOKUP_MEM,ALOOKUP_FAILS, 1239 optionTheory.option_CASES, 1240 optionTheory.NOT_SOME_NONE]) 1241 1242val lookup_fromAList_toAList = store_thm("lookup_fromAList_toAList", 1243 ``!t x. lookup x (fromAList (toAList t)) = lookup x t``, 1244 simp[lookup_fromAList,ALOOKUP_toAList]) 1245 1246val wf_fromAList = store_thm("wf_fromAList", 1247 ``!ls. wf (fromAList ls)``, 1248 Induct >> 1249 rw[fromAList_def,wf_def]>> 1250 Cases_on`h`>> 1251 rw[fromAList_def]>> 1252 simp[wf_insert]) 1253 1254val fromAList_toAList = store_thm("fromAList_toAList", 1255 ``!t. wf t ==> (fromAList (toAList t) = t)``, 1256 metis_tac[wf_fromAList,lookup_fromAList_toAList,spt_eq_thm]) 1257 1258val map_def = Define` 1259 (map f LN = LN) /\ 1260 (map f (LS a) = (LS (f a))) /\ 1261 (map f (BN t1 t2) = BN (map f t1) (map f t2)) /\ 1262 (map f (BS t1 a t2) = BS (map f t1) (f a) (map f t2))` 1263 1264val toList_map = store_thm("toList_map", 1265 ``!s. toList (map f s) = MAP f (toList s)``, 1266 Induct >> 1267 fs[toList_def,map_def,toListA_def] >> 1268 simp[Once toListA_append] >> 1269 simp[Once toListA_append,SimpRHS]) 1270 1271val domain_map = store_thm("domain_map", 1272 ``!s. domain (map f s) = domain s``, 1273 Induct >> simp[map_def]) 1274 1275val lookup_map = store_thm("lookup_map", 1276 ``!s x. lookup x (map f s) = OPTION_MAP f (lookup x s)``, 1277 Induct >> simp[map_def,lookup_def] >> rw[]) 1278 1279val map_LN = store_thm("map_LN[simp]", 1280 ``!t. (map f t = LN) <=> (t = LN)``, 1281 Cases \\ EVAL_TAC); 1282 1283val wf_map = store_thm("wf_map[simp]", 1284 ``!t f. wf (map f t) = wf t``, 1285 Induct \\ fs [wf_def,map_def]); 1286 1287val map_map_o = store_thm("map_map_o", 1288 ``!t f g. map f (map g t) = map (f o g) t``, 1289 Induct >> fs[map_def]) 1290 1291val map_insert = store_thm("map_insert", 1292 ``!f x y z. 1293 map f (insert x y z) = insert x (f y) (map f z)``, 1294 completeInduct_on`x`>> 1295 Induct_on`z`>> 1296 rw[]>> 1297 simp[Once map_def,Once insert_def]>> 1298 simp[Once insert_def,SimpRHS]>> 1299 BasicProvers.EVERY_CASE_TAC>>fs[map_def]>> 1300 `(x-1) DIV 2 < x` by 1301 (`0 < (2:num)` by fs[] >> 1302 imp_res_tac DIV_LT_X>> 1303 first_x_assum match_mp_tac>> 1304 DECIDE_TAC)>> 1305 fs[map_def]) 1306 1307val insert_insert = store_thm("insert_insert", 1308 ``!x1 x2 v1 v2 t. 1309 insert x1 v1 (insert x2 v2 t) = 1310 if x1 = x2 then insert x1 v1 t else insert x2 v2 (insert x1 v1 t)``, 1311 rpt strip_tac 1312 \\ qspec_tac (`x1`,`x1`) 1313 \\ qspec_tac (`v1`,`v1`) 1314 \\ qspec_tac (`t`,`t`) 1315 \\ qspec_tac (`v2`,`v2`) 1316 \\ qspec_tac (`x2`,`x2`) 1317 \\ recInduct insert_ind \\ rpt strip_tac \\ 1318 (Cases_on `k = 0` \\ fs [] THEN1 1319 (once_rewrite_tac [insert_def] \\ fs [] \\ rw [] 1320 THEN1 (once_rewrite_tac [insert_def] \\ fs []) 1321 \\ once_rewrite_tac [insert_def] \\ fs [] \\ rw []) 1322 \\ once_rewrite_tac [insert_def] \\ fs [] \\ rw [] 1323 \\ simp [Once insert_def] 1324 \\ once_rewrite_tac [EQ_SYM_EQ] 1325 \\ simp [Once insert_def] 1326 \\ Cases_on `x1` \\ fs [ADD1] 1327 \\ Cases_on `k` \\ fs [ADD1] 1328 \\ rw [] \\ fs [EVEN_ADD] 1329 \\ fs [GSYM ODD_EVEN] 1330 \\ fs [EVEN_EXISTS,ODD_EXISTS] \\ rpt BasicProvers.var_eq_tac 1331 \\ fs [ADD1,DIV_MULT|>ONCE_REWRITE_RULE[MULT_COMM], 1332 MULT_DIV|>ONCE_REWRITE_RULE[MULT_COMM]])); 1333 1334val insert_shadow = store_thm("insert_shadow", 1335 ``!t a b c. insert a b (insert a c t) = insert a b t``, 1336 once_rewrite_tac [insert_insert] \\ simp []); 1337 1338(* the sub-map relation, a partial order *) 1339 1340val spt_left_def = Define ` 1341 (spt_left LN = LN) /\ 1342 (spt_left (LS x) = LN) /\ 1343 (spt_left (BN t1 t2) = t1) /\ 1344 (spt_left (BS t1 x t2) = t1)` 1345 1346val spt_right_def = Define ` 1347 (spt_right LN = LN) /\ 1348 (spt_right (LS x) = LN) /\ 1349 (spt_right (BN t1 t2) = t2) /\ 1350 (spt_right (BS t1 x t2) = t2)` 1351 1352val spt_center_def = Define ` 1353 (spt_center (LS x) = SOME x) /\ 1354 (spt_center (BS t1 x t2) = SOME x) /\ 1355 (spt_center _ = NONE)` 1356 1357val subspt_eq = Define ` 1358 (subspt LN t <=> T) /\ 1359 (subspt (LS x) t <=> (spt_center t = SOME x)) /\ 1360 (subspt (BN t1 t2) t <=> 1361 subspt t1 (spt_left t) /\ subspt t2 (spt_right t)) /\ 1362 (subspt (BS t1 x t2) t <=> 1363 (spt_center t = SOME x) /\ 1364 subspt t1 (spt_left t) /\ subspt t2 (spt_right t))` 1365 1366val _ = save_thm("subspt_eq",subspt_eq); 1367 1368val subspt_lookup_lemma = Q.prove( 1369 `(!x y. ((if x = 0:num then SOME a else f x) = SOME y) ==> p x y) 1370 <=> 1371 p 0 a /\ (!x y. x <> 0 /\ (f x = SOME y) ==> p x y)`, 1372 metis_tac [optionTheory.SOME_11]); 1373 1374val subspt_lookup = Q.store_thm("subspt_lookup", 1375 `!t1 t2. 1376 subspt t1 t2 <=> 1377 !x y. (lookup x t1 = SOME y) ==> (lookup x t2 = SOME y)`, 1378 Induct 1379 \\ fs [lookup_def,subspt_eq] 1380 THEN1 (Cases_on `t2` \\ fs [lookup_def,spt_center_def]) 1381 \\ rw [] 1382 THEN1 1383 (Cases_on `t2` 1384 \\ fs [lookup_def,spt_center_def,spt_left_def,spt_right_def] 1385 \\ eq_tac \\ rw [] 1386 \\ TRY (Cases_on `x = 0` \\ fs [] \\ rw [] \\ fs [] \\ NO_TAC) 1387 \\ TRY (first_x_assum (fn th => qspec_then `2 * x + 1` mp_tac th THEN 1388 qspec_then `(2 * x + 1) + 1` mp_tac th)) 1389 \\ fs [MULT_DIV |> ONCE_REWRITE_RULE [MULT_COMM], 1390 DIV_MULT |> ONCE_REWRITE_RULE [MULT_COMM]] 1391 \\ fs [EVEN_ADD,EVEN_DOUBLE]) 1392 \\ Cases_on `spt_center t2` \\ fs [] 1393 THEN1 1394 (qexists_tac `0` \\ fs [] 1395 \\ Cases_on `t2` \\ fs [spt_center_def,lookup_def]) 1396 \\ reverse (Cases_on `x = a`) \\ fs [] 1397 THEN1 1398 (qexists_tac `0` \\ fs [] 1399 \\ Cases_on `t2` \\ fs [spt_center_def,lookup_def]) 1400 \\ BasicProvers.var_eq_tac 1401 \\ fs [subspt_lookup_lemma] 1402 \\ `lookup 0 t2 = SOME a` by 1403 (Cases_on `t2` \\ fs [spt_center_def,lookup_def]) 1404 \\ fs [] 1405 \\ Cases_on `t2` 1406 \\ fs [lookup_def,spt_center_def,spt_left_def,spt_right_def] 1407 \\ eq_tac \\ rw [] 1408 \\ TRY (Cases_on `x = 0` \\ fs [] \\ rw [] \\ fs [] \\ NO_TAC) 1409 \\ TRY (first_x_assum (fn th => qspec_then `2 * x + 1` mp_tac th THEN 1410 qspec_then `(2 * x + 1) + 1` mp_tac th)) 1411 \\ fs [MULT_DIV |> ONCE_REWRITE_RULE [MULT_COMM], 1412 DIV_MULT |> ONCE_REWRITE_RULE [MULT_COMM]] 1413 \\ fs [EVEN_ADD,EVEN_DOUBLE]); 1414 1415val subspt_domain = Q.store_thm("subspt_domain", 1416 `!t1 (t2:unit spt). 1417 subspt t1 t2 <=> domain t1 SUBSET domain t2`, 1418 fs [subspt_lookup,domain_lookup,pred_setTheory.SUBSET_DEF]); 1419 1420val subspt_def = Q.store_thm("subspt_def", 1421 `!sp1 sp2. 1422 subspt sp1 sp2 <=> 1423 !k. k IN domain sp1 ==> k IN domain sp2 /\ 1424 (lookup k sp2 = lookup k sp1)`, 1425 fs [subspt_lookup,domain_lookup] 1426 \\ metis_tac [optionTheory.SOME_11]); 1427 1428val subspt_refl = Q.store_thm( 1429 "subspt_refl[simp]", 1430 `subspt sp sp`, 1431 simp[subspt_def]) 1432 1433val subspt_trans = Q.store_thm( 1434 "subspt_trans", 1435 `subspt sp1 sp2 /\ subspt sp2 sp3 ==> subspt sp1 sp3`, 1436 simp [subspt_lookup]); 1437 1438val subspt_LN = Q.store_thm( 1439 "subspt_LN[simp]", 1440 `(subspt LN sp <=> T) /\ (subspt sp LN <=> (domain sp = {}))`, 1441 simp[subspt_def, pred_setTheory.EXTENSION]); 1442 1443(* filter values stored in sptree *) 1444 1445val filter_v_def = Define ` 1446 (filter_v f LN = LN) /\ 1447 (filter_v f (LS x) = if f x then LS x else LN) /\ 1448 (filter_v f (BN l r) = mk_BN (filter_v f l) (filter_v f r)) /\ 1449 (filter_v f (BS l x r) = 1450 if f x then mk_BS (filter_v f l) x (filter_v f r) 1451 else mk_BN (filter_v f l) (filter_v f r))`; 1452 1453val lookup_filter_v = store_thm("lookup_filter_v", 1454 ``!k t f. lookup k (filter_v f t) = case lookup k t of 1455 | SOME v => if f v then SOME v else NONE 1456 | NONE => NONE``, 1457 ho_match_mp_tac (theorem "lookup_ind") \\ rpt strip_tac \\ 1458 rw [filter_v_def, lookup_mk_BS, lookup_mk_BN] \\ rw [lookup_def] \\ fs []); 1459 1460val wf_filter_v = store_thm("wf_filter_v", 1461 ``!t f. wf t ==> wf (filter_v f t)``, 1462 Induct \\ rw [filter_v_def, wf_def, mk_BN_thm, mk_BS_thm] \\ fs []); 1463 1464val wf_mk_BN = Q.store_thm( 1465 "wf_mk_BN", 1466 `wf t1 /\ wf t2 ==> wf (mk_BN t1 t2)`, 1467 map_every Cases_on [`t1`, `t2`] >> simp[mk_BN_def, wf_def]) 1468 1469val wf_mk_BS = Q.store_thm( 1470 "wf_mk_BS", 1471 `wf t1 /\ wf t2 ==> wf (mk_BS t1 a t2)`, 1472 map_every Cases_on [`t1`, `t2`] >> simp[mk_BS_def, wf_def]) 1473 1474val wf_mapi = Q.store_thm( 1475 "wf_mapi", 1476 `wf (mapi f pt)`, 1477 simp[mapi_def] >> 1478 `!n. wf (mapi0 f n pt)` suffices_by simp[] >> Induct_on `pt` >> 1479 simp[wf_def, wf_mk_BN, wf_mk_BS]); 1480 1481val ALOOKUP_MAP_lemma = Q.prove( 1482 `ALOOKUP (MAP (\kv. (FST kv, f (FST kv) (SND kv))) al) n = 1483 OPTION_MAP (\v. f n v) (ALOOKUP al n)`, 1484 Induct_on `al` >> simp[pairTheory.FORALL_PROD] >> rw[]); 1485 1486val lookup_mk_BN = Q.store_thm( 1487 "lookup_mk_BN", 1488 `lookup i (mk_BN t1 t2) = 1489 if i = 0 then NONE 1490 else lookup ((i - 1) DIV 2) (if EVEN i then t1 else t2)`, 1491 map_every Cases_on [`t1`, `t2`] >> simp[mk_BN_def, lookup_def]); 1492 1493val MAP_foldi = Q.store_thm( 1494 "MAP_foldi", 1495 `!n acc. MAP f (foldi (\k v a. (k,v)::a) n acc pt) = 1496 foldi (\k v a. (f (k,v)::a)) n (MAP f acc) pt`, 1497 Induct_on `pt` >> simp[foldi_def]); 1498 1499val mapi_Alist = Q.store_thm( 1500 "mapi_Alist", 1501 `mapi f pt = 1502 fromAList (MAP (\kv. (FST kv,f (FST kv) (SND kv))) (toAList pt))`, 1503 simp[spt_eq_thm, wf_mapi, wf_fromAList, lookup_fromAList] >> 1504 srw_tac[boolSimps.ETA_ss][lookup_mapi, ALOOKUP_MAP_lemma, ALOOKUP_toAList]); 1505 1506val domain_mapi = Q.store_thm("domain_mapi", 1507 `domain (mapi f pt) = domain pt`, 1508 rw[pred_setTheory.EXTENSION,domain_lookup,lookup_mapi]); 1509 1510val size_domain = Q.store_thm("size_domain", 1511 `!t. size t = CARD (domain t)`, 1512 Induct_on `t` 1513 >- rw[size_def, domain_def] 1514 >- rw[size_def, domain_def] 1515 >> rw[pred_setTheory.CARD_UNION_EQN, pred_setTheory.CARD_INJ_IMAGE] 1516 >- 1517 (`IMAGE (\n. 2 * n + 2) (domain t) INTER 1518 IMAGE (\n. 2 * n + 1) (domain t') = {}` 1519 by (rw[GSYM pred_setTheory.DISJOINT_DEF, pred_setTheory.IN_DISJOINT] 1520 >> Cases_on `ODD x` 1521 >> fs[ODD_EXISTS, ADD1, oddevenlemma]) 1522 >> simp[]) >> 1523 `(({0} INTER IMAGE (\n. 2 * n + 2) (domain t)) = {}) /\ 1524 (({0} UNION (IMAGE (\n. 2 * n + 2) (domain t))) 1525 INTER (IMAGE (\n. 2 * n + 1) (domain t')) = {})` 1526 by (rw[GSYM pred_setTheory.DISJOINT_DEF, pred_setTheory.IN_DISJOINT] 1527 >> Cases_on `ODD x` 1528 >> fs[ODD_EXISTS, ADD1, oddevenlemma]) 1529 >> simp[]); 1530 1531val num_set_domain_eq = Q.store_thm("num_set_domain_eq", 1532 `!t1 t2:unit spt. 1533 wf t1 /\ wf t2 ==> 1534 ((domain t1 = domain t2) <=> (t1 = t2))`, 1535 rw[] >> EQ_TAC >> rw[spt_eq_thm] >> 1536 fs[pred_setTheory.EXTENSION, domain_lookup] >> 1537 pop_assum (qspec_then `n` mp_tac) >> strip_tac >> 1538 Cases_on `lookup n t1` >> fs[] >> Cases_on `lookup n t2` >> fs[]); 1539 1540val union_num_set_sym = Q.store_thm ("union_num_set_sym", 1541 `!(t1:unit spt) t2. union t1 t2 = union t2 t1`, 1542 Induct >> fs[union_def] >> rw[] >> CASE_TAC >> fs[union_def]); 1543 1544val difference_sub = Q.store_thm("difference_sub", 1545 `(difference a b = LN) ==> (domain a SUBSET domain b)`, 1546 rw[] >> 1547 `(domain (difference a b) = {})` by rw[domain_def] >> 1548 fs[pred_setTheory.EXTENSION, domain_difference, pred_setTheory.SUBSET_DEF] >> 1549 metis_tac[]); 1550 1551val wf_difference = Q.store_thm("wf_difference", 1552 `!t1 t2. wf t1 /\ wf t2 ==> wf (difference t1 t2)`, 1553 Induct >> rw[difference_def, wf_def] >> CASE_TAC >> fs[wf_def] 1554 >> rw[wf_def, wf_mk_BN, wf_mk_BS]); 1555 1556val delete_fail = Q.store_thm ("delete_fail", 1557 `!n t. wf t ==> (~(n IN domain t) <=> (delete n t = t))`, 1558 simp[domain_lookup] >> 1559 recInduct (fetch "-" "lookup_ind") >> 1560 rw[lookup_def, wf_def, delete_def, mk_BN_thm, mk_BS_thm]); 1561 1562val size_delete = Q.store_thm ( "size_delete", 1563 `!n t . size (delete n t) = 1564 if lookup n t = NONE then size t else size t - 1`, 1565 rw[size_def] >> fs[lookup_NONE_domain] >> 1566 TRY (qpat_assum `n NOTIN d` (qspecl_then [] mp_tac)) >> 1567 rfs[delete_fail, size_def] >> 1568 fs[size_domain,lookup_NONE_domain,size_domain]); 1569 1570val lookup_fromList_outside = Q.store_thm("lookup_fromList_outside", 1571 `!k. LENGTH args <= k ==> (lookup k (fromList args) = NONE)`, 1572 SIMP_TAC std_ss [lookup_fromList] \\ DECIDE_TAC); 1573 1574val lemmas = Q.prove( 1575 `(2 + 2 * n - 1 = 2 * n + 1:num) /\ 1576 ((2 + 2 * n' = 2 * n'' + 2) <=> (n' = n'':num)) /\ 1577 ((2 * m = 2 * n) <=> (m = n)) /\ 1578 ((2 * n'' + 1) DIV 2 = n'') /\ 1579 ((2 * n) DIV 2 = n) /\ 1580 (2 + 2 * n' <> 2 * n'' + 1) /\ 1581 (2 * m + 1 <> 2 * n' + 2)`, 1582 REPEAT STRIP_TAC \\ SIMP_TAC std_ss [] \\ fs [] 1583 \\ full_simp_tac(srw_ss())[ONCE_REWRITE_RULE [MULT_COMM] MULT_DIV] 1584 \\ full_simp_tac(srw_ss())[ONCE_REWRITE_RULE [MULT_COMM] DIV_MULT] 1585 \\ IMP_RES_TAC (METIS_PROVE [] ``(m = n) ==> (m MOD 2 = n MOD 2)``) 1586 \\ POP_ASSUM MP_TAC \\ SIMP_TAC std_ss [] 1587 \\ ONCE_REWRITE_TAC [MATCH_MP (GSYM MOD_PLUS) (DECIDE ``0 < 2:num``)] 1588 \\ EVAL_TAC \\ fs[MOD_EQ_0,ONCE_REWRITE_RULE [MULT_COMM] MOD_EQ_0]); 1589 1590val IN_domain = Q.store_thm("IN_domain", 1591 `!n x t1 t2. 1592 (n IN domain LN <=> F) /\ 1593 (n IN domain (LS x) <=> (n = 0)) /\ 1594 (n IN domain (BN t1 t2) <=> 1595 (n <> 0 /\ (if EVEN n then ((n-1) DIV 2) IN domain t1 1596 else ((n-1) DIV 2) IN domain t2))) /\ 1597 (n IN domain (BS t1 x t2) <=> 1598 ((n = 0) \/ (if EVEN n then ((n-1) DIV 2) IN domain t1 1599 else ((n-1) DIV 2) IN domain t2)))`, 1600 full_simp_tac(srw_ss())[domain_def] \\ REPEAT STRIP_TAC 1601 \\ Cases_on `n = 0` \\ full_simp_tac(srw_ss())[] 1602 \\ Cases_on `EVEN n` \\ full_simp_tac(srw_ss())[] 1603 \\ full_simp_tac(srw_ss())[GSYM ODD_EVEN] 1604 \\ IMP_RES_TAC EVEN_ODD_EXISTS 1605 \\ full_simp_tac(srw_ss())[ADD1] \\ full_simp_tac(srw_ss())[lemmas] 1606 \\ Cases_on `m` \\ full_simp_tac(srw_ss())[MULT_CLAUSES] 1607 \\ REPEAT STRIP_TAC \\ EQ_TAC \\ REPEAT STRIP_TAC 1608 \\ full_simp_tac(srw_ss())[lemmas]) 1609 1610val map_map_K = Q.store_thm("map_map_K", 1611 `!t. map (K a) (map f t) = map (K a) t`, 1612 Induct \\ full_simp_tac(srw_ss())[map_def]); 1613 1614val lookup_map_K = Q.store_thm("lookup_map_K", 1615 `!t n. lookup n (map (K x) t) = if n IN domain t then SOME x else NONE`, 1616 Induct \\ full_simp_tac(srw_ss())[IN_domain,map_def,lookup_def] 1617 \\ REPEAT STRIP_TAC \\ Cases_on `n = 0` \\ full_simp_tac(srw_ss())[] 1618 \\ Cases_on `EVEN n` \\ full_simp_tac(srw_ss())[]); 1619 1620val spt_fold_def = Define ` 1621 (spt_fold f acc LN = acc) /\ 1622 (spt_fold f acc (LS a) = f a acc) /\ 1623 (spt_fold f acc (BN t1 t2) = spt_fold f (spt_fold f acc t1) t2) /\ 1624 (spt_fold f acc (BS t1 a t2) = spt_fold f (f a (spt_fold f acc t1)) t2)` 1625 1626val IMP_size_LESS_size = store_thm("IMP_size_LESS_size", 1627 ``!x y. subspt x y /\ domain x <> domain y ==> size x < size y``, 1628 fs [size_domain,domain_difference] \\ rw [] 1629 \\ `?t. (domain y = domain x UNION t) /\ t <> EMPTY /\ 1630 (domain x INTER t = EMPTY)` by 1631 (qexists_tac `domain y DIFF domain x` 1632 \\ fs [pred_setTheory.EXTENSION] 1633 \\ qsuff_tac `domain x SUBSET domain y` 1634 THEN1 (fs [pred_setTheory.EXTENSION,pred_setTheory.SUBSET_DEF] \\ metis_tac []) 1635 \\ fs [domain_lookup,subspt_lookup,pred_setTheory.SUBSET_DEF] 1636 \\ rw [] \\ res_tac \\ fs []) 1637 \\ asm_rewrite_tac [] 1638 \\ `FINITE (domain y)` by fs [FINITE_domain] 1639 \\ `FINITE t` by metis_tac [pred_setTheory.FINITE_UNION] 1640 \\ fs [pred_setTheory.CARD_UNION_EQN] 1641 \\ `CARD t <> 0` by metis_tac [pred_setTheory.CARD_EQ_0] \\ fs []); 1642 1643val size_diff_less = store_thm("size_diff_less", 1644 ``!x y z t. 1645 domain z SUBSET domain y /\ t IN domain y /\ 1646 ~(t IN domain z) /\ t IN domain x ==> 1647 size (difference x y) < size (difference x z)``, 1648 rw [] 1649 \\ match_mp_tac IMP_size_LESS_size 1650 \\ fs [domain_difference,pred_setTheory.EXTENSION] 1651 \\ reverse conj_tac THEN1 metis_tac [] 1652 \\ fs [subspt_lookup,lookup_difference] 1653 \\ rw [] \\ fs [pred_setTheory.SUBSET_DEF,domain_lookup,PULL_EXISTS] 1654 \\ CCONTR_TAC 1655 \\ Cases_on `lookup x' z` \\ fs [] 1656 \\ res_tac \\ fs []); 1657 1658val inter_eq_LN = store_thm("inter_eq_LN", 1659 ``!x y. (inter x y = LN) <=> DISJOINT (domain x) (domain y)``, 1660 fs [spt_eq_thm,wf_inter,wf_def,lookup_def,lookup_inter_alt] 1661 \\ fs [domain_lookup,pred_setTheory.IN_DISJOINT] 1662 \\ metis_tac [optionTheory.NOT_SOME_NONE,optionTheory.SOME_11, 1663 optionTheory.option_CASES]); 1664 1665val _ = export_theory(); 1666