1 (* ========================================================================= *)
2 (* Computations with finite sets of nums. *)
4 (* (c) Copyright, Clelia Lomuto, Marco Maggesi, 2009. *)
5 (* Distributed with HOL Light under same license terms *)
6 (* ========================================================================= *)
8 (* ------------------------------------------------------------------------- *)
9 (* This file defines some conversions that operate on finite sets of nums *)
10 (* represented literally in a trie-like structure (we call them `ntries'). *)
11 (* ------------------------------------------------------------------------- *)
13 (* ------------------------------------------------------------------------- *)
15 (* # NTRIE_COMPUTE NTRIE_REDUCE_CONV *)
16 (* `{10, 1001, 3} INTER {3, 7, 10} SUBSET {10, 10000} UNION {3, 33}`;; *)
18 (* |- {10, 1001, 3} INTER {3, 7, 10} SUBSET {10, 10000} UNION {3, 33} <=> T *)
19 (* ------------------------------------------------------------------------- *)
21 (* ------------------------------------------------------------------------- *)
22 (* Constructors for the ntrie representation of a set of nums. *)
23 (* ------------------------------------------------------------------------- *)
25 let NEMPTY = new_definition
26 `NEMPTY:num->bool = {}`;;
28 let NZERO = new_definition
31 let NNODE = new_definition
32 `!s t. NNODE s t = IMAGE BIT0 s UNION IMAGE BIT1 t`;;
34 let NTRIE = new_definition
35 `!s:num->bool. NTRIE s = s`;;
37 let NTRIE_RELATIONS = prove
38 (`NNODE NEMPTY NEMPTY = NEMPTY /\
39 NNODE NZERO NEMPTY = NZERO`,
40 REWRITE_TAC[NEMPTY; NZERO; NNODE; EXTENSION; NOT_IN_EMPTY;
41 IN_INSERT; IN_UNION; IN_IMAGE] THEN
42 MESON_TAC[ARITH_EQ]);;
44 (* ------------------------------------------------------------------------- *)
46 (* ------------------------------------------------------------------------- *)
49 (`(!s n. NUMERAL n IN NTRIE s <=> n IN s) /\
50 (!n. ~(n IN NEMPTY)) /\
51 (!n. n IN NZERO <=> n = _0) /\
52 (!s t. _0 IN NNODE s t <=> _0 IN s) /\
53 (!s t n. BIT0 n IN NNODE s t <=> n IN s) /\
54 (!s t n. BIT1 n IN NNODE s t <=> n IN t)`,
55 REWRITE_TAC[NUMERAL; NTRIE; NEMPTY; NZERO; NNODE; NOT_IN_EMPTY; IN_INSERT;
56 IN_UNION; IN_IMAGE; ARITH_EQ] THEN
59 let NTRIE_IN_CONV : conv =
60 let tth,pths = CONJ_PAIR NTRIE_IN in
61 REWR_CONV tth THENC REWRITE_CONV[pths; CONJUNCT2 ARITH_EQ];;
63 (* ------------------------------------------------------------------------- *)
65 (* ------------------------------------------------------------------------- *)
67 let NTRIE_SUBSET = prove
68 (`(!s t. NTRIE s SUBSET NTRIE t <=> s SUBSET t) /\
69 (!s. NEMPTY SUBSET s) /\
70 (!s:num->bool. s SUBSET s) /\
71 ~(NZERO SUBSET NEMPTY) /\
72 (!s t. NNODE s t SUBSET NEMPTY <=> s SUBSET NEMPTY /\ t SUBSET NEMPTY) /\
73 (!s t. NNODE s t SUBSET NZERO <=> s SUBSET NZERO /\ t SUBSET NEMPTY) /\
74 (!s t. NZERO SUBSET NNODE s t <=> NZERO SUBSET s) /\
76 NNODE s1 t1 SUBSET NNODE s2 t2 <=> s1 SUBSET s2 /\ t1 SUBSET t2)`,
77 REWRITE_TAC[NTRIE; NEMPTY; NZERO; NNODE; EMPTY_SUBSET; SUBSET_REFL;
78 SING_SUBSET; NOT_IN_EMPTY] THEN
80 REWRITE_TAC[SUBSET; NOT_IN_EMPTY; IN_INSERT; IN_UNION; IN_IMAGE;
82 [MESON_TAC[]; MESON_TAC[ARITH_EQ]; MESON_TAC[]; EQ_TAC] THENL
83 [ALL_TAC; MESON_TAC[ARITH_EQ]] THEN
84 STRIP_TAC THEN CONJ_TAC THEN GEN_TAC THENL
85 [POP_ASSUM (MP_TAC o SPEC `BIT0 x`);
86 POP_ASSUM (MP_TAC o SPEC `BIT1 x`)] THEN
87 REWRITE_TAC[ARITH_EQ] THEN MESON_TAC[]);;
89 let NTRIE_SUBSET_CONV : conv =
90 let tth,pths = CONJ_PAIR NTRIE_SUBSET in
91 REWR_CONV tth THENC REWRITE_CONV[pths];;
93 (* ------------------------------------------------------------------------- *)
95 (* ------------------------------------------------------------------------- *)
98 (`(!s t. NTRIE s = NTRIE t <=> s = t) /\
99 (!s:num->bool. s = s) /\
102 (!s t. NNODE s t = NEMPTY <=> s = NEMPTY /\ t = NEMPTY) /\
103 (!s t. NEMPTY = NNODE s t <=> s = NEMPTY /\ t = NEMPTY) /\
104 (!s t. NNODE s t = NZERO <=> s = NZERO /\ t = NEMPTY) /\
105 (!s t. NZERO = NNODE s t <=> s = NZERO /\ t = NEMPTY) /\
106 (!s1 s2 t1 t2. NNODE s1 t1 = NNODE s2 t2 <=> s1 = s2 /\ t1 = t2)`,
107 REWRITE_TAC[GSYM SUBSET_ANTISYM_EQ; NTRIE_SUBSET; NEMPTY; NZERO] THEN
110 let NTRIE_EQ_CONV : conv =
111 let tth,pths = CONJ_PAIR NTRIE_EQ in
112 REWR_CONV tth THENC REWRITE_CONV[pths];;
114 (* ------------------------------------------------------------------------- *)
116 (* ------------------------------------------------------------------------- *)
118 let NTRIE_SING = prove
119 (`(!n. {NUMERAL n} = NTRIE {n}) /\
121 (!n. {BIT0 n} = if n = _0 then NZERO else NNODE {n} NEMPTY) /\
122 (!n. {BIT1 n} = NNODE NEMPTY {n})`,
123 REWRITE_TAC[NUMERAL; NTRIE; NEMPTY; NZERO; NNODE; IMAGE_CLAUSES;
125 GEN_TAC THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[ARITH_ZERO]);;
127 let NTRIE_SING_CONV =
128 let tth,pths = CONJ_PAIR NTRIE_SING in
129 REWR_CONV tth THENC RAND_CONV(REWRITE_CONV[pths; CONJUNCT2 ARITH_EQ]);;
131 (* ------------------------------------------------------------------------- *)
133 (* ------------------------------------------------------------------------- *)
135 let NTRIE_INSERT = prove
136 (`(!s n. NUMERAL n INSERT NTRIE s = NTRIE (n INSERT s)) /\
137 (!n. n INSERT NEMPTY = {n}) /\
138 _0 INSERT NZERO = NZERO /\
139 (!s t n. _0 INSERT NNODE s t = NNODE (_0 INSERT s) t) /\
140 (!n. BIT0 n INSERT NZERO = if n = _0 then NZERO else
141 NNODE (n INSERT NZERO) NEMPTY) /\
142 (!n. BIT1 n INSERT NZERO = NNODE NZERO {n}) /\
143 (!s t n. BIT0 n INSERT NNODE s t = NNODE (n INSERT s) t) /\
144 (!s t n. BIT1 n INSERT NNODE s t = NNODE s (n INSERT t))`,
145 REWRITE_TAC[NUMERAL; NTRIE; NEMPTY; NZERO; NNODE] THEN
146 REPEAT STRIP_TAC THEN TRY COND_CASES_TAC THEN
147 REWRITE_TAC[EXTENSION; IN_INSERT; NOT_IN_EMPTY; IN_UNION; IN_IMAGE] THEN
148 ASM_MESON_TAC[ARITH_EQ]);;
150 let NTRIE_INSERT_CONV : conv =
151 let tth,pths = CONJ_PAIR NTRIE_INSERT in
153 RAND_CONV(REWRITE_CONV[pths; CONJUNCT2 NTRIE_SING; CONJUNCT2 ARITH_EQ]);;
155 (* ------------------------------------------------------------------------- *)
157 (* ------------------------------------------------------------------------- *)
159 let NTRIE_UNION = prove
160 (`(!s t. NTRIE s UNION NTRIE t = NTRIE (s UNION t)) /\
161 (!s. s UNION NEMPTY = s) /\
162 (!s. NEMPTY UNION s = s) /\
163 NZERO UNION NZERO = NZERO /\
164 (!s t. NNODE s t UNION NZERO = NNODE (s UNION NZERO) t) /\
165 (!s t. NZERO UNION NNODE s t = NNODE (s UNION NZERO) t) /\
166 (!s t r q. NNODE s t UNION NNODE r q = NNODE (s UNION r) (t UNION q))`,
167 REWRITE_TAC[NTRIE; NEMPTY; NZERO; NNODE] THEN REPEAT STRIP_TAC THEN
168 TRY COND_CASES_TAC THEN
169 REWRITE_TAC[UNION_EMPTY; INSERT_UNION; NOT_IN_EMPTY; IN_INSERT; IN_UNION;
170 IN_IMAGE; EXTENSION] THEN
171 MESON_TAC[ARITH_EQ]);;
173 let NTRIE_UNION_CONV : conv =
174 let tth,pths = CONJ_PAIR NTRIE_UNION in
175 REWR_CONV tth THENC RAND_CONV(REWRITE_CONV[pths]);;
177 (* ------------------------------------------------------------------------- *)
179 (* Warning: rewriting with this theorem generates ntries which are not *)
180 (* "minimal". It has to be used in conjuction with NTRIE_RELATIONS. *)
181 (* ------------------------------------------------------------------------- *)
183 let NTRIE_INTER = prove
184 (`(!s t. NTRIE s INTER NTRIE t = NTRIE (s INTER t)) /\
185 (!s. NEMPTY INTER s = NEMPTY) /\
186 (!s. s INTER NEMPTY = NEMPTY) /\
187 NZERO INTER NZERO = NZERO /\
188 (!s t. NZERO INTER NNODE s t = NZERO INTER s) /\
189 (!s t. NNODE s t INTER NZERO = NZERO INTER s) /\
191 NNODE s1 t1 INTER NNODE s2 t2 = NNODE (s1 INTER s2) (t1 INTER t2))`,
192 REWRITE_TAC[NTRIE; NEMPTY; NZERO; NNODE; INTER_EMPTY; INSERT_INTER;
193 NOT_IN_EMPTY; IN_INSERT] THEN
194 REPEAT STRIP_TAC THENL
195 [REWRITE_TAC[IN_UNION; IN_IMAGE; ARITH_EQ] THEN ASM_MESON_TAC[];
197 ASM_REWRITE_TAC[EXTENSION; IN_UNION; IN_INTER; IN_IMAGE;
198 IN_INSERT; NOT_IN_EMPTY] THEN
199 ASM_MESON_TAC[ARITH_EQ];
200 REWRITE_TAC[EXTENSION; IN_INTER; IN_UNION; IN_IMAGE] THEN
201 MESON_TAC[ARITH_EQ]]);;
203 let NTRIE_INTER_CONV : conv =
204 let tth,pths = CONJ_PAIR NTRIE_INTER in
205 REWR_CONV tth THENC RAND_CONV(REWRITE_CONV[pths; NTRIE_RELATIONS]);;
207 (* ------------------------------------------------------------------------- *)
208 (* Deleting an element. *)
209 (* Warning: rewriting with this theorem generates ntries which are not *)
210 (* "minimal". It has to be used in conjuction with NTRIE_RELATIONS. *)
211 (* ------------------------------------------------------------------------- *)
213 let NTRIE_DELETE = prove
214 (`(!s n. NTRIE s DELETE NUMERAL n = NTRIE (s DELETE n)) /\
215 (!n. NEMPTY DELETE n = NEMPTY) /\
216 (!n. NZERO DELETE n = if n = _0 then NEMPTY else NZERO) /\
217 (!s t. NNODE s t DELETE _0 = NNODE (s DELETE _0) t) /\
218 (!s t n. NNODE s t DELETE BIT0 n = NNODE (s DELETE n) t) /\
219 (!s t n. NNODE s t DELETE BIT1 n = NNODE s (t DELETE n))`,
220 REWRITE_TAC[NUMERAL; NTRIE; NEMPTY; NZERO; NNODE] THEN REPEAT STRIP_TAC THEN
221 TRY COND_CASES_TAC THEN
222 ASM_REWRITE_TAC[EXTENSION; IN_DELETE; IN_UNION; IN_IMAGE;
223 NOT_IN_EMPTY; IN_INSERT] THEN
224 ASM_MESON_TAC[ARITH_EQ]);;
226 let NTRIE_DELETE_CONV : conv =
227 let tth,pths = CONJ_PAIR NTRIE_DELETE in
228 REWR_CONV tth THENC RAND_CONV(REWRITE_CONV[pths; NTRIE_RELATIONS]);;
230 (* ------------------------------------------------------------------------- *)
232 (* ------------------------------------------------------------------------- *)
234 let NTRIE_DISJOINT = prove
235 (`(!s t. DISJOINT (NTRIE s) (NTRIE t) <=> DISJOINT s t) /\
236 (!s. DISJOINT s NEMPTY) /\
237 (!s. DISJOINT NEMPTY s) /\
238 ~DISJOINT NZERO NZERO /\
239 (!s t. DISJOINT NZERO (NNODE s t) <=> DISJOINT s NZERO) /\
240 (!s t. DISJOINT (NNODE s t) NZERO <=> DISJOINT s NZERO) /\
241 (!s1 s2 t1 t2. DISJOINT (NNODE s1 t1) (NNODE s2 t2) <=>
242 DISJOINT s1 s2 /\ DISJOINT t1 t2)`,
243 REWRITE_TAC[NTRIE; DISJOINT; GSYM NEMPTY;
244 NTRIE_INTER; INTER_ACI; NTRIE_EQ]);;
246 let NTRIE_DISJOINT_CONV : conv =
247 let tth,pths = CONJ_PAIR NTRIE_DISJOINT in
248 REWR_CONV tth THENC REWRITE_CONV[pths];;
250 (* ------------------------------------------------------------------------- *)
252 (* ------------------------------------------------------------------------- *)
254 let NTRIE_DIFF = prove
255 (`(!s t. NTRIE s DIFF NTRIE t = NTRIE (s DIFF t)) /\
256 (!s. NEMPTY DIFF s = NEMPTY) /\
257 (!s. s DIFF NEMPTY = s) /\
258 NZERO DIFF NZERO = NEMPTY /\
259 (!s t. NZERO DIFF NNODE s t = NZERO DIFF s) /\
260 (!s t. NNODE s t DIFF NZERO = NNODE (s DIFF NZERO) t) /\
261 (!s1 t1 s2 t2. NNODE s1 t1 DIFF NNODE s2 t2 =
262 NNODE (s1 DIFF s2) (t1 DIFF t2))`,
263 REWRITE_TAC[NTRIE; NEMPTY; NZERO; NNODE; EMPTY_DIFF; DIFF_EMPTY;
264 DIFF_EQ_EMPTY; EXTENSION; NOT_IN_EMPTY; IN_INSERT; IN_DIFF;
265 IN_UNION; IN_IMAGE] THEN
266 MESON_TAC[ARITH_EQ]);;
268 let NTRIE_DIFF_CONV : conv =
269 let tth,pths = CONJ_PAIR NTRIE_DIFF in
270 REWR_CONV tth THENC REWRITE_CONV[pths];;
272 (* ------------------------------------------------------------------------- *)
274 (* ------------------------------------------------------------------------- *)
276 let NTRIE_IMAGE_DEF = new_definition
277 `!f acc s. NTRIE_IMAGE f acc s = IMAGE f s UNION acc`;;
279 let NTRIE_IMAGE = prove
280 (`(!f acc. NTRIE_IMAGE f acc NEMPTY = acc) /\
281 (!f acc. NTRIE_IMAGE f acc NZERO = f _0 INSERT acc) /\
282 (!f acc s t. NTRIE_IMAGE f acc (NNODE s t) =
283 NTRIE_IMAGE (\n. f (BIT1 n))
284 (NTRIE_IMAGE (\n. f (BIT0 n)) acc s)
286 REWRITE_TAC[NEMPTY; NZERO; NNODE; NTRIE_IMAGE_DEF; GSYM IMAGE_o; o_DEF;
287 IMAGE_UNION; IMAGE_CLAUSES; UNION_EMPTY; INSERT_UNION] THEN
288 REPEAT STRIP_TAC THENL [COND_CASES_TAC THEN ASM SET_TAC[]; SET_TAC[]]);;
290 let IMAGE_EQ_NTRIE_IMAGE = prove
291 (`!f s. IMAGE f (NTRIE s) = NTRIE_IMAGE (\n. f (NUMERAL n)) {} s`,
292 REWRITE_TAC [NUMERAL; NTRIE; ETA_AX; NTRIE_IMAGE_DEF; UNION_EMPTY]);;
294 let NTRIE_IMAGE_CONV : conv -> conv =
295 let [c1;c2;c3] = map REWR_CONV (CONJUNCTS NTRIE_IMAGE) in
298 (c1 ORELSEC (c2 THENC LAND_CONV (TRY_CONV BETA_CONV THENC cnv)) ORELSEC
300 RATOR_CONV (ONCE_DEPTH_CONV BETA_CONV THENC RAND_CONV conv) THENC
302 REWR_CONV IMAGE_EQ_NTRIE_IMAGE THENC (ONCE_DEPTH_CONV BETA_CONV) THENC conv;;
304 (* ------------------------------------------------------------------------- *)
305 (* Decoding of a set in ntrie form to the usual literal representation. *)
306 (* ------------------------------------------------------------------------- *)
308 let NTRIE_DECODE_CONV : conv =
309 let NTRIE_DECODE_THM = prove
310 (`!s. NTRIE s = NTRIE_IMAGE NUMERAL {} s`,
311 REWRITE_TAC[NTRIE; NUMERAL; NTRIE_IMAGE_DEF; UNION_EMPTY; IMAGE] THEN
313 and [c1;c2;c3] = map REWR_CONV (CONJUNCTS NTRIE_IMAGE) in
315 (c1 ORELSEC (c2 THENC LAND_CONV (TRY_CONV BETA_CONV)) ORELSEC
317 RATOR_CONV (ONCE_DEPTH_CONV BETA_CONV THENC RAND_CONV conv) THENC
319 REWR_CONV NTRIE_DECODE_THM THENC conv;;
321 (* ------------------------------------------------------------------------- *)
322 (* Encoding of a set from the usual literal form to the ntrie form. *)
323 (* ------------------------------------------------------------------------- *)
325 let NTRIE_ENCODE_CONV : conv=
326 let itm = `(INSERT):num->(num->bool)->num->bool`
327 and th = prove (`{} = NTRIE NEMPTY`, REWRITE_TAC[NTRIE; NEMPTY]) in
328 let cnv1 = REWR_CONV th
330 let fn,arg = dest_comb tm in
331 if rator fn <> itm then fail () else
332 AP_TERM fn (cnv arg) in
333 let rec conv tm = (cnv1 ORELSEC (cnv2 conv THENC NTRIE_INSERT_CONV)) tm in
336 (* ------------------------------------------------------------------------- *)
337 (* Final hack-together. *)
338 (* ------------------------------------------------------------------------- *)
340 let NTRIE_REL_CONV : conv =
341 let gconv_net = itlist (uncurry net_of_conv)
342 [`NTRIE s = NTRIE t`, NTRIE_EQ_CONV;
343 `NTRIE s SUBSET NTRIE t`, NTRIE_SUBSET_CONV;
344 `DISJOINT (NTRIE s) (NTRIE t)`, NTRIE_DISJOINT_CONV;
345 `NUMERA n IN NTRIE s`, NTRIE_IN_CONV]
347 REWRITES_CONV gconv_net;;
349 let NTRIE_RED_CONV : conv =
350 let gconv_net = itlist (uncurry net_of_conv)
351 [`NTRIE s = NTRIE t`, NTRIE_EQ_CONV;
352 `NTRIE s SUBSET NTRIE t`, NTRIE_SUBSET_CONV;
353 `DISJOINT (NTRIE s) (NTRIE t)`, NTRIE_DISJOINT_CONV;
354 `NUMERA n IN NTRIE s`, NTRIE_IN_CONV;
355 `NUMERAL n INSERT NTRIE s`, NTRIE_INSERT_CONV;
356 `NTRIE s UNION NTRIE t`, NTRIE_UNION_CONV;
357 `NTRIE s INTER NTRIE t`, NTRIE_INTER_CONV;
358 `NTRIE s DELETE NUMERAL n`, NTRIE_DELETE_CONV;
359 `NTRIE s DIFF NTRIE t`, NTRIE_DIFF_CONV]
361 REWRITES_CONV gconv_net;;
363 let NTRIE_REDUCE_CONV = DEPTH_CONV NTRIE_RED_CONV;;
365 let NTRIE_REDUCE_TAC = CONV_TAC NTRIE_REDUCE_CONV;;
367 let NTRIE_COMPUTE (cnv : conv) : conv =
368 ONCE_DEPTH_CONV NTRIE_ENCODE_CONV THENC
370 ONCE_DEPTH_CONV NTRIE_DECODE_CONV;;