patriciaScript.sml
1(* ========================================================================= *)
2(* FILE : patriciaScript.sml *)
3(* DESCRIPTION : A Patricia tree implementation of finite maps: num |-> 'a *)
4(* AUTHOR : Anthony Fox, University of Cambridge *)
5(* DATE : 2008 *)
6(* ========================================================================= *)
7
8(* interactive use:
9 app load ["wordsLib", "bitSyntax", "sortingTheory", "pred_setSyntax"];
10*)
11Theory patricia
12Ancestors
13 arithmetic numeral bit numeral_bit list rich_list sorting
14Libs
15 Q
16
17
18val _ = ParseExtras.temp_loose_equality()
19val _ = diminish_srw_ss ["NORMEQ"]
20
21(* ------------------------------------------------------------------------- *)
22
23val _ = set_fixity "'" (Infixl 2000);
24val _ = set_fixity "|+" (Infixl 600);
25val _ = set_fixity "|++" (Infixl 500);
26val _ = set_fixity "\\\\" (Infixl 600);
27
28Datatype: ptree = Empty | Leaf num 'a | Branch num num ptree ptree
29End
30
31Definition BRANCHING_BIT_def[nocompute]:
32 BRANCHING_BIT p0 p1 =
33 if (ODD p0 = EVEN p1) \/ (p0 = p1) then 0
34 else SUC (BRANCHING_BIT (DIV2 p0) (DIV2 p1))
35Termination
36 WF_REL_TAC `measure (\(x,y). x + y)` \\ SRW_TAC [ARITH_ss] [DIV2_def]
37 \\ Cases_on `ODD p0` \\ FULL_SIMP_TAC bool_ss []
38 \\ FULL_SIMP_TAC bool_ss [GSYM ODD_EVEN, GSYM EVEN_ODD]
39 \\ IMP_RES_TAC EVEN_ODD_EXISTS
40 \\ SRW_TAC [ARITH_ss] [ADD1,
41 ONCE_REWRITE_RULE [MULT_COMM] (CONJ ADD_DIV_ADD_DIV MULT_DIV)]
42End
43
44Definition PEEK_def[nocompute]:
45 (PEEK Empty k = NONE) /\
46 (PEEK (Leaf j d) k = if k = j then SOME d else NONE) /\
47 (PEEK (Branch p m l r) k = PEEK (if BIT m k then l else r) k)
48End
49
50Overload "'" = Term`$PEEK`
51
52Definition JOIN_def[nocompute]:
53 JOIN (p0,t0,p1,t1) =
54 let m = BRANCHING_BIT p0 p1 in
55 if BIT m p0 then
56 Branch (MOD_2EXP m p0) m t0 t1
57 else
58 Branch (MOD_2EXP m p0) m t1 t0
59End
60
61Definition ADD_def[nocompute]:
62 (ADD Empty (k,e) = Leaf k e) /\
63 (ADD (Leaf j d) (k,e) = if j = k then Leaf k e
64 else JOIN (k, Leaf k e, j, Leaf j d)) /\
65 (ADD (Branch p m l r) (k,e) =
66 if MOD_2EXP_EQ m k p then
67 if BIT m k then
68 Branch p m (ADD l (k,e)) r
69 else
70 Branch p m l (ADD r (k,e))
71 else
72 JOIN (k, Leaf k e, p, Branch p m l r))
73End
74
75Overload "|+" = Term`$ADD`
76
77Definition BRANCH_def[nocompute]:
78 (BRANCH (p,m,Empty,t) = t) /\
79 (BRANCH (p,m,t,Empty) = t) /\
80 (BRANCH (p,m,t0,t1) = Branch p m t0 t1)
81End
82
83Definition REMOVE_def[nocompute]:
84 (REMOVE Empty k = Empty) /\
85 (REMOVE (Leaf j d) k = if j = k then Empty else Leaf j d) /\
86 (REMOVE (Branch p m l r) k =
87 if MOD_2EXP_EQ m k p then
88 if BIT m k then
89 BRANCH (p, m, REMOVE l k, r)
90 else
91 BRANCH (p, m, l, REMOVE r k)
92 else
93 Branch p m l r)
94End
95
96Overload "\\\\" = Term`$REMOVE`
97
98Definition TRAVERSE_AUX_def:
99 (TRAVERSE_AUX Empty a = a) /\
100 (TRAVERSE_AUX (Leaf k d) a = k::a) /\
101 (TRAVERSE_AUX (Branch p m l r) a = TRAVERSE_AUX l (TRAVERSE_AUX r a))
102End
103
104Definition TRAVERSE_def[nocompute]:
105 (TRAVERSE Empty = []) /\
106 (TRAVERSE (Leaf j d) = [j]) /\
107 (TRAVERSE (Branch p m l r) = TRAVERSE l ++ TRAVERSE r)
108End
109
110Definition KEYS_def:
111 KEYS t = QSORT $< (TRAVERSE t)
112End
113
114Definition TRANSFORM_def[nocompute]:
115 (TRANSFORM f Empty = Empty) /\
116 (TRANSFORM f (Leaf j d) = Leaf j (f d)) /\
117 (TRANSFORM f (Branch p m l r) = Branch p m (TRANSFORM f l) (TRANSFORM f r))
118End
119
120Definition EVERY_LEAF_def[nocompute]:
121 (EVERY_LEAF P Empty = T) /\
122 (EVERY_LEAF P (Leaf j d) = P j d) /\
123 (EVERY_LEAF P (Branch p m l r) = EVERY_LEAF P l /\ EVERY_LEAF P r)
124End
125
126Definition EXISTS_LEAF_def[nocompute]:
127 (EXISTS_LEAF P Empty = F) /\
128 (EXISTS_LEAF P (Leaf j d) = P j d) /\
129 (EXISTS_LEAF P (Branch p m l r) = EXISTS_LEAF P l \/ EXISTS_LEAF P r)
130End
131
132Definition SIZE_def[nocompute]: SIZE t = LENGTH (TRAVERSE t)
133End
134
135Definition DEPTH_def[nocompute]:
136 (DEPTH Empty = 0) /\
137 (DEPTH (Leaf j d) = 1) /\
138 (DEPTH (Branch p m l r) = 1 + MAX (DEPTH l) (DEPTH r))
139End
140
141Definition IS_PTREE_def[nocompute]:
142 (IS_PTREE Empty = T) /\
143 (IS_PTREE (Leaf k d) = T) /\
144 (IS_PTREE (Branch p m l r) =
145 p < 2 ** m /\ IS_PTREE l /\ IS_PTREE r /\
146 ~(l = Empty) /\ ~(r = Empty) /\
147 EVERY_LEAF (\k d. MOD_2EXP_EQ m k p /\ BIT m k) l /\
148 EVERY_LEAF (\k d. MOD_2EXP_EQ m k p /\ ~BIT m k) r)
149End
150
151(* ------------------------------------------------------------------------- *)
152
153val _ = hide "set";
154Overload LIST_TO_SET = ``list$LIST_TO_SET``
155
156val _ = set_fixity "IN_PTREE" (Infix (NONASSOC, 425));
157val _ = set_fixity "INSERT_PTREE" (Infixr 490);
158val _ = set_fixity "UNION_PTREE" (Infixl 500);
159
160Type ptreeset = ``:unit ptree``
161
162Definition IN_PTREE_def[nocompute]: $IN_PTREE n t = IS_SOME (PEEK (t:unit ptree) n)
163End
164Definition INSERT_PTREE_def[nocompute]: $INSERT_PTREE n t = ADD t (n,())
165End
166
167val _ = add_listform {leftdelim = [TOK "<{"], rightdelim = [TOK "}>"],
168 separator = [TOK ";", BreakSpace(1,0)],
169 cons = "INSERT_PTREE", nilstr = "Empty",
170 block_info = (PP.INCONSISTENT, 0)};
171
172Definition PTREE_OF_NUMSET_def[nocompute]:
173 PTREE_OF_NUMSET t (s:num set) =
174 FOLDL (combin$C $INSERT_PTREE) t (SET_TO_LIST s)
175End
176
177Overload "|++" = Term`$PTREE_OF_NUMSET`
178
179Definition NUMSET_OF_PTREE_def:
180 NUMSET_OF_PTREE (t:unit ptree) = LIST_TO_SET (TRAVERSE t)
181End
182
183Definition UNION_PTREE_def:
184 $UNION_PTREE t1 t2 = PTREE_OF_NUMSET t1 (NUMSET_OF_PTREE t2)
185End
186
187Definition IS_EMPTY_def: (IS_EMPTY Empty = T) /\ (IS_EMPTY _ = F)
188End
189
190Definition FIND_def: FIND t k = THE (PEEK t k)
191End
192
193Definition ADD_LIST_def: ADD_LIST = FOLDL ADD
194End
195
196Overload "|++" = Term`$ADD_LIST`
197
198(* ------------------------------------------------------------------------- *)
199
200Theorem lem[local]:
201 !n a b. n < BRANCHING_BIT a b ==> (BIT n a = BIT n b)
202Proof
203 Induct
204 \\ SRW_TAC [] [Once BRANCHING_BIT_def, bitTheory.BIT0_ODD, GSYM BIT_DIV2,
205 DIV2_def]
206 \\ SPOSE_NOT_THEN STRIP_ASSUME_TAC
207 \\ `ODD a = EVEN b` by METIS_TAC [EVEN_ODD]
208 \\ FULL_SIMP_TAC arith_ss [Once BRANCHING_BIT_def]
209QED
210
211Theorem MOD_2EXP_EQ_BRANCHING_BIT[local]:
212 !a b. MOD_2EXP_EQ (BRANCHING_BIT a b) a b
213Proof
214 NTAC 2 STRIP_TAC \\ Cases_on `BRANCHING_BIT a b`
215 \\ SRW_TAC [ARITH_ss] [GSYM BIT_BITS_THM, GSYM BITS_ZERO3,
216 MOD_2EXP_EQ_def, MOD_2EXP_def, lem]
217QED
218
219Theorem NOT_MOD_2EXP_EQ_IMP_BRANCHING_BIT_LT[local]:
220 !n a b. ~MOD_2EXP_EQ n a b ==> BRANCHING_BIT a b < n
221Proof
222 Cases \\ SRW_TAC [] [GSYM BIT_BITS_THM, MOD_2EXP_EQ_def, MOD_2EXP_def,
223 GSYM BITS_ZERO3]
224 \\ SPOSE_NOT_THEN (STRIP_ASSUME_TAC o REWRITE_RULE [NOT_LESS])
225 \\ `x < BRANCHING_BIT a b` by DECIDE_TAC
226 \\ IMP_RES_TAC lem
227QED
228
229Theorem MOD_2EXP_EQ_BIT_EQ[local]:
230 !n a b. MOD_2EXP_EQ n a b ==> (!x. x < n ==> (BIT x a = BIT x b))
231Proof
232 Cases \\ SRW_TAC [ARITH_ss]
233 [MOD_2EXP_EQ_def, MOD_2EXP_def, GSYM BIT_BITS_THM, GSYM BITS_ZERO3]
234QED
235
236Theorem MOD_2EXP_EQ_REFL[local]:
237 !n a. MOD_2EXP_EQ n a a
238Proof METIS_TAC [MOD_2EXP_EQ_def]
239QED
240
241Theorem MOD_2EXP_EQ_SYM[local]:
242 !n a b. MOD_2EXP_EQ n a b = MOD_2EXP_EQ n b a
243Proof
244 METIS_TAC [MOD_2EXP_EQ_def]
245QED
246
247Theorem MOD_2EXP_EQ_TRANS[local]:
248 !n a b c. MOD_2EXP_EQ n a b /\ MOD_2EXP_EQ n b c ==> MOD_2EXP_EQ n a c
249Proof
250 METIS_TAC [MOD_2EXP_EQ_def]
251QED
252
253Theorem NOT_MOD_2EXP_EQ[local]:
254 !n a b. ~MOD_2EXP_EQ n a b ==> ~(a = b)
255Proof
256 METIS_TAC [MOD_2EXP_EQ_def]
257QED
258
259Theorem MOD_2EXP_EQ_MOD_2EXP[local]:
260 (!n a b. MOD_2EXP_EQ n a (MOD_2EXP n b) = MOD_2EXP_EQ n a b) /\
261 (!n a b. MOD_2EXP_EQ n (MOD_2EXP n a) b = MOD_2EXP_EQ n a b)
262Proof
263 SRW_TAC [ARITH_ss] [MOD_2EXP_EQ_def, MOD_2EXP_def]
264QED
265
266Theorem MONO_MOD_2EXP_EQ[local]:
267 !m n a b. n <= m /\ MOD_2EXP_EQ m a b ==> MOD_2EXP_EQ n a b
268Proof
269 Cases \\ Cases \\ SRW_TAC [ARITH_ss] [MOD_2EXP_EQ_def, MOD_2EXP_def,
270 GSYM BIT_BITS_THM, GSYM BITS_ZERO3]
271QED
272
273Theorem lem[local]:
274 !a b. ~(a = b) /\ ~(ODD a = EVEN b) ==> ~(a DIV 2 = b DIV 2)
275Proof
276 SRW_TAC [] [METIS_PROVE [EVEN_MOD2,ODD_MOD2_LEM,NOT_MOD2_LEM2]
277 ``~(ODD a = EVEN b) = (a MOD 2 = b MOD 2)``]
278 \\ STRIP_TAC
279 \\ PAT_ASSUM `~(a = b)` MATCH_MP_TAC
280 \\ ONCE_REWRITE_TAC [(SIMP_RULE std_ss [] o SPEC `2`) DIVISION]
281 \\ SRW_TAC [] []
282QED
283
284Theorem BRANCHING_BIT:
285 !a b. ~(a = b) ==> ~(BIT (BRANCHING_BIT a b) a = BIT (BRANCHING_BIT a b) b)
286Proof
287 Induct_on `BRANCHING_BIT a b` \\ SRW_TAC [] []
288 >| [
289 PAT_ASSUM `0 = x` (fn th => let val sth = SYM th in
290 SUBST1_TAC sth THEN ASSUME_TAC sth end)
291 \\ Cases_on `ODD a = EVEN b`
292 \\ FULL_SIMP_TAC arith_ss [EVEN_ODD, Once BRANCHING_BIT_def,
293 bitTheory.BIT0_ODD]
294 \\ METIS_TAC [],
295 ONCE_REWRITE_TAC [BRANCHING_BIT_def]
296 \\ SRW_TAC [] [GSYM BIT_DIV2, DIV2_def, bitTheory.BIT0_ODD]
297 >- METIS_TAC [EVEN_ODD]
298 \\ PAT_ASSUM `!a b. P` (SPECL_THEN [`a DIV 2`,`b DIV 2`] ASSUME_TAC)
299 \\ IMP_RES_TAC lem
300 \\ FULL_SIMP_TAC std_ss [lem]
301 \\ POP_ASSUM (K ALL_TAC) \\ POP_ASSUM MATCH_MP_TAC
302 \\ RULE_ASSUM_TAC (REWRITE_RULE [Once BRANCHING_BIT_def])
303 \\ FULL_SIMP_TAC std_ss [DIV2_def]]
304QED
305
306Theorem BRANCHING_BIT_ZERO:
307 !a b. (BRANCHING_BIT a b = 0) = (ODD a = EVEN b) \/ (a = b)
308Proof
309 SRW_TAC [ARITH_ss] [Once BRANCHING_BIT_def]
310QED
311
312Theorem BRANCHING_BIT_SYM:
313 !a b. BRANCHING_BIT a b = BRANCHING_BIT b a
314Proof
315 Induct_on ‘BRANCHING_BIT a b’ \\ SRW_TAC [] []
316 >- METIS_TAC [BRANCHING_BIT_ZERO,
317 ONCE_REWRITE_RULE [METIS_PROVE [ODD_EVEN]
318 “(ODD a = EVEN b) = (ODD b = EVEN a)”]
319 BRANCHING_BIT_ZERO]
320 \\ ONCE_REWRITE_TAC [BRANCHING_BIT_def]
321 \\ SRW_TAC [] [GSYM BIT_DIV2, DIV2_def] >| [
322 METIS_TAC [EVEN_ODD], METIS_TAC [EVEN_ODD],
323 qpat_x_assum ‘SUC _ = BRANCHING_BIT _ _’
324 (mp_tac o REWRITE_RULE [Once BRANCHING_BIT_def])
325 \\ FULL_SIMP_TAC (srw_ss()) []
326 \\ METIS_TAC [DIV2_def]
327 ]
328QED
329
330Theorem EVERY_LEAF_ADD:
331 !P t k d. P k d /\ EVERY_LEAF P t ==> EVERY_LEAF P (ADD t (k,d))
332Proof
333 Induct_on `t`
334 \\ SRW_TAC [boolSimps.LET_ss] [ADD_def, EVERY_LEAF_def, JOIN_def]
335QED
336
337Theorem MONO_EVERY_LEAF:
338 !P Q t. (!k d. P k d ==> Q k d) /\ EVERY_LEAF P t ==> EVERY_LEAF Q t
339Proof
340 Induct_on `t` \\ SRW_TAC [] [EVERY_LEAF_def] \\ METIS_TAC []
341QED
342
343Theorem NOT_ADD_EMPTY:
344 !t k d. ~(ADD t (k,d) = Empty)
345Proof
346 Cases \\ SRW_TAC [] [ADD_def, JOIN_def] \\ SRW_TAC [] []
347QED
348
349val MOD_2EXP_LT_COR =
350 METIS_PROVE [MOD_2EXP_LT, MOD_2EXP_def] ``MOD_2EXP x n < 2 ** x``;
351
352Theorem EMPTY_IS_PTREE[simp] =
353 EQT_ELIM (CONJUNCT1 IS_PTREE_def);
354
355Theorem ADD_IS_PTREE[simp]:
356 !t x. IS_PTREE t ==> IS_PTREE (ADD t x)
357Proof
358 Cases_on `x` \\ Induct
359 \\ SRW_TAC [boolSimps.LET_ss]
360 [MOD_2EXP_EQ_MOD_2EXP, MOD_2EXP_EQ_REFL, EVERY_LEAF_ADD,
361 IS_PTREE_def, ADD_def, JOIN_def, EVERY_LEAF_def]
362 \\ TRY (METIS_TAC [MOD_2EXP_EQ_SYM, MOD_2EXP_EQ_BRANCHING_BIT,
363 BRANCHING_BIT, NOT_ADD_EMPTY, MOD_2EXP_LT_COR])
364 >| [
365 SPEC_THEN `\k d. MOD_2EXP_EQ n k n0 /\ BIT n k`
366 MATCH_MP_TAC MONO_EVERY_LEAF
367 \\ `~BIT (BRANCHING_BIT q n0) n0`
368 by METIS_TAC [NOT_MOD_2EXP_EQ, BRANCHING_BIT],
369 SPEC_THEN `\k d. MOD_2EXP_EQ n k n0 /\ ~BIT n k`
370 MATCH_MP_TAC MONO_EVERY_LEAF
371 \\ `~BIT (BRANCHING_BIT q n0) n0`
372 by METIS_TAC [NOT_MOD_2EXP_EQ, BRANCHING_BIT],
373 SPEC_THEN `\k d. MOD_2EXP_EQ n k n0 /\ BIT n k`
374 MATCH_MP_TAC MONO_EVERY_LEAF
375 \\ `BIT (BRANCHING_BIT q n0) n0`
376 by METIS_TAC [NOT_MOD_2EXP_EQ, BRANCHING_BIT],
377 SPEC_THEN `\k d. MOD_2EXP_EQ n k n0 /\ ~BIT n k`
378 MATCH_MP_TAC MONO_EVERY_LEAF
379 \\ `BIT (BRANCHING_BIT q n0) n0`
380 by METIS_TAC [NOT_MOD_2EXP_EQ, BRANCHING_BIT]]
381 \\ SRW_TAC [] []
382 \\ IMP_RES_TAC NOT_MOD_2EXP_EQ_IMP_BRANCHING_BIT_LT
383 \\ `MOD_2EXP_EQ (BRANCHING_BIT q n0) n0 q`
384 by METIS_TAC [MOD_2EXP_EQ_BRANCHING_BIT, MOD_2EXP_EQ_SYM]
385 \\ METIS_TAC [MONO_MOD_2EXP_EQ, DECIDE ``a < b ==> a <= b:num``,
386 MOD_2EXP_EQ_SYM, MOD_2EXP_EQ_TRANS, MOD_2EXP_EQ_BIT_EQ]
387QED
388
389Theorem EVERY_LEAF_BRANCH:
390 !P p m l r. EVERY_LEAF P (BRANCH (p, m, l, r)) =
391 EVERY_LEAF P l /\ EVERY_LEAF P r
392Proof
393 Cases_on `l` \\ Cases_on `r` \\ SRW_TAC [] [BRANCH_def, EVERY_LEAF_def]
394QED
395
396Theorem EVERY_LEAF_REMOVE:
397 !P t k. EVERY_LEAF P t ==> EVERY_LEAF P (REMOVE t k)
398Proof
399 Induct_on `t` \\ SRW_TAC [] [REMOVE_def, EVERY_LEAF_def, EVERY_LEAF_BRANCH]
400QED
401
402Theorem IS_PTREE_BRANCH:
403 !p m l r. p < 2 ** m /\ ~((l = Empty) /\ (r = Empty)) /\
404 EVERY_LEAF (\k d. MOD_2EXP_EQ m k p /\ BIT m k) l /\
405 EVERY_LEAF (\k d. MOD_2EXP_EQ m k p /\ ~BIT m k) r /\
406 IS_PTREE l /\ IS_PTREE r ==>
407 IS_PTREE (BRANCH (p, m, l, r))
408Proof
409 Cases_on `l` \\ Cases_on `r`
410 \\ SRW_TAC [] [BRANCH_def, IS_PTREE_def, EVERY_LEAF_def]
411QED
412
413Theorem REMOVE_IS_PTREE[simp]:
414 !t k. IS_PTREE t ==> IS_PTREE (REMOVE t k)
415Proof
416 Induct \\ SRW_TAC [] [REMOVE_def, IS_PTREE_def]
417 \\ METIS_TAC [IS_PTREE_BRANCH, EVERY_LEAF_REMOVE]
418QED
419
420
421Theorem PEEK_NONE:
422 !P t k. (!d. ~P k d) /\ EVERY_LEAF P t ==> (PEEK t k = NONE)
423Proof
424 Induct_on `t` \\ SRW_TAC [] [EVERY_LEAF_def, PEEK_def] \\ METIS_TAC []
425QED
426
427val PEEK_NONE_LEFT = SPEC `\k d. MOD_2EXP_EQ n k n0 /\ BIT n k` PEEK_NONE;
428val PEEK_NONE_RIGHT = SPEC `\k d. MOD_2EXP_EQ n k n0 /\ ~BIT n k` PEEK_NONE;
429
430Theorem PEEK_ADD:
431 !t k d j. IS_PTREE t ==>
432 (PEEK (ADD t (k,d)) j = if k = j then SOME d else PEEK t j)
433Proof
434 Induct_on `t`
435 \\ SRW_TAC [boolSimps.LET_ss] [ADD_def, PEEK_def, JOIN_def, IS_PTREE_def]
436 \\ SRW_TAC [] [PEEK_def]
437 \\ METIS_TAC [NOT_MOD_2EXP_EQ_IMP_BRANCHING_BIT_LT, BRANCHING_BIT,
438 MOD_2EXP_EQ_BIT_EQ, NOT_MOD_2EXP_EQ, PEEK_NONE_LEFT, PEEK_NONE_RIGHT]
439QED
440
441Theorem BRANCH:
442 !p m l r. BRANCH (p,m,l,r) =
443 if l = Empty then r
444 else if r = Empty then l
445 else Branch p m l r
446Proof
447 Cases_on `l` \\ Cases_on `r` \\ SRW_TAC [] [BRANCH_def]
448QED
449
450Theorem PEEK_REMOVE:
451 !t k j. IS_PTREE t ==>
452 (PEEK (REMOVE t k) j = if k = j then NONE else PEEK t j)
453Proof
454 Induct_on `t`
455 \\ SRW_TAC [boolSimps.LET_ss]
456 [PEEK_def, REMOVE_def, IS_PTREE_def, IS_PTREE_BRANCH, BRANCH_def]
457 \\ SRW_TAC [] [BRANCH, PEEK_def]
458 \\ METIS_TAC [PEEK_NONE_LEFT, PEEK_NONE_RIGHT, PEEK_def]
459QED
460
461Theorem EVERY_LEAF_TRANSFORM:
462 !P Q f t. (!k d. P k d ==> Q k (f d)) /\ EVERY_LEAF P t ==>
463 EVERY_LEAF Q (TRANSFORM f t)
464Proof
465 Induct_on `t` \\ SRW_TAC [] [TRANSFORM_def, EVERY_LEAF_def] \\ METIS_TAC []
466QED
467
468val EVERY_LEAF_TRANSFORM_LEFT = (SIMP_RULE (srw_ss()) [] o
469 SPECL [`\k d. MOD_2EXP_EQ n k n0 /\ BIT n k`,
470 `\k d. MOD_2EXP_EQ n k n0 /\ BIT n k`]) EVERY_LEAF_TRANSFORM;
471
472val EVERY_LEAF_TRANSFORM_RIGHT = (SIMP_RULE (srw_ss()) [] o
473 SPECL [`\k d. MOD_2EXP_EQ n k n0 /\ ~BIT n k`,
474 `\k d. MOD_2EXP_EQ n k n0 /\ ~BIT n k`]) EVERY_LEAF_TRANSFORM;
475
476Theorem TRANSFORM_EMPTY:
477 !f t. (TRANSFORM f t = Empty) = (t = Empty)
478Proof
479 Cases_on `t` \\ SRW_TAC [] [TRANSFORM_def]
480QED
481
482Theorem TRANSFORM_IS_PTREE[simp]:
483 !f t. IS_PTREE t ==> IS_PTREE (TRANSFORM f t)
484Proof
485 Induct_on `t` \\ SRW_TAC [] [TRANSFORM_def, IS_PTREE_def, TRANSFORM_EMPTY]
486 \\ METIS_TAC [EVERY_LEAF_TRANSFORM_LEFT, EVERY_LEAF_TRANSFORM_RIGHT]
487QED
488
489
490Theorem PEEK_TRANSFORM:
491 !f t k. PEEK (TRANSFORM f t) k =
492 case PEEK t k of
493 NONE => NONE
494 | SOME x => SOME (f x)
495Proof
496 Induct_on `t` \\ SRW_TAC [] [TRANSFORM_def, PEEK_def]
497QED
498
499Theorem ADD_TRANSFORM:
500 !f t k d. TRANSFORM f (ADD t (k,d)) = ADD (TRANSFORM f t) (k,f d)
501Proof
502 Induct_on `t` \\ SRW_TAC [] [TRANSFORM_def, ADD_def, JOIN_def]
503 \\ SRW_TAC [] [TRANSFORM_def]
504QED
505
506Theorem TRANSFORM_BRANCH:
507 !f p m l r. TRANSFORM f (BRANCH (p,m,l,r)) =
508 BRANCH (p,m,TRANSFORM f l, TRANSFORM f r)
509Proof
510 Cases_on `l` \\ Cases_on `r` \\ SRW_TAC [] [BRANCH_def, TRANSFORM_def]
511QED
512
513Theorem REMOVE_TRANSFORM:
514 !f t k. TRANSFORM f (REMOVE t k) = REMOVE (TRANSFORM f t) k
515Proof
516 Induct_on `t` \\ SRW_TAC [] [TRANSFORM_def, REMOVE_def, TRANSFORM_BRANCH]
517QED
518
519Theorem REMOVE_ADD_EQ[simp]:
520 !t k d. REMOVE (ADD t (k,d)) k = REMOVE t k
521Proof
522 Induct
523 \\ SRW_TAC [boolSimps.LET_ss]
524 [MOD_2EXP_EQ_BRANCHING_BIT, MOD_2EXP_EQ_MOD_2EXP, MOD_2EXP_EQ_REFL,
525 REMOVE_def, ADD_def, JOIN_def, BRANCH_def]
526QED
527
528Theorem ADD_ADD[simp]:
529 !t k d e. ADD (ADD t (k,d)) (k,e) = ADD t (k,e)
530Proof
531 Induct \\ SRW_TAC [boolSimps.LET_ss]
532 [MOD_2EXP_EQ_MOD_2EXP, MOD_2EXP_EQ_REFL, ADD_def, JOIN_def]
533QED
534
535Theorem EVERY_LEAF_PEEK:
536 !P t k. EVERY_LEAF P t /\ IS_SOME (PEEK t k) ==> P k (THE (PEEK t k))
537Proof
538 Induct_on `t` \\ SRW_TAC [] [PEEK_def, EVERY_LEAF_def]
539QED
540
541val EVERY_LEAF_PEEK_LEFT = (SIMP_RULE (srw_ss()) [] o
542 SPEC `\k d. MOD_2EXP_EQ n k n0 /\ BIT n k`) EVERY_LEAF_PEEK;
543
544val EVERY_LEAF_PEEK_RIGHT = (SIMP_RULE (srw_ss()) [] o
545 SPEC `\k d. MOD_2EXP_EQ n k n0 /\ ~BIT n k`) EVERY_LEAF_PEEK;
546
547val PEEK_NONE_LEFT = SPEC `\k d. MOD_2EXP_EQ m k p /\ BIT m k` PEEK_NONE;
548val PEEK_NONE_RIGHT = SPEC `\k d. MOD_2EXP_EQ m k p /\ ~BIT m k` PEEK_NONE;
549
550Theorem IS_PTREE_PEEK:
551 (!k. ~IS_SOME (PEEK Empty k)) /\
552 (!k j b. IS_SOME (PEEK (Leaf j b) k) = (j = k)) /\
553 (!p m l r.
554 IS_PTREE (Branch p m l r) ==>
555 (?k. BIT m k /\ IS_SOME (PEEK l k)) /\
556 (?k. ~BIT m k /\ IS_SOME (PEEK r k)) /\
557 (!k n. ~MOD_2EXP_EQ m k p \/ n < m /\ ~(BIT n p = BIT n k) ==>
558 ~IS_SOME (PEEK l k) /\ ~IS_SOME (PEEK r k)))
559Proof
560 SRW_TAC [] [PEEK_def]
561 >| [
562 Induct_on `l` \\ SRW_TAC [] [IS_PTREE_def, PEEK_def]
563 >- (EXISTS_TAC `n` \\ FULL_SIMP_TAC (srw_ss()) [EVERY_LEAF_def])
564 \\ `IS_PTREE (Branch p m l r) /\ IS_PTREE (Branch p m l' r)`
565 by FULL_SIMP_TAC (srw_ss()) [IS_PTREE_def, EVERY_LEAF_def]
566 \\ METIS_TAC [EVERY_LEAF_PEEK_LEFT, EVERY_LEAF_PEEK_RIGHT],
567 Induct_on `r` \\ SRW_TAC [] [IS_PTREE_def, PEEK_def]
568 >- (EXISTS_TAC `n` \\ FULL_SIMP_TAC (srw_ss()) [EVERY_LEAF_def])
569 \\ `IS_PTREE (Branch p m l r) /\ IS_PTREE (Branch p m l r')`
570 by FULL_SIMP_TAC (srw_ss()) [IS_PTREE_def, EVERY_LEAF_def]
571 \\ METIS_TAC [EVERY_LEAF_PEEK_LEFT, EVERY_LEAF_PEEK_RIGHT],
572 FULL_SIMP_TAC (srw_ss()) [IS_PTREE_def]
573 \\ METIS_TAC [PEEK_NONE_LEFT, PEEK_NONE_RIGHT],
574 FULL_SIMP_TAC (srw_ss()) [IS_PTREE_def]
575 \\ METIS_TAC [PEEK_NONE_LEFT, PEEK_NONE_RIGHT],
576 FULL_SIMP_TAC (srw_ss()) [IS_PTREE_def]
577 \\ METIS_TAC [MOD_2EXP_EQ_BIT_EQ, PEEK_NONE_LEFT, PEEK_NONE_RIGHT],
578 FULL_SIMP_TAC (srw_ss()) [IS_PTREE_def]
579 \\ METIS_TAC [MOD_2EXP_EQ_BIT_EQ, PEEK_NONE_LEFT, PEEK_NONE_RIGHT]]
580QED
581
582val IS_NONE_SOME =
583 METIS_PROVE [optionTheory.IS_NONE_EQ_NONE, optionTheory.NOT_IS_SOME_EQ_NONE]
584 ``~IS_NONE x = IS_SOME x``;
585
586Theorem OPTION_EQ[local]:
587 !a b. (a = b) = (~IS_SOME a /\ ~IS_SOME b) \/
588 (IS_SOME a /\ IS_SOME b) /\ (THE a = THE b)
589Proof
590 Cases \\ Cases \\ SRW_TAC [] []
591QED
592
593Theorem LT_MOD_2EXP_EQ[local]:
594 !n a b. a < 2 ** n /\ b < 2 ** n /\ MOD_2EXP_EQ n a b ==> (a = b)
595Proof
596 SIMP_TAC (arith_ss++boolSimps.CONJ_ss)
597 [MOD_2EXP_EQ_def, MOD_2EXP_def, ZERO_LT_TWOEXP]
598QED
599
600val PEEK_NONE_LEFT = SPEC `\k d. MOD_2EXP_EQ n' k n0' /\ BIT n' k` PEEK_NONE;
601val PEEK_NONE_RIGHT = SPEC `\k d. MOD_2EXP_EQ n' k n0' /\ ~BIT n' k` PEEK_NONE;
602
603Theorem PTREE_EQ:
604 !t1 t2. IS_PTREE t1 /\ IS_PTREE t2 ==>
605 ((!k. PEEK t1 k = PEEK t2 k) = (t1 = t2))
606Proof
607 Induct \\ Induct_on `t2`
608 \\ SIMP_TAC (srw_ss()) []
609 \\ ONCE_REWRITE_TAC [OPTION_EQ]
610 \\ SIMP_TAC bool_ss [IS_PTREE_PEEK, IS_NONE_SOME]
611 \\ RW_TAC bool_ss [PEEK_def]
612 >| [
613 METIS_TAC [IS_PTREE_PEEK],
614 METIS_TAC [IS_PTREE_PEEK, optionTheory.THE_DEF],
615 METIS_TAC [IS_PTREE_PEEK], METIS_TAC [IS_PTREE_PEEK],
616 METIS_TAC [IS_PTREE_PEEK],
617 Tactical.REVERSE EQ_TAC >- METIS_TAC []
618 \\ STRIP_TAC
619 \\ IMP_RES_TAC IS_PTREE_PEEK
620 \\ NTAC 4 (POP_ASSUM (K ALL_TAC))
621 \\ `~(n < n')` by (Cases_on `~(BIT n n0' = BIT n k')` \\ METIS_TAC [])
622 \\ `~(n' < n)` by (Cases_on `~(BIT n' n0 = BIT n' k')` \\ PROVE_TAC [])
623 \\ `n = n'` by DECIDE_TAC
624 \\ `n0 < 2 ** n /\ n0' < 2 ** n`
625 by FULL_SIMP_TAC (srw_ss()) [IS_PTREE_def]
626 \\ `n0 = n0'`
627 by METIS_TAC [LT_MOD_2EXP_EQ, MOD_2EXP_EQ_TRANS, MOD_2EXP_EQ_SYM]
628 \\ `(t1 = t2) = (!k. PEEK t1 k = PEEK t2 k)`
629 by METIS_TAC [IS_PTREE_def]
630 \\ `(t1' = t2') = (!k. PEEK t1' k = PEEK t2' k)`
631 by METIS_TAC [IS_PTREE_def]
632 \\ FULL_SIMP_TAC bool_ss [GSYM OPTION_EQ]
633 \\ CONJ_TAC \\ STRIP_TAC
634 >| [Cases_on `BIT n' k''''` >- METIS_TAC [],
635 Tactical.REVERSE (Cases_on `BIT n' k''''`) >- METIS_TAC []]
636 \\ FULL_SIMP_TAC (srw_ss()) [IS_PTREE_def]
637 \\ METIS_TAC [PEEK_NONE_LEFT, PEEK_NONE_RIGHT]]
638QED
639
640Theorem REMOVE_REMOVE[simp]:
641 !t k. IS_PTREE t ==> (REMOVE (REMOVE t k) k = REMOVE t k)
642Proof
643 SRW_TAC [] [GSYM PTREE_EQ, PEEK_REMOVE]
644QED
645
646
647Theorem REMOVE_ADD:
648 !t k d j. IS_PTREE t ==>
649 (REMOVE (ADD t (k,d)) j =
650 if k = j then REMOVE t j else ADD (REMOVE t j) (k,d))
651Proof
652 SRW_TAC [] [GSYM PTREE_EQ, PEEK_REMOVE, PEEK_ADD]
653 \\ SRW_TAC [] []
654QED
655
656Theorem ADD_ADD_SYM:
657 !t k j d e. IS_PTREE t /\ ~(k = j) ==>
658 (ADD (ADD t (k,d)) (j,e) = ADD (ADD t (j,e)) (k,d))
659Proof
660 SRW_TAC [] [GSYM PTREE_EQ, PEEK_ADD] \\ SRW_TAC [] []
661QED
662
663(* ------------------------------------------------------------------------- *)
664
665Theorem FILTER_ALL:
666 !P l. (!n. n < LENGTH l ==> ~P (EL n l)) = (FILTER P l = [])
667Proof
668 Induct_on `l` \\ SRW_TAC [] []
669 >- (EXISTS_TAC `0` \\ SRW_TAC [] [])
670 \\ PAT_ASSUM `!P. x` (SPEC_THEN `P` (SUBST1_TAC o SYM))
671 \\ EQ_TAC \\ SRW_TAC [] []
672 >- METIS_TAC [LESS_MONO_EQ, EL, TL]
673 \\ Cases_on `n` >- SRW_TAC [] []
674 \\ METIS_TAC [LESS_MONO_EQ, EL, TL]
675QED
676
677Theorem TRAVERSE_TRANSFORM:
678 !f t. TRAVERSE (TRANSFORM f t) = TRAVERSE t
679Proof
680 Induct_on `t` \\ SRW_TAC [] [TRAVERSE_def, TRANSFORM_def]
681QED
682
683Theorem MEM_TRAVERSE_PEEK:
684 !t k. IS_PTREE t ==> (MEM k (TRAVERSE t) = IS_SOME (PEEK t k))
685Proof
686 Induct \\ SRW_TAC [] [TRAVERSE_def, PEEK_def, IS_PTREE_def]
687 \\ METIS_TAC [optionTheory.NOT_IS_SOME_EQ_NONE,
688 PEEK_NONE_LEFT, PEEK_NONE_RIGHT]
689QED
690
691Theorem IN_NUMSET_OF_PTREE:
692 !t n. IS_PTREE t ==> (n IN NUMSET_OF_PTREE t = n IN_PTREE t)
693Proof
694 SRW_TAC [] [NUMSET_OF_PTREE_def, IN_PTREE_def, MEM_TRAVERSE_PEEK]
695QED
696
697Theorem FOLD_INDUCT[local]:
698 !P f e l. P e /\ (!x y. P x ==> P (f x y)) ==> P (FOLDL f e l)
699Proof
700 Induct_on `l` \\ SRW_TAC [] []
701QED
702
703Theorem ADD_LIST_IS_PTREE[simp]:
704 !t l. IS_PTREE t ==> IS_PTREE (ADD_LIST t l)
705Proof
706 SRW_TAC [] [ADD_LIST_def]
707 \\ MATCH_MP_TAC FOLD_INDUCT
708 \\ SRW_TAC [] []
709 \\ Cases_on `y`
710 \\ SRW_TAC [] []
711QED
712
713Theorem ADD_LIST_TO_EMPTY_IS_PTREE:
714 !l. IS_PTREE (ADD_LIST Empty l)
715Proof
716 METIS_TAC [ADD_LIST_IS_PTREE, EMPTY_IS_PTREE]
717QED
718
719Theorem PTREE_OF_NUMSET_IS_PTREE[simp]:
720 !t s. IS_PTREE t ==> IS_PTREE (PTREE_OF_NUMSET t s)
721Proof
722 SRW_TAC [] [PTREE_OF_NUMSET_def]
723 \\ MATCH_MP_TAC FOLD_INDUCT
724 \\ SRW_TAC [] [INSERT_PTREE_def]
725QED
726
727Theorem PTREE_OF_NUMSET_IS_PTREE_EMPTY[simp] =
728 (SIMP_RULE (srw_ss()) [] o SPEC `Empty`) PTREE_OF_NUMSET_IS_PTREE;
729
730
731val EVERY_LEAF_PEEK_LEFT = (SIMP_RULE (srw_ss()) [] o
732 SPEC `\k d. MOD_2EXP_EQ m k p /\ BIT m k`) EVERY_LEAF_PEEK;
733
734val EVERY_LEAF_PEEK_RIGHT = (SIMP_RULE (srw_ss()) [] o
735 SPEC `\k d. MOD_2EXP_EQ m k p /\ ~BIT m k`) EVERY_LEAF_PEEK;
736
737Theorem NOT_KEY_LEFT_AND_RIGHT:
738 !p m l r k j.
739 IS_PTREE (Branch p m l r) /\
740 IS_SOME (PEEK l k) /\ IS_SOME (PEEK r j) ==> ~(k = j)
741Proof
742 SRW_TAC [] [IS_PTREE_def]
743 \\ METIS_TAC [EVERY_LEAF_PEEK_LEFT, EVERY_LEAF_PEEK_RIGHT]
744QED
745
746Theorem ALL_DISTINCT_TRAVERSE[simp]:
747 !t. IS_PTREE t ==> ALL_DISTINCT (TRAVERSE t)
748Proof
749 Induct \\ SRW_TAC [] [ALL_DISTINCT, TRAVERSE_def, ALL_DISTINCT_APPEND]
750 \\ `IS_PTREE t /\ IS_PTREE t'` by FULL_SIMP_TAC (srw_ss()) [IS_PTREE_def]
751 \\ METIS_TAC [MEM_TRAVERSE_PEEK, NOT_KEY_LEFT_AND_RIGHT]
752QED
753
754
755Theorem MEM_ALL_DISTINCT_IMP_PERM:
756 !l1 l2. ALL_DISTINCT l1 /\ ALL_DISTINCT l2 /\ (!x. MEM x l1 = MEM x l2) ==>
757 PERM l1 l2
758Proof
759 SRW_TAC [] [PERM_DEF, ALL_DISTINCT_FILTER]
760 \\ MATCH_MP_TAC listTheory.LIST_EQ
761 \\ Cases_on `MEM x l1` >- METIS_TAC []
762 \\ SPEC_THEN `$= x` ASSUME_TAC FILTER_ALL
763 \\ METIS_TAC [MEM_EL]
764QED
765
766Theorem MEM_TRAVERSE:
767 !t k. IS_PTREE t ==> (MEM k (TRAVERSE t) = k IN (NUMSET_OF_PTREE t))
768Proof
769 SRW_TAC [] [IN_NUMSET_OF_PTREE, IN_PTREE_def, MEM_TRAVERSE_PEEK]
770QED
771
772Theorem INSERT_PTREE_IS_PTREE[simp]:
773 !t x. IS_PTREE t ==> IS_PTREE (x INSERT_PTREE t)
774Proof
775 SRW_TAC [] [INSERT_PTREE_def]
776QED
777
778Theorem FINITE_NUMSET_OF_PTREE[simp]:
779 !t. FINITE (NUMSET_OF_PTREE t)
780Proof
781 SRW_TAC [] [NUMSET_OF_PTREE_def, FINITE_LIST_TO_SET]
782QED
783
784Theorem ADD_INSERT[simp] =
785 (GEN_ALL o SIMP_CONV (srw_ss()) [GSYM INSERT_PTREE_def, oneTheory.one])
786 ``ADD t (n,v:unit)``;
787
788
789Theorem IS_PTREE_FOLDR_INSERT_PTREE[local]:
790 !l t. IS_PTREE t ==> IS_PTREE (FOLDR (\x y. x INSERT_PTREE y) t l)
791Proof
792 Induct_on `l` \\ SRW_TAC [] []
793QED
794
795Theorem PEEK_INSERT_PTREE =
796 (GEN_ALL o SPEC_ALL o ONCE_REWRITE_RULE [oneTheory.one] o
797 REWRITE_RULE [ADD_INSERT] o ISPEC `t:ptreeset`) PEEK_ADD;
798
799Theorem MEM_TRAVERSE_INSERT_PTREE:
800 !t x h. IS_PTREE t ==>
801 (MEM x (TRAVERSE (h INSERT_PTREE t)) =
802 (x = h) \/ ~(x = h) /\ MEM x (TRAVERSE t))
803Proof
804 SRW_TAC [] [MEM_TRAVERSE_PEEK, PEEK_INSERT_PTREE]
805QED
806
807Theorem MEM_TRAVERSE_FOLDR[local]:
808 !l t x. IS_PTREE t ==>
809 (MEM x (TRAVERSE (FOLDR (\x y. x INSERT_PTREE y) (h INSERT_PTREE t) l)) =
810 (x = h) \/
811 ~(x = h) /\ MEM x (TRAVERSE (FOLDR (\x y. x INSERT_PTREE y) t l)))
812Proof
813 Induct
814 \\ SRW_TAC [] [IS_PTREE_FOLDR_INSERT_PTREE, MEM_TRAVERSE_INSERT_PTREE]
815 \\ METIS_TAC []
816QED
817
818Theorem PERM_INSERT_PTREE[local]:
819 !t l. IS_PTREE t /\ ALL_DISTINCT l ==>
820 (PERM (TRAVERSE (FOLDL (combin$C $INSERT_PTREE) t l))
821 (SET_TO_LIST (NUMSET_OF_PTREE t UNION LIST_TO_SET l)))
822Proof
823 REWRITE_TAC [FOLDL_FOLDR_REVERSE]
824 \\ Induct_on `l`
825 \\ SRW_TAC [] [TRAVERSE_def, FOLDR_APPEND, NUMSET_OF_PTREE_def]
826 \\ MATCH_MP_TAC MEM_ALL_DISTINCT_IMP_PERM
827 \\ SRW_TAC [] [MEM_SET_TO_LIST, FINITE_LIST_TO_SET, MEM_TRAVERSE_FOLDR,
828 IS_PTREE_FOLDR_INSERT_PTREE]
829 \\ RES_TAC \\ IMP_RES_TAC PERM_MEM_EQ \\ NTAC 2 (POP_ASSUM (K ALL_TAC))
830 \\ FULL_SIMP_TAC (srw_ss()) [MEM_SET_TO_LIST, MEM_TRAVERSE]
831 \\ METIS_TAC []
832QED
833
834Theorem PERM_INSERT_PTREE =
835 (GEN_ALL o SIMP_RULE (srw_ss()) [SET_TO_LIST_INV] o
836 DISCH `FINITE s` o SPECL [`t`, `SET_TO_LIST s`]) PERM_INSERT_PTREE;
837
838Theorem IN_PTREE_OF_NUMSET:
839 !t s n. IS_PTREE t /\ FINITE s ==>
840 (n IN_PTREE (PTREE_OF_NUMSET t s) = n IN_PTREE t \/ n IN s)
841Proof
842 SRW_TAC [] [IN_PTREE_def, GSYM MEM_TRAVERSE_PEEK, MEM_TRAVERSE]
843 \\ REWRITE_TAC [GSYM pred_setTheory.IN_UNION]
844 \\ `FINITE (NUMSET_OF_PTREE t UNION s)`
845 by SRW_TAC [] [pred_setTheory.FINITE_UNION]
846 \\ POP_ASSUM
847 (fn th => SUBST1_TAC (SPEC `n` (MATCH_MP SET_TO_LIST_IN_MEM th)))
848 \\ ASM_SIMP_TAC bool_ss [GSYM MEM_TRAVERSE, PTREE_OF_NUMSET_IS_PTREE]
849 \\ MATCH_MP_TAC PERM_MEM_EQ
850 \\ SRW_TAC [] [PTREE_OF_NUMSET_def, PERM_INSERT_PTREE]
851QED
852
853Theorem IN_PTREE_EMPTY[simp] = (GEN_ALL o EQF_ELIM o
854 SIMP_CONV (srw_ss()) [IN_PTREE_def, PEEK_def]) ``n IN_PTREE <{}>``;
855
856
857Theorem IN_PTREE_OF_NUMSET_EMPTY =
858 (GSYM o SIMP_RULE (srw_ss()) [] o SPEC `Empty`) IN_PTREE_OF_NUMSET;
859
860Theorem IS_SOME_EQ_UNIT[local]:
861 !a b:unit option. (IS_SOME a = IS_SOME b) = (a = b)
862Proof
863 Cases \\ Cases \\ SRW_TAC [] [oneTheory.one]
864QED
865
866Theorem PTREE_EXTENSION:
867 !t1 t2. IS_PTREE t1 /\ IS_PTREE t2 ==>
868 ((t1 = t2) = (!x. x IN_PTREE t1 = x IN_PTREE t2))
869Proof
870 SRW_TAC [] [GSYM PTREE_EQ, GSYM IS_SOME_EQ_UNIT, GSYM IN_PTREE_def]
871QED
872
873Theorem PTREE_OF_NUMSET_NUMSET_OF_PTREE:
874 !t s. IS_PTREE t /\ FINITE s ==>
875 (PTREE_OF_NUMSET Empty (NUMSET_OF_PTREE t UNION s) =
876 PTREE_OF_NUMSET t s)
877Proof
878 SRW_TAC [] [PTREE_EXTENSION, pred_setTheory.FINITE_UNION, IN_PTREE_OF_NUMSET]
879 \\ SRW_TAC [] [IN_PTREE_EMPTY, IN_NUMSET_OF_PTREE]
880QED
881
882Theorem NUMSET_OF_PTREE_PTREE_OF_NUMSET:
883 !t s. IS_PTREE t /\ FINITE s ==>
884 (NUMSET_OF_PTREE (PTREE_OF_NUMSET t s) =
885 NUMSET_OF_PTREE t UNION s)
886Proof
887 SRW_TAC []
888 [pred_setTheory.EXTENSION, IN_NUMSET_OF_PTREE, IN_PTREE_OF_NUMSET]
889QED
890
891Theorem NUMSET_OF_PTREE_EMPTY[simp]:
892 NUMSET_OF_PTREE Empty = {}
893Proof
894 SRW_TAC [] [NUMSET_OF_PTREE_def, TRAVERSE_def, LIST_TO_SET_THM]
895QED
896
897Theorem PTREE_OF_NUMSET_EMPTY[simp]:
898 !t. PTREE_OF_NUMSET t {} = t
899Proof
900 SRW_TAC [] [PTREE_OF_NUMSET_def, SET_TO_LIST_THM]
901QED
902
903
904Theorem NUMSET_OF_PTREE_PTREE_OF_NUMSET_EMPTY =
905 (SIMP_RULE (srw_ss()) [] o SPEC `Empty`) NUMSET_OF_PTREE_PTREE_OF_NUMSET;
906
907Theorem IN_PTREE_INSERT_PTREE:
908 !t m n. IS_PTREE t ==>
909 (n IN_PTREE (m INSERT_PTREE t) = (m = n) \/ n IN_PTREE t)
910Proof
911 SRW_TAC [] [IN_PTREE_def, PEEK_INSERT_PTREE]
912QED
913
914Theorem IN_PTREE_REMOVE:
915 !t m n. IS_PTREE t ==>
916 (n IN_PTREE (REMOVE t m) = ~(n = m) /\ n IN_PTREE t)
917Proof
918 SRW_TAC [] [IN_PTREE_def, PEEK_REMOVE]
919QED
920
921Theorem IN_PTREE_UNION_PTREE:
922 !t1 t2 n. IS_PTREE t1 /\ IS_PTREE t2 ==>
923 (n IN_PTREE (t1 UNION_PTREE t2) = n IN_PTREE t1 \/ n IN_PTREE t2)
924Proof
925 SRW_TAC [] [UNION_PTREE_def, IN_PTREE_OF_NUMSET]
926 \\ SRW_TAC [] [IN_NUMSET_OF_PTREE]
927QED
928
929Theorem UNION_PTREE_IS_PTREE[simp]:
930 !t1 t2. IS_PTREE t1 /\ IS_PTREE t2 ==>
931 IS_PTREE (t1 UNION_PTREE t2)
932Proof
933 SRW_TAC [] [UNION_PTREE_def]
934QED
935
936
937Theorem UNION_PTREE_COMM:
938 !t1 t2. IS_PTREE t1 /\ IS_PTREE t2 ==>
939 (t1 UNION_PTREE t2 = t2 UNION_PTREE t1)
940Proof
941 SRW_TAC [] [PTREE_EXTENSION] \\ METIS_TAC [IN_PTREE_UNION_PTREE]
942QED
943
944Theorem UNION_PTREE_COMM_EMPTY =
945 (GEN_ALL o SIMP_RULE (srw_ss()) [] o SPECL [`Empty`,`t`]) UNION_PTREE_COMM;
946
947Theorem UNION_PTREE_EMPTY:
948 (!t. t UNION_PTREE Empty = t) /\
949 (!t. IS_PTREE t ==> (Empty UNION_PTREE t = t))
950Proof
951 SRW_TAC [] [UNION_PTREE_COMM_EMPTY, UNION_PTREE_def]
952QED
953
954Theorem UNION_PTREE_ASSOC:
955 !t1 t2 t3. IS_PTREE t1 /\ IS_PTREE t2 /\ IS_PTREE t3 ==>
956 (t1 UNION_PTREE (t2 UNION_PTREE t3) =
957 t1 UNION_PTREE t2 UNION_PTREE t3)
958Proof
959 SRW_TAC [] [PTREE_EXTENSION, IN_PTREE_UNION_PTREE] \\ METIS_TAC []
960QED
961
962Theorem PTREE_OF_NUMSET_UNION:
963 !t s1 s2. IS_PTREE t /\ FINITE s1 /\ FINITE s2 ==>
964 (PTREE_OF_NUMSET t (s1 UNION s2) =
965 PTREE_OF_NUMSET (PTREE_OF_NUMSET t s1) s2)
966Proof
967 SRW_TAC [] [PTREE_EXTENSION, IN_PTREE_OF_NUMSET] \\ METIS_TAC []
968QED
969
970Theorem PTREE_OF_NUMSET_INSERT:
971 !t s x. IS_PTREE t /\ FINITE s ==>
972 (PTREE_OF_NUMSET t (x INSERT s) =
973 x INSERT_PTREE (PTREE_OF_NUMSET t s))
974Proof
975 SRW_TAC [] [PTREE_EXTENSION, IN_PTREE_OF_NUMSET, IN_PTREE_INSERT_PTREE]
976 \\ METIS_TAC []
977QED
978
979Theorem PTREE_OF_NUMSET_INSERT_EMPTY =
980 (SIMP_RULE (srw_ss()) [] o SPEC `Empty`) PTREE_OF_NUMSET_INSERT;
981
982Theorem PTREE_OF_NUMSET_DELETE:
983 !t s x. IS_PTREE t /\ FINITE s ==>
984 (PTREE_OF_NUMSET t (s DELETE x) =
985 if x IN_PTREE t then
986 PTREE_OF_NUMSET t s
987 else
988 REMOVE (PTREE_OF_NUMSET t s) x)
989Proof
990 SRW_TAC [] [PTREE_EXTENSION, IN_PTREE_OF_NUMSET, IN_PTREE_REMOVE]
991 \\ METIS_TAC []
992QED
993
994Theorem PTREE_OF_NUMSET_DELETE[allow_rebind] =
995 (SIMP_RULE (srw_ss()) [] o SPEC `Empty`) PTREE_OF_NUMSET_DELETE
996
997(* ------------------------------------------------------------------------- *)
998
999Theorem TRAVERSE_AUX_lem[local]:
1000 !t l. TRAVERSE_AUX t l = TRAVERSE_AUX t [] ++ l
1001Proof
1002 Induct
1003 >- SRW_TAC [] [TRAVERSE_AUX_def]
1004 >- SRW_TAC [] [TRAVERSE_AUX_def]
1005 \\ ONCE_REWRITE_TAC [TRAVERSE_AUX_def]
1006 \\ METIS_TAC [listTheory.APPEND_ASSOC]
1007QED
1008
1009Theorem TRAVERSE_AUX:
1010 !t. TRAVERSE t = TRAVERSE_AUX t []
1011Proof
1012 Induct \\ SRW_TAC [] [TRAVERSE_def, TRAVERSE_AUX_def]
1013 \\ METIS_TAC [TRAVERSE_AUX_lem]
1014QED
1015
1016Theorem PTREE_TRAVERSE_EQ:
1017 !t1 t2. IS_PTREE t1 /\ IS_PTREE t2 ==>
1018 ((!k. MEM k (TRAVERSE t1) = MEM k (TRAVERSE t2)) =
1019 (TRAVERSE t1 = TRAVERSE t2))
1020Proof
1021 REPEAT STRIP_TAC
1022 \\ EQ_TAC \\ SRW_TAC [] []
1023 \\ POP_ASSUM MP_TAC
1024 \\ `TRAVERSE t1 = TRAVERSE (TRANSFORM (K ()) t1)`
1025 by METIS_TAC [TRAVERSE_TRANSFORM]
1026 \\ `TRAVERSE t2 = TRAVERSE (TRANSFORM (K ()) t2)`
1027 by METIS_TAC [TRAVERSE_TRANSFORM]
1028 \\ NTAC 2 (POP_ASSUM SUBST1_TAC)
1029 \\ SRW_TAC [] [IS_SOME_EQ_UNIT, MEM_TRAVERSE_PEEK, PTREE_EQ]
1030QED
1031
1032val QSORT_EQ =
1033 METIS_PROVE [QSORT_PERM, PERM_TRANS, PERM_SYM, PERM_REFL]
1034 ``!R l1 l2. (QSORT R l1 = QSORT R l2) ==> PERM l1 l2``;
1035
1036Theorem QSORT_MEM_EQ =
1037 GEN_ALL (IMP_TRANS (SPEC_ALL QSORT_EQ) (SPEC_ALL PERM_MEM_EQ));
1038
1039Theorem KEYS_PEEK:
1040 !t1 t2. IS_PTREE t1 /\ IS_PTREE t2 ==>
1041 ((KEYS t1 = KEYS t2) = (TRAVERSE t1 = TRAVERSE t2))
1042Proof
1043 REPEAT STRIP_TAC \\ EQ_TAC \\ SRW_TAC [] [KEYS_def]
1044 \\ IMP_RES_TAC QSORT_MEM_EQ
1045 \\ NTAC 2 (POP_ASSUM (K ALL_TAC))
1046 \\ METIS_TAC [PTREE_TRAVERSE_EQ]
1047QED
1048
1049Theorem lem1[local]:
1050 !t k. IS_PTREE t /\ ~MEM k (TRAVERSE t) ==>
1051 PERM (SET_TO_LIST (NUMSET_OF_PTREE (k INSERT_PTREE t)))
1052 (k::TRAVERSE t)
1053Proof
1054 REPEAT STRIP_TAC
1055 \\ MATCH_MP_TAC MEM_ALL_DISTINCT_IMP_PERM
1056 \\ SRW_TAC [] [MEM_TRAVERSE, IN_NUMSET_OF_PTREE, IN_PTREE_INSERT_PTREE]
1057 \\ METIS_TAC []
1058QED
1059
1060val lem2 = (SIMP_RULE (srw_ss()) [PTREE_OF_NUMSET_INSERT,
1061 GSYM NUMSET_OF_PTREE_PTREE_OF_NUMSET] o
1062 SPECL [`t`, `{x}`]) PERM_INSERT_PTREE;
1063
1064Theorem PERM_ADD:
1065 !t k d. IS_PTREE t /\ ~MEM k (TRAVERSE t) ==>
1066 PERM (TRAVERSE (ADD t (k,d))) (k::TRAVERSE t)
1067Proof
1068 NTAC 3 STRIP_TAC
1069 \\ `TRAVERSE (ADD t (k,d)) = TRAVERSE (ADD (TRANSFORM (K ()) t) (k,()))`
1070 by REWRITE_TAC [TRAVERSE_TRANSFORM, (GSYM o SIMP_RULE std_ss [] o
1071 ISPEC `K ()`) ADD_TRANSFORM]
1072 \\ POP_ASSUM SUBST1_TAC
1073 \\ ISPECL_THEN [`K ()`,`t`] (SUBST1_TAC o SYM) TRAVERSE_TRANSFORM
1074 \\ SRW_TAC [] []
1075 \\ METIS_TAC [lem1, lem2, PERM_SYM, PERM_TRANS, TRANSFORM_IS_PTREE]
1076QED
1077
1078Theorem TRAVERSE_ADD_MEM[local]:
1079 !t k d. IS_PTREE t ==>
1080 (MEM j (TRAVERSE (ADD t (k,d))) =
1081 (j = k) \/ MEM j (TRAVERSE t))
1082Proof
1083 SRW_TAC [] [MEM_TRAVERSE_PEEK, PEEK_ADD]
1084QED
1085
1086Theorem PERM_NOT_ADD:
1087 !t k d. IS_PTREE t /\ MEM k (TRAVERSE t) ==>
1088 (TRAVERSE (ADD t (k,d)) = TRAVERSE t)
1089Proof
1090 SRW_TAC [] [GSYM PTREE_TRAVERSE_EQ, TRAVERSE_ADD_MEM]
1091 \\ METIS_TAC []
1092QED
1093
1094Theorem TRAVERSE_REMOVE_MEM[local]:
1095 !t k. IS_PTREE t ==>
1096 (MEM j (TRAVERSE (REMOVE t k)) =
1097 ~(j = k) /\ MEM j (TRAVERSE t))
1098Proof
1099 SRW_TAC [] [MEM_TRAVERSE_PEEK, PEEK_REMOVE]
1100QED
1101
1102Theorem PERM_NOT_REMOVE:
1103 !t k. IS_PTREE t /\ ~MEM k (TRAVERSE t) ==>
1104 (TRAVERSE (REMOVE t k) = TRAVERSE t)
1105Proof
1106 SRW_TAC [] [GSYM PTREE_TRAVERSE_EQ, TRAVERSE_REMOVE_MEM]
1107 \\ METIS_TAC []
1108QED
1109
1110Theorem PERM_DELETE_PTREE:
1111 !t:unit ptree k.
1112 IS_PTREE t /\ MEM k (TRAVERSE t) ==>
1113 PERM (TRAVERSE (REMOVE t k))
1114 (FILTER (\x. ~(x = k)) (TRAVERSE t))
1115Proof
1116 REPEAT STRIP_TAC
1117 \\ MATCH_MP_TAC MEM_ALL_DISTINCT_IMP_PERM
1118 \\ SRW_TAC [] [MEM_FILTER, MEM_TRAVERSE_PEEK,
1119 PEEK_REMOVE]
1120 \\ SRW_TAC [] [ALL_DISTINCT_FILTER, MEM_FILTER, FILTER_FILTER,
1121 METIS_PROVE [] ``~(x = k) ==>
1122 ((\x'. (x = x') /\ ~(x' = k)) = ($= x))``]
1123 \\ POP_ASSUM MP_TAC \\ SPEC_TAC (`x`,`x`)
1124 \\ ASM_SIMP_TAC (srw_ss()) [GSYM ALL_DISTINCT_FILTER]
1125QED
1126
1127Theorem FILTER_NONE:
1128 !P l. (!n. n < LENGTH l ==> P (EL n l)) ==> (FILTER P l = l)
1129Proof
1130 Induct_on `l` \\ SRW_TAC [] []
1131 >- POP_ASSUM (fn th => ASM_SIMP_TAC std_ss
1132 [(GEN_ALL o SIMP_RULE (srw_ss()) [] o SPEC `SUC n`) th])
1133 \\ POP_ASSUM (STRIP_ASSUME_TAC o SIMP_RULE (srw_ss()) [] o SPEC `0`)
1134QED
1135
1136Theorem MEM_NOT_NULL[local]:
1137 !l x. MEM x l ==> 0 < LENGTH l
1138Proof
1139 Cases \\ SRW_TAC [] []
1140QED
1141
1142Theorem LENGTH_FILTER_ONE_ALL_DISTINCT[local]:
1143 !l k. ALL_DISTINCT l /\ MEM k l ==>
1144 (LENGTH (FILTER (\x. ~(x = k)) l) = LENGTH l - 1)
1145Proof
1146 Induct \\ SRW_TAC [] []
1147 \\ FULL_SIMP_TAC (srw_ss()) []
1148 >- METIS_TAC [DECIDE ``0 < n ==> (SUC (n - 1) = n)``, MEM_NOT_NULL]
1149 \\ MATCH_MP_TAC (METIS_PROVE [] ``(a = b) ==> (LENGTH a = LENGTH b)``)
1150 \\ MATCH_MP_TAC FILTER_NONE
1151 \\ METIS_TAC [MEM_EL]
1152QED
1153
1154Theorem PERM_REMOVE:
1155 !t k. IS_PTREE t /\ MEM k (TRAVERSE t) ==>
1156 PERM (TRAVERSE (REMOVE t k)) (FILTER (\x. ~(x = k)) (TRAVERSE t))
1157Proof
1158 NTAC 2 STRIP_TAC
1159 \\ `TRAVERSE (REMOVE t k) = TRAVERSE (REMOVE (TRANSFORM (K ()) t) k)`
1160 by REWRITE_TAC [TRAVERSE_TRANSFORM, (GSYM o SIMP_RULE (srw_ss()) [] o
1161 ISPEC `K ()`) REMOVE_TRANSFORM]
1162 \\ POP_ASSUM SUBST1_TAC
1163 \\ ISPECL_THEN [`K ()`,`t`] (SUBST1_TAC o SYM) TRAVERSE_TRANSFORM
1164 \\ SRW_TAC [] [PERM_DELETE_PTREE]
1165QED
1166
1167Theorem SIZE_ADD:
1168 !t k d.
1169 IS_PTREE t ==>
1170 (SIZE (ADD t (k,d)) =
1171 if MEM k (TRAVERSE t) then
1172 SIZE t
1173 else
1174 SIZE t + 1)
1175Proof
1176 SRW_TAC [] [SIZE_def, PERM_NOT_ADD]
1177 \\ METIS_TAC [PERM_ADD, PERM_LENGTH, LENGTH, ADD1]
1178QED
1179
1180Theorem SIZE_REMOVE:
1181 !t k.
1182 IS_PTREE t ==>
1183 (SIZE (REMOVE t k) =
1184 if MEM k (TRAVERSE t) then
1185 SIZE t - 1
1186 else
1187 SIZE t)
1188Proof
1189 SRW_TAC [] [SIZE_def, PERM_NOT_REMOVE]
1190 \\ METIS_TAC [PERM_REMOVE, PERM_LENGTH, ALL_DISTINCT_TRAVERSE,
1191 LENGTH_FILTER_ONE_ALL_DISTINCT]
1192QED
1193
1194(* ------------------------------------------------------------------------- *)
1195
1196Theorem SIZE:
1197 (SIZE (Empty: 'a ptree) = 0) /\
1198 (!k d. SIZE (Leaf k d : 'a ptree) = 1) /\
1199 (!p m l r. SIZE (Branch p m l r : 'a ptree) = SIZE l + SIZE r)
1200Proof
1201 SRW_TAC [] [SIZE_def, TRAVERSE_def]
1202QED
1203val _ = computeLib.add_persistent_funs ["SIZE"];
1204
1205Theorem LENGTH_FOLDL_ADD[local]:
1206 !l t. IS_PTREE t /\ ALL_DISTINCT (TRAVERSE t ++ l) ==>
1207 (SIZE (FOLDL (combin$C $INSERT_PTREE) t l) = SIZE t + LENGTH l)
1208Proof
1209 Induct \\ SRW_TAC [] [SIZE]
1210 \\ `ALL_DISTINCT (TRAVERSE (h INSERT_PTREE t) ++ l) /\ ~MEM h (TRAVERSE t)`
1211 by (FULL_SIMP_TAC (srw_ss()) [ALL_DISTINCT_APPEND,
1212 MEM_TRAVERSE_INSERT_PTREE] \\ METIS_TAC [])
1213 \\ `SIZE (h INSERT_PTREE t) = SIZE t + 1`
1214 by RW_TAC std_ss [SIZE_ADD, INSERT_PTREE_def]
1215 \\ METIS_TAC [INSERT_PTREE_IS_PTREE, DECIDE ``a + 1 + b = a + SUC b``]
1216QED
1217
1218Theorem SIZE_PTREE_OF_NUMSET =
1219 (GEN_ALL o SIMP_RULE (srw_ss()) [GSYM PTREE_OF_NUMSET_def, SET_TO_LIST_CARD] o
1220 DISCH `FINITE s` o SPECL [`SET_TO_LIST s`,`t`]) LENGTH_FOLDL_ADD;
1221
1222Theorem SIZE_PTREE_OF_NUMSET_EMPTY =
1223 (SIMP_RULE (srw_ss()) [TRAVERSE_def, SIZE] o
1224 SPEC `Empty`) SIZE_PTREE_OF_NUMSET;
1225
1226Theorem CARD_LIST_TO_SET:
1227 !l. ALL_DISTINCT l ==> (CARD (LIST_TO_SET l) = LENGTH l)
1228Proof
1229 Induct \\ SRW_TAC [] [LIST_TO_SET_THM, ALL_DISTINCT]
1230QED
1231
1232Theorem CARD_NUMSET_OF_PTREE:
1233 !t. IS_PTREE t ==> (CARD (NUMSET_OF_PTREE t) = SIZE t)
1234Proof
1235 SRW_TAC [] [NUMSET_OF_PTREE_def, CARD_LIST_TO_SET, SIZE_def]
1236QED
1237
1238(* ------------------------------------------------------------------------- *)
1239
1240Theorem DELETE_UNION:
1241 !x s1 s2. (s1 UNION s2) DELETE x = (s1 DELETE x) UNION (s2 DELETE x)
1242Proof
1243 SRW_TAC [] [pred_setTheory.EXTENSION] \\ METIS_TAC []
1244QED
1245
1246val _ = computeLib.add_persistent_funs
1247 ["list.LIST_TO_SET_THM",
1248 "pred_set.EMPTY_DELETE",
1249 "pred_set.DELETE_INSERT",
1250 "DELETE_UNION",
1251 "pred_set.FINITE_EMPTY",
1252 "pred_set.FINITE_INSERT",
1253 "pred_set.FINITE_UNION",
1254 "pred_set.FINITE_DELETE",
1255 "TRAVERSE_AUX",
1256 "ADD_INSERT",
1257 "PTREE_OF_NUMSET_EMPTY"];
1258
1259(* ------------------------------------------------------------------------- *)