(* ========================================================================= *)
(* Computations with finite sets of nums.                                    *)
(*                                                                           *)
(*        (c) Copyright, Clelia Lomuto, Marco Maggesi, 2009.                 *)
(*          Distributed with HOL Light under same license terms              *)
(* ========================================================================= *)

(* ------------------------------------------------------------------------- *)
(* This file defines some conversions that operate on finite sets of nums    *)
(* represented literally in a trie-like structure (we call them `ntries').   *)
(* ------------------------------------------------------------------------- *)

(* ------------------------------------------------------------------------- *)
(* Example:                                                                  *)
(* # NTRIE_COMPUTE NTRIE_REDUCE_CONV                                         *)
(*   `{10, 1001, 3} INTER {3, 7, 10} SUBSET {10, 10000} UNION {3, 33}`;;     *)
(* val it : thm =                                                            *)
(* |- {10, 1001, 3} INTER {3, 7, 10} SUBSET {10, 10000} UNION {3, 33} <=> T  *)
(* ------------------------------------------------------------------------- *)

(* ------------------------------------------------------------------------- *)
(* Constructors for the ntrie representation of a set of nums.               *)
(* ------------------------------------------------------------------------- *)

let NEMPTY = new_definition
  `NEMPTY:num->bool = {}`;;
let NZERO = new_definition
  `NZERO = {_0}`;;
let NNODE = new_definition
  `!s t. NNODE s t = IMAGE BIT0 s UNION IMAGE BIT1 t`;;
let NTRIE = new_definition
  `!s:num->bool. NTRIE s = s`;;
let NTRIE_RELATIONS = 
prove (`NNODE NEMPTY NEMPTY = NEMPTY /\ NNODE NZERO NEMPTY = NZERO`,
REWRITE_TAC[NEMPTY; NZERO; NNODE; EXTENSION; NOT_IN_EMPTY; IN_INSERT; IN_UNION; IN_IMAGE] THEN MESON_TAC[ARITH_EQ]);;
(* ------------------------------------------------------------------------- *) (* Membership. *) (* ------------------------------------------------------------------------- *)
let NTRIE_IN = 
prove (`(!s n. NUMERAL n IN NTRIE s <=> n IN s) /\ (!n. ~(n IN NEMPTY)) /\ (!n. n IN NZERO <=> n = _0) /\ (!s t. _0 IN NNODE s t <=> _0 IN s) /\ (!s t n. BIT0 n IN NNODE s t <=> n IN s) /\ (!s t n. BIT1 n IN NNODE s t <=> n IN t)`,
REWRITE_TAC[NUMERAL; NTRIE; NEMPTY; NZERO; NNODE; NOT_IN_EMPTY; IN_INSERT; IN_UNION; IN_IMAGE; ARITH_EQ] THEN MESON_TAC[]);;
let NTRIE_IN_CONV : conv = let tth,pths = CONJ_PAIR NTRIE_IN in REWR_CONV tth THENC REWRITE_CONV[pths; CONJUNCT2 ARITH_EQ];; (* ------------------------------------------------------------------------- *) (* Inclusion. *) (* ------------------------------------------------------------------------- *)
let NTRIE_SUBSET = 
prove (`(!s t. NTRIE s SUBSET NTRIE t <=> s SUBSET t) /\ (!s. NEMPTY SUBSET s) /\ (!s:num->bool. s SUBSET s) /\ ~(NZERO SUBSET NEMPTY) /\ (!s t. NNODE s t SUBSET NEMPTY <=> s SUBSET NEMPTY /\ t SUBSET NEMPTY) /\ (!s t. NNODE s t SUBSET NZERO <=> s SUBSET NZERO /\ t SUBSET NEMPTY) /\ (!s t. NZERO SUBSET NNODE s t <=> NZERO SUBSET s) /\ (!s1 s2 t1 t2. NNODE s1 t1 SUBSET NNODE s2 t2 <=> s1 SUBSET s2 /\ t1 SUBSET t2)`,
REWRITE_TAC[NTRIE; NEMPTY; NZERO; NNODE; EMPTY_SUBSET; SUBSET_REFL; SING_SUBSET; NOT_IN_EMPTY] THEN REPEAT STRIP_TAC THEN REWRITE_TAC[SUBSET; NOT_IN_EMPTY; IN_INSERT; IN_UNION; IN_IMAGE; ARITH_EQ] THENL [MESON_TAC[]; MESON_TAC[ARITH_EQ]; MESON_TAC[]; EQ_TAC] THENL [ALL_TAC; MESON_TAC[ARITH_EQ]] THEN STRIP_TAC THEN CONJ_TAC THEN GEN_TAC THENL [POP_ASSUM (MP_TAC o SPEC `BIT0 x`); POP_ASSUM (MP_TAC o SPEC `BIT1 x`)] THEN REWRITE_TAC[ARITH_EQ] THEN MESON_TAC[]);;
let NTRIE_SUBSET_CONV : conv = let tth,pths = CONJ_PAIR NTRIE_SUBSET in REWR_CONV tth THENC REWRITE_CONV[pths];; (* ------------------------------------------------------------------------- *) (* Equality. *) (* ------------------------------------------------------------------------- *)
let NTRIE_EQ = 
prove (`(!s t. NTRIE s = NTRIE t <=> s = t) /\ (!s:num->bool. s = s) /\ ~(NZERO = NEMPTY) /\ ~(NEMPTY = NZERO) /\ (!s t. NNODE s t = NEMPTY <=> s = NEMPTY /\ t = NEMPTY) /\ (!s t. NEMPTY = NNODE s t <=> s = NEMPTY /\ t = NEMPTY) /\ (!s t. NNODE s t = NZERO <=> s = NZERO /\ t = NEMPTY) /\ (!s t. NZERO = NNODE s t <=> s = NZERO /\ t = NEMPTY) /\ (!s1 s2 t1 t2. NNODE s1 t1 = NNODE s2 t2 <=> s1 = s2 /\ t1 = t2)`,
REWRITE_TAC[GSYM SUBSET_ANTISYM_EQ; NTRIE_SUBSET; NEMPTY; NZERO] THEN SET_TAC[]);;
let NTRIE_EQ_CONV : conv = let tth,pths = CONJ_PAIR NTRIE_EQ in REWR_CONV tth THENC REWRITE_CONV[pths];; (* ------------------------------------------------------------------------- *) (* Singleton. *) (* ------------------------------------------------------------------------- *)
let NTRIE_SING = 
prove (`(!n. {NUMERAL n} = NTRIE {n}) /\ {_0} = NZERO /\ (!n. {BIT0 n} = if n = _0 then NZERO else NNODE {n} NEMPTY) /\ (!n. {BIT1 n} = NNODE NEMPTY {n})`,
REWRITE_TAC[NUMERAL; NTRIE; NEMPTY; NZERO; NNODE; IMAGE_CLAUSES; UNION_EMPTY] THEN GEN_TAC THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[ARITH_ZERO]);;
let NTRIE_SING_CONV = let tth,pths = CONJ_PAIR NTRIE_SING in REWR_CONV tth THENC RAND_CONV(REWRITE_CONV[pths; CONJUNCT2 ARITH_EQ]);; (* ------------------------------------------------------------------------- *) (* Insertion. *) (* ------------------------------------------------------------------------- *)
let NTRIE_INSERT = 
prove (`(!s n. NUMERAL n INSERT NTRIE s = NTRIE (n INSERT s)) /\ (!n. n INSERT NEMPTY = {n}) /\ _0 INSERT NZERO = NZERO /\ (!s t n. _0 INSERT NNODE s t = NNODE (_0 INSERT s) t) /\ (!n. BIT0 n INSERT NZERO = if n = _0 then NZERO else NNODE (n INSERT NZERO) NEMPTY) /\ (!n. BIT1 n INSERT NZERO = NNODE NZERO {n}) /\ (!s t n. BIT0 n INSERT NNODE s t = NNODE (n INSERT s) t) /\ (!s t n. BIT1 n INSERT NNODE s t = NNODE s (n INSERT t))`,
REWRITE_TAC[NUMERAL; NTRIE; NEMPTY; NZERO; NNODE] THEN REPEAT STRIP_TAC THEN TRY COND_CASES_TAC THEN REWRITE_TAC[EXTENSION; IN_INSERT; NOT_IN_EMPTY; IN_UNION; IN_IMAGE] THEN ASM_MESON_TAC[ARITH_EQ]);;
let NTRIE_INSERT_CONV : conv = let tth,pths = CONJ_PAIR NTRIE_INSERT in REWR_CONV tth THENC RAND_CONV(REWRITE_CONV[pths; CONJUNCT2 NTRIE_SING; CONJUNCT2 ARITH_EQ]);; (* ------------------------------------------------------------------------- *) (* Union. *) (* ------------------------------------------------------------------------- *)
let NTRIE_UNION = 
prove (`(!s t. NTRIE s UNION NTRIE t = NTRIE (s UNION t)) /\ (!s. s UNION NEMPTY = s) /\ (!s. NEMPTY UNION s = s) /\ NZERO UNION NZERO = NZERO /\ (!s t. NNODE s t UNION NZERO = NNODE (s UNION NZERO) t) /\ (!s t. NZERO UNION NNODE s t = NNODE (s UNION NZERO) t) /\ (!s t r q. NNODE s t UNION NNODE r q = NNODE (s UNION r) (t UNION q))`,
REWRITE_TAC[NTRIE; NEMPTY; NZERO; NNODE] THEN REPEAT STRIP_TAC THEN TRY COND_CASES_TAC THEN REWRITE_TAC[UNION_EMPTY; INSERT_UNION; NOT_IN_EMPTY; IN_INSERT; IN_UNION; IN_IMAGE; EXTENSION] THEN MESON_TAC[ARITH_EQ]);;
let NTRIE_UNION_CONV : conv = let tth,pths = CONJ_PAIR NTRIE_UNION in REWR_CONV tth THENC RAND_CONV(REWRITE_CONV[pths]);; (* ------------------------------------------------------------------------- *) (* Intersection. *) (* Warning: rewriting with this theorem generates ntries which are not *) (* "minimal". It has to be used in conjuction with NTRIE_RELATIONS. *) (* ------------------------------------------------------------------------- *)
let NTRIE_INTER = 
prove (`(!s t. NTRIE s INTER NTRIE t = NTRIE (s INTER t)) /\ (!s. NEMPTY INTER s = NEMPTY) /\ (!s. s INTER NEMPTY = NEMPTY) /\ NZERO INTER NZERO = NZERO /\ (!s t. NZERO INTER NNODE s t = NZERO INTER s) /\ (!s t. NNODE s t INTER NZERO = NZERO INTER s) /\ (!s1 s2 t1 t2. NNODE s1 t1 INTER NNODE s2 t2 = NNODE (s1 INTER s2) (t1 INTER t2))`,
REWRITE_TAC[NTRIE; NEMPTY; NZERO; NNODE; INTER_EMPTY; INSERT_INTER; NOT_IN_EMPTY; IN_INSERT] THEN REPEAT STRIP_TAC THENL [REWRITE_TAC[IN_UNION; IN_IMAGE; ARITH_EQ] THEN ASM_MESON_TAC[]; COND_CASES_TAC THEN ASM_REWRITE_TAC[EXTENSION; IN_UNION; IN_INTER; IN_IMAGE; IN_INSERT; NOT_IN_EMPTY] THEN ASM_MESON_TAC[ARITH_EQ]; REWRITE_TAC[EXTENSION; IN_INTER; IN_UNION; IN_IMAGE] THEN MESON_TAC[ARITH_EQ]]);;
let NTRIE_INTER_CONV : conv = let tth,pths = CONJ_PAIR NTRIE_INTER in REWR_CONV tth THENC RAND_CONV(REWRITE_CONV[pths; NTRIE_RELATIONS]);; (* ------------------------------------------------------------------------- *) (* Deleting an element. *) (* Warning: rewriting with this theorem generates ntries which are not *) (* "minimal". It has to be used in conjuction with NTRIE_RELATIONS. *) (* ------------------------------------------------------------------------- *)
let NTRIE_DELETE = 
prove (`(!s n. NTRIE s DELETE NUMERAL n = NTRIE (s DELETE n)) /\ (!n. NEMPTY DELETE n = NEMPTY) /\ (!n. NZERO DELETE n = if n = _0 then NEMPTY else NZERO) /\ (!s t. NNODE s t DELETE _0 = NNODE (s DELETE _0) t) /\ (!s t n. NNODE s t DELETE BIT0 n = NNODE (s DELETE n) t) /\ (!s t n. NNODE s t DELETE BIT1 n = NNODE s (t DELETE n))`,
REWRITE_TAC[NUMERAL; NTRIE; NEMPTY; NZERO; NNODE] THEN REPEAT STRIP_TAC THEN TRY COND_CASES_TAC THEN ASM_REWRITE_TAC[EXTENSION; IN_DELETE; IN_UNION; IN_IMAGE; NOT_IN_EMPTY; IN_INSERT] THEN ASM_MESON_TAC[ARITH_EQ]);;
let NTRIE_DELETE_CONV : conv = let tth,pths = CONJ_PAIR NTRIE_DELETE in REWR_CONV tth THENC RAND_CONV(REWRITE_CONV[pths; NTRIE_RELATIONS]);; (* ------------------------------------------------------------------------- *) (* Disjoint. *) (* ------------------------------------------------------------------------- *)
let NTRIE_DISJOINT = 
prove (`(!s t. DISJOINT (NTRIE s) (NTRIE t) <=> DISJOINT s t) /\ (!s. DISJOINT s NEMPTY) /\ (!s. DISJOINT NEMPTY s) /\ ~DISJOINT NZERO NZERO /\ (!s t. DISJOINT NZERO (NNODE s t) <=> DISJOINT s NZERO) /\ (!s t. DISJOINT (NNODE s t) NZERO <=> DISJOINT s NZERO) /\ (!s1 s2 t1 t2. DISJOINT (NNODE s1 t1) (NNODE s2 t2) <=> DISJOINT s1 s2 /\ DISJOINT t1 t2)`,
REWRITE_TAC[NTRIE; DISJOINT; GSYM NEMPTY; NTRIE_INTER; INTER_ACI; NTRIE_EQ]);;
let NTRIE_DISJOINT_CONV : conv = let tth,pths = CONJ_PAIR NTRIE_DISJOINT in REWR_CONV tth THENC REWRITE_CONV[pths];; (* ------------------------------------------------------------------------- *) (* Difference. *) (* ------------------------------------------------------------------------- *)
let NTRIE_DIFF = 
prove (`(!s t. NTRIE s DIFF NTRIE t = NTRIE (s DIFF t)) /\ (!s. NEMPTY DIFF s = NEMPTY) /\ (!s. s DIFF NEMPTY = s) /\ NZERO DIFF NZERO = NEMPTY /\ (!s t. NZERO DIFF NNODE s t = NZERO DIFF s) /\ (!s t. NNODE s t DIFF NZERO = NNODE (s DIFF NZERO) t) /\ (!s1 t1 s2 t2. NNODE s1 t1 DIFF NNODE s2 t2 = NNODE (s1 DIFF s2) (t1 DIFF t2))`,
let NTRIE_DIFF_CONV : conv = let tth,pths = CONJ_PAIR NTRIE_DIFF in REWR_CONV tth THENC REWRITE_CONV[pths];; (* ------------------------------------------------------------------------- *) (* Image. *) (* ------------------------------------------------------------------------- *)
let NTRIE_IMAGE_DEF = new_definition
  `!f acc s. NTRIE_IMAGE f acc s = IMAGE f s UNION acc`;;
let NTRIE_IMAGE = 
prove (`(!f acc. NTRIE_IMAGE f acc NEMPTY = acc) /\ (!f acc. NTRIE_IMAGE f acc NZERO = f _0 INSERT acc) /\ (!f acc s t. NTRIE_IMAGE f acc (NNODE s t) = NTRIE_IMAGE (\n. f (BIT1 n)) (NTRIE_IMAGE (\n. f (BIT0 n)) acc s) t)`,
REWRITE_TAC[NEMPTY; NZERO; NNODE; NTRIE_IMAGE_DEF; GSYM IMAGE_o; o_DEF; IMAGE_UNION; IMAGE_CLAUSES; UNION_EMPTY; INSERT_UNION] THEN REPEAT STRIP_TAC THENL [COND_CASES_TAC THEN ASM SET_TAC[]; SET_TAC[]]);;
let IMAGE_EQ_NTRIE_IMAGE = 
prove (`!f s. IMAGE f (NTRIE s) = NTRIE_IMAGE (\n. f (NUMERAL n)) {} s`,
REWRITE_TAC [NUMERAL; NTRIE; ETA_AX; NTRIE_IMAGE_DEF; UNION_EMPTY]);;
let NTRIE_IMAGE_CONV : conv -> conv = let [c1;c2;c3] = map REWR_CONV (CONJUNCTS NTRIE_IMAGE) in fun cnv -> let rec conv tm = (c1 ORELSEC (c2 THENC LAND_CONV (TRY_CONV BETA_CONV THENC cnv)) ORELSEC (c3 THENC RATOR_CONV (ONCE_DEPTH_CONV BETA_CONV THENC RAND_CONV conv) THENC conv)) tm in REWR_CONV IMAGE_EQ_NTRIE_IMAGE THENC (ONCE_DEPTH_CONV BETA_CONV) THENC conv;; (* ------------------------------------------------------------------------- *) (* Decoding of a set in ntrie form to the usual literal representation. *) (* ------------------------------------------------------------------------- *) let NTRIE_DECODE_CONV : conv =
let NTRIE_DECODE_THM = 
prove (`!s. NTRIE s = NTRIE_IMAGE NUMERAL {} s`,
REWRITE_TAC[NTRIE; NUMERAL; NTRIE_IMAGE_DEF; UNION_EMPTY; IMAGE] THEN SET_TAC[]) and [c1;c2;c3] = map REWR_CONV (CONJUNCTS NTRIE_IMAGE) in let rec conv tm = (c1 ORELSEC (c2 THENC LAND_CONV (TRY_CONV BETA_CONV)) ORELSEC (c3 THENC RATOR_CONV (ONCE_DEPTH_CONV BETA_CONV THENC RAND_CONV conv) THENC conv)) tm in REWR_CONV NTRIE_DECODE_THM THENC conv;;
(* ------------------------------------------------------------------------- *) (* Encoding of a set from the usual literal form to the ntrie form. *) (* ------------------------------------------------------------------------- *) let NTRIE_ENCODE_CONV : conv= let itm = `(INSERT):num->(num->bool)->num->bool` and th = prove (`{} = NTRIE NEMPTY`, REWRITE_TAC[NTRIE; NEMPTY]) in let cnv1 = REWR_CONV th and cnv2 cnv tm = let fn,arg = dest_comb tm in if rator fn <> itm then fail () else AP_TERM fn (cnv arg) in let rec conv tm = (cnv1 ORELSEC (cnv2 conv THENC NTRIE_INSERT_CONV)) tm in conv;; (* ------------------------------------------------------------------------- *) (* Final hack-together. *) (* ------------------------------------------------------------------------- *) let NTRIE_REL_CONV : conv = let gconv_net = itlist (uncurry net_of_conv) [`NTRIE s = NTRIE t`, NTRIE_EQ_CONV; `NTRIE s SUBSET NTRIE t`, NTRIE_SUBSET_CONV; `DISJOINT (NTRIE s) (NTRIE t)`, NTRIE_DISJOINT_CONV; `NUMERA n IN NTRIE s`, NTRIE_IN_CONV] (basic_net()) in REWRITES_CONV gconv_net;; let NTRIE_RED_CONV : conv = let gconv_net = itlist (uncurry net_of_conv) [`NTRIE s = NTRIE t`, NTRIE_EQ_CONV; `NTRIE s SUBSET NTRIE t`, NTRIE_SUBSET_CONV; `DISJOINT (NTRIE s) (NTRIE t)`, NTRIE_DISJOINT_CONV; `NUMERA n IN NTRIE s`, NTRIE_IN_CONV; `NUMERAL n INSERT NTRIE s`, NTRIE_INSERT_CONV; `NTRIE s UNION NTRIE t`, NTRIE_UNION_CONV; `NTRIE s INTER NTRIE t`, NTRIE_INTER_CONV; `NTRIE s DELETE NUMERAL n`, NTRIE_DELETE_CONV; `NTRIE s DIFF NTRIE t`, NTRIE_DIFF_CONV] (basic_net()) in REWRITES_CONV gconv_net;; let NTRIE_REDUCE_CONV = DEPTH_CONV NTRIE_RED_CONV;; let NTRIE_REDUCE_TAC = CONV_TAC NTRIE_REDUCE_CONV;; let NTRIE_COMPUTE (cnv : conv) : conv = ONCE_DEPTH_CONV NTRIE_ENCODE_CONV THENC cnv THENC ONCE_DEPTH_CONV NTRIE_DECODE_CONV;;