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;;