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