Update from HH
[hl193./.git] / Ntrie / ntrie.ml
1 (* ========================================================================= *)
2 (* Computations with finite sets of nums.                                    *)
3 (*                                                                           *)
4 (*        (c) Copyright, Clelia Lomuto, Marco Maggesi, 2009.                 *)
5 (*          Distributed with HOL Light under same license terms              *)
6 (* ========================================================================= *)
7
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 (* ------------------------------------------------------------------------- *)
12
13 (* ------------------------------------------------------------------------- *)
14 (* Example:                                                                  *)
15 (* # NTRIE_COMPUTE NTRIE_REDUCE_CONV                                         *)
16 (*   `{10, 1001, 3} INTER {3, 7, 10} SUBSET {10, 10000} UNION {3, 33}`;;     *)
17 (* val it : thm =                                                            *)
18 (* |- {10, 1001, 3} INTER {3, 7, 10} SUBSET {10, 10000} UNION {3, 33} <=> T  *)
19 (* ------------------------------------------------------------------------- *)
20
21 (* ------------------------------------------------------------------------- *)
22 (* Constructors for the ntrie representation of a set of nums.               *)
23 (* ------------------------------------------------------------------------- *)
24
25 let NEMPTY = new_definition
26   `NEMPTY:num->bool = {}`;;
27
28 let NZERO = new_definition
29   `NZERO = {_0}`;;
30
31 let NNODE = new_definition
32   `!s t. NNODE s t = IMAGE BIT0 s UNION IMAGE BIT1 t`;;
33
34 let NTRIE = new_definition
35   `!s:num->bool. NTRIE s = s`;;
36
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]);;
43
44 (* ------------------------------------------------------------------------- *)
45 (* Membership.                                                               *)
46 (* ------------------------------------------------------------------------- *)
47
48 let NTRIE_IN = prove
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
57    MESON_TAC[]);;
58
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];;
62
63 (* ------------------------------------------------------------------------- *)
64 (* Inclusion.                                                                *)
65 (* ------------------------------------------------------------------------- *)
66
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) /\
75     (!s1 s2 t1 t2.
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
79    REPEAT STRIP_TAC THEN
80    REWRITE_TAC[SUBSET; NOT_IN_EMPTY; IN_INSERT; IN_UNION; IN_IMAGE;
81                ARITH_EQ] THENL
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[]);;
88
89 let NTRIE_SUBSET_CONV : conv =
90   let tth,pths = CONJ_PAIR NTRIE_SUBSET in
91   REWR_CONV tth THENC REWRITE_CONV[pths];;
92
93 (* ------------------------------------------------------------------------- *)
94 (* Equality.                                                                 *)
95 (* ------------------------------------------------------------------------- *)
96
97 let NTRIE_EQ = prove
98   (`(!s t. NTRIE s = NTRIE t <=> s = t) /\
99     (!s:num->bool. s = s) /\
100     ~(NZERO = NEMPTY) /\
101     ~(NEMPTY = NZERO) /\
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
108    SET_TAC[]);;
109
110 let NTRIE_EQ_CONV : conv =
111   let tth,pths = CONJ_PAIR NTRIE_EQ in
112   REWR_CONV tth THENC REWRITE_CONV[pths];;
113
114 (* ------------------------------------------------------------------------- *)
115 (* Singleton.                                                                *)
116 (* ------------------------------------------------------------------------- *)
117
118 let NTRIE_SING = prove
119   (`(!n. {NUMERAL n} = NTRIE {n}) /\
120     {_0} = NZERO /\
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;
124                UNION_EMPTY] THEN
125    GEN_TAC THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[ARITH_ZERO]);;
126
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]);;
130
131 (* ------------------------------------------------------------------------- *)
132 (* Insertion.                                                                *)
133 (* ------------------------------------------------------------------------- *)
134
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]);;
149
150 let NTRIE_INSERT_CONV : conv =
151   let tth,pths = CONJ_PAIR NTRIE_INSERT in
152   REWR_CONV tth THENC
153   RAND_CONV(REWRITE_CONV[pths; CONJUNCT2 NTRIE_SING; CONJUNCT2 ARITH_EQ]);;
154
155 (* ------------------------------------------------------------------------- *)
156 (* Union.                                                                    *)
157 (* ------------------------------------------------------------------------- *)
158
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]);;
172
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]);;
176
177 (* ------------------------------------------------------------------------- *)
178 (* Intersection.                                                             *)
179 (* Warning: rewriting with this theorem generates ntries which are not       *)
180 (* "minimal".  It has to be used in conjuction with NTRIE_RELATIONS.         *)
181 (* ------------------------------------------------------------------------- *)
182
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) /\
190     (!s1 s2 t1 t2.
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[];
196     COND_CASES_TAC THEN
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]]);;
202
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]);;
206
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 (* ------------------------------------------------------------------------- *)
212
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]);;
225
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]);;
229
230 (* ------------------------------------------------------------------------- *)
231 (* Disjoint.                                                                 *)
232 (* ------------------------------------------------------------------------- *)
233
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]);;
245
246 let NTRIE_DISJOINT_CONV : conv =
247   let tth,pths = CONJ_PAIR NTRIE_DISJOINT in
248   REWR_CONV tth THENC REWRITE_CONV[pths];;
249
250 (* ------------------------------------------------------------------------- *)
251 (* Difference.                                                               *)
252 (* ------------------------------------------------------------------------- *)
253
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]);;
267
268 let NTRIE_DIFF_CONV : conv =
269   let tth,pths = CONJ_PAIR NTRIE_DIFF in
270   REWR_CONV tth THENC REWRITE_CONV[pths];;
271
272 (* ------------------------------------------------------------------------- *)
273 (* Image.                                                                    *)
274 (* ------------------------------------------------------------------------- *)
275
276 let NTRIE_IMAGE_DEF = new_definition
277   `!f acc s. NTRIE_IMAGE f acc s = IMAGE f s UNION acc`;;
278
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)
285                              t)`,
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[]]);;
289
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]);;
293
294 let NTRIE_IMAGE_CONV : conv -> conv =
295   let [c1;c2;c3] = map REWR_CONV (CONJUNCTS NTRIE_IMAGE) in
296   fun cnv ->
297   let rec conv tm =
298     (c1 ORELSEC (c2 THENC LAND_CONV (TRY_CONV BETA_CONV THENC cnv)) ORELSEC
299      (c3 THENC
300       RATOR_CONV (ONCE_DEPTH_CONV BETA_CONV THENC RAND_CONV conv) THENC
301       conv)) tm in
302   REWR_CONV IMAGE_EQ_NTRIE_IMAGE THENC (ONCE_DEPTH_CONV BETA_CONV) THENC conv;;
303
304 (* ------------------------------------------------------------------------- *)
305 (* Decoding of a set in ntrie form to the usual literal representation.      *)
306 (* ------------------------------------------------------------------------- *)
307
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
312      SET_TAC[])
313   and [c1;c2;c3] = map REWR_CONV (CONJUNCTS NTRIE_IMAGE) in
314   let rec conv tm =
315     (c1 ORELSEC (c2 THENC LAND_CONV (TRY_CONV BETA_CONV)) ORELSEC
316      (c3 THENC
317       RATOR_CONV (ONCE_DEPTH_CONV BETA_CONV THENC RAND_CONV conv) THENC
318       conv)) tm in
319   REWR_CONV NTRIE_DECODE_THM THENC conv;;
320
321 (* ------------------------------------------------------------------------- *)
322 (* Encoding of a set from the usual literal form to the ntrie form.          *)
323 (* ------------------------------------------------------------------------- *)
324
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
329   and cnv2 cnv tm =
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
334   conv;;
335
336 (* ------------------------------------------------------------------------- *)
337 (* Final hack-together.                                                      *)
338 (* ------------------------------------------------------------------------- *)
339
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]
346     (basic_net()) in
347   REWRITES_CONV gconv_net;;
348
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]
360     (basic_net()) in
361   REWRITES_CONV gconv_net;;
362
363 let NTRIE_REDUCE_CONV = DEPTH_CONV NTRIE_RED_CONV;;
364
365 let NTRIE_REDUCE_TAC = CONV_TAC NTRIE_REDUCE_CONV;;
366
367 let NTRIE_COMPUTE (cnv : conv) : conv =
368   ONCE_DEPTH_CONV NTRIE_ENCODE_CONV THENC
369   cnv THENC
370   ONCE_DEPTH_CONV NTRIE_DECODE_CONV;;